Email Gateway (Aug 18 2022 at 10:03): Email Gateway (Aug 18 2022 at 10:03):From: Tjark Weber <tjark.weber@gmx.de>
Clint,
On Friday 12 January 2007 17:44, clefort wrote:
I'm using straight Isar,Isabelle:
Isabelle comes with several object logics, e.g. HOL, FOL, ZF. (See
http://isabelle.in.tum.de/logics.html for details.) I was wondering
which one you are using. In ProofGeneral, you can check "Isabelle >
Logics" (the default is HOL, unless you changed it).
The F,S,HS and EQ are uninterpreted functions.
I'm attaching a copy of the trivial.thy file. Unfortunately I cannot
find a way to copy the goals.
,-----
lemma "\<forall>x. \<forall>y. \<forall>z. EQ(F(e,c),S(e,c),EQ(e,c))
\<and> EQ(HS(e,co),F(e,c),S(e,c))
\<Longrightarrow> \<forall>x. \<forall>y.
\<forall>z. EQ(S(e,c),F(e,c),HS(e,c))"
`-----
This lemma is different from the one that you posted earlier. It parses
fine now, but note that the bound variables (x, y, z) do not occur in the
formula at all.
,-----
apply (rule conjunct1)
apply (rule conjunct2)
apply (rule conjE)
apply (auto)
`-----
The first three of these apply statements are useful only for goals that
contain conjunctions. For your lemma, they are useless at best. Just
leave them away.
"apply auto" discards the redundant quantifiers to produce the following
subgoal:
\<lbrakk>EQ (F (e, c), S (e, c), EQ (e, c));
EQ (HS (e, co), F (e, c), S (e, c))\<rbrakk>
\<Longrightarrow> EQ (S (e, c), F (e, c), HS (e, c))
This subgoal is not provable if you have no additional information about the
functions involved. Isabelle can even give you an interpretation that makes
the formula false: try "Isabelle > Commands > refute" in ProofGeneral.
Best,
Tjark
Last updated: May 03 2024 at 04:19 UTC