Re: [isabelle] Several proof methods in one proof?



Victor Porton schrieb:
> I incidentally wrote:
> 
> lemma comp_fun2: "[| g: A->B1; f: B0->C; B1<=B0 |] ==> (f O g) : A->C"
> proof -
>   assume "g: A->B1" "f: B0->C" "B1<=B0"
>   with `g: A->B1` have "g: A->B0" by auto (rule fun_weaken_type)
>   with `f: B0->C` show "(f O g) : A->C" sorry
> qed
>  
> Surprisingly it works. But I don't understand what "auto (rule
> fun_weaken_type)" means. Is it both "auto" and "(rule fun_weaken_type)"?
> If yes, in which order these proof methods are applied?

That's a special idiom where the two proof methods are applied in
succession (from left to right). Doesn't work for three or more methods ;-)

> Which .pdf to read about that? Should I read a manual (tutorials seem
> not enough)?

You will find a precise description in the Isar reference manual.
Introductory manuals probably do not mention it.

Tobias

> -- 
> Victor Porton - http://portonvictor.org





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