Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Proving subgoals with bound variables with ass...


view this post on Zulip 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

E: rayl1@mcmaster.ca

![](cid:c769f1b5-f9e0-47ae-b86a-9d4d72fc61fc)
Outlook-wohzql0e.jpg


Last updated: Mar 29 2024 at 12:28 UTC