1(* Title: HOL/Tools/BNF/bnf_comp.ML 2 Author: Dmitriy Traytel, TU Muenchen 3 Author: Jasmin Blanchette, TU Muenchen 4 Copyright 2012 5 6Composition of bounded natural functors. 7*) 8 9signature BNF_COMP = 10sig 11 val typedef_threshold: int Config.T 12 val with_typedef_threshold: int -> (Proof.context -> Proof.context) -> Proof.context -> 13 Proof.context 14 val with_typedef_threshold_yield: int -> (Proof.context -> 'a * Proof.context) -> Proof.context -> 15 'a * Proof.context 16 17 val ID_bnf: BNF_Def.bnf 18 val DEADID_bnf: BNF_Def.bnf 19 20 type comp_cache 21 type unfold_set = 22 {map_unfolds: thm list, 23 set_unfoldss: thm list list, 24 rel_unfolds: thm list, 25 pred_unfolds: thm list} 26 27 val empty_comp_cache: comp_cache 28 val empty_unfolds: unfold_set 29 30 exception BAD_DEAD of typ * typ 31 32 val bnf_of_typ: bool -> BNF_Def.inline_policy -> (binding -> binding) -> 33 ((string * sort) list list -> (string * sort) list) -> (string * sort) list -> 34 (string * sort) list -> typ -> (comp_cache * unfold_set) * local_theory -> 35 (BNF_Def.bnf * (typ list * typ list)) * ((comp_cache * unfold_set) * local_theory) 36 val default_comp_sort: (string * sort) list list -> (string * sort) list 37 val clean_compose_bnf: BNF_Def.inline_policy -> (binding -> binding) -> binding -> BNF_Def.bnf -> 38 BNF_Def.bnf list -> unfold_set * local_theory -> BNF_Def.bnf * (unfold_set * local_theory) 39 val kill_bnf: (binding -> binding) -> int -> BNF_Def.bnf -> 40 (comp_cache * unfold_set) * local_theory -> 41 BNF_Def.bnf * ((comp_cache * unfold_set) * local_theory) 42 val lift_bnf: (binding -> binding) -> int -> BNF_Def.bnf -> 43 (comp_cache * unfold_set) * local_theory -> 44 BNF_Def.bnf * ((comp_cache * unfold_set) * local_theory) 45 val permute_bnf: (binding -> binding) -> int list -> int list -> BNF_Def.bnf -> 46 (comp_cache * unfold_set) * local_theory -> 47 BNF_Def.bnf * ((comp_cache * unfold_set) * local_theory) 48 val permute_and_kill_bnf: (binding -> binding) -> int -> int list -> int list -> BNF_Def.bnf -> 49 (comp_cache * unfold_set) * local_theory -> 50 BNF_Def.bnf * ((comp_cache * unfold_set) * local_theory) 51 val lift_and_permute_bnf: (binding -> binding) -> int -> int list -> int list -> BNF_Def.bnf -> 52 (comp_cache * unfold_set) * local_theory -> 53 BNF_Def.bnf * ((comp_cache * unfold_set) * local_theory) 54 val normalize_bnfs: (int -> binding -> binding) -> ''a list list -> ''a list -> 55 (''a list list -> ''a list) -> BNF_Def.bnf list -> (comp_cache * unfold_set) * local_theory -> 56 (int list list * ''a list) * (BNF_Def.bnf list * ((comp_cache * unfold_set) * local_theory)) 57 val compose_bnf: BNF_Def.inline_policy -> (int -> binding -> binding) -> 58 ((string * sort) list list -> (string * sort) list) -> BNF_Def.bnf -> BNF_Def.bnf list -> 59 typ list -> typ list list -> typ list list -> (comp_cache * unfold_set) * local_theory -> 60 (BNF_Def.bnf * (typ list * typ list)) * ((comp_cache * unfold_set) * local_theory) 61 type absT_info = 62 {absT: typ, 63 repT: typ, 64 abs: term, 65 rep: term, 66 abs_inject: thm, 67 abs_inverse: thm, 68 type_definition: thm} 69 70 val morph_absT_info: morphism -> absT_info -> absT_info 71 val mk_absT: theory -> typ -> typ -> typ -> typ 72 val mk_repT: typ -> typ -> typ -> typ 73 val mk_abs: typ -> term -> term 74 val mk_rep: typ -> term -> term 75 val seal_bnf: (binding -> binding) -> unfold_set -> binding -> bool -> typ list -> typ list -> 76 BNF_Def.bnf -> local_theory -> (BNF_Def.bnf * (typ list * absT_info)) * local_theory 77end; 78 79structure BNF_Comp : BNF_COMP = 80struct 81 82open BNF_Def 83open BNF_Util 84open BNF_Tactics 85open BNF_Comp_Tactics 86 87val typedef_threshold = Attrib.setup_config_int \<^binding>\<open>bnf_typedef_threshold\<close> (K 6); 88 89fun with_typedef_threshold threshold f lthy = 90 lthy 91 |> Config.put typedef_threshold threshold 92 |> f 93 |> Config.put typedef_threshold (Config.get lthy typedef_threshold); 94 95fun with_typedef_threshold_yield threshold f lthy = 96 lthy 97 |> Config.put typedef_threshold threshold 98 |> f 99 ||> Config.put typedef_threshold (Config.get lthy typedef_threshold); 100 101val ID_bnf = the (bnf_of \<^context> "BNF_Composition.ID"); 102val DEADID_bnf = the (bnf_of \<^context> "BNF_Composition.DEADID"); 103 104type comp_cache = (bnf * (typ list * typ list)) Typtab.table; 105 106fun key_of_types s Ts = Type (s, Ts); 107fun key_of_typess s = key_of_types s o map (key_of_types ""); 108fun typ_of_int n = Type (string_of_int n, []); 109fun typ_of_bnf bnf = 110 key_of_typess "" [[T_of_bnf bnf], lives_of_bnf bnf, sort Term_Ord.typ_ord (deads_of_bnf bnf)]; 111 112fun key_of_kill n bnf = key_of_types "k" [typ_of_int n, typ_of_bnf bnf]; 113fun key_of_lift n bnf = key_of_types "l" [typ_of_int n, typ_of_bnf bnf]; 114fun key_of_permute src dest bnf = 115 key_of_types "p" (map typ_of_int src @ map typ_of_int dest @ [typ_of_bnf bnf]); 116fun key_of_compose oDs Dss Ass outer inners = 117 key_of_types "c" (map (key_of_typess "") [[oDs], Dss, Ass, [map typ_of_bnf (outer :: inners)]]); 118 119fun cache_comp_simple key cache (bnf, (unfold_set, lthy)) = 120 (bnf, ((Typtab.update (key, (bnf, ([], []))) cache, unfold_set), lthy)); 121 122fun cache_comp key (bnf_Ds_As, ((cache, unfold_set), lthy)) = 123 (bnf_Ds_As, ((Typtab.update (key, bnf_Ds_As) cache, unfold_set), lthy)); 124 125type unfold_set = { 126 map_unfolds: thm list, 127 set_unfoldss: thm list list, 128 rel_unfolds: thm list, 129 pred_unfolds: thm list 130}; 131 132val empty_comp_cache = Typtab.empty; 133val empty_unfolds = {map_unfolds = [], set_unfoldss = [], rel_unfolds = [], pred_unfolds = []}; 134 135fun add_to_thms thms new = thms |> not (Thm.is_reflexive new) ? insert Thm.eq_thm new; 136fun adds_to_thms thms news = insert (eq_set Thm.eq_thm) (no_reflexive news) thms; 137 138fun add_to_unfolds map sets rel pred 139 {map_unfolds, set_unfoldss, rel_unfolds, pred_unfolds} = 140 {map_unfolds = add_to_thms map_unfolds map, 141 set_unfoldss = adds_to_thms set_unfoldss sets, 142 rel_unfolds = add_to_thms rel_unfolds rel, 143 pred_unfolds = add_to_thms pred_unfolds pred}; 144 145fun add_bnf_to_unfolds bnf = 146 add_to_unfolds (map_def_of_bnf bnf) (set_defs_of_bnf bnf) (rel_def_of_bnf bnf) (pred_def_of_bnf bnf); 147 148val bdTN = "bdT"; 149 150fun mk_killN n = "_kill" ^ string_of_int n; 151fun mk_liftN n = "_lift" ^ string_of_int n; 152fun mk_permuteN src dest = 153 "_permute_" ^ implode (map string_of_int src) ^ "_" ^ implode (map string_of_int dest); 154 155 156(*copied from Envir.expand_term_free*) 157fun expand_term_const defs = 158 let 159 val eqs = map ((fn ((x, U), u) => (x, (U, u))) o apfst dest_Const) defs; 160 val get = fn Const (x, _) => AList.lookup (op =) eqs x | _ => NONE; 161 in Envir.expand_term get end; 162 163val id_bnf_def = @{thm id_bnf_def}; 164val expand_id_bnf_def = expand_term_const [Thm.prop_of id_bnf_def |> Logic.dest_equals]; 165 166fun is_sum_prod_natLeq (Const (\<^const_name>\<open>csum\<close>, _) $ t $ u) = forall is_sum_prod_natLeq [t, u] 167 | is_sum_prod_natLeq (Const (\<^const_name>\<open>cprod\<close>, _) $ t $ u) = forall is_sum_prod_natLeq [t, u] 168 | is_sum_prod_natLeq t = t aconv \<^term>\<open>natLeq\<close>; 169 170fun clean_compose_bnf const_policy qualify b outer inners (unfold_set, lthy) = 171 let 172 val olive = live_of_bnf outer; 173 val onwits = nwits_of_bnf outer; 174 val odeads = deads_of_bnf outer; 175 val inner = hd inners; 176 val ilive = live_of_bnf inner; 177 val ideadss = map deads_of_bnf inners; 178 val inwitss = map nwits_of_bnf inners; 179 180 (* TODO: check olive = length inners > 0, 181 forall inner from inners. ilive = live, 182 forall inner from inners. idead = dead *) 183 184 val (oDs, lthy1) = apfst (map TFree) 185 (Variable.invent_types (map Type.sort_of_atyp odeads) lthy); 186 val (Dss, lthy2) = apfst (map (map TFree)) 187 (fold_map Variable.invent_types (map (map Type.sort_of_atyp) ideadss) lthy1); 188 val (Ass, lthy3) = apfst (replicate ilive o map TFree) 189 (Variable.invent_types (replicate ilive \<^sort>\<open>type\<close>) lthy2); 190 val As = if ilive > 0 then hd Ass else []; 191 val Ass_repl = replicate olive As; 192 val (Bs, names_lthy) = apfst (map TFree) 193 (Variable.invent_types (replicate ilive \<^sort>\<open>type\<close>) lthy3); 194 val Bss_repl = replicate olive Bs; 195 196 val (((((fs', Qs'), Ps'), Asets), xs), _) = names_lthy 197 |> apfst snd o mk_Frees' "f" (map2 (curry op -->) As Bs) 198 ||>> apfst snd o mk_Frees' "Q" (map2 mk_pred2T As Bs) 199 ||>> apfst snd o mk_Frees' "P" (map mk_pred1T As) 200 ||>> mk_Frees "A" (map HOLogic.mk_setT As) 201 ||>> mk_Frees "x" As; 202 203 val CAs = @{map 3} mk_T_of_bnf Dss Ass_repl inners; 204 val CCA = mk_T_of_bnf oDs CAs outer; 205 val CBs = @{map 3} mk_T_of_bnf Dss Bss_repl inners; 206 val outer_sets = mk_sets_of_bnf (replicate olive oDs) (replicate olive CAs) outer; 207 val inner_setss = 208 @{map 3} mk_sets_of_bnf (map (replicate ilive) Dss) (replicate olive Ass) inners; 209 val inner_bds = @{map 3} mk_bd_of_bnf Dss Ass_repl inners; 210 val outer_bd = mk_bd_of_bnf oDs CAs outer; 211 212 (*%f1 ... fn. outer.map (inner_1.map f1 ... fn) ... (inner_m.map f1 ... fn)*) 213 val mapx = fold_rev Term.abs fs' 214 (Term.list_comb (mk_map_of_bnf oDs CAs CBs outer, 215 map2 (fn Ds => (fn f => Term.list_comb (f, map Bound (ilive - 1 downto 0))) o 216 mk_map_of_bnf Ds As Bs) Dss inners)); 217 (*%Q1 ... Qn. outer.rel (inner_1.rel Q1 ... Qn) ... (inner_m.rel Q1 ... Qn)*) 218 val rel = fold_rev Term.abs Qs' 219 (Term.list_comb (mk_rel_of_bnf oDs CAs CBs outer, 220 map2 (fn Ds => (fn f => Term.list_comb (f, map Bound (ilive - 1 downto 0))) o 221 mk_rel_of_bnf Ds As Bs) Dss inners)); 222 (*%P1 ... Pn. outer.pred (inner_1.pred P1 ... Pn) ... (inner_m.pred P1 ... Pn)*) 223 val pred = fold_rev Term.abs Ps' 224 (Term.list_comb (mk_pred_of_bnf oDs CAs outer, 225 map2 (fn Ds => (fn f => Term.list_comb (f, map Bound (ilive - 1 downto 0))) o 226 mk_pred_of_bnf Ds As) Dss inners)); 227 228 (*Union o collect {outer.set_1 ... outer.set_m} o outer.map inner_1.set_i ... inner_m.set_i*) 229 (*Union o collect {image inner_1.set_i o outer.set_1 ... image inner_m.set_i o outer.set_m}*) 230 fun mk_set i = 231 let 232 val (setTs, T) = `(replicate olive o HOLogic.mk_setT) (nth As i); 233 val outer_set = mk_collect 234 (mk_sets_of_bnf (replicate olive oDs) (replicate olive setTs) outer) 235 (mk_T_of_bnf oDs setTs outer --> HOLogic.mk_setT T); 236 val inner_sets = map (fn sets => nth sets i) inner_setss; 237 val outer_map = mk_map_of_bnf oDs CAs setTs outer; 238 val map_inner_sets = Term.list_comb (outer_map, inner_sets); 239 val collect_image = mk_collect 240 (map2 (fn f => fn set => HOLogic.mk_comp (mk_image f, set)) inner_sets outer_sets) 241 (CCA --> HOLogic.mk_setT T); 242 in 243 (Library.foldl1 HOLogic.mk_comp [mk_Union T, outer_set, map_inner_sets], 244 HOLogic.mk_comp (mk_Union T, collect_image)) 245 end; 246 247 val (sets, sets_alt) = map_split mk_set (0 upto ilive - 1); 248 249 fun mk_simplified_set set = 250 let 251 val setT = fastype_of set; 252 val var_set' = Const (\<^const_name>\<open>id_bnf\<close>, setT --> setT) $ Var ((Name.uu, 0), setT); 253 val goal = mk_Trueprop_eq (var_set', set); 254 fun tac {context = ctxt, prems = _} = 255 mk_simplified_set_tac ctxt (collect_set_map_of_bnf outer); 256 val set'_eq_set = 257 Goal.prove (*no sorry*) names_lthy [] [] goal tac 258 |> Thm.close_derivation \<^here>; 259 val set' = fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of set'_eq_set))); 260 in 261 (set', set'_eq_set) 262 end; 263 264 val (sets', set'_eq_sets) = 265 map_split mk_simplified_set sets 266 ||> Proof_Context.export names_lthy lthy; 267 268 (*(inner_1.bd +c ... +c inner_m.bd) *c outer.bd*) 269 val bd = mk_cprod (Library.foldr1 (uncurry mk_csum) inner_bds) outer_bd; 270 271 val (bd', bd_ordIso_natLeq_thm_opt) = 272 if is_sum_prod_natLeq bd then 273 let 274 val bd' = \<^term>\<open>natLeq\<close>; 275 val bd_bd' = HOLogic.mk_prod (bd, bd'); 276 val ordIso = Const (\<^const_name>\<open>ordIso\<close>, HOLogic.mk_setT (fastype_of bd_bd')); 277 val goal = mk_Trueprop_mem (bd_bd', ordIso); 278 in 279 (bd', SOME (Goal.prove_sorry lthy [] [] goal (bd_ordIso_natLeq_tac o #context) 280 |> Thm.close_derivation \<^here>)) 281 end 282 else 283 (bd, NONE); 284 285 fun map_id0_tac ctxt = 286 mk_comp_map_id0_tac ctxt (map_id0_of_bnf outer) (map_cong0_of_bnf outer) 287 (map map_id0_of_bnf inners); 288 289 fun map_comp0_tac ctxt = 290 mk_comp_map_comp0_tac ctxt (map_comp0_of_bnf outer) (map_cong0_of_bnf outer) 291 (map map_comp0_of_bnf inners); 292 293 fun mk_single_set_map0_tac i ctxt = 294 mk_comp_set_map0_tac ctxt (nth set'_eq_sets i) (map_comp0_of_bnf outer) 295 (map_cong0_of_bnf outer) (collect_set_map_of_bnf outer) 296 (map ((fn thms => nth thms i) o set_map0_of_bnf) inners); 297 298 val set_map0_tacs = map mk_single_set_map0_tac (0 upto ilive - 1); 299 300 fun bd_card_order_tac ctxt = 301 mk_comp_bd_card_order_tac ctxt (map bd_card_order_of_bnf inners) (bd_card_order_of_bnf outer); 302 303 fun bd_cinfinite_tac ctxt = 304 mk_comp_bd_cinfinite_tac ctxt (bd_cinfinite_of_bnf inner) (bd_cinfinite_of_bnf outer); 305 306 val set_alt_thms = 307 if Config.get lthy quick_and_dirty then 308 [] 309 else 310 map (fn goal => 311 Goal.prove_sorry lthy [] [] goal 312 (fn {context = ctxt, prems = _} => 313 mk_comp_set_alt_tac ctxt (collect_set_map_of_bnf outer)) 314 |> Thm.close_derivation \<^here>) 315 (map2 (curry mk_Trueprop_eq) sets sets_alt); 316 317 fun map_cong0_tac ctxt = 318 mk_comp_map_cong0_tac ctxt set'_eq_sets set_alt_thms (map_cong0_of_bnf outer) 319 (map map_cong0_of_bnf inners); 320 321 val set_bd_tacs = 322 if Config.get lthy quick_and_dirty then 323 replicate ilive (K all_tac) 324 else 325 let 326 val outer_set_bds = set_bd_of_bnf outer; 327 val inner_set_bdss = map set_bd_of_bnf inners; 328 val inner_bd_Card_orders = map bd_Card_order_of_bnf inners; 329 fun single_set_bd_thm i j = 330 @{thm comp_single_set_bd} OF [nth inner_bd_Card_orders j, nth (nth inner_set_bdss j) i, 331 nth outer_set_bds j] 332 val single_set_bd_thmss = 333 map ((fn f => map f (0 upto olive - 1)) o single_set_bd_thm) (0 upto ilive - 1); 334 in 335 @{map 3} (fn set'_eq_set => fn set_alt => fn single_set_bds => fn ctxt => 336 mk_comp_set_bd_tac ctxt set'_eq_set bd_ordIso_natLeq_thm_opt set_alt single_set_bds) 337 set'_eq_sets set_alt_thms single_set_bd_thmss 338 end; 339 340 val in_alt_thm = 341 let 342 val inx = mk_in Asets sets CCA; 343 val in_alt = mk_in (map2 (mk_in Asets) inner_setss CAs) outer_sets CCA; 344 val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (inx, in_alt)); 345 in 346 Goal.prove_sorry lthy [] [] goal 347 (fn {context = ctxt, prems = _} => mk_comp_in_alt_tac ctxt set_alt_thms) 348 |> Thm.close_derivation \<^here> 349 end; 350 351 fun le_rel_OO_tac ctxt = mk_le_rel_OO_tac ctxt (le_rel_OO_of_bnf outer) (rel_mono_of_bnf outer) 352 (map le_rel_OO_of_bnf inners); 353 354 fun rel_OO_Grp_tac ctxt = 355 let 356 val outer_rel_Grp = rel_Grp_of_bnf outer RS sym; 357 val thm = 358 trans OF [in_alt_thm RS @{thm OO_Grp_cong}, 359 trans OF [@{thm arg_cong2[of _ _ _ _ relcompp]} OF 360 [trans OF [outer_rel_Grp RS @{thm arg_cong[of _ _ conversep]}, 361 rel_conversep_of_bnf outer RS sym], outer_rel_Grp], 362 trans OF [rel_OO_of_bnf outer RS sym, rel_cong0_of_bnf outer OF 363 (map (fn bnf => rel_OO_Grp_of_bnf bnf RS sym) inners)]]] RS sym; 364 in 365 unfold_thms_tac ctxt set'_eq_sets THEN rtac ctxt thm 1 366 end; 367 368 fun pred_set_tac ctxt = 369 let 370 val pred_alt = unfold_thms ctxt @{thms Ball_Collect} 371 (trans OF [pred_cong0_of_bnf outer OF map pred_set_of_bnf inners, pred_set_of_bnf outer]); 372 val in_alt = in_alt_thm RS @{thm Collect_inj} RS sym; 373 in 374 unfold_thms_tac ctxt (@{thm Ball_Collect} :: set'_eq_sets) THEN 375 HEADGOAL (rtac ctxt (trans OF [pred_alt, in_alt])) 376 end 377 378 val tacs = zip_axioms map_id0_tac map_comp0_tac map_cong0_tac set_map0_tacs bd_card_order_tac 379 bd_cinfinite_tac set_bd_tacs le_rel_OO_tac rel_OO_Grp_tac pred_set_tac; 380 381 val outer_wits = mk_wits_of_bnf (replicate onwits oDs) (replicate onwits CAs) outer; 382 383 val inner_witss = map (map (fn (I, wit) => Term.list_comb (wit, map (nth xs) I))) 384 (@{map 3} (fn Ds => fn n => mk_wits_of_bnf (replicate n Ds) (replicate n As)) 385 Dss inwitss inners); 386 387 val inner_witsss = map (map (nth inner_witss) o fst) outer_wits; 388 389 val wits = (inner_witsss, (map (single o snd) outer_wits)) 390 |-> map2 (fold (map_product (fn iwit => fn owit => owit $ iwit))) 391 |> flat 392 |> map (`(fn t => Term.add_frees t [])) 393 |> minimize_wits 394 |> map (fn (frees, t) => fold absfree frees t); 395 396 fun wit_tac ctxt = 397 mk_comp_wit_tac ctxt set'_eq_sets (wit_thms_of_bnf outer) (collect_set_map_of_bnf outer) 398 (maps wit_thms_of_bnf inners); 399 400 val (bnf', lthy') = 401 bnf_def const_policy (K Dont_Note) true qualify tacs wit_tac (SOME (oDs @ flat Dss)) 402 Binding.empty Binding.empty Binding.empty [] 403 (((((((b, CCA), mapx), sets'), bd'), wits), SOME rel), SOME pred) lthy; 404 405 val phi = 406 Morphism.thm_morphism "BNF" (unfold_thms lthy' [id_bnf_def]) 407 $> Morphism.term_morphism "BNF" expand_id_bnf_def; 408 409 val bnf'' = morph_bnf phi bnf'; 410 in 411 (bnf'', (add_bnf_to_unfolds bnf'' unfold_set, lthy')) 412 end; 413 414(* Killing live variables *) 415 416fun raw_kill_bnf qualify n bnf (accum as (unfold_set, lthy)) = 417 if n = 0 then (bnf, accum) else 418 let 419 val b = Binding.suffix_name (mk_killN n) (name_of_bnf bnf); 420 val live = live_of_bnf bnf; 421 val deads = deads_of_bnf bnf; 422 val nwits = nwits_of_bnf bnf; 423 424 (* TODO: check 0 < n <= live *) 425 426 val (Ds, lthy1) = apfst (map TFree) 427 (Variable.invent_types (map Type.sort_of_atyp deads) lthy); 428 val ((killedAs, As), lthy2) = apfst (`(take n) o map TFree) 429 (Variable.invent_types (replicate live \<^sort>\<open>type\<close>) lthy1); 430 val (Bs, _(*lthy3*)) = apfst (append killedAs o map TFree) 431 (Variable.invent_types (replicate (live - n) \<^sort>\<open>type\<close>) lthy2); 432 433 val ((Asets, lives), _(*names_lthy*)) = lthy 434 |> mk_Frees "A" (map HOLogic.mk_setT (drop n As)) 435 ||>> mk_Frees "x" (drop n As); 436 val xs = map (fn T => Const (\<^const_name>\<open>undefined\<close>, T)) killedAs @ lives; 437 438 val T = mk_T_of_bnf Ds As bnf; 439 440 (*bnf.map id ... id*) 441 val mapx = Term.list_comb (mk_map_of_bnf Ds As Bs bnf, map HOLogic.id_const killedAs); 442 (*bnf.rel (op =) ... (op =)*) 443 val rel = Term.list_comb (mk_rel_of_bnf Ds As Bs bnf, map HOLogic.eq_const killedAs); 444 (*bnf.pred (%_. True) ... (%_ True)*) 445 val pred = Term.list_comb (mk_pred_of_bnf Ds As bnf, 446 map (fn T => Term.absdummy T \<^term>\<open>True\<close>) killedAs); 447 448 val bnf_sets = mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf; 449 val sets = drop n bnf_sets; 450 451 val bd = mk_bd_of_bnf Ds As bnf; 452 453 fun map_id0_tac ctxt = rtac ctxt (map_id0_of_bnf bnf) 1; 454 fun map_comp0_tac ctxt = 455 unfold_thms_tac ctxt ((map_comp0_of_bnf bnf RS sym) :: 456 @{thms comp_assoc id_comp comp_id}) THEN rtac ctxt refl 1; 457 fun map_cong0_tac ctxt = 458 mk_kill_map_cong0_tac ctxt n (live - n) (map_cong0_of_bnf bnf); 459 val set_map0_tacs = map (fn thm => fn ctxt => rtac ctxt thm 1) (drop n (set_map0_of_bnf bnf)); 460 fun bd_card_order_tac ctxt = rtac ctxt (bd_card_order_of_bnf bnf) 1; 461 fun bd_cinfinite_tac ctxt = rtac ctxt (bd_cinfinite_of_bnf bnf) 1; 462 val set_bd_tacs = map (fn thm => fn ctxt => rtac ctxt thm 1) (drop n (set_bd_of_bnf bnf)); 463 464 val in_alt_thm = 465 let 466 val inx = mk_in Asets sets T; 467 val in_alt = mk_in (map HOLogic.mk_UNIV killedAs @ Asets) bnf_sets T; 468 val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (inx, in_alt)); 469 in 470 Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} => 471 kill_in_alt_tac ctxt) |> Thm.close_derivation \<^here> 472 end; 473 474 fun le_rel_OO_tac ctxt = 475 EVERY' [rtac ctxt @{thm ord_le_eq_trans}, rtac ctxt (le_rel_OO_of_bnf bnf)] 1 THEN 476 unfold_thms_tac ctxt @{thms eq_OO} THEN rtac ctxt refl 1; 477 478 fun rel_OO_Grp_tac ctxt = 479 let 480 val rel_Grp = rel_Grp_of_bnf bnf RS sym 481 val thm = 482 (trans OF [in_alt_thm RS @{thm OO_Grp_cong}, 483 trans OF [@{thm arg_cong2[of _ _ _ _ relcompp]} OF 484 [trans OF [rel_Grp RS @{thm arg_cong[of _ _ conversep]}, 485 rel_conversep_of_bnf bnf RS sym], rel_Grp], 486 trans OF [rel_OO_of_bnf bnf RS sym, rel_cong0_of_bnf bnf OF 487 (replicate n @{thm trans[OF Grp_UNIV_id[OF refl] eq_alt[symmetric]]} @ 488 replicate (live - n) @{thm Grp_fst_snd})]]] RS sym); 489 in 490 rtac ctxt thm 1 491 end; 492 493 fun pred_set_tac ctxt = mk_simple_pred_set_tac ctxt (pred_set_of_bnf bnf) in_alt_thm; 494 495 val tacs = zip_axioms map_id0_tac map_comp0_tac map_cong0_tac set_map0_tacs bd_card_order_tac 496 bd_cinfinite_tac set_bd_tacs le_rel_OO_tac rel_OO_Grp_tac pred_set_tac; 497 498 val bnf_wits = mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf; 499 500 val wits = map (fn t => fold absfree (Term.add_frees t []) t) 501 (map (fn (I, wit) => Term.list_comb (wit, map (nth xs) I)) bnf_wits); 502 503 fun wit_tac ctxt = mk_simple_wit_tac ctxt (wit_thms_of_bnf bnf); 504 505 val (bnf', lthy') = 506 bnf_def Smart_Inline (K Dont_Note) true qualify tacs wit_tac (SOME (Ds @ killedAs)) 507 Binding.empty Binding.empty Binding.empty [] 508 (((((((b, T), mapx), sets), bd), wits), SOME rel), SOME pred) lthy; 509 in 510 (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy')) 511 end; 512 513fun kill_bnf qualify n bnf (accum as ((cache, unfold_set), lthy)) = 514 let val key = key_of_kill n bnf in 515 (case Typtab.lookup cache key of 516 SOME (bnf, _) => (bnf, accum) 517 | NONE => cache_comp_simple key cache (raw_kill_bnf qualify n bnf (unfold_set, lthy))) 518 end; 519 520(* Adding dummy live variables *) 521 522fun raw_lift_bnf qualify n bnf (accum as (unfold_set, lthy)) = 523 if n = 0 then (bnf, accum) else 524 let 525 val b = Binding.suffix_name (mk_liftN n) (name_of_bnf bnf); 526 val live = live_of_bnf bnf; 527 val deads = deads_of_bnf bnf; 528 val nwits = nwits_of_bnf bnf; 529 530 (* TODO: check 0 < n *) 531 532 val (Ds, lthy1) = apfst (map TFree) 533 (Variable.invent_types (map Type.sort_of_atyp deads) lthy); 534 val ((newAs, As), lthy2) = apfst (chop n o map TFree) 535 (Variable.invent_types (replicate (n + live) \<^sort>\<open>type\<close>) lthy1); 536 val ((newBs, Bs), _(*lthy3*)) = apfst (chop n o map TFree) 537 (Variable.invent_types (replicate (n + live) \<^sort>\<open>type\<close>) lthy2); 538 539 val (Asets, _(*names_lthy*)) = lthy 540 |> mk_Frees "A" (map HOLogic.mk_setT (newAs @ As)); 541 542 val T = mk_T_of_bnf Ds As bnf; 543 544 (*%f1 ... fn. bnf.map*) 545 val mapx = 546 fold_rev Term.absdummy (map2 (curry op -->) newAs newBs) (mk_map_of_bnf Ds As Bs bnf); 547 (*%Q1 ... Qn. bnf.rel*) 548 val rel = fold_rev Term.absdummy (map2 mk_pred2T newAs newBs) (mk_rel_of_bnf Ds As Bs bnf); 549 (*%P1 ... Pn. bnf.pred*) 550 val pred = fold_rev Term.absdummy (map mk_pred1T newAs) (mk_pred_of_bnf Ds As bnf); 551 552 val bnf_sets = mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf; 553 val sets = map (fn A => absdummy T (HOLogic.mk_set A [])) newAs @ bnf_sets; 554 555 val bd = mk_bd_of_bnf Ds As bnf; 556 557 fun map_id0_tac ctxt = rtac ctxt (map_id0_of_bnf bnf) 1; 558 fun map_comp0_tac ctxt = 559 unfold_thms_tac ctxt ((map_comp0_of_bnf bnf RS sym) :: 560 @{thms comp_assoc id_comp comp_id}) THEN rtac ctxt refl 1; 561 fun map_cong0_tac ctxt = 562 rtac ctxt (map_cong0_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac ctxt 1); 563 val set_map0_tacs = 564 if Config.get lthy quick_and_dirty then 565 replicate (n + live) (K all_tac) 566 else 567 replicate n empty_natural_tac @ 568 map (fn thm => fn ctxt => rtac ctxt thm 1) (set_map0_of_bnf bnf); 569 fun bd_card_order_tac ctxt = rtac ctxt (bd_card_order_of_bnf bnf) 1; 570 fun bd_cinfinite_tac ctxt = rtac ctxt (bd_cinfinite_of_bnf bnf) 1; 571 val set_bd_tacs = 572 if Config.get lthy quick_and_dirty then 573 replicate (n + live) (K all_tac) 574 else 575 replicate n (fn ctxt => mk_lift_set_bd_tac ctxt (bd_Card_order_of_bnf bnf)) @ 576 (map (fn thm => fn ctxt => rtac ctxt thm 1) (set_bd_of_bnf bnf)); 577 578 val in_alt_thm = 579 let 580 val inx = mk_in Asets sets T; 581 val in_alt = mk_in (drop n Asets) bnf_sets T; 582 val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (inx, in_alt)); 583 in 584 Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} => lift_in_alt_tac ctxt) 585 |> Thm.close_derivation \<^here> 586 end; 587 588 fun le_rel_OO_tac ctxt = rtac ctxt (le_rel_OO_of_bnf bnf) 1; 589 590 fun rel_OO_Grp_tac ctxt = mk_simple_rel_OO_Grp_tac ctxt (rel_OO_Grp_of_bnf bnf) in_alt_thm; 591 592 fun pred_set_tac ctxt = mk_simple_pred_set_tac ctxt (pred_set_of_bnf bnf) in_alt_thm; 593 594 val tacs = zip_axioms map_id0_tac map_comp0_tac map_cong0_tac set_map0_tacs bd_card_order_tac 595 bd_cinfinite_tac set_bd_tacs le_rel_OO_tac rel_OO_Grp_tac pred_set_tac; 596 597 val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf); 598 599 fun wit_tac ctxt = mk_simple_wit_tac ctxt (wit_thms_of_bnf bnf); 600 601 val (bnf', lthy') = 602 bnf_def Smart_Inline (K Dont_Note) true qualify tacs wit_tac (SOME Ds) Binding.empty 603 Binding.empty Binding.empty [] 604 (((((((b, T), mapx), sets), bd), wits), SOME rel), SOME pred) lthy; 605 in 606 (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy')) 607 end; 608 609fun lift_bnf qualify n bnf (accum as ((cache, unfold_set), lthy)) = 610 let val key = key_of_lift n bnf in 611 (case Typtab.lookup cache key of 612 SOME (bnf, _) => (bnf, accum) 613 | NONE => cache_comp_simple key cache (raw_lift_bnf qualify n bnf (unfold_set, lthy))) 614 end; 615 616(* Changing the order of live variables *) 617 618fun raw_permute_bnf qualify src dest bnf (accum as (unfold_set, lthy)) = 619 if src = dest then (bnf, accum) else 620 let 621 val b = Binding.suffix_name (mk_permuteN src dest) (name_of_bnf bnf) |> Binding.reset_pos; 622 val live = live_of_bnf bnf; 623 val deads = deads_of_bnf bnf; 624 val nwits = nwits_of_bnf bnf; 625 626 fun permute xs = permute_like_unique (op =) src dest xs; 627 fun unpermute xs = permute_like_unique (op =) dest src xs; 628 629 val (Ds, lthy1) = apfst (map TFree) 630 (Variable.invent_types (map Type.sort_of_atyp deads) lthy); 631 val (As, lthy2) = apfst (map TFree) 632 (Variable.invent_types (replicate live \<^sort>\<open>type\<close>) lthy1); 633 val (Bs, _(*lthy3*)) = apfst (map TFree) 634 (Variable.invent_types (replicate live \<^sort>\<open>type\<close>) lthy2); 635 636 val (Asets, _(*names_lthy*)) = lthy 637 |> mk_Frees "A" (map HOLogic.mk_setT (permute As)); 638 639 val T = mk_T_of_bnf Ds As bnf; 640 641 (*%f(1) ... f(n). bnf.map f\<sigma>(1) ... f\<sigma>(n)*) 642 val mapx = fold_rev Term.absdummy (permute (map2 (curry op -->) As Bs)) 643 (Term.list_comb (mk_map_of_bnf Ds As Bs bnf, unpermute (map Bound (live - 1 downto 0)))); 644 (*%Q(1) ... Q(n). bnf.rel Q\<sigma>(1) ... Q\<sigma>(n)*) 645 val rel = fold_rev Term.absdummy (permute (map2 mk_pred2T As Bs)) 646 (Term.list_comb (mk_rel_of_bnf Ds As Bs bnf, unpermute (map Bound (live - 1 downto 0)))); 647 (*%P(1) ... P(n). bnf.pred P\<sigma>(1) ... P\<sigma>(n)*) 648 val pred = fold_rev Term.absdummy (permute (map mk_pred1T As)) 649 (Term.list_comb (mk_pred_of_bnf Ds As bnf, unpermute (map Bound (live - 1 downto 0)))); 650 651 val bnf_sets = mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf; 652 val sets = permute bnf_sets; 653 654 val bd = mk_bd_of_bnf Ds As bnf; 655 656 fun map_id0_tac ctxt = rtac ctxt (map_id0_of_bnf bnf) 1; 657 fun map_comp0_tac ctxt = rtac ctxt (map_comp0_of_bnf bnf) 1; 658 fun map_cong0_tac ctxt = 659 rtac ctxt (map_cong0_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac ctxt 1); 660 val set_map0_tacs = permute (map (fn thm => fn ctxt => rtac ctxt thm 1) (set_map0_of_bnf bnf)); 661 fun bd_card_order_tac ctxt = rtac ctxt (bd_card_order_of_bnf bnf) 1; 662 fun bd_cinfinite_tac ctxt = rtac ctxt (bd_cinfinite_of_bnf bnf) 1; 663 val set_bd_tacs = permute (map (fn thm => fn ctxt => rtac ctxt thm 1) (set_bd_of_bnf bnf)); 664 665 val in_alt_thm = 666 let 667 val inx = mk_in Asets sets T; 668 val in_alt = mk_in (unpermute Asets) bnf_sets T; 669 val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (inx, in_alt)); 670 in 671 Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} => 672 mk_permute_in_alt_tac ctxt src dest) 673 |> Thm.close_derivation \<^here> 674 end; 675 676 fun le_rel_OO_tac ctxt = rtac ctxt (le_rel_OO_of_bnf bnf) 1; 677 678 fun rel_OO_Grp_tac ctxt = mk_simple_rel_OO_Grp_tac ctxt (rel_OO_Grp_of_bnf bnf) in_alt_thm; 679 680 fun pred_set_tac ctxt = mk_simple_pred_set_tac ctxt (pred_set_of_bnf bnf) in_alt_thm; 681 682 val tacs = zip_axioms map_id0_tac map_comp0_tac map_cong0_tac set_map0_tacs bd_card_order_tac 683 bd_cinfinite_tac set_bd_tacs le_rel_OO_tac rel_OO_Grp_tac pred_set_tac; 684 685 val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf); 686 687 fun wit_tac ctxt = mk_simple_wit_tac ctxt (wit_thms_of_bnf bnf); 688 689 val (bnf', lthy') = 690 bnf_def Smart_Inline (K Dont_Note) true qualify tacs wit_tac (SOME Ds) Binding.empty 691 Binding.empty Binding.empty [] 692 (((((((b, T), mapx), sets), bd), wits), SOME rel), SOME pred) lthy; 693 in 694 (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy')) 695 end; 696 697fun permute_bnf qualify src dest bnf (accum as ((cache, unfold_set), lthy)) = 698 let val key = key_of_permute src dest bnf in 699 (case Typtab.lookup cache key of 700 SOME (bnf, _) => (bnf, accum) 701 | NONE => cache_comp_simple key cache (raw_permute_bnf qualify src dest bnf (unfold_set, lthy))) 702 end; 703 704(* Composition pipeline *) 705 706fun permute_and_kill_bnf qualify n src dest bnf = 707 permute_bnf qualify src dest bnf 708 #> uncurry (kill_bnf qualify n); 709 710fun lift_and_permute_bnf qualify n src dest bnf = 711 lift_bnf qualify n bnf 712 #> uncurry (permute_bnf qualify src dest); 713 714fun normalize_bnfs qualify Ass Ds flatten_tyargs bnfs accum = 715 let 716 val before_kill_src = map (fn As => 0 upto (length As - 1)) Ass; 717 val kill_poss = map (find_indices op = Ds) Ass; 718 val live_poss = map2 (subtract op =) kill_poss before_kill_src; 719 val before_kill_dest = map2 append kill_poss live_poss; 720 val kill_ns = map length kill_poss; 721 val (inners', accum') = 722 @{fold_map 5} (permute_and_kill_bnf o qualify) 723 (if length bnfs = 1 then [0] else 1 upto length bnfs) 724 kill_ns before_kill_src before_kill_dest bnfs accum; 725 726 val Ass' = map2 (map o nth) Ass live_poss; 727 val As = flatten_tyargs Ass'; 728 val after_lift_dest = replicate (length Ass') (0 upto (length As - 1)); 729 val old_poss = map (map (fn x => find_index (fn y => x = y) As)) Ass'; 730 val new_poss = map2 (subtract op =) old_poss after_lift_dest; 731 val after_lift_src = map2 append new_poss old_poss; 732 val lift_ns = map (fn xs => length As - length xs) Ass'; 733 in 734 ((kill_poss, As), @{fold_map 5} (lift_and_permute_bnf o qualify) 735 (if length bnfs = 1 then [0] else 1 upto length bnfs) 736 lift_ns after_lift_src after_lift_dest inners' accum') 737 end; 738 739fun default_comp_sort Ass = 740 Library.sort (Term_Ord.typ_ord o apply2 TFree) (fold (fold (insert (op =))) Ass []); 741 742fun raw_compose_bnf const_policy qualify flatten_tyargs outer inners oDs Dss tfreess accum = 743 let 744 val b = name_of_bnf outer; 745 746 val Ass = map (map Term.dest_TFree) tfreess; 747 val Ds = fold (fold Term.add_tfreesT) (oDs :: Dss) []; 748 749 val ((kill_poss, As), (inners', ((cache', unfold_set'), lthy'))) = 750 normalize_bnfs qualify Ass Ds flatten_tyargs inners accum; 751 752 val Ds = 753 oDs @ flat (@{map 3} (uncurry append oo curry swap oo map o nth) tfreess kill_poss Dss); 754 val As = map TFree As; 755 in 756 apfst (rpair (Ds, As)) 757 (apsnd (apfst (pair cache')) 758 (clean_compose_bnf const_policy (qualify 0) b outer inners' (unfold_set', lthy'))) 759 end; 760 761fun compose_bnf const_policy qualify flatten_tyargs outer inners oDs Dss tfreess 762 (accum as ((cache, _), _)) = 763 let val key = key_of_compose oDs Dss tfreess outer inners in 764 (case Typtab.lookup cache key of 765 SOME bnf_Ds_As => (bnf_Ds_As, accum) 766 | NONE => 767 cache_comp key 768 (raw_compose_bnf const_policy qualify flatten_tyargs outer inners oDs Dss tfreess accum)) 769 end; 770 771(* Hide the type of the bound (optimization) and unfold the definitions (nicer to the user) *) 772 773type absT_info = 774 {absT: typ, 775 repT: typ, 776 abs: term, 777 rep: term, 778 abs_inject: thm, 779 abs_inverse: thm, 780 type_definition: thm}; 781 782fun morph_absT_info phi 783 {absT, repT, abs, rep, abs_inject, abs_inverse, type_definition} = 784 {absT = Morphism.typ phi absT, 785 repT = Morphism.typ phi repT, 786 abs = Morphism.term phi abs, 787 rep = Morphism.term phi rep, 788 abs_inject = Morphism.thm phi abs_inject, 789 abs_inverse = Morphism.thm phi abs_inverse, 790 type_definition = Morphism.thm phi type_definition}; 791 792fun mk_absT thy repT absT repU = 793 let 794 val rho = Vartab.fold (cons o apsnd snd) (Sign.typ_match thy (repT, repU) Vartab.empty) []; 795 in Term.typ_subst_TVars rho absT end 796 handle Type.TYPE_MATCH => raise Term.TYPE ("mk_absT", [repT, absT, repU], []); 797 798fun mk_repT absT repT absU = 799 if absT = repT then absU 800 else 801 (case (absT, absU) of 802 (Type (C, Ts), Type (C', Us)) => 803 if C = C' then Term.typ_subst_atomic (Ts ~~ Us) repT 804 else raise Term.TYPE ("mk_repT", [absT, repT, absU], []) 805 | _ => raise Term.TYPE ("mk_repT", [absT, repT, absU], [])); 806 807fun mk_abs_or_rep _ absU (Const (\<^const_name>\<open>id_bnf\<close>, _)) = 808 Const (\<^const_name>\<open>id_bnf\<close>, absU --> absU) 809 | mk_abs_or_rep getT (Type (_, Us)) abs = 810 let val Ts = snd (dest_Type (getT (fastype_of abs))) 811 in Term.subst_atomic_types (Ts ~~ Us) abs end; 812 813val mk_abs = mk_abs_or_rep range_type; 814val mk_rep = mk_abs_or_rep domain_type; 815 816fun maybe_typedef force_out_of_line (b, As, mx) set opt_morphs tac lthy = 817 let 818 val threshold = Config.get lthy typedef_threshold; 819 val repT = HOLogic.dest_setT (fastype_of set); 820 val out_of_line = force_out_of_line orelse 821 (threshold >= 0 andalso Term.size_of_typ repT >= threshold); 822 in 823 if out_of_line then 824 typedef (b, As, mx) set opt_morphs tac lthy 825 |>> (fn (T_name, ({Rep_name, Abs_name, ...}, 826 {type_definition, Abs_inverse, Abs_inject, Abs_cases, ...}) : Typedef.info) => 827 (Type (T_name, map TFree As), 828 (Rep_name, Abs_name, type_definition, Abs_inverse, Abs_inject, Abs_cases))) 829 else 830 ((repT, 831 (\<^const_name>\<open>id_bnf\<close>, \<^const_name>\<open>id_bnf\<close>, 832 @{thm type_definition_id_bnf_UNIV}, 833 @{thm type_definition.Abs_inverse[OF type_definition_id_bnf_UNIV]}, 834 @{thm type_definition.Abs_inject[OF type_definition_id_bnf_UNIV]}, 835 @{thm type_definition.Abs_cases[OF type_definition_id_bnf_UNIV]})), lthy) 836 end; 837 838fun seal_bnf qualify (unfold_set : unfold_set) b force_out_of_line Ds all_Ds bnf lthy = 839 let 840 val live = live_of_bnf bnf; 841 val nwits = nwits_of_bnf bnf; 842 843 val ((As, As'), lthy1) = apfst (`(map TFree)) 844 (Variable.invent_types (replicate live \<^sort>\<open>type\<close>) (fold Variable.declare_typ all_Ds lthy)); 845 val (Bs, _) = apfst (map TFree) (Variable.invent_types (replicate live \<^sort>\<open>type\<close>) lthy1); 846 847 val ((((fs, fs'), (Rs, Rs')), (Ps, Ps')), _(*names_lthy*)) = lthy 848 |> mk_Frees' "f" (map2 (curry op -->) As Bs) 849 ||>> mk_Frees' "R" (map2 mk_pred2T As Bs) 850 ||>> mk_Frees' "P" (map mk_pred1T As); 851 852 val repTA = mk_T_of_bnf Ds As bnf; 853 val T_bind = qualify b; 854 val repTA_tfrees = Term.add_tfreesT repTA []; 855 val all_TA_params_in_order = fold_rev Term.add_tfreesT all_Ds As'; 856 val TA_params = 857 (if force_out_of_line then all_TA_params_in_order 858 else inter (op =) repTA_tfrees all_TA_params_in_order); 859 val ((TA, (Rep_name, Abs_name, type_definition, Abs_inverse, Abs_inject, _)), lthy) = 860 maybe_typedef force_out_of_line (T_bind, TA_params, NoSyn) (HOLogic.mk_UNIV repTA) NONE 861 (fn ctxt => EVERY' [rtac ctxt exI, rtac ctxt UNIV_I] 1) lthy; 862 863 val repTB = mk_T_of_bnf Ds Bs bnf; 864 val TB = Term.typ_subst_atomic (As ~~ Bs) TA; 865 val RepA = Const (Rep_name, TA --> repTA); 866 val RepB = Const (Rep_name, TB --> repTB); 867 val AbsA = Const (Abs_name, repTA --> TA); 868 val AbsB = Const (Abs_name, repTB --> TB); 869 val Abs_inject' = Abs_inject OF @{thms UNIV_I UNIV_I}; 870 val Abs_inverse' = Abs_inverse OF @{thms UNIV_I}; 871 872 val absT_info = {absT = TA, repT = repTA, abs = AbsA, rep = RepA, abs_inject = Abs_inject', 873 abs_inverse = Abs_inverse', type_definition = type_definition}; 874 875 val bnf_map = fold_rev Term.absfree fs' (HOLogic.mk_comp (HOLogic.mk_comp (AbsB, 876 Term.list_comb (mk_map_of_bnf Ds As Bs bnf, fs)), RepA)); 877 val bnf_sets = map ((fn t => HOLogic.mk_comp (t, RepA))) 878 (mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf); 879 val bnf_bd = mk_bd_of_bnf Ds As bnf; 880 val bnf_rel = fold_rev Term.absfree Rs' (mk_vimage2p RepA RepB $ 881 (Term.list_comb (mk_rel_of_bnf Ds As Bs bnf, Rs))); 882 val bnf_pred = fold_rev Term.absfree Ps' (HOLogic.mk_comp 883 (Term.list_comb (mk_pred_of_bnf Ds As bnf, Ps), RepA)); 884 885 (*bd may depend only on dead type variables*) 886 val bd_repT = fst (dest_relT (fastype_of bnf_bd)); 887 val bdT_bind = qualify (Binding.suffix_name ("_" ^ bdTN) b); 888 val params = Term.add_tfreesT bd_repT []; 889 val all_deads = map TFree (fold_rev Term.add_tfreesT all_Ds []); 890 891 val ((bdT, (_, Abs_bd_name, _, _, Abs_bdT_inject, Abs_bdT_cases)), lthy) = 892 maybe_typedef false (bdT_bind, params, NoSyn) (HOLogic.mk_UNIV bd_repT) NONE 893 (fn ctxt => EVERY' [rtac ctxt exI, rtac ctxt UNIV_I] 1) lthy; 894 895 val (bnf_bd', bd_ordIso, bd_card_order, bd_cinfinite) = 896 if bdT = bd_repT then (bnf_bd, bd_Card_order_of_bnf bnf RS @{thm ordIso_refl}, 897 bd_card_order_of_bnf bnf, bd_cinfinite_of_bnf bnf) 898 else 899 let 900 val bnf_bd' = mk_dir_image bnf_bd (Const (Abs_bd_name, bd_repT --> bdT)); 901 902 val Abs_bdT_inj = mk_Abs_inj_thm Abs_bdT_inject; 903 val Abs_bdT_bij = mk_Abs_bij_thm lthy Abs_bdT_inj Abs_bdT_cases; 904 905 val bd_ordIso = @{thm dir_image} OF [Abs_bdT_inj, bd_Card_order_of_bnf bnf]; 906 val bd_card_order = 907 @{thm card_order_dir_image} OF [Abs_bdT_bij, bd_card_order_of_bnf bnf]; 908 val bd_cinfinite = 909 (@{thm Cinfinite_cong} OF [bd_ordIso, bd_Cinfinite_of_bnf bnf]) RS conjunct1; 910 in 911 (bnf_bd', bd_ordIso, bd_card_order, bd_cinfinite) 912 end; 913 914 fun map_id0_tac ctxt = 915 rtac ctxt (@{thm type_copy_map_id0} OF [type_definition, map_id0_of_bnf bnf]) 1; 916 fun map_comp0_tac ctxt = 917 rtac ctxt (@{thm type_copy_map_comp0} OF [type_definition, map_comp0_of_bnf bnf]) 1; 918 fun map_cong0_tac ctxt = 919 EVERY' (rtac ctxt @{thm type_copy_map_cong0} :: rtac ctxt (map_cong0_of_bnf bnf) :: 920 map (fn i => EVERY' [select_prem_tac ctxt live (dtac ctxt meta_spec) i, etac ctxt meta_mp, 921 etac ctxt (o_apply RS equalityD2 RS set_mp)]) (1 upto live)) 1; 922 fun set_map0_tac thm ctxt = 923 rtac ctxt (@{thm type_copy_set_map0} OF [type_definition, thm]) 1; 924 val set_bd_tacs = map (fn thm => fn ctxt => rtac ctxt (@{thm ordLeq_ordIso_trans} OF 925 [thm, bd_ordIso] RS @{thm type_copy_set_bd}) 1) (set_bd_of_bnf bnf); 926 fun le_rel_OO_tac ctxt = 927 rtac ctxt (le_rel_OO_of_bnf bnf RS @{thm vimage2p_relcompp_mono}) 1; 928 fun rel_OO_Grp_tac ctxt = 929 (rtac ctxt (rel_OO_Grp_of_bnf bnf RS @{thm vimage2p_cong} RS trans) THEN' 930 (if force_out_of_line then subst_tac ctxt NONE else SELECT_GOAL o unfold_thms_tac ctxt) 931 [type_definition RS @{thm vimage2p_relcompp_converse}] THEN' 932 SELECT_GOAL (unfold_thms_tac ctxt [o_apply, 933 type_definition RS @{thm type_copy_vimage2p_Grp_Rep}, 934 type_definition RS @{thm vimage2p_relcompp_converse}]) THEN' 935 rtac ctxt refl) 1; 936 fun pred_set_tac ctxt = 937 HEADGOAL (EVERY' 938 [rtac ctxt (pred_set_of_bnf bnf RS @{thm arg_cong[of _ _ "\<lambda>f. f \<circ> _"]} RS trans), 939 SELECT_GOAL (unfold_thms_tac ctxt (@{thms Ball_comp_iff conj_comp_iff})), rtac ctxt refl]); 940 941 val tacs = zip_axioms map_id0_tac map_comp0_tac map_cong0_tac 942 (map set_map0_tac (set_map0_of_bnf bnf)) 943 (fn ctxt => rtac ctxt bd_card_order 1) (fn ctxt => rtac ctxt bd_cinfinite 1) 944 set_bd_tacs le_rel_OO_tac rel_OO_Grp_tac pred_set_tac; 945 946 val bnf_wits = map (fn (I, t) => 947 fold Term.absdummy (map (nth As) I) 948 (AbsA $ Term.list_comb (t, map Bound (0 upto length I - 1)))) 949 (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf); 950 951 fun wit_tac ctxt = 952 ALLGOALS (dtac ctxt (type_definition RS @{thm type_copy_wit})) THEN 953 mk_simple_wit_tac ctxt (wit_thms_of_bnf bnf); 954 955 val (bnf', lthy') = 956 bnf_def Hardly_Inline (user_policy Dont_Note) true qualify tacs wit_tac (SOME all_deads) 957 Binding.empty Binding.empty Binding.empty [] 958 (((((((b, TA), bnf_map), bnf_sets), bnf_bd'), bnf_wits), SOME bnf_rel), SOME bnf_pred) lthy; 959 960 val unfolds = @{thm id_bnf_apply} :: 961 (#map_unfolds unfold_set @ flat (#set_unfoldss unfold_set) @ 962 #rel_unfolds unfold_set @ #pred_unfolds unfold_set); 963 964 val bnf'' = bnf' |> morph_bnf_defs (Morphism.thm_morphism "BNF" (unfold_thms lthy' unfolds)); 965 966 val map_def = map_def_of_bnf bnf''; 967 val set_defs = set_defs_of_bnf bnf''; 968 val rel_def = rel_def_of_bnf bnf''; 969 970 val bnf_b = qualify b; 971 val def_qualify = 972 Thm.def_binding o Binding.concealed o Binding.qualify false (Binding.name_of bnf_b); 973 fun mk_prefix_binding pre = Binding.prefix_name (pre ^ "_") bnf_b; 974 val map_b = def_qualify (mk_prefix_binding mapN); 975 val rel_b = def_qualify (mk_prefix_binding relN); 976 val set_bs = if live = 1 then [def_qualify (mk_prefix_binding setN)] 977 else map (def_qualify o mk_prefix_binding o mk_setN) (1 upto live); 978 979 val notes = (map_b, map_def) :: (rel_b, rel_def) :: (set_bs ~~ set_defs) 980 |> map (fn (b, def) => ((b, []), [([def], [])])) 981 982 val (noted, lthy'') = lthy' 983 |> Local_Theory.notes notes 984 ||> (if repTA = TA then I else register_bnf_raw (fst (dest_Type TA)) bnf'') 985 in 986 ((morph_bnf (substitute_noted_thm noted) bnf'', (all_deads, absT_info)), lthy'') 987 end; 988 989exception BAD_DEAD of typ * typ; 990 991fun bnf_of_typ _ _ _ _ _ Ds0 (T as TFree T') accum = 992 (if member (op =) Ds0 T' then (DEADID_bnf, ([T], [])) else (ID_bnf, ([], [T])), accum) 993 | bnf_of_typ _ _ _ _ _ _ (TVar _) _ = error "Unexpected schematic variable" 994 | bnf_of_typ optim const_policy qualify' flatten_tyargs Xs Ds0 (T as Type (C, Ts)) 995 (accum as (_, lthy)) = 996 let 997 fun check_bad_dead ((_, (deads, _)), _) = 998 let val Ds = fold Term.add_tfreesT deads [] in 999 (case Library.inter (op =) Ds Xs of [] => () 1000 | X :: _ => raise BAD_DEAD (TFree X, T)) 1001 end; 1002 1003 val tfrees = subtract (op =) Ds0 (Term.add_tfreesT T []); 1004 val bnf_opt = if null tfrees then NONE else bnf_of lthy C; 1005 in 1006 (case bnf_opt of 1007 NONE => ((DEADID_bnf, ([T], [])), accum) 1008 | SOME bnf => 1009 if optim andalso forall (can Term.dest_TFree) Ts andalso length Ts = length tfrees then 1010 let 1011 val T' = T_of_bnf bnf; 1012 val deads = deads_of_bnf bnf; 1013 val lives = lives_of_bnf bnf; 1014 val tvars' = Term.add_tvarsT T' []; 1015 val Ds_As = 1016 apply2 (map (Term.typ_subst_TVars (map fst tvars' ~~ map TFree tfrees))) 1017 (deads, lives); 1018 in ((bnf, Ds_As), accum) end 1019 else 1020 let 1021 val name = Long_Name.base_name C; 1022 fun qualify i = 1023 let val namei = name ^ nonzero_string_of_int i; 1024 in qualify' o Binding.qualify true namei end; 1025 val odead = dead_of_bnf bnf; 1026 val olive = live_of_bnf bnf; 1027 val Ds = map (fn i => TFree (string_of_int i, [])) (1 upto odead); 1028 val Us = snd (Term.dest_Type (mk_T_of_bnf Ds (replicate olive dummyT) bnf)); 1029 val oDs_pos = map (fn x => find_index (fn y => x = y) Us) Ds 1030 |> filter (fn x => x >= 0); 1031 val oDs = map (nth Ts) oDs_pos; 1032 val Ts' = map (nth Ts) (subtract (op =) oDs_pos (0 upto length Ts - 1)); 1033 val ((inners, (Dss, Ass)), (accum', lthy')) = 1034 apfst (apsnd split_list o split_list) (@{fold_map 2} 1035 (fn i => bnf_of_typ optim Smart_Inline (qualify i) flatten_tyargs Xs Ds0) 1036 (if length Ts' = 1 then [0] else 1 upto length Ts') Ts' accum); 1037 in 1038 compose_bnf const_policy qualify flatten_tyargs bnf inners oDs Dss Ass (accum', lthy') 1039 end) 1040 |> tap check_bad_dead 1041 end; 1042 1043end; 1044