1(*  Title:      HOL/Tools/BNF/bnf_lfp_basic_sugar.ML
2    Author:     Jasmin Blanchette, TU Muenchen
3    Copyright   2014
4
5Registration of basic types as BNF least fixpoints (datatypes).
6*)
7
8structure BNF_LFP_Basic_Sugar : sig end =
9struct
10
11open Ctr_Sugar
12open BNF_Util
13open BNF_Def
14open BNF_Comp
15open BNF_FP_Rec_Sugar_Util
16open BNF_FP_Util
17open BNF_FP_Def_Sugar
18
19fun trivial_absT_info_of fpT =
20  {absT = fpT, repT = fpT, abs = Const (\<^const_name>\<open>id_bnf\<close>, fpT --> fpT),
21   rep = Const (\<^const_name>\<open>id_bnf\<close>, fpT --> fpT),
22   abs_inject = @{thm type_definition.Abs_inject[OF type_definition_id_bnf_UNIV UNIV_I UNIV_I]},
23   abs_inverse = @{thm type_definition.Abs_inverse[OF type_definition_id_bnf_UNIV UNIV_I]},
24   type_definition = @{thm type_definition_id_bnf_UNIV}};
25
26fun the_frozen_ctr_sugar_of ctxt fpT_name =
27  the (ctr_sugar_of ctxt fpT_name)
28  |> morph_ctr_sugar (Morphism.typ_morphism "BNF" Logic.unvarifyT_global
29    $> Morphism.term_morphism "BNF" (Term.map_types Logic.unvarifyT_global));
30
31fun trivial_fp_result_of fp_bnf fpT C xtor_map xtor_sets xtor_rel ctor_rec_o_map
32    xtor_rel_induct ctor_rec_transfer =
33  let
34    val xtors = [Const (\<^const_name>\<open>xtor\<close>, fpT --> fpT)];
35    val co_recs = [Const (\<^const_name>\<open>ctor_rec\<close>, (fpT --> C) --> (fpT --> C))];
36    val co_rec_thms = [map_id0_of_bnf fp_bnf RS @{thm ctor_rec}];
37    val co_rec_unique_thm = map_id0_of_bnf fp_bnf RS @{thm ctor_rec_unique};
38  in
39    {Ts = [fpT], bnfs = [fp_bnf], pre_bnfs = [ID_bnf], absT_infos = [trivial_absT_info_of fpT],
40     ctors = xtors, dtors = xtors, xtor_un_folds = co_recs,
41     xtor_co_recs = co_recs, xtor_co_induct = @{thm xtor_induct}, dtor_ctors = @{thms xtor_xtor},
42     ctor_dtors = @{thms xtor_xtor}, ctor_injects = @{thms xtor_inject},
43     dtor_injects = @{thms xtor_inject}, xtor_maps = [xtor_map],
44     xtor_map_unique = @{thm xtor_map_unique}, xtor_setss = [xtor_sets], xtor_rels = [xtor_rel],
45     xtor_un_fold_thms = co_rec_thms, xtor_co_rec_thms = co_rec_thms,
46     xtor_un_fold_unique = co_rec_unique_thm, xtor_co_rec_unique = co_rec_unique_thm,
47     xtor_un_fold_o_maps = [ctor_rec_o_map], xtor_co_rec_o_maps = [ctor_rec_o_map],
48     xtor_un_fold_transfers = [ctor_rec_transfer],
49     xtor_co_rec_transfers = [ctor_rec_transfer],
50     xtor_rel_co_induct = xtor_rel_induct, dtor_set_inducts = []}
51  end;
52
53fun fp_sugar_of_sum ctxt =
54  let
55    val fpT as Type (fpT_name, As) = \<^typ>\<open>'a + 'b\<close>;
56    val fpBT = \<^typ>\<open>'c + 'd\<close>;
57    val C = \<^typ>\<open>'e\<close>;
58    val X = \<^typ>\<open>'sum\<close>;
59    val ctr_Tss = map single As;
60
61    val fp_bnf = the (bnf_of ctxt fpT_name);
62    val xtor_map = @{thm xtor_map[of "map_sum f1 f2" for f1 f2]};
63    val xtor_sets = @{thms xtor_set[of setl] xtor_set[of setr]};
64    val xtor_rel = @{thm xtor_rel[of "rel_sum R1 R2" for R1 R2]};
65    val ctor_rec_o_map = @{thm ctor_rec_o_map[of _ "map_sum g1 g2" for g1 g2]};
66    val xtor_rel_induct = @{thm xtor_rel_induct[of "rel_sum R1 R2" for R1 R2]};
67    val ctor_rec_transfer = @{thm ctor_rec_transfer[of "rel_sum R1 R2" for R1 R2]};
68  in
69    {T = fpT,
70     BT = fpBT,
71     X = X,
72     fp = Least_FP,
73     fp_res_index = 0,
74     fp_res =
75       trivial_fp_result_of fp_bnf fpT C xtor_map xtor_sets xtor_rel ctor_rec_o_map xtor_rel_induct
76         ctor_rec_transfer,
77     pre_bnf = ID_bnf (*wrong*),
78     fp_bnf = fp_bnf,
79     absT_info = trivial_absT_info_of fpT,
80     fp_nesting_bnfs = [],
81     live_nesting_bnfs = [],
82     fp_ctr_sugar =
83       {ctrXs_Tss = ctr_Tss,
84        ctor_iff_dtor = @{thm xtor_iff_xtor},
85        ctr_defs = @{thms Inl_def_alt Inr_def_alt},
86        ctr_sugar = the_frozen_ctr_sugar_of ctxt fpT_name,
87        ctr_transfers = @{thms Inl_transfer Inr_transfer},
88        case_transfers = @{thms case_sum_transfer},
89        disc_transfers = @{thms isl_transfer},
90        sel_transfers = []},
91     fp_bnf_sugar =
92       {map_thms = @{thms map_sum.simps},
93        map_disc_iffs = @{thms isl_map_sum},
94        map_selss = map single @{thms map_sum_sel},
95        rel_injects = @{thms rel_sum_simps(1,4)},
96        rel_distincts = @{thms rel_sum_simps(2,3)[THEN eq_False[THEN iffD1]]},
97        rel_sels = @{thms rel_sum_sel},
98        rel_intros = @{thms rel_sum.intros},
99        rel_cases = @{thms rel_sum.cases},
100        pred_injects = @{thms pred_sum_inject},
101        set_thms = @{thms sum_set_simps},
102        set_selssss = [[[@{thms set_sum_sel(1)}], [[]]], [[[]], [@{thms set_sum_sel(2)}]]],
103        set_introssss = [[[@{thms setl.intros[OF refl]}], [[]]],
104          [[[]], [@{thms setr.intros[OF refl]}]]],
105        set_cases = @{thms setl.cases[simplified hypsubst_in_prems]
106          setr.cases[simplified hypsubst_in_prems]}},
107     fp_co_induct_sugar = SOME
108       {co_rec = Const (\<^const_name>\<open>case_sum\<close>, map (fn Ts => (Ts ---> C)) ctr_Tss ---> fpT --> C),
109        common_co_inducts = @{thms sum.induct},
110        co_inducts = @{thms sum.induct},
111        co_rec_def = @{thm ctor_rec_def_alt[of "case_sum f1 f2" for f1 f2]},
112        co_rec_thms = @{thms sum.case},
113        co_rec_discs = [],
114        co_rec_disc_iffs = [],
115        co_rec_selss = [],
116        co_rec_codes = [],
117        co_rec_transfers = @{thms case_sum_transfer},
118        co_rec_o_maps = @{thms case_sum_o_map_sum},
119        common_rel_co_inducts = @{thms rel_sum.inducts},
120        rel_co_inducts = @{thms rel_sum.induct},
121        common_set_inducts = [],
122        set_inducts = []}}
123  end;
124
125fun fp_sugar_of_prod ctxt =
126  let
127    val fpT as Type (fpT_name, As) = \<^typ>\<open>'a * 'b\<close>;
128    val fpBT = \<^typ>\<open>'c * 'd\<close>;
129    val C = \<^typ>\<open>'e\<close>;
130    val X = \<^typ>\<open>'prod\<close>;
131    val ctr_Ts = As;
132
133    val fp_bnf = the (bnf_of ctxt fpT_name);
134    val xtor_map = @{thm xtor_map[of "map_prod f1 f2" for f1 f2]};
135    val xtor_sets = @{thms xtor_set[of fsts] xtor_set[of snds]};
136    val xtor_rel = @{thm xtor_rel[of "rel_prod R1 R2" for R1 R2]};
137    val ctor_rec_o_map = @{thm ctor_rec_o_map[of _ "map_prod g1 g2" for g1 g2]};
138    val xtor_rel_induct = @{thm xtor_rel_induct[of "rel_prod R1 R2" for R1 R2]};
139    val ctor_rec_transfer = @{thm ctor_rec_transfer[of "rel_prod R1 R2" for R1 R2]};
140  in
141    {T = fpT,
142     BT = fpBT,
143     X = X,
144     fp = Least_FP,
145     fp_res_index = 0,
146     fp_res =
147       trivial_fp_result_of fp_bnf fpT C xtor_map xtor_sets xtor_rel ctor_rec_o_map xtor_rel_induct
148         ctor_rec_transfer,
149     pre_bnf = ID_bnf (*wrong*),
150     fp_bnf = fp_bnf,
151     absT_info = trivial_absT_info_of fpT,
152     fp_nesting_bnfs = [],
153     live_nesting_bnfs = [],
154     fp_ctr_sugar =
155       {ctrXs_Tss = [ctr_Ts],
156        ctor_iff_dtor = @{thm xtor_iff_xtor},
157        ctr_defs = @{thms Pair_def_alt},
158        ctr_sugar = the_frozen_ctr_sugar_of ctxt fpT_name,
159        ctr_transfers = @{thms Pair_transfer},
160        case_transfers = @{thms case_prod_transfer},
161        disc_transfers = [],
162        sel_transfers = @{thms fst_transfer snd_transfer}},
163     fp_bnf_sugar =
164       {map_thms = @{thms map_prod_simp},
165        map_disc_iffs = [],
166        map_selss = [@{thms fst_map_prod snd_map_prod}],
167        rel_injects = @{thms rel_prod_inject},
168        rel_distincts = [],
169        rel_sels = @{thms rel_prod_sel},
170        rel_intros = @{thms rel_prod.intros},
171        rel_cases = @{thms rel_prod.cases},
172        pred_injects = @{thms pred_prod_inject},
173        set_thms = @{thms prod_set_simps},
174        set_selssss = [[[@{thms fsts.intros}, []]], [[[], @{thms snds.intros}]]],
175        set_introssss = [[[@{thms fsts.intros[of "(a, b)" for a b, simplified fst_conv]}, []]],
176          [[[], @{thms snds.intros[of "(a, b)" for a b, simplified snd_conv]}]]],
177        set_cases = @{thms fsts.cases[simplified eq_fst_iff ex_neg_all_pos]
178          snds.cases[simplified eq_snd_iff ex_neg_all_pos]}},
179     fp_co_induct_sugar = SOME
180       {co_rec = Const (\<^const_name>\<open>case_prod\<close>, (ctr_Ts ---> C) --> fpT --> C),
181        common_co_inducts = @{thms prod.induct},
182        co_inducts = @{thms prod.induct},
183        co_rec_def = @{thm ctor_rec_def_alt[of "case_prod f" for f]},
184        co_rec_thms = @{thms prod.case},
185        co_rec_discs = [],
186        co_rec_disc_iffs = [],
187        co_rec_selss = [],
188        co_rec_codes = [],
189        co_rec_transfers = @{thms case_prod_transfer},
190        co_rec_o_maps = @{thms case_prod_o_map_prod},
191        common_rel_co_inducts = @{thms rel_prod.inducts},
192        rel_co_inducts = @{thms rel_prod.induct},
193        common_set_inducts = [],
194        set_inducts = []}}
195  end;
196
197val _ = Theory.setup (Named_Target.theory_map (fn lthy =>
198  fold (BNF_FP_Def_Sugar.register_fp_sugars (K true) o single o (fn f => f lthy))
199    [fp_sugar_of_sum, fp_sugar_of_prod] lthy));
200
201end;
202