Re: [isabelle] problem with opening proof



On Fri, May 22, 2009 at 02:23, Florian Haftmann
<florian.haftmann at informatik.tu-muenchen.de> wrote:
> Hi Chris,
>
>> fix ...
>> assume ... and ...
>> thus "EX x y. ..."
>> proof
>
> "proof" is short for "proof default", where the "default" method performs:

In the Isar documentation it says "Unless given explicitly by the
user, the default initial method is “rule”". Is this inaccurate? I
suppose if the mode is not proof(chain) then default is the same as
rule? And otherwise it's the same as erule? In fact, the "default"
method isn't in the documentation's index at all.

> 1. introduction using a suitable predeclared rule if no facts are
> chained in.
>
> 2. elimination using a suitable predeclared rule if any facts are
> chained in.

Thanks, I totally didn't know that at all. It does explain things,
though, except...

> So in your case it fails because there are no suitable elimination rules
> for your assumptions.

But why does it also fail for "proof (rule exI)"? What's the
difference between rule and intro that allows the latter to succeed?

Chris Capel
-- 
"What is it like to be a bat? What is it like to bat a bee? What is it
like to be a bee being batted? What is it like to be a batted bee?"
-- The Mind's I (Hofstadter, Dennet)





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