Re: [isabelle] rule Unifies With Chained Facts?



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





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