Re: [isabelle] Instantiating to a lambda expression



On Sat, 2011-01-15 at 15:52 +0000, John Munroe wrote:
> If i have
> 
> consts
> foo :: "real => real"
> bar :: "real => real"
> 
> and an axiom
> 
> same_ax: "ALL (g1::real=>real) g2 x y. (y > x & g1 y - g1 x = g2 y -
> g2 x) --> g1 = g2"

Axioms are evil.  It's all too easy to introduce inconsistencies.
Here's a proof of False from same_ax:

  lemma "False"
    apply (cut_tac same_ax)
    apply (drule_tac x="%x. 0" in spec)
    apply (drule_tac x="%x. 1" in spec)
    apply (auto dest: fun_cong)
  done

(The problem is that the scope of x and y in same_ax extends all the way
to the end of the formula.)

> However, if I change the type of bar to:
> 
> bar :: "real => real => real", the following won't go through:
> 
> lemma lem1: "ALL x. foo x = bar x 3"
> proof -
>   have "ALL x y. y > x --> foo y - foo x = bar y 3 - bar x 3"
>     sorry
>   then obtain r1 r2 where #: "r2 > r1" and ##: "foo r2 - foo r1 = bar
> r2 3 - bar r1 3"
>     by auto
>   then show ?thesis
>     using same_ax
>     by auto

Here's a proof of lem1 that's similar to the one you provided:

lemma lem1: "ALL x. foo x = bar x 3"
proof -
  have "ALL x y. y > x --> foo y - foo x = bar y 3 - bar x 3"
    sorry
  then obtain r1 r2 where #: "r2 > r1" and ##: "foo r2 - foo r1 = bar
r2 3 - bar r1 3"
    by auto
  then show ?thesis
    using same_ax[rule_format, of _ _ _ "%x. bar x 3"]
    by (auto dest: fun_cong)
qed

Kind regards,
Tjark






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