34 val cabs : cterm -> cterm -> cterm |
33 val cabs : cterm -> cterm -> cterm |
35 val read_def_cterm : |
34 val read_def_cterm : |
36 Sign.sg * (indexname -> typ option) * (indexname -> sort option) -> |
35 Sign.sg * (indexname -> typ option) * (indexname -> sort option) -> |
37 string list -> bool -> string * typ -> cterm * (indexname * typ) list |
36 string list -> bool -> string * typ -> cterm * (indexname * typ) list |
38 |
37 |
|
38 (*theories*) |
|
39 |
|
40 (*proof terms [must duplicate declaration as a specification]*) |
|
41 val full_deriv : bool ref |
|
42 datatype rule = |
|
43 MinProof |
|
44 | Axiom of theory * string |
|
45 | Theorem of theory * string |
|
46 | Assume of cterm |
|
47 | Implies_intr of cterm |
|
48 | Implies_intr_shyps |
|
49 | Implies_intr_hyps |
|
50 | Implies_elim |
|
51 | Forall_intr of cterm |
|
52 | Forall_elim of cterm |
|
53 | Reflexive of cterm |
|
54 | Symmetric |
|
55 | Transitive |
|
56 | Beta_conversion of cterm |
|
57 | Extensional |
|
58 | Abstract_rule of string * cterm |
|
59 | Combination |
|
60 | Equal_intr |
|
61 | Equal_elim |
|
62 | Trivial of cterm |
|
63 | Lift_rule of cterm * int |
|
64 | Assumption of int * Envir.env option |
|
65 | Instantiate of (indexname * ctyp) list * (cterm * cterm) list |
|
66 | Bicompose of bool * bool * int * int * Envir.env |
|
67 | Flexflex_rule of Envir.env |
|
68 | Class_triv of theory * class |
|
69 | VarifyT |
|
70 | FreezeT |
|
71 | RewriteC of cterm |
|
72 | CongC of cterm |
|
73 | Rewrite_cterm of cterm |
|
74 | Rename_params_rule of string list * int; |
|
75 |
|
76 datatype deriv = Infer of rule * deriv list |
|
77 | Oracle of string * exn ; |
|
78 |
39 (*meta theorems*) |
79 (*meta theorems*) |
40 type thm |
80 type thm |
41 exception THM of string * int * thm list |
81 exception THM of string * int * thm list |
42 val rep_thm : thm -> {sign: Sign.sg, maxidx: int, |
82 val rep_thm : thm -> {sign: Sign.sg, der: deriv, maxidx: int, |
43 shyps: sort list, hyps: term list, prop: term} |
83 shyps: sort list, hyps: term list, |
44 val crep_thm : thm -> {sign: Sign.sg, maxidx: int, |
84 prop: term} |
45 shyps: sort list, hyps: cterm list, prop: cterm} |
85 val crep_thm : thm -> {sign: Sign.sg, der: deriv, maxidx: int, |
|
86 shyps: sort list, hyps: cterm list, |
|
87 prop: cterm} |
46 val stamps_of_thm : thm -> string ref list |
88 val stamps_of_thm : thm -> string ref list |
47 val tpairs_of : thm -> (term * term) list |
89 val tpairs_of : thm -> (term * term) list |
48 val prems_of : thm -> term list |
90 val prems_of : thm -> term list |
49 val nprems_of : thm -> int |
91 val nprems_of : thm -> int |
50 val concl_of : thm -> term |
92 val concl_of : thm -> term |
51 val cprop_of : thm -> cterm |
93 val cprop_of : thm -> cterm |
52 val extra_shyps : thm -> sort list |
94 val extra_shyps : thm -> sort list |
53 val force_strip_shyps : bool ref (* FIXME tmp *) |
95 val force_strip_shyps : bool ref (* FIXME tmp *) |
54 val strip_shyps : thm -> thm |
96 val strip_shyps : thm -> thm |
55 val implies_intr_shyps: thm -> thm |
97 val implies_intr_shyps: thm -> thm |
56 val cert_axm : Sign.sg -> string * term -> string * term |
|
57 val read_axm : Sign.sg -> string * string -> string * term |
|
58 val inferT_axm : Sign.sg -> string * term -> string * term |
|
59 |
|
60 (*theories*) |
|
61 type theory |
|
62 exception THEORY of string * theory list |
|
63 val rep_theory : theory -> |
|
64 {sign: Sign.sg, new_axioms: term Symtab.table, parents: theory list} |
|
65 val sign_of : theory -> Sign.sg |
|
66 val syn_of : theory -> Syntax.syntax |
|
67 val stamps_of_thy : theory -> string ref list |
|
68 val parents_of : theory -> theory list |
|
69 val subthy : theory * theory -> bool |
|
70 val eq_thy : theory * theory -> bool |
|
71 val get_axiom : theory -> string -> thm |
98 val get_axiom : theory -> string -> thm |
|
99 val name_thm : theory * string * thm -> thm |
72 val axioms_of : theory -> (string * thm) list |
100 val axioms_of : theory -> (string * thm) list |
73 val proto_pure_thy : theory |
|
74 val pure_thy : theory |
|
75 val cpure_thy : theory |
|
76 (*theory primitives*) |
|
77 val add_classes : (class * class list) list -> theory -> theory |
|
78 val add_classrel : (class * class) list -> theory -> theory |
|
79 val add_defsort : sort -> theory -> theory |
|
80 val add_types : (string * int * mixfix) list -> theory -> theory |
|
81 val add_tyabbrs : (string * string list * string * mixfix) list |
|
82 -> theory -> theory |
|
83 val add_tyabbrs_i : (string * string list * typ * mixfix) list |
|
84 -> theory -> theory |
|
85 val add_arities : (string * sort list * sort) list -> theory -> theory |
|
86 val add_consts : (string * string * mixfix) list -> theory -> theory |
|
87 val add_consts_i : (string * typ * mixfix) list -> theory -> theory |
|
88 val add_syntax : (string * string * mixfix) list -> theory -> theory |
|
89 val add_syntax_i : (string * typ * mixfix) list -> theory -> theory |
|
90 val add_trfuns : |
|
91 (string * (Syntax.ast list -> Syntax.ast)) list * |
|
92 (string * (term list -> term)) list * |
|
93 (string * (term list -> term)) list * |
|
94 (string * (Syntax.ast list -> Syntax.ast)) list -> theory -> theory |
|
95 val add_trrules : (string * string)Syntax.trrule list -> theory -> theory |
|
96 val add_trrules_i : Syntax.ast Syntax.trrule list -> theory -> theory |
|
97 val add_axioms : (string * string) list -> theory -> theory |
|
98 val add_axioms_i : (string * term) list -> theory -> theory |
|
99 val add_thyname : string -> theory -> theory |
|
100 |
|
101 val merge_theories : theory * theory -> theory |
|
102 val merge_thy_list : bool -> theory list -> theory |
|
103 |
101 |
104 (*meta rules*) |
102 (*meta rules*) |
105 val assume : cterm -> thm |
103 val assume : cterm -> thm |
106 val compress : thm -> thm |
104 val compress : thm -> thm |
107 val implies_intr : cterm -> thm -> thm |
105 val implies_intr : cterm -> thm -> thm |
272 handle TYPE arg => error (Sign.exn_type_msg sign arg) |
270 handle TYPE arg => error (Sign.exn_type_msg sign arg) |
273 | TERM (msg, _) => error msg; |
271 | TERM (msg, _) => error msg; |
274 |
272 |
275 |
273 |
276 |
274 |
|
275 (*** Derivations ***) |
|
276 |
|
277 (*Names of rules in derivations. Includes logically trivial rules, if |
|
278 executed in ML.*) |
|
279 datatype rule = |
|
280 MinProof (*for building minimal proof terms*) |
|
281 (*Axioms/theorems*) |
|
282 | Axiom of theory * string |
|
283 | Theorem of theory * string (*via theorem db*) |
|
284 (*primitive inferences and compound versions of them*) |
|
285 | Assume of cterm |
|
286 | Implies_intr of cterm |
|
287 | Implies_intr_shyps |
|
288 | Implies_intr_hyps |
|
289 | Implies_elim |
|
290 | Forall_intr of cterm |
|
291 | Forall_elim of cterm |
|
292 | Reflexive of cterm |
|
293 | Symmetric |
|
294 | Transitive |
|
295 | Beta_conversion of cterm |
|
296 | Extensional |
|
297 | Abstract_rule of string * cterm |
|
298 | Combination |
|
299 | Equal_intr |
|
300 | Equal_elim |
|
301 (*derived rules for tactical proof*) |
|
302 | Trivial of cterm |
|
303 (*For lift_rule, the proof state is not a premise. |
|
304 Use cterm instead of thm to avoid mutual recursion.*) |
|
305 | Lift_rule of cterm * int |
|
306 | Assumption of int * Envir.env option (*includes eq_assumption*) |
|
307 | Instantiate of (indexname * ctyp) list * (cterm * cterm) list |
|
308 | Bicompose of bool * bool * int * int * Envir.env |
|
309 | Flexflex_rule of Envir.env (*identifies unifier chosen*) |
|
310 (*other derived rules*) |
|
311 | Class_triv of theory * class (*derived rule????*) |
|
312 | VarifyT |
|
313 | FreezeT |
|
314 (*for the simplifier*) |
|
315 | RewriteC of cterm |
|
316 | CongC of cterm |
|
317 | Rewrite_cterm of cterm |
|
318 (*Logical identities, recorded since they are part of the proof process*) |
|
319 | Rename_params_rule of string list * int; |
|
320 |
|
321 |
|
322 datatype deriv = Infer of rule * deriv list |
|
323 | Oracle of string * exn (*???*); |
|
324 |
|
325 |
|
326 val full_deriv = ref false; |
|
327 |
|
328 |
|
329 (*Suppress all atomic inferences, if using minimal derivations*) |
|
330 fun squash_derivs (Infer (_, []) :: drvs) = squash_derivs drvs |
|
331 | squash_derivs (der :: ders) = der :: squash_derivs ders |
|
332 | squash_derivs [] = []; |
|
333 |
|
334 (*Ensure sharing of the most likely derivation, the empty one!*) |
|
335 val min_infer = Infer (MinProof, []); |
|
336 |
|
337 (*Make a minimal inference*) |
|
338 fun make_min_infer [] = min_infer |
|
339 | make_min_infer [der] = der |
|
340 | make_min_infer ders = Infer (MinProof, ders); |
|
341 |
|
342 fun infer_derivs (rl, []) = Infer (rl, []) |
|
343 | infer_derivs (rl, ders) = |
|
344 if !full_deriv then Infer (rl, ders) |
|
345 else make_min_infer (squash_derivs ders); |
|
346 |
|
347 |
277 (*** Meta theorems ***) |
348 (*** Meta theorems ***) |
278 |
349 |
279 datatype thm = Thm of |
350 datatype thm = Thm of |
280 {sign: Sign.sg, (*signature for hyps and prop*) |
351 {sign: Sign.sg, (*signature for hyps and prop*) |
|
352 der: deriv, (*derivation*) |
281 maxidx: int, (*maximum index of any Var or TVar*) |
353 maxidx: int, (*maximum index of any Var or TVar*) |
282 shyps: sort list, (* FIXME comment *) |
354 shyps: sort list, (* FIXME comment *) |
283 hyps: term list, (*hypotheses*) |
355 hyps: term list, (*hypotheses*) |
284 prop: term}; (*conclusion*) |
356 prop: term}; (*conclusion*) |
285 |
357 |
286 fun rep_thm (Thm args) = args; |
358 fun rep_thm (Thm args) = args; |
287 |
359 |
288 fun crep_thm (Thm {sign, maxidx, shyps, hyps, prop}) = |
360 (*Version of rep_thm returning cterms instead of terms*) |
289 let fun cterm_of t = Cterm{sign=sign, t=t, T=fastype_of t, maxidx=maxidx}; |
361 fun crep_thm (Thm {sign, der, maxidx, shyps, hyps, prop}) = |
290 in {sign=sign, maxidx=maxidx, shyps=shyps, |
362 let fun ctermf max t = Cterm{sign=sign, t=t, T=propT, maxidx=max}; |
291 hyps=map cterm_of hyps, prop=cterm_of prop} |
363 in {sign=sign, der=der, maxidx=maxidx, shyps=shyps, |
|
364 hyps = map (ctermf ~1) hyps, |
|
365 prop = ctermf maxidx prop} |
292 end; |
366 end; |
293 |
367 |
294 (*errors involving theorems*) |
368 (*errors involving theorems*) |
295 exception THM of string * int * thm list; |
369 exception THM of string * int * thm list; |
296 |
370 |
364 (*get 'dangling' sort constraints of a thm*) |
438 (*get 'dangling' sort constraints of a thm*) |
365 fun extra_shyps (th as Thm {shyps, ...}) = |
439 fun extra_shyps (th as Thm {shyps, ...}) = |
366 shyps \\ add_thm_sorts (th, []); |
440 shyps \\ add_thm_sorts (th, []); |
367 |
441 |
368 |
442 |
369 (*Compression of theorems -- a separate rule, not integrated with the others, |
|
370 as it could be slow.*) |
|
371 fun compress (Thm {sign, maxidx, shyps, hyps, prop}) = |
|
372 Thm {sign = sign, |
|
373 maxidx = maxidx, |
|
374 shyps = shyps, |
|
375 hyps = map Term.compress_term hyps, |
|
376 prop = Term.compress_term prop}; |
|
377 |
|
378 |
|
379 (* fix_shyps *) |
443 (* fix_shyps *) |
380 |
444 |
381 (*preserve sort contexts of rule premises and substituted types*) |
445 (*preserve sort contexts of rule premises and substituted types*) |
382 fun fix_shyps thms Ts thm = |
446 fun fix_shyps thms Ts thm = |
383 let |
447 let |
384 val Thm {sign, maxidx, hyps, prop, ...} = thm; |
448 val Thm {sign, der, maxidx, hyps, prop, ...} = thm; |
385 val shyps = |
449 val shyps = |
386 add_thm_sorts (thm, add_typs_sorts (Ts, add_thms_shyps (thms, []))); |
450 add_thm_sorts (thm, add_typs_sorts (Ts, add_thms_shyps (thms, []))); |
387 in |
451 in |
388 Thm {sign = sign, maxidx = maxidx, |
452 Thm {sign = sign, |
389 shyps = shyps, hyps = hyps, prop = prop} |
453 der = der, (*No new derivation, as other rules call this*) |
|
454 maxidx = maxidx, |
|
455 shyps = shyps, hyps = hyps, prop = prop} |
390 end; |
456 end; |
391 |
457 |
392 |
458 |
393 (* strip_shyps *) (* FIXME improve? (e.g. only minimal extra sorts) *) |
459 (* strip_shyps *) (* FIXME improve? (e.g. only minimal extra sorts) *) |
394 |
460 |
395 val force_strip_shyps = ref true; (* FIXME tmp *) |
461 val force_strip_shyps = ref true; (* FIXME tmp *) |
396 |
462 |
397 (*remove extra sorts that are known to be syntactically non-empty*) |
463 (*remove extra sorts that are known to be syntactically non-empty*) |
398 fun strip_shyps thm = |
464 fun strip_shyps thm = |
399 let |
465 let |
400 val Thm {sign, maxidx, shyps, hyps, prop} = thm; |
466 val Thm {sign, der, maxidx, shyps, hyps, prop} = thm; |
401 val sorts = add_thm_sorts (thm, []); |
467 val sorts = add_thm_sorts (thm, []); |
402 val maybe_empty = not o Sign.nonempty_sort sign sorts; |
468 val maybe_empty = not o Sign.nonempty_sort sign sorts; |
403 val shyps' = filter (fn S => S mem sorts orelse maybe_empty S) shyps; |
469 val shyps' = filter (fn S => S mem sorts orelse maybe_empty S) shyps; |
404 in |
470 in |
405 Thm {sign = sign, maxidx = maxidx, |
471 Thm {sign = sign, der = der, maxidx = maxidx, |
406 shyps = |
472 shyps = |
407 (if eq_set (shyps', sorts) orelse not (! force_strip_shyps) then shyps' |
473 (if eq_set (shyps',sorts) orelse not (!force_strip_shyps) then shyps' |
408 else (* FIXME tmp *) |
474 else (* FIXME tmp *) |
409 (writeln ("WARNING Removed sort hypotheses: " ^ |
475 (writeln ("WARNING Removed sort hypotheses: " ^ |
410 commas (map Type.str_of_sort (shyps' \\ sorts))); |
476 commas (map Type.str_of_sort (shyps' \\ sorts))); |
411 writeln "WARNING Let's hope these sorts are non-empty!"; |
477 writeln "WARNING Let's hope these sorts are non-empty!"; |
412 sorts)), |
478 sorts)), |
413 hyps = hyps, prop = prop} |
479 hyps = hyps, |
|
480 prop = prop} |
414 end; |
481 end; |
415 |
482 |
416 |
483 |
417 (* implies_intr_shyps *) |
484 (* implies_intr_shyps *) |
418 |
485 |
420 fun implies_intr_shyps thm = |
487 fun implies_intr_shyps thm = |
421 (case extra_shyps thm of |
488 (case extra_shyps thm of |
422 [] => thm |
489 [] => thm |
423 | xshyps => |
490 | xshyps => |
424 let |
491 let |
425 val Thm {sign, maxidx, shyps, hyps, prop} = thm; |
492 val Thm {sign, der, maxidx, shyps, hyps, prop} = thm; |
426 val shyps' = logicS ins (shyps \\ xshyps); |
493 val shyps' = logicS ins (shyps \\ xshyps); |
427 val used_names = foldr add_term_tfree_names (prop :: hyps, []); |
494 val used_names = foldr add_term_tfree_names (prop :: hyps, []); |
428 val names = |
495 val names = |
429 tl (variantlist (replicate (length xshyps + 1) "'", used_names)); |
496 tl (variantlist (replicate (length xshyps + 1) "'", used_names)); |
430 val tfrees = map (TFree o rpair logicS) names; |
497 val tfrees = map (TFree o rpair logicS) names; |
431 |
498 |
432 fun mk_insort (T, S) = map (Logic.mk_inclass o pair T) S; |
499 fun mk_insort (T, S) = map (Logic.mk_inclass o pair T) S; |
433 val sort_hyps = flat (map2 mk_insort (tfrees, xshyps)); |
500 val sort_hyps = flat (map2 mk_insort (tfrees, xshyps)); |
434 in |
501 in |
435 Thm {sign = sign, maxidx = maxidx, shyps = shyps', |
502 Thm {sign = sign, |
436 hyps = hyps, prop = Logic.list_implies (sort_hyps, prop)} |
503 der = infer_derivs (Implies_intr_shyps, [der]), |
|
504 maxidx = maxidx, |
|
505 shyps = shyps', |
|
506 hyps = hyps, |
|
507 prop = Logic.list_implies (sort_hyps, prop)} |
437 end); |
508 end); |
438 |
509 |
439 |
510 |
440 |
511 (** Axioms **) |
441 (*** Theories ***) |
|
442 |
|
443 datatype theory = |
|
444 Theory of { |
|
445 sign: Sign.sg, |
|
446 new_axioms: term Symtab.table, |
|
447 parents: theory list}; |
|
448 |
|
449 fun rep_theory (Theory args) = args; |
|
450 |
|
451 (*errors involving theories*) |
|
452 exception THEORY of string * theory list; |
|
453 |
|
454 |
|
455 val sign_of = #sign o rep_theory; |
|
456 val syn_of = #syn o Sign.rep_sg o sign_of; |
|
457 |
|
458 (*stamps associated with a theory*) |
|
459 val stamps_of_thy = #stamps o Sign.rep_sg o sign_of; |
|
460 |
|
461 (*return the immediate ancestors*) |
|
462 val parents_of = #parents o rep_theory; |
|
463 |
|
464 |
|
465 (*compare theories*) |
|
466 val subthy = Sign.subsig o pairself sign_of; |
|
467 val eq_thy = Sign.eq_sg o pairself sign_of; |
|
468 |
|
469 |
512 |
470 (*look up the named axiom in the theory*) |
513 (*look up the named axiom in the theory*) |
471 fun get_axiom theory name = |
514 fun get_axiom theory name = |
472 let |
515 let |
473 fun get_ax [] = raise Match |
516 fun get_ax [] = raise Match |
474 | get_ax (Theory {sign, new_axioms, parents} :: thys) = |
517 | get_ax (thy :: thys) = |
475 (case Symtab.lookup (new_axioms, name) of |
518 let val {sign, new_axioms, parents} = rep_theory thy |
476 Some t => fix_shyps [] [] |
519 in case Symtab.lookup (new_axioms, name) of |
477 (Thm {sign = sign, maxidx = maxidx_of_term t, |
520 Some t => fix_shyps [] [] |
478 shyps = [], hyps = [], prop = t}) |
521 (Thm {sign = sign, |
479 | None => get_ax parents handle Match => get_ax thys); |
522 der = infer_derivs (Axiom(theory,name), []), |
|
523 maxidx = maxidx_of_term t, |
|
524 shyps = [], |
|
525 hyps = [], |
|
526 prop = t}) |
|
527 | None => get_ax parents handle Match => get_ax thys |
|
528 end; |
480 in |
529 in |
481 get_ax [theory] handle Match |
530 get_ax [theory] handle Match |
482 => raise THEORY ("get_axiom: no axiom " ^ quote name, [theory]) |
531 => raise THEORY ("get_axiom: no axiom " ^ quote name, [theory]) |
483 end; |
532 end; |
|
533 |
484 |
534 |
485 (*return additional axioms of this theory node*) |
535 (*return additional axioms of this theory node*) |
486 fun axioms_of thy = |
536 fun axioms_of thy = |
487 map (fn (s, _) => (s, get_axiom thy s)) |
537 map (fn (s, _) => (s, get_axiom thy s)) |
488 (Symtab.dest (#new_axioms (rep_theory thy))); |
538 (Symtab.dest (#new_axioms (rep_theory thy))); |
489 |
539 |
490 |
540 fun name_thm (thy, name, th as Thm {sign, der, maxidx, shyps, hyps, prop}) = |
491 (* the Pure theories *) |
541 if Sign.eq_sg (sign, sign_of thy) then |
492 |
542 Thm {sign = sign, |
493 val proto_pure_thy = |
543 der = Infer (Theorem(thy,name), []), |
494 Theory {sign = Sign.proto_pure, new_axioms = Symtab.null, parents = []}; |
544 maxidx = maxidx, |
495 |
545 shyps = shyps, |
496 val pure_thy = |
546 hyps = hyps, |
497 Theory {sign = Sign.pure, new_axioms = Symtab.null, parents = []}; |
547 prop = prop} |
498 |
548 else raise THM ("name_thm", 0, [th]); |
499 val cpure_thy = |
549 |
500 Theory {sign = Sign.cpure, new_axioms = Symtab.null, parents = []}; |
550 |
501 |
551 (*Compression of theorems -- a separate rule, not integrated with the others, |
502 |
552 as it could be slow.*) |
503 |
553 fun compress (Thm {sign, der, maxidx, shyps, hyps, prop}) = |
504 (** extend theory **) |
554 Thm {sign = sign, |
505 |
555 der = der, (*No derivation recorded!*) |
506 fun err_dup_axms names = |
556 maxidx = maxidx, |
507 error ("Duplicate axiom name(s) " ^ commas_quote names); |
557 shyps = shyps, |
508 |
558 hyps = map Term.compress_term hyps, |
509 fun ext_thy (thy as Theory {sign, new_axioms, parents}) sign1 new_axms = |
559 prop = Term.compress_term prop}; |
510 let |
560 |
511 val draft = Sign.is_draft sign; |
561 |
512 val new_axioms1 = |
562 (*** Meta rules ***) |
513 Symtab.extend_new (if draft then new_axioms else Symtab.null, new_axms) |
|
514 handle Symtab.DUPS names => err_dup_axms names; |
|
515 val parents1 = if draft then parents else [thy]; |
|
516 in |
|
517 Theory {sign = sign1, new_axioms = new_axioms1, parents = parents1} |
|
518 end; |
|
519 |
|
520 |
|
521 (* extend signature of a theory *) |
|
522 |
|
523 fun ext_sg extfun decls (thy as Theory {sign, ...}) = |
|
524 ext_thy thy (extfun decls sign) []; |
|
525 |
|
526 val add_classes = ext_sg Sign.add_classes; |
|
527 val add_classrel = ext_sg Sign.add_classrel; |
|
528 val add_defsort = ext_sg Sign.add_defsort; |
|
529 val add_types = ext_sg Sign.add_types; |
|
530 val add_tyabbrs = ext_sg Sign.add_tyabbrs; |
|
531 val add_tyabbrs_i = ext_sg Sign.add_tyabbrs_i; |
|
532 val add_arities = ext_sg Sign.add_arities; |
|
533 val add_consts = ext_sg Sign.add_consts; |
|
534 val add_consts_i = ext_sg Sign.add_consts_i; |
|
535 val add_syntax = ext_sg Sign.add_syntax; |
|
536 val add_syntax_i = ext_sg Sign.add_syntax_i; |
|
537 val add_trfuns = ext_sg Sign.add_trfuns; |
|
538 val add_trrules = ext_sg Sign.add_trrules; |
|
539 val add_trrules_i = ext_sg Sign.add_trrules_i; |
|
540 val add_thyname = ext_sg Sign.add_name; |
|
541 |
|
542 |
|
543 (* prepare axioms *) |
|
544 |
|
545 fun err_in_axm name = |
|
546 error ("The error(s) above occurred in axiom " ^ quote name); |
|
547 |
|
548 fun no_vars tm = |
|
549 if null (term_vars tm) andalso null (term_tvars tm) then tm |
|
550 else error "Illegal schematic variable(s) in term"; |
|
551 |
|
552 fun cert_axm sg (name, raw_tm) = |
|
553 let |
|
554 val Cterm {t, T, ...} = cterm_of sg raw_tm |
|
555 handle TYPE arg => error (Sign.exn_type_msg sg arg) |
|
556 | TERM (msg, _) => error msg; |
|
557 in |
|
558 assert (T = propT) "Term not of type prop"; |
|
559 (name, no_vars t) |
|
560 end |
|
561 handle ERROR => err_in_axm name; |
|
562 |
|
563 fun read_axm sg (name, str) = |
|
564 (name, no_vars (term_of (read_cterm sg (str, propT)))) |
|
565 handle ERROR => err_in_axm name; |
|
566 |
|
567 fun inferT_axm sg (name, pre_tm) = |
|
568 let val t = #2(Sign.infer_types sg (K None) (K None) [] true |
|
569 ([pre_tm], propT)) |
|
570 in (name, no_vars t) end |
|
571 handle ERROR => err_in_axm name; |
|
572 |
|
573 |
|
574 (* extend axioms of a theory *) |
|
575 |
|
576 fun ext_axms prep_axm axms (thy as Theory {sign, ...}) = |
|
577 let |
|
578 val sign1 = Sign.make_draft sign; |
|
579 val axioms = map (apsnd (Term.compress_term o Logic.varify) o |
|
580 prep_axm sign) |
|
581 axms; |
|
582 in |
|
583 ext_thy thy sign1 axioms |
|
584 end; |
|
585 |
|
586 val add_axioms = ext_axms read_axm; |
|
587 val add_axioms_i = ext_axms cert_axm; |
|
588 |
|
589 |
|
590 |
|
591 (** merge theories **) |
|
592 |
|
593 fun merge_thy_list mk_draft thys = |
|
594 let |
|
595 fun is_union thy = forall (fn t => subthy (t, thy)) thys; |
|
596 val is_draft = Sign.is_draft o sign_of; |
|
597 |
|
598 fun add_sign (sg, Theory {sign, ...}) = |
|
599 Sign.merge (sg, sign) handle TERM (msg, _) => error msg; |
|
600 in |
|
601 (case (find_first is_union thys, exists is_draft thys) of |
|
602 (Some thy, _) => thy |
|
603 | (None, true) => raise THEORY ("Illegal merge of draft theories", thys) |
|
604 | (None, false) => Theory { |
|
605 sign = |
|
606 (if mk_draft then Sign.make_draft else I) |
|
607 (foldl add_sign (Sign.proto_pure, thys)), |
|
608 new_axioms = Symtab.null, |
|
609 parents = thys}) |
|
610 end; |
|
611 |
|
612 fun merge_theories (thy1, thy2) = merge_thy_list false [thy1, thy2]; |
|
613 |
|
614 |
563 |
615 (* check that term does not contain same var with different typing/sorting *) |
564 (* check that term does not contain same var with different typing/sorting *) |
616 fun nodup_Vars(thm as Thm{prop,...}) s = |
565 fun nodup_Vars(thm as Thm{prop,...}) s = |
617 Sign.nodup_Vars prop handle TYPE(msg,_,_) => raise THM(s^": "^msg,0,[thm]); |
566 Sign.nodup_Vars prop handle TYPE(msg,_,_) => raise THM(s^": "^msg,0,[thm]); |
618 |
|
619 |
|
620 (*** Meta rules ***) |
|
621 |
567 |
622 (** 'primitive' rules **) |
568 (** 'primitive' rules **) |
623 |
569 |
624 (*discharge all assumptions t from ts*) |
570 (*discharge all assumptions t from ts*) |
625 val disch = gen_rem (op aconv); |
571 val disch = gen_rem (op aconv); |
630 in if T<>propT then |
576 in if T<>propT then |
631 raise THM("assume: assumptions must have type prop", 0, []) |
577 raise THM("assume: assumptions must have type prop", 0, []) |
632 else if maxidx <> ~1 then |
578 else if maxidx <> ~1 then |
633 raise THM("assume: assumptions may not contain scheme variables", |
579 raise THM("assume: assumptions may not contain scheme variables", |
634 maxidx, []) |
580 maxidx, []) |
635 else fix_shyps [] [] |
581 else Thm{sign = sign, |
636 (Thm{sign = sign, maxidx = ~1, shyps = [], hyps = [prop], prop = prop}) |
582 der = infer_derivs (Assume ct, []), |
|
583 maxidx = ~1, |
|
584 shyps = add_term_sorts(prop,[]), |
|
585 hyps = [prop], |
|
586 prop = prop} |
637 end; |
587 end; |
638 |
588 |
639 (*Implication introduction |
589 (*Implication introduction |
640 A |- B |
590 A |- B |
641 ------- |
591 ------- |
642 A ==> B |
592 A ==> B |
643 *) |
593 *) |
644 fun implies_intr cA (thB as Thm{sign,maxidx,hyps,prop,...}) : thm = |
594 fun implies_intr cA (thB as Thm{sign,der,maxidx,hyps,prop,...}) : thm = |
645 let val {sign=signA, t=A, T, maxidx=maxidxA} = rep_cterm cA |
595 let val {sign=signA, t=A, T, maxidx=maxidxA} = rep_cterm cA |
646 in if T<>propT then |
596 in if T<>propT then |
647 raise THM("implies_intr: assumptions must have type prop", 0, [thB]) |
597 raise THM("implies_intr: assumptions must have type prop", 0, [thB]) |
648 else fix_shyps [thB] [] |
598 else fix_shyps [thB] [] |
649 (Thm{sign= Sign.merge (sign,signA), maxidx= max[maxidxA, maxidx], |
599 (Thm{sign = Sign.merge (sign,signA), |
650 shyps= [], hyps= disch(hyps,A), prop= implies$A$prop}) |
600 der = infer_derivs (Implies_intr cA, [der]), |
|
601 maxidx = max[maxidxA, maxidx], |
|
602 shyps = [], |
|
603 hyps = disch(hyps,A), |
|
604 prop = implies$A$prop}) |
651 handle TERM _ => |
605 handle TERM _ => |
652 raise THM("implies_intr: incompatible signatures", 0, [thB]) |
606 raise THM("implies_intr: incompatible signatures", 0, [thB]) |
653 end; |
607 end; |
|
608 |
654 |
609 |
655 (*Implication elimination |
610 (*Implication elimination |
656 A ==> B A |
611 A ==> B A |
657 ------------ |
612 ------------ |
658 B |
613 B |
659 *) |
614 *) |
660 fun implies_elim thAB thA : thm = |
615 fun implies_elim thAB thA : thm = |
661 let val Thm{maxidx=maxA, hyps=hypsA, prop=propA,...} = thA |
616 let val Thm{maxidx=maxA, der=derA, hyps=hypsA, prop=propA,...} = thA |
662 and Thm{sign, maxidx, hyps, prop,...} = thAB; |
617 and Thm{sign, der, maxidx, hyps, prop,...} = thAB; |
663 fun err(a) = raise THM("implies_elim: "^a, 0, [thAB,thA]) |
618 fun err(a) = raise THM("implies_elim: "^a, 0, [thAB,thA]) |
664 in case prop of |
619 in case prop of |
665 imp$A$B => |
620 imp$A$B => |
666 if imp=implies andalso A aconv propA |
621 if imp=implies andalso A aconv propA |
667 then fix_shyps [thAB, thA] [] |
622 then fix_shyps [thAB, thA] [] |
668 (Thm{sign= merge_thm_sgs(thAB,thA), |
623 (Thm{sign= merge_thm_sgs(thAB,thA), |
669 maxidx= max[maxA,maxidx], |
624 der = infer_derivs (Implies_elim, [der,derA]), |
670 shyps= [], |
625 maxidx = max[maxA,maxidx], |
671 hyps= hypsA union hyps, (*dups suppressed*) |
626 shyps = [], |
672 prop= B}) |
627 hyps = hypsA union hyps, (*dups suppressed*) |
|
628 prop = B}) |
673 else err("major premise") |
629 else err("major premise") |
674 | _ => err("major premise") |
630 | _ => err("major premise") |
675 end; |
631 end; |
676 |
632 |
677 (*Forall introduction. The Free or Var x must not be free in the hypotheses. |
633 (*Forall introduction. The Free or Var x must not be free in the hypotheses. |
678 A |
634 A |
679 ----- |
635 ----- |
680 !!x.A |
636 !!x.A |
681 *) |
637 *) |
682 fun forall_intr cx (th as Thm{sign,maxidx,hyps,prop,...}) = |
638 fun forall_intr cx (th as Thm{sign,der,maxidx,hyps,prop,...}) = |
683 let val x = term_of cx; |
639 let val x = term_of cx; |
684 fun result(a,T) = fix_shyps [th] [] |
640 fun result(a,T) = fix_shyps [th] [] |
685 (Thm{sign= sign, maxidx= maxidx, shyps= [], hyps= hyps, |
641 (Thm{sign = sign, |
686 prop= all(T) $ Abs(a, T, abstract_over (x,prop))}) |
642 der = infer_derivs (Forall_intr cx, [der]), |
|
643 maxidx = maxidx, |
|
644 shyps = [], |
|
645 hyps = hyps, |
|
646 prop = all(T) $ Abs(a, T, abstract_over (x,prop))}) |
687 in case x of |
647 in case x of |
688 Free(a,T) => |
648 Free(a,T) => |
689 if exists (apl(x, Logic.occs)) hyps |
649 if exists (apl(x, Logic.occs)) hyps |
690 then raise THM("forall_intr: variable free in assumptions", 0, [th]) |
650 then raise THM("forall_intr: variable free in assumptions", 0, [th]) |
691 else result(a,T) |
651 else result(a,T) |
717 |
680 |
718 (* Equality *) |
681 (* Equality *) |
719 |
682 |
720 (* Definition of the relation =?= *) |
683 (* Definition of the relation =?= *) |
721 val flexpair_def = fix_shyps [] [] |
684 val flexpair_def = fix_shyps [] [] |
722 (Thm{sign= Sign.proto_pure, shyps= [], hyps= [], maxidx= 0, |
685 (Thm{sign= Sign.proto_pure, |
723 prop= term_of (read_cterm Sign.proto_pure |
686 der = Infer(Axiom(pure_thy, "flexpair_def"), []), |
724 ("(?t =?= ?u) == (?t == ?u::?'a::{})", propT))}); |
687 shyps = [], |
|
688 hyps = [], |
|
689 maxidx = 0, |
|
690 prop = term_of (read_cterm Sign.proto_pure |
|
691 ("(?t =?= ?u) == (?t == ?u::?'a::{})", propT))}); |
725 |
692 |
726 (*The reflexivity rule: maps t to the theorem t==t *) |
693 (*The reflexivity rule: maps t to the theorem t==t *) |
727 fun reflexive ct = |
694 fun reflexive ct = |
728 let val {sign, t, T, maxidx} = rep_cterm ct |
695 let val {sign, t, T, maxidx} = rep_cterm ct |
729 in fix_shyps [] [] |
696 in fix_shyps [] [] |
730 (Thm{sign= sign, shyps= [], hyps= [], maxidx= maxidx, |
697 (Thm{sign= sign, |
731 prop= Logic.mk_equals(t,t)}) |
698 der = infer_derivs (Reflexive ct, []), |
|
699 shyps = [], |
|
700 hyps = [], |
|
701 maxidx = maxidx, |
|
702 prop = Logic.mk_equals(t,t)}) |
732 end; |
703 end; |
733 |
704 |
734 (*The symmetry rule |
705 (*The symmetry rule |
735 t==u |
706 t==u |
736 ---- |
707 ---- |
737 u==t |
708 u==t |
738 *) |
709 *) |
739 fun symmetric (th as Thm{sign,shyps,hyps,prop,maxidx}) = |
710 fun symmetric (th as Thm{sign,der,maxidx,shyps,hyps,prop}) = |
740 case prop of |
711 case prop of |
741 (eq as Const("==",_)) $ t $ u => |
712 (eq as Const("==",_)) $ t $ u => |
742 (*no fix_shyps*) |
713 (*no fix_shyps*) |
743 Thm{sign=sign, shyps=shyps, hyps=hyps, maxidx=maxidx, prop= eq$u$t} |
714 Thm{sign = sign, |
|
715 der = infer_derivs (Symmetric, [der]), |
|
716 maxidx = maxidx, |
|
717 shyps = shyps, |
|
718 hyps = hyps, |
|
719 prop = eq$u$t} |
744 | _ => raise THM("symmetric", 0, [th]); |
720 | _ => raise THM("symmetric", 0, [th]); |
745 |
721 |
746 (*The transitive rule |
722 (*The transitive rule |
747 t1==u u==t2 |
723 t1==u u==t2 |
748 -------------- |
724 -------------- |
749 t1==t2 |
725 t1==t2 |
750 *) |
726 *) |
751 fun transitive th1 th2 = |
727 fun transitive th1 th2 = |
752 let val Thm{maxidx=max1, hyps=hyps1, prop=prop1,...} = th1 |
728 let val Thm{der=der1, maxidx=max1, hyps=hyps1, prop=prop1,...} = th1 |
753 and Thm{maxidx=max2, hyps=hyps2, prop=prop2,...} = th2; |
729 and Thm{der=der2, maxidx=max2, hyps=hyps2, prop=prop2,...} = th2; |
754 fun err(msg) = raise THM("transitive: "^msg, 0, [th1,th2]) |
730 fun err(msg) = raise THM("transitive: "^msg, 0, [th1,th2]) |
755 in case (prop1,prop2) of |
731 in case (prop1,prop2) of |
756 ((eq as Const("==",_)) $ t1 $ u, Const("==",_) $ u' $ t2) => |
732 ((eq as Const("==",_)) $ t1 $ u, Const("==",_) $ u' $ t2) => |
757 if not (u aconv u') then err"middle term" else |
733 if not (u aconv u') then err"middle term" else |
758 fix_shyps [th1, th2] [] |
734 fix_shyps [th1, th2] [] |
759 (Thm{sign= merge_thm_sgs(th1,th2), shyps= [], |
735 (Thm{sign= merge_thm_sgs(th1,th2), |
760 hyps= hyps1 union hyps2, |
736 der = infer_derivs (Transitive, [der1, der2]), |
761 maxidx= max[max1,max2], prop= eq$t1$t2}) |
737 maxidx = max[max1,max2], |
|
738 shyps = [], |
|
739 hyps = hyps1 union hyps2, |
|
740 prop = eq$t1$t2}) |
762 | _ => err"premises" |
741 | _ => err"premises" |
763 end; |
742 end; |
764 |
743 |
765 (*Beta-conversion: maps (%x.t)(u) to the theorem (%x.t)(u) == t[u/x] *) |
744 (*Beta-conversion: maps (%x.t)(u) to the theorem (%x.t)(u) == t[u/x] *) |
766 fun beta_conversion ct = |
745 fun beta_conversion ct = |
767 let val {sign, t, T, maxidx} = rep_cterm ct |
746 let val {sign, t, T, maxidx} = rep_cterm ct |
768 in case t of |
747 in case t of |
769 Abs(_,_,bodt) $ u => fix_shyps [] [] |
748 Abs(_,_,bodt) $ u => fix_shyps [] [] |
770 (Thm{sign= sign, shyps= [], hyps= [], |
749 (Thm{sign = sign, |
771 maxidx= maxidx_of_term t, |
750 der = infer_derivs (Beta_conversion ct, []), |
772 prop= Logic.mk_equals(t, subst_bounds([u],bodt))}) |
751 maxidx = maxidx_of_term t, |
|
752 shyps = [], |
|
753 hyps = [], |
|
754 prop = Logic.mk_equals(t, subst_bounds([u],bodt))}) |
773 | _ => raise THM("beta_conversion: not a redex", 0, []) |
755 | _ => raise THM("beta_conversion: not a redex", 0, []) |
774 end; |
756 end; |
775 |
757 |
776 (*The extensionality rule (proviso: x not free in f, g, or hypotheses) |
758 (*The extensionality rule (proviso: x not free in f, g, or hypotheses) |
777 f(x) == g(x) |
759 f(x) == g(x) |
778 ------------ |
760 ------------ |
779 f == g |
761 f == g |
780 *) |
762 *) |
781 fun extensional (th as Thm{sign,maxidx,shyps,hyps,prop}) = |
763 fun extensional (th as Thm{sign, der, maxidx,shyps,hyps,prop}) = |
782 case prop of |
764 case prop of |
783 (Const("==",_)) $ (f$x) $ (g$y) => |
765 (Const("==",_)) $ (f$x) $ (g$y) => |
784 let fun err(msg) = raise THM("extensional: "^msg, 0, [th]) |
766 let fun err(msg) = raise THM("extensional: "^msg, 0, [th]) |
785 in (if x<>y then err"different variables" else |
767 in (if x<>y then err"different variables" else |
786 case y of |
768 case y of |
825 f==g t==u |
815 f==g t==u |
826 ------------ |
816 ------------ |
827 f(t)==g(u) |
817 f(t)==g(u) |
828 *) |
818 *) |
829 fun combination th1 th2 = |
819 fun combination th1 th2 = |
830 let val Thm{maxidx=max1, shyps=shyps1, hyps=hyps1, prop=prop1,...} = th1 |
820 let val Thm{der=der1, maxidx=max1, shyps=shyps1, hyps=hyps1, |
831 and Thm{maxidx=max2, shyps=shyps2, hyps=hyps2, prop=prop2,...} = th2 |
821 prop=prop1,...} = th1 |
|
822 and Thm{der=der2, maxidx=max2, shyps=shyps2, hyps=hyps2, |
|
823 prop=prop2,...} = th2 |
832 in case (prop1,prop2) of |
824 in case (prop1,prop2) of |
833 (Const("==",_) $ f $ g, Const("==",_) $ t $ u) => |
825 (Const("==",_) $ f $ g, Const("==",_) $ t $ u) => |
834 let val thm = (*no fix_shyps*) |
826 let val thm = (*no fix_shyps*) |
835 Thm{sign= merge_thm_sgs(th1,th2), shyps= shyps1 union shyps2, |
827 Thm{sign = merge_thm_sgs(th1,th2), |
836 hyps= hyps1 union hyps2, |
828 der = infer_derivs (Combination, [der1, der2]), |
837 maxidx= max[max1,max2], prop= Logic.mk_equals(f$t, g$u)} |
829 maxidx = max[max1,max2], |
|
830 shyps = shyps1 union shyps2, |
|
831 hyps = hyps1 union hyps2, |
|
832 prop = Logic.mk_equals(f$t, g$u)} |
838 in nodup_Vars thm "combination"; thm end |
833 in nodup_Vars thm "combination"; thm end |
839 | _ => raise THM("combination: premises", 0, [th1,th2]) |
834 | _ => raise THM("combination: premises", 0, [th1,th2]) |
|
835 end; |
|
836 |
|
837 |
|
838 (* Equality introduction |
|
839 A==>B B==>A |
|
840 -------------- |
|
841 A==B |
|
842 *) |
|
843 fun equal_intr th1 th2 = |
|
844 let val Thm{der=der1,maxidx=max1, shyps=shyps1, hyps=hyps1, |
|
845 prop=prop1,...} = th1 |
|
846 and Thm{der=der2, maxidx=max2, shyps=shyps2, hyps=hyps2, |
|
847 prop=prop2,...} = th2; |
|
848 fun err(msg) = raise THM("equal_intr: "^msg, 0, [th1,th2]) |
|
849 in case (prop1,prop2) of |
|
850 (Const("==>",_) $ A $ B, Const("==>",_) $ B' $ A') => |
|
851 if A aconv A' andalso B aconv B' |
|
852 then |
|
853 (*no fix_shyps*) |
|
854 Thm{sign = merge_thm_sgs(th1,th2), |
|
855 der = infer_derivs (Equal_intr, [der1, der2]), |
|
856 maxidx = max[max1,max2], |
|
857 shyps = shyps1 union shyps2, |
|
858 hyps = hyps1 union hyps2, |
|
859 prop = Logic.mk_equals(A,B)} |
|
860 else err"not equal" |
|
861 | _ => err"premises" |
840 end; |
862 end; |
841 |
863 |
842 |
864 |
843 (*The equal propositions rule |
865 (*The equal propositions rule |
844 A==B A |
866 A==B A |
845 --------- |
867 --------- |
846 B |
868 B |
847 *) |
869 *) |
848 fun equal_elim th1 th2 = |
870 fun equal_elim th1 th2 = |
849 let val Thm{maxidx=max1, hyps=hyps1, prop=prop1,...} = th1 |
871 let val Thm{der=der1, maxidx=max1, hyps=hyps1, prop=prop1,...} = th1 |
850 and Thm{maxidx=max2, hyps=hyps2, prop=prop2,...} = th2; |
872 and Thm{der=der2, maxidx=max2, hyps=hyps2, prop=prop2,...} = th2; |
851 fun err(msg) = raise THM("equal_elim: "^msg, 0, [th1,th2]) |
873 fun err(msg) = raise THM("equal_elim: "^msg, 0, [th1,th2]) |
852 in case prop1 of |
874 in case prop1 of |
853 Const("==",_) $ A $ B => |
875 Const("==",_) $ A $ B => |
854 if not (prop2 aconv A) then err"not equal" else |
876 if not (prop2 aconv A) then err"not equal" else |
855 fix_shyps [th1, th2] [] |
877 fix_shyps [th1, th2] [] |
856 (Thm{sign= merge_thm_sgs(th1,th2), shyps= [], |
878 (Thm{sign= merge_thm_sgs(th1,th2), |
857 hyps= hyps1 union hyps2, |
879 der = infer_derivs (Equal_elim, [der1, der2]), |
858 maxidx= max[max1,max2], prop= B}) |
880 maxidx = max[max1,max2], |
|
881 shyps = [], |
|
882 hyps = hyps1 union hyps2, |
|
883 prop = B}) |
859 | _ => err"major premise" |
884 | _ => err"major premise" |
860 end; |
885 end; |
861 |
|
862 |
|
863 (* Equality introduction |
|
864 A==>B B==>A |
|
865 -------------- |
|
866 A==B |
|
867 *) |
|
868 fun equal_intr th1 th2 = |
|
869 let val Thm{maxidx=max1, shyps=shyps1, hyps=hyps1, prop=prop1,...} = th1 |
|
870 and Thm{maxidx=max2, shyps=shyps2, hyps=hyps2, prop=prop2,...} = th2; |
|
871 fun err(msg) = raise THM("equal_intr: "^msg, 0, [th1,th2]) |
|
872 in case (prop1,prop2) of |
|
873 (Const("==>",_) $ A $ B, Const("==>",_) $ B' $ A') => |
|
874 if A aconv A' andalso B aconv B' |
|
875 then |
|
876 (*no fix_shyps*) |
|
877 Thm{sign= merge_thm_sgs(th1,th2), shyps= shyps1 union shyps2, |
|
878 hyps= hyps1 union hyps2, |
|
879 maxidx= max[max1,max2], prop= Logic.mk_equals(A,B)} |
|
880 else err"not equal" |
|
881 | _ => err"premises" |
|
882 end; |
|
883 |
886 |
884 |
887 |
885 |
888 |
886 (**** Derived rules ****) |
889 (**** Derived rules ****) |
887 |
890 |
888 (*Discharge all hypotheses. Need not verify cterms or call fix_shyps. |
891 (*Discharge all hypotheses. Need not verify cterms or call fix_shyps. |
889 Repeated hypotheses are discharged only once; fold cannot do this*) |
892 Repeated hypotheses are discharged only once; fold cannot do this*) |
890 fun implies_intr_hyps (Thm{sign, maxidx, shyps, hyps=A::As, prop}) = |
893 fun implies_intr_hyps (Thm{sign, der, maxidx, shyps, hyps=A::As, prop}) = |
891 implies_intr_hyps (*no fix_shyps*) |
894 implies_intr_hyps (*no fix_shyps*) |
892 (Thm{sign=sign, maxidx=maxidx, shyps=shyps, |
895 (Thm{sign = sign, |
893 hyps= disch(As,A), prop= implies$A$prop}) |
896 der = infer_derivs (Implies_intr_hyps, [der]), |
|
897 maxidx = maxidx, |
|
898 shyps = shyps, |
|
899 hyps = disch(As,A), |
|
900 prop = implies$A$prop}) |
894 | implies_intr_hyps th = th; |
901 | implies_intr_hyps th = th; |
895 |
902 |
896 (*Smash" unifies the list of term pairs leaving no flex-flex pairs. |
903 (*Smash" unifies the list of term pairs leaving no flex-flex pairs. |
897 Instantiates the theorem and deletes trivial tpairs. |
904 Instantiates the theorem and deletes trivial tpairs. |
898 Resulting sequence may contain multiple elements if the tpairs are |
905 Resulting sequence may contain multiple elements if the tpairs are |
899 not all flex-flex. *) |
906 not all flex-flex. *) |
900 fun flexflex_rule (th as Thm{sign,maxidx,hyps,prop,...}) = |
907 fun flexflex_rule (th as Thm{sign, der, maxidx, hyps, prop,...}) = |
901 let fun newthm env = |
908 let fun newthm env = |
|
909 if Envir.is_empty env then th |
|
910 else |
902 let val (tpairs,horn) = |
911 let val (tpairs,horn) = |
903 Logic.strip_flexpairs (Envir.norm_term env prop) |
912 Logic.strip_flexpairs (Envir.norm_term env prop) |
904 (*Remove trivial tpairs, of the form t=t*) |
913 (*Remove trivial tpairs, of the form t=t*) |
905 val distpairs = filter (not o op aconv) tpairs |
914 val distpairs = filter (not o op aconv) tpairs |
906 val newprop = Logic.list_flexpairs(distpairs, horn) |
915 val newprop = Logic.list_flexpairs(distpairs, horn) |
907 in fix_shyps [th] (env_codT env) |
916 in fix_shyps [th] (env_codT env) |
908 (Thm{sign= sign, shyps= [], hyps= hyps, |
917 (Thm{sign = sign, |
909 maxidx= maxidx_of_term newprop, prop= newprop}) |
918 der = infer_derivs (Flexflex_rule env, [der]), |
|
919 maxidx = maxidx_of_term newprop, |
|
920 shyps = [], |
|
921 hyps = hyps, |
|
922 prop = newprop}) |
910 end; |
923 end; |
911 val (tpairs,_) = Logic.strip_flexpairs prop |
924 val (tpairs,_) = Logic.strip_flexpairs prop |
912 in Sequence.maps newthm |
925 in Sequence.maps newthm |
913 (Unify.smash_unifiers(sign, Envir.empty maxidx, tpairs)) |
926 (Unify.smash_unifiers(sign, Envir.empty maxidx, tpairs)) |
914 end; |
927 end; |
964 fun trivial ct : thm = |
982 fun trivial ct : thm = |
965 let val {sign, t=A, T, maxidx} = rep_cterm ct |
983 let val {sign, t=A, T, maxidx} = rep_cterm ct |
966 in if T<>propT then |
984 in if T<>propT then |
967 raise THM("trivial: the term must have type prop", 0, []) |
985 raise THM("trivial: the term must have type prop", 0, []) |
968 else fix_shyps [] [] |
986 else fix_shyps [] [] |
969 (Thm{sign= sign, maxidx= maxidx, shyps= [], hyps= [], |
987 (Thm{sign = sign, |
970 prop= implies$A$A}) |
988 der = infer_derivs (Trivial ct, []), |
|
989 maxidx = maxidx, |
|
990 shyps = [], |
|
991 hyps = [], |
|
992 prop = implies$A$A}) |
971 end; |
993 end; |
972 |
994 |
973 (*Axiom-scheme reflecting signature contents: "OFCLASS(?'a::c, c_class)" *) |
995 (*Axiom-scheme reflecting signature contents: "OFCLASS(?'a::c, c_class)" *) |
974 fun class_triv thy c = |
996 fun class_triv thy c = |
975 let |
997 let val sign = sign_of thy; |
976 val sign = sign_of thy; |
998 val Cterm {t, maxidx, ...} = |
977 val Cterm {t, maxidx, ...} = |
999 cterm_of sign (Logic.mk_inclass (TVar (("'a", 0), [c]), c)) |
978 cterm_of sign (Logic.mk_inclass (TVar (("'a", 0), [c]), c)) |
1000 handle TERM (msg, _) => raise THM ("class_triv: " ^ msg, 0, []); |
979 handle TERM (msg, _) => raise THM ("class_triv: " ^ msg, 0, []); |
|
980 in |
1001 in |
981 fix_shyps [] [] |
1002 fix_shyps [] [] |
982 (Thm {sign = sign, maxidx = maxidx, shyps = [], hyps = [], prop = t}) |
1003 (Thm {sign = sign, |
|
1004 der = infer_derivs (Class_triv(thy,c), []), |
|
1005 maxidx = maxidx, |
|
1006 shyps = [], |
|
1007 hyps = [], |
|
1008 prop = t}) |
983 end; |
1009 end; |
984 |
1010 |
985 |
1011 |
986 (* Replace all TFrees not in the hyps by new TVars *) |
1012 (* Replace all TFrees not in the hyps by new TVars *) |
987 fun varifyT(Thm{sign,maxidx,shyps,hyps,prop}) = |
1013 fun varifyT(Thm{sign,der,maxidx,shyps,hyps,prop}) = |
988 let val tfrees = foldr add_term_tfree_names (hyps,[]) |
1014 let val tfrees = foldr add_term_tfree_names (hyps,[]) |
989 in (*no fix_shyps*) |
1015 in (*no fix_shyps*) |
990 Thm{sign=sign, maxidx=max[0,maxidx], shyps=shyps, hyps=hyps, |
1016 Thm{sign = sign, |
991 prop= Type.varify(prop,tfrees)} |
1017 der = infer_derivs (VarifyT, [der]), |
|
1018 maxidx = max[0,maxidx], |
|
1019 shyps = shyps, |
|
1020 hyps = hyps, |
|
1021 prop = Type.varify(prop,tfrees)} |
992 end; |
1022 end; |
993 |
1023 |
994 (* Replace all TVars by new TFrees *) |
1024 (* Replace all TVars by new TFrees *) |
995 fun freezeT(Thm{sign,maxidx,shyps,hyps,prop}) = |
1025 fun freezeT(Thm{sign,der,maxidx,shyps,hyps,prop}) = |
996 let val prop' = Type.freeze prop |
1026 let val prop' = Type.freeze prop |
997 in (*no fix_shyps*) |
1027 in (*no fix_shyps*) |
998 Thm{sign=sign, maxidx=maxidx_of_term prop', shyps=shyps, hyps=hyps, |
1028 Thm{sign = sign, |
999 prop=prop'} |
1029 der = infer_derivs (FreezeT, [der]), |
|
1030 maxidx = maxidx_of_term prop', |
|
1031 shyps = shyps, |
|
1032 hyps = hyps, |
|
1033 prop = prop'} |
1000 end; |
1034 end; |
1001 |
1035 |
1002 |
1036 |
1003 (*** Inference rules for tactics ***) |
1037 (*** Inference rules for tactics ***) |
1004 |
1038 |
1012 handle TERM _ => raise THM("dest_state", i, [state]); |
1046 handle TERM _ => raise THM("dest_state", i, [state]); |
1013 |
1047 |
1014 (*Increment variables and parameters of orule as required for |
1048 (*Increment variables and parameters of orule as required for |
1015 resolution with goal i of state. *) |
1049 resolution with goal i of state. *) |
1016 fun lift_rule (state, i) orule = |
1050 fun lift_rule (state, i) orule = |
1017 let val Thm{shyps=sshyps,prop=sprop,maxidx=smax,...} = state; |
1051 let val Thm{shyps=sshyps, prop=sprop, maxidx=smax, sign=ssign,...} = state |
1018 val (Bi::_, _) = Logic.strip_prems(i, [], Logic.skip_flexpairs sprop) |
1052 val (Bi::_, _) = Logic.strip_prems(i, [], Logic.skip_flexpairs sprop) |
1019 handle TERM _ => raise THM("lift_rule", i, [orule,state]); |
1053 handle TERM _ => raise THM("lift_rule", i, [orule,state]) |
1020 val (lift_abs,lift_all) = Logic.lift_fns(Bi,smax+1); |
1054 val ct_Bi = Cterm {sign=ssign, maxidx=smax, T=propT, t=Bi} |
1021 val (Thm{sign,maxidx,shyps,hyps,prop}) = orule |
1055 val (lift_abs,lift_all) = Logic.lift_fns(Bi,smax+1) |
|
1056 val (Thm{sign, der, maxidx,shyps,hyps,prop}) = orule |
1022 val (tpairs,As,B) = Logic.strip_horn prop |
1057 val (tpairs,As,B) = Logic.strip_horn prop |
1023 in (*no fix_shyps*) |
1058 in (*no fix_shyps*) |
1024 Thm{hyps=hyps, sign= merge_thm_sgs(state,orule), |
1059 Thm{sign = merge_thm_sgs(state,orule), |
1025 shyps=sshyps union shyps, maxidx= maxidx+smax+1, |
1060 der = infer_derivs (Lift_rule(ct_Bi, i), [der]), |
1026 prop= Logic.rule_of(map (pairself lift_abs) tpairs, |
1061 maxidx = maxidx+smax+1, |
1027 map lift_all As, lift_all B)} |
1062 shyps=sshyps union shyps, |
|
1063 hyps=hyps, |
|
1064 prop = Logic.rule_of (map (pairself lift_abs) tpairs, |
|
1065 map lift_all As, |
|
1066 lift_all B)} |
1028 end; |
1067 end; |
1029 |
1068 |
1030 (*Solve subgoal Bi of proof state B1...Bn/C by assumption. *) |
1069 (*Solve subgoal Bi of proof state B1...Bn/C by assumption. *) |
1031 fun assumption i state = |
1070 fun assumption i state = |
1032 let val Thm{sign,maxidx,hyps,prop,...} = state; |
1071 let val Thm{sign,der,maxidx,hyps,prop,...} = state; |
1033 val (tpairs, Bs, Bi, C) = dest_state(state,i) |
1072 val (tpairs, Bs, Bi, C) = dest_state(state,i) |
1034 fun newth (env as Envir.Envir{maxidx, ...}, tpairs) = |
1073 fun newth (env as Envir.Envir{maxidx, ...}, tpairs) = |
1035 fix_shyps [state] (env_codT env) |
1074 fix_shyps [state] (env_codT env) |
1036 (Thm{sign=sign, shyps=[], hyps=hyps, maxidx=maxidx, prop= |
1075 (Thm{sign = sign, |
1037 if Envir.is_empty env then (*avoid wasted normalizations*) |
1076 der = infer_derivs (Assumption (i, Some env), [der]), |
1038 Logic.rule_of (tpairs, Bs, C) |
1077 maxidx = maxidx, |
1039 else (*normalize the new rule fully*) |
1078 shyps = [], |
1040 Envir.norm_term env (Logic.rule_of (tpairs, Bs, C))}); |
1079 hyps = hyps, |
|
1080 prop = |
|
1081 if Envir.is_empty env then (*avoid wasted normalizations*) |
|
1082 Logic.rule_of (tpairs, Bs, C) |
|
1083 else (*normalize the new rule fully*) |
|
1084 Envir.norm_term env (Logic.rule_of (tpairs, Bs, C))}); |
1041 fun addprfs [] = Sequence.null |
1085 fun addprfs [] = Sequence.null |
1042 | addprfs ((t,u)::apairs) = Sequence.seqof (fn()=> Sequence.pull |
1086 | addprfs ((t,u)::apairs) = Sequence.seqof (fn()=> Sequence.pull |
1043 (Sequence.mapp newth |
1087 (Sequence.mapp newth |
1044 (Unify.unifiers(sign,Envir.empty maxidx, (t,u)::tpairs)) |
1088 (Unify.unifiers(sign,Envir.empty maxidx, (t,u)::tpairs)) |
1045 (addprfs apairs))) |
1089 (addprfs apairs))) |
1046 in addprfs (Logic.assum_pairs Bi) end; |
1090 in addprfs (Logic.assum_pairs Bi) end; |
1047 |
1091 |
1048 (*Solve subgoal Bi of proof state B1...Bn/C by assumption. |
1092 (*Solve subgoal Bi of proof state B1...Bn/C by assumption. |
1049 Checks if Bi's conclusion is alpha-convertible to one of its assumptions*) |
1093 Checks if Bi's conclusion is alpha-convertible to one of its assumptions*) |
1050 fun eq_assumption i state = |
1094 fun eq_assumption i state = |
1051 let val Thm{sign,maxidx,hyps,prop,...} = state; |
1095 let val Thm{sign,der,maxidx,hyps,prop,...} = state; |
1052 val (tpairs, Bs, Bi, C) = dest_state(state,i) |
1096 val (tpairs, Bs, Bi, C) = dest_state(state,i) |
1053 in if exists (op aconv) (Logic.assum_pairs Bi) |
1097 in if exists (op aconv) (Logic.assum_pairs Bi) |
1054 then fix_shyps [state] [] |
1098 then fix_shyps [state] [] |
1055 (Thm{sign=sign, shyps=[], hyps=hyps, maxidx=maxidx, |
1099 (Thm{sign = sign, |
1056 prop=Logic.rule_of(tpairs, Bs, C)}) |
1100 der = infer_derivs (Assumption (i,None), [der]), |
|
1101 maxidx = maxidx, |
|
1102 shyps = [], |
|
1103 hyps = hyps, |
|
1104 prop = Logic.rule_of(tpairs, Bs, C)}) |
1057 else raise THM("eq_assumption", 0, [state]) |
1105 else raise THM("eq_assumption", 0, [state]) |
1058 end; |
1106 end; |
1059 |
1107 |
1060 |
1108 |
1061 (** User renaming of parameters in a subgoal **) |
1109 (** User renaming of parameters in a subgoal **) |
1492 val insts = Pattern.match (#tsig(Sign.rep_sg signt)) (rlhs,etat) |
1551 val insts = Pattern.match (#tsig(Sign.rep_sg signt)) (rlhs,etat) |
1493 val prop' = ren_inst(insts,rprop,rlhs,t); |
1552 val prop' = ren_inst(insts,rprop,rlhs,t); |
1494 val hyps' = hyps union hypst; |
1553 val hyps' = hyps union hypst; |
1495 val shyps' = add_insts_sorts (insts, shyps union shypst); |
1554 val shyps' = add_insts_sorts (insts, shyps union shypst); |
1496 val maxidx' = maxidx_of_term prop' |
1555 val maxidx' = maxidx_of_term prop' |
1497 val thm' = Thm{sign=signt, shyps=shyps', hyps=hyps', |
1556 val ct' = Cterm{sign = signt, (*used for deriv only*) |
1498 prop=prop', maxidx=maxidx'} |
1557 t = prop', |
|
1558 T = propT, |
|
1559 maxidx = maxidx'} |
|
1560 val der' = infer_derivs (RewriteC ct', [der]) |
|
1561 val thm' = Thm{sign = signt, |
|
1562 der = der', |
|
1563 shyps = shyps', |
|
1564 hyps = hyps', |
|
1565 prop = prop', |
|
1566 maxidx = maxidx'} |
1499 val (lhs',rhs') = Logic.dest_equals(Logic.strip_imp_concl prop') |
1567 val (lhs',rhs') = Logic.dest_equals(Logic.strip_imp_concl prop') |
1500 in if perm andalso not(termless(rhs',lhs')) then None else |
1568 in if perm andalso not(termless(rhs',lhs')) then None else |
1501 if Logic.count_prems(prop',0) = 0 |
1569 if Logic.count_prems(prop',0) = 0 |
1502 then (trace_thm "Rewriting:" thm'; Some(shyps',hyps',maxidx',rhs')) |
1570 then (trace_thm "Rewriting:" thm'; |
|
1571 Some(shyps', hyps', maxidx', rhs', der'::ders)) |
1503 else (trace_thm "Trying to rewrite:" thm'; |
1572 else (trace_thm "Trying to rewrite:" thm'; |
1504 case prover mss thm' of |
1573 case prover mss thm' of |
1505 None => (trace_thm "FAILED" thm'; None) |
1574 None => (trace_thm "FAILED" thm'; None) |
1506 | Some(thm2) => check_conv(thm2,prop')) |
1575 | Some(thm2) => check_conv(thm2,prop',ders)) |
1507 end |
1576 end |
1508 |
1577 |
1509 fun rews [] = None |
1578 fun rews [] = None |
1510 | rews (rrule::rrules) = |
1579 | rews (rrule::rrules) = |
1511 let val opt = rew rrule handle Pattern.MATCH => None |
1580 let val opt = rew rrule handle Pattern.MATCH => None |
1512 in case opt of None => rews rrules | some => some end; |
1581 in case opt of None => rews rrules | some => some end; |
1513 |
1582 |
1514 in case etat of |
1583 in case etat of |
1515 Abs(_,_,body) $ u => Some(shypst, hypst, maxidxt, subst_bounds([u], body)) |
1584 Abs(_,_,body) $ u => Some(shypst, hypst, maxidxt, |
|
1585 subst_bounds([u], body), |
|
1586 ders) |
1516 | _ => rews(Net.match_term net etat) |
1587 | _ => rews(Net.match_term net etat) |
1517 end; |
1588 end; |
1518 |
1589 |
1519 (*Conversion to apply a congruence rule to a term*) |
1590 (*Conversion to apply a congruence rule to a term*) |
1520 fun congc (prover,signt) {thm=cong,lhs=lhs} (shypst,hypst,maxidxt,t) = |
1591 fun congc (prover,signt) {thm=cong,lhs=lhs} (shypst,hypst,maxidxt,t,ders) = |
1521 let val Thm{sign,shyps,hyps,maxidx,prop,...} = cong |
1592 let val Thm{sign,der,shyps,hyps,maxidx,prop,...} = cong |
1522 val unit = if Sign.subsig(sign,signt) then () |
1593 val unit = if Sign.subsig(sign,signt) then () |
1523 else error("Congruence rule from different theory") |
1594 else error("Congruence rule from different theory") |
1524 val tsig = #tsig(Sign.rep_sg signt) |
1595 val tsig = #tsig(Sign.rep_sg signt) |
1525 val rprop = if maxidxt = ~1 then prop |
1596 val rprop = if maxidxt = ~1 then prop |
1526 else Logic.incr_indexes([],maxidxt+1) prop; |
1597 else Logic.incr_indexes([],maxidxt+1) prop; |
1527 val rlhs = if maxidxt = ~1 then lhs |
1598 val rlhs = if maxidxt = ~1 then lhs |
1528 else fst(Logic.dest_equals(Logic.strip_imp_concl rprop)) |
1599 else fst(Logic.dest_equals(Logic.strip_imp_concl rprop)) |
1529 val insts = Pattern.match tsig (rlhs,t) handle Pattern.MATCH => |
1600 val insts = Pattern.match tsig (rlhs,t) handle Pattern.MATCH => |
1530 error("Congruence rule did not match") |
1601 error("Congruence rule did not match") |
1531 val prop' = ren_inst(insts,rprop,rlhs,t); |
1602 val prop' = ren_inst(insts,rprop,rlhs,t); |
1532 val shyps' = add_insts_sorts (insts, shyps union shypst); |
1603 val shyps' = add_insts_sorts (insts, shyps union shypst) |
1533 val thm' = Thm{sign=signt, shyps=shyps', hyps=hyps union hypst, |
1604 val maxidx' = maxidx_of_term prop' |
1534 prop=prop', maxidx=maxidx_of_term prop'}; |
1605 val ct' = Cterm{sign = signt, (*used for deriv only*) |
|
1606 t = prop', |
|
1607 T = propT, |
|
1608 maxidx = maxidx'} |
|
1609 val thm' = Thm{sign = signt, |
|
1610 der = infer_derivs (CongC ct', [der]), |
|
1611 shyps = shyps', |
|
1612 hyps = hyps union hypst, |
|
1613 prop = prop', |
|
1614 maxidx = maxidx'}; |
1535 val unit = trace_thm "Applying congruence rule" thm'; |
1615 val unit = trace_thm "Applying congruence rule" thm'; |
1536 fun err() = error("Failed congruence proof!") |
1616 fun err() = error("Failed congruence proof!") |
1537 |
1617 |
1538 in case prover thm' of |
1618 in case prover thm' of |
1539 None => err() |
1619 None => err() |
1540 | Some(thm2) => (case check_conv(thm2,prop') of |
1620 | Some(thm2) => (case check_conv(thm2,prop',ders) of |
1541 None => err() | some => some) |
1621 None => err() | some => some) |
1542 end; |
1622 end; |
1543 |
1623 |
1544 |
1624 |
1545 |
1625 |
1546 fun bottomc ((simprem,useprem),prover,sign) = |
1626 fun bottomc ((simprem,useprem),prover,sign) = |
1547 let fun botc fail mss trec = |
1627 let fun botc fail mss trec = |
1548 (case subc mss trec of |
1628 (case subc mss trec of |
1549 some as Some(trec1) => |
1629 some as Some(trec1) => |
1550 (case rewritec (prover,sign) mss trec1 of |
1630 (case rewritec (prover,sign) mss trec1 of |
1551 Some(trec2) => botc false mss trec2 |
1631 Some(trec2) => botc false mss trec2 |
1552 | None => some) |
1632 | None => some) |
1553 | None => |
1633 | None => |
1554 (case rewritec (prover,sign) mss trec of |
1634 (case rewritec (prover,sign) mss trec of |
1555 Some(trec2) => botc false mss trec2 |
1635 Some(trec2) => botc false mss trec2 |
1556 | None => if fail then None else Some(trec))) |
1636 | None => if fail then None else Some(trec))) |
1557 |
1637 |
1558 and try_botc mss trec = (case botc true mss trec of |
1638 and try_botc mss trec = (case botc true mss trec of |
1559 Some(trec1) => trec1 |
1639 Some(trec1) => trec1 |
1560 | None => trec) |
1640 | None => trec) |
1561 |
1641 |
1562 and subc (mss as Mss{net,congs,bounds,prems,mk_rews}) |
1642 and subc (mss as Mss{net,congs,bounds,prems,mk_rews}) |
1563 (trec as (shyps,hyps,maxidx,t)) = |
1643 (trec as (shyps,hyps,maxidx,t0,ders)) = |
1564 (case t of |
1644 (case t0 of |
1565 Abs(a,T,t) => |
1645 Abs(a,T,t) => |
1566 let val b = variant bounds a |
1646 let val b = variant bounds a |
1567 val v = Free("." ^ b,T) |
1647 val v = Free("." ^ b,T) |
1568 val mss' = Mss{net=net, congs=congs, bounds=b::bounds, |
1648 val mss' = Mss{net=net, congs=congs, bounds=b::bounds, |
1569 prems=prems,mk_rews=mk_rews} |
1649 prems=prems,mk_rews=mk_rews} |
1570 in case botc true mss' (shyps,hyps,maxidx,subst_bounds([v],t)) of |
1650 in case botc true mss' |
1571 Some(shyps',hyps',maxidx',t') => |
1651 (shyps,hyps,maxidx,subst_bounds([v],t),ders) of |
1572 Some(shyps', hyps', maxidx', Abs(a, T, abstract_over(v,t'))) |
1652 Some(shyps',hyps',maxidx',t',ders') => |
1573 | None => None |
1653 Some(shyps', hyps', maxidx', |
1574 end |
1654 Abs(a, T, abstract_over(v,t')), |
1575 | t$u => (case t of |
1655 ders') |
1576 Const("==>",_)$s => Some(impc(shyps,hyps,maxidx,s,u,mss)) |
1656 | None => None |
1577 | Abs(_,_,body) => |
1657 end |
1578 let val trec = (shyps,hyps,maxidx,subst_bounds([u], body)) |
1658 | t$u => (case t of |
1579 in case subc mss trec of |
1659 Const("==>",_)$s => Some(impc(shyps,hyps,maxidx,s,u,mss,ders)) |
1580 None => Some(trec) |
1660 | Abs(_,_,body) => |
1581 | trec => trec |
1661 let val trec = (shyps,hyps,maxidx,subst_bounds([u],body),ders) |
1582 end |
1662 in case subc mss trec of |
1583 | _ => |
1663 None => Some(trec) |
1584 let fun appc() = |
1664 | trec => trec |
1585 (case botc true mss (shyps,hyps,maxidx,t) of |
1665 end |
1586 Some(shyps1,hyps1,maxidx1,t1) => |
1666 | _ => |
1587 (case botc true mss (shyps1,hyps1,maxidx,u) of |
1667 let fun appc() = |
1588 Some(shyps2,hyps2,maxidx2,u1) => |
1668 (case botc true mss (shyps,hyps,maxidx,t,ders) of |
1589 Some(shyps2,hyps2,max[maxidx1,maxidx2],t1$u1) |
1669 Some(shyps1,hyps1,maxidx1,t1,ders1) => |
1590 | None => |
1670 (case botc true mss (shyps1,hyps1,maxidx,u,ders1) of |
1591 Some(shyps1,hyps1,max[maxidx1,maxidx],t1$u)) |
1671 Some(shyps2,hyps2,maxidx2,u1,ders2) => |
1592 | None => |
1672 Some(shyps2, hyps2, max[maxidx1,maxidx2], |
1593 (case botc true mss (shyps,hyps,maxidx,u) of |
1673 t1$u1, ders2) |
1594 Some(shyps1,hyps1,maxidx1,u1) => |
1674 | None => |
1595 Some(shyps1,hyps1,max[maxidx,maxidx1],t$u1) |
1675 Some(shyps1, hyps1, max[maxidx1,maxidx], t1$u, |
1596 | None => None)) |
1676 ders1)) |
1597 val (h,ts) = strip_comb t |
1677 | None => |
1598 in case h of |
1678 (case botc true mss (shyps,hyps,maxidx,u,ders) of |
1599 Const(a,_) => |
1679 Some(shyps1,hyps1,maxidx1,u1,ders1) => |
1600 (case assoc(congs,a) of |
1680 Some(shyps1, hyps1, max[maxidx,maxidx1], |
1601 None => appc() |
1681 t$u1, ders1) |
1602 | Some(cong) => congc (prover mss,sign) cong trec) |
1682 | None => None)) |
1603 | _ => appc() |
1683 val (h,ts) = strip_comb t |
1604 end) |
1684 in case h of |
1605 | _ => None) |
1685 Const(a,_) => |
1606 |
1686 (case assoc(congs,a) of |
1607 and impc(shyps,hyps,maxidx,s,u,mss as Mss{mk_rews,...}) = |
1687 None => appc() |
1608 let val (shyps1,hyps1,_,s1) = |
1688 | Some(cong) => congc (prover mss,sign) cong trec) |
1609 if simprem then try_botc mss (shyps,hyps,maxidx,s) |
1689 | _ => appc() |
1610 else (shyps,hyps,0,s); |
1690 end) |
1611 val maxidx1 = maxidx_of_term s1 |
1691 | _ => None) |
1612 val mss1 = |
1692 |
1613 if not useprem orelse maxidx1 <> ~1 then mss |
1693 and impc(shyps, hyps, maxidx, s, u, mss as Mss{mk_rews,...}, ders) = |
1614 else let val thm = |
1694 let val (shyps1,hyps1,_,s1,ders1) = |
1615 Thm{sign=sign,shyps=add_term_sorts(s1,[]), |
1695 if simprem then try_botc mss (shyps,hyps,maxidx,s,ders) |
1616 hyps=[s1],prop=s1,maxidx= ~1} |
1696 else (shyps,hyps,0,s,ders); |
1617 in add_simps(add_prems(mss,[thm]), mk_rews thm) end |
1697 val maxidx1 = maxidx_of_term s1 |
1618 val (shyps2,hyps2,maxidx2,u1) = try_botc mss1 (shyps1,hyps1,maxidx,u) |
1698 val mss1 = |
1619 val hyps3 = if s1 mem hyps1 then hyps2 else hyps2\s1 |
1699 if not useprem orelse maxidx1 <> ~1 then mss |
1620 in (shyps2, hyps3, max[maxidx1,maxidx2], Logic.mk_implies(s1,u1)) end |
1700 else let val thm = assume (Cterm{sign=sign, t=s1, |
1621 |
1701 T=propT, maxidx=maxidx1}) |
1622 in try_botc end; |
1702 in add_simps(add_prems(mss,[thm]), mk_rews thm) end |
|
1703 val (shyps2,hyps2,maxidx2,u1,ders2) = |
|
1704 try_botc mss1 (shyps1,hyps1,maxidx,u,ders1) |
|
1705 val hyps3 = if s1 mem hyps1 then hyps2 else hyps2\s1 |
|
1706 in (shyps2, hyps3, max[maxidx1,maxidx2], |
|
1707 Logic.mk_implies(s1,u1), ders2) |
|
1708 end |
|
1709 |
|
1710 in try_botc end; |
1623 |
1711 |
1624 |
1712 |
1625 (*** Meta-rewriting: rewrites t to u and returns the theorem t==u ***) |
1713 (*** Meta-rewriting: rewrites t to u and returns the theorem t==u ***) |
1626 (* Parameters: |
1714 (* Parameters: |
1627 mode = (simplify A, use A in simplifying B) when simplifying A ==> B |
1715 mode = (simplify A, use A in simplifying B) when simplifying A ==> B |