src/Provers/trancl.ML
changeset 32285 ab9b66c2bbca
parent 32283 3bebc195c124
child 32740 9dd0a2f83429
equal deleted inserted replaced
32284:d8ee8a956f19 32285:ab9b66c2bbca
   531 end;
   531 end;
   532 
   532 
   533 
   533 
   534 fun trancl_tac ctxt = SUBGOAL (fn (A, n) => fn st =>
   534 fun trancl_tac ctxt = SUBGOAL (fn (A, n) => fn st =>
   535  let
   535  let
   536   val thy = Thm.theory_of_thm st;
   536   val thy = ProofContext.theory_of ctxt;
   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)));
   548  handle Cannot => Seq.empty);
   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 = Thm.theory_of_thm st;
   553   val thy = ProofContext.theory_of ctxt;
   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)));