1.1 --- a/src/Pure/thm.ML Fri Dec 13 17:37:42 1996 +0100
1.2 +++ b/src/Pure/thm.ML Fri Dec 13 17:38:17 1996 +0100
1.3 @@ -39,40 +39,40 @@
1.4
1.5 (*proof terms [must duplicate declaration as a specification]*)
1.6 datatype deriv_kind = MinDeriv | ThmDeriv | FullDeriv;
1.7 - val keep_derivs : deriv_kind ref
1.8 + val keep_derivs : deriv_kind ref
1.9 datatype rule =
1.10 - MinProof
1.11 + MinProof
1.12 | Oracle of theory * Sign.sg * exn
1.13 - | Axiom of theory * string
1.14 - | Theorem of string
1.15 - | Assume of cterm
1.16 - | Implies_intr of cterm
1.17 + | Axiom of theory * string
1.18 + | Theorem of string
1.19 + | Assume of cterm
1.20 + | Implies_intr of cterm
1.21 | Implies_intr_shyps
1.22 | Implies_intr_hyps
1.23 | Implies_elim
1.24 - | Forall_intr of cterm
1.25 - | Forall_elim of cterm
1.26 - | Reflexive of cterm
1.27 + | Forall_intr of cterm
1.28 + | Forall_elim of cterm
1.29 + | Reflexive of cterm
1.30 | Symmetric
1.31 | Transitive
1.32 - | Beta_conversion of cterm
1.33 + | Beta_conversion of cterm
1.34 | Extensional
1.35 - | Abstract_rule of string * cterm
1.36 + | Abstract_rule of string * cterm
1.37 | Combination
1.38 | Equal_intr
1.39 | Equal_elim
1.40 - | Trivial of cterm
1.41 - | Lift_rule of cterm * int
1.42 - | Assumption of int * Envir.env option
1.43 - | Instantiate of (indexname * ctyp) list * (cterm * cterm) list
1.44 - | Bicompose of bool * bool * int * int * Envir.env
1.45 - | Flexflex_rule of Envir.env
1.46 - | Class_triv of theory * class
1.47 + | Trivial of cterm
1.48 + | Lift_rule of cterm * int
1.49 + | Assumption of int * Envir.env option
1.50 + | Instantiate of (indexname * ctyp) list * (cterm * cterm) list
1.51 + | Bicompose of bool * bool * int * int * Envir.env
1.52 + | Flexflex_rule of Envir.env
1.53 + | Class_triv of theory * class
1.54 | VarifyT
1.55 | FreezeT
1.56 - | RewriteC of cterm
1.57 - | CongC of cterm
1.58 - | Rewrite_cterm of cterm
1.59 + | RewriteC of cterm
1.60 + | CongC of cterm
1.61 + | Rewrite_cterm of cterm
1.62 | Rename_params_rule of string list * int;
1.63
1.64 type deriv (* = rule mtree *)
1.65 @@ -81,11 +81,11 @@
1.66 type thm
1.67 exception THM of string * int * thm list
1.68 val rep_thm : thm -> {sign: Sign.sg, der: deriv, maxidx: int,
1.69 - shyps: sort list, hyps: term list,
1.70 - prop: term}
1.71 + shyps: sort list, hyps: term list,
1.72 + prop: term}
1.73 val crep_thm : thm -> {sign: Sign.sg, der: deriv, maxidx: int,
1.74 - shyps: sort list, hyps: cterm list,
1.75 - prop: cterm}
1.76 + shyps: sort list, hyps: cterm list,
1.77 + prop: cterm}
1.78 val stamps_of_thm : thm -> string ref list
1.79 val tpairs_of : thm -> (term * term) list
1.80 val prems_of : thm -> term list
1.81 @@ -152,7 +152,7 @@
1.82 val rewrite_cterm : bool * bool -> meta_simpset ->
1.83 (meta_simpset -> thm -> thm option) -> cterm -> thm
1.84
1.85 - val invoke_oracle : theory * Sign.sg * exn -> thm
1.86 + val invoke_oracle : theory * Sign.sg * exn -> thm
1.87 end;
1.88
1.89 structure Thm : THM =
1.90 @@ -248,7 +248,7 @@
1.91 Sign.infer_types sign types sorts used freeze (ts, T');
1.92 val ct = cterm_of sign t'
1.93 handle TYPE arg => error (Sign.exn_type_msg sign arg)
1.94 - | TERM (msg, _) => error msg;
1.95 + | TERM (msg, _) => error msg;
1.96 in (ct, tye) end;
1.97
1.98 fun read_cterm sign = #1 o read_def_cterm (sign, K None, K None) [] true;
1.99 @@ -260,14 +260,14 @@
1.100 let
1.101 val {tsig, syn, ...} = Sign.rep_sg sign
1.102 fun read (b,T) =
1.103 - case Syntax.read syn T b of
1.104 - [t] => t
1.105 - | _ => error("Error or ambiguity in parsing of " ^ b)
1.106 + case Syntax.read syn T b of
1.107 + [t] => t
1.108 + | _ => error("Error or ambiguity in parsing of " ^ b)
1.109 val (us,_) = Type.infer_types(tsig, Sign.const_type sign,
1.110 - K None, K None,
1.111 - [], true,
1.112 - map (Sign.certify_typ sign) Ts,
1.113 - ListPair.map read (bs,Ts))
1.114 + K None, K None,
1.115 + [], true,
1.116 + map (Sign.certify_typ sign) Ts,
1.117 + ListPair.map read (bs,Ts))
1.118 in map (cterm_of sign) us end
1.119 handle TYPE arg => error (Sign.exn_type_msg sign arg)
1.120 | TERM (msg, _) => error msg;
1.121 @@ -279,47 +279,47 @@
1.122 (*Names of rules in derivations. Includes logically trivial rules, if
1.123 executed in ML.*)
1.124 datatype rule =
1.125 - MinProof (*for building minimal proof terms*)
1.126 - | Oracle of theory * Sign.sg * exn (*oracles*)
1.127 + MinProof (*for building minimal proof terms*)
1.128 + | Oracle of theory * Sign.sg * exn (*oracles*)
1.129 (*Axioms/theorems*)
1.130 - | Axiom of theory * string
1.131 - | Theorem of string
1.132 + | Axiom of theory * string
1.133 + | Theorem of string
1.134 (*primitive inferences and compound versions of them*)
1.135 - | Assume of cterm
1.136 - | Implies_intr of cterm
1.137 + | Assume of cterm
1.138 + | Implies_intr of cterm
1.139 | Implies_intr_shyps
1.140 | Implies_intr_hyps
1.141 | Implies_elim
1.142 - | Forall_intr of cterm
1.143 - | Forall_elim of cterm
1.144 - | Reflexive of cterm
1.145 + | Forall_intr of cterm
1.146 + | Forall_elim of cterm
1.147 + | Reflexive of cterm
1.148 | Symmetric
1.149 | Transitive
1.150 - | Beta_conversion of cterm
1.151 + | Beta_conversion of cterm
1.152 | Extensional
1.153 - | Abstract_rule of string * cterm
1.154 + | Abstract_rule of string * cterm
1.155 | Combination
1.156 | Equal_intr
1.157 | Equal_elim
1.158 (*derived rules for tactical proof*)
1.159 - | Trivial of cterm
1.160 - (*For lift_rule, the proof state is not a premise.
1.161 - Use cterm instead of thm to avoid mutual recursion.*)
1.162 - | Lift_rule of cterm * int
1.163 - | Assumption of int * Envir.env option (*includes eq_assumption*)
1.164 - | Instantiate of (indexname * ctyp) list * (cterm * cterm) list
1.165 - | Bicompose of bool * bool * int * int * Envir.env
1.166 - | Flexflex_rule of Envir.env (*identifies unifier chosen*)
1.167 + | Trivial of cterm
1.168 + (*For lift_rule, the proof state is not a premise.
1.169 + Use cterm instead of thm to avoid mutual recursion.*)
1.170 + | Lift_rule of cterm * int
1.171 + | Assumption of int * Envir.env option (*includes eq_assumption*)
1.172 + | Instantiate of (indexname * ctyp) list * (cterm * cterm) list
1.173 + | Bicompose of bool * bool * int * int * Envir.env
1.174 + | Flexflex_rule of Envir.env (*identifies unifier chosen*)
1.175 (*other derived rules*)
1.176 - | Class_triv of theory * class (*derived rule????*)
1.177 + | Class_triv of theory * class (*derived rule????*)
1.178 | VarifyT
1.179 | FreezeT
1.180 (*for the simplifier*)
1.181 - | RewriteC of cterm
1.182 - | CongC of cterm
1.183 - | Rewrite_cterm of cterm
1.184 + | RewriteC of cterm
1.185 + | CongC of cterm
1.186 + | Rewrite_cterm of cterm
1.187 (*Logical identities, recorded since they are part of the proof process*)
1.188 - | Rename_params_rule of string list * int;
1.189 + | Rename_params_rule of string list * int;
1.190
1.191
1.192 type deriv = rule mtree;
1.193 @@ -334,15 +334,15 @@
1.194 fun squash_derivs [] = []
1.195 | squash_derivs (der::ders) =
1.196 (case der of
1.197 - Join (Oracle _, _) => der :: squash_derivs ders
1.198 - | Join (Theorem _, [der']) => if !keep_derivs=ThmDeriv
1.199 - then der :: squash_derivs ders
1.200 - else squash_derivs (der'::ders)
1.201 - | Join (Axiom _, _) => if !keep_derivs=ThmDeriv
1.202 - then der :: squash_derivs ders
1.203 - else squash_derivs ders
1.204 - | Join (_, []) => squash_derivs ders
1.205 - | _ => der :: squash_derivs ders);
1.206 + Join (Oracle _, _) => der :: squash_derivs ders
1.207 + | Join (Theorem _, [der']) => if !keep_derivs=ThmDeriv
1.208 + then der :: squash_derivs ders
1.209 + else squash_derivs (der'::ders)
1.210 + | Join (Axiom _, _) => if !keep_derivs=ThmDeriv
1.211 + then der :: squash_derivs ders
1.212 + else squash_derivs ders
1.213 + | Join (_, []) => squash_derivs ders
1.214 + | _ => der :: squash_derivs ders);
1.215
1.216
1.217 (*Ensure sharing of the most likely derivation, the empty one!*)
1.218 @@ -362,12 +362,12 @@
1.219 (*** Meta theorems ***)
1.220
1.221 datatype thm = Thm of
1.222 - {sign: Sign.sg, (*signature for hyps and prop*)
1.223 - der: deriv, (*derivation*)
1.224 - maxidx: int, (*maximum index of any Var or TVar*)
1.225 - shyps: sort list, (*sort hypotheses*)
1.226 - hyps: term list, (*hypotheses*)
1.227 - prop: term}; (*conclusion*)
1.228 + {sign: Sign.sg, (*signature for hyps and prop*)
1.229 + der: deriv, (*derivation*)
1.230 + maxidx: int, (*maximum index of any Var or TVar*)
1.231 + shyps: sort list, (*sort hypotheses*)
1.232 + hyps: term list, (*hypotheses*)
1.233 + prop: term}; (*conclusion*)
1.234
1.235 fun rep_thm (Thm args) = args;
1.236
1.237 @@ -463,9 +463,9 @@
1.238 add_thm_sorts (thm, add_typs_sorts (Ts, add_thms_shyps (thms, [])));
1.239 in
1.240 Thm {sign = sign,
1.241 - der = der, (*No new derivation, as other rules call this*)
1.242 - maxidx = maxidx,
1.243 - shyps = shyps, hyps = hyps, prop = prop}
1.244 + der = der, (*No new derivation, as other rules call this*)
1.245 + maxidx = maxidx,
1.246 + shyps = shyps, hyps = hyps, prop = prop}
1.247 end;
1.248
1.249
1.250 @@ -482,13 +482,13 @@
1.251 val shyps' = filter (fn S => mem_sort(S,sorts) orelse maybe_empty S) shyps;
1.252 in
1.253 Thm {sign = sign, der = der, maxidx = maxidx,
1.254 - shyps =
1.255 - (if eq_set_sort (shyps',sorts) orelse
1.256 - not (!force_strip_shyps) then shyps'
1.257 - else (* FIXME tmp *)
1.258 - (writeln ("WARNING Removed sort hypotheses: " ^
1.259 - commas (map Type.str_of_sort (shyps' \\ sorts)));
1.260 - writeln "WARNING Let's hope these sorts are non-empty!";
1.261 + shyps =
1.262 + (if eq_set_sort (shyps',sorts) orelse
1.263 + not (!force_strip_shyps) then shyps'
1.264 + else (* FIXME tmp *)
1.265 + (warning ("Removed sort hypotheses: " ^
1.266 + commas (map Type.str_of_sort (shyps' \\ sorts)));
1.267 + warning "Let's hope these sorts are non-empty!";
1.268 sorts)),
1.269 hyps = hyps,
1.270 prop = prop}
1.271 @@ -514,11 +514,11 @@
1.272 val sort_hyps = flat (map2 mk_insort (tfrees, xshyps));
1.273 in
1.274 Thm {sign = sign,
1.275 - der = infer_derivs (Implies_intr_shyps, [der]),
1.276 - maxidx = maxidx,
1.277 - shyps = shyps',
1.278 - hyps = hyps,
1.279 - prop = Logic.list_implies (sort_hyps, prop)}
1.280 + der = infer_derivs (Implies_intr_shyps, [der]),
1.281 + maxidx = maxidx,
1.282 + shyps = shyps',
1.283 + hyps = hyps,
1.284 + prop = Logic.list_implies (sort_hyps, prop)}
1.285 end);
1.286
1.287
1.288 @@ -529,16 +529,16 @@
1.289 let
1.290 fun get_ax [] = raise Match
1.291 | get_ax (thy :: thys) =
1.292 - let val {sign, new_axioms, parents, ...} = rep_theory thy
1.293 + let val {sign, new_axioms, parents, ...} = rep_theory thy
1.294 in case Symtab.lookup (new_axioms, name) of
1.295 - Some t => fix_shyps [] []
1.296 - (Thm {sign = sign,
1.297 - der = infer_derivs (Axiom(theory,name), []),
1.298 - maxidx = maxidx_of_term t,
1.299 - shyps = [],
1.300 - hyps = [],
1.301 - prop = t})
1.302 - | None => get_ax parents handle Match => get_ax thys
1.303 + Some t => fix_shyps [] []
1.304 + (Thm {sign = sign,
1.305 + der = infer_derivs (Axiom(theory,name), []),
1.306 + maxidx = maxidx_of_term t,
1.307 + shyps = [],
1.308 + hyps = [],
1.309 + prop = t})
1.310 + | None => get_ax parents handle Match => get_ax thys
1.311 end;
1.312 in
1.313 get_ax [theory] handle Match
1.314 @@ -554,22 +554,22 @@
1.315 (*Attach a label to a theorem to make proof objects more readable*)
1.316 fun name_thm (name, th as Thm {sign, der, maxidx, shyps, hyps, prop}) =
1.317 Thm {sign = sign,
1.318 - der = Join (Theorem name, [der]),
1.319 - maxidx = maxidx,
1.320 - shyps = shyps,
1.321 - hyps = hyps,
1.322 - prop = prop};
1.323 + der = Join (Theorem name, [der]),
1.324 + maxidx = maxidx,
1.325 + shyps = shyps,
1.326 + hyps = hyps,
1.327 + prop = prop};
1.328
1.329
1.330 (*Compression of theorems -- a separate rule, not integrated with the others,
1.331 as it could be slow.*)
1.332 fun compress (Thm {sign, der, maxidx, shyps, hyps, prop}) =
1.333 Thm {sign = sign,
1.334 - der = der, (*No derivation recorded!*)
1.335 - maxidx = maxidx,
1.336 - shyps = shyps,
1.337 - hyps = map Term.compress_term hyps,
1.338 - prop = Term.compress_term prop};
1.339 + der = der, (*No derivation recorded!*)
1.340 + maxidx = maxidx,
1.341 + shyps = shyps,
1.342 + hyps = map Term.compress_term hyps,
1.343 + prop = Term.compress_term prop};
1.344
1.345
1.346 (*** Meta rules ***)
1.347 @@ -580,11 +580,11 @@
1.348 fun nodup_Vars (thm as Thm{sign, der, maxidx, shyps, hyps, prop}) s =
1.349 (Sign.nodup_Vars prop;
1.350 Thm {sign = sign,
1.351 - der = der,
1.352 - maxidx = maxidx_of_term prop,
1.353 - shyps = shyps,
1.354 - hyps = hyps,
1.355 - prop = prop})
1.356 + der = der,
1.357 + maxidx = maxidx_of_term prop,
1.358 + shyps = shyps,
1.359 + hyps = hyps,
1.360 + prop = prop})
1.361 handle TYPE(msg,Ts,ts) => raise TYPE(s^": "^msg,Ts,ts);
1.362
1.363 (** 'primitive' rules **)
1.364 @@ -601,11 +601,11 @@
1.365 raise THM("assume: assumptions may not contain scheme variables",
1.366 maxidx, [])
1.367 else Thm{sign = sign,
1.368 - der = infer_derivs (Assume ct, []),
1.369 - maxidx = ~1,
1.370 - shyps = add_term_sorts(prop,[]),
1.371 - hyps = [prop],
1.372 - prop = prop}
1.373 + der = infer_derivs (Assume ct, []),
1.374 + maxidx = ~1,
1.375 + shyps = add_term_sorts(prop,[]),
1.376 + hyps = [prop],
1.377 + prop = prop}
1.378 end;
1.379
1.380 (*Implication introduction
1.381 @@ -619,11 +619,11 @@
1.382 raise THM("implies_intr: assumptions must have type prop", 0, [thB])
1.383 else fix_shyps [thB] []
1.384 (Thm{sign = Sign.merge (sign,signA),
1.385 - der = infer_derivs (Implies_intr cA, [der]),
1.386 - maxidx = Int.max(maxidxA, maxidx),
1.387 - shyps = [],
1.388 - hyps = disch(hyps,A),
1.389 - prop = implies$A$prop})
1.390 + der = infer_derivs (Implies_intr cA, [der]),
1.391 + maxidx = Int.max(maxidxA, maxidx),
1.392 + shyps = [],
1.393 + hyps = disch(hyps,A),
1.394 + prop = implies$A$prop})
1.395 handle TERM _ =>
1.396 raise THM("implies_intr: incompatible signatures", 0, [thB])
1.397 end;
1.398 @@ -643,11 +643,11 @@
1.399 if imp=implies andalso A aconv propA
1.400 then fix_shyps [thAB, thA] []
1.401 (Thm{sign= merge_thm_sgs(thAB,thA),
1.402 - der = infer_derivs (Implies_elim, [der,derA]),
1.403 - maxidx = Int.max(maxA,maxidx),
1.404 - shyps = [],
1.405 - hyps = union_term(hypsA,hyps), (*dups suppressed*)
1.406 - prop = B})
1.407 + der = infer_derivs (Implies_elim, [der,derA]),
1.408 + maxidx = Int.max(maxA,maxidx),
1.409 + shyps = [],
1.410 + hyps = union_term(hypsA,hyps), (*dups suppressed*)
1.411 + prop = B})
1.412 else err("major premise")
1.413 | _ => err("major premise")
1.414 end;
1.415 @@ -661,11 +661,11 @@
1.416 let val x = term_of cx;
1.417 fun result(a,T) = fix_shyps [th] []
1.418 (Thm{sign = sign,
1.419 - der = infer_derivs (Forall_intr cx, [der]),
1.420 - maxidx = maxidx,
1.421 - shyps = [],
1.422 - hyps = hyps,
1.423 - prop = all(T) $ Abs(a, T, abstract_over (x,prop))})
1.424 + der = infer_derivs (Forall_intr cx, [der]),
1.425 + maxidx = maxidx,
1.426 + shyps = [],
1.427 + hyps = hyps,
1.428 + prop = all(T) $ Abs(a, T, abstract_over (x,prop))})
1.429 in case x of
1.430 Free(a,T) =>
1.431 if exists (apl(x, Logic.occs)) hyps
1.432 @@ -683,20 +683,20 @@
1.433 fun forall_elim ct (th as Thm{sign,der,maxidx,hyps,prop,...}) : thm =
1.434 let val {sign=signt, t, T, maxidx=maxt} = rep_cterm ct
1.435 in case prop of
1.436 - Const("all",Type("fun",[Type("fun",[qary,_]),_])) $ A =>
1.437 - if T<>qary then
1.438 - raise THM("forall_elim: type mismatch", 0, [th])
1.439 - else let val thm = fix_shyps [th] []
1.440 - (Thm{sign= Sign.merge(sign,signt),
1.441 - der = infer_derivs (Forall_elim ct, [der]),
1.442 - maxidx = Int.max(maxidx, maxt),
1.443 - shyps = [],
1.444 - hyps = hyps,
1.445 - prop = betapply(A,t)})
1.446 - in if maxt >= 0 andalso maxidx >= 0
1.447 - then nodup_Vars thm "forall_elim"
1.448 - else thm (*no new Vars: no expensive check!*)
1.449 - end
1.450 + Const("all",Type("fun",[Type("fun",[qary,_]),_])) $ A =>
1.451 + if T<>qary then
1.452 + raise THM("forall_elim: type mismatch", 0, [th])
1.453 + else let val thm = fix_shyps [th] []
1.454 + (Thm{sign= Sign.merge(sign,signt),
1.455 + der = infer_derivs (Forall_elim ct, [der]),
1.456 + maxidx = Int.max(maxidx, maxt),
1.457 + shyps = [],
1.458 + hyps = hyps,
1.459 + prop = betapply(A,t)})
1.460 + in if maxt >= 0 andalso maxidx >= 0
1.461 + then nodup_Vars thm "forall_elim"
1.462 + else thm (*no new Vars: no expensive check!*)
1.463 + end
1.464 | _ => raise THM("forall_elim: not quantified", 0, [th])
1.465 end
1.466 handle TERM _ =>
1.467 @@ -713,18 +713,18 @@
1.468 hyps = [],
1.469 maxidx = 0,
1.470 prop = term_of (read_cterm Sign.proto_pure
1.471 - ("(?t =?= ?u) == (?t == ?u::?'a::{})", propT))});
1.472 + ("(?t =?= ?u) == (?t == ?u::?'a::{})", propT))});
1.473
1.474 (*The reflexivity rule: maps t to the theorem t==t *)
1.475 fun reflexive ct =
1.476 let val {sign, t, T, maxidx} = rep_cterm ct
1.477 in fix_shyps [] []
1.478 (Thm{sign= sign,
1.479 - der = infer_derivs (Reflexive ct, []),
1.480 - shyps = [],
1.481 - hyps = [],
1.482 - maxidx = maxidx,
1.483 - prop = Logic.mk_equals(t,t)})
1.484 + der = infer_derivs (Reflexive ct, []),
1.485 + shyps = [],
1.486 + hyps = [],
1.487 + maxidx = maxidx,
1.488 + prop = Logic.mk_equals(t,t)})
1.489 end;
1.490
1.491 (*The symmetry rule
1.492 @@ -736,12 +736,12 @@
1.493 case prop of
1.494 (eq as Const("==",_)) $ t $ u =>
1.495 (*no fix_shyps*)
1.496 - Thm{sign = sign,
1.497 - der = infer_derivs (Symmetric, [der]),
1.498 - maxidx = maxidx,
1.499 - shyps = shyps,
1.500 - hyps = hyps,
1.501 - prop = eq$u$t}
1.502 + Thm{sign = sign,
1.503 + der = infer_derivs (Symmetric, [der]),
1.504 + maxidx = maxidx,
1.505 + shyps = shyps,
1.506 + hyps = hyps,
1.507 + prop = eq$u$t}
1.508 | _ => raise THM("symmetric", 0, [th]);
1.509
1.510 (*The transitive rule
1.511 @@ -759,11 +759,11 @@
1.512 else let val thm =
1.513 fix_shyps [th1, th2] []
1.514 (Thm{sign= merge_thm_sgs(th1,th2),
1.515 - der = infer_derivs (Transitive, [der1, der2]),
1.516 + der = infer_derivs (Transitive, [der1, der2]),
1.517 maxidx = Int.max(max1,max2),
1.518 - shyps = [],
1.519 - hyps = union_term(hyps1,hyps2),
1.520 - prop = eq$t1$t2})
1.521 + shyps = [],
1.522 + hyps = union_term(hyps1,hyps2),
1.523 + prop = eq$t1$t2})
1.524 in if max1 >= 0 andalso max2 >= 0
1.525 then nodup_Vars thm "transitive"
1.526 else thm (*no new Vars: no expensive check!*)
1.527 @@ -777,11 +777,11 @@
1.528 in case t of
1.529 Abs(_,_,bodt) $ u => fix_shyps [] []
1.530 (Thm{sign = sign,
1.531 - der = infer_derivs (Beta_conversion ct, []),
1.532 - maxidx = maxidx,
1.533 - shyps = [],
1.534 - hyps = [],
1.535 - prop = Logic.mk_equals(t, subst_bound (u,bodt))})
1.536 + der = infer_derivs (Beta_conversion ct, []),
1.537 + maxidx = maxidx,
1.538 + shyps = [],
1.539 + hyps = [],
1.540 + prop = Logic.mk_equals(t, subst_bound (u,bodt))})
1.541 | _ => raise THM("beta_conversion: not a redex", 0, [])
1.542 end;
1.543
1.544 @@ -805,10 +805,10 @@
1.545 | _ => err"not a variable");
1.546 (*no fix_shyps*)
1.547 Thm{sign = sign,
1.548 - der = infer_derivs (Extensional, [der]),
1.549 - maxidx = maxidx,
1.550 - shyps = shyps,
1.551 - hyps = hyps,
1.552 + der = infer_derivs (Extensional, [der]),
1.553 + maxidx = maxidx,
1.554 + shyps = shyps,
1.555 + hyps = hyps,
1.556 prop = Logic.mk_equals(f,g)}
1.557 end
1.558 | _ => raise THM("extensional: premise", 0, [th]);
1.559 @@ -825,13 +825,13 @@
1.560 handle TERM _ =>
1.561 raise THM("abstract_rule: premise not an equality", 0, [th])
1.562 fun result T = fix_shyps [th] []
1.563 - (Thm{sign = sign,
1.564 - der = infer_derivs (Abstract_rule (a,cx), [der]),
1.565 - maxidx = maxidx,
1.566 - shyps = [],
1.567 - hyps = hyps,
1.568 - prop = Logic.mk_equals(Abs(a, T, abstract_over (x,t)),
1.569 - Abs(a, T, abstract_over (x,u)))})
1.570 + (Thm{sign = sign,
1.571 + der = infer_derivs (Abstract_rule (a,cx), [der]),
1.572 + maxidx = maxidx,
1.573 + shyps = [],
1.574 + hyps = hyps,
1.575 + prop = Logic.mk_equals(Abs(a, T, abstract_over (x,t)),
1.576 + Abs(a, T, abstract_over (x,u)))})
1.577 in case x of
1.578 Free(_,T) =>
1.579 if exists (apl(x, Logic.occs)) hyps
1.580 @@ -848,30 +848,30 @@
1.581 *)
1.582 fun combination th1 th2 =
1.583 let val Thm{der=der1, maxidx=max1, shyps=shyps1, hyps=hyps1,
1.584 - prop=prop1,...} = th1
1.585 + prop=prop1,...} = th1
1.586 and Thm{der=der2, maxidx=max2, shyps=shyps2, hyps=hyps2,
1.587 - prop=prop2,...} = th2
1.588 + prop=prop2,...} = th2
1.589 fun chktypes (f,t) =
1.590 - (case fastype_of f of
1.591 - Type("fun",[T1,T2]) =>
1.592 - if T1 <> fastype_of t then
1.593 - raise THM("combination: types", 0, [th1,th2])
1.594 - else ()
1.595 - | _ => raise THM("combination: not function type", 0,
1.596 - [th1,th2]))
1.597 + (case fastype_of f of
1.598 + Type("fun",[T1,T2]) =>
1.599 + if T1 <> fastype_of t then
1.600 + raise THM("combination: types", 0, [th1,th2])
1.601 + else ()
1.602 + | _ => raise THM("combination: not function type", 0,
1.603 + [th1,th2]))
1.604 in case (prop1,prop2) of
1.605 (Const("==",_) $ f $ g, Const("==",_) $ t $ u) =>
1.606 let val _ = chktypes (f,t)
1.607 - val thm = (*no fix_shyps*)
1.608 - Thm{sign = merge_thm_sgs(th1,th2),
1.609 - der = infer_derivs (Combination, [der1, der2]),
1.610 - maxidx = Int.max(max1,max2),
1.611 - shyps = union_sort(shyps1,shyps2),
1.612 - hyps = union_term(hyps1,hyps2),
1.613 - prop = Logic.mk_equals(f$t, g$u)}
1.614 + val thm = (*no fix_shyps*)
1.615 + Thm{sign = merge_thm_sgs(th1,th2),
1.616 + der = infer_derivs (Combination, [der1, der2]),
1.617 + maxidx = Int.max(max1,max2),
1.618 + shyps = union_sort(shyps1,shyps2),
1.619 + hyps = union_term(hyps1,hyps2),
1.620 + prop = Logic.mk_equals(f$t, g$u)}
1.621 in if max1 >= 0 andalso max2 >= 0
1.622 then nodup_Vars thm "combination"
1.623 - else thm (*no new Vars: no expensive check!*)
1.624 + else thm (*no new Vars: no expensive check!*)
1.625 end
1.626 | _ => raise THM("combination: premises", 0, [th1,th2])
1.627 end;
1.628 @@ -884,22 +884,22 @@
1.629 *)
1.630 fun equal_intr th1 th2 =
1.631 let val Thm{der=der1,maxidx=max1, shyps=shyps1, hyps=hyps1,
1.632 - prop=prop1,...} = th1
1.633 + prop=prop1,...} = th1
1.634 and Thm{der=der2, maxidx=max2, shyps=shyps2, hyps=hyps2,
1.635 - prop=prop2,...} = th2;
1.636 + prop=prop2,...} = th2;
1.637 fun err(msg) = raise THM("equal_intr: "^msg, 0, [th1,th2])
1.638 in case (prop1,prop2) of
1.639 (Const("==>",_) $ A $ B, Const("==>",_) $ B' $ A') =>
1.640 - if A aconv A' andalso B aconv B'
1.641 - then
1.642 - (*no fix_shyps*)
1.643 - Thm{sign = merge_thm_sgs(th1,th2),
1.644 - der = infer_derivs (Equal_intr, [der1, der2]),
1.645 - maxidx = Int.max(max1,max2),
1.646 - shyps = union_sort(shyps1,shyps2),
1.647 - hyps = union_term(hyps1,hyps2),
1.648 - prop = Logic.mk_equals(A,B)}
1.649 - else err"not equal"
1.650 + if A aconv A' andalso B aconv B'
1.651 + then
1.652 + (*no fix_shyps*)
1.653 + Thm{sign = merge_thm_sgs(th1,th2),
1.654 + der = infer_derivs (Equal_intr, [der1, der2]),
1.655 + maxidx = Int.max(max1,max2),
1.656 + shyps = union_sort(shyps1,shyps2),
1.657 + hyps = union_term(hyps1,hyps2),
1.658 + prop = Logic.mk_equals(A,B)}
1.659 + else err"not equal"
1.660 | _ => err"premises"
1.661 end;
1.662
1.663 @@ -918,11 +918,11 @@
1.664 if not (prop2 aconv A) then err"not equal" else
1.665 fix_shyps [th1, th2] []
1.666 (Thm{sign= merge_thm_sgs(th1,th2),
1.667 - der = infer_derivs (Equal_elim, [der1, der2]),
1.668 - maxidx = Int.max(max1,max2),
1.669 - shyps = [],
1.670 - hyps = union_term(hyps1,hyps2),
1.671 - prop = B})
1.672 + der = infer_derivs (Equal_elim, [der1, der2]),
1.673 + maxidx = Int.max(max1,max2),
1.674 + shyps = [],
1.675 + hyps = union_term(hyps1,hyps2),
1.676 + prop = B})
1.677 | _ => err"major premise"
1.678 end;
1.679
1.680 @@ -935,11 +935,11 @@
1.681 fun implies_intr_hyps (Thm{sign, der, maxidx, shyps, hyps=A::As, prop}) =
1.682 implies_intr_hyps (*no fix_shyps*)
1.683 (Thm{sign = sign,
1.684 - der = infer_derivs (Implies_intr_hyps, [der]),
1.685 - maxidx = maxidx,
1.686 - shyps = shyps,
1.687 + der = infer_derivs (Implies_intr_hyps, [der]),
1.688 + maxidx = maxidx,
1.689 + shyps = shyps,
1.690 hyps = disch(As,A),
1.691 - prop = implies$A$prop})
1.692 + prop = implies$A$prop})
1.693 | implies_intr_hyps th = th;
1.694
1.695 (*Smash" unifies the list of term pairs leaving no flex-flex pairs.
1.696 @@ -957,11 +957,11 @@
1.697 val newprop = Logic.list_flexpairs(distpairs, horn)
1.698 in fix_shyps [th] (env_codT env)
1.699 (Thm{sign = sign,
1.700 - der = infer_derivs (Flexflex_rule env, [der]),
1.701 - maxidx = maxidx_of_term newprop,
1.702 - shyps = [],
1.703 - hyps = hyps,
1.704 - prop = newprop})
1.705 + der = infer_derivs (Flexflex_rule env, [der]),
1.706 + maxidx = maxidx_of_term newprop,
1.707 + shyps = [],
1.708 + hyps = hyps,
1.709 + prop = newprop})
1.710 end;
1.711 val (tpairs,_) = Logic.strip_flexpairs prop
1.712 in Sequence.maps newthm
1.713 @@ -1003,11 +1003,11 @@
1.714 val newth =
1.715 fix_shyps [th] (map snd vTs)
1.716 (Thm{sign = newsign,
1.717 - der = infer_derivs (Instantiate(vcTs,ctpairs), [der]),
1.718 - maxidx = maxidx_of_term newprop,
1.719 - shyps = [],
1.720 - hyps = hyps,
1.721 - prop = newprop})
1.722 + der = infer_derivs (Instantiate(vcTs,ctpairs), [der]),
1.723 + maxidx = maxidx_of_term newprop,
1.724 + shyps = [],
1.725 + hyps = hyps,
1.726 + prop = newprop})
1.727 in if not(instl_ok(map #1 tpairs))
1.728 then raise THM("instantiate: variables not distinct", 0, [th])
1.729 else if not(null(findrep(map #1 vTs)))
1.730 @@ -1026,27 +1026,27 @@
1.731 raise THM("trivial: the term must have type prop", 0, [])
1.732 else fix_shyps [] []
1.733 (Thm{sign = sign,
1.734 - der = infer_derivs (Trivial ct, []),
1.735 - maxidx = maxidx,
1.736 - shyps = [],
1.737 - hyps = [],
1.738 - prop = implies$A$A})
1.739 + der = infer_derivs (Trivial ct, []),
1.740 + maxidx = maxidx,
1.741 + shyps = [],
1.742 + hyps = [],
1.743 + prop = implies$A$A})
1.744 end;
1.745
1.746 (*Axiom-scheme reflecting signature contents: "OFCLASS(?'a::c, c_class)" *)
1.747 fun class_triv thy c =
1.748 let val sign = sign_of thy;
1.749 val Cterm {t, maxidx, ...} =
1.750 - cterm_of sign (Logic.mk_inclass (TVar (("'a", 0), [c]), c))
1.751 - handle TERM (msg, _) => raise THM ("class_triv: " ^ msg, 0, []);
1.752 + cterm_of sign (Logic.mk_inclass (TVar (("'a", 0), [c]), c))
1.753 + handle TERM (msg, _) => raise THM ("class_triv: " ^ msg, 0, []);
1.754 in
1.755 fix_shyps [] []
1.756 (Thm {sign = sign,
1.757 - der = infer_derivs (Class_triv(thy,c), []),
1.758 - maxidx = maxidx,
1.759 - shyps = [],
1.760 - hyps = [],
1.761 - prop = t})
1.762 + der = infer_derivs (Class_triv(thy,c), []),
1.763 + maxidx = maxidx,
1.764 + shyps = [],
1.765 + hyps = [],
1.766 + prop = t})
1.767 end;
1.768
1.769
1.770 @@ -1055,10 +1055,10 @@
1.771 let val tfrees = foldr add_term_tfree_names (hyps,[])
1.772 in let val thm = (*no fix_shyps*)
1.773 Thm{sign = sign,
1.774 - der = infer_derivs (VarifyT, [der]),
1.775 - maxidx = Int.max(0,maxidx),
1.776 - shyps = shyps,
1.777 - hyps = hyps,
1.778 + der = infer_derivs (VarifyT, [der]),
1.779 + maxidx = Int.max(0,maxidx),
1.780 + shyps = shyps,
1.781 + hyps = hyps,
1.782 prop = Type.varify(prop,tfrees)}
1.783 in nodup_Vars thm "varifyT" end
1.784 (* this nodup_Vars check can be removed if thms are guaranteed not to contain
1.785 @@ -1070,10 +1070,10 @@
1.786 let val prop' = Type.freeze prop
1.787 in (*no fix_shyps*)
1.788 Thm{sign = sign,
1.789 - der = infer_derivs (FreezeT, [der]),
1.790 - maxidx = maxidx_of_term prop',
1.791 - shyps = shyps,
1.792 - hyps = hyps,
1.793 + der = infer_derivs (FreezeT, [der]),
1.794 + maxidx = maxidx_of_term prop',
1.795 + shyps = shyps,
1.796 + hyps = hyps,
1.797 prop = prop'}
1.798 end;
1.799
1.800 @@ -1101,13 +1101,13 @@
1.801 val (tpairs,As,B) = Logic.strip_horn prop
1.802 in (*no fix_shyps*)
1.803 Thm{sign = merge_thm_sgs(state,orule),
1.804 - der = infer_derivs (Lift_rule(ct_Bi, i), [der]),
1.805 - maxidx = maxidx+smax+1,
1.806 + der = infer_derivs (Lift_rule(ct_Bi, i), [der]),
1.807 + maxidx = maxidx+smax+1,
1.808 shyps=union_sort(sshyps,shyps),
1.809 - hyps=hyps,
1.810 + hyps=hyps,
1.811 prop = Logic.rule_of (map (pairself lift_abs) tpairs,
1.812 - map lift_all As,
1.813 - lift_all B)}
1.814 + map lift_all As,
1.815 + lift_all B)}
1.816 end;
1.817
1.818 (*Solve subgoal Bi of proof state B1...Bn/C by assumption. *)
1.819 @@ -1117,15 +1117,15 @@
1.820 fun newth (env as Envir.Envir{maxidx, ...}, tpairs) =
1.821 fix_shyps [state] (env_codT env)
1.822 (Thm{sign = sign,
1.823 - der = infer_derivs (Assumption (i, Some env), [der]),
1.824 - maxidx = maxidx,
1.825 - shyps = [],
1.826 - hyps = hyps,
1.827 - prop =
1.828 - if Envir.is_empty env then (*avoid wasted normalizations*)
1.829 - Logic.rule_of (tpairs, Bs, C)
1.830 - else (*normalize the new rule fully*)
1.831 - Envir.norm_term env (Logic.rule_of (tpairs, Bs, C))});
1.832 + der = infer_derivs (Assumption (i, Some env), [der]),
1.833 + maxidx = maxidx,
1.834 + shyps = [],
1.835 + hyps = hyps,
1.836 + prop =
1.837 + if Envir.is_empty env then (*avoid wasted normalizations*)
1.838 + Logic.rule_of (tpairs, Bs, C)
1.839 + else (*normalize the new rule fully*)
1.840 + Envir.norm_term env (Logic.rule_of (tpairs, Bs, C))});
1.841 fun addprfs [] = Sequence.null
1.842 | addprfs ((t,u)::apairs) = Sequence.seqof (fn()=> Sequence.pull
1.843 (Sequence.mapp newth
1.844 @@ -1141,11 +1141,11 @@
1.845 in if exists (op aconv) (Logic.assum_pairs Bi)
1.846 then fix_shyps [state] []
1.847 (Thm{sign = sign,
1.848 - der = infer_derivs (Assumption (i,None), [der]),
1.849 - maxidx = maxidx,
1.850 - shyps = [],
1.851 - hyps = hyps,
1.852 - prop = Logic.rule_of(tpairs, Bs, C)})
1.853 + der = infer_derivs (Assumption (i,None), [der]),
1.854 + maxidx = maxidx,
1.855 + shyps = [],
1.856 + hyps = hyps,
1.857 + prop = Logic.rule_of(tpairs, Bs, C)})
1.858 else raise THM("eq_assumption", 0, [state])
1.859 end;
1.860
1.861 @@ -1172,12 +1172,12 @@
1.862 | [] => (case cs inter_string freenames of
1.863 a::_ => error ("Bound/Free variable clash: " ^ a)
1.864 | [] => fix_shyps [state] []
1.865 - (Thm{sign = sign,
1.866 - der = infer_derivs (Rename_params_rule(cs,i), [der]),
1.867 - maxidx = maxidx,
1.868 - shyps = [],
1.869 - hyps = hyps,
1.870 - prop = Logic.rule_of(tpairs, Bs@[newBi], C)}))
1.871 + (Thm{sign = sign,
1.872 + der = infer_derivs (Rename_params_rule(cs,i), [der]),
1.873 + maxidx = maxidx,
1.874 + shyps = [],
1.875 + hyps = hyps,
1.876 + prop = Logic.rule_of(tpairs, Bs@[newBi], C)}))
1.877 end;
1.878
1.879 (*** Preservation of bound variable names ***)
1.880 @@ -1273,7 +1273,7 @@
1.881 (eres_flg, orule, nsubgoal) =
1.882 let val Thm{der=sder, maxidx=smax, shyps=sshyps, hyps=shyps, ...} = state
1.883 and Thm{der=rder, maxidx=rmax, shyps=rshyps, hyps=rhyps,
1.884 - prop=rprop,...} = orule
1.885 + prop=rprop,...} = orule
1.886 (*How many hyps to skip over during normalization*)
1.887 and nlift = Logic.count_prems(strip_all_body Bi,
1.888 if eres_flg then ~1 else 0)
1.889 @@ -1297,13 +1297,13 @@
1.890 end
1.891 val th = (*tuned fix_shyps*)
1.892 Thm{sign = sign,
1.893 - der = infer_derivs (Bicompose(match, eres_flg,
1.894 - 1 + length Bs, nsubgoal, env),
1.895 - [rder,sder]),
1.896 - maxidx = maxidx,
1.897 - shyps = add_env_sorts (env, union_sort(rshyps,sshyps)),
1.898 - hyps = union_term(rhyps,shyps),
1.899 - prop = Logic.rule_of normp}
1.900 + der = infer_derivs (Bicompose(match, eres_flg,
1.901 + 1 + length Bs, nsubgoal, env),
1.902 + [rder,sder]),
1.903 + maxidx = maxidx,
1.904 + shyps = add_env_sorts (env, union_sort(rshyps,sshyps)),
1.905 + hyps = union_term(rhyps,shyps),
1.906 + prop = Logic.rule_of normp}
1.907 in cons(th, thq) end handle COMPOSE => thq
1.908 val (rtpairs,rhorn) = Logic.strip_flexpairs(rprop);
1.909 val (rAs,B) = Logic.strip_prems(nsubgoal, [], rhorn)
1.910 @@ -1570,7 +1570,7 @@
1.911 if (lhs = lhs0) orelse
1.912 (lhs aconv Envir.norm_term (Envir.empty 0) lhs0)
1.913 then (trace_thm "SUCCEEDED" thm;
1.914 - Some(shyps, hyps, maxidx, rhs, der::ders))
1.915 + Some(shyps, hyps, maxidx, rhs, der::ders))
1.916 else err()
1.917 | _ => err()
1.918 end;
1.919 @@ -1605,22 +1605,22 @@
1.920 val hyps' = union_term(hyps,hypst);
1.921 val shyps' = add_insts_sorts (insts, union_sort(shyps,shypst));
1.922 val maxidx' = maxidx_of_term prop'
1.923 - val ct' = Cterm{sign = signt, (*used for deriv only*)
1.924 - t = prop',
1.925 - T = propT,
1.926 - maxidx = maxidx'}
1.927 - val der' = infer_derivs (RewriteC ct', [der])
1.928 + val ct' = Cterm{sign = signt, (*used for deriv only*)
1.929 + t = prop',
1.930 + T = propT,
1.931 + maxidx = maxidx'}
1.932 + val der' = infer_derivs (RewriteC ct', [der])
1.933 val thm' = Thm{sign = signt,
1.934 - der = der',
1.935 - shyps = shyps',
1.936 - hyps = hyps',
1.937 + der = der',
1.938 + shyps = shyps',
1.939 + hyps = hyps',
1.940 prop = prop',
1.941 - maxidx = maxidx'}
1.942 + maxidx = maxidx'}
1.943 val (lhs',rhs') = Logic.dest_equals(Logic.strip_imp_concl prop')
1.944 in if perm andalso not(termless(rhs',lhs')) then None else
1.945 if Logic.count_prems(prop',0) = 0
1.946 then (trace_thm "Rewriting:" thm';
1.947 - Some(shyps', hyps', maxidx', rhs', der'::ders))
1.948 + Some(shyps', hyps', maxidx', rhs', der'::ders))
1.949 else (trace_thm "Trying to rewrite:" thm';
1.950 case prover mss thm' of
1.951 None => (trace_thm "FAILED" thm'; None)
1.952 @@ -1632,19 +1632,19 @@
1.953 let val opt = rew rrule handle Pattern.MATCH => None
1.954 in case opt of None => rews rrules | some => some end;
1.955 fun sort_rrules rrs = let
1.956 - fun is_simple {thm as Thm{prop,...}, lhs, perm} = case prop of
1.957 - Const("==",_) $ _ $ _ => true
1.958 - | _ => false
1.959 - fun sort [] (re1,re2) = re1 @ re2
1.960 - | sort (rr::rrs) (re1,re2) = if is_simple rr
1.961 - then sort rrs (rr::re1,re2)
1.962 - else sort rrs (re1,rr::re2)
1.963 + fun is_simple {thm as Thm{prop,...}, lhs, perm} = case prop of
1.964 + Const("==",_) $ _ $ _ => true
1.965 + | _ => false
1.966 + fun sort [] (re1,re2) = re1 @ re2
1.967 + | sort (rr::rrs) (re1,re2) = if is_simple rr
1.968 + then sort rrs (rr::re1,re2)
1.969 + else sort rrs (re1,rr::re2)
1.970 in sort rrs ([],[])
1.971 end
1.972 in case etat of
1.973 Abs(_,_,body) $ u => Some(shypst, hypst, maxt,
1.974 - subst_bound (u, body),
1.975 - ders)
1.976 + subst_bound (u, body),
1.977 + ders)
1.978 | _ => rews (sort_rrules (Net.match_term net etat))
1.979 end;
1.980
1.981 @@ -1664,16 +1664,16 @@
1.982 val prop' = ren_inst(insts,rprop,rlhs,t);
1.983 val shyps' = add_insts_sorts (insts, union_sort(shyps,shypst))
1.984 val maxidx' = maxidx_of_term prop'
1.985 - val ct' = Cterm{sign = signt, (*used for deriv only*)
1.986 - t = prop',
1.987 - T = propT,
1.988 - maxidx = maxidx'}
1.989 + val ct' = Cterm{sign = signt, (*used for deriv only*)
1.990 + t = prop',
1.991 + T = propT,
1.992 + maxidx = maxidx'}
1.993 val thm' = Thm{sign = signt,
1.994 - der = infer_derivs (CongC ct', [der]),
1.995 - shyps = shyps',
1.996 - hyps = union_term(hyps,hypst),
1.997 + der = infer_derivs (CongC ct', [der]),
1.998 + shyps = shyps',
1.999 + hyps = union_term(hyps,hypst),
1.1000 prop = prop',
1.1001 - maxidx = maxidx'};
1.1002 + maxidx = maxidx'};
1.1003 val unit = trace_thm "Applying congruence rule" thm';
1.1004 fun err() = error("Failed congruence proof!")
1.1005
1.1006 @@ -1687,88 +1687,88 @@
1.1007
1.1008 fun bottomc ((simprem,useprem),prover,sign) =
1.1009 let fun botc fail mss trec =
1.1010 - (case subc mss trec of
1.1011 - some as Some(trec1) =>
1.1012 - (case rewritec (prover,sign) mss trec1 of
1.1013 - Some(trec2) => botc false mss trec2
1.1014 - | None => some)
1.1015 - | None =>
1.1016 - (case rewritec (prover,sign) mss trec of
1.1017 - Some(trec2) => botc false mss trec2
1.1018 - | None => if fail then None else Some(trec)))
1.1019 + (case subc mss trec of
1.1020 + some as Some(trec1) =>
1.1021 + (case rewritec (prover,sign) mss trec1 of
1.1022 + Some(trec2) => botc false mss trec2
1.1023 + | None => some)
1.1024 + | None =>
1.1025 + (case rewritec (prover,sign) mss trec of
1.1026 + Some(trec2) => botc false mss trec2
1.1027 + | None => if fail then None else Some(trec)))
1.1028
1.1029 and try_botc mss trec = (case botc true mss trec of
1.1030 - Some(trec1) => trec1
1.1031 - | None => trec)
1.1032 + Some(trec1) => trec1
1.1033 + | None => trec)
1.1034
1.1035 and subc (mss as Mss{net,congs,bounds,prems,mk_rews})
1.1036 - (trec as (shyps,hyps,maxidx,t0,ders)) =
1.1037 + (trec as (shyps,hyps,maxidx,t0,ders)) =
1.1038 (case t0 of
1.1039 - Abs(a,T,t) =>
1.1040 - let val b = variant bounds a
1.1041 - val v = Free("." ^ b,T)
1.1042 - val mss' = Mss{net=net, congs=congs, bounds=b::bounds,
1.1043 - prems=prems,mk_rews=mk_rews}
1.1044 - in case botc true mss'
1.1045 - (shyps,hyps,maxidx,subst_bound (v,t),ders) of
1.1046 - Some(shyps',hyps',maxidx',t',ders') =>
1.1047 - Some(shyps', hyps', maxidx',
1.1048 - Abs(a, T, abstract_over(v,t')),
1.1049 - ders')
1.1050 - | None => None
1.1051 - end
1.1052 - | t$u => (case t of
1.1053 - Const("==>",_)$s => Some(impc(shyps,hyps,maxidx,s,u,mss,ders))
1.1054 - | Abs(_,_,body) =>
1.1055 - let val trec = (shyps,hyps,maxidx,subst_bound (u,body),ders)
1.1056 - in case subc mss trec of
1.1057 - None => Some(trec)
1.1058 - | trec => trec
1.1059 - end
1.1060 - | _ =>
1.1061 - let fun appc() =
1.1062 - (case botc true mss (shyps,hyps,maxidx,t,ders) of
1.1063 - Some(shyps1,hyps1,maxidx1,t1,ders1) =>
1.1064 - (case botc true mss (shyps1,hyps1,maxidx,u,ders1) of
1.1065 - Some(shyps2,hyps2,maxidx2,u1,ders2) =>
1.1066 - Some(shyps2, hyps2, Int.max(maxidx1,maxidx2),
1.1067 - t1$u1, ders2)
1.1068 - | None =>
1.1069 - Some(shyps1, hyps1, Int.max(maxidx1,maxidx), t1$u,
1.1070 - ders1))
1.1071 - | None =>
1.1072 - (case botc true mss (shyps,hyps,maxidx,u,ders) of
1.1073 - Some(shyps1,hyps1,maxidx1,u1,ders1) =>
1.1074 - Some(shyps1, hyps1, Int.max(maxidx,maxidx1),
1.1075 - t$u1, ders1)
1.1076 - | None => None))
1.1077 - val (h,ts) = strip_comb t
1.1078 - in case h of
1.1079 - Const(a,_) =>
1.1080 - (case assoc_string(congs,a) of
1.1081 - None => appc()
1.1082 - | Some(cong) => (congc (prover mss,sign) cong trec
1.1083 + Abs(a,T,t) =>
1.1084 + let val b = variant bounds a
1.1085 + val v = Free("." ^ b,T)
1.1086 + val mss' = Mss{net=net, congs=congs, bounds=b::bounds,
1.1087 + prems=prems,mk_rews=mk_rews}
1.1088 + in case botc true mss'
1.1089 + (shyps,hyps,maxidx,subst_bound (v,t),ders) of
1.1090 + Some(shyps',hyps',maxidx',t',ders') =>
1.1091 + Some(shyps', hyps', maxidx',
1.1092 + Abs(a, T, abstract_over(v,t')),
1.1093 + ders')
1.1094 + | None => None
1.1095 + end
1.1096 + | t$u => (case t of
1.1097 + Const("==>",_)$s => Some(impc(shyps,hyps,maxidx,s,u,mss,ders))
1.1098 + | Abs(_,_,body) =>
1.1099 + let val trec = (shyps,hyps,maxidx,subst_bound (u,body),ders)
1.1100 + in case subc mss trec of
1.1101 + None => Some(trec)
1.1102 + | trec => trec
1.1103 + end
1.1104 + | _ =>
1.1105 + let fun appc() =
1.1106 + (case botc true mss (shyps,hyps,maxidx,t,ders) of
1.1107 + Some(shyps1,hyps1,maxidx1,t1,ders1) =>
1.1108 + (case botc true mss (shyps1,hyps1,maxidx,u,ders1) of
1.1109 + Some(shyps2,hyps2,maxidx2,u1,ders2) =>
1.1110 + Some(shyps2, hyps2, Int.max(maxidx1,maxidx2),
1.1111 + t1$u1, ders2)
1.1112 + | None =>
1.1113 + Some(shyps1, hyps1, Int.max(maxidx1,maxidx), t1$u,
1.1114 + ders1))
1.1115 + | None =>
1.1116 + (case botc true mss (shyps,hyps,maxidx,u,ders) of
1.1117 + Some(shyps1,hyps1,maxidx1,u1,ders1) =>
1.1118 + Some(shyps1, hyps1, Int.max(maxidx,maxidx1),
1.1119 + t$u1, ders1)
1.1120 + | None => None))
1.1121 + val (h,ts) = strip_comb t
1.1122 + in case h of
1.1123 + Const(a,_) =>
1.1124 + (case assoc_string(congs,a) of
1.1125 + None => appc()
1.1126 + | Some(cong) => (congc (prover mss,sign) cong trec
1.1127 handle Pattern.MATCH => appc() ) )
1.1128 - | _ => appc()
1.1129 - end)
1.1130 - | _ => None)
1.1131 + | _ => appc()
1.1132 + end)
1.1133 + | _ => None)
1.1134
1.1135 and impc(shyps, hyps, maxidx, s, u, mss as Mss{mk_rews,...}, ders) =
1.1136 let val (shyps1,hyps1,_,s1,ders1) =
1.1137 - if simprem then try_botc mss (shyps,hyps,maxidx,s,ders)
1.1138 - else (shyps,hyps,0,s,ders);
1.1139 - val maxidx1 = maxidx_of_term s1
1.1140 - val mss1 =
1.1141 - if not useprem orelse maxidx1 <> ~1 then mss
1.1142 - else let val thm = assume (Cterm{sign=sign, t=s1,
1.1143 - T=propT, maxidx=maxidx1})
1.1144 - in add_simps(add_prems(mss,[thm]), mk_rews thm) end
1.1145 - val (shyps2,hyps2,maxidx2,u1,ders2) =
1.1146 - try_botc mss1 (shyps1,hyps1,maxidx,u,ders1)
1.1147 - val hyps3 = if gen_mem (op aconv) (s1, hyps1)
1.1148 - then hyps2 else hyps2\s1
1.1149 + if simprem then try_botc mss (shyps,hyps,maxidx,s,ders)
1.1150 + else (shyps,hyps,0,s,ders);
1.1151 + val maxidx1 = maxidx_of_term s1
1.1152 + val mss1 =
1.1153 + if not useprem orelse maxidx1 <> ~1 then mss
1.1154 + else let val thm = assume (Cterm{sign=sign, t=s1,
1.1155 + T=propT, maxidx=maxidx1})
1.1156 + in add_simps(add_prems(mss,[thm]), mk_rews thm) end
1.1157 + val (shyps2,hyps2,maxidx2,u1,ders2) =
1.1158 + try_botc mss1 (shyps1,hyps1,maxidx,u,ders1)
1.1159 + val hyps3 = if gen_mem (op aconv) (s1, hyps1)
1.1160 + then hyps2 else hyps2\s1
1.1161 in (shyps2, hyps3, Int.max(maxidx1,maxidx2),
1.1162 - Logic.mk_implies(s1,u1), ders2)
1.1163 + Logic.mk_implies(s1,u1), ders2)
1.1164 end
1.1165
1.1166 in try_botc end;
1.1167 @@ -1785,34 +1785,34 @@
1.1168 let val {sign, t, T, maxidx} = rep_cterm ct;
1.1169 val (shyps,hyps,maxu,u,ders) =
1.1170 bottomc (mode,prover,sign) mss
1.1171 - (add_term_sorts(t,[]), [], maxidx, t, []);
1.1172 + (add_term_sorts(t,[]), [], maxidx, t, []);
1.1173 val prop = Logic.mk_equals(t,u)
1.1174 in
1.1175 Thm{sign = sign,
1.1176 - der = infer_derivs (Rewrite_cterm ct, ders),
1.1177 - maxidx = Int.max (maxidx,maxu),
1.1178 - shyps = shyps,
1.1179 - hyps = hyps,
1.1180 + der = infer_derivs (Rewrite_cterm ct, ders),
1.1181 + maxidx = Int.max (maxidx,maxu),
1.1182 + shyps = shyps,
1.1183 + hyps = hyps,
1.1184 prop = prop}
1.1185 end
1.1186
1.1187
1.1188 fun invoke_oracle (thy, sign, exn) =
1.1189 case #oraopt(rep_theory thy) of
1.1190 - None => raise THM ("No oracle in supplied theory", 0, [])
1.1191 + None => raise THM ("No oracle in supplied theory", 0, [])
1.1192 | Some oracle =>
1.1193 - let val sign' = Sign.merge(sign_of thy, sign)
1.1194 - val (prop, T, maxidx) =
1.1195 - Sign.certify_term sign' (oracle (sign', exn))
1.1196 + let val sign' = Sign.merge(sign_of thy, sign)
1.1197 + val (prop, T, maxidx) =
1.1198 + Sign.certify_term sign' (oracle (sign', exn))
1.1199 in if T<>propT then
1.1200 raise THM("Oracle's result must have type prop", 0, [])
1.1201 - else fix_shyps [] []
1.1202 - (Thm {sign = sign',
1.1203 - der = Join (Oracle(thy,sign,exn), []),
1.1204 - maxidx = maxidx,
1.1205 - shyps = [],
1.1206 - hyps = [],
1.1207 - prop = prop})
1.1208 + else fix_shyps [] []
1.1209 + (Thm {sign = sign',
1.1210 + der = Join (Oracle(thy,sign,exn), []),
1.1211 + maxidx = maxidx,
1.1212 + shyps = [],
1.1213 + hyps = [],
1.1214 + prop = prop})
1.1215 end;
1.1216
1.1217 end;