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, 14 Oct 1994 17:44:37 +0100
Received: by leopard.cs.byu.edu (1.38.193.4/16.2) id AA09867;
          Fri, 14 Oct 1994 10:40:42 -0600
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Received: from ilex.fernuni-hagen.de by leopard.cs.byu.edu 
          with SMTP (1.38.193.4/16.2) id AA09858;
          Fri, 14 Oct 1994 10:40:37 -0600
Received: from MAJESTIX.fernuni-hagen.de by ilex.FernUni-Hagen.de 
          with SMTP (PP); Fri, 14 Oct 1994 17:33:50 +0100
Received: from TRANSFIX.fernuni-hagen.de 
          by MAJESTIX.fernuni-hagen.de (4.1/SMI-4.1) id AA10153;
          Fri, 14 Oct 94 17:34:35 +0100
Date: Fri, 14 Oct 94 17:34:35 +0100
From: Norbert.Voelker@FernUni-Hagen.de (Norbert Voelker)
Message-Id: <9410141634.AA10153@MAJESTIX.fernuni-hagen.de>
To: info-hol@leopard.cs.byu.edu
Subject: Tom Melham's little puzzle in Isabelle/HOL

A solution in Isabelle/HOL can be given in five resolution steps 
with standard Isabelle/HOL theorems resp. the premise. 

val prems = goal HOL.thy 
  (!! x y. g(x) = g(y) ==> f(x) = f(y)) ==> ? h. ! x. h(g(x)) = f(x)";

Level 0
1. ? h. ! x. h(g(x)) = f(x)

>> br exI 1;  (* exI: "?P(?x) ==> ? x. ?P(x)"  *)
>> br allI 1; (* allI: (!!x. ?P(x)) ==> ! x. ?P(x) *)            

Level 2 
1. !!x. ?h(g(x)) = f(x)

>> br (hd prems) 1; (* hd prems = first premise *)

Level 3 
1. !!x. g(?x3(g(x))) = g(x)

>> br selectI 1;    (* selectI:  ?P(?x) ==> ?P(@x. ?P(x)) *)

Level 4
1. . !!x. g(?x5(x, ?x4(x))) = g(x)
Flex-flex pairs:
%x. ?x5(x, @xa. g(?x5(x, xa)) = g(x)) =?= %x. ?x3(g(x))

>> br refl 1;       (* refl: ?t = ?t *) 
No subgoals!

>> val meta_puzzle = result();

  (!!x y. ?g(x) = ?g(y) ==> ?f(x) = ?f(y)) 
     ==> 
  ? h. ! x. h(?g(x)) = ?f(x)"

I think this is a nice illustration of the power of unknowns - 
an explicit solution for h is never given.  

--Norbert