equal
deleted
inserted
replaced
21 val quiet_mode = Unsynchronized.ref false; |
21 val quiet_mode = Unsynchronized.ref false; |
22 val trace_domain = Unsynchronized.ref false; |
22 val trace_domain = Unsynchronized.ref false; |
23 |
23 |
24 fun message s = if !quiet_mode then () else writeln s; |
24 fun message s = if !quiet_mode then () else writeln s; |
25 fun trace s = if !trace_domain then tracing s else (); |
25 fun trace s = if !trace_domain then tracing s else (); |
26 |
|
27 local |
|
28 |
26 |
29 val adm_impl_admw = @{thm adm_impl_admw}; |
27 val adm_impl_admw = @{thm adm_impl_admw}; |
30 val adm_all = @{thm adm_all}; |
28 val adm_all = @{thm adm_all}; |
31 val adm_conj = @{thm adm_conj}; |
29 val adm_conj = @{thm adm_conj}; |
32 val adm_subst = @{thm adm_subst}; |
30 val adm_subst = @{thm adm_subst}; |
131 (* ----- general proofs ----------------------------------------------------- *) |
129 (* ----- general proofs ----------------------------------------------------- *) |
132 |
130 |
133 val all2E = @{lemma "!x y . P x y ==> (P x y ==> R) ==> R" by simp} |
131 val all2E = @{lemma "!x y . P x y ==> (P x y ==> R) ==> R" by simp} |
134 |
132 |
135 val dist_eqI = @{lemma "!!x::'a::po. ~ x << y ==> x ~= y" by (blast dest!: below_antisym_inverse)} |
133 val dist_eqI = @{lemma "!!x::'a::po. ~ x << y ==> x ~= y" by (blast dest!: below_antisym_inverse)} |
136 |
|
137 in |
|
138 |
134 |
139 fun theorems (((dname, _), cons) : eq, eqs : eq list) thy = |
135 fun theorems (((dname, _), cons) : eq, eqs : eq list) thy = |
140 let |
136 let |
141 |
137 |
142 val _ = message ("Proving isomorphism properties of domain "^dname^" ..."); |
138 val _ = message ("Proving isomorphism properties of domain "^dname^" ..."); |
1087 ((Binding.name "coind" , [coind] ), [])] |
1083 ((Binding.name "coind" , [coind] ), [])] |
1088 |> (if induct_failed then I |
1084 |> (if induct_failed then I |
1089 else snd o PureThy.add_thmss (map ind_rule (dnames ~~ inducts))) |
1085 else snd o PureThy.add_thmss (map ind_rule (dnames ~~ inducts))) |
1090 |> Sign.parent_path |> pair take_rews |
1086 |> Sign.parent_path |> pair take_rews |
1091 end; (* let *) |
1087 end; (* let *) |
1092 end; (* local *) |
|
1093 end; (* struct *) |
1088 end; (* struct *) |