src/Provers/classical.ML
changeset 7425 2089c70f2c6d
parent 7354 358b1c5391f0
child 7559 1d2c099e98f7
equal deleted inserted replaced
7424:ce03b804c5e7 7425:2089c70f2c6d
  1091 
  1091 
  1092     val tac = SUBGOAL (fn (goal, i) =>
  1092     val tac = SUBGOAL (fn (goal, i) =>
  1093       let
  1093       let
  1094         val irules = find_rules (Logic.strip_assums_concl goal) nets;
  1094         val irules = find_rules (Logic.strip_assums_concl goal) nets;
  1095         val rules = erules @ irules;
  1095         val rules = erules @ irules;
  1096         val ruleq = Method.forward_chain facts rules;
  1096         val ruleq = Method.multi_resolves facts rules;
  1097       in trace rules i; fn st => Seq.flat (Seq.map (fn rule => Tactic.rtac rule i st) ruleq) end);
  1097       in trace rules i; fn st => Seq.flat (Seq.map (fn rule => Tactic.rtac rule i st) ruleq) end);
  1098   in tac end;
  1098   in tac end;
  1099 
  1099 
  1100 fun rule_tac [] cs facts = some_rule_tac cs facts
  1100 fun rule_tac [] cs facts = some_rule_tac cs facts
  1101   | rule_tac rules _ facts = Method.rule_tac rules facts;
  1101   | rule_tac rules _ facts = Method.rule_tac rules facts;
  1113   let
  1113   let
  1114     val single_tac =
  1114     val single_tac =
  1115       if null rules then FIRST' (map (biresolve_from_nets_tac o netpair_of) (get_nets cs))
  1115       if null rules then FIRST' (map (biresolve_from_nets_tac o netpair_of) (get_nets cs))
  1116       else res_tac rules;
  1116       else res_tac rules;
  1117     fun multi_tac st = (single_tac THEN_ALL_NEW (TRY o (fn st => multi_tac st))) st;
  1117     fun multi_tac st = (single_tac THEN_ALL_NEW (TRY o (fn st => multi_tac st))) st;
  1118   in Method.same_tac facts THEN' multi_tac end;
  1118   in Method.insert_tac facts THEN' multi_tac end;
  1119 
  1119 
  1120 val intro_tac = intro_elim_tac (fn (inet, _) => (inet, Net.empty)) resolve_tac;
  1120 val intro_tac = intro_elim_tac (fn (inet, _) => (inet, Net.empty)) resolve_tac;
  1121 val elim_tac = intro_elim_tac (fn (_, enet) => (Net.empty, enet)) eresolve_tac;
  1121 val elim_tac = intro_elim_tac (fn (_, enet) => (Net.empty, enet)) eresolve_tac;
  1122 
  1122 
  1123 in
  1123 in
  1126 end;
  1126 end;
  1127 
  1127 
  1128 
  1128 
  1129 (* contradiction method *)
  1129 (* contradiction method *)
  1130 
  1130 
  1131 val contradiction = Method.METHOD (fn facts =>
  1131 val contradiction = Method.rule [Data.not_elim, Data.not_elim COMP Drule.swap_prems_rl];
  1132   FIRSTGOAL (Method.same_tac facts THEN' contr_tac));
       
  1133 
  1132 
  1134 
  1133 
  1135 (* automatic methods *)
  1134 (* automatic methods *)
  1136 
  1135 
  1137 val cla_modifiers =
  1136 val cla_modifiers =
  1147   Args.$$$ delN >> K (I, delrule_local)];
  1146   Args.$$$ delN >> K (I, delrule_local)];
  1148 
  1147 
  1149 val cla_args = Method.only_sectioned_args cla_modifiers;
  1148 val cla_args = Method.only_sectioned_args cla_modifiers;
  1150 
  1149 
  1151 fun cla_meth tac ctxt = Method.METHOD (fn facts =>
  1150 fun cla_meth tac ctxt = Method.METHOD (fn facts =>
  1152   ALLGOALS (Method.same_tac facts) THEN tac (get_local_claset ctxt));
  1151   ALLGOALS (Method.insert_tac facts) THEN tac (get_local_claset ctxt));
  1153 
  1152 
  1154 fun cla_meth' tac ctxt = Method.METHOD (fn facts =>
  1153 fun cla_meth' tac ctxt = Method.METHOD (fn facts =>
  1155   FIRSTGOAL (Method.same_tac facts THEN' tac (get_local_claset ctxt)));
  1154   FIRSTGOAL (Method.insert_tac facts THEN' tac (get_local_claset ctxt)));
  1156 
  1155 
  1157 val cla_method = cla_args o cla_meth;
  1156 val cla_method = cla_args o cla_meth;
  1158 val cla_method' = cla_args o cla_meth';
  1157 val cla_method' = cla_args o cla_meth';
  1159 
  1158 
  1160 
  1159 
  1161 
  1160 
  1162 (** setup_methods **)
  1161 (** setup_methods **)
  1163 
  1162 
  1164 val setup_methods = Method.add_methods
  1163 val setup_methods = Method.add_methods
  1165  [("default", Method.thms_args rule, "apply some rule (chain facts)"),
  1164  [("default", Method.thms_args rule, "apply some rule"),
  1166   ("rule", Method.thms_args rule, "apply some rule (chain facts)"),
  1165   ("rule", Method.thms_args rule, "apply some rule"),
  1167   ("intro", Method.thms_args intro, "apply some introduction rule (cut facts)"),
       
  1168   ("elim", Method.thms_args elim, "apply some elimination rule (cut facts)"),
       
  1169   ("contradiction", Method.no_args contradiction, "proof by contradiction"),
  1166   ("contradiction", Method.no_args contradiction, "proof by contradiction"),
       
  1167   ("intro", Method.thms_args intro, "repeatedly apply introduction rules"),
       
  1168   ("elim", Method.thms_args elim, "repeatedly apply elimination rules"),
  1170   ("safe_tac", cla_method safe_tac, "safe_tac (improper!)"),
  1169   ("safe_tac", cla_method safe_tac, "safe_tac (improper!)"),
  1171   ("safe_step_tac", cla_method' safe_step_tac, "safe_step_tac (improper!)"),
  1170   ("safe_step_tac", cla_method' safe_step_tac, "safe_step_tac (improper!)"),
  1172   ("step_tac", cla_method' step_tac, "step_tac (improper!)"),
  1171   ("step_tac", cla_method' step_tac, "step_tac (improper!)"),
  1173   ("fast", cla_method' fast_tac, "classical prover (depth-first)"),
  1172   ("fast", cla_method' fast_tac, "classical prover (depth-first)"),
  1174   ("best", cla_method' best_tac, "classical prover (best-first)"),
  1173   ("best", cla_method' best_tac, "classical prover (best-first)"),