Re: [isabelle] need help



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




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