src/HOL/Tools/BNF/bnf_lfp.ML
author traytel
Wed, 26 Feb 2014 23:09:29 +0100
changeset 55770 f2cf7f92c9ac
parent 55756 565a20b22f09
child 55803 74d3fe9031d8
permissions -rw-r--r--
intermediate typedef for the type of the bound (local to lfp)
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_lfp.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:     Andrei Popescu, 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
Datatype construction.
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_LFP =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    10
sig
51867
6d756057e736 signature tuning
blanchet
parents: 51866
diff changeset
    11
  val construct_lfp: mixfix list -> binding list -> binding list -> binding list list ->
6d756057e736 signature tuning
blanchet
parents: 51866
diff changeset
    12
    binding list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list ->
51866
142a82883831 removed dead code
blanchet
parents: 51865
diff changeset
    13
    local_theory -> BNF_FP_Util.fp_result * local_theory
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    14
end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    15
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    16
structure BNF_LFP : BNF_LFP =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    17
struct
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    18
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    19
open BNF_Def
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    20
open BNF_Util
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    21
open BNF_Tactics
49585
5c4a12550491 generate high-level "maps", "sets", and "rels" properties
blanchet
parents: 49584
diff changeset
    22
open BNF_Comp
51850
106afdf5806c renamed a few FP-related files, to make it clear that these are not the sum of LFP + GFP but rather shared basic libraries
blanchet
parents: 51839
diff changeset
    23
open BNF_FP_Util
49636
b7256a88a84b renamed ML file in preparation for next step
blanchet
parents: 49635
diff changeset
    24
open BNF_FP_Def_Sugar
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    25
open BNF_LFP_Util
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    26
open BNF_LFP_Tactics
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    27
49460
4dd451a075ce fixed infinite loop with trivial rel_O_Gr + tuning
blanchet
parents: 49459
diff changeset
    28
(*all BNFs have the same lives*)
54557
d71c2737ee21 correctly account for dead variables when naming set functions
blanchet
parents: 54492
diff changeset
    29
fun construct_lfp mixfixes map_bs rel_bs set_bss0 bs resBs (resDs, Dss) bnfs lthy =
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    30
  let
53143
ba80154a1118 configuration option to control timing output for (co)datatypes
traytel
parents: 53138
diff changeset
    31
    val time = time lthy;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    32
    val timer = time (Timer.startRealTimer ());
49580
040cfb087b3a leave out some internal theorems unless "bnf_note_all" is set
blanchet
parents: 49545
diff changeset
    33
49132
81487fc17185 added robustness
blanchet
parents: 49128
diff changeset
    34
    val live = live_of_bnf (hd bnfs);
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    35
    val n = length bnfs; (*active*)
49132
81487fc17185 added robustness
blanchet
parents: 49128
diff changeset
    36
    val ks = 1 upto n;
