src/Provers/trancl.ML
 changeset 32277 ff1e59a15146 parent 32215 87806301a813 child 32283 3bebc195c124
equal inserted replaced
32275:b10cbf4d3f55 32277:ff1e59a15146
`   529 in`
`   529 in`
`   530   findRtranclProof g tranclEdges subgoal`
`   530   findRtranclProof g tranclEdges subgoal`
`   531 end;`
`   531 end;`
`   532 `
`   532 `
`   533 `
`   533 `
`   534 fun trancl_tac ctxt = SUBGOAL (fn (A, n) =>`
`   534 fun trancl_tac ctxt = SUBGOAL (fn (A, n) => fn st =>`
`   535  let`
`   535  let`
`   536   val thy = ProofContext.theory_of ctxt;`
`   536   val thy = Thm.theory_of_thm st;`
`   537   val Hs = Logic.strip_assums_hyp A;`
`   537   val Hs = Logic.strip_assums_hyp A;`
`   538   val C = Logic.strip_assums_concl A;`
`   538   val C = Logic.strip_assums_concl A;`
`   539   val (rel, subgoals, prf) = mkconcl_trancl C;`
`   539   val (rel, subgoals, prf) = mkconcl_trancl C;`
`   540 `
`   540 `
`   541   val prems = flat (ListPair.map (mkasm_trancl rel) (Hs, 0 upto (length Hs - 1)));`
`   541   val prems = flat (ListPair.map (mkasm_trancl rel) (Hs, 0 upto (length Hs - 1)));`
`   542   val prfs = solveTrancl (prems, C);`
`   542   val prfs = solveTrancl (prems, C);`
`   543  in`
`   543  in`
`   544   FOCUS (fn {prems, ...} =>`
`   544   FOCUS (fn {prems, ...} =>`
`   545     let val thms = map (prove thy rel prems) prfs`
`   545     let val thms = map (prove thy rel prems) prfs`
`   546     in rtac (prove thy rel thms prf) 1 end) ctxt n`
`   546     in rtac (prove thy rel thms prf) 1 end) ctxt n st`
`   547  end`
`   547  end`
`   548  handle Cannot => no_tac);`
`   548  handle Cannot => Seq.empty);`
`   549 `
`   549 `
`   550 `
`   550 `
`   551 fun rtrancl_tac ctxt = SUBGOAL (fn (A, n) => fn st =>`
`   551 fun rtrancl_tac ctxt = SUBGOAL (fn (A, n) => fn st =>`
`   552  let`
`   552  let`
`   553   val thy = ProofContext.theory_of ctxt;`
`   553   val thy = Thm.theory_of_thm st;`
`   554   val Hs = Logic.strip_assums_hyp A;`
`   554   val Hs = Logic.strip_assums_hyp A;`
`   555   val C = Logic.strip_assums_concl A;`
`   555   val C = Logic.strip_assums_concl A;`
`   556   val (rel, subgoals, prf) = mkconcl_rtrancl C;`
`   556   val (rel, subgoals, prf) = mkconcl_rtrancl C;`
`   557 `
`   557 `
`   558   val prems = flat (ListPair.map (mkasm_rtrancl rel) (Hs, 0 upto (length Hs - 1)));`
`   558   val prems = flat (ListPair.map (mkasm_rtrancl rel) (Hs, 0 upto (length Hs - 1)));`