Re: [isabelle] schematic variables



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



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