lemma (in th8b) lem_mul_2: "times (suc m) n = plus (times n m) m"
  apply(induction n rule: p1)

locale th1 =
  fixes
    zero :: "'a"
    and suc :: "'a ⇒ 'a"
  assumes
    "suc n ≠ zero"
    and "suc n = suc m ⟶ n = m"

locale th2 = th1 +
  fixes
    plus :: "'a ⇒ 'a ⇒ 'a"
  assumes
     arith_1: "plus n zero = n"
    and plus_suc: "plus n (suc m) = suc ( plus n m)"

locale th3 = th2 +
  fixeslocale th8b = th3 +
  assumes p1:
"⋀x. ((⋀x . p zero ∧ ( p x ⟶ p (suc x)))) ⟹ p x"

    times :: "'a ⇒ 'a ⇒ 'a"
  assumes
    times_1: "times n zero = zero"
    and times_suc: "times n (suc m) =  plus (times n m) n"

locale th8b = th3 +
  assumes p1:
"⋀x. ((⋀x . p zero ∧ ( p x ⟶ p (suc x)))) ⟹ p x"