334 (* to *) |
334 (* to *) |
335 (* [| A1; ... ; An ; ~B |] ==> False *) |
335 (* [| A1; ... ; An ; ~B |] ==> False *) |
336 (* (handling meta-logical connectives in B properly before negating), *) |
336 (* (handling meta-logical connectives in B properly before negating), *) |
337 (* then replaces meta-logical connectives in the premises (i.e. "==>", *) |
337 (* then replaces meta-logical connectives in the premises (i.e. "==>", *) |
338 (* "!!" and "==") by connectives of the HOL object-logic (i.e. by *) |
338 (* "!!" and "==") by connectives of the HOL object-logic (i.e. by *) |
339 (* "-->", "!", and "="), then performs beta-eta-normalization *) |
339 (* "-->", "!", and "="), then performs beta-eta-normalization on the *) |
|
340 (* subgoal *) |
340 (* ------------------------------------------------------------------------- *) |
341 (* ------------------------------------------------------------------------- *) |
341 |
342 |
342 (* int -> Tactical.tactic *) |
343 (* int -> Tactical.tactic *) |
343 |
344 |
344 fun pre_cnf_tac i = rtac ccontr i THEN ObjectLogic.atomize_tac i THEN |
345 fun pre_cnf_tac i = rtac ccontr i THEN ObjectLogic.atomize_tac i THEN |
345 (fn st => Seq.single (Thm.equal_elim (Drule.beta_eta_conversion (cprop_of st)) st)); |
346 PRIMITIVE (Drule.fconv_rule (Drule.goals_conv (equal i) (Drule.beta_eta_conversion))); |
346 |
347 |
347 (* ------------------------------------------------------------------------- *) |
348 (* ------------------------------------------------------------------------- *) |
348 (* cnfsat_tac: checks if the empty clause "False" occurs among the premises; *) |
349 (* cnfsat_tac: checks if the empty clause "False" occurs among the premises; *) |
349 (* if not, eliminates conjunctions (i.e. each clause of the CNF formula *) |
350 (* if not, eliminates conjunctions (i.e. each clause of the CNF formula *) |
350 (* becomes a separate premise), then applies 'rawsat_tac' to solve the *) |
351 (* becomes a separate premise), then applies 'rawsat_tac' to solve the *) |