*To*: clefort <ipub at charter.net>*Subject*: Re: [isabelle] trivial proof to solve/reply*From*: Tjark Weber <tjark.weber at gmx.de>*Date*: Fri, 12 Jan 2007 18:38:09 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <216CEFA6-6EAB-4C3C-A385-66FA5974B400@charter.net>*References*: <19460EC2-DDF2-4FB6-8A44-578566CCA8F9@charter.net> <200701121728.47493.tjark.weber@gmx.de> <216CEFA6-6EAB-4C3C-A385-66FA5974B400@charter.net>*User-agent*: KMail/1.8

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

**References**:**[isabelle] trivial proof to solve***From:*clefort

**Re: [isabelle] trivial proof to solve***From:*Tjark Weber

- Previous by Date: Re: [isabelle] trivial proof to solve
- Next by Date: Re: [isabelle] Questios about evaluation and code extraction
- Previous by Thread: Re: [isabelle] trivial proof to solve
- Next by Thread: [isabelle] Questios about evaluation and code extraction
- Cl-isabelle-users January 2007 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list