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