*To*: Jun Inoue <jun.lambda at gmail.com>*Subject*: Re: [isabelle] rule Unifies With Chained Facts?*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Sat, 2 Apr 2011 08:00:27 -0700*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <x2wrjdyk3q.fsf@debian.localdomain.org>*References*: <x2wrjdyk3q.fsf@debian.localdomain.org>*Sender*: huffman.brian.c at gmail.com

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. 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". > (* 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

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

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

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

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