Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from dworshak.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Thu, 9 Sep 1993 10:50:23 +0100
Received: by dworshak.cs.uidaho.edu (1.37.109.4/16.2) id AA24840;
          Thu, 9 Sep 93 02:44:21 -0700
Sender: info-hol-request@cs.uidaho.edu
Errors-To: info-hol-request@cs.uidaho.edu
Precedence: bulk
Received: from arbi.Informatik.Uni-Oldenburg.DE by dworshak.cs.uidaho.edu 
          with SMTP (1.37.109.4/16.2) id AA24836; Thu, 9 Sep 93 02:43:22 -0700
Received: by arbi.informatik.uni-oldenburg.de (smail3.1.18 + xalias);
          Thu, 9 Sep 93 11:43 CES
Received: by aragorn.Informatik.Uni-Oldenburg.DE (Smail3.1.22.1) 
          id <m0oaiJF-0000hyC>; Thu, 9 Sep 93 11:28 CES
Received: from murphy.theorie by theoretica (4.1/SMI-4.1) id AA16684;
          Thu, 9 Sep 93 11:28:52 +0200
From: Juergen Bohn <Juergen.Bohn@arbi.informatik.uni-oldenburg.de>
Message-Id: <9309090928.AA16684@theoretica>
Subject: Re: a little proof challenge,2nd try
To: wishnu@cs.ruu.nl (Wishnu Prasetya)
Date: Thu, 9 Sep 1993 11:28:47 +0200 (MET DST)
Cc: info-hol@cs.uidaho.edu
In-Reply-To: <199309090848.AA01748@infix.cs.ruu.nl> from "Wishnu Prasetya" at Sep 9, 93 10:48:48 am
X-Mailer: ELM [version 2.4 PL20]
Content-Type: text
Content-Length: 3107

Re: Wishnu Prasetya
> 
>   > pushGoal libPenv
>   > "G // H |- exists v,w,y,z. (P x /\\ Q y) ->> ((P v \\/ R w) /\\ (R z ->> Q v))";
> 
> Correct me if I'm wrong, especially as I have NO experience with
> LAMBDA. But I gather from the code above that you're trying to prove
> 
>    "? v w y z. etc etc..."
> 
> while in the original problem it was:
> 
>    "?v w. !y z. etc etc..."

Sorry, my mistake. Here comes my second attempt. The proof is similar
to the first. The function `constGuide' computes a (LAMBDA-) guide to
the given subexpression. `omChoiceL' is something like case induction.
Of course I can combine the rule and tactic applications to one single
tactic. There is no predefined tactic which solves this goal (see mail
of Tobias Nipkow).

- Juergen
-- 
        Juergen Bohn	        |    Phone :   ++49-441-798-3122
 FB10 theoretische Informatik   |    FAX   :   ++49-441-798-2155
    Universitaet Oldenburg      |    EMail :       Juergen.Bohn@
        Postfach 2503  	        |    Informatik.Uni-Oldenburg.DE
      D-26111 Oldenburg         |       or :  uniol!Juergen.Bohn
--
pushGoal libPenv
"G // H |- exists v,w. forall y,z. (P x /\\ Q y) ->> ((P v \\/ R w) /\\ (R z ->> Q v))";
 
*******   LEVEL 1   *******
1: G // H
   |- exists v,w. forall y,z. P x /\ Q y ->> (P v \/ R w) /\ (R z ->> Q v)
   -----------------------------------------------------------------------
   G // H
   |- exists v,w. forall y,z. P x /\ Q y ->> (P v \/ R w) /\ (R z ->> Q v)
 
> at (rew allScopeRules);
 
*******   LEVEL 2   *******
1: G // H
   |- P x /\ (exists x. Q x)
      ->> exists x1. (P x1 \/ (exists x. R x)) /\ ((exists x. R x) ->> Q x1)
   -------------------------------------------------------------------------
   G // H
   |- exists v,w. forall y,z. P x /\ Q y ->> (P v \/ R w) /\ (R z ->> Q v)
 
> apprl impR;

*******   LEVEL 3   *******
1: G // P x /\ exists x. Q x $ H
   |- exists x1. (P x1 \/ (exists x. R x)) /\ ((exists x. R x) ->> Q x1)
   -----------------------------------------------------------------------
   G // H
   |- exists v,w. forall y,z. P x /\ Q y ->> (P v \/ R w) /\ (R z ->> Q v)
 
> apprl' (constGuide "exists x. R x") omChoiceL;

*******   LEVEL 4   *******
2: G // (exists x. R x) == FALSE $ P x /\ exists x. Q x $ H
   |- exists x. (P x \/ FALSE) /\ (FALSE ->> Q x)
1: G // (exists x. R x) == TRUE $ P x /\ exists x. Q x $ H
   |- exists x. (P x \/ TRUE) /\ (TRUE ->> Q x)
   -----------------------------------------------------------------------
   G // H
   |- exists v,w. forall y,z. P x /\ Q y ->> (P v \/ R w) /\ (R z ->> Q v)
 
> applyTacAll (rew []);
    
*******   LEVEL 5   *******
1: G // NOT (exists x. R x) $ P x /\ exists x. Q x $ H |- exists x. P x
   -----------------------------------------------------------------------
   G // H
   |- exists v,w. forall y,z. P x /\ Q y ->> (P v \/ R w) /\ (R z ->> Q v)
 
> at ( (instExRTac "x") thenT (rew []) );
 
*******   LEVEL 6   *******
   -----------------------------------------------------------------------
   G // H
   |- exists v,w. forall y,z. P x /\ Q y ->> (P v \/ R w) /\ (R z ->> Q v)