Re: [isabelle] Defines in locales in Isabelle 2009



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

locale foo =
  fixes x :: "'a => 'a => bool"
  and y :: "'a => 'a => bool"
  and P :: "'a => bool"
  and xs :: "'a => 'a => bool" ("_ ->* _")
  defines xs_def: "xs == (%a b. x a b & y a b)^**"
  assumes "a ->* b ==> P b"

interpretation f: foo["%a b. a > 0 & b <= Suc 0" "%a b. a < 10"
                      "%a.True"]

The feature that defined parameters may be omitted in interpretation has been withdrawn in an attempt to make defines more similar to assumes.

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.

Clemens





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