49460
4dd451a075ce fixed infinite loop with trivial rel_O_Gr + tuning
blanchet
parents: 49459
diff changeset
    37
    val m = live - n; (*passive, if 0 don't generate a new BNF*)
53566
5ff3a2d112d7 conceal internal bindings
traytel
parents: 53310
diff changeset
    38
5ff3a2d112d7 conceal internal bindings
traytel
parents: 53310
diff changeset
    39
    val note_all = Config.get lthy bnf_note_all;
52956
1b62f05ab4fd honor user tfree names
blanchet
parents: 52938
diff changeset
    40
    val b_names = map Binding.name_of bs;
53566
5ff3a2d112d7 conceal internal bindings
traytel
parents: 53310
diff changeset
    41
    val b_name = mk_common_name b_names;
5ff3a2d112d7 conceal internal bindings
traytel
parents: 53310
diff changeset
    42
    val b = Binding.name b_name;
5ff3a2d112d7 conceal internal bindings
traytel
parents: 53310
diff changeset
    43
    val mk_internal_b = Binding.name #> Binding.prefix true b_name #> Binding.conceal;
5ff3a2d112d7 conceal internal bindings
traytel
parents: 53310
diff changeset
    44
    fun mk_internal_bs name =
5ff3a2d112d7 conceal internal bindings
traytel
parents: 53310
diff changeset
    45
      map (fn b =>
54492
6fae4ecd4ab3 prefix internal names as well
blanchet
parents: 54487
diff changeset
    46
        Binding.prefix true b_name (Binding.prefix_name (name ^ "_") b) |> Binding.conceal) bs;
53566
5ff3a2d112d7 conceal internal bindings
traytel
parents: 53310
diff changeset
    47
    val external_bs = map2 (Binding.prefix false) b_names bs
5ff3a2d112d7 conceal internal bindings
traytel
parents: 53310
diff changeset
    48
      |> note_all = false ? map Binding.conceal;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    49
49460
4dd451a075ce fixed infinite loop with trivial rel_O_Gr + tuning
blanchet
parents: 49459
diff changeset
    50
    (* TODO: check if m, n, etc., are sane *)
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    51
49185
073d7d1b7488 respect order of/additional type variables supplied by the user in fixed point constructions;
traytel
parents: 49176
diff changeset
    52
    val deads = fold (union (op =)) Dss resDs;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    53
    val names_lthy = fold Variable.declare_typ deads lthy;
52956
1b62f05ab4fd honor user tfree names
blanchet
parents: 52938
diff changeset
    54
    val passives = map fst (subtract (op = o apsnd TFree) deads resBs);
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    55
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    56
    (* tvars *)
54841
af71b753c459 express weak pullback property of bnfs only in terms of the relator
traytel
parents: 54793
diff changeset
    57
    val (((((passiveAs, activeAs), passiveBs), activeBs), passiveCs), activeCs) =
52938
3b3e52d5e66b tuned name generation code (to make it easier to adapt later)
blanchet
parents: 52923
diff changeset
    58
      names_lthy
52956
1b62f05ab4fd honor user tfree names
blanchet
parents: 52938
diff changeset
    59
      |> variant_tfrees passives
52938
3b3e52d5e66b tuned name generation code (to make it easier to adapt later)
blanchet
parents: 52923
diff changeset
    60
      ||>> mk_TFrees n
52956
1b62f05ab4fd honor user tfree names
blanchet
parents: 52938
diff changeset
    61
      ||>> variant_tfrees passives
52938
3b3e52d5e66b tuned name generation code (to make it easier to adapt later)
blanchet
parents: 52923
diff changeset
    62
      ||>> mk_TFrees n
54841
af71b753c459 express weak pullback property of bnfs only in terms of the relator
traytel
parents: 54793
diff changeset
    63
      ||>> variant_tfrees passives
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    64
      ||>> mk_TFrees n
54841
af71b753c459 express weak pullback property of bnfs only in terms of the relator
traytel
parents: 54793
diff changeset
    65
      |> fst;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    66
52938
3b3e52d5e66b tuned name generation code (to make it easier to adapt later)
blanchet
parents: 52923
diff changeset
    67
    val allAs = passiveAs @ activeAs;
3b3e52d5e66b tuned name generation code (to make it easier to adapt later)
blanchet
parents: 52923
diff changeset
    68
    val allBs' = passiveBs @ activeBs;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    69
    val Ass = replicate n allAs;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    70
    val allBs = passiveAs @ activeBs;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    71
    val Bss = replicate n allBs;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    72
    val allCs = passiveAs @ activeCs;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    73
    val allCs' = passiveBs @ activeCs;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    74
    val Css' = replicate n allCs';
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    75
51866
142a82883831 removed dead code
blanchet
parents: 51865
diff changeset
    76
    (* types *)
49185
073d7d1b7488 respect order of/additional type variables supplied by the user in fixed point constructions;
traytel
parents: 49176
diff changeset
    77
    val dead_poss =
52956
1b62f05ab4fd honor user tfree names
blanchet
parents: 52938
diff changeset
    78
      map (fn x => if member (op =) deads (TFree x) then SOME (TFree x) else NONE) resBs;
49185
073d7d1b7488 respect order of/additional type variables supplied by the user in fixed point constructions;
traytel
parents: 49176
diff changeset
    79
    fun mk_param NONE passive = (hd passive, tl passive)
073d7d1b7488 respect order of/additional type variables supplied by the user in fixed point constructions;
traytel
parents: 49176
diff changeset
    80
      | mk_param (SOME a) passive = (a, passive);
073d7d1b7488 respect order of/additional type variables supplied by the user in fixed point constructions;
traytel
parents: 49176
diff changeset
    81
    val mk_params = fold_map mk_param dead_poss #> fst;
073d7d1b7488 respect order of/additional type variables supplied by the user in fixed point constructions;
traytel
parents: 49176
diff changeset
    82
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    83
    fun mk_FTs Ts = map2 (fn Ds => mk_T_of_bnf Ds Ts) Dss bnfs;
49185
073d7d1b7488 respect order of/additional type variables supplied by the user in fixed point constructions;
traytel
parents: 49176
diff changeset
    84
    val (params, params') = `(map Term.dest_TFree) (mk_params passiveAs);
55770
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
    85
    val (dead_params, dead_params') = `(map Term.dest_TFree) (subtract (op =) passiveAs params');
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    86
    val FTsAs = mk_FTs allAs;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    87
    val FTsBs = mk_FTs allBs;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    88
    val FTsCs = mk_FTs allCs;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    89
    val BTs = map HOLogic.mk_setT activeAs;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    90
    val B'Ts = map HOLogic.mk_setT activeBs;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    91
    val B''Ts = map HOLogic.mk_setT activeCs;
52923
traytel
parents: 52913
diff changeset
    92
    val sTs = map2 (curry op -->) FTsAs activeAs;
traytel
parents: 52913
diff changeset
    93
    val s'Ts = map2 (curry op -->) FTsBs activeBs;
traytel
parents: 52913
diff changeset
    94
    val s''Ts = map2 (curry op -->) FTsCs activeCs;
traytel
parents: 52913
diff changeset
    95
    val fTs = map2 (curry op -->) activeAs activeBs;
traytel
parents: 52913
diff changeset
    96
    val inv_fTs = map2 (curry op -->) activeBs activeAs;
traytel
parents: 52913
diff changeset
    97
    val self_fTs = map2 (curry op -->) activeAs activeAs;
traytel
parents: 52913
diff changeset
    98
    val gTs = map2 (curry op -->) activeBs activeCs;
traytel
parents: 52913
diff changeset
    99
    val all_gTs = map2 (curry op -->) allBs allCs';
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   100
    val prodBsAs = map2 (curry HOLogic.mk_prodT) activeBs activeAs;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   101
    val prodFTs = mk_FTs (passiveAs @ prodBsAs);
52923
traytel
parents: 52913
diff changeset
   102
    val prod_sTs = map2 (curry op -->) prodFTs activeAs;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   103
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   104
    (* terms *)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   105
    val mapsAsAs = map4 mk_map_of_bnf Dss Ass Ass bnfs;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   106
    val mapsAsBs = map4 mk_map_of_bnf Dss Ass Bss bnfs;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   107
    val mapsBsAs = map4 mk_map_of_bnf Dss Bss Ass bnfs;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   108
    val mapsBsCs' = map4 mk_map_of_bnf Dss Bss Css' bnfs;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   109
    val mapsAsCs' = map4 mk_map_of_bnf Dss Ass Css' bnfs;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   110
    val map_fsts = map4 mk_map_of_bnf Dss (replicate n (passiveAs @ prodBsAs)) Bss bnfs;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   111
    val map_fsts_rev = map4 mk_map_of_bnf Dss Bss (replicate n (passiveAs @ prodBsAs)) bnfs;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   112
    fun mk_setss Ts = map3 mk_sets_of_bnf (map (replicate live) Dss)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   113
      (map (replicate live) (replicate n Ts)) bnfs;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   114
    val setssAs = mk_setss allAs;
52635
4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents: 52505
diff changeset
   115
    val bd0s = map3 mk_bd_of_bnf Dss Ass bnfs;
4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents: 52505
diff changeset
   116
    val bds =
4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents: 52505
diff changeset
   117
      map3 (fn bd0 => fn Ds => fn bnf => mk_csum bd0
4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents: 52505
diff changeset
   118
        (mk_card_of (HOLogic.mk_UNIV
4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents: 52505
diff changeset
   119
          (mk_T_of_bnf Ds (replicate live (fst (dest_relT (fastype_of bd0)))) bnf))))
4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents: 52505
diff changeset
   120
      bd0s Dss bnfs;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   121
    val witss = map wits_of_bnf bnfs;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   122
55756
565a20b22f09 made tactics more robust
traytel
parents: 55702
diff changeset
   123
    val (((((((((((((((((zs, zs'), Bs), Bs_copy), B's), B''s), ss), prod_ss), s's), s''s),
565a20b22f09 made tactics more robust
traytel
parents: 55702
diff changeset
   124
      fs), fs_copy), inv_fs), self_fs), gs), all_gs), (xFs, xFs')),
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   125
      names_lthy) = lthy
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   126
      |> mk_Frees' "z" activeAs
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   127
      ||>> mk_Frees "B" BTs
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   128
      ||>> mk_Frees "B" BTs
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   129
      ||>> mk_Frees "B'" B'Ts
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   130
      ||>> mk_Frees "B''" B''Ts
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   131
      ||>> mk_Frees "s" sTs
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   132
      ||>> mk_Frees "prods" prod_sTs
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   133
      ||>> mk_Frees "s'" s'Ts
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   134
      ||>> mk_Frees "s''" s''Ts
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   135
      ||>> mk_Frees "f" fTs
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   136
      ||>> mk_Frees "f" fTs
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   137
      ||>> mk_Frees "f" inv_fTs
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   138
      ||>> mk_Frees "f" self_fTs
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   139
      ||>> mk_Frees "g" gTs
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   140
      ||>> mk_Frees "g" all_gTs
55756
565a20b22f09 made tactics more robust
traytel
parents: 55702
diff changeset
   141
      ||>> mk_Frees' "x" FTsAs;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   142
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   143
    val passive_UNIVs = map HOLogic.mk_UNIV passiveAs;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   144
    val active_UNIVs = map HOLogic.mk_UNIV activeAs;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   145
    val prod_UNIVs = map HOLogic.mk_UNIV prodBsAs;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   146
    val passive_ids = map HOLogic.id_const passiveAs;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   147
    val active_ids = map HOLogic.id_const activeAs;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   148
    val fsts = map fst_const prodBsAs;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   149
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   150
    (* thms *)
52635
4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents: 52505
diff changeset
   151
    val bd0_card_orders = map bd_card_order_of_bnf bnfs;
4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents: 52505
diff changeset
   152
    val bd0_Card_orders = map bd_Card_order_of_bnf bnfs;
4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents: 52505
diff changeset
   153
    val bd0_Cinfinites = map bd_Cinfinite_of_bnf bnfs;
4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents: 52505
diff changeset
   154
    val set_bd0ss = map set_bd_of_bnf bnfs;
4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents: 52505
diff changeset
   155
4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents: 52505
diff changeset
   156
    val bd_card_orders =
4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents: 52505
diff changeset
   157
      map (fn thm => @{thm card_order_csum} OF [thm, @{thm card_of_card_order_on}]) bd0_card_orders;
4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents: 52505
diff changeset
   158
    val bd_Card_order = @{thm Card_order_csum};
4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents: 52505
diff changeset
   159
    val bd_Card_orders = replicate n bd_Card_order;
4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents: 52505
diff changeset
   160
    val bd_Cinfinites = map (fn thm => thm RS @{thm Cinfinite_csum1}) bd0_Cinfinites;
4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents: 52505
diff changeset
   161
    val bd_Cnotzeros = map (fn thm => thm RS @{thm Cinfinite_Cnotzero}) bd_Cinfinites;
4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents: 52505
diff changeset
   162
    val bd_Cinfinite = hd bd_Cinfinites;
4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents: 52505
diff changeset
   163
    val set_bdss =
4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents: 52505
diff changeset
   164
      map2 (fn set_bd0s => fn bd0_Card_order =>
4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents: 52505
diff changeset
   165
        map (fn thm => ctrans OF [thm, bd0_Card_order RS @{thm ordLeq_csum1}]) set_bd0s)
4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents: 52505
diff changeset
   166
      set_bd0ss bd0_Card_orders;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   167
    val in_bds = map in_bd_of_bnf bnfs;
53287
271b34513bfb renamed BNF axiom
blanchet
parents: 53285
diff changeset
   168
    val sym_map_comps = map (fn bnf => map_comp0_of_bnf bnf RS sym) bnfs;
53288
050d0bc9afa5 renamed BNF fact
blanchet
parents: 53287
diff changeset
   169
    val map_comps = map map_comp_of_bnf bnfs;
51761
4c9f08836d87 renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents: 51758
diff changeset
   170
    val map_cong0s = map map_cong0_of_bnf bnfs;
53270
c8628119d18e renamed BNF axiom
blanchet
parents: 53258
diff changeset
   171
    val map_id0s = map map_id0_of_bnf bnfs;
53285
f09645642984 renamed BNF fact
blanchet
parents: 53270
diff changeset
   172
    val map_ids = map map_id_of_bnf bnfs;
53290
b6c3be868217 renamed BNF fact
blanchet
parents: 53289
diff changeset
   173
    val set_mapss = map set_map_of_bnf bnfs;
54841
af71b753c459 express weak pullback property of bnfs only in terms of the relator
traytel
parents: 54793
diff changeset
   174
    val rel_mono_strongs = map rel_mono_strong_of_bnf bnfs;
af71b753c459 express weak pullback property of bnfs only in terms of the relator
traytel
parents: 54793
diff changeset
   175
    val rel_OOs = map rel_OO_of_bnf bnfs;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   176
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   177
    val timer = time (timer "Extracted terms & thms");
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   178
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   179
    (* nonemptiness check *)
51070
6ca703425c01 made SML/NJ happy
traytel
parents: 49835
diff changeset
   180
    fun new_wit X (wit: nonemptiness_witness) = subset (op =) (#I wit, (0 upto m - 1) @ map snd X);
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   181
49341
d406979024d1 nicer error message, indicating which type is empty (relying on metatheoretical completeness proof here)
blanchet
parents: 49337
diff changeset
   182
    val all = m upto m + n - 1;
d406979024d1 nicer error message, indicating which type is empty (relying on metatheoretical completeness proof here)
blanchet
parents: 49337
diff changeset
   183
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   184
    fun enrich X = map_filter (fn i =>
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   185
      (case find_first (fn (_, i') => i = i') X of
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   186
        NONE =>
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   187
          (case find_index (new_wit X) (nth witss (i - m)) of
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   188
            ~1 => NONE
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   189
          | j => SOME (j, i))
49341
d406979024d1 nicer error message, indicating which type is empty (relying on metatheoretical completeness proof here)
blanchet
parents: 49337
diff changeset
   190
      | SOME ji => SOME ji)) all;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   191
    val reachable = fixpoint (op =) enrich [];
49341
d406979024d1 nicer error message, indicating which type is empty (relying on metatheoretical completeness proof here)
blanchet
parents: 49337
diff changeset
   192
    val _ = (case subtract (op =) (map snd reachable) all of
d406979024d1 nicer error message, indicating which type is empty (relying on metatheoretical completeness proof here)
blanchet
parents: 49337
diff changeset
   193
        [] => ()
49390
a4202c1f4f9d tuned error message
blanchet
parents: 49362
diff changeset
   194
      | i :: _ => error ("Cannot define empty datatype " ^ quote (Binding.name_of (nth bs (i - m)))));
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   195
49341
d406979024d1 nicer error message, indicating which type is empty (relying on metatheoretical completeness proof here)
blanchet
parents: 49337
diff changeset
   196
    val wit_thms = flat (map2 (fn bnf => fn (j, _) => nth (wit_thmss_of_bnf bnf) j) bnfs reachable);
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   197
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   198
    val timer = time (timer "Checked nonemptiness");
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   199
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   200
    (* derived thms *)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   201
52956
1b62f05ab4fd honor user tfree names
blanchet
parents: 52938
diff changeset
   202
    (*map g1 ... gm g(m+1) ... g(m+n) (map id ... id f(m+1) ... f(m+n) x) =
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   203
      map g1 ... gm (g(m+1) o f(m+1)) ... (g(m+n) o f(m+n)) x*)
53287
271b34513bfb renamed BNF axiom
blanchet
parents: 53285
diff changeset
   204
    fun mk_map_comp_id x mapAsBs mapBsCs mapAsCs map_comp0 =
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   205
      let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   206
        val lhs = Term.list_comb (mapBsCs, all_gs) $
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   207
          (Term.list_comb (mapAsBs, passive_ids @ fs) $ x);
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   208
        val rhs = Term.list_comb (mapAsCs,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   209
          take m all_gs @ map HOLogic.mk_comp (drop m all_gs ~~ fs)) $ x;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   210
      in
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51070
diff changeset
   211
        Goal.prove_sorry lthy [] []
49123
263b0e330d8b more work on sugar + simplify Trueprop + eq idiom everywhere
blanchet
parents: 49121
diff changeset
   212
          (fold_rev Logic.all (x :: fs @ all_gs) (mk_Trueprop_eq (lhs, rhs)))
55756
565a20b22f09 made tactics more robust
traytel
parents: 55702
diff changeset
   213
          (fn {context = ctxt, prems = _} => mk_map_comp_id_tac ctxt map_comp0)
49109
0e5b859e1c91 no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
traytel
parents: 49074
diff changeset
   214
        |> Thm.close_derivation
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   215
      end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   216
53288
050d0bc9afa5 renamed BNF fact
blanchet
parents: 53287
diff changeset
   217
    val map_comp_id_thms = map5 mk_map_comp_id xFs mapsAsBs mapsBsCs' mapsAsCs' map_comps;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   218
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   219
    (*forall a : set(m+1) x. f(m+1) a = a; ...; forall a : set(m+n) x. f(m+n) a = a ==>
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   220
      map id ... id f(m+1) ... f(m+n) x = x*)
53285
f09645642984 renamed BNF fact
blanchet
parents: 53270
diff changeset
   221
    fun mk_map_cong0L x mapAsAs sets map_cong0 map_id =
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   222
      let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   223
        fun mk_prem set f z z' = HOLogic.mk_Trueprop
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   224
          (mk_Ball (set $ x) (Term.absfree z' (HOLogic.mk_eq (f $ z, z))));
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   225
        val prems = map4 mk_prem (drop m sets) self_fs zs zs';
49123
263b0e330d8b more work on sugar + simplify Trueprop + eq idiom everywhere
blanchet
parents: 49121
diff changeset
   226
        val goal = mk_Trueprop_eq (Term.list_comb (mapAsAs, passive_ids @ self_fs) $ x, x);
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   227
      in
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51070
diff changeset
   228
        Goal.prove_sorry lthy [] []
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   229
          (fold_rev Logic.all (x :: self_fs) (Logic.list_implies (prems, goal)))
53285
f09645642984 renamed BNF fact
blanchet
parents: 53270
diff changeset
   230
          (K (mk_map_cong0L_tac m map_cong0 map_id))
49109
0e5b859e1c91 no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
traytel
parents: 49074
diff changeset
   231
        |> Thm.close_derivation
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   232
      end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   233
53285
f09645642984 renamed BNF fact
blanchet
parents: 53270
diff changeset
   234
    val map_cong0L_thms = map5 mk_map_cong0L xFs mapsAsAs setssAs map_cong0s map_ids;
49585
5c4a12550491 generate high-level "maps", "sets", and "rels" properties
blanchet
parents: 49584
diff changeset
   235
    val in_mono'_thms = map (fn bnf => in_mono_of_bnf bnf OF (replicate m subset_refl)) bnfs;
5c4a12550491 generate high-level "maps", "sets", and "rels" properties
blanchet
parents: 49584
diff changeset
   236
    val in_cong'_thms = map (fn bnf => in_cong_of_bnf bnf OF (replicate m refl)) bnfs;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   237
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   238
    val timer = time (timer "Derived simple theorems");
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   239
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   240
    (* algebra *)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   241
53566
5ff3a2d112d7 conceal internal bindings
traytel
parents: 53310
diff changeset
   242
    val alg_bind = mk_internal_b algN;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   243
    val alg_def_bind = (Thm.def_binding alg_bind, []);
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   244
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   245
    (*forall i = 1 ... n: (\<forall>x \<in> Fi_in UNIV .. UNIV B1 ... Bn. si x \<in> Bi)*)
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   246
    val alg_spec =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   247
      let
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   248
        val ins = map3 mk_in (replicate n (passive_UNIVs @ Bs)) setssAs FTsAs;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   249
        fun mk_alg_conjunct B s X x x' =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   250
          mk_Ball X (Term.absfree x' (HOLogic.mk_mem (s $ x, B)));
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   251
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   252
        val rhs = Library.foldr1 HOLogic.mk_conj (map5 mk_alg_conjunct Bs ss ins xFs xFs')
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   253
      in
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   254
        fold_rev (Term.absfree o Term.dest_Free) (Bs @ ss) rhs
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   255
      end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   256
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   257
    val ((alg_free, (_, alg_def_free)), (lthy, lthy_old)) =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   258
        lthy
55204
345ee77213b5 use Local_Theory.define instead of Specification.definition for internal constants
traytel
parents: 55197
diff changeset
   259
        |> Local_Theory.define ((alg_bind, NoSyn), (alg_def_bind, alg_spec))
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   260
        ||> `Local_Theory.restore;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   261
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   262
    val phi = Proof_Context.export_morphism lthy_old lthy;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   263
    val alg = fst (Term.dest_Const (Morphism.term phi alg_free));
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   264
    val alg_def = mk_unabs_def (2 * n) (Morphism.thm phi alg_def_free RS meta_eq_to_obj_eq);
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   265
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   266
    fun mk_alg Bs ss =
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   267
      let
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   268
        val args = Bs @ ss;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   269
        val Ts = map fastype_of args;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   270
        val algT = Library.foldr (op -->) (Ts, HOLogic.boolT);
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   271
      in
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   272
        Term.list_comb (Const (alg, algT), args)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   273
      end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   274
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   275
    val alg_set_thms =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   276
      let
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   277
        val alg_prem = HOLogic.mk_Trueprop (mk_alg Bs ss);
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51869
diff changeset
   278
        fun mk_prem x set B = HOLogic.mk_Trueprop (mk_leq (set $ x) B);
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   279
        fun mk_concl s x B = HOLogic.mk_Trueprop (HOLogic.mk_mem (s $ x, B));
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   280
        val premss = map2 ((fn x => fn sets => map2 (mk_prem x) (drop m sets) Bs)) xFs setssAs;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   281
        val concls = map3 mk_concl ss xFs Bs;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   282
        val goals = map3 (fn x => fn prems => fn concl =>
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   283
          fold_rev Logic.all (x :: Bs @ ss)
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   284
            (Logic.list_implies (alg_prem :: prems, concl))) xFs premss concls;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   285
      in
49109
0e5b859e1c91 no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
traytel
parents: 49074
diff changeset
   286
        map (fn goal =>
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51070
diff changeset
   287
          Goal.prove_sorry lthy [] [] goal (K (mk_alg_set_tac alg_def)) |> Thm.close_derivation)
49109
0e5b859e1c91 no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
traytel
parents: 49074
diff changeset
   288
        goals
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   289
      end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   290
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   291
    fun mk_talg BTs = mk_alg (map HOLogic.mk_UNIV BTs);
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   292
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   293
    val talg_thm =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   294
      let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   295
        val goal = fold_rev Logic.all ss
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   296
          (HOLogic.mk_Trueprop (mk_talg activeAs ss))
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   297
      in
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51070
diff changeset
   298
        Goal.prove_sorry lthy [] [] goal
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   299
          (K (stac alg_def 1 THEN CONJ_WRAP (K (EVERY' [rtac ballI, rtac UNIV_I] 1)) ss))
49109
0e5b859e1c91 no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
traytel
parents: 49074
diff changeset
   300
        |> Thm.close_derivation
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   301
      end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   302
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   303
    val timer = time (timer "Algebra definition & thms");
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   304
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   305
    val alg_not_empty_thms =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   306
      let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   307
        val alg_prem =
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   308
          HOLogic.mk_Trueprop (mk_alg Bs ss);
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   309
        val concls = map (HOLogic.mk_Trueprop o mk_not_empty) Bs;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   310
        val goals =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   311
          map (fn concl =>
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   312
            fold_rev Logic.all (Bs @ ss) (Logic.mk_implies (alg_prem, concl))) concls;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   313
      in
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   314
        map2 (fn goal => fn alg_set =>
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51070
diff changeset
   315
          Goal.prove_sorry lthy [] []
51798
ad3a241def73 uniform Proof.context for hyp_subst_tac;
wenzelm
parents: 51782
diff changeset
   316
            goal (K (mk_alg_not_empty_tac lthy alg_set alg_set_thms wit_thms))
49109
0e5b859e1c91 no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
traytel
parents: 49074
diff changeset
   317
          |> Thm.close_derivation)
0e5b859e1c91 no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
traytel
parents: 49074
diff changeset
   318
        goals alg_set_thms
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   319
      end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   320
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   321
    val timer = time (timer "Proved nonemptiness");
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   322
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   323
    (* morphism *)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   324
53566
5ff3a2d112d7 conceal internal bindings
traytel
parents: 53310
diff changeset
   325
    val mor_bind = mk_internal_b morN;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   326
    val mor_def_bind = (Thm.def_binding mor_bind, []);
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   327
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   328
    (*fbetw) forall i = 1 ... n: (\<forall>x \<in> Bi. f x \<in> B'i)*)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   329
    (*mor) forall i = 1 ... n: (\<forall>x \<in> Fi_in UNIV ... UNIV B1 ... Bn.
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   330
       f (s1 x) = s1' (Fi_map id ... id f1 ... fn x))*)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   331
    val mor_spec =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   332
      let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   333
        fun mk_fbetw f B1 B2 z z' =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   334
          mk_Ball B1 (Term.absfree z' (HOLogic.mk_mem (f $ z, B2)));
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   335
        fun mk_mor sets mapAsBs f s s' T x x' =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   336
          mk_Ball (mk_in (passive_UNIVs @ Bs) sets T)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   337
            (Term.absfree x' (HOLogic.mk_eq (f $ (s $ x), s' $
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   338
              (Term.list_comb (mapAsBs, passive_ids @ fs) $ x))));
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   339
        val rhs = HOLogic.mk_conj
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   340
          (Library.foldr1 HOLogic.mk_conj (map5 mk_fbetw fs Bs B's zs zs'),
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   341
          Library.foldr1 HOLogic.mk_conj
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   342
            (map8 mk_mor setssAs mapsAsBs fs ss s's FTsAs xFs xFs'))
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   343
      in
55204
345ee77213b5 use Local_Theory.define instead of Specification.definition for internal constants
traytel
parents: 55197
diff changeset
   344
        fold_rev (Term.absfree o Term.dest_Free) (Bs @ ss @ B's @ s's @ fs) rhs
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   345
      end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   346
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   347
    val ((mor_free, (_, mor_def_free)), (lthy, lthy_old)) =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   348
        lthy
55204
345ee77213b5 use Local_Theory.define instead of Specification.definition for internal constants
traytel
parents: 55197
diff changeset
   349
        |> Local_Theory.define ((mor_bind, NoSyn), (mor_def_bind, mor_spec))
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   350
        ||> `Local_Theory.restore;
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
    val phi = Proof_Context.export_morphism lthy_old lthy;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   353
    val mor = fst (Term.dest_Const (Morphism.term phi mor_free));
55204
345ee77213b5 use Local_Theory.define instead of Specification.definition for internal constants
traytel
parents: 55197
diff changeset
   354
    val mor_def = mk_unabs_def (5 * n) (Morphism.thm phi mor_def_free RS meta_eq_to_obj_eq);
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   355
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   356
    fun mk_mor Bs1 ss1 Bs2 ss2 fs =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   357
      let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   358
        val args = Bs1 @ ss1 @ Bs2 @ ss2 @ fs;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   359
        val Ts = map fastype_of (Bs1 @ ss1 @ Bs2 @ ss2 @ fs);
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   360
        val morT = Library.foldr (op -->) (Ts, HOLogic.boolT);
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   361
      in
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   362
        Term.list_comb (Const (mor, morT), args)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   363
      end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   364
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   365
    val (mor_image_thms, morE_thms) =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   366
      let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   367
        val prem = HOLogic.mk_Trueprop (mk_mor Bs ss B's s's fs);
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   368
        fun mk_image_goal f B1 B2 = fold_rev Logic.all (Bs @ ss @ B's @ s's @ fs)
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51869
diff changeset
   369
          (Logic.mk_implies (prem, HOLogic.mk_Trueprop (mk_leq (mk_image f $ B1) B2)));
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   370
        val image_goals = map3 mk_image_goal fs Bs B's;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   371
        fun mk_elim_prem sets x T = HOLogic.mk_Trueprop
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   372
          (HOLogic.mk_mem (x, mk_in (passive_UNIVs @ Bs) sets T));
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   373
        fun mk_elim_goal sets mapAsBs f s s' x T =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   374
          fold_rev Logic.all (x :: Bs @ ss @ B's @ s's @ fs)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   375
            (Logic.list_implies ([prem, mk_elim_prem sets x T],
49123
263b0e330d8b more work on sugar + simplify Trueprop + eq idiom everywhere
blanchet
parents: 49121
diff changeset
   376
              mk_Trueprop_eq (f $ (s $ x), s' $ Term.list_comb (mapAsBs, passive_ids @ fs @ [x]))));
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   377
        val elim_goals = map7 mk_elim_goal setssAs mapsAsBs fs ss s's xFs FTsAs;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   378
        fun prove goal =
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51070
diff changeset
   379
          Goal.prove_sorry lthy [] [] goal (K (mk_mor_elim_tac mor_def)) |> Thm.close_derivation;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   380
      in
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   381
        (map prove image_goals, map prove elim_goals)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   382
      end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   383
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   384
    val mor_incl_thm =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   385
      let
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51869
diff changeset
   386
        val prems = map2 (HOLogic.mk_Trueprop oo mk_leq) Bs Bs_copy;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   387
        val concl = HOLogic.mk_Trueprop (mk_mor Bs ss Bs_copy ss active_ids);
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   388
      in
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51070
diff changeset
   389
        Goal.prove_sorry lthy [] []
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   390
          (fold_rev Logic.all (Bs @ ss @ Bs_copy) (Logic.list_implies (prems, concl)))
53285
f09645642984 renamed BNF fact
blanchet
parents: 53270
diff changeset
   391
          (K (mk_mor_incl_tac mor_def map_ids))
49109
0e5b859e1c91 no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
traytel
parents: 49074
diff changeset
   392
        |> Thm.close_derivation
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   393
      end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   394
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   395
    val mor_comp_thm =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   396
      let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   397
        val prems =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   398
          [HOLogic.mk_Trueprop (mk_mor Bs ss B's s's fs),
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   399
           HOLogic.mk_Trueprop (mk_mor B's s's B''s s''s gs)];
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   400
        val concl =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   401
          HOLogic.mk_Trueprop (mk_mor Bs ss B''s s''s (map2 (curry HOLogic.mk_comp) gs fs));
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   402
      in
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51070
diff changeset
   403
        Goal.prove_sorry lthy [] []
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   404
          (fold_rev Logic.all (Bs @ ss @ B's @ s's @ B''s @ s''s @ fs @ gs)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   405
             (Logic.list_implies (prems, concl)))
53290
b6c3be868217 renamed BNF fact
blanchet
parents: 53289
diff changeset
   406
          (K (mk_mor_comp_tac mor_def set_mapss map_comp_id_thms))
49109
0e5b859e1c91 no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
traytel
parents: 49074
diff changeset
   407
        |> Thm.close_derivation
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   408
      end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   409
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   410
    val mor_inv_thm =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   411
      let
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51869
diff changeset
   412
        fun mk_inv_prem f inv_f B B' = HOLogic.mk_conj (mk_leq (mk_image inv_f $ B') B,
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   413
          HOLogic.mk_conj (mk_inver inv_f f B, mk_inver f inv_f B'));
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   414
        val prems = map HOLogic.mk_Trueprop
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   415
          ([mk_mor Bs ss B's s's fs, mk_alg Bs ss, mk_alg B's s's] @
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   416
          map4 mk_inv_prem fs inv_fs Bs B's);
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   417
        val concl = HOLogic.mk_Trueprop (mk_mor B's s's Bs ss inv_fs);
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   418
      in
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51070
diff changeset
   419
        Goal.prove_sorry lthy [] []
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   420
          (fold_rev Logic.all (Bs @ ss @ B's @ s's @ fs @ inv_fs)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   421
            (Logic.list_implies (prems, concl)))
53290
b6c3be868217 renamed BNF fact
blanchet
parents: 53289
diff changeset
   422
          (K (mk_mor_inv_tac alg_def mor_def set_mapss morE_thms map_comp_id_thms map_cong0L_thms))
49109
0e5b859e1c91 no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
traytel
parents: 49074
diff changeset
   423
        |> Thm.close_derivation
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   424
      end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   425
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   426
    val mor_cong_thm =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   427
      let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   428
        val prems = map HOLogic.mk_Trueprop
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   429
         (map2 (curry HOLogic.mk_eq) fs_copy fs @ [mk_mor Bs ss B's s's fs])
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   430
        val concl = HOLogic.mk_Trueprop (mk_mor Bs ss B's s's fs_copy);
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   431
      in
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51070
diff changeset
   432
        Goal.prove_sorry lthy [] []
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   433
          (fold_rev Logic.all (Bs @ ss @ B's @ s's @ fs @ fs_copy)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   434
             (Logic.list_implies (prems, concl)))
51798
ad3a241def73 uniform Proof.context for hyp_subst_tac;
wenzelm
parents: 51782
diff changeset
   435
          (K ((hyp_subst_tac lthy THEN' atac) 1))
49109
0e5b859e1c91 no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
traytel
parents: 49074
diff changeset
   436
        |> Thm.close_derivation
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   437
      end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   438
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   439
    val mor_str_thm =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   440
      let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   441
        val maps = map2 (fn Ds => fn bnf => Term.list_comb
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   442
          (mk_map_of_bnf Ds (passiveAs @ FTsAs) allAs bnf, passive_ids @ ss)) Dss bnfs;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   443
      in
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51070
diff changeset
   444
        Goal.prove_sorry lthy [] []
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   445
          (fold_rev Logic.all ss (HOLogic.mk_Trueprop
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   446
            (mk_mor (map HOLogic.mk_UNIV FTsAs) maps active_UNIVs ss ss)))
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   447
          (K (mk_mor_str_tac ks mor_def))
49109
0e5b859e1c91 no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
traytel
parents: 49074
diff changeset
   448
        |> Thm.close_derivation
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   449
      end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   450
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   451
    val mor_convol_thm =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   452
      let
49458
blanchet
parents: 49457
diff changeset
   453
        val maps = map3 (fn s => fn prod_s => fn mapx =>
blanchet
parents: 49457
diff changeset
   454
          mk_convol (HOLogic.mk_comp (s, Term.list_comb (mapx, passive_ids @ fsts)), prod_s))
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   455
          s's prod_ss map_fsts;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   456
      in
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51070
diff changeset
   457
        Goal.prove_sorry lthy [] []
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   458
          (fold_rev Logic.all (s's @ prod_ss) (HOLogic.mk_Trueprop
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   459
            (mk_mor prod_UNIVs maps (map HOLogic.mk_UNIV activeBs) s's fsts)))
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   460
          (K (mk_mor_convol_tac ks mor_def))
49109
0e5b859e1c91 no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
traytel
parents: 49074
diff changeset
   461
        |> Thm.close_derivation
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   462
      end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   463
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   464
    val mor_UNIV_thm =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   465
      let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   466
        fun mk_conjunct mapAsBs f s s' = HOLogic.mk_eq
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   467
            (HOLogic.mk_comp (f, s),
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   468
            HOLogic.mk_comp (s', Term.list_comb (mapAsBs, passive_ids @ fs)));
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   469
        val lhs = mk_mor active_UNIVs ss (map HOLogic.mk_UNIV activeBs) s's fs;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   470
        val rhs = Library.foldr1 HOLogic.mk_conj (map4 mk_conjunct mapsAsBs fs ss s's);
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   471
      in
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51070
diff changeset
   472
        Goal.prove_sorry lthy [] [] (fold_rev Logic.all (ss @ s's @ fs) (mk_Trueprop_eq (lhs, rhs)))
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   473
          (K (mk_mor_UNIV_tac m morE_thms mor_def))
49109
0e5b859e1c91 no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
traytel
parents: 49074
diff changeset
   474
        |> Thm.close_derivation
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   475
      end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   476
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   477
    val timer = time (timer "Morphism definition & thms");
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   478
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   479
    (* isomorphism *)
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
    (*mor Bs1 ss1 Bs2 ss2 fs \<and> (\<exists>gs. mor Bs2 ss2 Bs1 ss1 fs \<and>
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   482
       forall i = 1 ... n. (inver gs[i] fs[i] Bs1[i] \<and> inver fs[i] gs[i] Bs2[i]))*)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   483
    fun mk_iso Bs1 ss1 Bs2 ss2 fs gs =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   484
      let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   485
        val ex_inv_mor = list_exists_free gs
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   486
          (HOLogic.mk_conj (mk_mor Bs2 ss2 Bs1 ss1 gs,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   487
            Library.foldr1 HOLogic.mk_conj (map2 (curry HOLogic.mk_conj)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   488
              (map3 mk_inver gs fs Bs1) (map3 mk_inver fs gs Bs2))));
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   489
      in
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   490
        HOLogic.mk_conj (mk_mor Bs1 ss1 Bs2 ss2 fs, ex_inv_mor)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   491
      end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   492
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   493
    val iso_alt_thm =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   494
      let
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   495
        val prems = map HOLogic.mk_Trueprop [mk_alg Bs ss, mk_alg B's s's]
49123
263b0e330d8b more work on sugar + simplify Trueprop + eq idiom everywhere
blanchet
parents: 49121
diff changeset
   496
        val concl = mk_Trueprop_eq (mk_iso Bs ss B's s's fs inv_fs,
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   497
          HOLogic.mk_conj (mk_mor Bs ss B's s's fs,
49123
263b0e330d8b more work on sugar + simplify Trueprop + eq idiom everywhere
blanchet
parents: 49121
diff changeset
   498
            Library.foldr1 HOLogic.mk_conj (map3 mk_bij_betw fs Bs B's)));
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   499
      in
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51070
diff changeset
   500
        Goal.prove_sorry lthy [] []
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   501
          (fold_rev Logic.all (Bs @ ss @ B's @ s's @ fs) (Logic.list_implies (prems, concl)))
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   502
          (K (mk_iso_alt_tac mor_image_thms mor_inv_thm))
49109
0e5b859e1c91 no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
traytel
parents: 49074
diff changeset
   503
        |> Thm.close_derivation
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   504
      end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   505
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   506
    val timer = time (timer "Isomorphism definition & thms");
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   507
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   508
    (* algebra copies *)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   509
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   510
    val (copy_alg_thm, ex_copy_alg_thm) =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   511
      let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   512
        val prems = map HOLogic.mk_Trueprop
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   513
         (mk_alg Bs ss :: map3 mk_bij_betw inv_fs B's Bs);
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   514
        val inver_prems = map HOLogic.mk_Trueprop
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   515
          (map3 mk_inver inv_fs fs Bs @ map3 mk_inver fs inv_fs B's);
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   516
        val all_prems = prems @ inver_prems;
55756
565a20b22f09 made tactics more robust
traytel
parents: 55702
diff changeset
   517
        fun mk_s f s mapT = Library.foldl1 HOLogic.mk_comp [f, s,
565a20b22f09 made tactics more robust
traytel
parents: 55702
diff changeset
   518
          Term.list_comb (mapT, passive_ids @ inv_fs)];
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   519
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   520
        val alg = HOLogic.mk_Trueprop
55756
565a20b22f09 made tactics more robust
traytel
parents: 55702
diff changeset
   521
          (mk_alg B's (map3 mk_s fs ss mapsBsAs));
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51070
diff changeset
   522
        val copy_str_thm = Goal.prove_sorry lthy [] []
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   523
          (fold_rev Logic.all (Bs @ ss @ B's @ inv_fs @ fs)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   524
            (Logic.list_implies (all_prems, alg)))
53290
b6c3be868217 renamed BNF fact
blanchet
parents: 53289
diff changeset
   525
          (K (mk_copy_str_tac set_mapss alg_def alg_set_thms))
49109
0e5b859e1c91 no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
traytel
parents: 49074
diff changeset
   526
          |> Thm.close_derivation;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   527
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   528
        val iso = HOLogic.mk_Trueprop
55756
565a20b22f09 made tactics more robust
traytel
parents: 55702
diff changeset
   529
          (mk_iso B's (map3 mk_s fs ss mapsBsAs) Bs ss inv_fs fs_copy);
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51070
diff changeset
   530
        val copy_alg_thm = Goal.prove_sorry lthy [] []
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   531
          (fold_rev Logic.all (Bs @ ss @ B's @ inv_fs @ fs)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   532
            (Logic.list_implies (all_prems, iso)))
55756
565a20b22f09 made tactics more robust
traytel
parents: 55702
diff changeset
   533
          (fn {context = ctxt, prems = _} =>
565a20b22f09 made tactics more robust
traytel
parents: 55702
diff changeset
   534
            mk_copy_alg_tac ctxt set_mapss alg_set_thms mor_def iso_alt_thm copy_str_thm)
49109
0e5b859e1c91 no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
traytel
parents: 49074
diff changeset
   535
          |> Thm.close_derivation;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   536
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   537
        val ex = HOLogic.mk_Trueprop
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   538
          (list_exists_free s's
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   539
            (HOLogic.mk_conj (mk_alg B's s's,
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   540
              mk_iso B's s's Bs ss inv_fs fs_copy)));
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51070
diff changeset
   541
        val ex_copy_alg_thm = Goal.prove_sorry lthy [] []
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   542
          (fold_rev Logic.all (Bs @ ss @ B's @ inv_fs @ fs)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   543
             (Logic.list_implies (prems, ex)))
49109
0e5b859e1c91 no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
traytel
parents: 49074
diff changeset
   544
          (K (mk_ex_copy_alg_tac n copy_str_thm copy_alg_thm))
0e5b859e1c91 no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
traytel
parents: 49074
diff changeset
   545
          |> Thm.close_derivation;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   546
      in
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   547
        (copy_alg_thm, ex_copy_alg_thm)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   548
      end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   549
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   550
    val timer = time (timer "Copy thms");
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   551
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   552
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   553
    (* bounds *)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   554
55770
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   555
    val sum_bd = Library.foldr1 (uncurry mk_csum) bds;
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   556
    val sum_bdT = fst (dest_relT (fastype_of sum_bd));
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   557
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   558
    val (lthy, sbd, sbd_card_order, sbd_Cinfinite, sbd_Card_order, set_sbdss, in_sbds) =
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   559
      if n = 1
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   560
      then (lthy, sum_bd, hd bd_card_orders, bd_Cinfinite, bd_Card_order, set_bdss, in_bds)
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   561
      else
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   562
        let
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   563
          val sbdT_bind = mk_internal_b sum_bdTN;
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   564
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   565
          val ((sbdT_name, (sbdT_glob_info, sbdT_loc_info)), lthy) =
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   566
            typedef (sbdT_bind, dead_params, NoSyn)
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   567
              (HOLogic.mk_UNIV sum_bdT) NONE (EVERY' [rtac exI, rtac UNIV_I] 1) lthy;
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   568
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   569
          val sbdT = Type (sbdT_name, dead_params');
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   570
          val Abs_sbdT = Const (#Abs_name sbdT_glob_info, sum_bdT --> sbdT);
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   571
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   572
          val sbd_bind = mk_internal_b sum_bdN;
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   573
          val sbd_def_bind = (Thm.def_binding sbd_bind, []);
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   574
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   575
          val sbd_spec = mk_dir_image sum_bd Abs_sbdT;
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   576
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   577
          val ((sbd_free, (_, sbd_def_free)), (lthy, lthy_old)) =
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   578
            lthy
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   579
            |> Local_Theory.define ((sbd_bind, NoSyn), (sbd_def_bind, sbd_spec))
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   580
            ||> `Local_Theory.restore;
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   581
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   582
          val phi = Proof_Context.export_morphism lthy_old lthy;
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   583
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   584
          val sbd_def = Morphism.thm phi sbd_def_free RS meta_eq_to_obj_eq;
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   585
          val sbd = Const (fst (Term.dest_Const (Morphism.term phi sbd_free)), mk_relT (`I sbdT));
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   586
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   587
          val Abs_sbdT_inj = mk_Abs_inj_thm (#Abs_inject sbdT_loc_info);
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   588
          val Abs_sbdT_bij = mk_Abs_bij_thm lthy Abs_sbdT_inj (#Abs_cases sbdT_loc_info);
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   589
55770
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   590
          fun mk_sum_Cinfinite [thm] = thm
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   591
            | mk_sum_Cinfinite (thm :: thms) =
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   592
              @{thm Cinfinite_csum_strong} OF [thm, mk_sum_Cinfinite thms];
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   593
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   594
          val sum_Cinfinite = mk_sum_Cinfinite bd_Cinfinites;
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   595
          val sum_Card_order = sum_Cinfinite RS conjunct2;
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   596
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   597
          fun mk_sum_card_order [thm] = thm
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   598
            | mk_sum_card_order (thm :: thms) =
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   599
              @{thm card_order_csum} OF [thm, mk_sum_card_order thms];
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   600
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   601
          val sum_card_order = mk_sum_card_order bd_card_orders;
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   602
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   603
          val sbd_ordIso = @{thm ssubst_Pair_rhs} OF
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   604
            [@{thm dir_image} OF [Abs_sbdT_inj, sum_Card_order], sbd_def];
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   605
          val sbd_Cinfinite = @{thm Cinfinite_cong} OF [sbd_ordIso, sum_Cinfinite];
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   606
          val sbd_Card_order = sbd_Cinfinite RS conjunct2;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   607
55770
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   608
          val sbd_card_order = @{thm iffD2[OF arg_cong[of _ _ card_order]]} OF
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   609
            [sbd_def, @{thm card_order_dir_image} OF [Abs_sbdT_bij, sum_card_order]];
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   610
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   611
          fun mk_set_sbd i bd_Card_order bds =
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   612
            map (fn thm => @{thm ordLeq_ordIso_trans} OF
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   613
              [bd_Card_order RS mk_ordLeq_csum n i thm, sbd_ordIso]) bds;
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   614
          val set_sbdss = map3 mk_set_sbd ks bd_Card_orders set_bdss;
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   615
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   616
          fun mk_in_bd_sum i Co Cnz bd =
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   617
            Cnz RS ((@{thm ordLeq_ordIso_trans} OF
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   618
              [Co RS mk_ordLeq_csum n i (Co RS @{thm ordLeq_refl}), sbd_ordIso]) RS
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   619
              (bd RS @{thm ordLeq_transitive[OF _ cexp_mono2_Cnotzero[OF _ Card_order_csum]]}));
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   620
          val in_sbds = map4 mk_in_bd_sum ks bd_Card_orders bd_Cnotzeros in_bds;
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   621
       in
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   622
         (lthy, sbd, sbd_card_order, sbd_Cinfinite, sbd_Card_order, set_sbdss, in_sbds)
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   623
       end;
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   624
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   625
    val sbd_Cnotzero = sbd_Cinfinite RS @{thm Cinfinite_Cnotzero};
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   626
    val suc_bd = mk_cardSuc sbd;
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   627
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   628
    val field_suc_bd = mk_Field suc_bd;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   629
    val suc_bdT = fst (dest_relT (fastype_of suc_bd));
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   630
    fun mk_Asuc_bd [] = mk_cexp ctwo suc_bd
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   631
      | mk_Asuc_bd As =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   632
        mk_cexp (mk_csum (Library.foldr1 (uncurry mk_csum) (map mk_card_of As)) ctwo) suc_bd;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   633
55770
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   634
    val suc_bd_Card_order =  sbd_Card_order RS @{thm cardSuc_Card_order};
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   635
    val suc_bd_Cinfinite = sbd_Cinfinite RS @{thm Cinfinite_cardSuc};
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   636
    val suc_bd_Cnotzero = suc_bd_Cinfinite RS @{thm Cinfinite_Cnotzero};
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   637
    val suc_bd_worel = suc_bd_Card_order RS @{thm Card_order_wo_rel}
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   638
    val basis_Asuc = if m = 0 then @{thm ordLeq_refl[OF Card_order_ctwo]}
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   639
        else @{thm ordLeq_csum2[OF Card_order_ctwo]};
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   640
    val Asuc_bd_Cinfinite = suc_bd_Cinfinite RS (basis_Asuc RS @{thm Cinfinite_cexp});
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   641
51782
84e7225f5ab6 removed unnecessary assumptions in some theorems about cardinal exponentiation
traytel
parents: 51767
diff changeset
   642
    val suc_bd_Asuc_bd = @{thm ordLess_ordLeq_trans[OF ordLess_ctwo_cexp cexp_mono1]} OF
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   643
      [suc_bd_Card_order, basis_Asuc, suc_bd_Card_order];
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   644
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   645
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   646
    val Asuc_bd = mk_Asuc_bd passive_UNIVs;
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   647
    val Asuc_bdT = fst (dest_relT (fastype_of Asuc_bd));
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   648
    val II_BTs = replicate n (HOLogic.mk_setT Asuc_bdT);
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   649
    val II_sTs = map2 (fn Ds => fn bnf =>
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   650
      mk_T_of_bnf Ds (passiveAs @ replicate n Asuc_bdT) bnf --> Asuc_bdT) Dss bnfs;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   651
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   652
    val (((((((idxs, Asi_name), (idx, idx')), (jdx, jdx')), II_Bs), II_ss), Asuc_fs),
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   653
      names_lthy) = names_lthy
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   654
      |> mk_Frees "i" (replicate n suc_bdT)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   655
      ||>> (fn ctxt => apfst the_single (mk_fresh_names ctxt 1 "Asi"))
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   656
      ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "i") suc_bdT
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   657
      ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "j") suc_bdT
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   658
      ||>> mk_Frees "IIB" II_BTs
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   659
      ||>> mk_Frees "IIs" II_sTs
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   660
      ||>> mk_Frees "f" (map (fn T => Asuc_bdT --> T) activeAs);
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   661
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   662
    val suc_bd_limit_thm =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   663
      let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   664
        val prem = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   665
          (map (fn idx => HOLogic.mk_mem (idx, field_suc_bd)) idxs));
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   666
        fun mk_conjunct idx = HOLogic.mk_conj (mk_not_eq idx jdx,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   667
          HOLogic.mk_mem (HOLogic.mk_prod (idx, jdx), suc_bd));
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   668
        val concl = HOLogic.mk_Trueprop (mk_Bex field_suc_bd
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   669
          (Term.absfree jdx' (Library.foldr1 HOLogic.mk_conj (map mk_conjunct idxs))));
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   670
      in
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51070
diff changeset
   671
        Goal.prove_sorry lthy [] []
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   672
          (fold_rev Logic.all idxs (Logic.list_implies ([prem], concl)))
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   673
          (K (mk_bd_limit_tac n suc_bd_Cinfinite))
49109
0e5b859e1c91 no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
traytel
parents: 49074
diff changeset
   674
        |> Thm.close_derivation
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   675
      end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   676
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   677
    val timer = time (timer "Bounds");
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   678
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   679
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   680
    (* minimal algebra *)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   681
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   682
    fun mk_minG Asi i k = mk_UNION (mk_underS suc_bd $ i)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   683
      (Term.absfree jdx' (mk_nthN n (Asi $ jdx) k));
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   684
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   685
    fun mk_minH_component Asi i sets Ts s k =
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   686
      HOLogic.mk_binop @{const_name "sup"}
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   687
      (mk_minG Asi i k, mk_image s $ mk_in (passive_UNIVs @ map (mk_minG Asi i) ks) sets Ts);
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   688
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   689
    fun mk_min_algs ss =
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   690
      let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   691
        val BTs = map (range_type o fastype_of) ss;
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   692
        val Ts = passiveAs @ BTs;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   693
        val (Asi, Asi') = `Free (Asi_name, suc_bdT -->
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   694
          Library.foldr1 HOLogic.mk_prodT (map HOLogic.mk_setT BTs));
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   695
      in
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   696
         mk_worec suc_bd (Term.absfree Asi' (Term.absfree idx' (HOLogic.mk_tuple
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   697
           (map4 (mk_minH_component Asi idx) (mk_setss Ts) (mk_FTs Ts) ss ks))))
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   698
      end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   699
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   700
    val (min_algs_thms, min_algs_mono_thms, card_of_min_algs_thm, least_min_algs_thm) =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   701
      let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   702
        val i_field = HOLogic.mk_mem (idx, field_suc_bd);
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   703
        val min_algs = mk_min_algs ss;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   704
        val min_algss = map (fn k => mk_nthN n (min_algs $ idx) k) ks;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   705
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   706
        val concl = HOLogic.mk_Trueprop
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   707
          (HOLogic.mk_eq (min_algs $ idx, HOLogic.mk_tuple
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   708
            (map4 (mk_minH_component min_algs idx) setssAs FTsAs ss ks)));
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   709
        val goal = fold_rev Logic.all (idx :: ss)
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   710
          (Logic.mk_implies (HOLogic.mk_Trueprop i_field, concl));
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   711
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51070
diff changeset
   712
        val min_algs_thm = Goal.prove_sorry lthy [] [] goal
49109
0e5b859e1c91 no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
traytel
parents: 49074
diff changeset
   713
          (K (mk_min_algs_tac suc_bd_worel in_cong'_thms))
0e5b859e1c91 no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
traytel
parents: 49074
diff changeset
   714
          |> Thm.close_derivation;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   715
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   716
        val min_algs_thms = map (fn k => min_algs_thm RS mk_nthI n k) ks;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   717
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   718
        fun mk_mono_goal min_alg =
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   719
          fold_rev Logic.all ss (HOLogic.mk_Trueprop (mk_relChain suc_bd
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   720
            (Term.absfree idx' min_alg)));
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   721
49109
0e5b859e1c91 no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
traytel
parents: 49074
diff changeset
   722
        val monos =
0e5b859e1c91 no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
traytel
parents: 49074
diff changeset
   723
          map2 (fn goal => fn min_algs =>
51798
ad3a241def73 uniform Proof.context for hyp_subst_tac;
wenzelm
parents: 51782
diff changeset
   724
            Goal.prove_sorry lthy [] [] goal (K (mk_min_algs_mono_tac lthy min_algs))
49109
0e5b859e1c91 no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
traytel
parents: 49074
diff changeset
   725
            |> Thm.close_derivation)
0e5b859e1c91 no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
traytel
parents: 49074
diff changeset
   726
          (map mk_mono_goal min_algss) min_algs_thms;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   727
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   728
        fun mk_card_conjunct min_alg = mk_ordLeq (mk_card_of min_alg) Asuc_bd;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   729
        val card_conjunction = Library.foldr1 HOLogic.mk_conj (map mk_card_conjunct min_algss);
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   730
        val card_cT = certifyT lthy suc_bdT;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   731
        val card_ct = certify lthy (Term.absfree idx' card_conjunction);
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   732
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   733
        val card_of = singleton (Proof_Context.export names_lthy lthy)
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51070
diff changeset
   734
          (Goal.prove_sorry lthy [] []
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   735
            (HOLogic.mk_Trueprop (HOLogic.mk_imp (i_field, card_conjunction)))
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   736
            (K (mk_min_algs_card_of_tac card_cT card_ct
55770
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   737
              m suc_bd_worel min_algs_thms in_sbds
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   738
              sbd_Card_order sbd_Cnotzero suc_bd_Card_order suc_bd_Cinfinite suc_bd_Cnotzero
51812
329c62d99979 removed unreferenced thm
blanchet
parents: 51805
diff changeset
   739
              suc_bd_Asuc_bd Asuc_bd_Cinfinite)))
49109
0e5b859e1c91 no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
traytel
parents: 49074
diff changeset
   740
          |> Thm.close_derivation;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   741
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   742
        val least_prem = HOLogic.mk_Trueprop (mk_alg Bs ss);
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51869
diff changeset
   743
        val least_conjunction = Library.foldr1 HOLogic.mk_conj (map2 mk_leq min_algss Bs);
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   744
        val least_cT = certifyT lthy suc_bdT;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   745
        val least_ct = certify lthy (Term.absfree idx' least_conjunction);
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   746
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   747
        val least = singleton (Proof_Context.export names_lthy lthy)
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51070
diff changeset
   748
          (Goal.prove_sorry lthy [] []
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   749
            (Logic.mk_implies (least_prem,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   750
              HOLogic.mk_Trueprop (HOLogic.mk_imp (i_field, least_conjunction))))
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   751
            (K (mk_min_algs_least_tac least_cT least_ct
49109
0e5b859e1c91 no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
traytel
parents: 49074
diff changeset
   752
              suc_bd_worel min_algs_thms alg_set_thms)))
0e5b859e1c91 no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
traytel
parents: 49074
diff changeset
   753
          |> Thm.close_derivation;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   754
      in
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   755
        (min_algs_thms, monos, card_of, least)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   756
      end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   757
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   758
    val timer = time (timer "min_algs definition & thms");
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   759
53566
5ff3a2d112d7 conceal internal bindings
traytel
parents: 53310
diff changeset
   760
    val min_alg_binds = mk_internal_bs min_algN;
5ff3a2d112d7 conceal internal bindings
traytel
parents: 53310
diff changeset
   761
    fun min_alg_bind i = nth min_alg_binds (i - 1);
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   762
    val min_alg_def_bind = rpair [] o Thm.def_binding o min_alg_bind;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   763
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   764
    fun min_alg_spec i =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   765
      let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   766
        val rhs = mk_UNION (field_suc_bd)
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   767
          (Term.absfree idx' (mk_nthN n (mk_min_algs ss $ idx) i));
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   768
      in
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   769
        fold_rev (Term.absfree o Term.dest_Free) ss rhs
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   770
      end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   771
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   772
    val ((min_alg_frees, (_, min_alg_def_frees)), (lthy, lthy_old)) =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   773
        lthy
55204
345ee77213b5 use Local_Theory.define instead of Specification.definition for internal constants
traytel
parents: 55197
diff changeset
   774
        |> fold_map (fn i => Local_Theory.define
345ee77213b5 use Local_Theory.define instead of Specification.definition for internal constants
traytel
parents: 55197
diff changeset
   775
          ((min_alg_bind i, NoSyn), (min_alg_def_bind i, min_alg_spec i))) ks
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   776
        |>> apsnd split_list o split_list
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   777
        ||> `Local_Theory.restore;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   778
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   779
    val phi = Proof_Context.export_morphism lthy_old lthy;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   780
    val min_algs = map (fst o Term.dest_Const o Morphism.term phi) min_alg_frees;
55204
345ee77213b5 use Local_Theory.define instead of Specification.definition for internal constants
traytel
parents: 55197
diff changeset
   781
    val min_alg_defs = map (fn def =>
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   782
      mk_unabs_def n (Morphism.thm phi def RS meta_eq_to_obj_eq)) min_alg_def_frees;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   783
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   784
    fun mk_min_alg ss i =
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   785
      let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   786
        val T = HOLogic.mk_setT (range_type (fastype_of (nth ss (i - 1))))
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   787
        val Ts = map fastype_of ss;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   788
        val min_algT = Library.foldr (op -->) (Ts, T);
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   789
      in
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   790
        Term.list_comb (Const (nth min_algs (i - 1), min_algT), ss)
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   791
      end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   792
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   793
    val (alg_min_alg_thm, card_of_min_alg_thms, least_min_alg_thms, mor_incl_min_alg_thm) =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   794
      let
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   795
        val min_algs = map (mk_min_alg ss) ks;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   796
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   797
        val goal = fold_rev Logic.all ss (HOLogic.mk_Trueprop (mk_alg min_algs ss));
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51070
diff changeset
   798
        val alg_min_alg = Goal.prove_sorry lthy [] [] goal
55770
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   799
          (K (mk_alg_min_alg_tac m alg_def min_alg_defs suc_bd_limit_thm sbd_Cinfinite
f2cf7f92c9ac intermediate typedef for the type of the bound (local to lfp)
traytel
parents: 55756
diff changeset
   800
            set_sbdss min_algs_thms min_algs_mono_thms))
49109
0e5b859e1c91 no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
traytel
parents: 49074
diff changeset
   801
          |> Thm.close_derivation;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   802
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51070
diff changeset
   803
        fun mk_card_of_thm min_alg def = Goal.prove_sorry lthy [] []
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   804
          (fold_rev Logic.all ss
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   805
            (HOLogic.mk_Trueprop (mk_ordLeq (mk_card_of min_alg) Asuc_bd)))
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   806
          (K (mk_card_of_min_alg_tac def card_of_min_algs_thm
49109
0e5b859e1c91 no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
traytel
parents: 49074
diff changeset
   807
            suc_bd_Card_order suc_bd_Asuc_bd Asuc_bd_Cinfinite))
0e5b859e1c91 no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
traytel
parents: 49074
diff changeset
   808
          |> Thm.close_derivation;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   809
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   810
        val least_prem = HOLogic.mk_Trueprop (mk_alg Bs ss);
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51070
diff changeset
   811
        fun mk_least_thm min_alg B def = Goal.prove_sorry lthy [] []
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   812
          (fold_rev Logic.all (Bs @ ss)
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51869
diff changeset
   813
            (Logic.mk_implies (least_prem, HOLogic.mk_Trueprop (mk_leq min_alg B))))
49109
0e5b859e1c91 no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
traytel
parents: 49074
diff changeset
   814
          (K (mk_least_min_alg_tac def least_min_algs_thm))
0e5b859e1c91 no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
traytel
parents: 49074
diff changeset
   815
          |> Thm.close_derivation;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   816
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   817
        val leasts = map3 mk_least_thm min_algs Bs min_alg_defs;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   818
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   819
        val incl_prem = HOLogic.mk_Trueprop (mk_alg Bs ss);
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   820
        val incl_min_algs = map (mk_min_alg ss) ks;
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51070
diff changeset
   821
        val incl = Goal.prove_sorry lthy [] []
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   822
          (fold_rev Logic.all (Bs @ ss)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   823
            (Logic.mk_implies (incl_prem,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   824
              HOLogic.mk_Trueprop (mk_mor incl_min_algs ss Bs ss active_ids))))
49109
0e5b859e1c91 no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
traytel
parents: 49074
diff changeset
   825
          (K (EVERY' (rtac mor_incl_thm :: map etac leasts) 1))
0e5b859e1c91 no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
traytel
parents: 49074
diff changeset
   826
          |> Thm.close_derivation;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   827
      in
49109
0e5b859e1c91 no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
traytel
parents: 49074
diff changeset
   828
        (alg_min_alg, map2 mk_card_of_thm min_algs min_alg_defs, leasts, incl)
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   829
      end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   830
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   831
    val timer = time (timer "Minimal algebra definition & thms");
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   832
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   833
    val II_repT = HOLogic.mk_prodT (HOLogic.mk_tupleT II_BTs, HOLogic.mk_tupleT II_sTs);
53566
5ff3a2d112d7 conceal internal bindings
traytel
parents: 53310
diff changeset
   834
    val IIT_bind = mk_internal_b IITN;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   835
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   836
    val ((IIT_name, (IIT_glob_info, IIT_loc_info)), lthy) =
49835
31f32ec4d766 discontinued typedef with alternative name;
wenzelm
parents: 49833
diff changeset
   837
      typedef (IIT_bind, params, NoSyn)
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   838
        (HOLogic.mk_UNIV II_repT) NONE (EVERY' [rtac exI, rtac UNIV_I] 1) lthy;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   839
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   840
    val IIT = Type (IIT_name, params');
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   841
    val Abs_IIT = Const (#Abs_name IIT_glob_info, II_repT --> IIT);
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   842
    val Rep_IIT = Const (#Rep_name IIT_glob_info, IIT --> II_repT);
49228
e43910ccee74 open typedefs everywhere in the package
traytel
parents: 49227
diff changeset
   843
    val Abs_IIT_inverse_thm = UNIV_I RS #Abs_inverse IIT_loc_info;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   844
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   845
    val initT = IIT --> Asuc_bdT;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   846
    val active_initTs = replicate n initT;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   847
    val init_FTs = map2 (fn Ds => mk_T_of_bnf Ds (passiveAs @ active_initTs)) Dss bnfs;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   848
    val init_fTs = map (fn T => initT --> T) activeAs;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   849
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   850
    val (((((((iidx, iidx'), init_xs), (init_xFs, init_xFs')),
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   851
      init_fs), init_fs_copy), init_phis), names_lthy) = names_lthy
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   852
      |> yield_singleton (apfst (op ~~) oo mk_Frees' "i") IIT
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   853
      ||>> mk_Frees "ix" active_initTs
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   854
      ||>> mk_Frees' "x" init_FTs
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   855
      ||>> mk_Frees "f" init_fTs
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   856
      ||>> mk_Frees "f" init_fTs
49463
83ac281bcdc2 provide predicator, define relator
blanchet
parents: 49460
diff changeset
   857
      ||>> mk_Frees "P" (replicate n (mk_pred1T initT));
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   858
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   859
    val II = HOLogic.mk_Collect (fst iidx', IIT, list_exists_free (II_Bs @ II_ss)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   860
      (HOLogic.mk_conj (HOLogic.mk_eq (iidx,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   861
        Abs_IIT $ (HOLogic.mk_prod (HOLogic.mk_tuple II_Bs, HOLogic.mk_tuple II_ss))),
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   862
        mk_alg II_Bs II_ss)));
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   863
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   864
    val select_Bs = map (mk_nthN n (HOLogic.mk_fst (Rep_IIT $ iidx))) ks;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   865
    val select_ss = map (mk_nthN n (HOLogic.mk_snd (Rep_IIT $ iidx))) ks;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   866
53566
5ff3a2d112d7 conceal internal bindings
traytel
parents: 53310
diff changeset
   867
    val str_init_binds = mk_internal_bs str_initN;
5ff3a2d112d7 conceal internal bindings
traytel
parents: 53310
diff changeset
   868
    fun str_init_bind i = nth str_init_binds (i - 1);
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   869
    val str_init_def_bind = rpair [] o Thm.def_binding o str_init_bind;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   870
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   871
    fun str_init_spec i =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   872
      let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   873
        val init_xF = nth init_xFs (i - 1)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   874
        val select_s = nth select_ss (i - 1);
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   875
        val map = mk_map_of_bnf (nth Dss (i - 1))
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   876
          (passiveAs @ active_initTs) (passiveAs @ replicate n Asuc_bdT)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   877
          (nth bnfs (i - 1));
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   878
        val map_args = passive_ids @ replicate n (mk_rapp iidx Asuc_bdT);
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   879
        val rhs = select_s $ (Term.list_comb (map, map_args) $ init_xF);
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   880
      in
55204
345ee77213b5 use Local_Theory.define instead of Specification.definition for internal constants
traytel
parents: 55197
diff changeset
   881
        fold_rev (Term.absfree o Term.dest_Free) [init_xF, iidx] rhs
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   882
      end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   883
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   884
    val ((str_init_frees, (_, str_init_def_frees)), (lthy, lthy_old)) =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   885
      lthy
55204
345ee77213b5 use Local_Theory.define instead of Specification.definition for internal constants
traytel
parents: 55197
diff changeset
   886
      |> fold_map (fn i => Local_Theory.define
345ee77213b5 use Local_Theory.define instead of Specification.definition for internal constants
traytel
parents: 55197
diff changeset
   887
        ((str_init_bind i, NoSyn), (str_init_def_bind i, str_init_spec i))) ks
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   888
      |>> apsnd split_list o split_list
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   889
      ||> `Local_Theory.restore;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   890
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   891
    val phi = Proof_Context.export_morphism lthy_old lthy;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   892
    val str_inits =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   893
      map (Term.subst_atomic_types (map (`(Morphism.typ phi)) params') o Morphism.term phi)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   894
        str_init_frees;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   895
55204
345ee77213b5 use Local_Theory.define instead of Specification.definition for internal constants
traytel
parents: 55197
diff changeset
   896
    val str_init_defs = map (fn def =>
345ee77213b5 use Local_Theory.define instead of Specification.definition for internal constants
traytel
parents: 55197
diff changeset
   897
      mk_unabs_def 2 (Morphism.thm phi def RS meta_eq_to_obj_eq)) str_init_def_frees;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   898
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   899
    val car_inits = map (mk_min_alg str_inits) ks;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   900
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   901
    (*TODO: replace with instantiate? (problem: figure out right type instantiation)*)
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51070
diff changeset
   902
    val alg_init_thm = Goal.prove_sorry lthy [] []
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   903
      (HOLogic.mk_Trueprop (mk_alg car_inits str_inits))
49109
0e5b859e1c91 no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
traytel
parents: 49074
diff changeset
   904
      (K (rtac alg_min_alg_thm 1))
0e5b859e1c91 no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
traytel
parents: 49074
diff changeset
   905
      |> Thm.close_derivation;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   906
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51070
diff changeset
   907
    val alg_select_thm = Goal.prove_sorry lthy [] []
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   908
      (HOLogic.mk_Trueprop (mk_Ball II
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   909
        (Term.absfree iidx' (mk_alg select_Bs select_ss))))
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
   910
      (fn {context = ctxt, prems = _} => mk_alg_select_tac ctxt Abs_IIT_inverse_thm)
49109
0e5b859e1c91 no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
traytel
parents: 49074
diff changeset
   911
      |> Thm.close_derivation;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   912
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   913
    val mor_select_thm =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   914
      let
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   915
        val alg_prem = HOLogic.mk_Trueprop (mk_alg Bs ss);
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   916
        val i_prem = HOLogic.mk_Trueprop (HOLogic.mk_mem (iidx, II));
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   917
        val mor_prem = HOLogic.mk_Trueprop (mk_mor select_Bs select_ss Bs ss Asuc_fs);
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   918
        val prems = [alg_prem, i_prem, mor_prem];
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   919
        val concl = HOLogic.mk_Trueprop
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   920
          (mk_mor car_inits str_inits Bs ss
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   921
            (map (fn f => HOLogic.mk_comp (f, mk_rapp iidx Asuc_bdT)) Asuc_fs));
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   922
      in
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51070
diff changeset
   923
        Goal.prove_sorry lthy [] []
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   924
          (fold_rev Logic.all (iidx :: Bs @ ss @ Asuc_fs) (Logic.list_implies (prems, concl)))
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   925
          (K (mk_mor_select_tac mor_def mor_cong_thm mor_comp_thm mor_incl_min_alg_thm alg_def
53290
b6c3be868217 renamed BNF fact
blanchet
parents: 53289
diff changeset
   926
            alg_select_thm alg_set_thms set_mapss str_init_defs))
49109
0e5b859e1c91 no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
traytel
parents: 49074
diff changeset
   927
        |> Thm.close_derivation
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   928
      end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   929
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   930
    val (init_ex_mor_thm, init_unique_mor_thms) =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   931
      let
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   932
        val prem = HOLogic.mk_Trueprop (mk_alg Bs ss);
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   933
        val concl = HOLogic.mk_Trueprop
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   934
          (list_exists_free init_fs (mk_mor car_inits str_inits Bs ss init_fs));
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51070
diff changeset
   935
        val ex_mor = Goal.prove_sorry lthy [] []
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   936
          (fold_rev Logic.all (Bs @ ss) (Logic.mk_implies (prem, concl)))
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
   937
          (fn {context = ctxt, prems = _} => mk_init_ex_mor_tac ctxt Abs_IIT_inverse_thm
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
   938
            ex_copy_alg_thm alg_min_alg_thm card_of_min_alg_thms mor_comp_thm mor_select_thm
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
   939
            mor_incl_min_alg_thm)
49109
0e5b859e1c91 no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
traytel
parents: 49074
diff changeset
   940
          |> Thm.close_derivation;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   941
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   942
        val prems = map2 (HOLogic.mk_Trueprop oo curry HOLogic.mk_mem) init_xs car_inits
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   943
        val mor_prems = map HOLogic.mk_Trueprop
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   944
          [mk_mor car_inits str_inits Bs ss init_fs,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   945
          mk_mor car_inits str_inits Bs ss init_fs_copy];
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   946
        fun mk_fun_eq f g x = HOLogic.mk_eq (f $ x, g $ x);
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   947
        val unique = HOLogic.mk_Trueprop
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   948
          (Library.foldr1 HOLogic.mk_conj (map3 mk_fun_eq init_fs init_fs_copy init_xs));
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51070
diff changeset
   949
        val unique_mor = Goal.prove_sorry lthy [] []
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   950
          (fold_rev Logic.all (init_xs @ Bs @ ss @ init_fs @ init_fs_copy)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   951
            (Logic.list_implies (prems @ mor_prems, unique)))
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   952
          (K (mk_init_unique_mor_tac m alg_def alg_init_thm least_min_alg_thms
51761
4c9f08836d87 renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents: 51758
diff changeset
   953
            in_mono'_thms alg_set_thms morE_thms map_cong0s))
49109
0e5b859e1c91 no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
traytel
parents: 49074
diff changeset
   954
          |> Thm.close_derivation;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   955
      in
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   956
        (ex_mor, split_conj_thm unique_mor)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   957
      end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   958
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   959
    val init_setss = mk_setss (passiveAs @ active_initTs);
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   960
    val active_init_setss = map (drop m) init_setss;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   961
    val init_ins = map2 (fn sets => mk_in (passive_UNIVs @ car_inits) sets) init_setss init_FTs;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   962
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   963
    fun mk_closed phis =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   964
      let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   965
        fun mk_conjunct phi str_init init_sets init_in x x' =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   966
          let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   967
            val prem = Library.foldr1 HOLogic.mk_conj
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   968
              (map2 (fn set => mk_Ball (set $ x)) init_sets phis);
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   969
            val concl = phi $ (str_init $ x);
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   970
          in
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   971
            mk_Ball init_in (Term.absfree x' (HOLogic.mk_imp (prem, concl)))
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   972
          end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   973
      in
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   974
        Library.foldr1 HOLogic.mk_conj
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   975
          (map6 mk_conjunct phis str_inits active_init_setss init_ins init_xFs init_xFs')
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   976
      end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   977
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   978
    val init_induct_thm =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   979
      let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   980
        val prem = HOLogic.mk_Trueprop (mk_closed init_phis);
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   981
        val concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   982
          (map2 mk_Ball car_inits init_phis));
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   983
      in
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51070
diff changeset
   984
        Goal.prove_sorry lthy [] []
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   985
          (fold_rev Logic.all init_phis (Logic.mk_implies (prem, concl)))
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   986
          (K (mk_init_induct_tac m alg_def alg_init_thm least_min_alg_thms alg_set_thms))
49109
0e5b859e1c91 no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
traytel
parents: 49074
diff changeset
   987
        |> Thm.close_derivation
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   988
      end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   989
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   990
    val timer = time (timer "Initiality definition & thms");
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   991
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   992
    val ((T_names, (T_glob_infos, T_loc_infos)), lthy) =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   993
      lthy
53566
5ff3a2d112d7 conceal internal bindings
traytel
parents: 53310
diff changeset
   994
      |> fold_map3 (fn b => fn mx => fn car_init =>
5ff3a2d112d7 conceal internal bindings
traytel
parents: 53310
diff changeset
   995
        typedef (Binding.conceal b, params, mx) car_init NONE
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   996
          (EVERY' [rtac ssubst, rtac @{thm ex_in_conv}, resolve_tac alg_not_empty_thms,
49169
937a0fadddfb honor mixfix specifications
blanchet
parents: 49134
diff changeset
   997
            rtac alg_init_thm] 1)) bs mixfixes car_inits
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   998
      |>> apsnd split_list o split_list;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   999
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1000
    val Ts = map (fn name => Type (name, params')) T_names;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1001
    fun mk_Ts passive = map (Term.typ_subst_atomic (passiveAs ~~ passive)) Ts;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1002
    val Ts' = mk_Ts passiveBs;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1003
    val Rep_Ts = map2 (fn info => fn T => Const (#Rep_name info, T --> initT)) T_glob_infos Ts;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1004
    val Abs_Ts = map2 (fn info => fn T => Const (#Abs_name info, initT --> T)) T_glob_infos Ts;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1005
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1006
    val type_defs = map #type_definition T_loc_infos;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1007
    val Reps = map #Rep T_loc_infos;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1008
    val Rep_casess = map #Rep_cases T_loc_infos;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1009
    val Rep_injects = map #Rep_inject T_loc_infos;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1010
    val Rep_inverses = map #Rep_inverse T_loc_infos;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1011
    val Abs_inverses = map #Abs_inverse T_loc_infos;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1012
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1013
    fun mk_inver_thm mk_tac rep abs X thm =
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51070
diff changeset
  1014
      Goal.prove_sorry lthy [] []
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1015
        (HOLogic.mk_Trueprop (mk_inver rep abs X))
49109
0e5b859e1c91 no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
traytel
parents: 49074
diff changeset
  1016
        (K (EVERY' [rtac ssubst, rtac @{thm inver_def}, rtac ballI, mk_tac thm] 1))
0e5b859e1c91 no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
traytel
parents: 49074
diff changeset
  1017
      |> Thm.close_derivation;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1018
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1019
    val inver_Reps = map4 (mk_inver_thm rtac) Abs_Ts Rep_Ts (map HOLogic.mk_UNIV Ts) Rep_inverses;
49227
2652319c394e open typedef for datatypes
traytel
parents: 49222
diff changeset
  1020
    val inver_Abss = map4 (mk_inver_thm etac) Rep_Ts Abs_Ts car_inits Abs_inverses;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1021
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1022
    val timer = time (timer "THE TYPEDEFs & Rep/Abs thms");
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1023
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1024
    val UNIVs = map HOLogic.mk_UNIV Ts;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1025
    val FTs = mk_FTs (passiveAs @ Ts);
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1026
    val FTs' = mk_FTs (passiveBs @ Ts');
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1027
    fun mk_set_Ts T = passiveAs @ replicate n (HOLogic.mk_setT T);
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1028
    val setFTss = map (mk_FTs o mk_set_Ts) passiveAs;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1029
    val FTs_setss = mk_setss (passiveAs @ Ts);
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1030
    val FTs'_setss = mk_setss (passiveBs @ Ts');
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1031
    val map_FT_inits = map2 (fn Ds =>
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1032
      mk_map_of_bnf Ds (passiveAs @ Ts) (passiveAs @ active_initTs)) Dss bnfs;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1033
    val fTs = map2 (curry op -->) Ts activeAs;
49504
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49502
diff changeset
  1034
    val foldT = Library.foldr1 HOLogic.mk_prodT (map2 (curry op -->) Ts activeAs);
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1035
    val rec_sTs = map (Term.typ_subst_atomic (activeBs ~~ Ts)) prod_sTs;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1036
    val rec_maps = map (Term.subst_atomic_types (activeBs ~~ Ts)) map_fsts;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1037
    val rec_maps_rev = map (Term.subst_atomic_types (activeBs ~~ Ts)) map_fsts_rev;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1038
    val rec_fsts = map (Term.subst_atomic_types (activeBs ~~ Ts)) fsts;
51739
3514b90d0a8b (co)rec is (just as the (un)fold) the unique morphism;
traytel
parents: 51551
diff changeset
  1039
    val rec_UNIVs = map2 (HOLogic.mk_UNIV oo curry HOLogic.mk_prodT) Ts activeAs;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1040
55756
565a20b22f09 made tactics more robust
traytel
parents: 55702
diff changeset
  1041
    val (((((((((Izs1, Izs1'), (Izs2, Izs2')), xFs), yFs), (AFss, AFss')),
49504
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49502
diff changeset
  1042
      (fold_f, fold_f')), fs), rec_ss), names_lthy) = names_lthy
49331
f4169aa67513 free variable name tuning
blanchet
parents: 49330
diff changeset
  1043
      |> mk_Frees' "z1" Ts
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1044
      ||>> mk_Frees' "z2" Ts'
55756
565a20b22f09 made tactics more robust
traytel
parents: 55702
diff changeset
  1045
      ||>> mk_Frees "x" FTs
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1046
      ||>> mk_Frees "y" FTs'
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1047
      ||>> mk_Freess' "z" setFTss
49504
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49502
diff changeset
  1048
      ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "f") foldT
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1049
      ||>> mk_Frees "f" fTs
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1050
      ||>> mk_Frees "s" rec_sTs;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1051
49331
f4169aa67513 free variable name tuning
blanchet
parents: 49330
diff changeset
  1052
    val Izs = map2 retype_free Ts zs;
49463
83ac281bcdc2 provide predicator, define relator
blanchet
parents: 49460
diff changeset
  1053
    val phis = map2 retype_free (map mk_pred1T Ts) init_phis;
83ac281bcdc2 provide predicator, define relator
blanchet
parents: 49460
diff changeset
  1054
    val phi2s = map2 retype_free (map2 mk_pred2T Ts Ts') init_phis;
49330
276ff43ee0b1 reuse generated names (they look better + slightly more efficient)
blanchet
parents: 49327
diff changeset
  1055
54492
6fae4ecd4ab3 prefix internal names as well
blanchet
parents: 54487
diff changeset
  1056
    fun ctor_bind i = nth external_bs (i - 1) |> Binding.prefix_name (ctorN ^ "_");
53566
5ff3a2d112d7 conceal internal bindings
traytel
parents: 53310
diff changeset
  1057
    val ctor_def_bind = rpair [] o Binding.conceal o Thm.def_binding o ctor_bind;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1058
55756
565a20b22f09 made tactics more robust
traytel
parents: 55702
diff changeset
  1059
    fun ctor_spec abs str map_FT_init =
565a20b22f09 made tactics more robust
traytel
parents: 55702
diff changeset
  1060
      Library.foldl1 HOLogic.mk_comp [abs, str,
565a20b22f09 made tactics more robust
traytel
parents: 55702
diff changeset
  1061
        Term.list_comb (map_FT_init, map HOLogic.id_const passiveAs @ Rep_Ts)];
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1062
49501
acc9635a644a renamed "fld"/"unf" to "ctor"/"dtor"
blanchet
parents: 49498
diff changeset
  1063
    val ((ctor_frees, (_, ctor_def_frees)), (lthy, lthy_old)) =
49311
blanchet
parents: 49308
diff changeset
  1064
      lthy
55756
565a20b22f09 made tactics more robust
traytel
parents: 55702
diff changeset
  1065
      |> fold_map4 (fn i => fn abs => fn str => fn mapx =>
55204
345ee77213b5 use Local_Theory.define instead of Specification.definition for internal constants
traytel
parents: 55197
diff changeset
  1066
        Local_Theory.define
55756
565a20b22f09 made tactics more robust
traytel
parents: 55702
diff changeset
  1067
          ((ctor_bind i, NoSyn), (ctor_def_bind i, ctor_spec abs str mapx)))
565a20b22f09 made tactics more robust
traytel
parents: 55702
diff changeset
  1068
          ks Abs_Ts str_inits map_FT_inits
49311
blanchet
parents: 49308
diff changeset
  1069
      |>> apsnd split_list o split_list
blanchet
parents: 49308
diff changeset
  1070
      ||> `Local_Theory.restore;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1071
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1072
    val phi = Proof_Context.export_morphism lthy_old lthy;
49501
acc9635a644a renamed "fld"/"unf" to "ctor"/"dtor"
blanchet
parents: 49498
diff changeset
  1073
    fun mk_ctors passive =
49185
073d7d1b7488 respect order of/additional type variables supplied by the user in fixed point constructions;
traytel
parents: 49176
diff changeset
  1074
      map (Term.subst_atomic_types (map (Morphism.typ phi) params' ~~ (mk_params passive)) o
49501
acc9635a644a renamed "fld"/"unf" to "ctor"/"dtor"
blanchet
parents: 49498
diff changeset
  1075
        Morphism.term phi) ctor_frees;
acc9635a644a renamed "fld"/"unf" to "ctor"/"dtor"
blanchet
parents: 49498
diff changeset
  1076
    val ctors = mk_ctors passiveAs;
acc9635a644a renamed "fld"/"unf" to "ctor"/"dtor"
blanchet
parents: 49498
diff changeset
  1077
    val ctor's = mk_ctors passiveBs;
55204
345ee77213b5 use Local_Theory.define instead of Specification.definition for internal constants
traytel
parents: 55197
diff changeset
  1078
    val ctor_defs = map (fn def => Morphism.thm phi def RS meta_eq_to_obj_eq) ctor_def_frees;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1079
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1080
    val (mor_Rep_thm, mor_Abs_thm) =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1081
      let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1082
        val copy = alg_init_thm RS copy_alg_thm;
49227
2652319c394e open typedef for datatypes
traytel
parents: 49222
diff changeset
  1083
        fun mk_bij inj Rep cases = @{thm bij_betwI'} OF [inj, Rep, cases];
2652319c394e open typedef for datatypes
traytel
parents: 49222
diff changeset
  1084
        val bijs = map3 mk_bij Rep_injects Reps Rep_casess;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1085
        val mor_Rep =
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51070
diff changeset
  1086
          Goal.prove_sorry lthy [] []
49501
acc9635a644a renamed "fld"/"unf" to "ctor"/"dtor"
blanchet
parents: 49498
diff changeset
  1087
            (HOLogic.mk_Trueprop (mk_mor UNIVs ctors car_inits str_inits Rep_Ts))
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
  1088
            (fn {context = ctxt, prems = _} => mk_mor_Rep_tac ctxt ctor_defs copy bijs inver_Abss
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
  1089
              inver_Reps)
49109
0e5b859e1c91 no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
traytel
parents: 49074
diff changeset
  1090
          |> Thm.close_derivation;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1091
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1092
        val inv = mor_inv_thm OF [mor_Rep, talg_thm, alg_init_thm];
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1093
        val mor_Abs =
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51070
diff changeset
  1094
          Goal.prove_sorry lthy [] []
49501
acc9635a644a renamed "fld"/"unf" to "ctor"/"dtor"
blanchet
parents: 49498
diff changeset
  1095
            (HOLogic.mk_Trueprop (mk_mor car_inits str_inits UNIVs ctors Abs_Ts))
49109
0e5b859e1c91 no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
traytel
parents: 49074
diff changeset
  1096
            (K (mk_mor_Abs_tac inv inver_Abss inver_Reps))
0e5b859e1c91 no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
traytel
parents: 49074
diff changeset
  1097
          |> Thm.close_derivation;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1098
      in
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1099
        (mor_Rep, mor_Abs)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1100
      end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1101
49501
acc9635a644a renamed "fld"/"unf" to "ctor"/"dtor"
blanchet
parents: 49498
diff changeset
  1102
    val timer = time (timer "ctor definitions & thms");
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1103
49504
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49502
diff changeset
  1104
    val fold_fun = Term.absfree fold_f'
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49502
diff changeset
  1105
      (mk_mor UNIVs ctors active_UNIVs ss (map (mk_nthN n fold_f) ks));
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49502
diff changeset
  1106
    val foldx = HOLogic.choice_const foldT $ fold_fun;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1107
54492
6fae4ecd4ab3 prefix internal names as well
blanchet
parents: 54487
diff changeset
  1108
    fun fold_bind i = nth external_bs (i - 1) |> Binding.prefix_name (ctor_foldN ^ "_");
53566
5ff3a2d112d7 conceal internal bindings
traytel
parents: 53310
diff changeset
  1109
    val fold_def_bind = rpair [] o Binding.conceal o Thm.def_binding o fold_bind;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1110
55204
345ee77213b5 use Local_Theory.define instead of Specification.definition for internal constants
traytel
parents: 55197
diff changeset
  1111
    fun fold_spec i = fold_rev (Term.absfree o Term.dest_Free) ss (mk_nthN n foldx i);
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1112
49504
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49502
diff changeset
  1113
    val ((fold_frees, (_, fold_def_frees)), (lthy, lthy_old)) =
49311
blanchet
parents: 49308
diff changeset
  1114
      lthy
55204
345ee77213b5 use Local_Theory.define instead of Specification.definition for internal constants
traytel
parents: 55197
diff changeset
  1115
      |> fold_map (fn i =>
345ee77213b5 use Local_Theory.define instead of Specification.definition for internal constants
traytel
parents: 55197
diff changeset
  1116
        Local_Theory.define ((fold_bind i, NoSyn), (fold_def_bind i, fold_spec i))) ks
49311
blanchet
parents: 49308
diff changeset
  1117
      |>> apsnd split_list o split_list
blanchet
parents: 49308
diff changeset
  1118
      ||> `Local_Theory.restore;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1119
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1120
    val phi = Proof_Context.export_morphism lthy_old lthy;
49504
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49502
diff changeset
  1121
    val folds = map (Morphism.term phi) fold_frees;
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49502
diff changeset
  1122
    val fold_names = map (fst o dest_Const) folds;
52731
dacd47a0633f transfer rule for {c,d}tor_{,un}fold
traytel
parents: 52659
diff changeset
  1123
    fun mk_folds passives actives =
dacd47a0633f transfer rule for {c,d}tor_{,un}fold
traytel
parents: 52659
diff changeset
  1124
      map3 (fn name => fn T => fn active =>
dacd47a0633f transfer rule for {c,d}tor_{,un}fold
traytel
parents: 52659
diff changeset
  1125
        Const (name, Library.foldr (op -->)
52923
traytel
parents: 52913
diff changeset
  1126
          (map2 (curry op -->) (mk_FTs (passives @ actives)) actives, T --> active)))
52731
dacd47a0633f transfer rule for {c,d}tor_{,un}fold
traytel
parents: 52659
diff changeset
  1127
      fold_names (mk_Ts passives) actives;
49504
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49502
diff changeset
  1128
    fun mk_fold Ts ss i = Term.list_comb (Const (nth fold_names (i - 1), Library.foldr (op -->)
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1129
      (map fastype_of ss, nth Ts (i - 1) --> range_type (fastype_of (nth ss (i - 1))))), ss);
55204
345ee77213b5 use Local_Theory.define instead of Specification.definition for internal constants
traytel
parents: 55197
diff changeset
  1130
    val fold_defs = map (fn def =>
345ee77213b5 use Local_Theory.define instead of Specification.definition for internal constants
traytel
parents: 55197
diff changeset
  1131
      mk_unabs_def n (Morphism.thm phi def RS meta_eq_to_obj_eq)) fold_def_frees;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1132
49504
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49502
diff changeset
  1133
    val mor_fold_thm =
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1134
      let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1135
        val ex_mor = talg_thm RS init_ex_mor_thm;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1136
        val mor_cong = mor_cong_thm OF (map (mk_nth_conv n) ks);
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1137
        val mor_comp = mor_Rep_thm RS mor_comp_thm;
49504
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49502
diff changeset
  1138
        val cT = certifyT lthy foldT;
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49502
diff changeset
  1139
        val ct = certify lthy fold_fun
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1140
      in
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1141
        singleton (Proof_Context.export names_lthy lthy)
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51070
diff changeset
  1142
          (Goal.prove_sorry lthy [] []
49504
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49502
diff changeset
  1143
            (HOLogic.mk_Trueprop (mk_mor UNIVs ctors active_UNIVs ss (map (mk_fold Ts ss) ks)))
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49502
diff changeset
  1144
            (K (mk_mor_fold_tac cT ct fold_defs ex_mor (mor_comp RS mor_cong))))
49109
0e5b859e1c91 no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
traytel
parents: 49074
diff changeset
  1145
        |> Thm.close_derivation
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1146
      end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1147
49504
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49502
diff changeset
  1148
    val ctor_fold_thms = map (fn morE => rule_by_tactic lthy
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1149
      ((rtac CollectI THEN' CONJ_WRAP' (K (rtac @{thm subset_UNIV})) (1 upto m + n)) 1)
49504
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49502
diff changeset
  1150
      (mor_fold_thm RS morE)) morE_thms;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1151
49504
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49502
diff changeset
  1152
    val (fold_unique_mor_thms, fold_unique_mor_thm) =
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1153
      let
49501
acc9635a644a renamed "fld"/"unf" to "ctor"/"dtor"
blanchet
parents: 49498
diff changeset
  1154
        val prem = HOLogic.mk_Trueprop (mk_mor UNIVs ctors active_UNIVs ss fs);
49504
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49502
diff changeset
  1155
        fun mk_fun_eq f i = HOLogic.mk_eq (f, mk_fold Ts ss i);
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1156
        val unique = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 mk_fun_eq fs ks));
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51070
diff changeset
  1157
        val unique_mor = Goal.prove_sorry lthy [] []
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1158
          (fold_rev Logic.all (ss @ fs) (Logic.mk_implies (prem, unique)))
49504
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49502
diff changeset
  1159
          (K (mk_fold_unique_mor_tac type_defs init_unique_mor_thms Reps
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49502
diff changeset
  1160
            mor_comp_thm mor_Abs_thm mor_fold_thm))
49109
0e5b859e1c91 no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
traytel
parents: 49074
diff changeset
  1161
          |> Thm.close_derivation;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1162
      in
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1163
        `split_conj_thm unique_mor
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1164
      end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1165
52911
fe4c2418f069 tuned tactic;
traytel
parents: 52904
diff changeset
  1166
    val (ctor_fold_unique_thms, ctor_fold_unique_thm) =
fe4c2418f069 tuned tactic;
traytel
parents: 52904
diff changeset
  1167
      `split_conj_thm (mk_conjIN n RS
52904
traytel
parents: 52839
diff changeset
  1168
        (mor_UNIV_thm RS iffD2 RS fold_unique_mor_thm))
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1169
49504
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49502
diff changeset
  1170
    val fold_ctor_thms =
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1171
      map (fn thm => (mor_incl_thm OF replicate n @{thm subset_UNIV}) RS thm RS sym)
49504
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49502
diff changeset
  1172
        fold_unique_mor_thms;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1173
49504
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49502
diff changeset
  1174
    val ctor_o_fold_thms =
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1175
      let
49504
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49502
diff changeset
  1176
        val mor = mor_comp_thm OF [mor_fold_thm, mor_str_thm];
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1177
      in
49504
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49502
diff changeset
  1178
        map2 (fn unique => fn fold_ctor =>
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49502
diff changeset
  1179
          trans OF [mor RS unique, fold_ctor]) fold_unique_mor_thms fold_ctor_thms
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1180
      end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1181
49504
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49502
diff changeset
  1182
    val timer = time (timer "fold definitions & thms");
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1183
49501
acc9635a644a renamed "fld"/"unf" to "ctor"/"dtor"
blanchet
parents: 49498
diff changeset
  1184
    val map_ctors = map2 (fn Ds => fn bnf =>
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1185
      Term.list_comb (mk_map_of_bnf Ds (passiveAs @ FTs) (passiveAs @ Ts) bnf,
49501
acc9635a644a renamed "fld"/"unf" to "ctor"/"dtor"
blanchet
parents: 49498
diff changeset
  1186
        map HOLogic.id_const passiveAs @ ctors)) Dss bnfs;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1187
54492
6fae4ecd4ab3 prefix internal names as well
blanchet
parents: 54487
diff changeset
  1188
    fun dtor_bind i = nth external_bs (i - 1) |> Binding.prefix_name (dtorN ^ "_");
53566
5ff3a2d112d7 conceal internal bindings
traytel
parents: 53310
diff changeset
  1189
    val dtor_def_bind = rpair [] o Binding.conceal o Thm.def_binding o dtor_bind;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1190
55204
345ee77213b5 use Local_Theory.define instead of Specification.definition for internal constants
traytel
parents: 55197
diff changeset
  1191
    fun dtor_spec i = mk_fold Ts map_ctors i;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1192
49501
acc9635a644a renamed "fld"/"unf" to "ctor"/"dtor"
blanchet
parents: 49498
diff changeset
  1193
    val ((dtor_frees, (_, dtor_def_frees)), (lthy, lthy_old)) =
49311
blanchet
parents: 49308
diff changeset
  1194
      lthy
55204
345ee77213b5 use Local_Theory.define instead of Specification.definition for internal constants
traytel
parents: 55197
diff changeset
  1195
      |> fold_map (fn i =>
345ee77213b5 use Local_Theory.define instead of Specification.definition for internal constants
traytel
parents: 55197
diff changeset
  1196
        Local_Theory.define ((dtor_bind i, NoSyn), (dtor_def_bind i, dtor_spec i))) ks
49311
blanchet
parents: 49308
diff changeset
  1197
      |>> apsnd split_list o split_list
blanchet
parents: 49308
diff changeset
  1198
      ||> `Local_Theory.restore;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1199
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1200
    val phi = Proof_Context.export_morphism lthy_old lthy;
49501
acc9635a644a renamed "fld"/"unf" to "ctor"/"dtor"
blanchet
parents: 49498
diff changeset
  1201
    fun mk_dtors params =
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1202
      map (Term.subst_atomic_types (map (Morphism.typ phi) params' ~~ params) o Morphism.term phi)
49501
acc9635a644a renamed "fld"/"unf" to "ctor"/"dtor"
blanchet
parents: 49498
diff changeset
  1203
        dtor_frees;
acc9635a644a renamed "fld"/"unf" to "ctor"/"dtor"
blanchet
parents: 49498
diff changeset
  1204
    val dtors = mk_dtors params';
55204
345ee77213b5 use Local_Theory.define instead of Specification.definition for internal constants
traytel
parents: 55197
diff changeset
  1205
    val dtor_defs = map (fn def => Morphism.thm phi def RS meta_eq_to_obj_eq) dtor_def_frees;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1206
49504
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49502
diff changeset
  1207
    val ctor_o_dtor_thms = map2 (fold_thms lthy o single) dtor_defs ctor_o_fold_thms;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1208
49501
acc9635a644a renamed "fld"/"unf" to "ctor"/"dtor"
blanchet
parents: 49498
diff changeset
  1209
    val dtor_o_ctor_thms =
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1210
      let
49501
acc9635a644a renamed "fld"/"unf" to "ctor"/"dtor"
blanchet
parents: 49498
diff changeset
  1211
        fun mk_goal dtor ctor FT =
acc9635a644a renamed "fld"/"unf" to "ctor"/"dtor"
blanchet
parents: 49498
diff changeset
  1212
          mk_Trueprop_eq (HOLogic.mk_comp (dtor, ctor), HOLogic.id_const FT);
acc9635a644a renamed "fld"/"unf" to "ctor"/"dtor"
blanchet
parents: 49498
diff changeset
  1213
        val goals = map3 mk_goal dtors ctors FTs;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1214
      in
51761
4c9f08836d87 renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents: 51758
diff changeset
  1215
        map5 (fn goal => fn dtor_def => fn foldx => fn map_comp_id => fn map_cong0L =>
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51070
diff changeset
  1216
          Goal.prove_sorry lthy [] [] goal
51761
4c9f08836d87 renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents: 51758
diff changeset
  1217
            (K (mk_dtor_o_ctor_tac dtor_def foldx map_comp_id map_cong0L ctor_o_fold_thms))
49109
0e5b859e1c91 no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
traytel
parents: 49074
diff changeset
  1218
          |> Thm.close_derivation)
51761
4c9f08836d87 renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents: 51758
diff changeset
  1219
        goals dtor_defs ctor_fold_thms map_comp_id_thms map_cong0L_thms
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1220
      end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1221
49501
acc9635a644a renamed "fld"/"unf" to "ctor"/"dtor"
blanchet
parents: 49498
diff changeset
  1222
    val dtor_ctor_thms = map (fn thm => thm RS @{thm pointfree_idE}) dtor_o_ctor_thms;
acc9635a644a renamed "fld"/"unf" to "ctor"/"dtor"
blanchet
parents: 49498
diff changeset
  1223
    val ctor_dtor_thms = map (fn thm => thm RS @{thm pointfree_idE}) ctor_o_dtor_thms;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1224
49501
acc9635a644a renamed "fld"/"unf" to "ctor"/"dtor"
blanchet
parents: 49498
diff changeset
  1225
    val bij_dtor_thms =
acc9635a644a renamed "fld"/"unf" to "ctor"/"dtor"
blanchet
parents: 49498
diff changeset
  1226
      map2 (fn thm1 => fn thm2 => @{thm o_bij} OF [thm1, thm2]) ctor_o_dtor_thms dtor_o_ctor_thms;
acc9635a644a renamed "fld"/"unf" to "ctor"/"dtor"
blanchet
parents: 49498
diff changeset
  1227
    val inj_dtor_thms = map (fn thm => thm RS @{thm bij_is_inj}) bij_dtor_thms;
acc9635a644a renamed "fld"/"unf" to "ctor"/"dtor"
blanchet
parents: 49498
diff changeset
  1228
    val surj_dtor_thms = map (fn thm => thm RS @{thm bij_is_surj}) bij_dtor_thms;
acc9635a644a renamed "fld"/"unf" to "ctor"/"dtor"
blanchet
parents: 49498
diff changeset
  1229
    val dtor_nchotomy_thms = map (fn thm => thm RS @{thm surjD}) surj_dtor_thms;
acc9635a644a renamed "fld"/"unf" to "ctor"/"dtor"
blanchet
parents: 49498
diff changeset
  1230
    val dtor_inject_thms = map (fn thm => thm RS @{thm inj_eq}) inj_dtor_thms;
acc9635a644a renamed "fld"/"unf" to "ctor"/"dtor"
blanchet
parents: 49498
diff changeset
  1231
    val dtor_exhaust_thms = map (fn thm => thm RS exE) dtor_nchotomy_thms;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1232
49501
acc9635a644a renamed "fld"/"unf" to "ctor"/"dtor"
blanchet
parents: 49498
diff changeset
  1233
    val bij_ctor_thms =
acc9635a644a renamed "fld"/"unf" to "ctor"/"dtor"
blanchet
parents: 49498
diff changeset
  1234
      map2 (fn thm1 => fn thm2 => @{thm o_bij} OF [thm1, thm2]) dtor_o_ctor_thms ctor_o_dtor_thms;
acc9635a644a renamed "fld"/"unf" to "ctor"/"dtor"
blanchet
parents: 49498
diff changeset
  1235
    val inj_ctor_thms = map (fn thm => thm RS @{thm bij_is_inj}) bij_ctor_thms;
acc9635a644a renamed "fld"/"unf" to "ctor"/"dtor"
blanchet
parents: 49498
diff changeset
  1236
    val surj_ctor_thms = map (fn thm => thm RS @{thm bij_is_surj}) bij_ctor_thms;
acc9635a644a renamed "fld"/"unf" to "ctor"/"dtor"
blanchet
parents: 49498
diff changeset
  1237
    val ctor_nchotomy_thms = map (fn thm => thm RS @{thm surjD}) surj_ctor_thms;
acc9635a644a renamed "fld"/"unf" to "ctor"/"dtor"
blanchet
parents: 49498
diff changeset
  1238
    val ctor_inject_thms = map (fn thm => thm RS @{thm inj_eq}) inj_ctor_thms;
acc9635a644a renamed "fld"/"unf" to "ctor"/"dtor"
blanchet
parents: 49498
diff changeset
  1239
    val ctor_exhaust_thms = map (fn thm => thm RS exE) ctor_nchotomy_thms;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1240
49501
acc9635a644a renamed "fld"/"unf" to "ctor"/"dtor"
blanchet
parents: 49498
diff changeset
  1241
    val timer = time (timer "dtor definitions & thms");
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1242
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1243
    val fst_rec_pair_thms =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1244
      let
49504
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49502
diff changeset
  1245
        val mor = mor_comp_thm OF [mor_fold_thm, mor_convol_thm];
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1246
      in
49504
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49502
diff changeset
  1247
        map2 (fn unique => fn fold_ctor =>