Added some definitions and theorems needed for the
construction of datatypes involving function types.

--- a/src/HOL/Fun.ML	Fri Jul 16 12:02:06 1999 +0200
+++ b/src/HOL/Fun.ML	Fri Jul 16 12:09:48 1999 +0200
@@ -62,6 +62,18 @@
 by (Blast_tac 1);
 qed "UN_o";
 
+(** lemma for proving injectivity of representation functions for **)
+(** datatypes involving function types                            **)
+
+Goalw [o_def]
+  "[| !x y. g (f x) = g y --> f x = y; g o f = g o fa |] ==> f = fa";
+br ext 1;
+be allE 1;
+be allE 1;
+be mp 1;
+be fun_cong 1;
+qed "inj_fun_lemma";
+
 
 section "inj";
 (**NB: inj now just translates to inj_on**)
@@ -106,6 +118,11 @@
 by (rtac (rangeI RS minor) 1);
 qed "inj_transfer";
 
+Goalw [o_def] "[| inj f; f o g = f o h |] ==> g = h";
+by (rtac ext 1);
+by (etac injD 1);
+by (etac fun_cong 1);
+qed "inj_o";
 
 (*** inj_on f A: f is one-to-one over A ***)
 

--- a/src/HOL/Relation.ML	Fri Jul 16 12:02:06 1999 +0200
+++ b/src/HOL/Relation.ML	Fri Jul 16 12:09:48 1999 +0200
@@ -383,3 +383,24 @@
 by (Blast_tac 1);
 qed "Range_partial_func";
 
+
+(** Composition of function and relation **)
+
+Goalw [fun_rel_comp_def] "A <= B ==> fun_rel_comp f A <= fun_rel_comp f B";
+by (Fast_tac 1);
+qed "fun_rel_comp_mono";
+
+Goalw [fun_rel_comp_def] "! x. ?! y. (f x, y) : R ==> ?! g. g : fun_rel_comp f R";
+by (res_inst_tac [("a","%x. @y. (f x, y) : R")] ex1I 1);
+by (rtac CollectI 1);
+by (rtac allI 1);
+by (etac allE 1);
+by (rtac (select_eq_Ex RS iffD2) 1);
+by (etac ex1_implies_ex 1);
+by (rtac ext 1);
+by (etac CollectE 1);
+by (REPEAT (etac allE 1));
+by (rtac (select1_equality RS sym) 1);
+by (atac 1);
+by (atac 1);
+qed "fun_rel_comp_unique";

--- a/src/HOL/Relation.thy	Fri Jul 16 12:02:06 1999 +0200
+++ b/src/HOL/Relation.thy	Fri Jul 16 12:09:48 1999 +0200
@@ -7,14 +7,14 @@
 Relation = Prod +
 
 consts
-  O           :: "[('b * 'c)set, ('a * 'b)set] => ('a * 'c)set" (infixr 60)
-  converse    :: "('a*'b) set => ('b*'a) set"     ("(_^-1)" [1000] 999)
-  "^^"        :: "[('a*'b) set,'a set] => 'b set" (infixl 90)
+  O            :: "[('b * 'c)set, ('a * 'b)set] => ('a * 'c)set" (infixr 60)
+  converse     :: "('a*'b) set => ('b*'a) set"     ("(_^-1)" [1000] 999)
+  "^^"         :: "[('a*'b) set,'a set] => 'b set" (infixl 90)
   
 defs
-  comp_def      "r O s == {(x,z). ? y. (x,y):s & (y,z):r}"
-  converse_def  "r^-1 == {(y,x). (x,y):r}"
-  Image_def     "r ^^ s == {y. ? x:s. (x,y):r}"
+  comp_def         "r O s == {(x,z). ? y. (x,y):s & (y,z):r}"
+  converse_def     "r^-1 == {(y,x). (x,y):r}"
+  Image_def        "r ^^ s == {y. ? x:s. (x,y):r}"
   
 constdefs
   Id     :: "('a * 'a)set"                 (*the identity relation*)
@@ -44,6 +44,9 @@
   Univalent :: "('a * 'b)set => bool"
     "Univalent r == !x y. (x,y):r --> (!z. (x,z):r --> y=z)"
 
+  fun_rel_comp :: "['a => 'b, ('b * 'c) set] => ('a => 'c) set"
+    "fun_rel_comp f R == {g. !x. (f x, g x) : R}"
+
 syntax
   reflexive :: "('a * 'a)set => bool"       (*reflexivity over a type*)
 

