Re: [isabelle] need help
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)
On Mon, Jun 30, 2008 at 7:38 PM, Erich Kummerfeld <ekummerfeld at gmail.com>
> 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:
> S :: "'a => bool"
> B :: "'a => bool => bool"
> 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
> 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