--- 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}))
*}
--- 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
--- 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 *}
--- 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
--- 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]])
--- 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
--- 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