1(* Title: Pure/thm.ML 2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 3 Author: Makarius 4 5The very core of Isabelle's Meta Logic: certified types and terms, 6derivations, theorems, inference rules (including lifting and 7resolution), oracles. 8*) 9 10infix 0 RS RSN; 11 12signature BASIC_THM = 13sig 14 type ctyp 15 type cterm 16 exception CTERM of string * cterm list 17 type thm 18 type conv = cterm -> thm 19 exception THM of string * int * thm list 20 val RSN: thm * (int * thm) -> thm 21 val RS: thm * thm -> thm 22end; 23 24signature THM = 25sig 26 include BASIC_THM 27 (*certified types*) 28 val typ_of: ctyp -> typ 29 val global_ctyp_of: theory -> typ -> ctyp 30 val ctyp_of: Proof.context -> typ -> ctyp 31 val dest_ctyp: ctyp -> ctyp list 32 val dest_ctypN: int -> ctyp -> ctyp 33 val dest_ctyp0: ctyp -> ctyp 34 val dest_ctyp1: ctyp -> ctyp 35 val make_ctyp: ctyp -> ctyp list -> ctyp 36 (*certified terms*) 37 val term_of: cterm -> term 38 val typ_of_cterm: cterm -> typ 39 val ctyp_of_cterm: cterm -> ctyp 40 val maxidx_of_cterm: cterm -> int 41 val global_cterm_of: theory -> term -> cterm 42 val cterm_of: Proof.context -> term -> cterm 43 val renamed_term: term -> cterm -> cterm 44 val dest_comb: cterm -> cterm * cterm 45 val dest_fun: cterm -> cterm 46 val dest_arg: cterm -> cterm 47 val dest_fun2: cterm -> cterm 48 val dest_arg1: cterm -> cterm 49 val dest_abs: string option -> cterm -> cterm * cterm 50 val rename_tvar: indexname -> ctyp -> ctyp 51 val var: indexname * ctyp -> cterm 52 val apply: cterm -> cterm -> cterm 53 val lambda_name: string * cterm -> cterm -> cterm 54 val lambda: cterm -> cterm -> cterm 55 val adjust_maxidx_cterm: int -> cterm -> cterm 56 val incr_indexes_cterm: int -> cterm -> cterm 57 val match: cterm * cterm -> 58 ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list 59 val first_order_match: cterm * cterm -> 60 ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list 61 (*theorems*) 62 val fold_terms: (term -> 'a -> 'a) -> thm -> 'a -> 'a 63 val fold_atomic_ctyps: (ctyp -> 'a -> 'a) -> thm -> 'a -> 'a 64 val fold_atomic_cterms: (cterm -> 'a -> 'a) -> thm -> 'a -> 'a 65 val terms_of_tpairs: (term * term) list -> term list 66 val full_prop_of: thm -> term 67 val theory_id: thm -> Context.theory_id 68 val theory_name: thm -> string 69 val maxidx_of: thm -> int 70 val maxidx_thm: thm -> int -> int 71 val shyps_of: thm -> sort Ord_List.T 72 val hyps_of: thm -> term list 73 val prop_of: thm -> term 74 val tpairs_of: thm -> (term * term) list 75 val concl_of: thm -> term 76 val prems_of: thm -> term list 77 val nprems_of: thm -> int 78 val no_prems: thm -> bool 79 val major_prem_of: thm -> term 80 val cprop_of: thm -> cterm 81 val cprem_of: thm -> int -> cterm 82 val cconcl_of: thm -> cterm 83 val cprems_of: thm -> cterm list 84 val chyps_of: thm -> cterm list 85 exception CONTEXT of string * ctyp list * cterm list * thm list * Context.generic option 86 val theory_of_cterm: cterm -> theory 87 val theory_of_thm: thm -> theory 88 val trim_context_ctyp: ctyp -> ctyp 89 val trim_context_cterm: cterm -> cterm 90 val transfer_ctyp: theory -> ctyp -> ctyp 91 val transfer_cterm: theory -> cterm -> cterm 92 val transfer: theory -> thm -> thm 93 val transfer': Proof.context -> thm -> thm 94 val transfer'': Context.generic -> thm -> thm 95 val join_transfer: theory -> thm -> thm 96 val join_transfer_context: Proof.context * thm -> Proof.context * thm 97 val renamed_prop: term -> thm -> thm 98 val weaken: cterm -> thm -> thm 99 val weaken_sorts: sort list -> cterm -> cterm 100 val proof_bodies_of: thm list -> proof_body list 101 val proof_body_of: thm -> proof_body 102 val proof_of: thm -> proof 103 val reconstruct_proof_of: thm -> Proofterm.proof 104 val consolidate: thm list -> unit 105 val expose_proofs: theory -> thm list -> unit 106 val expose_proof: theory -> thm -> unit 107 val future: thm future -> cterm -> thm 108 val thm_deps: thm -> Proofterm.thm Ord_List.T 109 val extra_shyps: thm -> sort list 110 val strip_shyps: thm -> thm 111 val derivation_closed: thm -> bool 112 val derivation_name: thm -> string 113 val derivation_id: thm -> Proofterm.thm_id option 114 val raw_derivation_name: thm -> string 115 val expand_name: thm -> Proofterm.thm_header -> string option 116 val name_derivation: string * Position.T -> thm -> thm 117 val close_derivation: Position.T -> thm -> thm 118 val trim_context: thm -> thm 119 val axiom: theory -> string -> thm 120 val all_axioms_of: theory -> (string * thm) list 121 val get_tags: thm -> Properties.T 122 val map_tags: (Properties.T -> Properties.T) -> thm -> thm 123 val norm_proof: thm -> thm 124 val adjust_maxidx_thm: int -> thm -> thm 125 (*type classes*) 126 val the_classrel: theory -> class * class -> thm 127 val the_arity: theory -> string * sort list * class -> thm 128 val classrel_proof: theory -> class * class -> proof 129 val arity_proof: theory -> string * sort list * class -> proof 130 (*oracles*) 131 val add_oracle: binding * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory 132 val oracle_space: theory -> Name_Space.T 133 val pretty_oracle: Proof.context -> string -> Pretty.T 134 val extern_oracles: bool -> Proof.context -> (Markup.T * xstring) list 135 val check_oracle: Proof.context -> xstring * Position.T -> string 136 (*inference rules*) 137 val assume: cterm -> thm 138 val implies_intr: cterm -> thm -> thm 139 val implies_elim: thm -> thm -> thm 140 val forall_intr: cterm -> thm -> thm 141 val forall_elim: cterm -> thm -> thm 142 val reflexive: cterm -> thm 143 val symmetric: thm -> thm 144 val transitive: thm -> thm -> thm 145 val beta_conversion: bool -> conv 146 val eta_conversion: conv 147 val eta_long_conversion: conv 148 val abstract_rule: string -> cterm -> thm -> thm 149 val combination: thm -> thm -> thm 150 val equal_intr: thm -> thm -> thm 151 val equal_elim: thm -> thm -> thm 152 val solve_constraints: thm -> thm 153 val flexflex_rule: Proof.context option -> thm -> thm Seq.seq 154 val generalize: string list * string list -> int -> thm -> thm 155 val generalize_cterm: string list * string list -> int -> cterm -> cterm 156 val generalize_ctyp: string list -> int -> ctyp -> ctyp 157 val instantiate: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list -> 158 thm -> thm 159 val instantiate_cterm: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list -> 160 cterm -> cterm 161 val trivial: cterm -> thm 162 val of_class: ctyp * class -> thm 163 val unconstrainT: thm -> thm 164 val varifyT_global': (string * sort) list -> thm -> ((string * sort) * indexname) list * thm 165 val varifyT_global: thm -> thm 166 val legacy_freezeT: thm -> thm 167 val plain_prop_of: thm -> term 168 val dest_state: thm * int -> (term * term) list * term list * term * term 169 val lift_rule: cterm -> thm -> thm 170 val incr_indexes: int -> thm -> thm 171 val assumption: Proof.context option -> int -> thm -> thm Seq.seq 172 val eq_assumption: int -> thm -> thm 173 val rotate_rule: int -> int -> thm -> thm 174 val permute_prems: int -> int -> thm -> thm 175 val bicompose: Proof.context option -> {flatten: bool, match: bool, incremented: bool} -> 176 bool * thm * int -> int -> thm -> thm Seq.seq 177 val biresolution: Proof.context option -> bool -> (bool * thm) list -> int -> thm -> thm Seq.seq 178 val thynames_of_arity: theory -> string * class -> string list 179 val add_classrel: thm -> theory -> theory 180 val add_arity: thm -> theory -> theory 181end; 182 183structure Thm: THM = 184struct 185 186(*** Certified terms and types ***) 187 188(** certified types **) 189 190datatype ctyp = Ctyp of {cert: Context.certificate, T: typ, maxidx: int, sorts: sort Ord_List.T}; 191 192fun typ_of (Ctyp {T, ...}) = T; 193 194fun global_ctyp_of thy raw_T = 195 let 196 val T = Sign.certify_typ thy raw_T; 197 val maxidx = Term.maxidx_of_typ T; 198 val sorts = Sorts.insert_typ T []; 199 in Ctyp {cert = Context.Certificate thy, T = T, maxidx = maxidx, sorts = sorts} end; 200 201val ctyp_of = global_ctyp_of o Proof_Context.theory_of; 202 203fun dest_ctyp (Ctyp {cert, T = Type (_, Ts), maxidx, sorts}) = 204 map (fn T => Ctyp {cert = cert, T = T, maxidx = maxidx, sorts = sorts}) Ts 205 | dest_ctyp cT = raise TYPE ("dest_ctyp", [typ_of cT], []); 206 207fun dest_ctypN n (Ctyp {cert, T, maxidx, sorts}) = 208 let fun err () = raise TYPE ("dest_ctypN", [T], []) in 209 (case T of 210 Type (_, Ts) => 211 Ctyp {cert = cert, T = nth Ts n handle General.Subscript => err (), 212 maxidx = maxidx, sorts = sorts} 213 | _ => err ()) 214 end; 215 216val dest_ctyp0 = dest_ctypN 0; 217val dest_ctyp1 = dest_ctypN 1; 218 219fun join_certificate_ctyp (Ctyp {cert, ...}) cert0 = Context.join_certificate (cert0, cert); 220fun union_sorts_ctyp (Ctyp {sorts, ...}) sorts0 = Sorts.union sorts0 sorts; 221fun maxidx_ctyp (Ctyp {maxidx, ...}) maxidx0 = Int.max (maxidx0, maxidx); 222 223fun make_ctyp (Ctyp {cert, T, maxidx = _, sorts = _}) cargs = 224 let 225 val As = map typ_of cargs; 226 fun err () = raise TYPE ("make_ctyp", T :: As, []); 227 in 228 (case T of 229 Type (a, args) => 230 Ctyp { 231 cert = fold join_certificate_ctyp cargs cert, 232 maxidx = fold maxidx_ctyp cargs ~1, 233 sorts = fold union_sorts_ctyp cargs [], 234 T = if length args = length cargs then Type (a, As) else err ()} 235 | _ => err ()) 236 end; 237 238 239 240(** certified terms **) 241 242(*certified terms with checked typ, maxidx, and sorts*) 243datatype cterm = 244 Cterm of {cert: Context.certificate, t: term, T: typ, maxidx: int, sorts: sort Ord_List.T}; 245 246exception CTERM of string * cterm list; 247 248fun term_of (Cterm {t, ...}) = t; 249 250fun typ_of_cterm (Cterm {T, ...}) = T; 251 252fun ctyp_of_cterm (Cterm {cert, T, maxidx, sorts, ...}) = 253 Ctyp {cert = cert, T = T, maxidx = maxidx, sorts = sorts}; 254 255fun maxidx_of_cterm (Cterm {maxidx, ...}) = maxidx; 256 257fun global_cterm_of thy tm = 258 let 259 val (t, T, maxidx) = Sign.certify_term thy tm; 260 val sorts = Sorts.insert_term t []; 261 in Cterm {cert = Context.Certificate thy, t = t, T = T, maxidx = maxidx, sorts = sorts} end; 262 263val cterm_of = global_cterm_of o Proof_Context.theory_of; 264 265fun join_certificate0 (Cterm {cert = cert1, ...}, Cterm {cert = cert2, ...}) = 266 Context.join_certificate (cert1, cert2); 267 268fun renamed_term t' (Cterm {cert, t, T, maxidx, sorts}) = 269 if t aconv t' then Cterm {cert = cert, t = t', T = T, maxidx = maxidx, sorts = sorts} 270 else raise TERM ("renamed_term: terms disagree", [t, t']); 271 272 273(* destructors *) 274 275fun dest_comb (Cterm {t = c $ a, T, cert, maxidx, sorts}) = 276 let val A = Term.argument_type_of c 0 in 277 (Cterm {t = c, T = A --> T, cert = cert, maxidx = maxidx, sorts = sorts}, 278 Cterm {t = a, T = A, cert = cert, maxidx = maxidx, sorts = sorts}) 279 end 280 | dest_comb ct = raise CTERM ("dest_comb", [ct]); 281 282fun dest_fun (Cterm {t = c $ _, T, cert, maxidx, sorts}) = 283 let val A = Term.argument_type_of c 0 284 in Cterm {t = c, T = A --> T, cert = cert, maxidx = maxidx, sorts = sorts} end 285 | dest_fun ct = raise CTERM ("dest_fun", [ct]); 286 287fun dest_arg (Cterm {t = c $ a, T = _, cert, maxidx, sorts}) = 288 let val A = Term.argument_type_of c 0 289 in Cterm {t = a, T = A, cert = cert, maxidx = maxidx, sorts = sorts} end 290 | dest_arg ct = raise CTERM ("dest_arg", [ct]); 291 292 293fun dest_fun2 (Cterm {t = c $ _ $ _, T, cert, maxidx, sorts}) = 294 let 295 val A = Term.argument_type_of c 0; 296 val B = Term.argument_type_of c 1; 297 in Cterm {t = c, T = A --> B --> T, cert = cert, maxidx = maxidx, sorts = sorts} end 298 | dest_fun2 ct = raise CTERM ("dest_fun2", [ct]); 299 300fun dest_arg1 (Cterm {t = c $ a $ _, T = _, cert, maxidx, sorts}) = 301 let val A = Term.argument_type_of c 0 302 in Cterm {t = a, T = A, cert = cert, maxidx = maxidx, sorts = sorts} end 303 | dest_arg1 ct = raise CTERM ("dest_arg1", [ct]); 304 305fun dest_abs a (Cterm {t = Abs (x, T, t), T = Type ("fun", [_, U]), cert, maxidx, sorts}) = 306 let val (y', t') = Term.dest_abs (the_default x a, T, t) in 307 (Cterm {t = Free (y', T), T = T, cert = cert, maxidx = maxidx, sorts = sorts}, 308 Cterm {t = t', T = U, cert = cert, maxidx = maxidx, sorts = sorts}) 309 end 310 | dest_abs _ ct = raise CTERM ("dest_abs", [ct]); 311 312 313(* constructors *) 314 315fun rename_tvar (a, i) (Ctyp {cert, T, maxidx, sorts}) = 316 let 317 val S = 318 (case T of 319 TFree (_, S) => S 320 | TVar (_, S) => S 321 | _ => raise TYPE ("rename_tvar: no variable", [T], [])); 322 val _ = if i < 0 then raise TYPE ("rename_tvar: bad index", [TVar ((a, i), S)], []) else (); 323 in Ctyp {cert = cert, T = TVar ((a, i), S), maxidx = Int.max (i, maxidx), sorts = sorts} end; 324 325fun var ((x, i), Ctyp {cert, T, maxidx, sorts}) = 326 if i < 0 then raise TERM ("var: bad index", [Var ((x, i), T)]) 327 else Cterm {cert = cert, t = Var ((x, i), T), T = T, maxidx = Int.max (i, maxidx), sorts = sorts}; 328 329fun apply 330 (cf as Cterm {t = f, T = Type ("fun", [dty, rty]), maxidx = maxidx1, sorts = sorts1, ...}) 331 (cx as Cterm {t = x, T, maxidx = maxidx2, sorts = sorts2, ...}) = 332 if T = dty then 333 Cterm {cert = join_certificate0 (cf, cx), 334 t = f $ x, 335 T = rty, 336 maxidx = Int.max (maxidx1, maxidx2), 337 sorts = Sorts.union sorts1 sorts2} 338 else raise CTERM ("apply: types don't agree", [cf, cx]) 339 | apply cf cx = raise CTERM ("apply: first arg is not a function", [cf, cx]); 340 341fun lambda_name 342 (x, ct1 as Cterm {t = t1, T = T1, maxidx = maxidx1, sorts = sorts1, ...}) 343 (ct2 as Cterm {t = t2, T = T2, maxidx = maxidx2, sorts = sorts2, ...}) = 344 let val t = Term.lambda_name (x, t1) t2 in 345 Cterm {cert = join_certificate0 (ct1, ct2), 346 t = t, T = T1 --> T2, 347 maxidx = Int.max (maxidx1, maxidx2), 348 sorts = Sorts.union sorts1 sorts2} 349 end; 350 351fun lambda t u = lambda_name ("", t) u; 352 353 354(* indexes *) 355 356fun adjust_maxidx_cterm i (ct as Cterm {cert, t, T, maxidx, sorts}) = 357 if maxidx = i then ct 358 else if maxidx < i then 359 Cterm {maxidx = i, cert = cert, t = t, T = T, sorts = sorts} 360 else 361 Cterm {maxidx = Int.max (maxidx_of_term t, i), cert = cert, t = t, T = T, sorts = sorts}; 362 363fun incr_indexes_cterm i (ct as Cterm {cert, t, T, maxidx, sorts}) = 364 if i < 0 then raise CTERM ("negative increment", [ct]) 365 else if i = 0 then ct 366 else Cterm {cert = cert, t = Logic.incr_indexes ([], [], i) t, 367 T = Logic.incr_tvar i T, maxidx = maxidx + i, sorts = sorts}; 368 369 370 371(*** Derivations and Theorems ***) 372 373(* sort constraints *) 374 375type constraint = {theory: theory, typ: typ, sort: sort}; 376 377local 378 379val constraint_ord : constraint ord = 380 Context.theory_id_ord o apply2 (Context.theory_id o #theory) 381 <<< Term_Ord.typ_ord o apply2 #typ 382 <<< Term_Ord.sort_ord o apply2 #sort; 383 384val smash_atyps = 385 map_atyps (fn TVar (_, S) => Term.aT S | TFree (_, S) => Term.aT S | T => T); 386 387in 388 389val union_constraints = Ord_List.union constraint_ord; 390 391fun insert_constraints thy (T, S) = 392 let 393 val ignored = 394 S = [] orelse 395 (case T of 396 TFree (_, S') => S = S' 397 | TVar (_, S') => S = S' 398 | _ => false); 399 in 400 if ignored then I 401 else Ord_List.insert constraint_ord {theory = thy, typ = smash_atyps T, sort = S} 402 end; 403 404fun insert_constraints_env thy env = 405 let 406 val tyenv = Envir.type_env env; 407 fun insert ([], _) = I 408 | insert (S, T) = insert_constraints thy (Envir.norm_type tyenv T, S); 409 in tyenv |> Vartab.fold (insert o #2) end; 410 411end; 412 413 414(* datatype thm *) 415 416datatype thm = Thm of 417 deriv * (*derivation*) 418 {cert: Context.certificate, (*background theory certificate*) 419 tags: Properties.T, (*additional annotations/comments*) 420 maxidx: int, (*maximum index of any Var or TVar*) 421 constraints: constraint Ord_List.T, (*implicit proof obligations for sort constraints*) 422 shyps: sort Ord_List.T, (*sort hypotheses*) 423 hyps: term Ord_List.T, (*hypotheses*) 424 tpairs: (term * term) list, (*flex-flex pairs*) 425 prop: term} (*conclusion*) 426and deriv = Deriv of 427 {promises: (serial * thm future) Ord_List.T, 428 body: Proofterm.proof_body}; 429 430type conv = cterm -> thm; 431 432(*errors involving theorems*) 433exception THM of string * int * thm list; 434 435fun rep_thm (Thm (_, args)) = args; 436 437fun fold_terms f (Thm (_, {tpairs, prop, hyps, ...})) = 438 fold (fn (t, u) => f t #> f u) tpairs #> f prop #> fold f hyps; 439 440fun fold_atomic_ctyps f (th as Thm (_, {cert, maxidx, shyps, ...})) = 441 let fun ctyp T = Ctyp {cert = cert, T = T, maxidx = maxidx, sorts = shyps} 442 in (fold_terms o fold_types o fold_atyps) (f o ctyp) th end; 443 444fun fold_atomic_cterms f (th as Thm (_, {cert, maxidx, shyps, ...})) = 445 let fun cterm t T = Cterm {cert = cert, t = t, T = T, maxidx = maxidx, sorts = shyps} in 446 (fold_terms o fold_aterms) 447 (fn t as Const (_, T) => f (cterm t T) 448 | t as Free (_, T) => f (cterm t T) 449 | t as Var (_, T) => f (cterm t T) 450 | _ => I) th 451 end; 452 453 454fun terms_of_tpairs tpairs = fold_rev (fn (t, u) => cons t o cons u) tpairs []; 455 456fun eq_tpairs ((t, u), (t', u')) = t aconv t' andalso u aconv u'; 457fun union_tpairs ts us = Library.merge eq_tpairs (ts, us); 458val maxidx_tpairs = fold (fn (t, u) => Term.maxidx_term t #> Term.maxidx_term u); 459 460fun attach_tpairs tpairs prop = 461 Logic.list_implies (map Logic.mk_equals tpairs, prop); 462 463fun full_prop_of (Thm (_, {tpairs, prop, ...})) = attach_tpairs tpairs prop; 464 465 466val union_hyps = Ord_List.union Term_Ord.fast_term_ord; 467val insert_hyps = Ord_List.insert Term_Ord.fast_term_ord; 468val remove_hyps = Ord_List.remove Term_Ord.fast_term_ord; 469 470fun join_certificate1 (Cterm {cert = cert1, ...}, Thm (_, {cert = cert2, ...})) = 471 Context.join_certificate (cert1, cert2); 472 473fun join_certificate2 (Thm (_, {cert = cert1, ...}), Thm (_, {cert = cert2, ...})) = 474 Context.join_certificate (cert1, cert2); 475 476 477(* basic components *) 478 479val cert_of = #cert o rep_thm; 480val theory_id = Context.certificate_theory_id o cert_of; 481val theory_name = Context.theory_id_name o theory_id; 482 483val maxidx_of = #maxidx o rep_thm; 484fun maxidx_thm th i = Int.max (maxidx_of th, i); 485val shyps_of = #shyps o rep_thm; 486val hyps_of = #hyps o rep_thm; 487val prop_of = #prop o rep_thm; 488val tpairs_of = #tpairs o rep_thm; 489 490val concl_of = Logic.strip_imp_concl o prop_of; 491val prems_of = Logic.strip_imp_prems o prop_of; 492val nprems_of = Logic.count_prems o prop_of; 493fun no_prems th = nprems_of th = 0; 494 495fun major_prem_of th = 496 (case prems_of th of 497 prem :: _ => Logic.strip_assums_concl prem 498 | [] => raise THM ("major_prem_of: rule with no premises", 0, [th])); 499 500fun cprop_of (Thm (_, {cert, maxidx, shyps, prop, ...})) = 501 Cterm {cert = cert, maxidx = maxidx, T = propT, t = prop, sorts = shyps}; 502 503fun cprem_of (th as Thm (_, {cert, maxidx, shyps, prop, ...})) i = 504 Cterm {cert = cert, maxidx = maxidx, T = propT, sorts = shyps, 505 t = Logic.nth_prem (i, prop) handle TERM _ => raise THM ("cprem_of", i, [th])}; 506 507fun cconcl_of (th as Thm (_, {cert, maxidx, shyps, ...})) = 508 Cterm {cert = cert, maxidx = maxidx, T = propT, sorts = shyps, t = concl_of th}; 509 510fun cprems_of (th as Thm (_, {cert, maxidx, shyps, ...})) = 511 map (fn t => Cterm {cert = cert, maxidx = maxidx, T = propT, sorts = shyps, t = t}) 512 (prems_of th); 513 514fun chyps_of (Thm (_, {cert, shyps, hyps, ...})) = 515 map (fn t => Cterm {cert = cert, maxidx = ~1, T = propT, sorts = shyps, t = t}) hyps; 516 517 518(* implicit theory context *) 519 520exception CONTEXT of string * ctyp list * cterm list * thm list * Context.generic option; 521 522fun theory_of_cterm (ct as Cterm {cert, ...}) = 523 Context.certificate_theory cert 524 handle ERROR msg => raise CONTEXT (msg, [], [ct], [], NONE); 525 526fun theory_of_thm th = 527 Context.certificate_theory (cert_of th) 528 handle ERROR msg => raise CONTEXT (msg, [], [], [th], NONE); 529 530fun trim_context_ctyp cT = 531 (case cT of 532 Ctyp {cert = Context.Certificate_Id _, ...} => cT 533 | Ctyp {cert = Context.Certificate thy, T, maxidx, sorts} => 534 Ctyp {cert = Context.Certificate_Id (Context.theory_id thy), 535 T = T, maxidx = maxidx, sorts = sorts}); 536 537fun trim_context_cterm ct = 538 (case ct of 539 Cterm {cert = Context.Certificate_Id _, ...} => ct 540 | Cterm {cert = Context.Certificate thy, t, T, maxidx, sorts} => 541 Cterm {cert = Context.Certificate_Id (Context.theory_id thy), 542 t = t, T = T, maxidx = maxidx, sorts = sorts}); 543 544fun trim_context_thm th = 545 (case th of 546 Thm (_, {constraints = _ :: _, ...}) => 547 raise THM ("trim_context: pending sort constraints", 0, [th]) 548 | Thm (_, {cert = Context.Certificate_Id _, ...}) => th 549 | Thm (der, 550 {cert = Context.Certificate thy, tags, maxidx, constraints = [], shyps, hyps, 551 tpairs, prop}) => 552 Thm (der, 553 {cert = Context.Certificate_Id (Context.theory_id thy), 554 tags = tags, maxidx = maxidx, constraints = [], shyps = shyps, hyps = hyps, 555 tpairs = tpairs, prop = prop})); 556 557fun transfer_ctyp thy' cT = 558 let 559 val Ctyp {cert, T, maxidx, sorts} = cT; 560 val _ = 561 Context.subthy_id (Context.certificate_theory_id cert, Context.theory_id thy') orelse 562 raise CONTEXT ("Cannot transfer: not a super theory", [cT], [], [], 563 SOME (Context.Theory thy')); 564 val cert' = Context.join_certificate (Context.Certificate thy', cert); 565 in 566 if Context.eq_certificate (cert, cert') then cT 567 else Ctyp {cert = cert', T = T, maxidx = maxidx, sorts = sorts} 568 end; 569 570fun transfer_cterm thy' ct = 571 let 572 val Cterm {cert, t, T, maxidx, sorts} = ct; 573 val _ = 574 Context.subthy_id (Context.certificate_theory_id cert, Context.theory_id thy') orelse 575 raise CONTEXT ("Cannot transfer: not a super theory", [], [ct], [], 576 SOME (Context.Theory thy')); 577 val cert' = Context.join_certificate (Context.Certificate thy', cert); 578 in 579 if Context.eq_certificate (cert, cert') then ct 580 else Cterm {cert = cert', t = t, T = T, maxidx = maxidx, sorts = sorts} 581 end; 582 583fun transfer thy' th = 584 let 585 val Thm (der, {cert, tags, maxidx, constraints, shyps, hyps, tpairs, prop}) = th; 586 val _ = 587 Context.subthy_id (Context.certificate_theory_id cert, Context.theory_id thy') orelse 588 raise CONTEXT ("Cannot transfer: not a super theory", [], [], [th], 589 SOME (Context.Theory thy')); 590 val cert' = Context.join_certificate (Context.Certificate thy', cert); 591 in 592 if Context.eq_certificate (cert, cert') then th 593 else 594 Thm (der, 595 {cert = cert', 596 tags = tags, 597 maxidx = maxidx, 598 constraints = constraints, 599 shyps = shyps, 600 hyps = hyps, 601 tpairs = tpairs, 602 prop = prop}) 603 end; 604 605val transfer' = transfer o Proof_Context.theory_of; 606val transfer'' = transfer o Context.theory_of; 607 608fun join_transfer thy th = 609 (Context.subthy_id (theory_id th, Context.theory_id thy) ? transfer thy) th; 610 611fun join_transfer_context (ctxt, th) = 612 if Context.subthy_id (theory_id th, Context.theory_id (Proof_Context.theory_of ctxt)) 613 then (ctxt, transfer' ctxt th) 614 else (Context.raw_transfer (theory_of_thm th) ctxt, th); 615 616 617(* matching *) 618 619local 620 621fun gen_match match 622 (ct1 as Cterm {t = t1, sorts = sorts1, ...}, 623 ct2 as Cterm {t = t2, sorts = sorts2, maxidx = maxidx2, ...}) = 624 let 625 val cert = join_certificate0 (ct1, ct2); 626 val thy = Context.certificate_theory cert 627 handle ERROR msg => raise CONTEXT (msg, [], [ct1, ct2], [], NONE); 628 val (Tinsts, tinsts) = match thy (t1, t2) (Vartab.empty, Vartab.empty); 629 val sorts = Sorts.union sorts1 sorts2; 630 fun mk_cTinst ((a, i), (S, T)) = 631 (((a, i), S), Ctyp {T = T, cert = cert, maxidx = maxidx2, sorts = sorts}); 632 fun mk_ctinst ((x, i), (U, t)) = 633 let val T = Envir.subst_type Tinsts U in 634 (((x, i), T), Cterm {t = t, T = T, cert = cert, maxidx = maxidx2, sorts = sorts}) 635 end; 636 in (Vartab.fold (cons o mk_cTinst) Tinsts [], Vartab.fold (cons o mk_ctinst) tinsts []) end; 637 638in 639 640val match = gen_match Pattern.match; 641val first_order_match = gen_match Pattern.first_order_match; 642 643end; 644 645 646(*implicit alpha-conversion*) 647fun renamed_prop prop' (Thm (der, {cert, tags, maxidx, constraints, shyps, hyps, tpairs, prop})) = 648 if prop aconv prop' then 649 Thm (der, {cert = cert, tags = tags, maxidx = maxidx, constraints = constraints, shyps = shyps, 650 hyps = hyps, tpairs = tpairs, prop = prop'}) 651 else raise TERM ("renamed_prop: props disagree", [prop, prop']); 652 653fun make_context ths NONE cert = 654 (Context.Theory (Context.certificate_theory cert) 655 handle ERROR msg => raise CONTEXT (msg, [], [], ths, NONE)) 656 | make_context ths (SOME ctxt) cert = 657 let 658 val thy_id = Context.certificate_theory_id cert; 659 val thy_id' = Context.theory_id (Proof_Context.theory_of ctxt); 660 in 661 if Context.subthy_id (thy_id, thy_id') then Context.Proof ctxt 662 else raise CONTEXT ("Bad context", [], [], ths, SOME (Context.Proof ctxt)) 663 end; 664 665fun make_context_certificate ths opt_ctxt cert = 666 let 667 val context = make_context ths opt_ctxt cert; 668 val cert' = Context.Certificate (Context.theory_of context); 669 in (context, cert') end; 670 671(*explicit weakening: maps |- B to A |- B*) 672fun weaken raw_ct th = 673 let 674 val ct as Cterm {t = A, T, sorts, maxidx = maxidxA, ...} = adjust_maxidx_cterm ~1 raw_ct; 675 val Thm (der, {tags, maxidx, constraints, shyps, hyps, tpairs, prop, ...}) = th; 676 in 677 if T <> propT then 678 raise THM ("weaken: assumptions must have type prop", 0, []) 679 else if maxidxA <> ~1 then 680 raise THM ("weaken: assumptions may not contain schematic variables", maxidxA, []) 681 else 682 Thm (der, 683 {cert = join_certificate1 (ct, th), 684 tags = tags, 685 maxidx = maxidx, 686 constraints = constraints, 687 shyps = Sorts.union sorts shyps, 688 hyps = insert_hyps A hyps, 689 tpairs = tpairs, 690 prop = prop}) 691 end; 692 693fun weaken_sorts raw_sorts ct = 694 let 695 val Cterm {cert, t, T, maxidx, sorts} = ct; 696 val thy = theory_of_cterm ct; 697 val more_sorts = Sorts.make (map (Sign.certify_sort thy) raw_sorts); 698 val sorts' = Sorts.union sorts more_sorts; 699 in Cterm {cert = cert, t = t, T = T, maxidx = maxidx, sorts = sorts'} end; 700 701 702 703(** derivations and promised proofs **) 704 705fun make_deriv promises oracles thms proof = 706 Deriv {promises = promises, body = PBody {oracles = oracles, thms = thms, proof = proof}}; 707 708val empty_deriv = make_deriv [] [] [] MinProof; 709 710 711(* inference rules *) 712 713val promise_ord: (serial * thm future) ord = fn ((i, _), (j, _)) => int_ord (j, i); 714 715fun bad_proofs i = 716 error ("Illegal level of detail for proof objects: " ^ string_of_int i); 717 718fun deriv_rule2 f 719 (Deriv {promises = ps1, body = PBody {oracles = oracles1, thms = thms1, proof = prf1}}) 720 (Deriv {promises = ps2, body = PBody {oracles = oracles2, thms = thms2, proof = prf2}}) = 721 let 722 val ps = Ord_List.union promise_ord ps1 ps2; 723 val oracles = Proofterm.unions_oracles [oracles1, oracles2]; 724 val thms = Proofterm.unions_thms [thms1, thms2]; 725 val prf = 726 (case ! Proofterm.proofs of 727 2 => f prf1 prf2 728 | 1 => MinProof 729 | 0 => MinProof 730 | i => bad_proofs i); 731 in make_deriv ps oracles thms prf end; 732 733fun deriv_rule1 f = deriv_rule2 (K f) empty_deriv; 734 735fun deriv_rule0 make_prf = 736 if ! Proofterm.proofs <= 1 then empty_deriv 737 else deriv_rule1 I (make_deriv [] [] [] (make_prf ())); 738 739fun deriv_rule_unconditional f (Deriv {promises, body = PBody {oracles, thms, proof}}) = 740 make_deriv promises oracles thms (f proof); 741 742 743(* fulfilled proofs *) 744 745fun raw_promises_of (Thm (Deriv {promises, ...}, _)) = promises; 746 747fun join_promises [] = () 748 | join_promises promises = join_promises_of (Future.joins (map snd promises)) 749and join_promises_of thms = join_promises (Ord_List.make promise_ord (maps raw_promises_of thms)); 750 751fun fulfill_body (th as Thm (Deriv {promises, body}, _)) = 752 let val fulfilled_promises = map #1 promises ~~ map fulfill_body (Future.joins (map #2 promises)) 753 in Proofterm.fulfill_norm_proof (theory_of_thm th) fulfilled_promises body end; 754 755fun proof_bodies_of thms = (join_promises_of thms; map fulfill_body thms); 756val proof_body_of = singleton proof_bodies_of; 757val proof_of = Proofterm.proof_of o proof_body_of; 758 759fun reconstruct_proof_of thm = 760 Proofterm.reconstruct_proof (theory_of_thm thm) (prop_of thm) (proof_of thm); 761 762val consolidate = ignore o proof_bodies_of; 763 764fun expose_proofs thy thms = 765 if Proofterm.export_proof_boxes_required thy then 766 Proofterm.export_proof_boxes (proof_bodies_of (map (transfer thy) thms)) 767 else (); 768 769fun expose_proof thy = expose_proofs thy o single; 770 771 772(* future rule *) 773 774fun future_result i orig_cert orig_shyps orig_prop thm = 775 let 776 fun err msg = raise THM ("future_result: " ^ msg, 0, [thm]); 777 val Thm (Deriv {promises, ...}, {cert, constraints, shyps, hyps, tpairs, prop, ...}) = thm; 778 779 val _ = Context.eq_certificate (cert, orig_cert) orelse err "bad theory"; 780 val _ = prop aconv orig_prop orelse err "bad prop"; 781 val _ = null constraints orelse err "bad sort constraints"; 782 val _ = null tpairs orelse err "bad flex-flex constraints"; 783 val _ = null hyps orelse err "bad hyps"; 784 val _ = Sorts.subset (shyps, orig_shyps) orelse err "bad shyps"; 785 val _ = forall (fn (j, _) => i <> j) promises orelse err "bad dependencies"; 786 val _ = join_promises promises; 787 in thm end; 788 789fun future future_thm ct = 790 let 791 val Cterm {cert = cert, t = prop, T, maxidx, sorts} = ct; 792 val _ = T <> propT andalso raise CTERM ("future: prop expected", [ct]); 793 val _ = 794 if Proofterm.proofs_enabled () 795 then raise CTERM ("future: proof terms enabled", [ct]) else (); 796 797 val i = serial (); 798 val future = future_thm |> Future.map (future_result i cert sorts prop); 799 in 800 Thm (make_deriv [(i, future)] [] [] MinProof, 801 {cert = cert, 802 tags = [], 803 maxidx = maxidx, 804 constraints = [], 805 shyps = sorts, 806 hyps = [], 807 tpairs = [], 808 prop = prop}) 809 end; 810 811 812 813(** Axioms **) 814 815fun axiom thy name = 816 (case Name_Space.lookup (Theory.axiom_table thy) name of 817 SOME prop => 818 let 819 val der = deriv_rule0 (fn () => Proofterm.axm_proof name prop); 820 val cert = Context.Certificate thy; 821 val maxidx = maxidx_of_term prop; 822 val shyps = Sorts.insert_term prop []; 823 in 824 Thm (der, 825 {cert = cert, tags = [], maxidx = maxidx, 826 constraints = [], shyps = shyps, hyps = [], tpairs = [], prop = prop}) 827 end 828 | NONE => raise THEORY ("No axiom " ^ quote name, [thy])); 829 830fun all_axioms_of thy = 831 map (fn (name, _) => (name, axiom thy name)) (Theory.all_axioms_of thy); 832 833 834(* tags *) 835 836val get_tags = #tags o rep_thm; 837 838fun map_tags f (Thm (der, {cert, tags, maxidx, constraints, shyps, hyps, tpairs, prop})) = 839 Thm (der, {cert = cert, tags = f tags, maxidx = maxidx, constraints = constraints, 840 shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop}); 841 842 843(* technical adjustments *) 844 845fun norm_proof (th as Thm (der, args)) = 846 Thm (deriv_rule1 (Proofterm.rew_proof (theory_of_thm th)) der, args); 847 848fun adjust_maxidx_thm i 849 (th as Thm (der, {cert, tags, maxidx, constraints, shyps, hyps, tpairs, prop})) = 850 if maxidx = i then th 851 else if maxidx < i then 852 Thm (der, {maxidx = i, cert = cert, tags = tags, constraints = constraints, shyps = shyps, 853 hyps = hyps, tpairs = tpairs, prop = prop}) 854 else 855 Thm (der, {maxidx = Int.max (maxidx_tpairs tpairs (maxidx_of_term prop), i), 856 cert = cert, tags = tags, constraints = constraints, shyps = shyps, 857 hyps = hyps, tpairs = tpairs, prop = prop}); 858 859 860 861(*** Theory data ***) 862 863(* type classes *) 864 865structure Aritytab = 866 Table( 867 type key = string * sort list * class; 868 val ord = 869 fast_string_ord o apply2 #1 870 <<< fast_string_ord o apply2 #3 871 <<< list_ord Term_Ord.sort_ord o apply2 #2; 872 ); 873 874datatype classes = Classes of 875 {classrels: thm Symreltab.table, 876 arities: (thm * string * serial) Aritytab.table}; 877 878fun make_classes (classrels, arities) = Classes {classrels = classrels, arities = arities}; 879 880val empty_classes = make_classes (Symreltab.empty, Aritytab.empty); 881 882(*see Theory.at_begin hook for transitive closure of classrels and arity completion*) 883fun merge_classes 884 (Classes {classrels = classrels1, arities = arities1}, 885 Classes {classrels = classrels2, arities = arities2}) = 886 let 887 val classrels' = Symreltab.merge (K true) (classrels1, classrels2); 888 val arities' = Aritytab.merge (K true) (arities1, arities2); 889 in make_classes (classrels', arities') end; 890 891 892(* data *) 893 894structure Data = Theory_Data 895( 896 type T = 897 unit Name_Space.table * (*oracles: authentic derivation names*) 898 classes; (*type classes within the logic*) 899 900 val empty : T = (Name_Space.empty_table "oracle", empty_classes); 901 val extend = I; 902 fun merge ((oracles1, sorts1), (oracles2, sorts2)) : T = 903 (Name_Space.merge_tables (oracles1, oracles2), merge_classes (sorts1, sorts2)); 904); 905 906val get_oracles = #1 o Data.get; 907val map_oracles = Data.map o apfst; 908 909val get_classes = (fn (_, Classes args) => args) o Data.get; 910val get_classrels = #classrels o get_classes; 911val get_arities = #arities o get_classes; 912 913fun map_classes f = 914 (Data.map o apsnd) (fn Classes {classrels, arities} => make_classes (f (classrels, arities))); 915fun map_classrels f = map_classes (fn (classrels, arities) => (f classrels, arities)); 916fun map_arities f = map_classes (fn (classrels, arities) => (classrels, f arities)); 917 918 919(* type classes *) 920 921fun the_classrel thy (c1, c2) = 922 (case Symreltab.lookup (get_classrels thy) (c1, c2) of 923 SOME thm => transfer thy thm 924 | NONE => error ("Unproven class relation " ^ 925 Syntax.string_of_classrel (Proof_Context.init_global thy) [c1, c2])); 926 927fun the_arity thy (a, Ss, c) = 928 (case Aritytab.lookup (get_arities thy) (a, Ss, c) of 929 SOME (thm, _, _) => transfer thy thm 930 | NONE => error ("Unproven type arity " ^ 931 Syntax.string_of_arity (Proof_Context.init_global thy) (a, Ss, [c]))); 932 933val classrel_proof = proof_of oo the_classrel; 934val arity_proof = proof_of oo the_arity; 935 936 937(* solve sort constraints by pro-forma proof *) 938 939local 940 941fun union_digest (oracles1, thms1) (oracles2, thms2) = 942 (Proofterm.unions_oracles [oracles1, oracles2], Proofterm.unions_thms [thms1, thms2]); 943 944fun thm_digest (Thm (Deriv {body = PBody {oracles, thms, ...}, ...}, _)) = 945 (oracles, thms); 946 947fun constraint_digest ({theory = thy, typ, sort, ...}: constraint) = 948 Sorts.of_sort_derivation (Sign.classes_of thy) 949 {class_relation = fn _ => fn _ => fn (digest, c1) => fn c2 => 950 if c1 = c2 then ([], []) else union_digest digest (thm_digest (the_classrel thy (c1, c2))), 951 type_constructor = fn (a, _) => fn dom => fn c => 952 let val arity_digest = thm_digest (the_arity thy (a, (map o map) #2 dom, c)) 953 in (fold o fold) (union_digest o #1) dom arity_digest end, 954 type_variable = fn T => map (pair ([], [])) (Type.sort_of_atyp T)} 955 (typ, sort); 956 957in 958 959fun solve_constraints (thm as Thm (_, {constraints = [], ...})) = thm 960 | solve_constraints (thm as Thm (der, args)) = 961 let 962 val {cert, tags, maxidx, constraints, shyps, hyps, tpairs, prop} = args; 963 964 val thy = Context.certificate_theory cert; 965 val bad_thys = 966 constraints |> map_filter (fn {theory = thy', ...} => 967 if Context.eq_thy (thy, thy') then NONE else SOME thy'); 968 val () = 969 if null bad_thys then () 970 else 971 raise THEORY ("solve_constraints: bad theories for theorem\n" ^ 972 Syntax.string_of_term_global thy (prop_of thm), thy :: bad_thys); 973 974 val Deriv {promises, body = PBody {oracles, thms, proof}} = der; 975 val (oracles', thms') = (oracles, thms) 976 |> fold (fold union_digest o constraint_digest) constraints; 977 val body' = PBody {oracles = oracles', thms = thms', proof = proof}; 978 in 979 Thm (Deriv {promises = promises, body = body'}, 980 {constraints = [], cert = cert, tags = tags, maxidx = maxidx, 981 shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop}) 982 end; 983 984end; 985 986(*Dangling sort constraints of a thm*) 987fun extra_shyps (th as Thm (_, {shyps, ...})) = 988 Sorts.subtract (fold_terms Sorts.insert_term th []) shyps; 989 990(*Remove extra sorts that are witnessed by type signature information*) 991fun strip_shyps thm = 992 (case thm of 993 Thm (_, {shyps = [], ...}) => thm 994 | Thm (der, {cert, tags, maxidx, constraints, shyps, hyps, tpairs, prop}) => 995 let 996 val thy = theory_of_thm thm; 997 998 val algebra = Sign.classes_of thy; 999 val minimize = Sorts.minimize_sort algebra; 1000 val le = Sorts.sort_le algebra; 1001 fun lt (S1, S2) = le (S1, S2) andalso not (le (S2, S1)); 1002 fun rel (S1, S2) = if S1 = S2 then [] else [(Term.aT S1, S2)]; 1003 1004 val present = (fold_terms o fold_types o fold_atyps_sorts) (insert (eq_fst op =)) thm []; 1005 val extra = fold (Sorts.remove_sort o #2) present shyps; 1006 val witnessed = Sign.witness_sorts thy present extra; 1007 val non_witnessed = fold (Sorts.remove_sort o #2) witnessed extra |> map (`minimize); 1008 1009 val extra' = 1010 non_witnessed |> map_filter (fn (S, _) => 1011 if non_witnessed |> exists (fn (S', _) => lt (S', S)) then NONE else SOME S) 1012 |> Sorts.make; 1013 1014 val constrs' = 1015 non_witnessed |> maps (fn (S1, S2) => 1016 let val S0 = the (find_first (fn S => le (S, S1)) extra') 1017 in rel (S0, S1) @ rel (S1, S2) end); 1018 1019 val constraints' = fold (insert_constraints thy) (witnessed @ constrs') constraints; 1020 val shyps' = fold (Sorts.insert_sort o #2) present extra'; 1021 in 1022 Thm (deriv_rule_unconditional 1023 (Proofterm.strip_shyps_proof algebra present witnessed extra') der, 1024 {cert = cert, tags = tags, maxidx = maxidx, constraints = constraints', 1025 shyps = shyps', hyps = hyps, tpairs = tpairs, prop = prop}) 1026 end) 1027 |> solve_constraints; 1028 1029 1030 1031(*** Closed theorems with official name ***) 1032 1033(*non-deterministic, depends on unknown promises*) 1034fun derivation_closed (Thm (Deriv {body, ...}, _)) = 1035 Proofterm.compact_proof (Proofterm.proof_of body); 1036 1037(*non-deterministic, depends on unknown promises*) 1038fun raw_derivation_name (Thm (Deriv {body, ...}, {shyps, hyps, prop, ...})) = 1039 Proofterm.get_approximative_name shyps hyps prop (Proofterm.proof_of body); 1040 1041fun expand_name (Thm (Deriv {body, ...}, {shyps, hyps, prop, ...})) = 1042 let 1043 val self_id = 1044 (case Proofterm.get_identity shyps hyps prop (Proofterm.proof_of body) of 1045 NONE => K false 1046 | SOME {serial, ...} => fn (header: Proofterm.thm_header) => serial = #serial header); 1047 fun expand header = if self_id header orelse #name header = "" then SOME "" else NONE; 1048 in expand end; 1049 1050(*deterministic name of finished proof*) 1051fun derivation_name (thm as Thm (_, {shyps, hyps, prop, ...})) = 1052 Proofterm.get_approximative_name shyps hyps prop (proof_of thm); 1053 1054(*identified PThm node*) 1055fun derivation_id (thm as Thm (_, {shyps, hyps, prop, ...})) = 1056 Proofterm.get_id shyps hyps prop (proof_of thm); 1057 1058(*dependencies of PThm node*) 1059fun thm_deps (thm as Thm (Deriv {promises = [], body = PBody {thms, ...}, ...}, _)) = 1060 (case (derivation_id thm, thms) of 1061 (SOME {serial = i, ...}, [(j, thm_node)]) => 1062 if i = j then Proofterm.thm_node_thms thm_node else thms 1063 | _ => thms) 1064 | thm_deps thm = raise THM ("thm_deps: bad promises", 0, [thm]); 1065 1066fun name_derivation name_pos = 1067 strip_shyps #> (fn thm as Thm (der, args) => 1068 let 1069 val thy = theory_of_thm thm; 1070 1071 val Deriv {promises, body} = der; 1072 val {shyps, hyps, prop, tpairs, ...} = args; 1073 1074 val _ = null tpairs orelse raise THM ("name_derivation: bad flex-flex constraints", 0, [thm]); 1075 1076 val ps = map (apsnd (Future.map fulfill_body)) promises; 1077 val (pthm, proof) = 1078 Proofterm.thm_proof thy (classrel_proof thy) (arity_proof thy) 1079 name_pos shyps hyps prop ps body; 1080 val der' = make_deriv [] [] [pthm] proof; 1081 in Thm (der', args) end); 1082 1083fun close_derivation pos = 1084 solve_constraints #> (fn thm => 1085 if not (null (tpairs_of thm)) orelse derivation_closed thm then thm 1086 else name_derivation ("", pos) thm); 1087 1088val trim_context = solve_constraints #> trim_context_thm; 1089 1090 1091 1092(*** Oracles ***) 1093 1094fun add_oracle (b, oracle_fn) thy = 1095 let 1096 val (name, oracles') = Name_Space.define (Context.Theory thy) true (b, ()) (get_oracles thy); 1097 val thy' = map_oracles (K oracles') thy; 1098 fun invoke_oracle arg = 1099 let val Cterm {cert = cert2, t = prop, T, maxidx, sorts} = oracle_fn arg in 1100 if T <> propT then 1101 raise THM ("Oracle's result must have type prop: " ^ name, 0, []) 1102 else 1103 let 1104 val (oracle, prf) = 1105 (case ! Proofterm.proofs of 1106 2 => (((name, Position.thread_data ()), SOME prop), Proofterm.oracle_proof name prop) 1107 | 1 => (((name, Position.thread_data ()), SOME prop), MinProof) 1108 | 0 => (((name, Position.none), NONE), MinProof) 1109 | i => bad_proofs i); 1110 in 1111 Thm (make_deriv [] [oracle] [] prf, 1112 {cert = Context.join_certificate (Context.Certificate thy', cert2), 1113 tags = [], 1114 maxidx = maxidx, 1115 constraints = [], 1116 shyps = sorts, 1117 hyps = [], 1118 tpairs = [], 1119 prop = prop}) 1120 end 1121 end; 1122 in ((name, invoke_oracle), thy') end; 1123 1124val oracle_space = Name_Space.space_of_table o get_oracles; 1125 1126fun pretty_oracle ctxt = 1127 Name_Space.pretty ctxt (oracle_space (Proof_Context.theory_of ctxt)); 1128 1129fun extern_oracles verbose ctxt = 1130 map #1 (Name_Space.markup_table verbose ctxt (get_oracles (Proof_Context.theory_of ctxt))); 1131 1132fun check_oracle ctxt = 1133 Name_Space.check (Context.Proof ctxt) (get_oracles (Proof_Context.theory_of ctxt)) #> #1; 1134 1135 1136 1137(*** Meta rules ***) 1138 1139(** primitive rules **) 1140 1141(*The assumption rule A |- A*) 1142fun assume raw_ct = 1143 let val Cterm {cert, t = prop, T, maxidx, sorts} = adjust_maxidx_cterm ~1 raw_ct in 1144 if T <> propT then 1145 raise THM ("assume: prop", 0, []) 1146 else if maxidx <> ~1 then 1147 raise THM ("assume: variables", maxidx, []) 1148 else Thm (deriv_rule0 (fn () => Proofterm.Hyp prop), 1149 {cert = cert, 1150 tags = [], 1151 maxidx = ~1, 1152 constraints = [], 1153 shyps = sorts, 1154 hyps = [prop], 1155 tpairs = [], 1156 prop = prop}) 1157 end; 1158 1159(*Implication introduction 1160 [A] 1161 : 1162 B 1163 ------- 1164 A \<Longrightarrow> B 1165*) 1166fun implies_intr 1167 (ct as Cterm {t = A, T, maxidx = maxidx1, sorts, ...}) 1168 (th as Thm (der, {maxidx = maxidx2, hyps, constraints, shyps, tpairs, prop, ...})) = 1169 if T <> propT then 1170 raise THM ("implies_intr: assumptions must have type prop", 0, [th]) 1171 else 1172 Thm (deriv_rule1 (Proofterm.implies_intr_proof A) der, 1173 {cert = join_certificate1 (ct, th), 1174 tags = [], 1175 maxidx = Int.max (maxidx1, maxidx2), 1176 constraints = constraints, 1177 shyps = Sorts.union sorts shyps, 1178 hyps = remove_hyps A hyps, 1179 tpairs = tpairs, 1180 prop = Logic.mk_implies (A, prop)}); 1181 1182 1183(*Implication elimination 1184 A \<Longrightarrow> B A 1185 ------------ 1186 B 1187*) 1188fun implies_elim thAB thA = 1189 let 1190 val Thm (derA, 1191 {maxidx = maxidx1, hyps = hypsA, constraints = constraintsA, shyps = shypsA, 1192 tpairs = tpairsA, prop = propA, ...}) = thA 1193 and Thm (der, {maxidx = maxidx2, hyps, constraints, shyps, tpairs, prop, ...}) = thAB; 1194 fun err () = raise THM ("implies_elim: major premise", 0, [thAB, thA]); 1195 in 1196 (case prop of 1197 Const ("Pure.imp", _) $ A $ B => 1198 if A aconv propA then 1199 Thm (deriv_rule2 (curry Proofterm.%%) der derA, 1200 {cert = join_certificate2 (thAB, thA), 1201 tags = [], 1202 maxidx = Int.max (maxidx1, maxidx2), 1203 constraints = union_constraints constraintsA constraints, 1204 shyps = Sorts.union shypsA shyps, 1205 hyps = union_hyps hypsA hyps, 1206 tpairs = union_tpairs tpairsA tpairs, 1207 prop = B}) 1208 else err () 1209 | _ => err ()) 1210 end; 1211 1212(*Forall introduction. The Free or Var x must not be free in the hypotheses. 1213 [x] 1214 : 1215 A 1216 ------ 1217 \<And>x. A 1218*) 1219fun forall_intr 1220 (ct as Cterm {maxidx = maxidx1, t = x, T, sorts, ...}) 1221 (th as Thm (der, {maxidx = maxidx2, constraints, shyps, hyps, tpairs, prop, ...})) = 1222 let 1223 fun result a = 1224 Thm (deriv_rule1 (Proofterm.forall_intr_proof (a, x) NONE) der, 1225 {cert = join_certificate1 (ct, th), 1226 tags = [], 1227 maxidx = Int.max (maxidx1, maxidx2), 1228 constraints = constraints, 1229 shyps = Sorts.union sorts shyps, 1230 hyps = hyps, 1231 tpairs = tpairs, 1232 prop = Logic.all_const T $ Abs (a, T, abstract_over (x, prop))}); 1233 fun check_occs a x ts = 1234 if exists (fn t => Logic.occs (x, t)) ts then 1235 raise THM ("forall_intr: variable " ^ quote a ^ " free in assumptions", 0, [th]) 1236 else (); 1237 in 1238 (case x of 1239 Free (a, _) => (check_occs a x hyps; check_occs a x (terms_of_tpairs tpairs); result a) 1240 | Var ((a, _), _) => (check_occs a x (terms_of_tpairs tpairs); result a) 1241 | _ => raise THM ("forall_intr: not a variable", 0, [th])) 1242 end; 1243 1244(*Forall elimination 1245 \<And>x. A 1246 ------ 1247 A[t/x] 1248*) 1249fun forall_elim 1250 (ct as Cterm {t, T, maxidx = maxidx1, sorts, ...}) 1251 (th as Thm (der, {maxidx = maxidx2, constraints, shyps, hyps, tpairs, prop, ...})) = 1252 (case prop of 1253 Const ("Pure.all", Type ("fun", [Type ("fun", [qary, _]), _])) $ A => 1254 if T <> qary then 1255 raise THM ("forall_elim: type mismatch", 0, [th]) 1256 else 1257 Thm (deriv_rule1 (Proofterm.% o rpair (SOME t)) der, 1258 {cert = join_certificate1 (ct, th), 1259 tags = [], 1260 maxidx = Int.max (maxidx1, maxidx2), 1261 constraints = constraints, 1262 shyps = Sorts.union sorts shyps, 1263 hyps = hyps, 1264 tpairs = tpairs, 1265 prop = Term.betapply (A, t)}) 1266 | _ => raise THM ("forall_elim: not quantified", 0, [th])); 1267 1268 1269(* Equality *) 1270 1271(*Reflexivity 1272 t \<equiv> t 1273*) 1274fun reflexive (Cterm {cert, t, T = _, maxidx, sorts}) = 1275 Thm (deriv_rule0 (fn () => Proofterm.reflexive_proof), 1276 {cert = cert, 1277 tags = [], 1278 maxidx = maxidx, 1279 constraints = [], 1280 shyps = sorts, 1281 hyps = [], 1282 tpairs = [], 1283 prop = Logic.mk_equals (t, t)}); 1284 1285(*Symmetry 1286 t \<equiv> u 1287 ------ 1288 u \<equiv> t 1289*) 1290fun symmetric (th as Thm (der, {cert, maxidx, constraints, shyps, hyps, tpairs, prop, ...})) = 1291 (case prop of 1292 (eq as Const ("Pure.eq", _)) $ t $ u => 1293 Thm (deriv_rule1 Proofterm.symmetric_proof der, 1294 {cert = cert, 1295 tags = [], 1296 maxidx = maxidx, 1297 constraints = constraints, 1298 shyps = shyps, 1299 hyps = hyps, 1300 tpairs = tpairs, 1301 prop = eq $ u $ t}) 1302 | _ => raise THM ("symmetric", 0, [th])); 1303 1304(*Transitivity 1305 t1 \<equiv> u u \<equiv> t2 1306 ------------------ 1307 t1 \<equiv> t2 1308*) 1309fun transitive th1 th2 = 1310 let 1311 val Thm (der1, {maxidx = maxidx1, hyps = hyps1, constraints = constraints1, shyps = shyps1, 1312 tpairs = tpairs1, prop = prop1, ...}) = th1 1313 and Thm (der2, {maxidx = maxidx2, hyps = hyps2, constraints = constraints2, shyps = shyps2, 1314 tpairs = tpairs2, prop = prop2, ...}) = th2; 1315 fun err msg = raise THM ("transitive: " ^ msg, 0, [th1, th2]); 1316 in 1317 case (prop1, prop2) of 1318 ((eq as Const ("Pure.eq", Type (_, [U, _]))) $ t1 $ u, Const ("Pure.eq", _) $ u' $ t2) => 1319 if not (u aconv u') then err "middle term" 1320 else 1321 Thm (deriv_rule2 (Proofterm.transitive_proof U u) der1 der2, 1322 {cert = join_certificate2 (th1, th2), 1323 tags = [], 1324 maxidx = Int.max (maxidx1, maxidx2), 1325 constraints = union_constraints constraints1 constraints2, 1326 shyps = Sorts.union shyps1 shyps2, 1327 hyps = union_hyps hyps1 hyps2, 1328 tpairs = union_tpairs tpairs1 tpairs2, 1329 prop = eq $ t1 $ t2}) 1330 | _ => err "premises" 1331 end; 1332 1333(*Beta-conversion 1334 (\<lambda>x. t) u \<equiv> t[u/x] 1335 fully beta-reduces the term if full = true 1336*) 1337fun beta_conversion full (Cterm {cert, t, T = _, maxidx, sorts}) = 1338 let val t' = 1339 if full then Envir.beta_norm t 1340 else 1341 (case t of Abs (_, _, bodt) $ u => subst_bound (u, bodt) 1342 | _ => raise THM ("beta_conversion: not a redex", 0, [])); 1343 in 1344 Thm (deriv_rule0 (fn () => Proofterm.reflexive_proof), 1345 {cert = cert, 1346 tags = [], 1347 maxidx = maxidx, 1348 constraints = [], 1349 shyps = sorts, 1350 hyps = [], 1351 tpairs = [], 1352 prop = Logic.mk_equals (t, t')}) 1353 end; 1354 1355fun eta_conversion (Cterm {cert, t, T = _, maxidx, sorts}) = 1356 Thm (deriv_rule0 (fn () => Proofterm.reflexive_proof), 1357 {cert = cert, 1358 tags = [], 1359 maxidx = maxidx, 1360 constraints = [], 1361 shyps = sorts, 1362 hyps = [], 1363 tpairs = [], 1364 prop = Logic.mk_equals (t, Envir.eta_contract t)}); 1365 1366fun eta_long_conversion (Cterm {cert, t, T = _, maxidx, sorts}) = 1367 Thm (deriv_rule0 (fn () => Proofterm.reflexive_proof), 1368 {cert = cert, 1369 tags = [], 1370 maxidx = maxidx, 1371 constraints = [], 1372 shyps = sorts, 1373 hyps = [], 1374 tpairs = [], 1375 prop = Logic.mk_equals (t, Envir.eta_long [] t)}); 1376 1377(*The abstraction rule. The Free or Var x must not be free in the hypotheses. 1378 The bound variable will be named "a" (since x will be something like x320) 1379 t \<equiv> u 1380 -------------- 1381 \<lambda>x. t \<equiv> \<lambda>x. u 1382*) 1383fun abstract_rule a 1384 (Cterm {t = x, T, sorts, ...}) 1385 (th as Thm (der, {cert, maxidx, hyps, constraints, shyps, tpairs, prop, ...})) = 1386 let 1387 val (t, u) = Logic.dest_equals prop 1388 handle TERM _ => raise THM ("abstract_rule: premise not an equality", 0, [th]); 1389 val result = 1390 Thm (deriv_rule1 (Proofterm.abstract_rule_proof (a, x)) der, 1391 {cert = cert, 1392 tags = [], 1393 maxidx = maxidx, 1394 constraints = constraints, 1395 shyps = Sorts.union sorts shyps, 1396 hyps = hyps, 1397 tpairs = tpairs, 1398 prop = Logic.mk_equals 1399 (Abs (a, T, abstract_over (x, t)), Abs (a, T, abstract_over (x, u)))}); 1400 fun check_occs a x ts = 1401 if exists (fn t => Logic.occs (x, t)) ts then 1402 raise THM ("abstract_rule: variable " ^ quote a ^ " free in assumptions", 0, [th]) 1403 else (); 1404 in 1405 (case x of 1406 Free (a, _) => (check_occs a x hyps; check_occs a x (terms_of_tpairs tpairs); result) 1407 | Var ((a, _), _) => (check_occs a x (terms_of_tpairs tpairs); result) 1408 | _ => raise THM ("abstract_rule: not a variable", 0, [th])) 1409 end; 1410 1411(*The combination rule 1412 f \<equiv> g t \<equiv> u 1413 ------------- 1414 f t \<equiv> g u 1415*) 1416fun combination th1 th2 = 1417 let 1418 val Thm (der1, {maxidx = maxidx1, constraints = constraints1, shyps = shyps1, 1419 hyps = hyps1, tpairs = tpairs1, prop = prop1, ...}) = th1 1420 and Thm (der2, {maxidx = maxidx2, constraints = constraints2, shyps = shyps2, 1421 hyps = hyps2, tpairs = tpairs2, prop = prop2, ...}) = th2; 1422 fun chktypes fT tT = 1423 (case fT of 1424 Type ("fun", [T1, _]) => 1425 if T1 <> tT then 1426 raise THM ("combination: types", 0, [th1, th2]) 1427 else () 1428 | _ => raise THM ("combination: not function type", 0, [th1, th2])); 1429 in 1430 (case (prop1, prop2) of 1431 (Const ("Pure.eq", Type ("fun", [fT, _])) $ f $ g, 1432 Const ("Pure.eq", Type ("fun", [tT, _])) $ t $ u) => 1433 (chktypes fT tT; 1434 Thm (deriv_rule2 (Proofterm.combination_proof f g t u) der1 der2, 1435 {cert = join_certificate2 (th1, th2), 1436 tags = [], 1437 maxidx = Int.max (maxidx1, maxidx2), 1438 constraints = union_constraints constraints1 constraints2, 1439 shyps = Sorts.union shyps1 shyps2, 1440 hyps = union_hyps hyps1 hyps2, 1441 tpairs = union_tpairs tpairs1 tpairs2, 1442 prop = Logic.mk_equals (f $ t, g $ u)})) 1443 | _ => raise THM ("combination: premises", 0, [th1, th2])) 1444 end; 1445 1446(*Equality introduction 1447 A \<Longrightarrow> B B \<Longrightarrow> A 1448 ---------------- 1449 A \<equiv> B 1450*) 1451fun equal_intr th1 th2 = 1452 let 1453 val Thm (der1, {maxidx = maxidx1, constraints = constraints1, shyps = shyps1, 1454 hyps = hyps1, tpairs = tpairs1, prop = prop1, ...}) = th1 1455 and Thm (der2, {maxidx = maxidx2, constraints = constraints2, shyps = shyps2, 1456 hyps = hyps2, tpairs = tpairs2, prop = prop2, ...}) = th2; 1457 fun err msg = raise THM ("equal_intr: " ^ msg, 0, [th1, th2]); 1458 in 1459 (case (prop1, prop2) of 1460 (Const("Pure.imp", _) $ A $ B, Const("Pure.imp", _) $ B' $ A') => 1461 if A aconv A' andalso B aconv B' then 1462 Thm (deriv_rule2 (Proofterm.equal_intr_proof A B) der1 der2, 1463 {cert = join_certificate2 (th1, th2), 1464 tags = [], 1465 maxidx = Int.max (maxidx1, maxidx2), 1466 constraints = union_constraints constraints1 constraints2, 1467 shyps = Sorts.union shyps1 shyps2, 1468 hyps = union_hyps hyps1 hyps2, 1469 tpairs = union_tpairs tpairs1 tpairs2, 1470 prop = Logic.mk_equals (A, B)}) 1471 else err "not equal" 1472 | _ => err "premises") 1473 end; 1474 1475(*The equal propositions rule 1476 A \<equiv> B A 1477 --------- 1478 B 1479*) 1480fun equal_elim th1 th2 = 1481 let 1482 val Thm (der1, {maxidx = maxidx1, constraints = constraints1, shyps = shyps1, 1483 hyps = hyps1, tpairs = tpairs1, prop = prop1, ...}) = th1 1484 and Thm (der2, {maxidx = maxidx2, constraints = constraints2, shyps = shyps2, 1485 hyps = hyps2, tpairs = tpairs2, prop = prop2, ...}) = th2; 1486 fun err msg = raise THM ("equal_elim: " ^ msg, 0, [th1, th2]); 1487 in 1488 (case prop1 of 1489 Const ("Pure.eq", _) $ A $ B => 1490 if prop2 aconv A then 1491 Thm (deriv_rule2 (Proofterm.equal_elim_proof A B) der1 der2, 1492 {cert = join_certificate2 (th1, th2), 1493 tags = [], 1494 maxidx = Int.max (maxidx1, maxidx2), 1495 constraints = union_constraints constraints1 constraints2, 1496 shyps = Sorts.union shyps1 shyps2, 1497 hyps = union_hyps hyps1 hyps2, 1498 tpairs = union_tpairs tpairs1 tpairs2, 1499 prop = B}) 1500 else err "not equal" 1501 | _ => err "major premise") 1502 end; 1503 1504 1505 1506(**** Derived rules ****) 1507 1508(*Smash unifies the list of term pairs leaving no flex-flex pairs. 1509 Instantiates the theorem and deletes trivial tpairs. Resulting 1510 sequence may contain multiple elements if the tpairs are not all 1511 flex-flex.*) 1512fun flexflex_rule opt_ctxt = 1513 solve_constraints #> (fn th => 1514 let 1515 val Thm (der, {cert, maxidx, constraints, shyps, hyps, tpairs, prop, ...}) = th; 1516 val (context, cert') = make_context_certificate [th] opt_ctxt cert; 1517 in 1518 Unify.smash_unifiers context tpairs (Envir.empty maxidx) 1519 |> Seq.map (fn env => 1520 if Envir.is_empty env then th 1521 else 1522 let 1523 val tpairs' = tpairs |> map (apply2 (Envir.norm_term env)) 1524 (*remove trivial tpairs, of the form t \<equiv> t*) 1525 |> filter_out (op aconv); 1526 val der' = deriv_rule1 (Proofterm.norm_proof' env) der; 1527 val constraints' = 1528 insert_constraints_env (Context.certificate_theory cert') env constraints; 1529 val prop' = Envir.norm_term env prop; 1530 val maxidx = maxidx_tpairs tpairs' (maxidx_of_term prop'); 1531 val shyps = Envir.insert_sorts env shyps; 1532 in 1533 Thm (der', {cert = cert', tags = [], maxidx = maxidx, constraints = constraints', 1534 shyps = shyps, hyps = hyps, tpairs = tpairs', prop = prop'}) 1535 end) 1536 end); 1537 1538 1539(*Generalization of fixed variables 1540 A 1541 -------------------- 1542 A[?'a/'a, ?x/x, ...] 1543*) 1544 1545fun generalize ([], []) _ th = th 1546 | generalize (tfrees, frees) idx th = 1547 let 1548 val Thm (der, {cert, maxidx, constraints, shyps, hyps, tpairs, prop, ...}) = th; 1549 val _ = idx <= maxidx andalso raise THM ("generalize: bad index", idx, [th]); 1550 1551 val bad_type = 1552 if null tfrees then K false 1553 else Term.exists_subtype (fn TFree (a, _) => member (op =) tfrees a | _ => false); 1554 fun bad_term (Free (x, T)) = bad_type T orelse member (op =) frees x 1555 | bad_term (Var (_, T)) = bad_type T 1556 | bad_term (Const (_, T)) = bad_type T 1557 | bad_term (Abs (_, T, t)) = bad_type T orelse bad_term t 1558 | bad_term (t $ u) = bad_term t orelse bad_term u 1559 | bad_term (Bound _) = false; 1560 val _ = exists bad_term hyps andalso 1561 raise THM ("generalize: variable free in assumptions", 0, [th]); 1562 1563 val generalize = Term_Subst.generalize (tfrees, frees) idx; 1564 val prop' = generalize prop; 1565 val tpairs' = map (apply2 generalize) tpairs; 1566 val maxidx' = maxidx_tpairs tpairs' (maxidx_of_term prop'); 1567 in 1568 Thm (deriv_rule1 (Proofterm.generalize_proof (tfrees, frees) idx prop) der, 1569 {cert = cert, 1570 tags = [], 1571 maxidx = maxidx', 1572 constraints = constraints, 1573 shyps = shyps, 1574 hyps = hyps, 1575 tpairs = tpairs', 1576 prop = prop'}) 1577 end; 1578 1579fun generalize_cterm ([], []) _ ct = ct 1580 | generalize_cterm (tfrees, frees) idx (ct as Cterm {cert, t, T, maxidx, sorts}) = 1581 if idx <= maxidx then raise CTERM ("generalize_cterm: bad index", [ct]) 1582 else 1583 Cterm {cert = cert, sorts = sorts, 1584 T = Term_Subst.generalizeT tfrees idx T, 1585 t = Term_Subst.generalize (tfrees, frees) idx t, 1586 maxidx = Int.max (maxidx, idx)}; 1587 1588fun generalize_ctyp [] _ cT = cT 1589 | generalize_ctyp tfrees idx (Ctyp {cert, T, maxidx, sorts}) = 1590 if idx <= maxidx then raise CTERM ("generalize_ctyp: bad index", []) 1591 else 1592 Ctyp {cert = cert, sorts = sorts, 1593 T = Term_Subst.generalizeT tfrees idx T, 1594 maxidx = Int.max (maxidx, idx)}; 1595 1596 1597(*Instantiation of schematic variables 1598 A 1599 -------------------- 1600 A[t1/v1, ..., tn/vn] 1601*) 1602 1603local 1604 1605fun pretty_typing thy t T = Pretty.block 1606 [Syntax.pretty_term_global thy t, Pretty.str " ::", Pretty.brk 1, Syntax.pretty_typ_global thy T]; 1607 1608fun add_inst (v as (_, T), cu) (cert, sorts) = 1609 let 1610 val Cterm {t = u, T = U, cert = cert2, sorts = sorts_u, maxidx = maxidx_u, ...} = cu; 1611 val cert' = Context.join_certificate (cert, cert2); 1612 val sorts' = Sorts.union sorts_u sorts; 1613 in 1614 if T = U then ((v, (u, maxidx_u)), (cert', sorts')) 1615 else 1616 let 1617 val msg = 1618 (case cert' of 1619 Context.Certificate thy' => 1620 Pretty.string_of (Pretty.block 1621 [Pretty.str "instantiate: type conflict", 1622 Pretty.fbrk, pretty_typing thy' (Var v) T, 1623 Pretty.fbrk, pretty_typing thy' u U]) 1624 | Context.Certificate_Id _ => "instantiate: type conflict"); 1625 in raise TYPE (msg, [T, U], [Var v, u]) end 1626 end; 1627 1628fun add_instT (v as (_, S), cU) (cert, sorts) = 1629 let 1630 val Ctyp {T = U, cert = cert2, sorts = sorts_U, maxidx = maxidx_U, ...} = cU; 1631 val cert' = Context.join_certificate (cert, cert2); 1632 val thy' = Context.certificate_theory cert' 1633 handle ERROR msg => raise CONTEXT (msg, [cU], [], [], NONE); 1634 val sorts' = Sorts.union sorts_U sorts; 1635 in 1636 if Sign.of_sort thy' (U, S) then ((v, (U, maxidx_U)), (cert', sorts')) 1637 else raise TYPE ("Type not of sort " ^ Syntax.string_of_sort_global thy' S, [U], []) 1638 end; 1639 1640in 1641 1642(*Left-to-right replacements: ctpairs = [..., (vi, ti), ...]. 1643 Instantiates distinct Vars by terms of same type. 1644 Does NOT normalize the resulting theorem!*) 1645fun instantiate ([], []) th = th 1646 | instantiate (instT, inst) th = 1647 let 1648 val Thm (der, {cert, hyps, constraints, shyps, tpairs, prop, ...}) = th; 1649 val (inst', (instT', (cert', shyps'))) = 1650 (cert, shyps) |> fold_map add_inst inst ||> fold_map add_instT instT 1651 handle CONTEXT (msg, cTs, cts, ths, context) => 1652 raise CONTEXT (msg, cTs, cts, th :: ths, context); 1653 val subst = Term_Subst.instantiate_maxidx (instT', inst'); 1654 val (prop', maxidx1) = subst prop ~1; 1655 val (tpairs', maxidx') = 1656 fold_map (fn (t, u) => fn i => subst t i ||>> subst u) tpairs maxidx1; 1657 1658 val thy' = Context.certificate_theory cert'; 1659 val constraints' = 1660 fold (fn ((_, S), (T, _)) => insert_constraints thy' (T, S)) instT' constraints; 1661 in 1662 Thm (deriv_rule1 1663 (fn d => Proofterm.instantiate (map (apsnd #1) instT', map (apsnd #1) inst') d) der, 1664 {cert = cert', 1665 tags = [], 1666 maxidx = maxidx', 1667 constraints = constraints', 1668 shyps = shyps', 1669 hyps = hyps, 1670 tpairs = tpairs', 1671 prop = prop'}) 1672 |> solve_constraints 1673 end 1674 handle TYPE (msg, _, _) => raise THM (msg, 0, [th]); 1675 1676fun instantiate_cterm ([], []) ct = ct 1677 | instantiate_cterm (instT, inst) ct = 1678 let 1679 val Cterm {cert, t, T, sorts, ...} = ct; 1680 val (inst', (instT', (cert', sorts'))) = 1681 (cert, sorts) |> fold_map add_inst inst ||> fold_map add_instT instT; 1682 val subst = Term_Subst.instantiate_maxidx (instT', inst'); 1683 val substT = Term_Subst.instantiateT_maxidx instT'; 1684 val (t', maxidx1) = subst t ~1; 1685 val (T', maxidx') = substT T maxidx1; 1686 in Cterm {cert = cert', t = t', T = T', sorts = sorts', maxidx = maxidx'} end 1687 handle TYPE (msg, _, _) => raise CTERM (msg, [ct]); 1688 1689end; 1690 1691 1692(*The trivial implication A \<Longrightarrow> A, justified by assume and forall rules. 1693 A can contain Vars, not so for assume!*) 1694fun trivial (Cterm {cert, t = A, T, maxidx, sorts}) = 1695 if T <> propT then 1696 raise THM ("trivial: the term must have type prop", 0, []) 1697 else 1698 Thm (deriv_rule0 (fn () => Proofterm.trivial_proof), 1699 {cert = cert, 1700 tags = [], 1701 maxidx = maxidx, 1702 constraints = [], 1703 shyps = sorts, 1704 hyps = [], 1705 tpairs = [], 1706 prop = Logic.mk_implies (A, A)}); 1707 1708(*Axiom-scheme reflecting signature contents 1709 T :: c 1710 ------------------- 1711 OFCLASS(T, c_class) 1712*) 1713fun of_class (cT, raw_c) = 1714 let 1715 val Ctyp {cert, T, ...} = cT; 1716 val thy = Context.certificate_theory cert 1717 handle ERROR msg => raise CONTEXT (msg, [cT], [], [], NONE); 1718 val c = Sign.certify_class thy raw_c; 1719 val Cterm {t = prop, maxidx, sorts, ...} = global_cterm_of thy (Logic.mk_of_class (T, c)); 1720 in 1721 if Sign.of_sort thy (T, [c]) then 1722 Thm (deriv_rule0 (fn () => Proofterm.OfClass (T, c)), 1723 {cert = cert, 1724 tags = [], 1725 maxidx = maxidx, 1726 constraints = insert_constraints thy (T, [c]) [], 1727 shyps = sorts, 1728 hyps = [], 1729 tpairs = [], 1730 prop = prop}) 1731 else raise THM ("of_class: type not of class " ^ Syntax.string_of_sort_global thy [c], 0, []) 1732 end |> solve_constraints; 1733 1734(*Internalize sort constraints of type variables*) 1735val unconstrainT = 1736 strip_shyps #> (fn thm as Thm (der, args) => 1737 let 1738 val Deriv {promises, body} = der; 1739 val {cert, shyps, hyps, tpairs, prop, ...} = args; 1740 val thy = theory_of_thm thm; 1741 1742 fun err msg = raise THM ("unconstrainT: " ^ msg, 0, [thm]); 1743 val _ = null hyps orelse err "bad hyps"; 1744 val _ = null tpairs orelse err "bad flex-flex constraints"; 1745 val tfrees = rev (Term.add_tfree_names prop []); 1746 val _ = null tfrees orelse err ("illegal free type variables " ^ commas_quote tfrees); 1747 1748 val ps = map (apsnd (Future.map fulfill_body)) promises; 1749 val (pthm, proof) = 1750 Proofterm.unconstrain_thm_proof thy (classrel_proof thy) (arity_proof thy) 1751 shyps prop ps body; 1752 val der' = make_deriv [] [] [pthm] proof; 1753 val prop' = Proofterm.thm_node_prop (#2 pthm); 1754 in 1755 Thm (der', 1756 {cert = cert, 1757 tags = [], 1758 maxidx = maxidx_of_term prop', 1759 constraints = [], 1760 shyps = [[]], (*potentially redundant*) 1761 hyps = [], 1762 tpairs = [], 1763 prop = prop'}) 1764 end); 1765 1766(*Replace all TFrees not fixed or in the hyps by new TVars*) 1767fun varifyT_global' fixed (Thm (der, {cert, maxidx, constraints, shyps, hyps, tpairs, prop, ...})) = 1768 let 1769 val tfrees = fold Term.add_tfrees hyps fixed; 1770 val prop1 = attach_tpairs tpairs prop; 1771 val (al, prop2) = Type.varify_global tfrees prop1; 1772 val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2); 1773 in 1774 (al, Thm (deriv_rule1 (Proofterm.varify_proof prop tfrees) der, 1775 {cert = cert, 1776 tags = [], 1777 maxidx = Int.max (0, maxidx), 1778 constraints = constraints, 1779 shyps = shyps, 1780 hyps = hyps, 1781 tpairs = rev (map Logic.dest_equals ts), 1782 prop = prop3})) 1783 end; 1784 1785val varifyT_global = #2 o varifyT_global' []; 1786 1787(*Replace all TVars by TFrees that are often new*) 1788fun legacy_freezeT (Thm (der, {cert, constraints, shyps, hyps, tpairs, prop, ...})) = 1789 let 1790 val prop1 = attach_tpairs tpairs prop; 1791 val prop2 = Type.legacy_freeze prop1; 1792 val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2); 1793 in 1794 Thm (deriv_rule1 (Proofterm.legacy_freezeT prop1) der, 1795 {cert = cert, 1796 tags = [], 1797 maxidx = maxidx_of_term prop2, 1798 constraints = constraints, 1799 shyps = shyps, 1800 hyps = hyps, 1801 tpairs = rev (map Logic.dest_equals ts), 1802 prop = prop3}) 1803 end; 1804 1805fun plain_prop_of raw_thm = 1806 let 1807 val thm = strip_shyps raw_thm; 1808 fun err msg = raise THM ("plain_prop_of: " ^ msg, 0, [thm]); 1809 in 1810 if not (null (hyps_of thm)) then 1811 err "theorem may not contain hypotheses" 1812 else if not (null (extra_shyps thm)) then 1813 err "theorem may not contain sort hypotheses" 1814 else if not (null (tpairs_of thm)) then 1815 err "theorem may not contain flex-flex pairs" 1816 else prop_of thm 1817 end; 1818 1819 1820 1821(*** Inference rules for tactics ***) 1822 1823(*Destruct proof state into constraints, other goals, goal(i), rest *) 1824fun dest_state (state as Thm (_, {prop,tpairs,...}), i) = 1825 (case Logic.strip_prems(i, [], prop) of 1826 (B::rBs, C) => (tpairs, rev rBs, B, C) 1827 | _ => raise THM("dest_state", i, [state])) 1828 handle TERM _ => raise THM("dest_state", i, [state]); 1829 1830(*Prepare orule for resolution by lifting it over the parameters and 1831assumptions of goal.*) 1832fun lift_rule goal orule = 1833 let 1834 val Cterm {t = gprop, T, maxidx = gmax, sorts, ...} = goal; 1835 val inc = gmax + 1; 1836 val lift_abs = Logic.lift_abs inc gprop; 1837 val lift_all = Logic.lift_all inc gprop; 1838 val Thm (der, {maxidx, constraints, shyps, hyps, tpairs, prop, ...}) = orule; 1839 val (As, B) = Logic.strip_horn prop; 1840 in 1841 if T <> propT then raise THM ("lift_rule: the term must have type prop", 0, []) 1842 else 1843 Thm (deriv_rule1 (Proofterm.lift_proof gprop inc prop) der, 1844 {cert = join_certificate1 (goal, orule), 1845 tags = [], 1846 maxidx = maxidx + inc, 1847 constraints = constraints, 1848 shyps = Sorts.union shyps sorts, (*sic!*) 1849 hyps = hyps, 1850 tpairs = map (apply2 lift_abs) tpairs, 1851 prop = Logic.list_implies (map lift_all As, lift_all B)}) 1852 end; 1853 1854fun incr_indexes i (thm as Thm (der, {cert, maxidx, constraints, shyps, hyps, tpairs, prop, ...})) = 1855 if i < 0 then raise THM ("negative increment", 0, [thm]) 1856 else if i = 0 then thm 1857 else 1858 Thm (deriv_rule1 (Proofterm.incr_indexes i) der, 1859 {cert = cert, 1860 tags = [], 1861 maxidx = maxidx + i, 1862 constraints = constraints, 1863 shyps = shyps, 1864 hyps = hyps, 1865 tpairs = map (apply2 (Logic.incr_indexes ([], [], i))) tpairs, 1866 prop = Logic.incr_indexes ([], [], i) prop}); 1867 1868(*Solve subgoal Bi of proof state B1...Bn/C by assumption. *) 1869fun assumption opt_ctxt i state = 1870 let 1871 val Thm (der, {cert, maxidx, constraints, shyps, hyps, ...}) = state; 1872 val (context, cert') = make_context_certificate [state] opt_ctxt cert; 1873 val (tpairs, Bs, Bi, C) = dest_state (state, i); 1874 fun newth n (env, tpairs) = 1875 let 1876 val normt = Envir.norm_term env; 1877 fun assumption_proof prf = 1878 Proofterm.assumption_proof (map normt Bs) (normt Bi) n prf; 1879 in 1880 Thm (deriv_rule1 1881 (assumption_proof #> not (Envir.is_empty env) ? Proofterm.norm_proof' env) der, 1882 {tags = [], 1883 maxidx = Envir.maxidx_of env, 1884 constraints = insert_constraints_env (Context.certificate_theory cert') env constraints, 1885 shyps = Envir.insert_sorts env shyps, 1886 hyps = hyps, 1887 tpairs = if Envir.is_empty env then tpairs else map (apply2 normt) tpairs, 1888 prop = 1889 if Envir.is_empty env then Logic.list_implies (Bs, C) (*avoid wasted normalizations*) 1890 else normt (Logic.list_implies (Bs, C)) (*normalize the new rule fully*), 1891 cert = cert'}) 1892 end; 1893 1894 val (close, asms, concl) = Logic.assum_problems (~1, Bi); 1895 val concl' = close concl; 1896 fun addprfs [] _ = Seq.empty 1897 | addprfs (asm :: rest) n = Seq.make (fn () => Seq.pull 1898 (Seq.mapp (newth n) 1899 (if Term.could_unify (asm, concl) then 1900 (Unify.unifiers (context, Envir.empty maxidx, (close asm, concl') :: tpairs)) 1901 else Seq.empty) 1902 (addprfs rest (n + 1)))) 1903 in addprfs asms 1 end; 1904 1905(*Solve subgoal Bi of proof state B1...Bn/C by assumption. 1906 Checks if Bi's conclusion is alpha/eta-convertible to one of its assumptions*) 1907fun eq_assumption i state = 1908 let 1909 val Thm (der, {cert, maxidx, constraints, shyps, hyps, ...}) = state; 1910 val (tpairs, Bs, Bi, C) = dest_state (state, i); 1911 val (_, asms, concl) = Logic.assum_problems (~1, Bi); 1912 in 1913 (case find_index (fn asm => Envir.aeconv (asm, concl)) asms of 1914 ~1 => raise THM ("eq_assumption", 0, [state]) 1915 | n => 1916 Thm (deriv_rule1 (Proofterm.assumption_proof Bs Bi (n + 1)) der, 1917 {cert = cert, 1918 tags = [], 1919 maxidx = maxidx, 1920 constraints = constraints, 1921 shyps = shyps, 1922 hyps = hyps, 1923 tpairs = tpairs, 1924 prop = Logic.list_implies (Bs, C)})) 1925 end; 1926 1927 1928(*For rotate_tac: fast rotation of assumptions of subgoal i*) 1929fun rotate_rule k i state = 1930 let 1931 val Thm (der, {cert, maxidx, constraints, shyps, hyps, ...}) = state; 1932 val (tpairs, Bs, Bi, C) = dest_state (state, i); 1933 val params = Term.strip_all_vars Bi; 1934 val rest = Term.strip_all_body Bi; 1935 val asms = Logic.strip_imp_prems rest 1936 val concl = Logic.strip_imp_concl rest; 1937 val n = length asms; 1938 val m = if k < 0 then n + k else k; 1939 val Bi' = 1940 if 0 = m orelse m = n then Bi 1941 else if 0 < m andalso m < n then 1942 let val (ps, qs) = chop m asms 1943 in Logic.list_all (params, Logic.list_implies (qs @ ps, concl)) end 1944 else raise THM ("rotate_rule", k, [state]); 1945 in 1946 Thm (deriv_rule1 (Proofterm.rotate_proof Bs Bi' params asms m) der, 1947 {cert = cert, 1948 tags = [], 1949 maxidx = maxidx, 1950 constraints = constraints, 1951 shyps = shyps, 1952 hyps = hyps, 1953 tpairs = tpairs, 1954 prop = Logic.list_implies (Bs @ [Bi'], C)}) 1955 end; 1956 1957 1958(*Rotates a rule's premises to the left by k, leaving the first j premises 1959 unchanged. Does nothing if k=0 or if k equals n-j, where n is the 1960 number of premises. Useful with eresolve_tac and underlies defer_tac*) 1961fun permute_prems j k rl = 1962 let 1963 val Thm (der, {cert, maxidx, constraints, shyps, hyps, tpairs, prop, ...}) = rl; 1964 val prems = Logic.strip_imp_prems prop 1965 and concl = Logic.strip_imp_concl prop; 1966 val moved_prems = List.drop (prems, j) 1967 and fixed_prems = List.take (prems, j) 1968 handle General.Subscript => raise THM ("permute_prems: j", j, [rl]); 1969 val n_j = length moved_prems; 1970 val m = if k < 0 then n_j + k else k; 1971 val (prems', prop') = 1972 if 0 = m orelse m = n_j then (prems, prop) 1973 else if 0 < m andalso m < n_j then 1974 let 1975 val (ps, qs) = chop m moved_prems; 1976 val prems' = fixed_prems @ qs @ ps; 1977 in (prems', Logic.list_implies (prems', concl)) end 1978 else raise THM ("permute_prems: k", k, [rl]); 1979 in 1980 Thm (deriv_rule1 (Proofterm.permute_prems_proof prems' j m) der, 1981 {cert = cert, 1982 tags = [], 1983 maxidx = maxidx, 1984 constraints = constraints, 1985 shyps = shyps, 1986 hyps = hyps, 1987 tpairs = tpairs, 1988 prop = prop'}) 1989 end; 1990 1991 1992(* strip_apply f B A strips off all assumptions/parameters from A 1993 introduced by lifting over B, and applies f to remaining part of A*) 1994fun strip_apply f = 1995 let fun strip (Const ("Pure.imp", _) $ _ $ B1) 1996 (Const ("Pure.imp", _) $ A2 $ B2) = Logic.mk_implies (A2, strip B1 B2) 1997 | strip ((c as Const ("Pure.all", _)) $ Abs (_, _, t1)) 1998 ( Const ("Pure.all", _) $ Abs (a, T, t2)) = c $ Abs (a, T, strip t1 t2) 1999 | strip _ A = f A 2000 in strip end; 2001 2002fun strip_lifted (Const ("Pure.imp", _) $ _ $ B1) 2003 (Const ("Pure.imp", _) $ _ $ B2) = strip_lifted B1 B2 2004 | strip_lifted (Const ("Pure.all", _) $ Abs (_, _, t1)) 2005 (Const ("Pure.all", _) $ Abs (_, _, t2)) = strip_lifted t1 t2 2006 | strip_lifted _ A = A; 2007 2008(*Use the alist to rename all bound variables and some unknowns in a term 2009 dpairs = current disagreement pairs; tpairs = permanent ones (flexflex); 2010 Preserves unknowns in tpairs and on lhs of dpairs. *) 2011fun rename_bvs [] _ _ _ _ = K I 2012 | rename_bvs al dpairs tpairs B As = 2013 let 2014 val add_var = fold_aterms (fn Var ((x, _), _) => insert (op =) x | _ => I); 2015 val vids = [] 2016 |> fold (add_var o fst) dpairs 2017 |> fold (add_var o fst) tpairs 2018 |> fold (add_var o snd) tpairs; 2019 val vids' = fold (add_var o strip_lifted B) As []; 2020 (*unknowns appearing elsewhere be preserved!*) 2021 val al' = distinct ((op =) o apply2 fst) 2022 (filter_out (fn (x, y) => 2023 not (member (op =) vids' x) orelse 2024 member (op =) vids x orelse member (op =) vids y) al); 2025 val unchanged = filter_out (AList.defined (op =) al') vids'; 2026 fun del_clashing clash xs _ [] qs = 2027 if clash then del_clashing false xs xs qs [] else qs 2028 | del_clashing clash xs ys ((p as (x, y)) :: ps) qs = 2029 if member (op =) ys y 2030 then del_clashing true (x :: xs) (x :: ys) ps qs 2031 else del_clashing clash xs (y :: ys) ps (p :: qs); 2032 val al'' = del_clashing false unchanged unchanged al' []; 2033 fun rename (t as Var ((x, i), T)) = 2034 (case AList.lookup (op =) al'' x of 2035 SOME y => Var ((y, i), T) 2036 | NONE => t) 2037 | rename (Abs (x, T, t)) = 2038 Abs (the_default x (AList.lookup (op =) al x), T, rename t) 2039 | rename (f $ t) = rename f $ rename t 2040 | rename t = t; 2041 fun strip_ren f Ai = f rename B Ai 2042 in strip_ren end; 2043 2044(*Function to rename bounds/unknowns in the argument, lifted over B*) 2045fun rename_bvars dpairs = 2046 rename_bvs (fold_rev Term.match_bvars dpairs []) dpairs; 2047 2048 2049 2050(*** RESOLUTION ***) 2051 2052(** Lifting optimizations **) 2053 2054(*strip off pairs of assumptions/parameters in parallel -- they are 2055 identical because of lifting*) 2056fun strip_assums2 (Const("Pure.imp", _) $ _ $ B1, 2057 Const("Pure.imp", _) $ _ $ B2) = strip_assums2 (B1,B2) 2058 | strip_assums2 (Const("Pure.all",_)$Abs(a,T,t1), 2059 Const("Pure.all",_)$Abs(_,_,t2)) = 2060 let val (B1,B2) = strip_assums2 (t1,t2) 2061 in (Abs(a,T,B1), Abs(a,T,B2)) end 2062 | strip_assums2 BB = BB; 2063 2064 2065(*Faster normalization: skip assumptions that were lifted over*) 2066fun norm_term_skip env 0 t = Envir.norm_term env t 2067 | norm_term_skip env n (Const ("Pure.all", _) $ Abs (a, T, t)) = 2068 let 2069 val T' = Envir.norm_type (Envir.type_env env) T 2070 (*Must instantiate types of parameters because they are flattened; 2071 this could be a NEW parameter*) 2072 in Logic.all_const T' $ Abs (a, T', norm_term_skip env n t) end 2073 | norm_term_skip env n (Const ("Pure.imp", _) $ A $ B) = 2074 Logic.mk_implies (A, norm_term_skip env (n - 1) B) 2075 | norm_term_skip _ _ _ = error "norm_term_skip: too few assumptions??"; 2076 2077 2078(*unify types of schematic variables (non-lifted case)*) 2079fun unify_var_types context (th1, th2) env = 2080 let 2081 fun unify_vars (T :: Us) = fold (fn U => Pattern.unify_types context (T, U)) Us 2082 | unify_vars _ = I; 2083 val add_vars = 2084 full_prop_of #> 2085 fold_aterms (fn Var v => Vartab.insert_list (op =) v | _ => I); 2086 val vars = Vartab.empty |> add_vars th1 |> add_vars th2; 2087 in SOME (Vartab.fold (unify_vars o #2) vars env) end 2088 handle Pattern.Unif => NONE; 2089 2090(*Composition of object rule r=(A1...Am/B) with proof state s=(B1...Bn/C) 2091 Unifies B with Bi, replacing subgoal i (1 <= i <= n) 2092 If match then forbid instantiations in proof state 2093 If lifted then shorten the dpair using strip_assums2. 2094 If eres_flg then simultaneously proves A1 by assumption. 2095 nsubgoal is the number of new subgoals (written m above). 2096 Curried so that resolution calls dest_state only once. 2097*) 2098local exception COMPOSE 2099in 2100fun bicompose_aux opt_ctxt {flatten, match, incremented} (state, (stpairs, Bs, Bi, C), lifted) 2101 (eres_flg, orule, nsubgoal) = 2102 let val Thm (sder, {maxidx=smax, constraints = constraints2, shyps = shyps2, hyps = hyps2, ...}) = state 2103 and Thm (rder, {maxidx=rmax, constraints = constraints1, shyps = shyps1, hyps = hyps1, 2104 tpairs=rtpairs, prop=rprop,...}) = orule 2105 (*How many hyps to skip over during normalization*) 2106 and nlift = Logic.count_prems (strip_all_body Bi) + (if eres_flg then ~1 else 0) 2107 val (context, cert) = 2108 make_context_certificate [state, orule] opt_ctxt (join_certificate2 (state, orule)); 2109 (*Add new theorem with prop = "\<lbrakk>Bs; As\<rbrakk> \<Longrightarrow> C" to thq*) 2110 fun addth A (As, oldAs, rder', n) ((env, tpairs), thq) = 2111 let val normt = Envir.norm_term env; 2112 (*perform minimal copying here by examining env*) 2113 val (ntpairs, normp) = 2114 if Envir.is_empty env then (tpairs, (Bs @ As, C)) 2115 else 2116 let val ntps = map (apply2 normt) tpairs 2117 in if Envir.above env smax then 2118 (*no assignments in state; normalize the rule only*) 2119 if lifted 2120 then (ntps, (Bs @ map (norm_term_skip env nlift) As, C)) 2121 else (ntps, (Bs @ map normt As, C)) 2122 else if match then raise COMPOSE 2123 else (*normalize the new rule fully*) 2124 (ntps, (map normt (Bs @ As), normt C)) 2125 end 2126 val constraints' = 2127 union_constraints constraints1 constraints2 2128 |> insert_constraints_env (Context.certificate_theory cert) env; 2129 fun bicompose_proof prf1 prf2 = 2130 Proofterm.bicompose_proof flatten (map normt Bs) (map normt As) A oldAs n (nlift+1) 2131 prf1 prf2 2132 val th = 2133 Thm (deriv_rule2 2134 (if Envir.is_empty env then bicompose_proof 2135 else if Envir.above env smax then bicompose_proof o Proofterm.norm_proof' env 2136 else Proofterm.norm_proof' env oo bicompose_proof) rder' sder, 2137 {tags = [], 2138 maxidx = Envir.maxidx_of env, 2139 constraints = constraints', 2140 shyps = Envir.insert_sorts env (Sorts.union shyps1 shyps2), 2141 hyps = union_hyps hyps1 hyps2, 2142 tpairs = ntpairs, 2143 prop = Logic.list_implies normp, 2144 cert = cert}) 2145 in Seq.cons th thq end handle COMPOSE => thq; 2146 val (rAs,B) = Logic.strip_prems(nsubgoal, [], rprop) 2147 handle TERM _ => raise THM("bicompose: rule", 0, [orule,state]); 2148 (*Modify assumptions, deleting n-th if n>0 for e-resolution*) 2149 fun newAs(As0, n, dpairs, tpairs) = 2150 let val (As1, rder') = 2151 if not lifted then (As0, rder) 2152 else 2153 let val rename = rename_bvars dpairs tpairs B As0 2154 in (map (rename strip_apply) As0, 2155 deriv_rule1 (Proofterm.map_proof_terms (rename K) I) rder) 2156 end; 2157 in (map (if flatten then (Logic.flatten_params n) else I) As1, As1, rder', n) 2158 handle TERM _ => 2159 raise THM("bicompose: 1st premise", 0, [orule]) 2160 end; 2161 val BBi = if lifted then strip_assums2(B,Bi) else (B,Bi); 2162 val dpairs = BBi :: (rtpairs@stpairs); 2163 2164 (*elim-resolution: try each assumption in turn*) 2165 fun eres _ [] = raise THM ("bicompose: no premises", 0, [orule, state]) 2166 | eres env (A1 :: As) = 2167 let 2168 val A = SOME A1; 2169 val (close, asms, concl) = Logic.assum_problems (nlift + 1, A1); 2170 val concl' = close concl; 2171 fun tryasms [] _ = Seq.empty 2172 | tryasms (asm :: rest) n = 2173 if Term.could_unify (asm, concl) then 2174 let val asm' = close asm in 2175 (case Seq.pull (Unify.unifiers (context, env, (asm', concl') :: dpairs)) of 2176 NONE => tryasms rest (n + 1) 2177 | cell as SOME ((_, tpairs), _) => 2178 Seq.it_right (addth A (newAs (As, n, [BBi, (concl', asm')], tpairs))) 2179 (Seq.make (fn () => cell), 2180 Seq.make (fn () => Seq.pull (tryasms rest (n + 1))))) 2181 end 2182 else tryasms rest (n + 1); 2183 in tryasms asms 1 end; 2184 2185 (*ordinary resolution*) 2186 fun res env = 2187 (case Seq.pull (Unify.unifiers (context, env, dpairs)) of 2188 NONE => Seq.empty 2189 | cell as SOME ((_, tpairs), _) => 2190 Seq.it_right (addth NONE (newAs (rev rAs, 0, [BBi], tpairs))) 2191 (Seq.make (fn () => cell), Seq.empty)); 2192 2193 val env0 = Envir.empty (Int.max (rmax, smax)); 2194 in 2195 (case if incremented then SOME env0 else unify_var_types context (state, orule) env0 of 2196 NONE => Seq.empty 2197 | SOME env => if eres_flg then eres env (rev rAs) else res env) 2198 end; 2199end; 2200 2201fun bicompose opt_ctxt flags arg i state = 2202 bicompose_aux opt_ctxt flags (state, dest_state (state,i), false) arg; 2203 2204(*Quick test whether rule is resolvable with the subgoal with hyps Hs 2205 and conclusion B. If eres_flg then checks 1st premise of rule also*) 2206fun could_bires (Hs, B, eres_flg, rule) = 2207 let fun could_reshyp (A1::_) = exists (fn H => Term.could_unify (A1, H)) Hs 2208 | could_reshyp [] = false; (*no premise -- illegal*) 2209 in Term.could_unify(concl_of rule, B) andalso 2210 (not eres_flg orelse could_reshyp (prems_of rule)) 2211 end; 2212 2213(*Bi-resolution of a state with a list of (flag,rule) pairs. 2214 Puts the rule above: rule/state. Renames vars in the rules. *) 2215fun biresolution opt_ctxt match brules i state = 2216 let val (stpairs, Bs, Bi, C) = dest_state(state,i); 2217 val lift = lift_rule (cprem_of state i); 2218 val B = Logic.strip_assums_concl Bi; 2219 val Hs = Logic.strip_assums_hyp Bi; 2220 val compose = 2221 bicompose_aux opt_ctxt {flatten = true, match = match, incremented = true} 2222 (state, (stpairs, Bs, Bi, C), true); 2223 fun res [] = Seq.empty 2224 | res ((eres_flg, rule)::brules) = 2225 if Config.get_generic (make_context [state] opt_ctxt (cert_of state)) 2226 Pattern.unify_trace_failure orelse could_bires (Hs, B, eres_flg, rule) 2227 then Seq.make (*delay processing remainder till needed*) 2228 (fn()=> SOME(compose (eres_flg, lift rule, nprems_of rule), 2229 res brules)) 2230 else res brules 2231 in Seq.flat (res brules) end; 2232 2233(*Resolution: exactly one resolvent must be produced*) 2234fun tha RSN (i, thb) = 2235 (case Seq.chop 2 (biresolution NONE false [(false, tha)] i thb) of 2236 ([th], _) => solve_constraints th 2237 | ([], _) => raise THM ("RSN: no unifiers", i, [tha, thb]) 2238 | _ => raise THM ("RSN: multiple unifiers", i, [tha, thb])); 2239 2240(*Resolution: P \<Longrightarrow> Q, Q \<Longrightarrow> R gives P \<Longrightarrow> R*) 2241fun tha RS thb = tha RSN (1,thb); 2242 2243 2244 2245(**** Type classes ****) 2246 2247fun standard_tvars thm = 2248 let 2249 val thy = theory_of_thm thm; 2250 val tvars = rev (Term.add_tvars (prop_of thm) []); 2251 val names = Name.invent Name.context Name.aT (length tvars); 2252 val tinst = 2253 map2 (fn (ai, S) => fn b => ((ai, S), global_ctyp_of thy (TVar ((b, 0), S)))) tvars names; 2254 in instantiate (tinst, []) thm end 2255 2256 2257(* class relations *) 2258 2259val is_classrel = Symreltab.defined o get_classrels; 2260 2261fun complete_classrels thy = 2262 let 2263 fun complete (c, (_, (all_preds, all_succs))) (finished1, thy1) = 2264 let 2265 fun compl c1 c2 (finished2, thy2) = 2266 if is_classrel thy2 (c1, c2) then (finished2, thy2) 2267 else 2268 (false, 2269 thy2 2270 |> (map_classrels o Symreltab.update) ((c1, c2), 2271 (the_classrel thy2 (c1, c) RS the_classrel thy2 (c, c2)) 2272 |> standard_tvars 2273 |> close_derivation \<^here> 2274 |> tap (expose_proof thy2) 2275 |> trim_context)); 2276 2277 val proven = is_classrel thy1; 2278 val preds = Graph.Keys.fold (fn c1 => proven (c1, c) ? cons c1) all_preds []; 2279 val succs = Graph.Keys.fold (fn c2 => proven (c, c2) ? cons c2) all_succs []; 2280 in 2281 fold_product compl preds succs (finished1, thy1) 2282 end; 2283 in 2284 (case Graph.fold complete (Sorts.classes_of (Sign.classes_of thy)) (true, thy) of 2285 (true, _) => NONE 2286 | (_, thy') => SOME thy') 2287 end; 2288 2289 2290(* type arities *) 2291 2292fun thynames_of_arity thy (a, c) = 2293 (get_arities thy, []) |-> Aritytab.fold 2294 (fn ((a', _, c'), (_, name, ser)) => (a = a' andalso c = c') ? cons (name, ser)) 2295 |> sort (int_ord o apply2 #2) |> map #1; 2296 2297fun insert_arity_completions thy ((t, Ss, c), (th, thy_name, ser)) (finished, arities) = 2298 let 2299 val completions = 2300 Sign.super_classes thy c |> map_filter (fn c1 => 2301 if Aritytab.defined arities (t, Ss, c1) then NONE 2302 else 2303 let 2304 val th1 = 2305 (th RS the_classrel thy (c, c1)) 2306 |> standard_tvars 2307 |> close_derivation \<^here> 2308 |> tap (expose_proof thy) 2309 |> trim_context; 2310 in SOME ((t, Ss, c1), (th1, thy_name, ser)) end); 2311 val finished' = finished andalso null completions; 2312 val arities' = fold Aritytab.update completions arities; 2313 in (finished', arities') end; 2314 2315fun complete_arities thy = 2316 let 2317 val arities = get_arities thy; 2318 val (finished, arities') = 2319 Aritytab.fold (insert_arity_completions thy) arities (true, get_arities thy); 2320 in 2321 if finished then NONE 2322 else SOME (map_arities (K arities') thy) 2323 end; 2324 2325val _ = 2326 Theory.setup 2327 (Theory.at_begin complete_classrels #> 2328 Theory.at_begin complete_arities); 2329 2330 2331(* primitive rules *) 2332 2333fun add_classrel raw_th thy = 2334 let 2335 val th = strip_shyps (transfer thy raw_th); 2336 val th' = th |> unconstrainT |> tap (expose_proof thy) |> trim_context; 2337 val prop = plain_prop_of th; 2338 val (c1, c2) = Logic.dest_classrel prop; 2339 in 2340 thy 2341 |> Sign.primitive_classrel (c1, c2) 2342 |> map_classrels (Symreltab.update ((c1, c2), th')) 2343 |> perhaps complete_classrels 2344 |> perhaps complete_arities 2345 end; 2346 2347fun add_arity raw_th thy = 2348 let 2349 val th = strip_shyps (transfer thy raw_th); 2350 val th' = th |> unconstrainT |> tap (expose_proof thy) |> trim_context; 2351 val prop = plain_prop_of th; 2352 val (t, Ss, c) = Logic.dest_arity prop; 2353 val ar = ((t, Ss, c), (th', Context.theory_name thy, serial ())); 2354 in 2355 thy 2356 |> Sign.primitive_arity (t, Ss, [c]) 2357 |> map_arities (Aritytab.update ar #> curry (insert_arity_completions thy ar) true #> #2) 2358 end; 2359 2360end; 2361 2362structure Basic_Thm: BASIC_THM = Thm; 2363open Basic_Thm; 2364