src/CCL/Type.thy
changeset 32153 a0e57fb1b930
parent 32149 ef59550a55d3
child 35054 a5db9779b026
--- a/src/CCL/Type.thy	Thu Jul 23 20:05:20 2009 +0200
+++ b/src/CCL/Type.thy	Thu Jul 23 21:59:56 2009 +0200
@@ -123,39 +123,36 @@
 
 
 ML {*
-local
-  val lemma = thm "lem"
-  val bspec = thm "bspec"
-  val bexE = thm "bexE"
-in
-
-  fun mk_ncanT_tac ctxt defs top_crls crls s = prove_goalw (ProofContext.theory_of ctxt) defs s
-    (fn major::prems => [(resolve_tac ([major] RL top_crls) 1),
-                         (REPEAT_SOME (eresolve_tac (crls @ [exE,bexE,conjE,disjE]))),
-                         (ALLGOALS (asm_simp_tac (simpset_of ctxt))),
-                         (ALLGOALS (ares_tac (prems RL [lemma]) ORELSE'
-                                    etac bspec )),
-                         (safe_tac (claset_of ctxt addSIs prems))])
-end
+fun mk_ncanT_tac top_crls crls =
+  SUBPROOF (fn {context = ctxt, prems = major :: prems, ...} =>
+    resolve_tac ([major] RL top_crls) 1 THEN
+    REPEAT_SOME (eresolve_tac (crls @ [exE, @{thm bexE}, conjE, disjE])) THEN
+    ALLGOALS (asm_simp_tac (simpset_of ctxt)) THEN
+    ALLGOALS (ares_tac (prems RL [@{thm lem}]) ORELSE' etac @{thm bspec}) THEN
+    safe_tac (claset_of ctxt addSIs prems))
 *}
 
-ML {*
-  val ncanT_tac = mk_ncanT_tac @{context} [] @{thms case_rls} @{thms case_rls}
-*}
+method_setup ncanT = {*
+  Scan.succeed (SIMPLE_METHOD' o mk_ncanT_tac @{thms case_rls} @{thms case_rls})
+*} ""
 
-ML {*
-
-bind_thm ("ifT", ncanT_tac
-  "[| b:Bool; b=true ==> t:A(true); b=false ==> u:A(false) |] ==> if b then t else u : A(b)");
+lemma ifT:
+  "[| b:Bool; b=true ==> t:A(true); b=false ==> u:A(false) |] ==>
+    if b then t else u : A(b)"
+  by ncanT
 
-bind_thm ("applyT", ncanT_tac "[| f : Pi(A,B);  a:A |] ==> f ` a : B(a)");
+lemma applyT: "[| f : Pi(A,B);  a:A |] ==> f ` a : B(a)"
+  by ncanT
 
-bind_thm ("splitT", ncanT_tac
-  "[| p:Sigma(A,B); !!x y. [| x:A;  y:B(x); p=<x,y> |] ==> c(x,y):C(<x,y>) |] ==> split(p,c):C(p)");
+lemma splitT:
+  "[| p:Sigma(A,B); !!x y. [| x:A;  y:B(x); p=<x,y> |] ==> c(x,y):C(<x,y>) |]
+    ==> split(p,c):C(p)"
+  by ncanT
 
-bind_thm ("whenT", ncanT_tac
-  "[| p:A+B; !!x.[| x:A;  p=inl(x) |] ==> a(x):C(inl(x)); !!y.[| y:B;  p=inr(y) |] ==> b(y):C(inr(y)) |] ==> when(p,a,b) : C(p)");
-*}
+lemma whenT:
+  "[| p:A+B; !!x.[| x:A;  p=inl(x) |] ==> a(x):C(inl(x)); !!y.[| y:B;  p=inr(y) |]
+    ==> b(y):C(inr(y)) |] ==> when(p,a,b) : C(p)"
+  by ncanT
 
 lemmas ncanTs = ifT applyT splitT whenT
 
@@ -275,17 +272,20 @@
 
 lemmas icanTs = zeroT succT nilT consT
 
-ML {*
-val incanT_tac = mk_ncanT_tac @{context} [] @{thms icase_rls} @{thms case_rls};
-*}
+
+method_setup incanT = {*
+  Scan.succeed (SIMPLE_METHOD' o mk_ncanT_tac @{thms icase_rls} @{thms case_rls})
+*} ""
 
-ML {*
-bind_thm ("ncaseT", incanT_tac
-  "[| n:Nat; n=zero ==> b:C(zero); !!x.[| x:Nat;  n=succ(x) |] ==> c(x):C(succ(x)) |] ==> ncase(n,b,c) : C(n)");
+lemma ncaseT:
+  "[| n:Nat; n=zero ==> b:C(zero); !!x.[| x:Nat;  n=succ(x) |] ==> c(x):C(succ(x)) |]
+    ==> ncase(n,b,c) : C(n)"
+  by incanT
 
-bind_thm ("lcaseT", incanT_tac
-     "[| l:List(A); l=[] ==> b:C([]); !!h t.[| h:A;  t:List(A); l=h$t |] ==> c(h,t):C(h$t) |] ==> lcase(l,b,c) : C(l)");
-*}
+lemma lcaseT:
+  "[| l:List(A); l=[] ==> b:C([]); !!h t.[| h:A;  t:List(A); l=h$t |] ==>
+    c(h,t):C(h$t) |] ==> lcase(l,b,c) : C(l)"
+  by incanT
 
 lemmas incanTs = ncaseT lcaseT
 
@@ -337,7 +337,7 @@
 (*         - intro rules are type rules for canonical terms                *)
 (*         - elim rules are case rules (no non-canonical terms appear)     *)
 
-ML {* bind_thms ("XHEs", XH_to_Es (thms "XHs")) *}
+ML {* bind_thms ("XHEs", XH_to_Es @{thms XHs}) *}
 
 lemmas [intro!] = SubtypeI canTs icanTs
   and [elim!] = SubtypeE XHEs
@@ -392,88 +392,103 @@
   by simp
 
 
-(***)
+ML {*
+  val coinduct3_tac = SUBPROOF (fn {context = ctxt, prems = mono :: prems, ...} =>
+    (fast_tac (claset_of ctxt addIs
+        (mono RS @{thm coinduct3_mono_lemma} RS @{thm lfpI}) :: prems) 1));
+*}
+
+method_setup coinduct3 = {*
+  Scan.succeed (SIMPLE_METHOD' o coinduct3_tac)
+*} ""
+
+lemma ci3_RI: "[| mono(Agen);  a : R |] ==> a : lfp(%x. Agen(x) Un R Un A)"
+  by coinduct3
+
+lemma ci3_AgenI: "[| mono(Agen);  a : Agen(lfp(%x. Agen(x) Un R Un A)) |] ==>
+    a : lfp(%x. Agen(x) Un R Un A)"
+  by coinduct3
+
+lemma ci3_AI: "[| mono(Agen);  a : A |] ==> a : lfp(%x. Agen(x) Un R Un A)"
+  by coinduct3
 
 ML {*
-
-local
-  val lfpI = thm "lfpI"
-  val coinduct3_mono_lemma = thm "coinduct3_mono_lemma"
-  fun mk_thm s = prove_goal (the_context ()) s (fn mono::prems =>
-       [fast_tac (@{claset} addIs ((mono RS coinduct3_mono_lemma RS lfpI)::prems)) 1])
-in
-val ci3_RI    = mk_thm "[|  mono(Agen);  a : R |] ==> a : lfp(%x. Agen(x) Un R Un A)"
-val ci3_AgenI = mk_thm "[|  mono(Agen);  a : Agen(lfp(%x. Agen(x) Un R Un A)) |] ==> a : lfp(%x. Agen(x) Un R Un A)"
-val ci3_AI    = mk_thm "[|  mono(Agen);  a : A |] ==> a : lfp(%x. Agen(x) Un R Un A)"
+fun genIs_tac ctxt genXH gen_mono =
+  rtac (genXH RS iffD2) THEN'
+  simp_tac (simpset_of ctxt) THEN'
+  TRY o fast_tac (claset_of ctxt addIs
+        [genXH RS iffD2, gen_mono RS @{thm coinduct3_mono_lemma} RS @{thm lfpI}])
+*}
 
-fun mk_genIs thy defs genXH gen_mono s = prove_goalw thy defs s
-      (fn prems => [rtac (genXH RS iffD2) 1,
-                    simp_tac (global_simpset_of thy) 1,
-                    TRY (fast_tac (@{claset} addIs
-                            ([genXH RS iffD2,gen_mono RS coinduct3_mono_lemma RS lfpI]
-                             @ prems)) 1)])
-end;
-
-bind_thm ("ci3_RI", ci3_RI);
-bind_thm ("ci3_AgenI", ci3_AgenI);
-bind_thm ("ci3_AI", ci3_AI);
-*}
+method_setup genIs = {*
+  Attrib.thm -- Attrib.thm >> (fn (genXH, gen_mono) => fn ctxt =>
+    SIMPLE_METHOD' (genIs_tac ctxt genXH gen_mono))
+*} ""
 
 
 subsection {* POgen *}
 
 lemma PO_refl: "<a,a> : PO"
-  apply (rule po_refl [THEN PO_iff [THEN iffD1]])
-  done
+  by (rule po_refl [THEN PO_iff [THEN iffD1]])
+
+lemma POgenIs:
+  "<true,true> : POgen(R)"
+  "<false,false> : POgen(R)"
+  "[| <a,a'> : R;  <b,b'> : R |] ==> <<a,b>,<a',b'>> : POgen(R)"
+  "!!b b'. [|!!x. <b(x),b'(x)> : R |] ==><lam x. b(x),lam x. b'(x)> : POgen(R)"
+  "<one,one> : POgen(R)"
+  "<a,a'> : lfp(%x. POgen(x) Un R Un PO) ==>
+    <inl(a),inl(a')> : POgen(lfp(%x. POgen(x) Un R Un PO))"
+  "<b,b'> : lfp(%x. POgen(x) Un R Un PO) ==>
+    <inr(b),inr(b')> : POgen(lfp(%x. POgen(x) Un R Un PO))"
+  "<zero,zero> : POgen(lfp(%x. POgen(x) Un R Un PO))"
+  "<n,n'> : lfp(%x. POgen(x) Un R Un PO) ==>
+    <succ(n),succ(n')> : POgen(lfp(%x. POgen(x) Un R Un PO))"
+  "<[],[]> : POgen(lfp(%x. POgen(x) Un R Un PO))"
+  "[| <h,h'> : lfp(%x. POgen(x) Un R Un PO);  <t,t'> : lfp(%x. POgen(x) Un R Un PO) |]
+    ==> <h$t,h'$t'> : POgen(lfp(%x. POgen(x) Un R Un PO))"
+  unfolding data_defs by (genIs POgenXH POgen_mono)+
 
 ML {*
-
-val POgenIs = map (mk_genIs @{theory} @{thms data_defs} @{thm POgenXH} @{thm POgen_mono})
-  ["<true,true> : POgen(R)",
-   "<false,false> : POgen(R)",
-   "[| <a,a'> : R;  <b,b'> : R |] ==> <<a,b>,<a',b'>> : POgen(R)",
-   "[|!!x. <b(x),b'(x)> : R |] ==><lam x. b(x),lam x. b'(x)> : POgen(R)",
-   "<one,one> : POgen(R)",
-   "<a,a'> : lfp(%x. POgen(x) Un R Un PO) ==> <inl(a),inl(a')> : POgen(lfp(%x. POgen(x) Un R Un PO))",
-   "<b,b'> : lfp(%x. POgen(x) Un R Un PO) ==> <inr(b),inr(b')> : POgen(lfp(%x. POgen(x) Un R Un PO))",
-   "<zero,zero> : POgen(lfp(%x. POgen(x) Un R Un PO))",
-   "<n,n'> : lfp(%x. POgen(x) Un R Un PO) ==> <succ(n),succ(n')> : POgen(lfp(%x. POgen(x) Un R Un PO))",
-   "<[],[]> : POgen(lfp(%x. POgen(x) Un R Un PO))",
-   "[| <h,h'> : lfp(%x. POgen(x) Un R Un PO);  <t,t'> : lfp(%x. POgen(x) Un R Un PO) |] ==> <h$t,h'$t'> : POgen(lfp(%x. POgen(x) Un R Un PO))"];
-
-fun POgen_tac ctxt (rla,rlb) i =
+fun POgen_tac ctxt (rla, rlb) i =
   SELECT_GOAL (safe_tac (claset_of ctxt)) i THEN
   rtac (rlb RS (rla RS @{thm ssubst_pair})) i THEN
-  (REPEAT (resolve_tac (POgenIs @ [@{thm PO_refl} RS (@{thm POgen_mono} RS ci3_AI)] @
-    (POgenIs RL [@{thm POgen_mono} RS ci3_AgenI]) @ [@{thm POgen_mono} RS ci3_RI]) i));
-
+  (REPEAT (resolve_tac
+      (@{thms POgenIs} @ [@{thm PO_refl} RS (@{thm POgen_mono} RS @{thm ci3_AI})] @
+        (@{thms POgenIs} RL [@{thm POgen_mono} RS @{thm ci3_AgenI}]) @
+        [@{thm POgen_mono} RS @{thm ci3_RI}]) i))
 *}
 
 
 subsection {* EQgen *}
 
 lemma EQ_refl: "<a,a> : EQ"
-  apply (rule refl [THEN EQ_iff [THEN iffD1]])
-  done
+  by (rule refl [THEN EQ_iff [THEN iffD1]])
+
+lemma EQgenIs:
+  "<true,true> : EQgen(R)"
+  "<false,false> : EQgen(R)"
+  "[| <a,a'> : R;  <b,b'> : R |] ==> <<a,b>,<a',b'>> : EQgen(R)"
+  "!!b b'. [|!!x. <b(x),b'(x)> : R |] ==> <lam x. b(x),lam x. b'(x)> : EQgen(R)"
+  "<one,one> : EQgen(R)"
+  "<a,a'> : lfp(%x. EQgen(x) Un R Un EQ) ==>
+    <inl(a),inl(a')> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))"
+  "<b,b'> : lfp(%x. EQgen(x) Un R Un EQ) ==>
+    <inr(b),inr(b')> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))"
+  "<zero,zero> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))"
+  "<n,n'> : lfp(%x. EQgen(x) Un R Un EQ) ==>
+    <succ(n),succ(n')> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))"
+  "<[],[]> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))"
+  "[| <h,h'> : lfp(%x. EQgen(x) Un R Un EQ); <t,t'> : lfp(%x. EQgen(x) Un R Un EQ) |]
+    ==> <h$t,h'$t'> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))"
+  unfolding data_defs by (genIs EQgenXH EQgen_mono)+
 
 ML {*
-
-val EQgenIs = map (mk_genIs @{theory} @{thms data_defs} @{thm EQgenXH} @{thm EQgen_mono})
-  ["<true,true> : EQgen(R)",
-   "<false,false> : EQgen(R)",
-   "[| <a,a'> : R;  <b,b'> : R |] ==> <<a,b>,<a',b'>> : EQgen(R)",
-   "[|!!x. <b(x),b'(x)> : R |] ==> <lam x. b(x),lam x. b'(x)> : EQgen(R)",
-   "<one,one> : EQgen(R)",
-   "<a,a'> : lfp(%x. EQgen(x) Un R Un EQ) ==> <inl(a),inl(a')> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))",
-   "<b,b'> : lfp(%x. EQgen(x) Un R Un EQ) ==> <inr(b),inr(b')> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))",
-   "<zero,zero> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))",
-   "<n,n'> : lfp(%x. EQgen(x) Un R Un EQ) ==> <succ(n),succ(n')> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))",
-   "<[],[]> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))",
-   "[| <h,h'> : lfp(%x. EQgen(x) Un R Un EQ); <t,t'> : lfp(%x. EQgen(x) Un R Un EQ) |] ==> <h$t,h'$t'> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))"];
-
 fun EQgen_raw_tac i =
-  (REPEAT (resolve_tac (EQgenIs @ [@{thm EQ_refl} RS (@{thm EQgen_mono} RS ci3_AI)] @
-    (EQgenIs RL [@{thm EQgen_mono} RS ci3_AgenI]) @ [@{thm EQgen_mono} RS ci3_RI]) i))
+  (REPEAT (resolve_tac (@{thms EQgenIs} @
+        [@{thm EQ_refl} RS (@{thm EQgen_mono} RS @{thm ci3_AI})] @
+        (@{thms EQgenIs} RL [@{thm EQgen_mono} RS @{thm ci3_AgenI}]) @
+        [@{thm EQgen_mono} RS @{thm ci3_RI}]) i))
 
 (* Goals of the form R <= EQgen(R) - rewrite elements <a,b> : EQgen(R) using rews and *)
 (* then reduce this to a goal <a',b'> : R (hopefully?)                                *)
@@ -482,7 +497,7 @@
 fun EQgen_tac ctxt rews i =
  SELECT_GOAL
    (TRY (safe_tac (claset_of ctxt)) THEN
-    resolve_tac ((rews@[refl]) RL ((rews@[refl]) RL [@{thm ssubst_pair}])) i THEN
+    resolve_tac ((rews @ [refl]) RL ((rews @ [refl]) RL [@{thm ssubst_pair}])) i THEN
     ALLGOALS (simp_tac (simpset_of ctxt)) THEN
     ALLGOALS EQgen_raw_tac) i
 *}