Re: [isabelle] need help



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.