Email Gateway (Aug 18 2022 at 14:30): Email Gateway (Aug 18 2022 at 14:30):From: Steve W <s.wong.731@googlemail.com>
Hi,
I'm trying out addition in Real, but have run into some problems. Does
anyone know why the first example below doesn't work but the second does? Is
it a problem with the types?
1)
theory Test
imports Real
begin
typedecl T
consts
F :: "T => real"
t :: "T"
axioms
ax : "F(t) = 0"
lemma test: "EX x. F(x) + 1 ~= 0"
using ax
by auto
2)
theory Test
imports Real
begin
typedecl T
consts
F :: "T => real"
t :: "T"
axioms
ax : "F(t) = 0"
lemma test: "EX x. F(x) + 0 = 0"
using ax
by auto
Thanks in advance for any help.
Regards,
Steve
Email Gateway (Aug 18 2022 at 14:31):From: Brian Huffman <brianh@cs.pdx.edu>
On Wed, Jan 20, 2010 at 7:51 PM, Steve W <s.wong.731@googlemail.com> wrote:
I'm trying out addition in Real, but have run into some problems. Does
anyone know why the first example below doesn't work but the second does? Is
it a problem with the types?
Hi Steve,
This is not a problem with the types. It works exactly the same with
type int or rat as it does with real.
axioms
ax : "F(t) = 0"lemma test: "EX x. F(x) + 1 ~= 0"
using ax
by auto
You should realize that you are asking a lot of "auto" here, since
proving this lemma requires it to guess a witness for the existential
quantifier. The "auto" tactic can only guess witnesses in very limited
circumstances.
axioms
ax : "F(t) = 0"lemma test: "EX x. F(x) + 0 = 0"
using ax
by auto
Your second example happens to be one of the limited circumstances
where auto can solve an existential. Simplification replaces "F(x) +
0" with "F(x)", leaving the subgoal
"EX x. F(x) = 0"
which just happens to match up perfectly with the rule "ax" that you
provided. In general, you should only expect "auto" to solve
existentials if they can be solved in one step by rule exI.
Other tactics besides "auto" are better at solving existentials. For
example, the "metis" tactic can solve your goal:
lemma test: "EX x. F(x) + 1 ~= 0"
using ax
by (metis one_neq_zero add_0_left)
The drawback with metis is that you need to supply all the other
lemmas needed to solve the goal.
In the end, it is often easiest to just provide the witness yourself:
lemma test: "EX x. F(x) + 1 ~= 0"
proof
show "F(t) + 1 ~= 0"
using ax by simp
qed
Hope this helps,
Last updated: Apr 26 2024 at 08:19 UTC