Distributed Psubset stuff to basic set theory files, incl Finite.
Added stuff by bu.

--- a/src/HOL/Finite.ML	Fri May 16 17:14:55 1997 +0200
+++ b/src/HOL/Finite.ML	Fri May 16 17:40:41 1997 +0200
@@ -322,3 +322,28 @@
 by (rotate_tac ~1 1);
 by (asm_full_simp_tac (!simpset addsimps [subset_insert_iff,finite_subset]) 1);
 qed_spec_mp "card_mono";
+
+goalw Finite.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);
+qed_spec_mp "psubset_card" ;

--- a/src/HOL/IsaMakefile	Fri May 16 17:14:55 1997 +0200
+++ b/src/HOL/IsaMakefile	Fri May 16 17:40:41 1997 +0200
@@ -10,7 +10,7 @@
 
 NAMES = HOL Ord Set Fun subset equalities Prod Relation Trancl Sum WF WF_Rel \
 	mono Lfp Gfp NatDef Nat intr_elim indrule Inductive Finite Arith \
-	Psubset Sexp Univ List RelPow Option
+	Sexp Univ List RelPow Option
 
 FILES = ROOT.ML add_ind_def.ML datatype.ML hologic.ML \
 	ind_syntax.ML cladata.ML simpdata.ML \

--- a/src/HOL/Psubset.ML	Fri May 16 17:14:55 1997 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,83 +0,0 @@
-(*  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} *)
-
-

--- a/src/HOL/Psubset.thy	Fri May 16 17:14:55 1997 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,14 +0,0 @@
-(*  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

--- a/src/HOL/Set.ML	Fri May 16 17:14:55 1997 +0200
+++ b/src/HOL/Set.ML	Fri May 16 17:40:41 1997 +0200
@@ -666,3 +666,17 @@
 
 simpset := !simpset addcongs [ball_cong,bex_cong]
                     setmksimps (mksimps mksimps_pairs);
+
+Addsimps[subset_UNIV, empty_subsetI, subset_refl];
+
+
+(*** < ***)
+
+goalw Set.thy [psubset_def] "!!A::'a set. [| A <= B; A ~= B |] ==> A<B";
+by (Blast_tac 1);
+qed "psubsetI";
+
+goalw Set.thy [psubset_def]
+    "!!x. A < insert x B ==> (x ~: A) & A<=B | x:A & A-{x}<B";
+by (Auto_tac());
+qed "psubset_insertD";

--- a/src/HOL/Set.thy	Fri May 16 17:14:55 1997 +0200
+++ b/src/HOL/Set.thy	Fri May 16 17:40:41 1997 +0200
@@ -133,6 +133,7 @@
   Ball_def      "Ball A P       == ! x. x:A --> P(x)"
   Bex_def       "Bex A P        == ? x. x:A & P(x)"
   subset_def    "A <= B         == ! x:A. x:B"
+  psubset_def   "A < B          == (A::'a set) <= B & ~ A=B"
   Compl_def     "Compl A        == {x. ~x:A}"
   Un_def        "A Un B         == {x.x:A | x:B}"
   Int_def       "A Int B        == {x.x:A & x:B}"

--- a/src/HOL/WF_Rel.thy	Fri May 16 17:14:55 1997 +0200
+++ b/src/HOL/WF_Rel.thy	Fri May 16 17:40:41 1997 +0200
@@ -6,7 +6,7 @@
 Derived wellfounded relations: inverse image, relational product, measure, ...
 *)
 
-WF_Rel = WF + Psubset +
+WF_Rel = Finite +
 consts
  inv_image  :: "('b * 'b)set => ('a => 'b) => ('a * 'a)set"
  measure    :: "('a => nat) => ('a * 'a)set"

--- a/src/HOL/equalities.ML	Fri May 16 17:14:55 1997 +0200
+++ b/src/HOL/equalities.ML	Fri May 16 17:40:41 1997 +0200
@@ -22,6 +22,11 @@
 qed "subset_empty";
 Addsimps [subset_empty];
 
+goalw thy [psubset_def] "~ (A < {})";
+by (Blast_tac 1);
+qed "not_psubset_empty";
+AddIffs [not_psubset_empty];
+
 section "insert";
 
 (*NOT SUITABLE FOR REWRITING since {a} == insert a {}*)
@@ -55,6 +60,10 @@
 qed "insert_subset";
 Addsimps[insert_subset];
 
