Re: [isabelle] Difficulties with Isar proofs and fix



On Mon, 25 Feb 2008, Denis Bueno wrote:

> Basically I have a theorem whose conclusion is of the form: ALL x. ...
> (EX y. ... (ALL z. ...)).  I would like to show this by fix'ing an
> arbitrary x, exhibiting a y, and fix'ing an arbitrary z, then
> satisfying the respective bodies of each quantification.

Here is your proof in Isar:

lemma "ALL x :: 'a. EX y :: 'b. ALL z :: 'c. P x y z"
proof
  fix a :: 'a
  def b == "t :: 'b"
  have "ALL z. P a b z" 
  proof
    fix c
    show "P a b c" sorry
  qed
  then show "EX y. ALL z. P a y z" ..
qed

(Note that type constraints are needed here, because of the fully abstract 
formulation of the problem and sub-problems.)

Isar is very ``puristic'' in the sense in being ignorant of predicate 
logic.  The native way of expressing statements and proofs is via the 
Isabelle/Pure logical framework, which provides very powerful means to 
work with higher-order Natural Deduction rules.  Maybe the paper 
http://www4.in.tum.de/~wenzelm/papers/isar-framework.pdf helps to 
understand the basic approach.

In the above text there are certain situations where single introduction 
or elimination rules get involved; these are made explicit here:

lemma "ALL x :: 'a. EX y :: 'b. ALL z :: 'c. P x y z"
proof (rule allI)
  fix a :: 'a
  def b == "t :: 'b"
  have "ALL z. P a b z" 
  proof (rule allI)
    fix c
    show "P a b c" sorry
  qed
  then show "EX y. ALL z. P a y z" by (rule exI)
qed

This is indeed a bit awkward, so one could blame Isar for not supporting 
``standard'' logical connectives more directly.  On the other hand, by 
making proper use of Pure principles, things work out smoothly not just 
for ALL/EX, but any concept you have introduced in your application.  The 
idea is to derive intro/elim rules from your definitions, or even better 
let the system do it for you (using the 'inductive' package) as hinted in 
section 4.6 of the above article.

> theorem proposition_1_oif:
>   assumes S_Prop: "S : Prop"
>   and     S_SP:   "S : SP"
>   shows   lift_S_SHP: "[[S]] : SHP"
> apply (unfold SHP_def, unfold shp_def)
> apply (simp)
> (* at this point the goal is:
> ALL T. T : Prop & T ~: [[ S ]] -->
>            (EX M. M : Obs & M <| T & (ALL T'. T' : Prop & M <| T' -->
> T' ~: [[ S ]]))
> *)
> proof
>   fix T :: property
>   assume T_st: "T : Prop" "T ~: [[S]]"
> 
>   obtain M where M_st: "M : Obs" "M <| T" sorry
> 
>   fix T' :: property
>   assume T'_st: "T' : Prop" "M <| T'"
> 
>   hence "T' ~: [[ S ]]" sorry
>   with T'_st have "T' : Prop & M <| T' --> T' ~: [[ S ]]" by blast
>   hence "ALL T'. T' : Prop & M <| T' --> T' ~: [[ S ]]" ..

If you provide a working theory, we can play with it a little.  For the 
moment here are some general hints:

  * The abbreviations 'hence' for 'then have' and 'thus' for 'then show' 
    are better avoided, because they demand much more typing.  This 
    paradox is explained by the experience that the goal prefixing often 
    changes in proof development and massaging, e.g. 'then have' vs. 'from 
    blah have' vs. 'with blubb have' etc.

  * Local facts can be referenced literally, e.g. `S : Prop` (with ASCII 
    backquotes); no need to emulate the structure of statements in names 
    like S_Prop.


	Makarius





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