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.