105

1 
> goal Nat.thy "(k+m)+n = k+(m+n)";


2 
Level 0


3 
k + m + n = k + (m + n)


4 
1. k + m + n = k + (m + n)


5 
val it = [] : thm list


6 
> by (resolve_tac [induct] 1);


7 
Level 1


8 
k + m + n = k + (m + n)


9 
1. k + m + n = 0


10 
2. !!x. k + m + n = x ==> k + m + n = Suc(x)


11 
val it = () : unit


12 
> back();


13 
Level 1


14 
k + m + n = k + (m + n)


15 
1. k + m + n = k + 0


16 
2. !!x. k + m + n = k + x ==> k + m + n = k + Suc(x)


17 
val it = () : unit


18 
> back();


19 
Level 1


20 
k + m + n = k + (m + n)


21 
1. k + m + 0 = k + (m + 0)


22 
2. !!x. k + m + x = k + (m + x) ==> k + m + Suc(x) = k + (m + Suc(x))


23 
val it = () : unit


24 
> back();


25 
Level 1


26 
k + m + n = k + (m + n)


27 
1. k + m + n = k + (m + 0)


28 
2. !!x. k + m + n = k + (m + x) ==> k + m + n = k + (m + Suc(x))


29 
val it = () : unit


30 


31 
> val nat_congs = prths (mk_congs Nat.thy ["Suc", "op +"]);


32 
?Xa = ?Ya ==> Suc(?Xa) = Suc(?Ya)


33 


34 
[ ?Xa = ?Ya; ?Xb = ?Yb ] ==> ?Xa + ?Xb = ?Ya + ?Yb


35 


36 
?Xa = ?Ya ==> Suc(?Xa) = Suc(?Ya)


37 
[ ?Xa = ?Ya; ?Xb = ?Yb ] ==> ?Xa + ?Xb = ?Ya + ?Yb


38 
val nat_congs = [, ] : thm list


39 
> val add_ss = FOL_ss addcongs nat_congs


40 
# addrews [add_0, add_Suc];


41 
val add_ss = ? : simpset


42 
> goal Nat.thy "(k+m)+n = k+(m+n)";


43 
Level 0


44 
k + m + n = k + (m + n)


45 
1. k + m + n = k + (m + n)


46 
val it = [] : thm list


47 
> by (res_inst_tac [("n","k")] induct 1);


48 
Level 1


49 
k + m + n = k + (m + n)


50 
1. 0 + m + n = 0 + (m + n)


51 
2. !!x. x + m + n = x + (m + n) ==> Suc(x) + m + n = Suc(x) + (m + n)


52 
val it = () : unit


53 
> by (SIMP_TAC add_ss 1);


54 
Level 2


55 
k + m + n = k + (m + n)


56 
1. !!x. x + m + n = x + (m + n) ==> Suc(x) + m + n = Suc(x) + (m + n)


57 
val it = () : unit


58 
> by (ASM_SIMP_TAC add_ss 1);


59 
Level 3


60 
k + m + n = k + (m + n)


61 
No subgoals!


62 
val it = () : unit


63 
> val add_assoc = result();


64 
?k + ?m + ?n = ?k + (?m + ?n)


65 
val add_assoc = : thm
