Email Gateway (Jun 30 2022 at 12:10): Email Gateway (Jun 30 2022 at 12:10):From: Lekhani Ray <rayl1@mcmaster.ca>
Hello Isabelle users,
I am fairly new to Isabelle, hence I apologize if the question may seem silly.
I have a sublocale that gives me subgoals that have bound variables. The
subgoals are exact copies of assumptions I have inside some other locales.
When I instantiate them, they can only be done with free variables. How do I
work around this issue?
Given here are my 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))
Here is an (just a few) of the assumptions I will need to use
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, any reference to them ends up having schematic variables which I can
only replace with free variables. I was wondering how to work around this
issue?
Thank you,
Lekhani Ray
M.Sc, Computer Science
Computing and Software
C : +1 289-244-9754
Outlook-wohzql0e.jpg
Last updated: Jan 04 2025 at 20:18 UTC