src/Provers/trancl.ML
changeset 32283 3bebc195c124
parent 32277 ff1e59a15146
child 32285 ab9b66c2bbca
equal deleted inserted replaced
32282:853ef99c04cc 32283:3bebc195c124
   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   Subgoal.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 st
   546     in rtac (prove thy rel thms prf) 1 end) ctxt n st
   547  end
   547  end
   548  handle Cannot => Seq.empty);
   548  handle Cannot => Seq.empty);
   549 
   549 
   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)));
   559   val prfs = solveRtrancl (prems, C);
   559   val prfs = solveRtrancl (prems, C);
   560  in
   560  in
   561   FOCUS (fn {prems, ...} =>
   561   Subgoal.FOCUS (fn {prems, ...} =>
   562     let val thms = map (prove thy rel prems) prfs
   562     let val thms = map (prove thy rel prems) prfs
   563     in rtac (prove thy rel thms prf) 1 end) ctxt n st
   563     in rtac (prove thy rel thms prf) 1 end) ctxt n st
   564  end
   564  end
   565  handle Cannot => Seq.empty | Subscript => Seq.empty);
   565  handle Cannot => Seq.empty | Subscript => Seq.empty);
   566 
   566