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; Sat, 8 Oct 1994 16:37:30 +0100
Received: by leopard.cs.byu.edu (1.38.193.4/16.2) id AA22459;
          Sat, 8 Oct 1994 09:33:31 -0600
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.38.193.4/16.2) id AA22455;
          Sat, 8 Oct 1994 09:33:25 -0600
Received: from LocalHost.cs.ucla.edu by maui.cs.ucla.edu (Sendmail 4.1/3.26) 
          id AA26359; Sat, 8 Oct 94 08:26:58 PDT
Message-Id: <9410081526.AA26359@maui.cs.ucla.edu>
To: "Tom. F. Melham" <tfm@dcs.gla.ac.uk>
Subject: Re: A Little Puzzle.
Cc: info-hol@leopard.cs.byu.edu
Date: Sat, 08 Oct 94 08:26:57 PDT
From: chou@cs.ucla.edu


The trick is to Skolemize!

- Ching Tsun

=============================== CUT HERE ===============================

fun sing (x) = [x] ;

val Asm = (--`!x:'a. !y:'a. (g x :'b = g y) ==> (f x :'c = f y)`--) ;

val Lemma1 = TAC_PROOF (
([Asm], (--`
  !z:'b. ?h:'c. !x:'a. (z = g x) ==> (h = f x)
`--)), (
  GEN_TAC THEN
  DISJ_CASES_THEN2
      (CHOOSE_THEN (REWRITE_TAC o sing))
      (ASSUME_TAC o CONV_RULE NOT_EXISTS_CONV)
      (SPEC (--`?y. z = (g:'a->'b) y`--) EXCLUDED_MIDDLE) THENL
  [ EXISTS_TAC (--`(f:'a->'c) y`--) THEN ASM_REWRITE_TAC []
  , EXISTS_TAC (--`h:'c`--) THEN REPEAT STRIP_TAC THEN RES_TAC ]
)) ;

val Lemma2 = CONV_RULE (SKOLEM_CONV) (Lemma1) ;

val Lemma3 = TAC_PROOF (
([Asm], (--`
  ?h:'b->'c. !x:'a. (h (g x) = f x)
`--)), (
  CHOOSE_TAC (Lemma2) THEN EXISTS_TAC (--`h:'b->'c`--) THEN
  GEN_TAC THEN FIRST_ASSUM (MATCH_MP_TAC) THEN REWRITE_TAC []
)) ;

val Thm = prove (
(--`
  !g:'a->'b. !f:'a->'c.
  (!x y. (g x = g y) ==> (f x = f y)) ==> ?h. !x. (h (g x) = f x)
`--), (
  REPEAT STRIP_TAC THEN REWRITE_TAC [Lemma3]
)) ;