adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

trivial: autocorres: fix simpl_conv diagnostic

This commit is contained in:
Japheth Lim 2016-05-27 11:37:45 +10:00
parent 4ec1820f0e
commit 77429f19ec
1 changed files with 5 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
tools/autocorres/simpl_conv.ML
View File

@ -360,10 +360,11 @@ in
mk_L1corres_call_prop ctxt prog_info fn_info check_termination fn_name monad
|> Thm.cterm_of ctxt
|> Goal.init
|> apply_tac "unfold SIMPL body"
(case impl_thm of
NONE => (resolve_tac ctxt @{thms L1corres_undefined_call} 1)
| SOME thm => ((resolve_tac ctxt @{thms L1corres_Call} 1) THEN (resolve_tac ctxt [thm] 1) THEN tactic))
|> (case impl_thm of
NONE => apply_tac "unfold SIMPL body" (resolve_tac ctxt @{thms L1corres_undefined_call} 1)
| SOME def => apply_tac "unfold SIMPL body" (resolve_tac ctxt @{thms L1corres_Call} 1 THEN
resolve_tac ctxt [def] 1)
#> apply_tac "solve L1corres" tactic)
|> Goal.finish ctxt
(* Apply simplifications to the L1 term. *)
|> cleanup_thm ctxt do_opt trace_opt prog_info fn_name