# HG changeset patch # User lcp # Date 768229377 -7200 # Node ID 1180a3c5479e4aebdec960ccc9ccf0c58693a55f # Parent 6bea8fdc0e7039e19f447b406f95694cf813ed95 renaming/removal of filenames to correct case diff -r 6bea8fdc0e70 -r 1180a3c5479e src/ZF/Fin.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/Fin.ML Fri May 06 15:02:57 1994 +0200 @@ -0,0 +1,106 @@ +(* Title: ZF/ex/fin.ML + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1993 University of Cambridge + +Finite powerset operator + +could define cardinality? + +prove X:Fin(A) ==> EX n:nat. EX f. f:bij(X,n) + card(0)=0 + [| a~:b; b: Fin(A) |] ==> card(cons(a,b)) = succ(card(b)) + +b: Fin(A) ==> inj(b,b)<=surj(b,b) + +Limit(i) ==> Fin(Vfrom(A,i)) <= Un j:i. Fin(Vfrom(A,j)) +Fin(univ(A)) <= univ(A) +*) + +structure Fin = Inductive_Fun + (val thy = Arith.thy addconsts [(["Fin"],"i=>i")] + val rec_doms = [("Fin","Pow(A)")] + val sintrs = ["0 : Fin(A)", + "[| a: A; b: Fin(A) |] ==> cons(a,b) : Fin(A)"] + val monos = [] + val con_defs = [] + val type_intrs = [empty_subsetI, cons_subsetI, PowI] + val type_elims = [make_elim PowD]); + +store_theory "Fin" Fin.thy; + +val [Fin_0I, Fin_consI] = Fin.intrs; + + +goalw Fin.thy Fin.defs "!!A B. A<=B ==> Fin(A) <= Fin(B)"; +by (rtac lfp_mono 1); +by (REPEAT (rtac Fin.bnd_mono 1)); +by (REPEAT (ares_tac (Pow_mono::basic_monos) 1)); +val Fin_mono = result(); + +(* A : Fin(B) ==> A <= B *) +val FinD = Fin.dom_subset RS subsetD RS PowD; + +(** Induction on finite sets **) + +(*Discharging x~:y entails extra work*) +val major::prems = goal Fin.thy + "[| b: Fin(A); \ +\ P(0); \ +\ !!x y. [| x: A; y: Fin(A); x~:y; P(y) |] ==> P(cons(x,y)) \ +\ |] ==> P(b)"; +by (rtac (major RS Fin.induct) 1); +by (res_inst_tac [("Q","a:b")] (excluded_middle RS disjE) 2); +by (etac (cons_absorb RS ssubst) 3 THEN assume_tac 3); (*backtracking!*) +by (REPEAT (ares_tac prems 1)); +val Fin_induct = result(); + +(** Simplification for Fin **) +val Fin_ss = arith_ss addsimps Fin.intrs; + +(*The union of two finite sets is finite.*) +val major::prems = goal Fin.thy + "[| b: Fin(A); c: Fin(A) |] ==> b Un c : Fin(A)"; +by (rtac (major RS Fin_induct) 1); +by (ALLGOALS (asm_simp_tac (Fin_ss addsimps (prems@[Un_0, Un_cons])))); +val Fin_UnI = result(); + +(*The union of a set of finite sets is finite.*) +val [major] = goal Fin.thy "C : Fin(Fin(A)) ==> Union(C) : Fin(A)"; +by (rtac (major RS Fin_induct) 1); +by (ALLGOALS (asm_simp_tac (Fin_ss addsimps [Union_0, Union_cons, Fin_UnI]))); +val Fin_UnionI = result(); + +(*Every subset of a finite set is finite.*) +goal Fin.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)); +val Fin_subset_lemma = result(); + +goal Fin.thy "!!c b A. [| c<=b; b: Fin(A) |] ==> c: Fin(A)"; +by (REPEAT (ares_tac [Fin_subset_lemma RS spec RS mp] 1)); +val Fin_subset = result(); + +val major::prems = goal Fin.thy + "[| c: Fin(A); b: Fin(A); \ +\ P(b); \ +\ !!x y. [| x: A; y: Fin(A); x:y; P(y) |] ==> P(y-{x}) \ +\ |] ==> c<=b --> P(b-c)"; +by (rtac (major RS Fin_induct) 1); +by (rtac (Diff_cons RS ssubst) 2); +by (ALLGOALS (asm_simp_tac (Fin_ss addsimps (prems@[Diff_0, cons_subset_iff, + Diff_subset RS Fin_subset])))); +val Fin_0_induct_lemma = result(); + +val prems = goal Fin.thy + "[| b: Fin(A); \ +\ P(b); \ +\ !!x y. [| x: A; y: Fin(A); x:y; P(y) |] ==> P(y-{x}) \ +\ |] ==> P(0)"; +by (rtac (Diff_cancel RS subst) 1); +by (rtac (Fin_0_induct_lemma RS mp) 1); +by (REPEAT (ares_tac (subset_refl::prems) 1)); +val Fin_0_induct = result(); diff -r 6bea8fdc0e70 -r 1180a3c5479e src/ZF/Fin.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/Fin.thy Fri May 06 15:02:57 1994 +0200 @@ -0,0 +1,3 @@ +(*Dummy theory to document dependencies *) + +fin = Arith + "inductive" + "constructor" + "intr_elim" + "equalities" diff -r 6bea8fdc0e70 -r 1180a3c5479e src/ZF/Makefile --- a/src/ZF/Makefile Fri May 06 13:50:36 1994 +0200 +++ b/src/ZF/Makefile Fri May 06 15:02:57 1994 +0200 @@ -26,13 +26,13 @@ WF.thy WF.ML Ord.thy Ord.ML Nat.thy Nat.ML \ Epsilon.thy Epsilon.ML Arith.thy Arith.ML Univ.thy Univ.ML \ QUniv.thy QUniv.ML constructor.ML Datatype.ML \ - fin.ML List.ML ListFn.thy ListFn.ML + Fin.ML List.ML ListFn.thy ListFn.ML EX_FILES = ex/ROOT.ML ex/Acc.ML ex/Bin.ML ex/BinFn.ML ex/BinFn.thy\ ex/BT.ML ex/BT_Fn.ML ex/BT_Fn.thy ex/Comb.ML\ - ex/Contract0.ML ex/Contract0.thy ex/counit.ML ex/Data.ML\ + ex/Contract0.ML ex/Contract0.thy ex/CoUnit.ML ex/Data.ML\ ex/Enum.ML ex/Equiv.ML ex/Equiv.thy ex/Integ.ML ex/Integ.thy\ - ex/ListN.ML ex/llist.ML ex/LList_Eq.ML ex/LListFn.ML ex/LListFn.thy\ + ex/ListN.ML ex/LList.ML ex/LList_Eq.ML ex/LListFn.ML ex/LListFn.thy\ ex/misc.ML ex/ParContract.ML ex/Primrec0.ML ex/Primrec0.thy\ ex/Prop.ML ex/PropLog.ML ex/PropLog.thy ex/Ramsey.ML ex/Ramsey.thy\ ex/Rmap.ML ex/Term.ML ex/TermFn.ML ex/TermFn.thy ex/TF.ML\