src/Provers/trancl.ML
changeset 33063 4d462963a7db
parent 32768 e4a3f9c3d4f5
child 35281 206e2f1759cc
equal deleted inserted replaced
33062:542b34b178ec 33063:4d462963a7db
   536   val thy = ProofContext.theory_of ctxt;
   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 (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, ...} =>
   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
   553   val thy = ProofContext.theory_of ctxt;
   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 (map_index (mkasm_rtrancl rel o swap) Hs);
   559   val prfs = solveRtrancl (prems, C);
   559   val prfs = solveRtrancl (prems, C);
   560  in
   560  in
   561   Subgoal.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