--- a/src/HOL/Sum.ML	Fri Jul 16 12:02:06 1999 +0200
+++ b/src/HOL/Sum.ML	Fri Jul 16 12:09:48 1999 +0200
@@ -167,6 +167,17 @@
   "s=t ==> sum_case f g s = sum_case f g t"
   (fn [prem] => [rtac (prem RS arg_cong) 1]);
 
+val [p1,p2] = Goal "[| sum_case f1 f2 = sum_case g1 g2;  \
+  \  [| f1 = g1; f2 = g2 |] ==> P |] ==> P";
+by (cut_facts_tac [p1] 1);
+br p2 1;
+br ext 1;
+by (dres_inst_tac [("x","Inl x")] fun_cong 1);
+by (Asm_full_simp_tac 1);
+br ext 1;
+by (dres_inst_tac [("x","Inr x")] fun_cong 1);
+by (Asm_full_simp_tac 1);
+qed "sum_case_inject";
 
 
 (** Rules for the Part primitive **)

--- a/src/HOL/Univ.ML	Fri Jul 16 12:02:06 1999 +0200
+++ b/src/HOL/Univ.ML	Fri Jul 16 12:09:48 1999 +0200
@@ -24,7 +24,7 @@
 (** Push -- an injection, analogous to Cons on lists **)
 
 Goalw [Push_def] "Push i f = Push j g  ==> i=j";
-by (etac (fun_cong RS box_equals RS Suc_inject) 1);
+by (etac (fun_cong RS box_equals) 1);
 by (rtac nat_case_0 1);
 by (rtac nat_case_0 1);
 qed "Push_inject1";
@@ -42,8 +42,9 @@
 by (rtac ((major RS Push_inject2) RS ((major RS Push_inject1) RS minor)) 1);
 qed "Push_inject";
 
-Goalw [Push_def] "Push k f =(%z.0) ==> P";
-by (etac (fun_cong RS box_equals RS Suc_neq_Zero) 1);
+Goalw [Push_def] "Push (Inr (Suc k)) f = (%z. Inr 0) ==> P";
+by (rtac Suc_neq_Zero 1);
+by (etac (fun_cong RS box_equals RS Inr_inject) 1);
 by (rtac nat_case_0 1);
 by (rtac refl 1);
 qed "Push_neq_K0";
@@ -65,13 +66,13 @@
 
 (*** Introduction rules for Node ***)
 
-Goalw [Node_def] "(%k. 0,a) : Node";
+Goalw [Node_def] "(%k. Inr 0, a) : Node";
 by (Blast_tac 1);
 qed "Node_K0_I";
 
 Goalw [Node_def,Push_def]
     "p: Node ==> apfst (Push i) p : Node";
-by (blast_tac (claset() addSIs [apfst_conv, nat_case_Suc RS trans]) 1);
+by (fast_tac (claset() addSIs [apfst_conv, nat_case_Suc RS trans]) 1);
 qed "Node_Push_I";
 
 
@@ -205,23 +206,22 @@
 AddIffs  [Scons_not_Atom, Atom_not_Scons, Scons_Scons_eq];
 
 
-Goalw [ndepth_def] "ndepth (Abs_Node((%k.0, x))) = 0";
+Goalw [ndepth_def] "ndepth (Abs_Node((%k. Inr 0, x))) = 0";
 by (EVERY1[stac (Node_K0_I RS Abs_Node_inverse), stac split]);
 by (rtac Least_equality 1);
 by (rtac refl 1);
 by (etac less_zeroE 1);
 qed "ndepth_K0";
 
-Goal "k < Suc(LEAST x. f(x)=0) --> 0 < nat_case (Suc i) f k";
+Goal "k < Suc(LEAST x. f x = Inr 0) --> nat_case (Inr (Suc i)) f k ~= Inr 0";
 by (nat_ind_tac "k" 1);
 by (ALLGOALS Simp_tac);
 by (rtac impI 1);
-by (dtac not_less_Least 1);
-by (Asm_full_simp_tac 1);
+by (etac not_less_Least 1);
 val lemma = result();
 
 Goalw [ndepth_def,Push_Node_def]
-    "ndepth (Push_Node i n) = Suc(ndepth(n))";
+    "ndepth (Push_Node (Inr (Suc i)) n) = Suc(ndepth(n))";
 by (stac (Rep_Node RS Node_Push_I RS Abs_Node_inverse) 1);
 by (cut_facts_tac [rewrite_rule [Node_def] Rep_Node] 1);
 by Safe_tac;
