Stream: Beginner Questions

Topic: Proving subgoals with assumptions in other context

Lekhani Ray (Jul 01 2022 at 10:31):

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

1. ⋀n. plus n zero = n
2. ⋀n m. plus n (suc m) = suc (plus n m)
3. ⋀n. times n zero = zero
4. ⋀n m. times n (suc m) = plus (times n m) n
5. ⋀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: Apr 23 2024 at 16:19 UTC