src/HOL/Tools/BNF/bnf_lfp.ML
author traytel
Tue, 18 Feb 2014 14:51:26 +0100
changeset 55541 fd9ea8ae28f6
parent 55538 6a5986170c1d
child 55702 63c80031d8dd
permissions -rw-r--r--
syntactic simplifications of internal (co)datatype constructions
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);
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    85
    val FTsAs = mk_FTs allAs;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    86
    val FTsBs = mk_FTs allBs;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    87
    val FTsCs = mk_FTs allCs;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    88
    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
    89
    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
    90
    val B''Ts = map HOLogic.mk_setT activeCs;
52923
traytel
parents: 52913
diff changeset
    91
    val sTs = map2 (curry op -->) FTsAs activeAs;
traytel
parents: 52913
diff changeset
    92
    val s'Ts = map2 (curry op -->) FTsBs activeBs;
traytel
parents: 52913
diff changeset
    93
    val s''Ts = map2 (curry op -->) FTsCs activeCs;
traytel
parents: 52913
diff changeset
    94
    val fTs = map2 (curry op -->) activeAs activeBs;
traytel
parents: 52913
diff changeset
    95
    val inv_fTs = map2 (curry op -->) activeBs activeAs;
traytel
parents: 52913
diff changeset
    96
    val self_fTs = map2 (curry op -->) activeAs activeAs;
traytel
parents: 52913
diff changeset
    97
    val gTs = map2 (curry op -->) activeBs activeCs;
traytel
parents: 52913
diff changeset
    98
    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
    99
    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
   100
    val prodFTs = mk_FTs (passiveAs @ prodBsAs);
