> goal Nat.thy "(k+m)+n = k+(m+n)"; Level 0 k + m + n = k + (m + n) 1. k + m + n = k + (m + n) val it = [] : thm list > by (resolve_tac [induct] 1); Level 1 k + m + n = k + (m + n) 1. k + m + n = 0 2. !!x. k + m + n = x ==> k + m + n = Suc(x) val it = () : unit > back(); Level 1 k + m + n = k + (m + n) 1. k + m + n = k + 0 2. !!x. k + m + n = k + x ==> k + m + n = k + Suc(x) val it = () : unit > back(); Level 1 k + m + n = k + (m + n) 1. k + m + 0 = k + (m + 0) 2. !!x. k + m + x = k + (m + x) ==> k + m + Suc(x) = k + (m + Suc(x)) val it = () : unit > back(); Level 1 k + m + n = k + (m + n) 1. k + m + n = k + (m + 0) 2. !!x. k + m + n = k + (m + x) ==> k + m + n = k + (m + Suc(x)) val it = () : unit > val nat_congs = prths (mk_congs Nat.thy ["Suc", "op +"]); ?Xa = ?Ya ==> Suc(?Xa) = Suc(?Ya) [| ?Xa = ?Ya; ?Xb = ?Yb |] ==> ?Xa + ?Xb = ?Ya + ?Yb ?Xa = ?Ya ==> Suc(?Xa) = Suc(?Ya) [| ?Xa = ?Ya; ?Xb = ?Yb |] ==> ?Xa + ?Xb = ?Ya + ?Yb val nat_congs = [, ] : thm list > val add_ss = FOL_ss addcongs nat_congs # addrews [add_0, add_Suc]; val add_ss = ? : simpset > goal Nat.thy "(k+m)+n = k+(m+n)"; Level 0 k + m + n = k + (m + n) 1. k + m + n = k + (m + n) val it = [] : thm list > by (res_inst_tac [("n","k")] induct 1); Level 1 k + m + n = k + (m + n) 1. 0 + m + n = 0 + (m + n) 2. !!x. x + m + n = x + (m + n) ==> Suc(x) + m + n = Suc(x) + (m + n) val it = () : unit > by (SIMP_TAC add_ss 1); Level 2 k + m + n = k + (m + n) 1. !!x. x + m + n = x + (m + n) ==> Suc(x) + m + n = Suc(x) + (m + n) val it = () : unit > by (ASM_SIMP_TAC add_ss 1); Level 3 k + m + n = k + (m + n) No subgoals! val it = () : unit > val add_assoc = result(); ?k + ?m + ?n = ?k + (?m + ?n) val add_assoc = : thm