*To*: isabelle-users at cl.cam.ac.uk*Subject*: Re: [isabelle] schematic variables*From*: Mamoun FILALI-AMINE <filali at irit.fr>*Date*: Wed, 10 Aug 2011 11:12:22 +0200*In-reply-to*: <20110807112618.GA823@eloas>*Organization*: IRIT CNRS Université de Toulouse*References*: <4E3E6287.9090109@irit.fr> <20110807112618.GA823@eloas>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.6; rv:5.0) Gecko/20110624 Thunderbird/5.0

Hello, After discussing with Sascha Boehme, it seems to be technically impossible to match a goal against a pattern after unfolding with some rewrite rule: definition "foo x = bar x x" ... have "foo (f x)" (is "foo ?X") [pattern is possible] unfolding foo_def (is "bar ?X _") [pattern is not possible] However, according to Sascha, most of the time proofs can be restructured to avoid this need or Isabelle's proof methods (e.g., simp or auto) can collapse relevant proof steps such that these patterns are not necessary. Mamoun Le 07dimanche/08/11 7 à 13: 19, Sascha Boehme a écrit :

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

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:*Makarius

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

**Re: [isabelle] schematic variables***From:*Sascha Boehme

- Previous by Date: Re: [isabelle] Odd failure to match local statement with pending goal.
- Next by Date: Re: [isabelle] Question regarding sequent calculi in Isabelle
- Previous by Thread: Re: [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