Delivery-Date: 
Sender: info-hol-request@cs.uidaho.edu
Errors-To: info-hol-request@cs.uidaho.edu
Precedence: bulk
From: Konrad Slind <slind@informatik.tu-muenchen.de>
To: info-hol@cs.uidaho.edu
Subject: jjj proof challenge
Message-Id: <93Sep9.232007met_dst.8081@sunbroy14.informatik.tu-muenchen.de>
Date: Thu, 9 Sep 1993 23:20:05 +0200


A simple form of a conversion that ought to be standard in HOL is the
following: 

    val MOVE_QUANTS_IN_CONV = 
       REDEPTH_CONV 
          (FORALL_IMP_CONV ORELSEC FORALL_AND_CONV ORELSEC FORALL_OR_CONV 
           ORELSEC 
           EXISTS_AND_CONV ORELSEC EXISTS_IMP_CONV ORELSEC EXISTS_OR_CONV)
       THENC REWRITE_CONV[];

With it, a HOL proof would look almost identical to those done in IMPS
and EVES. Indeed, as Josh mentioned, the main problem in the proof is
the confusion caused by quantifiers having loose scopes.

   - g `!P Q R x.
           ?(v:'a) (w:'b).
            !y z. P x /\ Q y ==> (P v \/ R w) /\ (R z ==> Q v)`;
   = =
   (--`!P Q R x. ?v w. !y z. P x /\ Q y ==> (P v \/ R w) /\ (R z ==> Q v)`--)
   =============================


   - e (CONV_TAC MOVE_QUANTS_IN_CONV);
   OK..
   1 subgoal:
   (--`!P Q.
         (?x. P x) /\ (?y. Q y) ==>
         (!R. ?v. (P v \/ (?w. R w)) /\ ((?z. R z) ==> Q v))`--)
   =============================


   - e (REPEAT (GEN_TAC ORELSE STRIP_TAC));
   OK..
   1 subgoal:
   (--`?v. (P v \/ (?w. R w)) /\ ((?z. R z) ==> Q v)`--)
   =============================
     (--`P x`--)
     (--`Q y`--)


   - e (EXISTS_TAC (--`(?w:'b. R w) => y | x :'a`--) THEN 
        COND_CASES_TAC THEN ASM_REWRITE_TAC[]);
   OK..

   Top goal proved.
   |- !P Q R x. ?v w. !y z. P x /\ Q y ==> (P v \/ R w) /\ (R z ==> Q v)