# HG changeset patch
# User wenzelm
# Date 1415699692 -3600
# Node ID 8c9a319821b391f6afffd0e87d67c2707ef12ce3
# Parent  a62cdcc5344b02a7e6acc0096b5ed98874d19348
more Isar proof methods;

diff -r a62cdcc5344b -r 8c9a319821b3 src/CCL/CCL.thy
--- a/src/CCL/CCL.thy	Tue Nov 11 08:57:46 2014 +0100
+++ b/src/CCL/CCL.thy	Tue Nov 11 10:54:52 2014 +0100
@@ -418,12 +418,8 @@
   "~ <a,b> [= false"
   "~ false [= lam x. f(x)"
   "~ lam x. f(x) [= false"
-  by (tactic {*
-    REPEAT (rtac @{thm notI} 1 THEN
-      dtac @{thm case_pocong} 1 THEN
-      etac @{thm rev_mp} 5 THEN
-      ALLGOALS (simp_tac @{context}) THEN
-      REPEAT (resolve_tac [@{thm po_refl}, @{thm npo_lam_bot}] 1)) *})
+  by (rule notI, drule case_pocong, erule_tac [5] rev_mp, simp_all,
+    (rule po_refl npo_lam_bot)+)+
 
 lemmas npo_rls = npo_pair_lam npo_lam_pair npo_rls1
 
@@ -476,9 +472,9 @@
   apply (rule EQgen_mono | assumption)+
   done
 
-ML {*
-  fun eq_coinduct_tac ctxt s i = res_inst_tac ctxt [(("R", 0), s)] @{thm eq_coinduct} i
-  fun eq_coinduct3_tac ctxt s i = res_inst_tac ctxt [(("R", 0), s)] @{thm eq_coinduct3} i
+method_setup eq_coinduct3 = {*
+  Scan.lift Args.name >> (fn s => fn ctxt =>
+    SIMPLE_METHOD' (res_inst_tac ctxt [(("R", 0), s)] @{thm eq_coinduct3}))
 *}
 
 
diff -r a62cdcc5344b -r 8c9a319821b3 src/CCL/Type.thy
--- a/src/CCL/Type.thy	Tue Nov 11 08:57:46 2014 +0100
+++ b/src/CCL/Type.thy	Tue Nov 11 10:54:52 2014 +0100
@@ -502,4 +502,8 @@
     ALLGOALS EQgen_raw_tac) i
 *}
 
+method_setup EQgen = {*
+  Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (EQgen_tac ctxt ths))
+*}
+
 end
diff -r a62cdcc5344b -r 8c9a319821b3 src/CCL/Wfd.thy
--- a/src/CCL/Wfd.thy	Tue Nov 11 08:57:46 2014 +0100
+++ b/src/CCL/Wfd.thy	Tue Nov 11 10:54:52 2014 +0100
@@ -46,9 +46,10 @@
   apply blast
   done
 
-ML {*
-  fun wfd_strengthen_tac ctxt s i =
-    res_inst_tac ctxt [(("Q", 0), s)] @{thm wfd_strengthen_lemma} i THEN assume_tac ctxt (i+1)
+method_setup wfd_strengthen = {*
+  Scan.lift Args.name >> (fn s => fn ctxt =>
+    SIMPLE_METHOD' (fn i =>
+      res_inst_tac ctxt [(("Q", 0), s)] @{thm wfd_strengthen_lemma} i THEN assume_tac ctxt (i+1)))
 *}
 
 lemma wf_anti_sym: "[| Wfd(r);  <a,x>:r;  <x,a>:r |] ==> P"
@@ -116,7 +117,7 @@
   shows "Wfd(R**S)"
   apply (unfold Wfd_def)
   apply safe
-  apply (tactic {* wfd_strengthen_tac @{context} "%x. EX a b. x=<a,b>" 1 *})
+  apply (wfd_strengthen "%x. EX a b. x=<a,b>")
    apply (blast elim!: lex_pair)
   apply (subgoal_tac "ALL a b.<a,b>:P")
    apply blast
@@ -202,7 +203,7 @@
 lemma NatPR_wf: "Wfd(NatPR)"
   apply (unfold Wfd_def)
   apply clarify
