misc modernization: proper method setup instead of adhoc ML proofs;
authorwenzelm
Thu Jul 23 21:59:56 2009 +0200 (2009-07-23)
changeset 32153a0e57fb1b930
parent 32152 53716a67c3b1
child 32154 9721e8e4d48c
misc modernization: proper method setup instead of adhoc ML proofs;
src/CCL/CCL.thy
src/CCL/Fix.thy
src/CCL/Gfp.thy
src/CCL/Hered.thy
src/CCL/Lfp.thy
src/CCL/ROOT.ML
src/CCL/Set.thy
src/CCL/Term.thy
src/CCL/Trancl.thy
src/CCL/Type.thy
src/CCL/ex/Flag.thy
     1.1 --- a/src/CCL/CCL.thy	Thu Jul 23 20:05:20 2009 +0200
     1.2 +++ b/src/CCL/CCL.thy	Thu Jul 23 21:59:56 2009 +0200
     1.3 @@ -151,7 +151,8 @@
     1.4  
     1.5  
     1.6  lemmas ccl_data_defs = apply_def fix_def
     1.7 -  and [simp] = po_refl
     1.8 +
     1.9 +declare po_refl [simp]
    1.10  
    1.11  
    1.12  subsection {* Congruence Rules *}
    1.13 @@ -190,7 +191,7 @@
    1.14    fun mk_inj_rl thy rews s =
    1.15      let
    1.16        fun mk_inj_lemmas r = [@{thm arg_cong}] RL [r RS (r RS @{thm eq_lemma})]
    1.17 -      val inj_lemmas = List.concat (map mk_inj_lemmas rews)
    1.18 +      val inj_lemmas = maps mk_inj_lemmas rews
    1.19        val tac = REPEAT (ares_tac [iffI, allI, conjI] 1 ORELSE
    1.20          eresolve_tac inj_lemmas 1 ORELSE
    1.21          asm_simp_tac (Simplifier.theory_context thy @{simpset} addsimps rews) 1)
    1.22 @@ -240,7 +241,7 @@
    1.23    fun mk_lemma (ra,rb) = [lemma] RL [ra RS (rb RS eq_lemma)] RL
    1.24                             [distinctness RS notE,sym RS (distinctness RS notE)]
    1.25  in
    1.26 -  fun mk_lemmas rls = List.concat (map mk_lemma (mk_combs pair rls))
    1.27 +  fun mk_lemmas rls = maps mk_lemma (mk_combs pair rls)
    1.28    fun mk_dstnct_rls thy xs = mk_combs (mk_thm_str thy) xs
    1.29  end
    1.30  
    1.31 @@ -261,7 +262,7 @@
    1.32      (fn _ => [simp_tac (global_simpset_of thy addsimps (rls@inj_rls)) 1])
    1.33    in map (mk_dstnct_thm ccl_dstncts) (mk_dstnct_rls thy xs) end
    1.34  
    1.35 -fun mkall_dstnct_thms thy defs i_rls xss = List.concat (map (mk_dstnct_thms thy defs i_rls) xss)
    1.36 +fun mkall_dstnct_thms thy defs i_rls xss = maps (mk_dstnct_thms thy defs i_rls) xss
    1.37  
    1.38  (*** Rewriting and Proving ***)
    1.39  
    1.40 @@ -384,25 +385,25 @@
    1.41    apply (rule po_refl npo_lam_bot)+
    1.42    done
    1.43  
    1.44 -ML {*
    1.45 -
    1.46 -local
    1.47 -  fun mk_thm s = prove_goal @{theory} s (fn _ =>
    1.48 -                          [rtac notI 1, dtac @{thm case_pocong} 1, etac rev_mp 5,
    1.49 -                           ALLGOALS (simp_tac @{simpset}),
    1.50 -                           REPEAT (resolve_tac [@{thm po_refl}, @{thm npo_lam_bot}] 1)])
    1.51 -in
    1.52 +lemma npo_rls1:
    1.53 +  "~ true [= false"
    1.54 +  "~ false [= true"
    1.55 +  "~ true [= <a,b>"
    1.56 +  "~ <a,b> [= true"
    1.57 +  "~ true [= lam x. f(x)"
    1.58 +  "~ lam x. f(x) [= true"
    1.59 +  "~ false [= <a,b>"
    1.60 +  "~ <a,b> [= false"
    1.61 +  "~ false [= lam x. f(x)"
    1.62 +  "~ lam x. f(x) [= false"
    1.63 +  by (tactic {*
    1.64 +    REPEAT (rtac notI 1 THEN
    1.65 +      dtac @{thm case_pocong} 1 THEN
    1.66 +      etac rev_mp 5 THEN
    1.67 +      ALLGOALS (simp_tac @{simpset}) THEN
    1.68 +      REPEAT (resolve_tac [@{thm po_refl}, @{thm npo_lam_bot}] 1)) *})
    1.69  
    1.70 -val npo_rls = [@{thm npo_pair_lam}, @{thm npo_lam_pair}] @ map mk_thm
    1.71 -            ["~ true [= false",          "~ false [= true",
    1.72 -             "~ true [= <a,b>",          "~ <a,b> [= true",
    1.73 -             "~ true [= lam x. f(x)","~ lam x. f(x) [= true",
    1.74 -            "~ false [= <a,b>",          "~ <a,b> [= false",
    1.75 -            "~ false [= lam x. f(x)","~ lam x. f(x) [= false"]
    1.76 -end;
    1.77 -
    1.78 -bind_thms ("npo_rls", npo_rls);
    1.79 -*}
    1.80 +lemmas npo_rls = npo_pair_lam npo_lam_pair npo_rls1
    1.81  
    1.82  
    1.83  subsection {* Coinduction for @{text "[="} *}
     2.1 --- a/src/CCL/Fix.thy	Thu Jul 23 20:05:20 2009 +0200
     2.2 +++ b/src/CCL/Fix.thy	Thu Jul 23 21:59:56 2009 +0200
     2.3 @@ -1,5 +1,4 @@
     2.4  (*  Title:      CCL/Fix.thy
     2.5 -    ID:         $Id$
     2.6      Author:     Martin Coen
     2.7      Copyright   1993  University of Cambridge
     2.8  *)
     3.1 --- a/src/CCL/Gfp.thy	Thu Jul 23 20:05:20 2009 +0200
     3.2 +++ b/src/CCL/Gfp.thy	Thu Jul 23 21:59:56 2009 +0200
     3.3 @@ -1,5 +1,4 @@
     3.4  (*  Title:      CCL/Gfp.thy
     3.5 -    ID:         $Id$
     3.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3.7      Copyright   1992  University of Cambridge
     3.8  *)
     4.1 --- a/src/CCL/Hered.thy	Thu Jul 23 20:05:20 2009 +0200
     4.2 +++ b/src/CCL/Hered.thy	Thu Jul 23 21:59:56 2009 +0200
     4.3 @@ -110,23 +110,22 @@
     4.4  
     4.5  fun HTT_coinduct3_tac ctxt s i =
     4.6    res_inst_tac ctxt [(("R", 0), s)] @{thm HTT_coinduct3} i
     4.7 -
     4.8 -val HTTgenIs =
     4.9 -  map (mk_genIs @{theory} @{thms data_defs} @{thm HTTgenXH} @{thm HTTgen_mono})
    4.10 -  ["true : HTTgen(R)",
    4.11 -   "false : HTTgen(R)",
    4.12 -   "[| a : R;  b : R |] ==> <a,b> : HTTgen(R)",
    4.13 -   "[| !!x. b(x) : R |] ==> lam x. b(x) : HTTgen(R)",
    4.14 -   "one : HTTgen(R)",
    4.15 -   "a : lfp(%x. HTTgen(x) Un R Un HTT) ==> inl(a) : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))",
    4.16 -   "b : lfp(%x. HTTgen(x) Un R Un HTT) ==> inr(b) : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))",
    4.17 -   "zero : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))",
    4.18 -   "n : lfp(%x. HTTgen(x) Un R Un HTT) ==> succ(n) : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))",
    4.19 -   "[] : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))",
    4.20 -   "[| 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))"]
    4.21  *}
    4.22  
    4.23 -ML {* bind_thms ("HTTgenIs", HTTgenIs) *}
    4.24 +lemma HTTgenIs:
    4.25 +  "true : HTTgen(R)"
    4.26 +  "false : HTTgen(R)"
    4.27 +  "[| a : R;  b : R |] ==> <a,b> : HTTgen(R)"
    4.28 +  "!!b. [| !!x. b(x) : R |] ==> lam x. b(x) : HTTgen(R)"
    4.29 +  "one : HTTgen(R)"
    4.30 +  "a : lfp(%x. HTTgen(x) Un R Un HTT) ==> inl(a) : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))"
    4.31 +  "b : lfp(%x. HTTgen(x) Un R Un HTT) ==> inr(b) : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))"
    4.32 +  "zero : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))"
    4.33 +  "n : lfp(%x. HTTgen(x) Un R Un HTT) ==> succ(n) : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))"
    4.34 +  "[] : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))"
    4.35 +  "[| h : lfp(%x. HTTgen(x) Un R Un HTT); t : lfp(%x. HTTgen(x) Un R Un HTT) |] ==>
    4.36 +    h$t : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))"
    4.37 +  unfolding data_defs by (genIs HTTgenXH HTTgen_mono)+
    4.38  
    4.39  
    4.40  subsection {* Formation Rules for Types *}
     5.1 --- a/src/CCL/Lfp.thy	Thu Jul 23 20:05:20 2009 +0200
     5.2 +++ b/src/CCL/Lfp.thy	Thu Jul 23 21:59:56 2009 +0200
     5.3 @@ -1,5 +1,4 @@
     5.4  (*  Title:      CCL/Lfp.thy
     5.5 -    ID:         $Id$
     5.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     5.7      Copyright   1992  University of Cambridge
     5.8  *)
     6.1 --- a/src/CCL/ROOT.ML	Thu Jul 23 20:05:20 2009 +0200
     6.2 +++ b/src/CCL/ROOT.ML	Thu Jul 23 21:59:56 2009 +0200
     6.3 @@ -1,5 +1,4 @@
     6.4  (*  Title:      CCL/ROOT.ML
     6.5 -    ID:         $Id$
     6.6      Author:     Martin Coen, Cambridge University Computer Laboratory
     6.7      Copyright   1993  University of Cambridge
     6.8  
     7.1 --- a/src/CCL/Set.thy	Thu Jul 23 20:05:20 2009 +0200
     7.2 +++ b/src/CCL/Set.thy	Thu Jul 23 21:59:56 2009 +0200
     7.3 @@ -1,7 +1,3 @@
     7.4 -(*  Title:      CCL/Set.thy
     7.5 -    ID:         $Id$
     7.6 -*)
     7.7 -
     7.8  header {* Extending FOL by a modified version of HOL set theory *}
     7.9  
    7.10  theory Set
     8.1 --- a/src/CCL/Term.thy	Thu Jul 23 20:05:20 2009 +0200
     8.2 +++ b/src/CCL/Term.thy	Thu Jul 23 21:59:56 2009 +0200
     8.3 @@ -199,80 +199,81 @@
     8.4  
     8.5  lemmas rawBs = caseBs applyB applyBbot
     8.6  
     8.7 -ML {*
     8.8 -local
     8.9 -  val letrecB = thm "letrecB"
    8.10 -  val rawBs = thms "rawBs"
    8.11 -  val data_defs = thms "data_defs"
    8.12 -in
    8.13 +method_setup beta_rl = {*
    8.14 +  Scan.succeed (fn ctxt =>
    8.15 +    SIMPLE_METHOD' (CHANGED o
    8.16 +      simp_tac (simpset_of ctxt addsimps @{thms rawBs} setloop (stac @{thm letrecB}))))
    8.17 +*} ""
    8.18  
    8.19 -fun raw_mk_beta_rl defs s = prove_goalw (the_context ()) defs s
    8.20 -           (fn _ => [stac letrecB 1,
    8.21 -                     simp_tac (@{simpset} addsimps rawBs) 1]);
    8.22 -fun mk_beta_rl s = raw_mk_beta_rl data_defs s;
    8.23 +lemma ifBtrue: "if true then t else u = t"
    8.24 +  and ifBfalse: "if false then t else u = u"
    8.25 +  and ifBbot: "if bot then t else u = bot"
    8.26 +  unfolding data_defs by beta_rl+
    8.27 +
    8.28 +lemma whenBinl: "when(inl(a),t,u) = t(a)"
    8.29 +  and whenBinr: "when(inr(a),t,u) = u(a)"
    8.30 +  and whenBbot: "when(bot,t,u) = bot"
    8.31 +  unfolding data_defs by beta_rl+
    8.32  
    8.33 -fun raw_mk_beta_rl defs s = prove_goalw (the_context ()) defs s
    8.34 -           (fn _ => [simp_tac (@{simpset} addsimps rawBs
    8.35 -                               setloop (stac letrecB)) 1]);
    8.36 -fun mk_beta_rl s = raw_mk_beta_rl data_defs s;
    8.37 +lemma splitB: "split(<a,b>,h) = h(a,b)"
    8.38 +  and splitBbot: "split(bot,h) = bot"
    8.39 +  unfolding data_defs by beta_rl+
    8.40  
    8.41 -end
    8.42 -*}
    8.43 +lemma fstB: "fst(<a,b>) = a"
    8.44 +  and fstBbot: "fst(bot) = bot"
    8.45 +  unfolding data_defs by beta_rl+
    8.46  
    8.47 -ML {*
    8.48 -bind_thm ("ifBtrue", mk_beta_rl "if true then t else u = t");
    8.49 -bind_thm ("ifBfalse", mk_beta_rl "if false then t else u = u");
    8.50 -bind_thm ("ifBbot", mk_beta_rl "if bot then t else u = bot");
    8.51 +lemma sndB: "snd(<a,b>) = b"
    8.52 +  and sndBbot: "snd(bot) = bot"
    8.53 +  unfolding data_defs by beta_rl+
    8.54  
    8.55 -bind_thm ("whenBinl", mk_beta_rl "when(inl(a),t,u) = t(a)");
    8.56 -bind_thm ("whenBinr", mk_beta_rl "when(inr(a),t,u) = u(a)");
    8.57 -bind_thm ("whenBbot", mk_beta_rl "when(bot,t,u) = bot");
    8.58 +lemma thdB: "thd(<a,<b,c>>) = c"
    8.59 +  and thdBbot: "thd(bot) = bot"
    8.60 +  unfolding data_defs by beta_rl+
    8.61  
    8.62 -bind_thm ("splitB", mk_beta_rl "split(<a,b>,h) = h(a,b)");
    8.63 -bind_thm ("splitBbot", mk_beta_rl "split(bot,h) = bot");
    8.64 -bind_thm ("fstB", mk_beta_rl "fst(<a,b>) = a");
    8.65 -bind_thm ("fstBbot", mk_beta_rl "fst(bot) = bot");
    8.66 -bind_thm ("sndB", mk_beta_rl "snd(<a,b>) = b");
    8.67 -bind_thm ("sndBbot", mk_beta_rl "snd(bot) = bot");
    8.68 -bind_thm ("thdB", mk_beta_rl "thd(<a,<b,c>>) = c");
    8.69 -bind_thm ("thdBbot", mk_beta_rl "thd(bot) = bot");
    8.70 +lemma ncaseBzero: "ncase(zero,t,u) = t"
    8.71 +  and ncaseBsucc: "ncase(succ(n),t,u) = u(n)"
    8.72 +  and ncaseBbot: "ncase(bot,t,u) = bot"
    8.73 +  unfolding data_defs by beta_rl+
    8.74  
    8.75 -bind_thm ("ncaseBzero", mk_beta_rl "ncase(zero,t,u) = t");
    8.76 -bind_thm ("ncaseBsucc", mk_beta_rl "ncase(succ(n),t,u) = u(n)");
    8.77 -bind_thm ("ncaseBbot", mk_beta_rl "ncase(bot,t,u) = bot");
    8.78 -bind_thm ("nrecBzero", mk_beta_rl "nrec(zero,t,u) = t");
    8.79 -bind_thm ("nrecBsucc", mk_beta_rl "nrec(succ(n),t,u) = u(n,nrec(n,t,u))");
    8.80 -bind_thm ("nrecBbot", mk_beta_rl "nrec(bot,t,u) = bot");
    8.81 +lemma nrecBzero: "nrec(zero,t,u) = t"
    8.82 +  and nrecBsucc: "nrec(succ(n),t,u) = u(n,nrec(n,t,u))"
    8.83 +  and nrecBbot: "nrec(bot,t,u) = bot"
    8.84 +  unfolding data_defs by beta_rl+
    8.85 +
    8.86 +lemma lcaseBnil: "lcase([],t,u) = t"
    8.87 +  and lcaseBcons: "lcase(x$xs,t,u) = u(x,xs)"
    8.88 +  and lcaseBbot: "lcase(bot,t,u) = bot"
    8.89 +  unfolding data_defs by beta_rl+
    8.90  
    8.91 -bind_thm ("lcaseBnil", mk_beta_rl "lcase([],t,u) = t");
    8.92 -bind_thm ("lcaseBcons", mk_beta_rl "lcase(x$xs,t,u) = u(x,xs)");
    8.93 -bind_thm ("lcaseBbot", mk_beta_rl "lcase(bot,t,u) = bot");
    8.94 -bind_thm ("lrecBnil", mk_beta_rl "lrec([],t,u) = t");
    8.95 -bind_thm ("lrecBcons", mk_beta_rl "lrec(x$xs,t,u) = u(x,xs,lrec(xs,t,u))");
    8.96 -bind_thm ("lrecBbot", mk_beta_rl "lrec(bot,t,u) = bot");
    8.97 +lemma lrecBnil: "lrec([],t,u) = t"
    8.98 +  and lrecBcons: "lrec(x$xs,t,u) = u(x,xs,lrec(xs,t,u))"
    8.99 +  and lrecBbot: "lrec(bot,t,u) = bot"
   8.100 +  unfolding data_defs by beta_rl+
   8.101  
   8.102 -bind_thm ("letrec2B", raw_mk_beta_rl (thms "data_defs" @ [thm "letrec2_def"])
   8.103 -  "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))");
   8.104 +lemma letrec2B:
   8.105 +  "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))"
   8.106 +  unfolding data_defs letrec2_def by beta_rl+
   8.107  
   8.108 -bind_thm ("letrec3B", raw_mk_beta_rl (thms "data_defs" @ [thm "letrec3_def"])
   8.109 -  "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))");
   8.110 -
   8.111 -bind_thm ("napplyBzero", mk_beta_rl "f^zero`a = a");
   8.112 -bind_thm ("napplyBsucc", mk_beta_rl "f^succ(n)`a = f(f^n`a)");
   8.113 +lemma letrec3B:
   8.114 +  "letrec g x y z be h(x,y,z,g) in g(p,q,r) =
   8.115 +    h(p,q,r,%u v w. letrec g x y z be h(x,y,z,g) in g(u,v,w))"
   8.116 +  unfolding data_defs letrec3_def by beta_rl+
   8.117  
   8.118 -bind_thms ("termBs", [thm "letB", thm "applyB", thm "applyBbot", splitB,splitBbot,
   8.119 -  fstB,fstBbot,sndB,sndBbot,thdB,thdBbot,
   8.120 -  ifBtrue,ifBfalse,ifBbot,whenBinl,whenBinr,whenBbot,
   8.121 -  ncaseBzero,ncaseBsucc,ncaseBbot,nrecBzero,nrecBsucc,nrecBbot,
   8.122 -  lcaseBnil,lcaseBcons,lcaseBbot,lrecBnil,lrecBcons,lrecBbot,
   8.123 -  napplyBzero,napplyBsucc]);
   8.124 -*}
   8.125 +lemma napplyBzero: "f^zero`a = a"
   8.126 +  and napplyBsucc: "f^succ(n)`a = f(f^n`a)"
   8.127 +  unfolding data_defs by beta_rl+
   8.128 +
   8.129 +lemmas termBs = letB applyB applyBbot splitB splitBbot fstB fstBbot
   8.130 +  sndB sndBbot thdB thdBbot ifBtrue ifBfalse ifBbot whenBinl whenBinr
   8.131 +  whenBbot ncaseBzero ncaseBsucc ncaseBbot nrecBzero nrecBsucc
   8.132 +  nrecBbot lcaseBnil lcaseBcons lcaseBbot lrecBnil lrecBcons lrecBbot
   8.133 +  napplyBzero napplyBsucc
   8.134  
   8.135  
   8.136  subsection {* Constructors are injective *}
   8.137  
   8.138  ML {*
   8.139 -
   8.140  bind_thms ("term_injs", map (mk_inj_rl @{theory}
   8.141    [@{thm applyB}, @{thm splitB}, @{thm whenBinl}, @{thm whenBinr},
   8.142      @{thm ncaseBsucc}, @{thm lcaseBcons}])
   8.143 @@ -297,13 +298,17 @@
   8.144  ML {*
   8.145  
   8.146  local
   8.147 -  fun mk_thm s = prove_goalw @{theory} @{thms data_defs} s (fn _ =>
   8.148 -    [simp_tac (@{simpset} addsimps @{thms ccl_porews}) 1])
   8.149 +  fun mk_thm s =
   8.150 +    Goal.prove_global @{theory} [] [] (Syntax.read_prop_global @{theory} s)
   8.151 +      (fn _ =>
   8.152 +        rewrite_goals_tac @{thms data_defs} THEN
   8.153 +        simp_tac (@{simpset} addsimps @{thms ccl_porews}) 1);
   8.154  in
   8.155 -  val term_porews = map mk_thm ["inl(a) [= inl(a') <-> a [= a'",
   8.156 -                                "inr(b) [= inr(b') <-> b [= b'",
   8.157 -                                "succ(n) [= succ(n') <-> n [= n'",
   8.158 -                                "x$xs [= x'$xs' <-> x [= x'  & xs [= xs'"]
   8.159 +  val term_porews =
   8.160 +    map mk_thm ["inl(a) [= inl(a') <-> a [= a'",
   8.161 +      "inr(b) [= inr(b') <-> b [= b'",
   8.162 +      "succ(n) [= succ(n') <-> n [= n'",
   8.163 +      "x$xs [= x'$xs' <-> x [= x'  & xs [= xs'"]
   8.164  end;
   8.165  
   8.166  bind_thms ("term_porews", term_porews);
     9.1 --- a/src/CCL/Trancl.thy	Thu Jul 23 20:05:20 2009 +0200
     9.2 +++ b/src/CCL/Trancl.thy	Thu Jul 23 21:59:56 2009 +0200
     9.3 @@ -1,5 +1,4 @@
     9.4  (*  Title:      CCL/Trancl.thy
     9.5 -    ID:         $Id$
     9.6      Author:     Martin Coen, Cambridge University Computer Laboratory
     9.7      Copyright   1993  University of Cambridge
     9.8  *)
    10.1 --- a/src/CCL/Type.thy	Thu Jul 23 20:05:20 2009 +0200
    10.2 +++ b/src/CCL/Type.thy	Thu Jul 23 21:59:56 2009 +0200
    10.3 @@ -123,39 +123,36 @@
    10.4  
    10.5  
    10.6  ML {*
    10.7 -local
    10.8 -  val lemma = thm "lem"
    10.9 -  val bspec = thm "bspec"
   10.10 -  val bexE = thm "bexE"
   10.11 -in
   10.12 -
   10.13 -  fun mk_ncanT_tac ctxt defs top_crls crls s = prove_goalw (ProofContext.theory_of ctxt) defs s
   10.14 -    (fn major::prems => [(resolve_tac ([major] RL top_crls) 1),
   10.15 -                         (REPEAT_SOME (eresolve_tac (crls @ [exE,bexE,conjE,disjE]))),
   10.16 -                         (ALLGOALS (asm_simp_tac (simpset_of ctxt))),
   10.17 -                         (ALLGOALS (ares_tac (prems RL [lemma]) ORELSE'
   10.18 -                                    etac bspec )),
   10.19 -                         (safe_tac (claset_of ctxt addSIs prems))])
   10.20 -end
   10.21 +fun mk_ncanT_tac top_crls crls =
   10.22 +  SUBPROOF (fn {context = ctxt, prems = major :: prems, ...} =>
   10.23 +    resolve_tac ([major] RL top_crls) 1 THEN
   10.24 +    REPEAT_SOME (eresolve_tac (crls @ [exE, @{thm bexE}, conjE, disjE])) THEN
   10.25 +    ALLGOALS (asm_simp_tac (simpset_of ctxt)) THEN
   10.26 +    ALLGOALS (ares_tac (prems RL [@{thm lem}]) ORELSE' etac @{thm bspec}) THEN
   10.27 +    safe_tac (claset_of ctxt addSIs prems))
   10.28  *}
   10.29  
   10.30 -ML {*
   10.31 -  val ncanT_tac = mk_ncanT_tac @{context} [] @{thms case_rls} @{thms case_rls}
   10.32 -*}
   10.33 +method_setup ncanT = {*
   10.34 +  Scan.succeed (SIMPLE_METHOD' o mk_ncanT_tac @{thms case_rls} @{thms case_rls})
   10.35 +*} ""
   10.36  
   10.37 -ML {*
   10.38 -
   10.39 -bind_thm ("ifT", ncanT_tac
   10.40 -  "[| b:Bool; b=true ==> t:A(true); b=false ==> u:A(false) |] ==> if b then t else u : A(b)");
   10.41 +lemma ifT:
   10.42 +  "[| b:Bool; b=true ==> t:A(true); b=false ==> u:A(false) |] ==>
   10.43 +    if b then t else u : A(b)"
   10.44 +  by ncanT
   10.45  
   10.46 -bind_thm ("applyT", ncanT_tac "[| f : Pi(A,B);  a:A |] ==> f ` a : B(a)");
   10.47 +lemma applyT: "[| f : Pi(A,B);  a:A |] ==> f ` a : B(a)"
   10.48 +  by ncanT
   10.49  
   10.50 -bind_thm ("splitT", ncanT_tac
   10.51 -  "[| 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)");
   10.52 +lemma splitT:
   10.53 +  "[| p:Sigma(A,B); !!x y. [| x:A;  y:B(x); p=<x,y> |] ==> c(x,y):C(<x,y>) |]
   10.54 +    ==> split(p,c):C(p)"
   10.55 +  by ncanT
   10.56  
   10.57 -bind_thm ("whenT", ncanT_tac
   10.58 -  "[| 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)");
   10.59 -*}
   10.60 +lemma whenT:
   10.61 +  "[| p:A+B; !!x.[| x:A;  p=inl(x) |] ==> a(x):C(inl(x)); !!y.[| y:B;  p=inr(y) |]
   10.62 +    ==> b(y):C(inr(y)) |] ==> when(p,a,b) : C(p)"
   10.63 +  by ncanT
   10.64  
   10.65  lemmas ncanTs = ifT applyT splitT whenT
   10.66  
   10.67 @@ -275,17 +272,20 @@
   10.68  
   10.69  lemmas icanTs = zeroT succT nilT consT
   10.70  
   10.71 -ML {*
   10.72 -val incanT_tac = mk_ncanT_tac @{context} [] @{thms icase_rls} @{thms case_rls};
   10.73 -*}
   10.74 +
   10.75 +method_setup incanT = {*
   10.76 +  Scan.succeed (SIMPLE_METHOD' o mk_ncanT_tac @{thms icase_rls} @{thms case_rls})
   10.77 +*} ""
   10.78  
   10.79 -ML {*
   10.80 -bind_thm ("ncaseT", incanT_tac
   10.81 -  "[| n:Nat; n=zero ==> b:C(zero); !!x.[| x:Nat;  n=succ(x) |] ==> c(x):C(succ(x)) |] ==> ncase(n,b,c) : C(n)");
   10.82 +lemma ncaseT:
   10.83 +  "[| n:Nat; n=zero ==> b:C(zero); !!x.[| x:Nat;  n=succ(x) |] ==> c(x):C(succ(x)) |]
   10.84 +    ==> ncase(n,b,c) : C(n)"
   10.85 +  by incanT
   10.86  
   10.87 -bind_thm ("lcaseT", incanT_tac
   10.88 -     "[| 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)");
   10.89 -*}
   10.90 +lemma lcaseT:
   10.91 +  "[| l:List(A); l=[] ==> b:C([]); !!h t.[| h:A;  t:List(A); l=h$t |] ==>
   10.92 +    c(h,t):C(h$t) |] ==> lcase(l,b,c) : C(l)"
   10.93 +  by incanT
   10.94  
   10.95  lemmas incanTs = ncaseT lcaseT
   10.96  
   10.97 @@ -337,7 +337,7 @@
   10.98  (*         - intro rules are type rules for canonical terms                *)
   10.99  (*         - elim rules are case rules (no non-canonical terms appear)     *)
  10.100  
  10.101 -ML {* bind_thms ("XHEs", XH_to_Es (thms "XHs")) *}
  10.102 +ML {* bind_thms ("XHEs", XH_to_Es @{thms XHs}) *}
  10.103  
  10.104  lemmas [intro!] = SubtypeI canTs icanTs
  10.105    and [elim!] = SubtypeE XHEs
  10.106 @@ -392,88 +392,103 @@
  10.107    by simp
  10.108  
  10.109  
  10.110 -(***)
  10.111 +ML {*
  10.112 +  val coinduct3_tac = SUBPROOF (fn {context = ctxt, prems = mono :: prems, ...} =>
  10.113 +    (fast_tac (claset_of ctxt addIs
  10.114 +        (mono RS @{thm coinduct3_mono_lemma} RS @{thm lfpI}) :: prems) 1));
  10.115 +*}
  10.116 +
  10.117 +method_setup coinduct3 = {*
  10.118 +  Scan.succeed (SIMPLE_METHOD' o coinduct3_tac)
  10.119 +*} ""
  10.120 +
  10.121 +lemma ci3_RI: "[| mono(Agen);  a : R |] ==> a : lfp(%x. Agen(x) Un R Un A)"
  10.122 +  by coinduct3
  10.123 +
  10.124 +lemma ci3_AgenI: "[| mono(Agen);  a : Agen(lfp(%x. Agen(x) Un R Un A)) |] ==>
  10.125 +    a : lfp(%x. Agen(x) Un R Un A)"
  10.126 +  by coinduct3
  10.127 +
  10.128 +lemma ci3_AI: "[| mono(Agen);  a : A |] ==> a : lfp(%x. Agen(x) Un R Un A)"
  10.129 +  by coinduct3
  10.130  
  10.131  ML {*
  10.132 -
  10.133 -local
  10.134 -  val lfpI = thm "lfpI"
  10.135 -  val coinduct3_mono_lemma = thm "coinduct3_mono_lemma"
  10.136 -  fun mk_thm s = prove_goal (the_context ()) s (fn mono::prems =>
  10.137 -       [fast_tac (@{claset} addIs ((mono RS coinduct3_mono_lemma RS lfpI)::prems)) 1])
  10.138 -in
  10.139 -val ci3_RI    = mk_thm "[|  mono(Agen);  a : R |] ==> a : lfp(%x. Agen(x) Un R Un A)"
  10.140 -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)"
  10.141 -val ci3_AI    = mk_thm "[|  mono(Agen);  a : A |] ==> a : lfp(%x. Agen(x) Un R Un A)"
  10.142 +fun genIs_tac ctxt genXH gen_mono =
  10.143 +  rtac (genXH RS iffD2) THEN'
  10.144 +  simp_tac (simpset_of ctxt) THEN'
  10.145 +  TRY o fast_tac (claset_of ctxt addIs
  10.146 +        [genXH RS iffD2, gen_mono RS @{thm coinduct3_mono_lemma} RS @{thm lfpI}])
  10.147 +*}
  10.148  
  10.149 -fun mk_genIs thy defs genXH gen_mono s = prove_goalw thy defs s
  10.150 -      (fn prems => [rtac (genXH RS iffD2) 1,
  10.151 -                    simp_tac (global_simpset_of thy) 1,
  10.152 -                    TRY (fast_tac (@{claset} addIs
  10.153 -                            ([genXH RS iffD2,gen_mono RS coinduct3_mono_lemma RS lfpI]
  10.154 -                             @ prems)) 1)])
  10.155 -end;
  10.156 -
  10.157 -bind_thm ("ci3_RI", ci3_RI);
  10.158 -bind_thm ("ci3_AgenI", ci3_AgenI);
  10.159 -bind_thm ("ci3_AI", ci3_AI);
  10.160 -*}
  10.161 +method_setup genIs = {*
  10.162 +  Attrib.thm -- Attrib.thm >> (fn (genXH, gen_mono) => fn ctxt =>
  10.163 +    SIMPLE_METHOD' (genIs_tac ctxt genXH gen_mono))
  10.164 +*} ""
  10.165  
  10.166  
  10.167  subsection {* POgen *}
  10.168  
  10.169  lemma PO_refl: "<a,a> : PO"
  10.170 -  apply (rule po_refl [THEN PO_iff [THEN iffD1]])
  10.171 -  done
  10.172 +  by (rule po_refl [THEN PO_iff [THEN iffD1]])
  10.173 +
  10.174 +lemma POgenIs:
  10.175 +  "<true,true> : POgen(R)"
  10.176 +  "<false,false> : POgen(R)"
  10.177 +  "[| <a,a'> : R;  <b,b'> : R |] ==> <<a,b>,<a',b'>> : POgen(R)"
  10.178 +  "!!b b'. [|!!x. <b(x),b'(x)> : R |] ==><lam x. b(x),lam x. b'(x)> : POgen(R)"
  10.179 +  "<one,one> : POgen(R)"
  10.180 +  "<a,a'> : lfp(%x. POgen(x) Un R Un PO) ==>
  10.181 +    <inl(a),inl(a')> : POgen(lfp(%x. POgen(x) Un R Un PO))"
  10.182 +  "<b,b'> : lfp(%x. POgen(x) Un R Un PO) ==>
  10.183 +    <inr(b),inr(b')> : POgen(lfp(%x. POgen(x) Un R Un PO))"
  10.184 +  "<zero,zero> : POgen(lfp(%x. POgen(x) Un R Un PO))"
  10.185 +  "<n,n'> : lfp(%x. POgen(x) Un R Un PO) ==>
  10.186 +    <succ(n),succ(n')> : POgen(lfp(%x. POgen(x) Un R Un PO))"
  10.187 +  "<[],[]> : POgen(lfp(%x. POgen(x) Un R Un PO))"
  10.188 +  "[| <h,h'> : lfp(%x. POgen(x) Un R Un PO);  <t,t'> : lfp(%x. POgen(x) Un R Un PO) |]
  10.189 +    ==> <h$t,h'$t'> : POgen(lfp(%x. POgen(x) Un R Un PO))"
  10.190 +  unfolding data_defs by (genIs POgenXH POgen_mono)+
  10.191  
  10.192  ML {*
  10.193 -
  10.194 -val POgenIs = map (mk_genIs @{theory} @{thms data_defs} @{thm POgenXH} @{thm POgen_mono})
  10.195 -  ["<true,true> : POgen(R)",
  10.196 -   "<false,false> : POgen(R)",
  10.197 -   "[| <a,a'> : R;  <b,b'> : R |] ==> <<a,b>,<a',b'>> : POgen(R)",
  10.198 -   "[|!!x. <b(x),b'(x)> : R |] ==><lam x. b(x),lam x. b'(x)> : POgen(R)",
  10.199 -   "<one,one> : POgen(R)",
  10.200 -   "<a,a'> : lfp(%x. POgen(x) Un R Un PO) ==> <inl(a),inl(a')> : POgen(lfp(%x. POgen(x) Un R Un PO))",
  10.201 -   "<b,b'> : lfp(%x. POgen(x) Un R Un PO) ==> <inr(b),inr(b')> : POgen(lfp(%x. POgen(x) Un R Un PO))",
  10.202 -   "<zero,zero> : POgen(lfp(%x. POgen(x) Un R Un PO))",
  10.203 -   "<n,n'> : lfp(%x. POgen(x) Un R Un PO) ==> <succ(n),succ(n')> : POgen(lfp(%x. POgen(x) Un R Un PO))",
  10.204 -   "<[],[]> : POgen(lfp(%x. POgen(x) Un R Un PO))",
  10.205 -   "[| <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))"];
  10.206 -
  10.207 -fun POgen_tac ctxt (rla,rlb) i =
  10.208 +fun POgen_tac ctxt (rla, rlb) i =
  10.209    SELECT_GOAL (safe_tac (claset_of ctxt)) i THEN
  10.210    rtac (rlb RS (rla RS @{thm ssubst_pair})) i THEN
  10.211 -  (REPEAT (resolve_tac (POgenIs @ [@{thm PO_refl} RS (@{thm POgen_mono} RS ci3_AI)] @
  10.212 -    (POgenIs RL [@{thm POgen_mono} RS ci3_AgenI]) @ [@{thm POgen_mono} RS ci3_RI]) i));
  10.213 -
  10.214 +  (REPEAT (resolve_tac
  10.215 +      (@{thms POgenIs} @ [@{thm PO_refl} RS (@{thm POgen_mono} RS @{thm ci3_AI})] @
  10.216 +        (@{thms POgenIs} RL [@{thm POgen_mono} RS @{thm ci3_AgenI}]) @
  10.217 +        [@{thm POgen_mono} RS @{thm ci3_RI}]) i))
  10.218  *}
  10.219  
  10.220  
  10.221  subsection {* EQgen *}
  10.222  
  10.223  lemma EQ_refl: "<a,a> : EQ"
  10.224 -  apply (rule refl [THEN EQ_iff [THEN iffD1]])
  10.225 -  done
  10.226 +  by (rule refl [THEN EQ_iff [THEN iffD1]])
  10.227 +
  10.228 +lemma EQgenIs:
  10.229 +  "<true,true> : EQgen(R)"
  10.230 +  "<false,false> : EQgen(R)"
  10.231 +  "[| <a,a'> : R;  <b,b'> : R |] ==> <<a,b>,<a',b'>> : EQgen(R)"
  10.232 +  "!!b b'. [|!!x. <b(x),b'(x)> : R |] ==> <lam x. b(x),lam x. b'(x)> : EQgen(R)"
  10.233 +  "<one,one> : EQgen(R)"
  10.234 +  "<a,a'> : lfp(%x. EQgen(x) Un R Un EQ) ==>
  10.235 +    <inl(a),inl(a')> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))"
  10.236 +  "<b,b'> : lfp(%x. EQgen(x) Un R Un EQ) ==>
  10.237 +    <inr(b),inr(b')> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))"
  10.238 +  "<zero,zero> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))"
  10.239 +  "<n,n'> : lfp(%x. EQgen(x) Un R Un EQ) ==>
  10.240 +    <succ(n),succ(n')> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))"
  10.241 +  "<[],[]> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))"
  10.242 +  "[| <h,h'> : lfp(%x. EQgen(x) Un R Un EQ); <t,t'> : lfp(%x. EQgen(x) Un R Un EQ) |]
  10.243 +    ==> <h$t,h'$t'> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))"
  10.244 +  unfolding data_defs by (genIs EQgenXH EQgen_mono)+
  10.245  
  10.246  ML {*
  10.247 -
  10.248 -val EQgenIs = map (mk_genIs @{theory} @{thms data_defs} @{thm EQgenXH} @{thm EQgen_mono})
  10.249 -  ["<true,true> : EQgen(R)",
  10.250 -   "<false,false> : EQgen(R)",
  10.251 -   "[| <a,a'> : R;  <b,b'> : R |] ==> <<a,b>,<a',b'>> : EQgen(R)",
  10.252 -   "[|!!x. <b(x),b'(x)> : R |] ==> <lam x. b(x),lam x. b'(x)> : EQgen(R)",
  10.253 -   "<one,one> : EQgen(R)",
  10.254 -   "<a,a'> : lfp(%x. EQgen(x) Un R Un EQ) ==> <inl(a),inl(a')> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))",
  10.255 -   "<b,b'> : lfp(%x. EQgen(x) Un R Un EQ) ==> <inr(b),inr(b')> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))",
  10.256 -   "<zero,zero> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))",
  10.257 -   "<n,n'> : lfp(%x. EQgen(x) Un R Un EQ) ==> <succ(n),succ(n')> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))",
  10.258 -   "<[],[]> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))",
  10.259 -   "[| <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))"];
  10.260 -
  10.261  fun EQgen_raw_tac i =
  10.262 -  (REPEAT (resolve_tac (EQgenIs @ [@{thm EQ_refl} RS (@{thm EQgen_mono} RS ci3_AI)] @
  10.263 -    (EQgenIs RL [@{thm EQgen_mono} RS ci3_AgenI]) @ [@{thm EQgen_mono} RS ci3_RI]) i))
  10.264 +  (REPEAT (resolve_tac (@{thms EQgenIs} @
  10.265 +        [@{thm EQ_refl} RS (@{thm EQgen_mono} RS @{thm ci3_AI})] @
  10.266 +        (@{thms EQgenIs} RL [@{thm EQgen_mono} RS @{thm ci3_AgenI}]) @
  10.267 +        [@{thm EQgen_mono} RS @{thm ci3_RI}]) i))
  10.268  
  10.269  (* Goals of the form R <= EQgen(R) - rewrite elements <a,b> : EQgen(R) using rews and *)
  10.270  (* then reduce this to a goal <a',b'> : R (hopefully?)                                *)
  10.271 @@ -482,7 +497,7 @@
  10.272  fun EQgen_tac ctxt rews i =
  10.273   SELECT_GOAL
  10.274     (TRY (safe_tac (claset_of ctxt)) THEN
  10.275 -    resolve_tac ((rews@[refl]) RL ((rews@[refl]) RL [@{thm ssubst_pair}])) i THEN
  10.276 +    resolve_tac ((rews @ [refl]) RL ((rews @ [refl]) RL [@{thm ssubst_pair}])) i THEN
  10.277      ALLGOALS (simp_tac (simpset_of ctxt)) THEN
  10.278      ALLGOALS EQgen_raw_tac) i
  10.279  *}
    11.1 --- a/src/CCL/ex/Flag.thy	Thu Jul 23 20:05:20 2009 +0200
    11.2 +++ b/src/CCL/ex/Flag.thy	Thu Jul 23 21:59:56 2009 +0200
    11.3 @@ -1,5 +1,4 @@
    11.4  (*  Title:      CCL/ex/Flag.thy
    11.5 -    ID:         $Id$
    11.6      Author:     Martin Coen, Cambridge University Computer Laboratory
    11.7      Copyright   1993  University of Cambridge
    11.8  *)
    11.9 @@ -55,12 +54,10 @@
   11.10    and blueT: "blue : Colour"
   11.11    unfolding ColourXH by blast+
   11.12  
   11.13 -ML {*
   11.14 -bind_thm ("ccaseT", mk_ncanT_tac @{context}
   11.15 -  @{thms flag_defs} @{thms case_rls} @{thms case_rls}
   11.16 -  "[| c:Colour; c=red ==> r : C(red); c=white ==> w : C(white); c=blue ==> b : C(blue) |] ==> ccase(c,r,w,b) : C(c)");
   11.17 -*}
   11.18 -
   11.19 +lemma ccaseT:
   11.20 +  "[| c:Colour; c=red ==> r : C(red); c=white ==> w : C(white); c=blue ==> b : C(blue) |]
   11.21 +    ==> ccase(c,r,w,b) : C(c)"
   11.22 +  unfolding flag_defs by ncanT
   11.23  
   11.24  lemma "flag : List(Colour)->List(Colour)*List(Colour)*List(Colour)"
   11.25    apply (unfold flag_def)