--- a/src/CTT/Arith.thy Tue Nov 11 10:54:52 2014 +0100
+++ b/src/CTT/Arith.thy Tue Nov 11 11:41:58 2014 +0100
@@ -54,12 +54,12 @@
lemma add_typing: "[| a:N; b:N |] ==> a #+ b : N"
apply (unfold arith_defs)
-apply (tactic "typechk_tac @{context} []")
+apply typechk
done
lemma add_typingL: "[| a=c:N; b=d:N |] ==> a #+ b = c #+ d : N"
apply (unfold arith_defs)
-apply (tactic "equal_tac @{context} []")
+apply equal
done
@@ -67,12 +67,12 @@
lemma addC0: "b:N ==> 0 #+ b = b : N"
apply (unfold arith_defs)
-apply (tactic "rew_tac @{context} []")
+apply rew
done
lemma addC_succ: "[| a:N; b:N |] ==> succ(a) #+ b = succ(a #+ b) : N"
apply (unfold arith_defs)
-apply (tactic "rew_tac @{context} []")
+apply rew
done
@@ -82,24 +82,24 @@
lemma mult_typing: "[| a:N; b:N |] ==> a #* b : N"
apply (unfold arith_defs)
-apply (tactic {* typechk_tac @{context} [@{thm add_typing}] *})
+apply (typechk add_typing)
done
lemma mult_typingL: "[| a=c:N; b=d:N |] ==> a #* b = c #* d : N"
apply (unfold arith_defs)
-apply (tactic {* equal_tac @{context} [@{thm add_typingL}] *})
+apply (equal add_typingL)
done
(*computation for mult: 0 and successor cases*)
lemma multC0: "b:N ==> 0 #* b = 0 : N"
apply (unfold arith_defs)
-apply (tactic "rew_tac @{context} []")
+apply rew
done
lemma multC_succ: "[| a:N; b:N |] ==> succ(a) #* b = b #+ (a #* b) : N"
apply (unfold arith_defs)
-apply (tactic "rew_tac @{context} []")
+apply rew
done
@@ -109,12 +109,12 @@
lemma diff_typing: "[| a:N; b:N |] ==> a - b : N"
apply (unfold arith_defs)
-apply (tactic "typechk_tac @{context} []")
+apply typechk
done
lemma diff_typingL: "[| a=c:N; b=d:N |] ==> a - b = c - d : N"
apply (unfold arith_defs)
-apply (tactic "equal_tac @{context} []")
+apply equal
done
@@ -122,15 +122,15 @@
lemma diffC0: "a:N ==> a - 0 = a : N"
apply (unfold arith_defs)
-apply (tactic "rew_tac @{context} []")
+apply rew
done
(*Note: rec(a, 0, %z w.z) is pred(a). *)
lemma diff_0_eq_0: "b:N ==> 0 - b = 0 : N"
apply (unfold arith_defs)
-apply (tactic {* NE_tac @{context} "b" 1 *})
-apply (tactic "hyp_rew_tac @{context} []")
+apply (NE b)
+apply hyp_rew
done
@@ -138,9 +138,9 @@
succ(a) - succ(b) rewrites to pred(succ(a) - b) *)
lemma diff_succ_succ: "[| a:N; b:N |] ==> succ(a) - succ(b) = a - b : N"
apply (unfold arith_defs)
-apply (tactic "hyp_rew_tac @{context} []")
-apply (tactic {* NE_tac @{context} "b" 1 *})
-apply (tactic "hyp_rew_tac @{context} []")
+apply hyp_rew
+apply (NE b)
+apply hyp_rew
done
@@ -182,25 +182,35 @@
end
*}
+method_setup arith_rew = {*
+ Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD (arith_rew_tac ctxt ths))
+*}
+
+method_setup hyp_arith_rew = {*
+ Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD (hyp_arith_rew_tac ctxt ths))
+*}
+
subsection {* Addition *}
(*Associative law for addition*)
lemma add_assoc: "[| a:N; b:N; c:N |] ==> (a #+ b) #+ c = a #+ (b #+ c) : N"
-apply (tactic {* NE_tac @{context} "a" 1 *})
-apply (tactic "hyp_arith_rew_tac @{context} []")
+apply (NE a)
+apply hyp_arith_rew
done
(*Commutative law for addition. Can be proved using three inductions.
Must simplify after first induction! Orientation of rewrites is delicate*)
lemma add_commute: "[| a:N; b:N |] ==> a #+ b = b #+ a : N"
-apply (tactic {* NE_tac @{context} "a" 1 *})
-apply (tactic "hyp_arith_rew_tac @{context} []")
-apply (tactic {* NE_tac @{context} "b" 2 *})
+apply (NE a)
+apply hyp_arith_rew
apply (rule sym_elem)
-apply (tactic {* NE_tac @{context} "b" 1 *})
-apply (tactic "hyp_arith_rew_tac @{context} []")
+prefer 2
+apply (NE b)
+prefer 4
+apply (NE b)
+apply hyp_arith_rew
done
@@ -208,33 +218,33 @@
(*right annihilation in product*)
lemma mult_0_right: "a:N ==> a #* 0 = 0 : N"
-apply (tactic {* NE_tac @{context} "a" 1 *})
-apply (tactic "hyp_arith_rew_tac @{context} []")
+apply (NE a)
+apply hyp_arith_rew
done
(*right successor law for multiplication*)
lemma mult_succ_right: "[| a:N; b:N |] ==> a #* succ(b) = a #+ (a #* b) : N"
-apply (tactic {* NE_tac @{context} "a" 1 *})
-apply (tactic {* hyp_arith_rew_tac @{context} [@{thm add_assoc} RS @{thm sym_elem}] *})
+apply (NE a)
+apply (hyp_arith_rew add_assoc [THEN sym_elem])
apply (assumption | rule add_commute mult_typingL add_typingL intrL_rls refl_elem)+
done
(*Commutative law for multiplication*)
lemma mult_commute: "[| a:N; b:N |] ==> a #* b = b #* a : N"
-apply (tactic {* NE_tac @{context} "a" 1 *})
-apply (tactic {* hyp_arith_rew_tac @{context} [@{thm mult_0_right}, @{thm mult_succ_right}] *})
+apply (NE a)
+apply (hyp_arith_rew mult_0_right mult_succ_right)
done
(*addition distributes over multiplication*)
lemma add_mult_distrib: "[| a:N; b:N; c:N |] ==> (a #+ b) #* c = (a #* c) #+ (b #* c) : N"
-apply (tactic {* NE_tac @{context} "a" 1 *})
-apply (tactic {* hyp_arith_rew_tac @{context} [@{thm add_assoc} RS @{thm sym_elem}] *})
+apply (NE a)
+apply (hyp_arith_rew add_assoc [THEN sym_elem])
done
(*Associative law for multiplication*)
lemma mult_assoc: "[| a:N; b:N; c:N |] ==> (a #* b) #* c = a #* (b #* c) : N"
-apply (tactic {* NE_tac @{context} "a" 1 *})
-apply (tactic {* hyp_arith_rew_tac @{context} [@{thm add_mult_distrib}] *})
+apply (NE a)
+apply (hyp_arith_rew add_mult_distrib)
done
@@ -245,8 +255,8 @@
a - b = 0 iff a<=b a - b = succ(c) iff a>b *}
lemma diff_self_eq_0: "a:N ==> a - a = 0 : N"
-apply (tactic {* NE_tac @{context} "a" 1 *})
-apply (tactic "hyp_arith_rew_tac @{context} []")
+apply (NE a)
+apply hyp_arith_rew
done
@@ -258,20 +268,22 @@
Uses rewriting with a quantified, implicative inductive hypothesis.*)
schematic_lemma add_diff_inverse_lemma:
"b:N ==> ?a : PROD x:N. Eq(N, b-x, 0) --> Eq(N, b #+ (x-b), x)"
-apply (tactic {* NE_tac @{context} "b" 1 *})
+apply (NE b)
(*strip one "universal quantifier" but not the "implication"*)
apply (rule_tac [3] intr_rls)
(*case analysis on x in
(succ(u) <= x) --> (succ(u)#+(x-succ(u)) = x) *)
-apply (tactic {* NE_tac @{context} "x" 4 *}, tactic "assume_tac @{context} 4")
+prefer 4
+apply (NE x)
+apply assumption
(*Prepare for simplification of types -- the antecedent succ(u)<=x *)
-apply (rule_tac [5] replace_type)
-apply (rule_tac [4] replace_type)
-apply (tactic "arith_rew_tac @{context} []")
+apply (rule_tac [2] replace_type)
+apply (rule_tac [1] replace_type)
+apply arith_rew
(*Solves first 0 goal, simplifies others. Two sugbgoals remain.
Both follow by rewriting, (2) using quantified induction hyp*)
-apply (tactic "intr_tac @{context} []") (*strips remaining PRODs*)
-apply (tactic {* hyp_arith_rew_tac @{context} [@{thm add_0_right}] *})
+apply intr (*strips remaining PRODs*)
+apply (hyp_arith_rew add_0_right)
apply assumption
done
@@ -293,46 +305,46 @@
lemma absdiff_typing: "[| a:N; b:N |] ==> a |-| b : N"
apply (unfold arith_defs)
-apply (tactic "typechk_tac @{context} []")
+apply typechk
done
lemma absdiff_typingL: "[| a=c:N; b=d:N |] ==> a |-| b = c |-| d : N"
apply (unfold arith_defs)
-apply (tactic "equal_tac @{context} []")
+apply equal
done
lemma absdiff_self_eq_0: "a:N ==> a |-| a = 0 : N"
apply (unfold absdiff_def)
-apply (tactic {* arith_rew_tac @{context} [@{thm diff_self_eq_0}] *})
+apply (arith_rew diff_self_eq_0)
done
lemma absdiffC0: "a:N ==> 0 |-| a = a : N"
apply (unfold absdiff_def)
-apply (tactic "hyp_arith_rew_tac @{context} []")
+apply hyp_arith_rew
done
lemma absdiff_succ_succ: "[| a:N; b:N |] ==> succ(a) |-| succ(b) = a |-| b : N"
apply (unfold absdiff_def)
-apply (tactic "hyp_arith_rew_tac @{context} []")
+apply hyp_arith_rew
done
(*Note how easy using commutative laws can be? ...not always... *)
lemma absdiff_commute: "[| a:N; b:N |] ==> a |-| b = b |-| a : N"
apply (unfold absdiff_def)
apply (rule add_commute)
-apply (tactic {* typechk_tac @{context} [@{thm diff_typing}] *})
+apply (typechk diff_typing)
done
(*If a+b=0 then a=0. Surprisingly tedious*)
schematic_lemma add_eq0_lemma: "[| a:N; b:N |] ==> ?c : PROD u: Eq(N,a#+b,0) . Eq(N,a,0)"
-apply (tactic {* NE_tac @{context} "a" 1 *})
+apply (NE a)
apply (rule_tac [3] replace_type)
-apply (tactic "arith_rew_tac @{context} []")
-apply (tactic "intr_tac @{context} []") (*strips remaining PRODs*)
+apply arith_rew
+apply intr (*strips remaining PRODs*)
apply (rule_tac [2] zero_ne_succ [THEN FE])
apply (erule_tac [3] EqE [THEN sym_elem])
-apply (tactic {* typechk_tac @{context} [@{thm add_typing}] *})
+apply (typechk add_typing)
done
(*Version of above with the premise a+b=0.
@@ -341,7 +353,7 @@
apply (rule EqE)
apply (rule add_eq0_lemma [THEN ProdE])
apply (rule_tac [3] EqI)
-apply (tactic "typechk_tac @{context} []")
+apply typechk
done
(*Here is a lemma to infer a-b=0 and b-a=0 from a|-|b=0, below. *)
@@ -349,12 +361,12 @@
"[| a:N; b:N; a |-| b = 0 : N |] ==>
?a : SUM v: Eq(N, a-b, 0) . Eq(N, b-a, 0)"
apply (unfold absdiff_def)
-apply (tactic "intr_tac @{context} []")
-apply (tactic "eqintr_tac @{context}")
+apply intr
+apply eqintr
apply (rule_tac [2] add_eq0)
apply (rule add_eq0)
apply (rule_tac [6] add_commute [THEN trans_elem])
-apply (tactic {* typechk_tac @{context} [@{thm diff_typing}] *})
+apply (typechk diff_typing)
done
(*if a |-| b = 0 then a = b
@@ -362,11 +374,10 @@
lemma absdiff_eq0: "[| a |-| b = 0 : N; a:N; b:N |] ==> a = b : N"
apply (rule EqE)
apply (rule absdiff_eq0_lem [THEN SumE])
-apply (tactic "TRYALL (assume_tac @{context})")
-apply (tactic "eqintr_tac @{context}")
+apply eqintr
apply (rule add_diff_inverse [THEN sym_elem, THEN trans_elem])
-apply (rule_tac [3] EqE, tactic "assume_tac @{context} 3")
-apply (tactic {* hyp_arith_rew_tac @{context} [@{thm add_0_right}] *})
+apply (erule_tac [3] EqE)
+apply (hyp_arith_rew add_0_right)
done
@@ -376,12 +387,12 @@
lemma mod_typing: "[| a:N; b:N |] ==> a mod b : N"
apply (unfold mod_def)
-apply (tactic {* typechk_tac @{context} [@{thm absdiff_typing}] *})
+apply (typechk absdiff_typing)
done
lemma mod_typingL: "[| a=c:N; b=d:N |] ==> a mod b = c mod d : N"
apply (unfold mod_def)
-apply (tactic {* equal_tac @{context} [@{thm absdiff_typingL}] *})
+apply (equal absdiff_typingL)
done
@@ -389,13 +400,13 @@
lemma modC0: "b:N ==> 0 mod b = 0 : N"
apply (unfold mod_def)
-apply (tactic {* rew_tac @{context} [@{thm absdiff_typing}] *})
+apply (rew absdiff_typing)
done
lemma modC_succ:
"[| a:N; b:N |] ==> succ(a) mod b = rec(succ(a mod b) |-| b, 0, %x y. succ(a mod b)) : N"
apply (unfold mod_def)
-apply (tactic {* rew_tac @{context} [@{thm absdiff_typing}] *})
+apply (rew absdiff_typing)
done
@@ -403,12 +414,12 @@
lemma div_typing: "[| a:N; b:N |] ==> a div b : N"
apply (unfold div_def)
-apply (tactic {* typechk_tac @{context} [@{thm absdiff_typing}, @{thm mod_typing}] *})
+apply (typechk absdiff_typing mod_typing)
done
lemma div_typingL: "[| a=c:N; b=d:N |] ==> a div b = c div d : N"
apply (unfold div_def)
-apply (tactic {* equal_tac @{context} [@{thm absdiff_typingL}, @{thm mod_typingL}] *})
+apply (equal absdiff_typingL mod_typingL)
done
lemmas div_typing_rls = mod_typing div_typing absdiff_typing
@@ -418,14 +429,14 @@
lemma divC0: "b:N ==> 0 div b = 0 : N"
apply (unfold div_def)
-apply (tactic {* rew_tac @{context} [@{thm mod_typing}, @{thm absdiff_typing}] *})
+apply (rew mod_typing absdiff_typing)
done
lemma divC_succ:
"[| a:N; b:N |] ==> succ(a) div b =
rec(succ(a) mod b, succ(a div b), %x y. a div b) : N"
apply (unfold div_def)
-apply (tactic {* rew_tac @{context} [@{thm mod_typing}] *})
+apply (rew mod_typing)
done
@@ -433,37 +444,35 @@
lemma divC_succ2: "[| a:N; b:N |] ==>
succ(a) div b =rec(succ(a mod b) |-| b, succ(a div b), %x y. a div b) : N"
apply (rule divC_succ [THEN trans_elem])
-apply (tactic {* rew_tac @{context} (@{thms div_typing_rls} @ [@{thm modC_succ}]) *})
-apply (tactic {* NE_tac @{context} "succ (a mod b) |-|b" 1 *})
-apply (tactic {* rew_tac @{context} [@{thm mod_typing}, @{thm div_typing}, @{thm absdiff_typing}] *})
+apply (rew div_typing_rls modC_succ)
+apply (NE "succ (a mod b) |-|b")
+apply (rew mod_typing div_typing absdiff_typing)
done
(*for case analysis on whether a number is 0 or a successor*)
lemma iszero_decidable: "a:N ==> rec(a, inl(eq), %ka kb. inr(<ka, eq>)) :
Eq(N,a,0) + (SUM x:N. Eq(N,a, succ(x)))"
-apply (tactic {* NE_tac @{context} "a" 1 *})
+apply (NE a)
apply (rule_tac [3] PlusI_inr)
apply (rule_tac [2] PlusI_inl)
-apply (tactic "eqintr_tac @{context}")
-apply (tactic "equal_tac @{context} []")
+apply eqintr
+apply equal
done
(*Main Result. Holds when b is 0 since a mod 0 = a and a div 0 = 0 *)
lemma mod_div_equality: "[| a:N; b:N |] ==> a mod b #+ (a div b) #* b = a : N"
-apply (tactic {* NE_tac @{context} "a" 1 *})
-apply (tactic {* arith_rew_tac @{context} (@{thms div_typing_rls} @
- [@{thm modC0}, @{thm modC_succ}, @{thm divC0}, @{thm divC_succ2}]) *})
+apply (NE a)
+apply (arith_rew div_typing_rls modC0 modC_succ divC0 divC_succ2)
apply (rule EqE)
(*case analysis on succ(u mod b)|-|b *)
apply (rule_tac a1 = "succ (u mod b) |-| b" in iszero_decidable [THEN PlusE])
apply (erule_tac [3] SumE)
-apply (tactic {* hyp_arith_rew_tac @{context} (@{thms div_typing_rls} @
- [@{thm modC0}, @{thm modC_succ}, @{thm divC0}, @{thm divC_succ2}]) *})
+apply (hyp_arith_rew div_typing_rls modC0 modC_succ divC0 divC_succ2)
(*Replace one occurrence of b by succ(u mod b). Clumsy!*)
apply (rule add_typingL [THEN trans_elem])
apply (erule EqE [THEN absdiff_eq0, THEN sym_elem])
apply (rule_tac [3] refl_elem)
-apply (tactic {* hyp_arith_rew_tac @{context} @{thms div_typing_rls} *})
+apply (hyp_arith_rew div_typing_rls)
done
end
--- a/src/CTT/Bool.thy Tue Nov 11 10:54:52 2014 +0100
+++ b/src/CTT/Bool.thy Tue Nov 11 11:41:58 2014 +0100
@@ -33,7 +33,7 @@
(*formation rule*)
lemma boolF: "Bool type"
apply (unfold bool_defs)
-apply (tactic "typechk_tac @{context} []")
+apply typechk
done
@@ -41,21 +41,21 @@
lemma boolI_true: "true : Bool"
apply (unfold bool_defs)
-apply (tactic "typechk_tac @{context} []")
+apply typechk
done
lemma boolI_false: "false : Bool"
apply (unfold bool_defs)
-apply (tactic "typechk_tac @{context} []")
+apply typechk
done
(*elimination rule: typing of cond*)
lemma boolE:
"[| p:Bool; a : C(true); b : C(false) |] ==> cond(p,a,b) : C(p)"
apply (unfold bool_defs)
-apply (tactic "typechk_tac @{context} []")
+apply typechk
apply (erule_tac [!] TE)
-apply (tactic "typechk_tac @{context} []")
+apply typechk
done
lemma boolEL:
@@ -72,18 +72,18 @@
"[| a : C(true); b : C(false) |] ==> cond(true,a,b) = a : C(true)"
apply (unfold bool_defs)
apply (rule comp_rls)
-apply (tactic "typechk_tac @{context} []")
+apply typechk
apply (erule_tac [!] TE)
-apply (tactic "typechk_tac @{context} []")
+apply typechk
done
lemma boolC_false:
"[| a : C(true); b : C(false) |] ==> cond(false,a,b) = b : C(false)"
apply (unfold bool_defs)
apply (rule comp_rls)
-apply (tactic "typechk_tac @{context} []")
+apply typechk
apply (erule_tac [!] TE)
-apply (tactic "typechk_tac @{context} []")
+apply typechk
done
end
--- a/src/CTT/CTT.thy Tue Nov 11 10:54:52 2014 +0100
+++ b/src/CTT/CTT.thy Tue Nov 11 11:41:58 2014 +0100
@@ -378,7 +378,22 @@
REPEAT_FIRST (ASSUME ctxt (filt_resolve_tac (thms @ equal_rls) 3))
end
+*}
+method_setup form = {*
+ Scan.succeed (fn ctxt => SIMPLE_METHOD (form_tac ctxt))
+*}
+
+method_setup typechk = {*
+ Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD (typechk_tac ctxt ths))
+*}
+
+method_setup intr = {*
+ Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD (intr_tac ctxt ths))
+*}
+
+method_setup equal = {*
+ Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD (equal_tac ctxt ths))
*}
@@ -460,8 +475,32 @@
fun pc_tac ctxt thms = DEPTH_SOLVE_1 o (step_tac ctxt thms)
*}
+method_setup eqintr = {*
+ Scan.succeed (SIMPLE_METHOD o eqintr_tac)
+*}
+
+method_setup NE = {*
+ Scan.lift Args.name >> (fn s => fn ctxt => SIMPLE_METHOD' (NE_tac ctxt s))
+*}
+
+method_setup pc = {*
+ Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (pc_tac ctxt ths))
+*}
+
+method_setup add_mp = {*
+ Scan.succeed (SIMPLE_METHOD' o add_mp_tac)
+*}
+
ML_file "rew.ML"
+method_setup rew = {*
+ Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD (rew_tac ctxt ths))
+*}
+
+method_setup hyp_rew = {*
+ Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD (hyp_rew_tac ctxt ths))
+*}
+
subsection {* The elimination rules for fst/snd *}
@@ -480,7 +519,7 @@
apply (unfold basic_defs)
apply (rule major [THEN SumE])
apply (rule SumC [THEN subst_eqtyparg, THEN replace_type])
- apply (tactic {* typechk_tac @{context} @{thms assms} *})
+ apply (typechk assms)
done
end
--- a/src/CTT/ex/Elimination.thy Tue Nov 11 10:54:52 2014 +0100
+++ b/src/CTT/ex/Elimination.thy Tue Nov 11 11:41:58 2014 +0100
@@ -15,36 +15,36 @@
text "This finds the functions fst and snd!"
schematic_lemma [folded basic_defs]: "A type ==> ?a : (A*A) --> A"
-apply (tactic {* pc_tac @{context} [] 1 *})
+apply pc
done
schematic_lemma [folded basic_defs]: "A type ==> ?a : (A*A) --> A"
-apply (tactic {* pc_tac @{context} [] 1 *})
+apply pc
back
done
text "Double negation of the Excluded Middle"
schematic_lemma "A type ==> ?a : ((A + (A-->F)) --> F) --> F"
-apply (tactic "intr_tac @{context} []")
+apply intr
apply (rule ProdE)
apply assumption
-apply (tactic "pc_tac @{context} [] 1")
+apply pc
done
schematic_lemma "[| A type; B type |] ==> ?a : (A*B) --> (B*A)"
-apply (tactic "pc_tac @{context} [] 1")
+apply pc
done
(*The sequent version (ITT) could produce an interesting alternative
by backtracking. No longer.*)
text "Binary sums and products"
schematic_lemma "[| A type; B type; C type |] ==> ?a : (A+B --> C) --> (A-->C) * (B-->C)"
-apply (tactic "pc_tac @{context} [] 1")
+apply pc
done
(*A distributive law*)
schematic_lemma "[| A type; B type; C type |] ==> ?a : A * (B+C) --> (A*B + A*C)"
-apply (tactic "pc_tac @{context} [] 1")
+apply pc
done
(*more general version, same proof*)
@@ -53,12 +53,12 @@
and "!!x. x:A ==> B(x) type"
and "!!x. x:A ==> C(x) type"
shows "?a : (SUM x:A. B(x) + C(x)) --> (SUM x:A. B(x)) + (SUM x:A. C(x))"
-apply (tactic {* pc_tac @{context} @{thms assms} 1 *})
+apply (pc assms)
done
text "Construction of the currying functional"
schematic_lemma "[| A type; B type; C type |] ==> ?a : (A*B --> C) --> (A--> (B-->C))"
-apply (tactic "pc_tac @{context} [] 1")
+apply pc
done
(*more general goal with same proof*)
@@ -68,12 +68,12 @@
and "!!z. z: (SUM x:A. B(x)) ==> C(z) type"
shows "?a : PROD f: (PROD z : (SUM x:A . B(x)) . C(z)).
(PROD x:A . PROD y:B(x) . C(<x,y>))"
-apply (tactic {* pc_tac @{context} @{thms assms} 1 *})
+apply (pc assms)
done
text "Martin-Lof (1984), page 48: axiom of sum-elimination (uncurry)"
schematic_lemma "[| A type; B type; C type |] ==> ?a : (A --> (B-->C)) --> (A*B --> C)"
-apply (tactic "pc_tac @{context} [] 1")
+apply pc
done
(*more general goal with same proof*)
@@ -83,12 +83,12 @@
and "!!z. z: (SUM x:A . B(x)) ==> C(z) type"
shows "?a : (PROD x:A . PROD y:B(x) . C(<x,y>))
--> (PROD z : (SUM x:A . B(x)) . C(z))"
-apply (tactic {* pc_tac @{context} @{thms assms} 1 *})
+apply (pc assms)
done
text "Function application"
schematic_lemma "[| A type; B type |] ==> ?a : ((A --> B) * A) --> B"
-apply (tactic "pc_tac @{context} [] 1")
+apply pc
done
text "Basic test of quantifier reasoning"
@@ -99,7 +99,7 @@
shows
"?a : (SUM y:B . PROD x:A . C(x,y))
--> (PROD x:A . SUM y:B . C(x,y))"
-apply (tactic {* pc_tac @{context} @{thms assms} 1 *})
+apply (pc assms)
done
text "Martin-Lof (1984) pages 36-7: the combinator S"
@@ -109,7 +109,7 @@
and "!!x y.[| x:A; y:B(x) |] ==> C(x,y) type"
shows "?a : (PROD x:A. PROD y:B(x). C(x,y))
--> (PROD f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))"
-apply (tactic {* pc_tac @{context} @{thms assms} 1 *})
+apply (pc assms)
done
text "Martin-Lof (1984) page 58: the axiom of disjunction elimination"
@@ -119,13 +119,13 @@
and "!!z. z: A+B ==> C(z) type"
shows "?a : (PROD x:A. C(inl(x))) --> (PROD y:B. C(inr(y)))
--> (PROD z: A+B. C(z))"
-apply (tactic {* pc_tac @{context} @{thms assms} 1 *})
+apply (pc assms)
done
(*towards AXIOM OF CHOICE*)
schematic_lemma [folded basic_defs]:
"[| A type; B type; C type |] ==> ?a : (A --> B*C) --> (A-->B) * (A-->C)"
-apply (tactic "pc_tac @{context} [] 1")
+apply pc
done
@@ -137,15 +137,15 @@
and "!!x y.[| x:A; y:B(x) |] ==> C(x,y) type"
shows "?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)).
(SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))"
-apply (tactic {* intr_tac @{context} @{thms assms} *})
-apply (tactic "add_mp_tac @{context} 2")
-apply (tactic "add_mp_tac @{context} 1")
+apply (intr assms)
+prefer 2 apply add_mp
+prefer 2 apply add_mp
apply (erule SumE_fst)
apply (rule replace_type)
apply (rule subst_eqtyparg)
apply (rule comp_rls)
apply (rule_tac [4] SumE_snd)
-apply (tactic {* typechk_tac @{context} (@{thm SumE_fst} :: @{thms assms}) *})
+apply (typechk SumE_fst assms)
done
text "Axiom of choice. Proof without fst, snd. Harder still!"
@@ -155,19 +155,21 @@
and "!!x y.[| x:A; y:B(x) |] ==> C(x,y) type"
shows "?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)).
(SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))"
-apply (tactic {* intr_tac @{context} @{thms assms} *})
-(*Must not use add_mp_tac as subst_prodE hides the construction.*)
-apply (rule ProdE [THEN SumE], assumption)
-apply (tactic "TRYALL (assume_tac @{context})")
+apply (intr assms)
+(*Must not use add_mp as subst_prodE hides the construction.*)
+apply (rule ProdE [THEN SumE])
+apply assumption
+apply assumption
+apply assumption
apply (rule replace_type)
apply (rule subst_eqtyparg)
apply (rule comp_rls)
apply (erule_tac [4] ProdE [THEN SumE])
-apply (tactic {* typechk_tac @{context} @{thms assms} *})
+apply (typechk assms)
apply (rule replace_type)
apply (rule subst_eqtyparg)
apply (rule comp_rls)
-apply (tactic {* typechk_tac @{context} @{thms assms} *})
+apply (typechk assms)
apply assumption
done
@@ -183,11 +185,12 @@
apply (tactic {* biresolve_tac safe_brls 2 *})
(*Now must convert assumption C(z) into antecedent C(<kd,ke>) *)
apply (rule_tac [2] a = "y" in ProdE)
-apply (tactic {* typechk_tac @{context} @{thms assms} *})
+apply (typechk assms)
apply (rule SumE, assumption)
-apply (tactic "intr_tac @{context} []")
-apply (tactic "TRYALL (assume_tac @{context})")
-apply (tactic {* typechk_tac @{context} @{thms assms} *})
+apply intr
+defer 1
+apply assumption+
+apply (typechk assms)
done
end
--- a/src/CTT/ex/Equality.thy Tue Nov 11 10:54:52 2014 +0100
+++ b/src/CTT/ex/Equality.thy Tue Nov 11 11:41:58 2014 +0100
@@ -12,35 +12,35 @@
lemma split_eq: "p : Sum(A,B) ==> split(p,pair) = p : Sum(A,B)"
apply (rule EqE)
apply (rule elim_rls, assumption)
-apply (tactic "rew_tac @{context} []")
+apply rew
done
lemma when_eq: "[| A type; B type; p : A+B |] ==> when(p,inl,inr) = p : A + B"
apply (rule EqE)
apply (rule elim_rls, assumption)
-apply (tactic "rew_tac @{context} []")
+apply rew
done
(*in the "rec" formulation of addition, 0+n=n *)
lemma "p:N ==> rec(p,0, %y z. succ(y)) = p : N"
apply (rule EqE)
apply (rule elim_rls, assumption)
-apply (tactic "rew_tac @{context} []")
+apply rew
done
(*the harder version, n+0=n: recursive, uses induction hypothesis*)
lemma "p:N ==> rec(p,0, %y z. succ(z)) = p : N"
apply (rule EqE)
apply (rule elim_rls, assumption)
-apply (tactic "hyp_rew_tac @{context} []")
+apply hyp_rew
done
(*Associativity of addition*)
lemma "[| a:N; b:N; c:N |]
==> rec(rec(a, b, %x y. succ(y)), c, %x y. succ(y)) =
rec(a, rec(b, c, %x y. succ(y)), %x y. succ(y)) : N"
-apply (tactic {* NE_tac @{context} "a" 1 *})
-apply (tactic "hyp_rew_tac @{context} []")
+apply (NE a)
+apply hyp_rew
done
(*Martin-Lof (1984) page 62: pairing is surjective*)
@@ -52,7 +52,7 @@
lemma "[| a : A; b : B |] ==>
(lam u. split(u, %v w.<w,v>)) ` <a,b> = <b,a> : SUM x:B. A"
-apply (tactic "rew_tac @{context} []")
+apply rew
done
(*a contrived, complicated simplication, requires sum-elimination also*)
@@ -61,9 +61,9 @@
apply (rule reduction_rls)
apply (rule_tac [3] intrL_rls)
apply (rule_tac [4] EqE)
-apply (rule_tac [4] SumE, tactic "assume_tac @{context} 4")
+apply (erule_tac [4] SumE)
(*order of unifiers is essential here*)
-apply (tactic "rew_tac @{context} []")
+apply rew
done
end
--- a/src/CTT/ex/Synthesis.thy Tue Nov 11 10:54:52 2014 +0100
+++ b/src/CTT/ex/Synthesis.thy Tue Nov 11 11:41:58 2014 +0100
@@ -12,21 +12,21 @@
text "discovery of predecessor function"
schematic_lemma "?a : SUM pred:?A . Eq(N, pred`0, 0)
* (PROD n:N. Eq(N, pred ` succ(n), n))"
-apply (tactic "intr_tac @{context} []")
-apply (tactic "eqintr_tac @{context}")
+apply intr
+apply eqintr
apply (rule_tac [3] reduction_rls)
apply (rule_tac [5] comp_rls)
-apply (tactic "rew_tac @{context} []")
+apply rew
done
text "the function fst as an element of a function type"
schematic_lemma [folded basic_defs]:
"A type ==> ?a: SUM f:?B . PROD i:A. PROD j:A. Eq(A, f ` <i,j>, i)"
-apply (tactic "intr_tac @{context} []")
-apply (tactic "eqintr_tac @{context}")
+apply intr
+apply eqintr
apply (rule_tac [2] reduction_rls)
apply (rule_tac [4] comp_rls)
-apply (tactic "typechk_tac @{context} []")
+apply typechk
txt "now put in A everywhere"
apply assumption+
done
@@ -36,10 +36,10 @@
See following example.*)
schematic_lemma "?a : PROD i:N. Eq(?A, ?b(inl(i)), <0 , i>)
* Eq(?A, ?b(inr(i)), <succ(0), i>)"
-apply (tactic "intr_tac @{context} []")
-apply (tactic "eqintr_tac @{context}")
+apply intr
+apply eqintr
apply (rule comp_rls)
-apply (tactic "rew_tac @{context} []")
+apply rew
done
(*Here we allow the type to depend on i.
@@ -55,13 +55,13 @@
schematic_lemma [folded basic_defs]:
"?a : PROD i:N. PROD j:N. Eq(?A, ?b(inl(<i,j>)), i)
* Eq(?A, ?b(inr(<i,j>)), j)"
-apply (tactic "intr_tac @{context} []")
-apply (tactic "eqintr_tac @{context}")
+apply intr
+apply eqintr
apply (rule PlusC_inl [THEN trans_elem])
apply (rule_tac [4] comp_rls)
apply (rule_tac [7] reduction_rls)
apply (rule_tac [10] comp_rls)
-apply (tactic "typechk_tac @{context} []")
+apply typechk
done
(*similar but allows the type to depend on i and j*)
@@ -79,10 +79,10 @@
schematic_lemma [folded arith_defs]:
"?c : PROD n:N. Eq(N, ?f(0,n), n)
* (PROD m:N. Eq(N, ?f(succ(m), n), succ(?f(m,n))))"
-apply (tactic "intr_tac @{context} []")
-apply (tactic "eqintr_tac @{context}")
+apply intr
+apply eqintr
apply (rule comp_rls)
-apply (tactic "rew_tac @{context} []")
+apply rew
done
text "The addition function -- using explicit lambdas"
@@ -90,15 +90,15 @@
"?c : SUM plus : ?A .
PROD x:N. Eq(N, plus`0`x, x)
* (PROD y:N. Eq(N, plus`succ(y)`x, succ(plus`y`x)))"
-apply (tactic "intr_tac @{context} []")
-apply (tactic "eqintr_tac @{context}")
+apply intr
+apply eqintr
apply (tactic "resolve_tac [TSimp.split_eqn] 3")
apply (tactic "SELECT_GOAL (rew_tac @{context} []) 4")
apply (tactic "resolve_tac [TSimp.split_eqn] 3")
apply (tactic "SELECT_GOAL (rew_tac @{context} []) 4")
apply (rule_tac [3] p = "y" in NC_succ)
(** by (resolve_tac comp_rls 3); caused excessive branching **)
-apply (tactic "rew_tac @{context} []")
+apply rew
done
end
--- a/src/CTT/ex/Typechecking.thy Tue Nov 11 10:54:52 2014 +0100
+++ b/src/CTT/ex/Typechecking.thy Tue Nov 11 11:41:58 2014 +0100
@@ -34,54 +34,56 @@
subsection {* Multi-step proofs: Type inference *}
lemma "PROD w:N. N + N type"
-apply (tactic "form_tac @{context}")
+apply form
done
schematic_lemma "<0, succ(0)> : ?A"
-apply (tactic "intr_tac @{context} []")
+apply intr
done
schematic_lemma "PROD w:N . Eq(?A,w,w) type"
-apply (tactic "typechk_tac @{context} []")
+apply typechk
done
schematic_lemma "PROD x:N . PROD y:N . Eq(?A,x,y) type"
-apply (tactic "typechk_tac @{context} []")
+apply typechk
done
text "typechecking an application of fst"
schematic_lemma "(lam u. split(u, %v w. v)) ` <0, succ(0)> : ?A"
-apply (tactic "typechk_tac @{context} []")
+apply typechk
done
text "typechecking the predecessor function"
schematic_lemma "lam n. rec(n, 0, %x y. x) : ?A"
-apply (tactic "typechk_tac @{context} []")
+apply typechk
done
text "typechecking the addition function"
schematic_lemma "lam n. lam m. rec(n, m, %x y. succ(y)) : ?A"
-apply (tactic "typechk_tac @{context} []")
+apply typechk
done
(*Proofs involving arbitrary types.
For concreteness, every type variable left over is forced to be N*)
-ML {* val N_tac = TRYALL (rtac @{thm NF}) *}
+method_setup N = {*
+ Scan.succeed (fn _ => SIMPLE_METHOD (TRYALL (resolve_tac @{thms NF})))
+*}
schematic_lemma "lam w. <w,w> : ?A"
-apply (tactic "typechk_tac @{context} []")
-apply (tactic N_tac)
+apply typechk
+apply N
done
schematic_lemma "lam x. lam y. x : ?A"
-apply (tactic "typechk_tac @{context} []")
-apply (tactic N_tac)
+apply typechk
+apply N
done
text "typechecking fst (as a function object)"
schematic_lemma "lam i. split(i, %j k. j) : ?A"
-apply (tactic "typechk_tac @{context} []")
-apply (tactic N_tac)
+apply typechk
+apply N
done
end