equal
deleted
inserted
replaced
91 Envir.beta_eta_contract rel, r)) (Cls.decomp t); |
91 Envir.beta_eta_contract rel, r)) (Cls.decomp t); |
92 |
92 |
93 fun prove thy r asms = |
93 fun prove thy r asms = |
94 let |
94 let |
95 fun inst thm = |
95 fun inst thm = |
96 let val SOME (_, _, r', _) = decomp (concl_of thm) |
96 let val SOME (_, _, r', _) = decomp (Thm.concl_of thm) |
97 in Drule.cterm_instantiate [(cterm_of thy r', cterm_of thy r)] thm end; |
97 in Drule.cterm_instantiate [(Thm.cterm_of thy r', Thm.cterm_of thy r)] thm end; |
98 fun pr (Asm i) = nth asms i |
98 fun pr (Asm i) = nth asms i |
99 | pr (Thm (prfs, thm)) = map pr prfs MRS inst thm; |
99 | pr (Thm (prfs, thm)) = map pr prfs MRS inst thm; |
100 in pr end; |
100 in pr end; |
101 |
101 |
102 |
102 |
541 val prems = flat (map_index (mkasm_trancl rel o swap) Hs); |
541 val prems = flat (map_index (mkasm_trancl rel o swap) Hs); |
542 val prfs = solveTrancl (prems, C); |
542 val prfs = solveTrancl (prems, C); |
543 in |
543 in |
544 Subgoal.FOCUS (fn {context = ctxt', prems, concl, ...} => |
544 Subgoal.FOCUS (fn {context = ctxt', prems, concl, ...} => |
545 let |
545 let |
546 val SOME (_, _, rel', _) = decomp (term_of concl); |
546 val SOME (_, _, rel', _) = decomp (Thm.term_of concl); |
547 val thms = map (prove thy rel' prems) prfs |
547 val thms = map (prove thy rel' prems) prfs |
548 in resolve_tac ctxt' [prove thy rel' thms prf] 1 end) ctxt n st |
548 in resolve_tac ctxt' [prove thy rel' thms prf] 1 end) ctxt n st |
549 end |
549 end |
550 handle Cannot => Seq.empty); |
550 handle Cannot => Seq.empty); |
551 |
551 |
560 val prems = flat (map_index (mkasm_rtrancl rel o swap) Hs); |
560 val prems = flat (map_index (mkasm_rtrancl rel o swap) Hs); |
561 val prfs = solveRtrancl (prems, C); |
561 val prfs = solveRtrancl (prems, C); |
562 in |
562 in |
563 Subgoal.FOCUS (fn {context = ctxt', prems, concl, ...} => |
563 Subgoal.FOCUS (fn {context = ctxt', prems, concl, ...} => |
564 let |
564 let |
565 val SOME (_, _, rel', _) = decomp (term_of concl); |
565 val SOME (_, _, rel', _) = decomp (Thm.term_of concl); |
566 val thms = map (prove thy rel' prems) prfs |
566 val thms = map (prove thy rel' prems) prfs |
567 in resolve_tac ctxt' [prove thy rel' thms prf] 1 end) ctxt n st |
567 in resolve_tac ctxt' [prove thy rel' thms prf] 1 end) ctxt n st |
568 end |
568 end |
569 handle Cannot => Seq.empty | General.Subscript => Seq.empty); |
569 handle Cannot => Seq.empty | General.Subscript => Seq.empty); |
570 |
570 |