How do I prove a subgoal with bound variables with assumptions that have schematic variable?

I am an isabelle noob. 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)"

Any reference to the assumptions ends up having schematic variables and I can only replace them with free variables. How do I deal with the issue? Any help is widely appreciate

Solution

Your locale definition does not mean what you think it does.

In your definition:

  assumes
     arith_1: "plus n zero = n"
    and plus_suc: "plus n (suc m) = suc ( plus n m)"

means that n and m are fixed in the entire locale. What you really want is:

  assumes
     arith_1: "⋀n. plus n zero = n"
    and plus_suc: "⋀n m. plus n (suc m) = suc ( plus n m)"

This seems a bit strange at first, because it is the same behavior as for the theorems, but not the most natural one.