Re: [isabelle] simp and type variables



Quoting Elsa L Gunter <egunter at cs.uiuc.edu>:

Dear Isabelle Users,
 Is there a way in Isabelle to specialize the type variables in a
theorem to type expressions using the type variables of a goal context?
 And in particular, can this be combined with simp?

The "of" theorem attribute can only instantiate schematic term variables. But the "where" attribute can be used to instantiate either type variables or term variables. For example:

lemma foo: "True = (ALL x. x = x)"
by simp

If you type "thm foo" with the "show types" option enabled, you'll see that there is a schematic type variable in this theorem:
True = (ALL x::?'a. x = x)

Now, if you type "thm foo [where 'a=nat]" you will get the instantiated version:
True = (ALL x::nat. x = x)

You can also instantiate a schematic type variable with a specific free type variable (which may be mentioned in your proof context). For example, "thm foo [where'a='b]" gives "True = (ALL x::'b. x = x)" (notice that 'b is fixed, not a schematic variable, since it lacks a question mark)

You should be able to use an instantiated version as a simp rule, as in:
apply (simp only: foo [where 'a=nat])

- Brian








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