1(* Title: HOL/Tools/BNF/bnf_fp_def_sugar.ML 2 Author: Jasmin Blanchette, TU Muenchen 3 Author: Martin Desharnais, TU Muenchen 4 Copyright 2012, 2013, 2014 5 6Sugared datatype and codatatype constructions. 7*) 8 9signature BNF_FP_DEF_SUGAR = 10sig 11 type fp_ctr_sugar = 12 {ctrXs_Tss: typ list list, 13 ctor_iff_dtor: thm, 14 ctr_defs: thm list, 15 ctr_sugar: Ctr_Sugar.ctr_sugar, 16 ctr_transfers: thm list, 17 case_transfers: thm list, 18 disc_transfers: thm list, 19 sel_transfers: thm list} 20 21 type fp_bnf_sugar = 22 {map_thms: thm list, 23 map_disc_iffs: thm list, 24 map_selss: thm list list, 25 rel_injects: thm list, 26 rel_distincts: thm list, 27 rel_sels: thm list, 28 rel_intros: thm list, 29 rel_cases: thm list, 30 pred_injects: thm list, 31 set_thms: thm list, 32 set_selssss: thm list list list list, 33 set_introssss: thm list list list list, 34 set_cases: thm list} 35 36 type fp_co_induct_sugar = 37 {co_rec: term, 38 common_co_inducts: thm list, 39 co_inducts: thm list, 40 co_rec_def: thm, 41 co_rec_thms: thm list, 42 co_rec_discs: thm list, 43 co_rec_disc_iffs: thm list, 44 co_rec_selss: thm list list, 45 co_rec_codes: thm list, 46 co_rec_transfers: thm list, 47 co_rec_o_maps: thm list, 48 common_rel_co_inducts: thm list, 49 rel_co_inducts: thm list, 50 common_set_inducts: thm list, 51 set_inducts: thm list} 52 53 type fp_sugar = 54 {T: typ, 55 BT: typ, 56 X: typ, 57 fp: BNF_Util.fp_kind, 58 fp_res_index: int, 59 fp_res: BNF_FP_Util.fp_result, 60 pre_bnf: BNF_Def.bnf, 61 fp_bnf: BNF_Def.bnf, 62 absT_info: BNF_Comp.absT_info, 63 fp_nesting_bnfs: BNF_Def.bnf list, 64 live_nesting_bnfs: BNF_Def.bnf list, 65 fp_ctr_sugar: fp_ctr_sugar, 66 fp_bnf_sugar: fp_bnf_sugar, 67 fp_co_induct_sugar: fp_co_induct_sugar option} 68 69 val co_induct_of: 'a list -> 'a 70 val strong_co_induct_of: 'a list -> 'a 71 72 val morph_fp_bnf_sugar: morphism -> fp_bnf_sugar -> fp_bnf_sugar 73 val morph_fp_co_induct_sugar: morphism -> fp_co_induct_sugar -> fp_co_induct_sugar 74 val morph_fp_ctr_sugar: morphism -> fp_ctr_sugar -> fp_ctr_sugar 75 val morph_fp_sugar: morphism -> fp_sugar -> fp_sugar 76 val transfer_fp_sugar: theory -> fp_sugar -> fp_sugar 77 val fp_sugar_of: Proof.context -> string -> fp_sugar option 78 val fp_sugar_of_global: theory -> string -> fp_sugar option 79 val fp_sugars_of: Proof.context -> fp_sugar list 80 val fp_sugars_of_global: theory -> fp_sugar list 81 val fp_sugars_interpretation: string -> (fp_sugar list -> local_theory -> local_theory) -> 82 theory -> theory 83 val interpret_fp_sugars: (string -> bool) -> fp_sugar list -> local_theory -> local_theory 84 val register_fp_sugars_raw: fp_sugar list -> local_theory -> local_theory 85 val register_fp_sugars: (string -> bool) -> fp_sugar list -> local_theory -> local_theory 86 87 val merge_type_args: BNF_Util.fp_kind -> ''a list * ''a list -> ''a list 88 val type_args_named_constrained_of_spec: (((('a * 'b) * 'c) * 'd) * 'e) * 'f -> 'a 89 val type_binding_of_spec: (((('a * 'b) * 'c) * 'd) * 'e) * 'f -> 'b 90 val mixfix_of_spec: ((('a * 'b) * 'c) * 'd) * 'e -> 'b 91 val mixfixed_ctr_specs_of_spec: (('a * 'b) * 'c) * 'd -> 'b 92 val map_binding_of_spec: ('a * ('b * 'c * 'd)) * 'e -> 'b 93 val rel_binding_of_spec: ('a * ('b * 'c * 'd)) * 'e -> 'c 94 val pred_binding_of_spec: ('a * ('b * 'c * 'd)) * 'e -> 'd 95 val sel_default_eqs_of_spec: 'a * 'b -> 'b 96 97 val mk_parametricity_goal: Proof.context -> term list -> term -> term -> term 98 99 val flat_corec_preds_predsss_gettersss: 'a list -> 'a list list list -> 'a list list list -> 100 'a list 101 val mk_ctor: typ list -> term -> term 102 val mk_dtor: typ list -> term -> term 103 val mk_bnf_sets: BNF_Def.bnf -> string * term list 104 val liveness_of_fp_bnf: int -> BNF_Def.bnf -> bool list 105 val nesting_bnfs: Proof.context -> typ list list list -> typ list -> BNF_Def.bnf list 106 107 val massage_simple_notes: string -> (bstring * 'a list * (int -> 'b)) list -> 108 ((binding * 'c list) * ('a list * 'b) list) list 109 val massage_multi_notes: string list -> typ list -> 110 (string * 'a list list * (string -> 'b)) list -> 111 ((binding * 'b) * ('a list * 'c list) list) list 112 113 val define_ctrs_dtrs_for_type: string -> typ -> term -> term -> thm -> thm -> int -> int list -> 114 term -> binding list -> mixfix list -> typ list list -> local_theory -> 115 (term list list * term list * thm * thm list) * local_theory 116 val wrap_ctrs: (string -> bool) -> BNF_Util.fp_kind -> bool -> string -> thm -> int -> int list -> 117 thm -> thm -> binding list -> binding list list -> term list -> term list -> thm -> thm list -> 118 local_theory -> Ctr_Sugar.ctr_sugar * local_theory 119 val derive_map_set_rel_pred_thms: (string -> bool) -> BNF_Util.fp_kind -> int -> typ list -> 120 typ list -> typ -> typ -> thm list -> thm list -> thm list -> thm list -> thm list -> 121 thm list -> thm list -> thm list -> thm list -> string -> BNF_Def.bnf -> BNF_Def.bnf list -> 122 typ -> term -> thm -> thm -> thm -> thm list -> thm -> thm -> thm list -> thm -> thm list -> 123 thm list -> thm list -> typ list list -> Ctr_Sugar.ctr_sugar -> local_theory -> 124 (thm list * thm list * thm list list * thm list * thm list * thm list * thm list * thm list 125 * thm list * thm list * thm list list list list * thm list list list list * thm list 126 * thm list * thm list * thm list * thm list) * local_theory 127 128 type lfp_sugar_thms = (thm list * thm * Token.src list) * (thm list list * Token.src list) 129 130 val morph_lfp_sugar_thms: morphism -> lfp_sugar_thms -> lfp_sugar_thms 131 val transfer_lfp_sugar_thms: theory -> lfp_sugar_thms -> lfp_sugar_thms 132 133 type gfp_sugar_thms = 134 ((thm list * thm) list * (Token.src list * Token.src list)) 135 * thm list list 136 * thm list list 137 * (thm list list * Token.src list) 138 * (thm list list list * Token.src list) 139 140 val morph_gfp_sugar_thms: morphism -> gfp_sugar_thms -> gfp_sugar_thms 141 val transfer_gfp_sugar_thms: theory -> gfp_sugar_thms -> gfp_sugar_thms 142 143 val mk_co_recs_prelims: Proof.context -> BNF_Util.fp_kind -> typ list list list -> typ list -> 144 typ list -> typ list -> typ list -> int list -> int list list -> term list -> 145 term list 146 * (typ list list * typ list list list list * term list list * term list list list list) option 147 * (string * term list * term list list 148 * (((term list list * term list list * term list list list list * term list list list list) 149 * term list list list) * typ list)) option 150 val repair_nullary_single_ctr: typ list list -> typ list list 151 val mk_corec_p_pred_types: typ list -> int list -> typ list list 152 val mk_corec_fun_arg_types: typ list list list -> typ list -> typ list -> typ list -> int list -> 153 int list list -> term -> 154 typ list list 155 * (typ list list list list * typ list list list * typ list list list list * typ list) 156 val define_co_rec_as: BNF_Util.fp_kind -> typ list -> typ -> binding -> term -> local_theory -> 157 (term * thm) * local_theory 158 val define_rec: 159 typ list list * typ list list list list * term list list * term list list list list -> 160 (string -> binding) -> typ list -> typ list -> term list -> term -> Proof.context -> 161 (term * thm) * Proof.context 162 val define_corec: 'a * term list * term list list 163 * (((term list list * term list list * term list list list list * term list list list list) 164 * term list list list) * typ list) -> (string -> binding) -> 'b list -> typ list -> 165 term list -> term -> local_theory -> (term * thm) * local_theory 166 val mk_induct_raw_prem: (term -> term) -> Proof.context -> typ list list -> 167 (string * term list) list -> term -> term -> typ list -> typ list -> 168 term list * ((term * (term * term)) list * (int * term)) list * term 169 val finish_induct_prem: Proof.context -> int -> term list -> 170 term list * ((term * (term * term)) list * (int * term)) list * term -> term 171 val mk_coinduct_prem: Proof.context -> typ list list -> typ list list -> term list -> term -> 172 term -> term -> int -> term list -> term list list -> term list -> term list list -> 173 typ list list -> term 174 val mk_induct_attrs: term list list -> Token.src list 175 val mk_coinduct_attrs: typ list -> term list list -> term list list -> int list list -> 176 Token.src list * Token.src list 177 val derive_induct_recs_thms_for_types: (string -> bool) -> BNF_Def.bnf list -> 178 ('a * typ list list list list * term list list * 'b) option -> thm -> thm list -> 179 BNF_Def.bnf list -> BNF_Def.bnf list -> typ list -> typ list -> typ list -> 180 typ list list list -> thm list -> thm list -> thm list -> term list list -> thm list list -> 181 term list -> thm list -> Proof.context -> lfp_sugar_thms 182 val derive_coinduct_thms_for_types: Proof.context -> bool -> (term -> term) -> BNF_Def.bnf list -> 183 thm -> thm list -> BNF_Def.bnf list -> typ list -> typ list -> typ list list list -> int list -> 184 thm list -> thm list -> (thm -> thm) -> thm list list -> Ctr_Sugar.ctr_sugar list -> 185 (thm list * thm) list 186 val derive_coinduct_corecs_thms_for_types: Proof.context -> BNF_Def.bnf list -> 187 string * term list * term list list 188 * (((term list list * term list list * term list list list list * term list list list list) 189 * term list list list) * typ list) -> 190 thm -> thm list -> thm list -> thm list -> BNF_Def.bnf list -> typ list -> typ list -> 191 typ list -> typ list list list -> int list list -> int list list -> int list -> thm list -> 192 thm list -> (thm -> thm) -> thm list list -> Ctr_Sugar.ctr_sugar list -> term list -> 193 thm list -> gfp_sugar_thms 194 195 val co_datatypes: BNF_Util.fp_kind -> (mixfix list -> binding list -> binding list -> 196 binding list -> binding list list -> binding list -> (string * sort) list -> 197 typ list * typ list list -> BNF_Def.bnf list -> BNF_Comp.absT_info list -> local_theory -> 198 BNF_FP_Util.fp_result * local_theory) -> 199 Ctr_Sugar.ctr_options 200 * ((((((binding option * (typ * sort)) list * binding) * mixfix) 201 * ((binding, binding * typ) Ctr_Sugar.ctr_spec * mixfix) list) * 202 (binding * binding * binding)) 203 * term list) list -> 204 local_theory -> local_theory 205 val co_datatype_cmd: BNF_Util.fp_kind -> 206 (mixfix list -> binding list -> binding list -> binding list -> binding list list -> 207 binding list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list -> 208 BNF_Comp.absT_info list -> local_theory -> BNF_FP_Util.fp_result * Proof.context) -> 209 ((Proof.context -> Plugin_Name.filter) * bool) 210 * ((((((binding option * (string * string option)) list * binding) * mixfix) 211 * ((binding, binding * string) Ctr_Sugar.ctr_spec * mixfix) list) 212 * (binding * binding * binding)) * string list) list -> 213 Proof.context -> local_theory 214 215 val parse_ctr_arg: (binding * string) parser 216 val parse_ctr_specs: ((binding, binding * string) Ctr_Sugar.ctr_spec * mixfix) list parser 217 val parse_spec: ((((((binding option * (string * string option)) list * binding) * mixfix) 218 * ((binding, binding * string) Ctr_Sugar.ctr_spec * mixfix) list) 219 * (binding * binding * binding)) * string list) parser 220 val parse_co_datatype: (Ctr_Sugar.ctr_options_cmd 221 * ((((((binding option * (string * string option)) list * binding) * mixfix) 222 * ((binding, binding * string) Ctr_Sugar.ctr_spec * mixfix) list) 223 * (binding * binding * binding)) * string list) list) parser 224 225 val parse_co_datatype_cmd: BNF_Util.fp_kind -> (mixfix list -> binding list -> binding list -> 226 binding list -> binding list list -> binding list -> (string * sort) list -> 227 typ list * typ list list -> BNF_Def.bnf list -> BNF_Comp.absT_info list -> local_theory -> 228 BNF_FP_Util.fp_result * local_theory) -> 229 (local_theory -> local_theory) parser 230end; 231 232structure BNF_FP_Def_Sugar : BNF_FP_DEF_SUGAR = 233struct 234 235open Ctr_Sugar 236open BNF_FP_Rec_Sugar_Util 237open BNF_Util 238open BNF_Comp 239open BNF_Def 240open BNF_FP_Util 241open BNF_FP_Def_Sugar_Tactics 242 243val Eq_prefix = "Eq_"; 244 245val case_transferN = "case_transfer"; 246val ctor_iff_dtorN = "ctor_iff_dtor"; 247val ctr_transferN = "ctr_transfer"; 248val disc_transferN = "disc_transfer"; 249val sel_transferN = "sel_transfer"; 250val corec_codeN = "corec_code"; 251val corec_transferN = "corec_transfer"; 252val map_disc_iffN = "map_disc_iff"; 253val map_o_corecN = "map_o_corec"; 254val map_selN = "map_sel"; 255val pred_injectN = "pred_inject"; 256val rec_o_mapN = "rec_o_map"; 257val rec_transferN = "rec_transfer"; 258val set0N = "set0"; 259val set_casesN = "set_cases"; 260val set_introsN = "set_intros"; 261val set_inductN = "set_induct"; 262val set_selN = "set_sel"; 263 264type fp_ctr_sugar = 265 {ctrXs_Tss: typ list list, 266 ctor_iff_dtor: thm, 267 ctr_defs: thm list, 268 ctr_sugar: Ctr_Sugar.ctr_sugar, 269 ctr_transfers: thm list, 270 case_transfers: thm list, 271 disc_transfers: thm list, 272 sel_transfers: thm list}; 273 274type fp_bnf_sugar = 275 {map_thms: thm list, 276 map_disc_iffs: thm list, 277 map_selss: thm list list, 278 rel_injects: thm list, 279 rel_distincts: thm list, 280 rel_sels: thm list, 281 rel_intros: thm list, 282 rel_cases: thm list, 283 pred_injects: thm list, 284 set_thms: thm list, 285 set_selssss: thm list list list list, 286 set_introssss: thm list list list list, 287 set_cases: thm list}; 288 289type fp_co_induct_sugar = 290 {co_rec: term, 291 common_co_inducts: thm list, 292 co_inducts: thm list, 293 co_rec_def: thm, 294 co_rec_thms: thm list, 295 co_rec_discs: thm list, 296 co_rec_disc_iffs: thm list, 297 co_rec_selss: thm list list, 298 co_rec_codes: thm list, 299 co_rec_transfers: thm list, 300 co_rec_o_maps: thm list, 301 common_rel_co_inducts: thm list, 302 rel_co_inducts: thm list, 303 common_set_inducts: thm list, 304 set_inducts: thm list}; 305 306type fp_sugar = 307 {T: typ, 308 BT: typ, 309 X: typ, 310 fp: fp_kind, 311 fp_res_index: int, 312 fp_res: fp_result, 313 pre_bnf: bnf, 314 fp_bnf: bnf, 315 absT_info: absT_info, 316 fp_nesting_bnfs: bnf list, 317 live_nesting_bnfs: bnf list, 318 fp_ctr_sugar: fp_ctr_sugar, 319 fp_bnf_sugar: fp_bnf_sugar, 320 fp_co_induct_sugar: fp_co_induct_sugar option}; 321 322fun co_induct_of (i :: _) = i; 323fun strong_co_induct_of [_, s] = s; 324 325fun morph_fp_bnf_sugar phi ({map_thms, map_disc_iffs, map_selss, rel_injects, rel_distincts, 326 rel_sels, rel_intros, rel_cases, pred_injects, set_thms, set_selssss, set_introssss, 327 set_cases} : fp_bnf_sugar) = 328 {map_thms = map (Morphism.thm phi) map_thms, 329 map_disc_iffs = map (Morphism.thm phi) map_disc_iffs, 330 map_selss = map (map (Morphism.thm phi)) map_selss, 331 rel_injects = map (Morphism.thm phi) rel_injects, 332 rel_distincts = map (Morphism.thm phi) rel_distincts, 333 rel_sels = map (Morphism.thm phi) rel_sels, 334 rel_intros = map (Morphism.thm phi) rel_intros, 335 rel_cases = map (Morphism.thm phi) rel_cases, 336 pred_injects = map (Morphism.thm phi) pred_injects, 337 set_thms = map (Morphism.thm phi) set_thms, 338 set_selssss = map (map (map (map (Morphism.thm phi)))) set_selssss, 339 set_introssss = map (map (map (map (Morphism.thm phi)))) set_introssss, 340 set_cases = map (Morphism.thm phi) set_cases}; 341 342fun morph_fp_co_induct_sugar phi ({co_rec, common_co_inducts, co_inducts, co_rec_def, co_rec_thms, 343 co_rec_discs, co_rec_disc_iffs, co_rec_selss, co_rec_codes, co_rec_transfers, co_rec_o_maps, 344 common_rel_co_inducts, rel_co_inducts, common_set_inducts, set_inducts} : fp_co_induct_sugar) = 345 {co_rec = Morphism.term phi co_rec, 346 common_co_inducts = map (Morphism.thm phi) common_co_inducts, 347 co_inducts = map (Morphism.thm phi) co_inducts, 348 co_rec_def = Morphism.thm phi co_rec_def, 349 co_rec_thms = map (Morphism.thm phi) co_rec_thms, 350 co_rec_discs = map (Morphism.thm phi) co_rec_discs, 351 co_rec_disc_iffs = map (Morphism.thm phi) co_rec_disc_iffs, 352 co_rec_selss = map (map (Morphism.thm phi)) co_rec_selss, 353 co_rec_codes = map (Morphism.thm phi) co_rec_codes, 354 co_rec_transfers = map (Morphism.thm phi) co_rec_transfers, 355 co_rec_o_maps = map (Morphism.thm phi) co_rec_o_maps, 356 common_rel_co_inducts = map (Morphism.thm phi) common_rel_co_inducts, 357 rel_co_inducts = map (Morphism.thm phi) rel_co_inducts, 358 common_set_inducts = map (Morphism.thm phi) common_set_inducts, 359 set_inducts = map (Morphism.thm phi) set_inducts}; 360 361fun morph_fp_ctr_sugar phi ({ctrXs_Tss, ctor_iff_dtor, ctr_defs, ctr_sugar, ctr_transfers, 362 case_transfers, disc_transfers, sel_transfers} : fp_ctr_sugar) = 363 {ctrXs_Tss = map (map (Morphism.typ phi)) ctrXs_Tss, 364 ctor_iff_dtor = Morphism.thm phi ctor_iff_dtor, 365 ctr_defs = map (Morphism.thm phi) ctr_defs, 366 ctr_sugar = morph_ctr_sugar phi ctr_sugar, 367 ctr_transfers = map (Morphism.thm phi) ctr_transfers, 368 case_transfers = map (Morphism.thm phi) case_transfers, 369 disc_transfers = map (Morphism.thm phi) disc_transfers, 370 sel_transfers = map (Morphism.thm phi) sel_transfers}; 371 372fun morph_fp_sugar phi ({T, BT, X, fp, fp_res, fp_res_index, pre_bnf, fp_bnf, absT_info, 373 fp_nesting_bnfs, live_nesting_bnfs, fp_ctr_sugar, fp_bnf_sugar, 374 fp_co_induct_sugar} : fp_sugar) = 375 {T = Morphism.typ phi T, 376 BT = Morphism.typ phi BT, 377 X = Morphism.typ phi X, 378 fp = fp, 379 fp_res = morph_fp_result phi fp_res, 380 fp_res_index = fp_res_index, 381 pre_bnf = morph_bnf phi pre_bnf, 382 fp_bnf = morph_bnf phi fp_bnf, 383 absT_info = morph_absT_info phi absT_info, 384 fp_nesting_bnfs = map (morph_bnf phi) fp_nesting_bnfs, 385 live_nesting_bnfs = map (morph_bnf phi) live_nesting_bnfs, 386 fp_ctr_sugar = morph_fp_ctr_sugar phi fp_ctr_sugar, 387 fp_bnf_sugar = morph_fp_bnf_sugar phi fp_bnf_sugar, 388 fp_co_induct_sugar = Option.map (morph_fp_co_induct_sugar phi) fp_co_induct_sugar}; 389 390val transfer_fp_sugar = morph_fp_sugar o Morphism.transfer_morphism; 391 392structure Data = Generic_Data 393( 394 type T = fp_sugar Symtab.table; 395 val empty = Symtab.empty; 396 val extend = I; 397 fun merge data : T = Symtab.merge (K true) data; 398); 399 400fun fp_sugar_of_generic context = 401 Option.map (transfer_fp_sugar (Context.theory_of context)) o Symtab.lookup (Data.get context); 402 403fun fp_sugars_of_generic context = 404 Symtab.fold (cons o transfer_fp_sugar (Context.theory_of context) o snd) (Data.get context) []; 405 406val fp_sugar_of = fp_sugar_of_generic o Context.Proof; 407val fp_sugar_of_global = fp_sugar_of_generic o Context.Theory; 408 409val fp_sugars_of = fp_sugars_of_generic o Context.Proof; 410val fp_sugars_of_global = fp_sugars_of_generic o Context.Theory; 411 412structure FP_Sugar_Plugin = Plugin(type T = fp_sugar list); 413 414fun fp_sugars_interpretation name f = 415 FP_Sugar_Plugin.interpretation name (fn fp_sugars => fn lthy => 416 f (map (transfer_fp_sugar (Proof_Context.theory_of lthy)) fp_sugars) lthy); 417 418val interpret_fp_sugars = FP_Sugar_Plugin.data; 419 420val register_fp_sugars_raw = 421 fold (fn fp_sugar as {T = Type (s, _), ...} => 422 Local_Theory.declaration {syntax = false, pervasive = true} 423 (fn phi => Data.map (Symtab.update (s, morph_fp_sugar phi fp_sugar)))); 424 425fun register_fp_sugars plugins fp_sugars = 426 register_fp_sugars_raw fp_sugars #> interpret_fp_sugars plugins fp_sugars; 427 428fun interpret_bnfs_register_fp_sugars plugins Ts BTs Xs fp pre_bnfs absT_infos fp_nesting_bnfs 429 live_nesting_bnfs fp_res ctrXs_Tsss ctor_iff_dtors ctr_defss ctr_sugars co_recs co_rec_defs 430 map_thmss common_co_inducts co_inductss co_rec_thmss co_rec_discss co_rec_selsss rel_injectss 431 rel_distinctss map_disc_iffss map_selsss rel_selss rel_intross rel_casess pred_injectss 432 set_thmss set_selsssss set_introsssss set_casess ctr_transferss case_transferss disc_transferss 433 sel_transferss co_rec_disc_iffss co_rec_codess co_rec_transferss common_rel_co_inducts 434 rel_co_inductss common_set_inducts set_inductss co_rec_o_mapss noted = 435 let 436 val fp_sugars = 437 map_index (fn (kk, T) => 438 {T = T, BT = nth BTs kk, X = nth Xs kk, fp = fp, fp_res = fp_res, fp_res_index = kk, 439 pre_bnf = nth pre_bnfs kk, absT_info = nth absT_infos kk, 440 fp_bnf = nth (#bnfs fp_res) kk, 441 fp_nesting_bnfs = fp_nesting_bnfs, live_nesting_bnfs = live_nesting_bnfs, 442 fp_ctr_sugar = 443 {ctrXs_Tss = nth ctrXs_Tsss kk, 444 ctor_iff_dtor = nth ctor_iff_dtors kk, 445 ctr_defs = nth ctr_defss kk, 446 ctr_sugar = nth ctr_sugars kk, 447 ctr_transfers = nth ctr_transferss kk, 448 case_transfers = nth case_transferss kk, 449 disc_transfers = nth disc_transferss kk, 450 sel_transfers = nth sel_transferss kk}, 451 fp_bnf_sugar = 452 {map_thms = nth map_thmss kk, 453 map_disc_iffs = nth map_disc_iffss kk, 454 map_selss = nth map_selsss kk, 455 rel_injects = nth rel_injectss kk, 456 rel_distincts = nth rel_distinctss kk, 457 rel_sels = nth rel_selss kk, 458 rel_intros = nth rel_intross kk, 459 rel_cases = nth rel_casess kk, 460 pred_injects = nth pred_injectss kk, 461 set_thms = nth set_thmss kk, 462 set_selssss = nth set_selsssss kk, 463 set_introssss = nth set_introsssss kk, 464 set_cases = nth set_casess kk}, 465 fp_co_induct_sugar = SOME 466 {co_rec = nth co_recs kk, 467 common_co_inducts = common_co_inducts, 468 co_inducts = nth co_inductss kk, 469 co_rec_def = nth co_rec_defs kk, 470 co_rec_thms = nth co_rec_thmss kk, 471 co_rec_discs = nth co_rec_discss kk, 472 co_rec_disc_iffs = nth co_rec_disc_iffss kk, 473 co_rec_selss = nth co_rec_selsss kk, 474 co_rec_codes = nth co_rec_codess kk, 475 co_rec_transfers = nth co_rec_transferss kk, 476 co_rec_o_maps = nth co_rec_o_mapss kk, 477 common_rel_co_inducts = common_rel_co_inducts, 478 rel_co_inducts = nth rel_co_inductss kk, 479 common_set_inducts = common_set_inducts, 480 set_inducts = nth set_inductss kk}} 481 |> morph_fp_sugar (substitute_noted_thm noted)) Ts; 482 in 483 register_fp_sugars_raw fp_sugars 484 #> fold (interpret_bnf plugins) (#bnfs fp_res) 485 #> interpret_fp_sugars plugins fp_sugars 486 end; 487 488fun quasi_unambiguous_case_names names = 489 let 490 val ps = map (`Long_Name.base_name) names; 491 val dups = Library.duplicates (op =) (map fst ps); 492 fun underscore s = 493 let val ss = Long_Name.explode s 494 in space_implode "_" (drop (length ss - 2) ss) end; 495 in 496 map (fn (base, full) => if member (op =) dups base then underscore full else base) ps 497 |> Name.variant_list [] 498 end; 499 500fun zipper_map f = 501 let 502 fun zed _ [] = [] 503 | zed xs (y :: ys) = f (xs, y, ys) :: zed (xs @ [y]) ys; 504 in zed [] end; 505 506fun cannot_merge_types fp = 507 error ("Mutually " ^ co_prefix fp ^ "recursive types must have the same type parameters"); 508 509fun merge_type_arg fp T T' = if T = T' then T else cannot_merge_types fp; 510 511fun merge_type_args fp (As, As') = 512 if length As = length As' then map2 (merge_type_arg fp) As As' else cannot_merge_types fp; 513 514fun type_args_named_constrained_of_spec (((((ncAs, _), _), _), _), _) = ncAs; 515fun type_binding_of_spec (((((_, b), _), _), _), _) = b; 516fun mixfix_of_spec ((((_, mx), _), _), _) = mx; 517fun mixfixed_ctr_specs_of_spec (((_, mx_ctr_specs), _), _) = mx_ctr_specs; 518fun map_binding_of_spec ((_, (b, _, _)), _) = b; 519fun rel_binding_of_spec ((_, (_, b, _)), _) = b; 520fun pred_binding_of_spec ((_, (_, _, b)), _) = b; 521fun sel_default_eqs_of_spec (_, ts) = ts; 522 523fun ctr_sugar_kind_of_fp_kind Least_FP = Datatype 524 | ctr_sugar_kind_of_fp_kind Greatest_FP = Codatatype; 525 526fun uncurry_thm 0 thm = thm 527 | uncurry_thm 1 thm = thm 528 | uncurry_thm n thm = rotate_prems ~1 (uncurry_thm (n - 1) (rotate_prems 1 (conjI RS thm))); 529 530fun choose_binary_fun fs AB = 531 find_first (fastype_of #> binder_types #> (fn [A, B] => AB = (A, B))) fs; 532fun build_binary_fun_app fs t u = 533 Option.map (rapp u o rapp t) (choose_binary_fun fs (fastype_of t, fastype_of u)); 534 535fun build_the_rel ctxt Rs Ts A B = 536 build_rel [] ctxt Ts [] (the o choose_binary_fun Rs) (A, B); 537fun build_rel_app ctxt Rs Ts t u = 538 build_the_rel ctxt Rs Ts (fastype_of t) (fastype_of u) $ t $ u; 539 540fun build_set_app ctxt A t = Term.betapply (build_set ctxt A (fastype_of t), t); 541 542fun mk_parametricity_goal ctxt Rs t u = 543 let val prem = build_the_rel ctxt Rs [] (fastype_of t) (fastype_of u) in 544 HOLogic.mk_Trueprop (prem $ t $ u) 545 end; 546 547val name_of_set = name_of_const "set function" domain_type; 548 549val fundefcong_attrs = @{attributes [fundef_cong]}; 550val nitpicksimp_attrs = @{attributes [nitpick_simp]}; 551val simp_attrs = @{attributes [simp]}; 552 553val lists_bmoc = fold (fn xs => fn t => Term.list_comb (t, xs)); 554 555fun flat_corec_predss_getterss qss gss = maps (op @) (qss ~~ gss); 556 557fun flat_corec_preds_predsss_gettersss [] [qss] [gss] = flat_corec_predss_getterss qss gss 558 | flat_corec_preds_predsss_gettersss (p :: ps) (qss :: qsss) (gss :: gsss) = 559 p :: flat_corec_predss_getterss qss gss @ flat_corec_preds_predsss_gettersss ps qsss gsss; 560 561fun mk_flip (x, Type (_, [T1, Type (_, [T2, T3])])) = 562 Abs ("x", T1, Abs ("y", T2, Var (x, T2 --> T1 --> T3) $ Bound 0 $ Bound 1)); 563 564fun flip_rels ctxt n thm = 565 let 566 val Rs = Term.add_vars (Thm.prop_of thm) []; 567 val Rs' = rev (drop (length Rs - n) Rs); 568 in 569 infer_instantiate ctxt (map (fn f => (fst f, Thm.cterm_of ctxt (mk_flip f))) Rs') thm 570 end; 571 572fun mk_ctor_or_dtor get_T Ts t = 573 let val Type (_, Ts0) = get_T (fastype_of t) in 574 Term.subst_atomic_types (Ts0 ~~ Ts) t 575 end; 576 577val mk_ctor = mk_ctor_or_dtor range_type; 578val mk_dtor = mk_ctor_or_dtor domain_type; 579 580fun mk_bnf_sets bnf = 581 let 582 val Type (T_name, Us) = T_of_bnf bnf; 583 val lives = lives_of_bnf bnf; 584 val sets = sets_of_bnf bnf; 585 fun mk_set U = 586 (case find_index (curry (op =) U) lives of 587 ~1 => Term.dummy 588 | i => nth sets i); 589 in 590 (T_name, map mk_set Us) 591 end; 592 593fun mk_xtor_co_recs thy fp fpTs Cs ts0 = 594 let 595 val nn = length fpTs; 596 val (fpTs0, Cs0) = 597 map ((fp = Greatest_FP ? swap) o dest_funT o snd o strip_typeN nn o fastype_of) ts0 598 |> split_list; 599 val rho = tvar_subst thy (fpTs0 @ Cs0) (fpTs @ Cs); 600 in 601 map (Term.subst_TVars rho) ts0 602 end; 603 604fun liveness_of_fp_bnf n bnf = 605 (case T_of_bnf bnf of 606 Type (_, Ts) => map (not o member (op =) (deads_of_bnf bnf)) Ts 607 | _ => replicate n false); 608 609fun add_nesting_bnf_names Us = 610 let 611 fun add (Type (s, Ts)) ss = 612 let val (needs, ss') = fold_map add Ts ss in 613 if exists I needs then (true, insert (op =) s ss') else (false, ss') 614 end 615 | add T ss = (member (op =) Us T, ss); 616 in snd oo add end; 617 618fun nesting_bnfs ctxt ctr_Tsss Us = 619 map_filter (bnf_of ctxt) (fold (fold (fold (add_nesting_bnf_names Us))) ctr_Tsss []); 620 621fun indexify proj xs f p = f (find_index (curry (op =) (proj p)) xs) p; 622 623fun massage_simple_notes base = 624 filter_out (null o #2) 625 #> map (fn (thmN, thms, f_attrs) => 626 ((Binding.qualify true base (Binding.name thmN), []), 627 map_index (fn (i, thm) => ([thm], f_attrs i)) thms)); 628 629fun massage_multi_notes b_names Ts = 630 maps (fn (thmN, thmss, attrs) => 631 @{map 3} (fn b_name => fn Type (T_name, _) => fn thms => 632 ((Binding.qualify true b_name (Binding.name thmN), attrs T_name), [(thms, [])])) 633 b_names Ts thmss) 634 #> filter_out (null o fst o hd o snd); 635 636fun define_ctrs_dtrs_for_type fp_b_name fpT ctor dtor ctor_dtor dtor_ctor n ks abs ctr_bindings 637 ctr_mixfixes ctr_Tss lthy = 638 let 639 val ctor_absT = domain_type (fastype_of ctor); 640 641 val (((w, xss), u'), _) = lthy 642 |> yield_singleton (mk_Frees "w") ctor_absT 643 ||>> mk_Freess "x" ctr_Tss 644 ||>> yield_singleton Variable.variant_fixes fp_b_name; 645 646 val u = Free (u', fpT); 647 648 val ctor_iff_dtor_thm = 649 let 650 val goal = 651 fold_rev Logic.all [w, u] 652 (mk_Trueprop_eq (HOLogic.mk_eq (u, ctor $ w), HOLogic.mk_eq (dtor $ u, w))); 653 val vars = Variable.add_free_names lthy goal []; 654 in 655 Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, ...} => 656 mk_ctor_iff_dtor_tac ctxt (map (SOME o Thm.ctyp_of lthy) [ctor_absT, fpT]) 657 (Thm.cterm_of lthy ctor) (Thm.cterm_of lthy dtor) ctor_dtor dtor_ctor) 658 |> Thm.close_derivation \<^here> 659 end; 660 661 val ctr_rhss = 662 map2 (fn k => fn xs => fold_rev Term.lambda xs (ctor $ mk_absumprod ctor_absT abs n k xs)) 663 ks xss; 664 665 val ((raw_ctrs, raw_ctr_defs), (lthy, lthy_old)) = lthy 666 |> Local_Theory.open_target |> snd 667 |> apfst split_list o @{fold_map 3} (fn b => fn mx => fn rhs => 668 Local_Theory.define ((b, mx), 669 ((Thm.make_def_binding (Config.get lthy bnf_internals) b, []), rhs)) 670 #>> apsnd snd) ctr_bindings ctr_mixfixes ctr_rhss 671 ||> `Local_Theory.close_target; 672 673 val phi = Proof_Context.export_morphism lthy_old lthy; 674 675 val ctr_defs = map (Morphism.thm phi) raw_ctr_defs; 676 val ctrs0 = map (Morphism.term phi) raw_ctrs; 677 in 678 ((xss, ctrs0, ctor_iff_dtor_thm, ctr_defs), lthy) 679 end; 680 681fun wrap_ctrs plugins fp discs_sels fp_b_name ctor_inject n ms abs_inject type_definition 682 disc_bindings sel_bindingss sel_default_eqs ctrs0 ctor_iff_dtor_thm ctr_defs lthy = 683 let 684 val sumEN_thm' = unfold_thms lthy @{thms unit_all_eq1} (mk_absumprodE type_definition ms); 685 686 fun exhaust_tac {context = ctxt, prems = _} = 687 mk_exhaust_tac ctxt n ctr_defs ctor_iff_dtor_thm sumEN_thm'; 688 689 val inject_tacss = 690 map2 (fn ctr_def => fn 0 => [] | _ => [fn {context = ctxt, ...} => 691 mk_inject_tac ctxt ctr_def ctor_inject abs_inject]) ctr_defs ms; 692 693 val half_distinct_tacss = 694 map (map (fn (def, def') => fn {context = ctxt, ...} => 695 mk_half_distinct_tac ctxt ctor_inject abs_inject [def, def'])) 696 (mk_half_pairss (`I ctr_defs)); 697 698 val tacss = [exhaust_tac] :: inject_tacss @ half_distinct_tacss; 699 700 fun ctr_spec_of disc_b ctr0 sel_bs = ((disc_b, ctr0), sel_bs); 701 val ctr_specs = @{map 3} ctr_spec_of disc_bindings ctrs0 sel_bindingss; 702 703 val (ctr_sugar as {case_cong, ...}, lthy) = 704 free_constructors (ctr_sugar_kind_of_fp_kind fp) tacss 705 ((((plugins, discs_sels), standard_binding), ctr_specs), sel_default_eqs) lthy; 706 707 val anonymous_notes = 708 [([case_cong], fundefcong_attrs)] 709 |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])])); 710 711 val notes = 712 if Config.get lthy bnf_internals then 713 [(ctor_iff_dtorN, [ctor_iff_dtor_thm], K [])] 714 |> massage_simple_notes fp_b_name 715 else 716 []; 717 in 718 (ctr_sugar, lthy |> Local_Theory.notes (anonymous_notes @ notes) |> snd) 719 end; 720 721fun derive_map_set_rel_pred_thms plugins fp live As Bs C E abs_inverses ctr_defs fp_nesting_set_maps 722 fp_nesting_rel_eq_onps live_nesting_map_id0s live_nesting_set_maps live_nesting_rel_eqs 723 live_nesting_rel_eq_onps fp_nested_rel_eq_onps fp_b_name fp_bnf fp_bnfs fpT ctor ctor_dtor 724 dtor_ctor pre_map_def pre_set_defs pre_rel_def fp_map_thm fp_set_thms fp_rel_thm 725 extra_unfolds_map extra_unfolds_set extra_unfolds_rel ctr_Tss 726 ({casex, case_thms, discs, selss, sel_defs, ctrs, exhaust, exhaust_discs, disc_thmss, sel_thmss, 727 injects, distincts, distinct_discsss, ...} : ctr_sugar) 728 lthy = 729 let 730 val n = length ctr_Tss; 731 val ms = map length ctr_Tss; 732 733 val B_ify_T = Term.typ_subst_atomic (As ~~ Bs); 734 735 val fpBT = B_ify_T fpT; 736 val live_AsBs = filter (op <>) (As ~~ Bs); 737 val live_As = map fst live_AsBs; 738 val fTs = map (op -->) live_AsBs; 739 740 val ((((((((xss, yss), fs), Ps), Rs), ta), tb), thesis), names_lthy) = lthy 741 |> fold (fold Variable.declare_typ) [As, Bs] 742 |> mk_Freess "x" ctr_Tss 743 ||>> mk_Freess "y" (map (map B_ify_T) ctr_Tss) 744 ||>> mk_Frees "f" fTs 745 ||>> mk_Frees "P" (map mk_pred1T live_As) 746 ||>> mk_Frees "R" (map (uncurry mk_pred2T) live_AsBs) 747 ||>> yield_singleton (mk_Frees "a") fpT 748 ||>> yield_singleton (mk_Frees "b") fpBT 749 ||>> apfst HOLogic.mk_Trueprop o yield_singleton (mk_Frees "thesis") HOLogic.boolT; 750 751 val ctrAs = map (mk_ctr As) ctrs; 752 val ctrBs = map (mk_ctr Bs) ctrs; 753 754 val ctr_defs' = 755 map2 (fn m => fn def => mk_unabs_def m (HOLogic.mk_obj_eq def)) ms ctr_defs; 756 757 val ABfs = live_AsBs ~~ fs; 758 759 fun derive_rel_case relAsBs rel_inject_thms rel_distinct_thms = 760 let 761 val rel_Rs_a_b = list_comb (relAsBs, Rs) $ ta $ tb; 762 763 fun mk_assms ctrA ctrB ctxt = 764 let 765 val argA_Ts = binder_types (fastype_of ctrA); 766 val argB_Ts = binder_types (fastype_of ctrB); 767 val ((argAs, argBs), names_ctxt) = ctxt 768 |> mk_Frees "x" argA_Ts 769 ||>> mk_Frees "y" argB_Ts; 770 val ctrA_args = list_comb (ctrA, argAs); 771 val ctrB_args = list_comb (ctrB, argBs); 772 in 773 (fold_rev Logic.all (argAs @ argBs) (Logic.list_implies 774 (mk_Trueprop_eq (ta, ctrA_args) :: mk_Trueprop_eq (tb, ctrB_args) :: 775 map2 (HOLogic.mk_Trueprop oo build_rel_app lthy Rs []) argAs argBs, 776 thesis)), 777 names_ctxt) 778 end; 779 780 val (assms, names_lthy) = @{fold_map 2} mk_assms ctrAs ctrBs names_lthy; 781 val goal = Logic.list_implies (HOLogic.mk_Trueprop rel_Rs_a_b :: assms, thesis); 782 in 783 Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} => 784 mk_rel_case_tac ctxt (Thm.cterm_of ctxt ta) (Thm.cterm_of ctxt tb) exhaust injects 785 rel_inject_thms distincts rel_distinct_thms live_nesting_rel_eqs) 786 |> singleton (Proof_Context.export names_lthy lthy) 787 |> Thm.close_derivation \<^here> 788 end; 789 790 fun derive_case_transfer rel_case_thm = 791 let 792 val (S, names_lthy) = yield_singleton (mk_Frees "S") (mk_pred2T C E) names_lthy; 793 val caseA = mk_case As C casex; 794 val caseB = mk_case Bs E casex; 795 val goal = mk_parametricity_goal names_lthy (S :: Rs) caseA caseB; 796 in 797 Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} => 798 mk_case_transfer_tac ctxt rel_case_thm case_thms) 799 |> singleton (Proof_Context.export names_lthy lthy) 800 |> Thm.close_derivation \<^here> 801 end; 802 in 803 if live = 0 then 804 if plugins transfer_plugin then 805 let 806 val relAsBs = HOLogic.eq_const fpT; 807 val rel_case_thm = derive_rel_case relAsBs [] []; 808 809 val case_transfer_thm = derive_case_transfer rel_case_thm; 810 811 val notes = 812 [(case_transferN, [case_transfer_thm], K [])] 813 |> massage_simple_notes fp_b_name; 814 815 val (noted, lthy') = lthy 816 |> Local_Theory.notes notes; 817 818 val subst = Morphism.thm (substitute_noted_thm noted); 819 in 820 (([], [], [], [], [], [], [], [], [], [], [], [], [], [], [subst case_transfer_thm], [], 821 []), lthy') 822 end 823 else 824 (([], [], [], [], [], [], [], [], [], [], [], [], [], [], [], [], []), lthy) 825 else 826 let 827 val mapx = mk_map live As Bs (map_of_bnf fp_bnf); 828 val relAsBs = mk_rel live As Bs (rel_of_bnf fp_bnf); 829 val setAs = map (mk_set As) (sets_of_bnf fp_bnf); 830 val discAs = map (mk_disc_or_sel As) discs; 831 val discBs = map (mk_disc_or_sel Bs) discs; 832 val selAss = map (map (mk_disc_or_sel As)) selss; 833 val selBss = map (map (mk_disc_or_sel Bs)) selss; 834 835 val map_ctor_thm = 836 if fp = Least_FP then 837 fp_map_thm 838 else 839 let 840 val ctorA = mk_ctor As ctor; 841 val ctorB = mk_ctor Bs ctor; 842 843 val y_T = domain_type (fastype_of ctorA); 844 val (y as Free (y_s, _), _) = lthy 845 |> yield_singleton (mk_Frees "y") y_T; 846 847 val ctor_cong = 848 infer_instantiate' lthy [NONE, NONE, SOME (Thm.cterm_of lthy ctorB)] arg_cong; 849 val fp_map_thm' = fp_map_thm 850 |> infer_instantiate' lthy (replicate live NONE @ 851 [SOME (Thm.cterm_of lthy (ctorA $ y))]) 852 |> unfold_thms lthy [dtor_ctor]; 853 in 854 (fp_map_thm' RS ctor_cong RS (ctor_dtor RS sym RS trans)) 855 |> Drule.generalize ([], [y_s]) 856 end; 857 858 val map_thms = 859 let 860 fun mk_goal ctrA ctrB xs ys = 861 let 862 val fmap = list_comb (mapx, fs); 863 864 fun mk_arg (x as Free (_, T)) (Free (_, U)) = 865 if T = U then x 866 else build_map lthy [] [] (the o AList.lookup (op =) ABfs) (T, U) $ x; 867 868 val xs' = map2 mk_arg xs ys; 869 in 870 mk_Trueprop_eq (fmap $ list_comb (ctrA, xs), list_comb (ctrB, xs')) 871 end; 872 873 val goals = @{map 4} mk_goal ctrAs ctrBs xss yss; 874 val goal = Logic.mk_conjunction_balanced goals; 875 val vars = Variable.add_free_names lthy goal []; 876 in 877 Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => 878 mk_map_tac ctxt abs_inverses pre_map_def map_ctor_thm live_nesting_map_id0s ctr_defs' 879 extra_unfolds_map) 880 |> Thm.close_derivation \<^here> 881 |> Conjunction.elim_balanced (length goals) 882 end; 883 884 val set0_thms = 885 let 886 fun mk_goal A setA ctrA xs = 887 let 888 val sets = map (build_set_app lthy A) 889 (filter (exists_subtype_in [A] o fastype_of) xs); 890 in 891 mk_Trueprop_eq (setA $ list_comb (ctrA, xs), 892 (if null sets then HOLogic.mk_set A [] else Library.foldl1 mk_union sets)) 893 end; 894 895 val goals = 896 @{map 2} (fn live_A => fn setA => map2 (mk_goal live_A setA) ctrAs xss) live_As setAs 897 |> flat; 898 in 899 if null goals then 900 [] 901 else 902 let 903 val goal = Logic.mk_conjunction_balanced goals; 904 val vars = Variable.add_free_names lthy goal []; 905 in 906 Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => 907 mk_set0_tac ctxt abs_inverses pre_set_defs dtor_ctor fp_set_thms 908 fp_nesting_set_maps live_nesting_set_maps ctr_defs' extra_unfolds_set) 909 |> Thm.close_derivation \<^here> 910 |> Conjunction.elim_balanced (length goals) 911 end 912 end; 913 val set_thms = set0_thms 914 |> map (unfold_thms lthy @{thms insert_is_Un[THEN sym] Un_empty_left Un_insert_left}); 915 916 val rel_ctor_thm = 917 if fp = Least_FP then 918 fp_rel_thm 919 else 920 let 921 val ctorA = mk_ctor As ctor; 922 val ctorB = mk_ctor Bs ctor; 923 924 val y_T = domain_type (fastype_of ctorA); 925 val z_T = domain_type (fastype_of ctorB); 926 val ((y as Free (y_s, _), z as Free (z_s, _)), _) = lthy 927 |> yield_singleton (mk_Frees "y") y_T 928 ||>> yield_singleton (mk_Frees "z") z_T; 929 in 930 fp_rel_thm 931 |> infer_instantiate' lthy (replicate live NONE @ 932 [SOME (Thm.cterm_of lthy (ctorA $ y)), SOME (Thm.cterm_of lthy (ctorB $ z))]) 933 |> unfold_thms lthy [dtor_ctor] 934 |> Drule.generalize ([], [y_s, z_s]) 935 end; 936 937 val rel_inject_thms = 938 let 939 fun mk_goal ctrA ctrB xs ys = 940 let 941 val lhs = list_comb (relAsBs, Rs) $ list_comb (ctrA, xs) $ list_comb (ctrB, ys); 942 val conjuncts = map2 (build_rel_app lthy Rs []) xs ys; 943 in 944 HOLogic.mk_Trueprop 945 (if null conjuncts then lhs 946 else HOLogic.mk_eq (lhs, Library.foldr1 HOLogic.mk_conj conjuncts)) 947 end; 948 949 val goals = @{map 4} mk_goal ctrAs ctrBs xss yss; 950 val goal = Logic.mk_conjunction_balanced goals; 951 val vars = Variable.add_free_names lthy goal []; 952 in 953 Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => 954 mk_rel_tac ctxt abs_inverses pre_rel_def rel_ctor_thm live_nesting_rel_eqs ctr_defs' 955 extra_unfolds_rel) 956 |> Thm.close_derivation \<^here> 957 |> Conjunction.elim_balanced (length goals) 958 end; 959 960 val half_rel_distinct_thmss = 961 let 962 fun mk_goal ((ctrA, xs), (ctrB, ys)) = 963 HOLogic.mk_Trueprop (HOLogic.mk_not 964 (list_comb (relAsBs, Rs) $ list_comb (ctrA, xs) $ list_comb (ctrB, ys))); 965 966 val rel_infos = (ctrAs ~~ xss, ctrBs ~~ yss); 967 968 val goalss = map (map mk_goal) (mk_half_pairss rel_infos); 969 val goals = flat goalss; 970 in 971 unflat goalss 972 (if null goals then 973 [] 974 else 975 let 976 val goal = Logic.mk_conjunction_balanced goals; 977 val vars = Variable.add_free_names lthy goal []; 978 in 979 Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => 980 mk_rel_tac ctxt abs_inverses pre_rel_def rel_ctor_thm live_nesting_rel_eqs 981 ctr_defs' extra_unfolds_rel) 982 |> Thm.close_derivation \<^here> 983 |> Conjunction.elim_balanced (length goals) 984 end) 985 end; 986 987 val rel_flip = rel_flip_of_bnf fp_bnf; 988 989 fun mk_other_half_rel_distinct_thm thm = 990 flip_rels lthy live thm RS (rel_flip RS sym RS @{thm arg_cong[of _ _ Not]} RS iffD2); 991 992 val other_half_rel_distinct_thmss = 993 map (map mk_other_half_rel_distinct_thm) half_rel_distinct_thmss; 994 val (rel_distinct_thms, _) = 995 join_halves n half_rel_distinct_thmss other_half_rel_distinct_thmss; 996 997 fun mk_rel_intro_thm m thm = 998 uncurry_thm m (thm RS iffD2) handle THM _ => thm; 999 1000 val rel_intro_thms = map2 mk_rel_intro_thm ms rel_inject_thms; 1001 1002 val rel_code_thms = 1003 map (fn thm => thm RS @{thm eq_False[THEN iffD2]}) rel_distinct_thms @ 1004 map2 (fn thm => fn 0 => thm RS @{thm eq_True[THEN iffD2]} | _ => thm) rel_inject_thms ms; 1005 1006 val ctr_transfer_thms = 1007 let 1008 val goals = map2 (mk_parametricity_goal names_lthy Rs) ctrAs ctrBs; 1009 val goal = Logic.mk_conjunction_balanced goals; 1010 val vars = Variable.add_free_names lthy goal []; 1011 in 1012 Goal.prove_sorry lthy vars [] goal 1013 (fn {context = ctxt, prems = _} => 1014 mk_ctr_transfer_tac ctxt rel_intro_thms live_nesting_rel_eqs) 1015 |> Thm.close_derivation \<^here> 1016 |> Conjunction.elim_balanced (length goals) 1017 end; 1018 1019 val (set_cases_thms, set_cases_attrss) = 1020 let 1021 fun mk_prems assms elem t ctxt = 1022 (case fastype_of t of 1023 Type (type_name, xs) => 1024 (case bnf_of ctxt type_name of 1025 NONE => ([], ctxt) 1026 | SOME bnf => 1027 apfst flat (fold_map (fn set => fn ctxt => 1028 let 1029 val T = HOLogic.dest_setT (range_type (fastype_of set)); 1030 val new_var = not (T = fastype_of elem); 1031 val (x, ctxt') = 1032 if new_var then yield_singleton (mk_Frees "x") T ctxt else (elem, ctxt); 1033 in 1034 mk_prems (mk_Trueprop_mem (x, set $ t) :: assms) elem x ctxt' 1035 |>> map (new_var ? Logic.all x) 1036 end) (map (mk_set xs) (sets_of_bnf bnf)) ctxt)) 1037 | T => rpair ctxt 1038 (if T = fastype_of elem then [fold (curry Logic.mk_implies) assms thesis] else [])); 1039 in 1040 split_list (map (fn set => 1041 let 1042 val A = HOLogic.dest_setT (range_type (fastype_of set)); 1043 val (elem, names_lthy) = yield_singleton (mk_Frees "e") A names_lthy; 1044 val premss = 1045 map (fn ctr => 1046 let 1047 val (args, names_lthy) = 1048 mk_Frees "z" (binder_types (fastype_of ctr)) names_lthy; 1049 in 1050 flat (zipper_map (fn (prev_args, arg, next_args) => 1051 let 1052 val (args_with_elem, args_without_elem) = 1053 if fastype_of arg = A then 1054 (prev_args @ [elem] @ next_args, prev_args @ next_args) 1055 else 1056 `I (prev_args @ [arg] @ next_args); 1057 in 1058 mk_prems [mk_Trueprop_eq (ta, Term.list_comb (ctr, args_with_elem))] 1059 elem arg names_lthy 1060 |> fst 1061 |> map (fold_rev Logic.all args_without_elem) 1062 end) args) 1063 end) ctrAs; 1064 val goal = Logic.mk_implies (mk_Trueprop_mem (elem, set $ ta), thesis); 1065 val vars = Variable.add_free_names lthy goal []; 1066 val thm = 1067 Goal.prove_sorry lthy vars (flat premss) goal (fn {context = ctxt, prems} => 1068 mk_set_cases_tac ctxt (Thm.cterm_of ctxt ta) prems exhaust set_thms) 1069 |> Thm.close_derivation \<^here> 1070 |> rotate_prems ~1; 1071 1072 val cases_set_attr = 1073 Attrib.internal (K (Induct.cases_pred (name_of_set set))); 1074 1075 val ctr_names = quasi_unambiguous_case_names (flat 1076 (map (uncurry mk_names o map_prod length name_of_ctr) (premss ~~ ctrAs))); 1077 in 1078 (* TODO: @{attributes [elim?]} *) 1079 (thm, [Attrib.consumes 1, cases_set_attr, Attrib.case_names ctr_names]) 1080 end) setAs) 1081 end; 1082 1083 val (set_intros_thmssss, set_intros_thms) = 1084 let 1085 fun mk_goals A setA ctr_args t ctxt = 1086 (case fastype_of t of 1087 Type (type_name, innerTs) => 1088 (case bnf_of ctxt type_name of 1089 NONE => ([], ctxt) 1090 | SOME bnf => 1091 apfst flat (fold_map (fn set => fn ctxt => 1092 let 1093 val T = HOLogic.dest_setT (range_type (fastype_of set)); 1094 val (y, ctxt') = yield_singleton (mk_Frees "y") T ctxt; 1095 val assm = mk_Trueprop_mem (y, set $ t); 1096 in 1097 apfst (map (Logic.mk_implies o pair assm)) (mk_goals A setA ctr_args y ctxt') 1098 end) (map (mk_set innerTs) (sets_of_bnf bnf)) ctxt)) 1099 | T => (if T = A then [mk_Trueprop_mem (t, setA $ ctr_args)] else [], ctxt)); 1100 1101 val (goalssss, _) = 1102 fold_map (fn set => 1103 let val A = HOLogic.dest_setT (range_type (fastype_of set)) in 1104 @{fold_map 2} (fn ctr => fn xs => 1105 fold_map (mk_goals A set (Term.list_comb (ctr, xs))) xs) 1106 ctrAs xss 1107 end) setAs lthy; 1108 val goals = flat (flat (flat goalssss)); 1109 in 1110 `(unflattt goalssss) 1111 (if null goals then 1112 [] 1113 else 1114 let 1115 val goal = Logic.mk_conjunction_balanced goals; 1116 val vars = Variable.add_free_names lthy goal []; 1117 in 1118 Goal.prove_sorry lthy vars [] goal 1119 (fn {context = ctxt, prems = _} => mk_set_intros_tac ctxt set0_thms) 1120 |> Thm.close_derivation \<^here> 1121 |> Conjunction.elim_balanced (length goals) 1122 end) 1123 end; 1124 1125 val rel_sel_thms = 1126 let 1127 val n = length discAs; 1128 fun mk_conjunct n k discA selAs discB selBs = 1129 (if k = n then [] else [HOLogic.mk_eq (discA $ ta, discB $ tb)]) @ 1130 (if null selAs then 1131 [] 1132 else 1133 [Library.foldr HOLogic.mk_imp 1134 (if n = 1 then [] else [discA $ ta, discB $ tb], 1135 Library.foldr1 HOLogic.mk_conj (map2 (build_rel_app names_lthy Rs []) 1136 (map (rapp ta) selAs) (map (rapp tb) selBs)))]); 1137 1138 val goals = 1139 if n = 0 then 1140 [] 1141 else 1142 [mk_Trueprop_eq (build_rel_app names_lthy Rs [] ta tb, 1143 (case flat (@{map 5} (mk_conjunct n) (1 upto n) discAs selAss discBs selBss) of 1144 [] => \<^term>\<open>True\<close> 1145 | conjuncts => Library.foldr1 HOLogic.mk_conj conjuncts))]; 1146 1147 fun prove goal = 1148 Variable.add_free_names lthy goal [] 1149 |> (fn vars => Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => 1150 mk_rel_sel_tac ctxt (Thm.cterm_of ctxt ta) (Thm.cterm_of ctxt tb) exhaust 1151 (flat disc_thmss) (flat sel_thmss) rel_inject_thms distincts rel_distinct_thms 1152 live_nesting_rel_eqs)) 1153 |> Thm.close_derivation \<^here>; 1154 in 1155 map prove goals 1156 end; 1157 1158 val (rel_case_thm, rel_case_attrs) = 1159 let 1160 val thm = derive_rel_case relAsBs rel_inject_thms rel_distinct_thms; 1161 val ctr_names = quasi_unambiguous_case_names (map name_of_ctr ctrAs); 1162 in 1163 (thm, [Attrib.case_names ctr_names, Attrib.consumes 1] @ @{attributes [cases pred]}) 1164 end; 1165 1166 val case_transfer_thm = derive_case_transfer rel_case_thm; 1167 1168 val sel_transfer_thms = 1169 if null selAss then 1170 [] 1171 else 1172 let 1173 val shared_sels = foldl1 (uncurry (inter (op =))) (map (op ~~) (selAss ~~ selBss)); 1174 val goals = map (uncurry (mk_parametricity_goal names_lthy Rs)) shared_sels; 1175 in 1176 if null goals then 1177 [] 1178 else 1179 let 1180 val goal = Logic.mk_conjunction_balanced goals; 1181 val vars = Variable.add_free_names lthy goal []; 1182 in 1183 Goal.prove_sorry lthy vars [] goal 1184 (fn {context = ctxt, prems = _} => 1185 mk_sel_transfer_tac ctxt n sel_defs case_transfer_thm) 1186 |> Thm.close_derivation \<^here> 1187 |> Conjunction.elim_balanced (length goals) 1188 end 1189 end; 1190 1191 val disc_transfer_thms = 1192 let val goals = map2 (mk_parametricity_goal names_lthy Rs) discAs discBs in 1193 if null goals then 1194 [] 1195 else 1196 let 1197 val goal = Logic.mk_conjunction_balanced goals; 1198 val vars = Variable.add_free_names lthy goal []; 1199 in 1200 Goal.prove_sorry lthy vars [] goal 1201 (fn {context = ctxt, prems = _} => mk_disc_transfer_tac ctxt 1202 (the_single rel_sel_thms) (the_single exhaust_discs) 1203 (flat (flat distinct_discsss))) 1204 |> Thm.close_derivation \<^here> 1205 |> Conjunction.elim_balanced (length goals) 1206 end 1207 end; 1208 1209 val map_disc_iff_thms = 1210 let 1211 val discsB = map (mk_disc_or_sel Bs) discs; 1212 val discsA_t = map (fn disc1 => Term.betapply (disc1, ta)) discAs; 1213 1214 fun mk_goal (discA_t, discB) = 1215 if head_of discA_t aconv HOLogic.Not orelse is_refl_bool discA_t then 1216 NONE 1217 else 1218 SOME (mk_Trueprop_eq (betapply (discB, (Term.list_comb (mapx, fs) $ ta)), discA_t)); 1219 1220 val goals = map_filter mk_goal (discsA_t ~~ discsB); 1221 in 1222 if null goals then 1223 [] 1224 else 1225 let 1226 val goal = Logic.mk_conjunction_balanced goals; 1227 val vars = Variable.add_free_names lthy goal []; 1228 in 1229 Goal.prove_sorry lthy vars [] goal 1230 (fn {context = ctxt, prems = _} => 1231 mk_map_disc_iff_tac ctxt (Thm.cterm_of ctxt ta) exhaust (flat disc_thmss) 1232 map_thms) 1233 |> Thm.close_derivation \<^here> 1234 |> Conjunction.elim_balanced (length goals) 1235 end 1236 end; 1237 1238 val (map_sel_thmss, map_sel_thms) = 1239 let 1240 fun mk_goal discA selA selB = 1241 let 1242 val prem = Term.betapply (discA, ta); 1243 val lhs = selB $ (Term.list_comb (mapx, fs) $ ta); 1244 val lhsT = fastype_of lhs; 1245 val map_rhsT = 1246 map_atyps (perhaps (AList.lookup (op =) (map swap live_AsBs))) lhsT; 1247 val map_rhs = build_map lthy [] [] 1248 (the o (AList.lookup (op =) (live_AsBs ~~ fs))) (map_rhsT, lhsT); 1249 val rhs = (case map_rhs of 1250 Const (\<^const_name>\<open>id\<close>, _) => selA $ ta 1251 | _ => map_rhs $ (selA $ ta)); 1252 val concl = mk_Trueprop_eq (lhs, rhs); 1253 in 1254 if is_refl_bool prem then concl 1255 else Logic.mk_implies (HOLogic.mk_Trueprop prem, concl) 1256 end; 1257 1258 val goalss = @{map 3} (map2 o mk_goal) discAs selAss selBss; 1259 val goals = flat goalss; 1260 in 1261 `(unflat goalss) 1262 (if null goals then 1263 [] 1264 else 1265 let 1266 val goal = Logic.mk_conjunction_balanced goals; 1267 val vars = Variable.add_free_names lthy goal []; 1268 in 1269 Goal.prove_sorry lthy vars [] goal 1270 (fn {context = ctxt, prems = _} => 1271 mk_map_sel_tac ctxt (Thm.cterm_of ctxt ta) exhaust (flat disc_thmss) 1272 map_thms (flat sel_thmss) live_nesting_map_id0s) 1273 |> Thm.close_derivation \<^here> 1274 |> Conjunction.elim_balanced (length goals) 1275 end) 1276 end; 1277 1278 val (set_sel_thmssss, set_sel_thms) = 1279 let 1280 fun mk_goal setA discA selA ctxt = 1281 let 1282 val prem = Term.betapply (discA, ta); 1283 val sel_rangeT = range_type (fastype_of selA); 1284 val A = HOLogic.dest_setT (range_type (fastype_of setA)); 1285 1286 fun travese_nested_types t ctxt = 1287 (case fastype_of t of 1288 Type (type_name, innerTs) => 1289 (case bnf_of ctxt type_name of 1290 NONE => ([], ctxt) 1291 | SOME bnf => 1292 let 1293 fun seq_assm a set ctxt = 1294 let 1295 val T = HOLogic.dest_setT (range_type (fastype_of set)); 1296 val (x, ctxt') = yield_singleton (mk_Frees "x") T ctxt; 1297 val assm = mk_Trueprop_mem (x, set $ a); 1298 in 1299 travese_nested_types x ctxt' 1300 |>> map (Logic.mk_implies o pair assm) 1301 end; 1302 in 1303 fold_map (seq_assm t o mk_set innerTs) (sets_of_bnf bnf) ctxt 1304 |>> flat 1305 end) 1306 | T => 1307 if T = A then ([mk_Trueprop_mem (t, setA $ ta)], ctxt) else ([], ctxt)); 1308 1309 val (concls, ctxt') = 1310 if sel_rangeT = A then ([mk_Trueprop_mem (selA $ ta, setA $ ta)], ctxt) 1311 else travese_nested_types (selA $ ta) ctxt; 1312 in 1313 if exists_subtype_in [A] sel_rangeT then 1314 if is_refl_bool prem then (concls, ctxt') 1315 else (map (Logic.mk_implies o pair (HOLogic.mk_Trueprop prem)) concls, ctxt') 1316 else 1317 ([], ctxt) 1318 end; 1319 1320 val (goalssss, _) = 1321 fold_map (fn set => @{fold_map 2} (fold_map o mk_goal set) discAs selAss) 1322 setAs names_lthy; 1323 val goals = flat (flat (flat goalssss)); 1324 in 1325 `(unflattt goalssss) 1326 (if null goals then 1327 [] 1328 else 1329 let 1330 val goal = Logic.mk_conjunction_balanced goals; 1331 val vars = Variable.add_free_names lthy goal []; 1332 in 1333 Goal.prove_sorry lthy vars [] goal 1334 (fn {context = ctxt, prems = _} => 1335 mk_set_sel_tac ctxt (Thm.cterm_of ctxt ta) exhaust (flat disc_thmss) 1336 (flat sel_thmss) set0_thms) 1337 |> Thm.close_derivation \<^here> 1338 |> Conjunction.elim_balanced (length goals) 1339 end) 1340 end; 1341 1342 val pred_injects = 1343 let 1344 fun top_sweep_rewr_conv rewrs = 1345 Conv.top_sweep_conv (K (Conv.rewrs_conv rewrs)) \<^context>; 1346 1347 val rel_eq_onp_with_tops_of = Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.arg1_conv 1348 (top_sweep_rewr_conv @{thms eq_onp_top_eq_eq[symmetric, THEN eq_reflection]}))); 1349 1350 val eq_onps = map rel_eq_onp_with_tops_of 1351 (map rel_eq_onp_of_bnf fp_bnfs @ fp_nesting_rel_eq_onps @ live_nesting_rel_eq_onps @ 1352 fp_nested_rel_eq_onps); 1353 val cTs = map (SOME o Thm.ctyp_of lthy) (maps (replicate 2) live_As); 1354 val cts = map (SOME o Thm.cterm_of lthy) (map mk_eq_onp Ps); 1355 1356 val get_rhs = Thm.concl_of #> HOLogic.dest_Trueprop #> HOLogic.dest_eq #> snd; 1357 1358 val pred_eq_onp_conj = 1359 List.foldr (fn (_, thm) => thm RS @{thm eq_onp_live_step}) @{thm refl[of True]}; 1360 1361 fun predify_rel_inject rel_inject = 1362 let 1363 val conjuncts = try (get_rhs #> HOLogic.dest_conj) rel_inject |> the_default []; 1364 1365 fun postproc thm = 1366 if null conjuncts then 1367 thm RS (@{thm eq_onp_same_args} RS iffD1) 1368 else 1369 @{thm box_equals} OF [thm, @{thm eq_onp_same_args}, 1370 pred_eq_onp_conj conjuncts |> unfold_thms lthy @{thms simp_thms(21)}]; 1371 in 1372 rel_inject 1373 |> Thm.instantiate' cTs cts 1374 |> Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.arg_conv 1375 (Raw_Simplifier.rewrite lthy false 1376 @{thms eq_onp_top_eq_eq[symmetric, THEN eq_reflection]}))) 1377 |> unfold_thms lthy eq_onps 1378 |> postproc 1379 |> unfold_thms lthy @{thms top_conj} 1380 end; 1381 in 1382 rel_inject_thms 1383 |> map (unfold_thms lthy [@{thm conj_assoc}]) 1384 |> map predify_rel_inject 1385 |> Proof_Context.export names_lthy lthy 1386 end; 1387 1388 val anonymous_notes = 1389 [(rel_code_thms, nitpicksimp_attrs)] 1390 |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])])); 1391 1392 val notes = 1393 (if Config.get lthy bnf_internals then 1394 [(set0N, set0_thms, K [])] 1395 else 1396 []) @ 1397 [(case_transferN, [case_transfer_thm], K []), 1398 (ctr_transferN, ctr_transfer_thms, K []), 1399 (disc_transferN, disc_transfer_thms, K []), 1400 (sel_transferN, sel_transfer_thms, K []), 1401 (mapN, map_thms, K (nitpicksimp_attrs @ simp_attrs)), 1402 (map_disc_iffN, map_disc_iff_thms, K simp_attrs), 1403 (map_selN, map_sel_thms, K []), 1404 (pred_injectN, pred_injects, K simp_attrs), 1405 (rel_casesN, [rel_case_thm], K rel_case_attrs), 1406 (rel_distinctN, rel_distinct_thms, K simp_attrs), 1407 (rel_injectN, rel_inject_thms, K simp_attrs), 1408 (rel_introsN, rel_intro_thms, K []), 1409 (rel_selN, rel_sel_thms, K []), 1410 (setN, set_thms, K (case_fp fp nitpicksimp_attrs [] @ simp_attrs)), 1411 (set_casesN, set_cases_thms, nth set_cases_attrss), 1412 (set_introsN, set_intros_thms, K []), 1413 (set_selN, set_sel_thms, K [])] 1414 |> massage_simple_notes fp_b_name; 1415 1416 val (noted, lthy') = lthy 1417 |> uncurry (Spec_Rules.add Binding.empty Spec_Rules.equational) 1418 (`(single o lhs_head_of o hd) map_thms) 1419 |> fp = Least_FP ? 1420 uncurry (Spec_Rules.add Binding.empty Spec_Rules.equational) 1421 (`(single o lhs_head_of o hd) rel_code_thms) 1422 |> uncurry (Spec_Rules.add Binding.empty Spec_Rules.equational) 1423 (`(single o lhs_head_of o hd) set0_thms) 1424 |> plugins code_plugin ? Code.declare_default_eqns (map (rpair true) (rel_code_thms @ map_thms @ set_thms)) 1425 |> Local_Theory.notes (anonymous_notes @ notes); 1426 1427 val subst = Morphism.thm (substitute_noted_thm noted); 1428 in 1429 ((map subst map_thms, 1430 map subst map_disc_iff_thms, 1431 map (map subst) map_sel_thmss, 1432 map subst rel_inject_thms, 1433 map subst rel_distinct_thms, 1434 map subst rel_sel_thms, 1435 map subst rel_intro_thms, 1436 [subst rel_case_thm], 1437 map subst pred_injects, 1438 map subst set_thms, 1439 map (map (map (map subst))) set_sel_thmssss, 1440 map (map (map (map subst))) set_intros_thmssss, 1441 map subst set_cases_thms, 1442 map subst ctr_transfer_thms, 1443 [subst case_transfer_thm], 1444 map subst disc_transfer_thms, 1445 map subst sel_transfer_thms), lthy') 1446 end 1447 end; 1448 1449type lfp_sugar_thms = (thm list * thm * Token.src list) * (thm list list * Token.src list); 1450 1451fun morph_lfp_sugar_thms phi ((inducts, induct, induct_attrs), (recss, rec_attrs)) = 1452 ((map (Morphism.thm phi) inducts, Morphism.thm phi induct, induct_attrs), 1453 (map (map (Morphism.thm phi)) recss, rec_attrs)) : lfp_sugar_thms; 1454 1455val transfer_lfp_sugar_thms = morph_lfp_sugar_thms o Morphism.transfer_morphism; 1456 1457type gfp_sugar_thms = 1458 ((thm list * thm) list * (Token.src list * Token.src list)) 1459 * thm list list 1460 * thm list list 1461 * (thm list list * Token.src list) 1462 * (thm list list list * Token.src list); 1463 1464fun morph_gfp_sugar_thms phi ((coinducts_pairs, coinduct_attrs_pair), 1465 corecss, corec_discss, (corec_disc_iffss, corec_disc_iff_attrs), 1466 (corec_selsss, corec_sel_attrs)) = 1467 ((map (apfst (map (Morphism.thm phi)) o apsnd (Morphism.thm phi)) coinducts_pairs, 1468 coinduct_attrs_pair), 1469 map (map (Morphism.thm phi)) corecss, 1470 map (map (Morphism.thm phi)) corec_discss, 1471 (map (map (Morphism.thm phi)) corec_disc_iffss, corec_disc_iff_attrs), 1472 (map (map (map (Morphism.thm phi))) corec_selsss, corec_sel_attrs)) : gfp_sugar_thms; 1473 1474val transfer_gfp_sugar_thms = morph_gfp_sugar_thms o Morphism.transfer_morphism; 1475 1476fun unzip_recT (Type (\<^type_name>\<open>prod\<close>, [_, TFree x])) 1477 (T as Type (\<^type_name>\<open>prod\<close>, Ts as [_, TFree y])) = 1478 if x = y then [T] else Ts 1479 | unzip_recT _ (Type (\<^type_name>\<open>prod\<close>, Ts as [_, TFree _])) = Ts 1480 | unzip_recT _ T = [T]; 1481 1482fun mk_recs_args_types ctxt ctr_Tsss Cs absTs repTs ns mss ctor_rec_fun_Ts = 1483 let 1484 val Css = map2 replicate ns Cs; 1485 val x_Tssss = 1486 @{map 6} (fn absT => fn repT => fn n => fn ms => fn ctr_Tss => fn ctor_rec_fun_T => 1487 map2 (map2 unzip_recT) 1488 ctr_Tss (dest_absumprodT absT repT n ms (domain_type ctor_rec_fun_T))) 1489 absTs repTs ns mss ctr_Tsss ctor_rec_fun_Ts; 1490 1491 val x_Tsss' = map (map flat_rec_arg_args) x_Tssss; 1492 val f_Tss = map2 (map2 (curry (op --->))) x_Tsss' Css; 1493 1494 val ((fss, xssss), _) = ctxt 1495 |> mk_Freess "f" f_Tss 1496 ||>> mk_Freessss "x" x_Tssss; 1497 in 1498 (f_Tss, x_Tssss, fss, xssss) 1499 end; 1500 1501fun unzip_corecT (Type (\<^type_name>\<open>sum\<close>, _)) T = [T] 1502 | unzip_corecT _ (Type (\<^type_name>\<open>sum\<close>, Ts)) = Ts 1503 | unzip_corecT _ T = [T]; 1504 1505(*avoid "'a itself" arguments in corecursors*) 1506fun repair_nullary_single_ctr [[]] = [[HOLogic.unitT]] 1507 | repair_nullary_single_ctr Tss = Tss; 1508 1509fun mk_corec_fun_arg_types0 ctr_Tsss Cs absTs repTs ns mss fun_Ts = 1510 let 1511 val ctr_Tsss' = map repair_nullary_single_ctr ctr_Tsss; 1512 val g_absTs = map range_type fun_Ts; 1513 val g_Tsss = 1514 map repair_nullary_single_ctr (@{map 5} dest_absumprodT absTs repTs ns mss g_absTs); 1515 val g_Tssss = @{map 3} (fn C => map2 (map2 (map (curry (op -->) C) oo unzip_corecT))) 1516 Cs ctr_Tsss' g_Tsss; 1517 val q_Tssss = map (map (map (fn [_] => [] | [_, T] => [mk_pred1T (domain_type T)]))) g_Tssss; 1518 in 1519 (q_Tssss, g_Tsss, g_Tssss, g_absTs) 1520 end; 1521 1522fun mk_corec_p_pred_types Cs ns = map2 (fn n => replicate (Int.max (0, n - 1)) o mk_pred1T) ns Cs; 1523 1524fun mk_corec_fun_arg_types ctr_Tsss Cs absTs repTs ns mss dtor_corec = 1525 (mk_corec_p_pred_types Cs ns, 1526 mk_corec_fun_arg_types0 ctr_Tsss Cs absTs repTs ns mss 1527 (binder_fun_types (fastype_of dtor_corec))); 1528 1529fun mk_corecs_args_types ctxt ctr_Tsss Cs absTs repTs ns mss dtor_corec_fun_Ts = 1530 let 1531 val p_Tss = mk_corec_p_pred_types Cs ns; 1532 1533 val (q_Tssss, g_Tsss, g_Tssss, corec_types) = 1534 mk_corec_fun_arg_types0 ctr_Tsss Cs absTs repTs ns mss dtor_corec_fun_Ts; 1535 1536 val (((((Free (x, _), cs), pss), qssss), gssss), _) = ctxt 1537 |> yield_singleton (mk_Frees "x") dummyT 1538 ||>> mk_Frees "a" Cs 1539 ||>> mk_Freess "p" p_Tss 1540 ||>> mk_Freessss "q" q_Tssss 1541 ||>> mk_Freessss "g" g_Tssss; 1542 1543 val cpss = map2 (map o rapp) cs pss; 1544 1545 fun build_sum_inj mk_inj = build_map ctxt [] [] (uncurry mk_inj o dest_sumT o snd); 1546 1547 fun build_dtor_corec_arg _ [] [cg] = cg 1548 | build_dtor_corec_arg T [cq] [cg, cg'] = 1549 mk_If cq (build_sum_inj Inl_const (fastype_of cg, T) $ cg) 1550 (build_sum_inj Inr_const (fastype_of cg', T) $ cg'); 1551 1552 val pgss = @{map 3} flat_corec_preds_predsss_gettersss pss qssss gssss; 1553 val cqssss = map2 (map o map o map o rapp) cs qssss; 1554 val cgssss = map2 (map o map o map o rapp) cs gssss; 1555 val cqgsss = @{map 3} (@{map 3} (@{map 3} build_dtor_corec_arg)) g_Tsss cqssss cgssss; 1556 in 1557 (x, cs, cpss, (((pgss, pss, qssss, gssss), cqgsss), corec_types)) 1558 end; 1559 1560fun mk_co_recs_prelims ctxt fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_recs0 = 1561 let 1562 val thy = Proof_Context.theory_of ctxt; 1563 1564 val (xtor_co_rec_fun_Ts, xtor_co_recs) = 1565 mk_xtor_co_recs thy fp fpTs Cs xtor_co_recs0 |> `(binder_fun_types o fastype_of o hd); 1566 1567 val (recs_args_types, corecs_args_types) = 1568 if fp = Least_FP then 1569 mk_recs_args_types ctxt ctr_Tsss Cs absTs repTs ns mss xtor_co_rec_fun_Ts 1570 |> (rpair NONE o SOME) 1571 else 1572 mk_corecs_args_types ctxt ctr_Tsss Cs absTs repTs ns mss xtor_co_rec_fun_Ts 1573 |> (pair NONE o SOME); 1574 in 1575 (xtor_co_recs, recs_args_types, corecs_args_types) 1576 end; 1577 1578fun mk_preds_getterss_join c cps absT abs cqgss = 1579 let 1580 val n = length cqgss; 1581 val ts = map2 (mk_absumprod absT abs n) (1 upto n) cqgss; 1582 in 1583 Term.lambda c (mk_IfN absT cps ts) 1584 end; 1585 1586fun define_co_rec_as fp Cs fpT b rhs lthy0 = 1587 let 1588 val thy = Proof_Context.theory_of lthy0; 1589 1590 val ((cst, (_, def)), (lthy', lthy)) = lthy0 1591 |> Local_Theory.open_target |> snd 1592 |> Local_Theory.define 1593 ((b, NoSyn), ((Thm.make_def_binding (Config.get lthy0 bnf_internals) b, []), rhs)) 1594 ||> `Local_Theory.close_target; 1595 1596 val phi = Proof_Context.export_morphism lthy lthy'; 1597 1598 val cst' = mk_co_rec thy fp Cs fpT (Morphism.term phi cst); 1599 val def' = Morphism.thm phi def; 1600 in 1601 ((cst', def'), lthy') 1602 end; 1603 1604fun define_rec (_, _, fss, xssss) mk_binding fpTs Cs reps ctor_rec = 1605 let 1606 val nn = length fpTs; 1607 val (ctor_rec_absTs, fpT) = strip_typeN nn (fastype_of ctor_rec) 1608 |>> map domain_type ||> domain_type; 1609 in 1610 define_co_rec_as Least_FP Cs fpT (mk_binding recN) 1611 (fold_rev (fold_rev Term.lambda) fss (Term.list_comb (ctor_rec, 1612 @{map 4} (fn ctor_rec_absT => fn rep => fn fs => fn xsss => 1613 mk_case_absumprod ctor_rec_absT rep fs (map (map HOLogic.mk_tuple) xsss) 1614 (map flat_rec_arg_args xsss)) 1615 ctor_rec_absTs reps fss xssss))) 1616 end; 1617 1618fun define_corec (_, cs, cpss, (((pgss, _, _, _), cqgsss), f_absTs)) mk_binding fpTs Cs abss 1619 dtor_corec = 1620 let 1621 val nn = length fpTs; 1622 val fpT = range_type (snd (strip_typeN nn (fastype_of dtor_corec))); 1623 in 1624 define_co_rec_as Greatest_FP Cs fpT (mk_binding corecN) 1625 (fold_rev (fold_rev Term.lambda) pgss (Term.list_comb (dtor_corec, 1626 @{map 5} mk_preds_getterss_join cs cpss f_absTs abss cqgsss))) 1627 end; 1628 1629fun mk_induct_raw_prem_prems names_ctxt Xss setss_fp_nesting (x as Free (s, Type (T_name, Ts0))) 1630 (Type (_, Xs_Ts0)) = 1631 (case AList.lookup (op =) setss_fp_nesting T_name of 1632 NONE => [] 1633 | SOME raw_sets0 => 1634 let 1635 val (Xs_Ts, (Ts, raw_sets)) = 1636 filter (exists_subtype_in (flat Xss) o fst) (Xs_Ts0 ~~ (Ts0 ~~ raw_sets0)) 1637 |> split_list ||> split_list; 1638 val sets = map (mk_set Ts0) raw_sets; 1639 val (ys, names_ctxt') = names_ctxt |> mk_Frees s Ts; 1640 val xysets = map (pair x) (ys ~~ sets); 1641 val ppremss = map2 (mk_induct_raw_prem_prems names_ctxt' Xss setss_fp_nesting) ys Xs_Ts; 1642 in 1643 flat (map2 (map o apfst o cons) xysets ppremss) 1644 end) 1645 | mk_induct_raw_prem_prems _ Xss _ (x as Free (_, Type _)) X = 1646 [([], (find_index (fn Xs => member (op =) Xs X) Xss + 1, x))] 1647 | mk_induct_raw_prem_prems _ _ _ _ _ = []; 1648 1649fun mk_induct_raw_prem alter_x names_ctxt Xss setss_fp_nesting p ctr ctr_Ts ctrXs_Ts = 1650 let 1651 val (xs, names_ctxt') = names_ctxt |> mk_Frees "x" ctr_Ts; 1652 val pprems = 1653 flat (map2 (mk_induct_raw_prem_prems names_ctxt' Xss setss_fp_nesting) xs ctrXs_Ts); 1654 val y = Term.list_comb (ctr, map alter_x xs); 1655 val p' = enforce_type names_ctxt domain_type (fastype_of y) p; 1656 in (xs, pprems, HOLogic.mk_Trueprop (p' $ y)) end; 1657 1658fun close_induct_prem_prem nn ps xs t = 1659 fold_rev Logic.all (map Free (drop (nn + length xs) 1660 (rev (Term.add_frees t (map dest_Free xs @ map_filter (try dest_Free) ps))))) t; 1661 1662fun finish_induct_prem_prem ctxt nn ps xs (xysets, (j, x)) = 1663 let val p' = enforce_type ctxt domain_type (fastype_of x) (nth ps (j - 1)) in 1664 close_induct_prem_prem nn ps xs (Logic.list_implies (map (fn (x', (y, set)) => 1665 mk_Trueprop_mem (y, set $ x')) xysets, 1666 HOLogic.mk_Trueprop (p' $ x))) 1667 end; 1668 1669fun finish_induct_prem ctxt nn ps (xs, raw_pprems, concl) = 1670 fold_rev Logic.all xs (Logic.list_implies 1671 (map (finish_induct_prem_prem ctxt nn ps xs) raw_pprems, concl)); 1672 1673fun mk_coinduct_prem_ctr_concls ctxt Xss fpTss rs' n k udisc usels vdisc vsels ctrXs_Ts = 1674 let 1675 fun build_the_rel T Xs_T = 1676 build_rel [] ctxt [] [] (fn (T, X) => 1677 nth rs' (find_index (fn Xs => member (op =) Xs X) Xss) 1678 |> enforce_type ctxt domain_type T) 1679 (T, Xs_T) 1680 |> Term.subst_atomic_types (flat Xss ~~ flat fpTss); 1681 fun build_rel_app usel vsel Xs_T = 1682 fold rapp [usel, vsel] (build_the_rel (fastype_of usel) Xs_T); 1683 in 1684 (if k = n then [] else [HOLogic.mk_eq (udisc, vdisc)]) @ 1685 (if null usels then 1686 [] 1687 else 1688 [Library.foldr HOLogic.mk_imp (if n = 1 then [] else [udisc, vdisc], 1689 Library.foldr1 HOLogic.mk_conj (@{map 3} build_rel_app usels vsels ctrXs_Ts))]) 1690 end; 1691 1692fun mk_coinduct_prem_concl ctxt Xss fpTss rs' n udiscs uselss vdiscs vselss ctrXs_Tss = 1693 @{map 6} (mk_coinduct_prem_ctr_concls ctxt Xss fpTss rs' n) 1694 (1 upto n) udiscs uselss vdiscs vselss ctrXs_Tss 1695 |> flat |> Library.foldr1 HOLogic.mk_conj 1696 handle List.Empty => \<^term>\<open>True\<close>; 1697 1698fun mk_coinduct_prem ctxt Xss fpTss rs' uvr u v n udiscs uselss vdiscs vselss ctrXs_Tss = 1699 fold_rev Logic.all [u, v] (Logic.mk_implies (HOLogic.mk_Trueprop uvr, 1700 HOLogic.mk_Trueprop (mk_coinduct_prem_concl ctxt Xss fpTss rs' n udiscs uselss vdiscs vselss 1701 ctrXs_Tss))); 1702 1703fun postproc_co_induct ctxt nn prop prop_conj = 1704 Drule.zero_var_indexes 1705 #> `(conj_dests nn) 1706 #>> map (fn thm => Thm.permute_prems 0 ~1 (thm RS prop)) 1707 ##> (fn thm => Thm.permute_prems 0 (~ nn) 1708 (if nn = 1 then thm RS prop 1709 else funpow nn (fn thm => unfold_thms ctxt @{thms conj_assoc} (thm RS prop_conj)) thm)); 1710 1711fun mk_induct_attrs ctrss = 1712 let val induct_cases = quasi_unambiguous_case_names (maps (map name_of_ctr) ctrss); 1713 in [Attrib.case_names induct_cases] end; 1714 1715fun derive_rel_induct_thms_for_types ctxt nn fpA_Ts As Bs ctrAss ctrAs_Tsss exhausts ctor_rel_induct 1716 ctor_defss ctor_injects pre_rel_defs abs_inverses live_nesting_rel_eqs = 1717 let 1718 val B_ify_T = Term.typ_subst_atomic (As ~~ Bs); 1719 val B_ify = Term.map_types B_ify_T; 1720 1721 val fpB_Ts = map B_ify_T fpA_Ts; 1722 val ctrBs_Tsss = map (map (map B_ify_T)) ctrAs_Tsss; 1723 val ctrBss = map (map B_ify) ctrAss; 1724 1725 val ((((Rs, IRs), ctrAsss), ctrBsss), names_ctxt) = ctxt 1726 |> mk_Frees "R" (map2 mk_pred2T As Bs) 1727 ||>> mk_Frees "IR" (map2 mk_pred2T fpA_Ts fpB_Ts) 1728 ||>> mk_Freesss "a" ctrAs_Tsss 1729 ||>> mk_Freesss "b" ctrBs_Tsss; 1730 1731 val prems = 1732 let 1733 fun mk_prem ctrA ctrB argAs argBs = 1734 fold_rev Logic.all (argAs @ argBs) (fold_rev (curry Logic.mk_implies) 1735 (map2 (HOLogic.mk_Trueprop oo build_rel_app names_ctxt (Rs @ IRs) fpA_Ts) argAs argBs) 1736 (HOLogic.mk_Trueprop (build_rel_app names_ctxt (Rs @ IRs) fpA_Ts 1737 (Term.list_comb (ctrA, argAs)) (Term.list_comb (ctrB, argBs))))); 1738 in 1739 flat (@{map 4} (@{map 4} mk_prem) ctrAss ctrBss ctrAsss ctrBsss) 1740 end; 1741 1742 val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 mk_leq 1743 (map2 (build_the_rel ctxt (Rs @ IRs) []) fpA_Ts fpB_Ts) IRs)); 1744 val vars = Variable.add_free_names ctxt goal []; 1745 1746 val rel_induct0_thm = 1747 Goal.prove_sorry ctxt vars prems goal (fn {context = ctxt, prems} => 1748 mk_rel_induct0_tac ctxt ctor_rel_induct prems (map (Thm.cterm_of ctxt) IRs) exhausts 1749 ctor_defss ctor_injects pre_rel_defs abs_inverses live_nesting_rel_eqs) 1750 |> Thm.close_derivation \<^here>; 1751 in 1752 (postproc_co_induct ctxt nn @{thm predicate2D} @{thm predicate2D_conj} rel_induct0_thm, 1753 mk_induct_attrs ctrAss) 1754 end; 1755 1756fun derive_induct_recs_thms_for_types plugins pre_bnfs rec_args_typess ctor_induct ctor_rec_thms 1757 live_nesting_bnfs fp_nesting_bnfs fpTs Cs Xs ctrXs_Tsss pre_abs_inverses pre_type_definitions 1758 abs_inverses ctrss ctr_defss recs rec_defs ctxt = 1759 let 1760 val ctr_Tsss = map (map (binder_types o fastype_of)) ctrss; 1761 1762 val nn = length pre_bnfs; 1763 val ns = map length ctr_Tsss; 1764 val mss = map (map length) ctr_Tsss; 1765 1766 val pre_map_defs = map map_def_of_bnf pre_bnfs; 1767 val pre_set_defss = map set_defs_of_bnf pre_bnfs; 1768 val live_nesting_map_ident0s = map map_ident0_of_bnf live_nesting_bnfs; 1769 val fp_nesting_map_ident0s = map map_ident0_of_bnf fp_nesting_bnfs; 1770 val fp_nesting_set_maps = maps set_map_of_bnf fp_nesting_bnfs; 1771 1772 val fp_b_names = map base_name_of_typ fpTs; 1773 1774 val (((ps, xsss), us'), names_ctxt) = ctxt 1775 |> mk_Frees "P" (map mk_pred1T fpTs) 1776 ||>> mk_Freesss "x" ctr_Tsss 1777 ||>> Variable.variant_fixes fp_b_names; 1778 1779 val us = map2 (curry Free) us' fpTs; 1780 1781 val setss_fp_nesting = map mk_bnf_sets fp_nesting_bnfs; 1782 1783 val (induct_thms, induct_thm) = 1784 let 1785 val raw_premss = @{map 4} (@{map 3} 1786 o mk_induct_raw_prem I names_ctxt (map single Xs) setss_fp_nesting) 1787 ps ctrss ctr_Tsss ctrXs_Tsss; 1788 val concl = 1789 HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 (curry (op $)) ps us)); 1790 val goal = 1791 Library.foldr (Logic.list_implies o apfst (map (finish_induct_prem ctxt nn ps))) 1792 (raw_premss, concl); 1793 val vars = Variable.add_free_names ctxt goal []; 1794 val kksss = map (map (map (fst o snd) o #2)) raw_premss; 1795 1796 val ctor_induct' = ctor_induct OF (map2 mk_absumprodE pre_type_definitions mss); 1797 1798 val thm = 1799 Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, ...} => 1800 mk_induct_tac ctxt nn ns mss kksss (flat ctr_defss) ctor_induct' pre_abs_inverses 1801 abs_inverses fp_nesting_set_maps pre_set_defss) 1802 |> Thm.close_derivation \<^here>; 1803 in 1804 `(conj_dests nn) thm 1805 end; 1806 1807 val xctrss = map2 (map2 (curry Term.list_comb)) ctrss xsss; 1808 1809 fun mk_rec_thmss (_, x_Tssss, fss, _) recs rec_defs ctor_rec_thms = 1810 let 1811 val frecs = map (lists_bmoc fss) recs; 1812 1813 fun mk_goal frec xctr f xs fxs = 1814 fold_rev (fold_rev Logic.all) (xs :: fss) 1815 (mk_Trueprop_eq (frec $ xctr, Term.list_comb (f, fxs))); 1816 1817 fun maybe_tick (T, U) u f = 1818 if try (fst o HOLogic.dest_prodT) U = SOME T then 1819 Term.lambda u (HOLogic.mk_prod (u, f $ u)) 1820 else 1821 f; 1822 1823 fun build_rec (x as Free (_, T)) U = 1824 if T = U then 1825 x 1826 else 1827 let 1828 val build_simple = 1829 indexify (perhaps (try (snd o HOLogic.dest_prodT)) o snd) Cs 1830 (fn kk => fn TU => maybe_tick TU (nth us kk) (nth frecs kk)); 1831 in 1832 build_map ctxt [] [] build_simple (T, U) $ x 1833 end; 1834 1835 val fxsss = map2 (map2 (flat_rec_arg_args oo map2 (map o build_rec))) xsss x_Tssss; 1836 val goalss = @{map 5} (@{map 4} o mk_goal) frecs xctrss fss xsss fxsss; 1837 1838 val tacss = @{map 4} (map ooo 1839 mk_rec_tac pre_map_defs (fp_nesting_map_ident0s @ live_nesting_map_ident0s) rec_defs) 1840 ctor_rec_thms pre_abs_inverses abs_inverses ctr_defss; 1841 1842 fun prove goal tac = 1843 Goal.prove_sorry ctxt [] [] goal (tac o #context) 1844 |> Thm.close_derivation \<^here>; 1845 in 1846 map2 (map2 prove) goalss tacss 1847 end; 1848 1849 val rec_thmss = mk_rec_thmss (the rec_args_typess) recs rec_defs ctor_rec_thms; 1850 1851 in 1852 ((induct_thms, induct_thm, mk_induct_attrs ctrss), 1853 (rec_thmss, nitpicksimp_attrs @ simp_attrs)) 1854 end; 1855 1856fun mk_coinduct_attrs fpTs ctrss discss mss = 1857 let 1858 val fp_b_names = map base_name_of_typ fpTs; 1859 1860 fun mk_coinduct_concls ms discs ctrs = 1861 let 1862 fun mk_disc_concl disc = [name_of_disc disc]; 1863 fun mk_ctr_concl 0 _ = [] 1864 | mk_ctr_concl _ ctr = [name_of_ctr ctr]; 1865 val disc_concls = map mk_disc_concl (fst (split_last discs)) @ [[]]; 1866 val ctr_concls = map2 mk_ctr_concl ms ctrs; 1867 in 1868 flat (map2 append disc_concls ctr_concls) 1869 end; 1870 1871 val coinduct_cases = quasi_unambiguous_case_names (map (prefix Eq_prefix) fp_b_names); 1872 val coinduct_conclss = 1873 @{map 3} (quasi_unambiguous_case_names ooo mk_coinduct_concls) mss discss ctrss; 1874 1875 val coinduct_case_names_attr = Attrib.case_names coinduct_cases; 1876 val coinduct_case_concl_attrs = 1877 map2 (fn casex => fn concls => Attrib.case_conclusion (casex, concls)) 1878 coinduct_cases coinduct_conclss; 1879 1880 val common_coinduct_attrs = coinduct_case_names_attr :: coinduct_case_concl_attrs; 1881 val coinduct_attrs = Attrib.consumes 1 :: coinduct_case_names_attr :: coinduct_case_concl_attrs; 1882 in 1883 (coinduct_attrs, common_coinduct_attrs) 1884 end; 1885 1886fun derive_rel_coinduct_thms_for_types ctxt nn fpA_Ts ns As Bs mss (ctr_sugars : ctr_sugar list) 1887 abs_inverses abs_injects ctor_injects dtor_ctors rel_pre_defs ctor_defss dtor_rel_coinduct 1888 live_nesting_rel_eqs = 1889 let 1890 val B_ify_T = Term.typ_subst_atomic (As ~~ Bs); 1891 val fpB_Ts = map B_ify_T fpA_Ts; 1892 1893 val (Rs, IRs, fpAs, fpBs, _) = 1894 let 1895 val fp_names = map base_name_of_typ fpA_Ts; 1896 val ((((Rs, IRs), fpAs_names), fpBs_names), names_ctxt) = ctxt 1897 |> mk_Frees "R" (map2 mk_pred2T As Bs) 1898 ||>> mk_Frees "IR" (map2 mk_pred2T fpA_Ts fpB_Ts) 1899 ||>> Variable.variant_fixes fp_names 1900 ||>> Variable.variant_fixes (map (suffix "'") fp_names); 1901 in 1902 (Rs, IRs, map2 (curry Free) fpAs_names fpA_Ts, map2 (curry Free) fpBs_names fpB_Ts, 1903 names_ctxt) 1904 end; 1905 1906 val ((discA_tss, selA_tsss), (discB_tss, selB_tsss)) = 1907 let 1908 val discss = map #discs ctr_sugars; 1909 val selsss = map #selss ctr_sugars; 1910 1911 fun mk_discss ts Ts = map2 (map o rapp) ts (map (map (mk_disc_or_sel Ts)) discss); 1912 fun mk_selsss ts Ts = 1913 map2 (map o map o rapp) ts (map (map (map (mk_disc_or_sel Ts))) selsss); 1914 in 1915 ((mk_discss fpAs As, mk_selsss fpAs As), 1916 (mk_discss fpBs Bs, mk_selsss fpBs Bs)) 1917 end; 1918 1919 val prems = 1920 let 1921 fun mk_prem_ctr_concls n k discA_t selA_ts discB_t selB_ts = 1922 (if k = n then [] else [HOLogic.mk_eq (discA_t, discB_t)]) @ 1923 (case (selA_ts, selB_ts) of 1924 ([], []) => [] 1925 | (_ :: _, _ :: _) => 1926 [Library.foldr HOLogic.mk_imp 1927 (if n = 1 then [] else [discA_t, discB_t], 1928 Library.foldr1 HOLogic.mk_conj 1929 (map2 (build_rel_app ctxt (Rs @ IRs) fpA_Ts) selA_ts selB_ts))]); 1930 1931 fun mk_prem_concl n discA_ts selA_tss discB_ts selB_tss = 1932 Library.foldr1 HOLogic.mk_conj (flat (@{map 5} (mk_prem_ctr_concls n) 1933 (1 upto n) discA_ts selA_tss discB_ts selB_tss)) 1934 handle List.Empty => \<^term>\<open>True\<close>; 1935 1936 fun mk_prem IR tA tB n discA_ts selA_tss discB_ts selB_tss = 1937 fold_rev Logic.all [tA, tB] (Logic.mk_implies (HOLogic.mk_Trueprop (IR $ tA $ tB), 1938 HOLogic.mk_Trueprop (mk_prem_concl n discA_ts selA_tss discB_ts selB_tss))); 1939 in 1940 @{map 8} mk_prem IRs fpAs fpBs ns discA_tss selA_tsss discB_tss selB_tsss 1941 end; 1942 1943 val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 mk_leq 1944 IRs (map2 (build_the_rel ctxt (Rs @ IRs) []) fpA_Ts fpB_Ts))); 1945 val vars = Variable.add_free_names ctxt goal []; 1946 1947 val rel_coinduct0_thm = 1948 Goal.prove_sorry ctxt vars prems goal (fn {context = ctxt, prems} => 1949 mk_rel_coinduct0_tac ctxt dtor_rel_coinduct (map (Thm.cterm_of ctxt) IRs) prems 1950 (map #exhaust ctr_sugars) (map (flat o #disc_thmss) ctr_sugars) 1951 (map (flat o #sel_thmss) ctr_sugars) ctor_defss dtor_ctors ctor_injects abs_injects 1952 rel_pre_defs abs_inverses live_nesting_rel_eqs) 1953 |> Thm.close_derivation \<^here>; 1954 in 1955 (postproc_co_induct ctxt nn @{thm predicate2D} @{thm predicate2D_conj} rel_coinduct0_thm, 1956 mk_coinduct_attrs fpA_Ts (map #ctrs ctr_sugars) (map #discs ctr_sugars) mss) 1957 end; 1958 1959fun derive_set_induct_thms_for_types ctxt nn fpTs ctrss setss dtor_set_inducts exhausts set_pre_defs 1960 ctor_defs dtor_ctors Abs_pre_inverses = 1961 let 1962 fun mk_prems A Ps ctr_args t ctxt = 1963 (case fastype_of t of 1964 Type (type_name, innerTs) => 1965 (case bnf_of ctxt type_name of 1966 NONE => ([], ctxt) 1967 | SOME bnf => 1968 let 1969 fun seq_assm a set ctxt = 1970 let 1971 val X = HOLogic.dest_setT (range_type (fastype_of set)); 1972 val (x, ctxt') = yield_singleton (mk_Frees "x") X ctxt; 1973 val assm = mk_Trueprop_mem (x, set $ a); 1974 in 1975 (case build_binary_fun_app Ps x a of 1976 NONE => 1977 mk_prems A Ps ctr_args x ctxt' 1978 |>> map (Logic.all x o Logic.mk_implies o pair assm) 1979 | SOME f => 1980 ([Logic.all x 1981 (Logic.mk_implies (assm, 1982 Logic.mk_implies (HOLogic.mk_Trueprop f, 1983 HOLogic.mk_Trueprop (the (build_binary_fun_app Ps x ctr_args)))))], 1984 ctxt')) 1985 end; 1986 in 1987 fold_map (seq_assm t o mk_set innerTs) (sets_of_bnf bnf) ctxt 1988 |>> flat 1989 end) 1990 | T => 1991 if T = A then ([HOLogic.mk_Trueprop (the (build_binary_fun_app Ps t ctr_args))], ctxt) 1992 else ([], ctxt)); 1993 1994 fun mk_prems_for_ctr A Ps ctr ctxt = 1995 let 1996 val (args, ctxt') = mk_Frees "z" (binder_types (fastype_of ctr)) ctxt; 1997 in 1998 fold_map (mk_prems A Ps (list_comb (ctr, args))) args ctxt' 1999 |>> map (fold_rev Logic.all args) o flat 2000 |>> (fn prems => (prems, mk_names (length prems) (name_of_ctr ctr))) 2001 end; 2002 2003 fun mk_prems_and_concl_for_type A Ps ((fpT, ctrs), set) ctxt = 2004 let 2005 val ((x, fp), ctxt') = ctxt 2006 |> yield_singleton (mk_Frees "x") A 2007 ||>> yield_singleton (mk_Frees "a") fpT; 2008 val concl = mk_Ball (set $ fp) (Term.absfree (dest_Free x) 2009 (the (build_binary_fun_app Ps x fp))); 2010 in 2011 fold_map (mk_prems_for_ctr A Ps) ctrs ctxt' 2012 |>> split_list 2013 |>> map_prod flat flat 2014 |>> apfst (rpair concl) 2015 end; 2016 2017 fun mk_thm ctxt fpTs ctrss sets = 2018 let 2019 val A = HOLogic.dest_setT (range_type (fastype_of (hd sets))); 2020 val (Ps, ctxt') = mk_Frees "P" (map (fn fpT => A --> fpT --> HOLogic.boolT) fpTs) ctxt; 2021 val (((prems, concl), case_names), ctxt'') = 2022 fold_map (mk_prems_and_concl_for_type A Ps) (fpTs ~~ ctrss ~~ sets) ctxt' 2023 |>> apfst split_list o split_list 2024 |>> apfst (apfst flat) 2025 |>> apfst (apsnd (Library.foldr1 HOLogic.mk_conj)) 2026 |>> apsnd flat; 2027 2028 val vars = fold (Variable.add_free_names ctxt) (concl :: prems) []; 2029 val thm = 2030 Goal.prove_sorry ctxt vars prems (HOLogic.mk_Trueprop concl) 2031 (fn {context = ctxt, prems} => 2032 mk_set_induct0_tac ctxt (map (Thm.cterm_of ctxt'') Ps) prems dtor_set_inducts 2033 exhausts set_pre_defs ctor_defs dtor_ctors Abs_pre_inverses) 2034 |> Thm.close_derivation \<^here>; 2035 2036 val case_names_attr = Attrib.case_names (quasi_unambiguous_case_names case_names); 2037 val induct_set_attrs = map (Attrib.internal o K o Induct.induct_pred o name_of_set) sets; 2038 in 2039 (thm, case_names_attr :: induct_set_attrs) 2040 end 2041 val consumes_attr = Attrib.consumes 1; 2042 in 2043 map (mk_thm ctxt fpTs ctrss 2044 #> nn = 1 ? map_prod (fn thm => rotate_prems ~1 (thm RS bspec)) (cons consumes_attr)) 2045 (transpose setss) 2046 end; 2047 2048fun mk_coinduct_strong_thm coind rel_eqs rel_monos mk_vimage2p ctxt = 2049 let 2050 val n = Thm.nprems_of coind; 2051 val m = Thm.nprems_of (hd rel_monos) - n; 2052 fun mk_inst phi = 2053 (phi, Thm.cterm_of ctxt (mk_union (Var phi, HOLogic.eq_const (fst (dest_pred2T (#2 phi)))))); 2054 val insts = Term.add_vars (Thm.prop_of coind) [] |> rev |> take n |> map mk_inst; 2055 fun mk_unfold rel_eq rel_mono = 2056 let 2057 val eq = iffD2 OF [rel_eq RS @{thm predicate2_eqD}, refl]; 2058 val mono = rel_mono OF (replicate m @{thm order_refl} @ replicate n @{thm eq_subset}); 2059 in mk_vimage2p (eq RS (mono RS @{thm predicate2D})) RS eqTrueI end; 2060 val unfolds = map2 mk_unfold rel_eqs rel_monos @ @{thms sup_fun_def sup_bool_def 2061 imp_disjL all_conj_distrib subst_eq_imp simp_thms(18,21,35)}; 2062 in 2063 Thm.instantiate ([], insts) coind 2064 |> unfold_thms ctxt unfolds 2065 end; 2066 2067fun derive_coinduct_thms_for_types ctxt strong alter_r pre_bnfs dtor_coinduct dtor_ctors 2068 live_nesting_bnfs fpTs Xs ctrXs_Tsss ns pre_abs_inverses abs_inverses mk_vimage2p ctr_defss 2069 (ctr_sugars : ctr_sugar list) = 2070 let 2071 val nn = length pre_bnfs; 2072 2073 val pre_rel_defs = map rel_def_of_bnf pre_bnfs; 2074 val live_nesting_rel_eqs = map rel_eq_of_bnf live_nesting_bnfs; 2075 2076 val fp_b_names = map base_name_of_typ fpTs; 2077 2078 val discss = map #discs ctr_sugars; 2079 val selsss = map #selss ctr_sugars; 2080 val exhausts = map #exhaust ctr_sugars; 2081 val disc_thmsss = map #disc_thmss ctr_sugars; 2082 val sel_thmsss = map #sel_thmss ctr_sugars; 2083 2084 val (((rs, us'), vs'), _) = ctxt 2085 |> mk_Frees "R" (map (fn T => mk_pred2T T T) fpTs) 2086 ||>> Variable.variant_fixes fp_b_names 2087 ||>> Variable.variant_fixes (map (suffix "'") fp_b_names); 2088 2089 val us = map2 (curry Free) us' fpTs; 2090 val udiscss = map2 (map o rapp) us discss; 2091 val uselsss = map2 (map o map o rapp) us selsss; 2092 2093 val vs = map2 (curry Free) vs' fpTs; 2094 val vdiscss = map2 (map o rapp) vs discss; 2095 val vselsss = map2 (map o map o rapp) vs selsss; 2096 2097 val uvrs = @{map 3} (fn r => fn u => fn v => r $ u $ v) rs us vs; 2098 val uv_eqs = map2 (curry HOLogic.mk_eq) us vs; 2099 val strong_rs = 2100 @{map 4} (fn u => fn v => fn uvr => fn uv_eq => 2101 fold_rev Term.lambda [u, v] (HOLogic.mk_disj (uvr, uv_eq))) us vs uvrs uv_eqs; 2102 2103 val concl = 2104 HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj 2105 (@{map 3} (fn uvr => fn u => fn v => HOLogic.mk_imp (uvr, HOLogic.mk_eq (u, v))) 2106 uvrs us vs)) 2107 2108 fun mk_goal rs0' = 2109 Logic.list_implies (@{map 9} (mk_coinduct_prem ctxt (map single Xs) (map single fpTs) 2110 (map alter_r rs0')) 2111 uvrs us vs ns udiscss uselsss vdiscss vselsss ctrXs_Tsss, 2112 concl); 2113 2114 val goals = map mk_goal ([rs] @ (if strong then [strong_rs] else [])); 2115 2116 fun prove dtor_coinduct' goal = 2117 Variable.add_free_names ctxt goal [] 2118 |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, ...} => 2119 mk_coinduct_tac ctxt live_nesting_rel_eqs nn ns dtor_coinduct' pre_rel_defs pre_abs_inverses 2120 abs_inverses dtor_ctors exhausts ctr_defss disc_thmsss sel_thmsss)) 2121 |> Thm.close_derivation \<^here>; 2122 2123 val rel_eqs = map rel_eq_of_bnf pre_bnfs; 2124 val rel_monos = map rel_mono_of_bnf pre_bnfs; 2125 val dtor_coinducts = 2126 [dtor_coinduct] @ 2127 (if strong then [mk_coinduct_strong_thm dtor_coinduct rel_eqs rel_monos mk_vimage2p ctxt] 2128 else []); 2129 in 2130 map2 (postproc_co_induct ctxt nn mp @{thm conj_commute[THEN iffD1]} oo prove) 2131 dtor_coinducts goals 2132 end; 2133 2134fun derive_coinduct_corecs_thms_for_types ctxt pre_bnfs 2135 (x, cs, cpss, (((pgss, _, _, _), cqgsss), _)) dtor_coinduct dtor_injects dtor_ctors 2136 dtor_corec_thms live_nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss mss ns pre_abs_inverses abs_inverses 2137 mk_vimage2p ctr_defss (ctr_sugars : ctr_sugar list) corecs corec_defs = 2138 let 2139 fun mk_ctor_dtor_corec_thm dtor_inject dtor_ctor corec = 2140 iffD1 OF [dtor_inject, trans OF [corec, dtor_ctor RS sym]]; 2141 2142 val ctor_dtor_corec_thms = 2143 @{map 3} mk_ctor_dtor_corec_thm dtor_injects dtor_ctors dtor_corec_thms; 2144 2145 val pre_map_defs = map map_def_of_bnf pre_bnfs; 2146 val live_nesting_map_ident0s = map map_ident0_of_bnf live_nesting_bnfs; 2147 2148 val fp_b_names = map base_name_of_typ fpTs; 2149 2150 val ctrss = map #ctrs ctr_sugars; 2151 val discss = map #discs ctr_sugars; 2152 val selsss = map #selss ctr_sugars; 2153 val disc_thmsss = map #disc_thmss ctr_sugars; 2154 val discIss = map #discIs ctr_sugars; 2155 val sel_thmsss = map #sel_thmss ctr_sugars; 2156 2157 val coinduct_thms_pairs = derive_coinduct_thms_for_types ctxt true I pre_bnfs dtor_coinduct 2158 dtor_ctors live_nesting_bnfs fpTs Xs ctrXs_Tsss ns pre_abs_inverses abs_inverses mk_vimage2p 2159 ctr_defss ctr_sugars; 2160 2161 fun mk_maybe_not pos = not pos ? HOLogic.mk_not; 2162 2163 val gcorecs = map (lists_bmoc pgss) corecs; 2164 2165 val corec_thmss = 2166 let 2167 val (us', _) = ctxt 2168 |> Variable.variant_fixes fp_b_names; 2169 2170 val us = map2 (curry Free) us' fpTs; 2171 2172 fun mk_goal c cps gcorec n k ctr m cfs' = 2173 fold_rev (fold_rev Logic.all) ([c] :: pgss) 2174 (Logic.list_implies (seq_conds (HOLogic.mk_Trueprop oo mk_maybe_not) n k cps, 2175 mk_Trueprop_eq (gcorec $ c, Term.list_comb (ctr, take m cfs')))); 2176 2177 val mk_U = typ_subst_nonatomic (map2 (fn C => fn fpT => (mk_sumT (fpT, C), fpT)) Cs fpTs); 2178 2179 fun tack (c, u) f = 2180 let val x' = Free (x, mk_sumT (fastype_of u, fastype_of c)) in 2181 Term.lambda x' (mk_case_sum (Term.lambda u u, Term.lambda c (f $ c)) $ x') 2182 end; 2183 2184 fun build_corec cqg = 2185 let val T = fastype_of cqg in 2186 if exists_subtype_in Cs T then 2187 let 2188 val U = mk_U T; 2189 val build_simple = 2190 indexify fst (map2 (curry mk_sumT) fpTs Cs) 2191 (fn kk => fn _ => tack (nth cs kk, nth us kk) (nth gcorecs kk)); 2192 in 2193 build_map ctxt [] [] build_simple (T, U) $ cqg 2194 end 2195 else 2196 cqg 2197 end; 2198 2199 val cqgsss' = map (map (map build_corec)) cqgsss; 2200 val goalss = @{map 8} (@{map 4} oooo mk_goal) cs cpss gcorecs ns kss ctrss mss cqgsss'; 2201 2202 val tacss = 2203 @{map 4} (map ooo mk_corec_tac corec_defs live_nesting_map_ident0s) 2204 ctor_dtor_corec_thms pre_map_defs abs_inverses ctr_defss; 2205 2206 fun prove goal tac = 2207 Goal.prove_sorry ctxt [] [] goal (tac o #context) 2208 |> Thm.close_derivation \<^here>; 2209 in 2210 map2 (map2 prove) goalss tacss 2211 |> map (map (unfold_thms ctxt @{thms case_sum_if})) 2212 end; 2213 2214 val corec_disc_iff_thmss = 2215 let 2216 fun mk_goal c cps gcorec n k disc = 2217 mk_Trueprop_eq (disc $ (gcorec $ c), 2218 if n = 1 then \<^const>\<open>True\<close> 2219 else Library.foldr1 HOLogic.mk_conj (seq_conds mk_maybe_not n k cps)); 2220 2221 val goalss = @{map 6} (map2 oooo mk_goal) cs cpss gcorecs ns kss discss; 2222 2223 fun mk_case_split' cp = Thm.instantiate' [] [SOME (Thm.cterm_of ctxt cp)] @{thm case_split}; 2224 2225 val case_splitss' = map (map mk_case_split') cpss; 2226 2227 val tacss = @{map 3} (map oo mk_corec_disc_iff_tac) case_splitss' corec_thmss disc_thmsss; 2228 2229 fun prove goal tac = 2230 Variable.add_free_names ctxt goal [] 2231 |> (fn vars => Goal.prove_sorry ctxt vars [] goal (tac o #context)) 2232 |> Thm.close_derivation \<^here>; 2233 2234 fun proves [_] [_] = [] 2235 | proves goals tacs = map2 prove goals tacs; 2236 in 2237 map2 proves goalss tacss 2238 end; 2239 2240 fun mk_corec_disc_thms corecs discIs = map (op RS) (corecs ~~ discIs); 2241 2242 val corec_disc_thmss = map2 mk_corec_disc_thms corec_thmss discIss; 2243 2244 fun mk_corec_sel_thm corec_thm sel sel_thm = 2245 let 2246 val (domT, ranT) = dest_funT (fastype_of sel); 2247 val arg_cong' = 2248 Thm.instantiate' (map (SOME o Thm.ctyp_of ctxt) [domT, ranT]) 2249 [NONE, NONE, SOME (Thm.cterm_of ctxt sel)] arg_cong 2250 |> Thm.varifyT_global; 2251 val sel_thm' = sel_thm RSN (2, trans); 2252 in 2253 corec_thm RS arg_cong' RS sel_thm' 2254 end; 2255 2256 fun mk_corec_sel_thms corec_thmss = 2257 @{map 3} (@{map 3} (map2 o mk_corec_sel_thm)) corec_thmss selsss sel_thmsss; 2258 2259 val corec_sel_thmsss = mk_corec_sel_thms corec_thmss; 2260 in 2261 ((coinduct_thms_pairs, 2262 mk_coinduct_attrs fpTs (map #ctrs ctr_sugars) (map #discs ctr_sugars) mss), 2263 corec_thmss, 2264 corec_disc_thmss, 2265 (corec_disc_iff_thmss, simp_attrs), 2266 (corec_sel_thmsss, simp_attrs)) 2267 end; 2268 2269fun define_co_datatypes prepare_plugins prepare_constraint prepare_typ prepare_term fp construct_fp 2270 ((raw_plugins, discs_sels0), specs) lthy = 2271 let 2272 val plugins = prepare_plugins lthy raw_plugins; 2273 val discs_sels = discs_sels0 orelse fp = Greatest_FP; 2274 2275 val nn = length specs; 2276 val fp_bs = map type_binding_of_spec specs; 2277 val fp_b_names = map Binding.name_of fp_bs; 2278 val fp_common_name = mk_common_name fp_b_names; 2279 val map_bs = map map_binding_of_spec specs; 2280 val rel_bs = map rel_binding_of_spec specs; 2281 val pred_bs = map pred_binding_of_spec specs; 2282 2283 fun prepare_type_arg (_, (ty, c)) = 2284 let val TFree (s, _) = prepare_typ lthy ty in 2285 TFree (s, prepare_constraint lthy c) 2286 end; 2287 2288 val Ass0 = map (map prepare_type_arg o type_args_named_constrained_of_spec) specs; 2289 val unsorted_Ass0 = map (map (resort_tfree_or_tvar \<^sort>\<open>type\<close>)) Ass0; 2290 val unsorted_As = Library.foldr1 (merge_type_args fp) unsorted_Ass0; 2291 val num_As = length unsorted_As; 2292 2293 val set_boss = map (map fst o type_args_named_constrained_of_spec) specs; 2294 val set_bss = map (map (the_default Binding.empty)) set_boss; 2295 2296 fun add_fake_type spec = 2297 Typedecl.basic_typedecl {final = true} 2298 (type_binding_of_spec spec, num_As, Mixfix.reset_pos (mixfix_of_spec spec)); 2299 2300 val (fake_T_names, fake_lthy) = fold_map add_fake_type specs lthy; 2301 2302 val qsoty = quote o Syntax.string_of_typ fake_lthy; 2303 2304 val _ = (case Library.duplicates (op =) unsorted_As of [] => () 2305 | A :: _ => error ("Duplicate type parameter " ^ qsoty A ^ " in " ^ co_prefix fp ^ 2306 "datatype specification")); 2307 2308 val bad_args = 2309 map (Logic.type_map (singleton (Variable.polymorphic lthy))) unsorted_As 2310 |> filter_out Term.is_TVar; 2311 val _ = null bad_args orelse 2312 error ("Locally fixed type argument " ^ qsoty (hd bad_args) ^ " in " ^ co_prefix fp ^ 2313 "datatype specification"); 2314 2315 val mixfixes = map mixfix_of_spec specs; 2316 2317 val _ = (case Library.duplicates Binding.eq_name fp_bs of [] => () 2318 | b :: _ => error ("Duplicate type name declaration " ^ quote (Binding.name_of b))); 2319 2320 val mx_ctr_specss = map mixfixed_ctr_specs_of_spec specs; 2321 val ctr_specss = map (map fst) mx_ctr_specss; 2322 val ctr_mixfixess = map (map snd) mx_ctr_specss; 2323 2324 val disc_bindingss = map (map disc_of_ctr_spec) ctr_specss; 2325 val ctr_bindingss = 2326 map2 (fn fp_b_name => map (Binding.qualify false fp_b_name o ctr_of_ctr_spec)) fp_b_names 2327 ctr_specss; 2328 val ctr_argsss = map (map args_of_ctr_spec) ctr_specss; 2329 2330 val sel_bindingsss = map (map (map fst)) ctr_argsss; 2331 val fake_ctr_Tsss0 = map (map (map (prepare_typ fake_lthy o snd))) ctr_argsss; 2332 val raw_sel_default_eqss = map sel_default_eqs_of_spec specs; 2333 2334 val (As :: _) :: fake_ctr_Tsss = 2335 burrow (burrow (Syntax.check_typs fake_lthy)) (Ass0 :: fake_ctr_Tsss0); 2336 val As' = map dest_TFree As; 2337 2338 val rhs_As' = fold (fold (fold Term.add_tfreesT)) fake_ctr_Tsss []; 2339 val _ = (case subtract (op =) As' rhs_As' of [] => () 2340 | extras => error ("Extra type variables on right-hand side: " ^ 2341 commas (map (qsoty o TFree) extras))); 2342 2343 val fake_Ts = map (fn s => Type (s, As)) fake_T_names; 2344 2345 val ((((Bs0, Cs), Es), Xs), _) = lthy 2346 |> fold (Variable.declare_typ o resort_tfree_or_tvar dummyS) unsorted_As 2347 |> mk_TFrees num_As 2348 ||>> mk_TFrees nn 2349 ||>> mk_TFrees nn 2350 ||>> variant_tfrees fp_b_names; 2351 2352 fun eq_fpT_check (T as Type (s, Ts)) (T' as Type (s', Ts')) = 2353 s = s' andalso (Ts = Ts' orelse 2354 error ("Wrong type arguments in " ^ co_prefix fp ^ "recursive type " ^ qsoty T ^ 2355 " (expected " ^ qsoty T' ^ ")")) 2356 | eq_fpT_check _ _ = false; 2357 2358 fun freeze_fp (T as Type (s, Ts)) = 2359 (case find_index (eq_fpT_check T) fake_Ts of 2360 ~1 => Type (s, map freeze_fp Ts) 2361 | kk => nth Xs kk) 2362 | freeze_fp T = T; 2363 2364 val unfreeze_fp = Term.typ_subst_atomic (Xs ~~ fake_Ts); 2365 2366 val ctrXs_Tsss = map (map (map freeze_fp)) fake_ctr_Tsss; 2367 val ctrXs_repTs = map mk_sumprodT_balanced ctrXs_Tsss; 2368 2369 val _ = 2370 let 2371 fun add_deps i = 2372 fold (fn T => fold_index (fn (j, X) => 2373 (i <> j andalso exists_subtype_in [X] T) ? insert (op =) (i, j)) Xs); 2374 2375 val add_missing_nodes = fold (AList.default (op =) o rpair []) (0 upto nn - 1); 2376 2377 val deps = fold_index (uncurry (fold o add_deps)) ctrXs_Tsss [] 2378 |> AList.group (op =) 2379 |> add_missing_nodes; 2380 2381 val G = Int_Graph.make (map (apfst (rpair ())) deps); 2382 val sccs = map (sort int_ord) (Int_Graph.strong_conn G); 2383 2384 val str_of_scc = prefix (co_prefix fp ^ "datatype ") o 2385 space_implode " and " o map (suffix " = \<dots>" o Long_Name.base_name); 2386 2387 fun warn [_] = () 2388 | warn sccs = 2389 warning ("Defined types not fully mutually " ^ co_prefix fp ^ "recursive\n\ 2390 \Alternative specification:\n" ^ 2391 cat_lines (map (prefix " " o str_of_scc o map (nth fp_b_names)) sccs)); 2392 in 2393 warn (order_strong_conn (op =) Int_Graph.make Int_Graph.topological_order deps sccs) 2394 end; 2395 2396 val killed_As = 2397 map_filter (fn (A, set_bos) => if exists is_none set_bos then SOME A else NONE) 2398 (As ~~ transpose set_boss); 2399 2400 val (((pre_bnfs, absT_infos), _), (fp_res as {bnfs = fp_bnfs as any_fp_bnf :: _, ctors = ctors0, 2401 dtors = dtors0, xtor_co_recs = xtor_co_recs0, xtor_co_induct, dtor_ctors, ctor_dtors, 2402 ctor_injects, dtor_injects, xtor_maps, xtor_setss, xtor_rels, xtor_co_rec_thms, 2403 xtor_rel_co_induct, dtor_set_inducts, xtor_co_rec_transfers, xtor_co_rec_o_maps, ...}, 2404 lthy)) = 2405 fixpoint_bnf false I (construct_fp mixfixes map_bs rel_bs pred_bs set_bss) fp_bs 2406 (map dest_TFree As) (map dest_TFree killed_As) (map dest_TFree Xs) ctrXs_repTs 2407 empty_comp_cache lthy 2408 handle BAD_DEAD (X, X_backdrop) => 2409 (case X_backdrop of 2410 Type (bad_tc, _) => 2411 let 2412 val fake_T = qsoty (unfreeze_fp X); 2413 val fake_T_backdrop = qsoty (unfreeze_fp X_backdrop); 2414 fun register_hint () = 2415 "\nUse the " ^ quote (#1 \<^command_keyword>\<open>bnf\<close>) ^ " command to register " ^ 2416 quote bad_tc ^ " as a bounded natural functor to allow nested (co)recursion through \ 2417 \it"; 2418 in 2419 if is_some (bnf_of lthy bad_tc) orelse is_some (fp_sugar_of lthy bad_tc) then 2420 error ("Inadmissible " ^ co_prefix fp ^ "recursive occurrence of type " ^ fake_T ^ 2421 " in type expression " ^ fake_T_backdrop) 2422 else if is_some (Old_Datatype_Data.get_info (Proof_Context.theory_of lthy) 2423 bad_tc) then 2424 error ("Unsupported " ^ co_prefix fp ^ "recursive occurrence of type " ^ fake_T ^ 2425 " via the old-style datatype " ^ quote bad_tc ^ " in type expression " ^ 2426 fake_T_backdrop ^ register_hint ()) 2427 else 2428 error ("Unsupported " ^ co_prefix fp ^ "recursive occurrence of type " ^ fake_T ^ 2429 " via type constructor " ^ quote bad_tc ^ " in type expression " ^ fake_T_backdrop ^ 2430 register_hint ()) 2431 end); 2432 2433 val time = time lthy; 2434 val timer = time (Timer.startRealTimer ()); 2435 2436 val fp_nesting_bnfs = nesting_bnfs lthy ctrXs_Tsss Xs; 2437 val live_nesting_bnfs = nesting_bnfs lthy ctrXs_Tsss As; 2438 2439 val pre_map_defs = map map_def_of_bnf pre_bnfs; 2440 val pre_set_defss = map set_defs_of_bnf pre_bnfs; 2441 val pre_rel_defs = map rel_def_of_bnf pre_bnfs; 2442 val fp_nesting_set_maps = maps set_map_of_bnf fp_nesting_bnfs; 2443 val fp_nesting_rel_eq_onps = map rel_eq_onp_of_bnf fp_nesting_bnfs; 2444 val live_nesting_map_id0s = map map_id0_of_bnf live_nesting_bnfs; 2445 val live_nesting_map_ident0s = map map_ident0_of_bnf live_nesting_bnfs; 2446 val live_nesting_set_maps = maps set_map_of_bnf live_nesting_bnfs; 2447 val live_nesting_rel_eqs = map rel_eq_of_bnf live_nesting_bnfs; 2448 val live_nesting_rel_eq_onps = map rel_eq_onp_of_bnf live_nesting_bnfs; 2449 2450 val liveness = liveness_of_fp_bnf num_As any_fp_bnf; 2451 val live = live_of_bnf any_fp_bnf; 2452 val _ = 2453 if live = 0 andalso exists (not o Binding.is_empty) (map_bs @ rel_bs @ pred_bs) then 2454 warning "Map function, relator, and predicator names ignored" 2455 else 2456 (); 2457 2458 val Bs = @{map 3} (fn alive => fn A as TFree (_, S) => fn B => 2459 if alive then resort_tfree_or_tvar S B else A) 2460 liveness As Bs0; 2461 2462 val B_ify_T = Term.typ_subst_atomic (As ~~ Bs); 2463 val B_ify = Term.map_types B_ify_T; 2464 2465 val live_AsBs = filter (op <>) (As ~~ Bs); 2466 2467 val abss = map #abs absT_infos; 2468 val reps = map #rep absT_infos; 2469 val absTs = map #absT absT_infos; 2470 val repTs = map #repT absT_infos; 2471 val abs_injects = map #abs_inject absT_infos; 2472 val abs_inverses = map #abs_inverse absT_infos; 2473 val type_definitions = map #type_definition absT_infos; 2474 2475 val ctors = map (mk_ctor As) ctors0; 2476 val dtors = map (mk_dtor As) dtors0; 2477 2478 val fpTs = map (domain_type o fastype_of) dtors; 2479 val fpBTs = map B_ify_T fpTs; 2480 2481 val real_unfreeze_fp = Term.typ_subst_atomic (Xs ~~ fpTs); 2482 2483 val ctr_Tsss = map (map (map real_unfreeze_fp)) ctrXs_Tsss; 2484 val ns = map length ctr_Tsss; 2485 val kss = map (fn n => 1 upto n) ns; 2486 val mss = map (map length) ctr_Tsss; 2487 2488 val (xtor_co_recs, recs_args_types, corecs_args_types) = 2489 mk_co_recs_prelims lthy fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_recs0; 2490 2491 fun define_ctrs_dtrs_for_type_etc fp_bnf fp_b fpT C E ctor dtor xtor_co_rec ctor_dtor dtor_ctor 2492 ctor_inject pre_map_def pre_set_defs pre_rel_def fp_map_thm fp_set_thms fp_rel_thm n ks ms 2493 abs abs_inject type_definition ctr_bindings ctr_mixfixes ctr_Tss disc_bindings sel_bindingss 2494 raw_sel_default_eqs lthy = 2495 let 2496 val fp_b_name = Binding.name_of fp_b; 2497 2498 val ((xss, ctrs0, ctor_iff_dtor_thm, ctr_defs), lthy) = 2499 define_ctrs_dtrs_for_type fp_b_name fpT ctor dtor ctor_dtor dtor_ctor n ks abs 2500 ctr_bindings ctr_mixfixes ctr_Tss lthy; 2501 2502 val ctrs = map (mk_ctr As) ctrs0; 2503 2504 val sel_default_eqs = 2505 let 2506 val sel_Tss = map (map (curry (op -->) fpT)) ctr_Tss; 2507 val sel_bTs = 2508 flat sel_bindingss ~~ flat sel_Tss 2509 |> filter_out (Binding.is_empty o fst) 2510 |> distinct (Binding.eq_name o apply2 fst); 2511 val sel_default_lthy = fake_local_theory_for_sel_defaults sel_bTs lthy 2512 in 2513 map (prepare_term sel_default_lthy) raw_sel_default_eqs 2514 end; 2515 2516 fun mk_binding pre = 2517 Binding.qualify false fp_b_name (Binding.prefix_name (pre ^ "_") fp_b); 2518 2519 fun massage_res (ctr_sugar, maps_sets_rels) = 2520 (maps_sets_rels, (ctrs, xss, ctor_iff_dtor_thm, ctr_defs, ctr_sugar)); 2521 in 2522 (wrap_ctrs plugins fp discs_sels fp_b_name ctor_inject n ms abs_inject type_definition 2523 disc_bindings sel_bindingss sel_default_eqs ctrs0 ctor_iff_dtor_thm ctr_defs 2524 #> (fn (ctr_sugar, lthy) => 2525 derive_map_set_rel_pred_thms plugins fp live As Bs C E abs_inverses ctr_defs 2526 fp_nesting_set_maps fp_nesting_rel_eq_onps live_nesting_map_id0s live_nesting_set_maps 2527 live_nesting_rel_eqs live_nesting_rel_eq_onps [] fp_b_name fp_bnf fp_bnfs fpT ctor 2528 ctor_dtor dtor_ctor pre_map_def pre_set_defs pre_rel_def fp_map_thm fp_set_thms 2529 fp_rel_thm [] [] [] ctr_Tss ctr_sugar lthy 2530 |>> pair ctr_sugar) 2531 ##>> 2532 (if fp = Least_FP then define_rec (the recs_args_types) mk_binding fpTs Cs reps 2533 else define_corec (the corecs_args_types) mk_binding fpTs Cs abss) xtor_co_rec 2534 #>> apfst massage_res, lthy) 2535 end; 2536 2537 fun wrap_ctrs_derive_map_set_rel_pred_thms_define_co_rec_for_types (wrap_one_etcs, lthy) = 2538 fold_map I wrap_one_etcs lthy 2539 |>> apsnd split_list o apfst (apsnd @{split_list 5} o apfst @{split_list 17} o split_list) 2540 o split_list; 2541 2542 fun mk_simp_thms ({injects, distincts, case_thms, ...} : ctr_sugar) co_recs map_thms rel_injects 2543 rel_distincts set_thmss = 2544 injects @ distincts @ case_thms @ co_recs @ map_thms @ rel_injects @ rel_distincts @ 2545 set_thmss; 2546 2547 fun mk_co_rec_transfer_goals lthy co_recs = 2548 let 2549 val BE_ify = Term.subst_atomic_types (live_AsBs @ (Cs ~~ Es)); 2550 2551 val ((Rs, Ss), names_lthy) = lthy 2552 |> mk_Frees "R" (map (uncurry mk_pred2T) live_AsBs) 2553 ||>> mk_Frees "S" (map2 mk_pred2T Cs Es); 2554 2555 val co_recBs = map BE_ify co_recs; 2556 in 2557 (Rs, Ss, map2 (mk_parametricity_goal lthy (Rs @ Ss)) co_recs co_recBs, names_lthy) 2558 end; 2559 2560 fun derive_rec_transfer_thms lthy recs rec_defs (SOME (_, _, _, xsssss)) = 2561 let 2562 val (Rs, Ss, goals, _) = mk_co_rec_transfer_goals lthy recs; 2563 val goal = Logic.mk_conjunction_balanced goals; 2564 val vars = Variable.add_free_names lthy goal []; 2565 in 2566 Goal.prove_sorry lthy vars [] goal 2567 (fn {context = ctxt, prems = _} => 2568 mk_rec_transfer_tac ctxt nn ns (map (Thm.cterm_of ctxt) Ss) 2569 (map (Thm.cterm_of ctxt) Rs) xsssss rec_defs xtor_co_rec_transfers pre_rel_defs 2570 live_nesting_rel_eqs) 2571 |> Thm.close_derivation \<^here> 2572 |> Conjunction.elim_balanced nn 2573 end; 2574 2575 fun derive_rec_o_map_thmss lthy recs rec_defs = 2576 if live = 0 then 2577 replicate nn [] 2578 else 2579 let 2580 fun variant_names n pre = fst (Variable.variant_fixes (replicate n pre) lthy); 2581 2582 val maps0 = map map_of_bnf fp_bnfs; 2583 val f_names = variant_names num_As "f"; 2584 val fs = map2 (curry Free) f_names (map (op -->) (As ~~ Bs)); 2585 val live_gs = AList.find (op =) (fs ~~ liveness) true; 2586 2587 val gmaps = map (fn map0 => Term.list_comb (mk_map live As Bs map0, live_gs)) maps0; 2588 2589 val rec_arg_Ts = binder_fun_types (hd (map fastype_of recs)); 2590 2591 val num_rec_args = length rec_arg_Ts; 2592 val g_Ts = map B_ify_T rec_arg_Ts; 2593 val g_names = variant_names num_rec_args "g"; 2594 val gs = map2 (curry Free) g_names g_Ts; 2595 val grecs = map (fn recx => Term.list_comb (Term.map_types B_ify_T recx, gs)) recs; 2596 2597 val rec_o_map_lhss = map2 (curry HOLogic.mk_comp) grecs gmaps; 2598 2599 val ABfs = (As ~~ Bs) ~~ fs; 2600 2601 fun mk_rec_arg_arg (x as Free (_, T)) = 2602 let val U = B_ify_T T in 2603 if T = U then x else build_map lthy [] [] (the o AList.lookup (op =) ABfs) (T, U) $ x 2604 end; 2605 2606 fun mk_rec_o_map_arg rec_arg_T h = 2607 let 2608 val x_Ts = binder_types rec_arg_T; 2609 val m = length x_Ts; 2610 val x_names = variant_names m "x"; 2611 val xs = map2 (curry Free) x_names x_Ts; 2612 val xs' = map mk_rec_arg_arg xs; 2613 in 2614 fold_rev Term.lambda xs (Term.list_comb (h, xs')) 2615 end; 2616 2617 fun mk_rec_o_map_rhs recx = 2618 let val args = map2 mk_rec_o_map_arg rec_arg_Ts gs in 2619 Term.list_comb (recx, args) 2620 end; 2621 2622 val rec_o_map_rhss = map mk_rec_o_map_rhs recs; 2623 2624 val rec_o_map_goals = 2625 map2 (fold_rev (fold_rev Logic.all) [fs, gs] o HOLogic.mk_Trueprop oo 2626 curry HOLogic.mk_eq) rec_o_map_lhss rec_o_map_rhss; 2627 val rec_o_map_thms = 2628 @{map 3} (fn goal => fn rec_def => fn ctor_rec_o_map => 2629 Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} => 2630 mk_co_rec_o_map_tac ctxt rec_def pre_map_defs live_nesting_map_ident0s 2631 abs_inverses ctor_rec_o_map) 2632 |> Thm.close_derivation \<^here>) 2633 rec_o_map_goals rec_defs xtor_co_rec_o_maps; 2634 in 2635 map single rec_o_map_thms 2636 end; 2637 2638 fun derive_note_induct_recs_thms_for_types 2639 ((((map_thmss, map_disc_iffss, map_selsss, rel_injectss, rel_distinctss, rel_selss, 2640 rel_intross, rel_casess, pred_injectss, set_thmss, set_selsssss, set_introsssss, 2641 set_casess, ctr_transferss, case_transferss, disc_transferss, sel_transferss), 2642 (ctrss, _, ctor_iff_dtors, ctr_defss, ctr_sugars)), 2643 (recs, rec_defs)), lthy) = 2644 let 2645 val ((induct_thms, induct_thm, induct_attrs), (rec_thmss, rec_attrs)) = 2646 derive_induct_recs_thms_for_types plugins pre_bnfs recs_args_types xtor_co_induct 2647 xtor_co_rec_thms live_nesting_bnfs fp_nesting_bnfs fpTs Cs Xs ctrXs_Tsss abs_inverses 2648 type_definitions abs_inverses ctrss ctr_defss recs rec_defs lthy; 2649 2650 val rec_transfer_thmss = 2651 map single (derive_rec_transfer_thms lthy recs rec_defs recs_args_types); 2652 2653 val induct_type_attr = Attrib.internal o K o Induct.induct_type; 2654 val induct_pred_attr = Attrib.internal o K o Induct.induct_pred; 2655 2656 val ((rel_induct_thmss, common_rel_induct_thms), 2657 (rel_induct_attrs, common_rel_induct_attrs)) = 2658 if live = 0 then 2659 ((replicate nn [], []), ([], [])) 2660 else 2661 let 2662 val ((rel_induct_thms, common_rel_induct_thm), rel_induct_attrs) = 2663 derive_rel_induct_thms_for_types lthy nn fpTs As Bs ctrss ctr_Tsss 2664 (map #exhaust ctr_sugars) xtor_rel_co_induct ctr_defss ctor_injects 2665 pre_rel_defs abs_inverses live_nesting_rel_eqs; 2666 in 2667 ((map single rel_induct_thms, single common_rel_induct_thm), 2668 (rel_induct_attrs, rel_induct_attrs)) 2669 end; 2670 2671 val rec_o_map_thmss = derive_rec_o_map_thmss lthy recs rec_defs; 2672 2673 val simp_thmss = 2674 @{map 6} mk_simp_thms ctr_sugars rec_thmss map_thmss rel_injectss rel_distinctss 2675 set_thmss; 2676 2677 val common_notes = 2678 (if nn > 1 then 2679 [(inductN, [induct_thm], K induct_attrs), 2680 (rel_inductN, common_rel_induct_thms, K common_rel_induct_attrs)] 2681 else 2682 []) 2683 |> massage_simple_notes fp_common_name; 2684 2685 val notes = 2686 [(inductN, map single induct_thms, fn T_name => induct_attrs @ [induct_type_attr T_name]), 2687 (recN, rec_thmss, K rec_attrs), 2688 (rec_o_mapN, rec_o_map_thmss, K []), 2689 (rec_transferN, rec_transfer_thmss, K []), 2690 (rel_inductN, rel_induct_thmss, K (rel_induct_attrs @ [induct_pred_attr ""])), 2691 (simpsN, simp_thmss, K [])] 2692 |> massage_multi_notes fp_b_names fpTs; 2693 in 2694 lthy 2695 |> Spec_Rules.add Binding.empty Spec_Rules.equational recs (flat rec_thmss) 2696 |> plugins code_plugin ? Code.declare_default_eqns (map (rpair true) (flat rec_thmss)) 2697 |> Local_Theory.notes (common_notes @ notes) 2698 (* for "datatype_realizer.ML": *) 2699 |>> name_noted_thms 2700 (fst (dest_Type (hd fpTs)) ^ implode (map (prefix "_") (tl fp_b_names))) inductN 2701 |-> interpret_bnfs_register_fp_sugars plugins fpTs fpBTs Xs Least_FP pre_bnfs absT_infos 2702 fp_nesting_bnfs live_nesting_bnfs fp_res ctrXs_Tsss ctor_iff_dtors ctr_defss ctr_sugars 2703 recs rec_defs map_thmss [induct_thm] (map single induct_thms) rec_thmss (replicate nn []) 2704 (replicate nn []) rel_injectss rel_distinctss map_disc_iffss map_selsss rel_selss 2705 rel_intross rel_casess pred_injectss set_thmss set_selsssss set_introsssss set_casess 2706 ctr_transferss case_transferss disc_transferss sel_transferss (replicate nn []) 2707 (replicate nn []) rec_transfer_thmss common_rel_induct_thms rel_induct_thmss [] 2708 (replicate nn []) rec_o_map_thmss 2709 end; 2710 2711 fun derive_corec_transfer_thms lthy corecs corec_defs = 2712 let 2713 val (Rs, Ss, goals, _) = mk_co_rec_transfer_goals lthy corecs; 2714 val (_, _, _, (((pgss, pss, qssss, gssss), _), _)) = the corecs_args_types; 2715 val goal = Logic.mk_conjunction_balanced goals; 2716 val vars = Variable.add_free_names lthy goal []; 2717 in 2718 Goal.prove_sorry lthy vars [] goal 2719 (fn {context = ctxt, prems = _} => 2720 mk_corec_transfer_tac ctxt (map (Thm.cterm_of ctxt) Ss) (map (Thm.cterm_of ctxt) Rs) 2721 type_definitions corec_defs xtor_co_rec_transfers pre_rel_defs 2722 live_nesting_rel_eqs (flat pgss) pss qssss gssss) 2723 |> Thm.close_derivation \<^here> 2724 |> Conjunction.elim_balanced (length goals) 2725 end; 2726 2727 fun derive_map_o_corec_thmss lthy0 lthy2 corecs corec_defs = 2728 if live = 0 then 2729 replicate nn [] 2730 else 2731 let 2732 fun variant_names n pre = fst (Variable.variant_fixes (replicate n pre) lthy0); 2733 2734 val maps0 = map map_of_bnf fp_bnfs; 2735 val f_names = variant_names num_As "f"; 2736 val fs = map2 (curry Free) f_names (map (op -->) (As ~~ Bs)); 2737 val live_fs = AList.find (op =) (fs ~~ liveness) true; 2738 2739 val fmaps = map (fn map0 => Term.list_comb (mk_map live As Bs map0, live_fs)) maps0; 2740 2741 val corec_arg_Ts = binder_fun_types (hd (map fastype_of corecs)); 2742 2743 val num_rec_args = length corec_arg_Ts; 2744 val g_names = variant_names num_rec_args "g"; 2745 val gs = map2 (curry Free) g_names corec_arg_Ts; 2746 val gcorecs = map (fn corecx => Term.list_comb (corecx, gs)) corecs; 2747 2748 val map_o_corec_lhss = map2 (curry HOLogic.mk_comp) fmaps gcorecs; 2749 2750 val ABfs = (As ~~ Bs) ~~ fs; 2751 2752 fun mk_map_o_corec_arg corec_argB_T g = 2753 let 2754 val T = range_type (fastype_of g); 2755 val U = range_type corec_argB_T; 2756 in 2757 if T = U then 2758 g 2759 else 2760 HOLogic.mk_comp (build_map lthy2 [] [] (the o AList.lookup (op =) ABfs) (T, U), g) 2761 end; 2762 2763 fun mk_map_o_corec_rhs corecx = 2764 let val args = map2 (mk_map_o_corec_arg o B_ify_T) corec_arg_Ts gs in 2765 Term.list_comb (B_ify corecx, args) 2766 end; 2767 2768 val map_o_corec_rhss = map mk_map_o_corec_rhs corecs; 2769 2770 val map_o_corec_goals = 2771 map2 (fold_rev (fold_rev Logic.all) [fs, gs] o HOLogic.mk_Trueprop oo 2772 curry HOLogic.mk_eq) map_o_corec_lhss map_o_corec_rhss; 2773 2774 val map_o_corec_thms = 2775 @{map 3} (fn goal => fn corec_def => fn dtor_map_o_corec => 2776 Goal.prove_sorry lthy2 [] [] goal (fn {context = ctxt, ...} => 2777 mk_co_rec_o_map_tac ctxt corec_def pre_map_defs live_nesting_map_ident0s 2778 abs_inverses dtor_map_o_corec) 2779 |> Thm.close_derivation \<^here>) 2780 map_o_corec_goals corec_defs xtor_co_rec_o_maps; 2781 in 2782 map single map_o_corec_thms 2783 end; 2784 2785 fun derive_note_coinduct_corecs_thms_for_types 2786 ((((map_thmss, map_disc_iffss, map_selsss, rel_injectss, rel_distinctss, rel_selss, 2787 rel_intross, rel_casess, pred_injectss, set_thmss, set_selsssss, set_introsssss, 2788 set_casess, ctr_transferss, case_transferss, disc_transferss, sel_transferss), 2789 (_, _, ctor_iff_dtors, ctr_defss, ctr_sugars)), 2790 (corecs, corec_defs)), lthy) = 2791 let 2792 val (([(coinduct_thms, coinduct_thm), (coinduct_strong_thms, coinduct_strong_thm)], 2793 (coinduct_attrs, common_coinduct_attrs)), 2794 corec_thmss, corec_disc_thmss, 2795 (corec_disc_iff_thmss, corec_disc_iff_attrs), (corec_sel_thmsss, corec_sel_attrs)) = 2796 derive_coinduct_corecs_thms_for_types lthy pre_bnfs (the corecs_args_types) xtor_co_induct 2797 dtor_injects dtor_ctors xtor_co_rec_thms live_nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss mss 2798 ns abs_inverses abs_inverses I ctr_defss ctr_sugars corecs corec_defs; 2799 2800 fun distinct_prems ctxt thm = 2801 Goal.prove (*no sorry*) ctxt [] [] 2802 (thm |> Thm.prop_of |> Logic.strip_horn |>> distinct (op aconv) |> Logic.list_implies) 2803 (fn _ => HEADGOAL (cut_tac thm THEN' assume_tac ctxt) THEN ALLGOALS eq_assume_tac); 2804 2805 fun eq_ifIN _ [thm] = thm 2806 | eq_ifIN ctxt (thm :: thms) = 2807 distinct_prems ctxt (@{thm eq_ifI} OF 2808 (map (unfold_thms ctxt @{thms atomize_imp[of _ "t = u" for t u]}) 2809 [thm, eq_ifIN ctxt thms])); 2810 2811 val corec_code_thms = map (eq_ifIN lthy) corec_thmss; 2812 val corec_sel_thmss = map flat corec_sel_thmsss; 2813 2814 val coinduct_type_attr = Attrib.internal o K o Induct.coinduct_type; 2815 val coinduct_pred_attr = Attrib.internal o K o Induct.coinduct_pred; 2816 2817 val flat_corec_thms = append oo append; 2818 2819 val corec_transfer_thmss = map single (derive_corec_transfer_thms lthy corecs corec_defs); 2820 2821 val ((rel_coinduct_thmss, common_rel_coinduct_thms), 2822 (rel_coinduct_attrs, common_rel_coinduct_attrs)) = 2823 if live = 0 then 2824 ((replicate nn [], []), ([], [])) 2825 else 2826 let 2827 val ((rel_coinduct_thms, common_rel_coinduct_thm), 2828 (rel_coinduct_attrs, common_rel_coinduct_attrs)) = 2829 derive_rel_coinduct_thms_for_types lthy nn fpTs ns As Bs mss ctr_sugars abs_inverses 2830 abs_injects ctor_injects dtor_ctors pre_rel_defs ctr_defss xtor_rel_co_induct 2831 live_nesting_rel_eqs; 2832 in 2833 ((map single rel_coinduct_thms, single common_rel_coinduct_thm), 2834 (rel_coinduct_attrs, common_rel_coinduct_attrs)) 2835 end; 2836 2837 val map_o_corec_thmss = derive_map_o_corec_thmss lthy lthy corecs corec_defs; 2838 2839 val (set_induct_thms, set_induct_attrss) = 2840 derive_set_induct_thms_for_types lthy nn fpTs (map #ctrs ctr_sugars) 2841 (map (map (mk_set As)) (map sets_of_bnf fp_bnfs)) dtor_set_inducts 2842 (map #exhaust ctr_sugars) (flat pre_set_defss) (flat ctr_defss) dtor_ctors abs_inverses 2843 |> split_list; 2844 2845 val simp_thmss = 2846 @{map 6} mk_simp_thms ctr_sugars 2847 (@{map 3} flat_corec_thms corec_disc_thmss corec_disc_iff_thmss corec_sel_thmss) 2848 map_thmss rel_injectss rel_distinctss set_thmss; 2849 2850 val common_notes = 2851 (set_inductN, set_induct_thms, nth set_induct_attrss) :: 2852 (if nn > 1 then 2853 [(coinductN, [coinduct_thm], K common_coinduct_attrs), 2854 (coinduct_strongN, [coinduct_strong_thm], K common_coinduct_attrs), 2855 (rel_coinductN, common_rel_coinduct_thms, K common_rel_coinduct_attrs)] 2856 else []) 2857 |> massage_simple_notes fp_common_name; 2858 2859 val notes = 2860 [(coinductN, map single coinduct_thms, 2861 fn T_name => coinduct_attrs @ [coinduct_type_attr T_name]), 2862 (coinduct_strongN, map single coinduct_strong_thms, K coinduct_attrs), 2863 (corecN, corec_thmss, K []), 2864 (corec_codeN, map single corec_code_thms, K (nitpicksimp_attrs)), 2865 (corec_discN, corec_disc_thmss, K []), 2866 (corec_disc_iffN, corec_disc_iff_thmss, K corec_disc_iff_attrs), 2867 (corec_selN, corec_sel_thmss, K corec_sel_attrs), 2868 (corec_transferN, corec_transfer_thmss, K []), 2869 (map_o_corecN, map_o_corec_thmss, K []), 2870 (rel_coinductN, rel_coinduct_thmss, K (rel_coinduct_attrs @ [coinduct_pred_attr ""])), 2871 (simpsN, simp_thmss, K [])] 2872 |> massage_multi_notes fp_b_names fpTs; 2873 in 2874 lthy 2875 |> fold (Spec_Rules.add Binding.empty Spec_Rules.equational corecs) 2876 [flat corec_sel_thmss, flat corec_thmss] 2877 |> plugins code_plugin ? Code.declare_default_eqns (map (rpair true) corec_code_thms) 2878 |> Local_Theory.notes (common_notes @ notes) 2879 |-> interpret_bnfs_register_fp_sugars plugins fpTs fpBTs Xs Greatest_FP pre_bnfs absT_infos 2880 fp_nesting_bnfs live_nesting_bnfs fp_res ctrXs_Tsss ctor_iff_dtors ctr_defss ctr_sugars 2881 corecs corec_defs map_thmss [coinduct_thm, coinduct_strong_thm] 2882 (transpose [coinduct_thms, coinduct_strong_thms]) corec_thmss corec_disc_thmss 2883 corec_sel_thmsss rel_injectss rel_distinctss map_disc_iffss map_selsss rel_selss 2884 rel_intross rel_casess pred_injectss set_thmss set_selsssss set_introsssss set_casess 2885 ctr_transferss case_transferss disc_transferss sel_transferss corec_disc_iff_thmss 2886 (map single corec_code_thms) corec_transfer_thmss common_rel_coinduct_thms 2887 rel_coinduct_thmss set_induct_thms (replicate nn (if nn = 1 then set_induct_thms else [])) 2888 map_o_corec_thmss 2889 end; 2890 2891 val lthy = lthy 2892 |> live > 0 ? fold2 (fn Type (s, _) => fn bnf => register_bnf_raw s bnf) fpTs fp_bnfs 2893 |> @{fold_map 29} define_ctrs_dtrs_for_type_etc fp_bnfs fp_bs fpTs Cs Es ctors dtors 2894 xtor_co_recs ctor_dtors dtor_ctors ctor_injects pre_map_defs pre_set_defss pre_rel_defs 2895 xtor_maps xtor_setss xtor_rels ns kss mss abss abs_injects type_definitions ctr_bindingss 2896 ctr_mixfixess ctr_Tsss disc_bindingss sel_bindingsss raw_sel_default_eqss 2897 |> wrap_ctrs_derive_map_set_rel_pred_thms_define_co_rec_for_types 2898 |> case_fp fp derive_note_induct_recs_thms_for_types 2899 derive_note_coinduct_corecs_thms_for_types; 2900 2901 val timer = time (timer ("Constructors, discriminators, selectors, etc., for the new " ^ 2902 co_prefix fp ^ "datatype")); 2903 in 2904 lthy 2905 end; 2906 2907fun co_datatypes fp = define_co_datatypes (K I) (K I) (K I) (K I) fp; 2908 2909fun co_datatype_cmd fp construct_fp options lthy = 2910 define_co_datatypes Plugin_Name.make_filter Typedecl.read_constraint Syntax.parse_typ 2911 Syntax.parse_term fp construct_fp options lthy 2912 handle EMPTY_DATATYPE s => error ("Cannot define empty datatype " ^ quote s); 2913 2914val parse_ctr_arg = 2915 \<^keyword>\<open>(\<close> |-- parse_binding_colon -- Parse.typ --| \<^keyword>\<open>)\<close> 2916 || Parse.typ >> pair Binding.empty; 2917 2918val parse_ctr_specs = 2919 Parse.enum1 "|" (parse_ctr_spec Parse.binding parse_ctr_arg -- Parse.opt_mixfix); 2920 2921val parse_spec = 2922 parse_type_args_named_constrained -- Parse.binding -- Parse.opt_mixfix -- 2923 (\<^keyword>\<open>=\<close> |-- parse_ctr_specs) -- parse_map_rel_pred_bindings -- parse_sel_default_eqs; 2924 2925val parse_co_datatype = parse_ctr_options -- Parse.and_list1 parse_spec; 2926 2927fun parse_co_datatype_cmd fp construct_fp = 2928 parse_co_datatype >> co_datatype_cmd fp construct_fp; 2929 2930end; 2931