Hello, I am new to Isabelle here and apologize if the questions is not framed adequately.

I have a sublocale sublocale th8a ⊆ th7

which gives me 5 subgoals

- ⋀n. plus n zero = n
- ⋀n m. plus n (suc m) = suc (plus n m)
- ⋀n. times n zero = zero
- ⋀n m. times n (suc m) = plus (times n m) n
- ⋀x. (zero = zero ∨ (∃m. suc m = zero)) ∧

(x = zero ∨ (∃m. suc m = x) ⟶

suc x = zero ∨ (∃m. suc m = suc x)) ⟶

(∀x. x = zero ∨ (∃m. suc m = x))

The subgoals look an awful lot like some of the assumptions in other locales, like

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)"

However, everytime I use th2.arith_1 with proper substitutions it doesn't do anything for me.

Locale th8a looks like this

locale th8a = th1 +

assumes

"((∀x . p zero ∧ (∀x. p x ⟶ p (suc x))) ⟶ (∀x. p x))"

begin

definition

plus where "plus = (THE f. ∀ x y. f x zero = x ∧ f x (suc y) = suc (f x y))"

definition

times where "times = (THE g. ∀ x y. g x zero = zero ∧ g x (suc y) = plus (g x y) x)"

end

I was wondering if and how I might have to use the definition of plus and times to prove my subgoals?

Any help is widely appreciated.

Thank you,

Lekhani

Last updated: Sep 25 2022 at 23:25 UTC