*To*: Mamoun FILALI-AMINE <filali at irit.fr>*Subject*: Re: [isabelle] schematic variables*From*: Sascha Boehme <boehmes at in.tum.de>*Date*: Sun, 7 Aug 2011 13:26:19 +0200*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <4E3E6287.9090109@irit.fr>*References*: <4E3E6287.9090109@irit.fr>*User-agent*: Mutt/1.5.21 (2010-09-15)

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 >

**Follow-Ups**:**Re: [isabelle] schematic variables***From:*Mamoun FILALI-AMINE

**References**:**[isabelle] schematic variables***From:*Mamoun FILALI-AMINE

- Previous by Date: [isabelle] schematic variables
- Next by Date: Re: [isabelle] code generation for saturated naturals
- Previous by Thread: [isabelle] schematic variables
- Next by Thread: Re: [isabelle] schematic variables
- Cl-isabelle-users August 2011 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list