src/HOL/Tools/BNF/bnf_comp.ML
author traytel
Thu, 11 Dec 2014 14:01:40 +0100
changeset 59131 894d613f7f7c
parent 59058 a78612c67ec0
child 59710 4aa63424ba89
permissions -rw-r--r--
respect order of deads when retrieving bnfs from the database
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
55061
a0adf838e2d1 adjusted comments
blanchet
parents: 55060
diff changeset
     1
(*  Title:      HOL/Tools/BNF/bnf_comp.ML
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
     2
    Author:     Dmitriy Traytel, TU Muenchen
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
     3
    Author:     Jasmin Blanchette, TU Muenchen
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
     4
    Copyright   2012
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
     5
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
     6
Composition of bounded natural functors.
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
     7
*)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
     8
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
     9
signature BNF_COMP =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    10
sig
51837
087498724486 lowercase type constructor, for consistency (cf. fp_result not FP_result nor FP_Result)
blanchet
parents: 51782
diff changeset
    11
  val ID_bnf: BNF_Def.bnf
087498724486 lowercase type constructor, for consistency (cf. fp_result not FP_result nor FP_Result)
blanchet
parents: 51782
diff changeset
    12
  val DEADID_bnf: BNF_Def.bnf
49585
5c4a12550491 generate high-level "maps", "sets", and "rels" properties
blanchet
parents: 49538
diff changeset
    13
55706
064c7c249f55 added BNF cache (within one definition)
blanchet
parents: 55705
diff changeset
    14
  type comp_cache
49502
92a7c1842c78 tuned a few ML names
blanchet
parents: 49463
diff changeset
    15
  type unfold_set
55706
064c7c249f55 added BNF cache (within one definition)
blanchet
parents: 55705
diff changeset
    16
064c7c249f55 added BNF cache (within one definition)
blanchet
parents: 55705
diff changeset
    17
  val empty_comp_cache: comp_cache
49502
92a7c1842c78 tuned a few ML names
blanchet
parents: 49463
diff changeset
    18
  val empty_unfolds: unfold_set
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    19
53222
8b159677efb5 better error message
blanchet
parents: 53040
diff changeset
    20
  exception BAD_DEAD of typ * typ
8b159677efb5 better error message
blanchet
parents: 53040
diff changeset
    21
55856
bddaada24074 got rid of automatically generated fold constant and theorems (to reduce overhead)
blanchet
parents: 55855
diff changeset
    22
  val bnf_of_typ: BNF_Def.inline_policy -> (binding -> binding) ->
55703
a21069381ba5 optimization of 'bnf_of_typ' if all variables are dead
blanchet
parents: 55480
diff changeset
    23
    ((string * sort) list list -> (string * sort) list) -> (string * sort) list ->
55904
0ef30d52c5e4 more caching in composition pipeline
blanchet
parents: 55900
diff changeset
    24
    (string * sort) list -> typ -> (comp_cache * unfold_set) * local_theory ->
0ef30d52c5e4 more caching in composition pipeline
blanchet
parents: 55900
diff changeset
    25
    (BNF_Def.bnf * (typ list * typ list)) * ((comp_cache * unfold_set) * local_theory)
49014
332e5e661675 have "bnf_of_typ" command seal the BNF
blanchet
parents: 48975
diff changeset
    26
  val default_comp_sort: (string * sort) list list -> (string * sort) list
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    27
  val normalize_bnfs: (int -> binding -> binding) -> ''a list list -> ''a list ->
55904
0ef30d52c5e4 more caching in composition pipeline
blanchet
parents: 55900
diff changeset
    28
    (''a list list -> ''a list) -> BNF_Def.bnf list -> (comp_cache * unfold_set) * local_theory ->
0ef30d52c5e4 more caching in composition pipeline
blanchet
parents: 55900
diff changeset
    29
    (int list list * ''a list) * (BNF_Def.bnf list * ((comp_cache * unfold_set) * local_theory))
55803
74d3fe9031d8 joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents: 55707
diff changeset
    30
74d3fe9031d8 joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents: 55707
diff changeset
    31
  type absT_info =
74d3fe9031d8 joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents: 55707
diff changeset
    32
    {absT: typ,
74d3fe9031d8 joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents: 55707
diff changeset
    33
     repT: typ,
74d3fe9031d8 joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents: 55707
diff changeset
    34
     abs: term,
74d3fe9031d8 joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents: 55707
diff changeset
    35
     rep: term,
74d3fe9031d8 joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents: 55707
diff changeset
    36
     abs_inject: thm,
74d3fe9031d8 joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents: 55707
diff changeset
    37
     abs_inverse: thm,
74d3fe9031d8 joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents: 55707
diff changeset
    38
     type_definition: thm}
74d3fe9031d8 joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents: 55707
diff changeset
    39
74d3fe9031d8 joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents: 55707
diff changeset
    40
  val morph_absT_info: morphism -> absT_info -> absT_info
74d3fe9031d8 joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents: 55707
diff changeset
    41
  val mk_absT: theory -> typ -> typ -> typ -> typ
74d3fe9031d8 joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents: 55707
diff changeset
    42
  val mk_repT: typ -> typ -> typ -> typ
74d3fe9031d8 joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents: 55707
diff changeset
    43
  val mk_abs: typ -> term -> term
74d3fe9031d8 joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents: 55707
diff changeset
    44
  val mk_rep: typ -> term -> term
58332
be0f5d8d511b imported patch phantoms
blanchet
parents: 58297
diff changeset
    45
  val seal_bnf: (binding -> binding) -> unfold_set -> binding -> bool -> typ list -> BNF_Def.bnf ->
55904
0ef30d52c5e4 more caching in composition pipeline
blanchet
parents: 55900
diff changeset
    46
    local_theory -> (BNF_Def.bnf * (typ list * absT_info)) * local_theory
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    47
end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    48
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    49
structure BNF_Comp : BNF_COMP =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    50
struct
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    51
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    52
open BNF_Def
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    53
open BNF_Util
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    54
open BNF_Tactics
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    55
open BNF_Comp_Tactics
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    56
58128
43a1ba26a8cb renamed BNF theories
blanchet
parents: 57890
diff changeset
    57
val ID_bnf = the (bnf_of @{context} "BNF_Composition.ID");
43a1ba26a8cb renamed BNF theories
blanchet
parents: 57890
diff changeset
    58
val DEADID_bnf = the (bnf_of @{context} "BNF_Composition.DEADID");
49585
5c4a12550491 generate high-level "maps", "sets", and "rels" properties
blanchet
parents: 49538
diff changeset
    59
55706
064c7c249f55 added BNF cache (within one definition)
blanchet
parents: 55705
diff changeset
    60
type comp_cache = (bnf * (typ list * typ list)) Typtab.table;
064c7c249f55 added BNF cache (within one definition)
blanchet
parents: 55705
diff changeset
    61
55904
0ef30d52c5e4 more caching in composition pipeline
blanchet
parents: 55900
diff changeset
    62
fun key_of_types s Ts = Type (s, Ts);
0ef30d52c5e4 more caching in composition pipeline
blanchet
parents: 55900
diff changeset
    63
fun key_of_typess s = key_of_types s o map (key_of_types "");
0ef30d52c5e4 more caching in composition pipeline
blanchet
parents: 55900
diff changeset
    64
fun typ_of_int n = Type (string_of_int n, []);
0ef30d52c5e4 more caching in composition pipeline
blanchet
parents: 55900
diff changeset
    65
fun typ_of_bnf bnf =
0ef30d52c5e4 more caching in composition pipeline
blanchet
parents: 55900
diff changeset
    66
  key_of_typess "" [[T_of_bnf bnf], lives_of_bnf bnf, sort Term_Ord.typ_ord (deads_of_bnf bnf)];
0ef30d52c5e4 more caching in composition pipeline
blanchet
parents: 55900
diff changeset
    67
0ef30d52c5e4 more caching in composition pipeline
blanchet
parents: 55900
diff changeset
    68
fun key_of_kill n bnf = key_of_types "k" [typ_of_int n, typ_of_bnf bnf];
0ef30d52c5e4 more caching in composition pipeline
blanchet
parents: 55900
diff changeset
    69
fun key_of_lift n bnf = key_of_types "l" [typ_of_int n, typ_of_bnf bnf];
0ef30d52c5e4 more caching in composition pipeline
blanchet
parents: 55900
diff changeset
    70
fun key_of_permute src dest bnf =
0ef30d52c5e4 more caching in composition pipeline
blanchet
parents: 55900
diff changeset
    71
  key_of_types "p" (map typ_of_int src @ map typ_of_int dest @ [typ_of_bnf bnf]);
0ef30d52c5e4 more caching in composition pipeline
blanchet
parents: 55900
diff changeset
    72
fun key_of_compose oDs Dss Ass outer inners =
0ef30d52c5e4 more caching in composition pipeline
blanchet
parents: 55900
diff changeset
    73
  key_of_types "c" (map (key_of_typess "") [[oDs], Dss, Ass, [map typ_of_bnf (outer :: inners)]]);
0ef30d52c5e4 more caching in composition pipeline
blanchet
parents: 55900
diff changeset
    74
0ef30d52c5e4 more caching in composition pipeline
blanchet
parents: 55900
diff changeset
    75
fun cache_comp_simple key cache (bnf, (unfold_set, lthy)) =
0ef30d52c5e4 more caching in composition pipeline
blanchet
parents: 55900
diff changeset
    76
  (bnf, ((Typtab.update (key, (bnf, ([], []))) cache, unfold_set), lthy));
0ef30d52c5e4 more caching in composition pipeline
blanchet
parents: 55900
diff changeset
    77
0ef30d52c5e4 more caching in composition pipeline
blanchet
parents: 55900
diff changeset
    78
fun cache_comp key (bnf_Ds_As, ((cache, unfold_set), lthy)) =
0ef30d52c5e4 more caching in composition pipeline
blanchet
parents: 55900
diff changeset
    79
  (bnf_Ds_As, ((Typtab.update (key, bnf_Ds_As) cache, unfold_set), lthy));
0ef30d52c5e4 more caching in composition pipeline
blanchet
parents: 55900
diff changeset
    80
55706
064c7c249f55 added BNF cache (within one definition)
blanchet
parents: 55705
diff changeset
    81
(* TODO: Replace by "BNF_Defs.defs list"? *)
49502
92a7c1842c78 tuned a few ML names
blanchet
parents: 49463
diff changeset
    82
type unfold_set = {
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    83
  map_unfolds: thm list,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    84
  set_unfoldss: thm list list,
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51837
diff changeset
    85
  rel_unfolds: thm list
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    86
};
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    87
55706
064c7c249f55 added BNF cache (within one definition)
blanchet
parents: 55705
diff changeset
    88
val empty_comp_cache = Typtab.empty;
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51837
diff changeset
    89
val empty_unfolds = {map_unfolds = [], set_unfoldss = [], rel_unfolds = []};
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    90
49503
dbbde075a42e simplified code
blanchet
parents: 49502
diff changeset
    91
fun add_to_thms thms new = thms |> not (Thm.is_reflexive new) ? insert Thm.eq_thm new;
dbbde075a42e simplified code
blanchet
parents: 49502
diff changeset
    92
fun adds_to_thms thms news = insert (eq_set Thm.eq_thm) (no_reflexive news) thms;
dbbde075a42e simplified code
blanchet
parents: 49502
diff changeset
    93
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51837
diff changeset
    94
fun add_to_unfolds map sets rel
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51837
diff changeset
    95
  {map_unfolds, set_unfoldss, rel_unfolds} =
49503
dbbde075a42e simplified code
blanchet
parents: 49502
diff changeset
    96
  {map_unfolds = add_to_thms map_unfolds map,
dbbde075a42e simplified code
blanchet
parents: 49502
diff changeset
    97
    set_unfoldss = adds_to_thms set_unfoldss sets,
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51837
diff changeset
    98
    rel_unfolds = add_to_thms rel_unfolds rel};
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    99
49503
dbbde075a42e simplified code
blanchet
parents: 49502
diff changeset
   100
fun add_bnf_to_unfolds bnf =
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51837
diff changeset
   101
  add_to_unfolds (map_def_of_bnf bnf) (set_defs_of_bnf bnf) (rel_def_of_bnf bnf);
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   102
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   103
val bdTN = "bdT";
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   104
49425
f27f83f71e94 cleaned up internal naming scheme for bnfs
traytel
parents: 49304
diff changeset
   105
fun mk_killN n = "_kill" ^ string_of_int n;
f27f83f71e94 cleaned up internal naming scheme for bnfs
traytel
parents: 49304
diff changeset
   106
fun mk_liftN n = "_lift" ^ string_of_int n;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   107
fun mk_permuteN src dest =
49425
f27f83f71e94 cleaned up internal naming scheme for bnfs
traytel
parents: 49304
diff changeset
   108
  "_permute_" ^ implode (map string_of_int src) ^ "_" ^ implode (map string_of_int dest);
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   109
55935
8f20d09d294e move special BNFs used for composition only to BNF_Comp;
traytel
parents: 55930
diff changeset
   110
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   111
(*copied from Envir.expand_term_free*)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   112
fun expand_term_const defs =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   113
  let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   114
    val eqs = map ((fn ((x, U), u) => (x, (U, u))) o apfst dest_Const) defs;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   115
    val get = fn Const (x, _) => AList.lookup (op =) eqs x | _ => NONE;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   116
  in Envir.expand_term get end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   117
58181
6d527272f7b2 renamed internal constant
blanchet
parents: 58128
diff changeset
   118
val id_bnf_def = @{thm id_bnf_def};
6d527272f7b2 renamed internal constant
blanchet
parents: 58128
diff changeset
   119
val expand_id_bnf_def = expand_term_const [Thm.prop_of id_bnf_def |> Logic.dest_equals];
55937
traytel
parents: 55935
diff changeset
   120
55851
3d40cf74726c optimize cardinal bounds involving natLeq (omega)
blanchet
parents: 55803
diff changeset
   121
fun is_sum_prod_natLeq (Const (@{const_name csum}, _) $ t $ u) = forall is_sum_prod_natLeq [t, u]
3d40cf74726c optimize cardinal bounds involving natLeq (omega)
blanchet
parents: 55803
diff changeset
   122
  | is_sum_prod_natLeq (Const (@{const_name cprod}, _) $ t $ u) = forall is_sum_prod_natLeq [t, u]
55853
e776a4b813d1 use aconv to compare terms (for cleanliness)
blanchet
parents: 55851
diff changeset
   123
  | is_sum_prod_natLeq t = t aconv @{term natLeq};
55851
3d40cf74726c optimize cardinal bounds involving natLeq (omega)
blanchet
parents: 55803
diff changeset
   124
49502
92a7c1842c78 tuned a few ML names
blanchet
parents: 49463
diff changeset
   125
