src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML
author blanchet
Tue Oct 01 14:05:25 2013 +0200 (2013-10-01)
changeset 54006 9fe1bd54d437
parent 53974 612505263257
child 54009 f138452e8265
permissions -rw-r--r--
renamed theory file
blanchet@53303
     1
(*  Title:      HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML
blanchet@53303
     2
    Author:     Lorenz Panny, TU Muenchen
blanchet@53303
     3
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@53303
     4
    Copyright   2013
blanchet@53303
     5
blanchet@53303
     6
Library for recursor and corecursor sugar.
blanchet@53303
     7
*)
blanchet@53303
     8
blanchet@53303
     9
signature BNF_FP_REC_SUGAR_UTIL =
blanchet@53303
    10
sig
blanchet@53303
    11
  datatype rec_call =
blanchet@53303
    12
    No_Rec of int |
blanchet@53303
    13
    Direct_Rec of int (*before*) * int (*after*) |
blanchet@53303
    14
    Indirect_Rec of int
blanchet@53303
    15
blanchet@53303
    16
  datatype corec_call =
blanchet@53303
    17
    Dummy_No_Corec of int |
blanchet@53303
    18
    No_Corec of int |
blanchet@53303
    19
    Direct_Corec of int (*stop?*) * int (*end*) * int (*continue*) |
blanchet@53303
    20
    Indirect_Corec of int
blanchet@53303
    21
blanchet@53303
    22
  type rec_ctr_spec =
blanchet@53303
    23
    {ctr: term,
blanchet@53303
    24
     offset: int,
blanchet@53303
    25
     calls: rec_call list,
blanchet@53303
    26
     rec_thm: thm}
blanchet@53303
    27
blanchet@53303
    28
  type corec_ctr_spec =
blanchet@53303
    29
    {ctr: term,
blanchet@53303
    30
     disc: term,
blanchet@53303
    31
     sels: term list,
blanchet@53303
    32
     pred: int option,
blanchet@53303
    33
     calls: corec_call list,
blanchet@53705
    34
     discI: thm,
blanchet@53705
    35
     sel_thms: thm list,
blanchet@53475
    36
     collapse: thm,
blanchet@53475
    37
     corec_thm: thm,
blanchet@53475
    38
     disc_corec: thm,
blanchet@53475
    39
     sel_corecs: thm list}
blanchet@53303
    40
blanchet@53303
    41
  type rec_spec =
blanchet@53303
    42
    {recx: term,
blanchet@53329
    43
     nested_map_idents: thm list,
blanchet@53303
    44
     nested_map_comps: thm list,
blanchet@53303
    45
     ctr_specs: rec_ctr_spec list}
blanchet@53303
    46
blanchet@53303
    47
  type corec_spec =
blanchet@53303
    48
    {corec: term,
blanchet@53475
    49
     nested_maps: thm list,
blanchet@53475
    50
     nested_map_idents: thm list,
blanchet@53475
    51
     nested_map_comps: thm list,
blanchet@53303
    52
     ctr_specs: corec_ctr_spec list}
blanchet@53303
    53
blanchet@53871
    54
  val s_not: term -> term
blanchet@53878
    55
  val mk_conjs: term list -> term
blanchet@53878
    56
  val mk_disjs: term list -> term
blanchet@53878
    57
  val s_not_disj: term -> term list
blanchet@53878
    58
  val negate_conj: term list -> term list
blanchet@53878
    59
  val negate_disj: term list -> term list
blanchet@53878
    60
blanchet@53303
    61
  val massage_indirect_rec_call: Proof.context -> (term -> bool) -> (typ -> typ -> term -> term) ->
blanchet@53303
    62
    typ list -> term -> term -> term -> term
blanchet@53890
    63
  val massage_direct_corec_call: Proof.context -> (term -> bool) -> (typ list -> term -> term) ->
blanchet@53890
    64
    typ list -> term -> term
blanchet@53303
    65
  val massage_indirect_corec_call: Proof.context -> (term -> bool) ->
blanchet@53890
    66
    (typ list -> typ -> typ -> term -> term) -> typ list -> typ -> term -> term
blanchet@53727
    67
  val expand_corec_code_rhs: Proof.context -> (term -> bool) -> typ list -> term -> term
blanchet@53890
    68
  val massage_corec_code_rhs: Proof.context -> (typ list -> term -> term list -> term) ->
blanchet@53890
    69
    typ list -> term -> term
blanchet@53871
    70
  val fold_rev_corec_code_rhs: Proof.context -> (term list -> term -> term list -> 'a -> 'a) ->
blanchet@53871
    71
    typ list -> term -> 'a -> 'a
blanchet@53909
    72
  val case_thms_of_term: Proof.context -> typ list -> term ->
blanchet@53925
    73
    thm list * thm list * thm list * thm list
blanchet@53878
    74
blanchet@53303
    75
  val rec_specs_of: binding list -> typ list -> typ list -> (term -> int list) ->
blanchet@53303
    76
    ((term * term list list) list) list -> local_theory ->
blanchet@53303
    77
    (bool * rec_spec list * typ list * thm * thm list) * local_theory
blanchet@53303
    78
  val corec_specs_of: binding list -> typ list -> typ list -> (term -> int list) ->
blanchet@53303
    79
    ((term * term list list) list) list -> local_theory ->
blanchet@53303
    80
    (bool * corec_spec list * typ list * thm * thm * thm list * thm list) * local_theory
blanchet@53303
    81
end;
blanchet@53303
    82
blanchet@53303
    83
structure BNF_FP_Rec_Sugar_Util : BNF_FP_REC_SUGAR_UTIL =
blanchet@53303
    84
