author | blanchet |
Fri, 21 Sep 2012 15:53:29 +0200 | |
changeset 49502 | 92a7c1842c78 |
parent 49463 | 83ac281bcdc2 |
child 49503 | dbbde075a42e |
permissions | -rw-r--r-- |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
1 |
(* Title: HOL/Codatatype/Tools/bnf_comp.ML |
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 |
49502 | 11 |
type unfold_set |
12 |
val empty_unfolds: unfold_set |
|
13 |
val map_unfolds_of: unfold_set -> thm list |
|
14 |
val set_unfoldss_of: unfold_set -> thm list list |
|
15 |
val pred_unfolds_of: unfold_set -> thm list |
|
16 |
val rel_unfolds_of: unfold_set -> thm list |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
17 |
|
49425 | 18 |
val bnf_of_typ: BNF_Def.const_policy -> (binding -> binding) -> |
49502 | 19 |
((string * sort) list list -> (string * sort) list) -> typ -> unfold_set * Proof.context -> |
20 |
(BNF_Def.BNF * (typ list * typ list)) * (unfold_set * Proof.context) |
|
49014 | 21 |
val default_comp_sort: (string * sort) list list -> (string * sort) list |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
22 |
val normalize_bnfs: (int -> binding -> binding) -> ''a list list -> ''a list -> |
49502 | 23 |
(''a list list -> ''a list) -> BNF_Def.BNF list -> unfold_set -> Proof.context -> |
24 |
(int list list * ''a list) * (BNF_Def.BNF list * (unfold_set * Proof.context)) |
|
25 |
val seal_bnf: unfold_set -> binding -> typ list -> BNF_Def.BNF -> Proof.context -> |
|
49185
073d7d1b7488
respect order of/additional type variables supplied by the user in fixed point constructions;
traytel
parents:
49155
diff
changeset
|
26 |
(BNF_Def.BNF * typ list) * local_theory |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
27 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
28 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
29 |
structure BNF_Comp : BNF_COMP = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
30 |
struct |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
31 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
32 |
open BNF_Def |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
33 |
open BNF_Util |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
34 |
open BNF_Tactics |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
35 |
open BNF_Comp_Tactics |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
36 |
|
49502 | 37 |
type unfold_set = { |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
38 |
map_unfolds: thm list, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
39 |
set_unfoldss: thm list list, |
49463 | 40 |
pred_unfolds: thm list, |
49456 | 41 |
rel_unfolds: thm list |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
42 |
}; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
43 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
44 |
fun add_to_thms thms NONE = thms |
49460
4dd451a075ce
fixed infinite loop with trivial rel_O_Gr + tuning
blanchet
parents:
49459
diff
changeset
|
45 |
| add_to_thms thms (SOME new) = thms |> not (Thm.is_reflexive new) ? insert Thm.eq_thm new; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
46 |
fun adds_to_thms thms NONE = thms |
49460
4dd451a075ce
fixed infinite loop with trivial rel_O_Gr + tuning
blanchet
parents:
49459
diff
changeset
|
47 |
| adds_to_thms thms (SOME news) = insert (eq_set Thm.eq_thm) (no_reflexive news) thms; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
48 |
|
49502 | 49 |
val empty_unfolds = {map_unfolds = [], set_unfoldss = [], pred_unfolds = [], rel_unfolds = []}; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
50 |
|
49502 | 51 |
fun add_to_unfolds_opt map_opt sets_opt pred_opt rel_opt |
49463 | 52 |
{map_unfolds, set_unfoldss, pred_unfolds, rel_unfolds} = |
53 |
{map_unfolds = add_to_thms map_unfolds map_opt, |
|
54 |
set_unfoldss = adds_to_thms set_unfoldss sets_opt, |
|
55 |
pred_unfolds = add_to_thms pred_unfolds pred_opt, |
|
56 |
rel_unfolds = add_to_thms rel_unfolds rel_opt}; |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
57 |
|
49502 | 58 |
fun add_to_unfolds map sets pred rel = |
59 |
add_to_unfolds_opt (SOME map) (SOME sets) (SOME pred) (SOME rel); |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
60 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
61 |
val map_unfolds_of = #map_unfolds; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
62 |
val set_unfoldss_of = #set_unfoldss; |
49463 | 63 |
val pred_unfolds_of = #pred_unfolds; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
64 |
val rel_unfolds_of = #rel_unfolds; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
65 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
66 |
val bdTN = "bdT"; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
67 |
|
49425 | 68 |
fun mk_killN n = "_kill" ^ string_of_int n; |
69 |
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
|
70 |
fun mk_permuteN src dest = |
49425 | 71 |
"_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
|
72 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
73 |
(*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
|
74 |
fun expand_term_const defs = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
75 |
let |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
76 |
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
|
77 |
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
|
78 |
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
|
79 |
|
49502 | 80 |
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
|
81 |
let |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
82 |
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
|
83 |
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
|
84 |
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
|
85 |
val inner = hd inners; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
86 |
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
|
87 |
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
|
88 |
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
|
89 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
90 |
(* 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
|
91 |
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
|
92 |
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
|
93 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
94 |
val (oDs, lthy1) = apfst (map TFree) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
95 |
(Variable.invent_types (replicate odead HOLogic.typeS) lthy); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
96 |
val (Dss, lthy2) = apfst (map (map TFree)) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
97 |
(fold_map Variable.invent_types (map (fn n => replicate n HOLogic.typeS) ideads) lthy1); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
98 |
val (Ass, lthy3) = apfst (replicate ilive o map TFree) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
99 |
(Variable.invent_types (replicate ilive HOLogic.typeS) lthy2); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
100 |
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
|
101 |
val Ass_repl = replicate olive As; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
102 |
val (Bs, _(*lthy4*)) = apfst (map TFree) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
103 |
(Variable.invent_types (replicate ilive HOLogic.typeS) lthy3); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
104 |
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
|
105 |
|
49463 | 106 |
val ((((fs', Qs'), Asets), xs), _(*names_lthy*)) = lthy |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
107 |
|> apfst snd o mk_Frees' "f" (map2 (curry (op -->)) As Bs) |
49463 | 108 |
||>> apfst snd o mk_Frees' "Q" (map2 mk_pred2T As Bs) |
49456 | 109 |
||>> 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
|
110 |
||>> mk_Frees "x" As; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
111 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
112 |
val CAs = map3 mk_T_of_bnf Dss Ass_repl inners; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
113 |
val CCA = mk_T_of_bnf oDs CAs outer; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
114 |
val CBs = map3 mk_T_of_bnf Dss Bss_repl inners; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
115 |
val outer_sets = mk_sets_of_bnf (replicate olive oDs) (replicate olive CAs) outer; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
116 |
val inner_setss = map3 mk_sets_of_bnf (map (replicate ilive) Dss) (replicate olive Ass) inners; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
117 |
val inner_bds = map3 mk_bd_of_bnf Dss Ass_repl inners; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
118 |
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
|
119 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
120 |
(*%f1 ... fn. outer.map (inner_1.map f1 ... fn) ... (inner_m.map f1 ... fn)*) |
49303 | 121 |
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
|
122 |
(Term.list_comb (mk_map_of_bnf oDs CAs CBs outer, |
49463 | 123 |
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
|
124 |
mk_map_of_bnf Ds As Bs) Dss inners)); |
49463 | 125 |
(*%Q1 ... Qn. outer.pred (inner_1.pred Q1 ... Qn) ... (inner_m.pred Q1 ... Qn)*) |
126 |
val pred = fold_rev Term.abs Qs' |
|
127 |
(Term.list_comb (mk_pred_of_bnf oDs CAs CBs outer, |
|
128 |
map2 (fn Ds => (fn f => Term.list_comb (f, map Bound (ilive - 1 downto 0))) o |
|
129 |
mk_pred_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
|
130 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
131 |
(*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
|
132 |
(*Union o collect {image inner_1.set_i o outer.set_1 ... image inner_m.set_i o outer.set_m}*) |
49303 | 133 |
fun mk_set i = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
134 |
let |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
135 |
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
|
136 |
val outer_set = mk_collect |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
137 |
(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
|
138 |
(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
|
139 |
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
|
140 |
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
|
141 |
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
|
142 |
val collect_image = mk_collect |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
143 |
(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
|
144 |
(CCA --> HOLogic.mk_setT T); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
145 |
in |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
146 |
(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
|
147 |
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
|
148 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
149 |
|
49303 | 150 |
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
|
151 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
152 |
(*(inner_1.bd +c ... +c inner_m.bd) *c outer.bd*) |
49303 | 153 |
val bd = Term.absdummy CCA (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
|
154 |
|
49303 | 155 |
fun map_id_tac {context = ctxt, ...} = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
156 |
let |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
157 |
(*order the theorems by reverse size to prevent bad interaction with nonconfluent rewrite |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
158 |
rules*) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
159 |
val thms = (map map_id_of_bnf inners |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
160 |
|> map (`(Term.size_of_term o Thm.prop_of)) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
161 |
|> sort (rev_order o int_ord o pairself fst) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
162 |
|> map snd) @ [map_id_of_bnf outer]; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
163 |
in |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
164 |
(EVERY' (map (fn thm => subst_tac ctxt [thm]) thms) THEN' rtac refl) 1 |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
165 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
166 |
|
49303 | 167 |
fun map_comp_tac _ = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
168 |
mk_comp_map_comp_tac (map_comp_of_bnf outer) (map_cong_of_bnf outer) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
169 |
(map map_comp_of_bnf inners); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
170 |
|
49303 | 171 |
fun mk_single_set_natural_tac i _ = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
172 |
mk_comp_set_natural_tac (map_comp_of_bnf outer) (map_cong_of_bnf outer) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
173 |
(collect_set_natural_of_bnf outer) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
174 |
(map ((fn thms => nth thms i) o set_natural_of_bnf) inners); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
175 |
|
49303 | 176 |
val set_natural_tacs = map mk_single_set_natural_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
|
177 |
|
49303 | 178 |
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
|
179 |
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
|
180 |
|
49303 | 181 |
fun bd_cinfinite_tac _ = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
182 |
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
|
183 |
|
49303 | 184 |
val set_alt_thms = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
185 |
if ! quick_and_dirty then |
49456 | 186 |
[] |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
187 |
else |
49109
0e5b859e1c91
no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
traytel
parents:
49019
diff
changeset
|
188 |
map (fn goal => |
0e5b859e1c91
no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
traytel
parents:
49019
diff
changeset
|
189 |
Skip_Proof.prove lthy [] [] goal |
0e5b859e1c91
no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
traytel
parents:
49019
diff
changeset
|
190 |
(fn {context, ...} => (mk_comp_set_alt_tac context (collect_set_natural_of_bnf outer))) |
0e5b859e1c91
no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
traytel
parents:
49019
diff
changeset
|
191 |
|> Thm.close_derivation) |
49303 | 192 |
(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
|
193 |
|
49303 | 194 |
fun map_cong_tac _ = |
195 |
mk_comp_map_cong_tac set_alt_thms (map_cong_of_bnf outer) (map map_cong_of_bnf inners); |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
196 |
|
49303 | 197 |
val set_bd_tacs = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
198 |
if ! quick_and_dirty then |
49303 | 199 |
replicate (length set_alt_thms) (K all_tac) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
200 |
else |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
201 |
let |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
202 |
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
|
203 |
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
|
204 |
val inner_bd_Card_orders = map bd_Card_order_of_bnf inners; |
49303 | 205 |
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
|
206 |
@{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
|
207 |
nth outer_set_bds j] |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
208 |
val single_set_bd_thmss = |
49303 | 209 |
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
|
210 |
in |
49303 | 211 |
map2 (fn set_alt => fn single_set_bds => fn {context, ...} => |
212 |
mk_comp_set_bd_tac context set_alt single_set_bds) |
|
213 |
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
|
214 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
215 |
|
49303 | 216 |
val in_alt_thm = |
49155
f51ab68f882f
do not trivialize important internal theorem in quick_and_dirty mode
traytel
parents:
49123
diff
changeset
|
217 |
let |
49303 | 218 |
val inx = mk_in Asets sets CCA; |
219 |
val in_alt = mk_in (map2 (mk_in Asets) inner_setss CAs) outer_sets CCA; |
|
220 |
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
|
221 |
in |
f51ab68f882f
do not trivialize important internal theorem in quick_and_dirty mode
traytel
parents:
49123
diff
changeset
|
222 |
Skip_Proof.prove lthy [] [] goal |
49303 | 223 |
(fn {context, ...} => mk_comp_in_alt_tac context set_alt_thms) |
49155
f51ab68f882f
do not trivialize important internal theorem in quick_and_dirty mode
traytel
parents:
49123
diff
changeset
|
224 |
|> Thm.close_derivation |
f51ab68f882f
do not trivialize important internal theorem in quick_and_dirty mode
traytel
parents:
49123
diff
changeset
|
225 |
end; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
226 |
|
49303 | 227 |
fun in_bd_tac _ = |
228 |
mk_comp_in_bd_tac in_alt_thm (map in_bd_of_bnf inners) (in_bd_of_bnf outer) |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
229 |
(map bd_Cinfinite_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
|
230 |
|
49303 | 231 |
fun map_wpull_tac _ = |
232 |
mk_map_wpull_tac in_alt_thm (map map_wpull_of_bnf inners) (map_wpull_of_bnf outer); |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
233 |
|
49456 | 234 |
fun rel_O_Gr_tac _ = |
235 |
let |
|
49463 | 236 |
val basic_thms = @{thms mem_Collect_eq fst_conv snd_conv}; (*TODO: tune*) |
49456 | 237 |
val outer_rel_Gr = rel_Gr_of_bnf outer RS sym; |
238 |
val outer_rel_cong = rel_cong_of_bnf outer; |
|
49463 | 239 |
val thm = |
240 |
(trans OF [in_alt_thm RS @{thm subst_rel_def}, |
|
241 |
trans OF [@{thm arg_cong2[of _ _ _ _ relcomp]} OF |
|
242 |
[trans OF [outer_rel_Gr RS @{thm arg_cong[of _ _ converse]}, |
|
243 |
rel_converse_of_bnf outer RS sym], outer_rel_Gr], |
|
244 |
trans OF [rel_O_of_bnf outer RS sym, outer_rel_cong OF |
|
245 |
(map (fn bnf => rel_O_Gr_of_bnf bnf RS sym) inners)]]] RS sym) |
|
246 |
|> unfold_defs lthy (basic_thms @ rel_def_of_bnf outer :: map rel_def_of_bnf inners); |
|
49456 | 247 |
in |
49463 | 248 |
unfold_defs_tac lthy basic_thms THEN rtac thm 1 |
249 |
end; |
|
49456 | 250 |
|
49460
4dd451a075ce
fixed infinite loop with trivial rel_O_Gr + tuning
blanchet
parents:
49459
diff
changeset
|
251 |
val tacs = zip_axioms map_id_tac map_comp_tac map_cong_tac set_natural_tacs bd_card_order_tac |
49456 | 252 |
bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac rel_O_Gr_tac; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
253 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
254 |
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
|
255 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
256 |
val inner_witss = map (map (fn (I, wit) => Term.list_comb (wit, map (nth xs) I))) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
257 |
(map3 (fn Ds => fn n => mk_wits_of_bnf (replicate n Ds) (replicate n As)) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
258 |
Dss inwitss inners); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
259 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
260 |
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
|
261 |
|
49303 | 262 |
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
|
263 |
|-> 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
|
264 |
|> flat |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
265 |
|> 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
|
266 |
|> minimize_wits |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
267 |
|> 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
|
268 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
269 |
fun wit_tac {context = ctxt, ...} = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
270 |
mk_comp_wit_tac ctxt (wit_thms_of_bnf outer) (collect_set_natural_of_bnf outer) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
271 |
(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
|
272 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
273 |
val (bnf', lthy') = |
49461
de07eecb2664
adapting "More_BNFs" to new relators/predicators
blanchet
parents:
49460
diff
changeset
|
274 |
bnf_def const_policy (K Derive_Few_Facts) qualify tacs wit_tac (SOME (oDs @ flat Dss)) |
49463 | 275 |
(((((b, mapx), sets), bd), wits), SOME pred) lthy; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
276 |
|
49502 | 277 |
val unfold_set' = |
278 |
add_to_unfolds (map_def_of_bnf bnf') (set_defs_of_bnf bnf') (pred_def_of_bnf bnf') |
|
279 |
(rel_def_of_bnf bnf') unfold_set; |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
280 |
in |
49502 | 281 |
(bnf', (unfold_set', lthy')) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
282 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
283 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
284 |
(* Killing live variables *) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
285 |
|
49502 | 286 |
fun kill_bnf qualify n bnf (unfold_set, lthy) = if n = 0 then (bnf, (unfold_set, lthy)) else |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
287 |
let |
49425 | 288 |
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
|
289 |
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
|
290 |
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
|
291 |
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
|
292 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
293 |
(* TODO: check 0 < n <= live *) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
294 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
295 |
val (Ds, lthy1) = apfst (map TFree) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
296 |
(Variable.invent_types (replicate dead HOLogic.typeS) lthy); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
297 |
val ((killedAs, As), lthy2) = apfst (`(take n) o map TFree) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
298 |
(Variable.invent_types (replicate live HOLogic.typeS) lthy1); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
299 |
val (Bs, _(*lthy3*)) = apfst (append killedAs o map TFree) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
300 |
(Variable.invent_types (replicate (live - n) HOLogic.typeS) lthy2); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
301 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
302 |
val ((Asets, lives), _(*names_lthy*)) = lthy |
49456 | 303 |
|> 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
|
304 |
||>> 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
|
305 |
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
|
306 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
307 |
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
|
308 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
309 |
(*bnf.map id ... id*) |
49303 | 310 |
val mapx = Term.list_comb (mk_map_of_bnf Ds As Bs bnf, map HOLogic.id_const killedAs); |
49463 | 311 |
(*bnf.pred (op =) ... (op =)*) |
312 |
val pred = Term.list_comb (mk_pred_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
|
313 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
314 |
val bnf_sets = mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf; |
49303 | 315 |
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
|
316 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
317 |
(*(|UNIV :: A1 set| +c ... +c |UNIV :: An set|) *c bnf.bd*) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
318 |
val bnf_bd = mk_bd_of_bnf Ds As bnf; |
49303 | 319 |
val bd = mk_cprod |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
320 |
(Library.foldr1 (uncurry mk_csum) (map (mk_card_of o HOLogic.mk_UNIV) killedAs)) bnf_bd; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
321 |
|
49303 | 322 |
fun map_id_tac _ = rtac (map_id_of_bnf bnf) 1; |
323 |
fun map_comp_tac {context, ...} = |
|
49463 | 324 |
unfold_defs_tac context ((map_comp_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
325 |
rtac refl 1; |
49303 | 326 |
fun map_cong_tac {context, ...} = |
49304 | 327 |
mk_kill_map_cong_tac context n (live - n) (map_cong_of_bnf bnf); |
49303 | 328 |
val set_natural_tacs = map (fn thm => fn _ => rtac thm 1) (drop n (set_natural_of_bnf bnf)); |
49304 | 329 |
fun bd_card_order_tac _ = mk_kill_bd_card_order_tac n (bd_card_order_of_bnf bnf); |
330 |
fun bd_cinfinite_tac _ = mk_kill_bd_cinfinite_tac (bd_Cinfinite_of_bnf bnf); |
|
49303 | 331 |
val set_bd_tacs = |
49304 | 332 |
map (fn thm => fn _ => mk_kill_set_bd_tac (bd_Card_order_of_bnf bnf) thm) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
333 |
(drop n (set_bd_of_bnf bnf)); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
334 |
|
49303 | 335 |
val in_alt_thm = |
49155
f51ab68f882f
do not trivialize important internal theorem in quick_and_dirty mode
traytel
parents:
49123
diff
changeset
|
336 |
let |
49303 | 337 |
val inx = mk_in Asets sets T; |
338 |
val in_alt = mk_in (map HOLogic.mk_UNIV killedAs @ Asets) bnf_sets T; |
|
339 |
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
|
340 |
in |
49304 | 341 |
Skip_Proof.prove 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
|
342 |
end; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
343 |
|
49303 | 344 |
fun in_bd_tac _ = |
49304 | 345 |
mk_kill_in_bd_tac n (live > n) in_alt_thm (in_bd_of_bnf bnf) (bd_Card_order_of_bnf bnf) |
49303 | 346 |
(bd_Cinfinite_of_bnf bnf) (bd_Cnotzero_of_bnf bnf); |
347 |
fun map_wpull_tac _ = mk_map_wpull_tac in_alt_thm [] (map_wpull_of_bnf bnf); |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
348 |
|
49456 | 349 |
fun rel_O_Gr_tac _ = |
350 |
let |
|
351 |
val rel_Gr = rel_Gr_of_bnf bnf RS sym |
|
49463 | 352 |
val thm = |
353 |
(trans OF [in_alt_thm RS @{thm subst_rel_def}, |
|
354 |
trans OF [@{thm arg_cong2[of _ _ _ _ relcomp]} OF |
|
355 |
[trans OF [rel_Gr RS @{thm arg_cong[of _ _ converse]}, |
|
356 |
rel_converse_of_bnf bnf RS sym], rel_Gr], |
|
357 |
trans OF [rel_O_of_bnf bnf RS sym, rel_cong_of_bnf bnf OF |
|
358 |
(replicate n @{thm trans[OF Gr_UNIV_id[OF refl] Id_alt[symmetric]]} @ |
|
359 |
replicate (live - n) @{thm Gr_fst_snd})]]] RS sym) |
|
360 |
|> unfold_defs lthy (rel_def_of_bnf bnf :: @{thms Id_def' mem_Collect_eq split_conv}); |
|
49456 | 361 |
in |
49463 | 362 |
rtac thm 1 |
49456 | 363 |
end; |
364 |
||
49460
4dd451a075ce
fixed infinite loop with trivial rel_O_Gr + tuning
blanchet
parents:
49459
diff
changeset
|
365 |
val tacs = zip_axioms map_id_tac map_comp_tac map_cong_tac set_natural_tacs bd_card_order_tac |
49456 | 366 |
bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac rel_O_Gr_tac; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
367 |
|
49303 | 368 |
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
|
369 |
|
49303 | 370 |
val wits = map (fn t => fold absfree (Term.add_frees t []) t) |
371 |
(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
|
372 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
373 |
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
|
374 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
375 |
val (bnf', lthy') = |
49461
de07eecb2664
adapting "More_BNFs" to new relators/predicators
blanchet
parents:
49460
diff
changeset
|
376 |
bnf_def Smart_Inline (K Derive_Few_Facts) qualify tacs wit_tac (SOME (killedAs @ Ds)) |
49463 | 377 |
(((((b, mapx), sets), Term.absdummy T bd), wits), SOME pred) lthy; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
378 |
|
49502 | 379 |
val unfold_set' = |
380 |
add_to_unfolds (map_def_of_bnf bnf') (set_defs_of_bnf bnf') (pred_def_of_bnf bnf') |
|
381 |
(rel_def_of_bnf bnf') unfold_set; |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
382 |
in |
49502 | 383 |
(bnf', (unfold_set', lthy')) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
384 |
end; |
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 |
(* Adding dummy live variables *) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
387 |
|
49502 | 388 |
fun lift_bnf qualify n bnf (unfold_set, lthy) = if n = 0 then (bnf, (unfold_set, lthy)) else |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
389 |
let |
49425 | 390 |
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
|
391 |
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
|
392 |
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
|
393 |
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
|
394 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
395 |
(* TODO: check 0 < n *) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
396 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
397 |
val (Ds, lthy1) = apfst (map TFree) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
398 |
(Variable.invent_types (replicate dead HOLogic.typeS) lthy); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
399 |
val ((newAs, As), lthy2) = apfst (chop n o map TFree) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
400 |
(Variable.invent_types (replicate (n + live) HOLogic.typeS) lthy1); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
401 |
val ((newBs, Bs), _(*lthy3*)) = apfst (chop n o map TFree) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
402 |
(Variable.invent_types (replicate (n + live) HOLogic.typeS) lthy2); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
403 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
404 |
val (Asets, _(*names_lthy*)) = lthy |
49456 | 405 |
|> 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
|
406 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
407 |
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
|
408 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
409 |
(*%f1 ... fn. bnf.map*) |
49303 | 410 |
val mapx = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
411 |
fold_rev Term.absdummy (map2 (curry (op -->)) newAs newBs) (mk_map_of_bnf Ds As Bs bnf); |
49463 | 412 |
(*%Q1 ... Qn. bnf.pred*) |
413 |
val pred = fold_rev Term.absdummy (map2 mk_pred2T newAs newBs) (mk_pred_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
|
414 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
415 |
val bnf_sets = mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf; |
49303 | 416 |
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
|
417 |
|
49303 | 418 |
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
|
419 |
|
49303 | 420 |
fun map_id_tac _ = rtac (map_id_of_bnf bnf) 1; |
421 |
fun map_comp_tac {context, ...} = |
|
49463 | 422 |
unfold_defs_tac context ((map_comp_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
423 |
rtac refl 1; |
49303 | 424 |
fun map_cong_tac {context, ...} = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
425 |
rtac (map_cong_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac context 1); |
49303 | 426 |
val set_natural_tacs = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
427 |
if ! quick_and_dirty then |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
428 |
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
|
429 |
else |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
430 |
replicate n (K empty_natural_tac) @ |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
431 |
map (fn thm => fn _ => rtac thm 1) (set_natural_of_bnf bnf); |
49303 | 432 |
fun bd_card_order_tac _ = rtac (bd_card_order_of_bnf bnf) 1; |
433 |
fun bd_cinfinite_tac _ = rtac (bd_cinfinite_of_bnf bnf) 1; |
|
434 |
val set_bd_tacs = |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
435 |
if ! quick_and_dirty then |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
436 |
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
|
437 |
else |
49304 | 438 |
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
|
439 |
(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
|
440 |
|
49303 | 441 |
val in_alt_thm = |
49155
f51ab68f882f
do not trivialize important internal theorem in quick_and_dirty mode
traytel
parents:
49123
diff
changeset
|
442 |
let |
49303 | 443 |
val inx = mk_in Asets sets T; |
444 |
val in_alt = mk_in (drop n Asets) bnf_sets T; |
|
445 |
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
|
446 |
in |
49304 | 447 |
Skip_Proof.prove 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
|
448 |
end; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
449 |
|
49304 | 450 |
fun in_bd_tac _ = mk_lift_in_bd_tac n in_alt_thm (in_bd_of_bnf bnf) (bd_Card_order_of_bnf bnf); |
49303 | 451 |
fun map_wpull_tac _ = mk_map_wpull_tac in_alt_thm [] (map_wpull_of_bnf bnf); |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
452 |
|
49456 | 453 |
fun rel_O_Gr_tac _ = |
49463 | 454 |
mk_simple_rel_O_Gr_tac lthy (rel_def_of_bnf bnf) (rel_O_Gr_of_bnf bnf) in_alt_thm; |
49456 | 455 |
|
49460
4dd451a075ce
fixed infinite loop with trivial rel_O_Gr + tuning
blanchet
parents:
49459
diff
changeset
|
456 |
val tacs = zip_axioms map_id_tac map_comp_tac map_cong_tac set_natural_tacs bd_card_order_tac |
49456 | 457 |
bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac rel_O_Gr_tac; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
458 |
|
49303 | 459 |
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
|
460 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
461 |
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
|
462 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
463 |
val (bnf', lthy') = |
49461
de07eecb2664
adapting "More_BNFs" to new relators/predicators
blanchet
parents:
49460
diff
changeset
|
464 |
bnf_def Smart_Inline (K Derive_Few_Facts) qualify tacs wit_tac (SOME Ds) |
49463 | 465 |
(((((b, mapx), sets), Term.absdummy T bd), wits), SOME pred) lthy; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
466 |
|
49502 | 467 |
val unfold_set' = |
468 |
add_to_unfolds (map_def_of_bnf bnf') (set_defs_of_bnf bnf') (pred_def_of_bnf bnf') |
|
469 |
(pred_def_of_bnf bnf') unfold_set; |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
470 |
in |
49502 | 471 |
(bnf', (unfold_set', lthy')) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
472 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
473 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
474 |
(* 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
|
475 |
|
49502 | 476 |
fun permute_bnf qualify src dest bnf (unfold_set, lthy) = |
477 |
if src = dest then (bnf, (unfold_set, lthy)) else |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
478 |
let |
49425 | 479 |
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
|
480 |
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
|
481 |
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
|
482 |
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
|
483 |
fun permute xs = mk_permute src dest xs; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
484 |
fun permute_rev xs = mk_permute dest src xs; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
485 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
486 |
val (Ds, lthy1) = apfst (map TFree) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
487 |
(Variable.invent_types (replicate dead HOLogic.typeS) lthy); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
488 |
val (As, lthy2) = apfst (map TFree) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
489 |
(Variable.invent_types (replicate live HOLogic.typeS) lthy1); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
490 |
val (Bs, _(*lthy3*)) = apfst (map TFree) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
491 |
(Variable.invent_types (replicate live HOLogic.typeS) lthy2); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
492 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
493 |
val (Asets, _(*names_lthy*)) = lthy |
49456 | 494 |
|> 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
|
495 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
496 |
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
|
497 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
498 |
(*%f(1) ... f(n). bnf.map f\<sigma>(1) ... f\<sigma>(n)*) |
49303 | 499 |
val mapx = fold_rev Term.absdummy (permute (map2 (curry op -->) As Bs)) |
49463 | 500 |
(Term.list_comb (mk_map_of_bnf Ds As Bs bnf, permute_rev (map Bound (live - 1 downto 0)))); |
501 |
(*%Q(1) ... Q(n). bnf.pred Q\<sigma>(1) ... Q\<sigma>(n)*) |
|
502 |
val pred = fold_rev Term.absdummy (permute (map2 mk_pred2T As Bs)) |
|
503 |
(Term.list_comb (mk_pred_of_bnf Ds As Bs bnf, permute_rev (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
|
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 = permute 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 |
|
49303 | 510 |
fun map_id_tac _ = rtac (map_id_of_bnf bnf) 1; |
511 |
fun map_comp_tac _ = rtac (map_comp_of_bnf bnf) 1; |
|
512 |
fun map_cong_tac {context, ...} = |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
513 |
rtac (map_cong_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac context 1); |
49303 | 514 |
val set_natural_tacs = permute (map (fn thm => fn _ => rtac thm 1) (set_natural_of_bnf bnf)); |
515 |
fun bd_card_order_tac _ = rtac (bd_card_order_of_bnf bnf) 1; |
|
516 |
fun bd_cinfinite_tac _ = rtac (bd_cinfinite_of_bnf bnf) 1; |
|
517 |
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
|
518 |
|
49303 | 519 |
val in_alt_thm = |
49155
f51ab68f882f
do not trivialize important internal theorem in quick_and_dirty mode
traytel
parents:
49123
diff
changeset
|
520 |
let |
49303 | 521 |
val inx = mk_in Asets sets T; |
522 |
val in_alt = mk_in (permute_rev Asets) bnf_sets T; |
|
523 |
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
|
524 |
in |
f51ab68f882f
do not trivialize important internal theorem in quick_and_dirty mode
traytel
parents:
49123
diff
changeset
|
525 |
Skip_Proof.prove lthy [] [] goal (K (mk_permute_in_alt_tac src dest)) |
f51ab68f882f
do not trivialize important internal theorem in quick_and_dirty mode
traytel
parents:
49123
diff
changeset
|
526 |
|> Thm.close_derivation |
f51ab68f882f
do not trivialize important internal theorem in quick_and_dirty mode
traytel
parents:
49123
diff
changeset
|
527 |
end; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
528 |
|
49303 | 529 |
fun in_bd_tac _ = |
530 |
mk_permute_in_bd_tac src dest in_alt_thm (in_bd_of_bnf bnf) (bd_Card_order_of_bnf bnf); |
|
531 |
fun map_wpull_tac _ = mk_map_wpull_tac in_alt_thm [] (map_wpull_of_bnf bnf); |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
532 |
|
49456 | 533 |
fun rel_O_Gr_tac _ = |
49463 | 534 |
mk_simple_rel_O_Gr_tac lthy (rel_def_of_bnf bnf) (rel_O_Gr_of_bnf bnf) in_alt_thm; |
49456 | 535 |
|
49460
4dd451a075ce
fixed infinite loop with trivial rel_O_Gr + tuning
blanchet
parents:
49459
diff
changeset
|
536 |
val tacs = zip_axioms map_id_tac map_comp_tac map_cong_tac set_natural_tacs bd_card_order_tac |
49456 | 537 |
bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac rel_O_Gr_tac; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
538 |
|
49303 | 539 |
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
|
540 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
541 |
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
|
542 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
543 |
val (bnf', lthy') = |
49461
de07eecb2664
adapting "More_BNFs" to new relators/predicators
blanchet
parents:
49460
diff
changeset
|
544 |
bnf_def Smart_Inline (K Derive_Few_Facts) qualify tacs wit_tac (SOME Ds) |
49463 | 545 |
(((((b, mapx), sets), Term.absdummy T bd), wits), SOME pred) lthy; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
546 |
|
49502 | 547 |
val unfold_set' = |
548 |
add_to_unfolds (map_def_of_bnf bnf') (set_defs_of_bnf bnf') (pred_def_of_bnf bnf') |
|
549 |
(pred_def_of_bnf bnf') unfold_set; |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
550 |
in |
49502 | 551 |
(bnf', (unfold_set', lthy')) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
552 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
553 |
|
49014 | 554 |
(* Composition pipeline *) |
555 |
||
556 |
fun permute_and_kill qualify n src dest bnf = |
|
557 |
bnf |
|
558 |
|> permute_bnf qualify src dest |
|
49304 | 559 |
#> uncurry (kill_bnf qualify n); |
49014 | 560 |
|
561 |
fun lift_and_permute qualify n src dest bnf = |
|
562 |
bnf |
|
49304 | 563 |
|> lift_bnf qualify n |
49014 | 564 |
#> uncurry (permute_bnf qualify src dest); |
565 |
||
49502 | 566 |
fun normalize_bnfs qualify Ass Ds sort bnfs unfold_set lthy = |
49014 | 567 |
let |
568 |
val before_kill_src = map (fn As => 0 upto (length As - 1)) Ass; |
|
569 |
val kill_poss = map (find_indices Ds) Ass; |
|
570 |
val live_poss = map2 (subtract (op =)) kill_poss before_kill_src; |
|
571 |
val before_kill_dest = map2 append kill_poss live_poss; |
|
572 |
val kill_ns = map length kill_poss; |
|
49502 | 573 |
val (inners', (unfold_set', lthy')) = |
49014 | 574 |
fold_map5 (fn i => permute_and_kill (qualify i)) |
575 |
(if length bnfs = 1 then [0] else (1 upto length bnfs)) |
|
49502 | 576 |
kill_ns before_kill_src before_kill_dest bnfs (unfold_set, lthy); |
49014 | 577 |
|
578 |
val Ass' = map2 (map o nth) Ass live_poss; |
|
579 |
val As = sort Ass'; |
|
580 |
val after_lift_dest = replicate (length Ass') (0 upto (length As - 1)); |
|
581 |
val old_poss = map (map (fn x => find_index (fn y => x = y) As)) Ass'; |
|
582 |
val new_poss = map2 (subtract (op =)) old_poss after_lift_dest; |
|
583 |
val after_lift_src = map2 append new_poss old_poss; |
|
584 |
val lift_ns = map (fn xs => length As - length xs) Ass'; |
|
585 |
in |
|
586 |
((kill_poss, As), fold_map5 (fn i => lift_and_permute (qualify i)) |
|
587 |
(if length bnfs = 1 then [0] else (1 upto length bnfs)) |
|
49502 | 588 |
lift_ns after_lift_src after_lift_dest inners' (unfold_set', lthy')) |
49014 | 589 |
end; |
590 |
||
591 |
fun default_comp_sort Ass = |
|
592 |
Library.sort (Term_Ord.typ_ord o pairself TFree) (fold (fold (insert (op =))) Ass []); |
|
593 |
||
49502 | 594 |
fun compose_bnf const_policy qualify sort outer inners oDs Dss tfreess (unfold_set, lthy) = |
49014 | 595 |
let |
49425 | 596 |
val b = name_of_bnf outer; |
49014 | 597 |
|
49121 | 598 |
val Ass = map (map Term.dest_TFree) tfreess; |
49014 | 599 |
val Ds = fold (fold Term.add_tfreesT) (oDs :: Dss) []; |
600 |
||
49502 | 601 |
val ((kill_poss, As), (inners', (unfold_set', lthy'))) = |
602 |
normalize_bnfs qualify Ass Ds sort inners unfold_set lthy; |
|
49014 | 603 |
|
604 |
val Ds = oDs @ flat (map3 (append oo map o nth) tfreess kill_poss Dss); |
|
605 |
val As = map TFree As; |
|
606 |
in |
|
49425 | 607 |
apfst (rpair (Ds, As)) |
49502 | 608 |
(clean_compose_bnf const_policy (qualify 0) b outer inners' (unfold_set', lthy')) |
49014 | 609 |
end; |
610 |
||
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
611 |
(* 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
|
612 |
|
49502 | 613 |
fun seal_bnf unfold_set b Ds bnf lthy = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
614 |
let |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
615 |
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
|
616 |
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
|
617 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
618 |
val (As, lthy1) = apfst (map TFree) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
619 |
(Variable.invent_types (replicate live HOLogic.typeS) (fold Variable.declare_typ Ds lthy)); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
620 |
val (Bs, _) = apfst (map TFree) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
621 |
(Variable.invent_types (replicate live HOLogic.typeS) lthy1); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
622 |
|
49502 | 623 |
val map_unfolds = map_unfolds_of unfold_set; |
624 |
val set_unfoldss = set_unfoldss_of unfold_set; |
|
625 |
val pred_unfolds = pred_unfolds_of unfold_set; |
|
626 |
val rel_unfolds = rel_unfolds_of unfold_set; |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
627 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
628 |
val expand_maps = fold expand_term_const (map (single o Logic.dest_equals o Thm.prop_of) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
629 |
map_unfolds); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
630 |
val expand_sets = fold expand_term_const (map (map (Logic.dest_equals o Thm.prop_of)) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
631 |
set_unfoldss); |
49463 | 632 |
val expand_preds = fold expand_term_const (map (single o Logic.dest_equals o Thm.prop_of) |
633 |
pred_unfolds); |
|
634 |
val unfold_maps = fold (unfold_defs lthy o single) map_unfolds; |
|
635 |
val unfold_sets = fold (unfold_defs lthy) set_unfoldss; |
|
636 |
val unfold_preds = unfold_defs lthy pred_unfolds; |
|
637 |
val unfold_rels = unfold_defs lthy rel_unfolds; |
|
638 |
val unfold_all = unfold_sets o unfold_maps o unfold_preds o unfold_rels; |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
639 |
val bnf_map = expand_maps (mk_map_of_bnf Ds As Bs bnf); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
640 |
val bnf_sets = map (expand_maps o expand_sets) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
641 |
(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
|
642 |
val bnf_bd = mk_bd_of_bnf Ds As bnf; |
49463 | 643 |
val bnf_pred = expand_preds (mk_pred_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
|
644 |
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
|
645 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
646 |
(*bd should only depend on dead type variables!*) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
647 |
val bd_repT = fst (dest_relT (fastype_of bnf_bd)); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
648 |
val bdT_bind = Binding.suffix_name ("_" ^ bdTN) b; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
649 |
val params = fold Term.add_tfreesT Ds []; |
49185
073d7d1b7488
respect order of/additional type variables supplied by the user in fixed point constructions;
traytel
parents:
49155
diff
changeset
|
650 |
val deads = map TFree params; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
651 |
|
49228 | 652 |
val ((bdT_name, (bdT_glob_info, bdT_loc_info)), lthy) = |
653 |
typedef false NONE (bdT_bind, params, NoSyn) |
|
654 |
(HOLogic.mk_UNIV bd_repT) NONE (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
|
655 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
656 |
val bnf_bd' = mk_dir_image bnf_bd |
49185
073d7d1b7488
respect order of/additional type variables supplied by the user in fixed point constructions;
traytel
parents:
49155
diff
changeset
|
657 |
(Const (#Abs_name bdT_glob_info, bd_repT --> Type (bdT_name, deads))) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
658 |
|
49228 | 659 |
val Abs_bdT_inj = mk_Abs_inj_thm (#Abs_inject bdT_loc_info); |
660 |
val Abs_bdT_bij = mk_Abs_bij_thm lthy Abs_bdT_inj (#Abs_cases bdT_loc_info); |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
661 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
662 |
val bd_ordIso = @{thm dir_image} OF [Abs_bdT_inj, bd_Card_order_of_bnf bnf]; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
663 |
val bd_card_order = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
664 |
@{thm card_order_dir_image} OF [Abs_bdT_bij, bd_card_order_of_bnf bnf]; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
665 |
val bd_cinfinite = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
666 |
(@{thm Cinfinite_cong} OF [bd_ordIso, bd_Cinfinite_of_bnf bnf]) RS conjunct1; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
667 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
668 |
val set_bds = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
669 |
map (fn thm => @{thm ordLeq_ordIso_trans} OF [thm, bd_ordIso]) (set_bd_of_bnf bnf); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
670 |
val in_bd = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
671 |
@{thm ordLeq_ordIso_trans} OF [in_bd_of_bnf bnf, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
672 |
@{thm cexp_cong2_Cnotzero} OF [bd_ordIso, if live = 0 then |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
673 |
@{thm ctwo_Cnotzero} else @{thm ctwo_Cnotzero} RS @{thm csum_Cnotzero2}, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
674 |
bd_Card_order_of_bnf bnf]]; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
675 |
|
49463 | 676 |
fun mk_tac thm {context = ctxt, prems = _} = |
677 |
(rtac (unfold_all thm) THEN' |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
678 |
SOLVE o REPEAT_DETERM o (atac ORELSE' Goal.assume_rule_tac ctxt)) 1; |
49456 | 679 |
|
49460
4dd451a075ce
fixed infinite loop with trivial rel_O_Gr + tuning
blanchet
parents:
49459
diff
changeset
|
680 |
val tacs = zip_axioms (mk_tac (map_id_of_bnf bnf)) (mk_tac (map_comp_of_bnf bnf)) |
49456 | 681 |
(mk_tac (map_cong_of_bnf bnf)) (map mk_tac (set_natural_of_bnf bnf)) |
682 |
(K (rtac bd_card_order 1)) (K (rtac bd_cinfinite 1)) (map mk_tac set_bds) (mk_tac in_bd) |
|
49463 | 683 |
(mk_tac (map_wpull_of_bnf bnf)) |
684 |
(mk_tac (unfold_defs lthy [rel_def_of_bnf bnf] (rel_O_Gr_of_bnf bnf))); |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
685 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
686 |
val bnf_wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
687 |
|
49463 | 688 |
fun wit_tac _ = mk_simple_wit_tac (map unfold_all (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
|
689 |
|
49435 | 690 |
val policy = user_policy Derive_All_Facts; |
691 |
||
692 |
val (bnf', lthy') = bnf_def Hardly_Inline policy I tacs wit_tac (SOME deads) |
|
49463 | 693 |
(((((b, bnf_map), bnf_sets), Term.absdummy T bnf_bd'), bnf_wits), SOME bnf_pred) lthy; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
694 |
in |
49456 | 695 |
((bnf', deads), lthy') |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
696 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
697 |
|
49450 | 698 |
val ID_bnf = the (bnf_of @{context} "Basic_BNFs.ID"); |
699 |
val DEADID_bnf = the (bnf_of @{context} "Basic_BNFs.DEADID"); |
|
700 |
||
49456 | 701 |
fun bnf_of_typ _ _ _ (T as TFree _) accum = ((ID_bnf, ([], [T])), accum) |
49425 | 702 |
| bnf_of_typ _ _ _ (TVar _) _ = error "Unexpected schematic variable" |
49502 | 703 |
| bnf_of_typ const_policy qualify' sort (T as Type (C, Ts)) (unfold_set, lthy) = |
49186
4b5fa9d5e330
handle type constructors not known to be a BNF using the DEADID BNF
traytel
parents:
49185
diff
changeset
|
704 |
let |
4b5fa9d5e330
handle type constructors not known to be a BNF using the DEADID BNF
traytel
parents:
49185
diff
changeset
|
705 |
val tfrees = Term.add_tfreesT T []; |
49236 | 706 |
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
|
707 |
in |
49186
4b5fa9d5e330
handle type constructors not known to be a BNF using the DEADID BNF
traytel
parents:
49185
diff
changeset
|
708 |
(case bnf_opt of |
49502 | 709 |
NONE => ((DEADID_bnf, ([T], [])), (unfold_set, lthy)) |
49186
4b5fa9d5e330
handle type constructors not known to be a BNF using the DEADID BNF
traytel
parents:
49185
diff
changeset
|
710 |
| SOME bnf => |
4b5fa9d5e330
handle type constructors not known to be a BNF using the DEADID BNF
traytel
parents:
49185
diff
changeset
|
711 |
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
|
712 |
let |
4b5fa9d5e330
handle type constructors not known to be a BNF using the DEADID BNF
traytel
parents:
49185
diff
changeset
|
713 |
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
|
714 |
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
|
715 |
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
|
716 |
val tvars' = Term.add_tvarsT T' []; |
4b5fa9d5e330
handle type constructors not known to be a BNF using the DEADID BNF
traytel
parents:
49185
diff
changeset
|
717 |
val deads_lives = |
4b5fa9d5e330
handle type constructors not known to be a BNF using the DEADID BNF
traytel
parents:
49185
diff
changeset
|
718 |
pairself (map (Term.typ_subst_TVars (map fst tvars' ~~ map TFree tfrees))) |
4b5fa9d5e330
handle type constructors not known to be a BNF using the DEADID BNF
traytel
parents:
49185
diff
changeset
|
719 |
(deads, lives); |
49502 | 720 |
in ((bnf, deads_lives), (unfold_set, lthy)) end |
49186
4b5fa9d5e330
handle type constructors not known to be a BNF using the DEADID BNF
traytel
parents:
49185
diff
changeset
|
721 |
else |
4b5fa9d5e330
handle type constructors not known to be a BNF using the DEADID BNF
traytel
parents:
49185
diff
changeset
|
722 |
let |
49425 | 723 |
val name = Long_Name.base_name C; |
724 |
fun qualify i = |
|
725 |
let val namei = name ^ nonzero_string_of_int i; |
|
726 |
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
|
727 |
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
|
728 |
val olive = live_of_bnf bnf; |
4b5fa9d5e330
handle type constructors not known to be a BNF using the DEADID BNF
traytel
parents:
49185
diff
changeset
|
729 |
val oDs_pos = find_indices [TFree ("dead", [])] (snd (Term.dest_Type |
4b5fa9d5e330
handle type constructors not known to be a BNF using the DEADID BNF
traytel
parents:
49185
diff
changeset
|
730 |
(mk_T_of_bnf (replicate odead (TFree ("dead", []))) (replicate olive dummyT) bnf))); |
4b5fa9d5e330
handle type constructors not known to be a BNF using the DEADID BNF
traytel
parents:
49185
diff
changeset
|
731 |
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
|
732 |
val Ts' = map (nth Ts) (subtract (op =) oDs_pos (0 upto length Ts - 1)); |
49502 | 733 |
val ((inners, (Dss, Ass)), (unfold_set', lthy')) = |
49186
4b5fa9d5e330
handle type constructors not known to be a BNF using the DEADID BNF
traytel
parents:
49185
diff
changeset
|
734 |
apfst (apsnd split_list o split_list) |
49425 | 735 |
(fold_map2 (fn i => bnf_of_typ Smart_Inline (qualify i) sort) |
49502 | 736 |
(if length Ts' = 1 then [0] else (1 upto length Ts')) Ts' (unfold_set, lthy)); |
49186
4b5fa9d5e330
handle type constructors not known to be a BNF using the DEADID BNF
traytel
parents:
49185
diff
changeset
|
737 |
in |
49502 | 738 |
compose_bnf const_policy qualify sort bnf inners oDs Dss Ass (unfold_set', lthy') |
49186
4b5fa9d5e330
handle type constructors not known to be a BNF using the DEADID BNF
traytel
parents:
49185
diff
changeset
|
739 |
end) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
740 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
741 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
742 |
end; |