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,

lemma "[| x; y |] ==> x & y"
  apply (rule conjI)
  apply (assumption)
  apply (assumption)

On Mon, Jun 30, 2008 at 7:38 PM, Erich Kummerfeld <ekummerfeld at>

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