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