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
The subgoals look an awful lot like some of the assumptions in other locales, like
locale th2 = th1 +
plus :: "'a ⇒ 'a ⇒ 'a"
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 +
"((∀x . p zero ∧ (∀x. p x ⟶ p (suc x))) ⟶ (∀x. p x))"
plus where "plus = (THE f. ∀ x y. f x zero = x ∧ f x (suc y) = suc (f x y))"
times where "times = (THE g. ∀ x y. g x zero = zero ∧ g x (suc y) = plus (g x y) x)"
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.
Last updated: Sep 25 2022 at 23:25 UTC