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