diff --git a/src/HOL/Tools/BNF/bnf_fp_util.ML b/src/HOL/Tools/BNF/bnf_fp_util.ML --- a/src/HOL/Tools/BNF/bnf_fp_util.ML +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML @@ -1,1008 +1,1021 @@ (* Title: HOL/Tools/BNF/bnf_fp_util.ML Author: Dmitriy Traytel, TU Muenchen Author: Jasmin Blanchette, TU Muenchen Author: Martin Desharnais, TU Muenchen Author: Stefan Berghofer, TU Muenchen Copyright 2012, 2013, 2014 Shared library for the datatype and codatatype constructions. *) signature BNF_FP_UTIL = sig exception EMPTY_DATATYPE of string type fp_result = {Ts: typ list, bnfs: BNF_Def.bnf list, pre_bnfs: BNF_Def.bnf list, absT_infos: BNF_Comp.absT_info list, ctors: term list, dtors: term list, xtor_un_folds: term list, xtor_co_recs: term list, xtor_co_induct: thm, dtor_ctors: thm list, ctor_dtors: thm list, ctor_injects: thm list, dtor_injects: thm list, xtor_maps: thm list, xtor_map_unique: thm, xtor_setss: thm list list, xtor_rels: thm list, xtor_un_fold_thms: thm list, xtor_co_rec_thms: thm list, xtor_un_fold_unique: thm, xtor_co_rec_unique: thm, xtor_un_fold_o_maps: thm list, xtor_co_rec_o_maps: thm list, xtor_un_fold_transfers: thm list, xtor_co_rec_transfers: thm list, xtor_rel_co_induct: thm, dtor_set_inducts: thm list} val morph_fp_result: morphism -> fp_result -> fp_result val time: Proof.context -> Timer.real_timer -> string -> Timer.real_timer val fixpoint: ('a * 'a -> bool) -> ('a list -> 'a list) -> 'a list -> 'a list val IITN: string val LevN: string val algN: string val behN: string val bisN: string val carTN: string val caseN: string val coN: string val coinductN: string val coinduct_strongN: string val corecN: string val corec_discN: string val corec_disc_iffN: string val ctorN: string val ctor_dtorN: string val ctor_exhaustN: string val ctor_induct2N: string val ctor_inductN: string val ctor_injectN: string val ctor_foldN: string val ctor_fold_o_mapN: string val ctor_fold_transferN: string val ctor_fold_uniqueN: string val ctor_mapN: string val ctor_map_uniqueN: string val ctor_recN: string val ctor_rec_o_mapN: string val ctor_rec_transferN: string val ctor_rec_uniqueN: string val ctor_relN: string val ctor_rel_inductN: string val ctor_set_inclN: string val ctor_set_set_inclN: string val dtorN: string val dtor_coinductN: string val dtor_corecN: string val dtor_corec_o_mapN: string val dtor_corec_transferN: string val dtor_corec_uniqueN: string val dtor_ctorN: string val dtor_exhaustN: string val dtor_injectN: string val dtor_mapN: string val dtor_map_coinductN: string val dtor_map_coinduct_strongN: string val dtor_map_uniqueN: string val dtor_relN: string val dtor_rel_coinductN: string val dtor_set_inclN: string val dtor_set_set_inclN: string val dtor_coinduct_strongN: string val dtor_unfoldN: string val dtor_unfold_o_mapN: string val dtor_unfold_transferN: string val dtor_unfold_uniqueN: string val exhaustN: string val colN: string val inductN: string val injectN: string val isNodeN: string val lsbisN: string val mapN: string val map_uniqueN: string val min_algN: string val morN: string val nchotomyN: string val recN: string val rel_casesN: string val rel_coinductN: string val rel_inductN: string val rel_injectN: string val rel_introsN: string val rel_distinctN: string val rel_selN: string val rvN: string val corec_selN: string val set_inclN: string val set_set_inclN: string val setN: string val simpsN: string val strTN: string val str_initN: string val sum_bdN: string val sum_bdTN: string val uniqueN: string (* TODO: Don't index set facts. Isabelle packages traditionally generate uniform names. *) val mk_ctor_setN: int -> string val mk_dtor_setN: int -> string val mk_dtor_set_inductN: int -> string val mk_set_inductN: int -> string val co_prefix: BNF_Util.fp_kind -> string val split_conj_thm: thm -> thm list val split_conj_prems: int -> thm -> thm val mk_sumTN: typ list -> typ val mk_sumTN_balanced: typ list -> typ val mk_tupleT_balanced: typ list -> typ val mk_sumprodT_balanced: typ list list -> typ val mk_proj: typ -> int -> int -> term val mk_convol: term * term -> term val mk_rel_prod: term -> term -> term val mk_rel_sum: term -> term -> term val Inl_const: typ -> typ -> term val Inr_const: typ -> typ -> term val mk_tuple_balanced: term list -> term val mk_tuple1_balanced: typ list -> term list -> term val abs_curried_balanced: typ list -> term -> term val mk_tupled_fun: term -> term -> term list -> term val mk_case_sum: term * term -> term val mk_case_sumN: term list -> term val mk_case_absumprod: typ -> term -> term list -> term list list -> term list list -> term val mk_Inl: typ -> term -> term val mk_Inr: typ -> term -> term val mk_sumprod_balanced: typ -> int -> int -> term list -> term val mk_absumprod: typ -> term -> int -> int -> term list -> term val dest_sumT: typ -> typ * typ val dest_sumTN_balanced: int -> typ -> typ list val dest_tupleT_balanced: int -> typ -> typ list val dest_absumprodT: typ -> typ -> int -> int list -> typ -> typ list list val If_const: typ -> term val mk_Field: term -> term val mk_If: term -> term -> term -> term val mk_absumprodE: thm -> int list -> thm val mk_sum_caseN: int -> int -> thm val mk_sum_caseN_balanced: int -> int -> thm val mk_sum_Cinfinite: thm list -> thm val mk_sum_card_order: thm list -> thm val force_typ: Proof.context -> typ -> term -> term val mk_xtor_rel_co_induct_thm: BNF_Util.fp_kind -> term list -> term list -> term list -> term list -> term list -> term list -> term list -> term list -> ({prems: thm list, context: Proof.context} -> tactic) -> Proof.context -> thm val mk_xtor_co_iter_transfer_thms: BNF_Util.fp_kind -> term list -> term list -> term list -> term list -> term list -> term list -> term list -> ({prems: thm list, context: Proof.context} -> tactic) -> Proof.context -> thm list val mk_xtor_co_iter_o_map_thms: BNF_Util.fp_kind -> bool -> int -> thm -> thm list -> thm list -> thm list -> thm list -> thm list val derive_xtor_co_recs: BNF_Util.fp_kind -> binding list -> (typ list -> typ list) -> (typ list list * typ list) -> BNF_Def.bnf list -> term list -> term list -> thm -> thm list -> thm list -> thm list -> thm list -> (BNF_Comp.absT_info * BNF_Comp.absT_info) option list -> local_theory -> (term list * (thm list * thm * thm list * thm list)) * local_theory val raw_qualify: (binding -> binding) -> binding -> binding -> binding val fixpoint_bnf: bool -> (binding -> binding) -> (binding list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list -> BNF_Comp.absT_info list -> local_theory -> 'a) -> binding list -> (string * sort) list -> (string * sort) list -> (string * sort) list -> typ list -> BNF_Comp.comp_cache -> local_theory -> ((BNF_Def.bnf list * BNF_Comp.absT_info list) * BNF_Comp.comp_cache) * 'a - val fp_antiquote_setup: binding -> theory -> theory end; structure BNF_FP_Util : BNF_FP_UTIL = struct open Ctr_Sugar open BNF_Comp open BNF_Def open BNF_Util open BNF_FP_Util_Tactics exception EMPTY_DATATYPE of string; type fp_result = {Ts: typ list, bnfs: bnf list, pre_bnfs: BNF_Def.bnf list, absT_infos: BNF_Comp.absT_info list, ctors: term list, dtors: term list, xtor_un_folds: term list, xtor_co_recs: term list, xtor_co_induct: thm, dtor_ctors: thm list, ctor_dtors: thm list, ctor_injects: thm list, dtor_injects: thm list, xtor_maps: thm list, xtor_map_unique: thm, xtor_setss: thm list list, xtor_rels: thm list, xtor_un_fold_thms: thm list, xtor_co_rec_thms: thm list, xtor_un_fold_unique: thm, xtor_co_rec_unique: thm, xtor_un_fold_o_maps: thm list, xtor_co_rec_o_maps: thm list, xtor_un_fold_transfers: thm list, xtor_co_rec_transfers: thm list, xtor_rel_co_induct: thm, dtor_set_inducts: thm list}; fun morph_fp_result phi {Ts, bnfs, pre_bnfs, absT_infos, ctors, dtors, xtor_un_folds, xtor_co_recs, xtor_co_induct, dtor_ctors, ctor_dtors, ctor_injects, dtor_injects, xtor_maps, xtor_map_unique, xtor_setss, xtor_rels, xtor_un_fold_thms, xtor_co_rec_thms, xtor_un_fold_unique, xtor_co_rec_unique, xtor_un_fold_o_maps, xtor_co_rec_o_maps, xtor_un_fold_transfers, xtor_co_rec_transfers, xtor_rel_co_induct, dtor_set_inducts} = {Ts = map (Morphism.typ phi) Ts, bnfs = map (morph_bnf phi) bnfs, pre_bnfs = map (morph_bnf phi) pre_bnfs, absT_infos = map (morph_absT_info phi) absT_infos, ctors = map (Morphism.term phi) ctors, dtors = map (Morphism.term phi) dtors, xtor_un_folds = map (Morphism.term phi) xtor_un_folds, xtor_co_recs = map (Morphism.term phi) xtor_co_recs, xtor_co_induct = Morphism.thm phi xtor_co_induct, dtor_ctors = map (Morphism.thm phi) dtor_ctors, ctor_dtors = map (Morphism.thm phi) ctor_dtors, ctor_injects = map (Morphism.thm phi) ctor_injects, dtor_injects = map (Morphism.thm phi) dtor_injects, xtor_maps = map (Morphism.thm phi) xtor_maps, xtor_map_unique = Morphism.thm phi xtor_map_unique, xtor_setss = map (map (Morphism.thm phi)) xtor_setss, xtor_rels = map (Morphism.thm phi) xtor_rels, xtor_un_fold_thms = map (Morphism.thm phi) xtor_un_fold_thms, xtor_co_rec_thms = map (Morphism.thm phi) xtor_co_rec_thms, xtor_un_fold_unique = Morphism.thm phi xtor_un_fold_unique, xtor_co_rec_unique = Morphism.thm phi xtor_co_rec_unique, xtor_un_fold_o_maps = map (Morphism.thm phi) xtor_un_fold_o_maps, xtor_co_rec_o_maps = map (Morphism.thm phi) xtor_co_rec_o_maps, xtor_un_fold_transfers = map (Morphism.thm phi) xtor_un_fold_transfers, xtor_co_rec_transfers = map (Morphism.thm phi) xtor_co_rec_transfers, xtor_rel_co_induct = Morphism.thm phi xtor_rel_co_induct, dtor_set_inducts = map (Morphism.thm phi) dtor_set_inducts}; fun time ctxt timer msg = (if Config.get ctxt bnf_timing then warning (msg ^ ": " ^ string_of_int (Time.toMilliseconds (Timer.checkRealTimer timer)) ^ " ms") else (); Timer.startRealTimer ()); val preN = "pre_" val rawN = "raw_" val coN = "co" val unN = "un" val algN = "alg" val IITN = "IITN" val foldN = "fold" val unfoldN = unN ^ foldN val uniqueN = "unique" val transferN = "transfer" val simpsN = "simps" val ctorN = "ctor" val dtorN = "dtor" val ctor_foldN = ctorN ^ "_" ^ foldN val dtor_unfoldN = dtorN ^ "_" ^ unfoldN val ctor_fold_uniqueN = ctor_foldN ^ "_" ^ uniqueN val ctor_fold_o_mapN = ctor_foldN ^ "_o_" ^ mapN val dtor_unfold_uniqueN = dtor_unfoldN ^ "_" ^ uniqueN val dtor_unfold_o_mapN = dtor_unfoldN ^ "_o_" ^ mapN val ctor_fold_transferN = ctor_foldN ^ "_" ^ transferN val dtor_unfold_transferN = dtor_unfoldN ^ "_" ^ transferN val ctor_mapN = ctorN ^ "_" ^ mapN val dtor_mapN = dtorN ^ "_" ^ mapN val map_uniqueN = mapN ^ "_" ^ uniqueN val ctor_map_uniqueN = ctorN ^ "_" ^ map_uniqueN val dtor_map_uniqueN = dtorN ^ "_" ^ map_uniqueN val min_algN = "min_alg" val morN = "mor" val bisN = "bis" val lsbisN = "lsbis" val sum_bdTN = "sbdT" val sum_bdN = "sbd" val carTN = "carT" val strTN = "strT" val isNodeN = "isNode" val LevN = "Lev" val rvN = "recover" val behN = "beh" val setN = "set" val mk_ctor_setN = prefix (ctorN ^ "_") o mk_setN val mk_dtor_setN = prefix (dtorN ^ "_") o mk_setN fun mk_set_inductN i = mk_setN i ^ "_induct" val mk_dtor_set_inductN = prefix (dtorN ^ "_") o mk_set_inductN val str_initN = "str_init" val recN = "rec" val corecN = coN ^ recN val ctor_recN = ctorN ^ "_" ^ recN val ctor_rec_o_mapN = ctor_recN ^ "_o_" ^ mapN val ctor_rec_transferN = ctor_recN ^ "_" ^ transferN val ctor_rec_uniqueN = ctor_recN ^ "_" ^ uniqueN val dtor_corecN = dtorN ^ "_" ^ corecN val dtor_corec_o_mapN = dtor_corecN ^ "_o_" ^ mapN val dtor_corec_transferN = dtor_corecN ^ "_" ^ transferN val dtor_corec_uniqueN = dtor_corecN ^ "_" ^ uniqueN val ctor_dtorN = ctorN ^ "_" ^ dtorN val dtor_ctorN = dtorN ^ "_" ^ ctorN val nchotomyN = "nchotomy" val injectN = "inject" val exhaustN = "exhaust" val ctor_injectN = ctorN ^ "_" ^ injectN val ctor_exhaustN = ctorN ^ "_" ^ exhaustN val dtor_injectN = dtorN ^ "_" ^ injectN val dtor_exhaustN = dtorN ^ "_" ^ exhaustN val ctor_relN = ctorN ^ "_" ^ relN val dtor_relN = dtorN ^ "_" ^ relN val inductN = "induct" val coinductN = coN ^ inductN val ctor_inductN = ctorN ^ "_" ^ inductN val ctor_induct2N = ctor_inductN ^ "2" val dtor_map_coinductN = dtor_mapN ^ "_" ^ coinductN val dtor_coinductN = dtorN ^ "_" ^ coinductN val coinduct_strongN = coinductN ^ "_strong" val dtor_map_coinduct_strongN = dtor_mapN ^ "_" ^ coinduct_strongN val dtor_coinduct_strongN = dtorN ^ "_" ^ coinduct_strongN val colN = "col" val set_inclN = "set_incl" val ctor_set_inclN = ctorN ^ "_" ^ set_inclN val dtor_set_inclN = dtorN ^ "_" ^ set_inclN val set_set_inclN = "set_set_incl" val ctor_set_set_inclN = ctorN ^ "_" ^ set_set_inclN val dtor_set_set_inclN = dtorN ^ "_" ^ set_set_inclN val caseN = "case" val discN = "disc" val corec_discN = corecN ^ "_" ^ discN val iffN = "_iff" val corec_disc_iffN = corec_discN ^ iffN val distinctN = "distinct" val rel_distinctN = relN ^ "_" ^ distinctN val injectN = "inject" val rel_casesN = relN ^ "_cases" val rel_injectN = relN ^ "_" ^ injectN val rel_introsN = relN ^ "_intros" val rel_coinductN = relN ^ "_" ^ coinductN val rel_selN = relN ^ "_sel" val dtor_rel_coinductN = dtorN ^ "_" ^ rel_coinductN val rel_inductN = relN ^ "_" ^ inductN val ctor_rel_inductN = ctorN ^ "_" ^ rel_inductN val selN = "sel" val corec_selN = corecN ^ "_" ^ selN fun co_prefix fp = case_fp fp "" "co"; fun dest_sumT (Type (\<^type_name>\sum\, [T, T'])) = (T, T'); val dest_sumTN_balanced = Balanced_Tree.dest dest_sumT; fun dest_tupleT_balanced 0 \<^typ>\unit\ = [] | dest_tupleT_balanced n T = Balanced_Tree.dest HOLogic.dest_prodT n T; fun dest_absumprodT absT repT n ms = map2 dest_tupleT_balanced ms o dest_sumTN_balanced n o mk_repT absT repT; val mk_sumTN = Library.foldr1 mk_sumT; val mk_sumTN_balanced = Balanced_Tree.make mk_sumT; fun mk_tupleT_balanced [] = HOLogic.unitT | mk_tupleT_balanced Ts = Balanced_Tree.make HOLogic.mk_prodT Ts; val mk_sumprodT_balanced = mk_sumTN_balanced o map mk_tupleT_balanced; fun mk_proj T n k = let val (binders, _) = strip_typeN n T in fold_rev (fn T => fn t => Abs (Name.uu, T, t)) binders (Bound (n - k - 1)) end; fun mk_convol (f, g) = let val (fU, fTU) = `range_type (fastype_of f); val ((gT, gU), gTU) = `dest_funT (fastype_of g); val convolT = fTU --> gTU --> gT --> HOLogic.mk_prodT (fU, gU); in Const (\<^const_name>\convol\, convolT) $ f $ g end; fun mk_rel_prod R S = let val ((A1, A2), RT) = `dest_pred2T (fastype_of R); val ((B1, B2), ST) = `dest_pred2T (fastype_of S); val rel_prodT = RT --> ST --> mk_pred2T (HOLogic.mk_prodT (A1, B1)) (HOLogic.mk_prodT (A2, B2)); in Const (\<^const_name>\rel_prod\, rel_prodT) $ R $ S end; fun mk_rel_sum R S = let val ((A1, A2), RT) = `dest_pred2T (fastype_of R); val ((B1, B2), ST) = `dest_pred2T (fastype_of S); val rel_sumT = RT --> ST --> mk_pred2T (mk_sumT (A1, B1)) (mk_sumT (A2, B2)); in Const (\<^const_name>\rel_sum\, rel_sumT) $ R $ S end; fun Inl_const LT RT = Const (\<^const_name>\Inl\, LT --> mk_sumT (LT, RT)); fun mk_Inl RT t = Inl_const (fastype_of t) RT $ t; fun Inr_const LT RT = Const (\<^const_name>\Inr\, RT --> mk_sumT (LT, RT)); fun mk_Inr LT t = Inr_const LT (fastype_of t) $ t; fun mk_prod1 bound_Ts (t, u) = HOLogic.pair_const (fastype_of1 (bound_Ts, t)) (fastype_of1 (bound_Ts, u)) $ t $ u; fun mk_tuple1_balanced _ [] = HOLogic.unit | mk_tuple1_balanced bound_Ts ts = Balanced_Tree.make (mk_prod1 bound_Ts) ts; val mk_tuple_balanced = mk_tuple1_balanced []; fun abs_curried_balanced Ts t = t $ mk_tuple1_balanced (List.rev Ts) (map Bound (length Ts - 1 downto 0)) |> fold_rev (Term.abs o pair Name.uu) Ts; fun mk_sumprod_balanced T n k ts = Sum_Tree.mk_inj T n k (mk_tuple_balanced ts); fun mk_absumprod absT abs0 n k ts = let val abs = mk_abs absT abs0; in abs $ mk_sumprod_balanced (domain_type (fastype_of abs)) n k ts end; fun mk_case_sum (f, g) = let val (fT, T') = dest_funT (fastype_of f); val (gT, _) = dest_funT (fastype_of g); in Sum_Tree.mk_sumcase fT gT T' f g end; val mk_case_sumN = Library.foldr1 mk_case_sum; val mk_case_sumN_balanced = Balanced_Tree.make mk_case_sum; fun mk_tupled_fun f x xs = if xs = [x] then f else HOLogic.tupled_lambda x (Term.list_comb (f, xs)); fun mk_case_absumprod absT rep fs xss xss' = HOLogic.mk_comp (mk_case_sumN_balanced (@{map 3} mk_tupled_fun fs (map mk_tuple_balanced xss) xss'), mk_rep absT rep); fun If_const T = Const (\<^const_name>\If\, HOLogic.boolT --> T --> T --> T); fun mk_If p t f = let val T = fastype_of t in If_const T $ p $ t $ f end; fun mk_Field r = let val T = fst (dest_relT (fastype_of r)); in Const (\<^const_name>\Field\, mk_relT (T, T) --> HOLogic.mk_setT T) $ r end; (*dangerous; use with monotonic, converging functions only!*) fun fixpoint eq f X = if subset eq (f X, X) then X else fixpoint eq f (f X); (* stolen from "~~/src/HOL/Tools/Datatype/datatype_aux.ML" *) fun split_conj_thm th = ((th RS conjunct1) :: split_conj_thm (th RS conjunct2)) handle THM _ => [th]; fun split_conj_prems limit th = let fun split n i th = if i = n then th else split n (i + 1) (conjI RSN (i, th)) handle THM _ => th; in split limit 1 th end; fun mk_obj_sumEN_balanced n = Balanced_Tree.make (fn (thm1, thm2) => thm1 RSN (1, thm2 RSN (2, @{thm obj_sumE_f}))) (replicate n asm_rl); fun mk_tupled_allIN_balanced 0 = @{thm unit_all_impI} | mk_tupled_allIN_balanced n = let val (tfrees, _) = BNF_Util.mk_TFrees n \<^context>; val T = mk_tupleT_balanced tfrees; in @{thm asm_rl[of "\x. P x \ Q x" for P Q]} |> Thm.instantiate' [SOME (Thm.ctyp_of \<^context> T)] [] |> Raw_Simplifier.rewrite_goals_rule \<^context> @{thms split_paired_All[THEN eq_reflection]} |> (fn thm => impI RS funpow n (fn th => allI RS th) thm) |> Thm.varifyT_global end; fun mk_absumprodE type_definition ms = let val n = length ms in mk_obj_sumEN_balanced n OF map mk_tupled_allIN_balanced ms RS (type_definition RS @{thm type_copy_obj_one_point_absE}) end; fun mk_sum_caseN 1 1 = refl | mk_sum_caseN _ 1 = @{thm sum.case(1)} | mk_sum_caseN 2 2 = @{thm sum.case(2)} | mk_sum_caseN n k = trans OF [@{thm case_sum_step(2)}, mk_sum_caseN (n - 1) (k - 1)]; fun mk_sum_step base step thm = if Thm.eq_thm_prop (thm, refl) then base else trans OF [step, thm]; fun mk_sum_caseN_balanced 1 1 = refl | mk_sum_caseN_balanced n k = Balanced_Tree.access {left = mk_sum_step @{thm sum.case(1)} @{thm case_sum_step(1)}, right = mk_sum_step @{thm sum.case(2)} @{thm case_sum_step(2)}, init = refl} n k; fun mk_sum_Cinfinite [thm] = thm | mk_sum_Cinfinite (thm :: thms) = @{thm Cinfinite_csum_weak} OF [thm, mk_sum_Cinfinite thms]; fun mk_sum_card_order [thm] = thm | mk_sum_card_order (thm :: thms) = @{thm card_order_csum} OF [thm, mk_sum_card_order thms]; fun mk_xtor_rel_co_induct_thm fp pre_rels pre_phis rels phis xs ys xtors xtor's tac lthy = let val pre_relphis = map (fn rel => Term.list_comb (rel, phis @ pre_phis)) pre_rels; val relphis = map (fn rel => Term.list_comb (rel, phis)) rels; fun mk_xtor fp' xtor x = if fp = fp' then xtor $ x else x; val dtor = mk_xtor Greatest_FP; val ctor = mk_xtor Least_FP; fun flip f x y = if fp = Greatest_FP then f y x else f x y; fun mk_prem pre_relphi phi x y xtor xtor' = HOLogic.mk_Trueprop (list_all_free [x, y] (flip (curry HOLogic.mk_imp) (pre_relphi $ (dtor xtor x) $ (dtor xtor' y)) (phi $ (ctor xtor x) $ (ctor xtor' y)))); val prems = @{map 6} mk_prem pre_relphis pre_phis xs ys xtors xtor's; val concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 (flip mk_leq) relphis pre_phis)); in Goal.prove_sorry lthy (map (fst o dest_Free) (phis @ pre_phis)) prems concl tac |> Thm.close_derivation \<^here> |> (fn thm => thm OF (replicate (length pre_rels) @{thm allI[OF allI[OF impI]]})) end; fun mk_xtor_co_iter_transfer_thms fp pre_rels pre_iphis pre_ophis rels phis un_folds un_folds' tac lthy = let val pre_relphis = map (fn rel => Term.list_comb (rel, phis @ pre_iphis)) pre_rels; val relphis = map (fn rel => Term.list_comb (rel, phis)) rels; fun flip f x y = if fp = Greatest_FP then f y x else f x y; val arg_rels = map2 (flip mk_rel_fun) pre_relphis pre_ophis; fun mk_transfer relphi pre_phi un_fold un_fold' = fold_rev mk_rel_fun arg_rels (flip mk_rel_fun relphi pre_phi) $ un_fold $ un_fold'; val transfers = @{map 4} mk_transfer relphis pre_ophis un_folds un_folds'; val goal = fold_rev Logic.all (phis @ pre_ophis) (HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj transfers)); in Goal.prove_sorry lthy [] [] goal tac |> Thm.close_derivation \<^here> |> split_conj_thm end; fun mk_xtor_co_iter_o_map_thms fp is_rec m un_fold_unique xtor_maps xtor_un_folds sym_map_comps map_cong0s = let val n = length sym_map_comps; val rewrite_comp_comp2 = case_fp fp @{thm rewriteR_comp_comp2} @{thm rewriteL_comp_comp2}; val rewrite_comp_comp = case_fp fp @{thm rewriteR_comp_comp} @{thm rewriteL_comp_comp}; val map_cong_passive_args1 = replicate m (case_fp fp @{thm id_comp} @{thm comp_id} RS fun_cong); val map_cong_active_args1 = replicate n (if is_rec then case_fp fp @{thm convol_o} @{thm o_case_sum} RS fun_cong else refl); val map_cong_passive_args2 = replicate m (case_fp fp @{thm comp_id} @{thm id_comp} RS fun_cong); val map_cong_active_args2 = replicate n (if is_rec then case_fp fp @{thm map_prod_o_convol_id} @{thm case_sum_o_map_sum_id} else case_fp fp @{thm id_comp} @{thm comp_id} RS fun_cong); fun mk_map_congs passive active = map (fn thm => thm OF (passive @ active) RS @{thm ext}) map_cong0s; val map_cong1s = mk_map_congs map_cong_passive_args1 map_cong_active_args1; val map_cong2s = mk_map_congs map_cong_passive_args2 map_cong_active_args2; fun mk_rewrites map_congs = map2 (fn sym_map_comp => fn map_cong => mk_trans sym_map_comp map_cong RS rewrite_comp_comp) sym_map_comps map_congs; val rewrite1s = mk_rewrites map_cong1s; val rewrite2s = mk_rewrites map_cong2s; val unique_prems = @{map 4} (fn xtor_map => fn un_fold => fn rewrite1 => fn rewrite2 => mk_trans (rewrite_comp_comp2 OF [xtor_map, un_fold]) (mk_trans rewrite1 (mk_sym rewrite2))) xtor_maps xtor_un_folds rewrite1s rewrite2s; in split_conj_thm (un_fold_unique OF map (case_fp fp I mk_sym) unique_prems) end; fun force_typ ctxt T = Term.map_types Type_Infer.paramify_vars #> Type.constraint T #> Syntax.check_term ctxt #> singleton (Variable.polymorphic ctxt); fun absT_info_encodeT thy (SOME (src : absT_info, dst : absT_info)) src_absT = let val src_repT = mk_repT (#absT src) (#repT src) src_absT; val dst_absT = mk_absT thy (#repT dst) (#absT dst) src_repT; in dst_absT end | absT_info_encodeT _ NONE T = T; fun absT_info_decodeT thy = absT_info_encodeT thy o Option.map swap; fun absT_info_encode thy fp (opt as SOME (src : absT_info, dst : absT_info)) t = let val co_alg_funT = case_fp fp domain_type range_type; fun co_swap pair = case_fp fp I swap pair; val mk_co_comp = curry (HOLogic.mk_comp o co_swap); val mk_co_abs = case_fp fp mk_abs mk_rep; val mk_co_rep = case_fp fp mk_rep mk_abs; val co_abs = case_fp fp #abs #rep; val co_rep = case_fp fp #rep #abs; val src_absT = co_alg_funT (fastype_of t); val dst_absT = absT_info_encodeT thy opt src_absT; val co_src_abs = mk_co_abs src_absT (co_abs src); val co_dst_rep = mk_co_rep dst_absT (co_rep dst); in mk_co_comp (mk_co_comp t co_src_abs) co_dst_rep end | absT_info_encode _ _ NONE t = t; fun absT_info_decode thy fp = absT_info_encode thy fp o Option.map swap; fun mk_xtor_un_fold_xtor_thms ctxt fp un_folds xtors xtor_un_fold_unique map_id0s absT_info_opts = let val thy = Proof_Context.theory_of ctxt; fun mk_goal un_fold = let val rhs = list_comb (un_fold, @{map 2} (absT_info_encode thy fp) absT_info_opts xtors); val T = range_type (fastype_of rhs); in HOLogic.mk_eq (HOLogic.id_const T, rhs) end; val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map mk_goal un_folds)); fun mk_inverses NONE = [] | mk_inverses (SOME (src, dst)) = [#type_definition dst RS @{thm type_definition.Abs_inverse[OF _ UNIV_I]}, #type_definition src RS @{thm type_definition.Rep_inverse}]; val inverses = maps mk_inverses absT_info_opts; in Goal.prove_sorry ctxt [] [] goal (fn {context = ctxt, prems = _} => mk_xtor_un_fold_xtor_tac ctxt xtor_un_fold_unique map_id0s inverses) |> split_conj_thm |> map mk_sym end; fun derive_xtor_co_recs fp bs mk_Ts (Dss, resDs) pre_bnfs xtors0 un_folds0 xtor_un_fold_unique xtor_un_folds xtor_un_fold_transfers xtor_maps xtor_rels absT_info_opts lthy = let val thy = Proof_Context.theory_of lthy; fun co_swap pair = case_fp fp I swap pair; val mk_co_comp = curry (HOLogic.mk_comp o co_swap); fun mk_co_algT T U = case_fp fp (T --> U) (U --> T); val co_alg_funT = case_fp fp domain_type range_type; val mk_co_product = curry (case_fp fp mk_convol mk_case_sum); val co_proj1_const = case_fp fp fst_const (uncurry Inl_const o dest_sumT) o co_alg_funT; val co_proj2_const = case_fp fp snd_const (uncurry Inr_const o dest_sumT) o co_alg_funT; val mk_co_productT = curry (case_fp fp HOLogic.mk_prodT mk_sumT); val rewrite_comp_comp = case_fp fp @{thm rewriteL_comp_comp} @{thm rewriteR_comp_comp}; val n = length pre_bnfs; val live = live_of_bnf (hd pre_bnfs); val m = live - n; val ks = 1 upto n; val map_id0s = map map_id0_of_bnf pre_bnfs; val map_comps = map map_comp_of_bnf pre_bnfs; val map_cong0s = map map_cong0_of_bnf pre_bnfs; val map_transfers = map map_transfer_of_bnf pre_bnfs; val sym_map_comp0s = map (mk_sym o map_comp0_of_bnf) pre_bnfs; val deads = fold (union (op =)) Dss resDs; val ((((As, Bs), Xs), Ys), names_lthy) = lthy |> fold Variable.declare_typ deads |> mk_TFrees m ||>> mk_TFrees m ||>> mk_TFrees n ||>> mk_TFrees n; val XFTs = @{map 2} (fn Ds => mk_T_of_bnf Ds (As @ Xs)) Dss pre_bnfs; val co_algXFTs = @{map 2} mk_co_algT XFTs Xs; val Ts = mk_Ts As; val un_foldTs = @{map 2} (fn T => fn X => co_algXFTs ---> mk_co_algT T X) Ts Xs; val un_folds = @{map 2} (force_typ names_lthy) un_foldTs un_folds0; val ABs = As ~~ Bs; val XYs = Xs ~~ Ys; val Us = map (typ_subst_atomic ABs) Ts; val TFTs = @{map 2} (fn Ds => mk_T_of_bnf Ds (As @ Ts)) Dss pre_bnfs; val TFTs' = @{map 2} (absT_info_decodeT thy) absT_info_opts TFTs; val xtors = @{map 3} (force_typ names_lthy oo mk_co_algT) TFTs' Ts xtors0; val ids = map HOLogic.id_const As; val co_rec_Xs = @{map 2} mk_co_productT Ts Xs; val co_rec_Ys = @{map 2} mk_co_productT Us Ys; val co_rec_algXs = @{map 2} mk_co_algT co_rec_Xs Xs; val co_proj1s = map co_proj1_const co_rec_algXs; val co_rec_maps = @{map 2} (fn Ds => mk_map_of_bnf Ds (As @ case_fp fp co_rec_Xs Ts) (As @ case_fp fp Ts co_rec_Xs)) Dss pre_bnfs; val co_rec_Ts = @{map 2} (fn Ds => mk_T_of_bnf Ds (As @ co_rec_Xs)) Dss pre_bnfs val co_rec_argTs = @{map 2} mk_co_algT co_rec_Ts Xs; val co_rec_resTs = @{map 2} mk_co_algT Ts Xs; val (((co_rec_ss, fs), xs), names_lthy) = names_lthy |> mk_Frees "s" co_rec_argTs ||>> mk_Frees "f" co_rec_resTs ||>> mk_Frees "x" (case_fp fp TFTs' Xs); val co_rec_strs = @{map 4} (fn xtor => fn s => fn mapx => fn absT_info_opt => mk_co_product (mk_co_comp (absT_info_encode thy fp absT_info_opt xtor) (list_comb (mapx, ids @ co_proj1s))) s) xtors co_rec_ss co_rec_maps absT_info_opts; val theta = Xs ~~ co_rec_Xs; val co_rec_un_folds = map (subst_atomic_types theta) un_folds; val co_rec_spec0s = map (fn un_fold => list_comb (un_fold, co_rec_strs)) co_rec_un_folds; val co_rec_ids = @{map 2} (mk_co_comp o co_proj1_const) co_rec_algXs co_rec_spec0s; val co_rec_specs = @{map 2} (mk_co_comp o co_proj2_const) co_rec_algXs co_rec_spec0s; val co_recN = case_fp fp ctor_recN dtor_corecN; fun co_rec_bind i = nth bs (i - 1) |> Binding.prefix_name (co_recN ^ "_"); val co_rec_def_bind = rpair [] o Binding.concealed o Thm.def_binding o co_rec_bind; fun co_rec_spec i = fold_rev (Term.absfree o Term.dest_Free) co_rec_ss (nth co_rec_specs (i - 1)); val ((co_rec_frees, (_, co_rec_def_frees)), (lthy, lthy_old)) = lthy |> Local_Theory.open_target |> snd |> fold_map (fn i => Local_Theory.define ((co_rec_bind i, NoSyn), (co_rec_def_bind i, co_rec_spec i))) ks |>> apsnd split_list o split_list ||> `Local_Theory.close_target; val phi = Proof_Context.export_morphism lthy_old lthy; val co_rec_names = map (fst o dest_Const o Morphism.term phi) co_rec_frees; val co_recs = @{map 2} (fn name => fn resT => Const (name, co_rec_argTs ---> resT)) co_rec_names co_rec_resTs; val co_rec_defs = map (fn def => mk_unabs_def n (HOLogic.mk_obj_eq (Morphism.thm phi def))) co_rec_def_frees; val xtor_un_fold_xtor_thms = mk_xtor_un_fold_xtor_thms lthy fp (map (Term.subst_atomic_types (Xs ~~ Ts)) un_folds) xtors xtor_un_fold_unique map_id0s absT_info_opts; val co_rec_id_thms = let val goal = @{map 2} (fn T => fn t => HOLogic.mk_eq (t, HOLogic.id_const T)) Ts co_rec_ids |> Library.foldr1 HOLogic.mk_conj |> HOLogic.mk_Trueprop; val vars = Variable.add_free_names lthy goal []; in Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => mk_xtor_co_rec_id_tac ctxt xtor_un_fold_xtor_thms xtor_un_fold_unique xtor_un_folds map_comps) |> Thm.close_derivation \<^here> |> split_conj_thm end; val co_rec_app_ss = map (fn co_rec => list_comb (co_rec, co_rec_ss)) co_recs; val co_products = @{map 2} (fn T => mk_co_product (HOLogic.id_const T)) Ts co_rec_app_ss; val co_rec_maps_rev = @{map 2} (fn Ds => mk_map_of_bnf Ds (As @ case_fp fp Ts co_rec_Xs) (As @ case_fp fp co_rec_Xs Ts)) Dss pre_bnfs; fun mk_co_app f g x = case_fp fp (f $ (g $ x)) (g $ (f $ x)); val co_rec_expand_thms = map (fn thm => thm RS case_fp fp @{thm convol_expand_snd} @{thm case_sum_expand_Inr_pointfree}) co_rec_id_thms; val xtor_co_rec_thms = let fun mk_goal co_rec s mapx xtor x absT_info_opt = let val lhs = mk_co_app co_rec xtor x; val rhs = mk_co_app s (list_comb (mapx, ids @ co_products) |> absT_info_decode thy fp absT_info_opt) x; in mk_Trueprop_eq (lhs, rhs) end; val goals = @{map 6} mk_goal co_rec_app_ss co_rec_ss co_rec_maps_rev xtors xs absT_info_opts; in map2 (fn goal => fn un_fold => Variable.add_free_names lthy goal [] |> (fn vars => Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => mk_xtor_co_rec_tac ctxt un_fold co_rec_defs co_rec_expand_thms)) |> Thm.close_derivation \<^here>) goals xtor_un_folds end; val co_product_fs = @{map 2} (fn T => mk_co_product (HOLogic.id_const T)) Ts fs; val co_rec_expand'_thms = map (fn thm => thm RS case_fp fp @{thm convol_expand_snd'} @{thm case_sum_expand_Inr'}) co_rec_id_thms; val xtor_co_rec_unique_thm = let fun mk_prem f s mapx xtor absT_info_opt = let val lhs = mk_co_comp f xtor; val rhs = mk_co_comp s (list_comb (mapx, ids @ co_product_fs)) |> absT_info_decode thy fp absT_info_opt; in mk_Trueprop_eq (co_swap (lhs, rhs)) end; val prems = @{map 5} mk_prem fs co_rec_ss co_rec_maps_rev xtors absT_info_opts; val concl = @{map 2} (curry HOLogic.mk_eq) fs co_rec_app_ss |> Library.foldr1 HOLogic.mk_conj |> HOLogic.mk_Trueprop; val goal = Logic.list_implies (prems, concl); val vars = Variable.add_free_names lthy goal []; fun mk_inverses NONE = [] | mk_inverses (SOME (src, dst)) = [#type_definition dst RS @{thm type_copy_Rep_o_Abs} RS rewrite_comp_comp, #type_definition src RS @{thm type_copy_Abs_o_Rep}]; val inverses = maps mk_inverses absT_info_opts; in Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => mk_xtor_co_rec_unique_tac ctxt fp co_rec_defs co_rec_expand'_thms xtor_un_fold_unique map_id0s sym_map_comp0s inverses) |> Thm.close_derivation \<^here> end; val xtor_co_rec_o_map_thms = if forall is_none absT_info_opts then mk_xtor_co_iter_o_map_thms fp true m xtor_co_rec_unique_thm (map (mk_pointfree2 lthy) xtor_maps) (map (mk_pointfree2 lthy) xtor_co_rec_thms) sym_map_comp0s map_cong0s else replicate n refl (* FIXME *); val ABphiTs = @{map 2} mk_pred2T As Bs; val XYphiTs = @{map 2} mk_pred2T Xs Ys; val ((ABphis, XYphis), names_lthy) = names_lthy |> mk_Frees "R" ABphiTs ||>> mk_Frees "S" XYphiTs; val xtor_co_rec_transfer_thms = if forall is_none absT_info_opts then let val pre_rels = @{map 2} (fn Ds => mk_rel_of_bnf Ds (As @ co_rec_Xs) (Bs @ co_rec_Ys)) Dss pre_bnfs; val rels = @{map 3} (fn T => fn T' => Thm.prop_of #> HOLogic.dest_Trueprop #> fst o dest_comb #> fst o dest_comb #> funpow n (snd o dest_comb) #> case_fp fp (fst o dest_comb #> snd o dest_comb) (snd o dest_comb) #> head_of #> force_typ names_lthy (ABphiTs ---> mk_pred2T T T')) Ts Us xtor_un_fold_transfers; fun tac {context = ctxt, prems = _} = mk_xtor_co_rec_transfer_tac ctxt fp n m co_rec_defs xtor_un_fold_transfers map_transfers xtor_rels; val mk_rel_co_product = case_fp fp mk_rel_prod mk_rel_sum; val rec_phis = map2 (fn rel => mk_rel_co_product (Term.list_comb (rel, ABphis))) rels XYphis; in mk_xtor_co_iter_transfer_thms fp pre_rels rec_phis XYphis rels ABphis co_recs (map (subst_atomic_types (ABs @ XYs)) co_recs) tac lthy end else replicate n TrueI (* FIXME *); val notes = [(case_fp fp ctor_recN dtor_corecN, xtor_co_rec_thms), (case_fp fp ctor_rec_uniqueN dtor_corec_uniqueN, split_conj_thm xtor_co_rec_unique_thm), (case_fp fp ctor_rec_o_mapN dtor_corec_o_mapN, xtor_co_rec_o_map_thms), (case_fp fp ctor_rec_transferN dtor_corec_transferN, xtor_co_rec_transfer_thms)] |> map (apsnd (map single)) |> maps (fn (thmN, thmss) => map2 (fn b => fn thms => ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])) bs thmss); val lthy = lthy |> Config.get lthy bnf_internals ? snd o Local_Theory.notes notes; in ((co_recs, (xtor_co_rec_thms, xtor_co_rec_unique_thm, xtor_co_rec_o_map_thms, xtor_co_rec_transfer_thms)), lthy) end; fun raw_qualify extra_qualify base_b = let val qs = Binding.path_of base_b; val n = Binding.name_of base_b; in Binding.prefix_name rawN #> fold_rev (fn (s, mand) => Binding.qualify mand s) (qs @ [(n, true)]) #> extra_qualify #> Binding.concealed end; fun fixpoint_bnf force_out_of_line extra_qualify construct_fp bs resBs Ds0 Xs rhsXs comp_cache0 lthy = let val time = time lthy; val timer = time (Timer.startRealTimer ()); fun flatten_tyargs Ass = subtract (op =) Xs (filter (fn T => exists (fn Ts => member (op =) Ts T) Ass) resBs) @ Xs; val ((bnfs, (deadss, livess)), (comp_cache_unfold_set, lthy')) = apfst (apsnd split_list o split_list) (@{fold_map 2} (fn b => bnf_of_typ true Smart_Inline (raw_qualify extra_qualify b) flatten_tyargs Xs Ds0) bs rhsXs ((comp_cache0, empty_unfolds), lthy)); fun norm_qualify i = Binding.qualify true (Binding.name_of (nth bs (Int.max (0, i - 1)))) #> extra_qualify #> Binding.concealed; val Ass = map (map dest_TFree) livess; val Ds' = fold (fold Term.add_tfreesT) deadss []; val Ds = union (op =) Ds' Ds0; val missing = resBs |> fold (subtract (op =)) (Ds' :: Ass); val (dead_phantoms, live_phantoms) = List.partition (member (op =) Ds0) missing; val resBs' = resBs |> fold (subtract (op =)) [dead_phantoms, Ds]; val timer = time (timer "Construction of BNFs"); val ((kill_posss, _), (bnfs', ((comp_cache', unfold_set'), lthy''))) = normalize_bnfs norm_qualify Ass Ds (K (resBs' @ Xs)) bnfs (comp_cache_unfold_set, lthy'); val Dss = @{map 3} (fn lives => fn kill_posss => fn deads => deads @ map (nth lives) kill_posss) livess kill_posss deadss; val all_Dss = Dss |> force_out_of_line ? map (fn Ds' => union (op =) Ds' (map TFree Ds0)); fun pre_qualify b = Binding.qualify false (Binding.name_of b) #> extra_qualify #> not (Config.get lthy'' bnf_internals) ? Binding.concealed; val ((pre_bnfs, (deadss, absT_infos)), lthy''') = lthy'' |> @{fold_map 5} (fn b => seal_bnf (pre_qualify b) unfold_set' (Binding.prefix_name preN b)) bs (replicate (length rhsXs) (force_out_of_line orelse not (null live_phantoms))) Dss all_Dss bnfs' |>> split_list |>> apsnd split_list; val timer = time (timer "Normalization & sealing of BNFs"); val res = construct_fp bs resBs (map TFree dead_phantoms, deadss) pre_bnfs absT_infos lthy'''; val timer = time (timer "FP construction in total"); in (((pre_bnfs, absT_infos), comp_cache'), res) end; -fun fp_antiquote_setup binding = + +(** document antiquotations **) + +local + +fun antiquote_setup binding = Thy_Output.antiquotation_pretty_source_embedded binding (Args.type_name {proper = true, strict = true}) (fn ctxt => fn fcT_name => (case Ctr_Sugar.ctr_sugar_of ctxt fcT_name of NONE => error ("Not a known freely generated type name: " ^ quote fcT_name) | SOME {T = T0, ctrs = ctrs0, ...} => let val freezeT = Term.map_atyps (fn TVar ((s, _), S) => TFree (s, S) | T => T); val T = freezeT T0; val ctrs = map (Term.map_types freezeT) ctrs0; val pretty_typ_bracket = Syntax.pretty_typ (Config.put pretty_priority 1001 ctxt); fun pretty_ctr ctr = Pretty.block (Pretty.breaks (Syntax.pretty_term ctxt ctr :: map pretty_typ_bracket (binder_types (fastype_of ctr)))); in Pretty.block (Pretty.keyword1 (Binding.name_of binding) :: Pretty.brk 1 :: Syntax.pretty_typ ctxt T :: Pretty.str " =" :: Pretty.brk 1 :: flat (separate [Pretty.brk 1, Pretty.str "| "] (map (single o pretty_ctr) ctrs))) end)); +in + +val _ = + Theory.setup + (antiquote_setup \<^binding>\datatype\ #> + antiquote_setup \<^binding>\codatatype\); + end; + +end; diff --git a/src/HOL/Tools/BNF/bnf_gfp.ML b/src/HOL/Tools/BNF/bnf_gfp.ML --- a/src/HOL/Tools/BNF/bnf_gfp.ML +++ b/src/HOL/Tools/BNF/bnf_gfp.ML @@ -1,2611 +1,2609 @@ (* Title: HOL/Tools/BNF/bnf_gfp.ML Author: Dmitriy Traytel, TU Muenchen Author: Andrei Popescu, TU Muenchen Author: Jasmin Blanchette, TU Muenchen Copyright 2012 Codatatype construction. *) signature BNF_GFP = sig val construct_gfp: mixfix list -> binding list -> binding list -> binding list -> binding list list -> binding list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list -> BNF_Comp.absT_info list -> local_theory -> BNF_FP_Util.fp_result * local_theory end; structure BNF_GFP : BNF_GFP = struct open BNF_Def open BNF_Util open BNF_Tactics open BNF_Comp open BNF_FP_Util open BNF_FP_Def_Sugar open BNF_GFP_Util open BNF_GFP_Tactics datatype wit_tree = Wit_Leaf of int | Wit_Node of (int * int * int list) * wit_tree list; fun mk_tree_args (I, T) (I', Ts) = (sort_distinct int_ord (I @ I'), T :: Ts); fun finish Iss m seen i (nwit, I) = let val treess = map (fn j => if j < m orelse member (op =) seen j then [([j], Wit_Leaf j)] else map_index (finish Iss m (insert (op =) j seen) j) (nth Iss (j - m)) |> flat |> minimize_wits) I; in map (fn (I, t) => (I, Wit_Node ((i - m, nwit, filter (fn i => i < m) I), t))) (fold_rev (map_product mk_tree_args) treess [([], [])]) |> minimize_wits end; fun tree_to_ctor_wit vars _ _ (Wit_Leaf j) = ([j], nth vars j) | tree_to_ctor_wit vars ctors witss (Wit_Node ((i, nwit, I), subtrees)) = (I, nth ctors i $ (Term.list_comb (snd (nth (nth witss i) nwit), map (snd o tree_to_ctor_wit vars ctors witss) subtrees))); fun tree_to_coind_wits _ (Wit_Leaf _) = [] | tree_to_coind_wits lwitss (Wit_Node ((i, nwit, I), subtrees)) = ((i, I), nth (nth lwitss i) nwit) :: maps (tree_to_coind_wits lwitss) subtrees; (*all BNFs have the same lives*) fun construct_gfp mixfixes map_bs rel_bs pred_bs set_bss0 bs resBs (resDs, Dss) bnfs absT_infos lthy = let val time = time lthy; val timer = time (Timer.startRealTimer ()); val live = live_of_bnf (hd bnfs); val n = length bnfs; (*active*) val ks = 1 upto n; val m = live - n; (*passive, if 0 don't generate a new BNF*) val ls = 1 upto m; val internals = Config.get lthy bnf_internals; val b_names = map Binding.name_of bs; val b_name = mk_common_name b_names; val b = Binding.name b_name; fun mk_internal_of_b name = Binding.prefix_name (name ^ "_") #> Binding.prefix true b_name #> Binding.concealed; fun mk_internal_b name = mk_internal_of_b name b; fun mk_internal_bs name = map (mk_internal_of_b name) bs; val external_bs = map2 (Binding.prefix false) b_names bs |> not internals ? map Binding.concealed; val deads = fold (union (op =)) Dss resDs; val names_lthy = fold Variable.declare_typ deads lthy; val passives = map fst (subtract (op = o apsnd TFree) deads resBs); (* tvars *) val ((((((passiveAs, activeAs), passiveBs), activeBs), passiveCs), activeCs), idxT) = names_lthy |> variant_tfrees passives ||>> mk_TFrees n ||>> variant_tfrees passives ||>> mk_TFrees n ||>> mk_TFrees m ||>> mk_TFrees n ||> fst o mk_TFrees 1 ||> the_single; val allAs = passiveAs @ activeAs; val allBs' = passiveBs @ activeBs; val Ass = replicate n allAs; val allBs = passiveAs @ activeBs; val Bss = replicate n allBs; val allCs = passiveAs @ activeCs; val allCs' = passiveBs @ activeCs; val Css' = replicate n allCs'; (* types *) val dead_poss = map (fn x => if member (op =) deads (TFree x) then SOME (TFree x) else NONE) resBs; fun mk_param NONE passive = (hd passive, tl passive) | mk_param (SOME a) passive = (a, passive); val mk_params = fold_map mk_param dead_poss #> fst; fun mk_FTs Ts = map2 (fn Ds => mk_T_of_bnf Ds Ts) Dss bnfs; val (params, params') = `(map Term.dest_TFree) (mk_params passiveAs); val FTsAs = mk_FTs allAs; val FTsBs = mk_FTs allBs; val FTsCs = mk_FTs allCs; val ATs = map HOLogic.mk_setT passiveAs; val BTs = map HOLogic.mk_setT activeAs; val B'Ts = map HOLogic.mk_setT activeBs; val B''Ts = map HOLogic.mk_setT activeCs; val sTs = map2 (fn T => fn U => T --> U) activeAs FTsAs; val s'Ts = map2 (fn T => fn U => T --> U) activeBs FTsBs; val s''Ts = map2 (fn T => fn U => T --> U) activeCs FTsCs; val fTs = map2 (fn T => fn U => T --> U) activeAs activeBs; val self_fTs = map (fn T => T --> T) activeAs; val gTs = map2 (fn T => fn U => T --> U) activeBs activeCs; val all_gTs = map2 (fn T => fn U => T --> U) allBs allCs'; val RTs = map2 (fn T => fn U => HOLogic.mk_prodT (T, U)) activeAs activeBs; val sRTs = map2 (fn T => fn U => HOLogic.mk_prodT (T, U)) activeAs activeAs; val R'Ts = map2 (fn T => fn U => HOLogic.mk_prodT (T, U)) activeBs activeCs; val setsRTs = map HOLogic.mk_setT sRTs; val setRTs = map HOLogic.mk_setT RTs; val all_sbisT = HOLogic.mk_tupleT setsRTs; val setR'Ts = map HOLogic.mk_setT R'Ts; val FRTs = mk_FTs (passiveAs @ RTs); (* terms *) val mapsAsAs = @{map 4} mk_map_of_bnf Dss Ass Ass bnfs; val mapsAsBs = @{map 4} mk_map_of_bnf Dss Ass Bss bnfs; val mapsBsCs' = @{map 4} mk_map_of_bnf Dss Bss Css' bnfs; val mapsAsCs' = @{map 4} mk_map_of_bnf Dss Ass Css' bnfs; val map_fsts = @{map 4} mk_map_of_bnf Dss (replicate n (passiveAs @ RTs)) Ass bnfs; val map_snds = @{map 4} mk_map_of_bnf Dss (replicate n (passiveAs @ RTs)) Bss bnfs; fun mk_setss Ts = @{map 3} mk_sets_of_bnf (map (replicate live) Dss) (map (replicate live) (replicate n Ts)) bnfs; val setssAs = mk_setss allAs; val setssAs' = transpose setssAs; val bis_setss = mk_setss (passiveAs @ RTs); val relsAsBs = @{map 4} mk_rel_of_bnf Dss Ass Bss bnfs; val bds = @{map 3} mk_bd_of_bnf Dss Ass bnfs; val sum_bd = Library.foldr1 (uncurry mk_csum) bds; val sum_bdT = fst (dest_relT (fastype_of sum_bd)); val (sum_bdT_params, sum_bdT_params') = `(map TFree) (Term.add_tfreesT sum_bdT []); val ((((((((((zs, zs'), Bs), ss), fs), self_fs), all_gs), xFs), yFs), yFs_copy), _) = lthy |> mk_Frees' "b" activeAs ||>> mk_Frees "B" BTs ||>> mk_Frees "s" sTs ||>> mk_Frees "f" fTs ||>> mk_Frees "f" self_fTs ||>> mk_Frees "g" all_gTs ||>> mk_Frees "x" FTsAs ||>> mk_Frees "y" FTsBs ||>> mk_Frees "y" FTsBs; val passive_UNIVs = map HOLogic.mk_UNIV passiveAs; val passive_eqs = map HOLogic.eq_const passiveAs; val active_UNIVs = map HOLogic.mk_UNIV activeAs; val passive_ids = map HOLogic.id_const passiveAs; val active_ids = map HOLogic.id_const activeAs; val fsts = map fst_const RTs; val snds = map snd_const RTs; (* thms *) val bd_card_orders = map bd_card_order_of_bnf bnfs; val bd_card_order = hd bd_card_orders val bd_Card_orders = map bd_Card_order_of_bnf bnfs; val bd_Card_order = hd bd_Card_orders; val bd_Cinfinites = map bd_Cinfinite_of_bnf bnfs; val bd_Cinfinite = hd bd_Cinfinites; val in_monos = map in_mono_of_bnf bnfs; val map_comp0s = map map_comp0_of_bnf bnfs; val sym_map_comps = map mk_sym map_comp0s; val map_comps = map map_comp_of_bnf bnfs; val map_cong0s = map map_cong0_of_bnf bnfs; val map_id0s = map map_id0_of_bnf bnfs; val map_ids = map map_id_of_bnf bnfs; val set_bdss = map set_bd_of_bnf bnfs; val set_mapss = map set_map_of_bnf bnfs; val rel_congs = map rel_cong0_of_bnf bnfs; val rel_converseps = map rel_conversep_of_bnf bnfs; val rel_Grps = map rel_Grp_of_bnf bnfs; val le_rel_OOs = map le_rel_OO_of_bnf bnfs; val in_rels = map in_rel_of_bnf bnfs; val timer = time (timer "Extracted terms & thms"); (* derived thms *) (*map g1 ... gm g(m+1) ... g(m+n) (map id ... id f(m+1) ... f(m+n) x) = map g1 ... gm (g(m+1) o f(m+1)) ... (g(m+n) o f(m+n)) x*) fun mk_map_comp_id x mapAsBs mapBsCs mapAsCs map_comp0 = let val lhs = Term.list_comb (mapBsCs, all_gs) $ (Term.list_comb (mapAsBs, passive_ids @ fs) $ x); val rhs = Term.list_comb (mapAsCs, take m all_gs @ map HOLogic.mk_comp (drop m all_gs ~~ fs)) $ x; val goal = mk_Trueprop_eq (lhs, rhs); val vars = Variable.add_free_names lthy goal []; in Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => mk_map_comp_id_tac ctxt map_comp0) |> Thm.close_derivation \<^here> end; val map_comp_id_thms = @{map 5} mk_map_comp_id xFs mapsAsBs mapsBsCs' mapsAsCs' map_comps; (*forall a : set(m+1) x. f(m+1) a = a; ...; forall a : set(m+n) x. f(m+n) a = a ==> map id ... id f(m+1) ... f(m+n) x = x*) fun mk_map_cong0L x mapAsAs sets map_cong0 map_id = let fun mk_prem set f z z' = HOLogic.mk_Trueprop (mk_Ball (set $ x) (Term.absfree z' (HOLogic.mk_eq (f $ z, z)))); val prems = @{map 4} mk_prem (drop m sets) self_fs zs zs'; val goal = mk_Trueprop_eq (Term.list_comb (mapAsAs, passive_ids @ self_fs) $ x, x); val vars = Variable.add_free_names lthy goal []; in Goal.prove_sorry lthy vars [] (Logic.list_implies (prems, goal)) (fn {context = ctxt, prems = _} => mk_map_cong0L_tac ctxt m map_cong0 map_id) |> Thm.close_derivation \<^here> end; val map_cong0L_thms = @{map 5} mk_map_cong0L xFs mapsAsAs setssAs map_cong0s map_ids; val in_mono'_thms = map (fn thm => (thm OF (replicate m subset_refl)) RS @{thm set_mp}) in_monos; val map_arg_cong_thms = let val prems = map2 (curry mk_Trueprop_eq) yFs yFs_copy; val maps = map (fn mapx => Term.list_comb (mapx, all_gs)) mapsBsCs'; val concls = @{map 3} (fn x => fn y => fn mapx => mk_Trueprop_eq (mapx $ x, mapx $ y)) yFs yFs_copy maps; val goals = map2 (fn prem => fn concl => Logic.mk_implies (prem, concl)) prems concls; in map (fn goal => Variable.add_free_names lthy goal [] |> (fn vars => Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => (hyp_subst_tac ctxt THEN' rtac ctxt refl) 1)) |> Thm.close_derivation \<^here>) goals end; val timer = time (timer "Derived simple theorems"); (* coalgebra *) val coalg_bind = mk_internal_b (coN ^ algN) ; val coalg_def_bind = (Thm.def_binding coalg_bind, []); (*forall i = 1 ... n: (\x \ Bi. si \ Fi_in UNIV .. UNIV B1 ... Bn)*) val coalg_spec = let val ins = @{map 3} mk_in (replicate n (passive_UNIVs @ Bs)) setssAs FTsAs; fun mk_coalg_conjunct B s X z z' = mk_Ball B (Term.absfree z' (HOLogic.mk_mem (s $ z, X))); val rhs = Library.foldr1 HOLogic.mk_conj (@{map 5} mk_coalg_conjunct Bs ss ins zs zs') in fold_rev (Term.absfree o Term.dest_Free) (Bs @ ss) rhs end; val ((coalg_free, (_, coalg_def_free)), (lthy, lthy_old)) = lthy |> Local_Theory.open_target |> snd |> Local_Theory.define ((coalg_bind, NoSyn), (coalg_def_bind, coalg_spec)) ||> `Local_Theory.close_target; val phi = Proof_Context.export_morphism lthy_old lthy; val coalg = fst (Term.dest_Const (Morphism.term phi coalg_free)); val coalg_def = mk_unabs_def (2 * n) (HOLogic.mk_obj_eq (Morphism.thm phi coalg_def_free)); fun mk_coalg Bs ss = let val args = Bs @ ss; val Ts = map fastype_of args; val coalgT = Library.foldr (op -->) (Ts, HOLogic.boolT); in Term.list_comb (Const (coalg, coalgT), args) end; val((((((zs, zs'), Bs), B's), ss), s's), _) = lthy |> mk_Frees' "b" activeAs ||>> mk_Frees "B" BTs ||>> mk_Frees "B'" B'Ts ||>> mk_Frees "s" sTs ||>> mk_Frees "s'" s'Ts; val coalg_prem = HOLogic.mk_Trueprop (mk_coalg Bs ss); val coalg_in_thms = map (fn i => coalg_def RS iffD1 RS mk_conjunctN n i RS bspec) ks val coalg_set_thmss = let val coalg_prem = HOLogic.mk_Trueprop (mk_coalg Bs ss); fun mk_prem x B = mk_Trueprop_mem (x, B); fun mk_concl s x B set = HOLogic.mk_Trueprop (mk_leq (set $ (s $ x)) B); val prems = map2 mk_prem zs Bs; val conclss = @{map 3} (fn s => fn x => fn sets => map2 (mk_concl s x) Bs (drop m sets)) ss zs setssAs; val goalss = map2 (fn prem => fn concls => map (fn concl => Logic.list_implies (coalg_prem :: [prem], concl)) concls) prems conclss; in map (fn goals => map (fn goal => Variable.add_free_names lthy goal [] |> (fn vars => Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => mk_coalg_set_tac ctxt coalg_def)) |> Thm.close_derivation \<^here>) goals) goalss end; fun mk_tcoalg BTs = mk_coalg (map HOLogic.mk_UNIV BTs); val tcoalg_thm = let val goal = HOLogic.mk_Trueprop (mk_tcoalg activeAs ss); val vars = Variable.add_free_names lthy goal []; in Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => (rtac ctxt (coalg_def RS iffD2) 1 THEN CONJ_WRAP (K (EVERY' [rtac ctxt ballI, rtac ctxt CollectI, CONJ_WRAP' (K (EVERY' [rtac ctxt @{thm subset_UNIV}])) allAs] 1)) ss)) |> Thm.close_derivation \<^here> end; val timer = time (timer "Coalgebra definition & thms"); (* morphism *) val mor_bind = mk_internal_b morN; val mor_def_bind = (Thm.def_binding mor_bind, []); (*fbetw) forall i = 1 ... n: (\x \ Bi. fi x \ B'i)*) (*mor) forall i = 1 ... n: (\x \ Bi. Fi_map id ... id f1 ... fn (si x) = si' (fi x)*) val mor_spec = let fun mk_fbetw f B1 B2 z z' = mk_Ball B1 (Term.absfree z' (HOLogic.mk_mem (f $ z, B2))); fun mk_mor B mapAsBs f s s' z z' = mk_Ball B (Term.absfree z' (HOLogic.mk_eq (Term.list_comb (mapAsBs, passive_ids @ fs @ [s $ z]), s' $ (f $ z)))); val rhs = HOLogic.mk_conj (Library.foldr1 HOLogic.mk_conj (@{map 5} mk_fbetw fs Bs B's zs zs'), Library.foldr1 HOLogic.mk_conj (@{map 7} mk_mor Bs mapsAsBs fs ss s's zs zs')) in fold_rev (Term.absfree o Term.dest_Free) (Bs @ ss @ B's @ s's @ fs) rhs end; val ((mor_free, (_, mor_def_free)), (lthy, lthy_old)) = lthy |> Local_Theory.open_target |> snd |> Local_Theory.define ((mor_bind, NoSyn), (mor_def_bind, mor_spec)) ||> `Local_Theory.close_target; val phi = Proof_Context.export_morphism lthy_old lthy; val mor = fst (Term.dest_Const (Morphism.term phi mor_free)); val mor_def = mk_unabs_def (5 * n) (HOLogic.mk_obj_eq (Morphism.thm phi mor_def_free)); fun mk_mor Bs1 ss1 Bs2 ss2 fs = let val args = Bs1 @ ss1 @ Bs2 @ ss2 @ fs; val Ts = map fastype_of (Bs1 @ ss1 @ Bs2 @ ss2 @ fs); val morT = Library.foldr (op -->) (Ts, HOLogic.boolT); in Term.list_comb (Const (mor, morT), args) end; val ((((((((((((((zs, z's), Bs), Bs_copy), B's), B''s), ss), s's), s''s), fs), fs_copy), gs), RFs), Rs), _) = lthy |> mk_Frees "b" activeAs ||>> mk_Frees "b" activeBs ||>> mk_Frees "B" BTs ||>> mk_Frees "B" BTs ||>> mk_Frees "B'" B'Ts ||>> mk_Frees "B''" B''Ts ||>> mk_Frees "s" sTs ||>> mk_Frees "s'" s'Ts ||>> mk_Frees "s''" s''Ts ||>> mk_Frees "f" fTs ||>> mk_Frees "f" fTs ||>> mk_Frees "g" gTs ||>> mk_Frees "x" FRTs ||>> mk_Frees "R" setRTs; val mor_prem = HOLogic.mk_Trueprop (mk_mor Bs ss B's s's fs); val (mor_image_thms, morE_thms) = let val prem = HOLogic.mk_Trueprop (mk_mor Bs ss B's s's fs); fun mk_image_goal f B1 B2 = Logic.mk_implies (prem, HOLogic.mk_Trueprop (mk_leq (mk_image f $ B1) B2)); val image_goals = @{map 3} mk_image_goal fs Bs B's; fun mk_elim_goal B mapAsBs f s s' x = Logic.list_implies ([prem, mk_Trueprop_mem (x, B)], mk_Trueprop_eq (Term.list_comb (mapAsBs, passive_ids @ fs @ [s $ x]), s' $ (f $ x))); val elim_goals = @{map 6} mk_elim_goal Bs mapsAsBs fs ss s's zs; fun prove goal = Variable.add_free_names lthy goal [] |> (fn vars => Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => mk_mor_elim_tac ctxt mor_def)) |> Thm.close_derivation \<^here>; in (map prove image_goals, map prove elim_goals) end; val mor_image'_thms = map (fn thm => @{thm set_mp} OF [thm, imageI]) mor_image_thms; val mor_incl_thm = let val prems = map2 (HOLogic.mk_Trueprop oo mk_leq) Bs Bs_copy; val concl = HOLogic.mk_Trueprop (mk_mor Bs ss Bs_copy ss active_ids); val vars = fold (Variable.add_free_names lthy) (concl :: prems) []; in Goal.prove_sorry lthy vars [] (Logic.list_implies (prems, concl)) (fn {context = ctxt, prems = _} => mk_mor_incl_tac ctxt mor_def map_ids) |> Thm.close_derivation \<^here> end; val mor_id_thm = mor_incl_thm OF (replicate n subset_refl); val mor_comp_thm = let val prems = [HOLogic.mk_Trueprop (mk_mor Bs ss B's s's fs), HOLogic.mk_Trueprop (mk_mor B's s's B''s s''s gs)]; val concl = HOLogic.mk_Trueprop (mk_mor Bs ss B''s s''s (map2 (curry HOLogic.mk_comp) gs fs)); val vars = fold (Variable.add_free_names lthy) (concl :: prems) []; in Goal.prove_sorry lthy vars [] (Logic.list_implies (prems, concl)) (fn {context = ctxt, prems = _} => mk_mor_comp_tac ctxt mor_def mor_image'_thms morE_thms map_comp_id_thms) |> Thm.close_derivation \<^here> end; val mor_cong_thm = let val prems = map HOLogic.mk_Trueprop (map2 (curry HOLogic.mk_eq) fs_copy fs @ [mk_mor Bs ss B's s's fs]) val concl = HOLogic.mk_Trueprop (mk_mor Bs ss B's s's fs_copy); val vars = fold (Variable.add_free_names lthy) (concl :: prems) []; in Goal.prove_sorry lthy vars [] (Logic.list_implies (prems, concl)) (fn {context = ctxt, prems = _} => (hyp_subst_tac ctxt THEN' assume_tac ctxt) 1) |> Thm.close_derivation \<^here> end; val mor_UNIV_thm = let fun mk_conjunct mapAsBs f s s' = HOLogic.mk_eq (HOLogic.mk_comp (Term.list_comb (mapAsBs, passive_ids @ fs), s), HOLogic.mk_comp (s', f)); val lhs = mk_mor active_UNIVs ss (map HOLogic.mk_UNIV activeBs) s's fs; val rhs = Library.foldr1 HOLogic.mk_conj (@{map 4} mk_conjunct mapsAsBs fs ss s's); val vars = fold (Variable.add_free_names lthy) [lhs, rhs] []; in Goal.prove_sorry lthy vars [] (mk_Trueprop_eq (lhs, rhs)) (fn {context = ctxt, prems = _} => mk_mor_UNIV_tac ctxt morE_thms mor_def) |> Thm.close_derivation \<^here> end; val mor_str_thm = let val maps = map2 (fn Ds => fn bnf => Term.list_comb (mk_map_of_bnf Ds allAs (passiveAs @ FTsAs) bnf, passive_ids @ ss)) Dss bnfs; val goal = HOLogic.mk_Trueprop (mk_mor active_UNIVs ss (map HOLogic.mk_UNIV FTsAs) maps ss); val vars = Variable.add_free_names lthy goal []; in Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => mk_mor_str_tac ctxt ks mor_UNIV_thm) |> Thm.close_derivation \<^here> end; val timer = time (timer "Morphism definition & thms"); (* bisimulation *) val bis_bind = mk_internal_b bisN; val bis_def_bind = (Thm.def_binding bis_bind, []); fun mk_bis_le_conjunct R B1 B2 = mk_leq R (mk_Times (B1, B2)); val bis_le = Library.foldr1 HOLogic.mk_conj (@{map 3} mk_bis_le_conjunct Rs Bs B's) val bis_spec = let val fst_args = passive_ids @ fsts; val snd_args = passive_ids @ snds; fun mk_bis R s s' b1 b2 RF map1 map2 sets = list_all_free [b1, b2] (HOLogic.mk_imp (HOLogic.mk_mem (HOLogic.mk_prod (b1, b2), R), mk_Bex (mk_in (passive_UNIVs @ Rs) sets (snd (dest_Free RF))) (Term.absfree (dest_Free RF) (HOLogic.mk_conj (HOLogic.mk_eq (Term.list_comb (map1, fst_args) $ RF, s $ b1), HOLogic.mk_eq (Term.list_comb (map2, snd_args) $ RF, s' $ b2)))))); val rhs = HOLogic.mk_conj (bis_le, Library.foldr1 HOLogic.mk_conj (@{map 9} mk_bis Rs ss s's zs z's RFs map_fsts map_snds bis_setss)) in fold_rev (Term.absfree o Term.dest_Free) (Bs @ ss @ B's @ s's @ Rs) rhs end; val ((bis_free, (_, bis_def_free)), (lthy, lthy_old)) = lthy |> Local_Theory.open_target |> snd |> Local_Theory.define ((bis_bind, NoSyn), (bis_def_bind, bis_spec)) ||> `Local_Theory.close_target; val phi = Proof_Context.export_morphism lthy_old lthy; val bis = fst (Term.dest_Const (Morphism.term phi bis_free)); val bis_def = mk_unabs_def (5 * n) (HOLogic.mk_obj_eq (Morphism.thm phi bis_def_free)); fun mk_bis Bs1 ss1 Bs2 ss2 Rs = let val args = Bs1 @ ss1 @ Bs2 @ ss2 @ Rs; val Ts = map fastype_of args; val bisT = Library.foldr (op -->) (Ts, HOLogic.boolT); in Term.list_comb (Const (bis, bisT), args) end; val (((((((((((((((((zs, z's), Bs), B's), B''s), ss), s's), s''s), fs), (Rtuple, Rtuple')), Rs), Rs_copy), R's), sRs), (idx, idx')), Idx), Ris), _) = lthy |> mk_Frees "b" activeAs ||>> mk_Frees "b" activeBs ||>> mk_Frees "B" BTs ||>> mk_Frees "B'" B'Ts ||>> mk_Frees "B''" B''Ts ||>> mk_Frees "s" sTs ||>> mk_Frees "s'" s'Ts ||>> mk_Frees "s''" s''Ts ||>> mk_Frees "f" fTs ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "Rtuple") all_sbisT ||>> mk_Frees "R" setRTs ||>> mk_Frees "R" setRTs ||>> mk_Frees "R'" setR'Ts ||>> mk_Frees "R" setsRTs ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "i") idxT ||>> yield_singleton (mk_Frees "I") (HOLogic.mk_setT idxT) ||>> mk_Frees "Ri" (map (fn T => idxT --> T) setRTs); val bis_cong_thm = let val prems = map HOLogic.mk_Trueprop (mk_bis Bs ss B's s's Rs :: map2 (curry HOLogic.mk_eq) Rs_copy Rs) val concl = HOLogic.mk_Trueprop (mk_bis Bs ss B's s's Rs_copy); val vars = fold (Variable.add_free_names lthy) (concl :: prems) []; in Goal.prove_sorry lthy vars [] (Logic.list_implies (prems, concl)) (fn {context = ctxt, prems = _} => (hyp_subst_tac ctxt THEN' assume_tac ctxt) 1) |> Thm.close_derivation \<^here> end; val bis_rel_thm = let fun mk_conjunct R s s' b1 b2 rel = list_all_free [b1, b2] (HOLogic.mk_imp (HOLogic.mk_mem (HOLogic.mk_prod (b1, b2), R), Term.list_comb (rel, passive_eqs @ map mk_in_rel Rs) $ (s $ b1) $ (s' $ b2))); val rhs = HOLogic.mk_conj (bis_le, Library.foldr1 HOLogic.mk_conj (@{map 6} mk_conjunct Rs ss s's zs z's relsAsBs)) val goal = mk_Trueprop_eq (mk_bis Bs ss B's s's Rs, rhs); val vars = Variable.add_free_names lthy goal []; in Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => mk_bis_rel_tac ctxt m bis_def in_rels map_comps map_cong0s set_mapss) |> Thm.close_derivation \<^here> end; val bis_converse_thm = let val goal = Logic.mk_implies (HOLogic.mk_Trueprop (mk_bis Bs ss B's s's Rs), HOLogic.mk_Trueprop (mk_bis B's s's Bs ss (map mk_converse Rs))); val vars = Variable.add_free_names lthy goal []; in Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => mk_bis_converse_tac ctxt m bis_rel_thm rel_congs rel_converseps) |> Thm.close_derivation \<^here> end; val bis_O_thm = let val prems = [HOLogic.mk_Trueprop (mk_bis Bs ss B's s's Rs), HOLogic.mk_Trueprop (mk_bis B's s's B''s s''s R's)]; val concl = HOLogic.mk_Trueprop (mk_bis Bs ss B''s s''s (map2 (curry mk_rel_comp) Rs R's)); val vars = fold (Variable.add_free_names lthy) (concl :: prems) []; in Goal.prove_sorry lthy vars [] (Logic.list_implies (prems, concl)) (fn {context = ctxt, prems = _} => mk_bis_O_tac ctxt m bis_rel_thm rel_congs le_rel_OOs) |> Thm.close_derivation \<^here> end; val bis_Gr_thm = let val concl = HOLogic.mk_Trueprop (mk_bis Bs ss B's s's (map2 mk_Gr Bs fs)); val vars = fold (Variable.add_free_names lthy) ([coalg_prem, mor_prem, concl]) []; in Goal.prove_sorry lthy vars [] (Logic.list_implies ([coalg_prem, mor_prem], concl)) (fn {context = ctxt, prems = _} => mk_bis_Gr_tac ctxt bis_rel_thm rel_Grps mor_image_thms morE_thms coalg_in_thms) |> Thm.close_derivation \<^here> end; val bis_image2_thm = bis_cong_thm OF ((bis_O_thm OF [bis_Gr_thm RS bis_converse_thm, bis_Gr_thm]) :: replicate n @{thm image2_Gr}); val bis_Id_on_thm = bis_cong_thm OF ((mor_id_thm RSN (2, bis_Gr_thm)) :: replicate n @{thm Id_on_Gr}); val bis_Union_thm = let val prem = HOLogic.mk_Trueprop (mk_Ball Idx (Term.absfree idx' (mk_bis Bs ss B's s's (map (fn R => R $ idx) Ris)))); val concl = HOLogic.mk_Trueprop (mk_bis Bs ss B's s's (map (mk_UNION Idx) Ris)); val vars = fold (Variable.add_free_names lthy) [prem, concl] []; in Goal.prove_sorry lthy vars [] (Logic.mk_implies (prem, concl)) (fn {context = ctxt, prems = _} => mk_bis_Union_tac ctxt bis_def in_mono'_thms) |> Thm.close_derivation \<^here> end; (* self-bisimulation *) fun mk_sbis Bs ss Rs = mk_bis Bs ss Bs ss Rs; (* largest self-bisimulation *) val lsbis_binds = mk_internal_bs lsbisN; fun lsbis_bind i = nth lsbis_binds (i - 1); val lsbis_def_bind = rpair [] o Thm.def_binding o lsbis_bind; val all_sbis = HOLogic.mk_Collect (fst Rtuple', snd Rtuple', list_exists_free sRs (HOLogic.mk_conj (HOLogic.mk_eq (Rtuple, HOLogic.mk_tuple sRs), mk_sbis Bs ss sRs))); fun lsbis_spec i = fold_rev (Term.absfree o Term.dest_Free) (Bs @ ss) (mk_UNION all_sbis (Term.absfree Rtuple' (mk_nthN n Rtuple i))); val ((lsbis_frees, (_, lsbis_def_frees)), (lthy, lthy_old)) = lthy |> Local_Theory.open_target |> snd |> fold_map (fn i => Local_Theory.define ((lsbis_bind i, NoSyn), (lsbis_def_bind i, lsbis_spec i))) ks |>> apsnd split_list o split_list ||> `Local_Theory.close_target; val phi = Proof_Context.export_morphism lthy_old lthy; val lsbis_defs = map (fn def => mk_unabs_def (2 * n) (HOLogic.mk_obj_eq (Morphism.thm phi def))) lsbis_def_frees; val lsbiss = map (fst o Term.dest_Const o Morphism.term phi) lsbis_frees; fun mk_lsbis Bs ss i = let val args = Bs @ ss; val Ts = map fastype_of args; val RT = mk_relT (`I (HOLogic.dest_setT (fastype_of (nth Bs (i - 1))))); val lsbisT = Library.foldr (op -->) (Ts, RT); in Term.list_comb (Const (nth lsbiss (i - 1), lsbisT), args) end; val (((((zs, zs'), Bs), ss), sRs), _) = lthy |> mk_Frees' "b" activeAs ||>> mk_Frees "B" BTs ||>> mk_Frees "s" sTs ||>> mk_Frees "R" setsRTs; val sbis_prem = HOLogic.mk_Trueprop (mk_sbis Bs ss sRs); val coalg_prem = HOLogic.mk_Trueprop (mk_coalg Bs ss); val sbis_lsbis_thm = let val goal = HOLogic.mk_Trueprop (mk_sbis Bs ss (map (mk_lsbis Bs ss) ks)); val vars = Variable.add_free_names lthy goal []; in Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => mk_sbis_lsbis_tac ctxt lsbis_defs bis_Union_thm bis_cong_thm) |> Thm.close_derivation \<^here> end; val lsbis_incl_thms = map (fn i => sbis_lsbis_thm RS (bis_def RS iffD1 RS conjunct1 RS mk_conjunctN n i)) ks; val lsbisE_thms = map (fn i => (mk_specN 2 (sbis_lsbis_thm RS (bis_def RS iffD1 RS conjunct2 RS mk_conjunctN n i))) RS mp) ks; val incl_lsbis_thms = let fun mk_concl i R = HOLogic.mk_Trueprop (mk_leq R (mk_lsbis Bs ss i)); val goals = map2 (fn i => fn R => Logic.mk_implies (sbis_prem, mk_concl i R)) ks sRs; in @{map 3} (fn goal => fn i => fn def => Variable.add_free_names lthy goal [] |> (fn vars => Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => mk_incl_lsbis_tac ctxt n i def)) |> Thm.close_derivation \<^here>) goals ks lsbis_defs end; val equiv_lsbis_thms = let fun mk_concl i B = HOLogic.mk_Trueprop (mk_equiv B (mk_lsbis Bs ss i)); val goals = map2 (fn i => fn B => Logic.mk_implies (coalg_prem, mk_concl i B)) ks Bs; in @{map 3} (fn goal => fn l_incl => fn incl_l => Variable.add_free_names lthy goal [] |> (fn vars => Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => mk_equiv_lsbis_tac ctxt sbis_lsbis_thm l_incl incl_l bis_Id_on_thm bis_converse_thm bis_O_thm) |> Thm.close_derivation \<^here>)) goals lsbis_incl_thms incl_lsbis_thms end; val timer = time (timer "Bisimulations"); (* bounds *) val (lthy, sbd, sbdT, sbd_card_order, sbd_Cinfinite, sbd_Card_order, set_sbdss) = if n = 1 then (lthy, sum_bd, sum_bdT, bd_card_order, bd_Cinfinite, bd_Card_order, set_bdss) else let val sbdT_bind = mk_internal_b sum_bdTN; val ((sbdT_name, (sbdT_glob_info, sbdT_loc_info)), lthy) = typedef (sbdT_bind, sum_bdT_params', NoSyn) (HOLogic.mk_UNIV sum_bdT) NONE (fn ctxt => EVERY' [rtac ctxt exI, rtac ctxt UNIV_I] 1) lthy; val sbdT = Type (sbdT_name, sum_bdT_params); val Abs_sbdT = Const (#Abs_name sbdT_glob_info, sum_bdT --> sbdT); val sbd_bind = mk_internal_b sum_bdN; val sbd_def_bind = (Thm.def_binding sbd_bind, []); val sbd_spec = mk_dir_image sum_bd Abs_sbdT; val ((sbd_free, (_, sbd_def_free)), (lthy, lthy_old)) = lthy |> Local_Theory.open_target |> snd |> Local_Theory.define ((sbd_bind, NoSyn), (sbd_def_bind, sbd_spec)) ||> `Local_Theory.close_target; val phi = Proof_Context.export_morphism lthy_old lthy; val sbd_def = HOLogic.mk_obj_eq (Morphism.thm phi sbd_def_free); val sbd = Const (fst (Term.dest_Const (Morphism.term phi sbd_free)), mk_relT (`I sbdT)); val Abs_sbdT_inj = mk_Abs_inj_thm (#Abs_inject sbdT_loc_info); val Abs_sbdT_bij = mk_Abs_bij_thm lthy Abs_sbdT_inj (#Abs_cases sbdT_loc_info); val sum_Cinfinite = mk_sum_Cinfinite bd_Cinfinites; val sum_Card_order = sum_Cinfinite RS conjunct2; val sum_card_order = mk_sum_card_order bd_card_orders; val sbd_ordIso = @{thm ssubst_Pair_rhs} OF [@{thm dir_image} OF [Abs_sbdT_inj, sum_Card_order], sbd_def]; val sbd_card_order = @{thm iffD2[OF arg_cong[of _ _ card_order]]} OF [sbd_def, @{thm card_order_dir_image} OF [Abs_sbdT_bij, sum_card_order]]; val sbd_Cinfinite = @{thm Cinfinite_cong} OF [sbd_ordIso, sum_Cinfinite]; val sbd_Card_order = sbd_Cinfinite RS conjunct2; fun mk_set_sbd i bd_Card_order bds = map (fn thm => @{thm ordLeq_ordIso_trans} OF [bd_Card_order RS mk_ordLeq_csum n i thm, sbd_ordIso]) bds; val set_sbdss = @{map 3} mk_set_sbd ks bd_Card_orders set_bdss; in (lthy, sbd, sbdT, sbd_card_order, sbd_Cinfinite, sbd_Card_order, set_sbdss) end; val sbdTs = replicate n sbdT; val sum_sbdT = mk_sumTN sbdTs; val sum_sbd_listT = HOLogic.listT sum_sbdT; val sum_sbd_list_setT = HOLogic.mk_setT sum_sbd_listT; val bdTs = passiveAs @ replicate n sbdT; val to_sbd_maps = @{map 4} mk_map_of_bnf Dss Ass (replicate n bdTs) bnfs; val bdFTs = mk_FTs bdTs; val sbdFT = mk_sumTN bdFTs; val treeT = HOLogic.mk_prodT (sum_sbd_list_setT, sum_sbd_listT --> sbdFT); val treeQT = HOLogic.mk_setT treeT; val treeTs = passiveAs @ replicate n treeT; val treeQTs = passiveAs @ replicate n treeQT; val treeFTs = mk_FTs treeTs; val tree_maps = @{map 4} mk_map_of_bnf Dss (replicate n bdTs) (replicate n treeTs) bnfs; val final_maps = @{map 4} mk_map_of_bnf Dss (replicate n treeTs) (replicate n treeQTs) bnfs; val isNode_setss = mk_setss (passiveAs @ replicate n sbdT); val root = HOLogic.mk_set sum_sbd_listT [HOLogic.mk_list sum_sbdT []]; val Zero = HOLogic.mk_tuple (map (fn U => absdummy U root) activeAs); val Lev_recT = fastype_of Zero; val Nil = HOLogic.mk_tuple (@{map 3} (fn i => fn z => fn z'=> Term.absfree z' (mk_InN activeAs z i)) ks zs zs'); val rv_recT = fastype_of Nil; val (((((((((((((((zs, zs'), zs_copy), ss), (nat, nat')), (sumx, sumx')), (kks, kks')), (kl, kl')), (kl_copy, kl'_copy)), (Kl, Kl')), (lab, lab')), (Kl_lab, Kl_lab')), xs), (Lev_rec, Lev_rec')), (rv_rec, rv_rec')), _) = lthy |> mk_Frees' "b" activeAs ||>> mk_Frees "b" activeAs ||>> mk_Frees "s" sTs ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "n") HOLogic.natT ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "sumx") sum_sbdT ||>> mk_Frees' "k" sbdTs ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "kl") sum_sbd_listT ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "kl") sum_sbd_listT ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "Kl") sum_sbd_list_setT ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "lab") (sum_sbd_listT --> sbdFT) ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "Kl_lab") treeT ||>> mk_Frees "x" bdFTs ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "rec") Lev_recT ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "rec") rv_recT; val (k, k') = (hd kks, hd kks') val timer = time (timer "Bounds"); (* tree coalgebra *) val isNode_binds = mk_internal_bs isNodeN; fun isNode_bind i = nth isNode_binds (i - 1); val isNode_def_bind = rpair [] o Thm.def_binding o isNode_bind; val isNodeT = Library.foldr (op -->) (map fastype_of [Kl, lab, kl], HOLogic.boolT); val Succs = @{map 3} (fn i => fn k => fn k' => HOLogic.mk_Collect (fst k', snd k', HOLogic.mk_mem (mk_InN sbdTs k i, mk_Succ Kl kl))) ks kks kks'; fun isNode_spec sets x i = let val active_sets = drop m (map (fn set => set $ x) sets); val rhs = list_exists_free [x] (Library.foldr1 HOLogic.mk_conj (HOLogic.mk_eq (lab $ kl, mk_InN bdFTs x i) :: map2 (curry HOLogic.mk_eq) active_sets Succs)); in fold_rev (Term.absfree o Term.dest_Free) [Kl, lab, kl] rhs end; val ((isNode_frees, (_, isNode_def_frees)), (lthy, lthy_old)) = lthy |> Local_Theory.open_target |> snd |> @{fold_map 3} (fn i => fn x => fn sets => Local_Theory.define ((isNode_bind i, NoSyn), (isNode_def_bind i, isNode_spec sets x i))) ks xs isNode_setss |>> apsnd split_list o split_list ||> `Local_Theory.close_target; val phi = Proof_Context.export_morphism lthy_old lthy; val isNode_defs = map (fn def => mk_unabs_def 3 (HOLogic.mk_obj_eq (Morphism.thm phi def))) isNode_def_frees; val isNodes = map (fst o Term.dest_Const o Morphism.term phi) isNode_frees; fun mk_isNode kl i = Term.list_comb (Const (nth isNodes (i - 1), isNodeT), [Kl, lab, kl]); val isTree = let val empty = HOLogic.mk_mem (HOLogic.mk_list sum_sbdT [], Kl); val tree = mk_Ball Kl (Term.absfree kl' (Library.foldr1 HOLogic.mk_conj (@{map 4} (fn Succ => fn i => fn k => fn k' => mk_Ball Succ (Term.absfree k' (mk_isNode (mk_append (kl, HOLogic.mk_list sum_sbdT [mk_InN sbdTs k i])) i))) Succs ks kks kks'))); in HOLogic.mk_conj (empty, tree) end; val carT_binds = mk_internal_bs carTN; fun carT_bind i = nth carT_binds (i - 1); val carT_def_bind = rpair [] o Thm.def_binding o carT_bind; fun carT_spec i = HOLogic.mk_Collect (fst Kl_lab', snd Kl_lab', list_exists_free [Kl, lab] (HOLogic.mk_conj (HOLogic.mk_eq (Kl_lab, HOLogic.mk_prod (Kl, lab)), HOLogic.mk_conj (isTree, mk_isNode (HOLogic.mk_list sum_sbdT []) i)))); val ((carT_frees, (_, carT_def_frees)), (lthy, lthy_old)) = lthy |> Local_Theory.open_target |> snd |> fold_map (fn i => Local_Theory.define ((carT_bind i, NoSyn), (carT_def_bind i, carT_spec i))) ks |>> apsnd split_list o split_list ||> `Local_Theory.close_target; val phi = Proof_Context.export_morphism lthy_old lthy; val carT_defs = map (fn def => HOLogic.mk_obj_eq (Morphism.thm phi def)) carT_def_frees; val carTs = map (fst o Term.dest_Const o Morphism.term phi) carT_frees; fun mk_carT i = Const (nth carTs (i - 1), HOLogic.mk_setT treeT); val strT_binds = mk_internal_bs strTN; fun strT_bind i = nth strT_binds (i - 1); val strT_def_bind = rpair [] o Thm.def_binding o strT_bind; fun strT_spec mapFT FT i = let fun mk_f i k k' = let val in_k = mk_InN sbdTs k i; in Term.absfree k' (HOLogic.mk_prod (mk_Shift Kl in_k, mk_shift lab in_k)) end; val f = Term.list_comb (mapFT, passive_ids @ @{map 3} mk_f ks kks kks'); val (fTs1, fTs2) = apsnd tl (chop (i - 1) (map (fn T => T --> FT) bdFTs)); val fs = map mk_undefined fTs1 @ (f :: map mk_undefined fTs2); in HOLogic.mk_case_prod (Term.absfree Kl' (Term.absfree lab' (mk_case_sumN fs $ (lab $ HOLogic.mk_list sum_sbdT [])))) end; val ((strT_frees, (_, strT_def_frees)), (lthy, lthy_old)) = lthy |> Local_Theory.open_target |> snd |> @{fold_map 3} (fn i => fn mapFT => fn FT => Local_Theory.define ((strT_bind i, NoSyn), (strT_def_bind i, strT_spec mapFT FT i))) ks tree_maps treeFTs |>> apsnd split_list o split_list ||> `Local_Theory.close_target; val phi = Proof_Context.export_morphism lthy_old lthy; val strT_defs = map (fn def => trans OF [HOLogic.mk_obj_eq (Morphism.thm phi def) RS fun_cong, @{thm prod.case}]) strT_def_frees; val strTs = map (fst o Term.dest_Const o Morphism.term phi) strT_frees; fun mk_strT FT i = Const (nth strTs (i - 1), treeT --> FT); val carTAs = map mk_carT ks; val strTAs = map2 mk_strT treeFTs ks; val coalgT_thm = Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop (mk_coalg carTAs strTAs)) (fn {context = ctxt, prems = _} => mk_coalgT_tac ctxt m (coalg_def :: isNode_defs @ carT_defs) strT_defs set_mapss) |> Thm.close_derivation \<^here>; val timer = time (timer "Tree coalgebra"); fun mk_to_sbd s x i i' = mk_toCard (nth (nth setssAs (i - 1)) (m + i' - 1) $ (s $ x)) sbd; fun mk_from_sbd s x i i' = mk_fromCard (nth (nth setssAs (i - 1)) (m + i' - 1) $ (s $ x)) sbd; fun mk_to_sbd_thmss thm = map (map (fn set_sbd => thm OF [set_sbd, sbd_Card_order]) o drop m) set_sbdss; val to_sbd_inj_thmss = mk_to_sbd_thmss @{thm toCard_inj}; val from_to_sbd_thmss = mk_to_sbd_thmss @{thm fromCard_toCard}; val Lev_bind = mk_internal_b LevN; val Lev_def_bind = rpair [] (Thm.def_binding Lev_bind); val Lev_spec = let fun mk_Suc i s setsAs a a' = let val sets = drop m setsAs; fun mk_set i' set b = let val Cons = HOLogic.mk_eq (kl_copy, mk_Cons (mk_InN sbdTs (mk_to_sbd s a i i' $ b) i') kl) val b_set = HOLogic.mk_mem (b, set $ (s $ a)); val kl_rec = HOLogic.mk_mem (kl, mk_nthN n Lev_rec i' $ b); in HOLogic.mk_Collect (fst kl'_copy, snd kl'_copy, list_exists_free [b, kl] (HOLogic.mk_conj (Cons, HOLogic.mk_conj (b_set, kl_rec)))) end; in Term.absfree a' (Library.foldl1 mk_union (@{map 3} mk_set ks sets zs_copy)) end; val Suc = Term.absdummy HOLogic.natT (Term.absfree Lev_rec' (HOLogic.mk_tuple (@{map 5} mk_Suc ks ss setssAs zs zs'))); val rhs = mk_rec_nat Zero Suc; in fold_rev (Term.absfree o Term.dest_Free) ss rhs end; val ((Lev_free, (_, Lev_def_free)), (lthy, lthy_old)) = lthy |> Local_Theory.open_target |> snd |> Local_Theory.define ((Lev_bind, NoSyn), (Lev_def_bind, Lev_spec)) ||> `Local_Theory.close_target; val phi = Proof_Context.export_morphism lthy_old lthy; val Lev_def = mk_unabs_def n (HOLogic.mk_obj_eq (Morphism.thm phi Lev_def_free)); val Lev = fst (Term.dest_Const (Morphism.term phi Lev_free)); fun mk_Lev ss nat i = let val Ts = map fastype_of ss; val LevT = Library.foldr (op -->) (Ts, HOLogic.natT --> HOLogic.mk_tupleT (map (fn U => domain_type U --> sum_sbd_list_setT) Ts)); in mk_nthN n (Term.list_comb (Const (Lev, LevT), ss) $ nat) i end; val Lev_0s = flat (mk_rec_simps n @{thm rec_nat_0_imp} [Lev_def]); val Lev_Sucs = flat (mk_rec_simps n @{thm rec_nat_Suc_imp} [Lev_def]); val rv_bind = mk_internal_b rvN; val rv_def_bind = rpair [] (Thm.def_binding rv_bind); val rv_spec = let fun mk_Cons i s b b' = let fun mk_case i' = Term.absfree k' (mk_nthN n rv_rec i' $ (mk_from_sbd s b i i' $ k)); in Term.absfree b' (mk_case_sumN (map mk_case ks) $ sumx) end; val Cons = Term.absfree sumx' (Term.absdummy sum_sbd_listT (Term.absfree rv_rec' (HOLogic.mk_tuple (@{map 4} mk_Cons ks ss zs zs')))); val rhs = mk_rec_list Nil Cons; in fold_rev (Term.absfree o Term.dest_Free) ss rhs end; val ((rv_free, (_, rv_def_free)), (lthy, lthy_old)) = lthy |> Local_Theory.open_target |> snd |> Local_Theory.define ((rv_bind, NoSyn), (rv_def_bind, rv_spec)) ||> `Local_Theory.close_target; val phi = Proof_Context.export_morphism lthy_old lthy; val rv_def = mk_unabs_def n (HOLogic.mk_obj_eq (Morphism.thm phi rv_def_free)); val rv = fst (Term.dest_Const (Morphism.term phi rv_free)); fun mk_rv ss kl i = let val Ts = map fastype_of ss; val As = map domain_type Ts; val rvT = Library.foldr (op -->) (Ts, fastype_of kl --> HOLogic.mk_tupleT (map (fn U => U --> mk_sumTN As) As)); in mk_nthN n (Term.list_comb (Const (rv, rvT), ss) $ kl) i end; val rv_Nils = flat (mk_rec_simps n @{thm rec_list_Nil_imp} [rv_def]); val rv_Conss = flat (mk_rec_simps n @{thm rec_list_Cons_imp} [rv_def]); val beh_binds = mk_internal_bs behN; fun beh_bind i = nth beh_binds (i - 1); val beh_def_bind = rpair [] o Thm.def_binding o beh_bind; fun beh_spec i z = let fun mk_case i to_sbd_map s k k' = Term.absfree k' (mk_InN bdFTs (Term.list_comb (to_sbd_map, passive_ids @ map (mk_to_sbd s k i) ks) $ (s $ k)) i); val Lab = Term.absfree kl' (mk_case_sumN (@{map 5} mk_case ks to_sbd_maps ss zs zs') $ (mk_rv ss kl i $ z)); val rhs = HOLogic.mk_prod (mk_UNION (HOLogic.mk_UNIV HOLogic.natT) (Term.absfree nat' (mk_Lev ss nat i $ z)), Lab); in fold_rev (Term.absfree o Term.dest_Free) (ss @ [z]) rhs end; val ((beh_frees, (_, beh_def_frees)), (lthy, lthy_old)) = lthy |> Local_Theory.open_target |> snd |> @{fold_map 2} (fn i => fn z => Local_Theory.define ((beh_bind i, NoSyn), (beh_def_bind i, beh_spec i z))) ks zs |>> apsnd split_list o split_list ||> `Local_Theory.close_target; val phi = Proof_Context.export_morphism lthy_old lthy; val beh_defs = map (fn def => mk_unabs_def (n + 1) (HOLogic.mk_obj_eq (Morphism.thm phi def))) beh_def_frees; val behs = map (fst o Term.dest_Const o Morphism.term phi) beh_frees; fun mk_beh ss i = let val Ts = map fastype_of ss; val behT = Library.foldr (op -->) (Ts, nth activeAs (i - 1) --> treeT); in Term.list_comb (Const (nth behs (i - 1), behT), ss) end; val ((((((zs, zs_copy), zs_copy2), ss), (nat, nat')), (kl, kl')), _) = lthy |> mk_Frees "b" activeAs ||>> mk_Frees "b" activeAs ||>> mk_Frees "b" activeAs ||>> mk_Frees "s" sTs ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "n") HOLogic.natT ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "kl") sum_sbd_listT; val (length_Lev_thms, length_Lev'_thms) = let fun mk_conjunct i z = HOLogic.mk_imp (HOLogic.mk_mem (kl, mk_Lev ss nat i $ z), HOLogic.mk_eq (mk_size kl, nat)); val goal = list_all_free (kl :: zs) (Library.foldr1 HOLogic.mk_conj (map2 mk_conjunct ks zs)); val vars = Variable.add_free_names lthy goal []; val cts = map (SOME o Thm.cterm_of lthy) [Term.absfree nat' goal, nat]; val length_Lev = Goal.prove_sorry lthy vars [] (HOLogic.mk_Trueprop goal) (fn {context = ctxt, prems = _} => mk_length_Lev_tac ctxt cts Lev_0s Lev_Sucs) |> Thm.close_derivation \<^here>; val length_Lev' = mk_specN (n + 1) length_Lev; val length_Levs = map (fn i => length_Lev' RS mk_conjunctN n i RS mp) ks; fun mk_goal i z = Logic.mk_implies (mk_Trueprop_mem (kl, mk_Lev ss nat i $ z), mk_Trueprop_mem (kl, mk_Lev ss (mk_size kl) i $ z)); val goals = map2 mk_goal ks zs; val length_Levs' = map2 (fn goal => fn length_Lev => Variable.add_free_names lthy goal [] |> (fn vars => Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => mk_length_Lev'_tac ctxt length_Lev)) |> Thm.close_derivation \<^here>) goals length_Levs; in (length_Levs, length_Levs') end; val rv_last_thmss = let fun mk_conjunct i z i' z_copy = list_exists_free [z_copy] (HOLogic.mk_eq (mk_rv ss (mk_append (kl, HOLogic.mk_list sum_sbdT [mk_InN sbdTs k i'])) i $ z, mk_InN activeAs z_copy i')); val goal = list_all_free (k :: zs) (Library.foldr1 HOLogic.mk_conj (map2 (fn i => fn z => Library.foldr1 HOLogic.mk_conj (map2 (mk_conjunct i z) ks zs_copy)) ks zs)); val vars = Variable.add_free_names lthy goal []; val cTs = [SOME (Thm.ctyp_of lthy sum_sbdT)]; val cts = map (SOME o Thm.cterm_of lthy) [Term.absfree kl' goal, kl]; val rv_last = Goal.prove_sorry lthy vars [] (HOLogic.mk_Trueprop goal) (fn {context = ctxt, prems = _} => mk_rv_last_tac ctxt cTs cts rv_Nils rv_Conss) |> Thm.close_derivation \<^here>; val rv_last' = mk_specN (n + 1) rv_last; in map (fn i => map (fn i' => rv_last' RS mk_conjunctN n i RS mk_conjunctN n i') ks) ks end; val set_Lev_thmsss = let fun mk_conjunct i z = let fun mk_conjunct' i' sets s z' = let fun mk_conjunct'' i'' set z'' = HOLogic.mk_imp (HOLogic.mk_mem (z'', set $ (s $ z')), HOLogic.mk_mem (mk_append (kl, HOLogic.mk_list sum_sbdT [mk_InN sbdTs (mk_to_sbd s z' i' i'' $ z'') i'']), mk_Lev ss (HOLogic.mk_Suc nat) i $ z)); in HOLogic.mk_imp (HOLogic.mk_eq (mk_rv ss kl i $ z, mk_InN activeAs z' i'), (Library.foldr1 HOLogic.mk_conj (@{map 3} mk_conjunct'' ks (drop m sets) zs_copy2))) end; in HOLogic.mk_imp (HOLogic.mk_mem (kl, mk_Lev ss nat i $ z), Library.foldr1 HOLogic.mk_conj (@{map 4} mk_conjunct' ks setssAs ss zs_copy)) end; val goal = list_all_free (kl :: zs @ zs_copy @ zs_copy2) (Library.foldr1 HOLogic.mk_conj (map2 mk_conjunct ks zs)); val vars = Variable.add_free_names lthy goal []; val cts = map (SOME o Thm.cterm_of lthy) [Term.absfree nat' goal, nat]; val set_Lev = Goal.prove_sorry lthy vars [] (HOLogic.mk_Trueprop goal) (fn {context = ctxt, prems = _} => mk_set_Lev_tac ctxt cts Lev_0s Lev_Sucs rv_Nils rv_Conss from_to_sbd_thmss) |> Thm.close_derivation \<^here>; val set_Lev' = mk_specN (3 * n + 1) set_Lev; in map (fn i => map (fn i' => map (fn i'' => set_Lev' RS mk_conjunctN n i RS mp RS mk_conjunctN n i' RS mp RS mk_conjunctN n i'' RS mp) ks) ks) ks end; val set_image_Lev_thmsss = let fun mk_conjunct i z = let fun mk_conjunct' i' sets = let fun mk_conjunct'' i'' set s z'' = HOLogic.mk_imp (HOLogic.mk_eq (mk_rv ss kl i $ z, mk_InN activeAs z'' i''), HOLogic.mk_mem (k, mk_image (mk_to_sbd s z'' i'' i') $ (set $ (s $ z'')))); in HOLogic.mk_imp (HOLogic.mk_mem (mk_append (kl, HOLogic.mk_list sum_sbdT [mk_InN sbdTs k i']), mk_Lev ss (HOLogic.mk_Suc nat) i $ z), (Library.foldr1 HOLogic.mk_conj (@{map 4} mk_conjunct'' ks sets ss zs_copy))) end; in HOLogic.mk_imp (HOLogic.mk_mem (kl, mk_Lev ss nat i $ z), Library.foldr1 HOLogic.mk_conj (map2 mk_conjunct' ks (drop m setssAs'))) end; val goal = list_all_free (kl :: k :: zs @ zs_copy) (Library.foldr1 HOLogic.mk_conj (map2 mk_conjunct ks zs)); val vars = Variable.add_free_names lthy goal []; val cts = map (SOME o Thm.cterm_of lthy) [Term.absfree nat' goal, nat]; val set_image_Lev = Goal.prove_sorry lthy vars [] (HOLogic.mk_Trueprop goal) (fn {context = ctxt, prems = _} => mk_set_image_Lev_tac ctxt cts Lev_0s Lev_Sucs rv_Nils rv_Conss from_to_sbd_thmss to_sbd_inj_thmss) |> Thm.close_derivation \<^here>; val set_image_Lev' = mk_specN (2 * n + 2) set_image_Lev; in map (fn i => map (fn i' => map (fn i'' => set_image_Lev' RS mk_conjunctN n i RS mp RS mk_conjunctN n i'' RS mp RS mk_conjunctN n i' RS mp) ks) ks) ks end; val mor_beh_thm = let val goal = HOLogic.mk_Trueprop (mk_mor active_UNIVs ss carTAs strTAs (map (mk_beh ss) ks)); val vars = Variable.add_free_names lthy goal []; in Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => mk_mor_beh_tac ctxt m mor_def mor_cong_thm beh_defs carT_defs strT_defs isNode_defs to_sbd_inj_thmss from_to_sbd_thmss Lev_0s Lev_Sucs rv_Nils rv_Conss length_Lev_thms length_Lev'_thms rv_last_thmss set_Lev_thmsss set_image_Lev_thmsss set_mapss map_comp_id_thms map_cong0s) |> Thm.close_derivation \<^here> end; val timer = time (timer "Behavioral morphism"); val lsbisAs = map (mk_lsbis carTAs strTAs) ks; fun mk_str_final i = mk_univ (HOLogic.mk_comp (Term.list_comb (nth final_maps (i - 1), passive_ids @ map mk_proj lsbisAs), nth strTAs (i - 1))); val car_finals = map2 mk_quotient carTAs lsbisAs; val str_finals = map mk_str_final ks; val coalgT_set_thmss = map (map (fn thm => coalgT_thm RS thm)) coalg_set_thmss; val equiv_LSBIS_thms = map (fn thm => coalgT_thm RS thm) equiv_lsbis_thms; val congruent_str_final_thms = let fun mk_goal R final_map strT = HOLogic.mk_Trueprop (mk_congruent R (HOLogic.mk_comp (Term.list_comb (final_map, passive_ids @ map mk_proj lsbisAs), strT))); val goals = @{map 3} mk_goal lsbisAs final_maps strTAs; in @{map 4} (fn goal => fn lsbisE => fn map_comp_id => fn map_cong0 => Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} => mk_congruent_str_final_tac ctxt m lsbisE map_comp_id map_cong0 equiv_LSBIS_thms) |> Thm.close_derivation \<^here>) goals lsbisE_thms map_comp_id_thms map_cong0s end; val coalg_final_thm = Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop (mk_coalg car_finals str_finals)) (fn {context = ctxt, prems = _} => mk_coalg_final_tac ctxt m coalg_def congruent_str_final_thms equiv_LSBIS_thms set_mapss coalgT_set_thmss) |> Thm.close_derivation \<^here>; val mor_T_final_thm = Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop (mk_mor carTAs strTAs car_finals str_finals (map mk_proj lsbisAs))) (fn {context = ctxt, prems = _} => mk_mor_T_final_tac ctxt mor_def congruent_str_final_thms equiv_LSBIS_thms) |> Thm.close_derivation \<^here>; val mor_final_thm = mor_comp_thm OF [mor_beh_thm, mor_T_final_thm]; val in_car_final_thms = map (fn thm => thm OF [mor_final_thm, UNIV_I]) mor_image'_thms; val timer = time (timer "Final coalgebra"); val ((T_names, (T_glob_infos, T_loc_infos)), lthy) = lthy |> @{fold_map 4} (fn b => fn mx => fn car_final => fn in_car_final => typedef (b, params, mx) car_final NONE (fn ctxt => EVERY' [rtac ctxt exI, rtac ctxt in_car_final] 1)) bs mixfixes car_finals in_car_final_thms |>> apsnd split_list o split_list; val Ts = map (fn name => Type (name, params')) T_names; fun mk_Ts passive = map (Term.typ_subst_atomic (passiveAs ~~ passive)) Ts; val Ts' = mk_Ts passiveBs; val Rep_Ts = map2 (fn info => fn T => Const (#Rep_name info, T --> treeQT)) T_glob_infos Ts; val Abs_Ts = map2 (fn info => fn T => Const (#Abs_name info, treeQT --> T)) T_glob_infos Ts; val Reps = map #Rep T_loc_infos; val Rep_injects = map #Rep_inject T_loc_infos; val Abs_inverses = map #Abs_inverse T_loc_infos; val timer = time (timer "THE TYPEDEFs & Rep/Abs thms"); val UNIVs = map HOLogic.mk_UNIV Ts; val FTs = mk_FTs (passiveAs @ Ts); val FTs_setss = mk_setss (passiveAs @ Ts); val map_FTs = map2 (fn Ds => mk_map_of_bnf Ds treeQTs (passiveAs @ Ts)) Dss bnfs; val unfold_fTs = map2 (curry op -->) activeAs Ts; val emptys = map (fn T => HOLogic.mk_set T []) passiveAs; val Zeros = map (fn empty => HOLogic.mk_tuple (map (fn U => absdummy U empty) Ts)) emptys; val hrecTs = map fastype_of Zeros; val (((zs, ss), (Jzs, Jzs')), _) = lthy |> mk_Frees "b" activeAs ||>> mk_Frees "s" sTs ||>> mk_Frees' "z" Ts; fun dtor_bind i = nth external_bs (i - 1) |> Binding.prefix_name (dtorN ^ "_"); val dtor_def_bind = rpair [] o Binding.concealed o Thm.def_binding o dtor_bind; fun dtor_spec rep str map_FT Jz Jz' = Term.absfree Jz' (Term.list_comb (map_FT, map HOLogic.id_const passiveAs @ Abs_Ts) $ (str $ (rep $ Jz))); val ((dtor_frees, (_, dtor_def_frees)), (lthy, lthy_old)) = lthy |> Local_Theory.open_target |> snd |> @{fold_map 6} (fn i => fn rep => fn str => fn mapx => fn Jz => fn Jz' => Local_Theory.define ((dtor_bind i, NoSyn), (dtor_def_bind i, dtor_spec rep str mapx Jz Jz'))) ks Rep_Ts str_finals map_FTs Jzs Jzs' |>> apsnd split_list o split_list ||> `Local_Theory.close_target; val phi = Proof_Context.export_morphism lthy_old lthy; fun mk_dtors passive = map (Term.subst_atomic_types (map (Morphism.typ phi) params' ~~ (mk_params passive)) o Morphism.term phi) dtor_frees; val dtors = mk_dtors passiveAs; val dtor's = mk_dtors passiveBs; val dtor_defs = map (fn def => HOLogic.mk_obj_eq (Morphism.thm phi def) RS fun_cong) dtor_def_frees; val coalg_final_set_thmss = map (map (fn thm => coalg_final_thm RS thm)) coalg_set_thmss; val (mor_Rep_thm, mor_Abs_thm) = let val mor_Rep = Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop (mk_mor UNIVs dtors car_finals str_finals Rep_Ts)) (fn {context = ctxt, prems = _} => mk_mor_Rep_tac ctxt (mor_def :: dtor_defs) Reps Abs_inverses coalg_final_set_thmss map_comp_id_thms map_cong0L_thms) |> Thm.close_derivation \<^here>; val mor_Abs = Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop (mk_mor car_finals str_finals UNIVs dtors Abs_Ts)) (fn {context = ctxt, prems = _} => mk_mor_Abs_tac ctxt (mor_def :: dtor_defs) Abs_inverses) |> Thm.close_derivation \<^here>; in (mor_Rep, mor_Abs) end; val timer = time (timer "dtor definitions & thms"); fun unfold_bind i = nth external_bs (i - 1) |> Binding.prefix_name (dtor_unfoldN ^ "_"); val unfold_def_bind = rpair [] o Binding.concealed o Thm.def_binding o unfold_bind; fun unfold_spec abs f z = fold_rev (Term.absfree o Term.dest_Free) (ss @ [z]) (abs $ (f $ z)); val ((unfold_frees, (_, unfold_def_frees)), (lthy, lthy_old)) = lthy |> Local_Theory.open_target |> snd |> @{fold_map 4} (fn i => fn abs => fn f => fn z => Local_Theory.define ((unfold_bind i, NoSyn), (unfold_def_bind i, unfold_spec abs f z))) ks Abs_Ts (map (fn i => HOLogic.mk_comp (mk_proj (nth lsbisAs (i - 1)), mk_beh ss i)) ks) zs |>> apsnd split_list o split_list ||> `Local_Theory.close_target; val phi = Proof_Context.export_morphism lthy_old lthy; val unfolds = map (Morphism.term phi) unfold_frees; val unfold_names = map (fst o dest_Const) unfolds; fun mk_unfolds passives actives = @{map 3} (fn name => fn T => fn active => Const (name, Library.foldr (op -->) (map2 (curry op -->) actives (mk_FTs (passives @ actives)), active --> T))) unfold_names (mk_Ts passives) actives; fun mk_unfold Ts ss i = Term.list_comb (Const (nth unfold_names (i - 1), Library.foldr (op -->) (map fastype_of ss, domain_type (fastype_of (nth ss (i - 1))) --> nth Ts (i - 1))), ss); val unfold_defs = map (fn def => mk_unabs_def (n + 1) (HOLogic.mk_obj_eq (Morphism.thm phi def))) unfold_def_frees; val (((ss, TRs), unfold_fs), _) = lthy |> mk_Frees "s" sTs ||>> mk_Frees "r" (map (mk_relT o `I) Ts) ||>> mk_Frees "f" unfold_fTs; val mor_unfold_thm = let val Abs_inverses' = map2 (curry op RS) in_car_final_thms Abs_inverses; val morEs' = map (fn thm => (thm OF [mor_final_thm, UNIV_I]) RS sym) morE_thms; val goal = HOLogic.mk_Trueprop (mk_mor active_UNIVs ss UNIVs dtors (map (mk_unfold Ts ss) ks)); val vars = Variable.add_free_names lthy goal []; in Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => mk_mor_unfold_tac ctxt m mor_UNIV_thm dtor_defs unfold_defs Abs_inverses' morEs' map_comp_id_thms map_cong0s) |> Thm.close_derivation \<^here> end; val dtor_unfold_thms = map (fn thm => (thm OF [mor_unfold_thm, UNIV_I]) RS sym) morE_thms; val (raw_coind_thms, raw_coind_thm) = let val prem = HOLogic.mk_Trueprop (mk_sbis UNIVs dtors TRs); val concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 (fn R => fn T => mk_leq R (Id_const T)) TRs Ts)); val vars = fold (Variable.add_free_names lthy) [prem, concl] []; in `split_conj_thm (Goal.prove_sorry lthy vars [] (Logic.mk_implies (prem, concl)) (fn {context = ctxt, prems = _} => mk_raw_coind_tac ctxt bis_def bis_cong_thm bis_O_thm bis_converse_thm bis_Gr_thm tcoalg_thm coalgT_thm mor_T_final_thm sbis_lsbis_thm lsbis_incl_thms incl_lsbis_thms equiv_LSBIS_thms mor_Rep_thm Rep_injects) |> Thm.close_derivation \<^here>) end; val (unfold_unique_mor_thms, unfold_unique_mor_thm) = let val prem = HOLogic.mk_Trueprop (mk_mor active_UNIVs ss UNIVs dtors unfold_fs); fun mk_fun_eq f i = HOLogic.mk_eq (f, mk_unfold Ts ss i); val unique = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 mk_fun_eq unfold_fs ks)); val vars = fold (Variable.add_free_names lthy) [prem, unique] []; val bis_thm = tcoalg_thm RSN (2, tcoalg_thm RS bis_image2_thm); val mor_thm = mor_comp_thm OF [mor_final_thm, mor_Abs_thm]; val unique_mor = Goal.prove_sorry lthy vars [] (Logic.mk_implies (prem, unique)) (fn {context = ctxt, prems = _} => mk_unfold_unique_mor_tac ctxt raw_coind_thms bis_thm mor_thm unfold_defs) |> Thm.close_derivation \<^here>; in `split_conj_thm unique_mor end; val (dtor_unfold_unique_thms, dtor_unfold_unique_thm) = `split_conj_thm (split_conj_prems n (mor_UNIV_thm RS iffD2 RS unfold_unique_mor_thm)); val unfold_dtor_thms = map (fn thm => mor_id_thm RS thm RS sym) unfold_unique_mor_thms; val unfold_o_dtor_thms = let val mor = mor_comp_thm OF [mor_str_thm, mor_unfold_thm]; in map2 (fn unique => fn unfold_ctor => trans OF [mor RS unique, unfold_ctor]) unfold_unique_mor_thms unfold_dtor_thms end; val timer = time (timer "unfold definitions & thms"); val map_dtors = map2 (fn Ds => fn bnf => Term.list_comb (mk_map_of_bnf Ds (passiveAs @ Ts) (passiveAs @ FTs) bnf, map HOLogic.id_const passiveAs @ dtors)) Dss bnfs; fun ctor_bind i = nth external_bs (i - 1) |> Binding.prefix_name (ctorN ^ "_"); val ctor_def_bind = rpair [] o Binding.concealed o Thm.def_binding o ctor_bind; fun ctor_spec i = mk_unfold Ts map_dtors i; val ((ctor_frees, (_, ctor_def_frees)), (lthy, lthy_old)) = lthy |> Local_Theory.open_target |> snd |> fold_map (fn i => Local_Theory.define ((ctor_bind i, NoSyn), (ctor_def_bind i, ctor_spec i))) ks |>> apsnd split_list o split_list ||> `Local_Theory.close_target; val phi = Proof_Context.export_morphism lthy_old lthy; fun mk_ctors params = map (Term.subst_atomic_types (map (Morphism.typ phi) params' ~~ params) o Morphism.term phi) ctor_frees; val ctors = mk_ctors params'; val ctor_defs = map (fn def => HOLogic.mk_obj_eq (Morphism.thm phi def)) ctor_def_frees; val ctor_o_dtor_thms = map2 (Local_Defs.fold lthy o single) ctor_defs unfold_o_dtor_thms; val dtor_o_ctor_thms = let fun mk_goal dtor ctor FT = mk_Trueprop_eq (HOLogic.mk_comp (dtor, ctor), HOLogic.id_const FT); val goals = @{map 3} mk_goal dtors ctors FTs; in @{map 5} (fn goal => fn ctor_def => fn unfold => fn map_comp_id => fn map_cong0L => Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} => mk_dtor_o_ctor_tac ctxt ctor_def unfold map_comp_id map_cong0L unfold_o_dtor_thms) |> Thm.close_derivation \<^here>) goals ctor_defs dtor_unfold_thms map_comp_id_thms map_cong0L_thms end; val dtor_ctor_thms = map (fn thm => thm RS @{thm pointfree_idE}) dtor_o_ctor_thms; val ctor_dtor_thms = map (fn thm => thm RS @{thm pointfree_idE}) ctor_o_dtor_thms; val bij_dtor_thms = map2 (fn thm1 => fn thm2 => @{thm o_bij} OF [thm1, thm2]) ctor_o_dtor_thms dtor_o_ctor_thms; val inj_dtor_thms = map (fn thm => thm RS @{thm bij_is_inj}) bij_dtor_thms; val surj_dtor_thms = map (fn thm => thm RS @{thm bij_is_surj}) bij_dtor_thms; val dtor_nchotomy_thms = map (fn thm => thm RS @{thm surjD}) surj_dtor_thms; val dtor_inject_thms = map (fn thm => thm RS @{thm inj_eq}) inj_dtor_thms; val dtor_exhaust_thms = map (fn thm => thm RS exE) dtor_nchotomy_thms; val bij_ctor_thms = map2 (fn thm1 => fn thm2 => @{thm o_bij} OF [thm1, thm2]) dtor_o_ctor_thms ctor_o_dtor_thms; val inj_ctor_thms = map (fn thm => thm RS @{thm bij_is_inj}) bij_ctor_thms; val surj_ctor_thms = map (fn thm => thm RS @{thm bij_is_surj}) bij_ctor_thms; val ctor_nchotomy_thms = map (fn thm => thm RS @{thm surjD}) surj_ctor_thms; val ctor_inject_thms = map (fn thm => thm RS @{thm inj_eq}) inj_ctor_thms; val ctor_exhaust_thms = map (fn thm => thm RS exE) ctor_nchotomy_thms; val timer = time (timer "ctor definitions & thms"); val (((((Jzs, Jzs_copy), Jzs1), Jzs2), phis), _) = lthy |> mk_Frees "z" Ts ||>> mk_Frees "z'" Ts ||>> mk_Frees "z1" Ts ||>> mk_Frees "z2" Ts ||>> mk_Frees "P" (map2 mk_pred2T Ts Ts); val (coinduct_params, dtor_coinduct_thm) = let val rels = map (Term.subst_atomic_types ((activeAs ~~ Ts) @ (activeBs ~~ Ts))) relsAsBs; fun mk_concl phi z1 z2 = HOLogic.mk_imp (phi $ z1 $ z2, HOLogic.mk_eq (z1, z2)); val concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (@{map 3} mk_concl phis Jzs1 Jzs2)); fun mk_rel_prem phi dtor rel Jz Jz_copy = let val concl = Term.list_comb (rel, passive_eqs @ phis) $ (dtor $ Jz) $ (dtor $ Jz_copy); in HOLogic.mk_Trueprop (list_all_free [Jz, Jz_copy] (HOLogic.mk_imp (phi $ Jz $ Jz_copy, concl))) end; val rel_prems = @{map 5} mk_rel_prem phis dtors rels Jzs Jzs_copy; val dtor_coinduct_goal = Logic.list_implies (rel_prems, concl); val dtor_coinduct = Variable.add_free_names lthy dtor_coinduct_goal [] |> (fn vars => Goal.prove_sorry lthy vars [] dtor_coinduct_goal (fn {context = ctxt, prems = _} => mk_dtor_coinduct_tac ctxt m raw_coind_thm bis_rel_thm rel_congs)) |> Thm.close_derivation \<^here>; in (rev (Term.add_tfrees dtor_coinduct_goal []), dtor_coinduct) end; val timer = time (timer "coinduction"); fun mk_dtor_map_DEADID_thm dtor_inject map_id0 = trans OF [iffD2 OF [dtor_inject, id_apply], map_id0 RS sym]; fun mk_dtor_map_unique_DEADID_thm () = let val (funs, algs) = HOLogic.conjuncts (HOLogic.dest_Trueprop (Thm.concl_of dtor_unfold_unique_thm)) |> map_split HOLogic.dest_eq ||> snd o strip_comb o hd |> @{apply 2} (map (fst o dest_Var)); fun mk_fun_insts T ix = Thm.cterm_of lthy (Var (ix, T --> T)); val theta = (funs ~~ @{map 2} mk_fun_insts Ts funs) @ (algs ~~ map (Thm.cterm_of lthy) dtors); val dtor_unfold_dtors = (dtor_unfold_unique_thm OF map (fn thm => mk_trans (thm RS @{thm arg_cong2[of _ _ _ _ "(\)", OF _ refl]}) @{thm trans[OF id_o o_id[symmetric]]}) map_id0s) |> split_conj_thm |> map mk_sym; in infer_instantiate lthy theta dtor_unfold_unique_thm |> Morphism.thm (Local_Theory.target_morphism lthy) |> unfold_thms lthy dtor_unfold_dtors |> (fn thm => thm OF replicate n sym) end; (* thm trans[OF x.dtor_unfold_unique x.dtor_unfold_unique[symmetric, OF trans[OF arg_cong2[of _ _ _ _ "(o)", OF pre_x.map_id0 refl] trans[OF id_o o_id[symmetric]]]], OF sym] *) fun mk_dtor_Jrel_DEADID_thm dtor_inject bnf = trans OF [rel_eq_of_bnf bnf RS @{thm predicate2_eqD}, dtor_inject] RS sym; val JphiTs = map2 mk_pred2T passiveAs passiveBs; val Jpsi1Ts = map2 mk_pred2T passiveAs passiveCs; val Jpsi2Ts = map2 mk_pred2T passiveCs passiveBs; val prodTsTs' = map2 (curry HOLogic.mk_prodT) Ts Ts'; val fstsTsTs' = map fst_const prodTsTs'; val sndsTsTs' = map snd_const prodTsTs'; val activephiTs = map2 mk_pred2T activeAs activeBs; val activeJphiTs = map2 mk_pred2T Ts Ts'; val rels = map2 (fn Ds => mk_rel_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs; val ((((Jzs, Jz's), Jphis), activeJphis), _) = lthy |> mk_Frees "z" Ts ||>> mk_Frees "y" Ts' ||>> mk_Frees "R" JphiTs ||>> mk_Frees "JR" activeJphiTs; fun mk_Jrel_DEADID_coinduct_thm () = mk_xtor_rel_co_induct_thm Greatest_FP rels activeJphis (map HOLogic.eq_const Ts) Jphis Jzs Jz's dtors dtor's (fn {context = ctxt, prems} => (unfold_thms_tac ctxt @{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} THEN REPEAT_DETERM (rtac ctxt allI 1) THEN rtac ctxt (dtor_coinduct_thm OF prems) 1)) lthy; (*register new codatatypes as BNFs*) val (timer, Jbnfs, (dtor_Jmap_o_thms, dtor_Jmap_thms), dtor_Jmap_unique_thm, dtor_Jset_thmss', dtor_Jrel_thms, Jrel_coinduct_thm, Jbnf_notes, dtor_Jset_induct_thms, lthy) = if m = 0 then (timer, replicate n DEADID_bnf, map_split (`(mk_pointfree2 lthy)) (map2 mk_dtor_map_DEADID_thm dtor_inject_thms map_ids), mk_dtor_map_unique_DEADID_thm (), replicate n [], map2 mk_dtor_Jrel_DEADID_thm dtor_inject_thms bnfs, mk_Jrel_DEADID_coinduct_thm (), [], [], lthy) else let val fTs = map2 (curry op -->) passiveAs passiveBs; val gTs = map2 (curry op -->) passiveBs passiveCs; val uTs = map2 (curry op -->) Ts Ts'; val (((((nat, nat'), (Jzs, Jzs')), (hrecs, hrecs')), (fs, fs')), _) = lthy |> yield_singleton (apfst (op ~~) oo mk_Frees' "n") HOLogic.natT ||>> mk_Frees' "z" Ts ||>> mk_Frees' "rec" hrecTs ||>> mk_Frees' "f" fTs; val map_FTFT's = map2 (fn Ds => mk_map_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs; fun mk_maps ATs BTs Ts mk_T = map2 (fn Ds => mk_map_of_bnf Ds (ATs @ Ts) (BTs @ map mk_T Ts)) Dss bnfs; fun mk_Fmap mk_const fs Ts Fmap = Term.list_comb (Fmap, fs @ map mk_const Ts); fun mk_map mk_const mk_T Ts fs Ts' dtors mk_maps = mk_unfold Ts' (map2 (fn dtor => fn Fmap => HOLogic.mk_comp (mk_Fmap mk_const fs Ts Fmap, dtor)) dtors (mk_maps Ts mk_T)); val mk_map_id = mk_map HOLogic.id_const I; val mk_mapsAB = mk_maps passiveAs passiveBs; val fs_maps = map (mk_map_id Ts fs Ts' dtors mk_mapsAB) ks; val set_bss = map (flat o map2 (fn B => fn b => if member (op =) resDs (TFree B) then [] else [b]) resBs) set_bss0; fun col_bind j = mk_internal_b (colN ^ (if m = 1 then "" else string_of_int j)); val col_def_bind = rpair [] o Thm.def_binding o col_bind; fun col_spec j Zero hrec hrec' = let fun mk_Suc dtor sets z z' = let val (set, sets) = apfst (fn xs => nth xs (j - 1)) (chop m sets); fun mk_UN set k = mk_UNION (set $ (dtor $ z)) (mk_nthN n hrec k); in Term.absfree z' (mk_union (set $ (dtor $ z), Library.foldl1 mk_union (map2 mk_UN sets ks))) end; val Suc = Term.absdummy HOLogic.natT (Term.absfree hrec' (HOLogic.mk_tuple (@{map 4} mk_Suc dtors FTs_setss Jzs Jzs'))); in mk_rec_nat Zero Suc end; val ((col_frees, (_, col_def_frees)), (lthy, lthy_old)) = lthy |> Local_Theory.open_target |> snd |> @{fold_map 4} (fn j => fn Zero => fn hrec => fn hrec' => Local_Theory.define ((col_bind j, NoSyn), (col_def_bind j, col_spec j Zero hrec hrec'))) ls Zeros hrecs hrecs' |>> apsnd split_list o split_list ||> `Local_Theory.close_target; val phi = Proof_Context.export_morphism lthy_old lthy; val col_defs = map (fn def => HOLogic.mk_obj_eq (Morphism.thm phi def)) col_def_frees; val cols = map (fst o Term.dest_Const o Morphism.term phi) col_frees; fun mk_col Ts nat i j T = let val hrecT = HOLogic.mk_tupleT (map (fn U => U --> HOLogic.mk_setT T) Ts) val colT = HOLogic.natT --> hrecT; in mk_nthN n (Term.list_comb (Const (nth cols (j - 1), colT), [nat])) i end; val col_0ss = mk_rec_simps n @{thm rec_nat_0_imp} col_defs; val col_Sucss = mk_rec_simps n @{thm rec_nat_Suc_imp} col_defs; val col_0ss' = transpose col_0ss; val col_Sucss' = transpose col_Sucss; fun mk_set Ts i j T = Abs (Name.uu, nth Ts (i - 1), mk_UNION (HOLogic.mk_UNIV HOLogic.natT) (Term.absfree nat' (mk_col Ts nat i j T $ Bound 1))); val setss = map (fn i => map2 (mk_set Ts i) ls passiveAs) ks; val (Jbnf_consts, lthy) = @{fold_map 8} (fn b => fn map_b => fn rel_b => fn pred_b => fn set_bs => fn mapx => fn sets => fn T => fn lthy => define_bnf_consts Hardly_Inline (user_policy Note_Some lthy) false (SOME deads) map_b rel_b pred_b set_bs (((((((b, T), fold_rev Term.absfree fs' mapx), sets), sbd), [Const (\<^const_name>\undefined\, T)]), NONE), NONE) lthy) bs map_bs rel_bs pred_bs set_bss fs_maps setss Ts lthy; val (_, Jconsts, Jconst_defs, mk_Jconsts) = @{split_list 4} Jbnf_consts; val (_, Jsetss, Jbds_Ds, _, _, _) = @{split_list 6} Jconsts; val (Jmap_defs, Jset_defss, Jbd_defs, _, Jrel_defs, Jpred_defs) = @{split_list 6} Jconst_defs; val (mk_Jmaps_Ds, mk_Jt_Ds, _, mk_Jrels_Ds, mk_Jpreds_Ds, _, _) = @{split_list 7} mk_Jconsts; val Jrel_unabs_defs = map (fn def => mk_unabs_def m (HOLogic.mk_obj_eq def)) Jrel_defs; val Jpred_unabs_defs = map (fn def => mk_unabs_def m (HOLogic.mk_obj_eq def)) Jpred_defs; val Jset_defs = flat Jset_defss; fun mk_Jmaps As Bs = map (fn mk => mk deads As Bs) mk_Jmaps_Ds; fun mk_Jsetss As = map2 (fn mk => fn Jsets => map (mk deads As) Jsets) mk_Jt_Ds Jsetss; val Jbds = map2 (fn mk => mk deads passiveAs) mk_Jt_Ds Jbds_Ds; fun mk_Jrels As Bs = map (fn mk => mk deads As Bs) mk_Jrels_Ds; fun mk_Jpreds As = map (fn mk => mk deads As) mk_Jpreds_Ds; val Jmaps = mk_Jmaps passiveAs passiveBs; val (Jsetss_by_range, Jsetss_by_bnf) = `transpose (mk_Jsetss passiveAs); val timer = time (timer "bnf constants for the new datatypes"); val ((((((((((((((((((((ys, ys'), (nat, nat')), (Jzs, Jzs')), Jz's), Jzs_copy), Jz's_copy), dtor_set_induct_phiss), Jphis), Jpsi1s), Jpsi2s), activeJphis), fs), fs_copy), gs), us), (Jys, Jys')), (Jys_copy, Jys'_copy)), (ys_copy, ys'_copy)), Kss), names_lthy) = lthy |> mk_Frees' "y" passiveAs ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "n") HOLogic.natT ||>> mk_Frees' "z" Ts ||>> mk_Frees "y" Ts' ||>> mk_Frees "z'" Ts ||>> mk_Frees "y'" Ts' ||>> mk_Freess "P" (map (fn A => map (mk_pred2T A) Ts) passiveAs) ||>> mk_Frees "R" JphiTs ||>> mk_Frees "R" Jpsi1Ts ||>> mk_Frees "Q" Jpsi2Ts ||>> mk_Frees "JR" activeJphiTs ||>> mk_Frees "f" fTs ||>> mk_Frees "f" fTs ||>> mk_Frees "g" gTs ||>> mk_Frees "u" uTs ||>> mk_Frees' "b" Ts' ||>> mk_Frees' "b" Ts' ||>> mk_Frees' "y" passiveAs ||>> mk_Freess "K" (map (fn AT => map (fn T => T --> AT) Ts) ATs); val fs_Jmaps = map (fn m => Term.list_comb (m, fs)) Jmaps; val fs_copy_Jmaps = map (fn m => Term.list_comb (m, fs_copy)) Jmaps; val gs_Jmaps = map (fn m => Term.list_comb (m, gs)) (mk_Jmaps passiveBs passiveCs); val fgs_Jmaps = map (fn m => Term.list_comb (m, map2 (curry HOLogic.mk_comp) gs fs)) (mk_Jmaps passiveAs passiveCs); val (dtor_Jmap_thms, Jmap_thms) = let fun mk_goal fs_Jmap map dtor dtor' = mk_Trueprop_eq (HOLogic.mk_comp (dtor', fs_Jmap), HOLogic.mk_comp (Term.list_comb (map, fs @ fs_Jmaps), dtor)); val goals = @{map 4} mk_goal fs_Jmaps map_FTFT's dtors dtor's; val maps = @{map 5} (fn goal => fn unfold => fn map_comp => fn map_cong0 => fn map_arg_cong => Variable.add_free_names lthy goal [] |> (fn vars => Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jmap_defs THEN mk_map_tac ctxt m n map_arg_cong unfold map_comp map_cong0)) |> Thm.close_derivation \<^here>) goals dtor_unfold_thms map_comps map_cong0s map_arg_cong_thms; in map_split (fn thm => (thm RS @{thm comp_eq_dest}, thm)) maps end; val (dtor_Jmap_unique_thms, dtor_Jmap_unique_thm) = let fun mk_prem u map dtor dtor' = mk_Trueprop_eq (HOLogic.mk_comp (dtor', u), HOLogic.mk_comp (Term.list_comb (map, fs @ us), dtor)); val prems = @{map 4} mk_prem us map_FTFT's dtors dtor's; val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 (curry HOLogic.mk_eq) us fs_Jmaps)); val vars = fold (Variable.add_free_names lthy) (goal :: prems) []; in `split_conj_thm (Goal.prove_sorry lthy vars [] (Logic.list_implies (prems, goal)) (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jmap_defs THEN mk_dtor_map_unique_tac ctxt dtor_unfold_unique_thm sym_map_comps) |> Thm.close_derivation \<^here>) end; val Jmap_comp0_thms = let val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (@{map 3} (fn fmap => fn gmap => fn fgmap => HOLogic.mk_eq (HOLogic.mk_comp (gmap, fmap), fgmap)) fs_Jmaps gs_Jmaps fgs_Jmaps)) val vars = Variable.add_free_names lthy goal []; in split_conj_thm (Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => mk_map_comp0_tac ctxt Jmap_thms map_comp0s dtor_Jmap_unique_thm) |> Thm.close_derivation \<^here>) end; val timer = time (timer "map functions for the new codatatypes"); val Jset_minimal_thms = let fun mk_passive_prem set dtor x K = Logic.all x (HOLogic.mk_Trueprop (mk_leq (set $ (dtor $ x)) (K $ x))); fun mk_active_prem dtor x1 K1 set x2 K2 = fold_rev Logic.all [x1, x2] (Logic.mk_implies (mk_Trueprop_mem (x2, set $ (dtor $ x1)), HOLogic.mk_Trueprop (mk_leq (K2 $ x2) (K1 $ x1)))); val premss = map2 (fn j => fn Ks => @{map 4} mk_passive_prem (map (fn xs => nth xs (j - 1)) FTs_setss) dtors Jzs Ks @ flat (@{map 4} (fn sets => fn s => fn x1 => fn K1 => @{map 3} (mk_active_prem s x1 K1) (drop m sets) Jzs_copy Ks) FTs_setss dtors Jzs Ks)) ls Kss; val col_minimal_thms = let fun mk_conjunct j T i K x = mk_leq (mk_col Ts nat i j T $ x) (K $ x); fun mk_concl j T Ks = list_all_free Jzs (Library.foldr1 HOLogic.mk_conj (@{map 3} (mk_conjunct j T) ks Ks Jzs)); val concls = @{map 3} mk_concl ls passiveAs Kss; val goals = map2 (fn prems => fn concl => Logic.list_implies (prems, HOLogic.mk_Trueprop concl)) premss concls val ctss = map (fn phi => map (SOME o Thm.cterm_of lthy) [Term.absfree nat' phi, nat]) concls; in @{map 4} (fn goal => fn cts => fn col_0s => fn col_Sucs => Variable.add_free_names lthy goal [] |> (fn vars => Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => mk_col_minimal_tac ctxt m cts col_0s col_Sucs)) |> Thm.close_derivation \<^here>) goals ctss col_0ss' col_Sucss' end; fun mk_conjunct set K x = mk_leq (set $ x) (K $ x); fun mk_concl sets Ks = Library.foldr1 HOLogic.mk_conj (@{map 3} mk_conjunct sets Ks Jzs); val concls = map2 mk_concl Jsetss_by_range Kss; val goals = map2 (fn prems => fn concl => Logic.list_implies (prems, HOLogic.mk_Trueprop concl)) premss concls; in map2 (fn goal => fn col_minimal => Variable.add_free_names lthy goal [] |> (fn vars => Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jset_defs THEN mk_Jset_minimal_tac ctxt n col_minimal)) |> Thm.close_derivation \<^here>) goals col_minimal_thms end; val (dtor_Jset_incl_thmss, dtor_set_Jset_incl_thmsss) = let fun mk_set_incl_Jset dtor x set Jset = HOLogic.mk_Trueprop (mk_leq (set $ (dtor $ x)) (Jset $ x)); fun mk_set_Jset_incl_Jset dtor x y set Jset1 Jset2 = Logic.mk_implies (mk_Trueprop_mem (x, set $ (dtor $ y)), HOLogic.mk_Trueprop (mk_leq (Jset1 $ x) (Jset2 $ y))); val set_incl_Jset_goalss = @{map 4} (fn dtor => fn x => fn sets => fn Jsets => map2 (mk_set_incl_Jset dtor x) (take m sets) Jsets) dtors Jzs FTs_setss Jsetss_by_bnf; (*x(k) : F(i)set(m+k) (dtor(i) y(i)) ==> J(k)set(j) x(k) <= J(i)set(j) y(i)*) val set_Jset_incl_Jset_goalsss = @{map 4} (fn dtori => fn yi => fn sets => fn Jsetsi => @{map 3} (fn xk => fn set => fn Jsetsk => map2 (mk_set_Jset_incl_Jset dtori xk yi set) Jsetsk Jsetsi) Jzs_copy (drop m sets) Jsetss_by_bnf) dtors Jzs FTs_setss Jsetss_by_bnf; in (map2 (fn goals => fn rec_Sucs => map2 (fn goal => fn rec_Suc => Variable.add_free_names lthy goal [] |> (fn vars => Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jset_defs THEN mk_set_incl_Jset_tac ctxt rec_Suc)) |> Thm.close_derivation \<^here>) goals rec_Sucs) set_incl_Jset_goalss col_Sucss, map2 (fn goalss => fn rec_Sucs => map2 (fn k => fn goals => map2 (fn goal => fn rec_Suc => Variable.add_free_names lthy goal [] |> (fn vars => Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jset_defs THEN mk_set_Jset_incl_Jset_tac ctxt n rec_Suc k)) |> Thm.close_derivation \<^here>) goals rec_Sucs) ks goalss) set_Jset_incl_Jset_goalsss col_Sucss) end; val set_incl_Jset_thmss' = transpose dtor_Jset_incl_thmss; val set_Jset_incl_Jset_thmsss' = transpose (map transpose dtor_set_Jset_incl_thmsss); val set_Jset_thmss = map (map (fn thm => thm RS @{thm set_mp})) dtor_Jset_incl_thmss; val set_Jset_Jset_thmsss = map (map (map (fn thm => thm RS @{thm set_mp}))) dtor_set_Jset_incl_thmsss; val set_Jset_thmss' = transpose set_Jset_thmss; val set_Jset_Jset_thmsss' = transpose (map transpose set_Jset_Jset_thmsss); val dtor_Jset_induct_thms = let val incls = maps (map (fn thm => thm RS @{thm subset_Collect_iff})) dtor_Jset_incl_thmss @ @{thms subset_Collect_iff[OF subset_refl]}; val cTs = map (SOME o Thm.ctyp_of lthy) params'; fun mk_induct_tinst phis jsets y y' = @{map 4} (fn phi => fn jset => fn Jz => fn Jz' => SOME (Thm.cterm_of lthy (Term.absfree Jz' (HOLogic.mk_Collect (fst y', snd y', HOLogic.mk_conj (HOLogic.mk_mem (y, jset $ Jz), phi $ y $ Jz)))))) phis jsets Jzs Jzs'; in @{map 6} (fn set_minimal => fn set_set_inclss => fn jsets => fn y => fn y' => fn phis => ((set_minimal |> Thm.instantiate' cTs (mk_induct_tinst phis jsets y y') |> unfold_thms lthy incls) OF (replicate n ballI @ maps (map (fn thm => thm RS @{thm subset_CollectI})) set_set_inclss)) |> singleton (Proof_Context.export names_lthy lthy) |> rule_by_tactic lthy (ALLGOALS (TRY o etac lthy asm_rl))) Jset_minimal_thms set_Jset_incl_Jset_thmsss' Jsetss_by_range ys ys' dtor_set_induct_phiss end; val (dtor_Jset_thmss', dtor_Jset_thmss) = let fun mk_simp_goal relate pas_set act_sets sets dtor z set = relate (set $ z, mk_union (pas_set $ (dtor $ z), Library.foldl1 mk_union (map2 (fn X => mk_UNION (X $ (dtor $ z))) act_sets sets))); fun mk_goals eq = map2 (fn i => fn sets => @{map 4} (fn Fsets => mk_simp_goal eq (nth Fsets (i - 1)) (drop m Fsets) sets) FTs_setss dtors Jzs sets) ls Jsetss_by_range; val le_goals = map (HOLogic.mk_Trueprop o Library.foldr1 HOLogic.mk_conj) (mk_goals (uncurry mk_leq)); val set_le_thmss = map split_conj_thm (@{map 4} (fn goal => fn Jset_minimal => fn set_Jsets => fn set_Jset_Jsetss => Variable.add_free_names lthy goal [] |> (fn vars => Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => mk_set_le_tac ctxt n Jset_minimal set_Jsets set_Jset_Jsetss)) |> Thm.close_derivation \<^here>) le_goals Jset_minimal_thms set_Jset_thmss' set_Jset_Jset_thmsss'); val ge_goalss = map (map HOLogic.mk_Trueprop) (mk_goals (uncurry mk_leq o swap)); val set_ge_thmss = @{map 3} (@{map 3} (fn goal => fn set_incl_Jset => fn set_Jset_incl_Jsets => Variable.add_free_names lthy goal [] |> (fn vars => Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => mk_set_ge_tac ctxt n set_incl_Jset set_Jset_incl_Jsets)) |> Thm.close_derivation \<^here>)) ge_goalss set_incl_Jset_thmss' set_Jset_incl_Jset_thmsss' in map2 (map2 (fn le => fn ge => equalityI OF [le, ge])) set_le_thmss set_ge_thmss |> `transpose end; val timer = time (timer "set functions for the new codatatypes"); val colss = map2 (fn j => fn T => map (fn i => mk_col Ts nat i j T) ks) ls passiveAs; val colss' = map2 (fn j => fn T => map (fn i => mk_col Ts' nat i j T) ks) ls passiveBs; val col_natural_thmss = let fun mk_col_natural f map z col col' = HOLogic.mk_eq (mk_image f $ (col $ z), col' $ (map $ z)); fun mk_goal f cols cols' = list_all_free Jzs (Library.foldr1 HOLogic.mk_conj (@{map 4} (mk_col_natural f) fs_Jmaps Jzs cols cols')); val goals = @{map 3} mk_goal fs colss colss'; val ctss = map (fn phi => map (SOME o Thm.cterm_of lthy) [Term.absfree nat' phi, nat]) goals; val thms = @{map 4} (fn goal => fn cts => fn rec_0s => fn rec_Sucs => Variable.add_free_names lthy goal [] |> (fn vars => Goal.prove_sorry lthy vars [] (HOLogic.mk_Trueprop goal) (fn {context = ctxt, prems = _} => mk_col_natural_tac ctxt cts rec_0s rec_Sucs dtor_Jmap_thms set_mapss)) |> Thm.close_derivation \<^here>) goals ctss col_0ss' col_Sucss'; in map (split_conj_thm o mk_specN n) thms end; val col_bd_thmss = let fun mk_col_bd z col bd = mk_ordLeq (mk_card_of (col $ z)) bd; fun mk_goal bds cols = list_all_free Jzs (Library.foldr1 HOLogic.mk_conj (@{map 3} mk_col_bd Jzs cols bds)); val goals = map (mk_goal Jbds) colss; val ctss = map (fn phi => map (SOME o Thm.cterm_of lthy) [Term.absfree nat' phi, nat]) (map (mk_goal (replicate n sbd)) colss); val thms = @{map 5} (fn j => fn goal => fn cts => fn rec_0s => fn rec_Sucs => Variable.add_free_names lthy goal [] |> (fn vars => Goal.prove_sorry lthy vars [] (HOLogic.mk_Trueprop goal) (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jbd_defs THEN mk_col_bd_tac ctxt m j cts rec_0s rec_Sucs sbd_Card_order sbd_Cinfinite set_sbdss)) |> Thm.close_derivation \<^here>) ls goals ctss col_0ss' col_Sucss'; in map (split_conj_thm o mk_specN n) thms end; val map_cong0_thms = let val cTs = map (SOME o Thm.ctyp_of lthy o Term.typ_subst_atomic (passiveAs ~~ passiveBs) o TFree) coinduct_params; fun mk_prem z set f g y y' = mk_Ball (set $ z) (Term.absfree y' (HOLogic.mk_eq (f $ y, g $ y))); fun mk_prems sets z = Library.foldr1 HOLogic.mk_conj (@{map 5} (mk_prem z) sets fs fs_copy ys ys') fun mk_map_cong0 sets z fmap gmap = HOLogic.mk_imp (mk_prems sets z, HOLogic.mk_eq (fmap $ z, gmap $ z)); fun mk_coind_body sets (x, T) z fmap gmap y y_copy = HOLogic.mk_conj (HOLogic.mk_mem (z, HOLogic.mk_Collect (x, T, mk_prems sets z)), HOLogic.mk_conj (HOLogic.mk_eq (y, fmap $ z), HOLogic.mk_eq (y_copy, gmap $ z))) fun mk_cphi sets (z' as (x, T)) z fmap gmap y' y y'_copy y_copy = HOLogic.mk_exists (x, T, mk_coind_body sets z' z fmap gmap y y_copy) |> Term.absfree y'_copy |> Term.absfree y' |> Thm.cterm_of lthy; val cphis = @{map 9} mk_cphi Jsetss_by_bnf Jzs' Jzs fs_Jmaps fs_copy_Jmaps Jys' Jys Jys'_copy Jys_copy; val coinduct = Thm.instantiate' cTs (map SOME cphis) dtor_coinduct_thm; val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (@{map 4} mk_map_cong0 Jsetss_by_bnf Jzs fs_Jmaps fs_copy_Jmaps)); val vars = Variable.add_free_names lthy goal []; val thm = Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => mk_mcong_tac ctxt m (rtac ctxt coinduct) map_comps dtor_Jmap_thms map_cong0s set_mapss set_Jset_thmss set_Jset_Jset_thmsss in_rels) |> Thm.close_derivation \<^here>; in split_conj_thm thm end; val in_Jrels = map (fn def => trans OF [def, @{thm OO_Grp_alt}] RS @{thm predicate2_eqD}) Jrel_unabs_defs; val Jrels = mk_Jrels passiveAs passiveBs; val Jpreds = mk_Jpreds passiveAs; val Jrelphis = map (fn rel => Term.list_comb (rel, Jphis)) Jrels; val relphis = map (fn rel => Term.list_comb (rel, Jphis @ Jrelphis)) rels; val Jrelpsi1s = map (fn rel => Term.list_comb (rel, Jpsi1s)) (mk_Jrels passiveAs passiveCs); val Jrelpsi2s = map (fn rel => Term.list_comb (rel, Jpsi2s)) (mk_Jrels passiveCs passiveBs); val Jrelpsi12s = map (fn rel => Term.list_comb (rel, map2 (curry mk_rel_compp) Jpsi1s Jpsi2s)) Jrels; val dtor_Jrel_thms = let fun mk_goal Jz Jz' dtor dtor' Jrelphi relphi = mk_Trueprop_eq (Jrelphi $ Jz $ Jz', relphi $ (dtor $ Jz) $ (dtor' $ Jz')); val goals = @{map 6} mk_goal Jzs Jz's dtors dtor's Jrelphis relphis; in @{map 12} (fn i => fn goal => fn in_rel => fn map_comp0 => fn map_cong0 => fn dtor_map => fn dtor_sets => fn dtor_inject => fn dtor_ctor => fn set_map0s => fn dtor_set_incls => fn dtor_set_set_inclss => Variable.add_free_names lthy goal [] |> (fn vars => Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => mk_dtor_rel_tac ctxt in_Jrels i in_rel map_comp0 map_cong0 dtor_map dtor_sets dtor_inject dtor_ctor set_map0s dtor_set_incls dtor_set_set_inclss)) |> Thm.close_derivation \<^here>) ks goals in_rels map_comps map_cong0s dtor_Jmap_thms dtor_Jset_thmss' dtor_inject_thms dtor_ctor_thms set_mapss dtor_Jset_incl_thmss dtor_set_Jset_incl_thmsss end; val passiveABs = map2 (curry HOLogic.mk_prodT) passiveAs passiveBs; val zip_ranTs = passiveABs @ prodTsTs'; val allJphis = Jphis @ activeJphis; val zipFTs = mk_FTs zip_ranTs; val zipTs = @{map 3} (fn T => fn T' => fn FT => T --> T' --> FT) Ts Ts' zipFTs; val zip_zTs = mk_Ts passiveABs; val (((zips, (abs, abs')), (zip_zs, zip_zs')), _) = names_lthy |> mk_Frees "zip" zipTs ||>> mk_Frees' "ab" passiveABs ||>> mk_Frees' "z" zip_zTs; val Iphi_sets = map2 (fn phi => fn T => HOLogic.Collect_const T $ HOLogic.mk_case_prod phi) allJphis zip_ranTs; val in_phis = map2 (mk_in Iphi_sets) (mk_setss zip_ranTs) zipFTs; val fstABs = map fst_const passiveABs; val all_fsts = fstABs @ fstsTsTs'; val map_all_fsts = map2 (fn Ds => fn bnf => Term.list_comb (mk_map_of_bnf Ds zip_ranTs (passiveAs @ Ts) bnf, all_fsts)) Dss bnfs; val Jmap_fsts = map2 (fn map => fn T => if m = 0 then HOLogic.id_const T else Term.list_comb (map, fstABs)) (mk_Jmaps passiveABs passiveAs) Ts; val sndABs = map snd_const passiveABs; val all_snds = sndABs @ sndsTsTs'; val map_all_snds = map2 (fn Ds => fn bnf => Term.list_comb (mk_map_of_bnf Ds zip_ranTs (passiveBs @ Ts') bnf, all_snds)) Dss bnfs; val Jmap_snds = map2 (fn map => fn T => if m = 0 then HOLogic.id_const T else Term.list_comb (map, sndABs)) (mk_Jmaps passiveABs passiveBs) Ts; val zip_unfolds = map (mk_unfold zip_zTs (map HOLogic.mk_case_prod zips)) ks; val zip_setss = mk_Jsetss passiveABs |> transpose; fun Jrel_coinduct_tac {context = ctxt, prems = CIHs} = let fun mk_helper_prem phi in_phi zip x y map map' dtor dtor' = let val zipxy = zip $ x $ y; in HOLogic.mk_Trueprop (list_all_free [x, y] (HOLogic.mk_imp (phi $ x $ y, HOLogic.mk_conj (HOLogic.mk_mem (zipxy, in_phi), HOLogic.mk_conj (HOLogic.mk_eq (map $ zipxy, dtor $ x), HOLogic.mk_eq (map' $ zipxy, dtor' $ y)))))) end; val helper_prems = @{map 9} mk_helper_prem activeJphis in_phis zips Jzs Jz's map_all_fsts map_all_snds dtors dtor's; fun mk_helper_coind_phi fst phi x alt y map zip_unfold = list_exists_free [if fst then y else x] (HOLogic.mk_conj (phi $ x $ y, HOLogic.mk_eq (alt, map $ (zip_unfold $ HOLogic.mk_prod (x, y))))) val coind1_phis = @{map 6} (mk_helper_coind_phi true) activeJphis Jzs Jzs_copy Jz's Jmap_fsts zip_unfolds; val coind2_phis = @{map 6} (mk_helper_coind_phi false) activeJphis Jzs Jz's_copy Jz's Jmap_snds zip_unfolds; fun mk_cts zs z's phis = @{map 3} (fn z => fn z' => fn phi => SOME (Thm.cterm_of lthy (fold_rev (Term.absfree o Term.dest_Free) [z', z] phi))) zs z's phis @ map (SOME o Thm.cterm_of lthy) (splice z's zs); val cts1 = mk_cts Jzs Jzs_copy coind1_phis; val cts2 = mk_cts Jz's Jz's_copy coind2_phis; fun mk_helper_coind_concl z alt coind_phi = HOLogic.mk_imp (coind_phi, HOLogic.mk_eq (alt, z)); val helper_coind1_concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (@{map 3} mk_helper_coind_concl Jzs Jzs_copy coind1_phis)); val helper_coind2_concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (@{map 3} mk_helper_coind_concl Jz's Jz's_copy coind2_phis)); fun mk_helper_coind_thms fst concl cts = let val vars = fold (Variable.add_free_names lthy) (concl :: helper_prems) []; in Goal.prove_sorry lthy vars [] (Logic.list_implies (helper_prems, concl)) (fn {context = ctxt, prems = _} => mk_rel_coinduct_coind_tac ctxt fst m (infer_instantiate' ctxt cts dtor_coinduct_thm) ks map_comps map_cong0s map_arg_cong_thms set_mapss dtor_unfold_thms dtor_Jmap_thms in_rels) |> Thm.close_derivation \<^here> |> split_conj_thm end; val helper_coind1_thms = mk_helper_coind_thms true helper_coind1_concl cts1; val helper_coind2_thms = mk_helper_coind_thms false helper_coind2_concl cts2; fun mk_helper_ind_phi phi ab fst snd z active_phi x y zip_unfold = list_all_free [x, y] (HOLogic.mk_imp (HOLogic.mk_conj (active_phi $ x $ y, HOLogic.mk_eq (z, zip_unfold $ HOLogic.mk_prod (x, y))), phi $ (fst $ ab) $ (snd $ ab))); val helper_ind_phiss = @{map 4} (fn Jphi => fn ab => fn fst => fn snd => @{map 5} (mk_helper_ind_phi Jphi ab fst snd) zip_zs activeJphis Jzs Jz's zip_unfolds) Jphis abs fstABs sndABs; val ctss = map2 (fn ab' => fn phis => map2 (fn z' => fn phi => SOME (Thm.cterm_of lthy (Term.absfree ab' (Term.absfree z' phi)))) zip_zs' phis @ map (SOME o Thm.cterm_of lthy) zip_zs) abs' helper_ind_phiss; fun mk_helper_ind_concl ab' z ind_phi set = mk_Ball (set $ z) (Term.absfree ab' ind_phi); val mk_helper_ind_concls = @{map 3} (fn ab' => fn ind_phis => fn zip_sets => @{map 3} (mk_helper_ind_concl ab') zip_zs ind_phis zip_sets) abs' helper_ind_phiss zip_setss |> map (HOLogic.mk_Trueprop o Library.foldr1 HOLogic.mk_conj); val helper_ind_thmss = if m = 0 then replicate n [] else @{map 4} (fn concl => fn j => fn set_induct => fn cts => fold (Variable.add_free_names lthy) (concl :: helper_prems) [] |> (fn vars => Goal.prove_sorry lthy vars [] (Logic.list_implies (helper_prems, concl)) (fn {context = ctxt, prems = _} => mk_rel_coinduct_ind_tac ctxt m ks dtor_unfold_thms set_mapss j (infer_instantiate' ctxt cts set_induct))) |> Thm.close_derivation \<^here> |> split_conj_thm) mk_helper_ind_concls ls dtor_Jset_induct_thms ctss |> transpose; in mk_rel_coinduct_tac ctxt CIHs in_rels in_Jrels helper_ind_thmss helper_coind1_thms helper_coind2_thms end; val Jrel_coinduct_thm = mk_xtor_rel_co_induct_thm Greatest_FP rels activeJphis Jrels Jphis Jzs Jz's dtors dtor's Jrel_coinduct_tac lthy; val le_Jrel_OO_thm = let fun mk_le_Jrel_OO Jrelpsi1 Jrelpsi2 Jrelpsi12 = mk_leq (mk_rel_compp (Jrelpsi1, Jrelpsi2)) Jrelpsi12; val goals = @{map 3} mk_le_Jrel_OO Jrelpsi1s Jrelpsi2s Jrelpsi12s; val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj goals); val vars = Variable.add_free_names lthy goal []; in Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => mk_le_rel_OO_tac ctxt Jrel_coinduct_thm dtor_Jrel_thms le_rel_OOs) |> Thm.close_derivation \<^here> end; val timer = time (timer "helpers for BNF properties"); fun close_wit I wit = (I, fold_rev Term.absfree (map (nth ys') I) wit); val all_unitTs = replicate live HOLogic.unitT; val unitTs = replicate n HOLogic.unitT; val unit_funs = replicate n (Term.absdummy HOLogic.unitT HOLogic.unit); fun mk_map_args I = map (fn i => if member (op =) I i then Term.absdummy HOLogic.unitT (nth ys i) else mk_undefined (HOLogic.unitT --> nth passiveAs i)) (0 upto (m - 1)); fun mk_nat_wit Ds bnf (I, wit) () = let val passiveI = filter (fn i => i < m) I; val map_args = mk_map_args passiveI; in Term.absdummy HOLogic.unitT (Term.list_comb (mk_map_of_bnf Ds all_unitTs (passiveAs @ unitTs) bnf, map_args @ unit_funs) $ wit) end; fun mk_dummy_wit Ds bnf I = let val map_args = mk_map_args I; in Term.absdummy HOLogic.unitT (Term.list_comb (mk_map_of_bnf Ds all_unitTs (passiveAs @ unitTs) bnf, map_args @ unit_funs) $ mk_undefined (mk_T_of_bnf Ds all_unitTs bnf)) end; val nat_witss = map2 (fn Ds => fn bnf => mk_wits_of_bnf (replicate (nwits_of_bnf bnf) Ds) (replicate (nwits_of_bnf bnf) (replicate live HOLogic.unitT)) bnf |> map (fn (I, wit) => (I, Lazy.lazy (mk_nat_wit Ds bnf (I, Term.list_comb (wit, map (K HOLogic.unit) I)))))) Dss bnfs; val nat_wit_thmss = map2 (curry op ~~) nat_witss (map wit_thmss_of_bnf bnfs) val Iss = map (map fst) nat_witss; fun filter_wits (I, wit) = let val J = filter (fn i => i < m) I; in (J, (length J < length I, wit)) end; val wit_treess = map_index (fn (i, Is) => map_index (finish Iss m [i+m] (i+m)) Is) Iss |> map (minimize_wits o map filter_wits o minimize_wits o flat); val coind_wit_argsss = map (map (tree_to_coind_wits nat_wit_thmss o snd o snd) o filter (fst o snd)) wit_treess; val nonredundant_coind_wit_argsss = fold (fn i => fn argsss => nth_map (i - 1) (filter_out (fn xs => exists (fn ys => let val xs' = (map (fst o fst) xs, snd (fst (hd xs))); val ys' = (map (fst o fst) ys, snd (fst (hd ys))); in eq_pair (subset (op =)) (eq_set (op =)) (xs', ys') andalso not (fst xs' = fst ys') end) (flat argsss))) argsss) ks coind_wit_argsss; fun prepare_args args = let val I = snd (fst (hd args)); val (dummys, args') = map_split (fn i => (case find_first (fn arg => fst (fst arg) = i - 1) args of SOME (_, ((_, wit), thms)) => (NONE, (Lazy.force wit, thms)) | NONE => (SOME (i - 1), (mk_dummy_wit (nth Dss (i - 1)) (nth bnfs (i - 1)) I, [])))) ks; in ((I, dummys), apsnd flat (split_list args')) end; fun mk_coind_wits ((I, dummys), (args, thms)) = ((I, dummys), (map (fn i => mk_unfold Ts args i $ HOLogic.unit) ks, thms)); val coind_witss = maps (map (mk_coind_wits o prepare_args)) nonredundant_coind_wit_argsss; val witss = map2 (fn Ds => fn bnf => mk_wits_of_bnf (replicate (nwits_of_bnf bnf) Ds) (replicate (nwits_of_bnf bnf) (passiveAs @ Ts)) bnf) Dss bnfs; val ctor_witss = map (map (uncurry close_wit o tree_to_ctor_wit ys ctors witss o snd o snd) o filter_out (fst o snd)) wit_treess; fun mk_coind_wit_thms ((I, dummys), (wits, wit_thms)) = let fun mk_goal sets y y_copy y'_copy j = let fun mk_conjunct set z dummy wit = mk_Ball (set $ z) (Term.absfree y'_copy (if dummy = NONE orelse member (op =) I (j - 1) then HOLogic.mk_imp (HOLogic.mk_eq (z, wit), if member (op =) I (j - 1) then HOLogic.mk_eq (y_copy, y) else \<^term>\False\) else \<^term>\True\)); in HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (@{map 4} mk_conjunct sets Jzs dummys wits)) end; val goals = @{map 5} mk_goal Jsetss_by_range ys ys_copy ys'_copy ls; in map2 (fn goal => fn induct => Variable.add_free_names lthy goal [] |> (fn vars => Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => mk_coind_wit_tac ctxt induct dtor_unfold_thms (flat set_mapss) wit_thms)) |> Thm.close_derivation \<^here>) goals dtor_Jset_induct_thms |> map split_conj_thm |> transpose |> map (map_filter (try (fn thm => thm RS bspec RS mp))) |> curry op ~~ (map_index Library.I (map (close_wit I) wits)) |> filter (fn (_, thms) => length thms = m) end; val coind_wit_thms = maps mk_coind_wit_thms coind_witss; val (wit_thmss, all_witss) = fold (fn ((i, wit), thms) => fn witss => nth_map i (fn (thms', wits) => (thms @ thms', wit :: wits)) witss) coind_wit_thms (map (pair []) ctor_witss) |> map (apsnd (map snd o minimize_wits)) |> split_list; val timer = time (timer "witnesses"); val map_id0_tacs = map2 (fn thm => fn thm' => fn ctxt => mk_map_id0_tac ctxt Jmap_thms thm thm') dtor_unfold_unique_thms unfold_dtor_thms; val map_comp0_tacs = map (fn thm => fn ctxt => rtac ctxt (thm RS sym) 1) Jmap_comp0_thms; val map_cong0_tacs = map (fn thm => fn ctxt => mk_map_cong0_tac ctxt m thm) map_cong0_thms; val set_map0_tacss = map (map (fn col => fn ctxt => unfold_thms_tac ctxt Jset_defs THEN mk_set_map0_tac ctxt col)) (transpose col_natural_thmss); val Jbd_card_orders = map (fn def => Local_Defs.fold lthy [def] sbd_card_order) Jbd_defs; val Jbd_Cinfinites = map (fn def => Local_Defs.fold lthy [def] sbd_Cinfinite) Jbd_defs; val bd_co_tacs = map (fn thm => fn ctxt => rtac ctxt thm 1) Jbd_card_orders; val bd_cinf_tacs = map (fn thm => fn ctxt => rtac ctxt (thm RS conjunct1) 1) Jbd_Cinfinites; val set_bd_tacss = map2 (fn Cinf => map (fn col => fn ctxt => unfold_thms_tac ctxt Jset_defs THEN mk_set_bd_tac ctxt Cinf col)) Jbd_Cinfinites (transpose col_bd_thmss); val le_rel_OO_tacs = map (fn i => fn ctxt => rtac ctxt (le_Jrel_OO_thm RS mk_conjunctN n i) 1) ks; val rel_OO_Grp_tacs = map (fn def => fn ctxt => rtac ctxt def 1) Jrel_unabs_defs; val pred_set_tacs = map (fn def => fn ctxt => rtac ctxt def 1) Jpred_unabs_defs; val tacss = @{map 10} zip_axioms map_id0_tacs map_comp0_tacs map_cong0_tacs set_map0_tacss bd_co_tacs bd_cinf_tacs set_bd_tacss le_rel_OO_tacs rel_OO_Grp_tacs pred_set_tacs; fun wit_tac thms ctxt = mk_wit_tac ctxt n dtor_ctor_thms (flat dtor_Jset_thmss) (maps wit_thms_of_bnf bnfs) thms; val (Jbnfs, lthy) = @{fold_map 7} (fn tacs => fn map_b => fn rel_b => fn pred_b => fn set_bs => fn wit_thms => fn consts => bnf_def Hardly_Inline (user_policy Note_Some) false I tacs (wit_tac wit_thms) (SOME deads) map_b rel_b pred_b set_bs consts) tacss map_bs rel_bs pred_bs set_bss wit_thmss (((((((replicate n Binding.empty ~~ Ts) ~~ Jmaps) ~~ Jsetss_by_bnf) ~~ Jbds) ~~ all_witss) ~~ map SOME Jrels) ~~ map SOME Jpreds) lthy; val timer = time (timer "registered new codatatypes as BNFs"); val ls' = if m = 1 then [0] else ls; val Jbnf_common_notes = map2 (fn i => fn thm => (mk_dtor_set_inductN i, [thm])) ls' dtor_Jset_induct_thms |> map (fn (thmN, thms) => ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])); val Jbnf_notes = [(dtor_mapN, map single dtor_Jmap_thms), (dtor_map_uniqueN, map single dtor_Jmap_unique_thms), (dtor_relN, map single dtor_Jrel_thms), (dtor_set_inclN, dtor_Jset_incl_thmss), (dtor_set_set_inclN, map flat dtor_set_Jset_incl_thmsss)] @ map2 (fn i => fn thms => (mk_dtor_setN i, map single thms)) ls' dtor_Jset_thmss |> maps (fn (thmN, thmss) => map2 (fn b => fn thms => ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])) bs thmss) in (timer, Jbnfs, (Jmap_thms, dtor_Jmap_thms), dtor_Jmap_unique_thm, dtor_Jset_thmss', dtor_Jrel_thms, Jrel_coinduct_thm, Jbnf_common_notes @ Jbnf_notes, dtor_Jset_induct_thms, lthy) end; val ((Jphis, activephis), _) = lthy |> mk_Frees "R" JphiTs ||>> mk_Frees "S" activephiTs; val dtor_unfold_o_Jmap_thms = mk_xtor_co_iter_o_map_thms Greatest_FP false m dtor_unfold_unique_thm dtor_Jmap_o_thms (map (mk_pointfree2 lthy) dtor_unfold_thms) sym_map_comps map_cong0s; val rels = map2 (fn Ds => mk_rel_of_bnf Ds allAs allBs') Dss bnfs; val Jrels = if m = 0 then map HOLogic.eq_const Ts else map (mk_rel_of_bnf deads passiveAs passiveBs) Jbnfs; val dtor_unfold_transfer_thms = mk_xtor_co_iter_transfer_thms Greatest_FP rels activephis activephis Jrels Jphis (mk_unfolds passiveAs activeAs) (mk_unfolds passiveBs activeBs) (fn {context = ctxt, prems = _} => mk_unfold_transfer_tac ctxt m Jrel_coinduct_thm (map map_transfer_of_bnf bnfs) dtor_unfold_thms) lthy; val timer = time (timer "relator coinduction"); fun mk_Ts As = map (typ_subst_atomic (passiveAs ~~ As)) Ts; val export = map (Morphism.term (Local_Theory.target_morphism lthy)) val ((corecs, (dtor_corec_thms, dtor_corec_unique_thm, dtor_corec_o_Jmap_thms, dtor_corec_transfer_thms)), lthy) = lthy |> derive_xtor_co_recs Greatest_FP external_bs mk_Ts (Dss, resDs) bnfs (export dtors) (export unfolds) dtor_unfold_unique_thm dtor_unfold_thms dtor_unfold_transfer_thms dtor_Jmap_thms dtor_Jrel_thms (replicate n NONE); val timer = time (timer "recursor"); val common_notes = [(dtor_coinductN, [dtor_coinduct_thm]), (dtor_rel_coinductN, [Jrel_coinduct_thm])] |> map (fn (thmN, thms) => ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])); val notes = [(ctor_dtorN, ctor_dtor_thms), (ctor_exhaustN, ctor_exhaust_thms), (ctor_injectN, ctor_inject_thms), (dtor_ctorN, dtor_ctor_thms), (dtor_exhaustN, dtor_exhaust_thms), (dtor_injectN, dtor_inject_thms), (dtor_unfoldN, dtor_unfold_thms), (dtor_unfold_o_mapN, dtor_unfold_o_Jmap_thms), (dtor_unfold_transferN, dtor_unfold_transfer_thms), (dtor_unfold_uniqueN, dtor_unfold_unique_thms)] |> map (apsnd (map single)) |> maps (fn (thmN, thmss) => map2 (fn b => fn thms => ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])) bs thmss); val lthy' = lthy |> internals ? snd o Local_Theory.notes (common_notes @ notes @ Jbnf_notes); val fp_res = {Ts = Ts, bnfs = Jbnfs, pre_bnfs = bnfs, absT_infos = absT_infos, ctors = ctors, dtors = dtors, xtor_un_folds = unfolds, xtor_co_recs = export corecs, xtor_co_induct = dtor_coinduct_thm, dtor_ctors = dtor_ctor_thms, ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms, dtor_injects = dtor_inject_thms, xtor_maps = dtor_Jmap_thms, xtor_map_unique = dtor_Jmap_unique_thm, xtor_setss = dtor_Jset_thmss', xtor_rels = dtor_Jrel_thms, xtor_un_fold_thms = dtor_unfold_thms, xtor_co_rec_thms = dtor_corec_thms, xtor_un_fold_unique = dtor_unfold_unique_thm, xtor_co_rec_unique = dtor_corec_unique_thm, xtor_un_fold_o_maps = dtor_unfold_o_Jmap_thms, xtor_co_rec_o_maps = dtor_corec_o_Jmap_thms, xtor_un_fold_transfers = dtor_unfold_transfer_thms, xtor_co_rec_transfers = dtor_corec_transfer_thms, xtor_rel_co_induct = Jrel_coinduct_thm, dtor_set_inducts = dtor_Jset_induct_thms}; in timer; (fp_res, lthy') end; val _ = Outer_Syntax.local_theory \<^command_keyword>\codatatype\ "define coinductive datatypes" (parse_co_datatype_cmd Greatest_FP construct_gfp); -val _ = Theory.setup (fp_antiquote_setup \<^binding>\codatatype\); - end; diff --git a/src/HOL/Tools/BNF/bnf_lfp.ML b/src/HOL/Tools/BNF/bnf_lfp.ML --- a/src/HOL/Tools/BNF/bnf_lfp.ML +++ b/src/HOL/Tools/BNF/bnf_lfp.ML @@ -1,1875 +1,1873 @@ (* Title: HOL/Tools/BNF/bnf_lfp.ML Author: Dmitriy Traytel, TU Muenchen Author: Andrei Popescu, TU Muenchen Copyright 2012 Datatype construction. *) signature BNF_LFP = sig val construct_lfp: mixfix list -> binding list -> binding list -> binding list -> binding list list -> binding list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list -> BNF_Comp.absT_info list -> local_theory -> BNF_FP_Util.fp_result * local_theory end; structure BNF_LFP : BNF_LFP = struct open BNF_Def open BNF_Util open BNF_Tactics open BNF_Comp open BNF_FP_Util open BNF_FP_Def_Sugar open BNF_LFP_Util open BNF_LFP_Tactics (*all BNFs have the same lives*) fun construct_lfp mixfixes map_bs rel_bs pred_bs set_bss0 bs resBs (resDs, Dss) bnfs absT_infos lthy = let val time = time lthy; val timer = time (Timer.startRealTimer ()); val live = live_of_bnf (hd bnfs); val n = length bnfs; (*active*) val ks = 1 upto n; val m = live - n; (*passive, if 0 don't generate a new BNF*) val internals = Config.get lthy bnf_internals; val b_names = map Binding.name_of bs; val b_name = mk_common_name b_names; val b = Binding.name b_name; fun mk_internal_of_b name = Binding.prefix_name (name ^ "_") #> Binding.prefix true b_name #> Binding.concealed; fun mk_internal_b name = mk_internal_of_b name b; fun mk_internal_bs name = map (mk_internal_of_b name) bs; val external_bs = map2 (Binding.prefix false) b_names bs |> not internals ? map Binding.concealed; val deads = fold (union (op =)) Dss resDs; val names_lthy = fold Variable.declare_typ deads lthy; val passives = map fst (subtract (op = o apsnd TFree) deads resBs); (* tvars *) val (((((passiveAs, activeAs), passiveBs), activeBs), passiveCs), activeCs) = names_lthy |> variant_tfrees passives ||>> mk_TFrees n ||>> variant_tfrees passives ||>> mk_TFrees n ||>> variant_tfrees passives ||>> mk_TFrees n |> fst; val allAs = passiveAs @ activeAs; val allBs' = passiveBs @ activeBs; val Ass = replicate n allAs; val allBs = passiveAs @ activeBs; val Bss = replicate n allBs; val allCs = passiveAs @ activeCs; val allCs' = passiveBs @ activeCs; val Css' = replicate n allCs'; (* types *) val dead_poss = map (fn x => if member (op =) deads (TFree x) then SOME (TFree x) else NONE) resBs; fun mk_param NONE passive = (hd passive, tl passive) | mk_param (SOME a) passive = (a, passive); val mk_params = fold_map mk_param dead_poss #> fst; fun mk_FTs Ts = map2 (fn Ds => mk_T_of_bnf Ds Ts) Dss bnfs; val (params, params') = `(map Term.dest_TFree) (mk_params passiveAs); val FTsAs = mk_FTs allAs; val FTsBs = mk_FTs allBs; val FTsCs = mk_FTs allCs; val BTs = map HOLogic.mk_setT activeAs; val B'Ts = map HOLogic.mk_setT activeBs; val B''Ts = map HOLogic.mk_setT activeCs; val sTs = map2 (curry op -->) FTsAs activeAs; val s'Ts = map2 (curry op -->) FTsBs activeBs; val s''Ts = map2 (curry op -->) FTsCs activeCs; val fTs = map2 (curry op -->) activeAs activeBs; val inv_fTs = map2 (curry op -->) activeBs activeAs; val self_fTs = map2 (curry op -->) activeAs activeAs; val gTs = map2 (curry op -->) activeBs activeCs; val all_gTs = map2 (curry op -->) allBs allCs'; (* terms *) val mapsAsAs = @{map 4} mk_map_of_bnf Dss Ass Ass bnfs; val mapsAsBs = @{map 4} mk_map_of_bnf Dss Ass Bss bnfs; val mapsBsCs' = @{map 4} mk_map_of_bnf Dss Bss Css' bnfs; val mapsAsCs' = @{map 4} mk_map_of_bnf Dss Ass Css' bnfs; fun mk_setss Ts = @{map 3} mk_sets_of_bnf (map (replicate live) Dss) (map (replicate live) (replicate n Ts)) bnfs; val setssAs = mk_setss allAs; val bd0s = @{map 3} mk_bd_of_bnf Dss Ass bnfs; val bds = @{map 3} (fn bd0 => fn Ds => fn bnf => mk_csum bd0 (mk_card_of (HOLogic.mk_UNIV (mk_T_of_bnf Ds (replicate live (fst (dest_relT (fastype_of bd0)))) bnf)))) bd0s Dss bnfs; val witss = map wits_of_bnf bnfs; val ((((((((zs, zs'), Bs), ss), fs), self_fs), all_gs), (xFs, xFs')), _) = lthy |> mk_Frees' "z" activeAs ||>> mk_Frees "B" BTs ||>> mk_Frees "s" sTs ||>> mk_Frees "f" fTs ||>> mk_Frees "f" self_fTs ||>> mk_Frees "g" all_gTs ||>> mk_Frees' "x" FTsAs; val passive_UNIVs = map HOLogic.mk_UNIV passiveAs; val active_UNIVs = map HOLogic.mk_UNIV activeAs; val passive_ids = map HOLogic.id_const passiveAs; val active_ids = map HOLogic.id_const activeAs; (* thms *) val bd0_card_orders = map bd_card_order_of_bnf bnfs; val bd0_Card_orders = map bd_Card_order_of_bnf bnfs; val bd0_Cinfinites = map bd_Cinfinite_of_bnf bnfs; val set_bd0ss = map set_bd_of_bnf bnfs; val bd_Card_order = @{thm Card_order_csum}; val bd_Card_orders = replicate n bd_Card_order; val bd_Cinfinites = map (fn thm => thm RS @{thm Cinfinite_csum1}) bd0_Cinfinites; val bd_Cnotzeros = map (fn thm => thm RS @{thm Cinfinite_Cnotzero}) bd_Cinfinites; val bd_Cinfinite = hd bd_Cinfinites; val set_bdss = map2 (fn set_bd0s => fn bd0_Card_order => map (fn thm => ctrans OF [thm, bd0_Card_order RS @{thm ordLeq_csum1}]) set_bd0s) set_bd0ss bd0_Card_orders; val in_bds = map in_bd_of_bnf bnfs; val sym_map_comps = map (fn bnf => map_comp0_of_bnf bnf RS sym) bnfs; val map_comps = map map_comp_of_bnf bnfs; val map_cong0s = map map_cong0_of_bnf bnfs; val map_id0s = map map_id0_of_bnf bnfs; val map_ids = map map_id_of_bnf bnfs; val set_mapss = map set_map_of_bnf bnfs; val rel_mono_strong0s = map rel_mono_strong0_of_bnf bnfs; val le_rel_OOs = map le_rel_OO_of_bnf bnfs; val timer = time (timer "Extracted terms & thms"); (* nonemptiness check *) fun new_wit X (wit: nonemptiness_witness) = subset (op =) (#I wit, (0 upto m - 1) @ map snd X); val all = m upto m + n - 1; fun enrich X = map_filter (fn i => (case find_first (fn (_, i') => i = i') X of NONE => (case find_index (new_wit X) (nth witss (i - m)) of ~1 => NONE | j => SOME (j, i)) | SOME ji => SOME ji)) all; val reachable = fixpoint (op =) enrich []; val _ = (case subtract (op =) (map snd reachable) all of [] => () | i :: _ => raise EMPTY_DATATYPE (Binding.name_of (nth bs (i - m)))); val wit_thms = flat (map2 (fn bnf => fn (j, _) => nth (wit_thmss_of_bnf bnf) j) bnfs reachable); val timer = time (timer "Checked nonemptiness"); (* derived thms *) (*map g1 ... gm g(m+1) ... g(m+n) (map id ... id f(m+1) ... f(m+n) x) = map g1 ... gm (g(m+1) o f(m+1)) ... (g(m+n) o f(m+n)) x*) fun mk_map_comp_id x mapAsBs mapBsCs mapAsCs map_comp0 = let val lhs = Term.list_comb (mapBsCs, all_gs) $ (Term.list_comb (mapAsBs, passive_ids @ fs) $ x); val rhs = Term.list_comb (mapAsCs, take m all_gs @ map HOLogic.mk_comp (drop m all_gs ~~ fs)) $ x; val vars = fold (Variable.add_free_names lthy) [lhs, rhs] []; in Goal.prove_sorry lthy vars [] (mk_Trueprop_eq (lhs, rhs)) (fn {context = ctxt, prems = _} => mk_map_comp_id_tac ctxt map_comp0) |> Thm.close_derivation \<^here> end; val map_comp_id_thms = @{map 5} mk_map_comp_id xFs mapsAsBs mapsBsCs' mapsAsCs' map_comps; (*forall a : set(m+1) x. f(m+1) a = a; ...; forall a : set(m+n) x. f(m+n) a = a ==> map id ... id f(m+1) ... f(m+n) x = x*) fun mk_map_cong0L x mapAsAs sets map_cong0 map_id = let fun mk_prem set f z z' = HOLogic.mk_Trueprop (mk_Ball (set $ x) (Term.absfree z' (HOLogic.mk_eq (f $ z, z)))); val prems = @{map 4} mk_prem (drop m sets) self_fs zs zs'; val goal = mk_Trueprop_eq (Term.list_comb (mapAsAs, passive_ids @ self_fs) $ x, x); val vars = fold (Variable.add_free_names lthy) (goal :: prems) []; in Goal.prove_sorry lthy vars [] (Logic.list_implies (prems, goal)) (fn {context = ctxt, prems = _} => mk_map_cong0L_tac ctxt m map_cong0 map_id) |> Thm.close_derivation \<^here> end; val map_cong0L_thms = @{map 5} mk_map_cong0L xFs mapsAsAs setssAs map_cong0s map_ids; val in_mono'_thms = map (fn bnf => in_mono_of_bnf bnf OF (replicate m subset_refl)) bnfs; val in_cong'_thms = map (fn bnf => in_cong_of_bnf bnf OF (replicate m refl)) bnfs; val timer = time (timer "Derived simple theorems"); (* algebra *) val alg_bind = mk_internal_b algN; val alg_def_bind = (Thm.def_binding alg_bind, []); (*forall i = 1 ... n: (\x \ Fi_in UNIV .. UNIV B1 ... Bn. si x \ Bi)*) val alg_spec = let val ins = @{map 3} mk_in (replicate n (passive_UNIVs @ Bs)) setssAs FTsAs; fun mk_alg_conjunct B s X x x' = mk_Ball X (Term.absfree x' (HOLogic.mk_mem (s $ x, B))); val rhs = Library.foldr1 HOLogic.mk_conj (@{map 5} mk_alg_conjunct Bs ss ins xFs xFs') in fold_rev (Term.absfree o Term.dest_Free) (Bs @ ss) rhs end; val ((alg_free, (_, alg_def_free)), (lthy, lthy_old)) = lthy |> Local_Theory.open_target |> snd |> Local_Theory.define ((alg_bind, NoSyn), (alg_def_bind, alg_spec)) ||> `Local_Theory.close_target; val phi = Proof_Context.export_morphism lthy_old lthy; val alg = fst (Term.dest_Const (Morphism.term phi alg_free)); val alg_def = mk_unabs_def (2 * n) (HOLogic.mk_obj_eq (Morphism.thm phi alg_def_free)); fun mk_alg Bs ss = let val args = Bs @ ss; val Ts = map fastype_of args; val algT = Library.foldr (op -->) (Ts, HOLogic.boolT); in Term.list_comb (Const (alg, algT), args) end; val ((((((((zs, zs'), Bs), B's), ss), s's), fs), (xFs, xFs')), _) = lthy |> mk_Frees' "z" activeAs ||>> mk_Frees "B" BTs ||>> mk_Frees "B'" B'Ts ||>> mk_Frees "s" sTs ||>> mk_Frees "s'" s'Ts ||>> mk_Frees "f" fTs ||>> mk_Frees' "x" FTsAs; val alg_set_thms = let val alg_prem = HOLogic.mk_Trueprop (mk_alg Bs ss); fun mk_prem x set B = HOLogic.mk_Trueprop (mk_leq (set $ x) B); fun mk_concl s x B = mk_Trueprop_mem (s $ x, B); val premss = map2 ((fn x => fn sets => map2 (mk_prem x) (drop m sets) Bs)) xFs setssAs; val concls = @{map 3} mk_concl ss xFs Bs; val goals = map2 (fn prems => fn concl => Logic.list_implies (alg_prem :: prems, concl)) premss concls; in map (fn goal => Variable.add_free_names lthy goal [] |> (fn vars => Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => mk_alg_set_tac ctxt alg_def)) |> Thm.close_derivation \<^here>) goals end; val timer = time (timer "Algebra definition & thms"); val alg_not_empty_thms = let val alg_prem = HOLogic.mk_Trueprop (mk_alg Bs ss); val concls = map (HOLogic.mk_Trueprop o mk_not_empty) Bs; val goals = map (fn concl => Logic.mk_implies (alg_prem, concl)) concls; in map2 (fn goal => fn alg_set => Variable.add_free_names lthy goal [] |> (fn vars => Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => mk_alg_not_empty_tac ctxt alg_set alg_set_thms wit_thms)) |> Thm.close_derivation \<^here>) goals alg_set_thms end; val timer = time (timer "Proved nonemptiness"); (* morphism *) val mor_bind = mk_internal_b morN; val mor_def_bind = (Thm.def_binding mor_bind, []); (*fbetw) forall i = 1 ... n: (\x \ Bi. f x \ B'i)*) (*mor) forall i = 1 ... n: (\x \ Fi_in UNIV ... UNIV B1 ... Bn. f (s1 x) = s1' (Fi_map id ... id f1 ... fn x))*) val mor_spec = let fun mk_fbetw f B1 B2 z z' = mk_Ball B1 (Term.absfree z' (HOLogic.mk_mem (f $ z, B2))); fun mk_mor sets mapAsBs f s s' T x x' = mk_Ball (mk_in (passive_UNIVs @ Bs) sets T) (Term.absfree x' (HOLogic.mk_eq (f $ (s $ x), s' $ (Term.list_comb (mapAsBs, passive_ids @ fs) $ x)))); val rhs = HOLogic.mk_conj (Library.foldr1 HOLogic.mk_conj (@{map 5} mk_fbetw fs Bs B's zs zs'), Library.foldr1 HOLogic.mk_conj (@{map 8} mk_mor setssAs mapsAsBs fs ss s's FTsAs xFs xFs')) in fold_rev (Term.absfree o Term.dest_Free) (Bs @ ss @ B's @ s's @ fs) rhs end; val ((mor_free, (_, mor_def_free)), (lthy, lthy_old)) = lthy |> Local_Theory.open_target |> snd |> Local_Theory.define ((mor_bind, NoSyn), (mor_def_bind, mor_spec)) ||> `Local_Theory.close_target; val phi = Proof_Context.export_morphism lthy_old lthy; val mor = fst (Term.dest_Const (Morphism.term phi mor_free)); val mor_def = mk_unabs_def (5 * n) (HOLogic.mk_obj_eq (Morphism.thm phi mor_def_free)); fun mk_mor Bs1 ss1 Bs2 ss2 fs = let val args = Bs1 @ ss1 @ Bs2 @ ss2 @ fs; val Ts = map fastype_of (Bs1 @ ss1 @ Bs2 @ ss2 @ fs); val morT = Library.foldr (op -->) (Ts, HOLogic.boolT); in Term.list_comb (Const (mor, morT), args) end; val (((((((((((Bs, Bs_copy), B's), B''s), ss), s's), s''s), fs), fs_copy), gs), xFs), _) = lthy |> mk_Frees "B" BTs ||>> mk_Frees "B" BTs ||>> mk_Frees "B'" B'Ts ||>> mk_Frees "B''" B''Ts ||>> mk_Frees "s" sTs ||>> mk_Frees "s'" s'Ts ||>> mk_Frees "s''" s''Ts ||>> mk_Frees "f" fTs ||>> mk_Frees "f" fTs ||>> mk_Frees "g" gTs ||>> mk_Frees "x" FTsAs; val morE_thms = let val prem = HOLogic.mk_Trueprop (mk_mor Bs ss B's s's fs); fun mk_elim_prem sets x T = HOLogic.mk_Trueprop (HOLogic.mk_mem (x, mk_in (passive_UNIVs @ Bs) sets T)); fun mk_elim_goal sets mapAsBs f s s' x T = Logic.list_implies ([prem, mk_elim_prem sets x T], mk_Trueprop_eq (f $ (s $ x), s' $ Term.list_comb (mapAsBs, passive_ids @ fs @ [x]))); val elim_goals = @{map 7} mk_elim_goal setssAs mapsAsBs fs ss s's xFs FTsAs; fun prove goal = Variable.add_free_names lthy goal [] |> (fn vars => Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => mk_mor_elim_tac ctxt mor_def)) |> Thm.close_derivation \<^here>; in map prove elim_goals end; val mor_incl_thm = let val prems = map2 (HOLogic.mk_Trueprop oo mk_leq) Bs Bs_copy; val concl = HOLogic.mk_Trueprop (mk_mor Bs ss Bs_copy ss active_ids); val vars = fold (Variable.add_free_names lthy) (concl :: prems) []; in Goal.prove_sorry lthy vars [] (Logic.list_implies (prems, concl)) (fn {context = ctxt, prems = _} => mk_mor_incl_tac ctxt mor_def map_ids) |> Thm.close_derivation \<^here> end; val mor_comp_thm = let val prems = [HOLogic.mk_Trueprop (mk_mor Bs ss B's s's fs), HOLogic.mk_Trueprop (mk_mor B's s's B''s s''s gs)]; val concl = HOLogic.mk_Trueprop (mk_mor Bs ss B''s s''s (map2 (curry HOLogic.mk_comp) gs fs)); val vars = fold (Variable.add_free_names lthy) (concl :: prems) []; in Goal.prove_sorry lthy vars [] (Logic.list_implies (prems, concl)) (fn {context = ctxt, prems = _} => mk_mor_comp_tac ctxt mor_def set_mapss map_comp_id_thms) |> Thm.close_derivation \<^here> end; val mor_cong_thm = let val prems = map HOLogic.mk_Trueprop (map2 (curry HOLogic.mk_eq) fs_copy fs @ [mk_mor Bs ss B's s's fs]) val concl = HOLogic.mk_Trueprop (mk_mor Bs ss B's s's fs_copy); val vars = fold (Variable.add_free_names lthy) (concl :: prems) []; in Goal.prove_sorry lthy vars [] (Logic.list_implies (prems, concl)) (fn {context = ctxt, prems = _} => (hyp_subst_tac ctxt THEN' assume_tac ctxt) 1) |> Thm.close_derivation \<^here> end; val mor_str_thm = let val maps = map2 (fn Ds => fn bnf => Term.list_comb (mk_map_of_bnf Ds (passiveAs @ FTsAs) allAs bnf, passive_ids @ ss)) Dss bnfs; val goal = HOLogic.mk_Trueprop (mk_mor (map HOLogic.mk_UNIV FTsAs) maps active_UNIVs ss ss); val vars = Variable.add_free_names lthy goal []; in Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => mk_mor_str_tac ctxt ks mor_def) |> Thm.close_derivation \<^here> end; val mor_UNIV_thm = let fun mk_conjunct mapAsBs f s s' = HOLogic.mk_eq (HOLogic.mk_comp (f, s), HOLogic.mk_comp (s', Term.list_comb (mapAsBs, passive_ids @ fs))); val lhs = mk_mor active_UNIVs ss (map HOLogic.mk_UNIV activeBs) s's fs; val rhs = Library.foldr1 HOLogic.mk_conj (@{map 4} mk_conjunct mapsAsBs fs ss s's); val vars = fold (Variable.add_free_names lthy) [lhs, rhs] []; in Goal.prove_sorry lthy vars [] (mk_Trueprop_eq (lhs, rhs)) (fn {context = ctxt, prems = _} => mk_mor_UNIV_tac ctxt m morE_thms mor_def) |> Thm.close_derivation \<^here> end; val timer = time (timer "Morphism definition & thms"); (* bounds *) val sum_bd = Library.foldr1 (uncurry mk_csum) bds; val sum_bdT = fst (dest_relT (fastype_of sum_bd)); val (sum_bdT_params, sum_bdT_params') = `(map TFree) (Term.add_tfreesT sum_bdT []); val (lthy, sbd, sbd_Cinfinite, sbd_Card_order, set_sbdss, in_sbds) = if n = 1 then (lthy, sum_bd, bd_Cinfinite, bd_Card_order, set_bdss, in_bds) else let val sbdT_bind = mk_internal_b sum_bdTN; val ((sbdT_name, (sbdT_glob_info, sbdT_loc_info)), lthy) = typedef (sbdT_bind, sum_bdT_params', NoSyn) (HOLogic.mk_UNIV sum_bdT) NONE (fn ctxt => EVERY' [rtac ctxt exI, rtac ctxt UNIV_I] 1) lthy; val sbdT = Type (sbdT_name, sum_bdT_params); val Abs_sbdT = Const (#Abs_name sbdT_glob_info, sum_bdT --> sbdT); val sbd_bind = mk_internal_b sum_bdN; val sbd_def_bind = (Thm.def_binding sbd_bind, []); val sbd_spec = mk_dir_image sum_bd Abs_sbdT; val ((sbd_free, (_, sbd_def_free)), (lthy, lthy_old)) = lthy |> Local_Theory.open_target |> snd |> Local_Theory.define ((sbd_bind, NoSyn), (sbd_def_bind, sbd_spec)) ||> `Local_Theory.close_target; val phi = Proof_Context.export_morphism lthy_old lthy; val sbd_def = HOLogic.mk_obj_eq (Morphism.thm phi sbd_def_free); val sbd = Const (fst (Term.dest_Const (Morphism.term phi sbd_free)), mk_relT (`I sbdT)); val Abs_sbdT_inj = mk_Abs_inj_thm (#Abs_inject sbdT_loc_info); val sum_Cinfinite = mk_sum_Cinfinite bd_Cinfinites; val sum_Card_order = sum_Cinfinite RS conjunct2; val sbd_ordIso = @{thm ssubst_Pair_rhs} OF [@{thm dir_image} OF [Abs_sbdT_inj, sum_Card_order], sbd_def]; val sbd_Cinfinite = @{thm Cinfinite_cong} OF [sbd_ordIso, sum_Cinfinite]; val sbd_Card_order = sbd_Cinfinite RS conjunct2; fun mk_set_sbd i bd_Card_order bds = map (fn thm => @{thm ordLeq_ordIso_trans} OF [bd_Card_order RS mk_ordLeq_csum n i thm, sbd_ordIso]) bds; val set_sbdss = @{map 3} mk_set_sbd ks bd_Card_orders set_bdss; fun mk_in_bd_sum i Co Cnz bd = Cnz RS ((@{thm ordLeq_ordIso_trans} OF [Co RS mk_ordLeq_csum n i (Co RS @{thm ordLeq_refl}), sbd_ordIso]) RS (bd RS @{thm ordLeq_transitive[OF _ cexp_mono2_Cnotzero[OF _ Card_order_csum]]})); val in_sbds = @{map 4} mk_in_bd_sum ks bd_Card_orders bd_Cnotzeros in_bds; in (lthy, sbd, sbd_Cinfinite, sbd_Card_order, set_sbdss, in_sbds) end; val sbd_Cnotzero = sbd_Cinfinite RS @{thm Cinfinite_Cnotzero}; val suc_bd = mk_cardSuc sbd; val field_suc_bd = mk_Field suc_bd; val suc_bdT = fst (dest_relT (fastype_of suc_bd)); fun mk_Asuc_bd [] = mk_cexp ctwo suc_bd | mk_Asuc_bd As = mk_cexp (mk_csum (Library.foldr1 (uncurry mk_csum) (map mk_card_of As)) ctwo) suc_bd; val suc_bd_Card_order = sbd_Card_order RS @{thm cardSuc_Card_order}; val suc_bd_Cinfinite = sbd_Cinfinite RS @{thm Cinfinite_cardSuc}; val suc_bd_Cnotzero = suc_bd_Cinfinite RS @{thm Cinfinite_Cnotzero}; val suc_bd_worel = suc_bd_Card_order RS @{thm Card_order_wo_rel} val basis_Asuc = if m = 0 then @{thm ordLeq_refl[OF Card_order_ctwo]} else @{thm ordLeq_csum2[OF Card_order_ctwo]}; val Asuc_bd_Cinfinite = suc_bd_Cinfinite RS (basis_Asuc RS @{thm Cinfinite_cexp}); val suc_bd_Asuc_bd = @{thm ordLess_ordLeq_trans[OF ordLess_ctwo_cexp cexp_mono1]} OF [suc_bd_Card_order, basis_Asuc, suc_bd_Card_order]; val Asuc_bd = mk_Asuc_bd passive_UNIVs; val Asuc_bdT = fst (dest_relT (fastype_of Asuc_bd)); val II_BTs = replicate n (HOLogic.mk_setT Asuc_bdT); val II_sTs = map2 (fn Ds => fn bnf => mk_T_of_bnf Ds (passiveAs @ replicate n Asuc_bdT) bnf --> Asuc_bdT) Dss bnfs; val ((((((Bs, ss), idxs), Asi_name), (idx, idx')), (jdx, jdx')), _) = lthy |> mk_Frees "B" BTs ||>> mk_Frees "s" sTs ||>> mk_Frees "i" (replicate n suc_bdT) ||>> (fn ctxt => apfst the_single (mk_fresh_names ctxt 1 "Asi")) ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "i") suc_bdT ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "j") suc_bdT; val suc_bd_limit_thm = let val prem = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map (fn idx => HOLogic.mk_mem (idx, field_suc_bd)) idxs)); fun mk_conjunct idx = HOLogic.mk_conj (mk_not_eq idx jdx, HOLogic.mk_mem (HOLogic.mk_prod (idx, jdx), suc_bd)); val concl = HOLogic.mk_Trueprop (mk_Bex field_suc_bd (Term.absfree jdx' (Library.foldr1 HOLogic.mk_conj (map mk_conjunct idxs)))); val vars = fold (Variable.add_free_names lthy) [prem, concl] []; in Goal.prove_sorry lthy vars [] (Logic.list_implies ([prem], concl)) (fn {context = ctxt, prems = _} => mk_bd_limit_tac ctxt n suc_bd_Cinfinite) |> Thm.close_derivation \<^here> end; val timer = time (timer "Bounds"); (* minimal algebra *) fun mk_minG Asi i k = mk_UNION (mk_underS suc_bd $ i) (Term.absfree jdx' (mk_nthN n (Asi $ jdx) k)); fun mk_minH_component Asi i sets Ts s k = HOLogic.mk_binop \<^const_name>\sup\ (mk_minG Asi i k, mk_image s $ mk_in (passive_UNIVs @ map (mk_minG Asi i) ks) sets Ts); fun mk_min_algs ss = let val BTs = map (range_type o fastype_of) ss; val Ts = passiveAs @ BTs; val (Asi, Asi') = `Free (Asi_name, suc_bdT --> Library.foldr1 HOLogic.mk_prodT (map HOLogic.mk_setT BTs)); in mk_worec suc_bd (Term.absfree Asi' (Term.absfree idx' (HOLogic.mk_tuple (@{map 4} (mk_minH_component Asi idx) (mk_setss Ts) (mk_FTs Ts) ss ks)))) end; val (min_algs_thms, min_algs_mono_thms, card_of_min_algs_thm, least_min_algs_thm) = let val i_field = HOLogic.mk_mem (idx, field_suc_bd); val min_algs = mk_min_algs ss; val min_algss = map (fn k => mk_nthN n (min_algs $ idx) k) ks; val concl = HOLogic.mk_Trueprop (HOLogic.mk_eq (min_algs $ idx, HOLogic.mk_tuple (@{map 4} (mk_minH_component min_algs idx) setssAs FTsAs ss ks))); val goal = Logic.mk_implies (HOLogic.mk_Trueprop i_field, concl); val vars = Variable.add_free_names lthy goal []; val min_algs_thm = Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => mk_min_algs_tac ctxt suc_bd_worel in_cong'_thms) |> Thm.close_derivation \<^here>; val min_algs_thms = map (fn k => min_algs_thm RS mk_nthI n k) ks; fun mk_mono_goal min_alg = HOLogic.mk_Trueprop (mk_relChain suc_bd (Term.absfree idx' min_alg)); val monos = map2 (fn goal => fn min_algs => Variable.add_free_names lthy goal [] |> (fn vars => Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => mk_min_algs_mono_tac ctxt min_algs)) |> Thm.close_derivation \<^here>) (map mk_mono_goal min_algss) min_algs_thms; fun mk_card_conjunct min_alg = mk_ordLeq (mk_card_of min_alg) Asuc_bd; val card_conjunction = Library.foldr1 HOLogic.mk_conj (map mk_card_conjunct min_algss); val card_cT = Thm.ctyp_of lthy suc_bdT; val card_ct = Thm.cterm_of lthy (Term.absfree idx' card_conjunction); val card_of = let val goal = HOLogic.mk_Trueprop (HOLogic.mk_imp (i_field, card_conjunction)); val vars = Variable.add_free_names lthy goal []; in Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => mk_min_algs_card_of_tac ctxt card_cT card_ct m suc_bd_worel min_algs_thms in_sbds sbd_Card_order sbd_Cnotzero suc_bd_Card_order suc_bd_Cinfinite suc_bd_Cnotzero suc_bd_Asuc_bd Asuc_bd_Cinfinite) |> Thm.close_derivation \<^here> end; val least_prem = HOLogic.mk_Trueprop (mk_alg Bs ss); val least_conjunction = Library.foldr1 HOLogic.mk_conj (map2 mk_leq min_algss Bs); val least_cT = Thm.ctyp_of lthy suc_bdT; val least_ct = Thm.cterm_of lthy (Term.absfree idx' least_conjunction); val least = let val goal = Logic.mk_implies (least_prem, HOLogic.mk_Trueprop (HOLogic.mk_imp (i_field, least_conjunction))); val vars = Variable.add_free_names lthy goal []; in Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => mk_min_algs_least_tac ctxt least_cT least_ct suc_bd_worel min_algs_thms alg_set_thms) |> Thm.close_derivation \<^here> end; in (min_algs_thms, monos, card_of, least) end; val timer = time (timer "min_algs definition & thms"); val min_alg_binds = mk_internal_bs min_algN; fun min_alg_bind i = nth min_alg_binds (i - 1); val min_alg_def_bind = rpair [] o Thm.def_binding o min_alg_bind; fun min_alg_spec i = let val rhs = mk_UNION (field_suc_bd) (Term.absfree idx' (mk_nthN n (mk_min_algs ss $ idx) i)); in fold_rev (Term.absfree o Term.dest_Free) ss rhs end; val ((min_alg_frees, (_, min_alg_def_frees)), (lthy, lthy_old)) = lthy |> Local_Theory.open_target |> snd |> fold_map (fn i => Local_Theory.define ((min_alg_bind i, NoSyn), (min_alg_def_bind i, min_alg_spec i))) ks |>> apsnd split_list o split_list ||> `Local_Theory.close_target; val phi = Proof_Context.export_morphism lthy_old lthy; val min_algs = map (fst o Term.dest_Const o Morphism.term phi) min_alg_frees; val min_alg_defs = map (fn def => mk_unabs_def n (HOLogic.mk_obj_eq (Morphism.thm phi def))) min_alg_def_frees; fun mk_min_alg ss i = let val T = HOLogic.mk_setT (range_type (fastype_of (nth ss (i - 1)))) val Ts = map fastype_of ss; val min_algT = Library.foldr (op -->) (Ts, T); in Term.list_comb (Const (nth min_algs (i - 1), min_algT), ss) end; val min_algs = map (mk_min_alg ss) ks; val ((Bs, ss), _) = lthy |> mk_Frees "B" BTs ||>> mk_Frees "s" sTs; val (alg_min_alg_thm, card_of_min_alg_thms, least_min_alg_thms, mor_incl_min_alg_thm) = let val alg_min_alg = let val goal = HOLogic.mk_Trueprop (mk_alg min_algs ss); val vars = Variable.add_free_names lthy goal []; in Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => mk_alg_min_alg_tac ctxt m alg_def min_alg_defs suc_bd_limit_thm sbd_Cinfinite set_sbdss min_algs_thms min_algs_mono_thms) |> Thm.close_derivation \<^here> end; fun mk_card_of_thm min_alg def = let val goal = HOLogic.mk_Trueprop (mk_ordLeq (mk_card_of min_alg) Asuc_bd); val vars = Variable.add_free_names lthy goal []; in Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => mk_card_of_min_alg_tac ctxt def card_of_min_algs_thm suc_bd_Card_order suc_bd_Asuc_bd Asuc_bd_Cinfinite) |> Thm.close_derivation \<^here> end; fun mk_least_thm min_alg B def = let val prem = HOLogic.mk_Trueprop (mk_alg Bs ss); val goal = Logic.mk_implies (prem, HOLogic.mk_Trueprop (mk_leq min_alg B)); val vars = Variable.add_free_names lthy goal []; in Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => mk_least_min_alg_tac ctxt def least_min_algs_thm) |> Thm.close_derivation \<^here> end; val leasts = @{map 3} mk_least_thm min_algs Bs min_alg_defs; val incl = let val prem = HOLogic.mk_Trueprop (mk_alg Bs ss); val goal = Logic.mk_implies (prem, HOLogic.mk_Trueprop (mk_mor min_algs ss Bs ss active_ids)); val vars = Variable.add_free_names lthy goal []; in Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => EVERY' (rtac ctxt mor_incl_thm :: map (etac ctxt) leasts) 1) |> Thm.close_derivation \<^here> end; in (alg_min_alg, map2 mk_card_of_thm min_algs min_alg_defs, leasts, incl) end; val timer = time (timer "Minimal algebra definition & thms"); val II_repT = HOLogic.mk_prodT (HOLogic.mk_tupleT II_BTs, HOLogic.mk_tupleT II_sTs); val IIT_bind = mk_internal_b IITN; val ((IIT_name, (IIT_glob_info, IIT_loc_info)), lthy) = typedef (IIT_bind, params, NoSyn) (HOLogic.mk_UNIV II_repT) NONE (fn ctxt => EVERY' [rtac ctxt exI, rtac ctxt UNIV_I] 1) lthy; val IIT = Type (IIT_name, params'); val Abs_IIT = Const (#Abs_name IIT_glob_info, II_repT --> IIT); val Rep_IIT = Const (#Rep_name IIT_glob_info, IIT --> II_repT); val Abs_IIT_inverse_thm = UNIV_I RS #Abs_inverse IIT_loc_info; val initT = IIT --> Asuc_bdT; val active_initTs = replicate n initT; val init_FTs = map2 (fn Ds => mk_T_of_bnf Ds (passiveAs @ active_initTs)) Dss bnfs; val init_fTs = map (fn T => initT --> T) activeAs; val ((((II_Bs, II_ss), (iidx, iidx')), init_xFs), _) = lthy |> mk_Frees "IIB" II_BTs ||>> mk_Frees "IIs" II_sTs ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "i") IIT ||>> mk_Frees "x" init_FTs; val II = HOLogic.mk_Collect (fst iidx', IIT, list_exists_free (II_Bs @ II_ss) (HOLogic.mk_conj (HOLogic.mk_eq (iidx, Abs_IIT $ (HOLogic.mk_prod (HOLogic.mk_tuple II_Bs, HOLogic.mk_tuple II_ss))), mk_alg II_Bs II_ss))); val select_Bs = map (mk_nthN n (HOLogic.mk_fst (Rep_IIT $ iidx))) ks; val select_ss = map (mk_nthN n (HOLogic.mk_snd (Rep_IIT $ iidx))) ks; val str_init_binds = mk_internal_bs str_initN; fun str_init_bind i = nth str_init_binds (i - 1); val str_init_def_bind = rpair [] o Thm.def_binding o str_init_bind; fun str_init_spec i = let val init_xF = nth init_xFs (i - 1) val select_s = nth select_ss (i - 1); val map = mk_map_of_bnf (nth Dss (i - 1)) (passiveAs @ active_initTs) (passiveAs @ replicate n Asuc_bdT) (nth bnfs (i - 1)); val map_args = passive_ids @ replicate n (mk_rapp iidx Asuc_bdT); val rhs = select_s $ (Term.list_comb (map, map_args) $ init_xF); in fold_rev (Term.absfree o Term.dest_Free) [init_xF, iidx] rhs end; val ((str_init_frees, (_, str_init_def_frees)), (lthy, lthy_old)) = lthy |> Local_Theory.open_target |> snd |> fold_map (fn i => Local_Theory.define ((str_init_bind i, NoSyn), (str_init_def_bind i, str_init_spec i))) ks |>> apsnd split_list o split_list ||> `Local_Theory.close_target; val phi = Proof_Context.export_morphism lthy_old lthy; val str_inits = map (Term.subst_atomic_types (map (`(Morphism.typ phi)) params') o Morphism.term phi) str_init_frees; val str_init_defs = map (fn def => mk_unabs_def 2 (HOLogic.mk_obj_eq (Morphism.thm phi def))) str_init_def_frees; val car_inits = map (mk_min_alg str_inits) ks; val (((((((((Bs, ss), Asuc_fs), (iidx, iidx')), init_xs), (init_xFs, init_xFs')), init_fs), init_fs_copy), init_phis), _) = lthy |> mk_Frees "B" BTs ||>> mk_Frees "s" sTs ||>> mk_Frees "f" (map (fn T => Asuc_bdT --> T) activeAs) ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "i") IIT ||>> mk_Frees "ix" active_initTs ||>> mk_Frees' "x" init_FTs ||>> mk_Frees "f" init_fTs ||>> mk_Frees "f" init_fTs ||>> mk_Frees "P" (replicate n (mk_pred1T initT)); val alg_init_thm = infer_instantiate' lthy (map (SOME o Thm.cterm_of lthy) str_inits) alg_min_alg_thm; val alg_select_thm = Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop (mk_Ball II (Term.absfree iidx' (mk_alg select_Bs select_ss)))) (fn {context = ctxt, prems = _} => mk_alg_select_tac ctxt Abs_IIT_inverse_thm) |> Thm.close_derivation \<^here>; val mor_select_thm = let val i_prem = mk_Trueprop_mem (iidx, II); val mor_prem = HOLogic.mk_Trueprop (mk_mor select_Bs select_ss active_UNIVs ss Asuc_fs); val prems = [i_prem, mor_prem]; val concl = HOLogic.mk_Trueprop (mk_mor car_inits str_inits active_UNIVs ss (map (fn f => HOLogic.mk_comp (f, mk_rapp iidx Asuc_bdT)) Asuc_fs)); val vars = fold (Variable.add_free_names lthy) (concl :: prems) []; in Goal.prove_sorry lthy vars [] (Logic.list_implies (prems, concl)) (fn {context = ctxt, prems = _} => mk_mor_select_tac ctxt mor_def mor_cong_thm mor_comp_thm mor_incl_min_alg_thm alg_def alg_select_thm alg_set_thms set_mapss str_init_defs) |> Thm.close_derivation \<^here> end; val init_unique_mor_thms = let val prems = map2 (HOLogic.mk_Trueprop oo curry HOLogic.mk_mem) init_xs car_inits val mor_prems = map HOLogic.mk_Trueprop [mk_mor car_inits str_inits Bs ss init_fs, mk_mor car_inits str_inits Bs ss init_fs_copy]; fun mk_fun_eq f g x = HOLogic.mk_eq (f $ x, g $ x); val unique = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (@{map 3} mk_fun_eq init_fs init_fs_copy init_xs)); val cts = map (Thm.cterm_of lthy) ss; val all_prems = prems @ mor_prems; val vars = fold (Variable.add_free_names lthy) (unique :: all_prems) []; val unique_mor = Goal.prove_sorry lthy vars [] (Logic.list_implies (all_prems, unique)) (fn {context = ctxt, prems = _} => mk_init_unique_mor_tac ctxt cts m alg_def alg_init_thm least_min_alg_thms in_mono'_thms alg_set_thms morE_thms map_cong0s) |> Thm.close_derivation \<^here>; in split_conj_thm unique_mor end; val init_setss = mk_setss (passiveAs @ active_initTs); val active_init_setss = map (drop m) init_setss; val init_ins = map2 (fn sets => mk_in (passive_UNIVs @ car_inits) sets) init_setss init_FTs; fun mk_closed phis = let fun mk_conjunct phi str_init init_sets init_in x x' = let val prem = Library.foldr1 HOLogic.mk_conj (map2 (fn set => mk_Ball (set $ x)) init_sets phis); val concl = phi $ (str_init $ x); in mk_Ball init_in (Term.absfree x' (HOLogic.mk_imp (prem, concl))) end; in Library.foldr1 HOLogic.mk_conj (@{map 6} mk_conjunct phis str_inits active_init_setss init_ins init_xFs init_xFs') end; val init_induct_thm = let val prem = HOLogic.mk_Trueprop (mk_closed init_phis); val concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 mk_Ball car_inits init_phis)); val vars = fold (Variable.add_free_names lthy) [concl, prem] []; in Goal.prove_sorry lthy vars [] (Logic.mk_implies (prem, concl)) (fn {context = ctxt, prems = _} => mk_init_induct_tac ctxt m alg_def alg_init_thm least_min_alg_thms alg_set_thms) |> Thm.close_derivation \<^here> end; val timer = time (timer "Initiality definition & thms"); val ((T_names, (T_glob_infos, T_loc_infos)), lthy) = lthy |> @{fold_map 3} (fn b => fn mx => fn car_init => typedef (b, params, mx) car_init NONE (fn ctxt => EVERY' [rtac ctxt iffD2, rtac ctxt @{thm ex_in_conv}, resolve_tac ctxt alg_not_empty_thms, rtac ctxt alg_init_thm] 1)) bs mixfixes car_inits |>> apsnd split_list o split_list; val Ts = map (fn name => Type (name, params')) T_names; fun mk_Ts passive = map (Term.typ_subst_atomic (passiveAs ~~ passive)) Ts; val Ts' = mk_Ts passiveBs; val Rep_Ts = map2 (fn info => fn T => Const (#Rep_name info, T --> initT)) T_glob_infos Ts; val Abs_Ts = map2 (fn info => fn T => Const (#Abs_name info, initT --> T)) T_glob_infos Ts; val type_defs = map #type_definition T_loc_infos; val Reps = map #Rep T_loc_infos; val Rep_inverses = map #Rep_inverse T_loc_infos; val Abs_inverses = map #Abs_inverse T_loc_infos; val timer = time (timer "THE TYPEDEFs & Rep/Abs thms"); val UNIVs = map HOLogic.mk_UNIV Ts; val FTs = mk_FTs (passiveAs @ Ts); val FTs' = mk_FTs (passiveBs @ Ts'); fun mk_set_Ts T = passiveAs @ replicate n (HOLogic.mk_setT T); val setFTss = map (mk_FTs o mk_set_Ts) passiveAs; val FTs_setss = mk_setss (passiveAs @ Ts); val FTs'_setss = mk_setss (passiveBs @ Ts'); val map_FT_inits = map2 (fn Ds => mk_map_of_bnf Ds (passiveAs @ Ts) (passiveAs @ active_initTs)) Dss bnfs; val fTs = map2 (curry op -->) Ts activeAs; val foldT = Library.foldr1 HOLogic.mk_prodT (map2 (curry op -->) Ts activeAs); val ((ss, (fold_f, fold_f')), _) = lthy |> mk_Frees "s" sTs ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "f") foldT; fun ctor_bind i = nth external_bs (i - 1) |> Binding.prefix_name (ctorN ^ "_"); val ctor_def_bind = rpair [] o Binding.concealed o Thm.def_binding o ctor_bind; fun ctor_spec abs str map_FT_init = Library.foldl1 HOLogic.mk_comp [abs, str, Term.list_comb (map_FT_init, map HOLogic.id_const passiveAs @ Rep_Ts)]; val ((ctor_frees, (_, ctor_def_frees)), (lthy, lthy_old)) = lthy |> Local_Theory.open_target |> snd |> @{fold_map 4} (fn i => fn abs => fn str => fn mapx => Local_Theory.define ((ctor_bind i, NoSyn), (ctor_def_bind i, ctor_spec abs str mapx))) ks Abs_Ts str_inits map_FT_inits |>> apsnd split_list o split_list ||> `Local_Theory.close_target; val phi = Proof_Context.export_morphism lthy_old lthy; fun mk_ctors passive = map (Term.subst_atomic_types (map (Morphism.typ phi) params' ~~ (mk_params passive)) o Morphism.term phi) ctor_frees; val ctors = mk_ctors passiveAs; val ctor's = mk_ctors passiveBs; val ctor_defs = map (fn def => HOLogic.mk_obj_eq (Morphism.thm phi def)) ctor_def_frees; val (mor_Rep_thm, mor_Abs_thm) = let val defs = mor_def :: ctor_defs; val mor_Rep = Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop (mk_mor UNIVs ctors car_inits str_inits Rep_Ts)) (fn {context = ctxt, prems = _} => mk_mor_Rep_tac ctxt m defs Reps Abs_inverses alg_min_alg_thm alg_set_thms set_mapss) |> Thm.close_derivation \<^here>; fun mk_ct initFT str abs = Term.absdummy initFT (abs $ (str $ Bound 0)) val cts = @{map 3} (Thm.cterm_of lthy ooo mk_ct) init_FTs str_inits Abs_Ts; val mor_Abs = Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop (mk_mor car_inits str_inits UNIVs ctors Abs_Ts)) (fn {context = ctxt, prems = _} => mk_mor_Abs_tac ctxt cts defs Abs_inverses map_comp_id_thms map_cong0L_thms) |> Thm.close_derivation \<^here>; in (mor_Rep, mor_Abs) end; val timer = time (timer "ctor definitions & thms"); val fold_fun = Term.absfree fold_f' (mk_mor UNIVs ctors active_UNIVs ss (map (mk_nthN n fold_f) ks)); val foldx = HOLogic.choice_const foldT $ fold_fun; fun fold_bind i = nth external_bs (i - 1) |> Binding.prefix_name (ctor_foldN ^ "_"); val fold_def_bind = rpair [] o Binding.concealed o Thm.def_binding o fold_bind; fun fold_spec i = fold_rev (Term.absfree o Term.dest_Free) ss (mk_nthN n foldx i); val ((fold_frees, (_, fold_def_frees)), (lthy, lthy_old)) = lthy |> Local_Theory.open_target |> snd |> fold_map (fn i => Local_Theory.define ((fold_bind i, NoSyn), (fold_def_bind i, fold_spec i))) ks |>> apsnd split_list o split_list ||> `Local_Theory.close_target; val phi = Proof_Context.export_morphism lthy_old lthy; val folds = map (Morphism.term phi) fold_frees; val fold_names = map (fst o dest_Const) folds; fun mk_folds passives actives = @{map 3} (fn name => fn T => fn active => Const (name, Library.foldr (op -->) (map2 (curry op -->) (mk_FTs (passives @ actives)) actives, T --> active))) fold_names (mk_Ts passives) actives; fun mk_fold Ts ss i = Term.list_comb (Const (nth fold_names (i - 1), Library.foldr (op -->) (map fastype_of ss, nth Ts (i - 1) --> range_type (fastype_of (nth ss (i - 1))))), ss); val fold_defs = map (fn def => mk_unabs_def n (HOLogic.mk_obj_eq (Morphism.thm phi def))) fold_def_frees; (* algebra copies *) val ((((((Bs, B's), ss), s's), inv_fs), fs), _) = lthy |> mk_Frees "B" BTs ||>> mk_Frees "B'" B'Ts ||>> mk_Frees "s" sTs ||>> mk_Frees "s'" s'Ts ||>> mk_Frees "f" inv_fTs ||>> mk_Frees "f" fTs; val copy_thm = let val prems = HOLogic.mk_Trueprop (mk_alg Bs ss) :: @{map 3} (HOLogic.mk_Trueprop ooo mk_bij_betw) inv_fs B's Bs; val concl = HOLogic.mk_Trueprop (list_exists_free s's (HOLogic.mk_conj (mk_alg B's s's, mk_mor B's s's Bs ss inv_fs))); val vars = fold (Variable.add_free_names lthy) (concl :: prems) []; in Goal.prove_sorry lthy vars [] (Logic.list_implies (prems, concl)) (fn {context = ctxt, prems = _} => mk_copy_tac ctxt m alg_def mor_def alg_set_thms set_mapss) |> Thm.close_derivation \<^here> end; val init_ex_mor_thm = let val goal = HOLogic.mk_Trueprop (list_exists_free fs (mk_mor UNIVs ctors active_UNIVs ss fs)); val vars = Variable.add_free_names lthy goal []; in Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => mk_init_ex_mor_tac ctxt Abs_IIT_inverse_thm (alg_min_alg_thm RS copy_thm) card_of_min_alg_thms mor_Rep_thm mor_comp_thm mor_select_thm mor_incl_thm) |> Thm.close_derivation \<^here> end; val mor_fold_thm = let val mor_cong = mor_cong_thm OF (map (mk_nth_conv n) ks); val cT = Thm.ctyp_of lthy foldT; val ct = Thm.cterm_of lthy fold_fun val goal = HOLogic.mk_Trueprop (mk_mor UNIVs ctors active_UNIVs ss (map (mk_fold Ts ss) ks)); val vars = Variable.add_free_names lthy goal []; in Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, ...} => mk_mor_fold_tac ctxt cT ct fold_defs init_ex_mor_thm mor_cong) |> Thm.close_derivation \<^here> end; val ctor_fold_thms = map (fn morE => rule_by_tactic lthy ((rtac lthy CollectI THEN' CONJ_WRAP' (K (rtac lthy @{thm subset_UNIV})) (1 upto m + n)) 1) (mor_fold_thm RS morE)) morE_thms; val (fold_unique_mor_thms, fold_unique_mor_thm) = let val prem = HOLogic.mk_Trueprop (mk_mor UNIVs ctors active_UNIVs ss fs); fun mk_fun_eq f i = HOLogic.mk_eq (f, mk_fold Ts ss i); val unique = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 mk_fun_eq fs ks)); val vars = fold (Variable.add_free_names lthy) [prem, unique] []; val unique_mor = Goal.prove_sorry lthy vars [] (Logic.mk_implies (prem, unique)) (fn {context = ctxt, prems = _} => mk_fold_unique_mor_tac ctxt type_defs init_unique_mor_thms Reps mor_comp_thm mor_Abs_thm mor_fold_thm) |> Thm.close_derivation \<^here>; in `split_conj_thm unique_mor end; val (ctor_fold_unique_thms, ctor_fold_unique_thm) = `split_conj_thm (mk_conjIN n RS (mor_UNIV_thm RS iffD2 RS fold_unique_mor_thm)) val fold_ctor_thms = map (fn thm => (mor_incl_thm OF replicate n @{thm subset_UNIV}) RS thm RS sym) fold_unique_mor_thms; val ctor_o_fold_thms = let val mor = mor_comp_thm OF [mor_fold_thm, mor_str_thm]; in map2 (fn unique => fn fold_ctor => trans OF [mor RS unique, fold_ctor]) fold_unique_mor_thms fold_ctor_thms end; val timer = time (timer "fold definitions & thms"); val map_ctors = map2 (fn Ds => fn bnf => Term.list_comb (mk_map_of_bnf Ds (passiveAs @ FTs) (passiveAs @ Ts) bnf, map HOLogic.id_const passiveAs @ ctors)) Dss bnfs; fun dtor_bind i = nth external_bs (i - 1) |> Binding.prefix_name (dtorN ^ "_"); val dtor_def_bind = rpair [] o Binding.concealed o Thm.def_binding o dtor_bind; fun dtor_spec i = mk_fold Ts map_ctors i; val ((dtor_frees, (_, dtor_def_frees)), (lthy, lthy_old)) = lthy |> Local_Theory.open_target |> snd |> fold_map (fn i => Local_Theory.define ((dtor_bind i, NoSyn), (dtor_def_bind i, dtor_spec i))) ks |>> apsnd split_list o split_list ||> `Local_Theory.close_target; val phi = Proof_Context.export_morphism lthy_old lthy; fun mk_dtors params = map (Term.subst_atomic_types (map (Morphism.typ phi) params' ~~ params) o Morphism.term phi) dtor_frees; val dtors = mk_dtors params'; val dtor_defs = map (fn def => HOLogic.mk_obj_eq (Morphism.thm phi def)) dtor_def_frees; val ctor_o_dtor_thms = map2 (Local_Defs.fold lthy o single) dtor_defs ctor_o_fold_thms; val dtor_o_ctor_thms = let fun mk_goal dtor ctor FT = mk_Trueprop_eq (HOLogic.mk_comp (dtor, ctor), HOLogic.id_const FT); val goals = @{map 3} mk_goal dtors ctors FTs; in @{map 5} (fn goal => fn dtor_def => fn foldx => fn map_comp_id => fn map_cong0L => Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} => mk_dtor_o_ctor_tac ctxt dtor_def foldx map_comp_id map_cong0L ctor_o_fold_thms) |> Thm.close_derivation \<^here>) goals dtor_defs ctor_fold_thms map_comp_id_thms map_cong0L_thms end; val dtor_ctor_thms = map (fn thm => thm RS @{thm pointfree_idE}) dtor_o_ctor_thms; val ctor_dtor_thms = map (fn thm => thm RS @{thm pointfree_idE}) ctor_o_dtor_thms; val bij_dtor_thms = map2 (fn thm1 => fn thm2 => @{thm o_bij} OF [thm1, thm2]) ctor_o_dtor_thms dtor_o_ctor_thms; val inj_dtor_thms = map (fn thm => thm RS @{thm bij_is_inj}) bij_dtor_thms; val surj_dtor_thms = map (fn thm => thm RS @{thm bij_is_surj}) bij_dtor_thms; val dtor_nchotomy_thms = map (fn thm => thm RS @{thm surjD}) surj_dtor_thms; val dtor_inject_thms = map (fn thm => thm RS @{thm inj_eq}) inj_dtor_thms; val dtor_exhaust_thms = map (fn thm => thm RS exE) dtor_nchotomy_thms; val bij_ctor_thms = map2 (fn thm1 => fn thm2 => @{thm o_bij} OF [thm1, thm2]) dtor_o_ctor_thms ctor_o_dtor_thms; val inj_ctor_thms = map (fn thm => thm RS @{thm bij_is_inj}) bij_ctor_thms; val surj_ctor_thms = map (fn thm => thm RS @{thm bij_is_surj}) bij_ctor_thms; val ctor_nchotomy_thms = map (fn thm => thm RS @{thm surjD}) surj_ctor_thms; val ctor_inject_thms = map (fn thm => thm RS @{thm inj_eq}) inj_ctor_thms; val ctor_exhaust_thms = map (fn thm => thm RS exE) ctor_nchotomy_thms; val timer = time (timer "dtor definitions & thms"); val (((((((Izs, (Izs1, Izs1'))), (Izs2, Izs2')), xFs), yFs), init_phis), _) = lthy |> mk_Frees "z" Ts ||>> mk_Frees' "z1" Ts ||>> mk_Frees' "z2" Ts' ||>> mk_Frees "x" FTs ||>> mk_Frees "y" FTs' ||>> mk_Frees "P" (replicate n (mk_pred1T initT)); val phis = map2 retype_const_or_free (map mk_pred1T Ts) init_phis; val phi2s = map2 retype_const_or_free (map2 mk_pred2T Ts Ts') init_phis; val (ctor_induct_thm, induct_params) = let fun mk_prem phi ctor sets x = let fun mk_IH phi set z = let val prem = mk_Trueprop_mem (z, set $ x); val concl = HOLogic.mk_Trueprop (phi $ z); in Logic.all z (Logic.mk_implies (prem, concl)) end; val IHs = @{map 3} mk_IH phis (drop m sets) Izs; val concl = HOLogic.mk_Trueprop (phi $ (ctor $ x)); in Logic.all x (Logic.list_implies (IHs, concl)) end; val prems = @{map 4} mk_prem phis ctors FTs_setss xFs; fun mk_concl phi z = phi $ z; val concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 mk_concl phis Izs)); val goal = Logic.list_implies (prems, concl); val vars = Variable.add_free_names lthy goal []; in (Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => mk_ctor_induct_tac ctxt m set_mapss init_induct_thm morE_thms mor_Abs_thm Rep_inverses Abs_inverses Reps) |> Thm.close_derivation \<^here>, rev (Term.add_tfrees goal [])) end; val cTs = map (SOME o Thm.ctyp_of lthy o TFree) induct_params; val weak_ctor_induct_thms = let fun insts i = (replicate (i - 1) TrueI) @ (asm_rl :: replicate (n - i) TrueI); in map (fn i => (ctor_induct_thm OF insts i) RS mk_conjunctN n i) ks end; val (ctor_induct2_thm, induct2_params) = let fun mk_prem phi ctor ctor' sets sets' x y = let fun mk_IH phi set set' z1 z2 = let val prem1 = mk_Trueprop_mem (z1, (set $ x)); val prem2 = mk_Trueprop_mem (z2, (set' $ y)); val concl = HOLogic.mk_Trueprop (phi $ z1 $ z2); in fold_rev Logic.all [z1, z2] (Logic.list_implies ([prem1, prem2], concl)) end; val IHs = @{map 5} mk_IH phi2s (drop m sets) (drop m sets') Izs1 Izs2; val concl = HOLogic.mk_Trueprop (phi $ (ctor $ x) $ (ctor' $ y)); in fold_rev Logic.all [x, y] (Logic.list_implies (IHs, concl)) end; val prems = @{map 7} mk_prem phi2s ctors ctor's FTs_setss FTs'_setss xFs yFs; fun mk_concl phi z1 z2 = phi $ z1 $ z2; val concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (@{map 3} mk_concl phi2s Izs1 Izs2)); fun mk_t phi (z1, z1') (z2, z2') = Term.absfree z1' (HOLogic.mk_all (fst z2', snd z2', phi $ z1 $ z2)); val cts = @{map 3} (SOME o Thm.cterm_of lthy ooo mk_t) phi2s (Izs1 ~~ Izs1') (Izs2 ~~ Izs2'); val goal = Logic.list_implies (prems, concl); val vars = Variable.add_free_names lthy goal []; in (Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => mk_ctor_induct2_tac ctxt cTs cts ctor_induct_thm weak_ctor_induct_thms) |> Thm.close_derivation \<^here>, rev (Term.add_tfrees goal [])) end; val timer = time (timer "induction"); fun mk_ctor_map_DEADID_thm ctor_inject map_id0 = trans OF [id_apply, iffD2 OF [ctor_inject, map_id0 RS sym]]; fun mk_ctor_map_unique_DEADID_thm () = let val (funs, algs) = HOLogic.conjuncts (HOLogic.dest_Trueprop (Thm.concl_of ctor_fold_unique_thm)) |> map_split HOLogic.dest_eq ||> snd o strip_comb o hd |> @{apply 2} (map (fst o dest_Var)); fun mk_fun_insts T ix = Thm.cterm_of lthy (Var (ix, T --> T)); val theta = (funs ~~ @{map 2} mk_fun_insts Ts funs) @ (algs ~~ map (Thm.cterm_of lthy) ctors); val ctor_fold_ctors = (ctor_fold_unique_thm OF map (fn thm => mk_trans @{thm id_o} (mk_sym (thm RS @{thm trans[OF arg_cong2[of _ _ _ _ "(\)", OF refl] o_id]}))) map_id0s) |> split_conj_thm |> map mk_sym; in infer_instantiate lthy theta ctor_fold_unique_thm |> unfold_thms lthy ctor_fold_ctors |> Morphism.thm (Local_Theory.target_morphism lthy) end; fun mk_ctor_Irel_DEADID_thm ctor_inject bnf = trans OF [ctor_inject, rel_eq_of_bnf bnf RS @{thm predicate2_eqD} RS sym]; val IphiTs = map2 mk_pred2T passiveAs passiveBs; val Ipsi1Ts = map2 mk_pred2T passiveAs passiveCs; val Ipsi2Ts = map2 mk_pred2T passiveCs passiveBs; val activephiTs = map2 mk_pred2T activeAs activeBs; val activeIphiTs = map2 mk_pred2T Ts Ts'; val rels = map2 (fn Ds => mk_rel_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs; (*register new datatypes as BNFs*) val (timer, Ibnfs, (ctor_Imap_o_thms, ctor_Imap_thms), ctor_Imap_unique_thm, ctor_Iset_thmss', ctor_Irel_thms, Ibnf_notes, lthy) = if m = 0 then (timer, replicate n DEADID_bnf, map_split (`(mk_pointfree2 lthy)) (map2 mk_ctor_map_DEADID_thm ctor_inject_thms map_ids), mk_ctor_map_unique_DEADID_thm (), replicate n [], map2 mk_ctor_Irel_DEADID_thm ctor_inject_thms bnfs, [], lthy) else let val fTs = map2 (curry op -->) passiveAs passiveBs; val uTs = map2 (curry op -->) Ts Ts'; val ((((fs, fs'), (AFss, AFss')), (ys, ys')), _) = lthy |> mk_Frees' "f" fTs ||>> mk_Freess' "z" setFTss ||>> mk_Frees' "y" passiveAs; val map_FTFT's = map2 (fn Ds => mk_map_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs; fun mk_passive_maps ATs BTs Ts = map2 (fn Ds => mk_map_of_bnf Ds (ATs @ Ts) (BTs @ Ts)) Dss bnfs; fun mk_map_fold_arg fs Ts ctor fmap = HOLogic.mk_comp (ctor, Term.list_comb (fmap, fs @ map HOLogic.id_const Ts)); fun mk_map Ts fs Ts' ctors mk_maps = mk_fold Ts (map2 (mk_map_fold_arg fs Ts') ctors (mk_maps Ts')); val pmapsABT' = mk_passive_maps passiveAs passiveBs; val fs_maps = map (mk_map Ts fs Ts' ctor's pmapsABT') ks; val ls = 1 upto m; val setsss = map (mk_setss o mk_set_Ts) passiveAs; fun mk_col l T z z' sets = let fun mk_UN set = mk_Union T $ (set $ z); in Term.absfree z' (mk_union (nth sets (l - 1) $ z, Library.foldl1 mk_union (map mk_UN (drop m sets)))) end; val colss = @{map 5} (fn l => fn T => @{map 3} (mk_col l T)) ls passiveAs AFss AFss' setsss; val setss_by_range = map (fn cols => map (mk_fold Ts cols) ks) colss; val setss_by_bnf = transpose setss_by_range; val set_bss = map (flat o map2 (fn B => fn b => if member (op =) deads (TFree B) then [] else [b]) resBs) set_bss0; val ctor_witss = let val witss = map2 (fn Ds => fn bnf => mk_wits_of_bnf (replicate (nwits_of_bnf bnf) Ds) (replicate (nwits_of_bnf bnf) (passiveAs @ Ts)) bnf) Dss bnfs; fun close_wit (I, wit) = fold_rev Term.absfree (map (nth ys') I) wit; fun wit_apply (arg_I, arg_wit) (fun_I, fun_wit) = (union (op =) arg_I fun_I, fun_wit $ arg_wit); fun gen_arg support i = if i < m then [([i], nth ys i)] else maps (mk_wit support (nth ctors (i - m)) (i - m)) (nth support (i - m)) and mk_wit support ctor i (I, wit) = let val args = map (gen_arg (nth_map i (remove (op =) (I, wit)) support)) I; in (args, [([], wit)]) |-> fold (map_product wit_apply) |> map (apsnd (fn t => ctor $ t)) |> minimize_wits end; in @{map 3} (fn ctor => fn i => map close_wit o minimize_wits o maps (mk_wit witss ctor i)) ctors (0 upto n - 1) witss end; val (lthy, sbd0, sbd0_card_order, sbd0_Cinfinite, set_sbd0ss) = if n = 1 then (lthy, hd bd0s, hd bd0_card_orders, hd bd0_Cinfinites, set_bd0ss) else let val sum_bd0 = Library.foldr1 (uncurry mk_csum) bd0s; val sum_bd0T = fst (dest_relT (fastype_of sum_bd0)); val (sum_bd0T_params, sum_bd0T_params') = `(map TFree) (Term.add_tfreesT sum_bd0T []); val sbd0T_bind = mk_internal_b (sum_bdTN ^ "0"); val ((sbd0T_name, (sbd0T_glob_info, sbd0T_loc_info)), lthy) = typedef (sbd0T_bind, sum_bd0T_params', NoSyn) (HOLogic.mk_UNIV sum_bd0T) NONE (fn ctxt => EVERY' [rtac ctxt exI, rtac ctxt UNIV_I] 1) lthy; val sbd0T = Type (sbd0T_name, sum_bd0T_params); val Abs_sbd0T = Const (#Abs_name sbd0T_glob_info, sum_bd0T --> sbd0T); val sbd0_bind = mk_internal_b (sum_bdN ^ "0"); val sbd0_def_bind = (Thm.def_binding sbd0_bind, []); val sbd0_spec = mk_dir_image sum_bd0 Abs_sbd0T; val ((sbd0_free, (_, sbd0_def_free)), (lthy, lthy_old)) = lthy |> Local_Theory.open_target |> snd |> Local_Theory.define ((sbd0_bind, NoSyn), (sbd0_def_bind, sbd0_spec)) ||> `Local_Theory.close_target; val phi = Proof_Context.export_morphism lthy_old lthy; val sbd0_def = HOLogic.mk_obj_eq (Morphism.thm phi sbd0_def_free); val sbd0 = Const (fst (Term.dest_Const (Morphism.term phi sbd0_free)), mk_relT (`I sbd0T)); val Abs_sbd0T_inj = mk_Abs_inj_thm (#Abs_inject sbd0T_loc_info); val Abs_sbd0T_bij = mk_Abs_bij_thm lthy Abs_sbd0T_inj (#Abs_cases sbd0T_loc_info); val sum_Cinfinite = mk_sum_Cinfinite bd0_Cinfinites; val sum_Card_order = sum_Cinfinite RS conjunct2; val sum_card_order = mk_sum_card_order bd0_card_orders; val sbd0_ordIso = @{thm ssubst_Pair_rhs} OF [@{thm dir_image} OF [Abs_sbd0T_inj, sum_Card_order], sbd0_def]; val sbd0_Cinfinite = @{thm Cinfinite_cong} OF [sbd0_ordIso, sum_Cinfinite]; val sbd0_card_order = @{thm iffD2[OF arg_cong[of _ _ card_order]]} OF [sbd0_def, @{thm card_order_dir_image} OF [Abs_sbd0T_bij, sum_card_order]]; fun mk_set_sbd0 i bd0_Card_order bd0s = map (fn thm => @{thm ordLeq_ordIso_trans} OF [bd0_Card_order RS mk_ordLeq_csum n i thm, sbd0_ordIso]) bd0s; val set_sbd0ss = @{map 3} mk_set_sbd0 ks bd0_Card_orders set_bd0ss; in (lthy, sbd0, sbd0_card_order, sbd0_Cinfinite, set_sbd0ss) end; val (Ibnf_consts, lthy) = @{fold_map 9} (fn b => fn map_b => fn rel_b => fn pred_b => fn set_bs => fn mapx => fn sets => fn wits => fn T => fn lthy => define_bnf_consts Hardly_Inline (user_policy Note_Some lthy) false (SOME deads) map_b rel_b pred_b set_bs (((((((b, T), fold_rev Term.absfree fs' mapx), sets), sbd0), wits), NONE), NONE) lthy) bs map_bs rel_bs pred_bs set_bss fs_maps setss_by_bnf ctor_witss Ts lthy; val ((((((((((((((Izs, (Izs1, Izs1')), (Izs2, Izs2')), xFs), yFs))), Iphis), Ipsi1s), Ipsi2s), fs), fs_copy), us), (ys, ys')), _) = lthy |> mk_Frees "z" Ts ||>> mk_Frees' "z1" Ts ||>> mk_Frees' "z2" Ts' ||>> mk_Frees "x" FTs ||>> mk_Frees "y" FTs' ||>> mk_Frees "R" IphiTs ||>> mk_Frees "R" Ipsi1Ts ||>> mk_Frees "Q" Ipsi2Ts ||>> mk_Frees "f" fTs ||>> mk_Frees "f" fTs ||>> mk_Frees "u" uTs ||>> mk_Frees' "y" passiveAs; val (_, Iconsts, Iconst_defs, mk_Iconsts) = @{split_list 4} Ibnf_consts; val (_, Isetss, Ibds_Ds, Iwitss_Ds, _, _) = @{split_list 6} Iconsts; val (Imap_defs, Iset_defss, Ibd_defs, Iwit_defss, Irel_defs, Ipred_defs) = @{split_list 6} Iconst_defs; val (mk_Imaps_Ds, mk_It_Ds, _, mk_Irels_Ds, mk_Ipreds_Ds, _, _) = @{split_list 7} mk_Iconsts; val Irel_unabs_defs = map (fn def => mk_unabs_def m (HOLogic.mk_obj_eq def)) Irel_defs; val Ipred_unabs_defs = map (fn def => mk_unabs_def m (HOLogic.mk_obj_eq def)) Ipred_defs; val Iset_defs = flat Iset_defss; fun mk_Imaps As Bs = map (fn mk => mk deads As Bs) mk_Imaps_Ds; fun mk_Isetss As = map2 (fn mk => fn Isets => map (mk deads As) Isets) mk_It_Ds Isetss; val Ibds = map2 (fn mk => mk deads passiveAs) mk_It_Ds Ibds_Ds; val Iwitss = map2 (fn mk => fn Iwits => map (mk deads passiveAs o snd) Iwits) mk_It_Ds Iwitss_Ds; fun mk_Irels As Bs = map (fn mk => mk deads As Bs) mk_Irels_Ds; fun mk_Ipreds As = map (fn mk => mk deads As) mk_Ipreds_Ds; val Imaps = mk_Imaps passiveAs passiveBs; val fs_Imaps = map (fn m => Term.list_comb (m, fs)) Imaps; val fs_copy_Imaps = map (fn m => Term.list_comb (m, fs_copy)) Imaps; val (Isetss_by_range, Isetss_by_bnf) = `transpose (mk_Isetss passiveAs); val map_setss = map (fn T => map2 (fn Ds => mk_map_of_bnf Ds (passiveAs @ Ts) (mk_set_Ts T)) Dss bnfs) passiveAs; val timer = time (timer "bnf constants for the new datatypes"); val (ctor_Imap_thms, ctor_Imap_o_thms) = let fun mk_goal fs_map map ctor ctor' = mk_Trueprop_eq (HOLogic.mk_comp (fs_map, ctor), HOLogic.mk_comp (ctor', Term.list_comb (map, fs @ fs_Imaps))); val goals = @{map 4} mk_goal fs_Imaps map_FTFT's ctors ctor's; val maps = @{map 4} (fn goal => fn foldx => fn map_comp_id => fn map_cong0 => Variable.add_free_names lthy goal [] |> (fn vars => Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Imap_defs THEN mk_map_tac ctxt m n foldx map_comp_id map_cong0)) |> Thm.close_derivation \<^here>) goals ctor_fold_thms map_comp_id_thms map_cong0s; in `(map (fn thm => thm RS @{thm comp_eq_dest})) maps end; val (ctor_Imap_unique_thms, ctor_Imap_unique_thm) = let fun mk_prem u map ctor ctor' = mk_Trueprop_eq (HOLogic.mk_comp (u, ctor), HOLogic.mk_comp (ctor', Term.list_comb (map, fs @ us))); val prems = @{map 4} mk_prem us map_FTFT's ctors ctor's; val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 (curry HOLogic.mk_eq) us fs_Imaps)); val vars = fold (Variable.add_free_names lthy) (goal :: prems) []; val unique = Goal.prove_sorry lthy vars [] (Logic.list_implies (prems, goal)) (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Imap_defs THEN mk_ctor_map_unique_tac ctxt ctor_fold_unique_thm sym_map_comps) |> Thm.close_derivation \<^here>; in `split_conj_thm unique end; val timer = time (timer "map functions for the new datatypes"); val ctor_Iset_thmss = let fun mk_goal sets ctor set col map = mk_Trueprop_eq (HOLogic.mk_comp (set, ctor), HOLogic.mk_comp (col, Term.list_comb (map, passive_ids @ sets))); val goalss = @{map 3} (fn sets => @{map 4} (mk_goal sets) ctors sets) Isetss_by_range colss map_setss; val setss = map (map2 (fn foldx => fn goal => Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Iset_defs THEN mk_set_tac ctxt foldx) |> Thm.close_derivation \<^here>) ctor_fold_thms) goalss; fun mk_simp_goal pas_set act_sets sets ctor z set = mk_Trueprop_eq (set $ (ctor $ z), mk_union (pas_set $ z, Library.foldl1 mk_union (map2 (fn X => mk_UNION (X $ z)) act_sets sets))); val simp_goalss = map2 (fn i => fn sets => @{map 4} (fn Fsets => mk_simp_goal (nth Fsets (i - 1)) (drop m Fsets) sets) FTs_setss ctors xFs sets) ls Isetss_by_range; val ctor_setss = @{map 3} (fn i => @{map 3} (fn set_nats => fn goal => fn set => Variable.add_free_names lthy goal [] |> (fn vars => Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => mk_ctor_set_tac ctxt set (nth set_nats (i - 1)) (drop m set_nats))) |> Thm.close_derivation \<^here>) set_mapss) ls simp_goalss setss; in ctor_setss end; fun mk_set_thms ctor_set = (@{thm xt1(3)} OF [ctor_set, @{thm Un_upper1}]) :: map (fn i => (@{thm xt1(3)} OF [ctor_set, @{thm Un_upper2}]) RS (mk_Un_upper n i RS subset_trans) RSN (2, @{thm UN_upper} RS subset_trans)) (1 upto n); val set_Iset_thmsss = transpose (map (map mk_set_thms) ctor_Iset_thmss); val timer = time (timer "set functions for the new datatypes"); val cxs = map (SOME o Thm.cterm_of lthy) Izs; val Isetss_by_range' = map (map (Term.subst_atomic_types (passiveAs ~~ passiveBs))) Isetss_by_range; val Iset_Imap0_thmss = let fun mk_set_map0 f map z set set' = HOLogic.mk_eq (mk_image f $ (set $ z), set' $ (map $ z)); fun mk_cphi f map z set set' = Thm.cterm_of lthy (Term.absfree (dest_Free z) (mk_set_map0 f map z set set')); val csetss = map (map (Thm.cterm_of lthy)) Isetss_by_range'; val cphiss = @{map 3} (fn f => fn sets => fn sets' => (@{map 4} (mk_cphi f) fs_Imaps Izs sets sets')) fs Isetss_by_range Isetss_by_range'; val inducts = map (fn cphis => Thm.instantiate' cTs (map SOME cphis @ cxs) ctor_induct_thm) cphiss; val goals = @{map 3} (fn f => fn sets => fn sets' => HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (@{map 4} (mk_set_map0 f) fs_Imaps Izs sets sets'))) fs Isetss_by_range Isetss_by_range'; fun mk_tac ctxt induct = mk_set_nat_tac ctxt m (rtac ctxt induct) set_mapss ctor_Imap_thms; val thms = @{map 5} (fn goal => fn csets => fn ctor_sets => fn induct => fn i => Variable.add_free_names lthy goal [] |> (fn vars => Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => mk_tac ctxt induct csets ctor_sets i)) |> Thm.close_derivation \<^here>) goals csetss ctor_Iset_thmss inducts ls; in map split_conj_thm thms end; val Iset_bd_thmss = let fun mk_set_bd z bd set = mk_ordLeq (mk_card_of (set $ z)) bd; fun mk_cphi z set = Thm.cterm_of lthy (Term.absfree (dest_Free z) (mk_set_bd z sbd0 set)); val cphiss = map (map2 mk_cphi Izs) Isetss_by_range; val inducts = map (fn cphis => Thm.instantiate' cTs (map SOME cphis @ cxs) ctor_induct_thm) cphiss; val goals = map (fn sets => HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (@{map 3} mk_set_bd Izs Ibds sets))) Isetss_by_range; fun mk_tac ctxt induct = mk_set_bd_tac ctxt m (rtac ctxt induct) sbd0_Cinfinite set_sbd0ss; val thms = @{map 4} (fn goal => fn ctor_sets => fn induct => fn i => Variable.add_free_names lthy goal [] |> (fn vars => Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Ibd_defs THEN mk_tac ctxt induct ctor_sets i)) |> Thm.close_derivation \<^here>) goals ctor_Iset_thmss inducts ls; in map split_conj_thm thms end; val Imap_cong0_thms = let fun mk_prem z set f g y y' = mk_Ball (set $ z) (Term.absfree y' (HOLogic.mk_eq (f $ y, g $ y))); fun mk_map_cong0 sets z fmap gmap = HOLogic.mk_imp (Library.foldr1 HOLogic.mk_conj (@{map 5} (mk_prem z) sets fs fs_copy ys ys'), HOLogic.mk_eq (fmap $ z, gmap $ z)); fun mk_cphi sets z fmap gmap = Thm.cterm_of lthy (Term.absfree (dest_Free z) (mk_map_cong0 sets z fmap gmap)); val cphis = @{map 4} mk_cphi Isetss_by_bnf Izs fs_Imaps fs_copy_Imaps; val induct = Thm.instantiate' cTs (map SOME cphis @ cxs) ctor_induct_thm; val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (@{map 4} mk_map_cong0 Isetss_by_bnf Izs fs_Imaps fs_copy_Imaps)); val vars = Variable.add_free_names lthy goal []; val thm = Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => mk_mcong_tac ctxt (rtac ctxt induct) set_Iset_thmsss map_cong0s ctor_Imap_thms) |> Thm.close_derivation \<^here>; in split_conj_thm thm end; val in_rels = map in_rel_of_bnf bnfs; val in_Irels = map (fn def => trans OF [def, @{thm OO_Grp_alt}] RS @{thm predicate2_eqD}) Irel_unabs_defs; val ctor_Iset_incl_thmss = map (map hd) set_Iset_thmsss; val ctor_set_Iset_incl_thmsss = map (transpose o map tl) set_Iset_thmsss; val ctor_Iset_thmss' = transpose ctor_Iset_thmss; val Irels = mk_Irels passiveAs passiveBs; val Ipreds = mk_Ipreds passiveAs; val Irelphis = map (fn rel => Term.list_comb (rel, Iphis)) Irels; val relphis = map (fn rel => Term.list_comb (rel, Iphis @ Irelphis)) rels; val Irelpsi1s = map (fn rel => Term.list_comb (rel, Ipsi1s)) (mk_Irels passiveAs passiveCs); val Irelpsi2s = map (fn rel => Term.list_comb (rel, Ipsi2s)) (mk_Irels passiveCs passiveBs); val Irelpsi12s = map (fn rel => Term.list_comb (rel, map2 (curry mk_rel_compp) Ipsi1s Ipsi2s)) Irels; val ctor_Irel_thms = let fun mk_goal xF yF ctor ctor' Irelphi relphi = mk_Trueprop_eq (Irelphi $ (ctor $ xF) $ (ctor' $ yF), relphi $ xF $ yF); val goals = @{map 6} mk_goal xFs yFs ctors ctor's Irelphis relphis; in @{map 12} (fn i => fn goal => fn in_rel => fn map_comp0 => fn map_cong0 => fn ctor_map => fn ctor_sets => fn ctor_inject => fn ctor_dtor => fn set_map0s => fn ctor_set_incls => fn ctor_set_set_inclss => Variable.add_free_names lthy goal [] |> (fn vars => Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => mk_ctor_rel_tac ctxt in_Irels i in_rel map_comp0 map_cong0 ctor_map ctor_sets ctor_inject ctor_dtor set_map0s ctor_set_incls ctor_set_set_inclss)) |> Thm.close_derivation \<^here>) ks goals in_rels map_comps map_cong0s ctor_Imap_thms ctor_Iset_thmss' ctor_inject_thms ctor_dtor_thms set_mapss ctor_Iset_incl_thmss ctor_set_Iset_incl_thmsss end; val le_Irel_OO_thm = let fun mk_le_Irel_OO Irelpsi1 Irelpsi2 Irelpsi12 Iz1 Iz2 = HOLogic.mk_imp (mk_rel_compp (Irelpsi1, Irelpsi2) $ Iz1 $ Iz2, Irelpsi12 $ Iz1 $ Iz2); val goals = @{map 5} mk_le_Irel_OO Irelpsi1s Irelpsi2s Irelpsi12s Izs1 Izs2; val cTs = map (SOME o Thm.ctyp_of lthy o TFree) induct2_params; val cxs = map (SOME o Thm.cterm_of lthy) (splice Izs1 Izs2); fun mk_cphi z1 z2 goal = SOME (Thm.cterm_of lthy (Term.absfree z1 (Term.absfree z2 goal))); val cphis = @{map 3} mk_cphi Izs1' Izs2' goals; val induct = Thm.instantiate' cTs (cphis @ cxs) ctor_induct2_thm; val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj goals); val vars = Variable.add_free_names lthy goal []; in Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => mk_le_rel_OO_tac ctxt m induct ctor_nchotomy_thms ctor_Irel_thms rel_mono_strong0s le_rel_OOs) |> Thm.close_derivation \<^here> end; val timer = time (timer "helpers for BNF properties"); val map_id0_tacs = map (fn thm => fn ctxt => mk_map_id0_tac ctxt map_id0s thm) ctor_Imap_unique_thms; val map_comp0_tacs = map2 (fn thm => fn i => fn ctxt => mk_map_comp0_tac ctxt map_comps ctor_Imap_thms thm i) ctor_Imap_unique_thms ks; val map_cong0_tacs = map (fn thm => fn ctxt => mk_map_cong0_tac ctxt m thm) Imap_cong0_thms; val set_map0_tacss = map (map (fn thm => fn ctxt => mk_set_map0_tac ctxt thm)) (transpose Iset_Imap0_thmss); val bd_co_tacs = replicate n (fn ctxt => unfold_thms_tac ctxt Ibd_defs THEN rtac ctxt sbd0_card_order 1); val bd_cinf_tacs = replicate n (fn ctxt => unfold_thms_tac ctxt Ibd_defs THEN rtac ctxt (sbd0_Cinfinite RS conjunct1) 1); val set_bd_tacss = map (map (fn thm => fn ctxt => rtac ctxt thm 1)) (transpose Iset_bd_thmss); val le_rel_OO_tacs = map (fn i => fn ctxt => (rtac ctxt @{thm predicate2I} THEN' etac ctxt (le_Irel_OO_thm RS mk_conjunctN n i RS mp)) 1) ks; val rel_OO_Grp_tacs = map (fn def => fn ctxt => rtac ctxt def 1) Irel_unabs_defs; val pred_set_tacs = map (fn def => fn ctxt => rtac ctxt def 1) Ipred_unabs_defs; val tacss = @{map 10} zip_axioms map_id0_tacs map_comp0_tacs map_cong0_tacs set_map0_tacss bd_co_tacs bd_cinf_tacs set_bd_tacss le_rel_OO_tacs rel_OO_Grp_tacs pred_set_tacs; fun wit_tac ctxt = unfold_thms_tac ctxt (flat Iwit_defss) THEN mk_wit_tac ctxt n (flat ctor_Iset_thmss) (maps wit_thms_of_bnf bnfs); val (Ibnfs, lthy) = @{fold_map 6} (fn tacs => fn map_b => fn rel_b => fn pred_b => fn set_bs => fn consts => bnf_def Do_Inline (user_policy Note_Some) false I tacs wit_tac (SOME deads) map_b rel_b pred_b set_bs consts) tacss map_bs rel_bs pred_bs set_bss (((((((replicate n Binding.empty ~~ Ts) ~~ Imaps) ~~ Isetss_by_bnf) ~~ Ibds) ~~ Iwitss) ~~ map SOME Irels) ~~ map SOME Ipreds) lthy; val timer = time (timer "registered new datatypes as BNFs"); val ls' = if m = 1 then [0] else ls val Ibnf_common_notes = [(ctor_map_uniqueN, [ctor_Imap_unique_thm])] |> map (fn (thmN, thms) => ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])); val Ibnf_notes = [(ctor_mapN, map single ctor_Imap_thms), (ctor_relN, map single ctor_Irel_thms), (ctor_set_inclN, ctor_Iset_incl_thmss), (ctor_set_set_inclN, map flat ctor_set_Iset_incl_thmsss)] @ map2 (fn i => fn thms => (mk_ctor_setN i, map single thms)) ls' ctor_Iset_thmss |> maps (fn (thmN, thmss) => map2 (fn b => fn thms => ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])) bs thmss) in (timer, Ibnfs, (ctor_Imap_o_thms, ctor_Imap_thms), ctor_Imap_unique_thm, ctor_Iset_thmss', ctor_Irel_thms, Ibnf_common_notes @ Ibnf_notes, lthy) end; val ((((((xFs, yFs)), Iphis), activephis), activeIphis), _) = lthy |> mk_Frees "x" FTs ||>> mk_Frees "y" FTs' ||>> mk_Frees "R" IphiTs ||>> mk_Frees "S" activephiTs ||>> mk_Frees "IR" activeIphiTs; val ctor_fold_o_Imap_thms = mk_xtor_co_iter_o_map_thms Least_FP false m ctor_fold_unique_thm ctor_Imap_o_thms (map (mk_pointfree2 lthy) ctor_fold_thms) sym_map_comps map_cong0s; val Irels = if m = 0 then map HOLogic.eq_const Ts else map (mk_rel_of_bnf deads passiveAs passiveBs) Ibnfs; val Irel_induct_thm = mk_xtor_rel_co_induct_thm Least_FP rels activeIphis Irels Iphis xFs yFs ctors ctor's (fn {context = ctxt, prems = IHs} => mk_rel_induct_tac ctxt IHs m ctor_induct2_thm ks ctor_Irel_thms rel_mono_strong0s) lthy; val rels = map2 (fn Ds => mk_rel_of_bnf Ds allAs allBs') Dss bnfs; val ctor_fold_transfer_thms = mk_xtor_co_iter_transfer_thms Least_FP rels activephis activephis Irels Iphis (mk_folds passiveAs activeAs) (mk_folds passiveBs activeBs) (fn {context = ctxt, prems = _} => mk_fold_transfer_tac ctxt m Irel_induct_thm (map map_transfer_of_bnf bnfs) ctor_fold_thms) lthy; val timer = time (timer "relator induction"); fun mk_Ts As = map (typ_subst_atomic (passiveAs ~~ As)) Ts; val export = map (Morphism.term (Local_Theory.target_morphism lthy)) val ((recs, (ctor_rec_thms, ctor_rec_unique_thm, ctor_rec_o_Imap_thms, ctor_rec_transfer_thms)), lthy) = lthy |> derive_xtor_co_recs Least_FP external_bs mk_Ts (Dss, resDs) bnfs (export ctors) (export folds) ctor_fold_unique_thm ctor_fold_thms ctor_fold_transfer_thms ctor_Imap_thms ctor_Irel_thms (replicate n NONE); val timer = time (timer "recursor"); val common_notes = [(ctor_inductN, [ctor_induct_thm]), (ctor_induct2N, [ctor_induct2_thm]), (ctor_rel_inductN, [Irel_induct_thm])] |> map (fn (thmN, thms) => ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])); val notes = [(ctor_dtorN, ctor_dtor_thms), (ctor_exhaustN, ctor_exhaust_thms), (ctor_foldN, ctor_fold_thms), (ctor_fold_o_mapN, ctor_fold_o_Imap_thms), (ctor_fold_transferN, ctor_fold_transfer_thms), (ctor_fold_uniqueN, ctor_fold_unique_thms), (ctor_injectN, ctor_inject_thms), (dtor_ctorN, dtor_ctor_thms), (dtor_exhaustN, dtor_exhaust_thms), (dtor_injectN, dtor_inject_thms)] |> map (apsnd (map single)) |> maps (fn (thmN, thmss) => map2 (fn b => fn thms => ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])) bs thmss); val lthy' = lthy |> internals ? snd o Local_Theory.notes (common_notes @ notes @ Ibnf_notes); val fp_res = {Ts = Ts, bnfs = Ibnfs, pre_bnfs = bnfs, absT_infos = absT_infos, ctors = ctors, dtors = dtors, xtor_un_folds = folds, xtor_co_recs = export recs, xtor_co_induct = ctor_induct_thm, dtor_ctors = dtor_ctor_thms, ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms, dtor_injects = dtor_inject_thms, xtor_maps = ctor_Imap_thms, xtor_map_unique = ctor_Imap_unique_thm, xtor_setss = ctor_Iset_thmss', xtor_rels = ctor_Irel_thms, xtor_un_fold_thms = ctor_fold_thms, xtor_co_rec_thms = ctor_rec_thms, xtor_un_fold_unique = ctor_fold_unique_thm, xtor_co_rec_unique = ctor_rec_unique_thm, xtor_un_fold_o_maps = ctor_fold_o_Imap_thms, xtor_co_rec_o_maps = ctor_rec_o_Imap_thms, xtor_un_fold_transfers = ctor_fold_transfer_thms, xtor_co_rec_transfers = ctor_rec_transfer_thms, xtor_rel_co_induct = Irel_induct_thm, dtor_set_inducts = []}; in timer; (fp_res, lthy') end; val _ = Outer_Syntax.local_theory \<^command_keyword>\datatype\ "define inductive datatypes" (parse_co_datatype_cmd Least_FP construct_lfp); -val _ = Theory.setup (fp_antiquote_setup \<^binding>\datatype\); - end;