1(* Title: HOL/Tools/BNF/bnf_util.ML 2 Author: Dmitriy Traytel, TU Muenchen 3 Copyright 2012 4 5Library for bounded natural functors. 6*) 7 8signature BNF_UTIL = 9sig 10 include CTR_SUGAR_UTIL 11 include BNF_FP_REC_SUGAR_UTIL 12 13 val transfer_plugin: string 14 15 val unflatt: 'a list list list -> 'b list -> 'b list list list 16 val unflattt: 'a list list list list -> 'b list -> 'b list list list list 17 18 val mk_TFreess: int list -> Proof.context -> typ list list * Proof.context 19 val mk_Freesss: string -> typ list list list -> Proof.context -> 20 term list list list * Proof.context 21 val mk_Freessss: string -> typ list list list list -> Proof.context -> 22 term list list list list * Proof.context 23 val nonzero_string_of_int: int -> string 24 25 val binder_fun_types: typ -> typ list 26 val body_fun_type: typ -> typ 27 val strip_fun_type: typ -> typ list * typ 28 val strip_typeN: int -> typ -> typ list * typ 29 30 val mk_pred2T: typ -> typ -> typ 31 val mk_relT: typ * typ -> typ 32 val dest_relT: typ -> typ * typ 33 val dest_pred2T: typ -> typ * typ 34 val mk_sumT: typ * typ -> typ 35 36 val ctwo: term 37 val fst_const: typ -> term 38 val snd_const: typ -> term 39 val Id_const: typ -> term 40 41 val enforce_type: Proof.context -> (typ -> typ) -> typ -> term -> term 42 43 val mk_Ball: term -> term -> term 44 val mk_Bex: term -> term -> term 45 val mk_Card_order: term -> term 46 val mk_Field: term -> term 47 val mk_Gr: term -> term -> term 48 val mk_Grp: term -> term -> term 49 val mk_UNION: term -> term -> term 50 val mk_Union: typ -> term 51 val mk_card_binop: string -> (typ * typ -> typ) -> term -> term -> term 52 val mk_card_of: term -> term 53 val mk_card_order: term -> term 54 val mk_cexp: term -> term -> term 55 val mk_cinfinite: term -> term 56 val mk_collect: term list -> typ -> term 57 val mk_converse: term -> term 58 val mk_conversep: term -> term 59 val mk_cprod: term -> term -> term 60 val mk_csum: term -> term -> term 61 val mk_dir_image: term -> term -> term 62 val mk_eq_onp: term -> term 63 val mk_rel_fun: term -> term -> term 64 val mk_image: term -> term 65 val mk_in: term list -> term list -> typ -> term 66 val mk_inj: term -> term 67 val mk_leq: term -> term -> term 68 val mk_ordLeq: term -> term -> term 69 val mk_rel_comp: term * term -> term 70 val mk_rel_compp: term * term -> term 71 val mk_vimage2p: term -> term -> term 72 val mk_reflp: term -> term 73 val mk_symp: term -> term 74 val mk_transp: term -> term 75 val mk_union: term * term -> term 76 77 (*parameterized terms*) 78 val mk_nthN: int -> term -> int -> term 79 80 (*parameterized thms*) 81 val prod_injectD: thm 82 val prod_injectI: thm 83 val ctrans: thm 84 val id_apply: thm 85 val meta_mp: thm 86 val meta_spec: thm 87 val o_apply: thm 88 val rel_funD: thm 89 val rel_funI: thm 90 val set_mp: thm 91 val set_rev_mp: thm 92 val subset_UNIV: thm 93 94 val mk_conjIN: int -> thm 95 val mk_nthI: int -> int -> thm 96 val mk_nth_conv: int -> int -> thm 97 val mk_ordLeq_csum: int -> int -> thm -> thm 98 val mk_pointful: Proof.context -> thm -> thm 99 val mk_rel_funDN: int -> thm -> thm 100 val mk_rel_funDN_rotated: int -> thm -> thm 101 val mk_sym: thm -> thm 102 val mk_trans: thm -> thm -> thm 103 val mk_UnIN: int -> int -> thm 104 val mk_Un_upper: int -> int -> thm 105 106 val is_refl_bool: term -> bool 107 val is_refl: thm -> bool 108 val is_concl_refl: thm -> bool 109 val no_refl: thm list -> thm list 110 val no_reflexive: thm list -> thm list 111 112 val parse_type_args_named_constrained: (binding option * (string * string option)) list parser 113 val parse_map_rel_pred_bindings: (binding * binding * binding) parser 114 115 val typedef: binding * (string * sort) list * mixfix -> term -> 116 (binding * binding) option -> (Proof.context -> tactic) -> 117 local_theory -> (string * Typedef.info) * local_theory 118end; 119 120structure BNF_Util : BNF_UTIL = 121struct 122 123open Ctr_Sugar_Util 124open BNF_FP_Rec_Sugar_Util 125 126val transfer_plugin = Plugin_Name.declare_setup \<^binding>\<open>transfer\<close>; 127 128 129(* Library proper *) 130 131fun unfla0 xs = fold_map (fn _ => fn (c :: cs) => (c, cs)) xs; 132fun unflat0 xss = fold_map unfla0 xss; 133fun unflatt0 xsss = fold_map unflat0 xsss; 134fun unflattt0 xssss = fold_map unflatt0 xssss; 135 136fun unflatt xsss = fst o unflatt0 xsss; 137fun unflattt xssss = fst o unflattt0 xssss; 138 139val parse_type_arg_constrained = 140 Parse.type_ident -- Scan.option (\<^keyword>\<open>::\<close> |-- Parse.!!! Parse.sort); 141 142val parse_type_arg_named_constrained = 143 (Parse.reserved "dead" >> K NONE || parse_opt_binding_colon >> SOME) -- 144 parse_type_arg_constrained; 145 146val parse_type_args_named_constrained = 147 parse_type_arg_constrained >> (single o pair (SOME Binding.empty)) || 148 \<^keyword>\<open>(\<close> |-- Parse.!!! (Parse.list1 parse_type_arg_named_constrained --| \<^keyword>\<open>)\<close>) || 149 Scan.succeed []; 150 151val parse_map_rel_pred_binding = Parse.name --| \<^keyword>\<open>:\<close> -- Parse.binding; 152 153val no_map_rel = (Binding.empty, Binding.empty, Binding.empty); 154 155fun extract_map_rel_pred ("map", m) = (fn (_, r, p) => (m, r, p)) 156 | extract_map_rel_pred ("rel", r) = (fn (m, _, p) => (m, r, p)) 157 | extract_map_rel_pred ("pred", p) = (fn (m, r, _) => (m, r, p)) 158 | extract_map_rel_pred (s, _) = error ("Unknown label " ^ quote s ^ " (expected \"map\" or \"rel\")"); 159 160val parse_map_rel_pred_bindings = 161 \<^keyword>\<open>for\<close> |-- Scan.repeat parse_map_rel_pred_binding 162 >> (fn ps => fold extract_map_rel_pred ps no_map_rel) 163 || Scan.succeed no_map_rel; 164 165fun typedef (b, Ts, mx) set opt_morphs tac lthy = 166 let 167 (*Work around loss of qualification in "typedef" axioms by replicating it in the name*) 168 val b' = fold_rev Binding.prefix_name (map (suffix "_" o fst) (Binding.path_of b)) b; 169 170 val default_bindings = Typedef.default_bindings (Binding.concealed b'); 171 val bindings = 172 (case opt_morphs of 173 NONE => default_bindings 174 | SOME (Rep_name, Abs_name) => 175 {Rep_name = Binding.concealed Rep_name, 176 Abs_name = Binding.concealed Abs_name, 177 type_definition_name = #type_definition_name default_bindings}); 178 179 val ((name, info), (lthy, lthy_old)) = 180 lthy 181 |> Local_Theory.open_target |> snd 182 |> Typedef.add_typedef {overloaded = false} (b', Ts, mx) set (SOME bindings) tac 183 ||> `Local_Theory.close_target; 184 val phi = Proof_Context.export_morphism lthy_old lthy; 185 in 186 ((name, Typedef.transform_info phi info), lthy) 187 end; 188 189 190(* Term construction *) 191 192(** Fresh variables **) 193 194fun nonzero_string_of_int 0 = "" 195 | nonzero_string_of_int n = string_of_int n; 196 197val mk_TFreess = fold_map mk_TFrees; 198 199fun mk_Freesss x Tsss = @{fold_map 2} mk_Freess (mk_names (length Tsss) x) Tsss; 200fun mk_Freessss x Tssss = @{fold_map 2} mk_Freesss (mk_names (length Tssss) x) Tssss; 201 202 203(** Types **) 204 205(*maps [T1,...,Tn]--->T to ([T1,T2,...,Tn], T)*) 206fun strip_typeN 0 T = ([], T) 207 | strip_typeN n (Type (\<^type_name>\<open>fun\<close>, [T, T'])) = strip_typeN (n - 1) T' |>> cons T 208 | strip_typeN _ T = raise TYPE ("strip_typeN", [T], []); 209 210(*maps [T1,...,Tn]--->T-->U to ([T1,T2,...,Tn], T-->U), where U is not a function type*) 211fun strip_fun_type T = strip_typeN (num_binder_types T - 1) T; 212 213val binder_fun_types = fst o strip_fun_type; 214val body_fun_type = snd o strip_fun_type; 215 216fun mk_pred2T T U = mk_predT [T, U]; 217val mk_relT = HOLogic.mk_setT o HOLogic.mk_prodT; 218val dest_relT = HOLogic.dest_prodT o HOLogic.dest_setT; 219val dest_pred2T = apsnd Term.domain_type o Term.dest_funT; 220fun mk_sumT (LT, RT) = Type (\<^type_name>\<open>Sum_Type.sum\<close>, [LT, RT]); 221 222 223(** Constants **) 224 225fun fst_const T = Const (\<^const_name>\<open>fst\<close>, T --> fst (HOLogic.dest_prodT T)); 226fun snd_const T = Const (\<^const_name>\<open>snd\<close>, T --> snd (HOLogic.dest_prodT T)); 227fun Id_const T = Const (\<^const_name>\<open>Id\<close>, mk_relT (T, T)); 228 229 230(** Operators **) 231 232fun enforce_type ctxt get_T T t = 233 Term.subst_TVars (tvar_subst (Proof_Context.theory_of ctxt) [get_T (fastype_of t)] [T]) t; 234 235fun mk_converse R = 236 let 237 val RT = dest_relT (fastype_of R); 238 val RST = mk_relT (snd RT, fst RT); 239 in Const (\<^const_name>\<open>converse\<close>, fastype_of R --> RST) $ R end; 240 241fun mk_rel_comp (R, S) = 242 let 243 val RT = fastype_of R; 244 val ST = fastype_of S; 245 val RST = mk_relT (fst (dest_relT RT), snd (dest_relT ST)); 246 in Const (\<^const_name>\<open>relcomp\<close>, RT --> ST --> RST) $ R $ S end; 247 248fun mk_Gr A f = 249 let val ((AT, BT), FT) = `dest_funT (fastype_of f); 250 in Const (\<^const_name>\<open>Gr\<close>, HOLogic.mk_setT AT --> FT --> mk_relT (AT, BT)) $ A $ f end; 251 252fun mk_conversep R = 253 let 254 val RT = dest_pred2T (fastype_of R); 255 val RST = mk_pred2T (snd RT) (fst RT); 256 in Const (\<^const_name>\<open>conversep\<close>, fastype_of R --> RST) $ R end; 257 258fun mk_rel_compp (R, S) = 259 let 260 val RT = fastype_of R; 261 val ST = fastype_of S; 262 val RST = mk_pred2T (fst (dest_pred2T RT)) (snd (dest_pred2T ST)); 263 in Const (\<^const_name>\<open>relcompp\<close>, RT --> ST --> RST) $ R $ S end; 264 265fun mk_Grp A f = 266 let val ((AT, BT), FT) = `dest_funT (fastype_of f); 267 in Const (\<^const_name>\<open>Grp\<close>, HOLogic.mk_setT AT --> FT --> mk_pred2T AT BT) $ A $ f end; 268 269fun mk_image f = 270 let val (T, U) = dest_funT (fastype_of f); 271 in Const (\<^const_name>\<open>image\<close>, (T --> U) --> HOLogic.mk_setT T --> HOLogic.mk_setT U) $ f end; 272 273fun mk_Ball X f = 274 Const (\<^const_name>\<open>Ball\<close>, fastype_of X --> fastype_of f --> HOLogic.boolT) $ X $ f; 275 276fun mk_Bex X f = 277 Const (\<^const_name>\<open>Bex\<close>, fastype_of X --> fastype_of f --> HOLogic.boolT) $ X $ f; 278 279fun mk_UNION X f = 280 let 281 val (T, U) = dest_funT (fastype_of f); 282 in 283 Const (\<^const_name>\<open>Sup\<close>, HOLogic.mk_setT U --> U) 284 $ (Const (\<^const_name>\<open>image\<close>, (T --> U) --> fastype_of X --> HOLogic.mk_setT U) $ f $ X) 285 end; 286 287fun mk_Union T = 288 Const (\<^const_name>\<open>Sup\<close>, HOLogic.mk_setT (HOLogic.mk_setT T) --> HOLogic.mk_setT T); 289 290val mk_union = HOLogic.mk_binop \<^const_name>\<open>sup\<close>; 291 292fun mk_Field r = 293 let val T = fst (dest_relT (fastype_of r)); 294 in Const (\<^const_name>\<open>Field\<close>, mk_relT (T, T) --> HOLogic.mk_setT T) $ r end; 295 296fun mk_card_order bd = 297 let 298 val T = fastype_of bd; 299 val AT = fst (dest_relT T); 300 in 301 Const (\<^const_name>\<open>card_order_on\<close>, HOLogic.mk_setT AT --> T --> HOLogic.boolT) $ 302 HOLogic.mk_UNIV AT $ bd 303 end; 304 305fun mk_Card_order bd = 306 let 307 val T = fastype_of bd; 308 val AT = fst (dest_relT T); 309 in 310 Const (\<^const_name>\<open>card_order_on\<close>, HOLogic.mk_setT AT --> T --> HOLogic.boolT) $ 311 mk_Field bd $ bd 312 end; 313 314fun mk_cinfinite bd = Const (\<^const_name>\<open>cinfinite\<close>, fastype_of bd --> HOLogic.boolT) $ bd; 315 316fun mk_ordLeq t1 t2 = 317 HOLogic.mk_mem (HOLogic.mk_prod (t1, t2), 318 Const (\<^const_name>\<open>ordLeq\<close>, mk_relT (fastype_of t1, fastype_of t2))); 319 320fun mk_card_of A = 321 let 322 val AT = fastype_of A; 323 val T = HOLogic.dest_setT AT; 324 in 325 Const (\<^const_name>\<open>card_of\<close>, AT --> mk_relT (T, T)) $ A 326 end; 327 328fun mk_dir_image r f = 329 let val (T, U) = dest_funT (fastype_of f); 330 in Const (\<^const_name>\<open>dir_image\<close>, mk_relT (T, T) --> (T --> U) --> mk_relT (U, U)) $ r $ f end; 331 332fun mk_rel_fun R S = 333 let 334 val ((RA, RB), RT) = `dest_pred2T (fastype_of R); 335 val ((SA, SB), ST) = `dest_pred2T (fastype_of S); 336 in Const (\<^const_name>\<open>rel_fun\<close>, RT --> ST --> mk_pred2T (RA --> SA) (RB --> SB)) $ R $ S end; 337 338(*FIXME: "x"?*) 339(*(nth sets i) must be of type "T --> 'ai set"*) 340fun mk_in As sets T = 341 let 342 fun in_single set A = 343 let val AT = fastype_of A; 344 in Const (\<^const_name>\<open>less_eq\<close>, AT --> AT --> HOLogic.boolT) $ (set $ Free ("x", T)) $ A end; 345 in 346 if null sets then HOLogic.mk_UNIV T 347 else HOLogic.mk_Collect ("x", T, foldr1 (HOLogic.mk_conj) (map2 in_single sets As)) 348 end; 349 350fun mk_inj t = 351 let val T as Type (\<^type_name>\<open>fun\<close>, [domT, _]) = fastype_of t in 352 Const (\<^const_name>\<open>inj_on\<close>, T --> HOLogic.mk_setT domT --> HOLogic.boolT) $ t 353 $ HOLogic.mk_UNIV domT 354 end; 355 356fun mk_leq t1 t2 = 357 Const (\<^const_name>\<open>less_eq\<close>, fastype_of t1 --> fastype_of t2 --> HOLogic.boolT) $ t1 $ t2; 358 359fun mk_card_binop binop typop t1 t2 = 360 let 361 val (T1, relT1) = `(fst o dest_relT) (fastype_of t1); 362 val (T2, relT2) = `(fst o dest_relT) (fastype_of t2); 363 in Const (binop, relT1 --> relT2 --> mk_relT (typop (T1, T2), typop (T1, T2))) $ t1 $ t2 end; 364 365val mk_csum = mk_card_binop \<^const_name>\<open>csum\<close> mk_sumT; 366val mk_cprod = mk_card_binop \<^const_name>\<open>cprod\<close> HOLogic.mk_prodT; 367val mk_cexp = mk_card_binop \<^const_name>\<open>cexp\<close> (op --> o swap); 368val ctwo = \<^term>\<open>ctwo\<close>; 369 370fun mk_collect xs defT = 371 let val T = (case xs of [] => defT | (x::_) => fastype_of x); 372 in Const (\<^const_name>\<open>collect\<close>, HOLogic.mk_setT T --> T) $ (HOLogic.mk_set T xs) end; 373 374fun mk_vimage2p f g = 375 let 376 val (T1, T2) = dest_funT (fastype_of f); 377 val (U1, U2) = dest_funT (fastype_of g); 378 in 379 Const (\<^const_name>\<open>vimage2p\<close>, 380 (T1 --> T2) --> (U1 --> U2) --> mk_pred2T T2 U2 --> mk_pred2T T1 U1) $ f $ g 381 end; 382 383fun mk_eq_onp P = 384 let 385 val T = domain_type (fastype_of P); 386 in 387 Const (\<^const_name>\<open>eq_onp\<close>, (T --> HOLogic.boolT) --> T --> T --> HOLogic.boolT) $ P 388 end; 389 390fun mk_pred name R = 391 Const (name, uncurry mk_pred2T (fastype_of R |> dest_pred2T) --> HOLogic.boolT) $ R; 392val mk_reflp = mk_pred \<^const_name>\<open>reflp\<close>; 393val mk_symp = mk_pred \<^const_name>\<open>symp\<close>; 394val mk_transp = mk_pred \<^const_name>\<open>transp\<close>; 395 396fun mk_trans thm1 thm2 = trans OF [thm1, thm2]; 397fun mk_sym thm = thm RS sym; 398 399val prod_injectD = @{thm iffD1[OF prod.inject]}; 400val prod_injectI = @{thm iffD2[OF prod.inject]}; 401val ctrans = @{thm ordLeq_transitive}; 402val id_apply = @{thm id_apply}; 403val meta_mp = @{thm meta_mp}; 404val meta_spec = @{thm meta_spec}; 405val o_apply = @{thm o_apply}; 406val rel_funD = @{thm rel_funD}; 407val rel_funI = @{thm rel_funI}; 408val set_mp = @{thm set_mp}; 409val set_rev_mp = @{thm set_rev_mp}; 410val subset_UNIV = @{thm subset_UNIV}; 411 412fun mk_pointful ctxt thm = unfold_thms ctxt [o_apply] (thm RS fun_cong); 413 414fun mk_nthN 1 t 1 = t 415 | mk_nthN _ t 1 = HOLogic.mk_fst t 416 | mk_nthN 2 t 2 = HOLogic.mk_snd t 417 | mk_nthN n t m = mk_nthN (n - 1) (HOLogic.mk_snd t) (m - 1); 418 419fun mk_nth_conv n m = 420 let 421 fun thm b = if b then @{thm fstI} else @{thm sndI}; 422 fun mk_nth_conv _ 1 1 = refl 423 | mk_nth_conv _ _ 1 = @{thm fst_conv} 424 | mk_nth_conv _ 2 2 = @{thm snd_conv} 425 | mk_nth_conv b _ 2 = @{thm snd_conv} RS thm b 426 | mk_nth_conv b n m = mk_nth_conv false (n - 1) (m - 1) RS thm b; 427 in mk_nth_conv (not (m = n)) n m end; 428 429fun mk_nthI 1 1 = @{thm TrueE[OF TrueI]} 430 | mk_nthI n m = fold (curry op RS) (replicate (m - 1) @{thm sndI}) 431 (if m = n then @{thm TrueE[OF TrueI]} else @{thm fstI}); 432 433fun mk_conjIN 1 = @{thm TrueE[OF TrueI]} 434 | mk_conjIN n = mk_conjIN (n - 1) RSN (2, conjI); 435 436fun mk_ordLeq_csum 1 1 thm = thm 437 | mk_ordLeq_csum _ 1 thm = @{thm ordLeq_transitive} OF [thm, @{thm ordLeq_csum1}] 438 | mk_ordLeq_csum 2 2 thm = @{thm ordLeq_transitive} OF [thm, @{thm ordLeq_csum2}] 439 | mk_ordLeq_csum n m thm = @{thm ordLeq_transitive} OF 440 [mk_ordLeq_csum (n - 1) (m - 1) thm, @{thm ordLeq_csum2[OF Card_order_csum]}]; 441 442fun mk_rel_funDN n = funpow n (fn thm => thm RS rel_funD); 443 444val mk_rel_funDN_rotated = rotate_prems ~1 oo mk_rel_funDN; 445 446local 447 fun mk_Un_upper' 0 = @{thm subset_refl} 448 | mk_Un_upper' 1 = @{thm Un_upper1} 449 | mk_Un_upper' k = Library.foldr (op RS o swap) 450 (replicate (k - 1) @{thm subset_trans[OF Un_upper1]}, @{thm Un_upper1}); 451in 452 fun mk_Un_upper 1 1 = @{thm subset_refl} 453 | mk_Un_upper n 1 = mk_Un_upper' (n - 2) RS @{thm subset_trans[OF Un_upper1]} 454 | mk_Un_upper n m = mk_Un_upper' (n - m) RS @{thm subset_trans[OF Un_upper2]}; 455end; 456 457local 458 fun mk_UnIN' 0 = @{thm UnI2} 459 | mk_UnIN' m = mk_UnIN' (m - 1) RS @{thm UnI1}; 460in 461 fun mk_UnIN 1 1 = @{thm TrueE[OF TrueI]} 462 | mk_UnIN n 1 = Library.foldr1 (op RS o swap) (replicate (n - 1) @{thm UnI1}) 463 | mk_UnIN n m = mk_UnIN' (n - m) 464end; 465 466fun is_refl_bool t = 467 op aconv (HOLogic.dest_eq t) 468 handle TERM _ => false; 469 470fun is_refl_prop t = 471 op aconv (HOLogic.dest_eq (HOLogic.dest_Trueprop t)) 472 handle TERM _ => false; 473 474val is_refl = is_refl_prop o Thm.prop_of; 475val is_concl_refl = is_refl_prop o Logic.strip_imp_concl o Thm.prop_of; 476 477val no_refl = filter_out is_refl; 478val no_reflexive = filter_out Thm.is_reflexive; 479 480end; 481