ZF/Finite: added the finite function space, A-||>B
authorlcp
Tue Aug 16 19:03:45 1994 +0200 (1994-08-16)
changeset 534cd8bec47e175
parent 533 7357160bc56a
child 535 9d62c7e08699
ZF/Finite: added the finite function space, A-||>B
ZF/InfDatatype: added rules for the above
src/ZF/Finite.ML
src/ZF/Finite.thy
src/ZF/InfDatatype.ML
     1.1 --- a/src/ZF/Finite.ML	Tue Aug 16 19:01:26 1994 +0200
     1.2 +++ b/src/ZF/Finite.ML	Tue Aug 16 19:03:45 1994 +0200
     1.3 @@ -3,7 +3,7 @@
     1.4      Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.5      Copyright   1994  University of Cambridge
     1.6  
     1.7 -Finite powerset operator
     1.8 +Finite powerset operator; finite function space
     1.9  
    1.10  prove X:Fin(A) ==> |X| < nat
    1.11  
    1.12 @@ -12,6 +12,8 @@
    1.13  
    1.14  open Finite;
    1.15  
    1.16 +(*** Finite powerset operator ***)
    1.17 +
    1.18  goalw Finite.thy Fin.defs "!!A B. A<=B ==> Fin(A) <= Fin(B)";
    1.19  by (rtac lfp_mono 1);
    1.20  by (REPEAT (rtac Fin.bnd_mono 1));
    1.21 @@ -55,9 +57,10 @@
    1.22  goal Finite.thy "!!b A. b: Fin(A) ==> ALL z. z<=b --> z: Fin(A)";
    1.23  by (etac Fin_induct 1);
    1.24  by (simp_tac (Fin_ss addsimps [subset_empty_iff]) 1);
    1.25 -by (safe_tac (ZF_cs addSDs [subset_cons_iff RS iffD1]));
    1.26 -by (eres_inst_tac [("b","z")] (cons_Diff RS subst) 2);
    1.27 -by (ALLGOALS (asm_simp_tac Fin_ss));
    1.28 +by (asm_simp_tac (ZF_ss addsimps subset_cons_iff::distrib_rews) 1);
    1.29 +by (safe_tac ZF_cs);
    1.30 +by (eres_inst_tac [("b","z")] (cons_Diff RS subst) 1);
    1.31 +by (asm_simp_tac Fin_ss 1);
    1.32  val Fin_subset_lemma = result();
    1.33  
    1.34  goal Finite.thy "!!c b A. [| c<=b;  b: Fin(A) |] ==> c: Fin(A)";
    1.35 @@ -92,3 +95,47 @@
    1.36  by (asm_simp_tac (ZF_ss addsimps [succ_def, mem_not_refl RS cons_fun_eq]) 1);
    1.37  by (fast_tac (ZF_cs addSIs [Fin.consI]) 1);
    1.38  val nat_fun_subset_Fin = result();
    1.39 +
    1.40 +
    1.41 +(*** Finite function space ***)
    1.42 +
    1.43 +goalw Finite.thy FiniteFun.defs
    1.44 +    "!!A B C D. [| A<=C;  B<=D |] ==> A -||> B  <=  C -||> D";
    1.45 +by (rtac lfp_mono 1);
    1.46 +by (REPEAT (rtac FiniteFun.bnd_mono 1));
    1.47 +by (REPEAT (ares_tac (Fin_mono::Sigma_mono::basic_monos) 1));
    1.48 +val FiniteFun_mono = result();
    1.49 +
    1.50 +goal Finite.thy "!!A B. A<=B ==> A -||> A  <=  B -||> B";
    1.51 +by (REPEAT (ares_tac [FiniteFun_mono] 1));
    1.52 +val FiniteFun_mono1 = result();
    1.53 +
    1.54 +goal Finite.thy "!!h. h: A -||>B ==> h: domain(h) -> B";
    1.55 +by (etac FiniteFun.induct 1);
    1.56 +by (simp_tac (ZF_ss addsimps [empty_fun, domain_0]) 1);
    1.57 +by (asm_simp_tac (ZF_ss addsimps [fun_extend3, domain_cons]) 1);
    1.58 +val FiniteFun_is_fun = result();
    1.59 +
    1.60 +goal Finite.thy "!!h. h: A -||>B ==> domain(h) : Fin(A)";
    1.61 +by (etac FiniteFun.induct 1);
    1.62 +by (simp_tac (Fin_ss addsimps [domain_0]) 1);
    1.63 +by (asm_simp_tac (Fin_ss addsimps [domain_cons]) 1);
    1.64 +val FiniteFun_domain_Fin = result();
    1.65 +
    1.66 +val FiniteFun_apply_type = FiniteFun_is_fun RS apply_type |> standard;
    1.67 +
    1.68 +(*Every subset of a finite function is a finite function.*)
    1.69 +goal Finite.thy "!!b A. b: A-||>B ==> ALL z. z<=b --> z: A-||>B";
    1.70 +by (etac FiniteFun.induct 1);
    1.71 +by (simp_tac (ZF_ss addsimps subset_empty_iff::FiniteFun.intrs) 1);
    1.72 +by (asm_simp_tac (ZF_ss addsimps subset_cons_iff::distrib_rews) 1);
    1.73 +by (safe_tac ZF_cs);
    1.74 +by (eres_inst_tac [("b","z")] (cons_Diff RS subst) 1);
    1.75 +by (dtac (spec RS mp) 1 THEN assume_tac 1);
    1.76 +by (fast_tac (ZF_cs addSIs FiniteFun.intrs) 1);
    1.77 +val FiniteFun_subset_lemma = result();
    1.78 +
    1.79 +goal Finite.thy "!!c b A. [| c<=b;  b: A-||>B |] ==> c: A-||>B";
    1.80 +by (REPEAT (ares_tac [FiniteFun_subset_lemma RS spec RS mp] 1));
    1.81 +val FiniteFun_subset = result();
    1.82 +
     2.1 --- a/src/ZF/Finite.thy	Tue Aug 16 19:01:26 1994 +0200
     2.2 +++ b/src/ZF/Finite.thy	Tue Aug 16 19:03:45 1994 +0200
     2.3 @@ -7,7 +7,10 @@
     2.4  *)
     2.5  
     2.6  Finite = Arith + 
     2.7 -consts Fin :: "i=>i"
     2.8 +consts
     2.9 +  Fin 	    :: "i=>i"
    2.10 +  FiniteFun :: "[i,i]=>i"		("(_ -||>/ _)" [61, 60] 60)
    2.11 +
    2.12  inductive
    2.13    domains   "Fin(A)" <= "Pow(A)"
    2.14    intrs
    2.15 @@ -15,4 +18,12 @@
    2.16      consI   "[| a: A;  b: Fin(A) |] ==> cons(a,b) : Fin(A)"
    2.17    type_intrs "[empty_subsetI, cons_subsetI, PowI]"
    2.18    type_elims "[make_elim PowD]"
    2.19 +
    2.20 +inductive
    2.21 +  domains   "FiniteFun(A,B)" <= "Fin(A*B)"
    2.22 +  intrs
    2.23 +    emptyI  "0 : A -||> B"
    2.24 +    consI   "[| a: A;  b: B;  h: A -||> B;  a ~: domain(h)   \
    2.25 +\	     |] ==> cons(<a,b>,h) : A -||> B"
    2.26 +  type_intrs "Fin.intrs"
    2.27  end
     3.1 --- a/src/ZF/InfDatatype.ML	Tue Aug 16 19:01:26 1994 +0200
     3.2 +++ b/src/ZF/InfDatatype.ML	Tue Aug 16 19:03:45 1994 +0200
     3.3 @@ -3,11 +3,12 @@
     3.4      Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     3.5      Copyright   1994  University of Cambridge
     3.6  
     3.7 -Datatype Definitions involving ->
     3.8 -	Even infinite-branching!
     3.9 +Datatype Definitions involving function space and/or infinite-branching
    3.10  *)
    3.11  
    3.12 -(*** Closure under finite powerset ***)
    3.13 +(*** FINITE BRANCHING ***)
    3.14 +
    3.15 +(** Closure under finite powerset **)
    3.16  
    3.17  val Fin_Univ_thy = merge_theories (Univ.thy,Finite.thy);
    3.18  
    3.19 @@ -34,6 +35,12 @@
    3.20  val Fin_subset_VLimit = 
    3.21      [Fin_mono, Fin_VLimit] MRS subset_trans |> standard;
    3.22  
    3.23 +goalw Fin_Univ_thy [univ_def] "Fin(univ(A)) <= univ(A)";
    3.24 +by (rtac (Limit_nat RS Fin_VLimit) 1);
    3.25 +val Fin_univ = result();
    3.26 +
    3.27 +(** Closure under finite powers (functions from a fixed natural number) **)
    3.28 +
    3.29  goal Fin_Univ_thy
    3.30      "!!i. [| n: nat;  Limit(i) |] ==> n -> Vfrom(A,i) <= Vfrom(A,i)";
    3.31  by (eresolve_tac [nat_fun_subset_Fin RS subset_trans] 1);
    3.32 @@ -44,19 +51,47 @@
    3.33  val nat_fun_subset_VLimit = 
    3.34      [Pi_mono, nat_fun_VLimit] MRS subset_trans |> standard;
    3.35  
    3.36 -
    3.37 -goalw Fin_Univ_thy [univ_def] "Fin(univ(A)) <= univ(A)";
    3.38 -by (rtac (Limit_nat RS Fin_VLimit) 1);
    3.39 -val Fin_univ = result();
    3.40 -
    3.41 -val Fin_subset_univ = [Fin_mono, Fin_univ] MRS subset_trans |> standard;
    3.42 -
    3.43  goalw Fin_Univ_thy [univ_def] "!!i. n: nat ==> n -> univ(A) <= univ(A)";
    3.44  by (etac (Limit_nat RSN (2,nat_fun_VLimit)) 1);
    3.45  val nat_fun_univ = result();
    3.46  
    3.47  
    3.48 -(*** Infinite branching ***)
    3.49 +(** Closure under finite function space **)
    3.50 +
    3.51 +(*General but seldom-used version; normally the domain is fixed*)
    3.52 +goal Fin_Univ_thy
    3.53 +    "!!i. Limit(i) ==> Vfrom(A,i) -||> Vfrom(A,i) <= Vfrom(A,i)";
    3.54 +by (resolve_tac [FiniteFun.dom_subset RS subset_trans] 1);
    3.55 +by (REPEAT (ares_tac [Fin_subset_VLimit, Sigma_subset_VLimit, subset_refl] 1));
    3.56 +val FiniteFun_VLimit1 = result();
    3.57 +
    3.58 +goalw Fin_Univ_thy [univ_def] "univ(A) -||> univ(A) <= univ(A)";
    3.59 +by (rtac (Limit_nat RS FiniteFun_VLimit1) 1);
    3.60 +val FiniteFun_univ1 = result();
    3.61 +
    3.62 +(*Version for a fixed domain*)
    3.63 +goal Fin_Univ_thy
    3.64 +   "!!i.  [| W <= Vfrom(A,i); Limit(i) |] ==> W -||> Vfrom(A,i) <= Vfrom(A,i)";
    3.65 +by (eresolve_tac [subset_refl RSN (2, FiniteFun_mono) RS subset_trans] 1);
    3.66 +by (eresolve_tac [FiniteFun_VLimit1] 1);
    3.67 +val FiniteFun_VLimit = result();
    3.68 +
    3.69 +goalw Fin_Univ_thy [univ_def]
    3.70 +    "!!W. W <= univ(A) ==> W -||> univ(A) <= univ(A)";
    3.71 +by (etac (Limit_nat RSN (2, FiniteFun_VLimit)) 1);
    3.72 +val FiniteFun_univ = result();
    3.73 +
    3.74 +goal Fin_Univ_thy
    3.75 +    "!!W. [| f: W -||> univ(A);  W <= univ(A) |] ==> f : univ(A)";
    3.76 +by (eresolve_tac [FiniteFun_univ RS subsetD] 1);
    3.77 +by (assume_tac 1);
    3.78 +val FiniteFun_in_univ = result();
    3.79 +
    3.80 +(*Remove <= from the rule above*)
    3.81 +val FiniteFun_in_univ' = subsetI RSN (2, FiniteFun_in_univ);
    3.82 +
    3.83 +
    3.84 +(*** INFINITE BRANCHING ***)
    3.85  
    3.86  val fun_Limit_VfromE = 
    3.87      [apply_funtype, InfCard_csucc RS InfCard_is_Limit] MRS Limit_VfromE
    3.88 @@ -88,7 +123,7 @@
    3.89  
    3.90  (*Version for arbitrary index sets*)
    3.91  goal InfDatatype.thy
    3.92 -    "!!K. [| |W| le K;  W <= Vfrom(A,csucc(K));  InfCard(K) |] ==> \
    3.93 +    "!!K. [| |W| le K;  InfCard(K);  W <= Vfrom(A,csucc(K)) |] ==> \
    3.94  \         W -> Vfrom(A,csucc(K)) <= Vfrom(A,csucc(K))";
    3.95  by (safe_tac (ZF_cs addSDs [fun_Vcsucc_lemma, subset_Vcsucc]));
    3.96  by (resolve_tac [Vfrom RS ssubst] 1);