src/CCL/Hered.thy
changeset 32153 a0e57fb1b930
parent 32010 cb1a1c94b4cd
child 32154 9721e8e4d48c
--- a/src/CCL/Hered.thy	Thu Jul 23 20:05:20 2009 +0200
+++ b/src/CCL/Hered.thy	Thu Jul 23 21:59:56 2009 +0200
@@ -110,23 +110,22 @@
 
 fun HTT_coinduct3_tac ctxt s i =
   res_inst_tac ctxt [(("R", 0), s)] @{thm HTT_coinduct3} i
-
-val HTTgenIs =
-  map (mk_genIs @{theory} @{thms data_defs} @{thm HTTgenXH} @{thm HTTgen_mono})
-  ["true : HTTgen(R)",
-   "false : HTTgen(R)",
-   "[| a : R;  b : R |] ==> <a,b> : HTTgen(R)",
-   "[| !!x. b(x) : R |] ==> lam x. b(x) : HTTgen(R)",
-   "one : HTTgen(R)",
-   "a : lfp(%x. HTTgen(x) Un R Un HTT) ==> inl(a) : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))",
-   "b : lfp(%x. HTTgen(x) Un R Un HTT) ==> inr(b) : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))",
-   "zero : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))",
-   "n : lfp(%x. HTTgen(x) Un R Un HTT) ==> succ(n) : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))",
-   "[] : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))",
-   "[| h : lfp(%x. HTTgen(x) Un R Un HTT); t : lfp(%x. HTTgen(x) Un R Un HTT) |] ==> h$t : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))"]
 *}
 
-ML {* bind_thms ("HTTgenIs", HTTgenIs) *}
+lemma HTTgenIs:
+  "true : HTTgen(R)"
+  "false : HTTgen(R)"
+  "[| a : R;  b : R |] ==> <a,b> : HTTgen(R)"
+  "!!b. [| !!x. b(x) : R |] ==> lam x. b(x) : HTTgen(R)"
+  "one : HTTgen(R)"
+  "a : lfp(%x. HTTgen(x) Un R Un HTT) ==> inl(a) : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))"
+  "b : lfp(%x. HTTgen(x) Un R Un HTT) ==> inr(b) : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))"
+  "zero : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))"
+  "n : lfp(%x. HTTgen(x) Un R Un HTT) ==> succ(n) : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))"
+  "[] : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))"
+  "[| h : lfp(%x. HTTgen(x) Un R Un HTT); t : lfp(%x. HTTgen(x) Un R Un HTT) |] ==>
+    h$t : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))"
+  unfolding data_defs by (genIs HTTgenXH HTTgen_mono)+
 
 
 subsection {* Formation Rules for Types *}