+goal Set.thy "!!a. insert a A ~= insert a B ==> A ~= B";
+by (Blast_tac 1);
+qed "insert_lim";
+
 (* use new B rather than (A-{a}) to avoid infinite unfolding *)
 goal Set.thy "!!a. a:A ==> ? B. A = insert a B & a ~: B";
 by (res_inst_tac [("x","A-{a}")] exI 1);
@@ -82,6 +91,18 @@
 qed "image_insert";
 Addsimps[image_insert];
 
+goal Set.thy  "(f `` (UNION A B)) = (UN x:A.(f `` (B x)))";
+by (Blast_tac 1);
+qed "image_UNION";
+
+goal Set.thy "(%x. x) `` Y = Y";
+by (Blast_tac 1);
+qed "image_id";
+
+goal Set.thy "f``(range g) = range (%x. f (g x))";
+by(Blast_tac 1);
+qed "image_range";
+
 qed_goal "ball_image" Set.thy "(!y:F``S. P y) = (!x:S. P (F x))"
  (fn _ => [Blast_tac 1]);
 
@@ -104,9 +125,6 @@
 qed_goal "ball_range" Set.thy "(!y:range f. P y) = (!x. P (f x))"
  (fn _ => [Blast_tac 1]);
 
-qed_goalw "image_range" Set.thy [image_def]
- "f``range g = range (%x. f (g x))" 
- (fn _ => [rtac Collect_cong 1, Blast_tac 1]);
 
 section "Int";
 
@@ -167,10 +185,18 @@
 qed "Un_absorb";
 Addsimps[Un_absorb];
 
+goal Set.thy " A Un (A Un B) = A Un B";
+by (Blast_tac 1);
+qed "Un_left_absorb";
+
 goal Set.thy "A Un B  =  B Un A";
 by (Blast_tac 1);
 qed "Un_commute";
 
+goal Set.thy " A Un (B Un C) = B Un (A Un C)";
+by (Blast_tac 1);
+qed "Un_left_commute";
+
 goal Set.thy "(A Un B) Un C  =  A Un (B Un C)";
 by (Blast_tac 1);
 qed "Un_assoc";
@@ -329,6 +355,11 @@
 qed "UN_empty";
 Addsimps[UN_empty];
 
+goal Set.thy "(UN x:A. {}) = {}";
+by(Blast_tac 1);
+qed "UN_empty2";
+Addsimps[UN_empty2];
+
 goal Set.thy "(UN x:UNIV. B x) = (UN x. B x)";
 by (Blast_tac 1);
 qed "UN_UNIV";
@@ -349,6 +380,10 @@
 qed "UN_insert";
 Addsimps[UN_insert];
 
+goal Set.thy "(UN i: A Un B. M i) = ((UN i: A. M i) Un (UN i:B. M i))";
+by (Blast_tac 1);
+qed "UN_Un";
+
 goal Set.thy "(INT x:insert a A. B x) = B a Int INTER A B";
 by (Blast_tac 1);
 qed "INT_insert";
@@ -406,6 +441,11 @@
 by (Blast_tac 1);
 qed "INT_eq";
 
+goalw Set.thy [o_def] "UNION A (g o f) = UNION (f``A) g";
+by (Blast_tac 1);
+qed "UNION_o";
+
+
 (*Distributive laws...*)
 
 goal Set.thy "A Int Union(B) = (UN C:B. A Int C)";
@@ -542,7 +582,28 @@
 by (Blast_tac 1);
 qed "Diff_Int";
 
-Addsimps[subset_UNIV, empty_subsetI, subset_refl];
+goal Set.thy "(A Un B) - C = (A - C) Un (B - C)";
+by (Blast_tac 1);
+qed "Un_Diff";
+
+goal Set.thy "(A Int B) - C = (A - C) Int (B - C)";
+by (Blast_tac 1);
+qed "Int_Diff";
+
+
+section "Miscellany";
+
+goal Set.thy "(A = B) = ((A <= (B::'a set)) & (B<=A))";
+by (Blast_tac 1);
+qed "set_eq_subset";
+
+goal Set.thy "A <= B =  (! t.t:A --> t:B)";
+by (Blast_tac 1);
+qed "subset_iff";
+
+goalw thy [psubset_def] "((A::'a set) <= B) = ((A < B) | (A=B))";
+by (Blast_tac 1);
+qed "subset_iff_psubset_eq";
 
 
 (** Miniscoping: pushing in big Unions and Intersections **)