Re: [isabelle] Defines in locales in Isabelle 2009



On Wed, 22 Apr 2009, Clemens Ballarin wrote:

Quoting Andreas Lochbihler <lochbihl at ipd.info.uni-karlsruhe.de>:

2nd try:

interpretation f: foo "%a b. a > 0 & b <= Suc 0" "%a b. a < 10"
                     "%a. True"
                     "(%a b. a > 0 & b <= Suc 0 & a < 10)^**"

Now the explicit parameter is given, but unfold_locales nor
intro_locales longer work any longer (empty result sequence).

In apply-style you can do "apply -" to break up the goal followed by explicit goal addressing ("apply unfold_locales [1]" or similar). In proper Isar proofs, "proof" breaks up the goal for you.

In fact, this break up of simultaneous goals is implicit in any regular method application (with the exception of special simultaneous methods like "induct").

This means you can finish the proof script like this:

interpretation f:
  foo "%a b. a > 0 & b <= Suc 0" "%a b. a < 10" "%a. True"
    "(%a b. a > 0 & b <= Suc 0 & a < 10)^**"
  apply (unfold_locales)[1]
   apply (rule TrueI)
  apply simp
  done


	Makarius





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