--- 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 [= <a,b>"
+ "~ <a,b> [= true"
+ "~ true [= lam x. f(x)"
+ "~ lam x. f(x) [= true"
+ "~ false [= <a,b>"
+ "~ <a,b> [= 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 [= <a,b>", "~ <a,b> [= true",
- "~ true [= lam x. f(x)","~ lam x. f(x) [= true",
- "~ false [= <a,b>", "~ <a,b> [= 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 "[="} *}
--- 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
*)
--- 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
*)
--- 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 *}
--- 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
*)
--- 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
--- 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
--- 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(<a,b>,h) = h(a,b)"
+ and splitBbot: "split(bot,h) = bot"
+ unfolding data_defs by beta_rl+
-end
-*}
+lemma fstB: "fst(<a,b>) = 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(<a,b>) = 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(<a,<b,c>>) = c"
+ and thdBbot: "thd(bot) = bot"
+ unfolding data_defs by beta_rl+
-bind_thm ("splitB", mk_beta_rl "split(<a,b>,h) = h(a,b)");
-bind_thm ("splitBbot", mk_beta_rl "split(bot,h) = bot");
-bind_thm ("fstB", mk_beta_rl "fst(<a,b>) = a");
-bind_thm ("fstBbot", mk_beta_rl "fst(bot) = bot");
-bind_thm ("sndB", mk_beta_rl "snd(<a,b>) = b");
-bind_thm ("sndBbot", mk_beta_rl "snd(bot) = bot");
-bind_thm ("thdB", mk_beta_rl "thd(<a,<b,c>>) = 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);
--- 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
*)
--- 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
*}
--- 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)