author  paulson 
Fri, 16 Feb 1996 18:00:47 +0100  
changeset 1512  ce37c64244c0 
parent 1461  6bcb44e4d6e5 
child 1956  589af052bcd4 
permissions  rwrr 
1461  1 
(* Title: ZF/Finite.ML 
516  2 
ID: $Id$ 
1461  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
516  4 
Copyright 1994 University of Cambridge 
5 

534  6 
Finite powerset operator; finite function space 
516  7 

8 
prove X:Fin(A) ==> X < nat 

9 

10 
prove: b: Fin(A) ==> inj(b,b)<=surj(b,b) 

11 
*) 

12 

13 
open Finite; 

14 

534  15 
(*** Finite powerset operator ***) 
16 

516  17 
goalw Finite.thy Fin.defs "!!A B. A<=B ==> Fin(A) <= Fin(B)"; 
18 
by (rtac lfp_mono 1); 

19 
by (REPEAT (rtac Fin.bnd_mono 1)); 

20 
by (REPEAT (ares_tac (Pow_mono::basic_monos) 1)); 

760  21 
qed "Fin_mono"; 
516  22 

23 
(* A : Fin(B) ==> A <= B *) 

24 
val FinD = Fin.dom_subset RS subsetD RS PowD; 

25 

26 
(** Induction on finite sets **) 

27 

28 
(*Discharging x~:y entails extra work*) 

29 
val major::prems = goal Finite.thy 

30 
"[ b: Fin(A); \ 

31 
\ P(0); \ 

32 
\ !!x y. [ x: A; y: Fin(A); x~:y; P(y) ] ==> P(cons(x,y)) \ 

33 
\ ] ==> P(b)"; 

34 
by (rtac (major RS Fin.induct) 1); 

35 
by (excluded_middle_tac "a:b" 2); 

1461  36 
by (etac (cons_absorb RS ssubst) 3 THEN assume_tac 3); (*backtracking!*) 
516  37 
by (REPEAT (ares_tac prems 1)); 
760  38 
qed "Fin_induct"; 
516  39 

40 
(** Simplification for Fin **) 

41 
val Fin_ss = arith_ss addsimps Fin.intrs; 

42 

43 
(*The union of two finite sets is finite.*) 

44 
val major::prems = goal Finite.thy 

45 
"[ b: Fin(A); c: Fin(A) ] ==> b Un c : Fin(A)"; 

46 
by (rtac (major RS Fin_induct) 1); 

47 
by (ALLGOALS (asm_simp_tac (Fin_ss addsimps (prems@[Un_0, Un_cons])))); 

760  48 
qed "Fin_UnI"; 
516  49 

50 
(*The union of a set of finite sets is finite.*) 

51 
val [major] = goal Finite.thy "C : Fin(Fin(A)) ==> Union(C) : Fin(A)"; 

52 
by (rtac (major RS Fin_induct) 1); 

53 
by (ALLGOALS (asm_simp_tac (Fin_ss addsimps [Union_0, Union_cons, Fin_UnI]))); 

760  54 
qed "Fin_UnionI"; 
516  55 

56 
(*Every subset of a finite set is finite.*) 

57 
goal Finite.thy "!!b A. b: Fin(A) ==> ALL z. z<=b > z: Fin(A)"; 

58 
by (etac Fin_induct 1); 

59 
by (simp_tac (Fin_ss addsimps [subset_empty_iff]) 1); 

534  60 
by (asm_simp_tac (ZF_ss addsimps subset_cons_iff::distrib_rews) 1); 
61 
by (safe_tac ZF_cs); 

62 
by (eres_inst_tac [("b","z")] (cons_Diff RS subst) 1); 

63 
by (asm_simp_tac Fin_ss 1); 

760  64 
qed "Fin_subset_lemma"; 
516  65 

66 
goal Finite.thy "!!c b A. [ c<=b; b: Fin(A) ] ==> c: Fin(A)"; 

67 
by (REPEAT (ares_tac [Fin_subset_lemma RS spec RS mp] 1)); 

760  68 
qed "Fin_subset"; 
516  69 

70 
val major::prems = goal Finite.thy 

1461  71 
"[ c: Fin(A); b: Fin(A); \ 
72 
\ P(b); \ 

516  73 
\ !!x y. [ x: A; y: Fin(A); x:y; P(y) ] ==> P(y{x}) \ 
74 
\ ] ==> c<=b > P(bc)"; 

75 
by (rtac (major RS Fin_induct) 1); 

