Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Tue, 22 Mar 1994 19:36:41 +0000
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA29177;
          Tue, 22 Mar 1994 12:24:41 -0700
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Received: from Maui.CS.UCLA.EDU by leopard.cs.byu.edu 
          with SMTP (1.37.109.8/16.2) id AA29173;
          Tue, 22 Mar 1994 12:24:39 -0700
Received: from LocalHost.cs.ucla.edu by maui.cs.ucla.edu (Sendmail 4.1/3.25) 
          id AA05504; Tue, 22 Mar 94 11:24:24 PST
Message-Id: <9403221924.AA05504@maui.cs.ucla.edu>
To: info-hol@leopard.cs.byu.edu
Subject: Conversions for eliminating conditionals from a formula
Date: Tue, 22 Mar 94 11:24:23 PST
From: chou@cs.ucla.edu

Some of you may find the following conversions useful.  Two examples:

- COND_CONJ_CONV (--`((x=3) => f | g)(5) = h((x=3) => f | g) + 7`--) ;
val it =
  |- (((x = 3) => f | g) 5 = h ((x = 3) => f | g) + 7) =
     ((x = 3) ==> (f 5 = h f + 7)) /\ (~(x = 3) ==> (g 5 = h g + 7)) : thm

- COND_DISJ_CONV (--`((x=3) => f | g)(5) = h((x=3) => f | g) + 7`--) ;
val it =
  |- (((x = 3) => f | g) 5 = h ((x = 3) => f | g) + 7) =
     (x = 3) /\ (f 5 = h f + 7) \/ ~(x = 3) /\ (g 5 = h g + 7) : thm

Cheers,
- Ching Tsun


(*----------------------------------------------------------------------------
  Conversions for eliminating conditionals from a formula:
  
    COND_CONJ_CONV (--`P[b => x | y]`--) =
    |- P[b => x | y] = (b ==> P[x]) /\ (~b ==> P[y])
  
    COND_DISJ_CONV (--`P[b => x | y]`--) =
    |- P[b => x | y] = (b /\ P[x]) \/ (~b /\ P[y])
  
  where (b => x | y) is a free subterm of formula P.
----------------------------------------------------------------------------*)

local
  fun ABS_COND_CONV (tm) =
    let
      fun is_good_cond (c) = (is_cond c) andalso (free_in c tm) ;
      val c = find_term (is_good_cond) (tm) ;
      val x = genvar (type_of c) ;
      val tm' = subst [{redex = c, residue = x}] (tm) ;
    in
      SYM (BETA_CONV (--`(\^x. ^tm')(^c)`--))
    end ;
  
  val LHS_CONV = RATOR_CONV o RAND_CONV ;
  val RHS_CONV = RAND_CONV ;
  
  val COND_CONJ_THM = prove (
  (--`
    !P b x (y:'a). P(b => x | y) = (b ==> P(x)) /\ (~b ==> P(y))
  `--), (
    REPEAT GEN_TAC THEN COND_CASES_TAC THEN REWRITE_TAC []
  )) ;
  
  val COND_DISJ_THM = prove (
  (--`
    !P b x (y:'a). P(b => x | y) = (b /\ P(x)) \/ (~b /\ P(y))
  `--), (
    REPEAT GEN_TAC THEN COND_CASES_TAC THEN REWRITE_TAC []
  )) ;
in

val COND_CONJ_CONV =
  ABS_COND_CONV THENC REWR_CONV (COND_CONJ_THM) THENC
  (LHS_CONV o RHS_CONV) (BETA_CONV) THENC
  (RHS_CONV o RHS_CONV) (BETA_CONV) ;

val COND_DISJ_CONV =
  ABS_COND_CONV THENC REWR_CONV (COND_DISJ_THM) THENC
  (LHS_CONV o RHS_CONV) (BETA_CONV) THENC
  (RHS_CONV o RHS_CONV) (BETA_CONV) ;

end;