fun clean_compose_bnf const_policy qualify b outer inners (unfold_set, lthy) =
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   126
  let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   127
    val olive = live_of_bnf outer;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   128
    val onwits = nwits_of_bnf outer;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   129
    val odead = dead_of_bnf outer;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   130
    val inner = hd inners;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   131
    val ilive = live_of_bnf inner;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   132
    val ideads = map dead_of_bnf inners;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   133
    val inwitss = map nwits_of_bnf inners;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   134
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   135
    (* TODO: check olive = length inners > 0,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   136
                   forall inner from inners. ilive = live,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   137
                   forall inner from inners. idead = dead  *)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   138
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   139
    val (oDs, lthy1) = apfst (map TFree)
56254
a2dd9200854d more antiquotations;
wenzelm
parents: 56018
diff changeset
   140
      (Variable.invent_types (replicate odead @{sort type}) lthy);
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   141
    val (Dss, lthy2) = apfst (map (map TFree))
56254
a2dd9200854d more antiquotations;
wenzelm
parents: 56018
diff changeset
   142
      (fold_map Variable.invent_types (map (fn n => replicate n @{sort type}) ideads) lthy1);
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   143
    val (Ass, lthy3) = apfst (replicate ilive o map TFree)
56254
a2dd9200854d more antiquotations;
wenzelm
parents: 56018
diff changeset
   144
      (Variable.invent_types (replicate ilive @{sort type}) lthy2);
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   145
    val As = if ilive > 0 then hd Ass else [];
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   146
    val Ass_repl = replicate olive As;
55906
abf91ebd0820 simplify sets in BNF composition
blanchet
parents: 55904
diff changeset
   147
    val (Bs, names_lthy) = apfst (map TFree)
56254
a2dd9200854d more antiquotations;
wenzelm
parents: 56018
diff changeset
   148
      (Variable.invent_types (replicate ilive @{sort type}) lthy3);
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   149
    val Bss_repl = replicate olive Bs;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   150
55906
abf91ebd0820 simplify sets in BNF composition
blanchet
parents: 55904
diff changeset
   151
    val ((((fs', Qs'), Asets), xs), _) = names_lthy
52923
traytel
parents: 52660
diff changeset
   152
      |> apfst snd o mk_Frees' "f" (map2 (curry op -->) As Bs)
49463
83ac281bcdc2 provide predicator, define relator
blanchet
parents: 49461
diff changeset
   153
      ||>> apfst snd o mk_Frees' "Q" (map2 mk_pred2T As Bs)
49456
fa8302c8dea1 adapted BNF composition to new relator approach
blanchet
parents: 49455
diff changeset
   154
      ||>> mk_Frees "A" (map HOLogic.mk_setT As)
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   155
      ||>> mk_Frees "x" As;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   156
58634
9f10d82e8188 added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents: 58359
diff changeset
   157
    val CAs = @{map 3} mk_T_of_bnf Dss Ass_repl inners;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   158
    val CCA = mk_T_of_bnf oDs CAs outer;
58634
9f10d82e8188 added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents: 58359
diff changeset
   159
    val CBs = @{map 3} mk_T_of_bnf Dss Bss_repl inners;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   160
    val outer_sets = mk_sets_of_bnf (replicate olive oDs) (replicate olive CAs) outer;
58634
9f10d82e8188 added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents: 58359
diff changeset
   161
    val inner_setss = @{map 3} mk_sets_of_bnf (map (replicate ilive) Dss) (replicate olive Ass) inners;
9f10d82e8188 added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents: 58359
diff changeset
   162
    val inner_bds = @{map 3} mk_bd_of_bnf Dss Ass_repl inners;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   163
    val outer_bd = mk_bd_of_bnf oDs CAs outer;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   164
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   165
    (*%f1 ... fn. outer.map (inner_1.map f1 ... fn) ... (inner_m.map f1 ... fn)*)
49303
blanchet
parents: 49236
diff changeset
   166
    val mapx = fold_rev Term.abs fs'
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   167
      (Term.list_comb (mk_map_of_bnf oDs CAs CBs outer,
49463
83ac281bcdc2 provide predicator, define relator
blanchet
parents: 49461
diff changeset
   168
        map2 (fn Ds => (fn f => Term.list_comb (f, map Bound (ilive - 1 downto 0))) o
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   169
          mk_map_of_bnf Ds As Bs) Dss inners));
49507
8826d5a4332b renamed "pred" to "rel" (relator)
blanchet
parents: 49506
diff changeset
   170
    (*%Q1 ... Qn. outer.rel (inner_1.rel Q1 ... Qn) ... (inner_m.rel Q1 ... Qn)*)
8826d5a4332b renamed "pred" to "rel" (relator)
blanchet
parents: 49506
diff changeset
   171
    val rel = fold_rev Term.abs Qs'
8826d5a4332b renamed "pred" to "rel" (relator)
blanchet
parents: 49506
diff changeset
   172
      (Term.list_comb (mk_rel_of_bnf oDs CAs CBs outer,
49463
83ac281bcdc2 provide predicator, define relator
blanchet
parents: 49461
diff changeset
   173
        map2 (fn Ds => (fn f => Term.list_comb (f, map Bound (ilive - 1 downto 0))) o
49507
8826d5a4332b renamed "pred" to "rel" (relator)
blanchet
parents: 49506
diff changeset
   174
          mk_rel_of_bnf Ds As Bs) Dss inners));
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   175
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   176
    (*Union o collect {outer.set_1 ... outer.set_m} o outer.map inner_1.set_i ... inner_m.set_i*)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   177
    (*Union o collect {image inner_1.set_i o outer.set_1 ... image inner_m.set_i o outer.set_m}*)
49303
blanchet
parents: 49236
diff changeset
   178
    fun mk_set i =
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   179
      let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   180
        val (setTs, T) = `(replicate olive o HOLogic.mk_setT) (nth As i);
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   181
        val outer_set = mk_collect
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   182
          (mk_sets_of_bnf (replicate olive oDs) (replicate olive setTs) outer)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   183
          (mk_T_of_bnf oDs setTs outer --> HOLogic.mk_setT T);
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   184
        val inner_sets = map (fn sets => nth sets i) inner_setss;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   185
        val outer_map = mk_map_of_bnf oDs CAs setTs outer;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   186
        val map_inner_sets = Term.list_comb (outer_map, inner_sets);
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   187
        val collect_image = mk_collect
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   188
          (map2 (fn f => fn set => HOLogic.mk_comp (mk_image f, set)) inner_sets outer_sets)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   189
          (CCA --> HOLogic.mk_setT T);
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   190
      in
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   191
        (Library.foldl1 HOLogic.mk_comp [mk_Union T, outer_set, map_inner_sets],
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   192
        HOLogic.mk_comp (mk_Union T, collect_image))
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   193
      end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   194
49303
blanchet
parents: 49236
diff changeset
   195
    val (sets, sets_alt) = map_split mk_set (0 upto ilive - 1);
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   196
55906
abf91ebd0820 simplify sets in BNF composition
blanchet
parents: 55904
diff changeset
   197
    fun mk_simplified_set set =
abf91ebd0820 simplify sets in BNF composition
blanchet
parents: 55904
diff changeset
   198
      let
abf91ebd0820 simplify sets in BNF composition
blanchet
parents: 55904
diff changeset
   199
        val setT = fastype_of set;
58181
6d527272f7b2 renamed internal constant
blanchet
parents: 58128
diff changeset
   200
        val var_set' = Const (@{const_name id_bnf}, setT --> setT) $ Var ((Name.uu, 0), setT);
55908
e6d570cb0f5e no 'sorry' so that the schematic variable gets instantiated
blanchet
parents: 55906
diff changeset
   201
        val goal = mk_Trueprop_eq (var_set', set);
55930
25a90cebbbe5 more careful simplification of sets (cf. abf91ebd0820)---yields smaller terms
traytel
parents: 55908
diff changeset
   202
        fun tac {context = ctxt, prems = _} =
25a90cebbbe5 more careful simplification of sets (cf. abf91ebd0820)---yields smaller terms
traytel
parents: 55908
diff changeset
   203
          mk_simplified_set_tac ctxt (collect_set_map_of_bnf outer);
55906
abf91ebd0820 simplify sets in BNF composition
blanchet
parents: 55904
diff changeset
   204
        val set'_eq_set =
57890
1e13f63fb452 use Goal.prove_sorry instead of Goal.prove where possible (= no schematics in goal and tactic is expected to succeed)
traytel
parents: 57632
diff changeset
   205
          Goal.prove (*no sorry*) names_lthy [] [] goal tac
55906
abf91ebd0820 simplify sets in BNF composition
blanchet
parents: 55904
diff changeset
   206
          |> Thm.close_derivation;
abf91ebd0820 simplify sets in BNF composition
blanchet
parents: 55904
diff changeset
   207
        val set' = fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of set'_eq_set)));
abf91ebd0820 simplify sets in BNF composition
blanchet
parents: 55904
diff changeset
   208
      in
abf91ebd0820 simplify sets in BNF composition
blanchet
parents: 55904
diff changeset
   209
        (set', set'_eq_set)
abf91ebd0820 simplify sets in BNF composition
blanchet
parents: 55904
diff changeset
   210
      end;
abf91ebd0820 simplify sets in BNF composition
blanchet
parents: 55904
diff changeset
   211
abf91ebd0820 simplify sets in BNF composition
blanchet
parents: 55904
diff changeset
   212
    val (sets', set'_eq_sets) =
abf91ebd0820 simplify sets in BNF composition
blanchet
parents: 55904
diff changeset
   213
      map_split mk_simplified_set sets
abf91ebd0820 simplify sets in BNF composition
blanchet
parents: 55904
diff changeset
   214
      ||> Proof_Context.export names_lthy lthy;
abf91ebd0820 simplify sets in BNF composition
blanchet
parents: 55904
diff changeset
   215
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   216
    (*(inner_1.bd +c ... +c inner_m.bd) *c outer.bd*)
54421
632be352a5a3 more explicit syntax for defining a bnf
traytel
parents: 53289
diff changeset
   217
    val bd = mk_cprod (Library.foldr1 (uncurry mk_csum) inner_bds) outer_bd;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   218
55851
3d40cf74726c optimize cardinal bounds involving natLeq (omega)
blanchet
parents: 55803
diff changeset
   219
    val (bd', bd_ordIso_natLeq_thm_opt) =
3d40cf74726c optimize cardinal bounds involving natLeq (omega)
blanchet
parents: 55803
diff changeset
   220
      if is_sum_prod_natLeq bd then
3d40cf74726c optimize cardinal bounds involving natLeq (omega)
blanchet
parents: 55803
diff changeset
   221
        let
3d40cf74726c optimize cardinal bounds involving natLeq (omega)
blanchet
parents: 55803
diff changeset
   222
          val bd' = @{term natLeq};
3d40cf74726c optimize cardinal bounds involving natLeq (omega)
blanchet
parents: 55803
diff changeset
   223
          val bd_bd' = HOLogic.mk_prod (bd, bd');
3d40cf74726c optimize cardinal bounds involving natLeq (omega)
blanchet
parents: 55803
diff changeset
   224
          val ordIso = Const (@{const_name ordIso}, HOLogic.mk_setT (fastype_of bd_bd'));
57567
d554b0097ad4 add mk_Trueprop_mem utility function
desharna
parents: 56634
diff changeset
   225
          val goal = mk_Trueprop_mem (bd_bd', ordIso);
55851
3d40cf74726c optimize cardinal bounds involving natLeq (omega)
blanchet
parents: 55803
diff changeset
   226
        in
3d40cf74726c optimize cardinal bounds involving natLeq (omega)
blanchet
parents: 55803
diff changeset
   227
          (bd', SOME (Goal.prove_sorry lthy [] [] goal (K bd_ordIso_natLeq_tac)
3d40cf74726c optimize cardinal bounds involving natLeq (omega)
blanchet
parents: 55803
diff changeset
   228
            |> Thm.close_derivation))
3d40cf74726c optimize cardinal bounds involving natLeq (omega)
blanchet
parents: 55803
diff changeset
   229
        end
3d40cf74726c optimize cardinal bounds involving natLeq (omega)
blanchet
parents: 55803
diff changeset
   230
      else
3d40cf74726c optimize cardinal bounds involving natLeq (omega)
blanchet
parents: 55803
diff changeset
   231
        (bd, NONE);
3d40cf74726c optimize cardinal bounds involving natLeq (omega)
blanchet
parents: 55803
diff changeset
   232
53270
c8628119d18e renamed BNF axiom
blanchet
parents: 53264
diff changeset
   233
    fun map_id0_tac _ =
c8628119d18e renamed BNF axiom
blanchet
parents: 53264
diff changeset
   234
      mk_comp_map_id0_tac (map_id0_of_bnf outer) (map_cong0_of_bnf outer)
c8628119d18e renamed BNF axiom
blanchet
parents: 53264
diff changeset
   235
        (map map_id0_of_bnf inners);
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   236
53287
271b34513bfb renamed BNF axiom
blanchet
parents: 53270
diff changeset
   237
    fun map_comp0_tac _ =
271b34513bfb renamed BNF axiom
blanchet
parents: 53270
diff changeset
   238
      mk_comp_map_comp0_tac (map_comp0_of_bnf outer) (map_cong0_of_bnf outer)
271b34513bfb renamed BNF axiom
blanchet
parents: 53270
diff changeset
   239
        (map map_comp0_of_bnf inners);
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   240
55906
abf91ebd0820 simplify sets in BNF composition
blanchet
parents: 55904
diff changeset
   241
    fun mk_single_set_map0_tac i ctxt =
abf91ebd0820 simplify sets in BNF composition
blanchet
parents: 55904
diff changeset
   242
      mk_comp_set_map0_tac ctxt (nth set'_eq_sets i) (map_comp0_of_bnf outer)
abf91ebd0820 simplify sets in BNF composition
blanchet
parents: 55904
diff changeset
   243
        (map_cong0_of_bnf outer) (collect_set_map_of_bnf outer)
53289
5e0623448bdb renamed BNF axiom
blanchet
parents: 53288
diff changeset
   244
        (map ((fn thms => nth thms i) o set_map0_of_bnf) inners);
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   245
53289
5e0623448bdb renamed BNF axiom
blanchet
parents: 53288
diff changeset
   246
    val set_map0_tacs = map mk_single_set_map0_tac (0 upto ilive - 1);
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   247
49303
blanchet
parents: 49236
diff changeset
   248
    fun bd_card_order_tac _ =
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   249
      mk_comp_bd_card_order_tac (map bd_card_order_of_bnf inners) (bd_card_order_of_bnf outer);
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   250
49303
blanchet
parents: 49236
diff changeset
   251
    fun bd_cinfinite_tac _ =
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   252
      mk_comp_bd_cinfinite_tac (bd_cinfinite_of_bnf inner) (bd_cinfinite_of_bnf outer);
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   253
49303
blanchet
parents: 49236
diff changeset
   254
    val set_alt_thms =
52059
2f970c7f722b proper option quick_and_dirty;
wenzelm
parents: 51895
diff changeset
   255
      if Config.get lthy quick_and_dirty then
49456
fa8302c8dea1 adapted BNF composition to new relator approach
blanchet
parents: 49455
diff changeset
   256
        []
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   257
      else
49109
0e5b859e1c91 no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
traytel
parents: 49019
diff changeset
   258
        map (fn goal =>
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 50059
diff changeset
   259
          Goal.prove_sorry lthy [] [] goal
49714
2c7c32f34220 made SML/NJ happier
traytel
parents: 49713
diff changeset
   260
            (fn {context = ctxt, prems = _} =>
51766
f19a4d0ab1bf renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet
parents: 51761
diff changeset
   261
              mk_comp_set_alt_tac ctxt (collect_set_map_of_bnf outer))
49109
0e5b859e1c91 no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
traytel
parents: 49019
diff changeset
   262
          |> Thm.close_derivation)
49303
blanchet
parents: 49236
diff changeset
   263
        (map2 (curry (HOLogic.mk_Trueprop o HOLogic.mk_eq)) sets sets_alt);
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   264
55906
abf91ebd0820 simplify sets in BNF composition
blanchet
parents: 55904
diff changeset
   265
    fun map_cong0_tac ctxt =
abf91ebd0820 simplify sets in BNF composition
blanchet
parents: 55904
diff changeset
   266
      mk_comp_map_cong0_tac ctxt set'_eq_sets set_alt_thms (map_cong0_of_bnf outer)
abf91ebd0820 simplify sets in BNF composition
blanchet
parents: 55904
diff changeset
   267
        (map map_cong0_of_bnf inners);
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   268
49303
blanchet
parents: 49236
diff changeset
   269
    val set_bd_tacs =
52059
2f970c7f722b proper option quick_and_dirty;
wenzelm
parents: 51895
diff changeset
   270
      if Config.get lthy quick_and_dirty then
49669
620fa6272c48 fixed quick-and-dirty mode
blanchet
parents: 49630
diff changeset
   271
        replicate ilive (K all_tac)
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   272
      else
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   273
        let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   274
          val outer_set_bds = set_bd_of_bnf outer;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   275
          val inner_set_bdss = map set_bd_of_bnf inners;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   276
          val inner_bd_Card_orders = map bd_Card_order_of_bnf inners;
49303
blanchet
parents: 49236
diff changeset
   277
          fun single_set_bd_thm i j =
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   278
            @{thm comp_single_set_bd} OF [nth inner_bd_Card_orders j, nth (nth inner_set_bdss j) i,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   279
              nth outer_set_bds j]
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   280
          val single_set_bd_thmss =
49303
blanchet
parents: 49236
diff changeset
   281
            map ((fn f => map f (0 upto olive - 1)) o single_set_bd_thm) (0 upto ilive - 1);
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   282
        in
58634
9f10d82e8188 added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents: 58359
diff changeset
   283
          @{map 3} (fn set'_eq_set => fn set_alt => fn single_set_bds => fn ctxt =>
55906
abf91ebd0820 simplify sets in BNF composition
blanchet
parents: 55904
diff changeset
   284
            mk_comp_set_bd_tac ctxt set'_eq_set bd_ordIso_natLeq_thm_opt set_alt single_set_bds)
abf91ebd0820 simplify sets in BNF composition
blanchet
parents: 55904
diff changeset
   285
          set'_eq_sets set_alt_thms single_set_bd_thmss
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   286
        end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   287
49303
blanchet
parents: 49236
diff changeset
   288
    val in_alt_thm =
49155
f51ab68f882f do not trivialize important internal theorem in quick_and_dirty mode
traytel
parents: 49123
diff changeset
   289
      let
49303
blanchet
parents: 49236
diff changeset
   290
        val inx = mk_in Asets sets CCA;
blanchet
parents: 49236
diff changeset
   291
        val in_alt = mk_in (map2 (mk_in Asets) inner_setss CAs) outer_sets CCA;
blanchet
parents: 49236
diff changeset
   292
        val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (inx, in_alt));
49155
f51ab68f882f do not trivialize important internal theorem in quick_and_dirty mode
traytel
parents: 49123
diff changeset
   293
      in
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 50059
diff changeset
   294
        Goal.prove_sorry lthy [] [] goal
49714
2c7c32f34220 made SML/NJ happier
traytel
parents: 49713
diff changeset
   295
          (fn {context = ctxt, prems = _} => mk_comp_in_alt_tac ctxt set_alt_thms)
49155
f51ab68f882f do not trivialize important internal theorem in quick_and_dirty mode
traytel
parents: 49123
diff changeset
   296
        |> Thm.close_derivation
f51ab68f882f do not trivialize important internal theorem in quick_and_dirty mode
traytel
parents: 49123
diff changeset
   297
      end;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   298
54841
af71b753c459 express weak pullback property of bnfs only in terms of the relator
traytel
parents: 54742
diff changeset
   299
    fun le_rel_OO_tac _ = mk_le_rel_OO_tac (le_rel_OO_of_bnf outer) (rel_mono_of_bnf outer)
af71b753c459 express weak pullback property of bnfs only in terms of the relator
traytel
parents: 54742
diff changeset
   300
      (map le_rel_OO_of_bnf inners);
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   301
55906
abf91ebd0820 simplify sets in BNF composition
blanchet
parents: 55904
diff changeset
   302
    fun rel_OO_Grp_tac ctxt =
49456
fa8302c8dea1 adapted BNF composition to new relator approach
blanchet
parents: 49455
diff changeset
   303
      let
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51837
diff changeset
   304
        val outer_rel_Grp = rel_Grp_of_bnf outer RS sym;
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51837
diff changeset
   305
        val outer_rel_cong = rel_cong_of_bnf outer;
49463
83ac281bcdc2 provide predicator, define relator
blanchet
parents: 49461
diff changeset
   306
        val thm =
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51837
diff changeset
   307
          (trans OF [in_alt_thm RS @{thm OO_Grp_cong},
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51837
diff changeset
   308
             trans OF [@{thm arg_cong2[of _ _ _ _ relcompp]} OF
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51837
diff changeset
   309
               [trans OF [outer_rel_Grp RS @{thm arg_cong[of _ _ conversep]},
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51837
diff changeset
   310
                 rel_conversep_of_bnf outer RS sym], outer_rel_Grp],
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51837
diff changeset
   311
               trans OF [rel_OO_of_bnf outer RS sym, outer_rel_cong OF
55906
abf91ebd0820 simplify sets in BNF composition
blanchet
parents: 55904
diff changeset
   312
                 (map (fn bnf => rel_OO_Grp_of_bnf bnf RS sym) inners)]]] RS sym);
49456
fa8302c8dea1 adapted BNF composition to new relator approach
blanchet
parents: 49455
diff changeset
   313
      in
55906
abf91ebd0820 simplify sets in BNF composition
blanchet
parents: 55904
diff changeset
   314
        unfold_thms_tac ctxt set'_eq_sets THEN rtac thm 1
49463
83ac281bcdc2 provide predicator, define relator
blanchet
parents: 49461
diff changeset
   315
      end;
49456
fa8302c8dea1 adapted BNF composition to new relator approach
blanchet
parents: 49455
diff changeset
   316
53289
5e0623448bdb renamed BNF axiom
blanchet
parents: 53288
diff changeset
   317
    val tacs = zip_axioms map_id0_tac map_comp0_tac map_cong0_tac set_map0_tacs bd_card_order_tac
54841
af71b753c459 express weak pullback property of bnfs only in terms of the relator
traytel
parents: 54742
diff changeset
   318
      bd_cinfinite_tac set_bd_tacs le_rel_OO_tac rel_OO_Grp_tac;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   319
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   320
    val outer_wits = mk_wits_of_bnf (replicate onwits oDs) (replicate onwits CAs) outer;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   321
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   322
    val inner_witss = map (map (fn (I, wit) => Term.list_comb (wit, map (nth xs) I)))
58634
9f10d82e8188 added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents: 58359
diff changeset
   323
      (@{map 3} (fn Ds => fn n => mk_wits_of_bnf (replicate n Ds) (replicate n As))
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   324
        Dss inwitss inners);
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   325
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   326
    val inner_witsss = map (map (nth inner_witss) o fst) outer_wits;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   327
49303
blanchet
parents: 49236
diff changeset
   328
    val wits = (inner_witsss, (map (single o snd) outer_wits))
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   329
      |-> map2 (fold (map_product (fn iwit => fn owit => owit $ iwit)))
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   330
      |> flat
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   331
      |> map (`(fn t => Term.add_frees t []))
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   332
      |> minimize_wits
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   333
      |> map (fn (frees, t) => fold absfree frees t);
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   334
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
   335
    fun wit_tac ctxt =
