ZF/Finite: added the finite function space, A-||>B
ZF/InfDatatype: added rules for the above

--- a/src/ZF/Finite.ML	Tue Aug 16 19:01:26 1994 +0200
+++ b/src/ZF/Finite.ML	Tue Aug 16 19:03:45 1994 +0200
@@ -3,7 +3,7 @@
     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1994  University of Cambridge
 
-Finite powerset operator
+Finite powerset operator; finite function space
 
 prove X:Fin(A) ==> |X| < nat
 
@@ -12,6 +12,8 @@
 
 open Finite;
 
+(*** Finite powerset operator ***)
+
 goalw Finite.thy Fin.defs "!!A B. A<=B ==> Fin(A) <= Fin(B)";
 by (rtac lfp_mono 1);
 by (REPEAT (rtac Fin.bnd_mono 1));
@@ -55,9 +57,10 @@
 goal Finite.thy "!!b A. b: Fin(A) ==> ALL z. z<=b --> z: Fin(A)";
 by (etac Fin_induct 1);
 by (simp_tac (Fin_ss addsimps [subset_empty_iff]) 1);
-by (safe_tac (ZF_cs addSDs [subset_cons_iff RS iffD1]));
-by (eres_inst_tac [("b","z")] (cons_Diff RS subst) 2);
-by (ALLGOALS (asm_simp_tac Fin_ss));
+by (asm_simp_tac (ZF_ss addsimps subset_cons_iff::distrib_rews) 1);
+by (safe_tac ZF_cs);
+by (eres_inst_tac [("b","z")] (cons_Diff RS subst) 1);
+by (asm_simp_tac Fin_ss 1);
 val Fin_subset_lemma = result();
 
 goal Finite.thy "!!c b A. [| c<=b;  b: Fin(A) |] ==> c: Fin(A)";
@@ -92,3 +95,47 @@
 by (asm_simp_tac (ZF_ss addsimps [succ_def, mem_not_refl RS cons_fun_eq]) 1);
 by (fast_tac (ZF_cs addSIs [Fin.consI]) 1);
 val nat_fun_subset_Fin = result();
+
+
+(*** Finite function space ***)
+
+goalw Finite.thy FiniteFun.defs
+    "!!A B C D. [| A<=C;  B<=D |] ==> A -||> B  <=  C -||> D";
+by (rtac lfp_mono 1);
+by (REPEAT (rtac FiniteFun.bnd_mono 1));
+by (REPEAT (ares_tac (Fin_mono::Sigma_mono::basic_monos) 1));
+val FiniteFun_mono = result();
+
+goal Finite.thy "!!A B. A<=B ==> A -||> A  <=  B -||> B";
+by (REPEAT (ares_tac [FiniteFun_mono] 1));
+val FiniteFun_mono1 = result();
+
+goal Finite.thy "!!h. h: A -||>B ==> h: domain(h) -> B";
+by (etac FiniteFun.induct 1);
+by (simp_tac (ZF_ss addsimps [empty_fun, domain_0]) 1);
+by (asm_simp_tac (ZF_ss addsimps [fun_extend3, domain_cons]) 1);
+val FiniteFun_is_fun = result();
+
+goal Finite.thy "!!h. h: A -||>B ==> domain(h) : Fin(A)";
+by (etac FiniteFun.induct 1);
+by (simp_tac (Fin_ss addsimps [domain_0]) 1);
+by (asm_simp_tac (Fin_ss addsimps [domain_cons]) 1);
+val FiniteFun_domain_Fin = result();
+
+val FiniteFun_apply_type = FiniteFun_is_fun RS apply_type |> standard;
+
+(*Every subset of a finite function is a finite function.*)
+goal Finite.thy "!!b A. b: A-||>B ==> ALL z. z<=b --> z: A-||>B";
+by (etac FiniteFun.induct 1);
+by (simp_tac (ZF_ss addsimps subset_empty_iff::FiniteFun.intrs) 1);
+by (asm_simp_tac (ZF_ss addsimps subset_cons_iff::distrib_rews) 1);
+by (safe_tac ZF_cs);
+by (eres_inst_tac [("b","z")] (cons_Diff RS subst) 1);
+by (dtac (spec RS mp) 1 THEN assume_tac 1);
+by (fast_tac (ZF_cs addSIs FiniteFun.intrs) 1);
+val FiniteFun_subset_lemma = result();
+
+goal Finite.thy "!!c b A. [| c<=b;  b: A-||>B |] ==> c: A-||>B";
+by (REPEAT (ares_tac [FiniteFun_subset_lemma RS spec RS mp] 1));
+val FiniteFun_subset = result();
+

--- a/src/ZF/Finite.thy	Tue Aug 16 19:01:26 1994 +0200
+++ b/src/ZF/Finite.thy	Tue Aug 16 19:03:45 1994 +0200
@@ -7,7 +7,10 @@
 *)
 
 Finite = Arith + 
-consts Fin :: "i=>i"
+consts
+  Fin 	    :: "i=>i"
+  FiniteFun :: "[i,i]=>i"		("(_ -||>/ _)" [61, 60] 60)
+
 inductive
   domains   "Fin(A)" <= "Pow(A)"
   intrs
@@ -15,4 +18,12 @@
     consI   "[| a: A;  b: Fin(A) |] ==> cons(a,b) : Fin(A)"
   type_intrs "[empty_subsetI, cons_subsetI, PowI]"
   type_elims "[make_elim PowD]"
