*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] rule Unifies With Chained Facts?*From*: Jun Inoue <jun.lambda at gmail.com>*Date*: Fri, 01 Apr 2011 19:09:13 +0200*User-agent*: Gnus/5.13 (Gnus v5.13) Emacs/23.2 (gnu/linux)

Hi, I'm having trouble understanding how the rule/erule method interacts with the subtle difference between `this' and ==>. Given an introduction rule P - Q and a goal state with a chained fact (* call this state 1 *) using this: R goal: Q the tutorial says the rule method unifies only the Q's, but it appears to be matching P to R as well, failing if they don't match. But if the goal state were (* call this state 2 *) (`this' is empty) goal: R ==> Q then no matching seems to happen between P and R, and the method succeeds. I'm including a minimal concrete example below. A similar, but opposite, thing seems to happen with erule, which appears to (sometimes? always?) neglect chained facts when it searches for formulas to consume. So exactly which combinations of formulas do rule and erule unify? Where could I have found this information? 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'? Why wouldn't Isabelle do this massaging for me? (* Example: P = "n \<le> 1", Q = "n \<noteq> 2", and R = "n = 0". *) lemma the_rule_assm: fixes n :: int assumes "n \<le> 1" shows "n \<noteq> 2" using assms by arith (* The way the rule is declared makes no difference, as expected. *) lemma the_rule_imp: fixes n :: int shows "n \<le> 1 \<Longrightarrow> n \<noteq> 2" by arith (* 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 -- Jun Inoue

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

- Previous by Date: Re: [isabelle] Pairs/tuples
- Next by Date: Re: [isabelle] rule Unifies With Chained Facts?
- Previous by Thread: Re: [isabelle] Pairs/tuples
- 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