Email Gateway (Aug 18 2022 at 15:13): Email Gateway (Aug 18 2022 at 15:13):From: John Munroe <munddr@gmail.com>
Hi all,
I have a rather basic question:
Given the following constants and axioms:
typedecl T1
consts
F :: "T1 \<Rightarrow> real"
G :: "T1 \<Rightarrow> real"
C :: real
axioms
ax1: "\<exists>P. \<exists>s1\<in>P. \<exists>s2\<in>P. s1 \<noteq>
s2 \<and> F s1 < F s2 \<and> G s1 <= G s2"
ax1a: "\<exists>P. \<forall>s1\<in>P. \<forall>s2\<in>P. s1 \<noteq>
s2 \<and> F s1 < F s2 \<and> G s1 <= G s2"
ax2: "F p > 0"
ax3: "C > 0"
I can prove that "\<exists> func s. func s \<noteq> (\<lambda> s. (F
s, (C / F s)))" with
lemma lem1: "\<exists> func s. func s \<noteq> (\<lambda> s. (F s, (C / F s)))"
proof (intro exI)
have "\<forall> s1 s2 t. (F s1< F s2) --> (C / F s1) > (C / F s2)"
using ax3 ax2
by (simp add: divide_inverse real_less_def)
then show "(\<lambda> s. (F s, G s)) \<noteq> (\<lambda> s. (F s, (C
/ F s)))"
using ax1
apply (intro notI)
apply (simp add: expand_fun_eq real_mult_commute)
by (metis linorder_not_le)
qed
However, if I want to not use ax1 but use ax1a instead, the proof
breaks. Isn't ax1a stronger than ax1? If so, why can a proof using ax1
break when a stronger ax1a is used as a fact instead?
Any help will be appreciated.
Thanks
John
Email Gateway (Aug 18 2022 at 15:13):From: Lawrence Paulson <lp15@cam.ac.uk>
It is not stronger than ax1. In fact, ax1a can be proved as a theorem using auto. This is because P could simply denote the empty set.
Larry Paulson
Email Gateway (Aug 18 2022 at 15:13):From: Lawrence Paulson <lp15@cam.ac.uk>
This new version of your axiom still provable using auto and therefore completely weak. You might have better luck with this formulation:
lemma "\<exists>P. P \<noteq> {} \<and> (\<forall>s1\<in>P. \<forall>s2\<in>P. s1 \<noteq> s2 \<and> F s1 < F s2 \<and> G s1 <= G s2)"
Larry Paulson
Email Gateway (Aug 18 2022 at 15:13):From: John Munroe <munddr@gmail.com>
I see. But even if ax1 was:
ax1: "\<exists>P. \<exists>s1\<in>P. \<exists>s2\<in>P. P \<noteq> {}
\<and> s1 \<noteq> s2 \<and> F s1 < F s2 \<and> G s1 <= G s2"
and ax1a was:
ax1a: "\<exists>P. \<forall>s1\<in>P. \<forall>s2\<in>P. P \<noteq> {}
\<and> s1 \<noteq> s2 \<and> F s1 < F s2 \<and> G s1 <= G s2"
The second part of the proof still breaks. Am I supposed to simplify
the goal further?
Thanks
John
Email Gateway (Aug 18 2022 at 15:32):From: Tim McKenzie <tjm1983@gmail.com>
Certainly this will make it easier to prove the desired result, since
this formulation (as an axiom) allows you to derive a contradiction.
See attached.
Timothy
<><
Scratch.thy
Last updated: Apr 25 2024 at 01:08 UTC