Re: [isabelle] simple proof question



Ian Lynagh schrieb:
> Hi all,
> 
> I'm trying to write a simple proof in Isabelle, but I'm a little lost. I
> wonder if anyone can help me please? I've attached the script I have so
> far.
> 
> At the point at which I am stuck, I have
>     using this:
>         (EBool bool_, t) : STyping
> and I want to show that "t = TBool", which must be true as
>     STypingBool: "forall (b :: bool) ==> STyping (EBool b, TBool)"

For a start, your "forall (b :: bool) ==>" is a bit weird. Isabelle
accepted it but had to interpret "forall" as a free function variable to
make sense of it. Probably not what you meant. Note that "forall" is not
 Isabelle speak, and that outermost universal quantifiers can and should
be dropped. Just write "STyping (EBool b, TBool)".

Now the proof.

> is the only constructor matching that pattern. My best guess was
>     proof (cases this)

You cannot do a case distintinction on a theorem ("this") but only on a
term. This suggests

proof (cases t)

Although this step works, it does not get you anywhere. Before you start
the whole proof you should deduce some elimination rules that allow you
to move from "(EBool b, t) : STyping" to "t = TBool". This can be done
automatically:

inductive_cases STypingE[elim!]:
  "STyping (EBool b, t)"

The resulting lemma STypingE is what you need. The magic "[elim!]" tells
auto and blast and friends to apply this rule eagerly. Now your proof
should just be

from this have "t = TBool" by auto

Important: you will have to extend STypingE with other cases, at least

inductive_cases STypingE[elim!]:
  "STyping (EBool b, t)"
  "STyping (EInt n, t)"

Tobias


> but that says
>     *** empty result sequence -- proof command failed
>     *** At command "proof".
> Can anyone give me a pointer in the right direction please?
> 
> 
> I'm also not sure why I can't do
>     apply simpl
> immediately after
>     case EBool
> ? My goal here was to try to get "principalType (EBool bool)" to reduce.
> 
> 
> Finally, I'd also be very interested to know if the general structure
> looks sensible, or if there would be a more sensible way to write this
> sort of proof.
> 
> 
> Thanks
> Ian
> 
> 





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