struct
blanchet@53303
    85
blanchet@54006
    86
open Ctr_Sugar
blanchet@53303
    87
open BNF_Util
blanchet@53303
    88
open BNF_Def
blanchet@53303
    89
open BNF_FP_Util
blanchet@53303
    90
open BNF_FP_Def_Sugar
blanchet@53303
    91
open BNF_FP_N2M_Sugar
blanchet@53303
    92
blanchet@53303
    93
datatype rec_call =
blanchet@53303
    94
  No_Rec of int |
blanchet@53303
    95
  Direct_Rec of int * int |
blanchet@53303
    96
  Indirect_Rec of int;
blanchet@53303
    97
blanchet@53303
    98
datatype corec_call =
blanchet@53303
    99
  Dummy_No_Corec of int |
blanchet@53303
   100
  No_Corec of int |
blanchet@53303
   101
  Direct_Corec of int * int * int |
blanchet@53303
   102
  Indirect_Corec of int;
blanchet@53303
   103
blanchet@53303
   104
type rec_ctr_spec =
blanchet@53303
   105
  {ctr: term,
blanchet@53303
   106
   offset: int,
blanchet@53303
   107
   calls: rec_call list,
blanchet@53303
   108
   rec_thm: thm};
blanchet@53303
   109
blanchet@53303
   110
type corec_ctr_spec =
blanchet@53303
   111
  {ctr: term,
blanchet@53303
   112
   disc: term,
blanchet@53303
   113
   sels: term list,
blanchet@53303
   114
   pred: int option,
blanchet@53303
   115
   calls: corec_call list,
blanchet@53705
   116
   discI: thm,
blanchet@53705
   117
   sel_thms: thm list,
blanchet@53475
   118
   collapse: thm,
blanchet@53475
   119
   corec_thm: thm,
blanchet@53475
   120
   disc_corec: thm,
blanchet@53475
   121
   sel_corecs: thm list};
blanchet@53303
   122
blanchet@53303
   123
type rec_spec =
blanchet@53303
   124
  {recx: term,
blanchet@53329
   125
   nested_map_idents: thm list,
blanchet@53303
   126
   nested_map_comps: thm list,
blanchet@53303
   127
   ctr_specs: rec_ctr_spec list};
blanchet@53303
   128
blanchet@53303
   129
type corec_spec =
blanchet@53303
   130
  {corec: term,
blanchet@53475
   131
   nested_maps: thm list,
blanchet@53475
   132
   nested_map_idents: thm list,
blanchet@53475
   133
   nested_map_comps: thm list,
blanchet@53303
   134
   ctr_specs: corec_ctr_spec list};
blanchet@53303
   135
blanchet@53303
   136
val id_def = @{thm id_def};
blanchet@53303
   137
blanchet@53303
   138
exception AINT_NO_MAP of term;
blanchet@53303
   139
blanchet@53303
   140
fun ill_formed_rec_call ctxt t =
blanchet@53303
   141
  error ("Ill-formed recursive call: " ^ quote (Syntax.string_of_term ctxt t));
blanchet@53303
   142
fun ill_formed_corec_call ctxt t =
blanchet@53303
   143
  error ("Ill-formed corecursive call: " ^ quote (Syntax.string_of_term ctxt t));
blanchet@53303
   144
fun invalid_map ctxt t =
blanchet@53303
   145
  error ("Invalid map function in " ^ quote (Syntax.string_of_term ctxt t));
blanchet@53303
   146
fun unexpected_rec_call ctxt t =
blanchet@53303
   147
  error ("Unexpected recursive call: " ^ quote (Syntax.string_of_term ctxt t));
blanchet@53303
   148
fun unexpected_corec_call ctxt t =
blanchet@53303
   149
  error ("Unexpected corecursive call: " ^ quote (Syntax.string_of_term ctxt t));
blanchet@53303
   150
blanchet@53871
   151
fun s_not @{const True} = @{const False}
blanchet@53871
   152
  | s_not @{const False} = @{const True}
blanchet@53871
   153
  | s_not (@{const Not} $ t) = t
blanchet@53871
   154
  | s_not t = HOLogic.mk_not t
blanchet@53871
   155
blanchet@53878
   156
val mk_conjs = try (foldr1 HOLogic.mk_conj) #> the_default @{const True};
blanchet@53878
   157
val mk_disjs = try (foldr1 HOLogic.mk_disj) #> the_default @{const False};
blanchet@53878
   158
blanchet@53878
   159
val s_not_disj = map s_not o HOLogic.disjuncts;
blanchet@53878
   160
blanchet@53878
   161
fun negate_conj [t] = s_not_disj t
blanchet@53878
   162
  | negate_conj ts = [mk_disjs (map s_not ts)];
blanchet@53878
   163
blanchet@53878
   164
fun negate_disj [t] = s_not_disj t
blanchet@53878
   165
  | negate_disj ts = [mk_disjs (map (mk_conjs o s_not_disj) ts)];
blanchet@53878
   166
blanchet@53303
   167
fun factor_out_types ctxt massage destU U T =
blanchet@53303
   168
  (case try destU U of
blanchet@53303
   169
    SOME (U1, U2) => if U1 = T then massage T U2 else invalid_map ctxt
blanchet@53303
   170
  | NONE => invalid_map ctxt);
blanchet@53303
   171
blanchet@53303
   172
fun map_flattened_map_args ctxt s map_args fs =
blanchet@53303
   173
  let
blanchet@53303
   174
    val flat_fs = flatten_type_args_of_bnf (the (bnf_of ctxt s)) Term.dummy fs;
blanchet@53303
   175
    val flat_fs' = map_args flat_fs;
