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();