wenzelm@4396: 
lcp@359: Pretty.setmargin 70;
lcp@359: 
wenzelm@4396: 
wenzelm@4396: context Arith.thy;
wenzelm@4396: goal Arith.thy "0 + (x + 0) = x + 0 + 0";
wenzelm@4396: by (Simp_tac 1);
wenzelm@4396: 
wenzelm@4396: 
wenzelm@4396: 
wenzelm@4396: 
lcp@104: > goal Nat.thy "m+0 = m";
lcp@104: Level 0
lcp@104: m + 0 = m
lcp@104:  1. m + 0 = m
lcp@104: > by (res_inst_tac [("n","m")] induct 1);
lcp@104: Level 1
lcp@104: m + 0 = m
lcp@104:  1. 0 + 0 = 0
lcp@104:  2. !!x. x + 0 = x ==> Suc(x) + 0 = Suc(x)
lcp@104: > by (simp_tac add_ss 1);
lcp@104: Level 2
lcp@104: m + 0 = m
lcp@104:  1. !!x. x + 0 = x ==> Suc(x) + 0 = Suc(x)
lcp@104: > by (asm_simp_tac add_ss 1);
lcp@104: Level 3
lcp@104: m + 0 = m
lcp@104: No subgoals!
lcp@104: 
lcp@104: 
lcp@104: > goal Nat.thy "m+Suc(n) = Suc(m+n)";
lcp@104: Level 0
lcp@104: m + Suc(n) = Suc(m + n)
lcp@104:  1. m + Suc(n) = Suc(m + n)
lcp@104: val it = [] : thm list   
lcp@104: > by (res_inst_tac [("n","m")] induct 1);
lcp@104: Level 1
lcp@104: m + Suc(n) = Suc(m + n)
lcp@104:  1. 0 + Suc(n) = Suc(0 + n)
lcp@104:  2. !!x. x + Suc(n) = Suc(x + n) ==> Suc(x) + Suc(n) = Suc(Suc(x) + n)
lcp@104: val it = () : unit   
lcp@104: > by (simp_tac add_ss 1);
lcp@104: Level 2
lcp@104: m + Suc(n) = Suc(m + n)
lcp@104:  1. !!x. x + Suc(n) = Suc(x + n) ==> Suc(x) + Suc(n) = Suc(Suc(x) + n)
lcp@104: val it = () : unit   
lcp@104: > trace_simp := true;
lcp@104: val it = () : unit   
lcp@104: > by (asm_simp_tac add_ss 1);
lcp@104: Rewriting:
lcp@104: Suc(x) + Suc(n) == Suc(x + Suc(n))
lcp@104: Rewriting:
lcp@104: x + Suc(n) == Suc(x + n)
lcp@104: Rewriting:
lcp@104: Suc(x) + n == Suc(x + n)
lcp@104: Rewriting:
lcp@104: Suc(Suc(x + n)) = Suc(Suc(x + n)) == True
lcp@104: Level 3
lcp@104: m + Suc(n) = Suc(m + n)
lcp@104: No subgoals!
lcp@104: val it = () : unit   
lcp@104: 
lcp@104: 
lcp@104: 
lcp@104: > val prems = goal Nat.thy "(!!n. f(Suc(n)) = Suc(f(n))) ==> f(i+j) = i+f(j)";
lcp@104: Level 0
lcp@104: f(i + j) = i + f(j)
lcp@104:  1. f(i + j) = i + f(j)
lcp@104: > prths prems;
lcp@104: f(Suc(?n)) = Suc(f(?n))  [!!n. f(Suc(n)) = Suc(f(n))]
lcp@104: 
lcp@104: > by (res_inst_tac [("n","i")] induct 1);
lcp@104: Level 1
lcp@104: f(i + j) = i + f(j)
lcp@104:  1. f(0 + j) = 0 + f(j)
lcp@104:  2. !!x. f(x + j) = x + f(j) ==> f(Suc(x) + j) = Suc(x) + f(j)
lcp@104: > by (simp_tac f_ss 1);
lcp@104: Level 2
lcp@104: f(i + j) = i + f(j)
lcp@104:  1. !!x. f(x + j) = x + f(j) ==> f(Suc(x) + j) = Suc(x) + f(j)
lcp@104: > by (asm_simp_tac (f_ss addrews prems) 1);
lcp@104: Level 3
lcp@104: f(i + j) = i + f(j)
lcp@104: No subgoals!
lcp@359: 
lcp@359: 
lcp@359: 
lcp@359: > goal NatSum.thy "Suc(Suc(0))*sum(%i.i,Suc(n)) = n*Suc(n)";
lcp@359: Level 0
lcp@359: Suc(Suc(0)) * sum(%i. i, Suc(n)) = n * Suc(n)
lcp@359:  1. Suc(Suc(0)) * sum(%i. i, Suc(n)) = n * Suc(n)
lcp@359: 
lcp@359: > by (simp_tac natsum_ss 1);
lcp@359: Level 1
lcp@359: Suc(Suc(0)) * sum(%i. i, Suc(n)) = n * Suc(n)
lcp@359:  1. n + (n + (sum(%i. i, n) + sum(%i. i, n))) = n + n * n
lcp@359: 
lcp@359: > by (nat_ind_tac "n" 1);
lcp@359: Level 2
lcp@359: Suc(Suc(0)) * sum(%i. i, Suc(n)) = n * Suc(n)
lcp@359:  1. 0 + (0 + (sum(%i. i, 0) + sum(%i. i, 0))) = 0 + 0 * 0
lcp@359:  2. !!n1. n1 + (n1 + (sum(%i. i, n1) + sum(%i. i, n1))) =
lcp@359:           n1 + n1 * n1 ==>
lcp@359:           Suc(n1) +
lcp@359:           (Suc(n1) + (sum(%i. i, Suc(n1)) + sum(%i. i, Suc(n1)))) =
lcp@359:           Suc(n1) + Suc(n1) * Suc(n1)
lcp@359: 
lcp@359: > by (simp_tac natsum_ss 1);
lcp@359: Level 3
lcp@359: Suc(Suc(0)) * sum(%i. i, Suc(n)) = n * Suc(n)
lcp@359:  1. !!n1. n1 + (n1 + (sum(%i. i, n1) + sum(%i. i, n1))) =
lcp@359:           n1 + n1 * n1 ==>
lcp@359:           Suc(n1) +
lcp@359:           (Suc(n1) + (sum(%i. i, Suc(n1)) + sum(%i. i, Suc(n1)))) =
lcp@359:           Suc(n1) + Suc(n1) * Suc(n1)
lcp@359: 
lcp@359: > by (asm_simp_tac natsum_ss 1);
lcp@359: Level 4
lcp@359: Suc(Suc(0)) * sum(%i. i, Suc(n)) = n * Suc(n)
lcp@359: No subgoals!