# HG changeset patch # User wenzelm # Date 1013889574 -3600 # Node ID f4d10ad0ea7bf6d9a75c6859ef285248d5c25eed # Parent 4518acda6d93b7a89d2b27aa44fcf11339868c7f converted/deleted equalities.ML, mono.ML, subset.ML (see Set.thy); diff -r 4518acda6d93 -r f4d10ad0ea7b src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Fri Feb 15 20:43:44 2002 +0100 +++ b/src/HOL/IsaMakefile Sat Feb 16 20:59:34 2002 +0100 @@ -102,8 +102,7 @@ Transitive_Closure.thy Transitive_Closure.ML Typedef.thy \ Wellfounded_Recursion.ML Wellfounded_Recursion.thy Wellfounded_Relations.ML \ Wellfounded_Relations.thy arith_data.ML blastdata.ML cladata.ML \ - document/root.tex equalities.ML hologic.ML meson_lemmas.ML mono.ML \ - simpdata.ML subset.ML thy_syntax.ML + document/root.tex hologic.ML meson_lemmas.ML simpdata.ML thy_syntax.ML @$(ISATOOL) usedir -b -g true $(OUT)/Pure HOL diff -r 4518acda6d93 -r f4d10ad0ea7b src/HOL/Set.ML --- a/src/HOL/Set.ML Fri Feb 15 20:43:44 2002 +0100 +++ b/src/HOL/Set.ML Sat Feb 16 20:59:34 2002 +0100 @@ -1,6 +1,415 @@ (* legacy ML bindings *) +val Ball_def = thm "Ball_def"; +val Bex_def = thm "Bex_def"; +val CollectD = thm "CollectD"; +val CollectE = thm "CollectE"; +val CollectI = thm "CollectI"; +val Collect_all_eq = thm "Collect_all_eq"; +val Collect_ball_eq = thm "Collect_ball_eq"; +val Collect_bex_eq = thm "Collect_bex_eq"; +val Collect_cong = thm "Collect_cong"; +val Collect_conj_eq = thm "Collect_conj_eq"; +val Collect_const = thm "Collect_const"; +val Collect_disj_eq = thm "Collect_disj_eq"; +val Collect_empty_eq = thm "Collect_empty_eq"; +val Collect_ex_eq = thm "Collect_ex_eq"; +val Collect_mem_eq = thm "Collect_mem_eq"; +val Collect_mono = thm "Collect_mono"; +val Collect_neg_eq = thm "Collect_neg_eq"; +val ComplD = thm "ComplD"; +val ComplE = thm "ComplE"; +val ComplI = thm "ComplI"; +val Compl_Diff_eq = thm "Compl_Diff_eq"; +val Compl_INT = thm "Compl_INT"; +val Compl_Int = thm "Compl_Int"; +val Compl_UN = thm "Compl_UN"; +val Compl_UNIV_eq = thm "Compl_UNIV_eq"; +val Compl_Un = thm "Compl_Un"; +val Compl_anti_mono = thm "Compl_anti_mono"; +val Compl_def = thm "Compl_def"; +val Compl_disjoint = thm "Compl_disjoint"; +val Compl_disjoint2 = thm "Compl_disjoint2"; +val Compl_empty_eq = thm "Compl_empty_eq"; +val Compl_eq_Compl_iff = thm "Compl_eq_Compl_iff"; +val Compl_iff = thm "Compl_iff"; +val Compl_partition = thm "Compl_partition"; +val Compl_subset_Compl_iff = thm "Compl_subset_Compl_iff"; +val DiffD1 = thm "DiffD1"; +val DiffD2 = thm "DiffD2"; +val DiffE = thm "DiffE"; +val DiffI = thm "DiffI"; +val Diff_Compl = thm "Diff_Compl"; +val Diff_Int = thm "Diff_Int"; +val Diff_Int_distrib = thm "Diff_Int_distrib"; +val Diff_Int_distrib2 = thm "Diff_Int_distrib2"; +val Diff_UNIV = thm "Diff_UNIV"; +val Diff_Un = thm "Diff_Un"; +val Diff_cancel = thm "Diff_cancel"; +val Diff_disjoint = thm "Diff_disjoint"; +val Diff_empty = thm "Diff_empty"; +val Diff_eq = thm "Diff_eq"; +val Diff_eq_empty_iff = thm "Diff_eq_empty_iff"; +val Diff_iff = thm "Diff_iff"; +val Diff_insert = thm "Diff_insert"; +val Diff_insert0 = thm "Diff_insert0"; +val Diff_insert2 = thm "Diff_insert2"; +val Diff_insert_absorb = thm "Diff_insert_absorb"; +val Diff_mono = thm "Diff_mono"; +val Diff_partition = thm "Diff_partition"; +val Diff_subset = thm "Diff_subset"; +val Diff_triv = thm "Diff_triv"; +val INTER_def = thm "INTER_def"; +val INT_D = thm "INT_D"; +val INT_E = thm "INT_E"; +val INT_I = thm "INT_I"; +val INT_Int_distrib = thm "INT_Int_distrib"; +val INT_Un = thm "INT_Un"; +val INT_absorb = thm "INT_absorb"; +val INT_anti_mono = thm "INT_anti_mono"; +val INT_bool_eq = thm "INT_bool_eq"; +val INT_cong = thm "INT_cong"; +val INT_constant = thm "INT_constant"; +val INT_empty = thm "INT_empty"; +val INT_eq = thm "INT_eq"; +val INT_greatest = thm "INT_greatest"; +val INT_iff = thm "INT_iff"; +val INT_insert = thm "INT_insert"; +val INT_insert_distrib = thm "INT_insert_distrib"; +val INT_lower = thm "INT_lower"; +val INT_simps = thms "INT_simps"; +val INT_subset_iff = thm "INT_subset_iff"; +val IntD1 = thm "IntD1"; +val IntD2 = thm "IntD2"; +val IntE = thm "IntE"; +val IntI = thm "IntI"; +val Int_Collect = thm "Int_Collect"; +val Int_Collect_mono = thm "Int_Collect_mono"; +val Int_Diff = thm "Int_Diff"; +val Int_Inter_image = thm "Int_Inter_image"; +val Int_UNIV = thm "Int_UNIV"; +val Int_UNIV_left = thm "Int_UNIV_left"; +val Int_UNIV_right = thm "Int_UNIV_right"; +val Int_UN_distrib = thm "Int_UN_distrib"; +val Int_UN_distrib2 = thm "Int_UN_distrib2"; +val Int_Un_distrib = thm "Int_Un_distrib"; +val Int_Un_distrib2 = thm "Int_Un_distrib2"; +val Int_Union = thm "Int_Union"; +val Int_Union2 = thm "Int_Union2"; +val Int_absorb = thm "Int_absorb"; +val Int_absorb1 = thm "Int_absorb1"; +val Int_absorb2 = thm "Int_absorb2"; +val Int_ac = thms "Int_ac"; +val Int_assoc = thm "Int_assoc"; +val Int_commute = thm "Int_commute"; +val Int_def = thm "Int_def"; +val Int_empty_left = thm "Int_empty_left"; +val Int_empty_right = thm "Int_empty_right"; +val Int_eq_Inter = thm "Int_eq_Inter"; +val Int_greatest = thm "Int_greatest"; +val Int_iff = thm "Int_iff"; +val Int_insert_left = thm "Int_insert_left"; +val Int_insert_right = thm "Int_insert_right"; +val Int_left_absorb = thm "Int_left_absorb"; +val Int_left_commute = thm "Int_left_commute"; +val Int_lower1 = thm "Int_lower1"; +val Int_lower2 = thm "Int_lower2"; +val Int_mono = thm "Int_mono"; +val Int_subset_iff = thm "Int_subset_iff"; +val InterD = thm "InterD"; +val InterE = thm "InterE"; +val InterI = thm "InterI"; +val Inter_UNIV = thm "Inter_UNIV"; +val Inter_Un_distrib = thm "Inter_Un_distrib"; +val Inter_Un_subset = thm "Inter_Un_subset"; +val Inter_anti_mono = thm "Inter_anti_mono"; +val Inter_def = thm "Inter_def"; +val Inter_empty = thm "Inter_empty"; +val Inter_greatest = thm "Inter_greatest"; +val Inter_iff = thm "Inter_iff"; +val Inter_image_eq = thm "Inter_image_eq"; +val Inter_insert = thm "Inter_insert"; +val Inter_lower = thm "Inter_lower"; +val PowD = thm "PowD"; +val PowI = thm "PowI"; +val Pow_Compl = thm "Pow_Compl"; +val Pow_INT_eq = thm "Pow_INT_eq"; +val Pow_Int_eq = thm "Pow_Int_eq"; +val Pow_UNIV = thm "Pow_UNIV"; +val Pow_bottom = thm "Pow_bottom"; +val Pow_def = thm "Pow_def"; +val Pow_empty = thm "Pow_empty"; +val Pow_iff = thm "Pow_iff"; +val Pow_insert = thm "Pow_insert"; +val Pow_mono = thm "Pow_mono"; +val Pow_top = thm "Pow_top"; +val UNION_def = thm "UNION_def"; +val UNIV_I = thm "UNIV_I"; +val UNIV_def = thm "UNIV_def"; +val UNIV_not_empty = thm "UNIV_not_empty"; +val UNIV_witness = thm "UNIV_witness"; +val UN_E = thm "UN_E"; +val UN_I = thm "UN_I"; +val UN_Pow_subset = thm "UN_Pow_subset"; +val UN_UN_flatten = thm "UN_UN_flatten"; +val UN_Un = thm "UN_Un"; +val UN_Un_distrib = thm "UN_Un_distrib"; +val UN_absorb = thm "UN_absorb"; +val UN_bool_eq = thm "UN_bool_eq"; +val UN_cong = thm "UN_cong"; +val UN_constant = thm "UN_constant"; +val UN_empty = thm "UN_empty"; +val UN_empty2 = thm "UN_empty2"; +val UN_empty3 = thm "UN_empty3"; +val UN_eq = thm "UN_eq"; +val UN_iff = thm "UN_iff"; +val UN_insert = thm "UN_insert"; +val UN_insert_distrib = thm "UN_insert_distrib"; +val UN_least = thm "UN_least"; +val UN_mono = thm "UN_mono"; +val UN_simps = thms "UN_simps"; +val UN_singleton = thm "UN_singleton"; +val UN_subset_iff = thm "UN_subset_iff"; +val UN_upper = thm "UN_upper"; +val UnCI = thm "UnCI"; +val UnE = thm "UnE"; +val UnI1 = thm "UnI1"; +val UnI2 = thm "UnI2"; +val Un_Diff = thm "Un_Diff"; +val Un_Diff_Int = thm "Un_Diff_Int"; +val Un_Diff_cancel = thm "Un_Diff_cancel"; +val Un_Diff_cancel2 = thm "Un_Diff_cancel2"; +val Un_INT_distrib = thm "Un_INT_distrib"; +val Un_INT_distrib2 = thm "Un_INT_distrib2"; +val Un_Int_assoc_eq = thm "Un_Int_assoc_eq"; +val Un_Int_crazy = thm "Un_Int_crazy"; +val Un_Int_distrib = thm "Un_Int_distrib"; +val Un_Int_distrib2 = thm "Un_Int_distrib2"; +val Un_Inter = thm "Un_Inter"; +val Un_Pow_subset = thm "Un_Pow_subset"; +val Un_UNIV_left = thm "Un_UNIV_left"; +val Un_UNIV_right = thm "Un_UNIV_right"; +val Un_Union_image = thm "Un_Union_image"; +val Un_absorb = thm "Un_absorb"; +val Un_absorb1 = thm "Un_absorb1"; +val Un_absorb2 = thm "Un_absorb2"; +val Un_ac = thms "Un_ac"; +val Un_assoc = thm "Un_assoc"; +val Un_commute = thm "Un_commute"; +val Un_def = thm "Un_def"; +val Un_empty = thm "Un_empty"; +val Un_empty_left = thm "Un_empty_left"; +val Un_empty_right = thm "Un_empty_right"; +val Un_eq_UN = thm "Un_eq_UN"; +val Un_eq_Union = thm "Un_eq_Union"; +val Un_iff = thm "Un_iff"; +val Un_insert_left = thm "Un_insert_left"; +val Un_insert_right = thm "Un_insert_right"; +val Un_least = thm "Un_least"; +val Un_left_absorb = thm "Un_left_absorb"; +val Un_left_commute = thm "Un_left_commute"; +val Un_mono = thm "Un_mono"; +val Un_subset_iff = thm "Un_subset_iff"; +val Un_upper1 = thm "Un_upper1"; +val Un_upper2 = thm "Un_upper2"; +val UnionE = thm "UnionE"; +val UnionI = thm "UnionI"; +val Union_Int_subset = thm "Union_Int_subset"; +val Union_Pow_eq = thm "Union_Pow_eq"; +val Union_UNIV = thm "Union_UNIV"; +val Union_Un_distrib = thm "Union_Un_distrib"; +val Union_def = thm "Union_def"; +val Union_disjoint = thm "Union_disjoint"; +val Union_empty = thm "Union_empty"; +val Union_empty_conv = thm "Union_empty_conv"; +val Union_iff = thm "Union_iff"; +val Union_image_eq = thm "Union_image_eq"; +val Union_insert = thm "Union_insert"; +val Union_least = thm "Union_least"; +val Union_mono = thm "Union_mono"; +val Union_upper = thm "Union_upper"; +val all_bool_eq = thm "all_bool_eq"; +val all_mono = thm "all_mono"; +val all_not_in_conv = thm "all_not_in_conv"; +val atomize_ball = thm "atomize_ball"; +val ballE = thm "ballE"; +val ballI = thm "ballI"; +val ball_UN = thm "ball_UN"; +val ball_UNIV = thm "ball_UNIV"; +val ball_Un = thm "ball_Un"; +val ball_cong = thm "ball_cong"; +val ball_conj_distrib = thm "ball_conj_distrib"; +val ball_empty = thm "ball_empty"; +val ball_one_point1 = thm "ball_one_point1"; +val ball_one_point2 = thm "ball_one_point2"; +val ball_simps = thms "ball_simps"; +val ball_triv = thm "ball_triv"; +val basic_monos = thms "basic_monos"; +val bexCI = thm "bexCI"; +val bexE = thm "bexE"; +val bexI = thm "bexI"; +val bex_UN = thm "bex_UN"; +val bex_UNIV = thm "bex_UNIV"; +val bex_Un = thm "bex_Un"; +val bex_cong = thm "bex_cong"; +val bex_disj_distrib = thm "bex_disj_distrib"; +val bex_empty = thm "bex_empty"; +val bex_one_point1 = thm "bex_one_point1"; +val bex_one_point2 = thm "bex_one_point2"; +val bex_simps = thms "bex_simps"; +val bex_triv = thm "bex_triv"; +val bex_triv_one_point1 = thm "bex_triv_one_point1"; +val bex_triv_one_point2 = thm "bex_triv_one_point2"; +val bool_induct = thm "bool_induct"; +val bspec = thm "bspec"; +val conj_mono = thm "conj_mono"; +val contra_subsetD = thm "contra_subsetD"; +val diff_single_insert = thm "diff_single_insert"; +val disj_mono = thm "disj_mono"; +val disjoint_eq_subset_Compl = thm "disjoint_eq_subset_Compl"; +val disjoint_iff_not_equal = thm "disjoint_iff_not_equal"; +val distinct_lemma = thm "distinct_lemma"; +val double_complement = thm "double_complement"; +val double_diff = thm "double_diff"; +val emptyE = thm "emptyE"; +val empty_Diff = thm "empty_Diff"; +val empty_def = thm "empty_def"; +val empty_iff = thm "empty_iff"; +val empty_subsetI = thm "empty_subsetI"; +val eq_to_mono = thm "eq_to_mono"; +val eq_to_mono2 = thm "eq_to_mono2"; +val eqset_imp_iff = thm "eqset_imp_iff"; +val equalityCE = thm "equalityCE"; +val equalityD1 = thm "equalityD1"; +val equalityD2 = thm "equalityD2"; +val equalityE = thm "equalityE"; +val equalityI = thm "equalityI"; +val equals0D = thm "equals0D"; +val equals0I = thm "equals0I"; +val ex_bool_eq = thm "ex_bool_eq"; +val ex_mono = thm "ex_mono"; +val full_SetCompr_eq = thm "full_SetCompr_eq"; +val if_image_distrib = thm "if_image_distrib"; +val imageE = thm "imageE"; +val imageI = thm "imageI"; +val image_Collect = thm "image_Collect"; +val image_Un = thm "image_Un"; +val image_Union = thm "image_Union"; +val image_cong = thm "image_cong"; +val image_constant = thm "image_constant"; +val image_def = thm "image_def"; +val image_empty = thm "image_empty"; +val image_eqI = thm "image_eqI"; +val image_iff = thm "image_iff"; +val image_image = thm "image_image"; +val image_insert = thm "image_insert"; +val image_is_empty = thm "image_is_empty"; +val image_mono = thm "image_mono"; +val image_subsetI = thm "image_subsetI"; +val image_subset_iff = thm "image_subset_iff"; +val imp_mono = thm "imp_mono"; +val imp_refl = thm "imp_refl"; +val in_mono = thm "in_mono"; +val insertCI = thm "insertCI"; +val insertE = thm "insertE"; +val insertI1 = thm "insertI1"; +val insertI2 = thm "insertI2"; +val insert_Collect = thm "insert_Collect"; +val insert_Diff = thm "insert_Diff"; +val insert_Diff1 = thm "insert_Diff1"; +val insert_Diff_if = thm "insert_Diff_if"; +val insert_absorb = thm "insert_absorb"; +val insert_absorb2 = thm "insert_absorb2"; +val insert_commute = thm "insert_commute"; +val insert_def = thm "insert_def"; +val insert_iff = thm "insert_iff"; +val insert_image = thm "insert_image"; +val insert_is_Un = thm "insert_is_Un"; +val insert_mono = thm "insert_mono"; +val insert_not_empty = thm "insert_not_empty"; +val insert_subset = thm "insert_subset"; +val mem_Collect_eq = thm "mem_Collect_eq"; +val mem_simps = thms "mem_simps"; +val mk_disjoint_insert = thm "mk_disjoint_insert"; +val mono_Int = thm "mono_Int"; +val mono_Un = thm "mono_Un"; +val not_psubset_empty = thm "not_psubset_empty"; +val psubsetI = thm "psubsetI"; +val psubset_def = thm "psubset_def"; +val psubset_eq = thm "psubset_eq"; +val psubset_imp_ex_mem = thm "psubset_imp_ex_mem"; +val psubset_imp_subset = thm "psubset_imp_subset"; +val psubset_insert_iff = thm "psubset_insert_iff"; +val psubset_subset_trans = thm "psubset_subset_trans"; +val rangeE = thm "rangeE"; +val rangeI = thm "rangeI"; +val range_composition = thm "range_composition"; +val range_eqI = thm "range_eqI"; +val rev_bexI = thm "rev_bexI"; +val rev_image_eqI = thm "rev_image_eqI"; +val rev_subsetD = thm "rev_subsetD"; +val set_diff_def = thm "set_diff_def"; +val set_eq_subset = thm "set_eq_subset"; +val set_ext = thm "set_ext"; +val setup_induction = thm "setup_induction"; +val singletonD = thm "singletonD"; +val singletonE = thm "singletonE"; +val singletonI = thm "singletonI"; +val singleton_conv = thm "singleton_conv"; +val singleton_conv2 = thm "singleton_conv2"; +val singleton_iff = thm "singleton_iff"; +val singleton_inject = thm "singleton_inject"; +val singleton_insert_inj_eq = thm "singleton_insert_inj_eq"; +val singleton_insert_inj_eq' = thm "singleton_insert_inj_eq'"; +val split_if_eq1 = thm "split_if_eq1"; +val split_if_eq2 = thm "split_if_eq2"; +val split_if_mem1 = thm "split_if_mem1"; +val split_if_mem2 = thm "split_if_mem2"; +val split_ifs = thms "split_ifs"; +val strip = thms "strip"; +val subsetCE = thm "subsetCE"; +val subsetD = thm "subsetD"; +val subsetI = thm "subsetI"; +val subset_Compl_self_eq = thm "subset_Compl_self_eq"; +val subset_Pow_Union = thm "subset_Pow_Union"; +val subset_UNIV = thm "subset_UNIV"; +val subset_Un_eq = thm "subset_Un_eq"; +val subset_antisym = thm "subset_antisym"; +val subset_def = thm "subset_def"; +val subset_empty = thm "subset_empty"; +val subset_iff = thm "subset_iff"; +val subset_iff_psubset_eq = thm "subset_iff_psubset_eq"; +val subset_image_iff = thm "subset_image_iff"; +val subset_insert = thm "subset_insert"; +val subset_insertI = thm "subset_insertI"; +val subset_insert_iff = thm "subset_insert_iff"; +val subset_psubset_trans = thm "subset_psubset_trans"; +val subset_refl = thm "subset_refl"; +val subset_singletonD = thm "subset_singletonD"; +val subset_trans = thm "subset_trans"; +val vimageD = thm "vimageD"; +val vimageE = thm "vimageE"; +val vimageI = thm "vimageI"; +val vimageI2 = thm "vimageI2"; +val vimage_Collect = thm "vimage_Collect"; +val vimage_Collect_eq = thm "vimage_Collect_eq"; +val vimage_Compl = thm "vimage_Compl"; +val vimage_Diff = thm "vimage_Diff"; +val vimage_INT = thm "vimage_INT"; +val vimage_Int = thm "vimage_Int"; +val vimage_UN = thm "vimage_UN"; +val vimage_UNIV = thm "vimage_UNIV"; +val vimage_Un = thm "vimage_Un"; +val vimage_Union = thm "vimage_Union"; +val vimage_def = thm "vimage_def"; +val vimage_empty = thm "vimage_empty"; +val vimage_eq = thm "vimage_eq"; +val vimage_eq_UN = thm "vimage_eq_UN"; +val vimage_insert = thm "vimage_insert"; +val vimage_mono = thm "vimage_mono"; +val vimage_singleton_eq = thm "vimage_singleton_eq"; + structure Set = struct val thy = the_context (); @@ -24,25 +433,3 @@ val set_diff_def = set_diff_def; val subset_def = subset_def; end; - -val vimageD = thm "vimageD"; -val vimageE = thm "vimageE"; -val vimageI = thm "vimageI"; -val vimageI2 = thm "vimageI2"; -val vimage_Collect = thm "vimage_Collect"; -val vimage_Collect_eq = thm "vimage_Collect_eq"; -val vimage_Compl = thm "vimage_Compl"; -val vimage_Diff = thm "vimage_Diff"; -val vimage_INT = thm "vimage_INT"; -val vimage_Int = thm "vimage_Int"; -val vimage_UN = thm "vimage_UN"; -val vimage_UNIV = thm "vimage_UNIV"; -val vimage_Un = thm "vimage_Un"; -val vimage_Union = thm "vimage_Union"; -val vimage_def = thm "vimage_def"; -val vimage_empty = thm "vimage_empty"; -val vimage_eq = thm "vimage_eq"; -val vimage_eq_UN = thm "vimage_eq_UN"; -val vimage_insert = thm "vimage_insert"; -val vimage_mono = thm "vimage_mono"; -val vimage_singleton_eq = thm "vimage_singleton_eq"; diff -r 4518acda6d93 -r f4d10ad0ea7b src/HOL/Set.thy --- a/src/HOL/Set.thy Fri Feb 15 20:43:44 2002 +0100 +++ b/src/HOL/Set.thy Sat Feb 16 20:59:34 2002 +0100 @@ -6,8 +6,7 @@ header {* Set theory for higher-order logic *} -theory Set = HOL -files ("subset.ML") ("equalities.ML") ("mono.ML"): +theory Set = HOL: text {* A set in HOL is simply a predicate. *} @@ -339,7 +338,7 @@ subsubsection {* Subsets *} -lemma subsetI [intro!]: "(!!x. x:A ==> x:B) ==> A <= B" +lemma subsetI [intro!]: "(!!x. x:A ==> x:B) ==> A \ B" by (simp add: subset_def) text {* @@ -364,13 +363,13 @@ Blast.overloaded (\"image\", domain_type); " -lemma subsetD [elim]: "A <= B ==> c:A ==> c:B" +lemma subsetD [elim]: "A \ B ==> c \ A ==> c \ B" -- {* Rule in Modus Ponens style. *} by (unfold subset_def) blast declare subsetD [intro?] -- FIXME -lemma rev_subsetD: "c:A ==> A <= B ==> c:B" +lemma rev_subsetD: "c \ A ==> A \ B ==> c \ B" -- {* The same, with reversed premises for use with @{text erule} -- cf @{text rev_mp}. *} by (rule subsetD) @@ -378,7 +377,7 @@ declare rev_subsetD [intro?] -- FIXME text {* - \medskip Converts @{prop "A <= B"} to @{prop "x:A ==> x:B"}. + \medskip Converts @{prop "A \ B"} to @{prop "x \ A ==> x \ B"}. *} ML {* @@ -386,13 +385,13 @@ in fun impOfSubs th = th RSN (2, rev_subsetD) end; *} -lemma subsetCE [elim]: "A <= B ==> (c~:A ==> P) ==> (c:B ==> P) ==> P" +lemma subsetCE [elim]: "A \ B ==> (c \ A ==> P) ==> (c \ B ==> P) ==> P" -- {* Classical elimination rule. *} by (unfold subset_def) blast text {* - \medskip Takes assumptions @{prop "A <= B"}; @{prop "c:A"} and - creates the assumption @{prop "c:B"}. + \medskip Takes assumptions @{prop "A \ B"}; @{prop "c \ A"} and + creates the assumption @{prop "c \ B"}. *} ML {* @@ -400,46 +399,46 @@ in fun set_mp_tac i = etac subsetCE i THEN mp_tac i end; *} -lemma contra_subsetD: "A <= B ==> c ~: B ==> c ~: A" +lemma contra_subsetD: "A \ B ==> c \ B ==> c \ A" by blast -lemma subset_refl: "A <= (A::'a set)" +lemma subset_refl: "A \ A" by fast -lemma subset_trans: "A <= B ==> B <= C ==> A <= (C::'a set)" +lemma subset_trans: "A \ B ==> B \ C ==> A \ C" by blast subsubsection {* Equality *} -lemma subset_antisym [intro!]: "A <= B ==> B <= A ==> A = (B::'a set)" +lemma subset_antisym [intro!]: "A \ B ==> B \ A ==> A = B" -- {* Anti-symmetry of the subset relation. *} - by (rule set_ext) (blast intro: subsetD) - -lemmas equalityI = subset_antisym + by (rules intro: set_ext subsetD) + +lemmas equalityI [intro!] = subset_antisym text {* \medskip Equality rules from ZF set theory -- are they appropriate here? *} -lemma equalityD1: "A = B ==> A <= (B::'a set)" +lemma equalityD1: "A = B ==> A \ B" by (simp add: subset_refl) -lemma equalityD2: "A = B ==> B <= (A::'a set)" +lemma equalityD2: "A = B ==> B \ A" by (simp add: subset_refl) text {* \medskip Be careful when adding this to the claset as @{text subset_empty} is in the simpset: @{prop "A = {}"} goes to @{prop "{} - <= A"} and @{prop "A <= {}"} and then back to @{prop "A = {}"}! + \ A"} and @{prop "A \ {}"} and then back to @{prop "A = {}"}! *} -lemma equalityE: "A = B ==> (A <= B ==> B <= (A::'a set) ==> P) ==> P" +lemma equalityE: "A = B ==> (A \ B ==> B \ A ==> P) ==> P" by (simp add: subset_refl) lemma equalityCE [elim]: - "A = B ==> (c:A ==> c:B ==> P) ==> (c~:A ==> c~:B ==> P) ==> P" + "A = B ==> (c \ A ==> c \ B ==> P) ==> (c \ A ==> c \ B ==> P) ==> P" by blast text {* @@ -466,7 +465,7 @@ lemma UNIV_witness [intro?]: "EX x. x : UNIV" by simp -lemma subset_UNIV: "A <= UNIV" +lemma subset_UNIV: "A \ UNIV" by (rule subsetI) (rule UNIV_I) text {* @@ -490,14 +489,14 @@ lemma emptyE [elim!]: "a : {} ==> P" by simp -lemma empty_subsetI [iff]: "{} <= A" +lemma empty_subsetI [iff]: "{} \ A" -- {* One effect is to delete the ASSUMPTION @{prop "{} <= A"} *} by blast -lemma equals0I: "(!!y. y:A ==> False) ==> A = {}" +lemma equals0I: "(!!y. y \ A ==> False) ==> A = {}" by blast -lemma equals0D: "A={} ==> a ~: A" +lemma equals0D: "A = {} ==> a \ A" -- {* Use for reasoning about disjointness: @{prop "A Int B = {}"} *} by blast @@ -513,28 +512,28 @@ subsubsection {* The Powerset operator -- Pow *} -lemma Pow_iff [iff]: "(A : Pow B) = (A <= B)" +lemma Pow_iff [iff]: "(A \ Pow B) = (A \ B)" by (simp add: Pow_def) -lemma PowI: "A <= B ==> A : Pow B" +lemma PowI: "A \ B ==> A \ Pow B" by (simp add: Pow_def) -lemma PowD: "A : Pow B ==> A <= B" +lemma PowD: "A \ Pow B ==> A \ B" by (simp add: Pow_def) -lemma Pow_bottom: "{}: Pow B" +lemma Pow_bottom: "{} \ Pow B" by simp -lemma Pow_top: "A : Pow A" +lemma Pow_top: "A \ Pow A" by (simp add: subset_refl) subsubsection {* Set complement *} -lemma Compl_iff [simp]: "(c : -A) = (c~:A)" +lemma Compl_iff [simp]: "(c \ -A) = (c \ A)" by (unfold Compl_def) blast -lemma ComplI [intro!]: "(c:A ==> False) ==> c : -A" +lemma ComplI [intro!]: "(c \ A ==> False) ==> c \ -A" by (unfold Compl_def) blast text {* @@ -625,7 +624,7 @@ -- {* Classical introduction rule. *} by auto -lemma subset_insert_iff: "(A <= insert x B) = (if x:A then A - {x} <= B else A <= B)" +lemma subset_insert_iff: "(A \ insert x B) = (if x:A then A - {x} \ B else A \ B)" by auto @@ -646,13 +645,13 @@ lemma singleton_inject [dest!]: "{a} = {b} ==> a = b" by blast -lemma singleton_insert_inj_eq [iff]: "({b} = insert a A) = (a = b & A <= {b})" +lemma singleton_insert_inj_eq [iff]: "({b} = insert a A) = (a = b & A \ {b})" by blast -lemma singleton_insert_inj_eq' [iff]: "(insert a A = {b}) = (a = b & A <= {b})" +lemma singleton_insert_inj_eq' [iff]: "(insert a A = {b}) = (a = b & A \ {b})" by blast -lemma subset_singletonD: "A <= {x} ==> A={} | A = {x}" +lemma subset_singletonD: "A \ {x} ==> A = {} | A = {x}" by fast lemma singleton_conv [simp]: "{x. x = a} = {a}" @@ -661,7 +660,7 @@ lemma singleton_conv2 [simp]: "{x. a = x} = {a}" by blast -lemma diff_single_insert: "A - {x} <= B ==> x : A ==> A <= insert x B" +lemma diff_single_insert: "A - {x} \ B ==> x \ A ==> A \ insert x B" by blast @@ -772,18 +771,18 @@ lemma image_iff: "(z : f`A) = (EX x:A. z = f x)" by blast -lemma image_subset_iff: "(f`A <= B) = (ALL x:A. f x: B)" +lemma image_subset_iff: "(f`A \ B) = (\x\A. f x \ B)" -- {* This rewrite rule would confuse users if made default. *} by blast -lemma subset_image_iff: "(B <= f ` A) = (EX AA. AA <= A & B = f ` AA)" +lemma subset_image_iff: "(B \ f`A) = (EX AA. AA \ A & B = f`AA)" apply safe prefer 2 apply fast apply (rule_tac x = "{a. a : A & f a : B}" in exI) apply fast done -lemma image_subsetI: "(!!x. x:A ==> f x : B) ==> f`A <= B" +lemma image_subsetI: "(!!x. x \ A ==> f x \ B) ==> f`A \ B" -- {* Replaces the three steps @{text subsetI}, @{text imageE}, @{text hypsubst}, but breaks too many existing proofs. *} by blast @@ -792,13 +791,13 @@ \medskip Range of a function -- just a translation for image! *} -lemma range_eqI: "b = f x ==> b : range f" +lemma range_eqI: "b = f x ==> b \ range f" by simp -lemma rangeI: "f x : range f" +lemma rangeI: "f x \ range f" by simp -lemma rangeE [elim?]: "b : range (%x. f x) ==> (!!x. b = f x ==> P) ==> P" +lemma rangeE [elim?]: "b \ range (\x. f x) ==> (!!x. b = f x ==> P) ==> P" by blast @@ -852,32 +851,30 @@ subsubsection {* The ``proper subset'' relation *} -lemma psubsetI [intro!]: "(A::'a set) <= B ==> A ~= B ==> A < B" +lemma psubsetI [intro!]: "A \ B ==> A \ B ==> A \ B" by (unfold psubset_def) blast lemma psubset_insert_iff: - "(A < insert x B) = (if x:B then A < B else if x:A then A - {x} < B else A <= B)" - apply (simp add: psubset_def subset_insert_iff) - apply blast - done - -lemma psubset_eq: "((A::'a set) < B) = (A <= B & A ~= B)" + "(A \ insert x B) = (if x \ B then A \ B else if x \ A then A - {x} \ B else A \ B)" + by (auto simp add: psubset_def subset_insert_iff) + +lemma psubset_eq: "(A \ B) = (A \ B & A \ B)" by (simp only: psubset_def) -lemma psubset_imp_subset: "(A::'a set) < B ==> A <= B" +lemma psubset_imp_subset: "A \ B ==> A \ B" by (simp add: psubset_eq) -lemma psubset_subset_trans: "(A::'a set) < B ==> B <= C ==> A < C" +lemma psubset_subset_trans: "A \ B ==> B \ C ==> A \ C" by (auto simp add: psubset_eq) -lemma subset_psubset_trans: "(A::'a set) <= B ==> B < C ==> A < C" +lemma subset_psubset_trans: "A \ B ==> B \ C ==> A \ C" by (auto simp add: psubset_eq) -lemma psubset_imp_ex_mem: "A < B ==> EX b. b : (B - A)" +lemma psubset_imp_ex_mem: "A \ B ==> \b. b \ (B - A)" by (unfold psubset_def) blast lemma atomize_ball: - "(!!x. x:A ==> P x) == Trueprop (ALL x:A. P x)" + "(!!x. x \ A ==> P x) == Trueprop (\x\A. P x)" by (simp only: Ball_def atomize_all atomize_imp) declare atomize_ball [symmetric, rulify] @@ -885,9 +882,898 @@ subsection {* Further set-theory lemmas *} -use "subset.ML" -use "equalities.ML" -use "mono.ML" +subsubsection {* Derived rules involving subsets. *} + +text {* @{text insert}. *} + +lemma subset_insertI: "B \ insert a B" + apply (rule subsetI) + apply (erule insertI2) + done + +lemma subset_insert: "x \ A ==> (A \ insert x B) = (A \ B)" + by blast + + +text {* \medskip Big Union -- least upper bound of a set. *} + +lemma Union_upper: "B \ A ==> B \ Union A" + by (rules intro: subsetI UnionI) + +lemma Union_least: "(!!X. X \ A ==> X \ C) ==> Union A \ C" + by (rules intro: subsetI elim: UnionE dest: subsetD) + + +text {* \medskip General union. *} + +lemma UN_upper: "a \ A ==> B a \ (\x\A. B x)" + by blast + +lemma UN_least: "(!!x. x \ A ==> B x \ C) ==> (\x\A. B x) \ C" + by (rules intro: subsetI elim: UN_E dest: subsetD) + + +text {* \medskip Big Intersection -- greatest lower bound of a set. *} + +lemma Inter_lower: "B \ A ==> Inter A \ B" + by blast + +lemma Inter_greatest: "(!!X. X \ A ==> C \ X) ==> C \ Inter A" + by (rules intro: InterI subsetI dest: subsetD) + +lemma INT_lower: "a \ A ==> (\x\A. B x) \ B a" + by blast + +lemma INT_greatest: "(!!x. x \ A ==> C \ B x) ==> C \ (\x\A. B x)" + by (rules intro: INT_I subsetI dest: subsetD) + + +text {* \medskip Finite Union -- the least upper bound of two sets. *} + +lemma Un_upper1: "A \ A \ B" + by blast + +lemma Un_upper2: "B \ A \ B" + by blast + +lemma Un_least: "A \ C ==> B \ C ==> A \ B \ C" + by blast + + +text {* \medskip Finite Intersection -- the greatest lower bound of two sets. *} + +lemma Int_lower1: "A \ B \ A" + by blast + +lemma Int_lower2: "A \ B \ B" + by blast + +lemma Int_greatest: "C \ A ==> C \ B ==> C \ A \ B" + by blast + + +text {* \medskip Set difference. *} + +lemma Diff_subset: "A - B \ A" + by blast + + +text {* \medskip Monotonicity. *} + +lemma mono_Un: "mono f ==> f A \ f B \ f (A \ B)" + apply (rule Un_least) + apply (erule Un_upper1 [THEN [2] monoD]) + apply (erule Un_upper2 [THEN [2] monoD]) + done + +lemma mono_Int: "mono f ==> f (A \ B) \ f A \ f B" + apply (rule Int_greatest) + apply (erule Int_lower1 [THEN [2] monoD]) + apply (erule Int_lower2 [THEN [2] monoD]) + done + + +subsubsection {* Equalities involving union, intersection, inclusion, etc. *} + +text {* @{text "{}"}. *} + +lemma Collect_const [simp]: "{s. P} = (if P then UNIV else {})" + -- {* supersedes @{text "Collect_False_empty"} *} + by auto + +lemma subset_empty [simp]: "(A \ {}) = (A = {})" + by blast + +lemma not_psubset_empty [iff]: "\ (A < {})" + by (unfold psubset_def) blast + +lemma Collect_empty_eq [simp]: "(Collect P = {}) = (\x. \ P x)" + by auto + +lemma Collect_neg_eq: "{x. \ P x} = - {x. P x}" + by blast + +lemma Collect_disj_eq: "{x. P x | Q x} = {x. P x} \ {x. Q x}" + by blast + +lemma Collect_conj_eq: "{x. P x & Q x} = {x. P x} \ {x. Q x}" + by blast + +lemma Collect_all_eq: "{x. \y. P x y} = (\y. {x. P x y})" + by blast + +lemma Collect_ball_eq: "{x. \y\A. P x y} = (\y\A. {x. P x y})" + by blast + +lemma Collect_ex_eq: "{x. \y. P x y} = (\y. {x. P x y})" + by blast + +lemma Collect_bex_eq: "{x. \y\A. P x y} = (\y\A. {x. P x y})" + by blast + + +text {* \medskip @{text insert}. *} + +lemma insert_is_Un: "insert a A = {a} Un A" + -- {* NOT SUITABLE FOR REWRITING since @{text "{a} == insert a {}"} *} + by blast + +lemma insert_not_empty [simp]: "insert a A \ {}" + by blast + +lemmas empty_not_insert [simp] = insert_not_empty [symmetric, standard] + +lemma insert_absorb: "a \ A ==> insert a A = A" + -- {* @{text "[simp]"} causes recursive calls when there are nested inserts *} + -- {* with \emph{quadratic} running time *} + by blast + +lemma insert_absorb2 [simp]: "insert x (insert x A) = insert x A" + by blast + +lemma insert_commute: "insert x (insert y A) = insert y (insert x A)" + by blast + +lemma insert_subset [simp]: "(insert x A \ B) = (x \ B & A \ B)" + by blast + +lemma mk_disjoint_insert: "a \ A ==> \B. A = insert a B & a \ B" + -- {* use new @{text B} rather than @{text "A - {a}"} to avoid infinite unfolding *} + apply (rule_tac x = "A - {a}" in exI) + apply blast + done + +lemma insert_Collect: "insert a (Collect P) = {u. u \ a --> P u}" + by auto + +lemma UN_insert_distrib: "u \ A ==> (\x\A. insert a (B x)) = insert a (\x\A. B x)" + by blast + + +text {* \medskip @{text image}. *} + +lemma image_empty [simp]: "f`{} = {}" + by blast + +lemma image_insert [simp]: "f ` insert a B = insert (f a) (f`B)" + by blast + +lemma image_constant: "x \ A ==> (\x. c) ` A = {c}" + by blast + +lemma image_image: "f ` (g ` A) = (\x. f (g x)) ` A" + by blast + +lemma insert_image [simp]: "x \ A ==> insert (f x) (f`A) = f`A" + by blast + +lemma image_is_empty [iff]: "(f`A = {}) = (A = {})" + by blast + +lemma image_Collect: "f ` {x. P x} = {f x | x. P x}" + -- {* NOT suitable as a default simprule: the RHS isn't simpler than the LHS, *} + -- {* with its implicit quantifier and conjunction. Also image enjoys better *} + -- {* equational properties than does the RHS. *} + by blast + +lemma if_image_distrib [simp]: + "(\x. if P x then f x else g x) ` S + = (f ` (S \ {x. P x})) \ (g ` (S \ {x. \ P x}))" + by (auto simp add: image_def) + +lemma image_cong: "M = N ==> (!!x. x \ N ==> f x = g x) ==> f`M = g`N" + by (simp add: image_def) + + +text {* \medskip @{text range}. *} + +lemma full_SetCompr_eq: "{u. \x. u = f x} = range f" + by auto + +lemma range_composition [simp]: "range (\x. f (g x)) = f`range g" + apply (subst image_image) + apply simp + done + + +text {* \medskip @{text Int} *} + +lemma Int_absorb [simp]: "A \ A = A" + by blast + +lemma Int_left_absorb: "A \ (A \ B) = A \ B" + by blast + +lemma Int_commute: "A \ B = B \ A" + by blast + +lemma Int_left_commute: "A \ (B \ C) = B \ (A \ C)" + by blast + +lemma Int_assoc: "(A \ B) \ C = A \ (B \ C)" + by blast + +lemmas Int_ac = Int_assoc Int_left_absorb Int_commute Int_left_commute + -- {* Intersection is an AC-operator *} + +lemma Int_absorb1: "B \ A ==> A \ B = B" + by blast + +lemma Int_absorb2: "A \ B ==> A \ B = A" + by blast + +lemma Int_empty_left [simp]: "{} \ B = {}" + by blast + +lemma Int_empty_right [simp]: "A \ {} = {}" + by blast + +lemma disjoint_eq_subset_Compl: "(A \ B = {}) = (A \ -B)" + by blast + +lemma disjoint_iff_not_equal: "(A \ B = {}) = (\x\A. \y\B. x \ y)" + by blast + +lemma Int_UNIV_left [simp]: "UNIV \ B = B" + by blast + +lemma Int_UNIV_right [simp]: "A \ UNIV = A" + by blast + +lemma Int_eq_Inter: "A \ B = \{A, B}" + by blast + +lemma Int_Un_distrib: "A \ (B \ C) = (A \ B) \ (A \ C)" + by blast + +lemma Int_Un_distrib2: "(B \ C) \ A = (B \ A) \ (C \ A)" + by blast + +lemma Int_UNIV [simp]: "(A \ B = UNIV) = (A = UNIV & B = UNIV)" + by blast + +lemma Int_subset_iff: "(C \ A \ B) = (C \ A & C \ B)" + by blast + +lemma Int_Collect: "(x \ A \ {x. P x}) = (x \ A & P x)" + by blast + + +text {* \medskip @{text Un}. *} + +lemma Un_absorb [simp]: "A \ A = A" + by blast + +lemma Un_left_absorb: "A \ (A \ B) = A \ B" + by blast + +lemma Un_commute: "A \ B = B \ A" + by blast + +lemma Un_left_commute: "A \ (B \ C) = B \ (A \ C)" + by blast + +lemma Un_assoc: "(A \ B) \ C = A \ (B \ C)" + by blast + +lemmas Un_ac = Un_assoc Un_left_absorb Un_commute Un_left_commute + -- {* Union is an AC-operator *} + +lemma Un_absorb1: "A \ B ==> A \ B = B" + by blast + +lemma Un_absorb2: "B \ A ==> A \ B = A" + by blast + +lemma Un_empty_left [simp]: "{} \ B = B" + by blast + +lemma Un_empty_right [simp]: "A \ {} = A" + by blast + +lemma Un_UNIV_left [simp]: "UNIV \ B = UNIV" + by blast + +lemma Un_UNIV_right [simp]: "A \ UNIV = UNIV" + by blast + +lemma Un_eq_Union: "A \ B = \{A, B}" + by blast + +lemma Un_insert_left [simp]: "(insert a B) \ C = insert a (B \ C)" + by blast + +lemma Un_insert_right [simp]: "A \ (insert a B) = insert a (A \ B)" + by blast + +lemma Int_insert_left: + "(insert a B) Int C = (if a \ C then insert a (B \ C) else B \ C)" + by auto + +lemma Int_insert_right: + "A \ (insert a B) = (if a \ A then insert a (A \ B) else A \ B)" + by auto + +lemma Un_Int_distrib: "A \ (B \ C) = (A \ B) \ (A \ C)" + by blast + +lemma Un_Int_distrib2: "(B \ C) \ A = (B \ A) \ (C \ A)" + by blast + +lemma Un_Int_crazy: + "(A \ B) \ (B \ C) \ (C \ A) = (A \ B) \ (B \ C) \ (C \ A)" + by blast + +lemma subset_Un_eq: "(A \ B) = (A \ B = B)" + by blast + +lemma Un_empty [iff]: "(A \ B = {}) = (A = {} & B = {})" + by blast + +lemma Un_subset_iff: "(A \ B \ C) = (A \ C & B \ C)" + by blast + +lemma Un_Diff_Int: "(A - B) \ (A \ B) = A" + by blast + + +text {* \medskip Set complement *} + +lemma Compl_disjoint [simp]: "A \ -A = {}" + by blast + +lemma Compl_disjoint2 [simp]: "-A \ A = {}" + by blast + +lemma Compl_partition: "A \ (-A) = UNIV" + by blast + +lemma double_complement [simp]: "- (-A) = (A::'a set)" + by blast + +lemma Compl_Un [simp]: "-(A \ B) = (-A) \ (-B)" + by blast + +lemma Compl_Int [simp]: "-(A \ B) = (-A) \ (-B)" + by blast + +lemma Compl_UN [simp]: "-(\x\A. B x) = (\x\A. -B x)" + by blast + +lemma Compl_INT [simp]: "-(\x\A. B x) = (\x\A. -B x)" + by blast + +lemma subset_Compl_self_eq: "(A \ -A) = (A = {})" + by blast + +lemma Un_Int_assoc_eq: "((A \ B) \ C = A \ (B \ C)) = (C \ A)" + -- {* Halmos, Naive Set Theory, page 16. *} + by blast + +lemma Compl_UNIV_eq [simp]: "-UNIV = {}" + by blast + +lemma Compl_empty_eq [simp]: "-{} = UNIV" + by blast + +lemma Compl_subset_Compl_iff [iff]: "(-A \ -B) = (B \ A)" + by blast + +lemma Compl_eq_Compl_iff [iff]: "(-A = -B) = (A = (B::'a set))" + by blast + + +text {* \medskip @{text Union}. *} + +lemma Union_empty [simp]: "Union({}) = {}" + by blast + +lemma Union_UNIV [simp]: "Union UNIV = UNIV" + by blast + +lemma Union_insert [simp]: "Union (insert a B) = a \ \B" + by blast + +lemma Union_Un_distrib [simp]: "\(A Un B) = \A \ \B" + by blast + +lemma Union_Int_subset: "\(A \ B) \ \A \ \B" + by blast + +lemma Union_empty_conv [iff]: "(\A = {}) = (\x\A. x = {})" + by auto + +lemma Union_disjoint: "(\C \ A = {}) = (\B\C. B \ A = {})" + by blast + + +text {* \medskip @{text Inter}. *} + +lemma Inter_empty [simp]: "\{} = UNIV" + by blast + +lemma Inter_UNIV [simp]: "\UNIV = {}" + by blast + +lemma Inter_insert [simp]: "\(insert a B) = a \ \B" + by blast + +lemma Inter_Un_subset: "\A \ \B \ \(A \ B)" + by blast + +lemma Inter_Un_distrib: "\(A \ B) = \A \ \B" + by blast + + +text {* + \medskip @{text UN} and @{text INT}. + + Basic identities: *} + +lemma UN_empty [simp]: "(\x\{}. B x) = {}" + by blast + +lemma UN_empty2 [simp]: "(\x\A. {}) = {}" + by blast + +lemma UN_singleton [simp]: "(\x\A. {x}) = A" + by blast + +lemma UN_absorb: "k \ I ==> A k \ (\i\I. A i) = (\i\I. A i)" + by blast + +lemma INT_empty [simp]: "(\x\{}. B x) = UNIV" + by blast + +lemma INT_absorb: "k \ I ==> A k \ (\i\I. A i) = (\i\I. A i)" + by blast + +lemma UN_insert [simp]: "(\x\insert a A. B x) = B a \ UNION A B" + by blast + +lemma UN_Un: "(\i \ A \ B. M i) = (\i\A. M i) \ (\i\B. M i)" + by blast + +lemma UN_UN_flatten: "(\x \ (\y\A. B y). C x) = (\y\A. \x\B y. C x)" + by blast + +lemma UN_subset_iff: "((\i\I. A i) \ B) = (\i\I. A i \ B)" + by blast + +lemma INT_subset_iff: "(B \ (\i\I. A i)) = (\i\I. B \ A i)" + by blast + +lemma INT_insert [simp]: "(\x \ insert a A. B x) = B a \ INTER A B" + by blast + +lemma INT_Un: "(\i \ A \ B. M i) = (\i \ A. M i) \ (\i\B. M i)" + by blast + +lemma INT_insert_distrib: + "u \ A ==> (\x\A. insert a (B x)) = insert a (\x\A. B x)" + by blast + +lemma Union_image_eq [simp]: "\(B`A) = (\x\A. B x)" + by blast + +lemma image_Union: "f ` \S = (\x\S. f ` x)" + by blast + +lemma Inter_image_eq [simp]: "\(B`A) = (\x\A. B x)" + by blast + +lemma UN_constant [simp]: "(\y\A. c) = (if A = {} then {} else c)" + by auto + +lemma INT_constant [simp]: "(\y\A. c) = (if A = {} then UNIV else c)" + by auto + +lemma UN_eq: "(\x\A. B x) = \({Y. \x\A. Y = B x})" + by blast + +lemma INT_eq: "(\x\A. B x) = \({Y. \x\A. Y = B x})" + -- {* Look: it has an \emph{existential} quantifier *} + by blast + +lemma UN_empty3 [iff]: "(UNION A B = {}) = (\x\A. B x = {})" + by auto + + +text {* \medskip Distributive laws: *} + +lemma Int_Union: "A \ \B = (\C\B. A \ C)" + by blast + +lemma Int_Union2: "\B \ A = (\C\B. C \ A)" + by blast + +lemma Un_Union_image: "(\x\C. A x \ B x) = \(A`C) \ \(B`C)" + -- {* Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5: *} + -- {* Union of a family of unions *} + by blast + +lemma UN_Un_distrib: "(\i\I. A i \ B i) = (\i\I. A i) \ (\i\I. B i)" + -- {* Equivalent version *} + by blast + +lemma Un_Inter: "A \ \B = (\C\B. A \ C)" + by blast + +lemma Int_Inter_image: "(\x\C. A x \ B x) = \(A`C) \ \(B`C)" + by blast + +lemma INT_Int_distrib: "(\i\I. A i \ B i) = (\i\I. A i) \ (\i\I. B i)" + -- {* Equivalent version *} + by blast + +lemma Int_UN_distrib: "B \ (\i\I. A i) = (\i\I. B \ A i)" + -- {* Halmos, Naive Set Theory, page 35. *} + by blast + +lemma Un_INT_distrib: "B \ (\i\I. A i) = (\i\I. B \ A i)" + by blast + +lemma Int_UN_distrib2: "(\i\I. A i) \ (\j\J. B j) = (\i\I. \j\J. A i \ B j)" + by blast + +lemma Un_INT_distrib2: "(\i\I. A i) \ (\j\J. B j) = (\i\I. \j\J. A i \ B j)" + by blast + + +text {* \medskip Bounded quantifiers. + + The following are not added to the default simpset because + (a) they duplicate the body and (b) there are no similar rules for @{text Int}. *} + +lemma ball_Un: "(\x \ A \ B. P x) = ((\x\A. P x) & (\x\B. P x))" + by blast + +lemma bex_Un: "(\x \ A \ B. P x) = ((\x\A. P x) | (\x\B. P x))" + by blast + +lemma ball_UN: "(\z \ UNION A B. P z) = (\x\A. \z \ B x. P z)" + by blast + +lemma bex_UN: "(\z \ UNION A B. P z) = (\x\A. \z\B x. P z)" + by blast + + +text {* \medskip Set difference. *} + +lemma Diff_eq: "A - B = A \ (-B)" + by blast + +lemma Diff_eq_empty_iff [simp]: "(A - B = {}) = (A \ B)" + by blast + +lemma Diff_cancel [simp]: "A - A = {}" + by blast + +lemma Diff_triv: "A \ B = {} ==> A - B = A" + by (blast elim: equalityE) + +lemma empty_Diff [simp]: "{} - A = {}" + by blast + +lemma Diff_empty [simp]: "A - {} = A" + by blast + +lemma Diff_UNIV [simp]: "A - UNIV = {}" + by blast + +lemma Diff_insert0 [simp]: "x \ A ==> A - insert x B = A - B" + by blast + +lemma Diff_insert: "A - insert a B = A - B - {a}" + -- {* NOT SUITABLE FOR REWRITING since @{text "{a} == insert a 0"} *} + by blast + +lemma Diff_insert2: "A - insert a B = A - {a} - B" + -- {* NOT SUITABLE FOR REWRITING since @{text "{a} == insert a 0"} *} + by blast + +lemma insert_Diff_if: "insert x A - B = (if x \ B then A - B else insert x (A - B))" + by auto + +lemma insert_Diff1 [simp]: "x \ B ==> insert x A - B = A - B" + by blast + +lemma insert_Diff: "a \ A ==> insert a (A - {a}) = A" + by blast + +lemma Diff_insert_absorb: "x \ A ==> (insert x A) - {x} = A" + by auto + +lemma Diff_disjoint [simp]: "A \ (B - A) = {}" + by blast + +lemma Diff_partition: "A \ B ==> A \ (B - A) = B" + by blast + +lemma double_diff: "A \ B ==> B \ C ==> B - (C - A) = A" + by blast + +lemma Un_Diff_cancel [simp]: "A \ (B - A) = A \ B" + by blast + +lemma Un_Diff_cancel2 [simp]: "(B - A) \ A = B \ A" + by blast + +lemma Diff_Un: "A - (B \ C) = (A - B) \ (A - C)" + by blast + +lemma Diff_Int: "A - (B \ C) = (A - B) \ (A - C)" + by blast + +lemma Un_Diff: "(A \ B) - C = (A - C) \ (B - C)" + by blast + +lemma Int_Diff: "(A \ B) - C = A \ (B - C)" + by blast + +lemma Diff_Int_distrib: "C \ (A - B) = (C \ A) - (C \ B)" + by blast + +lemma Diff_Int_distrib2: "(A - B) \ C = (A \ C) - (B \ C)" + by blast + +lemma Diff_Compl [simp]: "A - (- B) = A \ B" + by auto + +lemma Compl_Diff_eq [simp]: "- (A - B) = -A \ B" + by blast + + +text {* \medskip Quantification over type @{typ bool}. *} + +lemma all_bool_eq: "(\b::bool. P b) = (P True & P False)" + apply auto + apply (tactic {* case_tac "b" 1 *}) + apply auto + done + +lemma bool_induct: "P True \ P False \ P x" + by (rule conjI [THEN all_bool_eq [THEN iffD2], THEN spec]) + +lemma ex_bool_eq: "(\b::bool. P b) = (P True | P False)" + apply auto + apply (tactic {* case_tac "b" 1 *}) + apply auto + done + +lemma Un_eq_UN: "A \ B = (\b. if b then A else B)" + by (auto simp add: split_if_mem2) + +lemma UN_bool_eq: "(\b::bool. A b) = (A True \ A False)" + apply auto + apply (tactic {* case_tac "b" 1 *}) + apply auto + done + +lemma INT_bool_eq: "(\b::bool. A b) = (A True \ A False)" + apply auto + apply (tactic {* case_tac "b" 1 *}) + apply auto + done + + +text {* \medskip @{text Pow} *} + +lemma Pow_empty [simp]: "Pow {} = {{}}" + by (auto simp add: Pow_def) + +lemma Pow_insert: "Pow (insert a A) = Pow A \ (insert a ` Pow A)" + by (blast intro: image_eqI [where ?x = "u - {a}", standard]) + +lemma Pow_Compl: "Pow (- A) = {-B | B. A \ Pow B}" + by (blast intro: exI [where ?x = "- u", standard]) + +lemma Pow_UNIV [simp]: "Pow UNIV = UNIV" + by blast + +lemma Un_Pow_subset: "Pow A \ Pow B \ Pow (A \ B)" + by blast + +lemma UN_Pow_subset: "(\x\A. Pow (B x)) \ Pow (\x\A. B x)" + by blast + +lemma subset_Pow_Union: "A \ Pow (\A)" + by blast + +lemma Union_Pow_eq [simp]: "\(Pow A) = A" + by blast + +lemma Pow_Int_eq [simp]: "Pow (A \ B) = Pow A \ Pow B" + by blast + +lemma Pow_INT_eq: "Pow (\x\A. B x) = (\x\A. Pow (B x))" + by blast + + +text {* \medskip Miscellany. *} + +lemma set_eq_subset: "(A = B) = (A \ B & B \ A)" + by blast + +lemma subset_iff: "(A \ B) = (\t. t \ A --> t \ B)" + by blast + +lemma subset_iff_psubset_eq: "(A \ B) = ((A \ B) | (A = B))" + by (unfold psubset_def) blast + +lemma all_not_in_conv [iff]: "(\x. x \ A) = (A = {})" + by blast + +lemma distinct_lemma: "f x \ f y ==> x \ y" + by rules + + +text {* \medskip Miniscoping: pushing in big Unions and Intersections. *} + +lemma UN_simps [simp]: + "!!a B C. (UN x:C. insert a (B x)) = (if C={} then {} else insert a (UN x:C. B x))" + "!!A B C. (UN x:C. A x Un B) = ((if C={} then {} else (UN x:C. A x) Un B))" + "!!A B C. (UN x:C. A Un B x) = ((if C={} then {} else A Un (UN x:C. B x)))" + "!!A B C. (UN x:C. A x Int B) = ((UN x:C. A x) Int B)" + "!!A B C. (UN x:C. A Int B x) = (A Int (UN x:C. B x))" + "!!A B C. (UN x:C. A x - B) = ((UN x:C. A x) - B)" + "!!A B C. (UN x:C. A - B x) = (A - (INT x:C. B x))" + "!!A B. (UN x: Union A. B x) = (UN y:A. UN x:y. B x)" + "!!A B C. (UN z: UNION A B. C z) = (UN x:A. UN z: B(x). C z)" + "!!A B f. (UN x:f`A. B x) = (UN a:A. B (f a))" + by auto + +lemma INT_simps [simp]: + "!!A B C. (INT x:C. A x Int B) = (if C={} then UNIV else (INT x:C. A x) Int B)" + "!!A B C. (INT x:C. A Int B x) = (if C={} then UNIV else A Int (INT x:C. B x))" + "!!A B C. (INT x:C. A x - B) = (if C={} then UNIV else (INT x:C. A x) - B)" + "!!A B C. (INT x:C. A - B x) = (if C={} then UNIV else A - (UN x:C. B x))" + "!!a B C. (INT x:C. insert a (B x)) = insert a (INT x:C. B x)" + "!!A B C. (INT x:C. A x Un B) = ((INT x:C. A x) Un B)" + "!!A B C. (INT x:C. A Un B x) = (A Un (INT x:C. B x))" + "!!A B. (INT x: Union A. B x) = (INT y:A. INT x:y. B x)" + "!!A B C. (INT z: UNION A B. C z) = (INT x:A. INT z: B(x). C z)" + "!!A B f. (INT x:f`A. B x) = (INT a:A. B (f a))" + by auto + +lemma ball_simps [simp]: + "!!A P Q. (ALL x:A. P x | Q) = ((ALL x:A. P x) | Q)" + "!!A P Q. (ALL x:A. P | Q x) = (P | (ALL x:A. Q x))" + "!!A P Q. (ALL x:A. P --> Q x) = (P --> (ALL x:A. Q x))" + "!!A P Q. (ALL x:A. P x --> Q) = ((EX x:A. P x) --> Q)" + "!!P. (ALL x:{}. P x) = True" + "!!P. (ALL x:UNIV. P x) = (ALL x. P x)" + "!!a B P. (ALL x:insert a B. P x) = (P a & (ALL x:B. P x))" + "!!A P. (ALL x:Union A. P x) = (ALL y:A. ALL x:y. P x)" + "!!A B P. (ALL x: UNION A B. P x) = (ALL a:A. ALL x: B a. P x)" + "!!P Q. (ALL x:Collect Q. P x) = (ALL x. Q x --> P x)" + "!!A P f. (ALL x:f`A. P x) = (ALL x:A. P (f x))" + "!!A P. (~(ALL x:A. P x)) = (EX x:A. ~P x)" + by auto + +lemma bex_simps [simp]: + "!!A P Q. (EX x:A. P x & Q) = ((EX x:A. P x) & Q)" + "!!A P Q. (EX x:A. P & Q x) = (P & (EX x:A. Q x))" + "!!P. (EX x:{}. P x) = False" + "!!P. (EX x:UNIV. P x) = (EX x. P x)" + "!!a B P. (EX x:insert a B. P x) = (P(a) | (EX x:B. P x))" + "!!A P. (EX x:Union A. P x) = (EX y:A. EX x:y. P x)" + "!!A B P. (EX x: UNION A B. P x) = (EX a:A. EX x:B a. P x)" + "!!P Q. (EX x:Collect Q. P x) = (EX x. Q x & P x)" + "!!A P f. (EX x:f`A. P x) = (EX x:A. P (f x))" + "!!A P. (~(EX x:A. P x)) = (ALL x:A. ~P x)" + by auto + +lemma ball_conj_distrib: + "(ALL x:A. P x & Q x) = ((ALL x:A. P x) & (ALL x:A. Q x))" + by blast + +lemma bex_disj_distrib: + "(EX x:A. P x | Q x) = ((EX x:A. P x) | (EX x:A. Q x))" + by blast + + +subsubsection {* Monotonicity of various operations *} + +lemma image_mono: "A \ B ==> f`A \ f`B" + by blast + +lemma Pow_mono: "A \ B ==> Pow A \ Pow B" + by blast + +lemma Union_mono: "A \ B ==> \A \ \B" + by blast + +lemma Inter_anti_mono: "B \ A ==> \A \ \B" + by blast + +lemma UN_mono: + "A \ B ==> (!!x. x \ A ==> f x \ g x) ==> + (\x\A. f x) \ (\x\B. g x)" + by (blast dest: subsetD) + +lemma INT_anti_mono: + "B \ A ==> (!!x. x \ A ==> f x \ g x) ==> + (\x\A. f x) \ (\x\A. g x)" + -- {* The last inclusion is POSITIVE! *} + by (blast dest: subsetD) + +lemma insert_mono: "C \ D ==> insert a C \ insert a D" + by blast + +lemma Un_mono: "A \ C ==> B \ D ==> A \ B \ C \ D" + by blast + +lemma Int_mono: "A \ C ==> B \ D ==> A \ B \ C \ D" + by blast + +lemma Diff_mono: "A \ C ==> D \ B ==> A - B \ C - D" + by blast + +lemma Compl_anti_mono: "A \ B ==> -B \ -A" + by blast + +text {* \medskip Monotonicity of implications. *} + +lemma in_mono: "A \ B ==> x \ A --> x \ B" + apply (rule impI) + apply (erule subsetD) + apply assumption + done + +lemma conj_mono: "P1 --> Q1 ==> P2 --> Q2 ==> (P1 & P2) --> (Q1 & Q2)" + by rules + +lemma disj_mono: "P1 --> Q1 ==> P2 --> Q2 ==> (P1 | P2) --> (Q1 | Q2)" + by rules + +lemma imp_mono: "Q1 --> P1 ==> P2 --> Q2 ==> (P1 --> P2) --> (Q1 --> Q2)" + by rules + +lemma imp_refl: "P --> P" .. + +lemma ex_mono: "(!!x. P x --> Q x) ==> (EX x. P x) --> (EX x. Q x)" + by rules + +lemma all_mono: "(!!x. P x --> Q x) ==> (ALL x. P x) --> (ALL x. Q x)" + by rules + +lemma Collect_mono: "(!!x. P x --> Q x) ==> Collect P \ Collect Q" + by blast + +lemma Int_Collect_mono: + "A \ B ==> (!!x. x \ A ==> P x --> Q x) ==> A \ Collect P \ B \ Collect Q" + by blast + +lemmas basic_monos = + subset_refl imp_refl disj_mono conj_mono + ex_mono Collect_mono in_mono + +lemma eq_to_mono: "a = b ==> c = d ==> b --> d ==> a --> c" + by rules + +lemma eq_to_mono2: "a = b ==> c = d ==> ~ b --> ~ d ==> ~ a --> ~ c" + by rules lemma Least_mono: "mono (f::'a::order => 'b::order) ==> EX x:S. ALL y:S. x <= y @@ -972,7 +1858,7 @@ -- {* NOT suitable for rewriting *} by blast -lemma vimage_mono: "A <= B ==> f -` A <= f -` B" +lemma vimage_mono: "A \ B ==> f -` A \ f -` B" -- {* monotonicity *} by blast @@ -985,10 +1871,10 @@ lemma back_subst: "P a ==> a = b ==> P b" by (rule subst) -lemma set_rev_mp: "x:A ==> A <= B ==> x:B" +lemma set_rev_mp: "x:A ==> A \ B ==> x:B" by (rule subsetD) -lemma set_mp: "A <= B ==> x:A ==> x:B" +lemma set_mp: "A \ B ==> x:A ==> x:B" by (rule subsetD) lemma order_neq_le_trans: "a ~= b ==> (a::'a::order) <= b ==> a < b" diff -r 4518acda6d93 -r f4d10ad0ea7b src/HOL/equalities.ML --- a/src/HOL/equalities.ML Fri Feb 15 20:43:44 2002 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,982 +0,0 @@ -(* Title: HOL/equalities.ML - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1994 University of Cambridge - -Equalities involving union, intersection, inclusion, etc. -*) - -AddSIs [equalityI]; - -section "{}"; - -(*supersedes Collect_False_empty*) -Goal "{s. P} = (if P then UNIV else {})"; -by (Force_tac 1); -qed "Collect_const"; -Addsimps [Collect_const]; - -Goal "(A <= {}) = (A = {})"; -by (Blast_tac 1); -qed "subset_empty"; -Addsimps[subset_empty]; - -Goalw [psubset_def] "~ (A < {})"; -by (Blast_tac 1); -qed "not_psubset_empty"; -AddIffs [not_psubset_empty]; - -Goal "(Collect P = {}) = (ALL x. ~ P x)"; -by Auto_tac; -qed "Collect_empty_eq"; -Addsimps[Collect_empty_eq]; - -Goal "{x. ~ (P x)} = - {x. P x}"; -by (Blast_tac 1); -qed "Collect_neg_eq"; - -Goal "{x. P x | Q x} = {x. P x} Un {x. Q x}"; -by (Blast_tac 1); -qed "Collect_disj_eq"; - -Goal "{x. P x & Q x} = {x. P x} Int {x. Q x}"; -by (Blast_tac 1); -qed "Collect_conj_eq"; - -Goal "{x. ALL y. P x y} = (INT y. {x. P x y})"; -by (Blast_tac 1); -qed "Collect_all_eq"; - -Goal "{x. ALL y: A. P x y} = (INT y: A. {x. P x y})"; -by (Blast_tac 1); -qed "Collect_ball_eq"; - -Goal "{x. EX y. P x y} = (UN y. {x. P x y})"; -by (Blast_tac 1); -qed "Collect_ex_eq"; - -Goal "{x. EX y: A. P x y} = (UN y: A. {x. P x y})"; -by (Blast_tac 1); -qed "Collect_bex_eq"; - - -section "insert"; - -(*NOT SUITABLE FOR REWRITING since {a} == insert a {}*) -Goal "insert a A = {a} Un A"; -by (Blast_tac 1); -qed "insert_is_Un"; - -Goal "insert a A ~= {}"; -by (Blast_tac 1); -qed"insert_not_empty"; -Addsimps[insert_not_empty]; - -bind_thm("empty_not_insert",insert_not_empty RS not_sym); -Addsimps[empty_not_insert]; - -Goal "a:A ==> insert a A = A"; -by (Blast_tac 1); -qed "insert_absorb"; -(* Addsimps [insert_absorb] causes recursive calls - when there are nested inserts, with QUADRATIC running time -*) - -Goal "insert x (insert x A) = insert x A"; -by (Blast_tac 1); -qed "insert_absorb2"; -Addsimps [insert_absorb2]; - -Goal "insert x (insert y A) = insert y (insert x A)"; -by (Blast_tac 1); -qed "insert_commute"; - -Goal "(insert x A <= B) = (x:B & A <= B)"; -by (Blast_tac 1); -qed "insert_subset"; -Addsimps[insert_subset]; - -(* use new B rather than (A-{a}) to avoid infinite unfolding *) -Goal "a:A ==> EX B. A = insert a B & a ~: B"; -by (res_inst_tac [("x","A-{a}")] exI 1); -by (Blast_tac 1); -qed "mk_disjoint_insert"; - -Goal "insert a (Collect P) = {u. u ~= a --> P u}"; -by Auto_tac; -qed "insert_Collect"; - -Goal "u: A ==> (UN x:A. insert a (B x)) = insert a (UN x:A. B x)"; -by (Blast_tac 1); -qed "UN_insert_distrib"; - -section "`"; - -Goal "f`{} = {}"; -by (Blast_tac 1); -qed "image_empty"; -Addsimps[image_empty]; - -Goal "f`insert a B = insert (f a) (f`B)"; -by (Blast_tac 1); -qed "image_insert"; -Addsimps[image_insert]; - -Goal "x:A ==> (%x. c) ` A = {c}"; -by (Blast_tac 1); -qed "image_constant"; - -Goal "f`(g`A) = (%x. f (g x)) ` A"; -by (Blast_tac 1); -qed "image_image"; - -Goal "x:A ==> insert (f x) (f`A) = f`A"; -by (Blast_tac 1); -qed "insert_image"; -Addsimps [insert_image]; - -Goal "(f`A = {}) = (A = {})"; -by (Blast_tac 1); -qed "image_is_empty"; -AddIffs [image_is_empty]; - -(*NOT suitable as a default simprule: the RHS isn't simpler than the LHS, - with its implicit quantifier and conjunction. Also image enjoys better - equational properties than does the RHS.*) -Goal "f ` {x. P x} = {f x | x. P x}"; -by (Blast_tac 1); -qed "image_Collect"; - -Goalw [image_def] "(%x. if P x then f x else g x) ` S \ -\ = (f ` (S Int {x. P x})) Un (g ` (S Int {x. ~(P x)}))"; -by (Simp_tac 1); -by (Blast_tac 1); -qed "if_image_distrib"; -Addsimps[if_image_distrib]; - -val prems = Goal "[|M = N; !!x. x:N ==> f x = g x|] ==> f`M = g`N"; -by (simp_tac (simpset() addsimps image_def::prems) 1); -qed "image_cong"; - - -section "range"; - -Goal "{u. EX x. u = f x} = range f"; -by Auto_tac; -qed "full_SetCompr_eq"; - -Goal "range (%x. f (g x)) = f`range g"; -by (stac image_image 1); -by (Simp_tac 1); -qed "range_composition"; -Addsimps[range_composition]; - -section "Int"; - -Goal "A Int A = A"; -by (Blast_tac 1); -qed "Int_absorb"; -Addsimps[Int_absorb]; - -Goal "A Int (A Int B) = A Int B"; -by (Blast_tac 1); -qed "Int_left_absorb"; - -Goal "A Int B = B Int A"; -by (Blast_tac 1); -qed "Int_commute"; - -Goal "A Int (B Int C) = B Int (A Int C)"; -by (Blast_tac 1); -qed "Int_left_commute"; - -Goal "(A Int B) Int C = A Int (B Int C)"; -by (Blast_tac 1); -qed "Int_assoc"; - -(*Intersection is an AC-operator*) -bind_thms ("Int_ac", [Int_assoc, Int_left_absorb, Int_commute, Int_left_commute]); - -Goal "B<=A ==> A Int B = B"; -by (Blast_tac 1); -qed "Int_absorb1"; - -Goal "A<=B ==> A Int B = A"; -by (Blast_tac 1); -qed "Int_absorb2"; - -Goal "{} Int B = {}"; -by (Blast_tac 1); -qed "Int_empty_left"; -Addsimps[Int_empty_left]; - -Goal "A Int {} = {}"; -by (Blast_tac 1); -qed "Int_empty_right"; -Addsimps[Int_empty_right]; - -Goal "(A Int B = {}) = (A <= -B)"; -by (Blast_tac 1); -qed "disjoint_eq_subset_Compl"; - -Goal "(A Int B = {}) = (ALL x:A. ALL y:B. x ~= y)"; -by (Blast_tac 1); -qed "disjoint_iff_not_equal"; - -Goal "UNIV Int B = B"; -by (Blast_tac 1); -qed "Int_UNIV_left"; -Addsimps[Int_UNIV_left]; - -Goal "A Int UNIV = A"; -by (Blast_tac 1); -qed "Int_UNIV_right"; -Addsimps[Int_UNIV_right]; - -Goal "A Int B = Inter{A,B}"; -by (Blast_tac 1); -qed "Int_eq_Inter"; - -Goal "A Int (B Un C) = (A Int B) Un (A Int C)"; -by (Blast_tac 1); -qed "Int_Un_distrib"; - -Goal "(B Un C) Int A = (B Int A) Un (C Int A)"; -by (Blast_tac 1); -qed "Int_Un_distrib2"; - -Goal "(A Int B = UNIV) = (A = UNIV & B = UNIV)"; -by (Blast_tac 1); -qed "Int_UNIV"; -Addsimps[Int_UNIV]; - -Goal "(C <= A Int B) = (C <= A & C <= B)"; -by (Blast_tac 1); -qed "Int_subset_iff"; - -Goal "(x : A Int {x. P x}) = (x : A & P x)"; -by (Blast_tac 1); -qed "Int_Collect"; - -section "Un"; - -Goal "A Un A = A"; -by (Blast_tac 1); -qed "Un_absorb"; -Addsimps[Un_absorb]; - -Goal "A Un (A Un B) = A Un B"; -by (Blast_tac 1); -qed "Un_left_absorb"; - -Goal "A Un B = B Un A"; -by (Blast_tac 1); -qed "Un_commute"; - -Goal "A Un (B Un C) = B Un (A Un C)"; -by (Blast_tac 1); -qed "Un_left_commute"; - -Goal "(A Un B) Un C = A Un (B Un C)"; -by (Blast_tac 1); -qed "Un_assoc"; - -(*Union is an AC-operator*) -bind_thms ("Un_ac", [Un_assoc, Un_left_absorb, Un_commute, Un_left_commute]); - -Goal "A<=B ==> A Un B = B"; -by (Blast_tac 1); -qed "Un_absorb1"; - -Goal "B<=A ==> A Un B = A"; -by (Blast_tac 1); -qed "Un_absorb2"; - -Goal "{} Un B = B"; -by (Blast_tac 1); -qed "Un_empty_left"; -Addsimps[Un_empty_left]; - -Goal "A Un {} = A"; -by (Blast_tac 1); -qed "Un_empty_right"; -Addsimps[Un_empty_right]; - -Goal "UNIV Un B = UNIV"; -by (Blast_tac 1); -qed "Un_UNIV_left"; -Addsimps[Un_UNIV_left]; - -Goal "A Un UNIV = UNIV"; -by (Blast_tac 1); -qed "Un_UNIV_right"; -Addsimps[Un_UNIV_right]; - -Goal "A Un B = Union{A,B}"; -by (Blast_tac 1); -qed "Un_eq_Union"; - -Goal "(insert a B) Un C = insert a (B Un C)"; -by (Blast_tac 1); -qed "Un_insert_left"; -Addsimps[Un_insert_left]; - -Goal "A Un (insert a B) = insert a (A Un B)"; -by (Blast_tac 1); -qed "Un_insert_right"; -Addsimps[Un_insert_right]; - -Goal "(insert a B) Int C = (if a:C then insert a (B Int C) \ -\ else B Int C)"; -by (Simp_tac 1); -by (Blast_tac 1); -qed "Int_insert_left"; - -Goal "A Int (insert a B) = (if a:A then insert a (A Int B) \ -\ else A Int B)"; -by (Simp_tac 1); -by (Blast_tac 1); -qed "Int_insert_right"; - -Goal "A Un (B Int C) = (A Un B) Int (A Un C)"; -by (Blast_tac 1); -qed "Un_Int_distrib"; - -Goal "(B Int C) Un A = (B Un A) Int (C Un A)"; -by (Blast_tac 1); -qed "Un_Int_distrib2"; - -Goal "(A Int B) Un (B Int C) Un (C Int A) = \ -\ (A Un B) Int (B Un C) Int (C Un A)"; -by (Blast_tac 1); -qed "Un_Int_crazy"; - -Goal "(A<=B) = (A Un B = B)"; -by (Blast_tac 1); -qed "subset_Un_eq"; - -Goal "(A Un B = {}) = (A = {} & B = {})"; -by (Blast_tac 1); -qed "Un_empty"; -AddIffs[Un_empty]; - -Goal "(A Un B <= C) = (A <= C & B <= C)"; -by (Blast_tac 1); -qed "Un_subset_iff"; - -Goal "(A - B) Un (A Int B) = A"; -by (Blast_tac 1); -qed "Un_Diff_Int"; - - -section "Set complement"; - -Goal "A Int -A = {}"; -by (Blast_tac 1); -qed "Compl_disjoint"; - -Goal "-A Int A = {}"; -by (Blast_tac 1); -qed "Compl_disjoint2"; -Addsimps[Compl_disjoint, Compl_disjoint2]; - -Goal "A Un (-A) = UNIV"; -by (Blast_tac 1); -qed "Compl_partition"; - -Goal "- (-A) = (A:: 'a set)"; -by (Blast_tac 1); -qed "double_complement"; -Addsimps[double_complement]; - -Goal "-(A Un B) = (-A) Int (-B)"; -by (Blast_tac 1); -qed "Compl_Un"; - -Goal "-(A Int B) = (-A) Un (-B)"; -by (Blast_tac 1); -qed "Compl_Int"; - -Goal "-(UN x:A. B(x)) = (INT x:A. -B(x))"; -by (Blast_tac 1); -qed "Compl_UN"; - -Goal "-(INT x:A. B(x)) = (UN x:A. -B(x))"; -by (Blast_tac 1); -qed "Compl_INT"; - -Addsimps [Compl_Un, Compl_Int, Compl_UN, Compl_INT]; - -Goal "(A <= -A) = (A = {})"; -by (Blast_tac 1); -qed "subset_Compl_self_eq"; - -(*Halmos, Naive Set Theory, page 16.*) -Goal "((A Int B) Un C = A Int (B Un C)) = (C<=A)"; -by (Blast_tac 1); -qed "Un_Int_assoc_eq"; - -Goal "-UNIV = {}"; -by (Blast_tac 1); -qed "Compl_UNIV_eq"; - -Goal "-{} = UNIV"; -by (Blast_tac 1); -qed "Compl_empty_eq"; - -Addsimps [Compl_UNIV_eq, Compl_empty_eq]; - -Goal "(-A <= -B) = (B <= (A::'a set))"; -by (Blast_tac 1); -qed "Compl_subset_Compl_iff"; -AddIffs [Compl_subset_Compl_iff]; - -Goal "(-A = -B) = (A = (B::'a set))"; -by (Blast_tac 1); -qed "Compl_eq_Compl_iff"; -AddIffs [Compl_eq_Compl_iff]; - - -section "Union"; - -Goal "Union({}) = {}"; -by (Blast_tac 1); -qed "Union_empty"; -Addsimps[Union_empty]; - -Goal "Union(UNIV) = UNIV"; -by (Blast_tac 1); -qed "Union_UNIV"; -Addsimps[Union_UNIV]; - -Goal "Union(insert a B) = a Un Union(B)"; -by (Blast_tac 1); -qed "Union_insert"; -Addsimps[Union_insert]; - -Goal "Union(A Un B) = Union(A) Un Union(B)"; -by (Blast_tac 1); -qed "Union_Un_distrib"; -Addsimps[Union_Un_distrib]; - -Goal "Union(A Int B) <= Union(A) Int Union(B)"; -by (Blast_tac 1); -qed "Union_Int_subset"; - -Goal "(Union A = {}) = (ALL x:A. x={})"; -by Auto_tac; -qed "Union_empty_conv"; -AddIffs [Union_empty_conv]; - -Goal "(Union(C) Int A = {}) = (ALL B:C. B Int A = {})"; -by (Blast_tac 1); -qed "Union_disjoint"; - -section "Inter"; - -Goal "Inter({}) = UNIV"; -by (Blast_tac 1); -qed "Inter_empty"; -Addsimps[Inter_empty]; - -Goal "Inter(UNIV) = {}"; -by (Blast_tac 1); -qed "Inter_UNIV"; -Addsimps[Inter_UNIV]; - -Goal "Inter(insert a B) = a Int Inter(B)"; -by (Blast_tac 1); -qed "Inter_insert"; -Addsimps[Inter_insert]; - -Goal "Inter(A) Un Inter(B) <= Inter(A Int B)"; -by (Blast_tac 1); -qed "Inter_Un_subset"; - -Goal "Inter(A Un B) = Inter(A) Int Inter(B)"; -by (Blast_tac 1); -qed "Inter_Un_distrib"; - -section "UN and INT"; - -(*Basic identities*) - -Goal "(UN x:{}. B x) = {}"; -by (Blast_tac 1); -qed "UN_empty"; -Addsimps[UN_empty]; - -Goal "(UN x:A. {}) = {}"; -by (Blast_tac 1); -qed "UN_empty2"; -Addsimps[UN_empty2]; - -Goal "(UN x:A. {x}) = A"; -by (Blast_tac 1); -qed "UN_singleton"; -Addsimps [UN_singleton]; - -Goal "k:I ==> A k Un (UN i:I. A i) = (UN i:I. A i)"; -by (Blast_tac 1); -qed "UN_absorb"; - -Goal "(INT x:{}. B x) = UNIV"; -by (Blast_tac 1); -qed "INT_empty"; -Addsimps[INT_empty]; - -Goal "k:I ==> A k Int (INT i:I. A i) = (INT i:I. A i)"; -by (Blast_tac 1); -qed "INT_absorb"; - -Goal "(UN x:insert a A. B x) = B a Un UNION A B"; -by (Blast_tac 1); -qed "UN_insert"; -Addsimps[UN_insert]; - -Goal "(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 "(UN x : (UN y:A. B y). C x) = (UN y:A. UN x: B y. C x)"; -by (Blast_tac 1); -qed "UN_UN_flatten"; - -Goal "((UN i:I. A i) <= B) = (ALL i:I. A i <= B)"; -by (Blast_tac 1); -qed "UN_subset_iff"; - -Goal "(B <= (INT i:I. A i)) = (ALL i:I. B <= A i)"; -by (Blast_tac 1); -qed "INT_subset_iff"; - -Goal "(INT x:insert a A. B x) = B a Int INTER A B"; -by (Blast_tac 1); -qed "INT_insert"; -Addsimps[INT_insert]; - -Goal "(INT i: A Un B. M i) = (INT i: A. M i) Int (INT i:B. M i)"; -by (Blast_tac 1); -qed "INT_Un"; - -Goal "u: A ==> (INT x:A. insert a (B x)) = insert a (INT x:A. B x)"; -by (Blast_tac 1); -qed "INT_insert_distrib"; - -Goal "Union(B`A) = (UN x:A. B(x))"; -by (Blast_tac 1); -qed "Union_image_eq"; -Addsimps [Union_image_eq]; - -Goal "f ` Union S = (UN x:S. f ` x)"; -by (Blast_tac 1); -qed "image_Union"; - -Goal "Inter(B`A) = (INT x:A. B(x))"; -by (Blast_tac 1); -qed "Inter_image_eq"; -Addsimps [Inter_image_eq]; - -Goal "(UN y:A. c) = (if A={} then {} else c)"; -by Auto_tac; -qed "UN_constant"; -Addsimps[UN_constant]; - -Goal "(INT y:A. c) = (if A={} then UNIV else c)"; -by Auto_tac; -qed "INT_constant"; -Addsimps[INT_constant]; - -Goal "(UN x:A. B(x)) = Union({Y. EX x:A. Y=B(x)})"; -by (Blast_tac 1); -qed "UN_eq"; - -(*Look: it has an EXISTENTIAL quantifier*) -Goal "(INT x:A. B(x)) = Inter({Y. EX x:A. Y=B(x)})"; -by (Blast_tac 1); -qed "INT_eq"; - -Goal "(UNION A B = {}) = (ALL x:A. B x = {})"; -by Auto_tac; -qed "UN_empty3"; -AddIffs [UN_empty3]; - - -(*Distributive laws...*) - -Goal "A Int Union(B) = (UN C:B. A Int C)"; -by (Blast_tac 1); -qed "Int_Union"; - -Goal "Union(B) Int A = (UN C:B. C Int A)"; -by (Blast_tac 1); -qed "Int_Union2"; - -(* Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5: - Union of a family of unions **) -Goal "(UN x:C. A(x) Un B(x)) = Union(A`C) Un Union(B`C)"; -by (Blast_tac 1); -qed "Un_Union_image"; - -(*Equivalent version*) -Goal "(UN i:I. A(i) Un B(i)) = (UN i:I. A(i)) Un (UN i:I. B(i))"; -by (Blast_tac 1); -qed "UN_Un_distrib"; - -Goal "A Un Inter(B) = (INT C:B. A Un C)"; -by (Blast_tac 1); -qed "Un_Inter"; - -Goal "(INT x:C. A(x) Int B(x)) = Inter(A`C) Int Inter(B`C)"; -by (Blast_tac 1); -qed "Int_Inter_image"; - -(*Equivalent version*) -Goal "(INT i:I. A(i) Int B(i)) = (INT i:I. A(i)) Int (INT i:I. B(i))"; -by (Blast_tac 1); -qed "INT_Int_distrib"; - -(*Halmos, Naive Set Theory, page 35.*) -Goal "B Int (UN i:I. A(i)) = (UN i:I. B Int A(i))"; -by (Blast_tac 1); -qed "Int_UN_distrib"; - -Goal "B Un (INT i:I. A(i)) = (INT i:I. B Un A(i))"; -by (Blast_tac 1); -qed "Un_INT_distrib"; - -Goal "(UN i:I. A(i)) Int (UN j:J. B(j)) = (UN i:I. UN j:J. A(i) Int B(j))"; -by (Blast_tac 1); -qed "Int_UN_distrib2"; - -Goal "(INT i:I. A(i)) Un (INT j:J. B(j)) = (INT i:I. INT j:J. A(i) Un B(j))"; -by (Blast_tac 1); -qed "Un_INT_distrib2"; - - -section"Bounded quantifiers"; - -(** The following are not added to the default simpset because - (a) they duplicate the body and (b) there are no similar rules for Int. **) - -Goal "(ALL x:A Un B. P x) = ((ALL x:A. P x) & (ALL x:B. P x))"; -by (Blast_tac 1); -qed "ball_Un"; - -Goal "(EX x:A Un B. P x) = ((EX x:A. P x) | (EX x:B. P x))"; -by (Blast_tac 1); -qed "bex_Un"; - -Goal "(ALL z: UNION A B. P z) = (ALL x:A. ALL z:B x. P z)"; -by (Blast_tac 1); -qed "ball_UN"; - -Goal "(EX z: UNION A B. P z) = (EX x:A. EX z:B x. P z)"; -by (Blast_tac 1); -qed "bex_UN"; - - -section "-"; - -Goal "A-B = A Int (-B)"; -by (Blast_tac 1); -qed "Diff_eq"; - -Goal "(A-B = {}) = (A<=B)"; -by (Blast_tac 1); -qed "Diff_eq_empty_iff"; -Addsimps[Diff_eq_empty_iff]; - -Goal "A-A = {}"; -by (Blast_tac 1); -qed "Diff_cancel"; -Addsimps[Diff_cancel]; - -Goal "A Int B = {} ==> A-B = A"; -by (blast_tac (claset() addEs [equalityE]) 1); -qed "Diff_triv"; - -Goal "{}-A = {}"; -by (Blast_tac 1); -qed "empty_Diff"; -Addsimps[empty_Diff]; - -Goal "A-{} = A"; -by (Blast_tac 1); -qed "Diff_empty"; -Addsimps[Diff_empty]; - -Goal "A-UNIV = {}"; -by (Blast_tac 1); -qed "Diff_UNIV"; -Addsimps[Diff_UNIV]; - -Goal "x~:A ==> A - insert x B = A-B"; -by (Blast_tac 1); -qed "Diff_insert0"; -Addsimps [Diff_insert0]; - -(*NOT SUITABLE FOR REWRITING since {a} == insert a 0*) -Goal "A - insert a B = A - B - {a}"; -by (Blast_tac 1); -qed "Diff_insert"; - -(*NOT SUITABLE FOR REWRITING since {a} == insert a 0*) -Goal "A - insert a B = A - {a} - B"; -by (Blast_tac 1); -qed "Diff_insert2"; - -Goal "insert x A - B = (if x:B then A-B else insert x (A-B))"; -by (Simp_tac 1); -by (Blast_tac 1); -qed "insert_Diff_if"; - -Goal "x:B ==> insert x A - B = A-B"; -by (Blast_tac 1); -qed "insert_Diff1"; -Addsimps [insert_Diff1]; - -Goal "a:A ==> insert a (A-{a}) = A"; -by (Blast_tac 1); -qed "insert_Diff"; - -Goal "x ~: A ==> (insert x A) - {x} = A"; -by Auto_tac; -qed "Diff_insert_absorb"; - -Goal "A Int (B-A) = {}"; -by (Blast_tac 1); -qed "Diff_disjoint"; -Addsimps[Diff_disjoint]; - -Goal "A<=B ==> A Un (B-A) = B"; -by (Blast_tac 1); -qed "Diff_partition"; - -Goal "[| A<=B; B<= C |] ==> (B - (C - A)) = (A :: 'a set)"; -by (Blast_tac 1); -qed "double_diff"; - -Goal "A Un (B-A) = A Un B"; -by (Blast_tac 1); -qed "Un_Diff_cancel"; - -Goal "(B-A) Un A = B Un A"; -by (Blast_tac 1); -qed "Un_Diff_cancel2"; - -Addsimps [Un_Diff_cancel, Un_Diff_cancel2]; - -Goal "A - (B Un C) = (A-B) Int (A-C)"; -by (Blast_tac 1); -qed "Diff_Un"; - -Goal "A - (B Int C) = (A-B) Un (A-C)"; -by (Blast_tac 1); -qed "Diff_Int"; - -Goal "(A Un B) - C = (A - C) Un (B - C)"; -by (Blast_tac 1); -qed "Un_Diff"; - -Goal "(A Int B) - C = A Int (B - C)"; -by (Blast_tac 1); -qed "Int_Diff"; - -Goal "C Int (A-B) = (C Int A) - (C Int B)"; -by (Blast_tac 1); -qed "Diff_Int_distrib"; - -Goal "(A-B) Int C = (A Int C) - (B Int C)"; -by (Blast_tac 1); -qed "Diff_Int_distrib2"; - -Goal "A - (- B) = A Int B"; -by Auto_tac; -qed "Diff_Compl"; -Addsimps [Diff_Compl]; - -Goal "- (A-B) = -A Un B"; -by (blast_tac (claset() addIs []) 1); -qed "Compl_Diff_eq"; -Addsimps [Compl_Diff_eq]; - - -section "Quantification over type \"bool\""; - -Goal "(ALL b::bool. P b) = (P True & P False)"; -by Auto_tac; -by (case_tac "b" 1); -by Auto_tac; -qed "all_bool_eq"; - -bind_thm ("bool_induct", conjI RS (all_bool_eq RS iffD2) RS spec); - -Goal "(EX b::bool. P b) = (P True | P False)"; -by Auto_tac; -by (case_tac "b" 1); -by Auto_tac; -qed "ex_bool_eq"; - -Goal "A Un B = (UN b. if b then A else B)"; -by (auto_tac(claset(), simpset() addsimps [split_if_mem2])); -qed "Un_eq_UN"; - -Goal "(UN b::bool. A b) = (A True Un A False)"; -by Auto_tac; -by (case_tac "b" 1); -by Auto_tac; -qed "UN_bool_eq"; - -Goal "(INT b::bool. A b) = (A True Int A False)"; -by Auto_tac; -by (case_tac "b" 1); -by Auto_tac; -qed "INT_bool_eq"; - - -section "Pow"; - -Goalw [Pow_def] "Pow {} = {{}}"; -by Auto_tac; -qed "Pow_empty"; -Addsimps [Pow_empty]; - -Goal "Pow (insert a A) = Pow A Un (insert a ` Pow A)"; -by (blast_tac (claset() addIs [inst "x" "?u-{a}" image_eqI]) 1); -qed "Pow_insert"; - -Goal "Pow (- A) = {-B |B. A: Pow B}"; -by (blast_tac (claset() addIs [inst "x" "- ?u" exI]) 1); -qed "Pow_Compl"; - -Goal "Pow UNIV = UNIV"; -by (Blast_tac 1); -qed "Pow_UNIV"; -Addsimps [Pow_UNIV]; - -Goal "Pow(A) Un Pow(B) <= Pow(A Un B)"; -by (Blast_tac 1); -qed "Un_Pow_subset"; - -Goal "(UN x:A. Pow(B(x))) <= Pow(UN x:A. B(x))"; -by (Blast_tac 1); -qed "UN_Pow_subset"; - -Goal "A <= Pow(Union(A))"; -by (Blast_tac 1); -qed "subset_Pow_Union"; - -Goal "Union(Pow(A)) = A"; -by (Blast_tac 1); -qed "Union_Pow_eq"; - -Goal "Pow(A Int B) = Pow(A) Int Pow(B)"; -by (Blast_tac 1); -qed "Pow_Int_eq"; - -Goal "Pow(INT x:A. B(x)) = (INT x:A. Pow(B(x)))"; -by (Blast_tac 1); -qed "Pow_INT_eq"; - -Addsimps [Union_Pow_eq, Pow_Int_eq]; - - -section "Miscellany"; - -Goal "(A = B) = ((A <= (B::'a set)) & (B<=A))"; -by (Blast_tac 1); -qed "set_eq_subset"; - -Goal "(A <= B) = (ALL t. t:A --> t:B)"; -by (Blast_tac 1); -qed "subset_iff"; - -Goalw [psubset_def] "((A::'a set) <= B) = ((A < B) | (A=B))"; -by (Blast_tac 1); -qed "subset_iff_psubset_eq"; - -Goal "(ALL x. x ~: A) = (A={})"; -by (Blast_tac 1); -qed "all_not_in_conv"; -AddIffs [all_not_in_conv]; - - -(** for datatypes **) -Goal "f x ~= f y ==> x ~= y"; -by (Fast_tac 1); -qed "distinct_lemma"; - - -(** Miniscoping: pushing in big Unions and Intersections **) -local - fun prover s = prove_goal (the_context ()) s - (fn _ => [Simp_tac 1, ALLGOALS Blast_tac]) -in -val UN_simps = map prover - ["(UN x:C. insert a (B x)) = (if C={} then {} else insert a (UN x:C. B x))", - "(UN x:C. A x Un B) = ((if C={} then {} else (UN x:C. A x) Un B))", - "(UN x:C. A Un B x) = ((if C={} then {} else A Un (UN x:C. B x)))", - "(UN x:C. A x Int B) = ((UN x:C. A x) Int B)", - "(UN x:C. A Int B x) = (A Int (UN x:C. B x))", - "(UN x:C. A x - B) = ((UN x:C. A x) - B)", - "(UN x:C. A - B x) = (A - (INT x:C. B x))", - "(UN x: Union A. B x) = (UN y:A. UN x:y. B x)", - "(UN z: UNION A B. C z) = (UN x:A. UN z: B(x). C z)", - "(UN x:f`A. B x) = (UN a:A. B(f a))"]; - -val INT_simps = map prover - ["(INT x:C. A x Int B) = (if C={} then UNIV else (INT x:C. A x) Int B)", - "(INT x:C. A Int B x) = (if C={} then UNIV else A Int (INT x:C. B x))", - "(INT x:C. A x - B) = (if C={} then UNIV else (INT x:C. A x) - B)", - "(INT x:C. A - B x) = (if C={} then UNIV else A - (UN x:C. B x))", - "(INT x:C. insert a (B x)) = insert a (INT x:C. B x)", - "(INT x:C. A x Un B) = ((INT x:C. A x) Un B)", - "(INT x:C. A Un B x) = (A Un (INT x:C. B x))", - "(INT x: Union A. B x) = (INT y:A. INT x:y. B x)", - "(INT z: UNION A B. C z) = (INT x:A. INT z: B(x). C z)", - "(INT x:f`A. B x) = (INT a:A. B(f a))"]; - - -val ball_simps = map prover - ["(ALL x:A. P x | Q) = ((ALL x:A. P x) | Q)", - "(ALL x:A. P | Q x) = (P | (ALL x:A. Q x))", - "(ALL x:A. P --> Q x) = (P --> (ALL x:A. Q x))", - "(ALL x:A. P x --> Q) = ((EX x:A. P x) --> Q)", - "(ALL x:{}. P x) = True", - "(ALL x:UNIV. P x) = (ALL x. P x)", - "(ALL x:insert a B. P x) = (P(a) & (ALL x:B. P x))", - "(ALL x:Union(A). P x) = (ALL y:A. ALL x:y. P x)", - "(ALL x: UNION A B. P x) = (ALL a:A. ALL x: B a. P x)", - "(ALL x:Collect Q. P x) = (ALL x. Q x --> P x)", - "(ALL x:f`A. P x) = (ALL x:A. P(f x))", - "(~(ALL x:A. P x)) = (EX x:A. ~P x)"]; - -val ball_conj_distrib = - prover "(ALL x:A. P x & Q x) = ((ALL x:A. P x) & (ALL x:A. Q x))"; - -val bex_simps = map prover - ["(EX x:A. P x & Q) = ((EX x:A. P x) & Q)", - "(EX x:A. P & Q x) = (P & (EX x:A. Q x))", - "(EX x:{}. P x) = False", - "(EX x:UNIV. P x) = (EX x. P x)", - "(EX x:insert a B. P x) = (P(a) | (EX x:B. P x))", - "(EX x:Union(A). P x) = (EX y:A. EX x:y. P x)", - "(EX x: UNION A B. P x) = (EX a:A. EX x: B a. P x)", - "(EX x:Collect Q. P x) = (EX x. Q x & P x)", - "(EX x:f`A. P x) = (EX x:A. P(f x))", - "(~(EX x:A. P x)) = (ALL x:A. ~P x)"]; - -val bex_disj_distrib = - prover "(EX x:A. P x | Q x) = ((EX x:A. P x) | (EX x:A. Q x))"; - -end; - -bind_thms ("UN_simps", UN_simps); -bind_thms ("INT_simps", INT_simps); -bind_thms ("ball_simps", ball_simps); -bind_thms ("bex_simps", bex_simps); -bind_thm ("ball_conj_distrib", ball_conj_distrib); -bind_thm ("bex_disj_distrib", bex_disj_distrib); - -Addsimps (UN_simps @ INT_simps @ ball_simps @ bex_simps); diff -r 4518acda6d93 -r f4d10ad0ea7b src/HOL/mono.ML --- a/src/HOL/mono.ML Fri Feb 15 20:43:44 2002 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,113 +0,0 @@ -(* Title: HOL/mono.ML - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1991 University of Cambridge - -Monotonicity of various operations -*) - -Goal "A<=B ==> f`A <= f`B"; -by (Blast_tac 1); -qed "image_mono"; - -Goal "A<=B ==> Pow(A) <= Pow(B)"; -by (Blast_tac 1); -qed "Pow_mono"; - -Goal "A<=B ==> Union(A) <= Union(B)"; -by (Blast_tac 1); -qed "Union_mono"; - -Goal "B<=A ==> Inter(A) <= Inter(B)"; -by (Blast_tac 1); -qed "Inter_anti_mono"; - -val prems = Goal - "[| A<=B; !!x. x:A ==> f(x)<=g(x) |] ==> \ -\ (UN x:A. f(x)) <= (UN x:B. g(x))"; -by (blast_tac (claset() addIs (prems RL [subsetD])) 1); -qed "UN_mono"; - -(*The last inclusion is POSITIVE! *) -val prems = Goal - "[| B<=A; !!x. x:A ==> f(x)<=g(x) |] ==> \ -\ (INT x:A. f(x)) <= (INT x:A. g(x))"; -by (blast_tac (claset() addIs (prems RL [subsetD])) 1); -qed "INT_anti_mono"; - -Goal "C<=D ==> insert a C <= insert a D"; -by (Blast_tac 1); -qed "insert_mono"; - -Goal "[| A<=C; B<=D |] ==> A Un B <= C Un D"; -by (Blast_tac 1); -qed "Un_mono"; - -Goal "[| A<=C; B<=D |] ==> A Int B <= C Int D"; -by (Blast_tac 1); -qed "Int_mono"; - -Goal "!!A::'a set. [| A<=C; D<=B |] ==> A-B <= C-D"; -by (Blast_tac 1); -qed "Diff_mono"; - -Goal "!!A::'a set. A <= B ==> -B <= -A"; -by (Blast_tac 1); -qed "Compl_anti_mono"; - -(** Monotonicity of implications. For inductive definitions **) - -Goal "A<=B ==> x:A --> x:B"; -by (rtac impI 1); -by (etac subsetD 1); -by (assume_tac 1); -qed "in_mono"; - -Goal "[| P1-->Q1; P2-->Q2 |] ==> (P1&P2) --> (Q1&Q2)"; -by (Blast_tac 1); -qed "conj_mono"; - -Goal "[| P1-->Q1; P2-->Q2 |] ==> (P1|P2) --> (Q1|Q2)"; -by (Blast_tac 1); -qed "disj_mono"; - -Goal "[| Q1-->P1; P2-->Q2 |] ==> (P1-->P2)-->(Q1-->Q2)"; -by (Blast_tac 1); -qed "imp_mono"; - -Goal "P-->P"; -by (rtac impI 1); -by (assume_tac 1); -qed "imp_refl"; - -val [PQimp] = Goal - "[| !!x. P(x) --> Q(x) |] ==> (EX x. P(x)) --> (EX x. Q(x))"; -by (blast_tac (claset() addIs [PQimp RS mp]) 1); -qed "ex_mono"; - -val [PQimp] = Goal - "[| !!x. P(x) --> Q(x) |] ==> (ALL x. P(x)) --> (ALL x. Q(x))"; -by (blast_tac (claset() addIs [PQimp RS mp]) 1); -qed "all_mono"; - -val [PQimp] = Goal - "[| !!x. P(x) --> Q(x) |] ==> Collect(P) <= Collect(Q)"; -by (blast_tac (claset() addIs [PQimp RS mp]) 1); -qed "Collect_mono"; - -val [subs,PQimp] = Goal - "[| A<=B; !!x. x:A ==> P(x) --> Q(x) \ -\ |] ==> A Int Collect(P) <= B Int Collect(Q)"; -by (blast_tac (claset() addIs [subs RS subsetD, PQimp RS mp]) 1); -qed "Int_Collect_mono"; - -val basic_monos = [subset_refl, imp_refl, disj_mono, conj_mono, - ex_mono, Collect_mono, in_mono]; - -Goal "[| a = b; c = d; b --> d |] ==> a --> c"; -by (Fast_tac 1); -qed "eq_to_mono"; - -Goal "[| a = b; c = d; ~ b --> ~ d |] ==> ~ a --> ~ c"; -by (Fast_tac 1); -qed "eq_to_mono2"; diff -r 4518acda6d93 -r f4d10ad0ea7b src/HOL/subset.ML --- a/src/HOL/subset.ML Fri Feb 15 20:43:44 2002 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,267 +0,0 @@ -(* Title: HOL/subset.ML - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1991 University of Cambridge - -Derived rules involving subsets. Union and Intersection as lattice -operations. -*) - -(* legacy ML bindings *) - -val Ball_def = thm "Ball_def"; -val Bex_def = thm "Bex_def"; -val Collect_mem_eq = thm "Collect_mem_eq"; -val Compl_def = thm "Compl_def"; -val INTER_def = thm "INTER_def"; -val Int_def = thm "Int_def"; -val Inter_def = thm "Inter_def"; -val Pow_def = thm "Pow_def"; -val UNION_def = thm "UNION_def"; -val UNIV_def = thm "UNIV_def"; -val Un_def = thm "Un_def"; -val Union_def = thm "Union_def"; -val empty_def = thm "empty_def"; -val image_def = thm "image_def"; -val insert_def = thm "insert_def"; -val mem_Collect_eq = thm "mem_Collect_eq"; -val psubset_def = thm "psubset_def"; -val set_diff_def = thm "set_diff_def"; -val subset_def = thm "subset_def"; -val CollectI = thm "CollectI"; -val CollectD = thm "CollectD"; -val set_ext = thm "set_ext"; -val Collect_cong = thm "Collect_cong"; -val CollectE = thm "CollectE"; -val ballI = thm "ballI"; -val strip = thms "strip"; -val bspec = thm "bspec"; -val ballE = thm "ballE"; -val bexI = thm "bexI"; -val rev_bexI = thm "rev_bexI"; -val bexCI = thm "bexCI"; -val bexE = thm "bexE"; -val ball_triv = thm "ball_triv"; -val bex_triv = thm "bex_triv"; -val bex_triv_one_point1 = thm "bex_triv_one_point1"; -val bex_triv_one_point2 = thm "bex_triv_one_point2"; -val bex_one_point1 = thm "bex_one_point1"; -val bex_one_point2 = thm "bex_one_point2"; -val ball_one_point1 = thm "ball_one_point1"; -val ball_one_point2 = thm "ball_one_point2"; -val ball_cong = thm "ball_cong"; -val bex_cong = thm "bex_cong"; -val subsetI = thm "subsetI"; -val subsetD = thm "subsetD"; -val rev_subsetD = thm "rev_subsetD"; -val subsetCE = thm "subsetCE"; -val contra_subsetD = thm "contra_subsetD"; -val subset_refl = thm "subset_refl"; -val subset_trans = thm "subset_trans"; -val subset_antisym = thm "subset_antisym"; -val equalityI = thm "equalityI"; -val equalityD1 = thm "equalityD1"; -val equalityD2 = thm "equalityD2"; -val equalityE = thm "equalityE"; -val equalityCE = thm "equalityCE"; -val setup_induction = thm "setup_induction"; -val eqset_imp_iff = thm "eqset_imp_iff"; -val UNIV_I = thm "UNIV_I"; -val UNIV_witness = thm "UNIV_witness"; -val subset_UNIV = thm "subset_UNIV"; -val ball_UNIV = thm "ball_UNIV"; -val bex_UNIV = thm "bex_UNIV"; -val empty_iff = thm "empty_iff"; -val emptyE = thm "emptyE"; -val empty_subsetI = thm "empty_subsetI"; -val equals0I = thm "equals0I"; -val equals0D = thm "equals0D"; -val ball_empty = thm "ball_empty"; -val bex_empty = thm "bex_empty"; -val UNIV_not_empty = thm "UNIV_not_empty"; -val Pow_iff = thm "Pow_iff"; -val PowI = thm "PowI"; -val PowD = thm "PowD"; -val Pow_bottom = thm "Pow_bottom"; -val Pow_top = thm "Pow_top"; -val Compl_iff = thm "Compl_iff"; -val ComplI = thm "ComplI"; -val ComplD = thm "ComplD"; -val ComplE = thm "ComplE"; -val Un_iff = thm "Un_iff"; -val UnI1 = thm "UnI1"; -val UnI2 = thm "UnI2"; -val UnCI = thm "UnCI"; -val UnE = thm "UnE"; -val Int_iff = thm "Int_iff"; -val IntI = thm "IntI"; -val IntD1 = thm "IntD1"; -val IntD2 = thm "IntD2"; -val IntE = thm "IntE"; -val Diff_iff = thm "Diff_iff"; -val DiffI = thm "DiffI"; -val DiffD1 = thm "DiffD1"; -val DiffD2 = thm "DiffD2"; -val DiffE = thm "DiffE"; -val insert_iff = thm "insert_iff"; -val insertI1 = thm "insertI1"; -val insertI2 = thm "insertI2"; -val insertE = thm "insertE"; -val insertCI = thm "insertCI"; -val subset_insert_iff = thm "subset_insert_iff"; -val singletonI = thm "singletonI"; -val singletonD = thm "singletonD"; -val singletonE = thm "singletonE"; -val singleton_iff = thm "singleton_iff"; -val singleton_inject = thm "singleton_inject"; -val singleton_insert_inj_eq = thm "singleton_insert_inj_eq"; -val singleton_insert_inj_eq' = thm "singleton_insert_inj_eq'"; -val subset_singletonD = thm "subset_singletonD"; -val singleton_conv = thm "singleton_conv"; -val singleton_conv2 = thm "singleton_conv2"; -val diff_single_insert = thm "diff_single_insert"; -val UN_iff = thm "UN_iff"; -val UN_I = thm "UN_I"; -val UN_E = thm "UN_E"; -val UN_cong = thm "UN_cong"; -val INT_iff = thm "INT_iff"; -val INT_I = thm "INT_I"; -val INT_D = thm "INT_D"; -val INT_E = thm "INT_E"; -val INT_cong = thm "INT_cong"; -val Union_iff = thm "Union_iff"; -val UnionI = thm "UnionI"; -val UnionE = thm "UnionE"; -val Inter_iff = thm "Inter_iff"; -val InterI = thm "InterI"; -val InterD = thm "InterD"; -val InterE = thm "InterE"; -val image_eqI = thm "image_eqI"; -val imageI = thm "imageI"; -val rev_image_eqI = thm "rev_image_eqI"; -val imageE = thm "imageE"; -val image_Un = thm "image_Un"; -val image_iff = thm "image_iff"; -val image_subset_iff = thm "image_subset_iff"; -val subset_image_iff = thm "subset_image_iff"; -val image_subsetI = thm "image_subsetI"; -val range_eqI = thm "range_eqI"; -val rangeI = thm "rangeI"; -val rangeE = thm "rangeE"; -val split_if_eq1 = thm "split_if_eq1"; -val split_if_eq2 = thm "split_if_eq2"; -val split_if_mem1 = thm "split_if_mem1"; -val split_if_mem2 = thm "split_if_mem2"; -val split_ifs = thms "split_ifs"; -val mem_simps = thms "mem_simps"; -val psubsetI = thm "psubsetI"; -val psubset_insert_iff = thm "psubset_insert_iff"; -val psubset_eq = thm "psubset_eq"; -val psubset_imp_subset = thm "psubset_imp_subset"; -val psubset_subset_trans = thm "psubset_subset_trans"; -val subset_psubset_trans = thm "subset_psubset_trans"; -val psubset_imp_ex_mem = thm "psubset_imp_ex_mem"; -val atomize_ball = thm "atomize_ball"; - - -(*** insert ***) - -Goal "B <= insert a B"; -by (rtac subsetI 1); -by (etac insertI2 1) ; -qed "subset_insertI"; - -Goal "x ~: A ==> (A <= insert x B) = (A <= B)"; -by (Blast_tac 1); -qed "subset_insert"; - -(*** Big Union -- least upper bound of a set ***) - -Goal "B:A ==> B <= Union(A)"; -by (REPEAT (ares_tac [subsetI,UnionI] 1)); -qed "Union_upper"; - -val [prem] = Goal "[| !!X. X:A ==> X<=C |] ==> Union(A) <= C"; -by (rtac subsetI 1); -by (REPEAT (eresolve_tac [asm_rl, UnionE, prem RS subsetD] 1)); -qed "Union_least"; - -(** General union **) - -Goal "a:A ==> B(a) <= (UN x:A. B(x))"; -by (Blast_tac 1); -qed "UN_upper"; - -val [prem] = Goal "[| !!x. x:A ==> B(x)<=C |] ==> (UN x:A. B(x)) <= C"; -by (rtac subsetI 1); -by (REPEAT (eresolve_tac [asm_rl, UN_E, prem RS subsetD] 1)); -qed "UN_least"; - - -(*** Big Intersection -- greatest lower bound of a set ***) - -Goal "B:A ==> Inter(A) <= B"; -by (Blast_tac 1); -qed "Inter_lower"; - -val [prem] = Goal "[| !!X. X:A ==> C<=X |] ==> C <= Inter(A)"; -by (rtac (InterI RS subsetI) 1); -by (REPEAT (eresolve_tac [asm_rl, prem RS subsetD] 1)); -qed "Inter_greatest"; - -Goal "a:A ==> (INT x:A. B(x)) <= B(a)"; -by (Blast_tac 1); -qed "INT_lower"; - -val [prem] = Goal "[| !!x. x:A ==> C<=B(x) |] ==> C <= (INT x:A. B(x))"; -by (rtac (INT_I RS subsetI) 1); -by (REPEAT (eresolve_tac [asm_rl, prem RS subsetD] 1)); -qed "INT_greatest"; - -(*** Finite Union -- the least upper bound of 2 sets ***) - -Goal "A <= A Un B"; -by (Blast_tac 1); -qed "Un_upper1"; - -Goal "B <= A Un B"; -by (Blast_tac 1); -qed "Un_upper2"; - -Goal "[| A<=C; B<=C |] ==> A Un B <= C"; -by (Blast_tac 1); -qed "Un_least"; - -(*** Finite Intersection -- the greatest lower bound of 2 sets *) - -Goal "A Int B <= A"; -by (Blast_tac 1); -qed "Int_lower1"; - -Goal "A Int B <= B"; -by (Blast_tac 1); -qed "Int_lower2"; - -Goal "[| C<=A; C<=B |] ==> C <= A Int B"; -by (Blast_tac 1); -qed "Int_greatest"; - -(*** Set difference ***) - -Goal "A-B <= (A::'a set)"; -by (Blast_tac 1) ; -qed "Diff_subset"; - -(*** Monotonicity ***) - -Goal "mono(f) ==> f(A) Un f(B) <= f(A Un B)"; -by (rtac Un_least 1); -by (etac (Un_upper1 RSN (2,monoD)) 1); -by (etac (Un_upper2 RSN (2,monoD)) 1); -qed "mono_Un"; - -Goal "mono(f) ==> f(A Int B) <= f(A) Int f(B)"; -by (rtac Int_greatest 1); -by (etac (Int_lower1 RSN (2,monoD)) 1); -by (etac (Int_lower2 RSN (2,monoD)) 1); -qed "mono_Int";