diff -r 000000000000 -r 7949f97df77a ex/Finite.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/ex/Finite.ML Thu Sep 16 12:21:07 1993 +0200 @@ -0,0 +1,101 @@ +open Finite; + +(** Monotonicity and unfolding of the function **) + +goal Finite.thy "mono(%F. insert({}, UN x:A. insert(x)``F))"; +by (rtac monoI 1); +by (fast_tac set_cs 1); +val Fin_bnd_mono = result(); + +goalw Finite.thy [Fin_def] "!!A B. A<=B ==> Fin(A) <= Fin(B)"; +br lfp_mono 1; +by(fast_tac set_cs 1); +val Fin_mono = result(); + +goalw Finite.thy [Fin_def] "Fin(A) <= {B. B <= A}"; +by (fast_tac (set_cs addSIs [lfp_lowerbound]) 1); +val Fin_subset_Pow = result(); + +(* A : Fin(B) ==> A <= B *) +val FinD = Fin_subset_Pow RS subsetD RS CollectD; + +val Fin_unfold = Fin_bnd_mono RS (Fin_def RS def_lfp_Tarski); + +goal Finite.thy "{} : Fin(A)"; +by (rtac (Fin_unfold RS ssubst) 1); +by (rtac insertI1 1); +val Fin_0I = result(); + +goal Finite.thy "!!a. [| a:A; F:Fin(A) |] ==> insert(a,F) : Fin(A)"; +by (rtac (Fin_unfold RS ssubst) 1); +by(fast_tac set_cs 1); +val Fin_insertI = result(); + +(*Discharging ~ x:y entails extra work*) +val major::prems = goal Finite.thy + "[| F:Fin(A); P({}); \ +\ !!F x. [| x:A; F:Fin(A); ~x:F; P(F) |] ==> P(insert(x,F)) \ +\ |] ==> P(F)"; +by (rtac (major RS (Fin_def RS def_induct)) 1); +by (rtac Fin_bnd_mono 1); +by (safe_tac set_cs); +(*Excluded middle on x:y would be more straightforward; + actual proof is inspired by Dov Gabbay's Restart Rule*) +by (rtac classical 2); +by (REPEAT (ares_tac prems 1)); +by (etac contrapos 1); +by (rtac (insert_absorb RS ssubst) 1); +by (REPEAT (assume_tac 1)); +val Fin_induct = result(); + +(** Simplification for Fin **) + +val Fin_ss = set_ss addsimps [Fin_0I, Fin_insertI]; + +(*The union of two finite sets is finite*) +val major::prems = goal Finite.thy + "[| F: Fin(A); G: Fin(A) |] ==> F Un G : Fin(A)"; +by (rtac (major RS Fin_induct) 1); +by (ALLGOALS (asm_simp_tac (Fin_ss addsimps (prems@[Un_insert_left])))); +val Fin_UnI = result(); + +(*Every subset of a finite set is finite*) +val [subs,fin] = goal Finite.thy "[| A<=B; B: Fin(M) |] ==> A: Fin(M)"; +by (EVERY1 [subgoal_tac "ALL C. C<=B --> C: Fin(M)", + rtac mp, etac spec, + rtac subs]); +by (rtac (fin RS Fin_induct) 1); +by (simp_tac (Fin_ss addsimps [subset_Un_eq]) 1); +by (safe_tac (set_cs addSDs [subset_insert_iff RS iffD1])); +by (eres_inst_tac [("t","C")] (insert_Diff RS subst) 2); +by (ALLGOALS (asm_simp_tac Fin_ss)); +val Fin_subset = result(); + +(*The image of a finite set is finite*) +val major::_ = goal Finite.thy + "F: Fin(A) ==> h``F : Fin(h``A)"; +by (rtac (major RS Fin_induct) 1); +by (simp_tac Fin_ss 1); +by (asm_simp_tac (set_ss addsimps [image_eqI RS Fin_insertI,image_insert]) 1); +val Fin_imageI = result(); + +val major::prems = goal Finite.thy + "[| c: Fin(A); b: Fin(A); \ +\ P(b); \ +\ !!(x::'a) 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_insert RS ssubst) 2); +by (ALLGOALS (asm_simp_tac (Fin_ss addsimps (prems@[insert_subset_iff, + Diff_subset RS Fin_subset])))); +val Fin_empty_induct_lemma = result(); + +val prems = goal Finite.thy + "[| b: Fin(A); \ +\ P(b); \ +\ !!x y. [| x:A; y: Fin(A); x:y; P(y) |] ==> P(y-{x}) \ +\ |] ==> P({})"; +by (rtac (Diff_cancel RS subst) 1); +by (rtac (Fin_empty_induct_lemma RS mp) 1); +by (REPEAT (ares_tac (subset_refl::prems) 1)); +val Fin_empty_induct = result();