-  apply (tactic {* wfd_strengthen_tac @{context} "%x. x:Nat" 1 *})
+  apply (wfd_strengthen "%x. x:Nat")
    apply (fastforce iff: NatPRXH)
   apply (erule Nat_ind)
    apply (fastforce iff: NatPRXH)+
@@ -211,7 +212,7 @@
 lemma ListPR_wf: "Wfd(ListPR(A))"
   apply (unfold Wfd_def)
   apply clarify
-  apply (tactic {* wfd_strengthen_tac @{context} "%x. x:List (A)" 1 *})
+  apply (wfd_strengthen "%x. x:List (A)")
    apply (fastforce iff: ListPRXH)
   apply (erule List_ind)
    apply (fastforce iff: ListPRXH)+
@@ -481,6 +482,18 @@
 end
 *}
 
+method_setup typechk = {*
+  Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (typechk_tac ctxt ths))
+*}
+
+method_setup clean_ccs = {*
+  Scan.succeed (SIMPLE_METHOD o clean_ccs_tac)
+*}
+
+method_setup gen_ccs = {*
+  Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (gen_ccs_tac ctxt ths))
+*}
+
 
 subsection {* Evaluation *}
 
diff -r a62cdcc5344b -r 8c9a319821b3 src/CCL/ex/Flag.thy
--- a/src/CCL/ex/Flag.thy	Tue Nov 11 08:57:46 2014 +0100
+++ b/src/CCL/ex/Flag.thy	Tue Nov 11 10:54:52 2014 +0100
@@ -62,17 +62,15 @@
 
 lemma "flag : List(Colour)->List(Colour)*List(Colour)*List(Colour)"
   apply (unfold flag_def)
-  apply (tactic {* typechk_tac @{context}
-    [@{thm redT}, @{thm whiteT}, @{thm blueT}, @{thm ccaseT}] 1 *})
-  apply (tactic "clean_ccs_tac @{context}")
+  apply (typechk redT whiteT blueT ccaseT)
+  apply clean_ccs
   apply (erule ListPRI [THEN ListPR_wf [THEN wfI]])
   apply assumption
   done
 
 lemma "flag : PROD l:List(Colour).{x:List(Colour)*List(Colour)*List(Colour).Flag(x,l)}"
   apply (unfold flag_def)
-  apply (tactic {* gen_ccs_tac @{context}
-    [@{thm redT}, @{thm whiteT}, @{thm blueT}, @{thm ccaseT}] 1 *})
+  apply (gen_ccs redT whiteT blueT ccaseT)
   oops
 
 end
diff -r a62cdcc5344b -r 8c9a319821b3 src/CCL/ex/List.thy
--- a/src/CCL/ex/List.thy	Tue Nov 11 08:57:46 2014 +0100
+++ b/src/CCL/ex/List.thy	Tue Nov 11 10:54:52 2014 +0100
@@ -75,13 +75,13 @@
 
 lemma mapT: "[| !!x. x:A==>f(x):B;  l : List(A) |] ==> map(f,l) : List(B)"
   apply (unfold map_def)
-  apply (tactic "typechk_tac @{context} [] 1")
+  apply typechk
   apply blast
   done
 
 lemma appendT: "[| l : List(A);  m : List(A) |] ==> l @ m : List(A)"
   apply (unfold append_def)
-  apply (tactic "typechk_tac @{context} [] 1")
+  apply typechk
   done
 
 lemma appendTS:
@@ -90,17 +90,17 @@
 
 lemma filterT: "[| f:A->Bool;   l : List(A) |] ==> filter(f,l) : List(A)"
   apply (unfold filter_def)
-  apply (tactic "typechk_tac @{context} [] 1")
+  apply typechk
   done
 
 lemma flatT: "l : List(List(A)) ==> flat(l) : List(A)"
   apply (unfold flat_def)
-  apply (tactic {* typechk_tac @{context} @{thms appendT} 1 *})
+  apply (typechk appendT)
   done
 
 lemma insertT: "[|  f : A->A->Bool; a:A; l : List(A) |] ==> insert(f,a,l) : List(A)"
   apply (unfold insert_def)
-  apply (tactic "typechk_tac @{context} [] 1")
+  apply typechk
   done
 
 lemma insertTS:
@@ -111,8 +111,8 @@
 lemma partitionT:
   "[| f:A->Bool;  l : List(A) |] ==> partition(f,l) : List(A)*List(A)"
   apply (unfold partition_def)
