diff -r 53716a67c3b1 -r a0e57fb1b930 src/CCL/Type.thy --- 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= |] ==> c(x,y):C() |] ==> split(p,c):C(p)"); +lemma splitT: + "[| p:Sigma(A,B); !!x y. [| x:A; y:B(x); p= |] ==> c(x,y):C() |] + ==> 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: " : PO" - apply (rule po_refl [THEN PO_iff [THEN iffD1]]) - done + by (rule po_refl [THEN PO_iff [THEN iffD1]]) + +lemma POgenIs: + " : POgen(R)" + " : POgen(R)" + "[| : R; : R |] ==> <,> : POgen(R)" + "!!b b'. [|!!x. : R |] ==> : POgen(R)" + " : POgen(R)" + " : lfp(%x. POgen(x) Un R Un PO) ==> + : POgen(lfp(%x. POgen(x) Un R Un PO))" + " : lfp(%x. POgen(x) Un R Un PO) ==> + : POgen(lfp(%x. POgen(x) Un R Un PO))" + " : POgen(lfp(%x. POgen(x) Un R Un PO))" + " : lfp(%x. POgen(x) Un R Un PO) ==> + : POgen(lfp(%x. POgen(x) Un R Un PO))" + "<[],[]> : POgen(lfp(%x. POgen(x) Un R Un PO))" + "[| : lfp(%x. POgen(x) Un R Un PO); : lfp(%x. POgen(x) Un R Un PO) |] + ==> : 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}) - [" : POgen(R)", - " : POgen(R)", - "[| : R; : R |] ==> <,> : POgen(R)", - "[|!!x. : R |] ==> : POgen(R)", - " : POgen(R)", - " : lfp(%x. POgen(x) Un R Un PO) ==> : POgen(lfp(%x. POgen(x) Un R Un PO))", - " : lfp(%x. POgen(x) Un R Un PO) ==> : POgen(lfp(%x. POgen(x) Un R Un PO))", - " : POgen(lfp(%x. POgen(x) Un R Un PO))", - " : lfp(%x. POgen(x) Un R Un PO) ==> : POgen(lfp(%x. POgen(x) Un R Un PO))", - "<[],[]> : POgen(lfp(%x. POgen(x) Un R Un PO))", - "[| : lfp(%x. POgen(x) Un R Un PO); : lfp(%x. POgen(x) Un R Un PO) |] ==> : 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: " : EQ" - apply (rule refl [THEN EQ_iff [THEN iffD1]]) - done + by (rule refl [THEN EQ_iff [THEN iffD1]]) + +lemma EQgenIs: + " : EQgen(R)" + " : EQgen(R)" + "[| : R; : R |] ==> <,> : EQgen(R)" + "!!b b'. [|!!x. : R |] ==> : EQgen(R)" + " : EQgen(R)" + " : lfp(%x. EQgen(x) Un R Un EQ) ==> + : EQgen(lfp(%x. EQgen(x) Un R Un EQ))" + " : lfp(%x. EQgen(x) Un R Un EQ) ==> + : EQgen(lfp(%x. EQgen(x) Un R Un EQ))" + " : EQgen(lfp(%x. EQgen(x) Un R Un EQ))" + " : lfp(%x. EQgen(x) Un R Un EQ) ==> + : EQgen(lfp(%x. EQgen(x) Un R Un EQ))" + "<[],[]> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))" + "[| : lfp(%x. EQgen(x) Un R Un EQ); : lfp(%x. EQgen(x) Un R Un EQ) |] + ==> : 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}) - [" : EQgen(R)", - " : EQgen(R)", - "[| : R; : R |] ==> <,> : EQgen(R)", - "[|!!x. : R |] ==> : EQgen(R)", - " : EQgen(R)", - " : lfp(%x. EQgen(x) Un R Un EQ) ==> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))", - " : lfp(%x. EQgen(x) Un R Un EQ) ==> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))", - " : EQgen(lfp(%x. EQgen(x) Un R Un EQ))", - " : lfp(%x. EQgen(x) Un R Un EQ) ==> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))", - "<[],[]> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))", - "[| : lfp(%x. EQgen(x) Un R Un EQ); : lfp(%x. EQgen(x) Un R Un EQ) |] ==> : 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 : EQgen(R) using rews and *) (* then reduce this to a goal : 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 *}