author | wenzelm |
Fri, 14 Aug 2020 14:40:24 +0200 | |
changeset 72154 | 2b41b710f6ef |
parent 71558 | 1cf958713cf7 |
child 72450 | 24bd1316eaae |
permissions | -rw-r--r-- |
60918 | 1 |
(* Title: HOL/Tools/BNF/bnf_lift.ML |
2 |
Author: Julian Biendarra, TU Muenchen |
|
71262 | 3 |
Author: Basil Fürer, ETH Zurich |
4 |
Author: Joshua Schneider, ETH Zurich |
|
60918 | 5 |
Author: Dmitriy Traytel, ETH Zurich |
71262 | 6 |
Copyright 2015, 2019 |
60918 | 7 |
|
8 |
Lifting of BNFs through typedefs. |
|
9 |
*) |
|
10 |
||
61067 | 11 |
signature BNF_LIFT = |
12 |
sig |
|
13 |
datatype lift_bnf_option = |
|
14 |
Plugins_Option of Proof.context -> Plugin_Name.filter |
|
15 |
| No_Warn_Wits |
|
71262 | 16 |
| No_Warn_Transfer |
60918 | 17 |
val copy_bnf: |
18 |
(((lift_bnf_option list * (binding option * (string * sort option)) list) * |
|
62324 | 19 |
string) * thm option) * (binding * binding * binding) -> |
60918 | 20 |
local_theory -> local_theory |
21 |
val copy_bnf_cmd: |
|
22 |
(((lift_bnf_option list * (binding option * (string * string option)) list) * |
|
62324 | 23 |
string) * (Facts.ref * Token.src list) option) * (binding * binding * binding) -> |
60918 | 24 |
local_theory -> local_theory |
25 |
val lift_bnf: |
|
62777 | 26 |
((((lift_bnf_option list * (binding option * (string * sort option)) list) * |
71494 | 27 |
string) * term list option) * thm list option) * (binding * binding * binding) -> |
60918 | 28 |
({context: Proof.context, prems: thm list} -> tactic) list -> |
29 |
local_theory -> local_theory |
|
30 |
val lift_bnf_cmd: |
|
31 |
((((lift_bnf_option list * (binding option * (string * string option)) list) * |
|
71494 | 32 |
string) * string list) * (Facts.ref * Token.src list) list option) * |
62324 | 33 |
(binding * binding * binding) -> local_theory -> Proof.state |
61067 | 34 |
end |
60918 | 35 |
|
61067 | 36 |
structure BNF_Lift : BNF_LIFT = |
37 |
struct |
|
60918 | 38 |
|
39 |
open Ctr_Sugar_Tactics |
|
40 |
open BNF_Util |
|
41 |
open BNF_Comp |
|
42 |
open BNF_Def |
|
43 |
||
61067 | 44 |
|
45 |
datatype lift_bnf_option = |
|
46 |
Plugins_Option of Proof.context -> Plugin_Name.filter |
|
71262 | 47 |
| No_Warn_Wits |
48 |
| No_Warn_Transfer; |
|
49 |
||
71494 | 50 |
datatype equiv_thm = Typedef | Quotient of thm |
71262 | 51 |
|
52 |
(** Util **) |
|
53 |
||
54 |
fun last2 [x, y] = ([], (x, y)) |
|
55 |
| last2 (x :: xs) = last2 xs |>> (fn y => x :: y) |
|
56 |
| last2 [] = raise Match; |
|
57 |
||
58 |
fun strip3 thm = (case Term.strip_comb (HOLogic.dest_Trueprop (Thm.prop_of thm)) of |
|
59 |
(_, [x1, x2, x3]) => (x1, x2, x3) |
|
60 |
| _ => error "strip3: wrong number of arguments"); |
|
61 |
||
62 |
val mk_Free = yield_singleton o mk_Frees; |
|
63 |
||
64 |
fun TWICE t = t THEN' t; |
|
65 |
||
66 |
fun prove lthy fvars tm tac = |
|
67 |
Goal.prove_sorry lthy (map (fst o dest_Free) fvars) [] tm (fn {context, ...} => tac context); |
|
68 |
||
69 |
(** Term construction **) |
|
70 |
||
71 |
fun mk_relT aT bT = aT --> bT --> HOLogic.boolT; |
|
72 |
fun mk_relcompp r s = let |
|
73 |
val (rT, sT) = apply2 fastype_of (r, s); |
|
74 |
val ((xT, _), (_, zTs)) = apply2 dest_funT (rT, sT); |
|
75 |
val T = rT --> sT --> mk_relT xT (fst (dest_funT zTs)); |
|
76 |
in Const (@{const_name relcompp}, T) $ r $ s end; |
|
77 |
val mk_OO = fold_rev mk_relcompp; |
|
78 |
||
79 |
(* option from sum *) |
|
80 |
fun mk_MaybeT T = mk_sumT (HOLogic.unitT, T); |
|
81 |
fun mk_Nothing T = BNF_FP_Util.mk_Inl T HOLogic.unit; |
|
82 |
val Just_const = BNF_FP_Util.Inr_const HOLogic.unitT; |
|
83 |
fun mk_Just tm = Just_const (fastype_of tm) $ tm; |
|
84 |
fun Maybe_map_const T = |
|
85 |
let val (xT, yT) = dest_funT T in |
|
86 |
Const (@{const_name map_sum}, (HOLogic.unitT --> HOLogic.unitT) --> T --> mk_MaybeT xT --> mk_MaybeT yT) $ |
|
87 |
HOLogic.id_const HOLogic.unitT |
|
88 |
end; |
|
89 |
fun mk_Maybe_map tm = Maybe_map_const (fastype_of tm) $ tm; |
|
90 |
fun fromJust_const T = Const (@{const_name sum.projr}, mk_MaybeT T --> T) |
|
91 |
||
92 |
fun rel_Maybe_const T U = |
|
93 |
Const (@{const_name rel_sum}, (HOLogic.unitT --> HOLogic.unitT --> HOLogic.boolT) --> |
|
94 |
(T --> U --> HOLogic.boolT) --> mk_MaybeT T --> mk_MaybeT U --> HOLogic.boolT) $ |
|
95 |
HOLogic.eq_const HOLogic.unitT |
|
96 |
fun set_Maybe_const T = Const (@{const_name Basic_BNFs.setr}, mk_MaybeT T --> HOLogic.mk_setT T) |
|
97 |
||
98 |
fun Inf_const T = Const (@{const_name Inf}, HOLogic.mk_setT T --> T); |
|
99 |
||
100 |
fun Image_const T = |
|
101 |
let |
|
102 |
val relT = HOLogic.mk_setT (HOLogic.mk_prodT (T, T)); |
|
103 |
val setT = HOLogic.mk_setT T; |
|
104 |
in Const (@{const_name Image}, relT --> setT --> setT) end; |
|
105 |
||
106 |
fun bot_const T = Const (@{const_name bot}, T); |
|
107 |
||
108 |
fun mk_insert x S = |
|
109 |
Const (@{const_name Set.insert}, fastype_of x --> fastype_of S --> fastype_of S) $ x $ S; |
|
110 |
||
111 |
fun mk_vimage f s = |
|
112 |
let val (xT, yT) = dest_funT (fastype_of f) in |
|
113 |
Const (@{const_name vimage}, (xT --> yT) --> HOLogic.mk_setT yT --> HOLogic.mk_setT xT) $ f $ s |
|
114 |
end; |
|
115 |
||
116 |
fun mk_case_prod (x, y) tm = let |
|
117 |
val ((x, xT), (y, yT)) = apply2 dest_Free (x, y); |
|
118 |
val prodT = HOLogic.mk_prodT (xT, yT); |
|
119 |
in HOLogic.Collect_const prodT $ (Const (@{const_name case_prod}, |
|
120 |
(xT --> yT --> HOLogic.boolT) --> prodT --> HOLogic.boolT) $ absfree (x, xT) |
|
121 |
(absfree (y, yT) tm)) end; |
|
122 |
||
123 |
fun mk_Trueprop_implies (ps, c) = |
|
124 |
Logic.list_implies (map HOLogic.mk_Trueprop ps, HOLogic.mk_Trueprop c); |
|
125 |
||
126 |
fun mk_Collect (v, tm) = let val (n, T) = dest_Free v in |
|
127 |
HOLogic.mk_Collect (n, T, tm) end; |
|
128 |
||
129 |
||
130 |
(** witnesses **) |
|
131 |
fun prepare_wits is_quotient RepT wits opts alphas wits_F var_as var_as' sets lthy = |
|
132 |
let |
|
133 |
fun binder_types_until_eq V T = |
|
134 |
let |
|
135 |
fun strip (TU as Type ("fun", [T, U])) = if V = TU then [] else T :: strip U |
|
136 |
| strip T = if V = T then [] else |
|
137 |
error ("Bad type for witness: " ^ quote (Syntax.string_of_typ lthy T)); |
|
138 |
in strip T end; |
|
139 |
||
140 |
val Iwits = the_default wits_F (Option.map (map (`(map (fn T => |
|
141 |
find_index (fn U => T = U) alphas) o binder_types_until_eq RepT o fastype_of))) wits); |
|
142 |
||
71469
d7ef73df3d15
lift BNF witnesses for quotients (unless better ones are specified by the user)
traytel
parents:
71393
diff
changeset
|
143 |
val Iwits = if is_quotient then |
d7ef73df3d15
lift BNF witnesses for quotients (unless better ones are specified by the user)
traytel
parents:
71393
diff
changeset
|
144 |
let |
d7ef73df3d15
lift BNF witnesses for quotients (unless better ones are specified by the user)
traytel
parents:
71393
diff
changeset
|
145 |
val subsumed_Iwits = |
d7ef73df3d15
lift BNF witnesses for quotients (unless better ones are specified by the user)
traytel
parents:
71393
diff
changeset
|
146 |
filter (fn (J, _) => exists (fn (I, _) => subset (op =) (I, J)) wits_F) Iwits; |
d7ef73df3d15
lift BNF witnesses for quotients (unless better ones are specified by the user)
traytel
parents:
71393
diff
changeset
|
147 |
val _ = if null subsumed_Iwits orelse exists (fn No_Warn_Wits => true | _ => false) opts |
d7ef73df3d15
lift BNF witnesses for quotients (unless better ones are specified by the user)
traytel
parents:
71393
diff
changeset
|
148 |
then () |
d7ef73df3d15
lift BNF witnesses for quotients (unless better ones are specified by the user)
traytel
parents:
71393
diff
changeset
|
149 |
else |
d7ef73df3d15
lift BNF witnesses for quotients (unless better ones are specified by the user)
traytel
parents:
71393
diff
changeset
|
150 |
let |
d7ef73df3d15
lift BNF witnesses for quotients (unless better ones are specified by the user)
traytel
parents:
71393
diff
changeset
|
151 |
val (suffix1, suffix2, be) = |
d7ef73df3d15
lift BNF witnesses for quotients (unless better ones are specified by the user)
traytel
parents:
71393
diff
changeset
|
152 |
(if length subsumed_Iwits = 1 then ("", "", "is") else ("s", "es", "are")) |
d7ef73df3d15
lift BNF witnesses for quotients (unless better ones are specified by the user)
traytel
parents:
71393
diff
changeset
|
153 |
in |
d7ef73df3d15
lift BNF witnesses for quotients (unless better ones are specified by the user)
traytel
parents:
71393
diff
changeset
|
154 |
subsumed_Iwits |
d7ef73df3d15
lift BNF witnesses for quotients (unless better ones are specified by the user)
traytel
parents:
71393
diff
changeset
|
155 |
|> map (Syntax.pretty_typ lthy o fastype_of o snd) |
d7ef73df3d15
lift BNF witnesses for quotients (unless better ones are specified by the user)
traytel
parents:
71393
diff
changeset
|
156 |
|> Pretty.big_list |
d7ef73df3d15
lift BNF witnesses for quotients (unless better ones are specified by the user)
traytel
parents:
71393
diff
changeset
|
157 |
("The following type" ^ suffix1 ^ " of nonemptiness witness" ^ suffix2 ^ |
d7ef73df3d15
lift BNF witnesses for quotients (unless better ones are specified by the user)
traytel
parents:
71393
diff
changeset
|
158 |
" of the raw type's BNF " ^ be ^ " subsumed by the existing raw witnesses:") |
d7ef73df3d15
lift BNF witnesses for quotients (unless better ones are specified by the user)
traytel
parents:
71393
diff
changeset
|
159 |
|> (fn pt => Pretty.chunks [pt, |
d7ef73df3d15
lift BNF witnesses for quotients (unless better ones are specified by the user)
traytel
parents:
71393
diff
changeset
|
160 |
Pretty.para ("You do not need to lift these subsumed witnesses.")]) |
d7ef73df3d15
lift BNF witnesses for quotients (unless better ones are specified by the user)
traytel
parents:
71393
diff
changeset
|
161 |
|> Pretty.string_of |
d7ef73df3d15
lift BNF witnesses for quotients (unless better ones are specified by the user)
traytel
parents:
71393
diff
changeset
|
162 |
|> warning |
d7ef73df3d15
lift BNF witnesses for quotients (unless better ones are specified by the user)
traytel
parents:
71393
diff
changeset
|
163 |
end; |
d7ef73df3d15
lift BNF witnesses for quotients (unless better ones are specified by the user)
traytel
parents:
71393
diff
changeset
|
164 |
in |
d7ef73df3d15
lift BNF witnesses for quotients (unless better ones are specified by the user)
traytel
parents:
71393
diff
changeset
|
165 |
filter_out (fn (J, _) => exists (fn (I, _) => subset (op =) (I, J)) wits_F) Iwits |
d7ef73df3d15
lift BNF witnesses for quotients (unless better ones are specified by the user)
traytel
parents:
71393
diff
changeset
|
166 |
end |
d7ef73df3d15
lift BNF witnesses for quotients (unless better ones are specified by the user)
traytel
parents:
71393
diff
changeset
|
167 |
else Iwits; |
d7ef73df3d15
lift BNF witnesses for quotients (unless better ones are specified by the user)
traytel
parents:
71393
diff
changeset
|
168 |
|
71262 | 169 |
val wit_goals = maps (BNF_Def.mk_wit_goals var_as var_as' sets) Iwits; |
170 |
||
71469
d7ef73df3d15
lift BNF witnesses for quotients (unless better ones are specified by the user)
traytel
parents:
71393
diff
changeset
|
171 |
val lost_wits = if is_quotient then [] else |
d7ef73df3d15
lift BNF witnesses for quotients (unless better ones are specified by the user)
traytel
parents:
71393
diff
changeset
|
172 |
filter_out (fn (J, _) => exists (fn (I, _) => subset (op =) (I, J)) Iwits) wits_F; |
71262 | 173 |
|
174 |
val _ = |
|
175 |
if null lost_wits orelse exists (fn No_Warn_Wits => true | _ => false) opts then () |
|
176 |
else |
|
177 |
let |
|
178 |
val what = (if is_quotient then "quotient type" else "typedef"); |
|
179 |
val (suffix1, suffix2, be) = |
|
180 |
(if length lost_wits = 1 then ("", "", "was") else ("s", "es", "were")) |
|
181 |
in |
|
182 |
lost_wits |
|
183 |
|> map (Syntax.pretty_typ lthy o fastype_of o snd) |
|
184 |
|> Pretty.big_list |
|
185 |
("The following type" ^ suffix1 ^ " of nonemptiness witness" ^ suffix2 ^ |
|
186 |
" of the raw type's BNF " ^ be ^ " lost:") |
|
187 |
|> (fn pt => Pretty.chunks [pt, |
|
188 |
Pretty.para ("You can specify a liftable witness (e.g., a term of one of the above types\ |
|
189 |
\ that satisfies the " ^ what ^ "'s invariant)\ |
|
190 |
\ using the annotation [wits: <term>].")]) |
|
191 |
|> Pretty.string_of |
|
192 |
|> warning |
|
193 |
end; |
|
194 |
in (Iwits, wit_goals) end; |
|
195 |
||
196 |
||
197 |
(** transfer theorems **) |
|
198 |
||
199 |
fun mk_transfer_thms' bnf_F bnf_G name consts Tss crel_def pcrel_def defs lthy = let |
|
200 |
||
201 |
val live = length (#alphas Tss); |
|
202 |
||
203 |
val (pcrel_tm, crel_tm) = apply2 (Thm.prop_of #> Logic.dest_equals #> fst #> head_of) |
|
204 |
(pcrel_def, crel_def); |
|
205 |
||
206 |
val (var_Qs, var_Rs) = fold Variable.declare_typ (#alphas Tss @ #deads Tss) lthy |
|
207 |
|> mk_Frees "Q" (map2 mk_relT (#alphas Tss) (#betas Tss)) |
|
208 |
||>> mk_Frees "R" (map2 mk_relT (#gammas Tss) (#deltas Tss)) |
|
209 |
|> fst; |
|
210 |
||
211 |
(* get the "pcrel :: args_raw => rep => abs \<Rightarrow> bool" term and instantiate types *) |
|
212 |
val (args_raw, (rep, abs)) = pcrel_tm |
|
213 |
|> fastype_of |
|
214 |
|> binder_types |
|
215 |
|> last2; |
|
216 |
val thy = Proof_Context.theory_of lthy; |
|
217 |
val tyenv_match = Vartab.empty |
|
218 |
|> Sign.typ_match thy ((rep, #rep Tss)) |
|
219 |
|> Sign.typ_match thy ((abs, #abs Tss)); |
|
220 |
val args = map (Envir.subst_type tyenv_match) args_raw; |
|
221 |
val (pcrel_a, pcrel_b) = Envir.subst_term (tyenv_match, Vartab.empty) pcrel_tm |
|
222 |
|> `(subst_atomic_types (#alphas Tss @ #betas Tss ~~ #gammas Tss @ #deltas Tss)); |
|
223 |
||
224 |
(* match "crel :: {?a F} \<Rightarrow> a G" with "rep_G :: {a F}" *) |
|
225 |
val tyenv_match = Vartab.empty |> Sign.typ_match thy |
|
226 |
(crel_tm |> fastype_of |> binder_types |> hd, #rep Tss); |
|
227 |
val crel_b = Envir.subst_term (tyenv_match, Vartab.empty) crel_tm |
|
228 |
|> subst_atomic_types (#alphas Tss ~~ #betas Tss) |
|
229 |
val crel_d = subst_atomic_types (#betas Tss ~~ #deltas Tss) crel_b; |
|
230 |
||
231 |
(* instantiate pcrel with Qs and Rs*) |
|
232 |
val dead_args = map binder_types args |
|
233 |
|> map (fn [T,U] => if T = U then SOME T else NONE | _ => NONE); |
|
234 |
val parametrize = let |
|
235 |
fun go (SOME T :: dTs) tms = HOLogic.eq_const T :: go dTs tms |
|
236 |
| go (_ :: dTs) (tm :: tms) = tm :: go dTs tms |
|
237 |
| go (_ :: dTs) tms = go dTs tms |
|
238 |
| go _ _ = []; |
|
239 |
in go dead_args end; |
|
240 |
||
241 |
val pcrel_Qs = list_comb (pcrel_b, parametrize var_Qs); |
|
242 |
val pcrel_Rs = list_comb (pcrel_a, parametrize var_Rs); |
|
243 |
||
244 |
(* get the order of the dead variables right *) |
|
245 |
val Ds0 = maps the_list dead_args; |
|
246 |
val permute_Ds = (mk_T_of_bnf Ds0 (#betas Tss) bnf_G, nth (binder_types (type_of pcrel_Qs)) 1) |
|
247 |
|> apply2 (fn Type (_, Ts) => Ts | _ => []) |> op~~ |> typ_subst_atomic; |
|
248 |
val Ds0 = map permute_Ds Ds0; |
|
249 |
||
250 |
(* terms for sets of the set_transfer thms *) |
|
251 |
val rel_sets_Q = @{map 3} (fn aT => fn bT => fn Q => |
|
252 |
mk_rel 1 [aT] [bT] @{term rel_set} $ Q) (#alphas Tss) (#betas Tss) var_Qs; |
|
253 |
||
254 |
(* rewrite rules for pcrel and BNF's relator: "pcrel Q = rel_F OO crel" *) |
|
255 |
fun mk_pcr_rel_F_eq Ts Us pcrel vs crel = |
|
256 |
let |
|
257 |
val thm = HOLogic.mk_Trueprop (HOLogic.mk_eq (pcrel, mk_relcompp (list_comb |
|
258 |
(mk_rel_of_bnf (#deads Tss) (Ts Tss) (Us Tss) bnf_F, vs)) crel)); |
|
259 |
fun tac ctxt = unfold_thms_tac ctxt (pcrel_def :: defs @ @{thm id_bnf_apply} :: |
|
260 |
Transfer.get_relator_eq ctxt) THEN (HEADGOAL (rtac ctxt refl)) |
|
261 |
in prove lthy vs thm tac |> mk_abs_def end; |
|
262 |
||
263 |
val pcr_rel_F_eqs = |
|
264 |
[mk_pcr_rel_F_eq #alphas #betas pcrel_Qs var_Qs crel_b, |
|
265 |
mk_pcr_rel_F_eq #gammas #deltas pcrel_Rs var_Rs crel_d]; |
|
266 |
||
267 |
(* create transfer-relations from term('s type) *) |
|
268 |
fun mk_transfer_rel' i tm = |
|
269 |
let |
|
270 |
fun go T' (n, q) = case T' of |
|
271 |
Type ("fun", [T as Type ("fun", _), U]) => |
|
272 |
go U (n+1, q) |>> mk_rel_fun (fst (go T (n, q))) |
|
273 |
| Type ("fun", [T, U]) => |
|
274 |
go T (n, q) |-> (fn x => fn st => go U st |>> mk_rel_fun x) |
|
275 |
| Type (@{type_name bool}, _) => (HOLogic.eq_const HOLogic.boolT, (n, q)) |
|
276 |
| Type (@{type_name set}, _) => (nth rel_sets_Q n, (n, q)) |
|
277 |
| Type _ => (if q then pcrel_Qs else pcrel_Rs, (n, not q)) |
|
278 |
| TFree _ => (nth (if q then var_Qs else var_Rs) n, (n, not q)) |
|
279 |
| _ => raise Match |
|
280 |
in go (fastype_of tm) (i, true) |> fst end; |
|
281 |
||
282 |
(* prove transfer rules *) |
|
283 |
fun prove_transfer_thm' i vars new_tm const = |
|
284 |
let |
|
285 |
val tm = HOLogic.mk_Trueprop (mk_transfer_rel' i new_tm $ #raw const $ new_tm); |
|
286 |
val tac = (fn ctxt => unfold_thms_tac ctxt (pcr_rel_F_eqs @ [crel_def]) THEN |
|
287 |
#tac const {Rs=var_Rs,Qs=var_Qs} ctxt); |
|
288 |
in prove lthy vars tm tac end; |
|
289 |
val prove_transfer_thm = prove_transfer_thm' 0; |
|
290 |
||
291 |
(* map transfer: "((Q ===> R) ===> pcr_G Q ===> pcr_G R) map_F' map_G" *) |
|
292 |
val map_G = mk_map_of_bnf Ds0 (#betas Tss) (#deltas Tss) bnf_G; |
|
293 |
val map_transfer = prove_transfer_thm (var_Qs @ var_Rs) map_G (#map consts); |
|
294 |
||
295 |
(* pred_transfer: "((Q ===> (=)) ===> pcr_G Q ===> (=)) pred_F' pred_G" *) |
|
296 |
val pred_G = mk_pred_of_bnf Ds0 (#betas Tss) bnf_G; |
|
297 |
val pred_transfer = #pred consts |> Option.map (fn p => |
|
298 |
("pred", [prove_transfer_thm (var_Qs @ var_Rs) pred_G p])); |
|
299 |
||
300 |
(* rel_transfer: "((Q ===> R ===> (=)) ===> pcr_G Q ===> pcr_G R ===> (=)) rel_F' rel_G" *) |
|
301 |
val rel_G = mk_rel_of_bnf Ds0 (#betas Tss) (#deltas Tss) bnf_G; |
|
302 |
val rel_transfer = prove_transfer_thm (var_Qs @ var_Rs) rel_G (#rel consts); |
|
303 |
||
304 |
(* set_transfer: "(pcr_G Q ===> rel_set Q) set_F' set_G" *) |
|
305 |
val sets_G = mk_sets_of_bnf (replicate live Ds0) (replicate live (#betas Tss)) bnf_G; |
|
306 |
fun mk_set_transfer i set_G raw tac = prove_transfer_thm' i var_Qs set_G {raw=raw, tac=tac}; |
|
307 |
val sets_transfer = @{map 4} mk_set_transfer |
|
308 |
(0 upto (live-1)) sets_G (#raws (#sets consts)) (#tacs (#sets consts)); |
|
309 |
||
310 |
(* export transfer theorems *) |
|
311 |
val transform = Morphism.thm (Morphism.thm_morphism "BNF" (unfold_thms lthy defs)) |> map; |
|
312 |
val b = Binding.qualified_name name; |
|
313 |
val qualify = |
|
314 |
let val qs = Binding.path_of b; |
|
315 |
in fold_rev (fn (s, mand) => Binding.qualify mand s) qs end; |
|
316 |
fun mk_binding n = Binding.name (n ^ "_transfer_raw") |
|
317 |
|> Binding.qualify true (Binding.name_of b) |> qualify; |
|
318 |
val notes = [("map", [map_transfer]), ("rel", [rel_transfer])] @ the_list pred_transfer @ |
|
319 |
[("set", sets_transfer)] |> map (fn (n, thms) => |
|
320 |
((mk_binding n, []), [(transform thms, @{attributes [transfer_rule]})])); |
|
321 |
||
322 |
in lthy |> Local_Theory.notes notes |> snd end; |
|
323 |
||
324 |
(* transfer theorems for map, pred (in case of a typedef), rel and sets *) |
|
325 |
fun mk_transfer_thms quiet bnf_F bnf_G name consts thm Tss defs lthy = let |
|
326 |
||
327 |
fun mk_crel_def quot_thm = |
|
328 |
(case thm of |
|
329 |
Quotient equiv => @{thm Quotient_crel_quotient} OF [quot_thm, equiv] |
|
71494 | 330 |
| Typedef => hd ([quot_thm] RL @{thms Quotient_crel_typedef Quotient_crel_typecopy})); |
71262 | 331 |
fun no_quotient _ = [Pretty.para ("No quotient theorem has been registered for " ^ |
332 |
Binding.name_of (name_of_bnf bnf_G) ^ "."), |
|
333 |
Pretty.para "Use setup_lifting to register a quotient or type definition theorem."]; |
|
334 |
fun wrong_quotient T lthy = [Pretty.para ("A wrong quotient theorem has been registered for " ^ |
|
335 |
Binding.name_of (name_of_bnf bnf_G) ^ "."), |
|
336 |
Pretty.para ("Expected raw type " ^ |
|
337 |
Pretty.string_of (Syntax.pretty_typ lthy (T_of_bnf bnf_F)) ^ |
|
338 |
" but the quotient theorem has raw type " ^ |
|
339 |
Pretty.string_of (Syntax.pretty_typ lthy T) ^ "."), |
|
340 |
Pretty.para "Use setup_lifting to register a different quotient or type definition theorem."]; |
|
341 |
fun pcr_why _ = [Pretty.para ("The pcr_" ^ Binding.name_of (name_of_bnf bnf_G) ^ |
|
342 |
" relator has not been defined.")]; |
|
343 |
fun warn_transfer why lthy = |
|
344 |
(Pretty.para "The transfer theorems can't be generated:" :: why lthy) |
|
345 |
|> Pretty.chunks |> Pretty.string_of |> warning |> K lthy; |
|
346 |
fun maybe_warn_transfer why = not quiet ? warn_transfer why; |
|
347 |
in |
|
348 |
case Lifting_Info.lookup_quotients lthy name of |
|
349 |
SOME {pcr_info, quot_thm} => |
|
350 |
(let |
|
351 |
val crel_def = mk_crel_def quot_thm; |
|
352 |
val rty = Lifting_Util.quot_thm_rty_qty quot_thm |> fst; |
|
353 |
val thy = Proof_Context.theory_of lthy; |
|
354 |
in |
|
355 |
if Sign.typ_instance thy (rty, T_of_bnf bnf_F) then |
|
356 |
(case pcr_info of |
|
357 |
SOME {pcrel_def, ...} => |
|
358 |
mk_transfer_thms' bnf_F bnf_G name consts Tss crel_def pcrel_def defs lthy |
|
359 |
| _ => maybe_warn_transfer pcr_why lthy) |
|
360 |
else maybe_warn_transfer (wrong_quotient rty) lthy |
|
361 |
end) |
|
362 |
| _ => maybe_warn_transfer no_quotient lthy |
|
363 |
end; |
|
364 |
||
365 |
||
366 |
(** typedef_bnf **) |
|
367 |
||
368 |
fun mk_typedef_transfer_tacs bnf_F bnf_G thms old_defs |
|
369 |
map_raw rel_raw pred_raw sets_raw = let |
|
370 |
||
371 |
val live = live_of_bnf bnf_G; |
|
372 |
val Abs_G_inverse = @{thm type_definition.Abs_inverse} OF [#typedef thms]; |
|
373 |
val Rep_G = @{thm type_definition.Rep} OF [#typedef thms]; |
|
374 |
||
375 |
fun common_tac addefs tac = (fn _ => fn ctxt => |
|
376 |
HEADGOAL (EVERY' [SELECT_GOAL (unfold_thms_tac ctxt addefs), |
|
377 |
REPEAT_DETERM o rtac ctxt rel_funI, |
|
378 |
SELECT_GOAL (unfold_thms_tac ctxt @{thms o_apply}), |
|
379 |
REPEAT_DETERM o eresolve_tac ctxt @{thms relcomppE exE conjE}, |
|
380 |
hyp_subst_tac ctxt]) THEN tac ctxt) |
|
381 |
||
382 |
fun map_tac ctxt = (HEADGOAL o EVERY') |
|
383 |
[rtac ctxt @{thm relcomppI}, |
|
384 |
etac ctxt (mk_rel_funDN (live+1) (map_transfer_of_bnf bnf_F)), |
|
385 |
REPEAT_DETERM_N live o assume_tac ctxt, |
|
386 |
SELECT_GOAL (unfold_thms_tac ctxt [Abs_G_inverse OF [#map_closed thms] OF [Rep_G]]), |
|
387 |
REPEAT_DETERM o rtac ctxt refl]; |
|
388 |
val map_tac = common_tac [#map old_defs] map_tac; |
|
389 |
||
390 |
fun rel_tac ctxt = |
|
391 |
HEADGOAL (etac ctxt (mk_rel_funDN (live+2) (rel_transfer_of_bnf bnf_F)) THEN' |
|
392 |
REPEAT_DETERM_N (live+1) o assume_tac ctxt); |
|
393 |
val rel_tac = common_tac (#rel old_defs :: @{thms vimage2p_def}) rel_tac; |
|
394 |
||
395 |
fun pred_tac ctxt = |
|
396 |
HEADGOAL (etac ctxt (mk_rel_funDN (live+1) (pred_transfer_of_bnf bnf_F)) THEN' |
|
397 |
REPEAT_DETERM_N live o (assume_tac ctxt)); |
|
398 |
val pred_tac = common_tac [#pred old_defs] pred_tac; |
|
399 |
||
400 |
fun set_tac set_transfer_thm ctxt = |
|
401 |
HEADGOAL (etac ctxt (rel_funD OF [set_transfer_thm])); |
|
402 |
fun mk_set_tac set_def set_transfer = common_tac [set_def] (set_tac set_transfer); |
|
403 |
val set_tacs = map2 mk_set_tac (#sets old_defs) (set_transfer_of_bnf bnf_F); |
|
404 |
||
405 |
in {map={raw=map_raw,tac=map_tac},rel={raw=rel_raw,tac=rel_tac}, |
|
406 |
sets={raws=sets_raw,tacs=set_tacs},pred=SOME{raw=pred_raw,tac=pred_tac}} end; |
|
60918 | 407 |
|
62324 | 408 |
fun typedef_bnf thm wits specs map_b rel_b pred_b opts lthy = |
60918 | 409 |
let |
61073 | 410 |
val plugins = |
411 |
get_first (fn Plugins_Option f => SOME (f lthy) | _ => NONE) (rev opts) |
|
71262 | 412 |
|> the_default Plugin_Name.default_filter; |
60918 | 413 |
|
414 |
(* extract Rep Abs F RepT AbsT *) |
|
71262 | 415 |
val (Rep_G, Abs_G, F) = strip3 thm; |
61073 | 416 |
val typ_Abs_G = dest_funT (fastype_of Abs_G); |
60918 | 417 |
val RepT = fst typ_Abs_G; (* F *) |
418 |
val AbsT = snd typ_Abs_G; (* G *) |
|
419 |
val AbsT_name = fst (dest_Type AbsT); |
|
420 |
val tvs = AbsT |> dest_Type |> snd |> map (fst o dest_TVar); |
|
421 |
val alpha0s = map (TFree o snd) specs; |
|
61067 | 422 |
|
62690 | 423 |
val _ = length tvs = length alpha0s orelse |
424 |
error ("Expected " ^ string_of_int (length tvs) ^ " type argument(s) to " ^ quote AbsT_name); |
|
425 |
||
60918 | 426 |
(* instantiate the new type variables newtvs to oldtvs *) |
427 |
val subst = subst_TVars (tvs ~~ alpha0s); |
|
428 |
val typ_subst = typ_subst_TVars (tvs ~~ alpha0s); |
|
429 |
||
430 |
val Rep_G = subst Rep_G; |
|
431 |
val Abs_G = subst Abs_G; |
|
432 |
val F = subst F; |
|
433 |
val RepT = typ_subst RepT; |
|
434 |
val AbsT = typ_subst AbsT; |
|
435 |
||
61073 | 436 |
fun flatten_tyargs Ass = |
437 |
map dest_TFree alpha0s |
|
71262 | 438 |
|> filter (fn T => exists (fn Ts => member op= Ts T) Ass); |
60918 | 439 |
|
440 |
val Ds0 = filter (is_none o fst) specs |> map snd; |
|
441 |
||
442 |
(* get the bnf for RepT *) |
|
71262 | 443 |
val ((bnf_F, (deads, alphas)), ((_, unfolds), lthy)) = |
62621 | 444 |
bnf_of_typ true Dont_Inline (Binding.qualify true AbsT_name) flatten_tyargs [] |
60918 | 445 |
Ds0 RepT ((empty_comp_cache, empty_unfolds), lthy); |
446 |
||
61073 | 447 |
val set_bs = |
448 |
map (fn T => find_index (fn U => T = U) alpha0s) alphas |
|
60918 | 449 |
|> map (the_default Binding.empty o fst o nth specs); |
450 |
||
61067 | 451 |
val _ = (case alphas of [] => error "No live variables" | _ => ()); |
60918 | 452 |
|
71261 | 453 |
val defs = #map_unfolds unfolds @ flat (#set_unfoldss unfolds) @ #rel_unfolds unfolds @ #pred_unfolds unfolds; |
60918 | 454 |
|
455 |
(* number of live variables *) |
|
71262 | 456 |
val live = length alphas; |
60918 | 457 |
|
458 |
(* state the three required properties *) |
|
459 |
val sorts = map Type.sort_of_atyp alphas; |
|
460 |
val names_lthy = fold Variable.declare_typ (alphas @ deads) lthy; |
|
71262 | 461 |
val (((alphas', betas), betas'), names_lthy) = names_lthy |
462 |
|> mk_TFrees' sorts |
|
463 |
||>> mk_TFrees' sorts |
|
464 |
||>> mk_TFrees' sorts; |
|
60918 | 465 |
|
71262 | 466 |
val map_F = mk_map_of_bnf deads alphas betas bnf_F; |
60918 | 467 |
|
71262 | 468 |
val (typ_fs, typ_aF) = fastype_of map_F |> strip_typeN live ||> domain_type; |
60918 | 469 |
val typ_pairs = map HOLogic.mk_prodT (alphas ~~ alphas'); |
470 |
val typ_subst_pair = typ_subst_atomic (alphas ~~ typ_pairs); |
|
471 |
val typ_pair = typ_subst_pair RepT; |
|
472 |
val subst_b = subst_atomic_types (alphas ~~ betas); |
|
473 |
val subst_a' = subst_atomic_types (alphas ~~ alphas'); |
|
474 |
val subst_pair = subst_atomic_types (alphas ~~ typ_pairs); |
|
475 |
val aF_set = F; |
|
476 |
val aF_set' = subst_a' F; |
|
477 |
val pairF_set = subst_pair F; |
|
71262 | 478 |
val bF_set = subst_b F; |
479 |
val map_F_fst = mk_map_of_bnf deads typ_pairs alphas bnf_F; |
|
480 |
val map_F_snd = mk_map_of_bnf deads typ_pairs alphas' bnf_F |
|
481 |
val sets_F_pairs = mk_sets_of_bnf (replicate live deads) (replicate live typ_pairs) bnf_F |
|
60918 | 482 |
val wits_F = mk_wits_of_bnf |
71262 | 483 |
(replicate (nwits_of_bnf bnf_F) deads) |
484 |
(replicate (nwits_of_bnf bnf_F) alphas) bnf_F; |
|
60918 | 485 |
|
486 |
(* val map_closed_F = @{term "\<And>f x. x \<in> F \<Longrightarrow> map_F f x \<in> F"}; *) |
|
487 |
val (var_fs, names_lthy) = mk_Frees "f" typ_fs names_lthy; |
|
488 |
val (var_x, names_lthy) = mk_Frees "x" [typ_aF] names_lthy |>> the_single; |
|
61073 | 489 |
val mem_x = HOLogic.mk_Trueprop (HOLogic.mk_mem (var_x, aF_set)); |
60918 | 490 |
val map_f = list_comb (map_F, var_fs); |
61073 | 491 |
val mem_map = HOLogic.mk_Trueprop (HOLogic.mk_mem (map_f $ var_x, bF_set)); |
60918 | 492 |
val imp_map = Logic.mk_implies (mem_x, mem_map); |
61073 | 493 |
val map_closed_F = fold_rev Logic.all var_fs (Logic.all var_x imp_map); |
60918 | 494 |
|
71262 | 495 |
(* val zip_closed_F = |
496 |
@{term "\<And>z. \<lbrakk>map_F fst z \<in> F; map_F snd z \<in> F\<rbrakk> \<Longrightarrow> |
|
497 |
\<exists>z' \<in> F. set_F z' \<subseteq> set_F z \<and> map_F fst z' = map_F fst z \<and> map_F snd z' = map_F snd z"}; *) |
|
498 |
val (var_z, names_lthy) = mk_Free "z" typ_pair names_lthy; |
|
499 |
val (var_z', names_lthy) = mk_Free "z'" typ_pair names_lthy; |
|
60918 | 500 |
val (pairs, names_lthy) = mk_Frees "tmp" typ_pairs names_lthy; |
71262 | 501 |
|
502 |
fun mk_map mfs f z = Term.list_comb (mfs, map (fst o Term.strip_comb o f) pairs) $ z; |
|
503 |
fun mk_set var = map (fn t => t $ var) sets_F_pairs; |
|
504 |
||
505 |
val (map_fst', map_fst) = apply2 (mk_map map_F_fst HOLogic.mk_fst) (var_z', var_z); |
|
506 |
val (map_snd', map_snd) = apply2 (mk_map map_F_snd HOLogic.mk_snd) (var_z', var_z); |
|
61073 | 507 |
val mem_map_fst = HOLogic.mk_Trueprop (HOLogic.mk_mem (map_fst, aF_set)); |
508 |
val mem_map_snd = HOLogic.mk_Trueprop (HOLogic.mk_mem (map_snd, aF_set')); |
|
71262 | 509 |
val ex_conj = foldr1 HOLogic.mk_conj (map2 mk_leq (mk_set var_z') (mk_set var_z) @ |
510 |
[HOLogic.mk_eq (map_fst', map_fst), HOLogic.mk_eq (map_snd', map_snd)]); |
|
511 |
val zip_concl = HOLogic.mk_Trueprop (mk_Bex pairF_set (absfree (dest_Free var_z') ex_conj)); |
|
512 |
val zip_closed_F = Logic.all var_z (Logic.list_implies ([mem_map_fst, mem_map_snd], zip_concl)); |
|
60918 | 513 |
|
514 |
(* val wit_closed_F = @{term "wit_F a \<in> F"}; *) |
|
515 |
val (var_as, names_lthy) = mk_Frees "a" alphas names_lthy; |
|
516 |
val (var_bs, _) = mk_Frees "a" alphas names_lthy; |
|
71262 | 517 |
val sets = mk_sets_of_bnf (replicate live deads) (replicate live alphas) bnf_F; |
518 |
val (Iwits, wit_goals) = |
|
519 |
prepare_wits false RepT wits opts alphas wits_F var_as var_bs sets lthy; |
|
60918 | 520 |
val wit_closed_Fs = |
61067 | 521 |
Iwits |> map (fn (I, wit_F) => |
60918 | 522 |
let |
523 |
val vars = map (nth var_as) I; |
|
524 |
val wit_a = list_comb (wit_F, vars); |
|
61073 | 525 |
in fold_rev Logic.all vars (HOLogic.mk_Trueprop (HOLogic.mk_mem (wit_a, aF_set))) end); |
60918 | 526 |
|
527 |
val goals = [map_closed_F, zip_closed_F] @ wit_closed_Fs @ |
|
71262 | 528 |
(case wits of NONE => [] | _ => wit_goals); |
60918 | 529 |
|
530 |
fun after_qed ([map_closed_thm] :: [zip_closed_thm] :: wit_thmss) lthy = |
|
61067 | 531 |
let |
532 |
val (wit_closed_thms, wit_thms) = |
|
533 |
(case wits of |
|
71262 | 534 |
NONE => (map the_single wit_thmss, wit_thms_of_bnf bnf_F) |
61067 | 535 |
| _ => chop (length wit_closed_Fs) (map the_single wit_thmss)) |
60918 | 536 |
|
61067 | 537 |
(* construct map set bd rel wit *) |
538 |
(* val map_G = @{term "\<lambda>f. Abs_G o map_F f o Rep_G"}; *) |
|
539 |
val Abs_Gb = subst_b Abs_G; |
|
71262 | 540 |
val map_G = fold_rev lambda var_fs |
61073 | 541 |
(HOLogic.mk_comp (HOLogic.mk_comp (Abs_Gb, map_f), Rep_G)); |
71262 | 542 |
val map_raw = fold_rev lambda var_fs map_f; |
60918 | 543 |
|
61067 | 544 |
(* val sets_G = [@{term "set_F o Rep_G"}]; *) |
71262 | 545 |
val sets_F = mk_sets_of_bnf (replicate live deads) (replicate live alphas) bnf_F; |
61067 | 546 |
val sets_G = map (fn set_F => HOLogic.mk_comp (set_F, Rep_G)) sets_F; |
60918 | 547 |
|
61067 | 548 |
(* val bd_G = @{term "bd_F"}; *) |
71262 | 549 |
val bd_F = mk_bd_of_bnf deads alphas bnf_F; |
61067 | 550 |
val bd_G = bd_F; |
551 |
||
552 |
(* val rel_G = @{term "\<lambda>R. BNF_Def.vimage2p Rep_G Rep_G (rel_F R)"}; *) |
|
71262 | 553 |
val rel_F = mk_rel_of_bnf deads alphas betas bnf_F; |
554 |
val (typ_Rs, _) = strip_typeN live (fastype_of rel_F); |
|
60918 | 555 |
|
61067 | 556 |
val (var_Rs, names_lthy) = mk_Frees "R" typ_Rs lthy; |
557 |
val Rep_Gb = subst_b Rep_G; |
|
558 |
val rel_G = fold_rev absfree (map dest_Free var_Rs) |
|
559 |
(mk_vimage2p Rep_G Rep_Gb $ list_comb (rel_F, var_Rs)); |
|
71262 | 560 |
val rel_raw = fold_rev absfree (map dest_Free var_Rs) (list_comb (rel_F, var_Rs)); |
60918 | 561 |
|
62324 | 562 |
(* val pred_G = @{term "\<lambda>P. pred_F P o Rep_G"}; *) |
71262 | 563 |
val pred_F = mk_pred_of_bnf deads alphas bnf_F; |
564 |
val (typ_Ps, _) = strip_typeN live (fastype_of pred_F); |
|
62324 | 565 |
|
566 |
val (var_Ps, names_lthy) = mk_Frees "P" typ_Ps names_lthy; |
|
567 |
val pred_G = fold_rev absfree (map dest_Free var_Ps) |
|
568 |
(HOLogic.mk_comp (list_comb (pred_F, var_Ps), Rep_G)); |
|
71262 | 569 |
val pred_raw = fold_rev absfree (map dest_Free var_Ps) (list_comb (pred_F, var_Ps)); |
62324 | 570 |
|
61067 | 571 |
(* val wits_G = [@{term "Abs_G o wit_F"}]; *) |
572 |
val (var_as, _) = mk_Frees "a" alphas names_lthy; |
|
573 |
val wits_G = |
|
574 |
map (fn (I, wit_F) => |
|
575 |
let |
|
576 |
val vs = map (nth var_as) I; |
|
577 |
in fold_rev absfree (map dest_Free vs) (Abs_G $ (list_comb (wit_F, vs))) end) |
|
578 |
Iwits; |
|
60918 | 579 |
|
61067 | 580 |
(* tactics *) |
581 |
val Rep_thm = thm RS @{thm type_definition.Rep}; |
|
582 |
val Abs_inverse_thm = thm RS @{thm type_definition.Abs_inverse}; |
|
583 |
val Abs_inject_thm = thm RS @{thm type_definition.Abs_inject}; |
|
584 |
val Rep_cases_thm = thm RS @{thm type_definition.Rep_cases}; |
|
585 |
val Rep_inverse_thm = thm RS @{thm type_definition.Rep_inverse}; |
|
60918 | 586 |
|
61067 | 587 |
fun map_id0_tac ctxt = |
588 |
HEADGOAL (EVERY' [rtac ctxt ext, |
|
71262 | 589 |
SELECT_GOAL (unfold_thms_tac ctxt [map_id0_of_bnf bnf_F, id_apply, o_apply, |
61067 | 590 |
Rep_inverse_thm]), |
591 |
rtac ctxt refl]); |
|
60918 | 592 |
|
61067 | 593 |
fun map_comp0_tac ctxt = |
60918 | 594 |
HEADGOAL (EVERY' [rtac ctxt ext, |
71262 | 595 |
SELECT_GOAL (unfold_thms_tac ctxt [map_comp0_of_bnf bnf_F, o_apply, |
60918 | 596 |
Rep_thm RS (map_closed_thm RS Abs_inverse_thm)]), |
61067 | 597 |
rtac ctxt refl]); |
60918 | 598 |
|
61067 | 599 |
fun map_cong0_tac ctxt = |
600 |
HEADGOAL (EVERY' ([SELECT_GOAL (unfold_thms_tac ctxt [o_apply]), |
|
601 |
rtac ctxt (([Rep_thm RS map_closed_thm, Rep_thm RS map_closed_thm] MRS |
|
602 |
Abs_inject_thm) RS iffD2), |
|
71262 | 603 |
rtac ctxt (map_cong0_of_bnf bnf_F)] @ replicate live (Goal.assume_rule_tac ctxt))); |
60918 | 604 |
|
61067 | 605 |
val set_map0s_tac = |
606 |
map (fn set_map => fn ctxt => |
|
607 |
HEADGOAL (EVERY' [rtac ctxt ext, |
|
608 |
SELECT_GOAL (unfold_thms_tac ctxt [set_map, o_apply, |
|
609 |
Rep_thm RS (map_closed_thm RS Abs_inverse_thm)]), |
|
610 |
rtac ctxt refl])) |
|
71262 | 611 |
(set_map_of_bnf bnf_F); |
61067 | 612 |
|
71262 | 613 |
fun card_order_bd_tac ctxt = HEADGOAL (rtac ctxt (bd_card_order_of_bnf bnf_F)); |
60918 | 614 |
|
71262 | 615 |
fun cinfinite_bd_tac ctxt = HEADGOAL (rtac ctxt (bd_cinfinite_of_bnf bnf_F)); |
61067 | 616 |
|
617 |
val set_bds_tac = |
|
618 |
map (fn set_bd => fn ctxt => |
|
619 |
HEADGOAL (EVERY' [SELECT_GOAL (unfold_thms_tac ctxt [o_apply]), rtac ctxt set_bd])) |
|
71262 | 620 |
(set_bd_of_bnf bnf_F); |
61067 | 621 |
|
622 |
fun le_rel_OO_tac ctxt = |
|
623 |
HEADGOAL (EVERY' [rtac ctxt @{thm vimage2p_relcompp_mono}, |
|
71262 | 624 |
rtac ctxt ((rel_OO_of_bnf bnf_F RS sym) RS @{thm ord_eq_le_trans}), |
61067 | 625 |
rtac ctxt @{thm order_refl}]); |
60918 | 626 |
|
61067 | 627 |
fun rel_OO_Grp_tac ctxt = |
628 |
HEADGOAL (EVERY' ([SELECT_GOAL (REPEAT_DETERM (HEADGOAL (rtac ctxt ext))), |
|
629 |
SELECT_GOAL (unfold_thms_tac ctxt [@{thm OO_Grp_alt}, mem_Collect_eq, |
|
71262 | 630 |
o_apply, @{thm vimage2p_def}, in_rel_of_bnf bnf_F, Bex_def, mem_Collect_eq]), |
61067 | 631 |
rtac ctxt iffI, |
71262 | 632 |
SELECT_GOAL (REPEAT_DETERM (HEADGOAL (eresolve_tac ctxt [exE, conjE]))), |
633 |
forward_tac ctxt |
|
634 |
[zip_closed_thm OF (replicate 2 (Rep_thm RSN (2, @{thm ssubst_mem})))], |
|
61067 | 635 |
assume_tac ctxt, |
71262 | 636 |
SELECT_GOAL (REPEAT_DETERM (HEADGOAL (eresolve_tac ctxt [bexE, conjE]))), |
637 |
etac ctxt Rep_cases_thm, |
|
61067 | 638 |
hyp_subst_tac ctxt, |
639 |
SELECT_GOAL (REPEAT_DETERM (HEADGOAL (rtac ctxt exI))), |
|
640 |
rtac ctxt conjI] @ |
|
71262 | 641 |
replicate live |
642 |
(EVERY' [TRY o rtac ctxt conjI, etac ctxt @{thm order_trans}, assume_tac ctxt]) @ |
|
643 |
[SELECT_GOAL (REPEAT_DETERM (HEADGOAL (rtac ctxt conjI))), |
|
644 |
REPEAT_DETERM_N 2 o EVERY' |
|
645 |
[rtac ctxt (trans OF [iffD2 OF [Abs_inject_thm OF |
|
646 |
[map_closed_thm OF [Rep_thm], Rep_thm]], Rep_inverse_thm]), |
|
647 |
etac ctxt trans, assume_tac ctxt], |
|
648 |
SELECT_GOAL (REPEAT_DETERM (HEADGOAL (eresolve_tac ctxt [exE, conjE]))), |
|
61067 | 649 |
rtac ctxt exI, |
650 |
rtac ctxt conjI] @ |
|
71262 | 651 |
replicate (live-1) (rtac ctxt conjI THEN' assume_tac ctxt) @ |
61067 | 652 |
[assume_tac ctxt, |
653 |
rtac ctxt conjI, |
|
654 |
REPEAT_DETERM_N 2 o EVERY' |
|
655 |
[rtac ctxt (iffD1 OF [Abs_inject_thm OF [map_closed_thm OF [Rep_thm], Rep_thm]]), |
|
656 |
etac ctxt (Rep_inverse_thm RS sym RSN (2, trans))]])); |
|
60918 | 657 |
|
62324 | 658 |
fun pred_set_tac ctxt = |
659 |
HEADGOAL (EVERY' |
|
71262 | 660 |
[rtac ctxt (pred_set_of_bnf bnf_F RS @{thm arg_cong[of _ _ "\<lambda>f. f \<circ> _"]} RS trans), |
62324 | 661 |
SELECT_GOAL (unfold_thms_tac ctxt (@{thms Ball_comp_iff conj_comp_iff})), |
662 |
rtac ctxt refl]); |
|
663 |
||
61067 | 664 |
fun wit_tac ctxt = |
665 |
HEADGOAL (EVERY' |
|
666 |
(map (fn thm => (EVERY' |
|
667 |
[SELECT_GOAL (unfold_thms_tac ctxt (o_apply :: |
|
668 |
(wit_closed_thms RL [Abs_inverse_thm]))), |
|
669 |
dtac ctxt thm, assume_tac ctxt])) |
|
670 |
wit_thms)); |
|
60918 | 671 |
|
61067 | 672 |
val tactics = [map_id0_tac, map_comp0_tac, map_cong0_tac] @ set_map0s_tac @ |
62324 | 673 |
[card_order_bd_tac, cinfinite_bd_tac] @ set_bds_tac @ |
674 |
[le_rel_OO_tac, rel_OO_Grp_tac, pred_set_tac]; |
|
60918 | 675 |
|
71262 | 676 |
val (bnf_G, lthy) = bnf_def Dont_Inline (user_policy Note_Some) true I |
62324 | 677 |
tactics wit_tac NONE map_b rel_b pred_b set_bs |
678 |
(((((((Binding.empty, AbsT), map_G), sets_G), bd_G), wits_G), SOME rel_G), SOME pred_G) |
|
61067 | 679 |
lthy; |
60928
141a1d485259
unfold intermediate definitions (stemming from composition) in lifted bnf operations
traytel
parents:
60918
diff
changeset
|
680 |
|
71262 | 681 |
val old_defs = |
682 |
{sets = set_defs_of_bnf bnf_G, map = map_def_of_bnf bnf_G, rel = rel_def_of_bnf bnf_G, |
|
683 |
pred = pred_def_of_bnf bnf_G}; |
|
684 |
||
685 |
val unfold_morphism = Morphism.thm_morphism "BNF" (unfold_thms lthy defs); |
|
686 |
val (bnf_G, lthy) = morph_bnf_defs unfold_morphism bnf_G |
|
66272
c6714a9562ae
store the unfolded definitions of the lifted bnf constants under "_def" name
traytel
parents:
63023
diff
changeset
|
687 |
|> (fn bnf => note_bnf_defs bnf lthy); |
71262 | 688 |
|
689 |
val quiet = exists (fn No_Warn_Transfer => true | _ => false) opts; |
|
690 |
||
691 |
val transfer_consts = mk_typedef_transfer_tacs bnf_F bnf_G |
|
692 |
{map_closed=map_closed_thm,typedef=thm} old_defs map_raw rel_raw pred_raw sets_F; |
|
61067 | 693 |
in |
71262 | 694 |
lthy |> BNF_Def.register_bnf plugins AbsT_name bnf_G |> |
71494 | 695 |
mk_transfer_thms quiet bnf_F bnf_G AbsT_name transfer_consts Typedef |
71262 | 696 |
{abs=typ_subst_atomic (alphas ~~ alphas') AbsT, rep=RepT, Ds0=map TFree Ds0, |
697 |
deads = deads, alphas=alphas, betas=alphas', gammas=betas, deltas=betas'} defs |
|
61067 | 698 |
end |
699 |
| after_qed _ _ = raise Match; |
|
60918 | 700 |
in |
701 |
(goals, after_qed, defs, lthy) |
|
702 |
end; |
|
703 |
||
61067 | 704 |
|
71262 | 705 |
(** quotient_bnf **) |
706 |
||
707 |
fun mk_quotient_transfer_tacs bnf_F Tss live qthms thms set_F'_thmss old_defs |
|
708 |
inst_REL_pos_distrI map_raw rel_raw sets_raw = let |
|
709 |
||
710 |
fun common_tac ctxt addefs = unfold_thms_tac ctxt (#REL qthms :: addefs) THEN |
|
711 |
(REPEAT_DETERM o HEADGOAL) (rtac ctxt rel_funI); |
|
712 |
||
713 |
(* quotient.map_transfer tactic *) |
|
714 |
val map_F_transfer = map_transfer_of_bnf bnf_F |> mk_rel_funDN (live+1); |
|
715 |
fun map_transfer_q _ ctxt = |
|
716 |
common_tac ctxt (#map old_defs :: @{thms o_def}) THEN |
|
717 |
(HEADGOAL o EVERY') [REPEAT_DETERM o eresolve_tac ctxt @{thms relcomppE}, |
|
718 |
rtac ctxt @{thm relcomppI[rotated]}, hyp_subst_tac ctxt THEN' EVERY' |
|
719 |
(map (rtac ctxt) [#rel_abs qthms, #map_F_rsp thms, (#rep_abs_rsp qthms), (#reflp qthms)]), |
|
720 |
hyp_subst_tac ctxt, rtac ctxt map_F_transfer, REPEAT_DETERM_N (live+1) o assume_tac ctxt]; |
|
721 |
||
722 |
(* quotient.rel_transfer tactic *) |
|
723 |
val rel_F_maps = rel_map_of_bnf bnf_F; |
|
724 |
val rel_F_map_iffD2s = map (fn thm => thm RS @{thm iffD2}) rel_F_maps; |
|
725 |
fun inst_REL_pos_distrI_order_refls vs aTs bTs ctxt = inst_REL_pos_distrI live vs aTs bTs ctxt |
|
726 |
OF (replicate (live+1) asm_rl @ replicate live @{thm order_refl}); |
|
727 |
fun rel_transfer_q {Qs, Rs} ctxt = EVERY |
|
728 |
[common_tac ctxt [#rel old_defs, @{thm vimage2p_def}], |
|
729 |
HEADGOAL (rtac ctxt iffI), |
|
730 |
(REPEAT_DETERM o ALLGOALS) |
|
731 |
(eresolve_tac ctxt @{thms exE conjE relcomppE} ORELSE' hyp_subst_tac ctxt), |
|
732 |
(HEADGOAL o EVERY') |
|
733 |
[REPEAT_DETERM o dtac ctxt @{thm rel_fun_rel_OO1}, |
|
734 |
rtac ctxt (inst_REL_pos_distrI 0 (map mk_conversep Qs) (#betas Tss) (#alphas Tss) ctxt), |
|
735 |
rtac ctxt @{thm relcomppI}, |
|
736 |
rtac ctxt (#symp qthms), |
|
737 |
rtac ctxt (#map_F_rsp thms), |
|
738 |
rtac ctxt (#rep_abs_rsp qthms), |
|
739 |
rtac ctxt (#reflp qthms), |
|
740 |
rtac ctxt @{thm relcomppI}, |
|
741 |
rtac ctxt (rel_flip_of_bnf bnf_F RS @{thm iffD1}), |
|
742 |
rtac ctxt (nth rel_F_map_iffD2s 0), |
|
743 |
rtac ctxt (nth rel_F_map_iffD2s 1), |
|
744 |
etac ctxt (#rel_monoD_rotated thms)], |
|
745 |
(REPEAT_DETERM_N live o HEADGOAL o EVERY') |
|
746 |
[rtac ctxt @{thm predicate2I}, |
|
747 |
rtac ctxt @{thm conversepI}, |
|
748 |
rtac ctxt @{thm Basic_BNFs.rel_sum_simps(4)[THEN iffD2]}, |
|
749 |
etac ctxt @{thm conversepI}], |
|
750 |
(HEADGOAL o EVERY') |
|
751 |
[rtac ctxt (inst_REL_pos_distrI_order_refls Rs (#gammas Tss) (#deltas Tss) ctxt), |
|
752 |
(SELECT_GOAL o REPEAT_DETERM o HEADGOAL) (etac ctxt @{thm relcomppI}), |
|
753 |
rtac ctxt @{thm relcomppI[rotated]}, |
|
754 |
rtac ctxt (#map_F_rsp thms), |
|
755 |
rtac ctxt (#rep_abs_rsp qthms OF [#reflp qthms]), |
|
756 |
SELECT_GOAL (unfold_thms_tac ctxt (@{thms rel_sum_simps} @ rel_F_maps)), |
|
757 |
assume_tac ctxt], |
|
758 |
(REPEAT_DETERM_N (2*live) o HEADGOAL) |
|
759 |
(rtac ctxt @{thm rel_sum_eq2_nonempty} ORELSE' rtac ctxt @{thm rel_sum_eq3_nonempty}), |
|
760 |
(REPEAT_DETERM_N live) |
|
761 |
(unfold_thms_tac ctxt @{thms sum.rel_compp[symmetric] eq_OO} THEN |
|
762 |
HEADGOAL (etac ctxt @{thm sum.rel_mono[OF order_refl]})), |
|
763 |
(HEADGOAL o EVERY') |
|
764 |
[(SELECT_GOAL o REPEAT_DETERM o HEADGOAL) (dtac ctxt @{thm rel_fun_rel_OO2}), |
|
765 |
rtac ctxt (inst_REL_pos_distrI 0 Qs (#alphas Tss) (#betas Tss) ctxt), |
|
766 |
rtac ctxt @{thm relcomppI}, |
|
767 |
rtac ctxt (#reflp qthms), |
|
768 |
rtac ctxt @{thm relcomppI}, |
|
769 |
rtac ctxt (nth rel_F_map_iffD2s 0), |
|
770 |
rtac ctxt (nth rel_F_map_iffD2s 1), |
|
771 |
etac ctxt (#rel_monoD_rotated thms)], |
|
772 |
(REPEAT_DETERM_N live o HEADGOAL o EVERY') |
|
773 |
[rtac ctxt @{thm predicate2I}, rtac ctxt @{thm rel_sum.intros(2)}, assume_tac ctxt], |
|
774 |
(HEADGOAL o EVERY') |
|
775 |
[rtac ctxt |
|
776 |
(inst_REL_pos_distrI_order_refls (map mk_conversep Rs) (#deltas Tss) (#gammas Tss) ctxt), |
|
777 |
rtac ctxt @{thm relcomppI}, |
|
778 |
etac ctxt (rotate_prems 1 (#transp qthms)), |
|
779 |
rtac ctxt (#map_F_rsp thms), |
|
780 |
rtac ctxt (#rep_abs_rsp qthms OF [#reflp qthms]), |
|
781 |
etac ctxt @{thm relcomppI}, |
|
782 |
rtac ctxt @{thm relcomppI}, |
|
783 |
etac ctxt (#transp qthms), |
|
784 |
rtac ctxt (#symp qthms), |
|
785 |
rtac ctxt (#map_F_rsp thms), |
|
786 |
rtac ctxt (#rep_abs_rsp qthms), |
|
787 |
rtac ctxt (#reflp qthms), |
|
788 |
rtac ctxt @{thm relcomppI[rotated]}, |
|
789 |
rtac ctxt (#reflp qthms), |
|
790 |
rtac ctxt (rel_flip_of_bnf bnf_F RS @{thm iffD1}), |
|
791 |
rtac ctxt (nth rel_F_map_iffD2s 0), |
|
792 |
rtac ctxt (nth rel_F_map_iffD2s 1), |
|
793 |
etac ctxt (#rel_monoD_rotated thms)], |
|
794 |
(REPEAT_DETERM_N live o HEADGOAL o EVERY') |
|
795 |
[rtac ctxt @{thm predicate2I}, |
|
796 |
rtac ctxt @{thm conversepI}, |
|
797 |
rtac ctxt @{thm rel_sum.intros(2)}, |
|
798 |
etac ctxt @{thm conversepI}], |
|
799 |
(REPEAT_DETERM_N (2*live) o HEADGOAL) |
|
800 |
(rtac ctxt @{thm rel_sum_eq2_nonempty} ORELSE' rtac ctxt @{thm rel_sum_eq3_nonempty}), |
|
801 |
(REPEAT_DETERM_N live o EVERY) |
|
802 |
[unfold_thms_tac ctxt @{thms sum.rel_compp[symmetric] eq_OO}, |
|
803 |
HEADGOAL (etac ctxt @{thm sum.rel_mono[OF order_refl]})]]; |
|
804 |
||
805 |
(* quotient.set_transfer tactics *) |
|
806 |
fun set_transfer_q set_G_def set_F'_thms _ ctxt = |
|
807 |
let val set_F'_rsp = mk_rel_funDN 1 (#set_F'_respect set_F'_thms) in |
|
808 |
common_tac ctxt (set_G_def :: @{thms o_def}) THEN |
|
809 |
(HEADGOAL o EVERY') |
|
810 |
[etac ctxt @{thm relcomppE}, hyp_subst_tac ctxt, |
|
811 |
SELECT_GOAL (unfold_thms_tac ctxt |
|
812 |
[set_F'_rsp OF [#rep_abs qthms] OF [#reflp qthms], @{thm rel_set_def}]), |
|
813 |
dtac ctxt (#rel_F_rel_F' thms), rtac ctxt conjI] THEN |
|
814 |
(REPEAT_DETERM_N 2 o HEADGOAL o EVERY') |
|
815 |
[SELECT_GOAL (unfold_thms_tac ctxt [#rel_F'_set thms]), |
|
816 |
REPEAT_DETERM o eresolve_tac ctxt [exE, conjE], |
|
817 |
REPEAT_DETERM o dtac ctxt (mk_sym set_F'_rsp), |
|
818 |
SELECT_GOAL (unfold_thms_tac ctxt [#set_map_F' set_F'_thms]), |
|
819 |
rtac ctxt ballI, dtac ctxt @{thm equalityD1[THEN subsetD]}, assume_tac ctxt, |
|
820 |
SELECT_GOAL (unfold_thms_tac ctxt @{thms image_iff}), |
|
821 |
etac ctxt bexE, dtac ctxt set_mp, assume_tac ctxt, |
|
822 |
SELECT_GOAL (unfold_thms_tac ctxt @{thms mem_Collect_eq case_prod_beta}), |
|
823 |
rtac ctxt bexI, hyp_subst_tac ctxt, assume_tac ctxt, etac ctxt @{thm hypsubst}, |
|
824 |
etac ctxt @{thm imageI}, assume_tac ctxt] |
|
825 |
end; |
|
826 |
in |
|
827 |
{map={raw=map_raw, tac=map_transfer_q}, |
|
828 |
rel={raw=rel_raw, tac=rel_transfer_q}, |
|
829 |
sets={raws=sets_raw,tacs=map2 set_transfer_q (#sets old_defs) set_F'_thmss}, |
|
830 |
pred=NONE} |
|
831 |
end; |
|
832 |
||
833 |
||
71494 | 834 |
fun quotient_bnf (equiv_thm, quot_thm) wits specs map_b rel_b pred_b opts lthy = |
71262 | 835 |
let |
836 |
(* extract rep_G and abs_G *) |
|
71393
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
71354
diff
changeset
|
837 |
val (equiv_rel, abs_G, rep_G) = strip3 quot_thm; |
71262 | 838 |
val (repT, absT) = dest_funT (fastype_of abs_G); (* ("?'a F", "?'a G") *) |
839 |
val absT_name = fst (dest_Type absT); |
|
840 |
||
841 |
val tvs = map (fst o dest_TVar) (snd (dest_Type absT)); |
|
842 |
val _ = length tvs = length specs orelse |
|
843 |
error ("Expected " ^ string_of_int (length tvs) ^ |
|
844 |
" type argument" ^ (if (length tvs) = 1 then "" else "s") ^ " to " ^ quote absT_name); |
|
845 |
||
846 |
(* instantiate TVars *) |
|
847 |
val alpha0s = map (TFree o snd) specs; |
|
848 |
val typ_subst = typ_subst_TVars (tvs ~~ alpha0s); |
|
849 |
val (repT, absT) = apply2 typ_subst (repT, absT); |
|
850 |
||
851 |
(* get the bnf for RepT *) |
|
852 |
val Ds0 = filter (is_none o fst) specs |> map snd; |
|
853 |
||
854 |
fun flatten_tyargs Ass = |
|
855 |
map dest_TFree alpha0s |> filter (fn T => exists (fn Ts => member op= Ts T) Ass); |
|
856 |
||
857 |
val ((bnf_F, (deads, alphas)), ((_, unfolds), lthy)) = |
|
858 |
bnf_of_typ true Dont_Inline (Binding.qualify true absT_name) flatten_tyargs |
|
859 |
[] Ds0 repT ((empty_comp_cache, empty_unfolds), lthy); |
|
860 |
val live = length alphas; |
|
861 |
val _ = (if live = 0 then error "No live variables" else ()); |
|
862 |
||
863 |
val defs = #map_unfolds unfolds @ flat (#set_unfoldss unfolds) @ #rel_unfolds unfolds; |
|
864 |
val set_bs = |
|
865 |
map (fn T => find_index (fn U => T = U) alpha0s) alphas |
|
866 |
|> map (the_default Binding.empty o fst o nth specs); |
|
867 |
||
868 |
(* create and instantiate all the needed type variables *) |
|
869 |
val subst = subst_TVars (tvs ~~ alpha0s); |
|
870 |
val (abs_G, rep_G) = apply2 subst (abs_G, rep_G); |
|
871 |
||
872 |
val sorts = map Type.sort_of_atyp alphas; |
|
873 |
val (((betas, gammas), deltas), names_lthy) = fold Variable.declare_typ (alphas @ deads) lthy |
|
874 |
|> mk_TFrees' sorts |
|
875 |
||>> mk_TFrees' sorts |
|
876 |
||>> mk_TFrees' sorts; |
|
877 |
||
878 |
fun subst_Ts tm Ts = subst_atomic_types (alphas ~~ Ts) tm; |
|
879 |
val subst_b = subst_atomic_types (alphas ~~ betas); |
|
880 |
val subst_Maybe = subst_atomic_types o map (swap o `mk_MaybeT); |
|
881 |
val equiv_rel_a = subst equiv_rel; |
|
882 |
val map_F = mk_map_of_bnf deads alphas betas bnf_F; |
|
883 |
val rel_F_ab = mk_rel_of_bnf deads alphas betas bnf_F; |
|
884 |
val rel_F_bc = mk_rel_of_bnf deads betas gammas bnf_F; |
|
885 |
val rel_F_ac = mk_rel_of_bnf deads alphas gammas bnf_F; |
|
886 |
val rel_F_option = mk_rel_of_bnf deads (map mk_MaybeT alphas) (map mk_MaybeT betas) bnf_F; |
|
887 |
val sets_F = mk_sets_of_bnf (replicate live deads) (replicate live alphas) bnf_F; |
|
888 |
val wits_F = mk_wits_of_bnf |
|
889 |
(replicate (nwits_of_bnf bnf_F) deads) (replicate (nwits_of_bnf bnf_F) alphas) bnf_F; |
|
890 |
||
891 |
val (typ_fs, (typ_aF, typ_bF)) = strip_typeN live (fastype_of map_F) ||> dest_funT; |
|
892 |
val typ_MaybeF = typ_subst_atomic (alphas ~~ map mk_MaybeT alphas) typ_aF; |
|
893 |
val typ_a_sets = map HOLogic.mk_setT alphas; |
|
894 |
val typ_pairs = map HOLogic.mk_prodT (alphas ~~ betas); |
|
895 |
val typ_fs' = map (typ_subst_atomic (map (swap o `mk_MaybeT) betas)) typ_fs; |
|
896 |
||
897 |
(* create all the needed variables *) |
|
898 |
val ((((((((((((((((((((((var_Ps, var_Qs), var_Rs), var_x), var_x'), var_y), var_y'), var_mx), |
|
899 |
var_As), var_As'), var_Ss), var_Bs), var_as), var_as'), var_bs), var_bs'), var_R), var_fs), |
|
900 |
var_fs'), var_gs), var_gs'), var_z), var_ts) = names_lthy |
|
901 |
|> mk_Frees "Ps" (map2 mk_relT alphas betas) |
|
902 |
||>> mk_Frees "Qs" (map2 mk_relT betas gammas) |
|
903 |
||>> mk_Frees "Rs" (map2 mk_relT alphas gammas) |
|
904 |
||>> mk_Free "x" typ_aF |
|
905 |
||>> mk_Free "x'" typ_aF |
|
906 |
||>> mk_Free "y" typ_bF |
|
907 |
||>> mk_Free "y'" (typ_subst_atomic (alphas ~~ gammas) typ_aF) |
|
908 |
||>> mk_Free "mx" typ_MaybeF |
|
909 |
||>> mk_Frees "As" typ_a_sets |
|
910 |
||>> mk_Frees "As'" typ_a_sets |
|
911 |
||>> mk_Frees "Ss" (map HOLogic.mk_setT typ_a_sets) |
|
912 |
||>> mk_Frees "Bs" (map HOLogic.mk_setT betas) |
|
913 |
||>> mk_Frees "as" alphas |
|
914 |
||>> mk_Frees "as'" alphas |
|
915 |
||>> mk_Frees "bs" betas |
|
916 |
||>> mk_Frees "bs'" betas |
|
917 |
||>> mk_Free "R" (typ_aF --> typ_bF --> HOLogic.boolT) |
|
918 |
||>> mk_Frees "fs" typ_fs |
|
919 |
||>> mk_Frees "fs'" typ_fs' |
|
920 |
||>> mk_Frees "gs" typ_fs |
|
921 |
||>> mk_Frees "gs'" typ_fs' |
|
922 |
||>> mk_Free "z" (typ_subst_atomic (alphas ~~ typ_pairs) typ_aF) |
|
923 |
||>> mk_Frees "ts" typ_pairs |
|
924 |
|> fst; |
|
925 |
||
926 |
(* create local definitions `b = tm` with n arguments *) |
|
927 |
fun suffix tm s = (dest_Const tm |> fst |> Long_Name.base_name) ^ s; |
|
928 |
fun define lthy b n tm = |
|
929 |
let |
|
930 |
val b = Binding.qualify true absT_name (Binding.qualified_name b); |
|
931 |
val ((tm, (_, def)), (lthy, lthy_old)) = lthy |
|
72154 | 932 |
|> Local_Theory.open_target |
71262 | 933 |
|> Local_Theory.define_internal (((Binding.concealed b, NoSyn), (Binding.empty_atts, tm))) |
934 |
||> `Local_Theory.close_target; |
|
935 |
val phi = Proof_Context.export_morphism lthy_old lthy; |
|
936 |
val tm = Term.subst_atomic_types |
|
937 |
(map (`(Morphism.typ phi)) (alphas @ betas @ gammas @ map TFree Ds0)) |
|
938 |
(Morphism.term phi tm); |
|
939 |
val def = mk_unabs_def n (HOLogic.mk_obj_eq (Morphism.thm phi def)); |
|
940 |
in ({def=def, tm=tm}, lthy) end; |
|
941 |
||
942 |
(* internally use REL, not the user-provided definition *) |
|
943 |
val (REL, lthy) = define lthy "REL" 0 equiv_rel_a; |
|
944 |
val REL_def = sym RS eq_reflection OF [#def REL]; |
|
945 |
fun REL_rewr_all ctxt thm = Conv.fconv_rule |
|
946 |
(Conv.top_conv (fn _ => Conv.try_conv (Conv.rewr_conv REL_def)) ctxt) thm; |
|
947 |
||
948 |
val equiv_rel_a' = equiv_rel_a; |
|
949 |
val equiv_rel_a = #tm REL; |
|
950 |
val (equiv_rel_b, equiv_rel_c) = apply2 (subst_Ts equiv_rel_a) (betas, gammas); |
|
951 |
||
952 |
(* rel_pos_distr: @{term "\<And>A B. |
|
953 |
A \<circ>\<circ> B \<noteq> bot \<Longrightarrow> REL \<circ>\<circ> rel_F A \<circ>\<circ> REL \<circ>\<circ> rel_F B \<circ>\<circ> REL \<le> REL \<circ>\<circ> rel_F (A \<circ>\<circ> B) \<circ>\<circ> REL"} *) |
|
954 |
fun compp_not_bot comp aT cT = let |
|
955 |
val T = mk_relT aT cT; |
|
956 |
val mk_eq = HOLogic.eq_const T; |
|
957 |
in HOLogic.mk_not (mk_eq $ comp $ bot_const T) end; |
|
958 |
val ab_comps = map2 mk_relcompp var_Ps var_Qs; |
|
959 |
val ne_comps = (@{map 3} compp_not_bot ab_comps alphas gammas); |
|
960 |
val ab_prem = foldr1 HOLogic.mk_conj ne_comps; |
|
961 |
||
962 |
val REL_pos_distrI_tm = let |
|
963 |
val le_relcomps = map2 mk_leq ab_comps var_Rs; |
|
964 |
val assm = mk_OO [equiv_rel_a, list_comb (rel_F_ab, var_Ps), |
|
965 |
equiv_rel_b, list_comb (rel_F_bc, var_Qs)] equiv_rel_c; |
|
966 |
val concl = mk_OO [equiv_rel_a, list_comb (rel_F_ac, var_Rs)] equiv_rel_c; |
|
967 |
in |
|
968 |
mk_Trueprop_implies |
|
969 |
([assm $ var_x $ var_y'] @ ne_comps @ le_relcomps, concl $ var_x $ var_y') |
|
970 |
end; |
|
971 |
||
972 |
val ab_concl = mk_leq |
|
973 |
(mk_OO [list_comb (rel_F_ab, var_Ps), equiv_rel_b] (list_comb (rel_F_bc, var_Qs))) |
|
974 |
(mk_OO [equiv_rel_a, list_comb (rel_F_ac, ab_comps)] (equiv_rel_c)); |
|
975 |
val ab_imp = Logic.mk_implies (apply2 HOLogic.mk_Trueprop (ab_prem, ab_concl)); |
|
976 |
val rel_pos_distr = fold_rev Logic.all (var_Ps @ var_Qs) ab_imp; |
|
977 |
||
978 |
(* {(x, y) . REL x y} *) |
|
979 |
fun mk_rel_pairs rel = mk_case_prod (var_x, var_x') (rel $ var_x $ var_x') |
|
980 |
val rel_pairs = mk_rel_pairs equiv_rel_a; |
|
981 |
||
982 |
(* rel_Inter: \<And>S. \<lbrakk> S \<noteq> {}; \<Inter>S \<noteq> {} \<rbrakk> \<Longrightarrow> |
|
983 |
(\<Inter>A\<in>S. {(x, y). REL x y} `` {x. set_F x \<subseteq> A}) \<subseteq> {(x, y). REL x y} `` {x. set_F x \<subseteq> \<Inter>S} *) |
|
984 |
fun rel_Inter_from_set_F (var_A, var_S) set_F = let |
|
985 |
||
986 |
val typ_aset = fastype_of var_A; |
|
987 |
||
988 |
(* \<Inter>S *) |
|
989 |
val inter_S = Inf_const typ_aset $ var_S; |
|
990 |
||
991 |
(* [S \<noteq> {}, \<Inter>S \<noteq> {}] *) |
|
992 |
fun not_empty x = let val ty = fastype_of x |
|
993 |
in HOLogic.mk_not (HOLogic.mk_eq (x, bot_const ty)) end; |
|
994 |
val prems = map (HOLogic.mk_Trueprop o not_empty) [var_S, inter_S]; |
|
995 |
||
996 |
(* {x. set_F x \<subseteq> A} *) |
|
997 |
val setF_sub_A = mk_in [var_A] [set_F] typ_aF; |
|
998 |
||
999 |
(* {x. set_F x \<subseteq> \<Inter>S} *) |
|
1000 |
val setF_sub_S = mk_in [inter_S] [set_F] typ_aF; |
|
1001 |
||
1002 |
val lhs = Inf_const (HOLogic.mk_setT typ_aF) $ (mk_image |
|
1003 |
(absfree (dest_Free var_A) (Image_const typ_aF $ rel_pairs $ setF_sub_A)) $ var_S); |
|
1004 |
val rhs = Image_const typ_aF $ rel_pairs $ setF_sub_S; |
|
1005 |
val concl = HOLogic.mk_Trueprop (mk_leq lhs rhs); |
|
1006 |
||
1007 |
in Logic.all var_S (Logic.list_implies (prems, concl)) end; |
|
1008 |
||
1009 |
val rel_Inters = map2 rel_Inter_from_set_F (var_As ~~ var_Ss) sets_F; |
|
1010 |
||
1011 |
(* map_F_Just = map_F Just *) |
|
1012 |
val map_F_Just = let |
|
1013 |
val option_tys = map mk_MaybeT alphas; |
|
1014 |
val somes = map Just_const alphas; |
|
1015 |
in list_comb (subst_atomic_types (betas ~~ option_tys) map_F, somes) end; |
|
1016 |
||
1017 |
fun mk_set_F'_tm typ_a set_F = |
|
1018 |
let |
|
1019 |
val typ_aset = HOLogic.mk_setT typ_a; |
|
1020 |
||
1021 |
(* set_F' x = (\<Inter>y\<in>{y. REL (map_F Just x) y}. UNION (set_F y) set_Maybe) *) |
|
1022 |
val sbind = mk_UNION (subst_Maybe alphas set_F $ var_mx) (set_Maybe_const typ_a); |
|
1023 |
val collection = HOLogic.Collect_const typ_MaybeF $ absfree (dest_Free var_mx) |
|
1024 |
(subst_Maybe alphas equiv_rel_a $ (map_F_Just $ var_x) $ var_mx); |
|
1025 |
val set_F'_tm = lambda var_x |
|
1026 |
(Inf_const typ_aset $ (mk_image (absfree (dest_Free var_mx) sbind) $ collection)); |
|
1027 |
in |
|
1028 |
set_F'_tm |
|
1029 |
end |
|
1030 |
||
1031 |
val sets = mk_sets_of_bnf (replicate live deads) (replicate live alphas) bnf_F; |
|
1032 |
val sets' = map2 mk_set_F'_tm alphas sets; |
|
1033 |
||
1034 |
val (Iwits, wit_goals) = |
|
1035 |
prepare_wits true repT wits opts alphas wits_F var_as var_as' sets' lthy; |
|
1036 |
||
71354
c71a44893645
eliminated one redundant proof obligation in lift_bnf for quotients
traytel
parents:
71262
diff
changeset
|
1037 |
val goals = rel_pos_distr :: rel_Inters @ |
71262 | 1038 |
(case wits of NONE => [] | _ => wit_goals); |
1039 |
||
1040 |
val plugins = |
|
1041 |
get_first (fn Plugins_Option f => SOME (f lthy) | _ => NONE) (rev opts) |> |
|
1042 |
the_default Plugin_Name.default_filter; |
|
1043 |
||
1044 |
fun after_qed thmss lthy = |
|
71354
c71a44893645
eliminated one redundant proof obligation in lift_bnf for quotients
traytel
parents:
71262
diff
changeset
|
1045 |
(case thmss of [rel_pos_distr_thm0] :: thmss => |
71262 | 1046 |
let |
1047 |
val equiv_thm' = REL_rewr_all lthy equiv_thm; |
|
1048 |
val rel_pos_distr_thm = |
|
1049 |
@{thm equivp_add_relconj} OF [equiv_thm', equiv_thm', rel_pos_distr_thm0]; |
|
1050 |
||
1051 |
val (rel_Inter_thms, wit_thmss) = apply2 (fn f => flat (f live thmss)) (take, drop); |
|
1052 |
||
1053 |
(* construct map_G, sets_G, bd_G, rel_G and wits_G *) |
|
1054 |
||
1055 |
(* map_G f = abs_G o map_F f o rep_G *) |
|
1056 |
val map_G = fold_rev lambda var_fs (HOLogic.mk_comp (HOLogic.mk_comp |
|
1057 |
(subst_Ts abs_G betas, list_comb (map_F, var_fs)), rep_G)); |
|
1058 |
val map_raw = fold_rev lambda var_fs (list_comb (map_F, var_fs)) |
|
1059 |
|> subst_atomic_types (betas ~~ gammas); |
|
1060 |
||
1061 |
(* Define set_G and the three auxiliary definitions (set_F', F_in, F_in') *) |
|
1062 |
fun mk_set_G var_A set_F lthy = let |
|
1063 |
val typ_a = HOLogic.dest_setT (fastype_of var_A); |
|
1064 |
val set_F'_tm = mk_set_F'_tm typ_a set_F |
|
1065 |
||
1066 |
val (set_F', lthy) = define lthy (suffix set_F "'") 1 set_F'_tm; |
|
1067 |
||
1068 |
(* set_G = set_F' o rep_G *) |
|
1069 |
val set_G = HOLogic.mk_comp (#tm set_F', rep_G); |
|
1070 |
||
1071 |
(* F_in A = {x. set_F x \<subseteq> A} *) |
|
1072 |
val F_in_tm = lambda var_A (mk_in [var_A] [set_F] typ_aF); |
|
1073 |
val (F_in, lthy) = define lthy (suffix set_F "_in") 1 F_in_tm; |
|
1074 |
||
1075 |
(* F_in' A = map_F Inr -` ({(x, y). REL x y} `` F_in (insert (Inl ()) (Inr ` A))) *) |
|
1076 |
val F_in' = lambda var_A (mk_vimage map_F_Just (Image_const typ_MaybeF $ |
|
1077 |
subst_Maybe alphas rel_pairs $ (subst_Maybe alphas (#tm F_in) $ mk_insert |
|
1078 |
(mk_Nothing typ_a) (mk_image (Just_const typ_a) $ var_A)))); |
|
1079 |
val (F_in', lthy) = define lthy (suffix set_F "_in'") 1 F_in'; |
|
1080 |
||
1081 |
in ((set_G, {set_F'=set_F', F_in=F_in, F_in'=F_in'}), lthy) end; |
|
1082 |
||
1083 |
val ((sets_G, set_F'_aux_defs), lthy) = |
|
1084 |
@{fold_map 2} mk_set_G var_As sets_F lthy |>> split_list; |
|
1085 |
||
1086 |
(* bd_G = bd_F *) |
|
1087 |
val bd_G = mk_bd_of_bnf deads alphas bnf_F; |
|
1088 |
||
1089 |
(* rel_F' A = |
|
1090 |
BNF_Def.vimage2p (map_F Just) (map_F Just) ((\<cong>) OO rel_F (rel_Maybe A) OO (\<cong>)) *) |
|
1091 |
val rel_Maybes = @{map 3} (fn v => fn aT => fn bT => rel_Maybe_const aT bT $ v); |
|
1092 |
val rel_F'_tm = let val equiv_equiv_rel_option = subst_Ts equiv_rel_a' o map mk_MaybeT in |
|
1093 |
mk_vimage2p map_F_Just (subst_atomic_types (alphas ~~ betas) map_F_Just) $ |
|
1094 |
mk_OO [equiv_equiv_rel_option alphas, list_comb (rel_F_option, rel_Maybes var_Ps alphas betas)] |
|
1095 |
(equiv_equiv_rel_option betas) end; |
|
1096 |
||
1097 |
val (rel_F', lthy) = |
|
1098 |
define lthy (suffix rel_F_ab "'") (live+2) (fold_rev lambda var_Ps rel_F'_tm); |
|
1099 |
||
1100 |
(* rel_G A = vimage2p rep_G rep_G (rel_F' A) *) |
|
1101 |
val rel_G = fold_rev lambda var_Ps (mk_vimage2p rep_G (subst_Ts rep_G betas) $ rel_F'_tm); |
|
1102 |
val rel_raw = fold_rev lambda var_Ps rel_F'_tm |
|
1103 |
|> subst_atomic_types (betas ~~ gammas); |
|
1104 |
||
1105 |
(* auxiliary lemmas *) |
|
1106 |
val bd_card_order = bd_card_order_of_bnf bnf_F; |
|
1107 |
val bd_cinfinite = bd_cinfinite_of_bnf bnf_F; |
|
1108 |
val in_rel = in_rel_of_bnf bnf_F; |
|
1109 |
val map_F_comp = map_comp_of_bnf bnf_F; |
|
1110 |
val map_F_comp0 = map_comp0_of_bnf bnf_F; |
|
1111 |
val map_F_cong = map_cong_of_bnf bnf_F; |
|
1112 |
val map_F_id0 = map_id0_of_bnf bnf_F; |
|
1113 |
val map_F_id = map_id_of_bnf bnf_F; |
|
1114 |
val rel_conversep = rel_conversep_of_bnf bnf_F; |
|
71354
c71a44893645
eliminated one redundant proof obligation in lift_bnf for quotients
traytel
parents:
71262
diff
changeset
|
1115 |
val rel_flip = rel_flip_of_bnf bnf_F; |
c71a44893645
eliminated one redundant proof obligation in lift_bnf for quotients
traytel
parents:
71262
diff
changeset
|
1116 |
val rel_eq_onp = rel_eq_onp_of_bnf bnf_F; |
71262 | 1117 |
val rel_Grp = rel_Grp_of_bnf bnf_F; |
1118 |
val rel_OO = rel_OO_of_bnf bnf_F; |
|
1119 |
val rel_map = rel_map_of_bnf bnf_F; |
|
1120 |
val rel_refl_strong = rel_refl_strong_of_bnf bnf_F; |
|
1121 |
val set_bd_thms = set_bd_of_bnf bnf_F; |
|
1122 |
val set_map_thms = set_map_of_bnf bnf_F; |
|
1123 |
||
71354
c71a44893645
eliminated one redundant proof obligation in lift_bnf for quotients
traytel
parents:
71262
diff
changeset
|
1124 |
|
c71a44893645
eliminated one redundant proof obligation in lift_bnf for quotients
traytel
parents:
71262
diff
changeset
|
1125 |
|
c71a44893645
eliminated one redundant proof obligation in lift_bnf for quotients
traytel
parents:
71262
diff
changeset
|
1126 |
(* map_F_respect: @{term "((=) ===> REL ===> REL) map_F map_F"} *) |
c71a44893645
eliminated one redundant proof obligation in lift_bnf for quotients
traytel
parents:
71262
diff
changeset
|
1127 |
val map_F_respect = HOLogic.mk_Trueprop (fold_rev mk_rel_fun (map2 (fn xT => fn yT => |
c71a44893645
eliminated one redundant proof obligation in lift_bnf for quotients
traytel
parents:
71262
diff
changeset
|
1128 |
HOLogic.eq_const (xT --> yT)) alphas betas @ [equiv_rel_a]) (equiv_rel_b) $ map_F $ map_F); |
c71a44893645
eliminated one redundant proof obligation in lift_bnf for quotients
traytel
parents:
71262
diff
changeset
|
1129 |
|
c71a44893645
eliminated one redundant proof obligation in lift_bnf for quotients
traytel
parents:
71262
diff
changeset
|
1130 |
fun map_F_respect_tac ctxt = |
c71a44893645
eliminated one redundant proof obligation in lift_bnf for quotients
traytel
parents:
71262
diff
changeset
|
1131 |
HEADGOAL (EVERY' |
c71a44893645
eliminated one redundant proof obligation in lift_bnf for quotients
traytel
parents:
71262
diff
changeset
|
1132 |
[REPEAT_DETERM_N (live + 1) o rtac ctxt @{thm rel_funI}, hyp_subst_tac ctxt, |
c71a44893645
eliminated one redundant proof obligation in lift_bnf for quotients
traytel
parents:
71262
diff
changeset
|
1133 |
rtac ctxt (BNF_FP_Util.split_conj_prems live rel_pos_distr_thm0 OF |
c71a44893645
eliminated one redundant proof obligation in lift_bnf for quotients
traytel
parents:
71262
diff
changeset
|
1134 |
replicate live @{thm Grp_conversep_nonempty} RS rev_mp), |
c71a44893645
eliminated one redundant proof obligation in lift_bnf for quotients
traytel
parents:
71262
diff
changeset
|
1135 |
rtac ctxt impI, dtac ctxt @{thm predicate2D}, etac ctxt @{thm relcomppI2[rotated]}, |
c71a44893645
eliminated one redundant proof obligation in lift_bnf for quotients
traytel
parents:
71262
diff
changeset
|
1136 |
rtac ctxt (rel_Grp RS @{thm predicate2_eqD} RS iffD2), rtac ctxt @{thm GrpI[OF refl]}, |
c71a44893645
eliminated one redundant proof obligation in lift_bnf for quotients
traytel
parents:
71262
diff
changeset
|
1137 |
REPEAT_DETERM o resolve_tac ctxt [CollectI, conjI, subset_UNIV], |
c71a44893645
eliminated one redundant proof obligation in lift_bnf for quotients
traytel
parents:
71262
diff
changeset
|
1138 |
rtac ctxt (rel_flip RS iffD2), |
c71a44893645
eliminated one redundant proof obligation in lift_bnf for quotients
traytel
parents:
71262
diff
changeset
|
1139 |
rtac ctxt (rel_Grp RS @{thm predicate2_eqD} RS iffD2), rtac ctxt @{thm GrpI[OF refl]}, |
c71a44893645
eliminated one redundant proof obligation in lift_bnf for quotients
traytel
parents:
71262
diff
changeset
|
1140 |
REPEAT_DETERM o resolve_tac ctxt [CollectI, conjI, subset_UNIV], |
c71a44893645
eliminated one redundant proof obligation in lift_bnf for quotients
traytel
parents:
71262
diff
changeset
|
1141 |
SELECT_GOAL (unfold_thms_tac ctxt (rel_eq_onp :: @{thms Grp_conversep_eq_onp})), |
c71a44893645
eliminated one redundant proof obligation in lift_bnf for quotients
traytel
parents:
71262
diff
changeset
|
1142 |
etac ctxt @{thm predicate2D[OF rel_conj_eq_onp, rotated]}, |
c71a44893645
eliminated one redundant proof obligation in lift_bnf for quotients
traytel
parents:
71262
diff
changeset
|
1143 |
rtac ctxt equiv_thm']); |
c71a44893645
eliminated one redundant proof obligation in lift_bnf for quotients
traytel
parents:
71262
diff
changeset
|
1144 |
|
c71a44893645
eliminated one redundant proof obligation in lift_bnf for quotients
traytel
parents:
71262
diff
changeset
|
1145 |
val map_F_respect_thm = prove lthy [] map_F_respect map_F_respect_tac; |
c71a44893645
eliminated one redundant proof obligation in lift_bnf for quotients
traytel
parents:
71262
diff
changeset
|
1146 |
|
71262 | 1147 |
val rel_funD = mk_rel_funDN (live+1); |
1148 |
val map_F_rsp = (rel_funD map_F_respect_thm) OF (replicate live refl); |
|
1149 |
fun map_F_rsp_of tms ctxt = (infer_instantiate' ctxt (NONE :: NONE |
|
1150 |
:: map (SOME o Thm.cterm_of ctxt) tms) map_F_rsp) |
|
1151 |
||
1152 |
val qthms = let |
|
1153 |
fun equivp_THEN thm = REL_rewr_all lthy equiv_thm RS thm; |
|
1154 |
fun Quotient3_THEN thm = REL_rewr_all lthy quot_thm RS thm; |
|
1155 |
in |
|
1156 |
{abs_rep = Quotient3_THEN @{thm Quotient3_abs_rep}, |
|
1157 |
rel_abs = Quotient3_THEN @{thm Quotient3_rel_abs}, |
|
1158 |
rep_abs = Quotient3_THEN @{thm Quotient3_rep_abs}, |
|
1159 |
rep_reflp = Quotient3_THEN @{thm Quotient3_rep_reflp}, |
|
1160 |
rep_abs_rsp = Quotient3_THEN @{thm rep_abs_rsp}, |
|
1161 |
reflp = equivp_THEN @{thm equivp_reflp}, |
|
1162 |
symp = equivp_THEN @{thm equivp_symp}, |
|
1163 |
transp = equivp_THEN @{thm equivp_transp}, |
|
1164 |
REL = REL_def} |
|
1165 |
end; |
|
1166 |
||
1167 |
(* lemma REL_OO_REL_left: REL OO REL OO R = REL OO R *) |
|
1168 |
val REL_OO_REL_left_thm = let |
|
1169 |
val tm = mk_Trueprop_eq |
|
1170 |
(mk_OO [equiv_rel_a, equiv_rel_a] var_R, mk_relcompp equiv_rel_a var_R) |
|
1171 |
fun tac ctxt = HEADGOAL (EVERY' |
|
1172 |
[rtac ctxt ext, |
|
1173 |
rtac ctxt ext, |
|
1174 |
rtac ctxt iffI, |
|
1175 |
TWICE (etac ctxt @{thm relcomppE}), |
|
1176 |
rtac ctxt @{thm relcomppI}, |
|
1177 |
etac ctxt (#transp qthms), |
|
1178 |
TWICE (assume_tac ctxt), |
|
1179 |
etac ctxt @{thm relcomppE}, |
|
1180 |
etac ctxt @{thm relcomppI}, |
|
1181 |
rtac ctxt @{thm relcomppI}, |
|
1182 |
rtac ctxt (#reflp qthms), |
|
1183 |
assume_tac ctxt]); |
|
1184 |
in prove lthy [var_R] tm tac end; |
|
1185 |
||
1186 |
(* Generate theorems related to the setters *) |
|
1187 |
val map_F_fs = list_comb (map_F, var_fs); |
|
1188 |
||
1189 |
(* aset aset asetset bset typ_b typ_b *) |
|
1190 |
fun mk_set_F'_thmss (((((var_A, var_A'), var_S), var_B), var_b), var_b') |
|
1191 |
set_F {set_F', F_in, F_in'} rel_Inter_thm set_map_F_thm (idx, vf) = |
|
1192 |
let |
|
1193 |
val (var_f, var_fs') = case vf of |
|
1194 |
(f :: fs) => (f, fs) |
|
1195 |
| _ => error "won't happen"; |
|
1196 |
||
1197 |
val typ_a = fastype_of var_f |> dest_funT |> fst; |
|
1198 |
val typ_b = fastype_of var_b; |
|
1199 |
val (typ_asetset, typ_aset) = `HOLogic.mk_setT (fastype_of var_A); |
|
1200 |
||
1201 |
val map_F_fs_x = map_F_fs $ var_x; |
|
1202 |
||
1203 |
(* F_in'_mono: A \<subseteq> B \<Longrightarrow> F_in' A \<subseteq> F_in' B *) |
|
1204 |
val F_in'_mono_tm = mk_Trueprop_implies |
|
1205 |
([mk_leq var_A var_A'], mk_leq (#tm F_in' $ var_A) (#tm F_in' $ var_A')); |
|
1206 |
fun F_in'_mono_tac ctxt = |
|
1207 |
unfold_thms_tac ctxt [#def F_in', #def F_in] THEN |
|
1208 |
HEADGOAL (EVERY' |
|
1209 |
[rtac ctxt subsetI, |
|
1210 |
etac ctxt vimageE, |
|
1211 |
etac ctxt @{thm ImageE}, |
|
1212 |
etac ctxt CollectE, |
|
1213 |
etac ctxt CollectE, |
|
1214 |
dtac ctxt @{thm case_prodD}, |
|
1215 |
hyp_subst_tac ctxt, |
|
1216 |
rtac ctxt (vimageI OF [refl]), |
|
1217 |
rtac ctxt @{thm ImageI}, |
|
1218 |
rtac ctxt CollectI, |
|
1219 |
rtac ctxt @{thm case_prodI}, |
|
1220 |
assume_tac ctxt ORELSE' rtac ctxt refl, |
|
1221 |
rtac ctxt CollectI, |
|
1222 |
etac ctxt subset_trans, |
|
1223 |
etac ctxt (@{thm insert_mono} OF [@{thm image_mono}])]); |
|
1224 |
val F_in'_mono_thm = prove lthy [var_A, var_A'] F_in'_mono_tm F_in'_mono_tac; |
|
1225 |
||
1226 |
(* F_in'_Inter: F_in' (\<Inter>S) = (\<Inter>A\<in>S. F_in' A) *) |
|
1227 |
val F_in'_Inter_tm = mk_Trueprop_eq ((#tm F_in' $ (Inf_const typ_aset $ var_S)), |
|
1228 |
(Inf_const (HOLogic.mk_setT typ_aF) $ (mk_image (#tm F_in') $ var_S))); |
|
1229 |
fun F_in'_Inter_tac ctxt = |
|
1230 |
Local_Defs.unfold_tac ctxt [#def F_in', #def F_in] |
|
1231 |
THEN HEADGOAL (rtac ctxt (infer_instantiate' ctxt |
|
1232 |
[SOME (Thm.cterm_of ctxt (HOLogic.mk_eq (var_S, bot_const typ_asetset)))] @{thm case_split}) |
|
1233 |
THEN' EVERY' [ |
|
1234 |
hyp_subst_tac ctxt, |
|
1235 |
SELECT_GOAL |
|
1236 |
(unfold_thms_tac ctxt @{thms Inter_empty INT_empty UNIV_sum_unit_conv}), |
|
1237 |
rtac ctxt @{thm set_eqI}, |
|
1238 |
rtac ctxt iffI, |
|
1239 |
rtac ctxt UNIV_I, |
|
1240 |
rtac ctxt (vimageI OF [refl]), |
|
1241 |
rtac ctxt @{thm ImageI}, |
|
1242 |
rtac ctxt CollectI, |
|
1243 |
rtac ctxt @{thm case_prodI}, |
|
1244 |
rtac ctxt (#reflp qthms), |
|
1245 |
rtac ctxt CollectI, |
|
1246 |
rtac ctxt subset_UNIV, |
|
1247 |
etac ctxt @{thm exE[OF ex_in_conv[THEN iffD2]]}, |
|
1248 |
EqSubst.eqsubst_tac ctxt [0] @{thms image_INT[of _ UNIV _ id, simplified]}, |
|
1249 |
rtac ctxt @{thm inj_Inr}, |
|
1250 |
assume_tac ctxt, |
|
1251 |
SELECT_GOAL (unfold_thms_tac ctxt @{thms INT_extend_simps vimage_INT[symmetric]}), |
|
1252 |
rtac ctxt @{thm arg_cong2[where f=vimage, OF refl]}, |
|
1253 |
rtac ctxt equalityI, |
|
1254 |
rtac ctxt subsetI, |
|
1255 |
rtac ctxt @{thm InterI}, |
|
1256 |
etac ctxt imageE, |
|
1257 |
etac ctxt @{thm ImageE}, |
|
1258 |
etac ctxt CollectE, |
|
1259 |
etac ctxt CollectE, |
|
1260 |
dtac ctxt @{thm case_prodD}, |
|
1261 |
hyp_subst_tac ctxt, |
|
1262 |
rtac ctxt @{thm ImageI[OF CollectI]}, |
|
1263 |
etac ctxt @{thm case_prodI} ORELSE' (SELECT_GOAL |
|
1264 |
(unfold_thms_tac ctxt @{thms prod.case}) THEN' rtac ctxt @{thm refl}), |
|
1265 |
rtac ctxt CollectI, |
|
1266 |
etac ctxt subset_trans, |
|
1267 |
etac ctxt @{thm INT_lower[OF imageI]}, |
|
1268 |
rtac ctxt (@{thm subset_trans} OF [asm_rl, rel_Inter_thm]), |
|
1269 |
K (unfold_thms_tac ctxt @{thms image_image}), |
|
1270 |
rtac ctxt subset_refl, |
|
1271 |
K (unfold_thms_tac ctxt @{thms INT_extend_simps ex_in_conv[symmetric]}), |
|
1272 |
rtac ctxt exI, |
|
1273 |
rtac ctxt imageI, |
|
1274 |
assume_tac ctxt, |
|
1275 |
rtac ctxt exI, |
|
1276 |
rtac ctxt @{thm InterI}, |
|
1277 |
etac ctxt imageE, |
|
1278 |
hyp_subst_tac ctxt, |
|
1279 |
rtac ctxt @{thm insertI1}]); |
|
1280 |
||
1281 |
val F_in'_Inter_thm = prove lthy [var_S] F_in'_Inter_tm F_in'_Inter_tac; |
|
1282 |
||
1283 |
(* set_F'_respect: (REL ===> (=)) set_F' set_F' *) |
|
1284 |
val set_F'_respect_tm = HOLogic.mk_Trueprop (mk_rel_fun equiv_rel_a |
|
1285 |
(HOLogic.eq_const typ_aset) $ #tm set_F' $ #tm set_F'); |
|
1286 |
fun set_F'_respect_tac ctxt = unfold_thms_tac ctxt (#def set_F' :: @{thms rel_fun_def}) |
|
1287 |
THEN HEADGOAL (EVERY' |
|
1288 |
[TWICE (rtac ctxt allI), |
|
1289 |
rtac ctxt impI, |
|
1290 |
dtac ctxt (map_F_rsp_of (map Just_const alphas) ctxt), |
|
1291 |
rtac ctxt @{thm INF_cong}, |
|
1292 |
rtac ctxt @{thm Collect_eqI}, |
|
1293 |
rtac ctxt iffI, |
|
1294 |
etac ctxt (#transp qthms OF [#symp qthms]), |
|
1295 |
assume_tac ctxt, |
|
1296 |
etac ctxt (#transp qthms), |
|
1297 |
assume_tac ctxt, |
|
1298 |
rtac ctxt refl]); |
|
1299 |
||
1300 |
(* F_in'_alt2: F_in' A = {x. set_F' x \<subseteq> A} *) |
|
1301 |
val F_in'_alt2_tm = mk_Trueprop_eq |
|
1302 |
(#tm F_in' $ var_A, mk_in [var_A] [#tm set_F'] typ_aF); |
|
1303 |
fun F_in'_alt2_tac ctxt = HEADGOAL (rtac ctxt equalityI THEN' |
|
1304 |
(Subgoal.FOCUS o K) (unfold_thms_tac ctxt (map #def [set_F', F_in', F_in])) ctxt |
|
1305 |
THEN' EVERY' |
|
1306 |
[rtac ctxt subsetI, |
|
1307 |
rtac ctxt CollectI, |
|
1308 |
rtac ctxt subsetI, |
|
1309 |
dtac ctxt vimageD, |
|
1310 |
etac ctxt @{thm ImageE}, |
|
1311 |
etac ctxt CollectE, |
|
1312 |
etac ctxt CollectE, |
|
1313 |
dtac ctxt @{thm case_prodD}, |
|
1314 |
dtac ctxt @{thm InterD}, |
|
1315 |
rtac ctxt @{thm imageI[OF CollectI]}, |
|
1316 |
etac ctxt (#symp qthms), |
|
1317 |
etac ctxt @{thm UnionE}, |
|
1318 |
etac ctxt imageE, |
|
1319 |
hyp_subst_tac ctxt, |
|
1320 |
etac ctxt @{thm subset_lift_sum_unitD}, |
|
1321 |
etac ctxt @{thm setr.cases}, |
|
1322 |
hyp_subst_tac ctxt, |
|
1323 |
assume_tac ctxt]) |
|
1324 |
THEN unfold_thms_tac ctxt [#def set_F'] THEN |
|
1325 |
(HEADGOAL o EVERY') |
|
1326 |
[rtac ctxt subsetI, |
|
1327 |
etac ctxt CollectE, |
|
1328 |
etac ctxt (subsetD OF [F_in'_mono_thm]), |
|
1329 |
EqSubst.eqsubst_tac ctxt [0] [F_in'_Inter_thm], |
|
1330 |
rtac ctxt @{thm InterI}] THEN |
|
1331 |
REPEAT_DETERM (HEADGOAL (etac ctxt @{thm imageE} THEN' hyp_subst_tac ctxt)) THEN |
|
1332 |
(HEADGOAL o EVERY') |
|
1333 |
[etac ctxt CollectE, |
|
1334 |
SELECT_GOAL (unfold_thms_tac ctxt (map #def [F_in', F_in])), |
|
1335 |
rtac ctxt @{thm vimageI[OF refl]}, |
|
1336 |
rtac ctxt @{thm ImageI}, |
|
1337 |
rtac ctxt CollectI, |
|
1338 |
rtac ctxt @{thm case_prodI}, |
|
1339 |
etac ctxt (#symp qthms), |
|
1340 |
rtac ctxt CollectI, |
|
1341 |
rtac ctxt subsetI, |
|
1342 |
rtac ctxt @{thm sum_insert_Inl_unit}, |
|
1343 |
assume_tac ctxt, |
|
1344 |
hyp_subst_tac ctxt, |
|
1345 |
rtac ctxt imageI, |
|
1346 |
rtac ctxt @{thm UnionI}, |
|
1347 |
rtac ctxt imageI, |
|
1348 |
assume_tac ctxt, |
|
1349 |
rtac ctxt @{thm setr.intros[OF refl]}]; |
|
1350 |
val F_in'_alt2_thm = prove lthy [var_A] F_in'_alt2_tm F_in'_alt2_tac; |
|
1351 |
||
1352 |
(* set_F'_alt: set_F' x = \<Inter>{A. x \<in> F_in' A} *) |
|
1353 |
val set_F'_alt_tm = mk_Trueprop_eq (#tm set_F' $ var_x, |
|
1354 |
Inf_const typ_aset $ mk_Collect (var_A, HOLogic.mk_mem (var_x, #tm F_in' $ var_A))); |
|
1355 |
fun set_F'_alt_tac ctxt = unfold_thms_tac ctxt [F_in'_alt2_thm] |
|
1356 |
THEN HEADGOAL (EVERY' |
|
1357 |
[rtac ctxt @{thm set_eqI}, |
|
1358 |
rtac ctxt iffI, |
|
1359 |
rtac ctxt @{thm InterI}, |
|
1360 |
etac ctxt CollectE, |
|
1361 |
etac ctxt CollectE, |
|
1362 |
dtac ctxt subsetD, |
|
1363 |
assume_tac ctxt, |
|
1364 |
assume_tac ctxt, |
|
1365 |
etac ctxt @{thm InterD}, |
|
1366 |
rtac ctxt CollectI, |
|
1367 |
rtac ctxt CollectI, |
|
1368 |
rtac ctxt subset_refl]); |
|
1369 |
val set_F'_alt_thm = prove lthy [var_x] set_F'_alt_tm set_F'_alt_tac; |
|
1370 |
||
1371 |
(* map_F_in_F_in'I: x \<in> F_in' B \<Longrightarrow> map_F f x \<in> F_in' (f ` B) *) |
|
1372 |
val map_F_in_F_in'I_tm = mk_Trueprop_implies ([HOLogic.mk_mem (var_x, #tm F_in' $ var_A')], |
|
1373 |
HOLogic.mk_mem (map_F_fs_x, subst_b (#tm F_in') $ (mk_image var_f $ var_A'))); |
|
1374 |
fun map_F_in_F_in'I_tac ctxt = |
|
1375 |
Local_Defs.unfold_tac ctxt ([#def F_in', #def F_in, Bex_def] @ @{thms vimage_def Image_iff}) THEN |
|
1376 |
HEADGOAL (EVERY' |
|
1377 |
[etac ctxt @{thm CollectE}, |
|
1378 |
etac ctxt exE, |
|
1379 |
etac ctxt conjE, |
|
1380 |
etac ctxt @{thm CollectE}, |
|
1381 |
etac ctxt @{thm CollectE}, |
|
1382 |
dtac ctxt @{thm case_prodD}, |
|
1383 |
rtac ctxt @{thm CollectI}, |
|
1384 |
rtac ctxt exI, |
|
1385 |
rtac ctxt @{thm conjI[rotated]}, |
|
1386 |
rtac ctxt @{thm CollectI}, |
|
1387 |
rtac ctxt @{thm case_prodI}, |
|
1388 |
dtac ctxt (map_F_rsp_of (map mk_Maybe_map var_fs) ctxt), |
|
1389 |
SELECT_GOAL (unfold_thms_tac ctxt (map_F_comp :: @{thms o_def map_sum.simps})), |
|
1390 |
assume_tac ctxt, |
|
1391 |
rtac ctxt CollectI, |
|
1392 |
SELECT_GOAL (unfold_thms_tac ctxt set_map_thms), |
|
1393 |
etac ctxt @{thm image_map_sum_unit_subset}]); |
|
1394 |
val map_F_in_F_in'I_thm = |
|
1395 |
prove lthy (var_A' :: var_x :: var_fs) map_F_in_F_in'I_tm map_F_in_F_in'I_tac; |
|
1396 |
||
1397 |
(* REL_preimage_eq: C \<inter> range f \<noteq> {} \<Longrightarrow> |
|
1398 |
{(a, b). REL a b} `` {x. set_F x \<subseteq> f -` C} = |
|
1399 |
map_F f -` {(a, b). REL a b} `` {x. set_F x \<subseteq> C} *) |
|
1400 |
val REL_preimage_eq_tm = mk_Trueprop_implies ([HOLogic.mk_not (HOLogic.mk_eq |
|
1401 |
(HOLogic.mk_binop @{const_name inf} (var_B, mk_image var_f $ HOLogic.mk_UNIV typ_a), |
|
1402 |
bot_const (HOLogic.mk_setT typ_b)))], HOLogic.mk_eq (Image_const typ_aF $ |
|
1403 |
rel_pairs $ mk_in [mk_vimage var_f var_B] [set_F] typ_aF, mk_vimage map_F_fs |
|
1404 |
(Image_const typ_bF $ subst_b rel_pairs $ mk_in [var_B] [subst_b set_F] typ_bF))); |
|
1405 |
||
1406 |
(* Bs \<inter> range fs \<noteq> {} \<Longrightarrow> set_F xb \<subseteq> Bs \<Longrightarrow> REL xb (map_F fs x) |
|
1407 |
\<Longrightarrow> x \<in> {(x, x'). REL x x'} `` {x. set_F x \<subseteq> fs -` Bs} *) |
|
1408 |
fun subgoal_tac {context = ctxt, params, ...} = let |
|
1409 |
val (x, y) = case params of |
|
1410 |
[(_, x), _, (_, y)] => (x, y) |
|
1411 |
| _ => error "won't happen"; |
|
1412 |
val cond = HOLogic.mk_conj (apply2 HOLogic.mk_mem ((var_b, var_B), (var_b', var_B))); |
|
1413 |
||
1414 |
(* ["\<lambda>x y. x \<in> B \<and> y \<in> B", "(Grp UNIV f_1)\<inverse>\<inverse>"] *) |
|
1415 |
val cvars = var_fs |> maps (fn f => let val fT = fastype_of f in |
|
1416 |
map (SOME o Thm.cterm_of ctxt) |
|
1417 |
[if f = var_f then |
|
1418 |
fold_rev lambda [var_b, var_b'] cond else HOLogic.eq_const (range_type fT), |
|
1419 |
mk_conversep (mk_Grp (HOLogic.mk_UNIV (domain_type fT)) f)] end); |
|
1420 |
val rel_pos_distr_thm_inst = infer_instantiate' ctxt (cvars @ [SOME y,SOME x]) |
|
1421 |
(@{thm predicate2D} OF [rel_pos_distr_thm]); |
|
1422 |
||
1423 |
(* GrpI[of "map_F f1 .. fN" x, OF refl CollectI, OF "B1 \<subseteq> UNIV \<and> ... \<and> Bn \<subseteq> UNIV"] *) |
|
1424 |
fun subset_UNIVs n = fold (fn a => fn b => conjI OF [a, b]) (replicate (n-1) |
|
1425 |
@{thm subset_UNIV}) @{thm subset_UNIV}; |
|
1426 |
val GrpI_inst = infer_instantiate' ctxt (map SOME [Thm.cterm_of ctxt map_F_fs, x]) |
|
1427 |
@{thm GrpI} OF [refl, CollectI] OF [subset_UNIVs live]; |
|
1428 |
||
1429 |
in EVERY [ |
|
1430 |
HEADGOAL (Method.insert_tac ctxt [rel_pos_distr_thm_inst]), |
|
1431 |
unfold_thms_tac ctxt [rel_conversep, rel_OO, rel_Grp], |
|
1432 |
HEADGOAL (etac ctxt @{thm meta_impE}), |
|
1433 |
REPEAT_DETERM_N (live-1) (HEADGOAL (rtac ctxt @{thm conjI[rotated]})), |
|
1434 |
REPEAT_DETERM_N live (HEADGOAL (etac ctxt @{thm relcompp_mem_Grp_neq_bot} ORELSE' |
|
1435 |
rtac ctxt @{thm relcompp_eq_Grp_neq_bot})), |
|
1436 |
HEADGOAL (EVERY' [etac ctxt @{thm meta_impE}, |
|
1437 |
rtac ctxt @{thm relcomppI}, |
|
1438 |
rtac ctxt (#reflp qthms), |
|
1439 |
rtac ctxt @{thm relcomppI}, |
|
1440 |
rtac ctxt rel_refl_strong]), |
|
1441 |
REPEAT_DETERM_N idx (HEADGOAL (rtac ctxt refl)), |
|
1442 |
HEADGOAL (rtac ctxt conjI THEN' TWICE (etac ctxt subsetD THEN' assume_tac ctxt)), |
|
1443 |
REPEAT_DETERM_N (live-idx-1) (HEADGOAL (rtac ctxt refl)), |
|
1444 |
HEADGOAL (EVERY' |
|
1445 |
[rtac ctxt @{thm relcomppI}, |
|
1446 |
assume_tac ctxt, |
|
1447 |
rtac ctxt @{thm relcomppI}, |
|
1448 |
rtac ctxt @{thm conversepI}, |
|
1449 |
rtac ctxt GrpI_inst, |
|
1450 |
rtac ctxt (#reflp qthms), |
|
1451 |
etac ctxt @{thm relcomppE}, |
|
1452 |
etac ctxt @{thm relcomppE}, |
|
1453 |
etac ctxt @{thm relcomppE}, |
|
1454 |
etac ctxt @{thm conversepE}, |
|
1455 |
etac ctxt @{thm GrpE}, |
|
1456 |
hyp_subst_tac ctxt, |
|
1457 |
rtac ctxt @{thm ImageI}, |
|
1458 |
rtac ctxt CollectI, |
|
1459 |
rtac ctxt @{thm case_prodI}, |
|
1460 |
assume_tac ctxt, |
|
1461 |
EqSubst.eqsubst_asm_tac ctxt [1] rel_map, |
|
1462 |
EqSubst.eqsubst_asm_tac ctxt [1] [in_rel_of_bnf bnf_F], |
|
1463 |
etac ctxt exE, |
|
1464 |
etac ctxt CollectE, |
|
1465 |
etac ctxt conjE, |
|
1466 |
etac ctxt conjE, |
|
1467 |
etac ctxt CollectE, |
|
1468 |
hyp_subst_tac ctxt, |
|
1469 |
rtac ctxt CollectI]), |
|
1470 |
unfold_thms_tac ctxt set_map_thms, |
|
1471 |
HEADGOAL (rtac ctxt (subsetI OF [vimageI] OF [refl]) THEN' |
|
1472 |
etac ctxt @{thm imageE} THEN' hyp_subst_tac ctxt), |
|
1473 |
REPEAT_DETERM_N 6 (HEADGOAL (etac ctxt Drule.thin_rl)), |
|
1474 |
REPEAT_DETERM_N (live-1) (HEADGOAL (etac ctxt conjE)), |
|
1475 |
HEADGOAL (EVERY' [dtac ctxt subsetD, assume_tac ctxt, etac ctxt CollectE]), |
|
1476 |
unfold_thms_tac ctxt @{thms split_beta}, |
|
1477 |
HEADGOAL (etac ctxt conjunct2)] end; |
|
1478 |
||
1479 |
fun REL_preimage_eq_tac ctxt = HEADGOAL (EVERY' |
|
1480 |
[rtac ctxt @{thm set_eqI}, |
|
1481 |
rtac ctxt iffI, |
|
1482 |
etac ctxt @{thm ImageE}, |
|
1483 |
etac ctxt CollectE, |
|
1484 |
etac ctxt CollectE, |
|
1485 |
dtac ctxt @{thm case_prodD}, |
|
1486 |
rtac ctxt (vimageI OF [refl]), |
|
1487 |
rtac ctxt @{thm ImageI}, |
|
1488 |
rtac ctxt CollectI, |
|
1489 |
rtac ctxt @{thm case_prodI}, |
|
1490 |
etac ctxt map_F_rsp, |
|
1491 |
rtac ctxt CollectI, |
|
1492 |
EqSubst.eqsubst_tac ctxt [0] [set_map_F_thm], |
|
1493 |
etac ctxt @{thm subset_vimage_image_subset}, |
|
1494 |
etac ctxt vimageE, |
|
1495 |
etac ctxt @{thm ImageE}, |
|
1496 |
TWICE (etac ctxt CollectE), |
|
1497 |
dtac ctxt @{thm case_prodD}, |
|
1498 |
hyp_subst_tac ctxt, |
|
1499 |
Subgoal.FOCUS_PARAMS subgoal_tac ctxt]); |
|
1500 |
||
1501 |
val REL_preimage_eq_thm = prove lthy (var_B :: var_fs) REL_preimage_eq_tm REL_preimage_eq_tac; |
|
1502 |
||
1503 |
(* set_map_F': set_F' (map_F f x) = f ` set_F' x *) |
|
1504 |
val set_map_F'_tm = mk_Trueprop_eq (subst_b (#tm set_F') |
|
1505 |
$ map_F_fs_x, mk_image var_f $ (#tm set_F' $ var_x)); |
|
1506 |
fun set_map_F'_tac ctxt = HEADGOAL (EVERY' |
|
1507 |
[rtac ctxt @{thm set_eqI}, |
|
1508 |
rtac ctxt iffI, |
|
1509 |
EqSubst.eqsubst_asm_tac ctxt [0] [set_F'_alt_thm], |
|
1510 |
etac ctxt @{thm InterD}, |
|
1511 |
rtac ctxt CollectI, |
|
1512 |
rtac ctxt map_F_in_F_in'I_thm, |
|
1513 |
SELECT_GOAL (unfold_thms_tac ctxt [F_in'_alt2_thm]), |
|
1514 |
rtac ctxt CollectI, |
|
1515 |
rtac ctxt subset_refl, |
|
1516 |
SELECT_GOAL (unfold_thms_tac ctxt [set_F'_alt_thm]), |
|
1517 |
rtac ctxt @{thm InterI}, |
|
1518 |
etac ctxt imageE, |
|
1519 |
etac ctxt CollectE, |
|
1520 |
hyp_subst_tac ctxt, |
|
1521 |
etac ctxt @{thm vimageD[OF InterD]}, |
|
1522 |
rtac ctxt CollectI]) THEN |
|
1523 |
(* map_F f x \<in> F_in' X \<Longrightarrow> x \<in> F_in' (f -` X) *) |
|
1524 |
HEADGOAL (Subgoal.FOCUS_PARAMS (fn {context = ctxt, params, ...} => |
|
1525 |
let |
|
1526 |
val X = nth params 1 |> snd |> Thm.term_of; |
|
1527 |
val Inr_img = mk_image (Just_const (HOLogic.dest_setT (fastype_of X))) $ X; |
|
1528 |
fun cvars_of ctxt = map (SOME o Thm.cterm_of ctxt); |
|
1529 |
val cut_thm = infer_instantiate' ctxt (cvars_of ctxt [Inr_img, var_f]) |
|
1530 |
@{thm insert_Inl_int_map_sum_unit}; |
|
1531 |
val preimage_thm = infer_instantiate' ctxt (cvars_of ctxt |
|
1532 |
(filter (fn f => var_f <> f) var_fs |> map mk_Maybe_map)) |
|
1533 |
(cut_thm RS REL_preimage_eq_thm); |
|
1534 |
in EVERY [ |
|
1535 |
unfold_thms_tac ctxt (map #def [F_in', F_in] @ preimage_thm :: map_F_comp :: |
|
1536 |
@{thms lift_sum_unit_vimage_commute vimage_comp o_def map_sum.simps}), |
|
1537 |
unfold_thms_tac ctxt [@{thm o_def[symmetric]}, map_F_comp0], |
|
1538 |
Local_Defs.fold_tac ctxt @{thms vimage_comp}, |
|
1539 |
HEADGOAL (etac ctxt (vimageI OF [refl]))] end) ctxt); |
|
1540 |
||
1541 |
(* set_F'_subset: set_F' x \<subseteq> set_F x *) |
|
1542 |
val set_F'_subset_tm = HOLogic.mk_Trueprop (mk_leq (#tm set_F' $ var_x) (set_F $ var_x)); |
|
1543 |
fun set_F'_subset_tac ctxt = |
|
1544 |
let val int_e_thm = infer_instantiate' ctxt |
|
1545 |
(replicate 3 NONE @ [SOME (Thm.cterm_of ctxt (map_F_Just $ var_x))]) @{thm INT_E}; |
|
1546 |
in HEADGOAL (EVERY' [SELECT_GOAL (Local_Defs.unfold_tac ctxt [#def set_F']), |
|
1547 |
rtac ctxt subsetI, |
|
1548 |
etac ctxt int_e_thm, |
|
1549 |
SELECT_GOAL (unfold_thms_tac ctxt [set_map_F_thm]), |
|
1550 |
etac ctxt @{thm UN_E}, |
|
1551 |
etac ctxt imageE, |
|
1552 |
hyp_subst_tac ctxt, |
|
1553 |
SELECT_GOAL (unfold_thms_tac ctxt @{thms sum_set_simps singleton_iff}), |
|
1554 |
hyp_subst_tac ctxt, |
|
1555 |
assume_tac ctxt, |
|
1556 |
etac ctxt notE, |
|
1557 |
rtac ctxt CollectI, |
|
1558 |
rtac ctxt (#reflp qthms)]) |
|
1559 |
end; |
|
1560 |
in |
|
1561 |
({F_in'_mono = F_in'_mono_thm, |
|
1562 |
F_in'_Inter = F_in'_Inter_thm, |
|
1563 |
set_F'_respect = prove lthy [] set_F'_respect_tm set_F'_respect_tac, |
|
1564 |
F_in'_alt2 = F_in'_alt2_thm, |
|
1565 |
set_F'_alt = set_F'_alt_thm, |
|
1566 |
map_F_in_F_in'I = map_F_in_F_in'I_thm, |
|
1567 |
set_map_F' = prove lthy (var_x :: var_fs) set_map_F'_tm set_map_F'_tac, |
|
1568 |
set_F'_subset = prove lthy [var_x] set_F'_subset_tm set_F'_subset_tac, |
|
1569 |
set_F'_def = #def set_F', |
|
1570 |
F_in_def = #def F_in, |
|
1571 |
F_in'_def = #def F_in'}, (idx + 1, var_fs')) |
|
1572 |
end; |
|
1573 |
||
1574 |
val set_F'_thmss = @{fold_map 5} mk_set_F'_thmss |
|
1575 |
(var_As ~~ var_As' ~~ var_Ss ~~ var_Bs ~~ var_bs ~~ var_bs') sets_F set_F'_aux_defs |
|
1576 |
rel_Inter_thms set_map_thms (0, var_fs) |
|
1577 |
|> fst; |
|
1578 |
||
1579 |
(* F_in'D: x \<in> F_in' A \<Longrightarrow> \<forall>a\<in>A. f a = g a \<Longrightarrow> REL (map_F f x) (map_F g x) *) |
|
1580 |
fun rel_map_F_fs_map_F_gs subst fs gs = subst equiv_rel_b $ |
|
1581 |
(list_comb (subst map_F, fs) $ var_x) $ (list_comb (subst map_F, gs) $ var_x); |
|
1582 |
val F_in'D_thm = let |
|
1583 |
fun mk_prem var_a var_Aset {F_in', ...} var_f var_g = |
|
1584 |
[HOLogic.mk_mem (var_x, #tm F_in' $ var_Aset), mk_Ball var_Aset |
|
1585 |
((absfree (dest_Free var_a)) (HOLogic.mk_eq (var_f $ var_a, var_g $ var_a)))]; |
|
1586 |
val prems = @{map 5} mk_prem var_as var_As set_F'_aux_defs var_fs' var_gs'; |
|
1587 |
val F_in'D_tm = mk_Trueprop_implies (flat prems, |
|
1588 |
rel_map_F_fs_map_F_gs (subst_Maybe betas) var_fs' var_gs'); |
|
1589 |
||
1590 |
fun map_F_rsp_of_case_sums fs ctxt = map_F_rsp_of |
|
1591 |
(@{map 2} (fn f => fn T => BNF_FP_Util.mk_case_sum |
|
1592 |
(Term.absdummy HOLogic.unitT (mk_Nothing T), f)) fs betas) ctxt; |
|
1593 |
||
1594 |
fun mk_var_fgs n = take n var_gs' @ drop n var_fs'; |
|
1595 |
fun F_in'D_tac ctxt = EVERY |
|
1596 |
(unfold_thms_tac ctxt |
|
1597 |
(maps (fn {F_in'_def, F_in_def, ...} => [F_in'_def, F_in_def]) set_F'_thmss) :: |
|
1598 |
map (REPEAT_DETERM_N live o HEADGOAL) |
|
1599 |
[etac ctxt vimageE, |
|
1600 |
etac ctxt @{thm ImageE}, |
|
1601 |
etac ctxt CollectE THEN' etac ctxt CollectE, |
|
1602 |
dtac ctxt @{thm case_prodD}] @ |
|
1603 |
HEADGOAL (hyp_subst_tac ctxt THEN' rotate_tac (~live)) :: |
|
1604 |
map (fn i => (HEADGOAL o EVERY') |
|
1605 |
[if i < live then rtac ctxt (#transp qthms) else K all_tac, |
|
1606 |
Ctr_Sugar_Tactics.select_prem_tac ctxt live (dresolve_tac ctxt [asm_rl]) i, |
|
1607 |
rtac ctxt (#transp qthms), |
|
1608 |
dtac ctxt (map_F_rsp_of_case_sums (mk_var_fgs (i-1)) ctxt), |
|
1609 |
SELECT_GOAL (unfold_thms_tac ctxt (map_F_comp :: @{thms case_sum_o_inj(2)})), |
|
1610 |
etac ctxt (#symp qthms), |
|
1611 |
dtac ctxt (map_F_rsp_of_case_sums (mk_var_fgs i) ctxt), |
|
1612 |
SELECT_GOAL (unfold_thms_tac ctxt (map_F_comp :: @{thms case_sum_o_inj(2)})), |
|
1613 |
EqSubst.eqsubst_tac ctxt [0] [map_F_cong OF replicate i refl @ asm_rl :: replicate (live-i) refl], |
|
1614 |
rtac ctxt @{thm sum.case_cong[OF refl refl]}, |
|
1615 |
etac ctxt bspec, |
|
1616 |
hyp_subst_tac ctxt, |
|
1617 |
etac ctxt @{thm subset_lift_sum_unitD}, |
|
1618 |
assume_tac ctxt, |
|
1619 |
assume_tac ctxt]) (1 upto live)); |
|
1620 |
||
1621 |
in prove lthy (var_x :: var_As @ var_fs' @ var_gs') F_in'D_tm F_in'D_tac end; |
|
1622 |
||
1623 |
(* map_F_cong': (\<And>a. a \<in> set_F' x \<Longrightarrow> f a = g a) \<Longrightarrow> REL (map_F f x) (map_F g x) *) |
|
1624 |
val map_F_cong'_thm = let |
|
1625 |
fun mk_prem {set_F', ...} var_a var_f var_g = Logic.all var_a |
|
1626 |
(mk_Trueprop_implies ([HOLogic.mk_mem (var_a, #tm set_F' $ var_x)], |
|
1627 |
HOLogic.mk_eq (var_f $ var_a, var_g $ var_a))); |
|
1628 |
val map_F_cong'_tm = Logic.list_implies |
|
1629 |
(@{map 4} mk_prem set_F'_aux_defs var_as var_fs var_gs, HOLogic.mk_Trueprop |
|
1630 |
(rel_map_F_fs_map_F_gs I var_fs var_gs)); |
|
1631 |
fun Just_o_fun bT f = HOLogic.mk_comp (Just_const bT, f); |
|
1632 |
fun map_F_Just_o_funs fs = list_comb |
|
1633 |
(subst_Maybe betas map_F, map2 Just_o_fun betas fs) $ var_x; |
|
1634 |
fun map_F_cong'_tac ctxt = let |
|
1635 |
val map_F_respect_inst = map_F_rsp |
|
1636 |
|> infer_instantiate' ctxt (map (SOME o Thm.cterm_of ctxt) |
|
1637 |
(map map_F_Just_o_funs [var_fs, var_gs] @ map fromJust_const betas)) |
|
1638 |
|> Local_Defs.unfold ctxt (map_F_comp :: @{thms o_assoc |
|
1639 |
Fun.o_apply[where f=projr and g=Inr, unfolded sum.sel] id_def[symmetric]}) |
|
1640 |
|> Local_Defs.unfold ctxt @{thms id_comp}; |
|
1641 |
in |
|
1642 |
HEADGOAL (rtac ctxt map_F_respect_inst THEN' rtac ctxt F_in'D_thm) THEN |
|
1643 |
EVERY (map (fn {F_in'_alt2, ...} => |
|
1644 |
unfold_thms_tac ctxt [F_in'_alt2] THEN |
|
1645 |
HEADGOAL (EVERY' |
|
1646 |
[rtac ctxt CollectI, |
|
1647 |
rtac ctxt subset_refl, |
|
1648 |
rtac ctxt ballI, |
|
1649 |
SELECT_GOAL (unfold_thms_tac ctxt [o_apply]), |
|
1650 |
rtac ctxt @{thm arg_cong[where f=Inr]}, |
|
1651 |
asm_full_simp_tac ctxt])) set_F'_thmss) end; |
|
1652 |
in prove lthy (var_x :: var_fs @ var_gs) map_F_cong'_tm map_F_cong'_tac end; |
|
1653 |
||
1654 |
(* rel_F'_set: "rel_F' P x y \<longleftrightarrow> |
|
1655 |
(\<exists>z. set_F' z \<subseteq> {(x, y). P x y} \<and> REL (map_F fst z) x \<and> REL (map_F snd z) y)" *) |
|
1656 |
val rel_F'_set_thm = let |
|
1657 |
val lhs = list_comb (#tm rel_F', var_Ps) $ var_x $ var_y; |
|
1658 |
fun mk_subset_A var_a var_b var_P {set_F', ...} = let |
|
1659 |
val collect_A = mk_case_prod (var_a, var_b) (var_P $ var_a $ var_b); |
|
1660 |
in mk_leq (subst_atomic_types (alphas ~~ typ_pairs) (#tm set_F') $ var_z) collect_A end; |
|
1661 |
val subset_As = @{map 4} mk_subset_A var_as var_bs var_Ps set_F'_aux_defs; |
|
1662 |
fun mk_map mfs f z = |
|
1663 |
Term.list_comb (mfs, map (fst o Term.strip_comb o f) var_ts) $ z; |
|
1664 |
val map_F_fst = mk_map_of_bnf deads typ_pairs alphas bnf_F; |
|
1665 |
val map_F_snd = mk_map_of_bnf deads typ_pairs betas bnf_F; |
|
1666 |
val map_fst = equiv_rel_a $ (mk_map map_F_fst HOLogic.mk_fst var_z) $ var_x; |
|
1667 |
val map_snd = equiv_rel_b $ (mk_map map_F_snd HOLogic.mk_snd var_z) $ var_y; |
|
1668 |
val rhs = let val (z, T) = dest_Free var_z in |
|
1669 |
HOLogic.mk_exists (z, T, fold_rev (fn a => fn b => HOLogic.mk_conj (a, b)) |
|
1670 |
(subset_As @ [map_fst]) map_snd) end; |
|
1671 |
val rel_F'_set_tm = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)); |
|
1672 |
||
1673 |
val maybePairsTs = map HOLogic.mk_prodT (map mk_MaybeT alphas ~~ map mk_MaybeT betas) |
|
1674 |
fun mk_map_prod_projr aT bT = let |
|
1675 |
val (mabT, (maT, mbT)) = `HOLogic.mk_prodT (apply2 mk_MaybeT (aT, bT)); |
|
1676 |
val map_prod_const = Const (@{const_name map_prod}, |
|
1677 |
(maT --> aT) --> (mbT --> bT) --> mabT --> HOLogic.mk_prodT (aT, bT)); |
|
1678 |
in map_prod_const $ fromJust_const aT $ fromJust_const bT end; |
|
1679 |
||
1680 |
fun exI_OF_tac ctxt tm = rtac ctxt |
|
1681 |
(infer_instantiate' ctxt (NONE :: [SOME (Thm.cterm_of ctxt tm)]) exI); |
|
1682 |
||
1683 |
(* REL (map_F Inr x) (map_F fst z) \<Longrightarrow> REL (map_F snd z) (map_F Inr y) \<Longrightarrow> |
|
1684 |
set_F z \<subseteq> {(x, y). rel_sum (=) P x y} \<Longrightarrow> |
|
1685 |
\<exists>z. set_F' z \<subseteq> {(x, y). P x y} \<and> REL (map_F fst z) x \<and> REL (map_F snd z) y *) |
|
1686 |
fun subgoal1_tac {context = ctxt, params, ...} = |
|
1687 |
let |
|
1688 |
val z = (case params of |
|
1689 |
(_ :: _ :: (_, ct) :: _) => Thm.term_of ct |
|
1690 |
| _ => error "won't happen"); |
|
1691 |
val map_F_projr_z = list_comb (mk_map_of_bnf deads maybePairsTs typ_pairs bnf_F, |
|
1692 |
map2 mk_map_prod_projr alphas betas) $ z; |
|
1693 |
in |
|
1694 |
HEADGOAL (exI_OF_tac ctxt map_F_projr_z) THEN |
|
1695 |
HEADGOAL (EVERY' (maps (fn {set_F'_subset, set_F'_respect, set_map_F', ...} => |
|
1696 |
[rtac ctxt conjI, |
|
1697 |
dtac ctxt (set_F'_subset RS @{thm order_trans}), |
|
1698 |
TWICE (dtac ctxt (set_F'_respect RS @{thm rel_funD})), |
|
1699 |
SELECT_GOAL (unfold_thms_tac ctxt [set_map_F']), |
|
1700 |
etac ctxt @{thm in_rel_sum_in_image_projr}, |
|
1701 |
TWICE (assume_tac ctxt)]) set_F'_thmss)) THEN |
|
1702 |
HEADGOAL (EVERY' (map (fn Ts => FIRST' |
|
1703 |
[dtac ctxt (map_F_rsp_of (map fromJust_const Ts) ctxt), |
|
1704 |
etac ctxt sym , assume_tac ctxt]) [alphas, betas])) THEN |
|
1705 |
unfold_thms_tac ctxt (map_F_comp :: |
|
1706 |
@{thms fst_comp_map_prod snd_comp_map_prod comp_projr_Inr} @ [map_F_id]) THEN |
|
1707 |
HEADGOAL (rtac ctxt conjI) THEN |
|
1708 |
HEADGOAL (etac ctxt (#symp qthms) THEN' assume_tac ctxt |
|
1709 |
ORELSE' (EVERY' (maps (fn Ts => |
|
1710 |
[dtac ctxt (map_F_rsp_of (map fromJust_const Ts) ctxt), |
|
1711 |
SELECT_GOAL (unfold_thms_tac ctxt (map_F_comp :: |
|
1712 |
@{thms fst_comp_map_prod snd_comp_map_prod comp_projr_Inr} @ [map_F_id])), |
|
1713 |
assume_tac ctxt]) [alphas, betas]))) end; |
|
1714 |
||
1715 |
(* set_F' z \<subseteq> {(x, y). P x y} \<Longrightarrow> REL (map_F fst z) x \<Longrightarrow> REL (map_F snd z) y \<Longrightarrow> |
|
1716 |
\<exists>b. REL (map_F Inr x) b \<and> (\<exists>ba. rel_F (rel_sum (=) P) b ba \<and> REL ba (map_F Inr y)) *) |
|
1717 |
fun subgoal2_tac {context = ctxt, params, ...} = let |
|
1718 |
val z = (case params of |
|
1719 |
((_, ct) :: _) => Thm.term_of ct |
|
1720 |
| _ => error "won't happen"); |
|
1721 |
||
1722 |
fun exI_map_Ifs_tac mk_proj Ts = exI_OF_tac ctxt (list_comb |
|
1723 |
(mk_map_of_bnf deads typ_pairs (map mk_MaybeT Ts) bnf_F, @{map 3} |
|
1724 |
(fn var_t => fn {set_F', ...} => fn T => lambda var_t (BNF_FP_Util.mk_If |
|
1725 |
(HOLogic.mk_mem (var_t, subst_Ts (#tm set_F') typ_pairs $ z)) |
|
1726 |
(mk_Just (mk_proj var_t)) (mk_Nothing T))) var_ts set_F'_aux_defs Ts) $ z) |
|
1727 |
||
1728 |
fun mk_REL_trans_map_F n = (rotate_prems n (#transp qthms) OF |
|
1729 |
[rel_funD map_F_respect_thm] OF (replicate live refl @ [#symp qthms])); |
|
1730 |
in |
|
1731 |
HEADGOAL (EVERY' |
|
1732 |
[exI_map_Ifs_tac HOLogic.mk_fst alphas, |
|
1733 |
rtac ctxt conjI, |
|
1734 |
etac ctxt (mk_REL_trans_map_F 0)]) THEN |
|
1735 |
unfold_thms_tac ctxt [map_F_comp, @{thm o_def}] THEN |
|
1736 |
HEADGOAL (rtac ctxt map_F_cong'_thm) THEN |
|
1737 |
REPEAT_DETERM_N live (HEADGOAL (etac ctxt @{thm if_P[symmetric]})) THEN |
|
1738 |
HEADGOAL (EVERY' [exI_map_Ifs_tac HOLogic.mk_snd betas, rtac ctxt conjI]) THEN |
|
1739 |
unfold_thms_tac ctxt rel_map THEN |
|
1740 |
HEADGOAL (rtac ctxt rel_refl_strong) THEN |
|
1741 |
REPEAT_DETERM_N live (HEADGOAL (etac ctxt @{thm subset_rel_sumI})) THEN |
|
1742 |
HEADGOAL (etac ctxt (mk_REL_trans_map_F 1 OF [#symp qthms])) THEN |
|
1743 |
unfold_thms_tac ctxt [map_F_comp, @{thm o_def}] THEN |
|
1744 |
HEADGOAL (rtac ctxt map_F_cong'_thm) THEN |
|
1745 |
REPEAT_DETERM_N live (HEADGOAL (etac ctxt @{thm if_P})) end; |
|
1746 |
||
1747 |
fun rel_F'_set_tac ctxt = EVERY |
|
1748 |
([unfold_thms_tac ctxt (#def rel_F' :: #REL qthms :: @{thms vimage2p_def relcompp_apply}), |
|
1749 |
HEADGOAL (rtac ctxt iffI), |
|
1750 |
(HEADGOAL o TWICE) (etac ctxt exE THEN' etac ctxt conjE), |
|
1751 |
HEADGOAL (EVERY' |
|
1752 |
[dtac ctxt (in_rel RS iffD1), |
|
1753 |
etac ctxt exE, |
|
1754 |
TWICE (etac ctxt conjE), |
|
1755 |
etac ctxt CollectE, |
|
1756 |
hyp_subst_tac ctxt]), |
|
1757 |
(REPEAT_DETERM_N (live-1) o HEADGOAL) (etac ctxt conjE), |
|
1758 |
HEADGOAL (Subgoal.FOCUS_PARAMS subgoal1_tac ctxt THEN' etac ctxt exE), |
|
1759 |
(REPEAT_DETERM_N (live+1) o HEADGOAL) (etac ctxt conjE), |
|
1760 |
HEADGOAL (Subgoal.FOCUS_PARAMS subgoal2_tac ctxt)]); |
|
1761 |
||
1762 |
in prove lthy (var_x :: var_y :: var_Ps) rel_F'_set_tm rel_F'_set_tac end; |
|
1763 |
||
1764 |
(* tactics *) |
|
1765 |
||
1766 |
(* map_G_id0: abs_G \<circ> map_F id \<circ> rep_G = id *) |
|
1767 |
fun map_G_id0_tac ctxt = HEADGOAL (EVERY' [SELECT_GOAL (unfold_thms_tac ctxt |
|
1768 |
[@{thm fun_eq_iff}, o_apply, map_F_id0, id_apply, #abs_rep qthms]), |
|
1769 |
rtac ctxt allI, rtac ctxt refl]); |
|
1770 |
||
1771 |
(* map_G (g \<circ> f) = map_G g \<circ> map_G f *) |
|
1772 |
fun map_G_comp0_tac ctxt = HEADGOAL (EVERY' [rtac ctxt ext, rtac ctxt sym, |
|
1773 |
SELECT_GOAL (unfold_thms_tac ctxt [o_apply, map_F_comp0]), rtac ctxt (#rel_abs qthms), |
|
1774 |
rtac ctxt map_F_rsp, rtac ctxt (#rep_abs qthms), rtac ctxt (#reflp qthms)]); |
|
1775 |
||
1776 |
(* map_G_cong: (\<And>z. z \<in> set_G x \<Longrightarrow> f z = g z) \<Longrightarrow> map_G f x = map_G g x *) |
|
1777 |
fun map_G_cong_tac ctxt = EVERY |
|
1778 |
[Local_Defs.fold_tac ctxt (map #set_F'_def set_F'_thmss), |
|
1779 |
unfold_thms_tac ctxt [o_apply], |
|
1780 |
HEADGOAL (rtac ctxt (#rel_abs qthms) THEN' rtac ctxt map_F_cong'_thm), |
|
1781 |
REPEAT_DETERM_N live (HEADGOAL (asm_full_simp_tac ctxt))]; |
|
1782 |
||
1783 |
(* set_G_map0_G: set_G \<circ> map_G f = f ` set_G *) |
|
1784 |
fun mk_set_G_map0_G_tac thms ctxt = |
|
1785 |
HEADGOAL (rtac ctxt ext) THEN |
|
1786 |
EVERY [unfold_thms_tac ctxt [o_apply], |
|
1787 |
Local_Defs.fold_tac ctxt [#set_F'_def thms]] THEN |
|
1788 |
HEADGOAL (EVERY' (map (rtac ctxt) |
|
1789 |
[trans OF [#set_map_F' thms RS sym, sym] RS sym, |
|
1790 |
@{thm rel_funD} OF [#set_F'_respect thms], |
|
1791 |
#rep_abs qthms, |
|
1792 |
map_F_rsp, |
|
1793 |
#rep_reflp qthms])); |
|
1794 |
||
1795 |
(* bd_card_order: card_order bd_F *) |
|
1796 |
fun bd_card_order_tac ctxt = HEADGOAL (rtac ctxt bd_card_order); |
|
1797 |
||
1798 |
(* bd_cinfinite: BNF_Cardinal_Arithmetic.cinfinite bd_F *) |
|
1799 |
fun bd_cinfinite_tac ctxt = HEADGOAL (rtac ctxt bd_cinfinite); |
|
1800 |
||
1801 |
(*target: ordLeq3 (card_of (set_F' (rep_G x_))) bd_F*) |
|
1802 |
fun mk_set_G_bd_tac thms set_bd_thm ctxt = EVERY |
|
1803 |
[Local_Defs.fold_tac ctxt [#set_F'_def thms], |
|
1804 |
unfold_thms_tac ctxt [o_apply], |
|
1805 |
HEADGOAL (rtac ctxt (@{thm ordLeq_transitive} OF |
|
1806 |
[@{thm card_of_mono1} OF [#set_F'_subset thms], set_bd_thm]))]; |
|
1807 |
||
1808 |
(* rel_compp: rel_G R OO rel_G S \<le> rel_G (R OO S) *) |
|
1809 |
fun rel_compp_tac ctxt = EVERY |
|
1810 |
[unfold_thms_tac ctxt [#REL qthms], |
|
1811 |
HEADGOAL (TWICE (rtac ctxt @{thm vimage2p_relcompp_mono})), |
|
1812 |
(unfold_thms_tac ctxt (REL_OO_REL_left_thm :: @{thms relcompp_assoc})), |
|
1813 |
(unfold_thms_tac ctxt [Local_Defs.unfold ctxt @{thms eq_OO} |
|
1814 |
(infer_instantiate' ctxt [HOLogic.eq_const HOLogic.unitT |> Thm.cterm_of ctxt |> SOME] |
|
1815 |
@{thm sum.rel_compp})]), |
|
1816 |
HEADGOAL (rtac ctxt rel_pos_distr_thm), |
|
1817 |
unfold_thms_tac ctxt |
|
1818 |
@{thms fun_eq_iff bot_apply bot_bool_def not_all eq_False not_not OO_def}, |
|
1819 |
REPEAT_DETERM (HEADGOAL (resolve_tac ctxt [exI, conjI, @{thm rel_sum.intros(1)}, refl]))]; |
|
1820 |
||
1821 |
(* rel_G R_ = (\<lambda>x y. \<exists>z. set_G z \<subseteq> {(x, y). R x y} \<and> map_G fst z = x \<and> map_G snd z = y) *) |
|
1822 |
fun rel_compp_Grp_tac ctxt = let |
|
1823 |
val _ = () |
|
1824 |
in EVERY [Local_Defs.fold_tac ctxt (@{thm Grp_def} :: map #set_F'_def set_F'_thmss), |
|
1825 |
unfold_thms_tac ctxt |
|
1826 |
[o_apply, @{thm mem_Collect_eq}, @{thm OO_Grp_alt}, @{thm vimage2p_def}], |
|
1827 |
Local_Defs.fold_tac ctxt [Local_Defs.unfold ctxt @{thms vimage2p_def} (#def rel_F')], |
|
1828 |
unfold_thms_tac ctxt [rel_F'_set_thm], |
|
1829 |
HEADGOAL (TWICE (rtac ctxt ext)), |
|
1830 |
HEADGOAL (rtac ctxt iffI), |
|
1831 |
REPEAT_DETERM (ALLGOALS (eresolve_tac ctxt [exE, conjE])), |
|
1832 |
HEADGOAL (rtac ctxt exI), |
|
1833 |
REPEAT_FIRST (resolve_tac ctxt [conjI]), |
|
1834 |
HEADGOAL (EVERY' (maps (fn {set_F'_respect, ...} => |
|
1835 |
[etac ctxt @{thm subset_trans[rotated]}, |
|
1836 |
rtac ctxt equalityD1, |
|
1837 |
rtac ctxt (@{thm rel_funD} OF [set_F'_respect]), |
|
1838 |
rtac ctxt (#rep_abs qthms), |
|
1839 |
rtac ctxt (#reflp qthms)]) set_F'_thmss)), |
|
1840 |
(HEADGOAL o TWICE o EVERY') |
|
1841 |
[rtac ctxt (trans OF [asm_rl, #abs_rep qthms]), |
|
1842 |
rtac ctxt (#rel_abs qthms), |
|
1843 |
etac ctxt (rotate_prems 1 (#transp qthms)), |
|
1844 |
rtac ctxt map_F_rsp, |
|
1845 |
rtac ctxt (#rep_abs qthms), |
|
1846 |
rtac ctxt (#reflp qthms) |
|
1847 |
], |
|
1848 |
HEADGOAL (rtac ctxt exI THEN' rtac ctxt conjI), |
|
1849 |
(REPEAT_DETERM_N live o HEADGOAL o EVERY') |
|
1850 |
[assume_tac ctxt, rtac ctxt conjI], |
|
1851 |
(HEADGOAL o TWICE o EVERY') [ |
|
1852 |
hyp_subst_tac ctxt, |
|
1853 |
rtac ctxt (#rep_abs_rsp qthms), |
|
1854 |
rtac ctxt map_F_rsp, |
|
1855 |
rtac ctxt (#rep_reflp qthms)]] |
|
1856 |
end; |
|
1857 |
||
1858 |
fun pred_G_set_G_tac ctxt = HEADGOAL (rtac ctxt refl); |
|
1859 |
||
1860 |
val tactics = map_G_id0_tac :: map_G_comp0_tac :: map_G_cong_tac :: |
|
1861 |
map mk_set_G_map0_G_tac set_F'_thmss @ |
|
1862 |
bd_card_order_tac :: bd_cinfinite_tac :: |
|
1863 |
map2 mk_set_G_bd_tac set_F'_thmss set_bd_thms @ |
|
1864 |
rel_compp_tac :: rel_compp_Grp_tac :: [pred_G_set_G_tac]; |
|
1865 |
||
71469
d7ef73df3d15
lift BNF witnesses for quotients (unless better ones are specified by the user)
traytel
parents:
71393
diff
changeset
|
1866 |
(* val wits_G = [abs_G o wit_F] *) |
d7ef73df3d15
lift BNF witnesses for quotients (unless better ones are specified by the user)
traytel
parents:
71393
diff
changeset
|
1867 |
val (wits_G, wit_thms) = |
d7ef73df3d15
lift BNF witnesses for quotients (unless better ones are specified by the user)
traytel
parents:
71393
diff
changeset
|
1868 |
let |
d7ef73df3d15
lift BNF witnesses for quotients (unless better ones are specified by the user)
traytel
parents:
71393
diff
changeset
|
1869 |
val wit_F_thmss = map (map2 (fn set_F' => fn wit => |
d7ef73df3d15
lift BNF witnesses for quotients (unless better ones are specified by the user)
traytel
parents:
71393
diff
changeset
|
1870 |
(#set_F'_subset set_F' RS set_mp RS wit) |
d7ef73df3d15
lift BNF witnesses for quotients (unless better ones are specified by the user)
traytel
parents:
71393
diff
changeset
|
1871 |
|> unfold_thms lthy [#set_F'_def set_F']) set_F'_thmss) |
d7ef73df3d15
lift BNF witnesses for quotients (unless better ones are specified by the user)
traytel
parents:
71393
diff
changeset
|
1872 |
(wit_thmss_of_bnf bnf_F); |
d7ef73df3d15
lift BNF witnesses for quotients (unless better ones are specified by the user)
traytel
parents:
71393
diff
changeset
|
1873 |
val (wits_F, wit_F_thmss) = split_list |
d7ef73df3d15
lift BNF witnesses for quotients (unless better ones are specified by the user)
traytel
parents:
71393
diff
changeset
|
1874 |
(filter_out (fn ((J, _), _) => exists (fn (I, _) => subset (op =) (I, J)) Iwits) |
d7ef73df3d15
lift BNF witnesses for quotients (unless better ones are specified by the user)
traytel
parents:
71393
diff
changeset
|
1875 |
(wits_F ~~ wit_F_thmss)); |
d7ef73df3d15
lift BNF witnesses for quotients (unless better ones are specified by the user)
traytel
parents:
71393
diff
changeset
|
1876 |
fun mk_wit (I, wit) = let val vars = (map (fn n => nth var_as n) I) |
d7ef73df3d15
lift BNF witnesses for quotients (unless better ones are specified by the user)
traytel
parents:
71393
diff
changeset
|
1877 |
in fold_rev lambda vars (abs_G $ list_comb (wit, vars)) end; |
d7ef73df3d15
lift BNF witnesses for quotients (unless better ones are specified by the user)
traytel
parents:
71393
diff
changeset
|
1878 |
in |
d7ef73df3d15
lift BNF witnesses for quotients (unless better ones are specified by the user)
traytel
parents:
71393
diff
changeset
|
1879 |
(map mk_wit (Iwits @ wits_F), wit_thmss @ flat wit_F_thmss) |
d7ef73df3d15
lift BNF witnesses for quotients (unless better ones are specified by the user)
traytel
parents:
71393
diff
changeset
|
1880 |
end; |
d7ef73df3d15
lift BNF witnesses for quotients (unless better ones are specified by the user)
traytel
parents:
71393
diff
changeset
|
1881 |
|
71262 | 1882 |
fun mk_wit_tacs ({set_F'_def, set_F'_respect, ...} :: set_F'_thmss) (w :: ws) ctxt = |
1883 |
EVERY [unfold_thms_tac ctxt [@{thm o_def}, |
|
1884 |
set_F'_respect RS @{thm rel_funD} OF [#rep_abs qthms OF [(#reflp qthms)]]], |
|
1885 |
unfold_thms_tac ctxt [set_F'_def], |
|
1886 |
HEADGOAL (etac ctxt w)] |
|
1887 |
THEN mk_wit_tacs set_F'_thmss ws ctxt |
|
1888 |
| mk_wit_tacs [] ws ctxt = mk_wit_tacs set_F'_thmss ws ctxt |
|
1889 |
| mk_wit_tacs _ _ _ = all_tac; |
|
1890 |
||
1891 |
val (bnf_G, lthy) = bnf_def Dont_Inline (user_policy Note_Some) true I |
|
1892 |
tactics (mk_wit_tacs [] wit_thms) NONE map_b rel_b pred_b set_bs |
|
1893 |
(((((((Binding.empty, absT), map_G), sets_G), bd_G), wits_G), SOME rel_G), NONE) lthy; |
|
1894 |
||
1895 |
val old_defs = |
|
1896 |
{sets = set_defs_of_bnf bnf_G, map = map_def_of_bnf bnf_G, rel = rel_def_of_bnf bnf_G}; |
|
1897 |
||
1898 |
val set_F'_defs = map (mk_abs_def o #set_F'_def) set_F'_thmss; |
|
1899 |
val unfold_morphism = Morphism.thm_morphism "BNF" |
|
1900 |
(unfold_thms lthy (defs @ #def REL :: set_F'_defs)); |
|
1901 |
val (bnf_G, lthy) = morph_bnf_defs unfold_morphism bnf_G |
|
1902 |
|> (fn bnf => note_bnf_defs bnf lthy); |
|
1903 |
||
1904 |
(* auxiliary lemmas transfer for transfer *) |
|
1905 |
val rel_monoD_rotated = rotate_prems ~1 (rel_mono_of_bnf bnf_F RS @{thm predicate2D}); |
|
1906 |
||
1907 |
val REL_pos_distrI = let |
|
1908 |
fun tac ctxt = EVERY |
|
1909 |
[HEADGOAL (dtac ctxt (rotate_prems ~1 (rel_pos_distr_thm RS @{thm predicate2D}))), |
|
1910 |
(REPEAT_DETERM o HEADGOAL) (rtac ctxt conjI ORELSE' assume_tac ctxt), |
|
1911 |
(REPEAT_DETERM o HEADGOAL) (etac ctxt @{thm relcomppE}), |
|
1912 |
HEADGOAL (dtac ctxt rel_monoD_rotated), |
|
1913 |
(REPEAT_DETERM o HEADGOAL) |
|
1914 |
(assume_tac ctxt ORELSE' rtac ctxt @{thm relcomppI})]; |
|
1915 |
in prove lthy (var_x :: var_y' :: var_Ps @ var_Qs @ var_Rs) REL_pos_distrI_tm tac end; |
|
1916 |
||
1917 |
val rel_F_rel_F' = let |
|
1918 |
val rel_F = mk_rel_of_bnf deads alphas betas bnf_F; |
|
1919 |
val rel_F_rel_F'_tm = (rel_F, #tm rel_F') |
|
1920 |
|> apply2 (fn R => HOLogic.mk_Trueprop (list_comb (R, var_Ps) $ var_x $ var_y)) |
|
1921 |
|> Logic.mk_implies; |
|
1922 |
fun rel_F_rel_F'_tac ctxt = EVERY |
|
1923 |
[HEADGOAL (dtac ctxt (in_rel_of_bnf bnf_F RS iffD1)), |
|
1924 |
unfold_thms_tac ctxt (rel_F'_set_thm :: @{thms mem_Collect_eq}), |
|
1925 |
(REPEAT_DETERM o HEADGOAL) (eresolve_tac ctxt [exE, conjE]), |
|
1926 |
HEADGOAL (rtac ctxt exI), |
|
1927 |
HEADGOAL (EVERY' (maps (fn thms => |
|
1928 |
[rtac ctxt conjI, |
|
1929 |
rtac ctxt subsetI, |
|
1930 |
dtac ctxt (set_mp OF [#set_F'_subset thms]), |
|
1931 |
dtac ctxt subsetD, |
|
1932 |
assume_tac ctxt, assume_tac ctxt]) set_F'_thmss)), |
|
1933 |
(REPEAT_DETERM o HEADGOAL) |
|
1934 |
(rtac ctxt conjI ORELSE' hyp_subst_tac ctxt THEN' rtac ctxt (#reflp qthms))] |
|
1935 |
in prove lthy (var_x :: var_y :: var_Ps) rel_F_rel_F'_tm rel_F_rel_F'_tac end; |
|
1936 |
||
1937 |
fun inst_REL_pos_distrI n vs aTs bTs ctxt = |
|
1938 |
infer_instantiate' ctxt (replicate n NONE @ (rel_Maybes vs aTs bTs |
|
1939 |
|> map (SOME o Thm.cterm_of ctxt))) REL_pos_distrI; |
|
1940 |
||
1941 |
val Tss = {abs = typ_subst_atomic (alphas ~~ betas) absT, rep = repT, Ds0 = map TFree Ds0, |
|
1942 |
deads = deads, alphas = alphas, betas = betas, gammas = gammas, deltas = deltas}; |
|
1943 |
||
1944 |
val thms = |
|
1945 |
{map_F_rsp = map_F_rsp, |
|
1946 |
rel_F'_def = #def rel_F', |
|
1947 |
rel_F_rel_F' = rel_F_rel_F', |
|
1948 |
rel_F'_set = rel_F'_set_thm, |
|
1949 |
rel_monoD_rotated = rel_monoD_rotated} |
|
1950 |
||
1951 |
val transfer_consts = mk_quotient_transfer_tacs bnf_F Tss live |
|
1952 |
qthms thms set_F'_thmss old_defs inst_REL_pos_distrI |
|
1953 |
map_raw rel_raw (map (#tm o #set_F') set_F'_aux_defs); |
|
1954 |
val quiet = exists (fn No_Warn_Transfer => true | _ => false) opts; |
|
1955 |
in |
|
1956 |
lthy |> BNF_Def.register_bnf plugins absT_name bnf_G |> |
|
1957 |
mk_transfer_thms quiet bnf_F bnf_G absT_name transfer_consts (Quotient equiv_thm) Tss |
|
1958 |
(defs @ #def REL :: set_F'_defs) |
|
1959 |
end |
|
1960 |
| _ => raise Match); |
|
1961 |
||
1962 |
in (goals, after_qed, #def REL :: defs, lthy) end; |
|
1963 |
||
1964 |
||
1965 |
(** main commands **) |
|
61067 | 1966 |
|
1967 |
local |
|
1968 |
||
60918 | 1969 |
fun prepare_common prepare_name prepare_sort prepare_term prepare_thm |
71494 | 1970 |
(((((plugins, raw_specs), raw_absT_name), raw_wits), xthms_opt), (map_b, rel_b, pred_b)) lthy = |
60918 | 1971 |
let |
71262 | 1972 |
val absT_name = prepare_name lthy raw_absT_name; |
1973 |
||
71494 | 1974 |
fun bad_input input = |
1975 |
Pretty.chunks [Pretty.para ("Expected theorem(s) of either form:"), |
|
1976 |
Pretty.item [Pretty.enum "," "" "" [Syntax.pretty_term lthy @{term "Quotient R Abs Rep T"}, |
|
1977 |
Syntax.pretty_term lthy @{term "reflp R"}]], |
|
1978 |
Pretty.item [Syntax.pretty_term lthy @{term "Quotient R Abs Rep T"}], |
|
1979 |
Pretty.item [Syntax.pretty_term lthy @{term "type_definition Rep Abs A"}], |
|
1980 |
Pretty.para ("Got"), Pretty.enum "," "" "" (map (Thm.pretty_thm lthy) input)] |
|
1981 |
|> Pretty.string_of |
|
1982 |
|> error; |
|
1983 |
||
1984 |
fun no_refl qthm = |
|
1985 |
Pretty.chunks [Pretty.para ("Could not find a reflexivity rule for the Quotient theorem:"), |
|
1986 |
Pretty.item [Thm.pretty_thm lthy qthm], |
|
1987 |
Pretty.para ("Try supplying a reflexivity theorem manually or registering it in setup_lifting.")] |
|
1988 |
|> Pretty.string_of |
|
1989 |
|> error; |
|
1990 |
||
1991 |
fun find_equiv_thm_via_Quotient qthm = |
|
1992 |
let |
|
1993 |
val refl_thms = Lifting_Info.get_reflexivity_rules lthy |
|
1994 |
|> map (unfold_thms lthy @{thms reflp_eq[symmetric]}); |
|
1995 |
in |
|
1996 |
(case refl_thms RL [qthm RS @{thm Quotient_reflp_imp_equivp}] of |
|
1997 |
[] => no_refl qthm |
|
1998 |
| thm :: _ => thm) |
|
1999 |
end; |
|
2000 |
||
2001 |
val (lift_thm, equiv_thm) = |
|
2002 |
(case Option.map (prepare_thm lthy) xthms_opt of |
|
2003 |
SOME (thms as [qthm, _]) => |
|
2004 |
(case try (fn thms => @{thm Quotient_reflp_imp_equivp} OF thms) thms of |
|
2005 |
SOME equiv_thm => (qthm RS @{thm Quotient_Quotient3}, Quotient equiv_thm) |
|
2006 |
| NONE => bad_input thms) |
|
2007 |
| SOME [thm] => |
|
2008 |
(case try (fn thm => thm RS @{thm Quotient_Quotient3}) thm of |
|
2009 |
SOME qthm => (qthm, Quotient (find_equiv_thm_via_Quotient thm)) |
|
2010 |
| NONE => if can (fn thm => thm RS @{thm type_definition.Rep}) thm |
|
2011 |
then (thm, Typedef) |
|
2012 |
else bad_input [thm]) |
|
2013 |
| NONE => (case Lifting_Info.lookup_quotients lthy absT_name of |
|
2014 |
SOME {quot_thm = qthm, ...} => |
|
71558
1cf958713cf7
remove Thm.transfer workaround made obsplete by cf2406e654cf
traytel
parents:
71494
diff
changeset
|
2015 |
(case [qthm] RL @{thms Quotient_eq_onp_typedef Quotient_eq_onp_type_copy} of |
1cf958713cf7
remove Thm.transfer workaround made obsplete by cf2406e654cf
traytel
parents:
71494
diff
changeset
|
2016 |
thm :: _ => (thm, Typedef) |
1cf958713cf7
remove Thm.transfer workaround made obsplete by cf2406e654cf
traytel
parents:
71494
diff
changeset
|
2017 |
| _ => (qthm RS @{thm Quotient_Quotient3}, |
1cf958713cf7
remove Thm.transfer workaround made obsplete by cf2406e654cf
traytel
parents:
71494
diff
changeset
|
2018 |
Quotient (find_equiv_thm_via_Quotient qthm))) |
71494 | 2019 |
| NONE => (Typedef.get_info lthy absT_name |> hd |> snd |> #type_definition, Typedef)) |
2020 |
| SOME thms => bad_input thms); |
|
61067 | 2021 |
val wits = (Option.map o map) (prepare_term lthy) raw_wits; |
2022 |
val specs = |
|
71262 | 2023 |
map (apsnd (apsnd (the_default @{sort type} o Option.map (prepare_sort lthy)))) raw_specs; |
60918 | 2024 |
|
71494 | 2025 |
val which_bnf = (case equiv_thm of |
2026 |
Quotient thm => quotient_bnf (thm, lift_thm) |
|
2027 |
| Typedef => typedef_bnf lift_thm); |
|
60918 | 2028 |
in |
71494 | 2029 |
which_bnf wits specs map_b rel_b pred_b plugins lthy |
60918 | 2030 |
end; |
2031 |
||
2032 |
fun prepare_lift_bnf prepare_name prepare_sort prepare_term prepare_thm = |
|
2033 |
(fn (goals, after_qed, definitions, lthy) => |
|
2034 |
lthy |
|
2035 |
|> Proof.theorem NONE after_qed (map (single o rpair []) goals) |
|
61841
4d3527b94f2a
more general types Proof.method / context_tactic;
wenzelm
parents:
61073
diff
changeset
|
2036 |
|> Proof.refine_singleton |
4d3527b94f2a
more general types Proof.method / context_tactic;
wenzelm
parents:
61073
diff
changeset
|
2037 |
(Method.Basic (fn ctxt => SIMPLE_METHOD (unfold_thms_tac ctxt definitions))) |
4d3527b94f2a
more general types Proof.method / context_tactic;
wenzelm
parents:
61073
diff
changeset
|
2038 |
|> Proof.refine_singleton (Method.primitive_text (K I))) oo |
60918 | 2039 |
prepare_common prepare_name prepare_sort prepare_term prepare_thm o apfst (apfst (apsnd SOME)); |
2040 |
||
2041 |
fun prepare_solve prepare_name prepare_typ prepare_sort prepare_thm tacs = |
|
63023
1f4b011c5738
unfold internal definitions before emitting a proof obligation
traytel
parents:
62969
diff
changeset
|
2042 |
(fn (goals, after_qed, definitions, lthy) => |
60918 | 2043 |
lthy |
71262 | 2044 |
|> after_qed (map2 (fn goal => fn tac => [Goal.prove_sorry lthy [] [] goal |
63023
1f4b011c5738
unfold internal definitions before emitting a proof obligation
traytel
parents:
62969
diff
changeset
|
2045 |
(fn (ctxtprems as {context = ctxt, prems = _}) => |
1f4b011c5738
unfold internal definitions before emitting a proof obligation
traytel
parents:
62969
diff
changeset
|
2046 |
unfold_thms_tac ctxt definitions THEN tac ctxtprems)]) |
1f4b011c5738
unfold internal definitions before emitting a proof obligation
traytel
parents:
62969
diff
changeset
|
2047 |
goals (tacs (length goals)))) oo |
62777 | 2048 |
prepare_common prepare_name prepare_typ prepare_sort prepare_thm; |
60918 | 2049 |
|
61067 | 2050 |
in |
2051 |
||
2052 |
val lift_bnf_cmd = |
|
2053 |
prepare_lift_bnf |
|
2054 |
(fst o dest_Type oo Proof_Context.read_type_name {proper = true, strict = false}) |
|
71494 | 2055 |
Syntax.read_sort Syntax.read_term Attrib.eval_thms; |
61067 | 2056 |
|
62777 | 2057 |
fun lift_bnf args tacs = |
2058 |
prepare_solve (K I) (K I) (K I) (K I) (K tacs) args; |
|
61067 | 2059 |
|
71262 | 2060 |
fun copy_bnf_tac {context = ctxt, prems = _} = |
2061 |
REPEAT_DETERM (resolve_tac ctxt [bexI, conjI, UNIV_I, refl, subset_refl] 1); |
|
2062 |
||
61067 | 2063 |
val copy_bnf = |
62777 | 2064 |
apfst (apfst (rpair NONE)) |
71494 | 2065 |
#> apfst (apsnd (Option.map single)) |
62777 | 2066 |
#> prepare_solve (K I) (K I) (K I) (K I) |
71262 | 2067 |
(fn n => replicate n copy_bnf_tac); |
61067 | 2068 |
|
2069 |
val copy_bnf_cmd = |
|
62777 | 2070 |
apfst (apfst (rpair NONE)) |
71494 | 2071 |
#> apfst (apsnd (Option.map single)) |
62777 | 2072 |
#> prepare_solve |
61067 | 2073 |
(fst o dest_Type oo Proof_Context.read_type_name {proper = true, strict = false}) |
71494 | 2074 |
Syntax.read_sort Syntax.read_term Attrib.eval_thms |
71262 | 2075 |
(fn n => replicate n copy_bnf_tac); |
61067 | 2076 |
|
2077 |
end; |
|
2078 |
||
71262 | 2079 |
(** outer syntax **) |
61067 | 2080 |
|
2081 |
local |
|
60918 | 2082 |
|
71262 | 2083 |
(* parsers *) |
2084 |
||
60918 | 2085 |
val parse_wits = |
71262 | 2086 |
@{keyword "["} |-- (Parse.name --| @{keyword ":"} -- Scan.repeat Parse.term >> |
60918 | 2087 |
(fn ("wits", Ts) => Ts |
2088 |
| (s, _) => error ("Unknown label " ^ quote s ^ " (expected \"wits\")"))) --| |
|
71262 | 2089 |
@{keyword "]"} || Scan.succeed []; |
60918 | 2090 |
|
71262 | 2091 |
fun parse_common_opts p = |
2092 |
Scan.optional (@{keyword "("} |-- |
|
60918 | 2093 |
Parse.list1 (Parse.group (K "option") |
71262 | 2094 |
(Scan.first (p :: [Plugin_Name.parse_filter >> Plugins_Option, |
2095 |
Parse.reserved "no_warn_transfer" >> K No_Warn_Transfer]))) |
|
2096 |
--| @{keyword ")"}) []; |
|
60918 | 2097 |
|
71262 | 2098 |
val parse_lift_opts = Parse.reserved "no_warn_wits" >> K No_Warn_Wits |> parse_common_opts; |
60918 | 2099 |
|
71262 | 2100 |
val parse_copy_opts = parse_common_opts Scan.fail; |
2101 |
||
2102 |
val parse_xthm = Scan.option (Parse.reserved "via" |-- Parse.thm); |
|
71494 | 2103 |
val parse_xthms = Scan.option (Parse.reserved "via" |-- Parse.thms1); |
60918 | 2104 |
|
61067 | 2105 |
in |
2106 |
||
71262 | 2107 |
(* exposed commands *) |
60918 | 2108 |
|
2109 |
val _ = |
|
71262 | 2110 |
Outer_Syntax.local_theory_to_proof @{command_keyword lift_bnf} |
2111 |
"register a quotient type/subtype of a bounded natural functor (BNF) as a BNF" |
|
2112 |
((parse_lift_opts -- parse_type_args_named_constrained -- Parse.type_const -- parse_wits -- |
|
71494 | 2113 |
parse_xthms -- parse_map_rel_pred_bindings) >> lift_bnf_cmd); |
71262 | 2114 |
|
2115 |
val _ = |
|
2116 |
Outer_Syntax.local_theory @{command_keyword copy_bnf} |
|
60918 | 2117 |
"register a type copy of a bounded natural functor (BNF) as a BNF" |
71262 | 2118 |
((parse_copy_opts -- parse_type_args_named_constrained -- Parse.type_const -- |
2119 |
parse_xthm -- parse_map_rel_pred_bindings) >> copy_bnf_cmd); |
|
60918 | 2120 |
|
61067 | 2121 |
end; |
2122 |
||
2123 |
end; |