[isabelle] rule Unifies With Chained Facts?



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





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