55906
abf91ebd0820 simplify sets in BNF composition
blanchet
parents: 55904
diff changeset
   336
      mk_comp_wit_tac ctxt set'_eq_sets (wit_thms_of_bnf outer) (collect_set_map_of_bnf outer)
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   337
        (maps wit_thms_of_bnf inners);
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   338
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   339
    val (bnf', lthy') =
56016
8875cdcfc85b unfold intermediate definitions after sealing the bnf
traytel
parents: 56013
diff changeset
   340
      bnf_def const_policy (K Dont_Note) true qualify tacs wit_tac (SOME (oDs @ flat Dss))
8875cdcfc85b unfold intermediate definitions after sealing the bnf
traytel
parents: 56013
diff changeset
   341
        Binding.empty Binding.empty [] ((((((b, CCA), mapx), sets'), bd'), wits), SOME rel) lthy;
55906
abf91ebd0820 simplify sets in BNF composition
blanchet
parents: 55904
diff changeset
   342
abf91ebd0820 simplify sets in BNF composition
blanchet
parents: 55904
diff changeset
   343
    val phi =
58181
6d527272f7b2 renamed internal constant
blanchet
parents: 58128
diff changeset
   344
      Morphism.thm_morphism "BNF" (unfold_thms lthy' [id_bnf_def])
6d527272f7b2 renamed internal constant
blanchet
parents: 58128
diff changeset
   345
      $> Morphism.term_morphism "BNF" expand_id_bnf_def;
55906
abf91ebd0820 simplify sets in BNF composition
blanchet
parents: 55904
diff changeset
   346
abf91ebd0820 simplify sets in BNF composition
blanchet
parents: 55904
diff changeset
   347
    val bnf'' = morph_bnf phi bnf';
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   348
  in
55906
abf91ebd0820 simplify sets in BNF composition
blanchet
parents: 55904
diff changeset
   349
    (bnf'', (add_bnf_to_unfolds bnf'' unfold_set, lthy'))
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   350
  end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   351
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   352
(* Killing live variables *)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   353
55904
0ef30d52c5e4 more caching in composition pipeline
blanchet
parents: 55900
diff changeset
   354
fun raw_kill_bnf qualify n bnf (accum as (unfold_set, lthy)) =
0ef30d52c5e4 more caching in composition pipeline
blanchet
parents: 55900
diff changeset
   355
  if n = 0 then (bnf, accum) else
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   356
  let
49425
f27f83f71e94 cleaned up internal naming scheme for bnfs
traytel
parents: 49304
diff changeset
   357
    val b = Binding.suffix_name (mk_killN n) (name_of_bnf bnf);
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   358
    val live = live_of_bnf bnf;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   359
    val dead = dead_of_bnf bnf;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   360
    val nwits = nwits_of_bnf bnf;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   361
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   362
    (* TODO: check 0 < n <= live *)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   363
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   364
    val (Ds, lthy1) = apfst (map TFree)
56254
a2dd9200854d more antiquotations;
wenzelm
parents: 56018
diff changeset
   365
      (Variable.invent_types (replicate dead @{sort type}) lthy);
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   366
    val ((killedAs, As), lthy2) = apfst (`(take n) o map TFree)
56254
a2dd9200854d more antiquotations;
wenzelm
parents: 56018
diff changeset
   367
      (Variable.invent_types (replicate live @{sort type}) lthy1);
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   368
    val (Bs, _(*lthy3*)) = apfst (append killedAs o map TFree)
56254
a2dd9200854d more antiquotations;
wenzelm
parents: 56018
diff changeset
   369
      (Variable.invent_types (replicate (live - n) @{sort type}) lthy2);
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   370
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   371
    val ((Asets, lives), _(*names_lthy*)) = lthy
49456
fa8302c8dea1 adapted BNF composition to new relator approach
blanchet
parents: 49455
diff changeset
   372
      |> mk_Frees "A" (map HOLogic.mk_setT (drop n As))
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   373
      ||>> mk_Frees "x" (drop n As);
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   374
    val xs = map (fn T => HOLogic.choice_const T $ absdummy T @{term True}) killedAs @ lives;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   375
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   376
    val T = mk_T_of_bnf Ds As bnf;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   377
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   378
    (*bnf.map id ... id*)
49303
blanchet
parents: 49236
diff changeset
   379
    val mapx = Term.list_comb (mk_map_of_bnf Ds As Bs bnf, map HOLogic.id_const killedAs);
49507
8826d5a4332b renamed "pred" to "rel" (relator)
blanchet
parents: 49506
diff changeset
   380
    (*bnf.rel (op =) ... (op =)*)
8826d5a4332b renamed "pred" to "rel" (relator)
blanchet
parents: 49506
diff changeset
   381
    val rel = Term.list_comb (mk_rel_of_bnf Ds As Bs bnf, map HOLogic.eq_const killedAs);
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   382
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   383
    val bnf_sets = mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf;
49303
blanchet
parents: 49236
diff changeset
   384
    val sets = drop n bnf_sets;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   385
55707
50cf04dd2584 clarified interaction with dead variables in the composition of BNFs
traytel
parents: 55706
diff changeset
   386
    val bd = mk_bd_of_bnf Ds As bnf;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   387
53270
c8628119d18e renamed BNF axiom
blanchet
parents: 53264
diff changeset
   388
    fun map_id0_tac _ = rtac (map_id0_of_bnf bnf) 1;
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
   389
    fun map_comp0_tac ctxt =
55067
a452de24a877 tuned names
blanchet
parents: 55061
diff changeset
   390
      unfold_thms_tac ctxt ((map_comp0_of_bnf bnf RS sym) ::
a452de24a877 tuned names
blanchet
parents: 55061
diff changeset
   391
        @{thms comp_assoc id_comp comp_id}) THEN rtac refl 1;
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
   392
    fun map_cong0_tac ctxt =
51761
4c9f08836d87 renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents: 51758
diff changeset
   393
      mk_kill_map_cong0_tac ctxt n (live - n) (map_cong0_of_bnf bnf);
53289
5e0623448bdb renamed BNF axiom
blanchet
parents: 53288
diff changeset
   394
    val set_map0_tacs = map (fn thm => fn _ => rtac thm 1) (drop n (set_map0_of_bnf bnf));
55707
50cf04dd2584 clarified interaction with dead variables in the composition of BNFs
traytel
parents: 55706
diff changeset
   395
    fun bd_card_order_tac _ = rtac (bd_card_order_of_bnf bnf) 1;
50cf04dd2584 clarified interaction with dead variables in the composition of BNFs
traytel
parents: 55706
diff changeset
   396
    fun bd_cinfinite_tac _ = rtac (bd_cinfinite_of_bnf bnf) 1;
50cf04dd2584 clarified interaction with dead variables in the composition of BNFs
traytel
parents: 55706
diff changeset
   397
    val set_bd_tacs = map (fn thm => fn _ => rtac thm 1) (drop n (set_bd_of_bnf bnf));
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   398
49303
blanchet
parents: 49236
diff changeset
   399
    val in_alt_thm =
49155
f51ab68f882f do not trivialize important internal theorem in quick_and_dirty mode
traytel
parents: 49123
diff changeset
   400
      let
49303
blanchet
parents: 49236
diff changeset
   401
        val inx = mk_in Asets sets T;
blanchet
parents: 49236
diff changeset
   402
        val in_alt = mk_in (map HOLogic.mk_UNIV killedAs @ Asets) bnf_sets T;
blanchet
parents: 49236
diff changeset
   403
        val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (inx, in_alt));
49155
f51ab68f882f do not trivialize important internal theorem in quick_and_dirty mode
traytel
parents: 49123
diff changeset
   404
      in
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 50059
diff changeset
   405
        Goal.prove_sorry lthy [] [] goal (K kill_in_alt_tac) |> Thm.close_derivation
49155
f51ab68f882f do not trivialize important internal theorem in quick_and_dirty mode
traytel
parents: 49123
diff changeset
   406
      end;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   407
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
   408
    fun le_rel_OO_tac ctxt =
54841
af71b753c459 express weak pullback property of bnfs only in terms of the relator
traytel
parents: 54742
diff changeset
   409
      EVERY' [rtac @{thm ord_le_eq_trans}, rtac (le_rel_OO_of_bnf bnf)] 1 THEN
af71b753c459 express weak pullback property of bnfs only in terms of the relator
traytel
parents: 54742
diff changeset
   410
      unfold_thms_tac ctxt @{thms eq_OO} THEN rtac refl 1;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   411
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51837
diff changeset
   412
    fun rel_OO_Grp_tac _ =
49456
fa8302c8dea1 adapted BNF composition to new relator approach
blanchet
parents: 49455
diff changeset
   413
      let
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51837
diff changeset
   414
        val rel_Grp = rel_Grp_of_bnf bnf RS sym
49463
83ac281bcdc2 provide predicator, define relator
blanchet
parents: 49461
diff changeset
   415
        val thm =
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51837
diff changeset
   416
          (trans OF [in_alt_thm RS @{thm OO_Grp_cong},
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51837
diff changeset
   417
            trans OF [@{thm arg_cong2[of _ _ _ _ relcompp]} OF
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51837
diff changeset
   418
              [trans OF [rel_Grp RS @{thm arg_cong[of _ _ conversep]},
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51837
diff changeset
   419
                rel_conversep_of_bnf bnf RS sym], rel_Grp],
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51837
diff changeset
   420
              trans OF [rel_OO_of_bnf bnf RS sym, rel_cong_of_bnf bnf OF
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51837
diff changeset
   421
                (replicate n @{thm trans[OF Grp_UNIV_id[OF refl] eq_alt[symmetric]]} @
52660
7f7311d04727 killed unused theorems
traytel
parents: 52635
diff changeset
   422
                 replicate (live - n) @{thm Grp_fst_snd})]]] RS sym);
49456
fa8302c8dea1 adapted BNF composition to new relator approach
blanchet
parents: 49455
diff changeset
   423
      in
49463
83ac281bcdc2 provide predicator, define relator
blanchet
parents: 49461
diff changeset
   424
        rtac thm 1
49456
fa8302c8dea1 adapted BNF composition to new relator approach
blanchet
parents: 49455
diff changeset
   425
      end;
fa8302c8dea1 adapted BNF composition to new relator approach
blanchet
parents: 49455
diff changeset
   426
53289
5e0623448bdb renamed BNF axiom
blanchet
parents: 53288
diff changeset
   427
    val tacs = zip_axioms map_id0_tac map_comp0_tac map_cong0_tac set_map0_tacs bd_card_order_tac
54841
af71b753c459 express weak pullback property of bnfs only in terms of the relator
traytel
parents: 54742
diff changeset
   428
      bd_cinfinite_tac set_bd_tacs le_rel_OO_tac rel_OO_Grp_tac;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   429
49303
blanchet
parents: 49236
diff changeset
   430
    val bnf_wits = mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   431
49303
blanchet
parents: 49236
diff changeset
   432
    val wits = map (fn t => fold absfree (Term.add_frees t []) t)
blanchet
parents: 49236
diff changeset
   433
      (map (fn (I, wit) => Term.list_comb (wit, map (nth xs) I)) bnf_wits);
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   434
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   435
    fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf);
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   436
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   437
    val (bnf', lthy') =
58297
e3a01b73579f new deads go to the end
traytel
parents: 58181
diff changeset
   438
      bnf_def Smart_Inline (K Dont_Note) true qualify tacs wit_tac (SOME (Ds @ killedAs))
56016
8875cdcfc85b unfold intermediate definitions after sealing the bnf
traytel
parents: 56013
diff changeset
   439
        Binding.empty Binding.empty [] ((((((b, T), mapx), sets), bd), wits), SOME rel) lthy;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   440
  in
49503
dbbde075a42e simplified code
blanchet
parents: 49502
diff changeset
   441
    (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   442
  end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   443
55904
0ef30d52c5e4 more caching in composition pipeline
blanchet
parents: 55900
diff changeset
   444
fun kill_bnf qualify n bnf (accum as ((cache, unfold_set), lthy)) =
0ef30d52c5e4 more caching in composition pipeline
blanchet
parents: 55900
diff changeset
   445
  let val key = key_of_kill n bnf in
0ef30d52c5e4 more caching in composition pipeline
blanchet
parents: 55900
diff changeset
   446
    (case Typtab.lookup cache key of
0ef30d52c5e4 more caching in composition pipeline
blanchet
parents: 55900
diff changeset
   447
      SOME (bnf, _) => (bnf, accum)
0ef30d52c5e4 more caching in composition pipeline
blanchet
parents: 55900
diff changeset
   448
    | NONE => cache_comp_simple key cache (raw_kill_bnf qualify n bnf (unfold_set, lthy)))
0ef30d52c5e4 more caching in composition pipeline
blanchet
parents: 55900
diff changeset
   449
  end;
0ef30d52c5e4 more caching in composition pipeline
blanchet
parents: 55900
diff changeset
   450
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   451
(* Adding dummy live variables *)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   452
55904
0ef30d52c5e4 more caching in composition pipeline
blanchet
parents: 55900
diff changeset
   453
fun raw_lift_bnf qualify n bnf (accum as (unfold_set, lthy)) =
0ef30d52c5e4 more caching in composition pipeline
blanchet
parents: 55900
diff changeset
   454
  if n = 0 then (bnf, accum) else
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   455
  let
49425
f27f83f71e94 cleaned up internal naming scheme for bnfs
traytel
parents: 49304
diff changeset
   456
    val b = Binding.suffix_name (mk_liftN n) (name_of_bnf bnf);
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   457
    val live = live_of_bnf bnf;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   458
    val dead = dead_of_bnf bnf;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   459
    val nwits = nwits_of_bnf bnf;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   460
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   461
    (* TODO: check 0 < n *)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   462
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   463
    val (Ds, lthy1) = apfst (map TFree)
56254
a2dd9200854d more antiquotations;
wenzelm
parents: 56018
diff changeset
   464
      (Variable.invent_types (replicate dead @{sort type}) lthy);
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   465
    val ((newAs, As), lthy2) = apfst (chop n o map TFree)
56254
a2dd9200854d more antiquotations;
wenzelm
parents: 56018
diff changeset
   466
      (Variable.invent_types (replicate (n + live) @{sort type}) lthy1);
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   467
    val ((newBs, Bs), _(*lthy3*)) = apfst (chop n o map TFree)
56254
a2dd9200854d more antiquotations;
wenzelm
parents: 56018
diff changeset
   468
      (Variable.invent_types (replicate (n + live) @{sort type}) lthy2);
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   469
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   470
    val (Asets, _(*names_lthy*)) = lthy
49456
fa8302c8dea1 adapted BNF composition to new relator approach
blanchet
parents: 49455
diff changeset
   471
      |> mk_Frees "A" (map HOLogic.mk_setT (newAs @ As));
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   472
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   473
    val T = mk_T_of_bnf Ds As bnf;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   474
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   475
    (*%f1 ... fn. bnf.map*)
49303
blanchet
parents: 49236
diff changeset
   476
    val mapx =
52923
traytel
parents: 52660
diff changeset
   477
      fold_rev Term.absdummy (map2 (curry op -->) newAs newBs) (mk_map_of_bnf Ds As Bs bnf);
49507
8826d5a4332b renamed "pred" to "rel" (relator)
blanchet
parents: 49506
diff changeset
   478
    (*%Q1 ... Qn. bnf.rel*)
8826d5a4332b renamed "pred" to "rel" (relator)
blanchet
parents: 49506
diff changeset
   479
    val rel = fold_rev Term.absdummy (map2 mk_pred2T newAs newBs) (mk_rel_of_bnf Ds As Bs bnf);
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   480
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   481
    val bnf_sets = mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf;
49303
blanchet
parents: 49236
diff changeset
   482
    val sets = map (fn A => absdummy T (HOLogic.mk_set A [])) newAs @ bnf_sets;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   483
49303
blanchet
parents: 49236
diff changeset
   484
    val bd = mk_bd_of_bnf Ds As bnf;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   485
53270
c8628119d18e renamed BNF axiom
blanchet
parents: 53264
diff changeset
   486
    fun map_id0_tac _ = rtac (map_id0_of_bnf bnf) 1;
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
   487
    fun map_comp0_tac ctxt =
55067
a452de24a877 tuned names
blanchet
parents: 55061
diff changeset
   488
      unfold_thms_tac ctxt ((map_comp0_of_bnf bnf RS sym) ::
a452de24a877 tuned names
blanchet
parents: 55061
diff changeset
   489
        @{thms comp_assoc id_comp comp_id}) THEN rtac refl 1;
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
   490
    fun map_cong0_tac ctxt =
51761
4c9f08836d87 renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents: 51758
diff changeset
   491
      rtac (map_cong0_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac ctxt 1);
53289
5e0623448bdb renamed BNF axiom
blanchet
parents: 53288
diff changeset
   492
    val set_map0_tacs =
52059
2f970c7f722b proper option quick_and_dirty;
wenzelm
parents: 51895
diff changeset
   493
      if Config.get lthy quick_and_dirty then
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   494
        replicate (n + live) (K all_tac)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   495
      else
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   496
        replicate n (K empty_natural_tac) @
53289
5e0623448bdb renamed BNF axiom
blanchet
parents: 53288
diff changeset
   497
        map (fn thm => fn _ => rtac thm 1) (set_map0_of_bnf bnf);
49303
blanchet
parents: 49236
diff changeset
   498
    fun bd_card_order_tac _ = rtac (bd_card_order_of_bnf bnf) 1;
blanchet
parents: 49236
diff changeset
   499
    fun bd_cinfinite_tac _ = rtac (bd_cinfinite_of_bnf bnf) 1;
blanchet
parents: 49236
diff changeset
   500
    val set_bd_tacs =
52059
2f970c7f722b proper option quick_and_dirty;
wenzelm
parents: 51895
diff changeset
   501
      if Config.get lthy quick_and_dirty then
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   502
        replicate (n + live) (K all_tac)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   503
      else
49304
blanchet
parents: 49303
diff changeset
   504
        replicate n (K (mk_lift_set_bd_tac (bd_Card_order_of_bnf bnf))) @
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   505
        (map (fn thm => fn _ => rtac thm 1) (set_bd_of_bnf bnf));
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   506
49303
blanchet
parents: 49236
diff changeset
   507
    val in_alt_thm =
49155
f51ab68f882f do not trivialize important internal theorem in quick_and_dirty mode
traytel
parents: 49123
diff changeset
   508
      let
49303
blanchet
parents: 49236
diff changeset
   509
        val inx = mk_in Asets sets T;
blanchet
parents: 49236
diff changeset
   510
        val in_alt = mk_in (drop n Asets) bnf_sets T;
blanchet
parents: 49236
diff changeset
   511
        val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (inx, in_alt));
49155
f51ab68f882f do not trivialize important internal theorem in quick_and_dirty mode
traytel
parents: 49123
diff changeset
   512
      in
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 50059
diff changeset
   513
        Goal.prove_sorry lthy [] [] goal (K lift_in_alt_tac) |> Thm.close_derivation
49155
f51ab68f882f do not trivialize important internal theorem in quick_and_dirty mode
traytel
parents: 49123
diff changeset
   514
      end;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   515
54841
af71b753c459 express weak pullback property of bnfs only in terms of the relator
traytel
parents: 54742
diff changeset
   516
    fun le_rel_OO_tac _ = rtac (le_rel_OO_of_bnf bnf) 1;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   517
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51837
diff changeset
   518
    fun rel_OO_Grp_tac _ = mk_simple_rel_OO_Grp_tac (rel_OO_Grp_of_bnf bnf) in_alt_thm;
49456
fa8302c8dea1 adapted BNF composition to new relator approach
blanchet
parents: 49455
diff changeset
   519
53289
5e0623448bdb renamed BNF axiom
blanchet
parents: 53288
diff changeset
   520
    val tacs = zip_axioms map_id0_tac map_comp0_tac map_cong0_tac set_map0_tacs bd_card_order_tac
54841
af71b753c459 express weak pullback property of bnfs only in terms of the relator
traytel
parents: 54742
diff changeset
   521
      bd_cinfinite_tac set_bd_tacs le_rel_OO_tac rel_OO_Grp_tac;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   522
49303
blanchet
parents: 49236
diff changeset
   523
    val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   524
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   525
    fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf);
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   526
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   527
    val (bnf', lthy') =
56016
8875cdcfc85b unfold intermediate definitions after sealing the bnf
traytel
parents: 56013
diff changeset
   528
      bnf_def Smart_Inline (K Dont_Note) true qualify tacs wit_tac (SOME Ds) Binding.empty
8875cdcfc85b unfold intermediate definitions after sealing the bnf
traytel
parents: 56013
diff changeset
   529
        Binding.empty [] ((((((b, T), mapx), sets), bd), wits), SOME rel) lthy;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   530
  in
49503
dbbde075a42e simplified code
blanchet
parents: 49502
diff changeset
   531
    (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   532
  end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   533
55904
0ef30d52c5e4 more caching in composition pipeline
blanchet
parents: 55900
diff changeset
   534
fun lift_bnf qualify n bnf (accum as ((cache, unfold_set), lthy)) =
0ef30d52c5e4 more caching in composition pipeline
blanchet
parents: 55900
diff changeset
   535
  let val key = key_of_lift n bnf in
0ef30d52c5e4 more caching in composition pipeline
blanchet
parents: 55900
diff changeset
   536
    (case Typtab.lookup cache key of
0ef30d52c5e4 more caching in composition pipeline
blanchet
parents: 55900
diff changeset
   537
      SOME (bnf, _) => (bnf, accum)
0ef30d52c5e4 more caching in composition pipeline
blanchet
parents: 55900
diff changeset
   538
    | NONE => cache_comp_simple key cache (raw_lift_bnf qualify n bnf (unfold_set, lthy)))
0ef30d52c5e4 more caching in composition pipeline
blanchet
parents: 55900
diff changeset
   539
  end;
0ef30d52c5e4 more caching in composition pipeline
blanchet
parents: 55900
diff changeset
   540
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   541
(* Changing the order of live variables *)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   542
55904
0ef30d52c5e4 more caching in composition pipeline
blanchet
parents: 55900
diff changeset
   543
fun raw_permute_bnf qualify src dest bnf (accum as (unfold_set, lthy)) =
0ef30d52c5e4 more caching in composition pipeline
blanchet
parents: 55900
diff changeset
   544
  if src = dest then (bnf, accum) else
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   545
  let
49425
f27f83f71e94 cleaned up internal naming scheme for bnfs
traytel
parents: 49304
diff changeset
   546
    val b = Binding.suffix_name (mk_permuteN src dest) (name_of_bnf bnf);
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   547
    val live = live_of_bnf bnf;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   548
    val dead = dead_of_bnf bnf;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   549
    val nwits = nwits_of_bnf bnf;
55480
59cc4a8bc28a allow different functions to recurse on the same type, like in the old package
blanchet
parents: 55197
diff changeset
   550
59cc4a8bc28a allow different functions to recurse on the same type, like in the old package
blanchet
parents: 55197
diff changeset
   551
    fun permute xs = permute_like_unique (op =) src dest xs;
59cc4a8bc28a allow different functions to recurse on the same type, like in the old package
blanchet
parents: 55197
diff changeset
   552
    fun unpermute xs = permute_like_unique (op =) dest src xs;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   553
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   554
    val (Ds, lthy1) = apfst (map TFree)
56254
a2dd9200854d more antiquotations;
wenzelm
parents: 56018
diff changeset
   555
      (Variable.invent_types (replicate dead @{sort type}) lthy);
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   556
    val (As, lthy2) = apfst (map TFree)
56254
a2dd9200854d more antiquotations;
wenzelm
parents: 56018
diff changeset
   557
      (Variable.invent_types (replicate live @{sort type}) lthy1);
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   558
    val (Bs, _(*lthy3*)) = apfst (map TFree)
56254
a2dd9200854d more antiquotations;
wenzelm
parents: 56018
diff changeset
   559
      (Variable.invent_types (replicate live @{sort type}) lthy2);
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   560
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   561
    val (Asets, _(*names_lthy*)) = lthy
49456
fa8302c8dea1 adapted BNF composition to new relator approach
blanchet
parents: 49455
diff changeset
   562
      |> mk_Frees "A" (map HOLogic.mk_setT (permute As));
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   563
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   564
    val T = mk_T_of_bnf Ds As bnf;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   565
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   566
    (*%f(1) ... f(n). bnf.map f\<sigma>(1) ... f\<sigma>(n)*)
49303
blanchet
parents: 49236
diff changeset
   567
    val mapx = fold_rev Term.absdummy (permute (map2 (curry op -->) As Bs))
53038
dd5ea8a51af0 generalized "mk_permute"
blanchet
parents: 52985
diff changeset
   568
      (Term.list_comb (mk_map_of_bnf Ds As Bs bnf, unpermute (map Bound (live - 1 downto 0))));
49507
8826d5a4332b renamed "pred" to "rel" (relator)
blanchet
parents: 49506
diff changeset
   569
    (*%Q(1) ... Q(n). bnf.rel Q\<sigma>(1) ... Q\<sigma>(n)*)
8826d5a4332b renamed "pred" to "rel" (relator)
blanchet
parents: 49506
diff changeset
   570
    val rel = fold_rev Term.absdummy (permute (map2 mk_pred2T As Bs))
53038
dd5ea8a51af0 generalized "mk_permute"
blanchet
parents: 52985
diff changeset
   571
      (Term.list_comb (mk_rel_of_bnf Ds As Bs bnf, unpermute (map Bound (live - 1 downto 0))));
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   572
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   573
    val bnf_sets = mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf;
49303
blanchet
parents: 49236
diff changeset
   574
    val sets = permute bnf_sets;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   575
49303
blanchet
parents: 49236
diff changeset
   576
    val bd = mk_bd_of_bnf Ds As bnf;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   577
53270
c8628119d18e renamed BNF axiom
blanchet
parents: 53264
diff changeset
   578
    fun map_id0_tac _ = rtac (map_id0_of_bnf bnf) 1;
53287
271b34513bfb renamed BNF axiom
blanchet
parents: 53270
diff changeset
   579
    fun map_comp0_tac _ = rtac (map_comp0_of_bnf bnf) 1;
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
   580
    fun map_cong0_tac ctxt =
51761
4c9f08836d87 renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents: 51758
diff changeset
   581
      rtac (map_cong0_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac ctxt 1);
53289
5e0623448bdb renamed BNF axiom
blanchet
parents: 53288
diff changeset
   582
    val set_map0_tacs = permute (map (fn thm => fn _ => rtac thm 1) (set_map0_of_bnf bnf));
49303
blanchet
parents: 49236
diff changeset
   583
    fun bd_card_order_tac _ = rtac (bd_card_order_of_bnf bnf) 1;
blanchet
parents: 49236
diff changeset
   584
    fun bd_cinfinite_tac _ = rtac (bd_cinfinite_of_bnf bnf) 1;
blanchet
parents: 49236
diff changeset
   585
    val set_bd_tacs = permute (map (fn thm => fn _ => rtac thm 1) (set_bd_of_bnf bnf));
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   586
49303
blanchet
parents: 49236
diff changeset
   587
    val in_alt_thm =
49155
f51ab68f882f do not trivialize important internal theorem in quick_and_dirty mode
traytel
parents: 49123
diff changeset
   588
      let
49303
blanchet
parents: 49236
diff changeset
   589
        val inx = mk_in Asets sets T;
53038
dd5ea8a51af0 generalized "mk_permute"
blanchet
parents: 52985
diff changeset
   590
        val in_alt = mk_in (unpermute Asets) bnf_sets T;
49303
blanchet
parents: 49236
diff changeset
   591
        val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (inx, in_alt));
49155
f51ab68f882f do not trivialize important internal theorem in quick_and_dirty mode
traytel
parents: 49123
diff changeset
   592
      in
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 50059
diff changeset
   593
        Goal.prove_sorry lthy [] [] goal (K (mk_permute_in_alt_tac src dest))
49155
f51ab68f882f do not trivialize important internal theorem in quick_and_dirty mode
traytel
parents: 49123
diff changeset
   594
        |> Thm.close_derivation
f51ab68f882f do not trivialize important internal theorem in quick_and_dirty mode
traytel
parents: 49123
diff changeset
   595
      end;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   596
54841
af71b753c459 express weak pullback property of bnfs only in terms of the relator
traytel
parents: 54742
diff changeset
   597
    fun le_rel_OO_tac _ = rtac (le_rel_OO_of_bnf bnf) 1;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   598
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51837
diff changeset
   599
    fun rel_OO_Grp_tac _ = mk_simple_rel_OO_Grp_tac (rel_OO_Grp_of_bnf bnf) in_alt_thm;
49456
fa8302c8dea1 adapted BNF composition to new relator approach
blanchet
parents: 49455
diff changeset
   600
53289
5e0623448bdb renamed BNF axiom
blanchet
parents: 53288
diff changeset
   601
    val tacs = zip_axioms map_id0_tac map_comp0_tac map_cong0_tac set_map0_tacs bd_card_order_tac
54841
af71b753c459 express weak pullback property of bnfs only in terms of the relator
traytel
parents: 54742
diff changeset
   602
      bd_cinfinite_tac set_bd_tacs le_rel_OO_tac rel_OO_Grp_tac;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   603
49303
blanchet
parents: 49236
diff changeset
   604
    val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   605
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   606
    fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf);
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   607
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   608
    val (bnf', lthy') =
56016
8875cdcfc85b unfold intermediate definitions after sealing the bnf
traytel
parents: 56013
diff changeset
   609
      bnf_def Smart_Inline (K Dont_Note) true qualify tacs wit_tac (SOME Ds) Binding.empty
8875cdcfc85b unfold intermediate definitions after sealing the bnf
traytel
parents: 56013
diff changeset
   610
        Binding.empty [] ((((((b, T), mapx), sets), bd), wits), SOME rel) lthy;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   611
  in
49503
dbbde075a42e simplified code
blanchet
parents: 49502
diff changeset
   612
    (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   613
  end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   614
55904
0ef30d52c5e4 more caching in composition pipeline
blanchet
parents: 55900
diff changeset
   615
fun permute_bnf qualify src dest bnf (accum as ((cache, unfold_set), lthy)) =
0ef30d52c5e4 more caching in composition pipeline
blanchet
parents: 55900
diff changeset
   616
  let val key = key_of_permute src dest bnf in
0ef30d52c5e4 more caching in composition pipeline
blanchet
parents: 55900
diff changeset
   617
    (case Typtab.lookup cache key of
0ef30d52c5e4 more caching in composition pipeline
blanchet
parents: 55900
diff changeset
   618
      SOME (bnf, _) => (bnf, accum)
0ef30d52c5e4 more caching in composition pipeline
blanchet
parents: 55900
diff changeset
   619
    | NONE => cache_comp_simple key cache (raw_permute_bnf qualify src dest bnf (unfold_set, lthy)))
0ef30d52c5e4 more caching in composition pipeline
blanchet
parents: 55900
diff changeset
   620
  end;
0ef30d52c5e4 more caching in composition pipeline
blanchet
parents: 55900
diff changeset
   621
49014
332e5e661675 have "bnf_of_typ" command seal the BNF
blanchet
parents: 48975
diff changeset
   622
(* Composition pipeline *)
332e5e661675 have "bnf_of_typ" command seal the BNF
blanchet
parents: 48975
diff changeset
   623
332e5e661675 have "bnf_of_typ" command seal the BNF
blanchet
parents: 48975
diff changeset
   624
fun permute_and_kill qualify n src dest bnf =
55703
a21069381ba5 optimization of 'bnf_of_typ' if all variables are dead
blanchet
parents: 55480
diff changeset
   625
  permute_bnf qualify src dest bnf
49304
blanchet
parents: 49303
diff changeset
   626
  #> uncurry (kill_bnf qualify n);
49014
332e5e661675 have "bnf_of_typ" command seal the BNF
blanchet
parents: 48975
diff changeset
   627
332e5e661675 have "bnf_of_typ" command seal the BNF
blanchet
parents: 48975
diff changeset
   628
fun lift_and_permute qualify n src dest bnf =
55703
a21069381ba5 optimization of 'bnf_of_typ' if all variables are dead
blanchet
parents: 55480
diff changeset
   629
  lift_bnf qualify n bnf
49014
332e5e661675 have "bnf_of_typ" command seal the BNF
blanchet
parents: 48975
diff changeset
   630
  #> uncurry (permute_bnf qualify src dest);
332e5e661675 have "bnf_of_typ" command seal the BNF
blanchet
parents: 48975
diff changeset
   631
58332
be0f5d8d511b imported patch phantoms
blanchet
parents: 58297
diff changeset
   632
fun normalize_bnfs qualify Ass Ds flatten_tyargs bnfs accum =
49014
332e5e661675 have "bnf_of_typ" command seal the BNF
blanchet
parents: 48975
diff changeset
   633
  let
332e5e661675 have "bnf_of_typ" command seal the BNF
blanchet
parents: 48975
diff changeset
   634
    val before_kill_src = map (fn As => 0 upto (length As - 1)) Ass;
52985
9e22d6264277 generalized library function
traytel
parents: 52923
diff changeset
   635
    val kill_poss = map (find_indices op = Ds) Ass;
9e22d6264277 generalized library function
traytel
parents: 52923
diff changeset
   636
    val live_poss = map2 (subtract op =) kill_poss before_kill_src;
49014
332e5e661675 have "bnf_of_typ" command seal the BNF
blanchet
parents: 48975
diff changeset
   637
    val before_kill_dest = map2 append kill_poss live_poss;
332e5e661675 have "bnf_of_typ" command seal the BNF
blanchet
parents: 48975
diff changeset
   638
    val kill_ns = map length kill_poss;
55904
0ef30d52c5e4 more caching in composition pipeline
blanchet
parents: 55900
diff changeset
   639
    val (inners', accum') =
58634
9f10d82e8188 added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents: 58359
diff changeset
   640
      @{fold_map 5} (fn i => permute_and_kill (qualify i))
49014
332e5e661675 have "bnf_of_typ" command seal the BNF
blanchet
parents: 48975
diff changeset
   641
        (if length bnfs = 1 then [0] else (1 upto length bnfs))
55904
0ef30d52c5e4 more caching in composition pipeline
blanchet
parents: 55900
diff changeset
   642
        kill_ns before_kill_src before_kill_dest bnfs accum;
49014
332e5e661675 have "bnf_of_typ" command seal the BNF
blanchet
parents: 48975
diff changeset
   643
332e5e661675 have "bnf_of_typ" command seal the BNF
blanchet
parents: 48975
diff changeset
   644
    val Ass' = map2 (map o nth) Ass live_poss;
58332
be0f5d8d511b imported patch phantoms
blanchet
parents: 58297
diff changeset
   645
    val As = flatten_tyargs Ass';
49014
332e5e661675 have "bnf_of_typ" command seal the BNF
blanchet
parents: 48975
diff changeset
   646
    val after_lift_dest = replicate (length Ass') (0 upto (length As - 1));
332e5e661675 have "bnf_of_typ" command seal the BNF
blanchet
parents: 48975
diff changeset
   647
    val old_poss = map (map (fn x => find_index (fn y => x = y) As)) Ass';
52985
9e22d6264277 generalized library function
traytel
parents: 52923
diff changeset
   648
    val new_poss = map2 (subtract op =) old_poss after_lift_dest;
49014
332e5e661675 have "bnf_of_typ" command seal the BNF
blanchet
parents: 48975
diff changeset
   649
    val after_lift_src = map2 append new_poss old_poss;
332e5e661675 have "bnf_of_typ" command seal the BNF
blanchet
parents: 48975
diff changeset
   650
    val lift_ns = map (fn xs => length As - length xs) Ass';
332e5e661675 have "bnf_of_typ" command seal the BNF
blanchet
parents: 48975
diff changeset
   651
  in
58634
9f10d82e8188 added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents: 58359
diff changeset
   652
    ((kill_poss, As), @{fold_map 5} (fn i => lift_and_permute (qualify i))
55703
a21069381ba5 optimization of 'bnf_of_typ' if all variables are dead
blanchet
parents: 55480
diff changeset
   653
      (if length bnfs = 1 then [0] else 1 upto length bnfs)
55904
0ef30d52c5e4 more caching in composition pipeline
blanchet
parents: 55900
diff changeset
   654
      lift_ns after_lift_src after_lift_dest inners' accum')
49014
332e5e661675 have "bnf_of_typ" command seal the BNF
blanchet
parents: 48975
diff changeset
   655
  end;
332e5e661675 have "bnf_of_typ" command seal the BNF
blanchet
parents: 48975
diff changeset
   656
332e5e661675 have "bnf_of_typ" command seal the BNF
blanchet
parents: 48975
diff changeset
   657
fun default_comp_sort Ass =
59058
a78612c67ec0 renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents: 58959
diff changeset
   658
  Library.sort (Term_Ord.typ_ord o apply2 TFree) (fold (fold (insert (op =))) Ass []);
49014
332e5e661675 have "bnf_of_typ" command seal the BNF
blanchet
parents: 48975
diff changeset
   659
58332
be0f5d8d511b imported patch phantoms
blanchet
parents: 58297
diff changeset
   660
fun raw_compose_bnf const_policy qualify flatten_tyargs outer inners oDs Dss tfreess accum =
49014
332e5e661675 have "bnf_of_typ" command seal the BNF
blanchet
parents: 48975
diff changeset
   661
  let
49425
f27f83f71e94 cleaned up internal naming scheme for bnfs
traytel
parents: 49304
diff changeset
   662
    val b = name_of_bnf outer;
49014
332e5e661675 have "bnf_of_typ" command seal the BNF
blanchet
parents: 48975
diff changeset
   663
49121
9e0acaa470ab more work on FP sugar
blanchet
parents: 49109
diff changeset
   664
    val Ass = map (map Term.dest_TFree) tfreess;
49014
332e5e661675 have "bnf_of_typ" command seal the BNF
blanchet
parents: 48975
diff changeset
   665
    val Ds = fold (fold Term.add_tfreesT) (oDs :: Dss) [];
332e5e661675 have "bnf_of_typ" command seal the BNF
blanchet
parents: 48975
diff changeset
   666
55904
0ef30d52c5e4 more caching in composition pipeline
blanchet
parents: 55900
diff changeset
   667
    val ((kill_poss, As), (inners', ((cache', unfold_set'), lthy'))) =
58332
be0f5d8d511b imported patch phantoms
blanchet
parents: 58297
diff changeset
   668
      normalize_bnfs qualify Ass Ds flatten_tyargs inners accum;
49014
332e5e661675 have "bnf_of_typ" command seal the BNF
blanchet
parents: 48975
diff changeset
   669
58634
9f10d82e8188 added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents: 58359
diff changeset
   670
    val Ds = oDs @ flat (@{map 3} (uncurry append oo curry swap oo map o nth) tfreess kill_poss Dss);
49014
332e5e661675 have "bnf_of_typ" command seal the BNF
blanchet
parents: 48975
diff changeset
   671
    val As = map TFree As;
332e5e661675 have "bnf_of_typ" command seal the BNF
blanchet
parents: 48975
diff changeset
   672
  in
49425
f27f83f71e94 cleaned up internal naming scheme for bnfs
traytel
parents: 49304
diff changeset
   673
    apfst (rpair (Ds, As))
55904
0ef30d52c5e4 more caching in composition pipeline
blanchet
parents: 55900
diff changeset
   674
      (apsnd (apfst (pair cache'))
0ef30d52c5e4 more caching in composition pipeline
blanchet
parents: 55900
diff changeset
   675
        (clean_compose_bnf const_policy (qualify 0) b outer inners' (unfold_set', lthy')))
0ef30d52c5e4 more caching in composition pipeline
blanchet
parents: 55900
diff changeset
   676
  end;
0ef30d52c5e4 more caching in composition pipeline
blanchet
parents: 55900
diff changeset
   677
58332
be0f5d8d511b imported patch phantoms
blanchet
parents: 58297
diff changeset
   678
fun compose_bnf const_policy qualify flatten_tyargs outer inners oDs Dss tfreess
be0f5d8d511b imported patch phantoms
blanchet
parents: 58297
diff changeset
   679
    (accum as ((cache, _), _)) =
55904
0ef30d52c5e4 more caching in composition pipeline
blanchet
parents: 55900
diff changeset
   680
  let val key = key_of_compose oDs Dss tfreess outer inners in
0ef30d52c5e4 more caching in composition pipeline
blanchet
parents: 55900
diff changeset
   681
    (case Typtab.lookup cache key of
0ef30d52c5e4 more caching in composition pipeline
blanchet
parents: 55900
diff changeset
   682
      SOME bnf_Ds_As => (bnf_Ds_As, accum)
0ef30d52c5e4 more caching in composition pipeline
blanchet
parents: 55900
diff changeset
   683
    | NONE =>
58332
be0f5d8d511b imported patch phantoms
blanchet
parents: 58297
diff changeset
   684
      cache_comp key
be0f5d8d511b imported patch phantoms
blanchet
parents: 58297
diff changeset
   685
        (raw_compose_bnf const_policy qualify flatten_tyargs outer inners oDs Dss tfreess accum))
49014
332e5e661675 have "bnf_of_typ" command seal the BNF
blanchet
parents: 48975
diff changeset
   686
  end;
332e5e661675 have "bnf_of_typ" command seal the BNF
blanchet
parents: 48975
diff changeset
   687
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   688
(* Hide the type of the bound (optimization) and unfold the definitions (nicer to the user) *)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   689
55803
74d3fe9031d8 joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents: 55707
diff changeset
   690
type absT_info =
74d3fe9031d8 joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents: 55707
diff changeset
   691
  {absT: typ,
74d3fe9031d8 joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents: 55707
diff changeset
   692
   repT: typ,
74d3fe9031d8 joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents: 55707
diff changeset
   693
   abs: term,
74d3fe9031d8 joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents: 55707
diff changeset
   694
   rep: term,
74d3fe9031d8 joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents: 55707
diff changeset
   695
   abs_inject: thm,
74d3fe9031d8 joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents: 55707
diff changeset
   696
   abs_inverse: thm,
74d3fe9031d8 joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents: 55707
diff changeset
   697
   type_definition: thm};
74d3fe9031d8 joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents: 55707
diff changeset
   698
74d3fe9031d8 joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents: 55707
diff changeset
   699
fun morph_absT_info phi
74d3fe9031d8 joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents: 55707
diff changeset
   700
  {absT, repT, abs, rep, abs_inject, abs_inverse, type_definition} =
74d3fe9031d8 joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents: 55707
diff changeset
   701
  {absT = Morphism.typ phi absT,
74d3fe9031d8 joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents: 55707
diff changeset
   702
   repT = Morphism.typ phi repT,
74d3fe9031d8 joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents: 55707
diff changeset
   703
   abs = Morphism.term phi abs,
74d3fe9031d8 joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents: 55707
diff changeset
   704
   rep = Morphism.term phi rep,
74d3fe9031d8 joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents: 55707
diff changeset
   705
   abs_inject = Morphism.thm phi abs_inject,
74d3fe9031d8 joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents: 55707
diff changeset
   706
   abs_inverse = Morphism.thm phi abs_inverse,
74d3fe9031d8 joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents: 55707
diff changeset
   707
   type_definition = Morphism.thm phi type_definition};
74d3fe9031d8 joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents: 55707
diff changeset
   708
74d3fe9031d8 joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents: 55707
diff changeset
   709
fun mk_absT thy repT absT repU =
55900
21aa30ea6806 propagate the exception that is expected later on
traytel
parents: 55856
diff changeset
   710
  let
56634
a001337c8d24 tuned whitespace
blanchet
parents: 56254
diff changeset
   711
    val rho = Vartab.fold (cons o apsnd snd) (Sign.typ_match thy (repT, repU) Vartab.empty) [];
55900
21aa30ea6806 propagate the exception that is expected later on
traytel
parents: 55856
diff changeset
   712
  in Term.typ_subst_TVars rho absT end
21aa30ea6806 propagate the exception that is expected later on
traytel
parents: 55856
diff changeset
   713
  handle Type.TYPE_MATCH => raise Term.TYPE ("mk_absT", [repT, absT, repU], []);
55803
74d3fe9031d8 joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents: 55707
diff changeset
   714
55854
ee270328a781 make 'typedef' optional, depending on size of original type
blanchet
parents: 55853
diff changeset
   715
fun mk_repT absT repT absU =
ee270328a781 make 'typedef' optional, depending on size of original type
blanchet
parents: 55853
diff changeset
   716
  if absT = repT then absU
ee270328a781 make 'typedef' optional, depending on size of original type
blanchet
parents: 55853
diff changeset
   717
  else
ee270328a781 make 'typedef' optional, depending on size of original type
blanchet
parents: 55853
diff changeset
   718
    (case (absT, absU) of
ee270328a781 make 'typedef' optional, depending on size of original type
blanchet
parents: 55853
diff changeset
   719
      (Type (C, Ts), Type (C', Us)) =>
ee270328a781 make 'typedef' optional, depending on size of original type
blanchet
parents: 55853
diff changeset
   720
        if C = C' then Term.typ_subst_atomic (Ts ~~ Us) repT
ee270328a781 make 'typedef' optional, depending on size of original type
blanchet
parents: 55853
diff changeset
   721
        else raise Term.TYPE ("mk_repT", [absT, repT, absT], [])
ee270328a781 make 'typedef' optional, depending on size of original type
blanchet
parents: 55853
diff changeset
   722
    | _ => raise Term.TYPE ("mk_repT", [absT, repT, absT], []));
55803
74d3fe9031d8 joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents: 55707
diff changeset
   723
58181
6d527272f7b2 renamed internal constant
blanchet
parents: 58128
diff changeset
   724
fun mk_abs_or_rep _ absU (Const (@{const_name id_bnf}, _)) =
6d527272f7b2 renamed internal constant
blanchet
parents: 58128
diff changeset
   725
    Const (@{const_name id_bnf}, absU --> absU)
55854
ee270328a781 make 'typedef' optional, depending on size of original type
blanchet
parents: 55853
diff changeset
   726
  | mk_abs_or_rep getT (Type (_, Us)) abs =
ee270328a781 make 'typedef' optional, depending on size of original type
blanchet
parents: 55853
diff changeset
   727
    let val Ts = snd (dest_Type (getT (fastype_of abs)))
ee270328a781 make 'typedef' optional, depending on size of original type
blanchet
parents: 55853
diff changeset
   728
    in Term.subst_atomic_types (Ts ~~ Us) abs end;
55803
74d3fe9031d8 joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents: 55707
diff changeset
   729
74d3fe9031d8 joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents: 55707
diff changeset
   730
val mk_abs = mk_abs_or_rep range_type;
74d3fe9031d8 joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents: 55707
diff changeset
   731
val mk_rep = mk_abs_or_rep domain_type;
74d3fe9031d8 joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents: 55707
diff changeset
   732
55854
ee270328a781 make 'typedef' optional, depending on size of original type
blanchet
parents: 55853
diff changeset
   733
val smart_max_inline_type_size = 5; (*FUDGE*)
ee270328a781 make 'typedef' optional, depending on size of original type
blanchet
parents: 55853
diff changeset
   734
58332
be0f5d8d511b imported patch phantoms
blanchet
parents: 58297
diff changeset
   735
fun maybe_typedef force_out_of_line (b, As, mx) set opt_morphs tac =
55854
ee270328a781 make 'typedef' optional, depending on size of original type
blanchet
parents: 55853
diff changeset
   736
  let
ee270328a781 make 'typedef' optional, depending on size of original type
blanchet
parents: 55853
diff changeset
   737
    val repT = HOLogic.dest_setT (fastype_of set);
58332
be0f5d8d511b imported patch phantoms
blanchet
parents: 58297
diff changeset
   738
    val out_of_line = force_out_of_line orelse Term.size_of_typ repT > smart_max_inline_type_size;
55854
ee270328a781 make 'typedef' optional, depending on size of original type
blanchet
parents: 55853
diff changeset
   739
  in
58332
be0f5d8d511b imported patch phantoms
blanchet
parents: 58297
diff changeset
   740
    if out_of_line then
be0f5d8d511b imported patch phantoms
blanchet
parents: 58297
diff changeset
   741
      typedef (b, As, mx) set opt_morphs tac
be0f5d8d511b imported patch phantoms
blanchet
parents: 58297
diff changeset
   742
      #>> (fn (T_name, ({Rep_name, Abs_name, ...},
be0f5d8d511b imported patch phantoms
blanchet
parents: 58297
diff changeset
   743
          {type_definition, Abs_inverse, Abs_inject, Abs_cases, ...}) : Typedef.info) =>
be0f5d8d511b imported patch phantoms
blanchet
parents: 58297
diff changeset
   744
        (Type (T_name, map TFree As),
be0f5d8d511b imported patch phantoms
blanchet
parents: 58297
diff changeset
   745
          (Rep_name, Abs_name, type_definition, Abs_inverse, Abs_inject, Abs_cases)))
be0f5d8d511b imported patch phantoms
blanchet
parents: 58297
diff changeset
   746
    else
55854
ee270328a781 make 'typedef' optional, depending on size of original type
blanchet
parents: 55853
diff changeset
   747
      pair (repT,
58181
6d527272f7b2 renamed internal constant
blanchet
parents: 58128
diff changeset
   748
        (@{const_name id_bnf}, @{const_name id_bnf},
6d527272f7b2 renamed internal constant
blanchet
parents: 58128
diff changeset
   749
         @{thm type_definition_id_bnf_UNIV},
6d527272f7b2 renamed internal constant
blanchet
parents: 58128
diff changeset
   750
         @{thm type_definition.Abs_inverse[OF type_definition_id_bnf_UNIV]},
6d527272f7b2 renamed internal constant
blanchet
parents: 58128
diff changeset
   751
         @{thm type_definition.Abs_inject[OF type_definition_id_bnf_UNIV]},
6d527272f7b2 renamed internal constant
blanchet
parents: 58128
diff changeset
   752
         @{thm type_definition.Abs_cases[OF type_definition_id_bnf_UNIV]}))
55854
ee270328a781 make 'typedef' optional, depending on size of original type
blanchet
parents: 55853
diff changeset
   753
  end;
ee270328a781 make 'typedef' optional, depending on size of original type
blanchet
parents: 55853
diff changeset
   754
58332
be0f5d8d511b imported patch phantoms
blanchet
parents: 58297
diff changeset
   755
fun seal_bnf qualify (unfold_set : unfold_set) b has_live_phantoms Ds bnf lthy =
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   756
  let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   757
    val live = live_of_bnf bnf;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   758
    val nwits = nwits_of_bnf bnf;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   759
58332
be0f5d8d511b imported patch phantoms
blanchet
parents: 58297
diff changeset
   760
    val ((As, As'), lthy1) = apfst (`(map TFree))
56254
a2dd9200854d more antiquotations;
wenzelm
parents: 56018
diff changeset
   761
      (Variable.invent_types (replicate live @{sort type}) (fold Variable.declare_typ Ds lthy));
58332
be0f5d8d511b imported patch phantoms
blanchet
parents: 58297
diff changeset
   762
    val (Bs, _) = apfst (map TFree) (Variable.invent_types (replicate live @{sort type}) lthy1);
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   763
55803
74d3fe9031d8 joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents: 55707
diff changeset
   764
    val (((fs, fs'), (Rs, Rs')), _(*names_lthy*)) = lthy
74d3fe9031d8 joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents: 55707
diff changeset
   765
      |> mk_Frees' "f" (map2 (curry op -->) As Bs)
55937
traytel
parents: 55935
diff changeset
   766
      ||>> mk_Frees' "R" (map2 mk_pred2T As Bs);
55803
74d3fe9031d8 joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents: 55707
diff changeset
   767
74d3fe9031d8 joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents: 55707
diff changeset
   768
    val repTA = mk_T_of_bnf Ds As bnf;
74d3fe9031d8 joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents: 55707
diff changeset
   769
    val T_bind = qualify b;
58332
be0f5d8d511b imported patch phantoms
blanchet
parents: 58297
diff changeset
   770
    val TA_params = Term.add_tfreesT repTA (if has_live_phantoms then As' else []);
56012
158dc03db8be made typedef for the type of the bound optional (size-based)
traytel
parents: 56010
diff changeset
   771
    val ((TA, (Rep_name, Abs_name, type_definition, Abs_inverse, Abs_inject, _)), lthy) =
58332
be0f5d8d511b imported patch phantoms
blanchet
parents: 58297
diff changeset
   772
      maybe_typedef has_live_phantoms (T_bind, TA_params, NoSyn) (HOLogic.mk_UNIV repTA) NONE
58959
1f195ed99941 proper proof context for typedef;
wenzelm
parents: 58634
diff changeset
   773
        (fn _ => EVERY' [rtac exI, rtac UNIV_I] 1) lthy;
55854
ee270328a781 make 'typedef' optional, depending on size of original type
blanchet
parents: 55853
diff changeset
   774
ee270328a781 make 'typedef' optional, depending on size of original type
blanchet
parents: 55853
diff changeset
   775
    val repTB = mk_T_of_bnf Ds Bs bnf;
ee270328a781 make 'typedef' optional, depending on size of original type
blanchet
parents: 55853
diff changeset
   776
    val TB = Term.typ_subst_atomic (As ~~ Bs) TA;
ee270328a781 make 'typedef' optional, depending on size of original type
blanchet
parents: 55853
diff changeset
   777
    val RepA = Const (Rep_name, TA --> repTA);
ee270328a781 make 'typedef' optional, depending on size of original type
blanchet
parents: 55853
diff changeset
   778
    val RepB = Const (Rep_name, TB --> repTB);
ee270328a781 make 'typedef' optional, depending on size of original type
blanchet
parents: 55853
diff changeset
   779
    val AbsA = Const (Abs_name, repTA --> TA);
ee270328a781 make 'typedef' optional, depending on size of original type
blanchet
parents: 55853
diff changeset
   780
    val AbsB = Const (Abs_name, repTB --> TB);
ee270328a781 make 'typedef' optional, depending on size of original type
blanchet
parents: 55853
diff changeset
   781
    val Abs_inject' = Abs_inject OF @{thms UNIV_I UNIV_I};
ee270328a781 make 'typedef' optional, depending on size of original type
blanchet
parents: 55853
diff changeset
   782
    val Abs_inverse' = Abs_inverse OF @{thms UNIV_I};
55803
74d3fe9031d8 joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents: 55707
diff changeset
   783
74d3fe9031d8 joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents: 55707
diff changeset
   784
    val absT_info = {absT = TA, repT = repTA, abs = AbsA, rep = RepA, abs_inject = Abs_inject',
55854
ee270328a781 make 'typedef' optional, depending on size of original type
blanchet
parents: 55853
diff changeset
   785
      abs_inverse = Abs_inverse', type_definition = type_definition};
55803
74d3fe9031d8 joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents: 55707
diff changeset
   786
74d3fe9031d8 joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents: 55707
diff changeset
   787
    val bnf_map = fold_rev Term.absfree fs' (HOLogic.mk_comp (HOLogic.mk_comp (AbsB,
56016
8875cdcfc85b unfold intermediate definitions after sealing the bnf
traytel
parents: 56013
diff changeset
   788
      Term.list_comb (mk_map_of_bnf Ds As Bs bnf, fs)), RepA));
8875cdcfc85b unfold intermediate definitions after sealing the bnf
traytel
parents: 56013
diff changeset
   789
    val bnf_sets = map ((fn t => HOLogic.mk_comp (t, RepA)))
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   790
      (mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf);
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   791
    val bnf_bd = mk_bd_of_bnf Ds As bnf;
55803
74d3fe9031d8 joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents: 55707
diff changeset
   792
    val bnf_rel = fold_rev Term.absfree Rs' (mk_vimage2p RepA RepB $
56016
8875cdcfc85b unfold intermediate definitions after sealing the bnf
traytel
parents: 56013
diff changeset
   793
      (Term.list_comb (mk_rel_of_bnf Ds As Bs bnf, Rs)));
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   794
55704
a97b9b81e195 optimized 'bnf_of_typ' further w.r.t. dead variables
blanchet
parents: 55703
diff changeset
   795
    (*bd may depend only on dead type variables*)
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   796
    val bd_repT = fst (dest_relT (fastype_of bnf_bd));
53264
1973b821168c qualify generated constants uniformly
blanchet
parents: 53222
diff changeset
   797
    val bdT_bind = qualify (Binding.suffix_name ("_" ^ bdTN) b);
55707
50cf04dd2584 clarified interaction with dead variables in the composition of BNFs
traytel
parents: 55706
diff changeset
   798
    val params = Term.add_tfreesT bd_repT [];
50cf04dd2584 clarified interaction with dead variables in the composition of BNFs
traytel
parents: 55706
diff changeset
   799
    val all_deads = map TFree (fold Term.add_tfreesT Ds []);
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   800
56012
158dc03db8be made typedef for the type of the bound optional (size-based)
traytel
parents: 56010
diff changeset
   801
    val ((bdT, (_, Abs_bd_name, _, _, Abs_bdT_inject, Abs_bdT_cases)), lthy) =
58332
be0f5d8d511b imported patch phantoms
blanchet
parents: 58297
diff changeset
   802
      maybe_typedef false (bdT_bind, params, NoSyn)
58959
1f195ed99941 proper proof context for typedef;
wenzelm
parents: 58634
diff changeset
   803
        (HOLogic.mk_UNIV bd_repT) NONE (fn _ => EVERY' [rtac exI, rtac UNIV_I] 1) lthy;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   804
56012
158dc03db8be made typedef for the type of the bound optional (size-based)
traytel
parents: 56010
diff changeset
   805
    val (bnf_bd', bd_ordIso, bd_card_order, bd_cinfinite) =
158dc03db8be made typedef for the type of the bound optional (size-based)
traytel
parents: 56010
diff changeset
   806
      if bdT = bd_repT then (bnf_bd, bd_Card_order_of_bnf bnf RS @{thm ordIso_refl},
158dc03db8be made typedef for the type of the bound optional (size-based)
traytel
parents: 56010
diff changeset
   807
        bd_card_order_of_bnf bnf, bd_cinfinite_of_bnf bnf)
158dc03db8be made typedef for the type of the bound optional (size-based)
traytel
parents: 56010
diff changeset
   808
      else
158dc03db8be made typedef for the type of the bound optional (size-based)
traytel
parents: 56010
diff changeset
   809
        let
158dc03db8be made typedef for the type of the bound optional (size-based)
traytel
parents: 56010
diff changeset
   810
          val bnf_bd' = mk_dir_image bnf_bd (Const (Abs_bd_name, bd_repT --> bdT));
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   811
56012
158dc03db8be made typedef for the type of the bound optional (size-based)
traytel
parents: 56010
diff changeset
   812
          val Abs_bdT_inj = mk_Abs_inj_thm Abs_bdT_inject;
158dc03db8be made typedef for the type of the bound optional (size-based)
traytel
parents: 56010
diff changeset
   813
          val Abs_bdT_bij = mk_Abs_bij_thm lthy Abs_bdT_inj Abs_bdT_cases;
57567
d554b0097ad4 add mk_Trueprop_mem utility function
desharna
parents: 56634
diff changeset
   814
56012
158dc03db8be made typedef for the type of the bound optional (size-based)
traytel
parents: 56010
diff changeset
   815
          val bd_ordIso = @{thm dir_image} OF [Abs_bdT_inj, bd_Card_order_of_bnf bnf];
158dc03db8be made typedef for the type of the bound optional (size-based)
traytel
parents: 56010
diff changeset
   816
          val bd_card_order =
158dc03db8be made typedef for the type of the bound optional (size-based)
traytel
parents: 56010
diff changeset
   817
            @{thm card_order_dir_image} OF [Abs_bdT_bij, bd_card_order_of_bnf bnf];
158dc03db8be made typedef for the type of the bound optional (size-based)
traytel
parents: 56010
diff changeset
   818
          val bd_cinfinite =
158dc03db8be made typedef for the type of the bound optional (size-based)
traytel
parents: 56010
diff changeset
   819
            (@{thm Cinfinite_cong} OF [bd_ordIso, bd_Cinfinite_of_bnf bnf]) RS conjunct1;
158dc03db8be made typedef for the type of the bound optional (size-based)
traytel
parents: 56010
diff changeset
   820
        in
158dc03db8be made typedef for the type of the bound optional (size-based)
traytel
parents: 56010
diff changeset
   821
          (bnf_bd', bd_ordIso, bd_card_order, bd_cinfinite)
158dc03db8be made typedef for the type of the bound optional (size-based)
traytel
parents: 56010
diff changeset
   822
        end;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   823
56016
8875cdcfc85b unfold intermediate definitions after sealing the bnf
traytel
parents: 56013
diff changeset
   824
    fun map_id0_tac _ =
8875cdcfc85b unfold intermediate definitions after sealing the bnf
traytel
parents: 56013
diff changeset
   825
      rtac (@{thm type_copy_map_id0} OF [type_definition, map_id0_of_bnf bnf]) 1;
8875cdcfc85b unfold intermediate definitions after sealing the bnf
traytel
parents: 56013
diff changeset
   826
    fun map_comp0_tac _ =
8875cdcfc85b unfold intermediate definitions after sealing the bnf
traytel
parents: 56013
diff changeset
   827
      rtac (@{thm type_copy_map_comp0} OF [type_definition, map_comp0_of_bnf bnf]) 1;
8875cdcfc85b unfold intermediate definitions after sealing the bnf
traytel
parents: 56013
diff changeset
   828
    fun map_cong0_tac _ =
8875cdcfc85b unfold intermediate definitions after sealing the bnf
traytel
parents: 56013
diff changeset
   829
      EVERY' (rtac @{thm type_copy_map_cong0} :: rtac (map_cong0_of_bnf bnf) ::
55803
74d3fe9031d8 joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents: 55707
diff changeset
   830
        map (fn i => EVERY' [select_prem_tac live (dtac meta_spec) i, etac meta_mp,
74d3fe9031d8 joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents: 55707
diff changeset
   831
          etac (o_apply RS equalityD2 RS set_mp)]) (1 upto live)) 1;
56016
8875cdcfc85b unfold intermediate definitions after sealing the bnf
traytel
parents: 56013
diff changeset
   832
    fun set_map0_tac thm _ =
8875cdcfc85b unfold intermediate definitions after sealing the bnf
traytel
parents: 56013
diff changeset
   833
      rtac (@{thm type_copy_set_map0} OF [type_definition, thm]) 1;
8875cdcfc85b unfold intermediate definitions after sealing the bnf
traytel
parents: 56013
diff changeset
   834
    val set_bd_tacs = map (fn thm => fn _ => rtac (@{thm ordLeq_ordIso_trans} OF
8875cdcfc85b unfold intermediate definitions after sealing the bnf
traytel
parents: 56013
diff changeset
   835
        [thm, bd_ordIso] RS @{thm type_copy_set_bd}) 1) (set_bd_of_bnf bnf);
8875cdcfc85b unfold intermediate definitions after sealing the bnf
traytel
parents: 56013
diff changeset
   836
    fun le_rel_OO_tac _ =
8875cdcfc85b unfold intermediate definitions after sealing the bnf
traytel
parents: 56013
diff changeset
   837
      rtac (le_rel_OO_of_bnf bnf RS @{thm vimage2p_relcompp_mono}) 1;
55803
74d3fe9031d8 joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents: 55707
diff changeset
   838
    fun rel_OO_Grp_tac ctxt =
56016
8875cdcfc85b unfold intermediate definitions after sealing the bnf
traytel
parents: 56013
diff changeset
   839
      (rtac (rel_OO_Grp_of_bnf bnf RS @{thm vimage2p_cong} RS trans) THEN'
58359
3782c7b0d1cc avoid 'subst_tac' when possible (it is suspected of not helping 'HOL-Proofs')
blanchet
parents: 58332
diff changeset
   840
       (if has_live_phantoms then subst_tac ctxt NONE else SELECT_GOAL o unfold_thms_tac ctxt)
3782c7b0d1cc avoid 'subst_tac' when possible (it is suspected of not helping 'HOL-Proofs')
blanchet
parents: 58332
diff changeset
   841
         [type_definition RS @{thm vimage2p_relcompp_converse}] THEN'
58332
be0f5d8d511b imported patch phantoms
blanchet
parents: 58297
diff changeset
   842
       SELECT_GOAL (unfold_thms_tac ctxt [o_apply,
be0f5d8d511b imported patch phantoms
blanchet
parents: 58297
diff changeset
   843
         type_definition RS @{thm type_copy_vimage2p_Grp_Rep},
be0f5d8d511b imported patch phantoms
blanchet
parents: 58297
diff changeset
   844
         type_definition RS @{thm vimage2p_relcompp_converse}]) THEN'
be0f5d8d511b imported patch phantoms
blanchet
parents: 58297
diff changeset
   845
       rtac refl) 1;
49456
fa8302c8dea1 adapted BNF composition to new relator approach
blanchet
parents: 49455
diff changeset
   846
55803
74d3fe9031d8 joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents: 55707
diff changeset
   847
    val tacs = zip_axioms map_id0_tac map_comp0_tac map_cong0_tac
74d3fe9031d8 joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents: 55707
diff changeset
   848
      (map set_map0_tac (set_map0_of_bnf bnf)) (K (rtac bd_card_order 1)) (K (rtac bd_cinfinite 1))
74d3fe9031d8 joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents: 55707
diff changeset
   849
      set_bd_tacs le_rel_OO_tac rel_OO_Grp_tac;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   850
55803
74d3fe9031d8 joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents: 55707
diff changeset
   851
    val bnf_wits = map (fn (I, t) =>
74d3fe9031d8 joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents: 55707
diff changeset
   852
        fold Term.absdummy (map (nth As) I)
56016
8875cdcfc85b unfold intermediate definitions after sealing the bnf
traytel
parents: 56013
diff changeset
   853
          (AbsA $ Term.list_comb (t, map Bound (0 upto length I - 1))))
55803
74d3fe9031d8 joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents: 55707
diff changeset
   854
      (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   855
56016
8875cdcfc85b unfold intermediate definitions after sealing the bnf
traytel
parents: 56013
diff changeset
   856
    fun wit_tac _ = ALLGOALS (dtac (type_definition RS @{thm type_copy_wit})) THEN
8875cdcfc85b unfold intermediate definitions after sealing the bnf
traytel
parents: 56013
diff changeset
   857
      mk_simple_wit_tac (wit_thms_of_bnf bnf);
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   858
53264
1973b821168c qualify generated constants uniformly
blanchet
parents: 53222
diff changeset
   859
    val (bnf', lthy') =
56016
8875cdcfc85b unfold intermediate definitions after sealing the bnf
traytel
parents: 56013
diff changeset
   860
      bnf_def Hardly_Inline (user_policy Dont_Note) true qualify tacs wit_tac (SOME all_deads)
53264
1973b821168c qualify generated constants uniformly
blanchet
parents: 53222
diff changeset
   861
        Binding.empty Binding.empty []
55803
74d3fe9031d8 joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents: 55707
diff changeset
   862
        ((((((b, TA), bnf_map), bnf_sets), bnf_bd'), bnf_wits), SOME bnf_rel) lthy;
56016
8875cdcfc85b unfold intermediate definitions after sealing the bnf
traytel
parents: 56013
diff changeset
   863
58181
6d527272f7b2 renamed internal constant
blanchet
parents: 58128
diff changeset
   864
    val unfolds = @{thm id_bnf_apply} ::
56016
8875cdcfc85b unfold intermediate definitions after sealing the bnf
traytel
parents: 56013
diff changeset
   865
      (#map_unfolds unfold_set @ flat (#set_unfoldss unfold_set) @ #rel_unfolds unfold_set);
8875cdcfc85b unfold intermediate definitions after sealing the bnf
traytel
parents: 56013
diff changeset
   866
8875cdcfc85b unfold intermediate definitions after sealing the bnf
traytel
parents: 56013
diff changeset
   867
    val bnf'' = bnf' |> morph_bnf_defs (Morphism.thm_morphism "BNF" (unfold_thms lthy' unfolds));
57567
d554b0097ad4 add mk_Trueprop_mem utility function
desharna
parents: 56634
diff changeset
   868
56016
8875cdcfc85b unfold intermediate definitions after sealing the bnf
traytel
parents: 56013
diff changeset
   869
    val map_def = map_def_of_bnf bnf'';
8875cdcfc85b unfold intermediate definitions after sealing the bnf
traytel
parents: 56013
diff changeset
   870
    val set_defs = set_defs_of_bnf bnf'';
56018
c3fc8692dbc1 copy-paste typo
traytel
parents: 56016
diff changeset
   871
    val rel_def = rel_def_of_bnf bnf'';
56016
8875cdcfc85b unfold intermediate definitions after sealing the bnf
traytel
parents: 56013
diff changeset
   872
8875cdcfc85b unfold intermediate definitions after sealing the bnf
traytel
parents: 56013
diff changeset
   873
    val bnf_b = qualify b;
8875cdcfc85b unfold intermediate definitions after sealing the bnf
traytel
parents: 56013
diff changeset
   874
    val def_qualify =
8875cdcfc85b unfold intermediate definitions after sealing the bnf
traytel
parents: 56013
diff changeset
   875
      Thm.def_binding o Binding.conceal o Binding.qualify false (Binding.name_of bnf_b);
8875cdcfc85b unfold intermediate definitions after sealing the bnf
traytel
parents: 56013
diff changeset
   876
    fun mk_prefix_binding pre = Binding.prefix_name (pre ^ "_") bnf_b;
8875cdcfc85b unfold intermediate definitions after sealing the bnf
traytel
parents: 56013
diff changeset
   877
    val map_b = def_qualify (mk_prefix_binding mapN);
8875cdcfc85b unfold intermediate definitions after sealing the bnf
traytel
parents: 56013
diff changeset
   878
    val rel_b = def_qualify (mk_prefix_binding relN);
8875cdcfc85b unfold intermediate definitions after sealing the bnf
traytel
parents: 56013
diff changeset
   879
    val set_bs = if live = 1 then [def_qualify (mk_prefix_binding setN)]
8875cdcfc85b unfold intermediate definitions after sealing the bnf
traytel
parents: 56013
diff changeset
   880
      else map (fn i => def_qualify (mk_prefix_binding (mk_setN i))) (1 upto live);
8875cdcfc85b unfold intermediate definitions after sealing the bnf
traytel
parents: 56013
diff changeset
   881
8875cdcfc85b unfold intermediate definitions after sealing the bnf
traytel
parents: 56013
diff changeset
   882
    val notes = (map_b, map_def) :: (rel_b, rel_def) :: (set_bs ~~ set_defs)
8875cdcfc85b unfold intermediate definitions after sealing the bnf
traytel
parents: 56013
diff changeset
   883
      |> map (fn (b, def) => ((b, []), [([def], [])]))
57632
231e90cf2892 use the noted theorems in 'BNF_Comp'
blanchet
parents: 57567
diff changeset
   884
231e90cf2892 use the noted theorems in 'BNF_Comp'
blanchet
parents: 57567
diff changeset
   885
    val (noted, lthy'') = lthy' |> Local_Theory.notes notes
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   886
  in
57632
231e90cf2892 use the noted theorems in 'BNF_Comp'
blanchet
parents: 57567
diff changeset
   887
    ((morph_bnf (substitute_noted_thm noted) bnf'', (all_deads, absT_info)), lthy'')
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   888
  end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   889
53222
8b159677efb5 better error message
blanchet
parents: 53040
diff changeset
   890
exception BAD_DEAD of typ * typ;
8b159677efb5 better error message
blanchet
parents: 53040
diff changeset
   891
55704
a97b9b81e195 optimized 'bnf_of_typ' further w.r.t. dead variables
blanchet
parents: 55703
diff changeset
   892
fun bnf_of_typ _ _ _ _ Ds0 (T as TFree T') accum =
a97b9b81e195 optimized 'bnf_of_typ' further w.r.t. dead variables
blanchet
parents: 55703
diff changeset
   893
    (if member (op =) Ds0 T' then (DEADID_bnf, ([T], [])) else (ID_bnf, ([], [T])), accum)
55703
a21069381ba5 optimization of 'bnf_of_typ' if all variables are dead
blanchet
parents: 55480
diff changeset
   894
  | bnf_of_typ _ _ _ _ _ (TVar _) _ = error "Unexpected schematic variable"
58332
be0f5d8d511b imported patch phantoms
blanchet
parents: 58297
diff changeset
   895
  | bnf_of_typ const_policy qualify' flatten_tyargs Xs Ds0 (T as Type (C, Ts))
be0f5d8d511b imported patch phantoms
blanchet
parents: 58297
diff changeset
   896
      (accum as (_, lthy)) =
49186
4b5fa9d5e330 handle type constructors not known to be a BNF using the DEADID BNF
traytel
parents: 49185
diff changeset
   897
    let
53222
8b159677efb5 better error message
blanchet
parents: 53040
diff changeset
   898
      fun check_bad_dead ((_, (deads, _)), _) =
8b159677efb5 better error message
blanchet
parents: 53040
diff changeset
   899
        let val Ds = fold Term.add_tfreesT deads [] in
8b159677efb5 better error message
blanchet
parents: 53040
diff changeset
   900
          (case Library.inter (op =) Ds Xs of [] => ()
55705
a98a045a6169 updated docs
blanchet
parents: 55704
diff changeset
   901
          | X :: _ => raise BAD_DEAD (TFree X, T))
53222
8b159677efb5 better error message
blanchet
parents: 53040
diff changeset
   902
        end;
8b159677efb5 better error message
blanchet
parents: 53040
diff changeset
   903
55704
a97b9b81e195 optimized 'bnf_of_typ' further w.r.t. dead variables
blanchet
parents: 55703
diff changeset
   904
      val tfrees = subtract (op =) Ds0 (Term.add_tfreesT T []);
a97b9b81e195 optimized 'bnf_of_typ' further w.r.t. dead variables
blanchet
parents: 55703
diff changeset
   905
      val bnf_opt = if null tfrees then NONE else bnf_of lthy C;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   906
    in
49186
4b5fa9d5e330 handle type constructors not known to be a BNF using the DEADID BNF
traytel
parents: 49185
diff changeset
   907
      (case bnf_opt of
55704
a97b9b81e195 optimized 'bnf_of_typ' further w.r.t. dead variables
blanchet
parents: 55703
diff changeset
   908
        NONE => ((DEADID_bnf, ([T], [])), accum)
49186
4b5fa9d5e330 handle type constructors not known to be a BNF using the DEADID BNF
traytel
parents: 49185
diff changeset
   909
      | SOME bnf =>
4b5fa9d5e330 handle type constructors not known to be a BNF using the DEADID BNF
traytel
parents: 49185
diff changeset
   910
        if forall (can Term.dest_TFree) Ts andalso length Ts = length tfrees then
4b5fa9d5e330 handle type constructors not known to be a BNF using the DEADID BNF
traytel
parents: 49185
diff changeset
   911
          let
4b5fa9d5e330 handle type constructors not known to be a BNF using the DEADID BNF
traytel
parents: 49185
diff changeset
   912
            val T' = T_of_bnf bnf;
4b5fa9d5e330 handle type constructors not known to be a BNF using the DEADID BNF
traytel
parents: 49185
diff changeset
   913
            val deads = deads_of_bnf bnf;
4b5fa9d5e330 handle type constructors not known to be a BNF using the DEADID BNF
traytel
parents: 49185
diff changeset
   914
            val lives = lives_of_bnf bnf;
4b5fa9d5e330 handle type constructors not known to be a BNF using the DEADID BNF
traytel
parents: 49185
diff changeset
   915
            val tvars' = Term.add_tvarsT T' [];
55904
0ef30d52c5e4 more caching in composition pipeline
blanchet
parents: 55900
diff changeset
   916
            val Ds_As =
59058
a78612c67ec0 renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents: 58959
diff changeset
   917
              apply2 (map (Term.typ_subst_TVars (map fst tvars' ~~ map TFree tfrees)))
49186
4b5fa9d5e330 handle type constructors not known to be a BNF using the DEADID BNF
traytel
parents: 49185
diff changeset
   918
                (deads, lives);
55904
0ef30d52c5e4 more caching in composition pipeline
blanchet
parents: 55900
diff changeset
   919
          in ((bnf, Ds_As), accum) end
49186
4b5fa9d5e330 handle type constructors not known to be a BNF using the DEADID BNF
traytel
parents: 49185
diff changeset
   920
        else
4b5fa9d5e330 handle type constructors not known to be a BNF using the DEADID BNF
traytel
parents: 49185
diff changeset
   921
          let
49425
f27f83f71e94 cleaned up internal naming scheme for bnfs
traytel
parents: 49304
diff changeset
   922
            val name = Long_Name.base_name C;
f27f83f71e94 cleaned up internal naming scheme for bnfs
traytel
parents: 49304
diff changeset
   923
            fun qualify i =
f27f83f71e94 cleaned up internal naming scheme for bnfs
traytel
parents: 49304
diff changeset
   924
              let val namei = name ^ nonzero_string_of_int i;
f27f83f71e94 cleaned up internal naming scheme for bnfs
traytel
parents: 49304
diff changeset
   925
              in qualify' o Binding.qualify true namei end;
49186
4b5fa9d5e330 handle type constructors not known to be a BNF using the DEADID BNF
traytel
parents: 49185
diff changeset
   926
            val odead = dead_of_bnf bnf;
4b5fa9d5e330 handle type constructors not known to be a BNF using the DEADID BNF
traytel
parents: 49185
diff changeset
   927
            val olive = live_of_bnf bnf;
59131
894d613f7f7c respect order of deads when retrieving bnfs from the database
traytel
parents: 59058
diff changeset
   928
            val Ds = map (fn i => TFree (string_of_int i, [])) (1 upto odead);
894d613f7f7c respect order of deads when retrieving bnfs from the database
traytel
parents: 59058
diff changeset
   929
            val Us = snd (Term.dest_Type (mk_T_of_bnf Ds (replicate olive dummyT) bnf));
894d613f7f7c respect order of deads when retrieving bnfs from the database
traytel
parents: 59058
diff changeset
   930
            val oDs_pos = map (fn x => find_index (fn y => x = y) Us) Ds
894d613f7f7c respect order of deads when retrieving bnfs from the database
traytel
parents: 59058
diff changeset
   931
              |> filter (fn x => x >= 0);
49186
4b5fa9d5e330 handle type constructors not known to be a BNF using the DEADID BNF
traytel
parents: 49185
diff changeset
   932
            val oDs = map (nth Ts) oDs_pos;
4b5fa9d5e330 handle type constructors not known to be a BNF using the DEADID BNF
traytel
parents: 49185
diff changeset
   933
            val Ts' = map (nth Ts) (subtract (op =) oDs_pos (0 upto length Ts - 1));
55904
0ef30d52c5e4 more caching in composition pipeline
blanchet
parents: 55900
diff changeset
   934
            val ((inners, (Dss, Ass)), (accum', lthy')) =
49186
4b5fa9d5e330 handle type constructors not known to be a BNF using the DEADID BNF
traytel
parents: 49185
diff changeset
   935
              apfst (apsnd split_list o split_list)
58634
9f10d82e8188 added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents: 58359
diff changeset
   936
                (@{fold_map 2} (fn i => bnf_of_typ Smart_Inline (qualify i) flatten_tyargs Xs Ds0)
55706
064c7c249f55 added BNF cache (within one definition)
blanchet
parents: 55705
diff changeset
   937
                (if length Ts' = 1 then [0] else (1 upto length Ts')) Ts' accum);
49186
4b5fa9d5e330 handle type constructors not known to be a BNF using the DEADID BNF
traytel
parents: 49185
diff changeset
   938
          in
58332
be0f5d8d511b imported patch phantoms
blanchet
parents: 58297
diff changeset
   939
            compose_bnf const_policy qualify flatten_tyargs bnf inners oDs Dss Ass (accum', lthy')
49186
4b5fa9d5e330 handle type constructors not known to be a BNF using the DEADID BNF
traytel
parents: 49185
diff changeset
   940
          end)
53222
8b159677efb5 better error message
blanchet
parents: 53040
diff changeset
   941
      |> tap check_bad_dead
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   942
    end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   943
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   944
end;