# HG changeset patch # User wenzelm # Date 1248379196 -7200 # Node ID a0e57fb1b930a4aecd92c693541798aa6155a262 # Parent 53716a67c3b1251a9fde6091bcfa5d7555ff08fa misc modernization: proper method setup instead of adhoc ML proofs; diff -r 53716a67c3b1 -r a0e57fb1b930 src/CCL/CCL.thy --- a/src/CCL/CCL.thy Thu Jul 23 20:05:20 2009 +0200 +++ b/src/CCL/CCL.thy Thu Jul 23 21:59:56 2009 +0200 @@ -151,7 +151,8 @@ lemmas ccl_data_defs = apply_def fix_def - and [simp] = po_refl + +declare po_refl [simp] subsection {* Congruence Rules *} @@ -190,7 +191,7 @@ fun mk_inj_rl thy rews s = let fun mk_inj_lemmas r = [@{thm arg_cong}] RL [r RS (r RS @{thm eq_lemma})] - val inj_lemmas = List.concat (map mk_inj_lemmas rews) + val inj_lemmas = maps mk_inj_lemmas rews val tac = REPEAT (ares_tac [iffI, allI, conjI] 1 ORELSE eresolve_tac inj_lemmas 1 ORELSE asm_simp_tac (Simplifier.theory_context thy @{simpset} addsimps rews) 1) @@ -240,7 +241,7 @@ fun mk_lemma (ra,rb) = [lemma] RL [ra RS (rb RS eq_lemma)] RL [distinctness RS notE,sym RS (distinctness RS notE)] in - fun mk_lemmas rls = List.concat (map mk_lemma (mk_combs pair rls)) + fun mk_lemmas rls = maps mk_lemma (mk_combs pair rls) fun mk_dstnct_rls thy xs = mk_combs (mk_thm_str thy) xs end @@ -261,7 +262,7 @@ (fn _ => [simp_tac (global_simpset_of thy addsimps (rls@inj_rls)) 1]) in map (mk_dstnct_thm ccl_dstncts) (mk_dstnct_rls thy xs) end -fun mkall_dstnct_thms thy defs i_rls xss = List.concat (map (mk_dstnct_thms thy defs i_rls) xss) +fun mkall_dstnct_thms thy defs i_rls xss = maps (mk_dstnct_thms thy defs i_rls) xss (*** Rewriting and Proving ***) @@ -384,25 +385,25 @@ apply (rule po_refl npo_lam_bot)+ done -ML {* - -local - fun mk_thm s = prove_goal @{theory} s (fn _ => - [rtac notI 1, dtac @{thm case_pocong} 1, etac rev_mp 5, - ALLGOALS (simp_tac @{simpset}), - REPEAT (resolve_tac [@{thm po_refl}, @{thm npo_lam_bot}] 1)]) -in +lemma npo_rls1: + "~ true [= false" + "~ false [= true" + "~ true [= " + "~ [= true" + "~ true [= lam x. f(x)" + "~ lam x. f(x) [= true" + "~ false [= " + "~ [= false" + "~ false [= lam x. f(x)" + "~ lam x. f(x) [= false" + by (tactic {* + REPEAT (rtac notI 1 THEN + dtac @{thm case_pocong} 1 THEN + etac rev_mp 5 THEN + ALLGOALS (simp_tac @{simpset}) THEN + REPEAT (resolve_tac [@{thm po_refl}, @{thm npo_lam_bot}] 1)) *}) -val npo_rls = [@{thm npo_pair_lam}, @{thm npo_lam_pair}] @ map mk_thm - ["~ true [= false", "~ false [= true", - "~ true [= ", "~ [= true", - "~ true [= lam x. f(x)","~ lam x. f(x) [= true", - "~ false [= ", "~ [= false", - "~ false [= lam x. f(x)","~ lam x. f(x) [= false"] -end; - -bind_thms ("npo_rls", npo_rls); -*} +lemmas npo_rls = npo_pair_lam npo_lam_pair npo_rls1 subsection {* Coinduction for @{text "[="} *} diff -r 53716a67c3b1 -r a0e57fb1b930 src/CCL/Fix.thy --- a/src/CCL/Fix.thy Thu Jul 23 20:05:20 2009 +0200 +++ b/src/CCL/Fix.thy Thu Jul 23 21:59:56 2009 +0200 @@ -1,5 +1,4 @@ (* Title: CCL/Fix.thy - ID: $Id$ Author: Martin Coen Copyright 1993 University of Cambridge *) diff -r 53716a67c3b1 -r a0e57fb1b930 src/CCL/Gfp.thy --- a/src/CCL/Gfp.thy Thu Jul 23 20:05:20 2009 +0200 +++ b/src/CCL/Gfp.thy Thu Jul 23 21:59:56 2009 +0200 @@ -1,5 +1,4 @@ (* Title: CCL/Gfp.thy - ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1992 University of Cambridge *) diff -r 53716a67c3b1 -r a0e57fb1b930 src/CCL/Hered.thy --- 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 |] ==> : 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 |] ==> : 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 *} diff -r 53716a67c3b1 -r a0e57fb1b930 src/CCL/Lfp.thy --- a/src/CCL/Lfp.thy Thu Jul 23 20:05:20 2009 +0200 +++ b/src/CCL/Lfp.thy Thu Jul 23 21:59:56 2009 +0200 @@ -1,5 +1,4 @@ (* Title: CCL/Lfp.thy - ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1992 University of Cambridge *) diff -r 53716a67c3b1 -r a0e57fb1b930 src/CCL/ROOT.ML --- a/src/CCL/ROOT.ML Thu Jul 23 20:05:20 2009 +0200 +++ b/src/CCL/ROOT.ML Thu Jul 23 21:59:56 2009 +0200 @@ -1,5 +1,4 @@ (* Title: CCL/ROOT.ML - ID: $Id$ Author: Martin Coen, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge diff -r 53716a67c3b1 -r a0e57fb1b930 src/CCL/Set.thy --- a/src/CCL/Set.thy Thu Jul 23 20:05:20 2009 +0200 +++ b/src/CCL/Set.thy Thu Jul 23 21:59:56 2009 +0200 @@ -1,7 +1,3 @@ -(* Title: CCL/Set.thy - ID: $Id$ -*) - header {* Extending FOL by a modified version of HOL set theory *} theory Set diff -r 53716a67c3b1 -r a0e57fb1b930 src/CCL/Term.thy --- a/src/CCL/Term.thy Thu Jul 23 20:05:20 2009 +0200 +++ b/src/CCL/Term.thy Thu Jul 23 21:59:56 2009 +0200 @@ -199,80 +199,81 @@ lemmas rawBs = caseBs applyB applyBbot -ML {* -local - val letrecB = thm "letrecB" - val rawBs = thms "rawBs" - val data_defs = thms "data_defs" -in +method_setup beta_rl = {* + Scan.succeed (fn ctxt => + SIMPLE_METHOD' (CHANGED o + simp_tac (simpset_of ctxt addsimps @{thms rawBs} setloop (stac @{thm letrecB})))) +*} "" -fun raw_mk_beta_rl defs s = prove_goalw (the_context ()) defs s - (fn _ => [stac letrecB 1, - simp_tac (@{simpset} addsimps rawBs) 1]); -fun mk_beta_rl s = raw_mk_beta_rl data_defs s; +lemma ifBtrue: "if true then t else u = t" + and ifBfalse: "if false then t else u = u" + and ifBbot: "if bot then t else u = bot" + unfolding data_defs by beta_rl+ + +lemma whenBinl: "when(inl(a),t,u) = t(a)" + and whenBinr: "when(inr(a),t,u) = u(a)" + and whenBbot: "when(bot,t,u) = bot" + unfolding data_defs by beta_rl+ -fun raw_mk_beta_rl defs s = prove_goalw (the_context ()) defs s - (fn _ => [simp_tac (@{simpset} addsimps rawBs - setloop (stac letrecB)) 1]); -fun mk_beta_rl s = raw_mk_beta_rl data_defs s; +lemma splitB: "split(,h) = h(a,b)" + and splitBbot: "split(bot,h) = bot" + unfolding data_defs by beta_rl+ -end -*} +lemma fstB: "fst() = a" + and fstBbot: "fst(bot) = bot" + unfolding data_defs by beta_rl+ -ML {* -bind_thm ("ifBtrue", mk_beta_rl "if true then t else u = t"); -bind_thm ("ifBfalse", mk_beta_rl "if false then t else u = u"); -bind_thm ("ifBbot", mk_beta_rl "if bot then t else u = bot"); +lemma sndB: "snd() = b" + and sndBbot: "snd(bot) = bot" + unfolding data_defs by beta_rl+ -bind_thm ("whenBinl", mk_beta_rl "when(inl(a),t,u) = t(a)"); -bind_thm ("whenBinr", mk_beta_rl "when(inr(a),t,u) = u(a)"); -bind_thm ("whenBbot", mk_beta_rl "when(bot,t,u) = bot"); +lemma thdB: "thd(>) = c" + and thdBbot: "thd(bot) = bot" + unfolding data_defs by beta_rl+ -bind_thm ("splitB", mk_beta_rl "split(,h) = h(a,b)"); -bind_thm ("splitBbot", mk_beta_rl "split(bot,h) = bot"); -bind_thm ("fstB", mk_beta_rl "fst() = a"); -bind_thm ("fstBbot", mk_beta_rl "fst(bot) = bot"); -bind_thm ("sndB", mk_beta_rl "snd() = b"); -bind_thm ("sndBbot", mk_beta_rl "snd(bot) = bot"); -bind_thm ("thdB", mk_beta_rl "thd(>) = c"); -bind_thm ("thdBbot", mk_beta_rl "thd(bot) = bot"); +lemma ncaseBzero: "ncase(zero,t,u) = t" + and ncaseBsucc: "ncase(succ(n),t,u) = u(n)" + and ncaseBbot: "ncase(bot,t,u) = bot" + unfolding data_defs by beta_rl+ -bind_thm ("ncaseBzero", mk_beta_rl "ncase(zero,t,u) = t"); -bind_thm ("ncaseBsucc", mk_beta_rl "ncase(succ(n),t,u) = u(n)"); -bind_thm ("ncaseBbot", mk_beta_rl "ncase(bot,t,u) = bot"); -bind_thm ("nrecBzero", mk_beta_rl "nrec(zero,t,u) = t"); -bind_thm ("nrecBsucc", mk_beta_rl "nrec(succ(n),t,u) = u(n,nrec(n,t,u))"); -bind_thm ("nrecBbot", mk_beta_rl "nrec(bot,t,u) = bot"); +lemma nrecBzero: "nrec(zero,t,u) = t" + and nrecBsucc: "nrec(succ(n),t,u) = u(n,nrec(n,t,u))" + and nrecBbot: "nrec(bot,t,u) = bot" + unfolding data_defs by beta_rl+ + +lemma lcaseBnil: "lcase([],t,u) = t" + and lcaseBcons: "lcase(x$xs,t,u) = u(x,xs)" + and lcaseBbot: "lcase(bot,t,u) = bot" + unfolding data_defs by beta_rl+ -bind_thm ("lcaseBnil", mk_beta_rl "lcase([],t,u) = t"); -bind_thm ("lcaseBcons", mk_beta_rl "lcase(x$xs,t,u) = u(x,xs)"); -bind_thm ("lcaseBbot", mk_beta_rl "lcase(bot,t,u) = bot"); -bind_thm ("lrecBnil", mk_beta_rl "lrec([],t,u) = t"); -bind_thm ("lrecBcons", mk_beta_rl "lrec(x$xs,t,u) = u(x,xs,lrec(xs,t,u))"); -bind_thm ("lrecBbot", mk_beta_rl "lrec(bot,t,u) = bot"); +lemma lrecBnil: "lrec([],t,u) = t" + and lrecBcons: "lrec(x$xs,t,u) = u(x,xs,lrec(xs,t,u))" + and lrecBbot: "lrec(bot,t,u) = bot" + unfolding data_defs by beta_rl+ -bind_thm ("letrec2B", raw_mk_beta_rl (thms "data_defs" @ [thm "letrec2_def"]) - "letrec g x y be h(x,y,g) in g(p,q) = h(p,q,%u v. letrec g x y be h(x,y,g) in g(u,v))"); +lemma letrec2B: + "letrec g x y be h(x,y,g) in g(p,q) = h(p,q,%u v. letrec g x y be h(x,y,g) in g(u,v))" + unfolding data_defs letrec2_def by beta_rl+ -bind_thm ("letrec3B", raw_mk_beta_rl (thms "data_defs" @ [thm "letrec3_def"]) - "letrec g x y z be h(x,y,z,g) in g(p,q,r) = h(p,q,r,%u v w. letrec g x y z be h(x,y,z,g) in g(u,v,w))"); - -bind_thm ("napplyBzero", mk_beta_rl "f^zero`a = a"); -bind_thm ("napplyBsucc", mk_beta_rl "f^succ(n)`a = f(f^n`a)"); +lemma letrec3B: + "letrec g x y z be h(x,y,z,g) in g(p,q,r) = + h(p,q,r,%u v w. letrec g x y z be h(x,y,z,g) in g(u,v,w))" + unfolding data_defs letrec3_def by beta_rl+ -bind_thms ("termBs", [thm "letB", thm "applyB", thm "applyBbot", splitB,splitBbot, - fstB,fstBbot,sndB,sndBbot,thdB,thdBbot, - ifBtrue,ifBfalse,ifBbot,whenBinl,whenBinr,whenBbot, - ncaseBzero,ncaseBsucc,ncaseBbot,nrecBzero,nrecBsucc,nrecBbot, - lcaseBnil,lcaseBcons,lcaseBbot,lrecBnil,lrecBcons,lrecBbot, - napplyBzero,napplyBsucc]); -*} +lemma napplyBzero: "f^zero`a = a" + and napplyBsucc: "f^succ(n)`a = f(f^n`a)" + unfolding data_defs by beta_rl+ + +lemmas termBs = letB applyB applyBbot splitB splitBbot fstB fstBbot + sndB sndBbot thdB thdBbot ifBtrue ifBfalse ifBbot whenBinl whenBinr + whenBbot ncaseBzero ncaseBsucc ncaseBbot nrecBzero nrecBsucc + nrecBbot lcaseBnil lcaseBcons lcaseBbot lrecBnil lrecBcons lrecBbot + napplyBzero napplyBsucc subsection {* Constructors are injective *} ML {* - bind_thms ("term_injs", map (mk_inj_rl @{theory} [@{thm applyB}, @{thm splitB}, @{thm whenBinl}, @{thm whenBinr}, @{thm ncaseBsucc}, @{thm lcaseBcons}]) @@ -297,13 +298,17 @@ ML {* local - fun mk_thm s = prove_goalw @{theory} @{thms data_defs} s (fn _ => - [simp_tac (@{simpset} addsimps @{thms ccl_porews}) 1]) + fun mk_thm s = + Goal.prove_global @{theory} [] [] (Syntax.read_prop_global @{theory} s) + (fn _ => + rewrite_goals_tac @{thms data_defs} THEN + simp_tac (@{simpset} addsimps @{thms ccl_porews}) 1); in - val term_porews = map mk_thm ["inl(a) [= inl(a') <-> a [= a'", - "inr(b) [= inr(b') <-> b [= b'", - "succ(n) [= succ(n') <-> n [= n'", - "x$xs [= x'$xs' <-> x [= x' & xs [= xs'"] + val term_porews = + map mk_thm ["inl(a) [= inl(a') <-> a [= a'", + "inr(b) [= inr(b') <-> b [= b'", + "succ(n) [= succ(n') <-> n [= n'", + "x$xs [= x'$xs' <-> x [= x' & xs [= xs'"] end; bind_thms ("term_porews", term_porews); diff -r 53716a67c3b1 -r a0e57fb1b930 src/CCL/Trancl.thy --- a/src/CCL/Trancl.thy Thu Jul 23 20:05:20 2009 +0200 +++ b/src/CCL/Trancl.thy Thu Jul 23 21:59:56 2009 +0200 @@ -1,5 +1,4 @@ (* Title: CCL/Trancl.thy - ID: $Id$ Author: Martin Coen, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge *) 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 *} diff -r 53716a67c3b1 -r a0e57fb1b930 src/CCL/ex/Flag.thy --- a/src/CCL/ex/Flag.thy Thu Jul 23 20:05:20 2009 +0200 +++ b/src/CCL/ex/Flag.thy Thu Jul 23 21:59:56 2009 +0200 @@ -1,5 +1,4 @@ (* Title: CCL/ex/Flag.thy - ID: $Id$ Author: Martin Coen, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge *) @@ -55,12 +54,10 @@ and blueT: "blue : Colour" unfolding ColourXH by blast+ -ML {* -bind_thm ("ccaseT", mk_ncanT_tac @{context} - @{thms flag_defs} @{thms case_rls} @{thms case_rls} - "[| c:Colour; c=red ==> r : C(red); c=white ==> w : C(white); c=blue ==> b : C(blue) |] ==> ccase(c,r,w,b) : C(c)"); -*} - +lemma ccaseT: + "[| c:Colour; c=red ==> r : C(red); c=white ==> w : C(white); c=blue ==> b : C(blue) |] + ==> ccase(c,r,w,b) : C(c)" + unfolding flag_defs by ncanT lemma "flag : List(Colour)->List(Colour)*List(Colour)*List(Colour)" apply (unfold flag_def)