1(* Title: HOL/Tools/BNF/bnf_lift.ML 2 Author: Julian Biendarra, TU Muenchen 3 Author: Basil F��rer, ETH Zurich 4 Author: Joshua Schneider, ETH Zurich 5 Author: Dmitriy Traytel, ETH Zurich 6 Copyright 2015, 2019 7 8Lifting of BNFs through typedefs. 9*) 10 11signature BNF_LIFT = 12sig 13 datatype lift_bnf_option = 14 Plugins_Option of Proof.context -> Plugin_Name.filter 15 | No_Warn_Wits 16 | No_Warn_Transfer 17 val copy_bnf: 18 (((lift_bnf_option list * (binding option * (string * sort option)) list) * 19 string) * thm option) * (binding * binding * binding) -> 20 local_theory -> local_theory 21 val copy_bnf_cmd: 22 (((lift_bnf_option list * (binding option * (string * string option)) list) * 23 string) * (Facts.ref * Token.src list) option) * (binding * binding * binding) -> 24 local_theory -> local_theory 25 val lift_bnf: 26 ((((lift_bnf_option list * (binding option * (string * sort option)) list) * 27 string) * term list option) * thm list option) * (binding * binding * binding) -> 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) * 32 string) * string list) * (Facts.ref * Token.src list) list option) * 33 (binding * binding * binding) -> local_theory -> Proof.state 34end 35 36structure BNF_Lift : BNF_LIFT = 37struct 38 39open Ctr_Sugar_Tactics 40open BNF_Util 41open BNF_Comp 42open BNF_Def 43 44 45datatype lift_bnf_option = 46 Plugins_Option of Proof.context -> Plugin_Name.filter 47| No_Warn_Wits 48| No_Warn_Transfer; 49 50datatype equiv_thm = Typedef | Quotient of thm 51 52(** Util **) 53 54fun last2 [x, y] = ([], (x, y)) 55 | last2 (x :: xs) = last2 xs |>> (fn y => x :: y) 56 | last2 [] = raise Match; 57 58fun 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 62val mk_Free = yield_singleton o mk_Frees; 63 64fun TWICE t = t THEN' t; 65 66fun 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 71fun mk_relT aT bT = aT --> bT --> HOLogic.boolT; 72fun 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; 77val mk_OO = fold_rev mk_relcompp; 78 79(* option from sum *) 80fun mk_MaybeT T = mk_sumT (HOLogic.unitT, T); 81fun mk_Nothing T = BNF_FP_Util.mk_Inl T HOLogic.unit; 82val Just_const = BNF_FP_Util.Inr_const HOLogic.unitT; 83fun mk_Just tm = Just_const (fastype_of tm) $ tm; 84fun 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; 89fun mk_Maybe_map tm = Maybe_map_const (fastype_of tm) $ tm; 90fun fromJust_const T = Const (@{const_name sum.projr}, mk_MaybeT T --> T) 91 92fun 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 96fun set_Maybe_const T = Const (@{const_name Basic_BNFs.setr}, mk_MaybeT T --> HOLogic.mk_setT T) 97 98fun Inf_const T = Const (@{const_name Inf}, HOLogic.mk_setT T --> T); 99 100fun 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 106fun bot_const T = Const (@{const_name bot}, T); 107 108fun mk_insert x S = 109 Const (@{const_name Set.insert}, fastype_of x --> fastype_of S --> fastype_of S) $ x $ S; 110 111fun 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 116fun 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 123fun mk_Trueprop_implies (ps, c) = 124 Logic.list_implies (map HOLogic.mk_Trueprop ps, HOLogic.mk_Trueprop c); 125 126fun mk_Collect (v, tm) = let val (n, T) = dest_Free v in 127 HOLogic.mk_Collect (n, T, tm) end; 128 129 130(** witnesses **) 131fun 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 143 val Iwits = if is_quotient then 144 let 145 val subsumed_Iwits = 146 filter (fn (J, _) => exists (fn (I, _) => subset (op =) (I, J)) wits_F) Iwits; 147 val _ = if null subsumed_Iwits orelse exists (fn No_Warn_Wits => true | _ => false) opts 148 then () 149 else 150 let 151 val (suffix1, suffix2, be) = 152 (if length subsumed_Iwits = 1 then ("", "", "is") else ("s", "es", "are")) 153 in 154 subsumed_Iwits 155 |> map (Syntax.pretty_typ lthy o fastype_of o snd) 156 |> Pretty.big_list 157 ("The following type" ^ suffix1 ^ " of nonemptiness witness" ^ suffix2 ^ 158 " of the raw type's BNF " ^ be ^ " subsumed by the existing raw witnesses:") 159 |> (fn pt => Pretty.chunks [pt, 160 Pretty.para ("You do not need to lift these subsumed witnesses.")]) 161 |> Pretty.string_of 162 |> warning 163 end; 164 in 165 filter_out (fn (J, _) => exists (fn (I, _) => subset (op =) (I, J)) wits_F) Iwits 166 end 167 else Iwits; 168 169 val wit_goals = maps (BNF_Def.mk_wit_goals var_as var_as' sets) Iwits; 170 171 val lost_wits = if is_quotient then [] else 172 filter_out (fn (J, _) => exists (fn (I, _) => subset (op =) (I, J)) Iwits) wits_F; 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 199fun 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 *) 325fun 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] 330 | Typedef => hd ([quot_thm] RL @{thms Quotient_crel_typedef Quotient_crel_typecopy})); 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 368fun 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; 407 408fun typedef_bnf thm wits specs map_b rel_b pred_b opts lthy = 409 let 410 val plugins = 411 get_first (fn Plugins_Option f => SOME (f lthy) | _ => NONE) (rev opts) 412 |> the_default Plugin_Name.default_filter; 413 414 (* extract Rep Abs F RepT AbsT *) 415 val (Rep_G, Abs_G, F) = strip3 thm; 416 val typ_Abs_G = dest_funT (fastype_of Abs_G); 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; 422 423 val _ = length tvs = length alpha0s orelse 424 error ("Expected " ^ string_of_int (length tvs) ^ " type argument(s) to " ^ quote AbsT_name); 425 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 436 fun flatten_tyargs Ass = 437 map dest_TFree alpha0s 438 |> filter (fn T => exists (fn Ts => member op= Ts T) Ass); 439 440 val Ds0 = filter (is_none o fst) specs |> map snd; 441 442 (* get the bnf for RepT *) 443 val ((bnf_F, (deads, alphas)), ((_, unfolds), lthy)) = 444 bnf_of_typ true Dont_Inline (Binding.qualify true AbsT_name) flatten_tyargs [] 445 Ds0 RepT ((empty_comp_cache, empty_unfolds), lthy); 446 447 val set_bs = 448 map (fn T => find_index (fn U => T = U) alpha0s) alphas 449 |> map (the_default Binding.empty o fst o nth specs); 450 451 val _ = (case alphas of [] => error "No live variables" | _ => ()); 452 453 val defs = #map_unfolds unfolds @ flat (#set_unfoldss unfolds) @ #rel_unfolds unfolds @ #pred_unfolds unfolds; 454 455 (* number of live variables *) 456 val live = length alphas; 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; 461 val (((alphas', betas), betas'), names_lthy) = names_lthy 462 |> mk_TFrees' sorts 463 ||>> mk_TFrees' sorts 464 ||>> mk_TFrees' sorts; 465 466 val map_F = mk_map_of_bnf deads alphas betas bnf_F; 467 468 val (typ_fs, typ_aF) = fastype_of map_F |> strip_typeN live ||> domain_type; 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; 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 482 val wits_F = mk_wits_of_bnf 483 (replicate (nwits_of_bnf bnf_F) deads) 484 (replicate (nwits_of_bnf bnf_F) alphas) bnf_F; 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; 489 val mem_x = HOLogic.mk_Trueprop (HOLogic.mk_mem (var_x, aF_set)); 490 val map_f = list_comb (map_F, var_fs); 491 val mem_map = HOLogic.mk_Trueprop (HOLogic.mk_mem (map_f $ var_x, bF_set)); 492 val imp_map = Logic.mk_implies (mem_x, mem_map); 493 val map_closed_F = fold_rev Logic.all var_fs (Logic.all var_x imp_map); 494 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; 500 val (pairs, names_lthy) = mk_Frees "tmp" typ_pairs names_lthy; 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); 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')); 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)); 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; 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; 520 val wit_closed_Fs = 521 Iwits |> map (fn (I, wit_F) => 522 let 523 val vars = map (nth var_as) I; 524 val wit_a = list_comb (wit_F, vars); 525 in fold_rev Logic.all vars (HOLogic.mk_Trueprop (HOLogic.mk_mem (wit_a, aF_set))) end); 526 527 val goals = [map_closed_F, zip_closed_F] @ wit_closed_Fs @ 528 (case wits of NONE => [] | _ => wit_goals); 529 530 fun after_qed ([map_closed_thm] :: [zip_closed_thm] :: wit_thmss) lthy = 531 let 532 val (wit_closed_thms, wit_thms) = 533 (case wits of 534 NONE => (map the_single wit_thmss, wit_thms_of_bnf bnf_F) 535 | _ => chop (length wit_closed_Fs) (map the_single wit_thmss)) 536 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; 540 val map_G = fold_rev lambda var_fs 541 (HOLogic.mk_comp (HOLogic.mk_comp (Abs_Gb, map_f), Rep_G)); 542 val map_raw = fold_rev lambda var_fs map_f; 543 544 (* val sets_G = [@{term "set_F o Rep_G"}]; *) 545 val sets_F = mk_sets_of_bnf (replicate live deads) (replicate live alphas) bnf_F; 546 val sets_G = map (fn set_F => HOLogic.mk_comp (set_F, Rep_G)) sets_F; 547 548 (* val bd_G = @{term "bd_F"}; *) 549 val bd_F = mk_bd_of_bnf deads alphas bnf_F; 550 val bd_G = bd_F; 551 552 (* val rel_G = @{term "\<lambda>R. BNF_Def.vimage2p Rep_G Rep_G (rel_F R)"}; *) 553 val rel_F = mk_rel_of_bnf deads alphas betas bnf_F; 554 val (typ_Rs, _) = strip_typeN live (fastype_of rel_F); 555 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)); 560 val rel_raw = fold_rev absfree (map dest_Free var_Rs) (list_comb (rel_F, var_Rs)); 561 562 (* val pred_G = @{term "\<lambda>P. pred_F P o Rep_G"}; *) 563 val pred_F = mk_pred_of_bnf deads alphas bnf_F; 564 val (typ_Ps, _) = strip_typeN live (fastype_of pred_F); 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)); 569 val pred_raw = fold_rev absfree (map dest_Free var_Ps) (list_comb (pred_F, var_Ps)); 570 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; 579 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}; 586 587 fun map_id0_tac ctxt = 588 HEADGOAL (EVERY' [rtac ctxt ext, 589 SELECT_GOAL (unfold_thms_tac ctxt [map_id0_of_bnf bnf_F, id_apply, o_apply, 590 Rep_inverse_thm]), 591 rtac ctxt refl]); 592 593 fun map_comp0_tac ctxt = 594 HEADGOAL (EVERY' [rtac ctxt ext, 595 SELECT_GOAL (unfold_thms_tac ctxt [map_comp0_of_bnf bnf_F, o_apply, 596 Rep_thm RS (map_closed_thm RS Abs_inverse_thm)]), 597 rtac ctxt refl]); 598 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), 603 rtac ctxt (map_cong0_of_bnf bnf_F)] @ replicate live (Goal.assume_rule_tac ctxt))); 604 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])) 611 (set_map_of_bnf bnf_F); 612 613 fun card_order_bd_tac ctxt = HEADGOAL (rtac ctxt (bd_card_order_of_bnf bnf_F)); 614 615 fun cinfinite_bd_tac ctxt = HEADGOAL (rtac ctxt (bd_cinfinite_of_bnf bnf_F)); 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])) 620 (set_bd_of_bnf bnf_F); 621 622 fun le_rel_OO_tac ctxt = 623 HEADGOAL (EVERY' [rtac ctxt @{thm vimage2p_relcompp_mono}, 624 rtac ctxt ((rel_OO_of_bnf bnf_F RS sym) RS @{thm ord_eq_le_trans}), 625 rtac ctxt @{thm order_refl}]); 626 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, 630 o_apply, @{thm vimage2p_def}, in_rel_of_bnf bnf_F, Bex_def, mem_Collect_eq]), 631 rtac ctxt iffI, 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})))], 635 assume_tac ctxt, 636 SELECT_GOAL (REPEAT_DETERM (HEADGOAL (eresolve_tac ctxt [bexE, conjE]))), 637 etac ctxt Rep_cases_thm, 638 hyp_subst_tac ctxt, 639 SELECT_GOAL (REPEAT_DETERM (HEADGOAL (rtac ctxt exI))), 640 rtac ctxt conjI] @ 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]))), 649 rtac ctxt exI, 650 rtac ctxt conjI] @ 651 replicate (live-1) (rtac ctxt conjI THEN' assume_tac ctxt) @ 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))]])); 657 658 fun pred_set_tac ctxt = 659 HEADGOAL (EVERY' 660 [rtac ctxt (pred_set_of_bnf bnf_F RS @{thm arg_cong[of _ _ "\<lambda>f. f \<circ> _"]} RS trans), 661 SELECT_GOAL (unfold_thms_tac ctxt (@{thms Ball_comp_iff conj_comp_iff})), 662 rtac ctxt refl]); 663 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)); 671 672 val tactics = [map_id0_tac, map_comp0_tac, map_cong0_tac] @ set_map0s_tac @ 673 [card_order_bd_tac, cinfinite_bd_tac] @ set_bds_tac @ 674 [le_rel_OO_tac, rel_OO_Grp_tac, pred_set_tac]; 675 676 val (bnf_G, lthy) = bnf_def Dont_Inline (user_policy Note_Some) true I 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) 679 lthy; 680 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 687 |> (fn bnf => note_bnf_defs bnf lthy); 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; 693 in 694 lthy |> BNF_Def.register_bnf plugins AbsT_name bnf_G |> 695 mk_transfer_thms quiet bnf_F bnf_G AbsT_name transfer_consts Typedef 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 698 end 699 | after_qed _ _ = raise Match; 700 in 701 (goals, after_qed, defs, lthy) 702 end; 703 704 705(** quotient_bnf **) 706 707fun 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 834fun quotient_bnf (equiv_thm, quot_thm) wits specs map_b rel_b pred_b opts lthy = 835 let 836 (* extract rep_G and abs_G *) 837 val (equiv_rel, abs_G, rep_G) = strip3 quot_thm; 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 932 |> Local_Theory.open_target |> snd 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 1037 val goals = rel_pos_distr :: rel_Inters @ 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 = 1045 (case thmss of [rel_pos_distr_thm0] :: thmss => 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; 1115 val rel_flip = rel_flip_of_bnf bnf_F; 1116 val rel_eq_onp = rel_eq_onp_of_bnf bnf_F; 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 1124 1125 1126 (* map_F_respect: @{term "((=) ===> REL ===> REL) map_F map_F"} *) 1127 val map_F_respect = HOLogic.mk_Trueprop (fold_rev mk_rel_fun (map2 (fn xT => fn yT => 1128 HOLogic.eq_const (xT --> yT)) alphas betas @ [equiv_rel_a]) (equiv_rel_b) $ map_F $ map_F); 1129 1130 fun map_F_respect_tac ctxt = 1131 HEADGOAL (EVERY' 1132 [REPEAT_DETERM_N (live + 1) o rtac ctxt @{thm rel_funI}, hyp_subst_tac ctxt, 1133 rtac ctxt (BNF_FP_Util.split_conj_prems live rel_pos_distr_thm0 OF 1134 replicate live @{thm Grp_conversep_nonempty} RS rev_mp), 1135 rtac ctxt impI, dtac ctxt @{thm predicate2D}, etac ctxt @{thm relcomppI2[rotated]}, 1136 rtac ctxt (rel_Grp RS @{thm predicate2_eqD} RS iffD2), rtac ctxt @{thm GrpI[OF refl]}, 1137 REPEAT_DETERM o resolve_tac ctxt [CollectI, conjI, subset_UNIV], 1138 rtac ctxt (rel_flip RS iffD2), 1139 rtac ctxt (rel_Grp RS @{thm predicate2_eqD} RS iffD2), rtac ctxt @{thm GrpI[OF refl]}, 1140 REPEAT_DETERM o resolve_tac ctxt [CollectI, conjI, subset_UNIV], 1141 SELECT_GOAL (unfold_thms_tac ctxt (rel_eq_onp :: @{thms Grp_conversep_eq_onp})), 1142 etac ctxt @{thm predicate2D[OF rel_conj_eq_onp, rotated]}, 1143 rtac ctxt equiv_thm']); 1144 1145 val map_F_respect_thm = prove lthy [] map_F_respect map_F_respect_tac; 1146 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 1866 (* val wits_G = [abs_G o wit_F] *) 1867 val (wits_G, wit_thms) = 1868 let 1869 val wit_F_thmss = map (map2 (fn set_F' => fn wit => 1870 (#set_F'_subset set_F' RS set_mp RS wit) 1871 |> unfold_thms lthy [#set_F'_def set_F']) set_F'_thmss) 1872 (wit_thmss_of_bnf bnf_F); 1873 val (wits_F, wit_F_thmss) = split_list 1874 (filter_out (fn ((J, _), _) => exists (fn (I, _) => subset (op =) (I, J)) Iwits) 1875 (wits_F ~~ wit_F_thmss)); 1876 fun mk_wit (I, wit) = let val vars = (map (fn n => nth var_as n) I) 1877 in fold_rev lambda vars (abs_G $ list_comb (wit, vars)) end; 1878 in 1879 (map mk_wit (Iwits @ wits_F), wit_thmss @ flat wit_F_thmss) 1880 end; 1881 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 **) 1966 1967local 1968 1969fun prepare_common prepare_name prepare_sort prepare_term prepare_thm 1970 (((((plugins, raw_specs), raw_absT_name), raw_wits), xthms_opt), (map_b, rel_b, pred_b)) lthy = 1971 let 1972 val absT_name = prepare_name lthy raw_absT_name; 1973 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, ...} => 2015 let 2016 val qthm = Thm.transfer' lthy qthm; 2017 in 2018 case [qthm] RL @{thms Quotient_eq_onp_typedef Quotient_eq_onp_type_copy} of 2019 thm :: _ => (thm, Typedef) 2020 | _ => (qthm RS @{thm Quotient_Quotient3}, 2021 Quotient (find_equiv_thm_via_Quotient qthm)) 2022 end 2023 | NONE => (Typedef.get_info lthy absT_name |> hd |> snd |> #type_definition, Typedef)) 2024 | SOME thms => bad_input thms); 2025 val wits = (Option.map o map) (prepare_term lthy) raw_wits; 2026 val specs = 2027 map (apsnd (apsnd (the_default @{sort type} o Option.map (prepare_sort lthy)))) raw_specs; 2028 2029 val which_bnf = (case equiv_thm of 2030 Quotient thm => quotient_bnf (thm, lift_thm) 2031 | Typedef => typedef_bnf lift_thm); 2032 in 2033 which_bnf wits specs map_b rel_b pred_b plugins lthy 2034 end; 2035 2036fun prepare_lift_bnf prepare_name prepare_sort prepare_term prepare_thm = 2037 (fn (goals, after_qed, definitions, lthy) => 2038 lthy 2039 |> Proof.theorem NONE after_qed (map (single o rpair []) goals) 2040 |> Proof.refine_singleton 2041 (Method.Basic (fn ctxt => SIMPLE_METHOD (unfold_thms_tac ctxt definitions))) 2042 |> Proof.refine_singleton (Method.primitive_text (K I))) oo 2043 prepare_common prepare_name prepare_sort prepare_term prepare_thm o apfst (apfst (apsnd SOME)); 2044 2045fun prepare_solve prepare_name prepare_typ prepare_sort prepare_thm tacs = 2046 (fn (goals, after_qed, definitions, lthy) => 2047 lthy 2048 |> after_qed (map2 (fn goal => fn tac => [Goal.prove_sorry lthy [] [] goal 2049 (fn (ctxtprems as {context = ctxt, prems = _}) => 2050 unfold_thms_tac ctxt definitions THEN tac ctxtprems)]) 2051 goals (tacs (length goals)))) oo 2052 prepare_common prepare_name prepare_typ prepare_sort prepare_thm; 2053 2054in 2055 2056val lift_bnf_cmd = 2057 prepare_lift_bnf 2058 (fst o dest_Type oo Proof_Context.read_type_name {proper = true, strict = false}) 2059 Syntax.read_sort Syntax.read_term Attrib.eval_thms; 2060 2061fun lift_bnf args tacs = 2062 prepare_solve (K I) (K I) (K I) (K I) (K tacs) args; 2063 2064fun copy_bnf_tac {context = ctxt, prems = _} = 2065 REPEAT_DETERM (resolve_tac ctxt [bexI, conjI, UNIV_I, refl, subset_refl] 1); 2066 2067val copy_bnf = 2068 apfst (apfst (rpair NONE)) 2069 #> apfst (apsnd (Option.map single)) 2070 #> prepare_solve (K I) (K I) (K I) (K I) 2071 (fn n => replicate n copy_bnf_tac); 2072 2073val copy_bnf_cmd = 2074 apfst (apfst (rpair NONE)) 2075 #> apfst (apsnd (Option.map single)) 2076 #> prepare_solve 2077 (fst o dest_Type oo Proof_Context.read_type_name {proper = true, strict = false}) 2078 Syntax.read_sort Syntax.read_term Attrib.eval_thms 2079 (fn n => replicate n copy_bnf_tac); 2080 2081end; 2082 2083(** outer syntax **) 2084 2085local 2086 2087(* parsers *) 2088 2089val parse_wits = 2090 @{keyword "["} |-- (Parse.name --| @{keyword ":"} -- Scan.repeat Parse.term >> 2091 (fn ("wits", Ts) => Ts 2092 | (s, _) => error ("Unknown label " ^ quote s ^ " (expected \"wits\")"))) --| 2093 @{keyword "]"} || Scan.succeed []; 2094 2095fun parse_common_opts p = 2096 Scan.optional (@{keyword "("} |-- 2097 Parse.list1 (Parse.group (K "option") 2098 (Scan.first (p :: [Plugin_Name.parse_filter >> Plugins_Option, 2099 Parse.reserved "no_warn_transfer" >> K No_Warn_Transfer]))) 2100 --| @{keyword ")"}) []; 2101 2102val parse_lift_opts = Parse.reserved "no_warn_wits" >> K No_Warn_Wits |> parse_common_opts; 2103 2104val parse_copy_opts = parse_common_opts Scan.fail; 2105 2106val parse_xthm = Scan.option (Parse.reserved "via" |-- Parse.thm); 2107val parse_xthms = Scan.option (Parse.reserved "via" |-- Parse.thms1); 2108 2109in 2110 2111(* exposed commands *) 2112 2113val _ = 2114 Outer_Syntax.local_theory_to_proof @{command_keyword lift_bnf} 2115 "register a quotient type/subtype of a bounded natural functor (BNF) as a BNF" 2116 ((parse_lift_opts -- parse_type_args_named_constrained -- Parse.type_const -- parse_wits -- 2117 parse_xthms -- parse_map_rel_pred_bindings) >> lift_bnf_cmd); 2118 2119val _ = 2120 Outer_Syntax.local_theory @{command_keyword copy_bnf} 2121 "register a type copy of a bounded natural functor (BNF) as a BNF" 2122 ((parse_copy_opts -- parse_type_args_named_constrained -- Parse.type_const -- 2123 parse_xthm -- parse_map_rel_pred_bindings) >> copy_bnf_cmd); 2124 2125end; 2126 2127end; 2128