149 val combination: thm -> thm -> thm |
149 val combination: thm -> thm -> thm |
150 val equal_intr: thm -> thm -> thm |
150 val equal_intr: thm -> thm -> thm |
151 val equal_elim: thm -> thm -> thm |
151 val equal_elim: thm -> thm -> thm |
152 val solve_constraints: thm -> thm |
152 val solve_constraints: thm -> thm |
153 val flexflex_rule: Proof.context option -> thm -> thm Seq.seq |
153 val flexflex_rule: Proof.context option -> thm -> thm Seq.seq |
154 val generalize: string list * string list -> int -> thm -> thm |
154 val generalize: Symtab.set * Symtab.set -> int -> thm -> thm |
155 val generalize_cterm: string list * string list -> int -> cterm -> cterm |
155 val generalize_cterm: Symtab.set * Symtab.set -> int -> cterm -> cterm |
156 val generalize_ctyp: string list -> int -> ctyp -> ctyp |
156 val generalize_ctyp: Symtab.set -> int -> ctyp -> ctyp |
157 val instantiate: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list -> |
157 val instantiate: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list -> |
158 thm -> thm |
158 thm -> thm |
159 val instantiate_cterm: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list -> |
159 val instantiate_cterm: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list -> |
160 cterm -> cterm |
160 cterm -> cterm |
161 val trivial: cterm -> thm |
161 val trivial: cterm -> thm |
1540 A |
1540 A |
1541 -------------------- |
1541 -------------------- |
1542 A[?'a/'a, ?x/x, ...] |
1542 A[?'a/'a, ?x/x, ...] |
1543 *) |
1543 *) |
1544 |
1544 |
1545 fun generalize ([], []) _ th = th |
1545 fun generalize (tfrees, frees) idx th = |
1546 | generalize (tfrees, frees) idx th = |
1546 if Symtab.is_empty tfrees andalso Symtab.is_empty frees then th |
1547 let |
1547 else |
1548 val Thm (der, {cert, maxidx, constraints, shyps, hyps, tpairs, prop, ...}) = th; |
1548 let |
1549 val _ = idx <= maxidx andalso raise THM ("generalize: bad index", idx, [th]); |
1549 val Thm (der, {cert, maxidx, constraints, shyps, hyps, tpairs, prop, ...}) = th; |
1550 |
1550 val _ = idx <= maxidx andalso raise THM ("generalize: bad index", idx, [th]); |
1551 val bad_type = |
1551 |
1552 if null tfrees then K false |
1552 val bad_type = |
1553 else Term.exists_subtype (fn TFree (a, _) => member (op =) tfrees a | _ => false); |
1553 if Symtab.is_empty tfrees then K false |
1554 fun bad_term (Free (x, T)) = bad_type T orelse member (op =) frees x |
1554 else Term.exists_subtype (fn TFree (a, _) => Symtab.defined tfrees a | _ => false); |
1555 | bad_term (Var (_, T)) = bad_type T |
1555 fun bad_term (Free (x, T)) = bad_type T orelse Symtab.defined frees x |
1556 | bad_term (Const (_, T)) = bad_type T |
1556 | bad_term (Var (_, T)) = bad_type T |
1557 | bad_term (Abs (_, T, t)) = bad_type T orelse bad_term t |
1557 | bad_term (Const (_, T)) = bad_type T |
1558 | bad_term (t $ u) = bad_term t orelse bad_term u |
1558 | bad_term (Abs (_, T, t)) = bad_type T orelse bad_term t |
1559 | bad_term (Bound _) = false; |
1559 | bad_term (t $ u) = bad_term t orelse bad_term u |
1560 val _ = exists bad_term hyps andalso |
1560 | bad_term (Bound _) = false; |
1561 raise THM ("generalize: variable free in assumptions", 0, [th]); |
1561 val _ = exists bad_term hyps andalso |
1562 |
1562 raise THM ("generalize: variable free in assumptions", 0, [th]); |
1563 val generalize = Term_Subst.generalize (tfrees, frees) idx; |
1563 |
1564 val prop' = generalize prop; |
1564 val generalize = Term_Subst.generalize (tfrees, frees) idx; |
1565 val tpairs' = map (apply2 generalize) tpairs; |
1565 val prop' = generalize prop; |
1566 val maxidx' = maxidx_tpairs tpairs' (maxidx_of_term prop'); |
1566 val tpairs' = map (apply2 generalize) tpairs; |
1567 in |
1567 val maxidx' = maxidx_tpairs tpairs' (maxidx_of_term prop'); |
1568 Thm (deriv_rule1 (Proofterm.generalize_proof (tfrees, frees) idx prop) der, |
1568 in |
1569 {cert = cert, |
1569 Thm (deriv_rule1 (Proofterm.generalize_proof (tfrees, frees) idx prop) der, |
1570 tags = [], |
1570 {cert = cert, |
1571 maxidx = maxidx', |
1571 tags = [], |
1572 constraints = constraints, |
1572 maxidx = maxidx', |
1573 shyps = shyps, |
1573 constraints = constraints, |
1574 hyps = hyps, |
1574 shyps = shyps, |
1575 tpairs = tpairs', |
1575 hyps = hyps, |
1576 prop = prop'}) |
1576 tpairs = tpairs', |
1577 end; |
1577 prop = prop'}) |
1578 |
1578 end; |
1579 fun generalize_cterm ([], []) _ ct = ct |
1579 |
1580 | generalize_cterm (tfrees, frees) idx (ct as Cterm {cert, t, T, maxidx, sorts}) = |
1580 fun generalize_cterm (tfrees, frees) idx (ct as Cterm {cert, t, T, maxidx, sorts}) = |
1581 if idx <= maxidx then raise CTERM ("generalize_cterm: bad index", [ct]) |
1581 if Symtab.is_empty tfrees andalso Symtab.is_empty frees then ct |
1582 else |
1582 else if idx <= maxidx then raise CTERM ("generalize_cterm: bad index", [ct]) |
1583 Cterm {cert = cert, sorts = sorts, |
1583 else |
1584 T = Term_Subst.generalizeT tfrees idx T, |
1584 Cterm {cert = cert, sorts = sorts, |
1585 t = Term_Subst.generalize (tfrees, frees) idx t, |
1585 T = Term_Subst.generalizeT tfrees idx T, |
1586 maxidx = Int.max (maxidx, idx)}; |
1586 t = Term_Subst.generalize (tfrees, frees) idx t, |
1587 |
1587 maxidx = Int.max (maxidx, idx)}; |
1588 fun generalize_ctyp [] _ cT = cT |
1588 |
1589 | generalize_ctyp tfrees idx (Ctyp {cert, T, maxidx, sorts}) = |
1589 fun generalize_ctyp tfrees idx (cT as Ctyp {cert, T, maxidx, sorts}) = |
1590 if idx <= maxidx then raise CTERM ("generalize_ctyp: bad index", []) |
1590 if Symtab.is_empty tfrees then cT |
1591 else |
1591 else if idx <= maxidx then raise CTERM ("generalize_ctyp: bad index", []) |
1592 Ctyp {cert = cert, sorts = sorts, |
1592 else |
1593 T = Term_Subst.generalizeT tfrees idx T, |
1593 Ctyp {cert = cert, sorts = sorts, |
1594 maxidx = Int.max (maxidx, idx)}; |
1594 T = Term_Subst.generalizeT tfrees idx T, |
|
1595 maxidx = Int.max (maxidx, idx)}; |
1595 |
1596 |
1596 |
1597 |
1597 (*Instantiation of schematic variables |
1598 (*Instantiation of schematic variables |
1598 A |
1599 A |
1599 -------------------- |
1600 -------------------- |