-  apply (tactic "typechk_tac @{context} [] 1")
-  apply (tactic "clean_ccs_tac @{context}")
+  apply typechk
+  apply clean_ccs
   apply (rule ListPRI [THEN wfstI, THEN ListPR_wf [THEN wmap_wf, THEN wfI]])
     apply assumption+
   apply (rule ListPRI [THEN wfstI, THEN ListPR_wf [THEN wmap_wf, THEN wfI]])
diff -r a62cdcc5344b -r 8c9a319821b3 src/CCL/ex/Nat.thy
--- a/src/CCL/ex/Nat.thy	Tue Nov 11 08:57:46 2014 +0100
+++ b/src/CCL/ex/Nat.thy	Tue Nov 11 10:54:52 2014 +0100
@@ -67,32 +67,32 @@
 
 lemma addT: "[| a:Nat;  b:Nat |] ==> a #+ b : Nat"
   apply (unfold add_def)
-  apply (tactic {* typechk_tac @{context} [] 1 *})
+  apply typechk
   done
 
 lemma multT: "[| a:Nat;  b:Nat |] ==> a #* b : Nat"
   apply (unfold add_def mult_def)
-  apply (tactic {* typechk_tac @{context} [] 1 *})
+  apply typechk
   done
 
 (* Defined to return zero if a<b *)
 lemma subT: "[| a:Nat;  b:Nat |] ==> a #- b : Nat"
   apply (unfold sub_def)
-  apply (tactic {* typechk_tac @{context} [] 1 *})
-  apply (tactic {* clean_ccs_tac @{context} *})
+  apply typechk
+  apply clean_ccs
   apply (erule NatPRI [THEN wfstI, THEN NatPR_wf [THEN wmap_wf, THEN wfI]])
   done
 
 lemma leT: "[| a:Nat;  b:Nat |] ==> a #<= b : Bool"
   apply (unfold le_def)
-  apply (tactic {* typechk_tac @{context} [] 1 *})
-  apply (tactic {* clean_ccs_tac @{context} *})
+  apply typechk
+  apply clean_ccs
   apply (erule NatPRI [THEN wfstI, THEN NatPR_wf [THEN wmap_wf, THEN wfI]])
   done
 
 lemma ltT: "[| a:Nat;  b:Nat |] ==> a #< b : Bool"
   apply (unfold not_def lt_def)
-  apply (tactic {* typechk_tac @{context} @{thms leT} 1 *})
+  apply (typechk leT)
   done
 
 
@@ -102,7 +102,7 @@
 
 lemma "[| a:Nat;  b:Nat |] ==> ackermann(a,b) : Nat"
   apply (unfold ackermann_def)
-  apply (tactic {* gen_ccs_tac @{context} [] 1 *})
+  apply gen_ccs
   apply (erule NatPRI [THEN lexI1 [THEN relI]] NatPRI [THEN lexI2 [THEN relI]])+
   done
 
diff -r a62cdcc5344b -r 8c9a319821b3 src/CCL/ex/Stream.thy
--- a/src/CCL/ex/Stream.thy	Tue Nov 11 08:57:46 2014 +0100
+++ b/src/CCL/ex/Stream.thy	Tue Nov 11 10:54:52 2014 +0100
@@ -27,12 +27,11 @@
 lemma map_comp:
   assumes 1: "l:Lists(A)"
   shows "map(f \<circ> g,l) = map(f,map(g,l))"
-  apply (tactic {* eq_coinduct3_tac @{context}
-    "{p. EX x y. p=<x,y> & (EX l:Lists (A) .x=map (f \<circ> g,l) & y=map (f,map (g,l)))}" 1 *})
+  apply (eq_coinduct3 "{p. EX x y. p=<x,y> & (EX l:Lists (A) .x=map (f \<circ> g,l) & y=map (f,map (g,l)))}")
    apply (blast intro: 1)
   apply safe
   apply (drule ListsXH [THEN iffD1])
-  apply (tactic "EQgen_tac @{context} [] 1")
+  apply EQgen
    apply fastforce
   done
 
@@ -41,12 +40,11 @@
 lemma map_id:
   assumes 1: "l:Lists(A)"
   shows "map(%x. x,l) = l"
