Distributed Psubset stuff to basic set theory files, incl Finite.
authornipkow
Fri May 16 17:40:41 1997 +0200 (1997-05-16)
changeset 3222726a9b069947
parent 3221 90211fa9ee7e
child 3223 49f1a09576c2
Distributed Psubset stuff to basic set theory files, incl Finite.
Added stuff by bu.
src/HOL/Finite.ML
src/HOL/IsaMakefile
src/HOL/Psubset.ML
src/HOL/Psubset.thy
src/HOL/Set.ML
src/HOL/Set.thy
src/HOL/WF_Rel.thy
src/HOL/equalities.ML
     1.1 --- a/src/HOL/Finite.ML	Fri May 16 17:14:55 1997 +0200
     1.2 +++ b/src/HOL/Finite.ML	Fri May 16 17:40:41 1997 +0200
     1.3 @@ -322,3 +322,28 @@
     1.4  by (rotate_tac ~1 1);
     1.5  by (asm_full_simp_tac (!simpset addsimps [subset_insert_iff,finite_subset]) 1);
     1.6  qed_spec_mp "card_mono";
     1.7 +
     1.8 +goalw Finite.thy [psubset_def]
     1.9 +"!!B. finite B ==> !A. A < B --> card(A) < card(B)";
    1.10 +by (etac finite_induct 1);
    1.11 +by (Simp_tac 1);
    1.12 +by (Blast_tac 1);
    1.13 +by (strip_tac 1);
    1.14 +by (etac conjE 1);
    1.15 +by (case_tac "x:A" 1);
    1.16 +(*1*)
    1.17 +by (dtac mk_disjoint_insert 1);
    1.18 +by (etac exE 1);
    1.19 +by (etac conjE 1);
    1.20 +by (hyp_subst_tac 1);
    1.21 +by (rotate_tac ~1 1);
    1.22 +by (asm_full_simp_tac (!simpset addsimps [subset_insert_iff,finite_subset]) 1);
    1.23 +by (dtac insert_lim 1);
    1.24 +by (Asm_full_simp_tac 1);
    1.25 +(*2*)
    1.26 +by (rotate_tac ~1 1);
    1.27 +by (asm_full_simp_tac (!simpset addsimps [subset_insert_iff,finite_subset]) 1);
    1.28 +by (case_tac "A=F" 1);
    1.29 +by (Asm_simp_tac 1);
    1.30 +by (Asm_simp_tac 1);
    1.31 +qed_spec_mp "psubset_card" ;
     2.1 --- a/src/HOL/IsaMakefile	Fri May 16 17:14:55 1997 +0200
     2.2 +++ b/src/HOL/IsaMakefile	Fri May 16 17:40:41 1997 +0200
     2.3 @@ -10,7 +10,7 @@
     2.4  
     2.5  NAMES = HOL Ord Set Fun subset equalities Prod Relation Trancl Sum WF WF_Rel \
     2.6  	mono Lfp Gfp NatDef Nat intr_elim indrule Inductive Finite Arith \
     2.7 -	Psubset Sexp Univ List RelPow Option
     2.8 +	Sexp Univ List RelPow Option
     2.9  
    2.10  FILES = ROOT.ML add_ind_def.ML datatype.ML hologic.ML \
    2.11  	ind_syntax.ML cladata.ML simpdata.ML \
     3.1 --- a/src/HOL/Psubset.ML	Fri May 16 17:14:55 1997 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,83 +0,0 @@
     3.4 -(*  Title:      Psubset.ML
     3.5 -    Author:     Martin Coen, Cambridge University Computer Laboratory
     3.6 -    Copyright   1993  University of Cambridge
     3.7 -
     3.8 -Properties of subsets and empty sets.
     3.9 -*)
    3.10 -
    3.11 -open Psubset;
    3.12 -
    3.13 -(*********)
    3.14 -
    3.15 -(*** Rules for subsets ***)
    3.16 -
    3.17 -goal Set.thy "A <= B =  (! t.t:A --> t:B)";
    3.18 -by (Blast_tac 1);
    3.19 -qed "subset_iff";
    3.20 -
    3.21 -goalw thy [psubset_def] "!!A::'a set. [| A <= B; A ~= B |] ==> A<B";
    3.22 -by (Blast_tac 1);
    3.23 -qed "psubsetI";
    3.24 -
    3.25 -
    3.26 -goalw thy [psubset_def] "((A::'a set) <= B) = ((A < B) | (A=B))";
    3.27 -by (Blast_tac 1);
    3.28 -qed "subset_iff_psubset_eq";
    3.29 -
    3.30 -
    3.31 -goal Set.thy "!!a. insert a A ~= insert a B ==> A ~= B";
    3.32 -by (Blast_tac 1);
    3.33 -qed "insert_lim";
    3.34 -
    3.35 -(* This is an adaptation of the proof for the "<=" version in Finite. *) 
    3.36 -
    3.37 -goalw thy [psubset_def]
    3.38 -"!!B. finite B ==> !A. A < B --> card(A) < card(B)";
    3.39 -by (etac finite_induct 1);
    3.40 -by (Simp_tac 1);
    3.41 -by (Blast_tac 1);
    3.42 -by (strip_tac 1);
    3.43 -by (etac conjE 1);
    3.44 -by (case_tac "x:A" 1);
    3.45 -(*1*)
    3.46 -by (dtac mk_disjoint_insert 1);
    3.47 -by (etac exE 1);
    3.48 -by (etac conjE 1);
    3.49 -by (hyp_subst_tac 1);
    3.50 -by (rotate_tac ~1 1);
    3.51 -by (asm_full_simp_tac (!simpset addsimps [subset_insert_iff,finite_subset]) 1);
    3.52 -by (dtac insert_lim 1);
    3.53 -by (Asm_full_simp_tac 1);
    3.54 -(*2*)
    3.55 -by (rotate_tac ~1 1);
    3.56 -by (asm_full_simp_tac (!simpset addsimps [subset_insert_iff,finite_subset]) 1);
    3.57 -by (case_tac "A=F" 1);
    3.58 -by (Asm_simp_tac 1);
    3.59 -by (Asm_simp_tac 1);
    3.60 -by (subgoal_tac "card A <= card F" 1);
    3.61 -by (Asm_simp_tac 2);
    3.62 -by (Auto_tac());
    3.63 -qed_spec_mp "psubset_card" ;
    3.64 -
    3.65 -
    3.66 -goal Set.thy "(A = B) = ((A <= (B::'a set)) & (B<=A))";
    3.67 -by (Blast_tac 1);
    3.68 -qed "set_eq_subset";
    3.69 -
    3.70 -
    3.71 -goalw thy [psubset_def] "~ (A < {})";
    3.72 -by (Blast_tac 1);
    3.73 -qed "not_psubset_empty";
    3.74 -
    3.75 -AddIffs [not_psubset_empty];
    3.76 -
    3.77 -goalw thy [psubset_def]
    3.78 -    "!!x. A < insert x B ==> (x ~: A) & A<=B | x:A & A-{x}<B";
    3.79 -by (Auto_tac());
    3.80 -qed "psubset_insertD";
    3.81 -
    3.82 -
    3.83 -(*NB we do not have  [| A < B; C < D |] ==> A Un C < B Un D
    3.84 -  even for finite sets: consider A={1}, C={2}, B=D={1,2} *)
    3.85 -
    3.86 -
     4.1 --- a/src/HOL/Psubset.thy	Fri May 16 17:14:55 1997 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,14 +0,0 @@
     4.4 -(*  Title:      Psubset.thy
     4.5 -    Author:     Martin Coen, Cambridge University Computer Laboratory
     4.6 -    Copyright   1993  University of Cambridge
     4.7 -
     4.8 -The "Proper Subset" relation
     4.9 -*)
    4.10 -
    4.11 -Psubset = Finite + 
    4.12 -
    4.13 -rules   (*not allowed as "defs" because < is overloaded*)
    4.14 -
    4.15 -  psubset_def    "A < B == A <= B & ~ A=B"
    4.16 -
    4.17 -end
     5.1 --- a/src/HOL/Set.ML	Fri May 16 17:14:55 1997 +0200
     5.2 +++ b/src/HOL/Set.ML	Fri May 16 17:40:41 1997 +0200
     5.3 @@ -666,3 +666,17 @@
     5.4  
     5.5  simpset := !simpset addcongs [ball_cong,bex_cong]
     5.6                      setmksimps (mksimps mksimps_pairs);
     5.7 +
     5.8 +Addsimps[subset_UNIV, empty_subsetI, subset_refl];
     5.9 +
    5.10 +
    5.11 +(*** < ***)
    5.12 +
    5.13 +goalw Set.thy [psubset_def] "!!A::'a set. [| A <= B; A ~= B |] ==> A<B";
    5.14 +by (Blast_tac 1);
    5.15 +qed "psubsetI";
    5.16 +
    5.17 +goalw Set.thy [psubset_def]
    5.18 +    "!!x. A < insert x B ==> (x ~: A) & A<=B | x:A & A-{x}<B";
    5.19 +by (Auto_tac());
    5.20 +qed "psubset_insertD";
     6.1 --- a/src/HOL/Set.thy	Fri May 16 17:14:55 1997 +0200
     6.2 +++ b/src/HOL/Set.thy	Fri May 16 17:40:41 1997 +0200
     6.3 @@ -133,6 +133,7 @@
     6.4    Ball_def      "Ball A P       == ! x. x:A --> P(x)"
     6.5    Bex_def       "Bex A P        == ? x. x:A & P(x)"
     6.6    subset_def    "A <= B         == ! x:A. x:B"
     6.7 +  psubset_def   "A < B          == (A::'a set) <= B & ~ A=B"
     6.8    Compl_def     "Compl A        == {x. ~x:A}"
     6.9    Un_def        "A Un B         == {x.x:A | x:B}"
    6.10    Int_def       "A Int B        == {x.x:A & x:B}"
     7.1 --- a/src/HOL/WF_Rel.thy	Fri May 16 17:14:55 1997 +0200
     7.2 +++ b/src/HOL/WF_Rel.thy	Fri May 16 17:40:41 1997 +0200
     7.3 @@ -6,7 +6,7 @@
     7.4  Derived wellfounded relations: inverse image, relational product, measure, ...
     7.5  *)
     7.6  
     7.7 -WF_Rel = WF + Psubset +
     7.8 +WF_Rel = Finite +
     7.9  consts
    7.10   inv_image  :: "('b * 'b)set => ('a => 'b) => ('a * 'a)set"
    7.11   measure    :: "('a => nat) => ('a * 'a)set"
     8.1 --- a/src/HOL/equalities.ML	Fri May 16 17:14:55 1997 +0200
     8.2 +++ b/src/HOL/equalities.ML	Fri May 16 17:40:41 1997 +0200
     8.3 @@ -22,6 +22,11 @@
     8.4  qed "subset_empty";
     8.5  Addsimps [subset_empty];
     8.6  
     8.7 +goalw thy [psubset_def] "~ (A < {})";
     8.8 +by (Blast_tac 1);
     8.9 +qed "not_psubset_empty";
    8.10 +AddIffs [not_psubset_empty];
    8.11 +
    8.12  section "insert";
    8.13  
    8.14  (*NOT SUITABLE FOR REWRITING since {a} == insert a {}*)
    8.15 @@ -55,6 +60,10 @@
    8.16  qed "insert_subset";
    8.17  Addsimps[insert_subset];
    8.18  
    8.19 +goal Set.thy "!!a. insert a A ~= insert a B ==> A ~= B";
    8.20 +by (Blast_tac 1);
    8.21 +qed "insert_lim";
    8.22 +
    8.23  (* use new B rather than (A-{a}) to avoid infinite unfolding *)
    8.24  goal Set.thy "!!a. a:A ==> ? B. A = insert a B & a ~: B";
    8.25  by (res_inst_tac [("x","A-{a}")] exI 1);
    8.26 @@ -82,6 +91,18 @@
    8.27  qed "image_insert";
    8.28  Addsimps[image_insert];
    8.29  
    8.30 +goal Set.thy  "(f `` (UNION A B)) = (UN x:A.(f `` (B x)))";
    8.31 +by (Blast_tac 1);
    8.32 +qed "image_UNION";
    8.33 +
    8.34 +goal Set.thy "(%x. x) `` Y = Y";
    8.35 +by (Blast_tac 1);
    8.36 +qed "image_id";
    8.37 +
    8.38 +goal Set.thy "f``(range g) = range (%x. f (g x))";
    8.39 +by(Blast_tac 1);
    8.40 +qed "image_range";
    8.41 +
    8.42  qed_goal "ball_image" Set.thy "(!y:F``S. P y) = (!x:S. P (F x))"
    8.43   (fn _ => [Blast_tac 1]);
    8.44  
    8.45 @@ -104,9 +125,6 @@
    8.46  qed_goal "ball_range" Set.thy "(!y:range f. P y) = (!x. P (f x))"
    8.47   (fn _ => [Blast_tac 1]);
    8.48  
    8.49 -qed_goalw "image_range" Set.thy [image_def]
    8.50 - "f``range g = range (%x. f (g x))" 
    8.51 - (fn _ => [rtac Collect_cong 1, Blast_tac 1]);
    8.52  
    8.53  section "Int";
    8.54  
    8.55 @@ -167,10 +185,18 @@
    8.56  qed "Un_absorb";
    8.57  Addsimps[Un_absorb];
    8.58  
    8.59 +goal Set.thy " A Un (A Un B) = A Un B";
    8.60 +by (Blast_tac 1);
    8.61 +qed "Un_left_absorb";
    8.62 +
    8.63  goal Set.thy "A Un B  =  B Un A";
    8.64  by (Blast_tac 1);
    8.65  qed "Un_commute";
    8.66  
    8.67 +goal Set.thy " A Un (B Un C) = B Un (A Un C)";
    8.68 +by (Blast_tac 1);
    8.69 +qed "Un_left_commute";
    8.70 +
    8.71  goal Set.thy "(A Un B) Un C  =  A Un (B Un C)";
    8.72  by (Blast_tac 1);
    8.73  qed "Un_assoc";
    8.74 @@ -329,6 +355,11 @@
    8.75  qed "UN_empty";
    8.76  Addsimps[UN_empty];
    8.77  
    8.78 +goal Set.thy "(UN x:A. {}) = {}";
    8.79 +by(Blast_tac 1);
    8.80 +qed "UN_empty2";
    8.81 +Addsimps[UN_empty2];
    8.82 +
    8.83  goal Set.thy "(UN x:UNIV. B x) = (UN x. B x)";
    8.84  by (Blast_tac 1);
    8.85  qed "UN_UNIV";
    8.86 @@ -349,6 +380,10 @@
    8.87  qed "UN_insert";
    8.88  Addsimps[UN_insert];
    8.89  
    8.90 +goal Set.thy "(UN i: A Un B. M i) = ((UN i: A. M i) Un (UN i:B. M i))";
    8.91 +by (Blast_tac 1);
    8.92 +qed "UN_Un";
    8.93 +
    8.94  goal Set.thy "(INT x:insert a A. B x) = B a Int INTER A B";
    8.95  by (Blast_tac 1);
    8.96  qed "INT_insert";
    8.97 @@ -406,6 +441,11 @@
    8.98  by (Blast_tac 1);
    8.99  qed "INT_eq";
   8.100  
   8.101 +goalw Set.thy [o_def] "UNION A (g o f) = UNION (f``A) g";
   8.102 +by (Blast_tac 1);
   8.103 +qed "UNION_o";
   8.104 +
   8.105 +
   8.106  (*Distributive laws...*)
   8.107  
   8.108  goal Set.thy "A Int Union(B) = (UN C:B. A Int C)";
   8.109 @@ -542,7 +582,28 @@
   8.110  by (Blast_tac 1);
   8.111  qed "Diff_Int";
   8.112  
   8.113 -Addsimps[subset_UNIV, empty_subsetI, subset_refl];
   8.114 +goal Set.thy "(A Un B) - C = (A - C) Un (B - C)";
   8.115 +by (Blast_tac 1);
   8.116 +qed "Un_Diff";
   8.117 +
   8.118 +goal Set.thy "(A Int B) - C = (A - C) Int (B - C)";
   8.119 +by (Blast_tac 1);
   8.120 +qed "Int_Diff";
   8.121 +
   8.122 +
   8.123 +section "Miscellany";
   8.124 +
   8.125 +goal Set.thy "(A = B) = ((A <= (B::'a set)) & (B<=A))";
   8.126 +by (Blast_tac 1);
   8.127 +qed "set_eq_subset";
   8.128 +
   8.129 +goal Set.thy "A <= B =  (! t.t:A --> t:B)";
   8.130 +by (Blast_tac 1);
   8.131 +qed "subset_iff";
   8.132 +
   8.133 +goalw thy [psubset_def] "((A::'a set) <= B) = ((A < B) | (A=B))";
   8.134 +by (Blast_tac 1);
   8.135 +qed "subset_iff_psubset_eq";
   8.136  
   8.137  
   8.138  (** Miniscoping: pushing in big Unions and Intersections **)