blanchet@53303
   176
  in
blanchet@53303
   177
    permute_like (op aconv) flat_fs fs flat_fs'
blanchet@53303
   178
  end;
blanchet@53303
   179
blanchet@53734
   180
fun massage_indirect_rec_call ctxt has_call raw_massage_fun bound_Ts y y' =
blanchet@53303
   181
  let
blanchet@53303
   182
    val typof = curry fastype_of1 bound_Ts;
blanchet@53303
   183
    val build_map_fst = build_map ctxt (fst_const o fst);
blanchet@53303
   184
blanchet@53303
   185
    val yT = typof y;
blanchet@53303
   186
    val yU = typof y';
blanchet@53303
   187
blanchet@53303
   188
    fun y_of_y' () = build_map_fst (yU, yT) $ y';
blanchet@53303
   189
    val elim_y = Term.map_aterms (fn t => if t = y then y_of_y' () else t);
blanchet@53303
   190
blanchet@53734
   191
    fun massage_direct_fun U T t =
blanchet@53734
   192
      if has_call t then factor_out_types ctxt raw_massage_fun HOLogic.dest_prodT U T t
blanchet@53734
   193
      else HOLogic.mk_comp (t, build_map_fst (U, T));
blanchet@53303
   194
blanchet@53303
   195
    fun massage_map (Type (_, Us)) (Type (s, Ts)) t =
blanchet@53303
   196
        (case try (dest_map ctxt s) t of
blanchet@53303
   197
          SOME (map0, fs) =>
blanchet@53303
   198
          let
blanchet@53303
   199
            val Type (_, ran_Ts) = range_type (typof t);
blanchet@53303
   200
            val map' = mk_map (length fs) Us ran_Ts map0;
blanchet@53303
   201
            val fs' = map_flattened_map_args ctxt s (map3 massage_map_or_map_arg Us Ts) fs;
blanchet@53303
   202
          in
blanchet@53870
   203
            Term.list_comb (map', fs')
blanchet@53303
   204
          end
blanchet@53303
   205
        | NONE => raise AINT_NO_MAP t)
blanchet@53303
   206
      | massage_map _ _ t = raise AINT_NO_MAP t
blanchet@53303
   207
    and massage_map_or_map_arg U T t =
blanchet@53303
   208
      if T = U then
blanchet@53303
   209
        if has_call t then unexpected_rec_call ctxt t else t
blanchet@53303
   210
      else
blanchet@53303
   211
        massage_map U T t
blanchet@53734
   212
        handle AINT_NO_MAP _ => massage_direct_fun U T t;
blanchet@53303
   213
blanchet@53303
   214
    fun massage_call (t as t1 $ t2) =
blanchet@53303
   215
        if t2 = y then
blanchet@53303
   216
          massage_map yU yT (elim_y t1) $ y'
blanchet@53303
   217
          handle AINT_NO_MAP t' => invalid_map ctxt t'
blanchet@53303
   218
        else
blanchet@53303
   219
          ill_formed_rec_call ctxt t
blanchet@53303
   220
      | massage_call t = if t = y then y_of_y' () else ill_formed_rec_call ctxt t;
blanchet@53303
   221
  in
blanchet@53724
   222
    massage_call
blanchet@53303
   223
  end;
blanchet@53303
   224
blanchet@53909
   225
fun fold_rev_let_if_case ctxt f bound_Ts t =
blanchet@53866
   226
  let
blanchet@53870
   227
    val thy = Proof_Context.theory_of ctxt;
blanchet@53870
   228
blanchet@53871
   229
    fun fld conds t =
blanchet@53866
   230
      (case Term.strip_comb t of
blanchet@53871
   231
        (Const (@{const_name Let}, _), [arg1, arg2]) => fld conds (betapply (arg2, arg1))
blanchet@53871
   232
      | (Const (@{const_name If}, _), [cond, then_branch, else_branch]) =>
blanchet@53887
   233
        fld (conds @ HOLogic.conjuncts cond) then_branch
blanchet@53879
   234
        o fld (conds @ s_not_disj cond) else_branch
blanchet@53896
   235
      | (Const (c, _), args as _ :: _ :: _) =>
blanchet@53896
   236
        let val n = num_binder_types (Sign.the_const_type thy c) - 1 in
blanchet@53924
   237
          if n >= 0 andalso n < length args then
blanchet@53896
   238
            (case fastype_of1 (bound_Ts, nth args n) of
blanchet@53896
   239
              Type (s, Ts) =>
blanchet@53896
   240
              (case dest_case ctxt s Ts t of
blanchet@53909
   241
                NONE => apsnd (f conds t)
blanchet@53896
   242
              | SOME (conds', branches) =>
blanchet@53909
   243
                apfst (cons s) o fold_rev (uncurry fld)
blanchet@53909
   244
                  (map (append conds o HOLogic.conjuncts) conds' ~~ branches))
blanchet@53909
   245
            | _ => apsnd (f conds t))
blanchet@53896
   246
          else
blanchet@53909
   247
            apsnd (f conds t)
blanchet@53866
   248
        end
blanchet@53909
   249
      | _ => apsnd (f conds t))
blanchet@53866
   250
  in
blanchet@53909
   251
    fld [] t o pair []
blanchet@53866
   252
  end;
blanchet@53866
   253
blanchet@53870
   254
fun case_of ctxt = ctr_sugar_of ctxt #> Option.map (fst o dest_Const o #casex);
blanchet@53870
   255
blanchet@53890
   256
fun massage_let_if_case ctxt has_call massage_leaf =
blanchet@53723
   257
  let
blanchet@53888
   258
    val thy = Proof_Context.theory_of ctxt;
blanchet@53888
   259
blanchet@53888
   260
    fun check_no_call t = if has_call t then unexpected_corec_call ctxt t else ();
blanchet@53835
   261
blanchet@53895
   262
    fun massage_abs bound_Ts (Abs (s, T, t)) = Abs (s, T, massage_abs (T :: bound_Ts) t)
blanchet@53893
   263
      | massage_abs bound_Ts t = massage_rec bound_Ts t
blanchet@53893
   264
    and massage_rec bound_Ts t =
blanchet@53890
   265
      let val typof = curry fastype_of1 bound_Ts in
blanchet@53890
   266
        (case Term.strip_comb t of
blanchet@53890
   267
          (Const (@{const_name Let}, _), [arg1, arg2]) =>
blanchet@53890
   268
          massage_rec bound_Ts (betapply (arg2, arg1))
blanchet@53893
   269
        | (Const (@{const_name If}, _), obj :: (branches as [_, _])) =>
blanchet@53890
   270
          let val branches' = map (massage_rec bound_Ts) branches in
blanchet@53890
   271
            Term.list_comb (If_const (typof (hd branches')) $ tap check_no_call obj, branches')
blanchet@53890
   272
          end
blanchet@53896
   273
        | (Const (c, _), args as _ :: _ :: _) =>
blanchet@53896
   274
          let
blanchet@53896
   275
            val gen_T = Sign.the_const_type thy c;
blanchet@53896
   276
            val (gen_branch_Ts, gen_body_fun_T) = strip_fun_type gen_T;
blanchet@53896
   277
            val n = length gen_branch_Ts;
blanchet@53896
   278
          in
blanchet@53924
   279
            if n < length args then
blanchet@53896
   280
              (case gen_body_fun_T of
blanchet@53896
   281
                Type (_, [Type (T_name, _), _]) =>
blanchet@53896
   282
                if case_of ctxt T_name = SOME c then
blanchet@53891
   283
                  let
blanchet@53891
   284
                    val (branches, obj_leftovers) = chop n args;
blanchet@53893
   285
                    val branches' = map (massage_abs bound_Ts o Envir.eta_long bound_Ts) branches;
blanchet@53896
   286
                    val branch_Ts' = map typof branches';
blanchet@53896
   287
                    val casex' = Const (c, branch_Ts' ---> map typof obj_leftovers --->
blanchet@53896
   288
                      snd (strip_typeN (num_binder_types (hd gen_branch_Ts)) (hd branch_Ts')));
blanchet@53891
   289
                  in
blanchet@53895
   290
                    Term.list_comb (casex', branches' @ tap (List.app check_no_call) obj_leftovers)
blanchet@53891
   291
                  end
blanchet@53891
   292
                else
blanchet@53891
   293
                  massage_leaf bound_Ts t
blanchet@53891
   294
              | _ => massage_leaf bound_Ts t)
blanchet@53891
   295
            else
blanchet@53891
   296
              massage_leaf bound_Ts t
blanchet@53890
   297
          end
blanchet@53890
   298
        | _ => massage_leaf bound_Ts t)
blanchet@53890
   299
      end
blanchet@53723
   300
  in
blanchet@53723
   301
    massage_rec
blanchet@53723
   302
  end;
blanchet@53303
   303
blanchet@53866
   304
val massage_direct_corec_call = massage_let_if_case;
blanchet@53303
   305
blanchet@53734
   306
fun massage_indirect_corec_call ctxt has_call raw_massage_call bound_Ts U t =
blanchet@53303
   307
  let
panny@53411
   308
    val build_map_Inl = build_map ctxt (uncurry Inl_const o dest_sumT o snd)
blanchet@53303
   309
blanchet@53890
   310
    fun massage_direct_call bound_Ts U T t =
blanchet@53890
   311
      if has_call t then factor_out_types ctxt (raw_massage_call bound_Ts) dest_sumT U T t
panny@53411
   312
      else build_map_Inl (T, U) $ t;
blanchet@53303
   313
blanchet@53890
   314
    fun massage_direct_fun bound_Ts U T t =
blanchet@53890
   315
      let
blanchet@53890
   316
        val var = Var ((Name.uu, Term.maxidx_of_term t + 1),
blanchet@53890
   317
          domain_type (fastype_of1 (bound_Ts, t)));
blanchet@53890
   318
      in
blanchet@53890
   319
        Term.lambda var (massage_direct_call bound_Ts U T (t $ var))
blanchet@53303
   320
      end;
blanchet@53303
   321
blanchet@53890
   322
    fun massage_map bound_Ts (Type (_, Us)) (Type (s, Ts)) t =
blanchet@53303
   323
        (case try (dest_map ctxt s) t of
blanchet@53303
   324
          SOME (map0, fs) =>
blanchet@53303
   325
          let
blanchet@53890
   326
            val Type (_, dom_Ts) = domain_type (fastype_of1 (bound_Ts, t));
blanchet@53303
   327
            val map' = mk_map (length fs) dom_Ts Us map0;
blanchet@53890
   328
            val fs' =
blanchet@53890
   329
              map_flattened_map_args ctxt s (map3 (massage_map_or_map_arg bound_Ts) Us Ts) fs;
blanchet@53303
   330
          in
blanchet@53870
   331
            Term.list_comb (map', fs')
blanchet@53303
   332
          end
blanchet@53303
   333
        | NONE => raise AINT_NO_MAP t)
blanchet@53890
   334
      | massage_map _ _ _ t = raise AINT_NO_MAP t
blanchet@53890
   335
    and massage_map_or_map_arg bound_Ts U T t =
blanchet@53303
   336
      if T = U then
blanchet@53303
   337
        if has_call t then unexpected_corec_call ctxt t else t
blanchet@53303
   338
      else
blanchet@53890
   339
        massage_map bound_Ts U T t
blanchet@53890
   340
        handle AINT_NO_MAP _ => massage_direct_fun bound_Ts U T t;
blanchet@53303
   341
blanchet@53890
   342
    fun massage_call bound_Ts U T =
blanchet@53890
   343
      massage_let_if_case ctxt has_call (fn bound_Ts => fn t =>
blanchet@53732
   344
        if has_call t then
blanchet@53732
   345
          (case U of
blanchet@53732
   346
            Type (s, Us) =>
blanchet@53732
   347
            (case try (dest_ctr ctxt s) t of
blanchet@53732
   348
              SOME (f, args) =>
blanchet@53890
   349
              let
blanchet@53890
   350
                val typof = curry fastype_of1 bound_Ts;
blanchet@53890
   351
                val f' = mk_ctr Us f
blanchet@53890
   352
                val f'_T = typof f';
blanchet@53890
   353
                val arg_Ts = map typof args;
blanchet@53890
   354
              in
blanchet@53890
   355
                Term.list_comb (f', map3 (massage_call bound_Ts) (binder_types f'_T) arg_Ts args)
blanchet@53732
   356
              end
blanchet@53732
   357
            | NONE =>
blanchet@53732
   358
              (case t of
blanchet@53732
   359
                t1 $ t2 =>
blanchet@53732
   360
                (if has_call t2 then
blanchet@53890
   361
                  massage_direct_call bound_Ts U T t
blanchet@53732
   362
                else
blanchet@53890
   363
                  massage_map bound_Ts U T t1 $ t2
blanchet@53890
   364
                  handle AINT_NO_MAP _ => massage_direct_call bound_Ts U T t)
blanchet@53890
   365
              | Abs (s, T', t') =>
blanchet@53890
   366
                Abs (s, T', massage_call (T' :: bound_Ts) (range_type U) (range_type T) t')
blanchet@53890
   367
              | _ => massage_direct_call bound_Ts U T t))
blanchet@53732
   368
          | _ => ill_formed_corec_call ctxt t)
blanchet@53732
   369
        else
blanchet@53889
   370
          build_map_Inl (T, U) $ t) bound_Ts;
blanchet@53960
   371
blanchet@53960
   372
    val T = fastype_of1 (bound_Ts, t);
blanchet@53303
   373
  in
blanchet@53960
   374
    if has_call t then massage_call bound_Ts U T t else build_map_Inl (T, U) $ t
blanchet@53303
   375
  end;
blanchet@53303
   376
blanchet@53727
   377
fun expand_ctr_term ctxt s Ts t =
blanchet@53867
   378
  (case ctr_sugar_of ctxt s of
blanchet@53870
   379
    SOME {ctrs, casex, ...} =>
blanchet@53870
   380
    Term.list_comb (mk_case Ts (Type (s, Ts)) casex, map (mk_ctr Ts) ctrs) $ t
blanchet@53727
   381
  | NONE => raise Fail "expand_ctr_term");
blanchet@53726
   382
blanchet@53727
   383
fun expand_corec_code_rhs ctxt has_call bound_Ts t =
blanchet@53727
   384
  (case fastype_of1 (bound_Ts, t) of
blanchet@53889
   385
    Type (s, Ts) =>
blanchet@53893
   386
    massage_let_if_case ctxt has_call (fn _ => fn t =>
blanchet@53892
   387
      if can (dest_ctr ctxt s) t then t else expand_ctr_term ctxt s Ts t) bound_Ts t
blanchet@53727
   388
  | _ => raise Fail "expand_corec_code_rhs");
blanchet@53727
   389
blanchet@53727
   390
fun massage_corec_code_rhs ctxt massage_ctr =
blanchet@53890
   391
  massage_let_if_case ctxt (K false)
blanchet@53890
   392
    (fn bound_Ts => uncurry (massage_ctr bound_Ts) o Term.strip_comb);
blanchet@53865
   393
blanchet@53871
   394
fun fold_rev_corec_code_rhs ctxt f =
blanchet@53909
   395
  snd ooo fold_rev_let_if_case ctxt (fn conds => uncurry (f conds) o Term.strip_comb);
blanchet@53909
   396
blanchet@53909
   397
fun case_thms_of_term ctxt bound_Ts t =
blanchet@53909
   398
  let
blanchet@53909
   399
    val (caseT_names, _) = fold_rev_let_if_case ctxt (K (K I)) bound_Ts t ();
blanchet@53909
   400
    val ctr_sugars = map (the o ctr_sugar_of ctxt) caseT_names;
blanchet@53909
   401
  in
blanchet@53925
   402
    (maps #distincts ctr_sugars, maps #discIs ctr_sugars, maps #sel_splits ctr_sugars,
blanchet@53925
   403
     maps #sel_split_asms ctr_sugars)
blanchet@53909
   404
  end;
blanchet@53731
   405
blanchet@53303
   406
fun indexed xs h = let val h' = h + length xs in (h upto h' - 1, h') end;
blanchet@53303
   407
fun indexedd xss = fold_map indexed xss;
blanchet@53303
   408
fun indexeddd xsss = fold_map indexedd xsss;
blanchet@53303
   409
fun indexedddd xssss = fold_map indexeddd xssss;
blanchet@53303
   410
blanchet@53303
   411
fun find_index_eq hs h = find_index (curry (op =) h) hs;
blanchet@53303
   412
blanchet@53476
   413
(*FIXME: remove special cases for products and sum once they are registered as datatypes*)
blanchet@53476
   414
fun map_thms_of_typ ctxt (Type (s, _)) =
blanchet@53476
   415
    if s = @{type_name prod} then
blanchet@53476
   416
      @{thms map_pair_simp}
blanchet@53476
   417
    else if s = @{type_name sum} then
blanchet@53476
   418
      @{thms sum_map.simps}
blanchet@53476
   419
    else
blanchet@53476
   420
      (case fp_sugar_of ctxt s of
blanchet@53476
   421
        SOME {index, mapss, ...} => nth mapss index
blanchet@53476
   422
      | NONE => [])
blanchet@53476
   423
  | map_thms_of_typ _ _ = [];
blanchet@53476
   424
blanchet@53303
   425
val lose_co_rec = false (*FIXME: try true?*);
blanchet@53303
   426
blanchet@53303
   427
fun rec_specs_of bs arg_Ts res_Ts get_indices callssss0 lthy =
blanchet@53303
   428
  let
blanchet@53303
   429
    val thy = Proof_Context.theory_of lthy;
blanchet@53303
   430
blanchet@53746
   431
    val ((missing_arg_Ts, perm0_kks,
blanchet@53303
   432
          fp_sugars as {nested_bnfs, fp_res = {xtor_co_iterss = ctor_iters1 :: _, ...},
blanchet@53746
   433
            co_inducts = [induct_thm], ...} :: _, (lfp_sugar_thms, _)), lthy') =
blanchet@53303
   434
      nested_to_mutual_fps lose_co_rec Least_FP bs arg_Ts get_indices callssss0 lthy;
blanchet@53303
   435
blanchet@53303
   436
    val perm_fp_sugars = sort (int_ord o pairself #index) fp_sugars;
blanchet@53303
   437
blanchet@53303
   438
    val indices = map #index fp_sugars;
blanchet@53303
   439
    val perm_indices = map #index perm_fp_sugars;
blanchet@53303
   440
blanchet@53303
   441
    val perm_ctrss = map (#ctrs o of_fp_sugar #ctr_sugars) perm_fp_sugars;
blanchet@53303
   442
    val perm_ctr_Tsss = map (map (binder_types o fastype_of)) perm_ctrss;
blanchet@53303
   443
    val perm_fpTs = map (body_type o fastype_of o hd) perm_ctrss;
blanchet@53303
   444
blanchet@53303
   445
    val nn0 = length arg_Ts;
blanchet@53303
   446
    val nn = length perm_fpTs;
blanchet@53303
   447
    val kks = 0 upto nn - 1;
blanchet@53303
   448
    val perm_ns = map length perm_ctr_Tsss;
blanchet@53303
   449
    val perm_mss = map (map length) perm_ctr_Tsss;
blanchet@53303
   450
blanchet@53303
   451
    val perm_Cs = map (body_type o fastype_of o co_rec_of o of_fp_sugar (#xtor_co_iterss o #fp_res))
blanchet@53303
   452
      perm_fp_sugars;
blanchet@53592
   453
    val perm_fun_arg_Tssss =
blanchet@53592
   454
      mk_iter_fun_arg_types perm_ctr_Tsss perm_ns perm_mss (co_rec_of ctor_iters1);
blanchet@53303
   455
blanchet@53303
   456
    fun unpermute0 perm0_xs = permute_like (op =) perm0_kks kks perm0_xs;
blanchet@53303
   457
    fun unpermute perm_xs = permute_like (op =) perm_indices indices perm_xs;
blanchet@53303
   458
blanchet@53303
   459
    val induct_thms = unpermute0 (conj_dests nn induct_thm);
blanchet@53303
   460
blanchet@53303
   461
    val fpTs = unpermute perm_fpTs;
blanchet@53303
   462
    val Cs = unpermute perm_Cs;
blanchet@53303
   463
blanchet@53303
   464
    val As_rho = tvar_subst thy (take nn0 fpTs) arg_Ts;
blanchet@53303
   465
    val Cs_rho = map (fst o dest_TVar) Cs ~~ pad_list HOLogic.unitT nn res_Ts;
blanchet@53303
   466
blanchet@53303
   467
    val substA = Term.subst_TVars As_rho;
blanchet@53303
   468
    val substAT = Term.typ_subst_TVars As_rho;
blanchet@53303
   469
    val substCT = Term.typ_subst_TVars Cs_rho;
blanchet@53303
   470
blanchet@53303
   471
    val perm_Cs' = map substCT perm_Cs;
blanchet@53303
   472
blanchet@53303
   473
    fun offset_of_ctr 0 _ = 0
wenzelm@53974
   474
      | offset_of_ctr n (({ctrs, ...} : ctr_sugar) :: ctr_sugars) =
blanchet@53303
   475
        length ctrs + offset_of_ctr (n - 1) ctr_sugars;
blanchet@53303
   476
blanchet@53303
   477
    fun call_of [i] [T] = (if exists_subtype_in Cs T then Indirect_Rec else No_Rec) i
blanchet@53303
   478
      | call_of [i, i'] _ = Direct_Rec (i, i');
blanchet@53303
   479
blanchet@53303
   480
    fun mk_ctr_spec ctr offset fun_arg_Tss rec_thm =
blanchet@53303
   481
      let
blanchet@53303
   482
        val (fun_arg_hss, _) = indexedd fun_arg_Tss 0;
blanchet@53303
   483
        val fun_arg_hs = flat_rec_arg_args fun_arg_hss;
blanchet@53303
   484
        val fun_arg_iss = map (map (find_index_eq fun_arg_hs)) fun_arg_hss;
blanchet@53303
   485
      in
blanchet@53303
   486
        {ctr = substA ctr, offset = offset, calls = map2 call_of fun_arg_iss fun_arg_Tss,
blanchet@53303
   487
         rec_thm = rec_thm}
blanchet@53303
   488
      end;
blanchet@53303
   489
wenzelm@53974
   490
    fun mk_ctr_specs index (ctr_sugars : ctr_sugar list) iter_thmsss =
blanchet@53303
   491
      let
blanchet@53303
   492
        val ctrs = #ctrs (nth ctr_sugars index);
blanchet@53303
   493
        val rec_thmss = co_rec_of (nth iter_thmsss index);
blanchet@53303
   494
        val k = offset_of_ctr index ctr_sugars;
blanchet@53303
   495
        val n = length ctrs;
blanchet@53303
   496
      in
blanchet@53303
   497
        map4 mk_ctr_spec ctrs (k upto k + n - 1) (nth perm_fun_arg_Tssss index) rec_thmss
blanchet@53303
   498
      end;
blanchet@53303
   499
wenzelm@53974
   500
    fun mk_spec ({T, index, ctr_sugars, co_iterss = iterss, co_iter_thmsss = iter_thmsss, ...}
wenzelm@53974
   501
      : fp_sugar) =
blanchet@53303
   502
      {recx = mk_co_iter thy Least_FP (substAT T) perm_Cs' (co_rec_of (nth iterss index)),
blanchet@53329
   503
       nested_map_idents = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nested_bnfs,
blanchet@53303
   504
       nested_map_comps = map map_comp_of_bnf nested_bnfs,
blanchet@53303
   505
       ctr_specs = mk_ctr_specs index ctr_sugars iter_thmsss};
blanchet@53303
   506
  in
blanchet@53746
   507
    ((is_some lfp_sugar_thms, map mk_spec fp_sugars, missing_arg_Ts, induct_thm, induct_thms),
blanchet@53746
   508
     lthy')
blanchet@53303
   509
  end;
blanchet@53303
   510
blanchet@53303
   511
fun corec_specs_of bs arg_Ts res_Ts get_indices callssss0 lthy =
blanchet@53303
   512
  let
blanchet@53303
   513
    val thy = Proof_Context.theory_of lthy;
blanchet@53303
   514
blanchet@53746
   515
    val ((missing_res_Ts, perm0_kks,
blanchet@53475
   516
          fp_sugars as {nested_bnfs, fp_res = {xtor_co_iterss = dtor_coiters1 :: _, ...},
blanchet@53746
   517
            co_inducts = coinduct_thms, ...} :: _, (_, gfp_sugar_thms)), lthy') =
blanchet@53303
   518
      nested_to_mutual_fps lose_co_rec Greatest_FP bs res_Ts get_indices callssss0 lthy;
blanchet@53303
   519
blanchet@53303
   520
    val perm_fp_sugars = sort (int_ord o pairself #index) fp_sugars;
blanchet@53303
   521
blanchet@53303
   522
    val indices = map #index fp_sugars;
blanchet@53303
   523
    val perm_indices = map #index perm_fp_sugars;
blanchet@53303
   524
blanchet@53303
   525
    val perm_ctrss = map (#ctrs o of_fp_sugar #ctr_sugars) perm_fp_sugars;
blanchet@53303
   526
    val perm_ctr_Tsss = map (map (binder_types o fastype_of)) perm_ctrss;
blanchet@53303
   527
    val perm_fpTs = map (body_type o fastype_of o hd) perm_ctrss;
blanchet@53303
   528
blanchet@53303
   529
    val nn0 = length res_Ts;
blanchet@53303
   530
    val nn = length perm_fpTs;
blanchet@53303
   531
    val kks = 0 upto nn - 1;
blanchet@53303
   532
    val perm_ns = map length perm_ctr_Tsss;
blanchet@53303
   533
blanchet@53303
   534
    val perm_Cs = map (domain_type o body_fun_type o fastype_of o co_rec_of o
blanchet@53303
   535
      of_fp_sugar (#xtor_co_iterss o #fp_res)) perm_fp_sugars;
blanchet@53303
   536
    val (perm_p_Tss, (perm_q_Tssss, _, perm_f_Tssss, _)) =
blanchet@53591
   537
      mk_coiter_fun_arg_types perm_ctr_Tsss perm_Cs perm_ns (co_rec_of dtor_coiters1);
blanchet@53303
   538
blanchet@53303
   539
    val (perm_p_hss, h) = indexedd perm_p_Tss 0;
blanchet@53303
   540
    val (perm_q_hssss, h') = indexedddd perm_q_Tssss h;
blanchet@53303
   541
    val (perm_f_hssss, _) = indexedddd perm_f_Tssss h';
blanchet@53303
   542
blanchet@53303
   543
    val fun_arg_hs =
blanchet@53303
   544
      flat (map3 flat_corec_preds_predsss_gettersss perm_p_hss perm_q_hssss perm_f_hssss);
blanchet@53303
   545
blanchet@53303
   546
    fun unpermute0 perm0_xs = permute_like (op =) perm0_kks kks perm0_xs;
blanchet@53303
   547
    fun unpermute perm_xs = permute_like (op =) perm_indices indices perm_xs;
blanchet@53303
   548
blanchet@53303
   549
    val coinduct_thmss = map (unpermute0 o conj_dests nn) coinduct_thms;
blanchet@53303
   550
blanchet@53303
   551
    val p_iss = map (map (find_index_eq fun_arg_hs)) (unpermute perm_p_hss);
blanchet@53303
   552
    val q_issss = map (map (map (map (find_index_eq fun_arg_hs)))) (unpermute perm_q_hssss);
blanchet@53303
   553
    val f_issss = map (map (map (map (find_index_eq fun_arg_hs)))) (unpermute perm_f_hssss);
blanchet@53303
   554
blanchet@53303
   555
    val f_Tssss = unpermute perm_f_Tssss;
blanchet@53303
   556
    val fpTs = unpermute perm_fpTs;
blanchet@53303
   557
    val Cs = unpermute perm_Cs;
blanchet@53303
   558
blanchet@53303
   559
    val As_rho = tvar_subst thy (take nn0 fpTs) res_Ts;
blanchet@53303
   560
    val Cs_rho = map (fst o dest_TVar) Cs ~~ pad_list HOLogic.unitT nn arg_Ts;
blanchet@53303
   561
blanchet@53303
   562
    val substA = Term.subst_TVars As_rho;
blanchet@53303
   563
    val substAT = Term.typ_subst_TVars As_rho;
blanchet@53303
   564
    val substCT = Term.typ_subst_TVars Cs_rho;
blanchet@53303
   565
blanchet@53303
   566
    val perm_Cs' = map substCT perm_Cs;
blanchet@53303
   567
blanchet@53303
   568
    fun call_of nullary [] [g_i] [Type (@{type_name fun}, [_, T])] =
blanchet@53303
   569
        (if exists_subtype_in Cs T then Indirect_Corec
blanchet@53303
   570
         else if nullary then Dummy_No_Corec
blanchet@53303
   571
         else No_Corec) g_i
blanchet@53303
   572
      | call_of _ [q_i] [g_i, g_i'] _ = Direct_Corec (q_i, g_i, g_i');
blanchet@53303
   573
blanchet@53705
   574
    fun mk_ctr_spec ctr disc sels p_ho q_iss f_iss f_Tss discI sel_thms collapse corec_thm
blanchet@53705
   575
        disc_corec sel_corecs =
blanchet@53303
   576
      let val nullary = not (can dest_funT (fastype_of ctr)) in
blanchet@53303
   577
        {ctr = substA ctr, disc = substA disc, sels = map substA sels, pred = p_ho,
blanchet@53705
   578
         calls = map3 (call_of nullary) q_iss f_iss f_Tss, discI = discI, sel_thms = sel_thms,
blanchet@53705
   579
         collapse = collapse, corec_thm = corec_thm, disc_corec = disc_corec,
blanchet@53705
   580
         sel_corecs = sel_corecs}
blanchet@53303
   581
      end;
blanchet@53303
   582
wenzelm@53974
   583
    fun mk_ctr_specs index (ctr_sugars : ctr_sugar list) p_is q_isss f_isss f_Tsss
wenzelm@53974
   584
        coiter_thmsss disc_coitersss sel_coiterssss =
blanchet@53303
   585
      let
blanchet@53303
   586
        val ctrs = #ctrs (nth ctr_sugars index);
blanchet@53303
   587
        val discs = #discs (nth ctr_sugars index);
blanchet@53303
   588
        val selss = #selss (nth ctr_sugars index);
blanchet@53303
   589
        val p_ios = map SOME p_is @ [NONE];
blanchet@53705
   590
        val discIs = #discIs (nth ctr_sugars index);
blanchet@53705
   591
        val sel_thmss = #sel_thmss (nth ctr_sugars index);
blanchet@53475
   592
        val collapses = #collapses (nth ctr_sugars index);
blanchet@53475
   593
        val corec_thms = co_rec_of (nth coiter_thmsss index);
blanchet@53741
   594
        val disc_corecs = co_rec_of (nth disc_coitersss index);
blanchet@53475
   595
        val sel_corecss = co_rec_of (nth sel_coiterssss index);
blanchet@53303
   596
      in
blanchet@53705
   597
        map13 mk_ctr_spec ctrs discs selss p_ios q_isss f_isss f_Tsss discIs sel_thmss collapses
blanchet@53705
   598
          corec_thms disc_corecs sel_corecss
blanchet@53303
   599
      end;
blanchet@53303
   600
wenzelm@53974
   601
    fun mk_spec ({T, index, ctr_sugars, co_iterss = coiterss, co_iter_thmsss = coiter_thmsss,
wenzelm@53974
   602
          disc_co_itersss = disc_coitersss, sel_co_iterssss = sel_coiterssss, ...} : fp_sugar)
blanchet@53303
   603
        p_is q_isss f_isss f_Tsss =
blanchet@53303
   604
      {corec = mk_co_iter thy Greatest_FP (substAT T) perm_Cs' (co_rec_of (nth coiterss index)),
blanchet@53476
   605
       nested_maps = maps (map_thms_of_typ lthy o T_of_bnf) nested_bnfs,
blanchet@53475
   606
       nested_map_idents = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nested_bnfs,
blanchet@53475
   607
       nested_map_comps = map map_comp_of_bnf nested_bnfs,
blanchet@53475
   608
       ctr_specs = mk_ctr_specs index ctr_sugars p_is q_isss f_isss f_Tsss coiter_thmsss
blanchet@53475
   609
         disc_coitersss sel_coiterssss};
blanchet@53303
   610
  in
blanchet@53746
   611
    ((is_some gfp_sugar_thms, map5 mk_spec fp_sugars p_iss q_issss f_issss f_Tssss, missing_res_Ts,
blanchet@53303
   612
      co_induct_of coinduct_thms, strong_co_induct_of coinduct_thms, co_induct_of coinduct_thmss,
blanchet@53303
   613
      strong_co_induct_of coinduct_thmss), lthy')
blanchet@53303
   614
  end;
blanchet@53303
   615
blanchet@53303
   616
end;