*To*: "Perry James" <perry at dsrg.org>*Subject*: Re: [isabelle] need help*From*: "Erich Kummerfeld" <ekummerfeld at gmail.com>*Date*: Tue, 1 Jul 2008 10:16:42 -0400*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <20d5caff0807010605u5c9fe8a1pabe7a11f0e21852a@mail.gmail.com>*References*: <e1cf6040806301638p43bbd405qc6725eaf490047de@mail.gmail.com> <20d5caff0807010605u5c9fe8a1pabe7a11f0e21852a@mail.gmail.com>

Hi Perry, The trick I'm trying to accomplish with the first problem actually ties into the second problem I'm having. Basically I'm trying to solve [| B x False; S x |] ==> False by transforming it into [| B x False & S x |] ==> False and then using the axiom I mentioned earlier. Neither of these steps appears to work though and that's my confusion. Best, Erich On Tue, Jul 1, 2008 at 9:05 AM, Perry James <perry at dsrg.org> wrote: > Hi Erich, > For your first question, I think you want to use an introduction rule > instead of an elimination. I haven't yet worked with axioms, so I'll leave > that to others. > Hope this helps, > Perry > > lemma "[| x; y |] ==> x & y" > apply (rule conjI) > apply (assumption) > apply (assumption) > done > > > > On Mon, Jun 30, 2008 at 7:38 PM, Erich Kummerfeld <ekummerfeld at gmail.com> > wrote: > >> Hi, >> >> I'm fairly new to Isabelle and sequent calculus in general and am having a >> couple difficulties. The first regards applying the conjI rule to a >> hypothesis. When I apply (drule conjI) to [| y; x|] ==> x & y I expect to >> get x & y ==> x & y, but instead get 1. y ==> ?Q 2. [| y; x & ?Q |] ==> x >> & >> y. Being able to deduct forwards from a hypothesis of form [| x; y |] to >> get a new hypothesis of form x & y is my goal here. >> >> The second problem I'm having is with the defining and use of axioms. >> This >> is the code I'm using: >> >> consts >> S :: "'a => bool" >> B :: "'a => bool => bool" >> >> axioms >> sb: "((B x y) & (S x) ==> y" >> >> I'm not certain how I am defining or using these wrong, but when I try to >> use it in a theorem it does not do what I expect it to. >> >> theorem "((B x z) & (S x) ==> z" >> apply (simp add: sb) >> >> yields the empty result sequence error rather than the "no subgoals!" that >> I >> would expect. >> >> Thanks in advance for the help, I've been hammering at these problems all >> day and have been able to boil them down to these simple cases but have no >> idea why they are failing. >> >> -Erich Kummerfeld >> > >

**Follow-Ups**:**Re: [isabelle] need help***From:*Lawrence Paulson

**Re: [isabelle] need help***From:*Jeremy Dawson

**References**:**[isabelle] need help***From:*Erich Kummerfeld

**Re: [isabelle] need help***From:*Perry James

- Previous by Date: Re: [isabelle] need help
- Next by Date: Re: [isabelle] need help
- Previous by Thread: Re: [isabelle] need help
- Next by Thread: Re: [isabelle] need help
- Cl-isabelle-users July 2008 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