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; Fri, 18 Nov 1994 17:34:26 +0000
Received: by leopard.cs.byu.edu (1.38.193.4/16.2) id AA02778;
          Fri, 18 Nov 1994 10:15:02 -0700
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Received: from iraun1.ira.uka.de by leopard.cs.byu.edu 
          with SMTP (1.38.193.4/16.2) id AA02729;
          Fri, 18 Nov 1994 10:13:57 -0700
Received: from i80fs2.ira.uka.de by iraun1.ira.uka.de with SMTP (PP);
          Fri, 18 Nov 1994 18:10:23 +0100
Received: from ira.uka.de by i80fs2.ira.uka.de id <00482-0@i80fs2.ira.uka.de>;
          Fri, 18 Nov 1994 18:14:08 +0100
Date: Fri, 18 Nov 94 18:14:06 EST
From: reetz <reetz@ira.uka.de>
To: info-hol@leopard.cs.byu.edu
Cc: slind@informatik.tu-muenchen.de
Subject: INL is one-one
Message-Id: <"i80fs2.ira.484:18.11.94.17.14.11"@ira.uka.de>

I wonder that INL from theory "sum" is one-one was never proven/
stored there (same for INR, of course). One might like to add it:

val INL_one_one =
 prove(--`

 !x y.(((INL x):'a+'b) = INL y) = (x = y)

 `--,
 EVERY [
  REPEAT GEN_TAC
  ,
  EQ_TAC
  THENL [
   EVERY [
    REWRITE_TAC [definition "sum" "INL_DEF"]
    ,
    REWRITE_TAC [
    let
     val th1 =
      prove(--`

      ?(v1:'a) (v2:'b).
      ((\b x' y. (x' = x) /\ b) = (\b (x:'a) (y:'b). (x = v1) /\ b)) \/
      ((\b x' y. (x' = x) /\ b) = (\b x y. (y = v2) /\ ~b))
      
      `--,
      EVERY [
       CONV_TAC(REDEPTH_CONV FUN_EQ_CONV)
       ,
       BETA_TAC
       ,
       REWRITE_TAC []
       ,
       EXISTS_TAC (--`x:'a`--)
       ,
       REWRITE_TAC []
      ])
     val th2 =
      prove(--`

      ?(v1:'a) (v2:'b).
      ((\b x y'. (x = y) /\ b) = (\b (x:'a) (y:'b). (x = v1) /\ b)) \/
      ((\b x y'. (x = y) /\ b) = (\b x y. (y = v2) /\ ~b))    

      `--,
      EVERY [
       CONV_TAC(REDEPTH_CONV FUN_EQ_CONV)
       ,
       BETA_TAC
       ,
       REWRITE_TAC []
       ,
       EXISTS_TAC (--`y:'a`--)
       ,
       REWRITE_TAC []
      ])
     val th3 =
      REWRITE_RULE [definition "sum" "IS_SUM_REP"]
      (ISPECL 
      [--`\b (x':'a) (y:'b). (x' = x) /\ b`--,
       --`\b (x:'a) (y':'b). (x = y) /\ b`--]
      (prove_abs_fn_one_one (definition "sum" "sum_ISO_DEF")))
    in
     MP (MP th3 th1) th2
    end
    ]
    ,
    CONV_TAC(REDEPTH_CONV FUN_EQ_CONV)
    ,
    BETA_TAC
    ,
    DISCH_TAC
    ,
    POP_ASSUM (ASSUME_TAC o (SPEC (--`T`--)))
    ,
    RULE_ASSUM_TAC (REWRITE_RULE [])
    ,
    POP_ASSUM (ASSUME_TAC o (ISPEC (--`x:'a`--)))
    ,
    RULE_ASSUM_TAC (REWRITE_RULE [])
    ,
    ASM_REWRITE_TAC [] 
   ]
   ,
   EVERY [
    DISCH_TAC
    ,
    ASM_REWRITE_TAC []
   ]
  ]
 ]);

(**************************************************************)
(*                                                            *)
(*  Ralf Reetz                                                *)
(*                                                            *)
(*  University of Karlsruhe                                   *)
(*  Institut fuer Rechnerentwurf und Fehlertoleranz           *)
(*  76128 Karlsruhe, Zirkel 2, Postfach 6980, Germany         *)
(*                                                            *)
(*  e-mail: reetz@ira.uka.de                                  *)
(*  WWW:    http://goethe.ira.uka.de/people/reetz/reetz.html  *)
(*                                                            *)
(**************************************************************)