# HG changeset patch # User traytel # Date 1394104646 -3600 # Node ID 25a90cebbbe5a2df88b82872d571971dadd1f8db # Parent 91f245c23bc540fad6cf04df9e5c8433bce79fce more careful simplification of sets (cf. abf91ebd0820)---yields smaller terms diff -r 91f245c23bc5 -r 25a90cebbbe5 src/HOL/BNF_Comp.thy --- a/src/HOL/BNF_Comp.thy Wed Mar 05 17:23:28 2014 -0800 +++ b/src/HOL/BNF_Comp.thy Thu Mar 06 12:17:26 2014 +0100 @@ -57,14 +57,6 @@ lemma UN_image_subset: "\(f ` g x) \ X = (g x \ {x. f x \ X})" by blast -lemma mem_UN_compreh_ex_eq: "(z : \{y. \x\A. y = F x}) = (\x\A. z : F x)" -by blast - -lemma UN_compreh_ex_eq_eq: -"\{y. \x\A. y = {}} = {}" -"\{y. \x\A. y = {x}} = A" -by blast+ - lemma comp_set_bd_Union_o_collect: "|\\((\f. f x) ` X)| \o hbd \ |(Union \ collect X) x| \o hbd" by (unfold comp_apply collect_def SUP_def) diff -r 91f245c23bc5 -r 25a90cebbbe5 src/HOL/BNF_FP_Base.thy --- a/src/HOL/BNF_FP_Base.thy Wed Mar 05 17:23:28 2014 -0800 +++ b/src/HOL/BNF_FP_Base.thy Thu Mar 06 12:17:26 2014 +0100 @@ -98,13 +98,6 @@ "setr (Inr x) = {x}" unfolding sum_set_defs by simp+ -lemma UN_compreh_eq_eq: -"\{y. y = A} = A" -by blast+ - -lemma ex_in_single: "(\x \ {y}. P x) = P y" -by blast - lemma spec2: "\x y. P x y \ P x y" by blast diff -r 91f245c23bc5 -r 25a90cebbbe5 src/HOL/Tools/BNF/bnf_comp.ML --- a/src/HOL/Tools/BNF/bnf_comp.ML Wed Mar 05 17:23:28 2014 -0800 +++ b/src/HOL/Tools/BNF/bnf_comp.ML Thu Mar 06 12:17:26 2014 +0100 @@ -197,7 +197,8 @@ val setT = fastype_of set; val var_set' = Const (@{const_name id_bnf_comp}, setT --> setT) $ Var ((Name.uu, 0), setT); val goal = mk_Trueprop_eq (var_set', set); - fun tac {context = ctxt, prems = _} = mk_simplified_set_tac ctxt; + fun tac {context = ctxt, prems = _} = + mk_simplified_set_tac ctxt (collect_set_map_of_bnf outer); val set'_eq_set = Goal.prove names_lthy [] [] goal tac |> Thm.close_derivation; diff -r 91f245c23bc5 -r 25a90cebbbe5 src/HOL/Tools/BNF/bnf_comp_tactics.ML --- a/src/HOL/Tools/BNF/bnf_comp_tactics.ML Wed Mar 05 17:23:28 2014 -0800 +++ b/src/HOL/Tools/BNF/bnf_comp_tactics.ML Thu Mar 06 12:17:26 2014 +0100 @@ -31,7 +31,7 @@ val mk_le_rel_OO_tac: thm -> thm -> thm list -> tactic val mk_simple_rel_OO_Grp_tac: thm -> thm -> tactic val mk_simple_wit_tac: thm list -> tactic - val mk_simplified_set_tac: Proof.context -> tactic + val mk_simplified_set_tac: Proof.context -> thm -> tactic val bd_ordIso_natLeq_tac: tactic end; @@ -144,12 +144,13 @@ rtac @{thm cprod_com}) 1 end; -val comp_in_alt_thms = @{thms o_apply collect_def SUP_def image_insert image_empty Union_insert - Union_empty Un_empty_right Union_Un_distrib Un_subset_iff conj_subset_def UN_image_subset +val comp_in_alt_thms = @{thms o_apply collect_def image_insert image_empty Union_insert UN_insert + UN_empty Union_empty Un_empty_right Union_Un_distrib Un_subset_iff conj_subset_def UN_image_subset conj_assoc}; fun mk_comp_in_alt_tac ctxt comp_set_alts = - unfold_thms_tac ctxt (comp_set_alts @ comp_in_alt_thms) THEN + unfold_thms_tac ctxt comp_set_alts THEN + unfold_thms_tac ctxt comp_in_alt_thms THEN unfold_thms_tac ctxt @{thms set_eq_subset} THEN rtac conjI 1 THEN REPEAT_DETERM ( @@ -161,13 +162,14 @@ atac ORELSE' (rtac subset_UNIV)) 1)) ORELSE rtac subset_UNIV 1)); -val comp_wit_thms = @{thms Union_empty_conv o_apply collect_def SUP_def +val comp_wit_thms = @{thms Union_empty_conv o_apply collect_def UN_insert UN_empty Un_empty_right Union_image_insert Union_image_empty}; fun mk_comp_wit_tac ctxt set'_eq_sets Gwit_thms collect_set_map Fwit_thms = unfold_thms_tac ctxt set'_eq_sets THEN ALLGOALS (dtac @{thm in_Union_o_assoc}) THEN - unfold_thms_tac ctxt (collect_set_map :: comp_wit_thms) THEN + unfold_thms_tac ctxt [collect_set_map] THEN + unfold_thms_tac ctxt comp_wit_thms THEN REPEAT_DETERM ((atac ORELSE' REPEAT_DETERM o eresolve_tac @{thms UnionE UnE} THEN' etac imageE THEN' TRY o dresolve_tac Gwit_thms THEN' @@ -236,13 +238,12 @@ val cprod_thms = @{thms cprod_cong1 cprod_cong2 cprod_cong cprod_dup[OF natLeq_cinfinite natLeq_Card_order]}; -(*inspired by "bnf_fp_def_sugar_tactics.ML"*) val simplified_set_simps = - @{thms SUP_empty Sup_empty Sup_insert UN_insert Un_empty_left Un_empty_right Un_iff - Union_Un_distrib collect_def[abs_def] image_def o_def map_pair_simp mem_Collect_eq - mem_UN_compreh_ex_eq UN_compreh_ex_eq_eq sum.set_map prod.set_map id_bnf_comp_def}; + @{thms collect_def[abs_def] UN_insert UN_empty Un_empty_right Un_empty_left + o_def Union_Un_distrib Union_image_eq UN_empty2 UN_singleton id_bnf_comp_def}; -fun mk_simplified_set_tac ctxt = +fun mk_simplified_set_tac ctxt collect_set_map = + unfold_thms_tac ctxt (collect_set_map :: @{thms comp_assoc}) THEN unfold_thms_tac ctxt simplified_set_simps THEN rtac refl 1; val bd_ordIso_natLeq_tac = diff -r 91f245c23bc5 -r 25a90cebbbe5 src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Wed Mar 05 17:23:28 2014 -0800 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Thu Mar 06 12:17:26 2014 +0100 @@ -39,10 +39,9 @@ val sum_prod_thms_map = @{thms id_apply map_pair_simp prod.case sum.case sum_map.simps}; val sum_prod_thms_set = - @{thms SUP_empty Sup_empty Sup_insert UN_insert Un_empty_left Un_empty_right Un_iff - Union_Un_distrib collect_def[abs_def] image_def o_apply map_pair_simp - mem_Collect_eq mem_UN_compreh_ex_eq prod_set_simps sum_map.simps sum_set_simps - UN_compreh_ex_eq_eq UN_compreh_eq_eq ex_in_single}; + @{thms UN_empty UN_insert Un_empty_left Un_empty_right Un_iff UN_simps(10) UN_iff + Union_Un_distrib image_iff o_apply map_pair_simp + mem_Collect_eq prod_set_simps sum_map.simps sum_set_simps}; val sum_prod_thms_rel = @{thms prod_rel_apply sum_rel_simps id_apply}; fun hhf_concl_conv cv ctxt ct =