diff -r 3567d0571932 -r 8feb2c4bef1a src/CTT/Arith.thy --- a/src/CTT/Arith.thy Fri Apr 23 23:33:48 2010 +0200 +++ b/src/CTT/Arith.thy Fri Apr 23 23:35:43 2010 +0200 @@ -256,7 +256,8 @@ (*Addition is the inverse of subtraction: if b<=x then b#+(x-b) = x. An example of induction over a quantified formula (a product). Uses rewriting with a quantified, implicative inductive hypothesis.*) -lemma add_diff_inverse_lemma: "b:N ==> ?a : PROD x:N. Eq(N, b-x, 0) --> Eq(N, b #+ (x-b), x)" +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 *}) (*strip one "universal quantifier" but not the "implication"*) apply (rule_tac [3] intr_rls) @@ -324,7 +325,7 @@ done (*If a+b=0 then a=0. Surprisingly tedious*) -lemma add_eq0_lemma: "[| a:N; b:N |] ==> ?c : PROD u: Eq(N,a#+b,0) . Eq(N,a,0)" +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 (rule_tac [3] replace_type) apply (tactic "arith_rew_tac []") @@ -344,7 +345,7 @@ done (*Here is a lemma to infer a-b=0 and b-a=0 from a|-|b=0, below. *) -lemma absdiff_eq0_lem: +schematic_lemma absdiff_eq0_lem: "[| 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)