1(* Title: HOL/Tools/Lifting/lifting_info.ML 2 Author: Ondrej Kuncar 3 4Context data for the lifting package. 5*) 6 7signature LIFTING_INFO = 8sig 9 type quot_map = {rel_quot_thm: thm} 10 val lookup_quot_maps: Proof.context -> string -> quot_map option 11 val print_quot_maps: Proof.context -> unit 12 13 type pcr = {pcrel_def: thm, pcr_cr_eq: thm} 14 type quotient = {quot_thm: thm, pcr_info: pcr option} 15 val pcr_eq: pcr * pcr -> bool 16 val quotient_eq: quotient * quotient -> bool 17 val transform_quotient: morphism -> quotient -> quotient 18 val lookup_quotients: Proof.context -> string -> quotient option 19 val lookup_quot_thm_quotients: Proof.context -> thm -> quotient option 20 val update_quotients: string -> quotient -> Context.generic -> Context.generic 21 val delete_quotients: thm -> Context.generic -> Context.generic 22 val print_quotients: Proof.context -> unit 23 24 type restore_data = {quotient : quotient, transfer_rules: thm Item_Net.T} 25 val lookup_restore_data: Proof.context -> string -> restore_data option 26 val init_restore_data: string -> quotient -> Context.generic -> Context.generic 27 val add_transfer_rules_in_restore_data: string -> thm Item_Net.T -> Context.generic -> Context.generic 28 29 val get_relator_eq_onp_rules: Proof.context -> thm list 30 31 val get_reflexivity_rules: Proof.context -> thm list 32 val add_reflexivity_rule_attribute: attribute 33 34 type relator_distr_data = {pos_mono_rule: thm, neg_mono_rule: thm, 35 pos_distr_rules: thm list, neg_distr_rules: thm list} 36 val lookup_relator_distr_data: Proof.context -> string -> relator_distr_data option 37 38 val add_no_code_type: string -> Context.generic -> Context.generic 39 val is_no_code_type: Proof.context -> string -> bool 40 41 val get_quot_maps : Proof.context -> quot_map Symtab.table 42 val get_quotients : Proof.context -> quotient Symtab.table 43 val get_relator_distr_data : Proof.context -> relator_distr_data Symtab.table 44 val get_restore_data : Proof.context -> restore_data Symtab.table 45 val get_no_code_types : Proof.context -> unit Symtab.table 46end 47 48structure Lifting_Info: LIFTING_INFO = 49struct 50 51open Lifting_Util 52 53 54(* context data *) 55 56type quot_map = {rel_quot_thm: thm} 57type pcr = {pcrel_def: thm, pcr_cr_eq: thm} 58type quotient = {quot_thm: thm, pcr_info: pcr option} 59type relator_distr_data = {pos_mono_rule: thm, neg_mono_rule: thm, 60 pos_distr_rules: thm list, neg_distr_rules: thm list} 61type restore_data = {quotient : quotient, transfer_rules: thm Item_Net.T} 62 63fun pcr_eq ({pcrel_def = pcrel_def1, pcr_cr_eq = pcr_cr_eq1}, 64 {pcrel_def = pcrel_def2, pcr_cr_eq = pcr_cr_eq2}) = 65 Thm.eq_thm (pcrel_def1, pcrel_def2) andalso Thm.eq_thm (pcr_cr_eq1, pcr_cr_eq2) 66 67fun quotient_eq ({quot_thm = quot_thm1, pcr_info = pcr_info1}, 68 {quot_thm = quot_thm2, pcr_info = pcr_info2}) = 69 Thm.eq_thm (quot_thm1, quot_thm2) andalso eq_option pcr_eq (pcr_info1, pcr_info2) 70 71fun join_restore_data key (rd1:restore_data, rd2) = 72 if pointer_eq (rd1, rd2) then raise Symtab.SAME else 73 if not (quotient_eq (#quotient rd1, #quotient rd2)) then raise Symtab.DUP key else 74 { quotient = #quotient rd1, 75 transfer_rules = Item_Net.merge (#transfer_rules rd1, #transfer_rules rd2)} 76 77structure Data = Generic_Data 78( 79 type T = 80 { quot_maps : quot_map Symtab.table, 81 quotients : quotient Symtab.table, 82 reflexivity_rules : thm Item_Net.T, 83 relator_distr_data : relator_distr_data Symtab.table, 84 restore_data : restore_data Symtab.table, 85 no_code_types : unit Symtab.table 86 } 87 val empty = 88 { quot_maps = Symtab.empty, 89 quotients = Symtab.empty, 90 reflexivity_rules = Thm.full_rules, 91 relator_distr_data = Symtab.empty, 92 restore_data = Symtab.empty, 93 no_code_types = Symtab.empty 94 } 95 val extend = I 96 fun merge 97 ( { quot_maps = qm1, quotients = q1, reflexivity_rules = rr1, relator_distr_data = rdd1, 98 restore_data = rd1, no_code_types = nct1 }, 99 { quot_maps = qm2, quotients = q2, reflexivity_rules = rr2, relator_distr_data = rdd2, 100 restore_data = rd2, no_code_types = nct2 } ) = 101 { quot_maps = Symtab.merge (K true) (qm1, qm2), 102 quotients = Symtab.merge (K true) (q1, q2), 103 reflexivity_rules = Item_Net.merge (rr1, rr2), 104 relator_distr_data = Symtab.merge (K true) (rdd1, rdd2), 105 restore_data = Symtab.join join_restore_data (rd1, rd2), 106 no_code_types = Symtab.merge (K true) (nct1, nct2) 107 } 108) 109 110fun map_data f1 f2 f3 f4 f5 f6 111 { quot_maps, quotients, reflexivity_rules, relator_distr_data, restore_data, no_code_types } = 112 { quot_maps = f1 quot_maps, 113 quotients = f2 quotients, 114 reflexivity_rules = f3 reflexivity_rules, 115 relator_distr_data = f4 relator_distr_data, 116 restore_data = f5 restore_data, 117 no_code_types = f6 no_code_types 118 } 119 120fun map_quot_maps f = map_data f I I I I I 121fun map_quotients f = map_data I f I I I I 122fun map_reflexivity_rules f = map_data I I f I I I 123fun map_relator_distr_data f = map_data I I I f I I 124fun map_restore_data f = map_data I I I I f I 125fun map_no_code_types f = map_data I I I I I f 126 127val get_quot_maps' = #quot_maps o Data.get 128val get_quotients' = #quotients o Data.get 129val get_reflexivity_rules' = #reflexivity_rules o Data.get 130val get_relator_distr_data' = #relator_distr_data o Data.get 131val get_restore_data' = #restore_data o Data.get 132val get_no_code_types' = #no_code_types o Data.get 133 134val get_quot_maps = get_quot_maps' o Context.Proof 135val get_quotients = get_quotients' o Context.Proof 136val get_relator_distr_data = get_relator_distr_data' o Context.Proof 137val get_restore_data = get_restore_data' o Context.Proof 138val get_no_code_types = get_no_code_types' o Context.Proof 139 140 141(* info about Quotient map theorems *) 142 143val lookup_quot_maps = Symtab.lookup o get_quot_maps 144 145fun quot_map_thm_sanity_check rel_quot_thm ctxt = 146 let 147 fun quot_term_absT ctxt quot_term = 148 let 149 val (_, abs, _, _) = (dest_Quotient o HOLogic.dest_Trueprop) quot_term 150 handle TERM (_, [t]) => error (Pretty.string_of (Pretty.block 151 [Pretty.str "The Quotient map theorem is not in the right form.", 152 Pretty.brk 1, 153 Pretty.str "The following term is not the Quotient predicate:", 154 Pretty.brk 1, 155 Syntax.pretty_term ctxt t])) 156 in 157 fastype_of abs 158 end 159 160 val ((_, [rel_quot_thm_fixed]), ctxt') = Variable.importT [rel_quot_thm] ctxt 161 val rel_quot_thm_prop = Thm.prop_of rel_quot_thm_fixed 162 val rel_quot_thm_concl = Logic.strip_imp_concl rel_quot_thm_prop 163 val rel_quot_thm_prems = Logic.strip_imp_prems rel_quot_thm_prop; 164 val concl_absT = quot_term_absT ctxt' rel_quot_thm_concl 165 val concl_tfrees = Term.add_tfree_namesT (concl_absT) [] 166 val prems_tfrees = fold (fn typ => fn list => Term.add_tfree_namesT (quot_term_absT ctxt' typ) list) 167 rel_quot_thm_prems [] 168 val extra_prem_tfrees = 169 case subtract (op =) concl_tfrees prems_tfrees of 170 [] => [] 171 | extras => [Pretty.block ([Pretty.str "Extra type variables in the premises:", 172 Pretty.brk 1] @ 173 ((Pretty.commas o map (Pretty.str o quote)) extras) @ 174 [Pretty.str "."])] 175 val errs = extra_prem_tfrees 176 in 177 if null errs then () else error (cat_lines (["Sanity check of the quotient map theorem failed:",""] 178 @ (map Pretty.string_of errs))) 179 end 180 181 182fun add_quot_map rel_quot_thm context = 183 let 184 val _ = Context.cases (K ()) (quot_map_thm_sanity_check rel_quot_thm) context 185 val rel_quot_thm_concl = (Logic.strip_imp_concl o Thm.prop_of) rel_quot_thm 186 val (_, abs, _, _) = (dest_Quotient o HOLogic.dest_Trueprop) rel_quot_thm_concl 187 val relatorT_name = (fst o dest_Type o fst o dest_funT o fastype_of) abs 188 val minfo = {rel_quot_thm = Thm.trim_context rel_quot_thm} 189 in 190 Data.map (map_quot_maps (Symtab.update (relatorT_name, minfo))) context 191 end 192 193val _ = 194 Theory.setup 195 (Attrib.setup \<^binding>\<open>quot_map\<close> (Scan.succeed (Thm.declaration_attribute add_quot_map)) 196 "declaration of the Quotient map theorem") 197 198fun print_quot_maps ctxt = 199 let 200 fun prt_map (ty_name, {rel_quot_thm}) = 201 Pretty.block (separate (Pretty.brk 2) 202 [Pretty.str "type:", 203 Pretty.str ty_name, 204 Pretty.str "quot. theorem:", 205 Syntax.pretty_term ctxt (Thm.prop_of rel_quot_thm)]) 206 in 207 map prt_map (Symtab.dest (get_quot_maps ctxt)) 208 |> Pretty.big_list "maps for type constructors:" 209 |> Pretty.writeln 210 end 211 212 213(* info about quotient types *) 214 215fun transform_pcr_info phi {pcrel_def, pcr_cr_eq} = 216 {pcrel_def = Morphism.thm phi pcrel_def, pcr_cr_eq = Morphism.thm phi pcr_cr_eq} 217 218fun transform_quotient phi {quot_thm, pcr_info} = 219 {quot_thm = Morphism.thm phi quot_thm, pcr_info = Option.map (transform_pcr_info phi) pcr_info} 220 221fun lookup_quotients ctxt type_name = 222 Symtab.lookup (get_quotients ctxt) type_name 223 |> Option.map (transform_quotient (Morphism.transfer_morphism' ctxt)) 224 225fun lookup_quot_thm_quotients ctxt quot_thm = 226 let 227 val (_, qtyp) = quot_thm_rty_qty quot_thm 228 val qty_full_name = (fst o dest_Type) qtyp 229 fun compare_data (data:quotient) = Thm.eq_thm_prop (#quot_thm data, quot_thm) 230 in 231 case lookup_quotients ctxt qty_full_name of 232 SOME quotient => if compare_data quotient then SOME quotient else NONE 233 | NONE => NONE 234 end 235 236fun update_quotients type_name qinfo context = 237 let val qinfo' = transform_quotient Morphism.trim_context_morphism qinfo 238 in Data.map (map_quotients (Symtab.update (type_name, qinfo'))) context end 239 240fun delete_quotients quot_thm context = 241 let 242 val (_, qtyp) = quot_thm_rty_qty quot_thm 243 val qty_full_name = (fst o dest_Type) qtyp 244 in 245 if is_some (lookup_quot_thm_quotients (Context.proof_of context) quot_thm) 246 then Data.map (map_quotients (Symtab.delete qty_full_name)) context 247 else context 248 end 249 250fun print_quotients ctxt = 251 let 252 fun prt_quot (qty_name, {quot_thm, pcr_info}: quotient) = 253 Pretty.block (separate (Pretty.brk 2) 254 ([Pretty.str "type:", Pretty.str qty_name, 255 Pretty.str "quot thm:", Thm.pretty_thm ctxt quot_thm] @ 256 (case pcr_info of 257 NONE => [] 258 | SOME {pcrel_def, pcr_cr_eq, ...} => 259 [Pretty.str "pcrel_def thm:", Thm.pretty_thm ctxt pcrel_def, 260 Pretty.str "pcr_cr_eq thm:", Thm.pretty_thm ctxt pcr_cr_eq]))) 261 in 262 map prt_quot (Symtab.dest (get_quotients ctxt)) 263 |> Pretty.big_list "quotients:" 264 |> Pretty.writeln 265 end 266 267val _ = 268 Theory.setup 269 (Attrib.setup \<^binding>\<open>quot_del\<close> (Scan.succeed (Thm.declaration_attribute delete_quotients)) 270 "deletes the Quotient theorem") 271 272(* data for restoring Transfer/Lifting context *) 273 274fun lookup_restore_data ctxt bundle_name = Symtab.lookup (get_restore_data ctxt) bundle_name 275 276fun update_restore_data bundle_name restore_data context = 277 Data.map (map_restore_data (Symtab.update (bundle_name, restore_data))) context 278 279fun init_restore_data bundle_name qinfo context = 280 update_restore_data bundle_name { quotient = qinfo, transfer_rules = Thm.full_rules } context 281 282fun add_transfer_rules_in_restore_data bundle_name transfer_rules context = 283 (case Symtab.lookup (get_restore_data' context) bundle_name of 284 SOME restore_data => 285 update_restore_data bundle_name { quotient = #quotient restore_data, 286 transfer_rules = Item_Net.merge ((#transfer_rules restore_data), transfer_rules) } context 287 | NONE => error ("The restore data " ^ quote bundle_name ^ " is not defined.")) 288 289 290(* theorems that a relator of an eq_onp is an eq_onp of the corresponding predicate *) 291 292fun get_relator_eq_onp_rules ctxt = 293 map safe_mk_meta_eq (rev (Named_Theorems.get ctxt \<^named_theorems>\<open>relator_eq_onp\<close>)) 294 295 296(* info about reflexivity rules *) 297 298fun get_reflexivity_rules ctxt = 299 Item_Net.content (get_reflexivity_rules' (Context.Proof ctxt)) 300 |> map (Thm.transfer' ctxt) 301 302fun add_reflexivity_rule thm = 303 Data.map (map_reflexivity_rules (Item_Net.update (Thm.trim_context thm))) 304 305val add_reflexivity_rule_attribute = Thm.declaration_attribute add_reflexivity_rule 306 307 308(* info about relator distributivity theorems *) 309 310fun map_relator_distr_data' f1 f2 f3 f4 311 {pos_mono_rule, neg_mono_rule, pos_distr_rules, neg_distr_rules} = 312 {pos_mono_rule = f1 pos_mono_rule, 313 neg_mono_rule = f2 neg_mono_rule, 314 pos_distr_rules = f3 pos_distr_rules, 315 neg_distr_rules = f4 neg_distr_rules} 316 317fun map_pos_mono_rule f = map_relator_distr_data' f I I I 318fun map_neg_mono_rule f = map_relator_distr_data' I f I I 319fun map_pos_distr_rules f = map_relator_distr_data' I I f I 320fun map_neg_distr_rules f = map_relator_distr_data' I I I f 321 322fun introduce_polarities rule = 323 let 324 val dest_less_eq = HOLogic.dest_bin \<^const_name>\<open>less_eq\<close> dummyT 325 val prems_pairs = map (dest_less_eq o HOLogic.dest_Trueprop) (Thm.prems_of rule) 326 val equal_prems = filter op= prems_pairs 327 val _ = 328 if null equal_prems then () 329 else error "The rule contains reflexive assumptions." 330 val concl_pairs = rule 331 |> Thm.concl_of 332 |> HOLogic.dest_Trueprop 333 |> dest_less_eq 334 |> apply2 (snd o strip_comb) 335 |> op ~~ 336 |> filter_out op = 337 338 val _ = if has_duplicates op= concl_pairs 339 then error "The rule contains duplicated variables in the conlusion." else () 340 341 fun rewrite_prem prem_pair = 342 if member op= concl_pairs prem_pair 343 then HOLogic.Trueprop_conv (Conv.rewr_conv (Thm.symmetric @{thm POS_def})) 344 else if member op= concl_pairs (swap prem_pair) 345 then HOLogic.Trueprop_conv (Conv.rewr_conv (Thm.symmetric @{thm NEG_def})) 346 else error "The rule contains a non-relevant assumption." 347 348 fun rewrite_prems [] = Conv.all_conv 349 | rewrite_prems (x::xs) = Conv.implies_conv (rewrite_prem x) (rewrite_prems xs) 350 351 val rewrite_prems_conv = rewrite_prems prems_pairs 352 val rewrite_concl_conv = 353 Conv.concl_conv ~1 (HOLogic.Trueprop_conv (Conv.rewr_conv (Thm.symmetric @{thm POS_def}))) 354 in 355 (Conv.fconv_rule (rewrite_prems_conv then_conv rewrite_concl_conv)) rule 356 end 357 handle 358 TERM _ => error "The rule has a wrong format." 359 | CTERM _ => error "The rule has a wrong format." 360 361fun negate_mono_rule mono_rule = 362 let 363 val rewr_conv = HOLogic.Trueprop_conv (Conv.rewrs_conv [@{thm POS_NEG}, @{thm NEG_POS}]) 364 in 365 Conv.fconv_rule (Conv.prems_conv ~1 rewr_conv then_conv Conv.concl_conv ~1 rewr_conv) mono_rule 366 end; 367 368fun add_reflexivity_rules mono_rule context = 369 let 370 val ctxt = Context.proof_of context 371 val thy = Context.theory_of context 372 373 fun find_eq_rule thm = 374 let 375 val concl_rhs = (hd o get_args 1 o HOLogic.dest_Trueprop o Thm.concl_of) thm 376 val rules = Transfer.retrieve_relator_eq ctxt concl_rhs 377 in 378 find_first (fn th => Pattern.matches thy (concl_rhs, 379 (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.concl_of) th)) rules 380 end 381 382 val eq_rule = find_eq_rule mono_rule; 383 val eq_rule = if is_some eq_rule then the eq_rule else error 384 "No corresponding rule that the relator preserves equality was found." 385 in 386 context 387 |> add_reflexivity_rule (Drule.zero_var_indexes (@{thm ord_le_eq_trans} OF [mono_rule, eq_rule])) 388 |> add_reflexivity_rule 389 (Drule.zero_var_indexes (@{thm ord_eq_le_trans} OF [sym OF [eq_rule], mono_rule])) 390 end 391 392fun add_mono_rule mono_rule context = 393 let 394 val pol_mono_rule = introduce_polarities mono_rule 395 val mono_ruleT_name = (fst o dest_Type o fst o relation_types o fst o relation_types o snd o 396 dest_Const o head_of o HOLogic.dest_Trueprop o Thm.concl_of) pol_mono_rule 397 in 398 if Symtab.defined (get_relator_distr_data' context) mono_ruleT_name 399 then 400 (if Context_Position.is_visible_generic context then 401 warning ("Monotonicity rule for type " ^ quote mono_ruleT_name ^ " is already_defined.") 402 else (); context) 403 else 404 let 405 val neg_mono_rule = negate_mono_rule pol_mono_rule 406 val relator_distr_data = {pos_mono_rule = pol_mono_rule, neg_mono_rule = neg_mono_rule, 407 pos_distr_rules = [], neg_distr_rules = []} 408 in 409 context 410 |> Data.map (map_relator_distr_data (Symtab.update (mono_ruleT_name, relator_distr_data))) 411 |> add_reflexivity_rules mono_rule 412 end 413 end; 414 415local 416 fun add_distr_rule update_entry distr_rule context = 417 let 418 val distr_ruleT_name = (fst o dest_Type o fst o relation_types o fst o relation_types o snd o 419 dest_Const o head_of o HOLogic.dest_Trueprop o Thm.concl_of) distr_rule 420 in 421 if Symtab.defined (get_relator_distr_data' context) distr_ruleT_name then 422 Data.map (map_relator_distr_data (Symtab.map_entry distr_ruleT_name (update_entry distr_rule))) 423 context 424 else error "The monotonicity rule is not defined." 425 end 426 427 fun rewrite_concl_conv thm ctm = 428 Conv.concl_conv ~1 (HOLogic.Trueprop_conv (Conv.rewr_conv (Thm.symmetric thm))) ctm 429 handle CTERM _ => error "The rule has a wrong format." 430 431in 432 fun add_pos_distr_rule distr_rule context = 433 let 434 val distr_rule = Conv.fconv_rule (rewrite_concl_conv @{thm POS_def}) distr_rule 435 fun update_entry distr_rule data = 436 map_pos_distr_rules (cons (@{thm POS_trans} OF [distr_rule, #pos_mono_rule data])) data 437 in 438 add_distr_rule update_entry distr_rule context 439 end 440 handle THM _ => error "Combining of the distr. rule and the monotonicity rule together has failed." 441 442 fun add_neg_distr_rule distr_rule context = 443 let 444 val distr_rule = Conv.fconv_rule (rewrite_concl_conv @{thm NEG_def}) distr_rule 445 fun update_entry distr_rule data = 446 map_neg_distr_rules (cons (@{thm NEG_trans} OF [distr_rule, #neg_mono_rule data])) data 447 in 448 add_distr_rule update_entry distr_rule context 449 end 450 handle THM _ => error "Combining of the distr. rule and the monotonicity rule together has failed." 451end 452 453local 454 val eq_refl2 = sym RS @{thm eq_refl} 455in 456 fun add_eq_distr_rule distr_rule context = 457 let 458 val pos_distr_rule = @{thm eq_refl} OF [distr_rule] 459 val neg_distr_rule = eq_refl2 OF [distr_rule] 460 in 461 context 462 |> add_pos_distr_rule pos_distr_rule 463 |> add_neg_distr_rule neg_distr_rule 464 end 465end; 466 467local 468 fun sanity_check rule = 469 let 470 val assms = map (perhaps (try HOLogic.dest_Trueprop)) (Thm.prems_of rule) 471 val concl = (perhaps (try HOLogic.dest_Trueprop)) (Thm.concl_of rule); 472 val (lhs, rhs) = 473 (case concl of 474 Const (\<^const_name>\<open>less_eq\<close>, _) $ (lhs as Const (\<^const_name>\<open>relcompp\<close>,_) $ _ $ _) $ rhs => 475 (lhs, rhs) 476 | Const (\<^const_name>\<open>less_eq\<close>, _) $ rhs $ (lhs as Const (\<^const_name>\<open>relcompp\<close>,_) $ _ $ _) => 477 (lhs, rhs) 478 | Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (lhs as Const (\<^const_name>\<open>relcompp\<close>,_) $ _ $ _) $ rhs => 479 (lhs, rhs) 480 | _ => error "The rule has a wrong format.") 481 482 val lhs_vars = Term.add_vars lhs [] 483 val rhs_vars = Term.add_vars rhs [] 484 val assms_vars = fold Term.add_vars assms []; 485 val _ = 486 if has_duplicates op= lhs_vars 487 then error "Left-hand side has variable duplicates" else () 488 val _ = 489 if subset op= (rhs_vars, lhs_vars) then () 490 else error "Extra variables in the right-hand side of the rule" 491 val _ = 492 if subset op= (assms_vars, lhs_vars) then () 493 else error "Extra variables in the assumptions of the rule" 494 val rhs_args = (snd o strip_comb) rhs; 495 fun check_comp t = 496 (case t of 497 Const (\<^const_name>\<open>relcompp\<close>, _) $ Var _ $ Var _ => () 498 | _ => error "There is an argument on the rhs that is not a composition.") 499 val _ = map check_comp rhs_args 500 in () end 501in 502 503 fun add_distr_rule distr_rule context = 504 let 505 val _ = sanity_check distr_rule 506 val concl = (perhaps (try HOLogic.dest_Trueprop)) (Thm.concl_of distr_rule) 507 in 508 (case concl of 509 Const (\<^const_name>\<open>less_eq\<close>, _) $ (Const (\<^const_name>\<open>relcompp\<close>,_) $ _ $ _) $ _ => 510 add_pos_distr_rule distr_rule context 511 | Const (\<^const_name>\<open>less_eq\<close>, _) $ _ $ (Const (\<^const_name>\<open>relcompp\<close>,_) $ _ $ _) => 512 add_neg_distr_rule distr_rule context 513 | Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (Const (\<^const_name>\<open>relcompp\<close>,_) $ _ $ _) $ _ => 514 add_eq_distr_rule distr_rule context) 515 end 516end 517 518fun get_distr_rules_raw context = 519 Symtab.fold (fn (_, {pos_distr_rules, neg_distr_rules, ...}) => fn rules => 520 pos_distr_rules @ neg_distr_rules @ rules) 521 (get_relator_distr_data' context) [] 522 |> map (Thm.transfer'' context) 523 524fun get_mono_rules_raw context = 525 Symtab.fold (fn (_, {pos_mono_rule, neg_mono_rule, ...}) => fn rules => 526 [pos_mono_rule, neg_mono_rule] @ rules) 527 (get_relator_distr_data' context) [] 528 |> map (Thm.transfer'' context) 529 530val lookup_relator_distr_data = Symtab.lookup o get_relator_distr_data 531 532val _ = 533 Theory.setup 534 (Attrib.setup \<^binding>\<open>relator_mono\<close> (Scan.succeed (Thm.declaration_attribute add_mono_rule)) 535 "declaration of relator's monotonicity" 536 #> Attrib.setup \<^binding>\<open>relator_distr\<close> (Scan.succeed (Thm.declaration_attribute add_distr_rule)) 537 "declaration of relator's distributivity over OO" 538 #> Global_Theory.add_thms_dynamic 539 (\<^binding>\<open>relator_distr_raw\<close>, get_distr_rules_raw) 540 #> Global_Theory.add_thms_dynamic 541 (\<^binding>\<open>relator_mono_raw\<close>, get_mono_rules_raw)) 542 543 544(* no_code types *) 545 546fun add_no_code_type type_name context = 547 Data.map (map_no_code_types (Symtab.update (type_name, ()))) context; 548 549fun is_no_code_type context type_name = (Symtab.defined o get_no_code_types) context type_name 550 551 552(* setup fixed eq_onp rules *) 553 554val _ = Context.>> 555 (fold (Named_Theorems.add_thm \<^named_theorems>\<open>relator_eq_onp\<close> o 556 Transfer.prep_transfer_domain_thm \<^context>) 557 @{thms composed_equiv_rel_eq_onp composed_equiv_rel_eq_eq_onp}) 558 559 560(* setup fixed reflexivity rules *) 561 562val _ = Context.>> (fold add_reflexivity_rule 563 @{thms order_refl[of "(=)"] eq_onp_le_eq Quotient_composition_le_eq Quotient_composition_ge_eq 564 bi_unique_OO bi_total_OO right_unique_OO right_total_OO left_unique_OO left_total_OO}) 565 566 567(* outer syntax commands *) 568 569val _ = 570 Outer_Syntax.command \<^command_keyword>\<open>print_quot_maps\<close> "print quotient map functions" 571 (Scan.succeed (Toplevel.keep (print_quot_maps o Toplevel.context_of))) 572 573val _ = 574 Outer_Syntax.command \<^command_keyword>\<open>print_quotients\<close> "print quotients" 575 (Scan.succeed (Toplevel.keep (print_quotients o Toplevel.context_of))) 576 577end 578