Re: [isabelle] rule Unifies With Chained Facts?



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





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