# HG changeset patch # User wenzelm # Date 1415702518 -3600 # Node ID 5b026cfc5f04649ff1463338f2552f842465ebeb # Parent 8c9a319821b391f6afffd0e87d67c2707ef12ce3 more Isar proof methods; diff -r 8c9a319821b3 -r 5b026cfc5f04 src/CTT/Arith.thy --- 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()) : 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 diff -r 8c9a319821b3 -r 5b026cfc5f04 src/CTT/Bool.thy --- 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 diff -r 8c9a319821b3 -r 5b026cfc5f04 src/CTT/CTT.thy --- 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 diff -r 8c9a319821b3 -r 5b026cfc5f04 src/CTT/ex/Elimination.thy --- 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())" -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()) --> (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() *) 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 diff -r 8c9a319821b3 -r 5b026cfc5f04 src/CTT/ex/Equality.thy --- 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.)) ` = : 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 diff -r 8c9a319821b3 -r 5b026cfc5f04 src/CTT/ex/Synthesis.thy --- 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)" -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)), )" -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) * Eq(?A, ?b(inr()), 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 diff -r 8c9a319821b3 -r 5b026cfc5f04 src/CTT/ex/Typechecking.thy --- 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. : ?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