*To*: Brian Huffman <brianh at cs.pdx.edu>*Subject*: Re: [isabelle] rule Unifies With Chained Facts?*From*: Jun Inoue <jun.lambda at gmail.com>*Date*: Sun, 03 Apr 2011 01:28:29 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <AANLkTi=pe3_ONb9dQ8nZFeadm9=fQJGgWJfnGnnGmba0@mail.gmail.com> (Brian Huffman's message of "Sat, 2 Apr 2011 08:00:27 -0700")*References*: <x2wrjdyk3q.fsf@debian.localdomain.org> <AANLkTi=pe3_ONb9dQ8nZFeadm9=fQJGgWJfnGnnGmba0@mail.gmail.com>*User-agent*: Gnus/5.13 (Gnus v5.13) Emacs/23.2 (gnu/linux)

Brian Huffman <brianh at cs.pdx.edu> writes: > On Fri, Apr 1, 2011 at 10:09 AM, Jun Inoue <jun.lambda at gmail.com> wrote: >> (* call this state 1 *) >> using this: >> R >> goal: >> Q > [...] >> (* call this state 2 *) >> (`this' is empty) >> goal: >> R ==> Q > [...] >> When I have state 1, how do I massage it into state 2 so that I can >> invoke rule without unifying the rule's premises to anything, or erule >> with unification to `this'? > > Hi Jun, > > This particular question, at least, has an easy answer: just use > "apply -", i.e. use the method whose name is just a single hyphen. Its > only effect is to add any chained facts to the goal as ordinary > assumptions. It is often used in structured proofs with "proof -", > where it is usually a no-op. Another pattern that you can find in the > sources is "by - (rule foo, simp)" or similar. I have also used "by - > (rule exI)" in several places in HOLCF where "by (rule exI)" fails for > some reason. Hi Brian, thanks for the tip! I was trying "by (-, rule foo)", but now I see why that was no good. :) For the record, if anyone reads this in the archives: "by - (rule foo)" performs two separate method calls, a no-op and (rule foo), which automatically induces a "stick assumptions into the premises" step in between, whereas "by (-, rule foo)" performs one call to a single, composite method which does nothing special in between the no-op and (rule foo). > > It is a bit confusing how "rule" treats chained facts in a special > way, when nearly all other methods start by adding any chained facts > into the goal as premises before continuing with their normal > behavior. It is also a bit inconvenient that there is no single method > that has the "insert chained facts, then apply a rule" behavior; but > at least there is an easy workaround with "-" followed by "rule". I tripped over this separation between assumptions before, when I found that "show" doesn't unify exported premises with any pending goal's premises but only assumptions with goals' premises. Why does Isar have this (IMHO idiosyncratic) distinction between assumptions and premises? I suppose it's there for a reason, but to me it seems like Isar would be more streamlined and novice-friendly if the two notions are identified, or always automatically bridged. PS. Not to be too nosy here, but if the authors of the Isabelle Tutorial ever see this, please consider making a little note of this behavior of "rule" in Section 5.7 (or maybe in the "Structured Proofs in Isar/HOL" document). Clearly pointing out the general difference between assumptions and premises could be even better... > >> (* The way the theorem to prove with the rule is declared does make >> a difference, as is highly unexpected. *) >> theorem test_assm: >> fixes n :: int >> assumes "n = 0" >> shows "n \<noteq> 2" >> using assms >> (* Unification fails using either of the rules defined above, >> apparently trying to match n \<le> 1 with n = 0". *) >> (*apply (rule the_rule_assm) (* Clash: HOL.eq =/= Orderings.ord_class.less_eq *)*) >> (* apply (rule the_rule_imp) (* Clash: HOL.eq =/= Orderings.ord_class.less_eq *)*) >> oops >> >> (* The same rules work, apparently without trying to >> unify n \<le> 1 with n = 0, if the lemmas are stated >> this way. *) >> theorem test_imp: >> fixes n :: int >> shows "n = 0 \<Longrightarrow> n \<noteq> 2" >> using assms >> apply (rule the_rule_assm) (* works *) >> oops >> >> theorem test'': >> fixes n :: int >> shows "n = 0 \<Longrightarrow> n \<noteq> 2" >> using assms >> apply (rule the_rule_imp) (* works *) >> oops > > The theorem list "assms" only includes propositions listed in > "assumes" clauses. Since there are no "assumes" clauses in either of > the last two theorems, "assms" is actually empty, so there are no > chained facts, and "rule" doesn't try to unify with any assumptions. > > - Brian > -- Jun Inoue

**Follow-Ups**:**Re: [isabelle] rule Unifies With Chained Facts?***From:*Rafal Kolanski

**Re: [isabelle] rule Unifies With Chained Facts?***From:*Makarius

**References**:**[isabelle] rule Unifies With Chained Facts?***From:*Jun Inoue

**Re: [isabelle] rule Unifies With Chained Facts?***From:*Brian Huffman

- Previous by Date: Re: [isabelle] Converting apply-style induction to Structured Isar
- Next by Date: Re: [isabelle] rule Unifies With Chained Facts?
- Previous by Thread: Re: [isabelle] rule Unifies With Chained Facts?
- Next by Thread: Re: [isabelle] rule Unifies With Chained Facts?
- Cl-isabelle-users April 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