--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Psubset.ML Thu May 15 12:45:42 1997 +0200
@@ -0,0 +1,83 @@
+(* Title: Psubset.ML
+ Author: Martin Coen, Cambridge University Computer Laboratory
+ Copyright 1993 University of Cambridge
+
+Properties of subsets and empty sets.
+*)
+
+open Psubset;
+
+(*********)
+
+(*** Rules for subsets ***)
+
+goal Set.thy "A <= B = (! t.t:A --> t:B)";
+by (Blast_tac 1);
+qed "subset_iff";
+
+goalw thy [psubset_def] "!!A::'a set. [| A <= B; A ~= B |] ==> A<B";
+by (Blast_tac 1);
+qed "psubsetI";
+
+
+goalw thy [psubset_def] "((A::'a set) <= B) = ((A < B) | (A=B))";
+by (Blast_tac 1);
+qed "subset_iff_psubset_eq";
+
+
+goal Set.thy "!!a. insert a A ~= insert a B ==> A ~= B";
+by (Blast_tac 1);
+qed "insert_lim";
+
+(* This is an adaptation of the proof for the "<=" version in Finite. *)
+
+goalw thy [psubset_def]
+"!!B. finite B ==> !A. A < B --> card(A) < card(B)";
+by (etac finite_induct 1);
+by (Simp_tac 1);
+by (Blast_tac 1);
+by (strip_tac 1);
+by (etac conjE 1);
+by (case_tac "x:A" 1);
+(*1*)
+by (dtac mk_disjoint_insert 1);
+by (etac exE 1);
+by (etac conjE 1);
+by (hyp_subst_tac 1);
+by (rotate_tac ~1 1);
+by (asm_full_simp_tac (!simpset addsimps [subset_insert_iff,finite_subset]) 1);
+by (dtac insert_lim 1);
+by (Asm_full_simp_tac 1);
+(*2*)
+by (rotate_tac ~1 1);
+by (asm_full_simp_tac (!simpset addsimps [subset_insert_iff,finite_subset]) 1);
+by (case_tac "A=F" 1);
+by (Asm_simp_tac 1);
+by (Asm_simp_tac 1);
+by (subgoal_tac "card A <= card F" 1);
+by (Asm_simp_tac 2);
+by (Auto_tac());
+qed_spec_mp "psubset_card" ;
+
+
+goal Set.thy "(A = B) = ((A <= (B::'a set)) & (B<=A))";
+by (Blast_tac 1);
+qed "set_eq_subset";
+
+
+goalw thy [psubset_def] "~ (A < {})";
+by (Blast_tac 1);
+qed "not_psubset_empty";
+
+AddIffs [not_psubset_empty];
+
+goalw thy [psubset_def]
+ "!!x. A < insert x B ==> (x ~: A) & A<=B | x:A & A-{x}<B";
+by (Auto_tac());
+qed "psubset_insertD";
+
+
+(*NB we do not have [| A < B; C < D |] ==> A Un C < B Un D
+ even for finite sets: consider A={1}, C={2}, B=D={1,2} *)
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Psubset.thy Thu May 15 12:45:42 1997 +0200
@@ -0,0 +1,14 @@
+(* Title: Psubset.thy
+ Author: Martin Coen, Cambridge University Computer Laboratory
+ Copyright 1993 University of Cambridge
+
+The "Proper Subset" relation
+*)
+
+Psubset = Finite +
+
+rules (*not allowed as "defs" because < is overloaded*)
+
+ psubset_def "A < B == A <= B & ~ A=B"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/WF_Rel.ML Thu May 15 12:45:42 1997 +0200
@@ -0,0 +1,119 @@
+(* Title: HOL/WF_Rel
+ ID: $Id$
+ Author: Konrad Slind
+ Copyright 1996 TU Munich
+
+Derived wellfounded relations: inverse image, relational product, measure, ...
+*)
+
+open WF_Rel;
+
+
+(*----------------------------------------------------------------------------
+ * The inverse image into a wellfounded relation is wellfounded.
+ *---------------------------------------------------------------------------*)
+
+goal thy "!!r. wf(r) ==> wf(inv_image r (f::'a=>'b))";
+by (full_simp_tac (!simpset addsimps [inv_image_def, wf_eq_minimal]) 1);
+by (Step_tac 1);
+by (subgoal_tac "? (w::'b). w : {w. ? (x::'a). x: Q & (f x = w)}" 1);
+by (blast_tac (!claset delrules [allE]) 2);
+by (etac allE 1);
+by (mp_tac 1);
+by (Blast_tac 1);
+qed "wf_inv_image";
+AddSIs [wf_inv_image];
+
+(*----------------------------------------------------------------------------
+ * All measures are wellfounded.
+ *---------------------------------------------------------------------------*)
+
+goalw thy [measure_def] "wf (measure f)";
+by (rtac wf_inv_image 1);
+by (rtac wf_trancl 1);
+by (rtac wf_pred_nat 1);
+qed "wf_measure";
+AddIffs [wf_measure];
+
+(*----------------------------------------------------------------------------
+ * Wellfoundedness of lexicographic combinations
+ *---------------------------------------------------------------------------*)
+
+goal Prod.thy "!!P. !a b. P((a,b)) ==> !p. P(p)";
+by (rtac allI 1);
+by (rtac (surjective_pairing RS ssubst) 1);
+by (Blast_tac 1);
+qed "split_all_pair";
+
+val [wfa,wfb] = goalw thy [wf_def,lex_prod_def]
+ "[| wf(ra); wf(rb) |] ==> wf(ra**rb)";
+by (EVERY1 [rtac allI,rtac impI, rtac split_all_pair]);
+by (rtac (wfa RS spec RS mp) 1);
+by (EVERY1 [rtac allI,rtac impI]);
+by (rtac (wfb RS spec RS mp) 1);
+by (Blast_tac 1);
+qed "wf_lex_prod";
+AddSIs [wf_lex_prod];
+
+(*----------------------------------------------------------------------------
+ * Wellfoundedness of relational product
+ *---------------------------------------------------------------------------*)
+val [wfa,wfb] = goalw thy [wf_def,rprod_def]
+ "[| wf(ra); wf(rb) |] ==> wf(rprod ra rb)";
+by (EVERY1 [rtac allI,rtac impI, rtac split_all_pair]);
+by (rtac (wfa RS spec RS mp) 1);
+by (EVERY1 [rtac allI,rtac impI]);
+by (rtac (wfb RS spec RS mp) 1);
+by (Blast_tac 1);
+qed "wf_rel_prod";
+AddSIs [wf_rel_prod];
+
+
+(*---------------------------------------------------------------------------
+ * Wellfoundedness of subsets
+ *---------------------------------------------------------------------------*)
+
+goal thy "!!r. [| wf(r); p<=r |] ==> wf(p)";
+by (full_simp_tac (!simpset addsimps [wf_eq_minimal]) 1);
+by (Fast_tac 1);
+qed "wf_subset";
+
+(*---------------------------------------------------------------------------
+ * Wellfoundedness of the empty relation.
+ *---------------------------------------------------------------------------*)
+
+goal thy "wf({})";
+by (simp_tac (!simpset addsimps [wf_def]) 1);
+qed "wf_empty";
+AddSIs [wf_empty];
+
+
+(*---------------------------------------------------------------------------
+ * Transitivity of WF combinators.
+ *---------------------------------------------------------------------------*)
+goalw thy [trans_def, lex_prod_def]
+ "!!R1 R2. [| trans R1; trans R2 |] ==> trans (R1 ** R2)";
+by (Simp_tac 1);
+by (Blast_tac 1);
+qed "trans_lex_prod";
+AddSIs [trans_lex_prod];
+
+goalw thy [trans_def, rprod_def]
+ "!!R1 R2. [| trans R1; trans R2 |] ==> trans (rprod R1 R2)";
+by (Simp_tac 1);
+by (Blast_tac 1);
+qed "trans_rprod";
+AddSIs [trans_rprod];
+
+
+(*---------------------------------------------------------------------------
+ * Wellfoundedness of proper subset on finite sets.
+ *---------------------------------------------------------------------------*)
+goalw thy [finite_psubset_def] "wf(finite_psubset)";
+by (rtac (wf_measure RS wf_subset) 1);
+by (simp_tac (!simpset addsimps[measure_def, inv_image_def,
+ symmetric less_def])1);
+by (fast_tac (!claset addIs [psubset_card]) 1);
+qed "wf_finite_psubset";
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/WF_Rel.thy Thu May 15 12:45:42 1997 +0200
@@ -0,0 +1,32 @@
+(* Title: HOL/WF_Rel
+ ID: $Id$
+ Author: Konrad Slind
+ Copyright 1995 TU Munich
+
+Derived wellfounded relations: inverse image, relational product, measure, ...
+*)
+
+WF_Rel = WF + Psubset +
+consts
+ inv_image :: "('b * 'b)set => ('a => 'b) => ('a * 'a)set"
+ measure :: "('a => nat) => ('a * 'a)set"
+ "**" :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set" (infixl 70)
+ rprod :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set"
+ finite_psubset :: "('a set * 'a set) set"
+
+defs
+ inv_image_def "inv_image r f == {(x,y). (f(x), f(y)) : r}"
+
+ measure_def "measure == inv_image (trancl pred_nat)"
+
+ lex_prod_def "ra**rb == {p. ? a a' b b'.
+ p = ((a,b),(a',b')) &
+ ((a,a') : ra | a=a' & (b,b') : rb)}"
+
+ rprod_def "rprod ra rb == {p. ? a a' b b'.
+ p = ((a,b),(a',b')) &
+ ((a,a') : ra & (b,b') : rb)}"
+
+ (* finite proper subset*)
+ finite_psubset_def "finite_psubset == {(A,B). A < B & finite B}"
+end