+
+inductive
+  domains   "FiniteFun(A,B)" <= "Fin(A*B)"
+  intrs
+    emptyI  "0 : A -||> B"
+    consI   "[| a: A;  b: B;  h: A -||> B;  a ~: domain(h)   \
+\	     |] ==> cons(<a,b>,h) : A -||> B"
+  type_intrs "Fin.intrs"
 end

--- a/src/ZF/InfDatatype.ML	Tue Aug 16 19:01:26 1994 +0200
+++ b/src/ZF/InfDatatype.ML	Tue Aug 16 19:03:45 1994 +0200
@@ -3,11 +3,12 @@
     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1994  University of Cambridge
 
-Datatype Definitions involving ->
-	Even infinite-branching!
+Datatype Definitions involving function space and/or infinite-branching
 *)
 
-(*** Closure under finite powerset ***)
+(*** FINITE BRANCHING ***)
+
+(** Closure under finite powerset **)
 
 val Fin_Univ_thy = merge_theories (Univ.thy,Finite.thy);
 
@@ -34,6 +35,12 @@
 val Fin_subset_VLimit = 
     [Fin_mono, Fin_VLimit] MRS subset_trans |> standard;
 
+goalw Fin_Univ_thy [univ_def] "Fin(univ(A)) <= univ(A)";
+by (rtac (Limit_nat RS Fin_VLimit) 1);
+val Fin_univ = result();
+
+(** Closure under finite powers (functions from a fixed natural number) **)
+
 goal Fin_Univ_thy
     "!!i. [| n: nat;  Limit(i) |] ==> n -> Vfrom(A,i) <= Vfrom(A,i)";
 by (eresolve_tac [nat_fun_subset_Fin RS subset_trans] 1);
@@ -44,19 +51,47 @@
 val nat_fun_subset_VLimit = 
     [Pi_mono, nat_fun_VLimit] MRS subset_trans |> standard;
 
-
-goalw Fin_Univ_thy [univ_def] "Fin(univ(A)) <= univ(A)";
-by (rtac (Limit_nat RS Fin_VLimit) 1);
-val Fin_univ = result();
-
-val Fin_subset_univ = [Fin_mono, Fin_univ] MRS subset_trans |> standard;
-
 goalw Fin_Univ_thy [univ_def] "!!i. n: nat ==> n -> univ(A) <= univ(A)";
 by (etac (Limit_nat RSN (2,nat_fun_VLimit)) 1);
 val nat_fun_univ = result();
 
 
-(*** Infinite branching ***)
+(** Closure under finite function space **)
+
+(*General but seldom-used version; normally the domain is fixed*)
+goal Fin_Univ_thy
+    "!!i. Limit(i) ==> Vfrom(A,i) -||> Vfrom(A,i) <= Vfrom(A,i)";
+by (resolve_tac [FiniteFun.dom_subset RS subset_trans] 1);
+by (REPEAT (ares_tac [Fin_subset_VLimit, Sigma_subset_VLimit, subset_refl] 1));
+val FiniteFun_VLimit1 = result();
+
+goalw Fin_Univ_thy [univ_def] "univ(A) -||> univ(A) <= univ(A)";
+by (rtac (Limit_nat RS FiniteFun_VLimit1) 1);
+val FiniteFun_univ1 = result();
+
+(*Version for a fixed domain*)
+goal Fin_Univ_thy
+   "!!i.  [| W <= Vfrom(A,i); Limit(i) |] ==> W -||> Vfrom(A,i) <= Vfrom(A,i)";
+by (eresolve_tac [subset_refl RSN (2, FiniteFun_mono) RS subset_trans] 1);
+by (eresolve_tac [FiniteFun_VLimit1] 1);
+val FiniteFun_VLimit = result();
+
+goalw Fin_Univ_thy [univ_def]
+    "!!W. W <= univ(A) ==> W -||> univ(A) <= univ(A)";
+by (etac (Limit_nat RSN (2, FiniteFun_VLimit)) 1);
+val FiniteFun_univ = result();
+
+goal Fin_Univ_thy
+    "!!W. [| f: W -||> univ(A);  W <= univ(A) |] ==> f : univ(A)";
+by (eresolve_tac [FiniteFun_univ RS subsetD] 1);
+by (assume_tac 1);
+val FiniteFun_in_univ = result();
+
+(*Remove <= from the rule above*)
+val FiniteFun_in_univ' = subsetI RSN (2, FiniteFun_in_univ);
+
+
+(*** INFINITE BRANCHING ***)
 
 val fun_Limit_VfromE = 
     [apply_funtype, InfCard_csucc RS InfCard_is_Limit] MRS Limit_VfromE
@@ -88,7 +123,7 @@
 
 (*Version for arbitrary index sets*)
 goal InfDatatype.thy
-    "!!K. [| |W| le K;  W <= Vfrom(A,csucc(K));  InfCard(K) |] ==> \
+    "!!K. [| |W| le K;  InfCard(K);  W <= Vfrom(A,csucc(K)) |] ==> \
 \         W -> Vfrom(A,csucc(K)) <= Vfrom(A,csucc(K))";
 by (safe_tac (ZF_cs addSDs [fun_Vcsucc_lemma, subset_Vcsucc]));
 by (resolve_tac [Vfrom RS ssubst] 1);