src/Provers/trancl.ML
changeset 32277 ff1e59a15146
parent 32215 87806301a813
child 32283 3bebc195c124
equal deleted 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)));