52923
traytel
parents: 52913
diff changeset
   101
    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
   102
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   103
    (* terms *)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   104
    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
   105
    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
   106
    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
   107
    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
   108
    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
   109
    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
   110
    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
   111
    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
   112
      (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
   113
    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
   114
    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
   115
    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
   116
      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
   117
        (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
   118
          (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
   119
      bd0s Dss bnfs;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   120
    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
   121
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   122
    val ((((((((((((((((((zs, zs'), Bs), Bs_copy), B's), B''s), ss), prod_ss), s's), s''s),
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   123
      fs), fs_copy), inv_fs), self_fs), gs), all_gs), (xFs, xFs')), (yFs, yFs')),
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   124
      names_lthy) = lthy
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   125
      |> mk_Frees' "z" activeAs
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   126
      ||>> mk_Frees "B" BTs
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'" B'Ts
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 "s" sTs
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   131
      ||>> mk_Frees "prods" prod_sTs
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   132
      ||>> mk_Frees "s'" s'Ts
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 "f" fTs
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" inv_fTs
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   137
      ||>> mk_Frees "f" self_fTs
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   138
      ||>> mk_Frees "g" gTs
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   139
      ||>> mk_Frees "g" all_gTs
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   140
      ||>> mk_Frees' "x" FTsAs
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   141
      ||>> mk_Frees' "y" FTsBs;
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;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   163
    val bd_Cnotzero = hd bd_Cnotzeros;
52635
4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents: 52505
diff changeset
   164
    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
   165
      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
   166
        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
   167
      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
   168
    val in_bds = map in_bd_of_bnf bnfs;
53287
271b34513bfb renamed BNF axiom
blanchet
parents: 53285
diff changeset
   169
    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
   170
    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
   171
    val map_cong0s = map map_cong0_of_bnf bnfs;
53270
c8628119d18e renamed BNF axiom
blanchet
parents: 53258
diff changeset
   172
    val map_id0s = map map_id0_of_bnf bnfs;
53285
f09645642984 renamed BNF fact
blanchet
parents: 53270
diff changeset
   173
    val map_ids = map map_id_of_bnf bnfs;
53290
b6c3be868217 renamed BNF fact
blanchet
parents: 53289
diff changeset
   174
    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
   175
    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
   176
    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
   177
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   178
    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
   179
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   180
    (* nonemptiness check *)
51070
6ca703425c01 made SML/NJ happy
traytel
parents: 49835
diff changeset
   181
    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
   182
49341
d406979024d1 nicer error message, indicating which type is empty (relying on metatheoretical completeness proof here)
blanchet
parents: 49337
diff changeset
   183
    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
   184
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   185
    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
   186
      (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
   187
        NONE =>
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   188
          (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
   189
            ~1 => NONE
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   190
          | 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
   191
      | 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
   192
    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
   193
    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
   194
        [] => ()
49390
a4202c1f4f9d tuned error message
blanchet
parents: 49362
diff changeset
   195
      | 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
   196
49341
d406979024d1 nicer error message, indicating which type is empty (relying on metatheoretical completeness proof here)
blanchet
parents: 49337
diff changeset
   197
    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
   198
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   199
    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
   200
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   201
    (* derived thms *)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   202
52956
1b62f05ab4fd honor user tfree names
blanchet
parents: 52938
diff changeset
   203
    (*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
   204
      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
   205
    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
   206
      let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   207
        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
   208
          (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
   209
        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
   210
          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
   211
      in
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51070
diff changeset
   212
        Goal.prove_sorry lthy [] []
49123
263b0e330d8b more work on sugar + simplify Trueprop + eq idiom everywhere
blanchet
parents: 49121
diff changeset
   213
          (fold_rev Logic.all (x :: fs @ all_gs) (mk_Trueprop_eq (lhs, rhs)))
53287
271b34513bfb renamed BNF axiom
blanchet
parents: 53285
diff changeset
   214
          (K (mk_map_comp_id_tac map_comp0))
49109
0e5b859e1c91 no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
traytel
parents: 49074
diff changeset
   215
        |> Thm.close_derivation
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   216
      end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   217
53288
050d0bc9afa5 renamed BNF fact
blanchet
parents: 53287
diff changeset
   218
    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
   219
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   220
    (*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
   221
      map id ... id f(m+1) ... f(m+n) x = x*)
53285
f09645642984 renamed BNF fact
blanchet
parents: 53270
diff changeset
   222
    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
   223
      let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   224
        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
   225
          (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
   226
        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
   227
        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
   228
      in
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51070
diff changeset
   229
        Goal.prove_sorry lthy [] []
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   230
          (fold_rev Logic.all (x :: self_fs) (Logic.list_implies (prems, goal)))
53285
f09645642984 renamed BNF fact
blanchet
parents: 53270
diff changeset
   231
          (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
   232
        |> Thm.close_derivation
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   233
      end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   234
53285
f09645642984 renamed BNF fact
blanchet
parents: 53270
diff changeset
   235
    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
   236
    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
   237
    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
   238
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   239
    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
   240
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   241
    (* algebra *)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   242
53566
5ff3a2d112d7 conceal internal bindings
traytel
parents: 53310
diff changeset
   243
    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
   244
    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
   245
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   246
    (*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
   247
    val alg_spec =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   248
      let
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   249
        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
   250
        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
   251
          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
   252
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   253
        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
   254
      in
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   255
        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
   256
      end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   257
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   258
    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
   259
        lthy
55204
345ee77213b5 use Local_Theory.define instead of Specification.definition for internal constants
traytel
parents: 55197
diff changeset
   260
        |> 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
   261
        ||> `Local_Theory.restore;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   262
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   263
    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
   264
    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
   265
    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
   266
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   267
    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
   268
      let
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   269
        val args = Bs @ ss;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   270
        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
   271
        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
   272
      in
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   273
        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
   274
      end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   275
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   276
    val alg_set_thms =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   277
      let
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   278
        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
   279
        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
   280
        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
   281
        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
   282
        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
   283
        val goals = map3 (fn x => fn prems => fn concl =>
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   284
          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
   285
            (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
   286
      in
49109
0e5b859e1c91 no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
traytel
parents: 49074
diff changeset
   287
        map (fn goal =>
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51070
diff changeset
   288
          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
   289
        goals
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   290
      end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   291
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   292
    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
   293
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   294
    val talg_thm =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   295
      let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   296
        val goal = fold_rev Logic.all ss
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   297
          (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
   298
      in
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51070
diff changeset
   299
        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
   300
          (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
   301
        |> Thm.close_derivation
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   302
      end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   303
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   304
    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
   305
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   306
    val alg_not_empty_thms =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   307
      let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   308
        val alg_prem =
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   309
          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
   310
        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
   311
        val goals =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   312
          map (fn concl =>
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   313
            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
   314
      in
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   315
        map2 (fn goal => fn alg_set =>
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51070
diff changeset
   316
          Goal.prove_sorry lthy [] []
51798
ad3a241def73 uniform Proof.context for hyp_subst_tac;
wenzelm
parents: 51782
diff changeset
   317
            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
   318
          |> Thm.close_derivation)
0e5b859e1c91 no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
traytel
parents: 49074
diff changeset
   319
        goals alg_set_thms
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   320
      end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   321
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   322
    val timer = time (timer "Proved nonemptiness");
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   323
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   324
    (* morphism *)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   325
53566
5ff3a2d112d7 conceal internal bindings
traytel
parents: 53310
diff changeset
   326
    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
   327
    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
   328
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   329
    (*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
   330
    (*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
   331
       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
   332
    val mor_spec =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   333
      let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   334
        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
   335
          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
   336
        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
   337
          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
   338
            (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
   339
              (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
   340
        val rhs = HOLogic.mk_conj
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 (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
   342
          Library.foldr1 HOLogic.mk_conj
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   343
            (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
   344
      in
55204
345ee77213b5 use Local_Theory.define instead of Specification.definition for internal constants
traytel
parents: 55197
diff changeset
   345
        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
   346
      end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   347
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   348
    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
   349
        lthy
55204
345ee77213b5 use Local_Theory.define instead of Specification.definition for internal constants
traytel
parents: 55197
diff changeset
   350
        |> 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
   351
        ||> `Local_Theory.restore;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   352
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   353
    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
   354
    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
   355
    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
   356
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   357
    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
   358
      let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   359
        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
   360
        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
   361
        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
   362
      in
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   363
        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
   364
      end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   365
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   366
    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
   367
      let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   368
        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
   369
        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
   370
          (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
   371
        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
   372
        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
   373
          (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
   374
        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
   375
          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
   376
            (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
   377
              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
   378
        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
   379
        fun prove goal =
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51070
diff changeset
   380
          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
   381
      in
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   382
        (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
   383
      end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   384
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   385
    val mor_incl_thm =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   386
      let
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51869
diff changeset
   387
        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
   388
        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
   389
      in
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51070
diff changeset
   390
        Goal.prove_sorry lthy [] []
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   391
          (fold_rev Logic.all (Bs @ ss @ Bs_copy) (Logic.list_implies (prems, concl)))
53285
f09645642984 renamed BNF fact
blanchet
parents: 53270
diff changeset
   392
          (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
   393
        |> Thm.close_derivation
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   394
      end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   395
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   396
    val mor_comp_thm =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   397
      let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   398
        val prems =
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 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
   400
           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
   401
        val concl =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   402
          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
   403
      in
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51070
diff changeset
   404
        Goal.prove_sorry lthy [] []
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   405
          (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
   406
             (Logic.list_implies (prems, concl)))
53290
b6c3be868217 renamed BNF fact
blanchet
parents: 53289
diff changeset
   407
          (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
   408
        |> Thm.close_derivation
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   409
      end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   410
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   411
    val mor_inv_thm =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   412
      let
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51869
diff changeset
   413
        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
   414
          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
   415
        val prems = map HOLogic.mk_Trueprop
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   416
          ([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
   417
          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
   418
        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
   419
      in
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51070
diff changeset
   420
        Goal.prove_sorry lthy [] []
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   421
          (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
   422
            (Logic.list_implies (prems, concl)))
53290
b6c3be868217 renamed BNF fact
blanchet
parents: 53289
diff changeset
   423
          (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
   424
        |> Thm.close_derivation
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   425
      end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   426
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   427
    val mor_cong_thm =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   428
      let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   429
        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
   430
         (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
   431
        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
   432
      in
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51070
diff changeset
   433
        Goal.prove_sorry lthy [] []
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   434
          (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
   435
             (Logic.list_implies (prems, concl)))
51798
ad3a241def73 uniform Proof.context for hyp_subst_tac;
wenzelm
parents: 51782
diff changeset
   436
          (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
   437
        |> Thm.close_derivation
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   438
      end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   439
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   440
    val mor_str_thm =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   441
      let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   442
        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
   443
          (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
   444
      in
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51070
diff changeset
   445
        Goal.prove_sorry lthy [] []
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   446
          (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
   447
            (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
   448
          (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
   449
        |> Thm.close_derivation
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   450
      end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   451
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   452
    val mor_convol_thm =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   453
      let
49458
blanchet
parents: 49457
diff changeset
   454
        val maps = map3 (fn s => fn prod_s => fn mapx =>
blanchet
parents: 49457
diff changeset
   455
          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
   456
          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
   457
      in
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51070
diff changeset
   458
        Goal.prove_sorry lthy [] []
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   459
          (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
   460
            (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
   461
          (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
   462
        |> Thm.close_derivation
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   463
      end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   464
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   465
    val mor_UNIV_thm =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   466
      let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   467
        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
   468
            (HOLogic.mk_comp (f, s),
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   469
            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
   470
        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
   471
        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
   472
      in
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51070
diff changeset
   473
        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
   474
          (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
   475
        |> Thm.close_derivation
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   476
      end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   477
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   478
    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
   479
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   480
    (* isomorphism *)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   481
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   482
    (*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
   483
       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
   484
    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
   485
      let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   486
        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
   487
          (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
   488
            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
   489
              (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
   490
      in
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   491
        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
   492
      end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   493
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   494
    val iso_alt_thm =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   495
      let
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   496
        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
   497
        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
   498
          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
   499
            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
   500
      in
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51070
diff changeset
   501
        Goal.prove_sorry lthy [] []
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   502
          (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
   503
          (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
   504
        |> Thm.close_derivation
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   505
      end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   506
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   507
    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
   508
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   509
    (* algebra copies *)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   510
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   511
    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
   512
      let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   513
        val prems = map HOLogic.mk_Trueprop
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   514
         (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
   515
        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
   516
          (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
   517
        val all_prems = prems @ inver_prems;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   518
        fun mk_s f s mapT y y' = Term.absfree y' (f $ (s $
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   519
          (Term.list_comb (mapT, passive_ids @ inv_fs) $ y)));
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   520
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   521
        val alg = HOLogic.mk_Trueprop
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   522
          (mk_alg B's (map5 mk_s fs ss mapsBsAs yFs yFs'));
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51070
diff changeset
   523
        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
   524
          (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
   525
            (Logic.list_implies (all_prems, alg)))
53290
b6c3be868217 renamed BNF fact
blanchet
parents: 53289
diff changeset
   526
          (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
   527
          |> Thm.close_derivation;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   528
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   529
        val iso = HOLogic.mk_Trueprop
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   530
          (mk_iso B's (map5 mk_s fs ss mapsBsAs yFs yFs') Bs ss inv_fs fs_copy);
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51070
diff changeset
   531
        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
   532
          (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
   533
            (Logic.list_implies (all_prems, iso)))
53290
b6c3be868217 renamed BNF fact
blanchet
parents: 53289
diff changeset
   534
          (K (mk_copy_alg_tac 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
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   555
    val sum_Card_order = if n = 1 then bd_Card_order else @{thm Card_order_csum};
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   556
    val sum_Cnotzero = if n = 1 then bd_Cnotzero else bd_Cnotzero RS @{thm csum_Cnotzero1};
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   557
    val sum_Cinfinite = if n = 1 then bd_Cinfinite else bd_Cinfinite RS @{thm Cinfinite_csum1};
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   558
    fun mk_set_bd_sums i bd_Card_order bds =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   559
      if n = 1 then bds
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   560
      else map (fn thm => bd_Card_order RS mk_ordLeq_csum n i thm) bds;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   561
    val set_bd_sumss = map3 mk_set_bd_sums ks bd_Card_orders set_bdss;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   562
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   563
    fun mk_in_bd_sum i Co Cnz bd =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   564
      if n = 1 then bd
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   565
      else Cnz RS ((Co RS mk_ordLeq_csum n i (Co RS @{thm ordLeq_refl})) RS
51782
84e7225f5ab6 removed unnecessary assumptions in some theorems about cardinal exponentiation
traytel
parents: 51767
diff changeset
   566
        (bd RS @{thm ordLeq_transitive[OF _ cexp_mono2_Cnotzero[OF _ Card_order_csum]]}));
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   567
    val in_bd_sums = map4 mk_in_bd_sum ks bd_Card_orders bd_Cnotzeros in_bds;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   568
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   569
    val sum_bd = Library.foldr1 (uncurry mk_csum) bds;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   570
    val suc_bd = mk_cardSuc sum_bd;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   571
    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
   572
    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
   573
    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
   574
      | mk_Asuc_bd As =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   575
        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
   576
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   577
    val suc_bd_Card_order = if n = 1 then bd_Card_order RS @{thm cardSuc_Card_order}
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   578
      else @{thm cardSuc_Card_order[OF Card_order_csum]};
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   579
    val suc_bd_Cinfinite = if n = 1 then bd_Cinfinite RS @{thm Cinfinite_cardSuc}
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   580
      else bd_Cinfinite RS @{thm Cinfinite_cardSuc[OF Cinfinite_csum1]};
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   581
    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
   582
    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
   583
    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
   584
        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
   585
    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
   586
51782
84e7225f5ab6 removed unnecessary assumptions in some theorems about cardinal exponentiation
traytel
parents: 51767
diff changeset
   587
    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
   588
      [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
   589
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   590
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   591
    val Asuc_bd = mk_Asuc_bd passive_UNIVs;
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   592
    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
   593
    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
   594
    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
   595
      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
   596
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   597
    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
   598
      names_lthy) = names_lthy
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   599
      |> 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
   600
      ||>> (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
   601
      ||>> 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
   602
      ||>> 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
   603
      ||>> mk_Frees "IIB" II_BTs
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   604
      ||>> mk_Frees "IIs" II_sTs
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   605
      ||>> 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
   606
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   607
    val suc_bd_limit_thm =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   608
      let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   609
        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
   610
          (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
   611
        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
   612
          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
   613
        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
   614
          (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
   615
      in
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51070
diff changeset
   616
        Goal.prove_sorry lthy [] []
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   617
          (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
   618
          (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
   619
        |> Thm.close_derivation
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   620
      end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   621
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   622
    val timer = time (timer "Bounds");
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   623
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   624
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   625
    (* minimal algebra *)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   626
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   627
    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
   628
      (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
   629
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   630
    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
   631
      HOLogic.mk_binop @{const_name "sup"}
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   632
      (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
   633
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   634
    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
   635
      let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   636
        val BTs = map (range_type o fastype_of) ss;
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   637
        val Ts = passiveAs @ BTs;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   638
        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
   639
          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
   640
      in
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   641
         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
   642
           (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
   643
      end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   644
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   645
    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
   646
      let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   647
        val i_field = HOLogic.mk_mem (idx, field_suc_bd);
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   648
        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
   649
        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
   650
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   651
        val concl = HOLogic.mk_Trueprop
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   652
          (HOLogic.mk_eq (min_algs $ idx, HOLogic.mk_tuple
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   653
            (map4 (mk_minH_component min_algs idx) setssAs FTsAs ss ks)));
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   654
        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
   655
          (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
   656
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51070
diff changeset
   657
        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
   658
          (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
   659
          |> Thm.close_derivation;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   660
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   661
        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
   662
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   663
        fun mk_mono_goal min_alg =
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   664
          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
   665
            (Term.absfree idx' min_alg)));
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   666
49109
0e5b859e1c91 no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
traytel
parents: 49074
diff changeset
   667
        val monos =
0e5b859e1c91 no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
traytel
parents: 49074
diff changeset
   668
          map2 (fn goal => fn min_algs =>
51798
ad3a241def73 uniform Proof.context for hyp_subst_tac;
wenzelm
parents: 51782
diff changeset
   669
            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
   670
            |> Thm.close_derivation)
0e5b859e1c91 no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
traytel
parents: 49074
diff changeset
   671
          (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
   672
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   673
        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
   674
        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
   675
        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
   676
        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
   677
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   678
        val card_of = singleton (Proof_Context.export names_lthy lthy)
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51070
diff changeset
   679
          (Goal.prove_sorry lthy [] []
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   680
            (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
   681
            (K (mk_min_algs_card_of_tac card_cT card_ct
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   682
              m suc_bd_worel min_algs_thms in_bd_sums
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   683
              sum_Card_order sum_Cnotzero suc_bd_Card_order suc_bd_Cinfinite suc_bd_Cnotzero
51812
329c62d99979 removed unreferenced thm
blanchet
parents: 51805
diff changeset
   684
              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
   685
          |> Thm.close_derivation;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   686
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   687
        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
   688
        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
   689
        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
   690
        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
   691
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   692
        val least = singleton (Proof_Context.export names_lthy lthy)
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51070
diff changeset
   693
          (Goal.prove_sorry lthy [] []
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   694
            (Logic.mk_implies (least_prem,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   695
              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
   696
            (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
   697
              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
   698
          |> Thm.close_derivation;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   699
      in
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   700
        (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
   701
      end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   702
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   703
    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
   704
53566
5ff3a2d112d7 conceal internal bindings
traytel
parents: 53310
diff changeset
   705
    val min_alg_binds = mk_internal_bs min_algN;
5ff3a2d112d7 conceal internal bindings
traytel
parents: 53310
diff changeset
   706
    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
   707
    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
   708
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   709
    fun min_alg_spec i =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   710
      let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   711
        val rhs = mk_UNION (field_suc_bd)
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   712
          (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
   713
      in
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   714
        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
   715
      end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   716
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   717
    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
   718
        lthy
55204
345ee77213b5 use Local_Theory.define instead of Specification.definition for internal constants
traytel
parents: 55197
diff changeset
   719
        |> fold_map (fn i => Local_Theory.define
345ee77213b5 use Local_Theory.define instead of Specification.definition for internal constants
traytel
parents: 55197
diff changeset
   720
          ((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
   721
        |>> 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
   722
        ||> `Local_Theory.restore;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   723
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   724
    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
   725
    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
   726
    val min_alg_defs = map (fn def =>
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   727
      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
   728
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   729
    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
   730
      let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   731
        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
   732
        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
   733
        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
   734
      in
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   735
        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
   736
      end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   737
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   738
    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
   739
      let
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   740
        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
   741
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   742
        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
   743
        val alg_min_alg = 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
   744
          (K (mk_alg_min_alg_tac m alg_def min_alg_defs suc_bd_limit_thm sum_Cinfinite
49109
0e5b859e1c91 no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
traytel
parents: 49074
diff changeset
   745
            set_bd_sumss min_algs_thms min_algs_mono_thms))
0e5b859e1c91 no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
traytel
parents: 49074
diff changeset
   746
          |> Thm.close_derivation;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   747
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51070
diff changeset
   748
        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
   749
          (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
   750
            (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
   751
          (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
   752
            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
   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
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   755
        val least_prem = HOLogic.mk_Trueprop (mk_alg Bs ss);
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51070
diff changeset
   756
        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
   757
          (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
   758
            (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
   759
          (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
   760
          |> Thm.close_derivation;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   761
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   762
        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
   763
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   764
        val incl_prem = HOLogic.mk_Trueprop (mk_alg Bs ss);
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   765
        val incl_min_algs = map (mk_min_alg ss) ks;
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51070
diff changeset
   766
        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
   767
          (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
   768
            (Logic.mk_implies (incl_prem,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   769
              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
   770
          (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
   771
          |> Thm.close_derivation;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   772
      in
49109
0e5b859e1c91 no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
traytel
parents: 49074
diff changeset
   773
        (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
   774
      end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   775
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   776
    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
   777
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   778
    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
   779
    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
   780
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   781
    val ((IIT_name, (IIT_glob_info, IIT_loc_info)), lthy) =
49835
31f32ec4d766 discontinued typedef with alternative name;
wenzelm
parents: 49833
diff changeset
   782
      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
   783
        (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
   784
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   785
    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
   786
    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
   787
    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
   788
    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
   789
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   790
    val initT = IIT --> Asuc_bdT;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   791
    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
   792
    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
   793
    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
   794
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   795
    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
   796
      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
   797
      |> 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
   798
      ||>> mk_Frees "ix" active_initTs
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   799
      ||>> mk_Frees' "x" init_FTs
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   800
      ||>> mk_Frees "f" init_fTs
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   801
      ||>> mk_Frees "f" init_fTs
49463
83ac281bcdc2 provide predicator, define relator
blanchet
parents: 49460
diff changeset
   802
      ||>> 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
   803
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   804
    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
   805
      (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
   806
        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
   807
        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
   808
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   809
    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
   810
    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
   811
53566
5ff3a2d112d7 conceal internal bindings
traytel
parents: 53310
diff changeset
   812
    val str_init_binds = mk_internal_bs str_initN;
5ff3a2d112d7 conceal internal bindings
traytel
parents: 53310
diff changeset
   813
    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
   814
    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
   815
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   816
    fun str_init_spec i =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   817
      let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   818
        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
   819
        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
   820
        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
   821
          (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
   822
          (nth bnfs (i - 1));
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   823
        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
   824
        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
   825
      in
55204
345ee77213b5 use Local_Theory.define instead of Specification.definition for internal constants
traytel
parents: 55197
diff changeset
   826
        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
   827
      end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   828
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   829
    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
   830
      lthy
55204
345ee77213b5 use Local_Theory.define instead of Specification.definition for internal constants
traytel
parents: 55197
diff changeset
   831
      |> fold_map (fn i => Local_Theory.define
345ee77213b5 use Local_Theory.define instead of Specification.definition for internal constants
traytel
parents: 55197
diff changeset
   832
        ((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
   833
      |>> 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
   834
      ||> `Local_Theory.restore;
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 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
   837
    val str_inits =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   838
      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
   839
        str_init_frees;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   840
55204
345ee77213b5 use Local_Theory.define instead of Specification.definition for internal constants
traytel
parents: 55197
diff changeset
   841
    val str_init_defs = map (fn def =>
345ee77213b5 use Local_Theory.define instead of Specification.definition for internal constants
traytel
parents: 55197
diff changeset
   842
      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
   843
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   844
    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
   845
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   846
    (*TODO: replace with instantiate? (problem: figure out right type instantiation)*)
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51070
diff changeset
   847
    val alg_init_thm = Goal.prove_sorry lthy [] []
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   848
      (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
   849
      (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
   850
      |> Thm.close_derivation;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   851
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51070
diff changeset
   852
    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
   853
      (HOLogic.mk_Trueprop (mk_Ball II
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   854
        (Term.absfree iidx' (mk_alg select_Bs select_ss))))
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
   855
      (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
   856
      |> Thm.close_derivation;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   857
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   858
    val mor_select_thm =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   859
      let
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   860
        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
   861
        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
   862
        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
   863
        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
   864
        val concl = HOLogic.mk_Trueprop
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   865
          (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
   866
            (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
   867
      in
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51070
diff changeset
   868
        Goal.prove_sorry lthy [] []
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   869
          (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
   870
          (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
   871
            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
   872
        |> Thm.close_derivation
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   873
      end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   874
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   875
    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
   876
      let
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55538
diff changeset
   877
        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
   878
        val concl = HOLogic.mk_Trueprop
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   879
          (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
   880
        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
   881
          (fold_rev Logic.all (Bs @ ss) (Logic.mk_implies (prem, concl)))
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
   882
          (fn {context = ctxt, prems = _} => mk_init_ex_mor_tac ctxt Abs_IIT_inverse_thm
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
   883
            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
   884
            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
   885
          |> Thm.close_derivation;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   886
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   887
        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
   888
        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
   889
          [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
   890
          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
   891
        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
   892
        val unique = HOLogic.mk_Trueprop
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   893
          (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
   894
        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
   895
          (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
   896
            (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
   897
          (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
   898
            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
   899
          |> Thm.close_derivation;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   900
      in
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   901
        (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
   902
      end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   903
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   904
    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
   905
    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
   906
    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
   907
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   908
    fun mk_closed phis =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   909
      let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   910
        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
   911
          let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   912
            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
   913
              (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
   914
            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
   915
          in
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   916
            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
   917
          end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   918
      in
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   919
        Library.foldr1 HOLogic.mk_conj
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   920
          (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
   921
      end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   922
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   923
    val init_induct_thm =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   924
      let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   925
        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
   926
        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
   927
          (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
   928
      in
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51070
diff changeset
   929
        Goal.prove_sorry lthy [] []
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   930
          (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
   931
          (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
   932
        |> Thm.close_derivation
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   933
      end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   934
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   935
    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
   936
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   937
    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
   938
      lthy
53566
5ff3a2d112d7 conceal internal bindings
traytel
parents: 53310
diff changeset
   939
      |> fold_map3 (fn b => fn mx => fn car_init =>
5ff3a2d112d7 conceal internal bindings
traytel
parents: 53310
diff changeset
   940
        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
   941
          (EVERY' [rtac ssubst, rtac @{thm ex_in_conv}, resolve_tac alg_not_empty_thms,
49169
937a0fadddfb honor mixfix specifications
blanchet
parents: 49134
diff changeset
   942
            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
   943
      |>> 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
   944
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   945
    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
   946
    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
   947
    val Ts' = mk_Ts passiveBs;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   948
    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
   949
    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
   950
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   951
    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
   952
    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
   953
    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
   954
    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
   955
    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
   956
    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
   957
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   958
    fun mk_inver_thm mk_tac rep abs X thm =
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51070
diff changeset
   959
      Goal.prove_sorry lthy [] []
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   960
        (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
   961
        (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
   962
      |> Thm.close_derivation;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   963
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   964
    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
   965
    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
   966
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   967
    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
   968
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   969
    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
   970
    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
   971
    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
   972
    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
   973
    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
   974
    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
   975
    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
   976
    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
   977
      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
   978
    val fTs = map2 (curry op -->) Ts activeAs;
49504
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49502
diff changeset
   979
    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
   980
    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
   981
    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
   982
    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
   983
    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
   984
    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
   985
49331
f4169aa67513 free variable name tuning
blanchet
parents: 49330
diff changeset
   986
    val (((((((((Izs1, Izs1'), (Izs2, Izs2')), (xFs, xFs')), yFs), (AFss, AFss')),
49504
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49502
diff changeset
   987
      (fold_f, fold_f')), fs), rec_ss), names_lthy) = names_lthy
49331
f4169aa67513 free variable name tuning
blanchet
parents: 49330
diff changeset
   988
      |> mk_Frees' "z1" Ts
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   989
      ||>> mk_Frees' "z2" Ts'
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   990
      ||>> mk_Frees' "x" FTs
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   991
      ||>> mk_Frees "y" FTs'
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   992
      ||>> mk_Freess' "z" setFTss
49504
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49502
diff changeset
   993
      ||>> 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
   994
      ||>> mk_Frees "f" fTs
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   995
      ||>> mk_Frees "s" rec_sTs;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   996
49331
f4169aa67513 free variable name tuning
blanchet
parents: 49330
diff changeset
   997
    val Izs = map2 retype_free Ts zs;
49463
83ac281bcdc2 provide predicator, define relator
blanchet
parents: 49460
diff changeset
   998
    val phis = map2 retype_free (map mk_pred1T Ts) init_phis;
83ac281bcdc2 provide predicator, define relator
blanchet
parents: 49460
diff changeset
   999
    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
  1000
54492
6fae4ecd4ab3 prefix internal names as well
blanchet
parents: 54487
diff changeset
  1001
    fun ctor_bind i = nth external_bs (i - 1) |> Binding.prefix_name (ctorN ^ "_");
53566
5ff3a2d112d7 conceal internal bindings
traytel
parents: 53310
diff changeset
  1002
    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
  1003
55204
345ee77213b5 use Local_Theory.define instead of Specification.definition for internal constants
traytel
parents: 55197
diff changeset
  1004
    fun ctor_spec abs str map_FT_init x x' =
345ee77213b5 use Local_Theory.define instead of Specification.definition for internal constants
traytel
parents: 55197
diff changeset
  1005
      Term.absfree x' (abs $ (str $
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1006
          (Term.list_comb (map_FT_init, map HOLogic.id_const passiveAs @ Rep_Ts) $ x)));
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1007
49501
acc9635a644a renamed "fld"/"unf" to "ctor"/"dtor"
blanchet
parents: 49498
diff changeset
  1008
    val ((ctor_frees, (_, ctor_def_frees)), (lthy, lthy_old)) =
49311
blanchet
parents: 49308
diff changeset
  1009
      lthy
49458
blanchet
parents: 49457
diff changeset
  1010
      |> fold_map6 (fn i => fn abs => fn str => fn mapx => fn x => fn x' =>
55204
345ee77213b5 use Local_Theory.define instead of Specification.definition for internal constants
traytel
parents: 55197
diff changeset
  1011
        Local_Theory.define
345ee77213b5 use Local_Theory.define instead of Specification.definition for internal constants
traytel
parents: 55197
diff changeset
  1012
          ((ctor_bind i, NoSyn), (ctor_def_bind i, ctor_spec abs str mapx x x')))
49311
blanchet
parents: 49308
diff changeset
  1013
          ks Abs_Ts str_inits map_FT_inits xFs xFs'
blanchet
parents: 49308
diff changeset
  1014
      |>> apsnd split_list o split_list
blanchet
parents: 49308
diff changeset
  1015
      ||> `Local_Theory.restore;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1016
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1017
    val phi = Proof_Context.export_morphism lthy_old lthy;
49501
acc9635a644a renamed "fld"/"unf" to "ctor"/"dtor"
blanchet
parents: 49498
diff changeset
  1018
    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
  1019
      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
  1020
        Morphism.term phi) ctor_frees;
acc9635a644a renamed "fld"/"unf" to "ctor"/"dtor"
blanchet
parents: 49498
diff changeset
  1021
    val ctors = mk_ctors passiveAs;
acc9635a644a renamed "fld"/"unf" to "ctor"/"dtor"
blanchet
parents: 49498
diff changeset
  1022
    val ctor's = mk_ctors passiveBs;
55204
345ee77213b5 use Local_Theory.define instead of Specification.definition for internal constants
traytel
parents: 55197
diff changeset
  1023
    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
  1024
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1025
    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
  1026
      let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1027
        val copy = alg_init_thm RS copy_alg_thm;
49227
2652319c394e open typedef for datatypes
traytel
parents: 49222
diff changeset
  1028
        fun mk_bij inj Rep cases = @{thm bij_betwI'} OF [inj, Rep, cases];
2652319c394e open typedef for datatypes
traytel
parents: 49222
diff changeset
  1029
        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
  1030
        val mor_Rep =
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51070
diff changeset
  1031
          Goal.prove_sorry lthy [] []
49501
acc9635a644a renamed "fld"/"unf" to "ctor"/"dtor"
blanchet
parents: 49498
diff changeset
  1032
            (HOLogic.mk_Trueprop (mk_mor UNIVs ctors car_inits str_inits Rep_Ts))
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
  1033
            (fn {context = ctxt, prems = _} => mk_mor_Rep_tac ctxt ctor_defs copy bijs inver_Abss
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
  1034
              inver_Reps)
49109
0e5b859e1c91 no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
traytel
parents: 49074
diff changeset
  1035
          |> Thm.close_derivation;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1036
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1037
        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
  1038
        val mor_Abs =
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51070
diff changeset
  1039
          Goal.prove_sorry lthy [] []
49501
acc9635a644a renamed "fld"/"unf" to "ctor"/"dtor"
blanchet
parents: 49498
diff changeset
  1040
            (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
  1041
            (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
  1042
          |> Thm.close_derivation;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1043
      in
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1044
        (mor_Rep, mor_Abs)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1045
      end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1046
49501
acc9635a644a renamed "fld"/"unf" to "ctor"/"dtor"
blanchet
parents: 49498
diff changeset
  1047
    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
  1048
49504
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49502
diff changeset
  1049
    val fold_fun = Term.absfree fold_f'
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49502
diff changeset
  1050
      (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
  1051
    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
  1052
54492
6fae4ecd4ab3 prefix internal names as well
blanchet
parents: 54487
diff changeset
  1053
    fun fold_bind i = nth external_bs (i - 1) |> Binding.prefix_name (ctor_foldN ^ "_");
53566
5ff3a2d112d7 conceal internal bindings
traytel
parents: 53310
diff changeset
  1054
    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
  1055
55204
345ee77213b5 use Local_Theory.define instead of Specification.definition for internal constants
traytel
parents: 55197
diff changeset
  1056
    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
  1057
49504
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49502
diff changeset
  1058
    val ((fold_frees, (_, fold_def_frees)), (lthy, lthy_old)) =
49311
blanchet
parents: 49308
diff changeset
  1059
      lthy
55204
345ee77213b5 use Local_Theory.define instead of Specification.definition for internal constants
traytel
parents: 55197
diff changeset
  1060
      |> fold_map (fn i =>
345ee77213b5 use Local_Theory.define instead of Specification.definition for internal constants
traytel
parents: 55197
diff changeset
  1061
        Local_Theory.define ((fold_bind i, NoSyn), (fold_def_bind i, fold_spec i))) ks
49311
blanchet
parents: 49308
diff changeset
  1062
      |>> apsnd split_list o split_list
blanchet
parents: 49308
diff changeset
  1063
      ||> `Local_Theory.restore;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1064
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1065
    val phi = Proof_Context.export_morphism lthy_old lthy;
49504
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49502
diff changeset
  1066
    val folds = map (Morphism.term phi) fold_frees;
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49502
diff changeset
  1067
    val fold_names = map (fst o dest_Const) folds;
52731
dacd47a0633f transfer rule for {c,d}tor_{,un}fold
traytel
parents: 52659
diff changeset
  1068
    fun mk_folds passives actives =
dacd47a0633f transfer rule for {c,d}tor_{,un}fold
traytel
parents: 52659
diff changeset
  1069
      map3 (fn name => fn T => fn active =>
dacd47a0633f transfer rule for {c,d}tor_{,un}fold
traytel
parents: 52659
diff changeset
  1070
        Const (name, Library.foldr (op -->)
52923
traytel
parents: 52913
diff changeset
  1071
          (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
  1072
      fold_names (mk_Ts passives) actives;
49504
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49502
diff changeset
  1073
    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
  1074
      (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
  1075
    val fold_defs = map (fn def =>
345ee77213b5 use Local_Theory.define instead of Specification.definition for internal constants
traytel
parents: 55197
diff changeset
  1076
      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
  1077
49504
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49502
diff changeset
  1078
    val mor_fold_thm =
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1079
      let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1080
        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
  1081
        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
  1082
        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
  1083
        val cT = certifyT lthy foldT;
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49502
diff changeset
  1084
        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
  1085
      in
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1086
        singleton (Proof_Context.export names_lthy lthy)
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51070
diff changeset
  1087
          (Goal.prove_sorry lthy [] []
49504
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49502
diff changeset
  1088
            (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
  1089
            (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
  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
      end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1092
49504
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49502
diff changeset
  1093
    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
  1094
      ((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
  1095
      (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
  1096
49504
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49502
diff changeset
  1097
    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
  1098
      let
49501
acc9635a644a renamed "fld"/"unf" to "ctor"/"dtor"
blanchet
parents: 49498
diff changeset
  1099
        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
  1100
        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
  1101
        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
  1102
        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
  1103
          (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
  1104
          (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
  1105
            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
  1106
          |> Thm.close_derivation;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1107
      in
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1108
        `split_conj_thm unique_mor
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1109
      end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1110
52911
fe4c2418f069 tuned tactic;
traytel
parents: 52904
diff changeset
  1111
    val (ctor_fold_unique_thms, ctor_fold_unique_thm) =
fe4c2418f069 tuned tactic;
traytel
parents: 52904
diff changeset
  1112
      `split_conj_thm (mk_conjIN n RS
52904
traytel
parents: 52839
diff changeset
  1113
        (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
  1114
49504
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49502
diff changeset
  1115
    val fold_ctor_thms =
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1116
      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
  1117
        fold_unique_mor_thms;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1118
49504
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49502
diff changeset
  1119
    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
  1120
      let
49504
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49502
diff changeset
  1121
        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
  1122
      in
49504
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49502
diff changeset
  1123
        map2 (fn unique => fn fold_ctor =>
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49502
diff changeset
  1124
          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
  1125
      end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1126
49504
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49502
diff changeset
  1127
    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
  1128
49501
acc9635a644a renamed "fld"/"unf" to "ctor"/"dtor"
blanchet
parents: 49498
diff changeset
  1129
    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
  1130
      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
  1131
        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
  1132
54492
6fae4ecd4ab3 prefix internal names as well
blanchet
parents: 54487
diff changeset
  1133
    fun dtor_bind i = nth external_bs (i - 1) |> Binding.prefix_name (dtorN ^ "_");
53566
5ff3a2d112d7 conceal internal bindings
traytel
parents: 53310
diff changeset
  1134
    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
  1135
55204
345ee77213b5 use Local_Theory.define instead of Specification.definition for internal constants
traytel
parents: 55197
diff changeset
  1136
    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
  1137
49501
acc9635a644a renamed "fld"/"unf" to "ctor"/"dtor"
blanchet
parents: 49498
diff changeset
  1138
    val ((dtor_frees, (_, dtor_def_frees)), (lthy, lthy_old)) =
49311
blanchet
parents: 49308
diff changeset
  1139
      lthy
55204
345ee77213b5 use Local_Theory.define instead of Specification.definition for internal constants
traytel
parents: 55197
diff changeset
  1140
      |> fold_map (fn i =>
345ee77213b5 use Local_Theory.define instead of Specification.definition for internal constants
traytel
parents: 55197
diff changeset
  1141
        Local_Theory.define ((dtor_bind i, NoSyn), (dtor_def_bind i, dtor_spec i))) ks
49311
blanchet
parents: 49308
diff changeset
  1142
      |>> apsnd split_list o split_list
blanchet
parents: 49308
diff changeset
  1143
      ||> `Local_Theory.restore;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1144
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1145
    val phi = Proof_Context.export_morphism lthy_old lthy;
49501
acc9635a644a renamed "fld"/"unf" to "ctor"/"dtor"
blanchet
parents: 49498
diff changeset
  1146
    fun mk_dtors params =
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1147
      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
  1148
        dtor_frees;
acc9635a644a renamed "fld"/"unf" to "ctor"/"dtor"
blanchet
parents: 49498
diff changeset
  1149
    val dtors = mk_dtors params';
55204
345ee77213b5 use Local_Theory.define instead of Specification.definition for internal constants
traytel
parents: 55197
diff changeset
  1150
    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
  1151
49504
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49502
diff changeset
  1152
    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
  1153
49501
acc9635a644a renamed "fld"/"unf" to "ctor"/"dtor"
blanchet
parents: 49498
diff changeset
  1154
    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
  1155
      let
49501
acc9635a644a renamed "fld"/"unf" to "ctor"/"dtor"
blanchet
parents: 49498
diff changeset
  1156
        fun mk_goal dtor ctor FT =
acc9635a644a renamed "fld"/"unf" to "ctor"/"dtor"
blanchet
parents: 49498
diff changeset
  1157
          mk_Trueprop_eq (HOLogic.mk_comp (dtor, ctor), HOLogic.id_const FT);
acc9635a644a renamed "fld"/"unf" to "ctor"/"dtor"
blanchet
parents: 49498
diff changeset
  1158
        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
  1159
      in
51761
4c9f08836d87 renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents: 51758
diff changeset
  1160
        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
  1161
          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
  1162
            (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
  1163
          |> Thm.close_derivation)
51761
4c9f08836d87 renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents: 51758
diff changeset
  1164
        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
  1165
      end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1166
49501
acc9635a644a renamed "fld"/"unf" to "ctor"/"dtor"
blanchet
parents: 49498
diff changeset
  1167
    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
  1168
    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
  1169
49501
acc9635a644a renamed "fld"/"unf" to "ctor"/"dtor"
blanchet
parents: 49498
diff changeset
  1170
    val bij_dtor_thms =
acc9635a644a renamed "fld"/"unf" to "ctor"/"dtor"
blanchet
parents: 49498
diff changeset
  1171
      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
  1172
    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
  1173
    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
  1174
    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
  1175
    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
  1176
    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
  1177
49501
acc9635a644a renamed "fld"/"unf" to "ctor"/"dtor"
blanchet
parents: 49498
diff changeset
  1178
    val bij_ctor_thms =
acc9635a644a renamed "fld"/"unf" to "ctor"/"dtor"
blanchet
parents: 49498
diff changeset
  1179
      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
  1180
    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
  1181
    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
  1182
    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
  1183
    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
  1184
    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
  1185
49501
acc9635a644a renamed "fld"/"unf" to "ctor"/"dtor"
blanchet
parents: 49498
diff changeset
  1186
    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
  1187
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1188
    val fst_rec_pair_thms =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1189
      let
49504
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49502
diff changeset
  1190
        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
  1191
      in
49504
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49502
diff changeset
  1192
        map2 (fn unique => fn fold_ctor =>
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49502
diff changeset
  1193
          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
  1194
      end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1195
54492
6fae4ecd4ab3 prefix internal names as well
blanchet
parents: 54487
diff changeset
  1196
    fun rec_bind i = nth external_bs (i - 1) |> Binding.prefix_name (ctor_recN ^ "_");
53566
5ff3a2d112d7 conceal internal bindings
traytel
parents: 53310
diff changeset
  1197
    val rec_def_bind = rpair [] o Binding.conceal o Thm.def_binding o rec_bind;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1198
51739
3514b90d0a8b (co)rec is (just as the (un)fold) the unique morphism;
traytel
parents: 51551
diff changeset
  1199
    val rec_strs =
3514b90d0a8b (co)rec is (just as the (un)fold) the unique morphism;
traytel
parents: 51551
diff changeset
  1200
      map3 (fn ctor => fn prod_s => fn mapx =>
3514b90d0a8b (co)rec is (just as the (un)fold) the unique morphism;
traytel
parents: 51551
diff changeset
  1201
        mk_convol (HOLogic.mk_comp (ctor, Term.list_comb (mapx, passive_ids @ rec_fsts)), prod_s))
3514b90d0a8b (co)rec is (just as the (un)fold) the unique morphism;
traytel
parents: 51551
diff changeset
  1202
      ctors rec_ss rec_maps;
3514b90d0a8b (co)rec is (just as the (un)fold) the unique morphism;
traytel
parents: 51551
diff changeset
  1203
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1204
    fun rec_spec i T AT =
55204
345ee77213b5 use Local_Theory.define instead of Specification.definition for internal constants
traytel
parents: 55197
diff changeset
  1205
      fold_rev (Term.absfree o Term.dest_Free) rec_ss
345ee77213b5 use Local_Theory.define instead of Specification.definition for internal constants
traytel
parents: 55197
diff changeset
  1206
        (HOLogic.mk_comp (snd_const (HOLogic.mk_prodT (T, AT)), mk_fold Ts rec_strs i));
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1207
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1208
    val ((rec_frees, (_, rec_def_frees)), (lthy, lthy_old)) =
49311
blanchet
parents: 49308
diff changeset
  1209
      lthy
blanchet
parents: 49308
diff changeset
  1210
      |> fold_map3 (fn i => fn T => fn AT =>
55204
345ee77213b5 use Local_Theory.define instead of Specification.definition for internal constants
traytel
parents: 55197
diff changeset
  1211
        Local_Theory.define ((rec_bind i, NoSyn), (rec_def_bind i, rec_spec i T AT))) ks Ts activeAs
49311
blanchet
parents: 49308
diff changeset
  1212
      |>> apsnd split_list o split_list
blanchet
parents: 49308
diff changeset
  1213
      ||> `Local_Theory.restore;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1214
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1215
    val phi = Proof_Context.export_morphism lthy_old lthy;
49176
6d29d2db5f88 construct high-level iterator RHS
blanchet
parents: 49169
diff changeset
  1216
    val recs = map (Morphism.term phi) rec_frees;
6d29d2db5f88 construct high-level iterator RHS
blanchet
parents: 49169
diff changeset
  1217
    val rec_names = map (fst o dest_Const) recs;
6d29d2db5f88 construct high-level iterator RHS
blanchet
parents: 49169
diff changeset
  1218
    fun mk_rec ss i = Term.list_comb (Const (nth rec_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
  1219
      (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
  1220
    val rec_defs = map (fn def =>
345ee77213b5 use Local_Theory.define instead of Specification.definition for internal constants
traytel
parents: 55197
diff changeset
  1221
      mk_unabs_def n (Morphism.thm phi def RS meta_eq_to_obj_eq)) rec_def_frees;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1222
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1223
    val convols = map2 (fn T => fn i => mk_convol (HOLogic.id_const T, mk_rec rec_ss i)) Ts ks;
49504
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49502
diff changeset
  1224
    val ctor_rec_thms =
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1225
      let
49501
acc9635a644a renamed "fld"/"unf" to "ctor"/"dtor"
blanchet
parents: 49498
diff changeset
  1226
        fun mk_goal i rec_s rec_map ctor x =
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1227
          let
49501
acc9635a644a renamed "fld"/"unf" to "ctor"/"dtor"
blanchet
parents: 49498
diff changeset
  1228
            val lhs = mk_rec rec_ss i $ (ctor $ x);
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1229
            val rhs = rec_s $ (Term.list_comb (rec_map, passive_ids @ convols) $ x);
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1230
          in
49123
263b0e330d8b more work on sugar + simplify Trueprop + eq idiom everywhere
blanchet
parents: 49121
diff changeset
  1231
            fold_rev Logic.all (x :: rec_ss) (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
  1232
          end;
49501
acc9635a644a renamed "fld"/"unf" to "ctor"/"dtor"
blanchet
parents: 49498
diff changeset
  1233
        val goals = map5 mk_goal ks rec_ss rec_maps_rev ctors xFs;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1234
      in
49504
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49502
diff changeset
  1235
        map2 (fn goal => fn foldx =>
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
  1236
          Goal.prove_sorry lthy [] [] goal
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
  1237
            (fn {context = ctxt, prems = _} => mk_rec_tac ctxt rec_defs foldx fst_rec_pair_thms)
49109
0e5b859e1c91 no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
traytel
parents: 49074
diff changeset
  1238
          |> Thm.close_derivation)
49504
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49502
diff changeset
  1239
        goals ctor_fold_thms
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1240
      end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1241
51739
3514b90d0a8b (co)rec is (just as the (un)fold) the unique morphism;
traytel
parents: 51551
diff changeset
  1242
    val rec_unique_mor_thm =
3514b90d0a8b (co)rec is (just as the (un)fold) the unique morphism;
traytel
parents: 51551
diff changeset
  1243
      let
3514b90d0a8b (co)rec is (just as the (un)fold) the unique morphism;
traytel
parents: 51551
diff changeset
  1244
        val id_fs = map2 (fn T => fn f => mk_convol (HOLogic.id_const T, f)) Ts fs;
3514b90d0a8b (co)rec is (just as the (un)fold) the unique morphism;
traytel
parents: 51551
diff changeset
  1245
        val prem = HOLogic.mk_Trueprop (mk_mor UNIVs ctors rec_UNIVs rec_strs id_fs);
3514b90d0a8b (co)rec is (just as the (un)fold) the unique morphism;
traytel
parents: 51551
diff changeset