register 'Spec_Rules' for new-style (co)datatypes
authorblanchet
Fri Feb 14 07:53:45 2014 +0100 (2014-02-14)
changeset 55463942c2153b5b4
parent 55462 78a06c7b5b87
child 55464 56fa33537869
register 'Spec_Rules' for new-style (co)datatypes
src/HOL/BNF_GFP.thy
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
     1.1 --- a/src/HOL/BNF_GFP.thy	Fri Feb 14 07:53:45 2014 +0100
     1.2 +++ b/src/HOL/BNF_GFP.thy	Fri Feb 14 07:53:45 2014 +0100
     1.3 @@ -287,16 +287,16 @@
     1.4  definition image2p where
     1.5    "image2p f g R = (\<lambda>x y. \<exists>x' y'. R x' y' \<and> f x' = x \<and> g y' = y)"
     1.6  
     1.7 -lemma image2pI: "R x y \<Longrightarrow> (image2p f g R) (f x) (g y)"
     1.8 +lemma image2pI: "R x y \<Longrightarrow> image2p f g R (f x) (g y)"
     1.9    unfolding image2p_def by blast
    1.10  
    1.11 -lemma image2pE: "\<lbrakk>(image2p f g R) fx gy; (\<And>x y. fx = f x \<Longrightarrow> gy = g y \<Longrightarrow> R x y \<Longrightarrow> P)\<rbrakk> \<Longrightarrow> P"
    1.12 +lemma image2pE: "\<lbrakk>image2p f g R fx gy; (\<And>x y. fx = f x \<Longrightarrow> gy = g y \<Longrightarrow> R x y \<Longrightarrow> P)\<rbrakk> \<Longrightarrow> P"
    1.13    unfolding image2p_def by blast
    1.14  
    1.15 -lemma fun_rel_iff_geq_image2p: "(fun_rel R S) f g = (image2p f g R \<le> S)"
    1.16 +lemma fun_rel_iff_geq_image2p: "fun_rel R S f g = (image2p f g R \<le> S)"
    1.17    unfolding fun_rel_def image2p_def by auto
    1.18  
    1.19 -lemma fun_rel_image2p: "(fun_rel R (image2p f g R)) f g"
    1.20 +lemma fun_rel_image2p: "fun_rel R (image2p f g R) f g"
    1.21    unfolding fun_rel_def image2p_def by auto
    1.22  
    1.23  
    1.24 @@ -341,7 +341,7 @@
    1.25  lemma univ_preserves:
    1.26  assumes ECH: "equiv A r" and RES: "f respects r" and
    1.27          PRES: "\<forall> x \<in> A. f x \<in> B"
    1.28 -shows "\<forall> X \<in> A//r. univ f X \<in> B"
    1.29 +shows "\<forall>X \<in> A//r. univ f X \<in> B"
    1.30  proof
    1.31    fix X assume "X \<in> A//r"
    1.32    then obtain x where x: "x \<in> A" and X: "X = proj r x" using ECH proj_image[of r A] by blast
     2.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Feb 14 07:53:45 2014 +0100
     2.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Feb 14 07:53:45 2014 +0100
     2.3 @@ -222,6 +222,9 @@
     2.4  
     2.5  val lists_bmoc = fold (fn xs => fn t => Term.list_comb (t, xs));
     2.6  
     2.7 +fun lhs_head_of_hd (thm :: _) =
     2.8 +  [Term.head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of thm))))];
     2.9 +
    2.10  fun flat_rec_arg_args xss =
    2.11    (* FIXME (once the old datatype package is phased out): The first line below gives the preferred
    2.12       order. The second line is for compatibility with the old datatype package. *)
    2.13 @@ -1293,6 +1296,7 @@
    2.14  
    2.15                val map_thms = map2 mk_map_thm ctr_defs' cxIns;
    2.16                val set_thmss = map mk_set_thms fp_set_thms;
    2.17 +              val set_thms = flat set_thmss;
    2.18  
    2.19                val rel_infos = (ctr_defs' ~~ cxIns, ctr_defs' ~~ cyIns);
    2.20  
    2.21 @@ -1324,23 +1328,30 @@
    2.22                val (rel_distinct_thms, _) =
    2.23                  join_halves n half_rel_distinct_thmss other_half_rel_distinct_thmss;
    2.24  
    2.25 +              val rel_eq_thms =
    2.26 +                map (fn th => th RS @{thm eq_False[THEN iffD2]}) rel_distinct_thms @
    2.27 +                map2 (fn th => fn 0 => th RS @{thm eq_True[THEN iffD2]} | _ => th)
    2.28 +                  rel_inject_thms ms;
    2.29 +
    2.30                val anonymous_notes =
    2.31                  [([case_cong], fundefcong_attrs),
    2.32 -                 (map (fn th => th RS @{thm eq_False[THEN iffD2]}) rel_distinct_thms,
    2.33 -                  code_nitpicksimp_attrs),
    2.34 -                 (map2 (fn th => fn 0 => th RS @{thm eq_True[THEN iffD2]} | _ => th)
    2.35 -                    rel_inject_thms ms, code_nitpicksimp_attrs)]
    2.36 +                 (rel_eq_thms, code_nitpicksimp_attrs)]
    2.37                  |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
    2.38  
    2.39                val notes =
    2.40                  [(mapN, map_thms, code_nitpicksimp_attrs @ simp_attrs),
    2.41                   (rel_distinctN, rel_distinct_thms, simp_attrs),
    2.42                   (rel_injectN, rel_inject_thms, simp_attrs),
    2.43 -                 (setN, flat set_thmss, code_nitpicksimp_attrs @ simp_attrs)]
    2.44 +                 (setN, set_thms, code_nitpicksimp_attrs @ simp_attrs)]
    2.45                  |> massage_simple_notes fp_b_name;
    2.46              in
    2.47                (((map_thms, rel_inject_thms, rel_distinct_thms, set_thmss), ctr_sugar),
    2.48 -               lthy |> Local_Theory.notes (anonymous_notes @ notes) |> snd)
    2.49 +               lthy
    2.50 +               |> Spec_Rules.add Spec_Rules.Equational (`lhs_head_of_hd map_thms)
    2.51 +               |> Spec_Rules.add Spec_Rules.Equational (`lhs_head_of_hd rel_eq_thms)
    2.52 +               |> Spec_Rules.add Spec_Rules.Equational (`lhs_head_of_hd set_thms)
    2.53 +               |> Local_Theory.notes (anonymous_notes @ notes)
    2.54 +               |> snd)
    2.55              end;
    2.56  
    2.57          fun mk_binding pre = Binding.qualify false fp_b_name (Binding.prefix_name (pre ^ "_") fp_b);
    2.58 @@ -1393,6 +1404,8 @@
    2.59            |> massage_multi_notes;
    2.60        in
    2.61          lthy
    2.62 +        |> Spec_Rules.add Spec_Rules.Equational (map un_fold_of iterss, flat fold_thmss)
    2.63 +        |> Spec_Rules.add Spec_Rules.Equational (map co_rec_of iterss, flat rec_thmss)
    2.64          |> Local_Theory.notes (common_notes @ notes) |> snd
    2.65          |> register_fp_sugars Least_FP pre_bnfs nested_bnfs nesting_bnfs fp_res ctr_defss ctr_sugars
    2.66            iterss mapss [induct_thm] (transpose [induct_thms]) (transpose [fold_thmss, rec_thmss])
    2.67 @@ -1449,8 +1462,15 @@
    2.68             (strong_coinductN, map single strong_coinduct_thms, K coinduct_attrs),
    2.69             (unfoldN, unfold_thmss, K coiter_attrs)]
    2.70            |> massage_multi_notes;
    2.71 +
    2.72 +        (* TODO: code theorems *)
    2.73 +        fun add_spec_rules coiter_of sel_thmss ctr_thmss =
    2.74 +          fold (curry (Spec_Rules.add Spec_Rules.Equational) (map coiter_of coiterss))
    2.75 +            [flat sel_thmss, flat ctr_thmss]
    2.76        in
    2.77          lthy
    2.78 +        |> add_spec_rules un_fold_of sel_unfold_thmss unfold_thmss
    2.79 +        |> add_spec_rules co_rec_of sel_corec_thmss corec_thmss
    2.80          |> Local_Theory.notes (common_notes @ notes) |> snd
    2.81          |> register_fp_sugars Greatest_FP pre_bnfs nested_bnfs nesting_bnfs fp_res ctr_defss
    2.82            ctr_sugars coiterss mapss [coinduct_thm, strong_coinduct_thm]