don't register equations of the form 'f x = ...' as simp rules, even if they are safe (noncorecursive), because they unfold too aggresively concepts users are likely to want to stay folded
authorblanchet
Wed Oct 02 16:29:40 2013 +0200 (2013-10-02)
changeset 54030732b53d9b720
parent 54029 4edfd0fd5536
child 54031 a3281fbe6856
don't register equations of the form 'f x = ...' as simp rules, even if they are safe (noncorecursive), because they unfold too aggresively concepts users are likely to want to stay folded
src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML
src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Oct 02 15:53:20 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Oct 02 16:29:40 2013 +0200
     1.3 @@ -53,7 +53,7 @@
     1.4    type gfp_sugar_thms =
     1.5      ((thm list * thm) list * Args.src list)
     1.6      * (thm list list * thm list list * Args.src list)
     1.7 -    * (thm list list * thm list list) * (thm list list * thm list list * Args.src list)
     1.8 +    * (thm list list * thm list list * Args.src list)
     1.9      * (thm list list * thm list list * Args.src list)
    1.10      * (thm list list list * thm list list list * Args.src list)
    1.11  
    1.12 @@ -397,7 +397,7 @@
    1.13  type gfp_sugar_thms =
    1.14    ((thm list * thm) list * Args.src list)
    1.15    * (thm list list * thm list list * Args.src list)
    1.16 -  * (thm list list * thm list list) * (thm list list * thm list list * Args.src list)
    1.17 +  * (thm list list * thm list list * Args.src list)
    1.18    * (thm list list * thm list list * Args.src list)
    1.19    * (thm list list list * thm list list list * Args.src list);
    1.20  
    1.21 @@ -908,7 +908,7 @@
    1.22      val fcoiterss' as [gunfolds, hcorecs] =
    1.23        map2 (fn (pfss, _) => map (lists_bmoc pfss)) (map fst coiters_args_types) coiterss';
    1.24  
    1.25 -    val (unfold_thmss, corec_thmss, safe_unfold_thmss, safe_corec_thmss) =
    1.26 +    val (unfold_thmss, corec_thmss) =
    1.27        let
    1.28          fun mk_goal pfss c cps fcoiter n k ctr m cfs' =
    1.29            fold_rev (fold_rev Logic.all) ([c] :: pfss)
    1.30 @@ -956,18 +956,8 @@
    1.31          val corec_thmss =
    1.32            map2 (map2 prove) corec_goalss corec_tacss
    1.33            |> map (map (unfold_thms lthy @{thms sum_case_if}));
    1.34 -
    1.35 -        val unfold_safesss = map2 (map2 (map2 (curry op =))) crgsss' crgsss;
    1.36 -        val corec_safesss = map2 (map2 (map2 (curry op =))) cshsss' cshsss;
    1.37 -
    1.38 -        val filter_safesss =
    1.39 -          map2 (map_filter (fn (safes, thm) => if forall I safes then SOME thm else NONE) oo
    1.40 -            curry (op ~~));
    1.41 -
    1.42 -        val safe_unfold_thmss = filter_safesss unfold_safesss unfold_thmss;
    1.43 -        val safe_corec_thmss = filter_safesss corec_safesss corec_thmss;
    1.44        in
    1.45 -        (unfold_thmss, corec_thmss, safe_unfold_thmss, safe_corec_thmss)
    1.46 +        (unfold_thmss, corec_thmss)
    1.47        end;
    1.48  
    1.49      val (disc_unfold_iff_thmss, disc_corec_iff_thmss) =
    1.50 @@ -1035,7 +1025,6 @@
    1.51    in
    1.52      ((coinduct_thms_pairs, coinduct_case_attrs),
    1.53       (unfold_thmss, corec_thmss, code_nitpick_simp_attrs),
    1.54 -     (safe_unfold_thmss, safe_corec_thmss),
    1.55       (disc_unfold_thmss, disc_corec_thmss, []),
    1.56       (disc_unfold_iff_thmss, disc_corec_iff_thmss, simp_attrs),
    1.57       (sel_unfold_thmsss, sel_corec_thmsss, simp_attrs))
    1.58 @@ -1464,7 +1453,6 @@
    1.59          val (([(coinduct_thms, coinduct_thm), (strong_coinduct_thms, strong_coinduct_thm)],
    1.60                coinduct_attrs),
    1.61               (unfold_thmss, corec_thmss, coiter_attrs),
    1.62 -             (safe_unfold_thmss, safe_corec_thmss),
    1.63               (disc_unfold_thmss, disc_corec_thmss, disc_coiter_attrs),
    1.64               (disc_unfold_iff_thmss, disc_corec_iff_thmss, disc_coiter_iff_attrs),
    1.65               (sel_unfold_thmsss, sel_corec_thmsss, sel_coiter_attrs)) =
    1.66 @@ -1477,21 +1465,14 @@
    1.67  
    1.68          val coinduct_type_attr = Attrib.internal o K o Induct.coinduct_type;
    1.69  
    1.70 -        fun flat_coiter_thms coiters disc_coiters disc_coiter_iffs sel_coiters =
    1.71 -          coiters @ disc_coiters @ disc_coiter_iffs @ sel_coiters;
    1.72 +        val flat_coiter_thms = append oo append;
    1.73  
    1.74          val simp_thmss =
    1.75            map7 mk_simp_thms ctr_sugars
    1.76 -            (map4 flat_coiter_thms safe_unfold_thmss disc_unfold_thmss disc_unfold_iff_thmss
    1.77 -               sel_unfold_thmss)
    1.78 -            (map4 flat_coiter_thms safe_corec_thmss disc_corec_thmss disc_corec_iff_thmss
    1.79 -               sel_corec_thmss)
    1.80 +            (map3 flat_coiter_thms disc_unfold_thmss disc_unfold_iff_thmss sel_unfold_thmss)
    1.81 +            (map3 flat_coiter_thms disc_corec_thmss disc_corec_iff_thmss sel_corec_thmss)
    1.82              mapss rel_injects rel_distincts setss;
    1.83  
    1.84 -        val anonymous_notes =
    1.85 -          [(flat safe_unfold_thmss @ flat safe_corec_thmss, simp_attrs)]
    1.86 -          |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
    1.87 -
    1.88          val common_notes =
    1.89            (if nn > 1 then
    1.90               [(coinductN, [coinduct_thm], coinduct_attrs),
    1.91 @@ -1521,7 +1502,7 @@
    1.92            |> Generic_Target.theory_declaration;
    1.93        in
    1.94          lthy
    1.95 -        |> Local_Theory.notes (anonymous_notes @ common_notes @ notes) |> snd
    1.96 +        |> Local_Theory.notes (common_notes @ notes) |> snd
    1.97          |> register_fp_sugars Greatest_FP pre_bnfs nested_bnfs nesting_bnfs fp_res ctr_defss
    1.98            ctr_sugars coiterss mapss [coinduct_thm, strong_coinduct_thm]
    1.99            (transpose [unfold_thmss, corec_thmss]) (transpose [disc_unfold_thmss, disc_corec_thmss])
     2.1 --- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Wed Oct 02 15:53:20 2013 +0200
     2.2 +++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Wed Oct 02 16:29:40 2013 +0200
     2.3 @@ -157,7 +157,7 @@
     2.4            derive_coinduct_coiters_thms_for_types pre_bnfs (the coiters_args_types) xtor_co_induct
     2.5              dtor_injects dtor_ctors xtor_co_iter_thmss nesting_bnfs fpTs Cs kss mss ns ctr_defss
     2.6              ctr_sugars co_iterss co_iter_defss (Proof_Context.export lthy no_defs_lthy) lthy
     2.7 -          |> `(fn ((coinduct_thms_pairs, _), (unfold_thmss, corec_thmss, _), _,
     2.8 +          |> `(fn ((coinduct_thms_pairs, _), (unfold_thmss, corec_thmss, _),
     2.9                    (disc_unfold_thmss, disc_corec_thmss, _), _,
    2.10                    (sel_unfold_thmsss, sel_corec_thmsss, _)) =>
    2.11              (map snd coinduct_thms_pairs, unfold_thmss, corec_thmss, disc_unfold_thmss,
     3.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Wed Oct 02 15:53:20 2013 +0200
     3.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Wed Oct 02 16:29:40 2013 +0200
     3.3 @@ -918,20 +918,10 @@
     3.4          val ctr_thmss = map5 (maps oooo prove_ctr) disc_alists sel_alists disc_eqnss sel_eqnss
     3.5            (map #ctr_specs corec_specs);
     3.6  
     3.7 -        val safess = map (map (not o exists_subterm (member (op =) (map SOME fun_names) o
     3.8 -          try (fst o dest_Free)) o snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o
     3.9 -          Logic.strip_imp_concl o drop_All o prop_of)) ctr_thmss;
    3.10 -        val safe_ctr_thmss = map (map snd o filter fst o (op ~~)) (safess ~~ ctr_thmss);
    3.11 -
    3.12 -        val simp_thmss =
    3.13 -          map3 (fn x => fn y => fn z => x @ y @ z) disc_thmss sel_thmss safe_ctr_thmss;
    3.14 +        val simp_thmss = map2 append disc_thmss sel_thmss
    3.15  
    3.16          val common_name = mk_common_name fun_names;
    3.17  
    3.18 -        val anonymous_notes =
    3.19 -          [(flat safe_ctr_thmss, simp_attrs)]
    3.20 -          |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
    3.21 -
    3.22          val notes =
    3.23            [(coinductN, map (if n2m then single else K []) coinduct_thms, []),
    3.24             (codeN, ctr_thmss(*FIXME*), code_nitpick_attrs),
    3.25 @@ -953,7 +943,7 @@
    3.26            |> map (fn (thmN, thms, attrs) =>
    3.27              ((Binding.qualify true common_name (Binding.name thmN), attrs), [(thms, [])]));
    3.28        in
    3.29 -        lthy |> Local_Theory.notes (anonymous_notes @ notes @ common_notes) |> snd
    3.30 +        lthy |> Local_Theory.notes (notes @ common_notes) |> snd
    3.31        end;
    3.32  
    3.33      fun after_qed thmss' = fold_map Local_Theory.define defs #-> prove thmss';