src/Provers/classical.ML
changeset 7329 9053ad9a9768
parent 7302 43a0a5097701
child 7354 358b1c5391f0
equal deleted inserted replaced
7328:4265615b4206 7329:9053ad9a9768
  1155 
  1155 
  1156 (* intro / elim methods *)
  1156 (* intro / elim methods *)
  1157 
  1157 
  1158 local
  1158 local
  1159 
  1159 
  1160 fun intro_elim_tac netpair_of _ [] cs facts =
  1160 fun intro_elim_tac netpair_of res_tac rules cs facts =
  1161       Method.same_tac facts THEN'
  1161   let
  1162         (REPEAT1 o FIRST' (map (biresolve_from_nets_tac o netpair_of) (get_nets cs)))
  1162     val single_tac =
  1163   | intro_elim_tac _ res_tac rules _ facts =
  1163       if null rules then FIRST' (map (biresolve_from_nets_tac o netpair_of) (get_nets cs))
  1164       Method.same_tac facts THEN' (REPEAT1 o res_tac rules);
  1164       else res_tac rules;
       
  1165     fun multi_tac st = (single_tac THEN_ALL_NEW (TRY o (fn st => multi_tac st))) st;
       
  1166   in Method.same_tac facts THEN' multi_tac end;
  1165 
  1167 
  1166 val intro_tac = intro_elim_tac (fn (inet, _) => (inet, Net.empty)) resolve_tac;
  1168 val intro_tac = intro_elim_tac (fn (inet, _) => (inet, Net.empty)) resolve_tac;
  1167 val elim_tac = intro_elim_tac (fn (_, enet) => (Net.empty, enet)) eresolve_tac;
  1169 val elim_tac = intro_elim_tac (fn (_, enet) => (Net.empty, enet)) eresolve_tac;
  1168 
  1170 
  1169 in
  1171 in