more careful simplification of sets (cf. abf91ebd0820)---yields smaller terms
authortraytel
Thu Mar 06 12:17:26 2014 +0100 (2014-03-06)
changeset 5593025a90cebbbe5
parent 55929 91f245c23bc5
child 55931 62156e694f3d
more careful simplification of sets (cf. abf91ebd0820)---yields smaller terms
src/HOL/BNF_Comp.thy
src/HOL/BNF_FP_Base.thy
src/HOL/Tools/BNF/bnf_comp.ML
src/HOL/Tools/BNF/bnf_comp_tactics.ML
src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
     1.1 --- a/src/HOL/BNF_Comp.thy	Wed Mar 05 17:23:28 2014 -0800
     1.2 +++ b/src/HOL/BNF_Comp.thy	Thu Mar 06 12:17:26 2014 +0100
     1.3 @@ -57,14 +57,6 @@
     1.4  lemma UN_image_subset: "\<Union>(f ` g x) \<subseteq> X = (g x \<subseteq> {x. f x \<subseteq> X})"
     1.5  by blast
     1.6  
     1.7 -lemma mem_UN_compreh_ex_eq: "(z : \<Union>{y. \<exists>x\<in>A. y = F x}) = (\<exists>x\<in>A. z : F x)"
     1.8 -by blast
     1.9 -
    1.10 -lemma UN_compreh_ex_eq_eq:
    1.11 -"\<Union>{y. \<exists>x\<in>A. y = {}} = {}"
    1.12 -"\<Union>{y. \<exists>x\<in>A. y = {x}} = A"
    1.13 -by blast+
    1.14 -
    1.15  lemma comp_set_bd_Union_o_collect: "|\<Union>\<Union>((\<lambda>f. f x) ` X)| \<le>o hbd \<Longrightarrow> |(Union \<circ> collect X) x| \<le>o hbd"
    1.16  by (unfold comp_apply collect_def SUP_def)
    1.17  
     2.1 --- a/src/HOL/BNF_FP_Base.thy	Wed Mar 05 17:23:28 2014 -0800
     2.2 +++ b/src/HOL/BNF_FP_Base.thy	Thu Mar 06 12:17:26 2014 +0100
     2.3 @@ -98,13 +98,6 @@
     2.4  "setr (Inr x) = {x}"
     2.5  unfolding sum_set_defs by simp+
     2.6  
     2.7 -lemma UN_compreh_eq_eq:
     2.8 -"\<Union>{y. y = A} = A"
     2.9 -by blast+
    2.10 -
    2.11 -lemma ex_in_single: "(\<exists>x \<in> {y}. P x) = P y"
    2.12 -by blast
    2.13 -
    2.14  lemma spec2: "\<forall>x y. P x y \<Longrightarrow> P x y"
    2.15  by blast
    2.16  
     3.1 --- a/src/HOL/Tools/BNF/bnf_comp.ML	Wed Mar 05 17:23:28 2014 -0800
     3.2 +++ b/src/HOL/Tools/BNF/bnf_comp.ML	Thu Mar 06 12:17:26 2014 +0100
     3.3 @@ -197,7 +197,8 @@
     3.4          val setT = fastype_of set;
     3.5          val var_set' = Const (@{const_name id_bnf_comp}, setT --> setT) $ Var ((Name.uu, 0), setT);
     3.6          val goal = mk_Trueprop_eq (var_set', set);
     3.7 -        fun tac {context = ctxt, prems = _} = mk_simplified_set_tac ctxt;
     3.8 +        fun tac {context = ctxt, prems = _} =
     3.9 +          mk_simplified_set_tac ctxt (collect_set_map_of_bnf outer);
    3.10          val set'_eq_set =
    3.11            Goal.prove names_lthy [] [] goal tac
    3.12            |> Thm.close_derivation;
     4.1 --- a/src/HOL/Tools/BNF/bnf_comp_tactics.ML	Wed Mar 05 17:23:28 2014 -0800
     4.2 +++ b/src/HOL/Tools/BNF/bnf_comp_tactics.ML	Thu Mar 06 12:17:26 2014 +0100
     4.3 @@ -31,7 +31,7 @@
     4.4    val mk_le_rel_OO_tac: thm -> thm -> thm list -> tactic
     4.5    val mk_simple_rel_OO_Grp_tac: thm -> thm -> tactic
     4.6    val mk_simple_wit_tac: thm list -> tactic
     4.7 -  val mk_simplified_set_tac: Proof.context -> tactic
     4.8 +  val mk_simplified_set_tac: Proof.context -> thm -> tactic
     4.9    val bd_ordIso_natLeq_tac: tactic
    4.10  end;
    4.11  
    4.12 @@ -144,12 +144,13 @@
    4.13       rtac @{thm cprod_com}) 1
    4.14    end;
    4.15  
    4.16 -val comp_in_alt_thms = @{thms o_apply collect_def SUP_def image_insert image_empty Union_insert
    4.17 -  Union_empty Un_empty_right Union_Un_distrib Un_subset_iff conj_subset_def UN_image_subset
    4.18 +val comp_in_alt_thms = @{thms o_apply collect_def image_insert image_empty Union_insert UN_insert
    4.19 +  UN_empty Union_empty Un_empty_right Union_Un_distrib Un_subset_iff conj_subset_def UN_image_subset
    4.20    conj_assoc};
    4.21  
    4.22  fun mk_comp_in_alt_tac ctxt comp_set_alts =
    4.23 -  unfold_thms_tac ctxt (comp_set_alts @ comp_in_alt_thms) THEN
    4.24 +  unfold_thms_tac ctxt comp_set_alts THEN
    4.25 +  unfold_thms_tac ctxt comp_in_alt_thms THEN
    4.26    unfold_thms_tac ctxt @{thms set_eq_subset} THEN
    4.27    rtac conjI 1 THEN
    4.28    REPEAT_DETERM (
    4.29 @@ -161,13 +162,14 @@
    4.30         atac ORELSE'
    4.31         (rtac subset_UNIV)) 1)) ORELSE rtac subset_UNIV 1));
    4.32  
    4.33 -val comp_wit_thms = @{thms Union_empty_conv o_apply collect_def SUP_def
    4.34 +val comp_wit_thms = @{thms Union_empty_conv o_apply collect_def UN_insert UN_empty Un_empty_right
    4.35    Union_image_insert Union_image_empty};
    4.36  
    4.37  fun mk_comp_wit_tac ctxt set'_eq_sets Gwit_thms collect_set_map Fwit_thms =
    4.38    unfold_thms_tac ctxt set'_eq_sets THEN
    4.39    ALLGOALS (dtac @{thm in_Union_o_assoc}) THEN
    4.40 -  unfold_thms_tac ctxt (collect_set_map :: comp_wit_thms) THEN
    4.41 +  unfold_thms_tac ctxt [collect_set_map] THEN
    4.42 +  unfold_thms_tac ctxt comp_wit_thms THEN
    4.43    REPEAT_DETERM ((atac ORELSE'
    4.44      REPEAT_DETERM o eresolve_tac @{thms UnionE UnE} THEN'
    4.45      etac imageE THEN' TRY o dresolve_tac Gwit_thms THEN'
    4.46 @@ -236,13 +238,12 @@
    4.47  val cprod_thms =
    4.48    @{thms cprod_cong1 cprod_cong2 cprod_cong cprod_dup[OF natLeq_cinfinite natLeq_Card_order]};
    4.49  
    4.50 -(*inspired by "bnf_fp_def_sugar_tactics.ML"*)
    4.51  val simplified_set_simps =
    4.52 -  @{thms SUP_empty Sup_empty Sup_insert UN_insert Un_empty_left Un_empty_right Un_iff
    4.53 -      Union_Un_distrib collect_def[abs_def] image_def o_def map_pair_simp mem_Collect_eq
    4.54 -      mem_UN_compreh_ex_eq UN_compreh_ex_eq_eq sum.set_map prod.set_map id_bnf_comp_def};
    4.55 +  @{thms collect_def[abs_def] UN_insert UN_empty Un_empty_right Un_empty_left
    4.56 +    o_def Union_Un_distrib Union_image_eq UN_empty2 UN_singleton id_bnf_comp_def};
    4.57  
    4.58 -fun mk_simplified_set_tac ctxt =
    4.59 +fun mk_simplified_set_tac ctxt collect_set_map =
    4.60 +  unfold_thms_tac ctxt (collect_set_map :: @{thms comp_assoc}) THEN
    4.61    unfold_thms_tac ctxt simplified_set_simps THEN rtac refl 1;
    4.62  
    4.63  val bd_ordIso_natLeq_tac =
     5.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Wed Mar 05 17:23:28 2014 -0800
     5.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Thu Mar 06 12:17:26 2014 +0100
     5.3 @@ -39,10 +39,9 @@
     5.4  
     5.5  val sum_prod_thms_map = @{thms id_apply map_pair_simp prod.case sum.case sum_map.simps};
     5.6  val sum_prod_thms_set =
     5.7 -  @{thms SUP_empty Sup_empty Sup_insert UN_insert Un_empty_left Un_empty_right Un_iff
     5.8 -      Union_Un_distrib collect_def[abs_def] image_def o_apply map_pair_simp
     5.9 -      mem_Collect_eq mem_UN_compreh_ex_eq prod_set_simps sum_map.simps sum_set_simps
    5.10 -      UN_compreh_ex_eq_eq UN_compreh_eq_eq ex_in_single};
    5.11 +  @{thms UN_empty UN_insert Un_empty_left Un_empty_right Un_iff UN_simps(10) UN_iff
    5.12 +      Union_Un_distrib image_iff o_apply map_pair_simp
    5.13 +      mem_Collect_eq prod_set_simps sum_map.simps sum_set_simps};
    5.14  val sum_prod_thms_rel = @{thms prod_rel_apply sum_rel_simps id_apply};
    5.15  
    5.16  fun hhf_concl_conv cv ctxt ct =