-  apply (tactic {* eq_coinduct3_tac @{context}
-    "{p. EX x y. p=<x,y> & (EX l:Lists (A) .x=map (%x. x,l) & y=l) }" 1 *})
+  apply (eq_coinduct3 "{p. EX x y. p=<x,y> & (EX l:Lists (A) .x=map (%x. x,l) & y=l) }")
   apply (blast intro: 1)
   apply safe
   apply (drule ListsXH [THEN iffD1])
-  apply (tactic "EQgen_tac @{context} [] 1")
+  apply EQgen
   apply blast
   done
 
@@ -57,14 +55,14 @@
   assumes "l:Lists(A)"
     and "m:Lists(A)"
   shows "map(f,l@m) = map(f,l) @ map(f,m)"
-  apply (tactic {* eq_coinduct3_tac @{context}
-    "{p. EX x y. p=<x,y> & (EX l:Lists (A). EX m:Lists (A). x=map (f,l@m) & y=map (f,l) @ map (f,m))}" 1 *})
+  apply (eq_coinduct3
+    "{p. EX x y. p=<x,y> & (EX l:Lists (A). EX m:Lists (A). x=map (f,l@m) & y=map (f,l) @ map (f,m))}")
   apply (blast intro: assms)
   apply safe
   apply (drule ListsXH [THEN iffD1])
-  apply (tactic "EQgen_tac @{context} [] 1")
+  apply EQgen
   apply (drule ListsXH [THEN iffD1])
-  apply (tactic "EQgen_tac @{context} [] 1")
+  apply EQgen
   apply blast
   done
 
@@ -76,12 +74,12 @@
     and "l:Lists(A)"
     and "m:Lists(A)"
   shows "k @ l @ m = (k @ l) @ m"
-  apply (tactic {* eq_coinduct3_tac @{context}
-    "{p. EX x y. p=<x,y> & (EX k:Lists (A). EX l:Lists (A). EX m:Lists (A). x=k @ l @ m & y= (k @ l) @ m) }" 1*})
+  apply (eq_coinduct3
+    "{p. EX x y. p=<x,y> & (EX k:Lists (A). EX l:Lists (A). EX m:Lists (A). x=k @ l @ m & y= (k @ l) @ m) }")
   apply (blast intro: assms)
   apply safe
   apply (drule ListsXH [THEN iffD1])
-  apply (tactic "EQgen_tac @{context} [] 1")
+  apply EQgen
    prefer 2
    apply blast
   apply (tactic {* DEPTH_SOLVE (etac (XH_to_E @{thm ListsXH}) 1
@@ -94,12 +92,11 @@
 lemma ilist_append:
   assumes "l:ILists(A)"
   shows "l @ m = l"
-  apply (tactic {* eq_coinduct3_tac @{context}
-    "{p. EX x y. p=<x,y> & (EX l:ILists (A) .EX m. x=l@m & y=l)}" 1 *})
+  apply (eq_coinduct3 "{p. EX x y. p=<x,y> & (EX l:ILists (A) .EX m. x=l@m & y=l)}")
   apply (blast intro: assms)
   apply safe
   apply (drule IListsXH [THEN iffD1])
-  apply (tactic "EQgen_tac @{context} [] 1")
+  apply EQgen
   apply blast
   done
 
@@ -128,10 +125,10 @@
   done
 
 lemma iter1_iter2_eq: "iter1(f,a) = iter2(f,a)"
-  apply (tactic {* eq_coinduct3_tac @{context}
-    "{p. EX x y. p=<x,y> & (EX n:Nat. x=iter1 (f,f^n`a) & y=map (f) ^n`iter2 (f,a))}" 1*})
+  apply (eq_coinduct3
+    "{p. EX x y. p=<x,y> & (EX n:Nat. x=iter1 (f,f^n`a) & y=map (f) ^n`iter2 (f,a))}")
   apply (fast intro!: napplyBzero [symmetric] napplyBzero [symmetric, THEN arg_cong])
-  apply (tactic {* EQgen_tac @{context} [@{thm iter1B}, @{thm iter2Blemma}] 1 *})
+  apply (EQgen iter1B iter2Blemma)
   apply (subst napply_f, assumption)
   apply (rule_tac f1 = f in napplyBsucc [THEN subst])
   apply blast