# Re: [isabelle] schematic variables

```Hello Mamoun,

Your example does not contain schematic variables after unfolding with
ref_def.  Instead, the goal looks as follows:

\<forall>s. (A \<union> B) s \<longrightarrow> (A' \<union> B') s

The most common form to instantiate schematic variables in facts is
via the "of" attribute, for example as follows:

thm refl  (* is "?t = ?t" *)

thm refl[of x]  (* is "x = x" *)

This can also be applied to intermediate steps in a proof:

lemma "\<exists>n::nat. n \<ge> 0"
proof -
{
fix n :: nat
have "n \<ge> 0" by simp
}
(* we proved "?n \<ge> 0" *)
note this[of "1 :: nat"]  (* is "1 \<ge> 0" *)
then show ?thesis ..
qed

A different form of this proof introduces schematic variables into the
goal, but in most cases it's best to let some tactic instantiate
these variables automatically:

lemma "\<exists>n::nat. n \<ge> 0"
apply (rule exI)  (* the goal is now "?n \<ge> 0" *)
apply simp  (* instantiates "?n" appropriately and solves the goal *)
done

Cheers,
Sascha

Mamoun FILALI-AMINE wrote:
> Hello,
>
>   I wonder if it is possible to instantiate schematic variables
> after unfolding (see example below).
> thanks
>
> Mamoun
>
> --------
>
> definition "ref P Q = (\<forall> s. P s \<longrightarrow> Q s)"
>
> theorem
>   assumes r1: "ref A A'"
>   assumes r2: "ref B B'"
> shows "ref (A \<union> B) (A' \<union> B')"
> proof -
>   have "?thesis" unfolding ref_def (* is "\<forall> s. ?L s
> \<longrightarrow> ?R s" *)
>

> begin:vcard
> fn:Mamoun FILALI-AMINE
> n:FILALI-AMINE;Mamoun
> adr;quoted-printable:118 Route de Narbonne;;IRIT Universit=C3=A9 Paul Sabatier;Toulouse;;31062 cedex 9;France
> email;internet:filali at irit.fr
> tel;work:00 33 5 61 55 69 26
> tel;fax:00 33 5 61 55 64 48
> version:2.1
> end:vcard
>

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.