104

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


2 
Level 0


3 
m + 0 = m


4 
1. m + 0 = m


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


6 
Level 1


7 
m + 0 = m


8 
1. 0 + 0 = 0


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


10 
> by (simp_tac add_ss 1);


11 
Level 2


12 
m + 0 = m


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


14 
> by (asm_simp_tac add_ss 1);


15 
Level 3


16 
m + 0 = m


17 
No subgoals!


18 


19 


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


21 
Level 0


22 
m + Suc(n) = Suc(m + n)


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


24 
val it = [] : thm list


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


26 
Level 1


27 
m + Suc(n) = Suc(m + n)


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


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


30 
val it = () : unit


31 
> by (simp_tac add_ss 1);


32 
Level 2


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


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


35 
val it = () : unit


36 
> trace_simp := true;


37 
val it = () : unit


38 
> by (asm_simp_tac add_ss 1);


39 
Rewriting:


40 
Suc(x) + Suc(n) == Suc(x + Suc(n))


41 
Rewriting:


42 
x + Suc(n) == Suc(x + n)


43 
Rewriting:


44 
Suc(x) + n == Suc(x + n)


45 
Rewriting:


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


47 
Level 3


48 
m + Suc(n) = Suc(m + n)


49 
No subgoals!


50 
val it = () : unit


51 


52 


53 


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


55 
Level 0


56 
f(i + j) = i + f(j)


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


58 
> prths prems;


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


60 


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


62 
Level 1


63 
f(i + j) = i + f(j)


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


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


66 
> by (simp_tac f_ss 1);


67 
Level 2


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


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


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


71 
Level 3


72 
f(i + j) = i + f(j)


73 
No subgoals!
