1(* Title: Pure/logic.ML 2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 3 Author: Makarius 4 5Abstract syntax operations of the Pure meta-logic. 6*) 7 8signature LOGIC = 9sig 10 val all_const: typ -> term 11 val all: term -> term -> term 12 val dependent_all_name: string * term -> term -> term 13 val is_all: term -> bool 14 val dest_all: term -> (string * typ) * term 15 val list_all: (string * typ) list * term -> term 16 val all_constraint: (string -> typ option) -> string * string -> term -> term 17 val dependent_all_constraint: (string -> typ option) -> string * string -> term -> term 18 val mk_equals: term * term -> term 19 val dest_equals: term -> term * term 20 val implies: term 21 val mk_implies: term * term -> term 22 val dest_implies: term -> term * term 23 val list_implies: term list * term -> term 24 val strip_imp_prems: term -> term list 25 val strip_imp_concl: term -> term 26 val strip_prems: int * term list * term -> term list * term 27 val count_prems: term -> int 28 val nth_prem: int * term -> term 29 val close_term: (string * term) list -> term -> term 30 val close_prop: (string * term) list -> term list -> term -> term 31 val close_prop_constraint: (string -> typ option) -> 32 (string * string) list -> term list -> term -> term 33 val true_prop: term 34 val conjunction: term 35 val mk_conjunction: term * term -> term 36 val mk_conjunction_list: term list -> term 37 val mk_conjunction_balanced: term list -> term 38 val dest_conjunction: term -> term * term 39 val dest_conjunction_list: term -> term list 40 val dest_conjunction_balanced: int -> term -> term list 41 val dest_conjunctions: term -> term list 42 val strip_horn: term -> term list * term 43 val mk_type: typ -> term 44 val dest_type: term -> typ 45 val type_map: (term -> term) -> typ -> typ 46 val const_of_class: class -> string 47 val class_of_const: string -> class 48 val mk_of_class: typ * class -> term 49 val dest_of_class: term -> typ * class 50 val mk_of_sort: typ * sort -> term list 51 val name_classrel: string * string -> string 52 val mk_classrel: class * class -> term 53 val dest_classrel: term -> class * class 54 val name_arities: arity -> string list 55 val name_arity: string * sort list * class -> string 56 val mk_arities: arity -> term list 57 val mk_arity: string * sort list * class -> term 58 val dest_arity: term -> string * sort list * class 59 val dummy_tfree: sort -> typ 60 type unconstrain_context = 61 {present_map: (typ * typ) list, 62 constraints_map: (sort * typ) list, 63 atyp_map: typ -> typ, 64 map_atyps: typ -> typ, 65 constraints: ((typ * class) * term) list, 66 outer_constraints: (typ * class) list}; 67 val unconstrainT: sort list -> term -> unconstrain_context * term 68 val protectC: term 69 val protect: term -> term 70 val unprotect: term -> term 71 val mk_term: term -> term 72 val dest_term: term -> term 73 val occs: term * term -> bool 74 val close_form: term -> term 75 val combound: term * int * int -> term 76 val rlist_abs: (string * typ) list * term -> term 77 val incr_tvar_same: int -> typ Same.operation 78 val incr_tvar: int -> typ -> typ 79 val incr_indexes_same: string list * typ list * int -> term Same.operation 80 val incr_indexes: string list * typ list * int -> term -> term 81 val lift_abs: int -> term -> term -> term 82 val lift_all: int -> term -> term -> term 83 val strip_assums_hyp: term -> term list 84 val strip_assums_concl: term -> term 85 val strip_params: term -> (string * typ) list 86 val has_meta_prems: term -> bool 87 val flatten_params: int -> term -> term 88 val list_rename_params: string list -> term -> term 89 val assum_pairs: int * term -> (term * term) list 90 val assum_problems: int * term -> (term -> term) * term list * term 91 val bad_schematic: indexname -> string 92 val bad_fixed: string -> string 93 val varifyT_global: typ -> typ 94 val unvarifyT_global: typ -> typ 95 val varify_types_global: term -> term 96 val unvarify_types_global: term -> term 97 val varify_global: term -> term 98 val unvarify_global: term -> term 99 val get_goal: term -> int -> term 100 val goal_params: term -> int -> term * term list 101 val prems_of_goal: term -> int -> term list 102 val concl_of_goal: term -> int -> term 103end; 104 105structure Logic : LOGIC = 106struct 107 108 109(*** Abstract syntax operations on the meta-connectives ***) 110 111(** all **) 112 113fun all_const T = Const ("Pure.all", (T --> propT) --> propT); 114 115fun all v t = all_const (Term.fastype_of v) $ lambda v t; 116 117fun dependent_all_name (x, v) t = 118 let 119 val x' = if x = "" then Term.term_name v else x; 120 val T = Term.fastype_of v; 121 val t' = Term.abstract_over (v, t); 122 in if Term.is_dependent t' then all_const T $ Abs (x', T, t') else t end; 123 124fun is_all (Const ("Pure.all", _) $ Abs _) = true 125 | is_all _ = false; 126 127fun dest_all (Const ("Pure.all", _) $ Abs (abs as (_, T, _))) = 128 let val (x, b) = Term.dest_abs abs (*potentially slow*) 129 in ((x, T), b) end 130 | dest_all t = raise TERM ("dest_all", [t]); 131 132fun list_all ([], t) = t 133 | list_all ((a, T) :: vars, t) = all_const T $ Abs (a, T, list_all (vars, t)); 134 135 136(* operations before type-inference *) 137 138local 139 140fun abs_body default_type z tm = 141 let 142 fun abs lev (Abs (x, T, b)) = Abs (x, T, abs (lev + 1) b) 143 | abs lev (t $ u) = abs lev t $ abs lev u 144 | abs lev (a as Free (x, T)) = 145 if x = z then 146 Type.constraint (the_default dummyT (default_type x)) 147 (Type.constraint T (Bound lev)) 148 else a 149 | abs _ a = a; 150 in abs 0 (Term.incr_boundvars 1 tm) end; 151 152in 153 154fun all_constraint default_type (y, z) t = 155 all_const dummyT $ Abs (y, dummyT, abs_body default_type z t); 156 157fun dependent_all_constraint default_type (y, z) t = 158 let val t' = abs_body default_type z t 159 in if Term.is_dependent t' then all_const dummyT $ Abs (y, dummyT, t') else t end; 160 161end; 162 163 164(** equality **) 165 166fun mk_equals (t, u) = 167 let val T = Term.fastype_of t 168 in Const ("Pure.eq", T --> T --> propT) $ t $ u end; 169 170fun dest_equals (Const ("Pure.eq", _) $ t $ u) = (t, u) 171 | dest_equals t = raise TERM ("dest_equals", [t]); 172 173 174 175(** implies **) 176 177val implies = Const ("Pure.imp", propT --> propT --> propT); 178 179fun mk_implies (A, B) = implies $ A $ B; 180 181fun dest_implies (Const ("Pure.imp", _) $ A $ B) = (A, B) 182 | dest_implies A = raise TERM ("dest_implies", [A]); 183 184 185(** nested implications **) 186 187(* [A1,...,An], B goes to A1\<Longrightarrow>...An\<Longrightarrow>B *) 188fun list_implies ([], B) = B 189 | list_implies (A::As, B) = implies $ A $ list_implies(As,B); 190 191(* A1\<Longrightarrow>...An\<Longrightarrow>B goes to [A1,...,An], where B is not an implication *) 192fun strip_imp_prems (Const("Pure.imp", _) $ A $ B) = A :: strip_imp_prems B 193 | strip_imp_prems _ = []; 194 195(* A1\<Longrightarrow>...An\<Longrightarrow>B goes to B, where B is not an implication *) 196fun strip_imp_concl (Const("Pure.imp", _) $ A $ B) = strip_imp_concl B 197 | strip_imp_concl A = A : term; 198 199(*Strip and return premises: (i, [], A1\<Longrightarrow>...Ai\<Longrightarrow>B) 200 goes to ([Ai, A(i-1),...,A1] , B) (REVERSED) 201 if i<0 or else i too big then raises TERM*) 202fun strip_prems (0, As, B) = (As, B) 203 | strip_prems (i, As, Const("Pure.imp", _) $ A $ B) = 204 strip_prems (i-1, A::As, B) 205 | strip_prems (_, As, A) = raise TERM("strip_prems", A::As); 206 207(*Count premises -- quicker than (length o strip_prems) *) 208fun count_prems (Const ("Pure.imp", _) $ _ $ B) = 1 + count_prems B 209 | count_prems _ = 0; 210 211(*Select Ai from A1\<Longrightarrow>...Ai\<Longrightarrow>B*) 212fun nth_prem (1, Const ("Pure.imp", _) $ A $ _) = A 213 | nth_prem (i, Const ("Pure.imp", _) $ _ $ B) = nth_prem (i - 1, B) 214 | nth_prem (_, A) = raise TERM ("nth_prem", [A]); 215 216(*strip a proof state (Horn clause): 217 B1 \<Longrightarrow> ... Bn \<Longrightarrow> C goes to ([B1, ..., Bn], C) *) 218fun strip_horn A = (strip_imp_prems A, strip_imp_concl A); 219 220 221(* close -- omit vacuous quantifiers *) 222 223val close_term = fold_rev Term.dependent_lambda_name; 224 225fun close_prop xs As B = 226 fold_rev dependent_all_name xs (list_implies (As, B)); 227 228fun close_prop_constraint default_type xs As B = 229 fold_rev (dependent_all_constraint default_type) xs (list_implies (As, B)); 230 231 232(** conjunction **) 233 234val true_prop = all_const propT $ Abs ("dummy", propT, mk_implies (Bound 0, Bound 0)); 235val conjunction = Const ("Pure.conjunction", propT --> propT --> propT); 236 237 238(*A &&& B*) 239fun mk_conjunction (A, B) = conjunction $ A $ B; 240 241(*A &&& B &&& C -- improper*) 242fun mk_conjunction_list [] = true_prop 243 | mk_conjunction_list ts = foldr1 mk_conjunction ts; 244 245(*(A &&& B) &&& (C &&& D) -- balanced*) 246fun mk_conjunction_balanced [] = true_prop 247 | mk_conjunction_balanced ts = Balanced_Tree.make mk_conjunction ts; 248 249 250(*A &&& B*) 251fun dest_conjunction (Const ("Pure.conjunction", _) $ A $ B) = (A, B) 252 | dest_conjunction t = raise TERM ("dest_conjunction", [t]); 253 254(*A &&& B &&& C -- improper*) 255fun dest_conjunction_list t = 256 (case try dest_conjunction t of 257 NONE => [t] 258 | SOME (A, B) => A :: dest_conjunction_list B); 259 260(*(A &&& B) &&& (C &&& D) -- balanced*) 261fun dest_conjunction_balanced 0 _ = [] 262 | dest_conjunction_balanced n t = Balanced_Tree.dest dest_conjunction n t; 263 264(*((A &&& B) &&& C) &&& D &&& E -- flat*) 265fun dest_conjunctions t = 266 (case try dest_conjunction t of 267 NONE => [t] 268 | SOME (A, B) => dest_conjunctions A @ dest_conjunctions B); 269 270 271 272(** types as terms **) 273 274fun mk_type ty = Const ("Pure.type", Term.itselfT ty); 275 276fun dest_type (Const ("Pure.type", Type ("itself", [ty]))) = ty 277 | dest_type t = raise TERM ("dest_type", [t]); 278 279fun type_map f = dest_type o f o mk_type; 280 281 282 283(** type classes **) 284 285(* const names *) 286 287val classN = "_class"; 288 289val const_of_class = suffix classN; 290 291fun class_of_const c = unsuffix classN c 292 handle Fail _ => raise TERM ("class_of_const: bad name " ^ quote c, []); 293 294 295(* class/sort membership *) 296 297fun mk_of_class (ty, c) = 298 Const (const_of_class c, Term.itselfT ty --> propT) $ mk_type ty; 299 300fun dest_of_class (Const (c_class, _) $ ty) = (dest_type ty, class_of_const c_class) 301 | dest_of_class t = raise TERM ("dest_of_class", [t]); 302 303fun mk_of_sort (ty, S) = map (fn c => mk_of_class (ty, c)) S; 304 305 306(* class relations *) 307 308fun name_classrel (c1, c2) = 309 Long_Name.base_name c1 ^ "_" ^ Long_Name.base_name c2; 310 311fun mk_classrel (c1, c2) = mk_of_class (Term.aT [c1], c2); 312 313fun dest_classrel tm = 314 (case dest_of_class tm of 315 (TVar (_, [c1]), c2) => (c1, c2) 316 | _ => raise TERM ("dest_classrel", [tm])); 317 318 319(* type arities *) 320 321fun name_arities (t, _, S) = 322 let val b = Long_Name.base_name t 323 in S |> map (fn c => Long_Name.base_name c ^ "_" ^ b) end; 324 325fun name_arity (t, dom, c) = hd (name_arities (t, dom, [c])); 326 327fun mk_arities (t, Ss, S) = 328 let val T = Type (t, ListPair.map TFree (Name.invent Name.context Name.aT (length Ss), Ss)) 329 in map (fn c => mk_of_class (T, c)) S end; 330 331fun mk_arity (t, Ss, c) = the_single (mk_arities (t, Ss, [c])); 332 333fun dest_arity tm = 334 let 335 fun err () = raise TERM ("dest_arity", [tm]); 336 337 val (ty, c) = dest_of_class tm; 338 val (t, tvars) = 339 (case ty of 340 Type (t, tys) => (t, map dest_TVar tys handle TYPE _ => err ()) 341 | _ => err ()); 342 val Ss = 343 if has_duplicates (eq_fst (op =)) tvars then err () 344 else map snd tvars; 345 in (t, Ss, c) end; 346 347 348(* internalized sort constraints *) 349 350fun dummy_tfree S = TFree ("'dummy", S); 351 352type unconstrain_context = 353 {present_map: (typ * typ) list, 354 constraints_map: (sort * typ) list, 355 atyp_map: typ -> typ, 356 map_atyps: typ -> typ, 357 constraints: ((typ * class) * term) list, 358 outer_constraints: (typ * class) list}; 359 360fun unconstrainT shyps prop = 361 let 362 val present = rev ((fold_types o fold_atyps_sorts) (insert (eq_fst op =)) prop []); 363 val extra = fold (Sorts.remove_sort o #2) present shyps; 364 365 val n = length present; 366 val (names1, names2) = Name.invent Name.context Name.aT (n + length extra) |> chop n; 367 368 val present_map = 369 map2 (fn (T, S) => fn a => (T, TVar ((a, 0), S))) present names1; 370 val constraints_map = 371 map2 (fn (_, S) => fn a => (S, TVar ((a, 0), S))) present names1 @ 372 map2 (fn S => fn a => (S, TVar ((a, 0), S))) extra names2; 373 374 fun atyp_map T = 375 (case AList.lookup (op =) present_map T of 376 SOME U => U 377 | NONE => 378 (case AList.lookup (op =) constraints_map (Type.sort_of_atyp T) of 379 SOME U => U 380 | NONE => raise TYPE ("Dangling type variable ", [T], [prop]))); 381 382 val map_atyps = Term.map_atyps (Type.strip_sorts o atyp_map); 383 384 val constraints = 385 constraints_map |> maps (fn (_, T as TVar (ai, S)) => 386 map (fn c => ((T, c), mk_of_class (TVar (ai, []), c))) S); 387 388 val outer_constraints = 389 maps (fn (T, S) => map (pair T) S) (present @ map (`dummy_tfree) extra); 390 391 val ucontext = 392 {present_map = present_map, 393 constraints_map = constraints_map, 394 atyp_map = atyp_map, 395 map_atyps = map_atyps, 396 constraints = constraints, 397 outer_constraints = outer_constraints}; 398 val prop' = prop 399 |> Term.map_types map_atyps 400 |> curry list_implies (map #2 constraints); 401 in (ucontext, prop') end; 402 403 404 405(** protected propositions and embedded terms **) 406 407val protectC = Const ("Pure.prop", propT --> propT); 408fun protect t = protectC $ t; 409 410fun unprotect (Const ("Pure.prop", _) $ t) = t 411 | unprotect t = raise TERM ("unprotect", [t]); 412 413 414fun mk_term t = Const ("Pure.term", Term.fastype_of t --> propT) $ t; 415 416fun dest_term (Const ("Pure.term", _) $ t) = t 417 | dest_term t = raise TERM ("dest_term", [t]); 418 419 420 421(*** Low-level term operations ***) 422 423(*Does t occur in u? Or is alpha-convertible to u? 424 The term t must contain no loose bound variables*) 425fun occs (t, u) = exists_subterm (fn s => t aconv s) u; 426 427(*Close up a formula over all free variables by quantification*) 428fun close_form A = fold (all o Free) (Term.add_frees A []) A; 429 430 431 432(*** Specialized operations for resolution... ***) 433 434(*computes t(Bound(n+k-1),...,Bound(n)) *) 435fun combound (t, n, k) = 436 if k>0 then combound (t,n+1,k-1) $ (Bound n) else t; 437 438(* ([xn,...,x1], t) goes to \<lambda>x1 ... xn. t *) 439fun rlist_abs ([], body) = body 440 | rlist_abs ((a,T)::pairs, body) = rlist_abs(pairs, Abs(a, T, body)); 441 442fun incr_tvar_same 0 = Same.same 443 | incr_tvar_same k = Term_Subst.map_atypsT_same 444 (fn TVar ((a, i), S) => TVar ((a, i + k), S) 445 | _ => raise Same.SAME); 446 447fun incr_tvar k T = incr_tvar_same k T handle Same.SAME => T; 448 449(*For all variables in the term, increment indexnames and lift over the Us 450 result is ?Gidx(B.(lev+n-1),...,B.lev) where lev is abstraction level *) 451fun incr_indexes_same ([], [], 0) = Same.same 452 | incr_indexes_same (fixed, Ts, k) = 453 let 454 val n = length Ts; 455 val incrT = incr_tvar_same k; 456 457 fun incr lev (Var ((x, i), T)) = 458 combound (Var ((x, i + k), Ts ---> Same.commit incrT T), lev, n) 459 | incr lev (Free (x, T)) = 460 if member (op =) fixed x then 461 combound (Free (x, Ts ---> Same.commit incrT T), lev, n) 462 else Free (x, incrT T) 463 | incr lev (Abs (x, T, body)) = 464 (Abs (x, incrT T, incr (lev + 1) body handle Same.SAME => body) 465 handle Same.SAME => Abs (x, T, incr (lev + 1) body)) 466 | incr lev (t $ u) = 467 (incr lev t $ (incr lev u handle Same.SAME => u) 468 handle Same.SAME => t $ incr lev u) 469 | incr _ (Const (c, T)) = Const (c, incrT T) 470 | incr _ (Bound _) = raise Same.SAME; 471 in incr 0 end; 472 473fun incr_indexes arg t = incr_indexes_same arg t handle Same.SAME => t; 474 475 476(* Lifting functions from subgoal and increment: 477 lift_abs operates on terms 478 lift_all operates on propositions *) 479 480fun lift_abs inc = 481 let 482 fun lift Ts (Const ("Pure.imp", _) $ _ $ B) t = lift Ts B t 483 | lift Ts (Const ("Pure.all", _) $ Abs (a, T, B)) t = Abs (a, T, lift (T :: Ts) B t) 484 | lift Ts _ t = incr_indexes ([], rev Ts, inc) t; 485 in lift [] end; 486 487fun lift_all inc = 488 let 489 fun lift Ts ((c as Const ("Pure.imp", _)) $ A $ B) t = c $ A $ lift Ts B t 490 | lift Ts ((c as Const ("Pure.all", _)) $ Abs (a, T, B)) t = c $ Abs (a, T, lift (T :: Ts) B t) 491 | lift Ts _ t = incr_indexes ([], rev Ts, inc) t; 492 in lift [] end; 493 494(*Strips assumptions in goal, yielding list of hypotheses. *) 495fun strip_assums_hyp B = 496 let 497 fun strip Hs (Const ("Pure.imp", _) $ H $ B) = strip (H :: Hs) B 498 | strip Hs (Const ("Pure.all", _) $ Abs (a, T, t)) = 499 strip (map (incr_boundvars 1) Hs) t 500 | strip Hs B = rev Hs 501 in strip [] B end; 502 503(*Strips assumptions in goal, yielding conclusion. *) 504fun strip_assums_concl (Const("Pure.imp", _) $ H $ B) = strip_assums_concl B 505 | strip_assums_concl (Const("Pure.all", _) $ Abs (a, T, t)) = strip_assums_concl t 506 | strip_assums_concl B = B; 507 508(*Make a list of all the parameters in a subgoal, even if nested*) 509fun strip_params (Const("Pure.imp", _) $ H $ B) = strip_params B 510 | strip_params (Const("Pure.all", _) $ Abs (a, T, t)) = (a, T) :: strip_params t 511 | strip_params B = []; 512 513(*test for nested meta connectives in prems*) 514val has_meta_prems = 515 let 516 fun is_meta (Const ("Pure.eq", _) $ _ $ _) = true 517 | is_meta (Const ("Pure.imp", _) $ _ $ _) = true 518 | is_meta (Const ("Pure.all", _) $ _) = true 519 | is_meta _ = false; 520 fun ex_meta (Const ("Pure.imp", _) $ A $ B) = is_meta A orelse ex_meta B 521 | ex_meta (Const ("Pure.all", _) $ Abs (_, _, B)) = ex_meta B 522 | ex_meta _ = false; 523 in ex_meta end; 524 525(*Removes the parameters from a subgoal and renumber bvars in hypotheses, 526 where j is the total number of parameters (precomputed) 527 If n>0 then deletes assumption n. *) 528fun remove_params j n A = 529 if j=0 andalso n<=0 then A (*nothing left to do...*) 530 else case A of 531 Const("Pure.imp", _) $ H $ B => 532 if n=1 then (remove_params j (n-1) B) 533 else implies $ (incr_boundvars j H) $ (remove_params j (n-1) B) 534 | Const("Pure.all",_)$Abs(a,T,t) => remove_params (j-1) n t 535 | _ => if n>0 then raise TERM("remove_params", [A]) 536 else A; 537 538(*Move all parameters to the front of the subgoal, renaming them apart; 539 if n>0 then deletes assumption n. *) 540fun flatten_params n A = 541 let val params = strip_params A; 542 val vars = ListPair.zip (Name.variant_list [] (map #1 params), 543 map #2 params) 544 in list_all (vars, remove_params (length vars) n A) end; 545 546(*Makes parameters in a goal have the names supplied by the list cs.*) 547fun list_rename_params cs (Const ("Pure.imp", _) $ A $ B) = 548 implies $ A $ list_rename_params cs B 549 | list_rename_params (c :: cs) ((a as Const ("Pure.all", _)) $ Abs (_, T, t)) = 550 a $ Abs (c, T, list_rename_params cs t) 551 | list_rename_params cs B = B; 552 553 554 555(*** Treatment of "assume", "erule", etc. ***) 556 557(*Strips assumptions in goal yielding 558 HS = [Hn,...,H1], params = [xm,...,x1], and B, 559 where x1...xm are the parameters. This version (21.1.2005) REQUIRES 560 the the parameters to be flattened, but it allows erule to work on 561 assumptions of the form \<And>x. phi. Any \<And> after the outermost string 562 will be regarded as belonging to the conclusion, and left untouched. 563 Used ONLY by assum_pairs. 564 Unless nasms<0, it can terminate the recursion early; that allows 565 erule to work on assumptions of the form P\<Longrightarrow>Q.*) 566fun strip_assums_imp (0, Hs, B) = (Hs, B) (*recursion terminated by nasms*) 567 | strip_assums_imp (nasms, Hs, Const("Pure.imp", _) $ H $ B) = 568 strip_assums_imp (nasms-1, H::Hs, B) 569 | strip_assums_imp (_, Hs, B) = (Hs, B); (*recursion terminated by B*) 570 571(*Strips OUTER parameters only.*) 572fun strip_assums_all (params, Const("Pure.all",_)$Abs(a,T,t)) = 573 strip_assums_all ((a,T)::params, t) 574 | strip_assums_all (params, B) = (params, B); 575 576(*Produces disagreement pairs, one for each assumption proof, in order. 577 A is the first premise of the lifted rule, and thus has the form 578 H1 \<Longrightarrow> ... Hk \<Longrightarrow> B and the pairs are (H1,B),...,(Hk,B). 579 nasms is the number of assumptions in the original subgoal, needed when B 580 has the form B1 \<Longrightarrow> B2: it stops B1 from being taken as an assumption. *) 581fun assum_pairs(nasms,A) = 582 let val (params, A') = strip_assums_all ([],A) 583 val (Hs,B) = strip_assums_imp (nasms,[],A') 584 fun abspar t = rlist_abs(params, t) 585 val D = abspar B 586 fun pairrev ([], pairs) = pairs 587 | pairrev (H::Hs, pairs) = pairrev(Hs, (abspar H, D) :: pairs) 588 in pairrev (Hs,[]) 589 end; 590 591fun assum_problems (nasms, A) = 592 let 593 val (params, A') = strip_assums_all ([], A) 594 val (Hs, B) = strip_assums_imp (nasms, [], A') 595 fun abspar t = rlist_abs (params, t) 596 in (abspar, rev Hs, B) end; 597 598 599(* global schematic variables *) 600 601fun bad_schematic xi = "Illegal schematic variable: " ^ quote (Term.string_of_vname xi); 602fun bad_fixed x = "Illegal fixed variable: " ^ quote x; 603 604fun varifyT_global_same ty = ty 605 |> Term_Subst.map_atypsT_same 606 (fn TFree (a, S) => TVar ((a, 0), S) 607 | TVar (ai, _) => raise TYPE (bad_schematic ai, [ty], [])); 608 609fun unvarifyT_global_same ty = ty 610 |> Term_Subst.map_atypsT_same 611 (fn TVar ((a, 0), S) => TFree (a, S) 612 | TVar (ai, _) => raise TYPE (bad_schematic ai, [ty], []) 613 | TFree (a, _) => raise TYPE (bad_fixed a, [ty], [])); 614 615val varifyT_global = Same.commit varifyT_global_same; 616val unvarifyT_global = Same.commit unvarifyT_global_same; 617 618fun varify_types_global tm = tm 619 |> Same.commit (Term_Subst.map_types_same varifyT_global_same) 620 handle TYPE (msg, _, _) => raise TERM (msg, [tm]); 621 622fun unvarify_types_global tm = tm 623 |> Same.commit (Term_Subst.map_types_same unvarifyT_global_same) 624 handle TYPE (msg, _, _) => raise TERM (msg, [tm]); 625 626fun varify_global tm = tm 627 |> Same.commit (Term_Subst.map_aterms_same 628 (fn Free (x, T) => Var ((x, 0), T) 629 | Var (xi, _) => raise TERM (bad_schematic xi, [tm]) 630 | _ => raise Same.SAME)) 631 |> varify_types_global; 632 633fun unvarify_global tm = tm 634 |> Same.commit (Term_Subst.map_aterms_same 635 (fn Var ((x, 0), T) => Free (x, T) 636 | Var (xi, _) => raise TERM (bad_schematic xi, [tm]) 637 | Free (x, _) => raise TERM (bad_fixed x, [tm]) 638 | _ => raise Same.SAME)) 639 |> unvarify_types_global; 640 641 642(* goal states *) 643 644fun get_goal st i = 645 nth_prem (i, st) handle TERM _ => 646 error ("Subgoal number " ^ string_of_int i ^ " out of range (a total of " ^ 647 string_of_int (count_prems st) ^ " subgoals)"); 648 649(*reverses parameters for substitution*) 650fun goal_params st i = 651 let val gi = get_goal st i 652 val rfrees = map Free (Term.rename_wrt_term gi (strip_params gi)) 653 in (gi, rfrees) end; 654 655fun concl_of_goal st i = 656 let val (gi, rfrees) = goal_params st i 657 val B = strip_assums_concl gi 658 in subst_bounds (rfrees, B) end; 659 660fun prems_of_goal st i = 661 let val (gi, rfrees) = goal_params st i 662 val As = strip_assums_hyp gi 663 in map (fn A => subst_bounds (rfrees, A)) As end; 664 665end; 666