src/Provers/trancl.ML
changeset 35281 206e2f1759cc
parent 33063 4d462963a7db
child 36692 54b64d4ad524
equal deleted inserted replaced
35280:54ab4921f826 35281:206e2f1759cc
   539   val (rel, subgoals, prf) = mkconcl_trancl C;
   539   val (rel, subgoals, prf) = mkconcl_trancl C;
   540 
   540 
   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 {prems, ...} =>
   544   Subgoal.FOCUS (fn {prems, concl, ...} =>
   545     let val thms = map (prove thy rel prems) prfs
   545     let
   546     in rtac (prove thy rel thms prf) 1 end) ctxt n st
   546       val SOME (_, _, rel', _) = decomp (term_of concl);
       
   547       val thms = map (prove thy rel' prems) prfs
       
   548     in rtac (prove thy rel' thms prf) 1 end) ctxt n st
   547  end
   549  end
   548  handle Cannot => Seq.empty);
   550  handle Cannot => Seq.empty);
   549 
   551 
   550 
   552 
   551 fun rtrancl_tac ctxt = SUBGOAL (fn (A, n) => fn st =>
   553 fun rtrancl_tac ctxt = SUBGOAL (fn (A, n) => fn st =>
   556   val (rel, subgoals, prf) = mkconcl_rtrancl C;
   558   val (rel, subgoals, prf) = mkconcl_rtrancl C;
   557 
   559 
   558   val prems = flat (map_index (mkasm_rtrancl rel o swap) Hs);
   560   val prems = flat (map_index (mkasm_rtrancl rel o swap) Hs);
   559   val prfs = solveRtrancl (prems, C);
   561   val prfs = solveRtrancl (prems, C);
   560  in
   562  in
   561   Subgoal.FOCUS (fn {prems, ...} =>
   563   Subgoal.FOCUS (fn {prems, concl, ...} =>
   562     let val thms = map (prove thy rel prems) prfs
   564     let
   563     in rtac (prove thy rel thms prf) 1 end) ctxt n st
   565       val SOME (_, _, rel', _) = decomp (term_of concl);
       
   566       val thms = map (prove thy rel' prems) prfs
       
   567     in rtac (prove thy rel' thms prf) 1 end) ctxt n st
   564  end
   568  end
   565  handle Cannot => Seq.empty | Subscript => Seq.empty);
   569  handle Cannot => Seq.empty | Subscript => Seq.empty);
   566 
   570 
   567 end;
   571 end;