@@ -376,6 +376,69 @@
 qed "inj_In1";
 
 
+(*** Function spaces ***)
+
+Goalw [Lim_def] "Lim f = Lim g ==> f = g";
+by (rtac ext 1);
+by (rtac ccontr 1);
+by (etac equalityE 1);
+by (subgoal_tac "? y. y : f x & y ~: g x | y ~: f x & y : g x" 1);
+by (Blast_tac 2);
+by (etac exE 1);
+by (etac disjE 1);
+by (REPEAT (EVERY [
+  dtac subsetD 1,
+  Fast_tac 1,
+  etac UnionE 1,
+  dtac CollectD 1,
+  etac exE 1,
+  hyp_subst_tac 1,
+  etac imageE 1,
+  etac Push_Node_inject 1,
+  Asm_full_simp_tac 1,
+  TRY (thin_tac "?S <= ?T" 1)]));
+qed "Lim_inject";
+
+Goalw [Funs_def] "S <= T ==> Funs S <= Funs T";
+by (Blast_tac 1);
+qed "Funs_mono";
+
+val [p] = goalw thy [Funs_def] "(!!x. f x : S) ==> f : Funs S";
+br CollectI 1;
+br subsetI 1;
+be rangeE 1;
+be ssubst 1;
+br p 1;
+qed "FunsI";
+
+Goalw [Funs_def] "f : Funs S ==> f x : S";
+be CollectE 1;
+be subsetD 1;
+br rangeI 1;
+qed "FunsD";
+
+val [p1, p2] = goalw thy [o_def]
+  "[| f : Funs R; !!x. x : R ==> r (a x) = x |] ==> r o (a o f) = f";
+br ext 1;
+br p2 1;
+br (p1 RS FunsD) 1;
+qed "Funs_inv";
+
+val [p1, p2] = Goalw [o_def] "[| f : Funs (range g); !!h. f = g o h ==> P |] ==> P";
+by (cut_facts_tac [p1] 1);
+by (res_inst_tac [("h", "%x. @y. f x = g y")] p2 1);
+br ext 1;
+bd FunsD 1;
+be rangeE 1;
+be (exI RS (select_eq_Ex RS iffD2)) 1;
+qed "Funs_rangeE";
+
+Goal "a : S ==> (%x. a) : Funs S";
+by (rtac FunsI 1);
+by (atac 1);
+qed "Funs_nonempty";
+
+
 (*** proving equality of sets and functions using ntrunc ***)
 
 Goalw [ntrunc_def] "ntrunc k M <= M";

--- a/src/HOL/Univ.thy	Fri Jul 16 12:02:06 1999 +0200
+++ b/src/HOL/Univ.thy	Fri Jul 16 12:09:48 1999 +0200
@@ -3,7 +3,7 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
-Declares the type 'a node, a subtype of (nat=>nat) * ('a+nat)
+Declares the type ('a, 'b) node, a subtype of (nat=>'b+nat) * ('a+nat)
 
 Defines "Cartesian Product" and "Disjoint Sum" as set operations.
 Could <*> be generalized to a general summation (Sigma)?
@@ -16,36 +16,40 @@
 global
 
 typedef (Node)
-  'a node = "{p. EX f x k. p = (f::nat=>nat, x::'a+nat) & f(k)=0}"
+  ('a, 'b) node = "{p. EX f x k. p = (f::nat=>'b+nat, x::'a+nat) & f k = Inr 0}"
 
 types
-  'a item = 'a node set
+  'a item = ('a, unit) node set
+  ('a, 'b) dtree = ('a, 'b) node set
 
 consts
   apfst     :: "['a=>'c, 'a*'b] => 'c*'b"
-  Push      :: [nat, nat=>nat] => (nat=>nat)
+  Push      :: "[('b + nat), nat => ('b + nat)] => (nat => ('b + nat))"
 