76 
by (rtac (Diff_cons RS ssubst) 2); 

77 
by (ALLGOALS (asm_simp_tac (Fin_ss addsimps (prems@[Diff_0, cons_subset_iff, 

1461  78 
Diff_subset RS Fin_subset])))); 
760  79 
qed "Fin_0_induct_lemma"; 
516  80 

81 
val prems = goal Finite.thy 

1461  82 
"[ b: Fin(A); \ 
83 
\ P(b); \ 

516  84 
\ !!x y. [ x: A; y: Fin(A); x:y; P(y) ] ==> P(y{x}) \ 
85 
\ ] ==> P(0)"; 

86 
by (rtac (Diff_cancel RS subst) 1); 

87 
by (rtac (Fin_0_induct_lemma RS mp) 1); 

88 
by (REPEAT (ares_tac (subset_refl::prems) 1)); 

760  89 
qed "Fin_0_induct"; 
516  90 

91 
(*Functions from a finite ordinal*) 

92 
val prems = goal Finite.thy "n: nat ==> n>A <= Fin(nat*A)"; 

93 
by (nat_ind_tac "n" prems 1); 

94 
by (simp_tac (ZF_ss addsimps [Pi_empty1, Fin.emptyI, subset_iff, cons_iff]) 1); 

95 
by (asm_simp_tac (ZF_ss addsimps [succ_def, mem_not_refl RS cons_fun_eq]) 1); 

96 
by (fast_tac (ZF_cs addSIs [Fin.consI]) 1); 

760  97 
qed "nat_fun_subset_Fin"; 
534  98 

99 

100 
(*** Finite function space ***) 

101 

102 
goalw Finite.thy FiniteFun.defs 

103 
"!!A B C D. [ A<=C; B<=D ] ==> A > B <= C > D"; 

104 
by (rtac lfp_mono 1); 

105 
by (REPEAT (rtac FiniteFun.bnd_mono 1)); 

106 
by (REPEAT (ares_tac (Fin_mono::Sigma_mono::basic_monos) 1)); 

760  107 
qed "FiniteFun_mono"; 
534  108 

109 
goal Finite.thy "!!A B. A<=B ==> A > A <= B > B"; 

110 
by (REPEAT (ares_tac [FiniteFun_mono] 1)); 

760  111 
qed "FiniteFun_mono1"; 
534  112 

113 
goal Finite.thy "!!h. h: A >B ==> h: domain(h) > B"; 

114 
by (etac FiniteFun.induct 1); 

115 
by (simp_tac (ZF_ss addsimps [empty_fun, domain_0]) 1); 

116 
by (asm_simp_tac (ZF_ss addsimps [fun_extend3, domain_cons]) 1); 

760  117 
qed "FiniteFun_is_fun"; 
534  118 

119 
goal Finite.thy "!!h. h: A >B ==> domain(h) : Fin(A)"; 

120 
by (etac FiniteFun.induct 1); 

121 
by (simp_tac (Fin_ss addsimps [domain_0]) 1); 

122 
by (asm_simp_tac (Fin_ss addsimps [domain_cons]) 1); 

760  123 
qed "FiniteFun_domain_Fin"; 
534  124 

803
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
760
diff
changeset

125 
bind_thm ("FiniteFun_apply_type", FiniteFun_is_fun RS apply_type); 
534  126 

127 
(*Every subset of a finite function is a finite function.*) 

128 
goal Finite.thy "!!b A. b: A>B ==> ALL z. z<=b > z: A>B"; 

129 
by (etac FiniteFun.induct 1); 

130 
by (simp_tac (ZF_ss addsimps subset_empty_iff::FiniteFun.intrs) 1); 

131 
by (asm_simp_tac (ZF_ss addsimps subset_cons_iff::distrib_rews) 1); 

132 
by (safe_tac ZF_cs); 

133 
by (eres_inst_tac [("b","z")] (cons_Diff RS subst) 1); 

134 
by (dtac (spec RS mp) 1 THEN assume_tac 1); 

135 
by (fast_tac (ZF_cs addSIs FiniteFun.intrs) 1); 

760  136 
qed "FiniteFun_subset_lemma"; 
534  137 

138 
goal Finite.thy "!!c b A. [ c<=b; b: A>B ] ==> c: A>B"; 

139 
by (REPEAT (ares_tac [FiniteFun_subset_lemma RS spec RS mp] 1)); 

760  140 
qed "FiniteFun_subset"; 
534  141 