# HG changeset patch # User nipkow # Date 863797241 -7200 # Node ID 726a9b069947c417f256b14953f094544f451f05 # Parent 90211fa9ee7e3ff228a0a09fc8f3ccd314f4fd86 Distributed Psubset stuff to basic set theory files, incl Finite. Added stuff by bu. diff -r 90211fa9ee7e -r 726a9b069947 src/HOL/Finite.ML --- 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" ; diff -r 90211fa9ee7e -r 726a9b069947 src/HOL/IsaMakefile --- 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 \ diff -r 90211fa9ee7e -r 726a9b069947 src/HOL/Psubset.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 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} A Un C < B Un D - even for finite sets: consider A={1}, C={2}, B=D={1,2} *) - - diff -r 90211fa9ee7e -r 726a9b069947 src/HOL/Psubset.thy --- 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 diff -r 90211fa9ee7e -r 726a9b069947 src/HOL/Set.ML --- 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 (x ~: A) & A<=B | x:A & A-{x} 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}" diff -r 90211fa9ee7e -r 726a9b069947 src/HOL/WF_Rel.thy --- 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" diff -r 90211fa9ee7e -r 726a9b069947 src/HOL/equalities.ML --- 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 **)