1(* Title: HOL/Tools/Lifting/lifting_def_code_dt.ML 2 Author: Ondrej Kuncar 3 4Workaround that allows us to execute lifted constants that have 5as a return type a datatype containing a subtype; lift_definition command 6*) 7 8signature LIFTING_DEF_CODE_DT = 9sig 10 type rep_isom_data 11 val isom_of_rep_isom_data: rep_isom_data -> term 12 val transfer_of_rep_isom_data: rep_isom_data -> thm 13 val bundle_name_of_rep_isom_data: rep_isom_data -> string 14 val pointer_of_rep_isom_data: rep_isom_data -> string 15 16 type code_dt 17 val rty_of_code_dt: code_dt -> typ 18 val qty_of_code_dt: code_dt -> typ 19 val wit_of_code_dt: code_dt -> term 20 val wit_thm_of_code_dt: code_dt -> thm 21 val rep_isom_data_of_code_dt: code_dt -> rep_isom_data option 22 val morph_code_dt: morphism -> code_dt -> code_dt 23 val mk_witness_of_code_dt: typ -> code_dt -> term 24 val mk_rep_isom_of_code_dt: typ -> code_dt -> term option 25 26 val code_dt_of: Proof.context -> typ * typ -> code_dt option 27 val code_dt_of_global: theory -> typ * typ -> code_dt option 28 val all_code_dt_of: Proof.context -> code_dt list 29 val all_code_dt_of_global: theory -> code_dt list 30 31 type config_code_dt = { code_dt: bool, lift_config: Lifting_Def.config } 32 val default_config_code_dt: config_code_dt 33 34 val add_lift_def_code_dt: 35 config_code_dt -> binding * mixfix -> typ -> term -> thm -> thm list -> local_theory -> 36 Lifting_Def.lift_def * local_theory 37 38 val lift_def_code_dt: 39 config_code_dt -> binding * mixfix -> typ -> term -> (Proof.context -> tactic) -> thm list -> 40 local_theory -> Lifting_Def.lift_def * local_theory 41 42 val lift_def_cmd: 43 string list * (binding * string option * mixfix) * string * (Facts.ref * Token.src list) list -> 44 local_theory -> Proof.state 45end 46 47structure Lifting_Def_Code_Dt: LIFTING_DEF_CODE_DT = 48struct 49 50open Ctr_Sugar_Util BNF_Util BNF_FP_Util BNF_FP_Def_Sugar Lifting_Def Lifting_Util 51 52infix 0 MRSL 53 54(** data structures **) 55 56(* all type variables in qty are in rty *) 57datatype rep_isom_data = REP_ISOM of { isom: term, transfer: thm, bundle_name: string, pointer: string } 58fun isom_of_rep_isom_data (REP_ISOM rep_isom) = #isom rep_isom; 59fun transfer_of_rep_isom_data (REP_ISOM rep_isom) = #transfer rep_isom; 60fun bundle_name_of_rep_isom_data (REP_ISOM rep_isom) = #bundle_name rep_isom; 61fun pointer_of_rep_isom_data (REP_ISOM rep_isom) = #pointer rep_isom; 62 63datatype code_dt = CODE_DT of { rty: typ, qty: typ, wit: term, wit_thm: thm, 64 rep_isom_data: rep_isom_data option }; 65fun rty_of_code_dt (CODE_DT code_dt) = #rty code_dt; 66fun qty_of_code_dt (CODE_DT code_dt) = #qty code_dt; 67fun wit_of_code_dt (CODE_DT code_dt) = #wit code_dt; 68fun wit_thm_of_code_dt (CODE_DT code_dt) = #wit_thm code_dt; 69fun rep_isom_data_of_code_dt (CODE_DT code_dt) = #rep_isom_data code_dt; 70fun ty_alpha_equiv (T, U) = Type.raw_instance (T, U) andalso Type.raw_instance (U, T); 71fun code_dt_eq c = (ty_alpha_equiv o apply2 rty_of_code_dt) c 72 andalso (ty_alpha_equiv o apply2 qty_of_code_dt) c; 73fun term_of_code_dt code_dt = code_dt |> `rty_of_code_dt ||> qty_of_code_dt |> HOLogic.mk_prodT 74 |> Net.encode_type |> single; 75 76(* modulo renaming, typ must contain TVars *) 77fun is_code_dt_of_type (rty, qty) code_dt = code_dt |> `rty_of_code_dt ||> qty_of_code_dt 78 |> HOLogic.mk_prodT |> curry ty_alpha_equiv (HOLogic.mk_prodT (rty, qty)); 79 80fun mk_rep_isom_data isom transfer bundle_name pointer = 81 REP_ISOM { isom = isom, transfer = transfer, bundle_name = bundle_name, pointer = pointer} 82 83fun mk_code_dt rty qty wit wit_thm rep_isom_data = 84 CODE_DT { rty = rty, qty = qty, wit = wit, wit_thm = wit_thm, rep_isom_data = rep_isom_data }; 85 86fun map_rep_isom_data f1 f2 f3 f4 87 (REP_ISOM { isom = isom, transfer = transfer, bundle_name = bundle_name, pointer = pointer }) = 88 REP_ISOM { isom = f1 isom, transfer = f2 transfer, bundle_name = f3 bundle_name, pointer = f4 pointer }; 89 90fun map_code_dt f1 f2 f3 f4 f5 f6 f7 f8 91 (CODE_DT {rty = rty, qty = qty, wit = wit, wit_thm = wit_thm, rep_isom_data = rep_isom_data}) = 92 CODE_DT {rty = f1 rty, qty = f2 qty, wit = f3 wit, wit_thm = f4 wit_thm, 93 rep_isom_data = Option.map (map_rep_isom_data f5 f6 f7 f8) rep_isom_data}; 94 95fun update_rep_isom isom transfer binding pointer i = mk_code_dt (rty_of_code_dt i) (qty_of_code_dt i) 96 (wit_of_code_dt i) (wit_thm_of_code_dt i) (SOME (mk_rep_isom_data isom transfer binding pointer)) 97 98fun morph_code_dt phi = 99 let 100 val mty = Morphism.typ phi 101 val mterm = Morphism.term phi 102 val mthm = Morphism.thm phi 103 in 104 map_code_dt mty mty mterm mthm mterm mthm I I 105 end 106 107val transfer_code_dt = morph_code_dt o Morphism.transfer_morphism; 108 109structure Data = Generic_Data 110( 111 type T = code_dt Item_Net.T 112 val empty = Item_Net.init code_dt_eq term_of_code_dt 113 val extend = I 114 val merge = Item_Net.merge 115); 116 117fun code_dt_of_generic context (rty, qty) = 118 let 119 val typ = HOLogic.mk_prodT (rty, qty) 120 val prefiltred = Item_Net.retrieve_matching (Data.get context) (Net.encode_type typ) 121 in 122 prefiltred |> filter (is_code_dt_of_type (rty, qty)) 123 |> map (transfer_code_dt (Context.theory_of context)) |> find_first (fn _ => true) 124 end; 125 126fun code_dt_of ctxt (rty, qty) = 127 let 128 val sch_rty = Logic.type_map (singleton (Variable.polymorphic ctxt)) rty 129 val sch_qty = Logic.type_map (singleton (Variable.polymorphic ctxt)) qty 130 in 131 code_dt_of_generic (Context.Proof ctxt) (sch_rty, sch_qty) 132 end; 133 134fun code_dt_of_global thy (rty, qty) = 135 let 136 val sch_rty = Logic.varifyT_global rty 137 val sch_qty = Logic.varifyT_global qty 138 in 139 code_dt_of_generic (Context.Theory thy) (sch_rty, sch_qty) 140 end; 141 142fun all_code_dt_of_generic context = 143 Item_Net.content (Data.get context) |> map (transfer_code_dt (Context.theory_of context)); 144 145val all_code_dt_of = all_code_dt_of_generic o Context.Proof; 146val all_code_dt_of_global = all_code_dt_of_generic o Context.Theory; 147 148fun update_code_dt code_dt = 149 Local_Theory.open_target #> snd 150 #> Local_Theory.declaration {syntax = false, pervasive = true} 151 (fn phi => Data.map (Item_Net.update (morph_code_dt phi code_dt))) 152 #> Local_Theory.close_target 153 154fun mk_match_of_code_dt qty code_dt = Vartab.empty |> Type.raw_match (qty_of_code_dt code_dt, qty) 155 |> Vartab.dest |> map (fn (x, (S, T)) => (TVar (x, S), T)); 156 157fun mk_witness_of_code_dt qty code_dt = 158 Term.subst_atomic_types (mk_match_of_code_dt qty code_dt) (wit_of_code_dt code_dt) 159 160fun mk_rep_isom_of_code_dt qty code_dt = Option.map 161 (isom_of_rep_isom_data #> Term.subst_atomic_types (mk_match_of_code_dt qty code_dt)) 162 (rep_isom_data_of_code_dt code_dt) 163 164 165(** unique name for a type **) 166 167fun var_name name sort = if sort = \<^sort>\<open>{type}\<close> orelse sort = [] then ["x" ^ name] 168 else "x" ^ name :: "x_" :: sort @ ["x_"]; 169 170fun concat_Tnames (Type (name, ts)) = name :: maps concat_Tnames ts 171 | concat_Tnames (TFree (name, sort)) = var_name name sort 172 | concat_Tnames (TVar ((name, _), sort)) = var_name name sort; 173 174fun unique_Tname (rty, qty) = 175 let 176 val Tnames = map Long_Name.base_name (concat_Tnames rty @ ["x_x"] @ concat_Tnames qty); 177 in 178 fold (Binding.qualify false) (tl Tnames) (Binding.name (hd Tnames)) 179 end; 180 181(** witnesses **) 182 183fun mk_undefined T = Const (\<^const_name>\<open>undefined\<close>, T); 184 185fun mk_witness quot_thm = 186 let 187 val wit_thm = quot_thm RS @{thm type_definition_Quotient_not_empty_witness} 188 val wit = quot_thm_rep quot_thm $ mk_undefined (quot_thm_rty_qty quot_thm |> snd) 189 in 190 (wit, wit_thm) 191 end 192 193(** config **) 194 195type config_code_dt = { code_dt: bool, lift_config: config } 196val default_config_code_dt = { code_dt = false, lift_config = default_config } 197 198 199(** Main code **) 200 201val ld_no_notes = { notes = false } 202 203fun comp_lift_error _ _ = error "Composition of abstract types has not been implemented yet." 204 205fun lift qty (quot_thm, (lthy, rel_eq_onps)) = 206 let 207 val quot_thm = Lifting_Term.force_qty_type lthy qty quot_thm 208 val (rty, qty) = quot_thm_rty_qty quot_thm; 209 in 210 if is_none (code_dt_of lthy (rty, qty)) then 211 let 212 val (wit, wit_thm) = (mk_witness quot_thm 213 handle THM _ => error ("code_dt: " ^ quote (Tname qty) ^ " was not defined as a subtype.")) 214 val code_dt = mk_code_dt rty qty wit wit_thm NONE 215 in 216 (quot_thm, (update_code_dt code_dt lthy, rel_eq_onps)) 217 end 218 else 219 (quot_thm, (lthy, rel_eq_onps)) 220 end; 221 222fun case_tac rule = 223 Subgoal.FOCUS_PARAMS (fn {context = ctxt, params, ...} => 224 HEADGOAL (rtac ctxt (infer_instantiate' ctxt [SOME (snd (hd params))] rule))); 225 226fun bundle_name_of_bundle_binding binding phi context = 227 Name_Space.full_name (Name_Space.naming_of context) (Morphism.binding phi binding); 228 229fun prove_schematic_quot_thm actions ctxt = 230 Lifting_Term.prove_schematic_quot_thm actions (Lifting_Info.get_quotients ctxt) ctxt 231 232fun prove_code_dt (rty, qty) lthy = 233 let 234 val (fold_quot_thm: (local_theory * thm list) Lifting_Term.fold_quot_thm) = 235 { constr = constr, lift = lift, comp_lift = comp_lift_error }; 236 in prove_schematic_quot_thm fold_quot_thm lthy (rty, qty) (lthy, []) |> snd end 237and add_lift_def_code_dt config var qty rhs rsp_thm par_thms lthy = 238 let 239 fun binop_conv2 cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2 240 fun ret_rel_conv conv ctm = 241 case (Thm.term_of ctm) of 242 Const (\<^const_name>\<open>rel_fun\<close>, _) $ _ $ _ => 243 binop_conv2 Conv.all_conv conv ctm 244 | _ => conv ctm 245 fun R_conv rel_eq_onps = Transfer.top_sweep_rewr_conv @{thms eq_onp_top_eq_eq[symmetric, THEN eq_reflection]} 246 then_conv Transfer.bottom_rewr_conv rel_eq_onps 247 248 val (ret_lift_def, lthy1) = add_lift_def (#lift_config config) var qty rhs rsp_thm par_thms lthy 249 in 250 if (not (#code_dt config) orelse (code_eq_of_lift_def ret_lift_def <> NONE_EQ) 251 andalso (code_eq_of_lift_def ret_lift_def <> UNKNOWN_EQ)) 252 (* Let us try even in case of UNKNOWN_EQ. If this leads to problems, the user can always 253 say that they do not want this workaround. *) 254 then (ret_lift_def, lthy1) 255 else 256 let 257 val lift_def = inst_of_lift_def lthy1 qty ret_lift_def 258 val rty = rty_of_lift_def lift_def 259 val rty_ret = body_type rty 260 val qty_ret = body_type qty 261 262 val (lthy2, rel_eq_onps) = prove_code_dt (rty_ret, qty_ret) lthy1 263 val code_dt = code_dt_of lthy2 (rty_ret, qty_ret) 264 in 265 if is_none code_dt orelse is_none (rep_isom_data_of_code_dt (the code_dt)) 266 then (ret_lift_def, lthy2) 267 else 268 let 269 val code_dt = the code_dt 270 val rhs = dest_comb (rhs_of_lift_def lift_def) |> snd 271 val rep_isom_data = code_dt |> rep_isom_data_of_code_dt |> the 272 val pointer = pointer_of_rep_isom_data rep_isom_data 273 val quot_active = 274 Lifting_Info.lookup_restore_data lthy2 pointer |> the |> #quotient |> #quot_thm 275 |> Lifting_Info.lookup_quot_thm_quotients lthy2 |> is_some 276 val qty_code_dt_bundle_name = bundle_name_of_rep_isom_data rep_isom_data 277 val rep_isom = mk_rep_isom_of_code_dt qty_ret code_dt |> the 278 val lthy3 = if quot_active then lthy2 else Bundle.includes [qty_code_dt_bundle_name] lthy2 279 fun qty_isom_of_rep_isom rep = rep |> dest_Const |> snd |> domain_type 280 val qty_isom = qty_isom_of_rep_isom rep_isom 281 val f'_var = (Binding.suffix_name "_aux" (fst var), NoSyn); 282 val f'_qty = strip_type qty |> fst |> rpair qty_isom |> op ---> 283 val f'_rsp_rel = Lifting_Term.equiv_relation lthy3 (rty, f'_qty); 284 val rsp = rsp_thm_of_lift_def lift_def 285 val rel_eq_onps_conv = HOLogic.Trueprop_conv (Conv.fun2_conv (ret_rel_conv (R_conv rel_eq_onps))) 286 val rsp_norm = Conv.fconv_rule rel_eq_onps_conv rsp 287 val f'_rsp_goal = HOLogic.mk_Trueprop (f'_rsp_rel $ rhs $ rhs); 288 val f'_rsp = Goal.prove_sorry lthy3 [] [] f'_rsp_goal 289 (fn {context = ctxt, prems = _} => 290 HEADGOAL (CONVERSION (rel_eq_onps_conv) THEN' rtac ctxt rsp_norm)) 291 |> Thm.close_derivation \<^here> 292 val (f'_lift_def, lthy4) = add_lift_def ld_no_notes f'_var f'_qty rhs f'_rsp [] lthy3 293 val f'_lift_def = inst_of_lift_def lthy4 f'_qty f'_lift_def 294 val f'_lift_const = mk_lift_const_of_lift_def f'_qty f'_lift_def 295 val (args, args_ctxt) = mk_Frees "x" (binder_types qty) lthy4 296 val f_alt_def_goal_lhs = list_comb (lift_const_of_lift_def lift_def, args); 297 val f_alt_def_goal_rhs = rep_isom $ list_comb (f'_lift_const, args); 298 val f_alt_def_goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (f_alt_def_goal_lhs, f_alt_def_goal_rhs)); 299 fun f_alt_def_tac ctxt i = 300 EVERY' [Transfer.gen_frees_tac [] ctxt, DETERM o Transfer.transfer_tac true ctxt, 301 SELECT_GOAL (Local_Defs.unfold0_tac ctxt [id_apply]), rtac ctxt refl] i; 302 val rep_isom_transfer = transfer_of_rep_isom_data rep_isom_data 303 val (_, transfer_ctxt) = args_ctxt 304 |> Proof_Context.note_thms "" 305 (Binding.empty_atts, [([rep_isom_transfer], [Transfer.transfer_add])]) 306 val f_alt_def = 307 Goal.prove_sorry transfer_ctxt [] [] f_alt_def_goal 308 (fn {context = goal_ctxt, ...} => HEADGOAL (f_alt_def_tac goal_ctxt)) 309 |> Thm.close_derivation \<^here> 310 |> singleton (Variable.export transfer_ctxt lthy4) 311 val lthy5 = lthy4 312 |> Local_Theory.note ((Binding.empty, @{attributes [code]}), [f_alt_def]) 313 |> snd 314 (* if processing a mutual datatype (there is a cycle!) the corresponding quotient 315 will be needed later and will be forgotten later *) 316 |> (if quot_active then I else Lifting_Setup.lifting_forget pointer) 317 in 318 (ret_lift_def, lthy5) 319 end 320 end 321 end 322and mk_rep_isom qty_isom_bundle (rty, qty, qty_isom) lthy0 = 323 let 324 (* logical definition of qty qty_isom isomorphism *) 325 val uTname = unique_Tname (rty, qty) 326 fun eq_onp_to_top_tac ctxt = SELECT_GOAL (Local_Defs.unfold0_tac ctxt 327 (@{thm eq_onp_top_eq_eq[symmetric]} :: Lifting_Info.get_relator_eq_onp_rules ctxt)) 328 fun lift_isom_tac ctxt = HEADGOAL (eq_onp_to_top_tac ctxt 329 THEN' (rtac ctxt @{thm id_transfer})); 330 331 val (rep_isom_lift_def, lthy1) = lthy0 332 |> Local_Theory.open_target |> snd 333 |> lift_def ld_no_notes (Binding.qualify_name true uTname "Rep_isom", NoSyn) 334 (qty_isom --> qty) (HOLogic.id_const rty) lift_isom_tac [] 335 |>> inst_of_lift_def lthy0 (qty_isom --> qty); 336 val (abs_isom, lthy2) = lthy1 337 |> lift_def ld_no_notes (Binding.qualify_name true uTname "Abs_isom", NoSyn) 338 (qty --> qty_isom) (HOLogic.id_const rty) lift_isom_tac [] 339 |>> mk_lift_const_of_lift_def (qty --> qty_isom); 340 val rep_isom = lift_const_of_lift_def rep_isom_lift_def 341 342 val pointer = Lifting_Setup.pointer_of_bundle_binding lthy2 qty_isom_bundle 343 fun code_dt phi context = 344 code_dt_of lthy2 (rty, qty) |> the 345 |> update_rep_isom rep_isom (transfer_rules_of_lift_def rep_isom_lift_def |> hd) 346 (bundle_name_of_bundle_binding qty_isom_bundle phi context) pointer; 347 val lthy3 = lthy2 348 |> Local_Theory.declaration {syntax = false, pervasive = true} 349 (fn phi => fn context => Data.map (Item_Net.update (morph_code_dt phi (code_dt phi context))) context) 350 |> Local_Theory.close_target 351 352 (* in order to make the qty qty_isom isomorphism executable we have to define discriminators 353 and selectors for qty_isom *) 354 val (rty_name, typs) = dest_Type rty 355 val (_, qty_typs) = dest_Type qty 356 val fp = BNF_FP_Def_Sugar.fp_sugar_of lthy3 rty_name 357 val fp = if is_some fp then the fp 358 else error ("code_dt: " ^ quote rty_name ^ " is not a datatype.") 359 val ctr_sugar = fp |> #fp_ctr_sugar |> #ctr_sugar 360 val ctrs = map (Ctr_Sugar.mk_ctr typs) (#ctrs ctr_sugar); 361 val qty_ctrs = map (Ctr_Sugar.mk_ctr qty_typs) (#ctrs ctr_sugar); 362 val ctr_Tss = map (dest_Const #> snd #> binder_types) ctrs; 363 val qty_ctr_Tss = map (dest_Const #> snd #> binder_types) qty_ctrs; 364 365 val n = length ctrs; 366 val ks = 1 upto n; 367 val (xss, _) = mk_Freess "x" ctr_Tss lthy3; 368 369 fun sel_retT (rty' as Type (s, rtys'), qty' as Type (s', qtys')) = 370 if (rty', qty') = (rty, qty) then qty_isom else (if s = s' 371 then Type (s, map sel_retT (rtys' ~~ qtys')) else qty') 372 | sel_retT (_, qty') = qty'; 373 374 val sel_retTs = map2 (map2 (sel_retT oo pair)) ctr_Tss qty_ctr_Tss 375 376 fun lazy_prove_code_dt (rty, qty) lthy = 377 if is_none (code_dt_of lthy (rty, qty)) then prove_code_dt (rty, qty) lthy |> fst else lthy; 378 379 val lthy4 = fold2 (fold2 (lazy_prove_code_dt oo pair)) ctr_Tss sel_retTs lthy3 380 381 val sel_argss = @{map 4} (fn k => fn xs => @{map 2} (fn x => fn qty_ret => 382 (k, qty_ret, (xs, x)))) ks xss xss sel_retTs; 383 384 fun mk_sel_casex (_, _, (_, x)) = Ctr_Sugar.mk_case typs (x |> dest_Free |> snd) (#casex ctr_sugar); 385 val dis_casex = Ctr_Sugar.mk_case typs HOLogic.boolT (#casex ctr_sugar); 386 fun mk_sel_case_args lthy ctr_Tss ks (k, qty_ret, (xs, x)) = 387 let 388 val T = x |> dest_Free |> snd; 389 fun gen_undef_wit Ts wits = 390 case code_dt_of lthy (T, qty_ret) of 391 SOME code_dt => 392 (fold_rev (Term.lambda o curry Free Name.uu) Ts (mk_witness_of_code_dt qty_ret code_dt), 393 wit_thm_of_code_dt code_dt :: wits) 394 | NONE => (fold_rev (Term.lambda o curry Free Name.uu) Ts (mk_undefined T), wits) 395 in 396 @{fold_map 2} (fn Ts => fn k' => fn wits => 397 (if k = k' then (fold_rev Term.lambda xs x, wits) else gen_undef_wit Ts wits)) ctr_Tss ks [] 398 end; 399 fun mk_sel_rhs arg = 400 let val (sel_rhs, wits) = mk_sel_case_args lthy4 ctr_Tss ks arg 401 in (arg |> #2, wits, list_comb (mk_sel_casex arg, sel_rhs)) end; 402 fun mk_dis_case_args args k = map (fn (k', arg) => (if k = k' 403 then fold_rev Term.lambda arg \<^const>\<open>True\<close> else fold_rev Term.lambda arg \<^const>\<open>False\<close>)) args; 404 val sel_rhs = map (map mk_sel_rhs) sel_argss 405 val dis_rhs = map (fn k => list_comb (dis_casex, mk_dis_case_args (ks ~~ xss) k)) ks 406 val dis_qty = qty_isom --> HOLogic.boolT; 407 val dis_names = map (fn k => Binding.qualify_name true uTname ("dis" ^ string_of_int k)) ks; 408 409 val (diss, lthy5) = @{fold_map 2} (fn b => fn rhs => fn lthy => 410 lift_def ld_no_notes (b, NoSyn) dis_qty rhs (K all_tac) [] lthy 411 |>> mk_lift_const_of_lift_def dis_qty) dis_names dis_rhs lthy4 412 413 val unfold_lift_sel_rsp = @{lemma "(\<And>x. P1 x \<Longrightarrow> P2 (f x)) \<Longrightarrow> (rel_fun (eq_onp P1) (eq_onp P2)) f f" 414 by (simp add: eq_onp_same_args rel_fun_eq_onp_rel)} 415 416 fun lift_sel_tac exhaust_rule dt_rules wits ctxt i = 417 (Method.insert_tac ctxt wits THEN' 418 eq_onp_to_top_tac ctxt THEN' (* normalize *) 419 rtac ctxt unfold_lift_sel_rsp THEN' 420 case_tac exhaust_rule ctxt THEN_ALL_NEW ( 421 EVERY' [hyp_subst_tac ctxt, (* does not kill wits because = was rewritten to eq_onp top *) 422 Raw_Simplifier.rewrite_goal_tac ctxt (map safe_mk_meta_eq dt_rules), 423 REPEAT_DETERM o etac ctxt conjE, assume_tac ctxt])) i 424 val pred_simps = Transfer.lookup_pred_data lthy5 (Tname rty) |> the |> Transfer.pred_simps 425 val sel_tac = lift_sel_tac (#exhaust ctr_sugar) (#case_thms ctr_sugar @ pred_simps) 426 val sel_names = 427 map (fn (k, xs) => 428 map (fn k' => Binding.qualify_name true uTname ("sel" ^ string_of_int k ^ string_of_int k')) 429 (1 upto length xs)) (ks ~~ ctr_Tss); 430 val (selss, lthy6) = @{fold_map 2} (@{fold_map 2} (fn b => fn (qty_ret, wits, rhs) => fn lthy => 431 lift_def_code_dt { code_dt = true, lift_config = ld_no_notes } 432 (b, NoSyn) (qty_isom --> qty_ret) rhs (HEADGOAL o sel_tac wits) [] lthy 433 |>> mk_lift_const_of_lift_def (qty_isom --> qty_ret))) sel_names sel_rhs lthy5 434 435 (* now we can execute the qty qty_isom isomorphism *) 436 fun mk_type_definition newT oldT RepC AbsC A = 437 let 438 val typedefC = 439 Const (\<^const_name>\<open>type_definition\<close>, 440 (newT --> oldT) --> (oldT --> newT) --> HOLogic.mk_setT oldT --> HOLogic.boolT); 441 in typedefC $ RepC $ AbsC $ A end; 442 val typedef_goal = mk_type_definition qty_isom qty rep_isom abs_isom (HOLogic.mk_UNIV qty) |> 443 HOLogic.mk_Trueprop; 444 fun typ_isom_tac ctxt i = 445 EVERY' [ SELECT_GOAL (Local_Defs.unfold0_tac ctxt @{thms type_definition_def}), 446 DETERM o Transfer.transfer_tac true ctxt, 447 SELECT_GOAL (Local_Defs.unfold0_tac ctxt @{thms eq_onp_top_eq_eq}) (* normalize *), 448 Raw_Simplifier.rewrite_goal_tac ctxt 449 (map safe_mk_meta_eq @{thms id_apply simp_thms Ball_def}), 450 rtac ctxt TrueI] i; 451 452 val (_, transfer_ctxt) = 453 Proof_Context.note_thms "" 454 (Binding.empty_atts, 455 [(@{thms right_total_UNIV_transfer}, [Transfer.transfer_add]), 456 (@{thms Domain_eq_top}, [Transfer.transfer_domain_add])]) lthy6; 457 458 val quot_thm_isom = 459 Goal.prove_sorry transfer_ctxt [] [] typedef_goal 460 (fn {context = goal_ctxt, ...} => typ_isom_tac goal_ctxt 1) 461 |> Thm.close_derivation \<^here> 462 |> singleton (Variable.export transfer_ctxt lthy6) 463 |> (fn thm => @{thm UNIV_typedef_to_Quotient} OF [thm, @{thm reflexive}]) 464 val qty_isom_name = Tname qty_isom; 465 val quot_isom_rep = 466 let 467 val (quotients : Lifting_Term.quotients) = 468 Symtab.insert (Lifting_Info.quotient_eq) 469 (qty_isom_name, {quot_thm = quot_thm_isom, pcr_info = NONE}) Symtab.empty 470 val id_actions = { constr = K I, lift = K I, comp_lift = K I } 471 in 472 fn ctxt => fn (rty, qty) => Lifting_Term.prove_schematic_quot_thm id_actions quotients 473 ctxt (rty, qty) () |> fst |> Lifting_Term.force_qty_type ctxt qty 474 |> quot_thm_rep 475 end; 476 val (x, x_ctxt) = yield_singleton (mk_Frees "x") qty_isom lthy6; 477 478 fun mk_ctr ctr ctr_Ts sels = 479 let 480 val sel_ret_Ts = map (dest_Const #> snd #> body_type) sels; 481 482 fun rep_isom lthy t (rty, qty) = 483 let 484 val rep = quot_isom_rep lthy (rty, qty) 485 in 486 if is_Const rep andalso (rep |> dest_Const |> fst) = \<^const_name>\<open>id\<close> then 487 t else rep $ t 488 end; 489 in 490 @{fold 3} (fn sel => fn ctr_T => fn sel_ret_T => fn ctr => 491 ctr $ rep_isom x_ctxt (sel $ x) (ctr_T, sel_ret_T)) sels ctr_Ts sel_ret_Ts ctr 492 end; 493 494 (* stolen from Metis *) 495 exception BREAK_LIST 496 fun break_list (x :: xs) = (x, xs) 497 | break_list _ = raise BREAK_LIST 498 499 val (ctr, ctrs) = qty_ctrs |> rev |> break_list; 500 val (ctr_Ts, ctr_Tss) = qty_ctr_Tss |> rev |> break_list; 501 val (sel, rselss) = selss |> rev |> break_list; 502 val rdiss = rev diss |> tl; 503 504 val first_ctr = mk_ctr ctr ctr_Ts sel; 505 506 fun mk_If_ctr dis ctr ctr_Ts sel elsex = mk_If (dis$x) (mk_ctr ctr ctr_Ts sel) elsex; 507 508 val rhs = @{fold 4} mk_If_ctr rdiss ctrs ctr_Tss rselss first_ctr; 509 510 val rep_isom_code_goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (rep_isom$x, rhs)); 511 512 local 513 val rep_isom_code_tac_rules = map safe_mk_meta_eq @{thms refl id_apply if_splits simp_thms} 514 in 515 fun rep_isom_code_tac (ctr_sugar:Ctr_Sugar.ctr_sugar) ctxt i = 516 let 517 val exhaust = ctr_sugar |> #exhaust 518 val cases = ctr_sugar |> #case_thms 519 val map_ids = fp |> #fp_nesting_bnfs |> map BNF_Def.map_id0_of_bnf 520 val simp_rules = map safe_mk_meta_eq (cases @ map_ids) @ rep_isom_code_tac_rules 521 in 522 EVERY' [Transfer.gen_frees_tac [] ctxt, DETERM o (Transfer.transfer_tac true ctxt), 523 case_tac exhaust ctxt THEN_ALL_NEW EVERY' [hyp_subst_tac ctxt, 524 Raw_Simplifier.rewrite_goal_tac ctxt simp_rules, rtac ctxt TrueI ]] i 525 end 526 end 527 528 (* stolen from bnf_fp_n2m.ML *) 529 fun force_typ ctxt T = 530 Term.map_types Type_Infer.paramify_vars 531 #> Type.constraint T 532 #> singleton (Type_Infer_Context.infer_types ctxt); 533 534 (* The following tests that types in rty have corresponding arities imposed by constraints of 535 the datatype fp. Otherwise rep_isom_code_tac could fail (especially transfer in it) is such 536 a way that it is not easy to infer the problem with sorts. 537 *) 538 val _ = yield_singleton (mk_Frees "x") (#T fp) x_ctxt |> fst |> force_typ x_ctxt qty 539 540 val rep_isom_code = 541 Goal.prove_sorry x_ctxt [] [] rep_isom_code_goal 542 (fn {context = goal_ctxt, ...} => rep_isom_code_tac ctr_sugar goal_ctxt 1) 543 |> Thm.close_derivation \<^here> 544 |> singleton(Variable.export x_ctxt lthy6) 545 in 546 lthy6 547 |> snd o Local_Theory.note ((Binding.empty, @{attributes [code]}), [rep_isom_code]) 548 |> Lifting_Setup.lifting_forget pointer 549 |> pair (selss, diss, rep_isom_code) 550 end 551and constr qty (quot_thm, (lthy0, rel_eq_onps)) = 552 let 553 val quot_thm = Lifting_Term.force_qty_type lthy0 qty quot_thm 554 val (rty, qty) = quot_thm_rty_qty quot_thm 555 val rty_name = Tname rty; 556 val pred_data = Transfer.lookup_pred_data lthy0 rty_name 557 val pred_data = if is_some pred_data then the pred_data 558 else error ("code_dt: " ^ quote rty_name ^ " is not a datatype.") 559 val rel_eq_onp = safe_mk_meta_eq (Transfer.rel_eq_onp pred_data); 560 val rel_eq_onps = insert Thm.eq_thm rel_eq_onp rel_eq_onps 561 val R_conv = Transfer.top_sweep_rewr_conv @{thms eq_onp_top_eq_eq[symmetric, THEN eq_reflection]} 562 then_conv Conv.rewr_conv rel_eq_onp 563 val quot_thm = Conv.fconv_rule(HOLogic.Trueprop_conv (Quotient_R_conv R_conv)) quot_thm; 564 in 565 if is_none (code_dt_of lthy0 (rty, qty)) then 566 let 567 val non_empty_pred = quot_thm RS @{thm type_definition_Quotient_not_empty} 568 val pred = quot_thm_rel quot_thm |> dest_comb |> snd; 569 val (pred, lthy1) = lthy0 570 |> Local_Theory.open_target |> snd 571 |> yield_singleton (Variable.import_terms true) pred; 572 val TFrees = Term.add_tfreesT qty [] 573 574 fun non_empty_typedef_tac non_empty_pred ctxt i = 575 (Method.insert_tac ctxt [non_empty_pred] THEN' 576 SELECT_GOAL (Local_Defs.unfold0_tac ctxt [mem_Collect_eq]) THEN' assume_tac ctxt) i 577 val uTname = unique_Tname (rty, qty) 578 val Tdef_set = HOLogic.mk_Collect ("x", rty, pred $ Free("x", rty)); 579 val ((_, tcode_dt), lthy2) = lthy1 580 |> conceal_naming_result 581 (typedef (Binding.concealed uTname, TFrees, NoSyn) 582 Tdef_set NONE (fn lthy => HEADGOAL (non_empty_typedef_tac non_empty_pred lthy))); 583 val type_definition_thm = tcode_dt |> snd |> #type_definition; 584 val qty_isom = tcode_dt |> fst |> #abs_type; 585 586 val (binding, lthy3) = lthy2 587 |> conceal_naming_result 588 (Lifting_Setup.setup_by_typedef_thm {notes = false} type_definition_thm) 589 ||> Local_Theory.close_target 590 val (wit, wit_thm) = mk_witness quot_thm; 591 val code_dt = mk_code_dt rty qty wit wit_thm NONE; 592 val lthy4 = lthy3 593 |> update_code_dt code_dt 594 |> mk_rep_isom binding (rty, qty, qty_isom) |> snd 595 in 596 (quot_thm, (lthy4, rel_eq_onps)) 597 end 598 else 599 (quot_thm, (lthy0, rel_eq_onps)) 600 end 601and lift_def_code_dt config = gen_lift_def (add_lift_def_code_dt config) 602 603 604(** from parsed parameters to the config record **) 605 606fun map_config_code_dt f1 f2 ({code_dt = code_dt, lift_config = lift_config}: config_code_dt) = 607 {code_dt = f1 code_dt, lift_config = f2 lift_config} 608 609fun update_config_code_dt nval = map_config_code_dt (K nval) I 610 611val config_flags = [("code_dt", update_config_code_dt true)] 612 613fun evaluate_params params = 614 let 615 fun eval_param param config = 616 case AList.lookup (op =) config_flags param of 617 SOME update => update config 618 | NONE => error ("Unknown parameter: " ^ (quote param)) 619 in 620 fold eval_param params default_config_code_dt 621 end 622 623(** 624 625 lift_definition command. It opens a proof of a corresponding respectfulness 626 theorem in a user-friendly, readable form. Then add_lift_def_code_dt is called internally. 627 628**) 629 630local 631 val eq_onp_assms_tac_fixed_rules = map (Transfer.prep_transfer_domain_thm \<^context>) 632 [@{thm pcr_Domainp_total}, @{thm pcr_Domainp_par_left_total}, @{thm pcr_Domainp_par}, 633 @{thm pcr_Domainp}] 634in 635fun mk_readable_rsp_thm_eq tm ctxt = 636 let 637 val ctm = Thm.cterm_of ctxt tm 638 639 fun assms_rewr_conv tactic rule ct = 640 let 641 fun prove_extra_assms thm = 642 let 643 val assms = cprems_of thm 644 fun finish thm = if Thm.no_prems thm then SOME (Goal.conclude thm) else NONE 645 fun prove ctm = Option.mapPartial finish (SINGLE tactic (Goal.init ctm)) 646 in 647 map_interrupt prove assms 648 end 649 650 fun cconl_of thm = Drule.strip_imp_concl (Thm.cprop_of thm) 651 fun lhs_of thm = fst (Thm.dest_equals (cconl_of thm)) 652 fun rhs_of thm = snd (Thm.dest_equals (cconl_of thm)) 653 val rule1 = Thm.incr_indexes (Thm.maxidx_of_cterm ct + 1) rule; 654 val lhs = lhs_of rule1; 655 val rule2 = Thm.rename_boundvars (Thm.term_of lhs) (Thm.term_of ct) rule1; 656 val rule3 = 657 Thm.instantiate (Thm.match (lhs, ct)) rule2 658 handle Pattern.MATCH => raise CTERM ("assms_rewr_conv", [lhs, ct]); 659 val proved_assms = prove_extra_assms rule3 660 in 661 case proved_assms of 662 SOME proved_assms => 663 let 664 val rule3 = proved_assms MRSL rule3 665 val rule4 = 666 if lhs_of rule3 aconvc ct then rule3 667 else 668 let val ceq = Thm.dest_fun2 (Thm.cprop_of rule3) 669 in rule3 COMP Thm.trivial (Thm.mk_binop ceq ct (rhs_of rule3)) end 670 in Thm.transitive rule4 (Thm.beta_conversion true (rhs_of rule4)) end 671 | NONE => Conv.no_conv ct 672 end 673 674 fun assms_rewrs_conv tactic rules = Conv.first_conv (map (assms_rewr_conv tactic) rules) 675 676 fun simp_arrows_conv ctm = 677 let 678 val unfold_conv = Conv.rewrs_conv 679 [@{thm rel_fun_eq_eq_onp[THEN eq_reflection]}, 680 @{thm rel_fun_eq_onp_rel[THEN eq_reflection]}, 681 @{thm rel_fun_eq[THEN eq_reflection]}, 682 @{thm rel_fun_eq_rel[THEN eq_reflection]}, 683 @{thm rel_fun_def[THEN eq_reflection]}] 684 fun binop_conv2 cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2 685 val eq_onp_assms_tac_rules = @{thm left_unique_OO} :: 686 eq_onp_assms_tac_fixed_rules @ (Transfer.get_transfer_raw ctxt) 687 val intro_top_rule = @{thm eq_onp_top_eq_eq[symmetric, THEN eq_reflection]} 688 val kill_tops = Transfer.top_sweep_rewr_conv [@{thm eq_onp_top_eq_eq[THEN eq_reflection]}] 689 val eq_onp_assms_tac = (CONVERSION kill_tops THEN' 690 TRY o REPEAT_ALL_NEW (resolve_tac ctxt eq_onp_assms_tac_rules) 691 THEN_ALL_NEW (DETERM o Transfer.eq_tac ctxt)) 1 692 val relator_eq_onp_conv = Conv.bottom_conv 693 (K (Conv.try_conv (assms_rewrs_conv eq_onp_assms_tac 694 (intro_top_rule :: Lifting_Info.get_relator_eq_onp_rules ctxt)))) ctxt 695 then_conv kill_tops 696 val relator_eq_conv = Conv.bottom_conv 697 (K (Conv.try_conv (Conv.rewrs_conv (Transfer.get_relator_eq ctxt)))) ctxt 698 in 699 case (Thm.term_of ctm) of 700 Const (\<^const_name>\<open>rel_fun\<close>, _) $ _ $ _ => 701 (binop_conv2 simp_arrows_conv simp_arrows_conv then_conv unfold_conv) ctm 702 | _ => (relator_eq_onp_conv then_conv relator_eq_conv) ctm 703 end 704 705 val unfold_ret_val_invs = Conv.bottom_conv 706 (K (Conv.try_conv (Conv.rewr_conv @{thm eq_onp_same_args[THEN eq_reflection]}))) ctxt 707 val unfold_inv_conv = 708 Conv.top_sweep_conv (K (Conv.rewr_conv @{thm eq_onp_def[THEN eq_reflection]})) ctxt 709 val simp_conv = HOLogic.Trueprop_conv (Conv.fun2_conv simp_arrows_conv) 710 val univq_conv = Conv.rewr_conv @{thm HOL.all_simps(6)[symmetric, THEN eq_reflection]} 711 val univq_prenex_conv = Conv.top_conv (K (Conv.try_conv univq_conv)) ctxt 712 val beta_conv = Thm.beta_conversion true 713 val eq_thm = 714 (simp_conv then_conv univq_prenex_conv then_conv beta_conv then_conv unfold_ret_val_invs 715 then_conv unfold_inv_conv) ctm 716 in 717 Object_Logic.rulify ctxt (eq_thm RS Drule.equal_elim_rule2) 718 end 719end 720 721fun rename_to_tnames ctxt term = 722 let 723 fun all_typs (Const (\<^const_name>\<open>Pure.all\<close>, _) $ Abs (_, T, t)) = T :: all_typs t 724 | all_typs _ = [] 725 726 fun rename (Const (\<^const_name>\<open>Pure.all\<close>, T1) $ Abs (_, T2, t)) (new_name :: names) = 727 (Const (\<^const_name>\<open>Pure.all\<close>, T1) $ Abs (new_name, T2, rename t names)) 728 | rename t _ = t 729 730 val (fixed_def_t, _) = yield_singleton (Variable.importT_terms) term ctxt 731 val new_names = Old_Datatype_Prop.make_tnames (all_typs fixed_def_t) 732 in 733 rename term new_names 734 end 735 736fun quot_thm_err ctxt (rty, qty) pretty_msg = 737 let 738 val error_msg = cat_lines 739 ["Lifting failed for the following types:", 740 Pretty.string_of (Pretty.block 741 [Pretty.str "Raw type:", Pretty.brk 2, Syntax.pretty_typ ctxt rty]), 742 Pretty.string_of (Pretty.block 743 [Pretty.str "Abstract type:", Pretty.brk 2, Syntax.pretty_typ ctxt qty]), 744 "", 745 (Pretty.string_of (Pretty.block 746 [Pretty.str "Reason:", Pretty.brk 2, pretty_msg]))] 747 in 748 error error_msg 749 end 750 751fun check_rty_err ctxt (rty_schematic, rty_forced) (raw_var, rhs_raw) = 752 let 753 val (_, ctxt') = Proof_Context.read_var raw_var ctxt 754 val rhs = Syntax.read_term ctxt' rhs_raw 755 val error_msg = cat_lines 756 ["Lifting failed for the following term:", 757 Pretty.string_of (Pretty.block 758 [Pretty.str "Term:", Pretty.brk 2, Syntax.pretty_term ctxt rhs]), 759 Pretty.string_of (Pretty.block 760 [Pretty.str "Type:", Pretty.brk 2, Syntax.pretty_typ ctxt rty_schematic]), 761 "", 762 (Pretty.string_of (Pretty.block 763 [Pretty.str "Reason:", 764 Pretty.brk 2, 765 Pretty.str "The type of the term cannot be instantiated to", 766 Pretty.brk 1, 767 Pretty.quote (Syntax.pretty_typ ctxt rty_forced), 768 Pretty.str "."]))] 769 in 770 error error_msg 771 end 772 773fun lift_def_cmd (params, raw_var, rhs_raw, par_xthms) lthy0 = 774 let 775 val config = evaluate_params params 776 val ((binding, SOME qty, mx), lthy1) = Proof_Context.read_var raw_var lthy0 777 val var = (binding, mx) 778 val rhs = Syntax.read_term lthy1 rhs_raw 779 val par_thms = Attrib.eval_thms lthy1 par_xthms 780 val (goal, after_qed) = lthy1 781 |> prepare_lift_def (add_lift_def_code_dt config) var qty rhs par_thms 782 val (goal, after_qed) = 783 case goal of 784 NONE => (goal, K (after_qed Drule.dummy_thm)) 785 | SOME prsp_tm => 786 let 787 val readable_rsp_thm_eq = mk_readable_rsp_thm_eq prsp_tm lthy1 788 val (readable_rsp_tm, _) = Logic.dest_implies (Thm.prop_of readable_rsp_thm_eq) 789 val readable_rsp_tm_tnames = rename_to_tnames lthy1 readable_rsp_tm 790 791 fun after_qed' [[thm]] lthy = 792 let 793 val internal_rsp_thm = 794 Goal.prove lthy [] [] prsp_tm (fn {context = goal_ctxt, ...} => 795 rtac goal_ctxt readable_rsp_thm_eq 1 THEN 796 Proof_Context.fact_tac goal_ctxt [thm] 1) 797 in after_qed internal_rsp_thm lthy end 798 in (SOME readable_rsp_tm_tnames, after_qed') end 799 fun after_qed_with_err_handling thmss ctxt = (after_qed thmss ctxt 800 handle Lifting_Term.QUOT_THM (rty, qty, msg) => quot_thm_err lthy1 (rty, qty) msg) 801 handle Lifting_Term.CHECK_RTY (rty_schematic, rty_forced) => 802 check_rty_err lthy1 (rty_schematic, rty_forced) (raw_var, rhs_raw); 803 in 804 lthy1 805 |> Proof.theorem NONE (snd oo after_qed_with_err_handling) [map (rpair []) (the_list goal)] 806 end 807 808fun lift_def_cmd_with_err_handling (params, (raw_var, rhs_raw, par_xthms)) lthy = 809 (lift_def_cmd (params, raw_var, rhs_raw, par_xthms) lthy 810 handle Lifting_Term.QUOT_THM (rty, qty, msg) => quot_thm_err lthy (rty, qty) msg) 811 handle Lifting_Term.CHECK_RTY (rty_schematic, rty_forced) => 812 check_rty_err lthy (rty_schematic, rty_forced) (raw_var, rhs_raw); 813 814val parse_param = Parse.name 815val parse_params = Scan.optional (Args.parens (Parse.list parse_param)) []; 816 817 818(* command syntax *) 819 820val _ = 821 Outer_Syntax.local_theory_to_proof \<^command_keyword>\<open>lift_definition\<close> 822 "definition for constants over the quotient type" 823 (parse_params -- 824 (((Parse.binding -- (\<^keyword>\<open>::\<close> |-- (Parse.typ >> SOME) -- Parse.opt_mixfix') 825 >> Scan.triple2) -- 826 (\<^keyword>\<open>is\<close> |-- Parse.term) -- 827 Scan.optional (\<^keyword>\<open>parametric\<close> |-- Parse.!!! Parse.thms1) []) >> Scan.triple1) 828 >> lift_def_cmd_with_err_handling); 829 830end 831