-  Push_Node :: [nat, 'a node] => 'a node
-  ndepth    :: 'a node => nat
+  Push_Node :: "[('b + nat), ('a, 'b) node] => ('a, 'b) node"
+  ndepth    :: ('a, 'b) node => nat
 
-  Atom      :: "('a+nat) => 'a item"
-  Leaf      :: 'a => 'a item
-  Numb      :: nat => 'a item
-  Scons     :: ['a item, 'a item]=> 'a item
-  In0,In1   :: 'a item => 'a item
+  Atom      :: "('a + nat) => ('a, 'b) dtree"
+  Leaf      :: 'a => ('a, 'b) dtree
+  Numb      :: nat => ('a, 'b) dtree
+  Scons     :: [('a, 'b) dtree, ('a, 'b) dtree] => ('a, 'b) dtree
+  In0,In1   :: ('a, 'b) dtree => ('a, 'b) dtree
 
-  ntrunc    :: [nat, 'a item] => 'a item
+  Lim       :: ('b => ('a, 'b) dtree) => ('a, 'b) dtree
+  Funs      :: "'u set => ('t => 'u) set"
 
-  "<*>"  :: ['a item set, 'a item set]=> 'a item set (infixr 80)
-  "<+>"  :: ['a item set, 'a item set]=> 'a item set (infixr 70)
+  ntrunc    :: [nat, ('a, 'b) dtree] => ('a, 'b) dtree
+
+  "<*>"  :: [('a, 'b) dtree set, ('a, 'b) dtree set]=> ('a, 'b) dtree set (infixr 80)
+  "<+>"  :: [('a, 'b) dtree set, ('a, 'b) dtree set]=> ('a, 'b) dtree set (infixr 70)
 
-  Split  :: [['a item, 'a item]=>'b, 'a item] => 'b
-  Case   :: [['a item]=>'b, ['a item]=>'b, 'a item] => 'b
+  Split  :: [[('a, 'b) dtree, ('a, 'b) dtree]=>'c, ('a, 'b) dtree] => 'c
+  Case   :: [[('a, 'b) dtree]=>'c, [('a, 'b) dtree]=>'c, ('a, 'b) dtree] => 'c
 
-  "<**>" :: "[('a item * 'a item)set, ('a item * 'a item)set] 
-           => ('a item * 'a item)set" (infixr 80)
-  "<++>" :: "[('a item * 'a item)set, ('a item * 'a item)set] 
-           => ('a item * 'a item)set" (infixr 70)
+  "<**>" :: "[(('a, 'b) dtree * ('a, 'b) dtree)set, (('a, 'b) dtree * ('a, 'b) dtree)set] 
+           => (('a, 'b) dtree * ('a, 'b) dtree)set" (infixr 80)
+  "<++>" :: "[(('a, 'b) dtree * ('a, 'b) dtree)set, (('a, 'b) dtree * ('a, 'b) dtree)set] 
+           => (('a, 'b) dtree * ('a, 'b) dtree)set" (infixr 70)
 
 
 local
@@ -56,13 +60,13 @@
 
   (*crude "lists" of nats -- needed for the constructions*)
   apfst_def  "apfst == (%f (x,y). (f(x),y))"
-  Push_def   "Push == (%b h. nat_case (Suc b) h)"
+  Push_def   "Push == (%b h. nat_case b h)"
 
   (** operations on S-expressions -- sets of nodes **)
 
   (*S-expression constructors*)
-  Atom_def   "Atom == (%x. {Abs_Node((%k.0, x))})"
-  Scons_def  "Scons M N == (Push_Node(0) `` M) Un (Push_Node(Suc(0)) `` N)"
+  Atom_def   "Atom == (%x. {Abs_Node((%k. Inr 0, x))})"
+  Scons_def  "Scons M N == (Push_Node (Inr 1) `` M) Un (Push_Node (Inr 2) `` N)"
 
   (*Leaf nodes, with arbitrary or nat labels*)
   Leaf_def   "Leaf == Atom o Inl"
@@ -72,8 +76,12 @@
   In0_def    "In0(M) == Scons (Numb 0) M"
   In1_def    "In1(M) == Scons (Numb 1) M"
 
+  (*Function spaces*)
+  Lim_def "Lim f == Union {z. ? x. z = Push_Node (Inl x) `` (f x)}"
+  Funs_def "Funs S == {f. range f <= S}"
+
   (*the set of nodes with depth less than k*)
-  ndepth_def "ndepth(n) == (%(f,x). LEAST k. f(k)=0) (Rep_Node n)"
+  ndepth_def "ndepth(n) == (%(f,x). LEAST k. f k = Inr 0) (Rep_Node n)"
   ntrunc_def "ntrunc k N == {n. n:N & ndepth(n)<k}"
 
   (*products and sums for the "universe"*)