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

WIP: autocorres: parallelise ac_corres; add mono theorems to theory

This commit is contained in:
Japheth Lim 2016-06-29 23:44:35 +10:00
parent e238064215
commit 3ade9cb717
1 changed files with 4 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
tools/autocorres/autocorres.ML
View File

@ -675,13 +675,14 @@ let
Utils.define_lemma (make_function_name f ^ "_ac_corres") thm #> snd)
ac_corres_thms lthy
(* Name final mono theorems. *)
(* Name final mono theorems and add them to the simpset. *)
val lthy =
fold (fn (f, info) => fn lthy =>
case #mono_thm info of
NONE => lthy
| SOME thm =>
Utils.define_lemma (make_function_name f ^ "_mono") thm lthy |> snd)
| SOME mono_thm =>
Utils.define_lemma (make_function_name f ^ "_mono") mono_thm lthy |> snd
|> Utils.simp_add [mono_thm])
(Symtab.dest ts_info) lthy
(* Save function info for future reference. *)