# 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.