4396

1 

359

2 
Pretty.setmargin 70;


3 

4396

4 


5 
context Arith.thy;


6 
goal Arith.thy "0 + (x + 0) = x + 0 + 0";


7 
by (Simp_tac 1);


8 


9 


10 


11 

104

12 
> goal Nat.thy "m+0 = m";


13 
Level 0


14 
m + 0 = m


15 
1. m + 0 = m


16 
> by (res_inst_tac [("n","m")] induct 1);


17 
Level 1


18 
m + 0 = m


19 
1. 0 + 0 = 0


20 
2. !!x. x + 0 = x ==> Suc(x) + 0 = Suc(x)


21 
> by (simp_tac add_ss 1);


22 
Level 2


23 
m + 0 = m


24 
1. !!x. x + 0 = x ==> Suc(x) + 0 = Suc(x)


25 
> by (asm_simp_tac add_ss 1);


26 
Level 3


27 
m + 0 = m


28 
No subgoals!


29 


30 


31 
> goal Nat.thy "m+Suc(n) = Suc(m+n)";


32 
Level 0


33 
m + Suc(n) = Suc(m + n)


34 
1. m + Suc(n) = Suc(m + n)


35 
val it = [] : thm list


36 
> by (res_inst_tac [("n","m")] induct 1);


37 
Level 1


38 
m + Suc(n) = Suc(m + n)


39 
1. 0 + Suc(n) = Suc(0 + n)


40 
2. !!x. x + Suc(n) = Suc(x + n) ==> Suc(x) + Suc(n) = Suc(Suc(x) + n)


41 
val it = () : unit


42 
> by (simp_tac add_ss 1);


43 
Level 2


44 
m + Suc(n) = Suc(m + n)


45 
1. !!x. x + Suc(n) = Suc(x + n) ==> Suc(x) + Suc(n) = Suc(Suc(x) + n)


46 
val it = () : unit


47 
> trace_simp := true;


48 
val it = () : unit


49 
> by (asm_simp_tac add_ss 1);


50 
Rewriting:


51 
Suc(x) + Suc(n) == Suc(x + Suc(n))


52 
Rewriting:


53 
x + Suc(n) == Suc(x + n)


54 
Rewriting:


55 
Suc(x) + n == Suc(x + n)


56 
Rewriting:


57 
Suc(Suc(x + n)) = Suc(Suc(x + n)) == True


58 
Level 3


59 
m + Suc(n) = Suc(m + n)


60 
No subgoals!


61 
val it = () : unit


62 


63 


64 


65 
> val prems = goal Nat.thy "(!!n. f(Suc(n)) = Suc(f(n))) ==> f(i+j) = i+f(j)";


66 
Level 0


67 
f(i + j) = i + f(j)


68 
1. f(i + j) = i + f(j)


69 
> prths prems;


70 
f(Suc(?n)) = Suc(f(?n)) [!!n. f(Suc(n)) = Suc(f(n))]


71 


72 
> by (res_inst_tac [("n","i")] induct 1);


73 
Level 1


74 
f(i + j) = i + f(j)


75 
1. f(0 + j) = 0 + f(j)


76 
2. !!x. f(x + j) = x + f(j) ==> f(Suc(x) + j) = Suc(x) + f(j)


77 
> by (simp_tac f_ss 1);


78 
Level 2


79 
f(i + j) = i + f(j)


80 
1. !!x. f(x + j) = x + f(j) ==> f(Suc(x) + j) = Suc(x) + f(j)


81 
> by (asm_simp_tac (f_ss addrews prems) 1);


82 
Level 3


83 
f(i + j) = i + f(j)


84 
No subgoals!

359

85 


86 


87 


88 
> goal NatSum.thy "Suc(Suc(0))*sum(%i.i,Suc(n)) = n*Suc(n)";


89 
Level 0


90 
Suc(Suc(0)) * sum(%i. i, Suc(n)) = n * Suc(n)


91 
1. Suc(Suc(0)) * sum(%i. i, Suc(n)) = n * Suc(n)


92 


93 
> by (simp_tac natsum_ss 1);


94 
Level 1


95 
Suc(Suc(0)) * sum(%i. i, Suc(n)) = n * Suc(n)


96 
1. n + (n + (sum(%i. i, n) + sum(%i. i, n))) = n + n * n


97 


98 
> by (nat_ind_tac "n" 1);


99 
Level 2


100 
Suc(Suc(0)) * sum(%i. i, Suc(n)) = n * Suc(n)


101 
1. 0 + (0 + (sum(%i. i, 0) + sum(%i. i, 0))) = 0 + 0 * 0


102 
2. !!n1. n1 + (n1 + (sum(%i. i, n1) + sum(%i. i, n1))) =


103 
n1 + n1 * n1 ==>


104 
Suc(n1) +


105 
(Suc(n1) + (sum(%i. i, Suc(n1)) + sum(%i. i, Suc(n1)))) =


106 
Suc(n1) + Suc(n1) * Suc(n1)


107 


108 
> by (simp_tac natsum_ss 1);


109 
Level 3


110 
Suc(Suc(0)) * sum(%i. i, Suc(n)) = n * Suc(n)


111 
1. !!n1. n1 + (n1 + (sum(%i. i, n1) + sum(%i. i, n1))) =


112 
n1 + n1 * n1 ==>


113 
Suc(n1) +


114 
(Suc(n1) + (sum(%i. i, Suc(n1)) + sum(%i. i, Suc(n1)))) =


115 
Suc(n1) + Suc(n1) * Suc(n1)


116 


117 
> by (asm_simp_tac natsum_ss 1);


118 
Level 4


119 
Suc(Suc(0)) * sum(%i. i, Suc(n)) = n * Suc(n)


120 
No subgoals!
