Re: [isabelle] trivial proof to solve/reply


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 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 

 \<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.


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