src/HOL/Tools/cnf_funcs.ML
author wenzelm
Sun, 01 Mar 2009 23:36:12 +0100
changeset 30190 479806475f3c
parent 29265 5b4247055bd7
child 30607 c3d1590debd8
permissions -rw-r--r--
use long names for old-style fold combinators;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
     1
(*  Title:      HOL/Tools/cnf_funcs.ML
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
     2
    Author:     Alwen Tiu, QSL Team, LORIA (http://qsl.loria.fr)
29265
5b4247055bd7 moved old add_term_vars, add_term_frees etc. to structure OldTerm;
wenzelm
parents: 26341
diff changeset
     3
    Author:     Tjark Weber, TU Muenchen
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
     4
24958
ff15f76741bd rationalized redundant code
paulson
parents: 21576
diff changeset
     5
  FIXME: major overlaps with the code in meson.ML
ff15f76741bd rationalized redundant code
paulson
parents: 21576
diff changeset
     6
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
     7
  Description:
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
     8
  This file contains functions and tactics to transform a formula into
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
     9
  Conjunctive Normal Form (CNF).
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    10
  A formula in CNF is of the following form:
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    11
19236
150e8b0fb991 clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents: 17809
diff changeset
    12
      (x11 | x12 | ... | x1n) & ... & (xm1 | xm2 | ... | xmk)
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
    13
      False
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
    14
      True
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    15
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
    16
  where each xij is a literal (a positive or negative atomic Boolean term),
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
    17
  i.e. the formula is a conjunction of disjunctions of literals, or
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
    18
  "False", or "True".
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
    19
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
    20
  A (non-empty) disjunction of literals is referred to as "clause".
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    21
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    22
  For the purpose of SAT proof reconstruction, we also make use of another
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    23
  representation of clauses, which we call the "raw clauses".
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    24
  Raw clauses are of the form
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    25
20440
e6fe74eebda3 faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents: 19236
diff changeset
    26
      [..., x1', x2', ..., xn'] |- False ,
19236
150e8b0fb991 clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents: 17809
diff changeset
    27
150e8b0fb991 clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents: 17809
diff changeset
    28
  where each xi is a literal, and each xi' is the negation normal form of ~xi.
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    29
19236
150e8b0fb991 clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents: 17809
diff changeset
    30
  Literals are successively removed from the hyps of raw clauses by resolution
150e8b0fb991 clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents: 17809
diff changeset
    31
  during SAT proof reconstruction.
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    32
*)
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    33
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    34
signature CNF =
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    35
sig
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
    36
	val is_atom           : Term.term -> bool
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
    37
	val is_literal        : Term.term -> bool
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
    38
	val is_clause         : Term.term -> bool
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
    39
	val clause_is_trivial : Term.term -> bool
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
    40
20440
e6fe74eebda3 faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents: 19236
diff changeset
    41
	val clause2raw_thm : Thm.thm -> Thm.thm
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    42
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
    43
	val weakening_tac : int -> Tactical.tactic  (* removes the first hypothesis of a subgoal *)
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    44
20547
wenzelm
parents: 20440
diff changeset
    45
	val make_cnf_thm  : theory -> Term.term -> Thm.thm
wenzelm
parents: 20440
diff changeset
    46
	val make_cnfx_thm : theory -> Term.term ->  Thm.thm
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
    47
	val cnf_rewrite_tac  : int -> Tactical.tactic  (* converts all prems of a subgoal to CNF *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
    48
	val cnfx_rewrite_tac : int -> Tactical.tactic  (* converts all prems of a subgoal to (almost) definitional CNF *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
    49
end;
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    50
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    51
structure cnf : CNF =
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    52
struct
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    53
20440
e6fe74eebda3 faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents: 19236
diff changeset
    54
fun thm_by_auto (G : string) : thm =
26341
2f5a4367a39e avoid Auto_tac;
wenzelm
parents: 24958
diff changeset
    55
	prove_goal (the_context ()) G (fn prems => [cut_facts_tac prems 1, CLASIMPSET auto_tac]);
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    56
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
    57
(* Thm.thm *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
    58
val clause2raw_notE      = thm_by_auto "[| P; ~P |] ==> False";
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
    59
val clause2raw_not_disj  = thm_by_auto "[| ~P; ~Q |] ==> ~(P | Q)";
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
    60
val clause2raw_not_not   = thm_by_auto "P ==> ~~P";
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    61
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
    62
val iff_refl             = thm_by_auto "(P::bool) = P";
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
    63
val iff_trans            = thm_by_auto "[| (P::bool) = Q; Q = R |] ==> P = R";
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
    64
val conj_cong            = thm_by_auto "[| P = P'; Q = Q' |] ==> (P & Q) = (P' & Q')";
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
    65
val disj_cong            = thm_by_auto "[| P = P'; Q = Q' |] ==> (P | Q) = (P' | Q')";
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    66
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
    67
val make_nnf_imp         = thm_by_auto "[| (~P) = P'; Q = Q' |] ==> (P --> Q) = (P' | Q')";
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
    68
val make_nnf_iff         = thm_by_auto "[| P = P'; (~P) = NP; Q = Q'; (~Q) = NQ |] ==> (P = Q) = ((P' | NQ) & (NP | Q'))";
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
    69
val make_nnf_not_false   = thm_by_auto "(~False) = True";
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
    70
val make_nnf_not_true    = thm_by_auto "(~True) = False";
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
    71
val make_nnf_not_conj    = thm_by_auto "[| (~P) = P'; (~Q) = Q' |] ==> (~(P & Q)) = (P' | Q')";
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
    72
val make_nnf_not_disj    = thm_by_auto "[| (~P) = P'; (~Q) = Q' |] ==> (~(P | Q)) = (P' & Q')";
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
    73
val make_nnf_not_imp     = thm_by_auto "[| P = P'; (~Q) = Q' |] ==> (~(P --> Q)) = (P' & Q')";
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
    74
val make_nnf_not_iff     = thm_by_auto "[| P = P'; (~P) = NP; Q = Q'; (~Q) = NQ |] ==> (~(P = Q)) = ((P' | Q') & (NP | NQ))";
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
    75
val make_nnf_not_not     = thm_by_auto "P = P' ==> (~~P) = P'";
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    76
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
    77
val simp_TF_conj_True_l  = thm_by_auto "[| P = True; Q = Q' |] ==> (P & Q) = Q'";
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
    78
val simp_TF_conj_True_r  = thm_by_auto "[| P = P'; Q = True |] ==> (P & Q) = P'";
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
    79
val simp_TF_conj_False_l = thm_by_auto "P = False ==> (P & Q) = False";
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
    80
val simp_TF_conj_False_r = thm_by_auto "Q = False ==> (P & Q) = False";
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
    81
val simp_TF_disj_True_l  = thm_by_auto "P = True ==> (P | Q) = True";
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
    82
val simp_TF_disj_True_r  = thm_by_auto "Q = True ==> (P | Q) = True";
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
    83
val simp_TF_disj_False_l = thm_by_auto "[| P = False; Q = Q' |] ==> (P | Q) = Q'";
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
    84
val simp_TF_disj_False_r = thm_by_auto "[| P = P'; Q = False |] ==> (P | Q) = P'";
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    85
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
    86
val make_cnf_disj_conj_l = thm_by_auto "[| (P | R) = PR; (Q | R) = QR |] ==> ((P & Q) | R) = (PR & QR)";
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
    87
val make_cnf_disj_conj_r = thm_by_auto "[| (P | Q) = PQ; (P | R) = PR |] ==> (P | (Q & R)) = (PQ & PR)";
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    88
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
    89
val make_cnfx_disj_ex_l = thm_by_auto "((EX (x::bool). P x) | Q) = (EX x. P x | Q)";
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
    90
val make_cnfx_disj_ex_r = thm_by_auto "(P | (EX (x::bool). Q x)) = (EX x. P | Q x)";
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
    91
val make_cnfx_newlit    = thm_by_auto "(P | Q) = (EX x. (P | x) & (Q | ~x))";
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
    92
val make_cnfx_ex_cong   = thm_by_auto "(ALL (x::bool). P x = Q x) ==> (EX x. P x) = (EX x. Q x)";
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    93
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
    94
val weakening_thm        = thm_by_auto "[| P; Q |] ==> Q";
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    95
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
    96
val cnftac_eq_imp        = thm_by_auto "[| P = Q; P |] ==> Q";
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    97
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
    98
(* Term.term -> bool *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
    99
fun is_atom (Const ("False", _))                                           = false
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   100
  | is_atom (Const ("True", _))                                            = false
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   101
  | is_atom (Const ("op &", _) $ _ $ _)                                    = false
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   102
  | is_atom (Const ("op |", _) $ _ $ _)                                    = false
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   103
  | is_atom (Const ("op -->", _) $ _ $ _)                                  = false
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   104
  | is_atom (Const ("op =", Type ("fun", Type ("bool", []) :: _)) $ _ $ _) = false
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   105
  | is_atom (Const ("Not", _) $ _)                                         = false
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   106
  | is_atom _                                                              = true;
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   107
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   108
(* Term.term -> bool *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   109
fun is_literal (Const ("Not", _) $ x) = is_atom x
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   110
  | is_literal x                      = is_atom x;
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   111
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   112
(* Term.term -> bool *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   113
fun is_clause (Const ("op |", _) $ x $ y) = is_clause x andalso is_clause y
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   114
  | is_clause x                           = is_literal x;
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   115
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   116
(* ------------------------------------------------------------------------- *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   117
(* clause_is_trivial: a clause is trivially true if it contains both an atom *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   118
(*      and the atom's negation                                              *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   119
(* ------------------------------------------------------------------------- *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   120
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   121
(* Term.term -> bool *)
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   122
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   123
fun clause_is_trivial c =
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   124
	let
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   125
		(* Term.term -> Term.term *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   126
		fun dual (Const ("Not", _) $ x) = x
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   127
		  | dual x                      = HOLogic.Not $ x
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   128
		(* Term.term list -> bool *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   129
		fun has_duals []      = false
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   130
		  | has_duals (x::xs) = (dual x) mem xs orelse has_duals xs
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   131
	in
24958
ff15f76741bd rationalized redundant code
paulson
parents: 21576
diff changeset
   132
		has_duals (HOLogic.disjuncts c)
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   133
	end;
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   134
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   135
(* ------------------------------------------------------------------------- *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   136
(* clause2raw_thm: translates a clause into a raw clause, i.e.               *)
20440
e6fe74eebda3 faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents: 19236
diff changeset
   137
(*        [...] |- x1 | ... | xn                                             *)
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   138
(*      (where each xi is a literal) is translated to                        *)
20440
e6fe74eebda3 faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents: 19236
diff changeset
   139
(*        [..., x1', ..., xn'] |- False ,                                    *)
e6fe74eebda3 faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents: 19236
diff changeset
   140
(*      where each xi' is the negation normal form of ~xi                    *)
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   141
(* ------------------------------------------------------------------------- *)
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   142
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   143
(* Thm.thm -> Thm.thm *)
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   144
20440
e6fe74eebda3 faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents: 19236
diff changeset
   145
fun clause2raw_thm clause =
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   146
let
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   147
	(* eliminates negated disjunctions from the i-th premise, possibly *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   148
	(* adding new premises, then continues with the (i+1)-th premise   *)
20440
e6fe74eebda3 faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents: 19236
diff changeset
   149
	(* int -> Thm.thm -> Thm.thm *)
e6fe74eebda3 faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents: 19236
diff changeset
   150
	fun not_disj_to_prem i thm =
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   151
		if i > nprems_of thm then
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   152
			thm
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   153
		else
20440
e6fe74eebda3 faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents: 19236
diff changeset
   154
			not_disj_to_prem (i+1) (Seq.hd (REPEAT_DETERM (rtac clause2raw_not_disj i) thm))
e6fe74eebda3 faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents: 19236
diff changeset
   155
	(* moves all premises to hyps, i.e. "[...] |- A1 ==> ... ==> An ==> B" *)
e6fe74eebda3 faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents: 19236
diff changeset
   156
	(* becomes "[..., A1, ..., An] |- B"                                   *)
e6fe74eebda3 faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents: 19236
diff changeset
   157
	(* Thm.thm -> Thm.thm *)
e6fe74eebda3 faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents: 19236
diff changeset
   158
	fun prems_to_hyps thm =
e6fe74eebda3 faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents: 19236
diff changeset
   159
		fold (fn cprem => fn thm' =>
e6fe74eebda3 faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents: 19236
diff changeset
   160
			Thm.implies_elim thm' (Thm.assume cprem)) (cprems_of thm) thm
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   161
in
20440
e6fe74eebda3 faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents: 19236
diff changeset
   162
	(* [...] |- ~(x1 | ... | xn) ==> False *)
e6fe74eebda3 faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents: 19236
diff changeset
   163
	(clause2raw_notE OF [clause])
e6fe74eebda3 faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents: 19236
diff changeset
   164
	(* [...] |- ~x1 ==> ... ==> ~xn ==> False *)
e6fe74eebda3 faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents: 19236
diff changeset
   165
	|> not_disj_to_prem 1
e6fe74eebda3 faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents: 19236
diff changeset
   166
	(* [...] |- x1' ==> ... ==> xn' ==> False *)
e6fe74eebda3 faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents: 19236
diff changeset
   167
	|> Seq.hd o TRYALL (rtac clause2raw_not_not)
e6fe74eebda3 faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents: 19236
diff changeset
   168
	(* [..., x1', ..., xn'] |- False *)
e6fe74eebda3 faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents: 19236
diff changeset
   169
	|> prems_to_hyps
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   170
end;
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   171
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   172
(* ------------------------------------------------------------------------- *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   173
(* inst_thm: instantiates a theorem with a list of terms                     *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   174
(* ------------------------------------------------------------------------- *)
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   175
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   176
fun inst_thm thy ts thm =
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   177
	instantiate' [] (map (SOME o cterm_of thy) ts) thm;
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   178
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   179
(* ------------------------------------------------------------------------- *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   180
(*                         Naive CNF transformation                          *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   181
(* ------------------------------------------------------------------------- *)
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   182
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   183
(* ------------------------------------------------------------------------- *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   184
(* make_nnf_thm: produces a theorem of the form t = t', where t' is the      *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   185
(*      negation normal form (i.e. negation only occurs in front of atoms)   *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   186
(*      of t; implications ("-->") and equivalences ("=" on bool) are        *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   187
(*      eliminated (possibly causing an exponential blowup)                  *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   188
(* ------------------------------------------------------------------------- *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   189
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   190
(* Theory.theory -> Term.term -> Thm.thm *)
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   191
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   192
fun make_nnf_thm thy (Const ("op &", _) $ x $ y) =
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   193
	let
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   194
		val thm1 = make_nnf_thm thy x
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   195
		val thm2 = make_nnf_thm thy y
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   196
	in
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   197
		conj_cong OF [thm1, thm2]
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   198
	end
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   199
  | make_nnf_thm thy (Const ("op |", _) $ x $ y) =
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   200
	let
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   201
		val thm1 = make_nnf_thm thy x
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   202
		val thm2 = make_nnf_thm thy y
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   203
	in
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   204
		disj_cong OF [thm1, thm2]
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   205
	end
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   206
  | make_nnf_thm thy (Const ("op -->", _) $ x $ y) =
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   207
	let
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   208
		val thm1 = make_nnf_thm thy (HOLogic.Not $ x)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   209
		val thm2 = make_nnf_thm thy y
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   210
	in
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   211
		make_nnf_imp OF [thm1, thm2]
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   212
	end
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   213
  | make_nnf_thm thy (Const ("op =", Type ("fun", Type ("bool", []) :: _)) $ x $ y) =
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   214
	let
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   215
		val thm1 = make_nnf_thm thy x
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   216
		val thm2 = make_nnf_thm thy (HOLogic.Not $ x)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   217
		val thm3 = make_nnf_thm thy y
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   218
		val thm4 = make_nnf_thm thy (HOLogic.Not $ y)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   219
	in
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   220
		make_nnf_iff OF [thm1, thm2, thm3, thm4]
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   221
	end
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   222
  | make_nnf_thm thy (Const ("Not", _) $ Const ("False", _)) =
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   223
	make_nnf_not_false
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   224
  | make_nnf_thm thy (Const ("Not", _) $ Const ("True", _)) =
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   225
	make_nnf_not_true
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   226
  | make_nnf_thm thy (Const ("Not", _) $ (Const ("op &", _) $ x $ y)) =
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   227
	let
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   228
		val thm1 = make_nnf_thm thy (HOLogic.Not $ x)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   229
		val thm2 = make_nnf_thm thy (HOLogic.Not $ y)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   230
	in
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   231
		make_nnf_not_conj OF [thm1, thm2]
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   232
	end
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   233
  | make_nnf_thm thy (Const ("Not", _) $ (Const ("op |", _) $ x $ y)) =
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   234
	let
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   235
		val thm1 = make_nnf_thm thy (HOLogic.Not $ x)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   236
		val thm2 = make_nnf_thm thy (HOLogic.Not $ y)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   237
	in
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   238
		make_nnf_not_disj OF [thm1, thm2]
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   239
	end
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   240
  | make_nnf_thm thy (Const ("Not", _) $ (Const ("op -->", _) $ x $ y)) =
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   241
	let
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   242
		val thm1 = make_nnf_thm thy x
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   243
		val thm2 = make_nnf_thm thy (HOLogic.Not $ y)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   244
	in
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   245
		make_nnf_not_imp OF [thm1, thm2]
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   246
	end
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   247
  | make_nnf_thm thy (Const ("Not", _) $ (Const ("op =", Type ("fun", Type ("bool", []) :: _)) $ x $ y)) =
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   248
	let
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   249
		val thm1 = make_nnf_thm thy x
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   250
		val thm2 = make_nnf_thm thy (HOLogic.Not $ x)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   251
		val thm3 = make_nnf_thm thy y
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   252
		val thm4 = make_nnf_thm thy (HOLogic.Not $ y)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   253
	in
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   254
		make_nnf_not_iff OF [thm1, thm2, thm3, thm4]
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   255
	end
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   256
  | make_nnf_thm thy (Const ("Not", _) $ (Const ("Not", _) $ x)) =
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   257
	let
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   258
		val thm1 = make_nnf_thm thy x
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   259
	in
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   260
		make_nnf_not_not OF [thm1]
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   261
	end
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   262
  | make_nnf_thm thy t =
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   263
	inst_thm thy [t] iff_refl;
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   264
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   265
(* ------------------------------------------------------------------------- *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   266
(* simp_True_False_thm: produces a theorem t = t', where t' is equivalent to *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   267
(*      t, but simplified wrt. the following theorems:                       *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   268
(*        (True & x) = x                                                     *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   269
(*        (x & True) = x                                                     *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   270
(*        (False & x) = False                                                *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   271
(*        (x & False) = False                                                *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   272
(*        (True | x) = True                                                  *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   273
(*        (x | True) = True                                                  *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   274
(*        (False | x) = x                                                    *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   275
(*        (x | False) = x                                                    *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   276
(*      No simplification is performed below connectives other than & and |. *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   277
(*      Optimization: The right-hand side of a conjunction (disjunction) is  *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   278
(*      simplified only if the left-hand side does not simplify to False     *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   279
(*      (True, respectively).                                                *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   280
(* ------------------------------------------------------------------------- *)
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   281
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   282
(* Theory.theory -> Term.term -> Thm.thm *)
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   283
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   284
fun simp_True_False_thm thy (Const ("op &", _) $ x $ y) =
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   285
	let
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   286
		val thm1 = simp_True_False_thm thy x
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   287
		val x'   = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   288
	in
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   289
		if x' = HOLogic.false_const then
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   290
			simp_TF_conj_False_l OF [thm1]  (* (x & y) = False *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   291
		else
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   292
			let
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   293
				val thm2 = simp_True_False_thm thy y
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   294
				val y'   = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm2
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   295
			in
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   296
				if x' = HOLogic.true_const then
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   297
					simp_TF_conj_True_l OF [thm1, thm2]  (* (x & y) = y' *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   298
				else if y' = HOLogic.false_const then
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   299
					simp_TF_conj_False_r OF [thm2]  (* (x & y) = False *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   300
				else if y' = HOLogic.true_const then
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   301
					simp_TF_conj_True_r OF [thm1, thm2]  (* (x & y) = x' *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   302
				else
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   303
					conj_cong OF [thm1, thm2]  (* (x & y) = (x' & y') *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   304
			end
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   305
	end
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   306
  | simp_True_False_thm thy (Const ("op |", _) $ x $ y) =
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   307
	let
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   308
		val thm1 = simp_True_False_thm thy x
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   309
		val x'   = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   310
	in
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   311
		if x' = HOLogic.true_const then
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   312
			simp_TF_disj_True_l OF [thm1]  (* (x | y) = True *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   313
		else
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   314
			let
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   315
				val thm2 = simp_True_False_thm thy y
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   316
				val y'   = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm2
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   317
			in
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   318
				if x' = HOLogic.false_const then
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   319
					simp_TF_disj_False_l OF [thm1, thm2]  (* (x | y) = y' *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   320
				else if y' = HOLogic.true_const then
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   321
					simp_TF_disj_True_r OF [thm2]  (* (x | y) = True *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   322
				else if y' = HOLogic.false_const then
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   323
					simp_TF_disj_False_r OF [thm1, thm2]  (* (x | y) = x' *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   324
				else
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   325
					disj_cong OF [thm1, thm2]  (* (x | y) = (x' | y') *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   326
			end
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   327
	end
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   328
  | simp_True_False_thm thy t =
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   329
	inst_thm thy [t] iff_refl;  (* t = t *)
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   330
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   331
(* ------------------------------------------------------------------------- *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   332
(* make_cnf_thm: given any HOL term 't', produces a theorem t = t', where t' *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   333
(*      is in conjunction normal form.  May cause an exponential blowup      *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   334
(*      in the length of the term.                                           *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   335
(* ------------------------------------------------------------------------- *)
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   336
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   337
(* Theory.theory -> Term.term -> Thm.thm *)
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   338
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   339
fun make_cnf_thm thy t =
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   340
let
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   341
	(* Term.term -> Thm.thm *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   342
	fun make_cnf_thm_from_nnf (Const ("op &", _) $ x $ y) =
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   343
		let
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   344
			val thm1 = make_cnf_thm_from_nnf x
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   345
			val thm2 = make_cnf_thm_from_nnf y
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   346
		in
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   347
			conj_cong OF [thm1, thm2]
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   348
		end
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   349
	  | make_cnf_thm_from_nnf (Const ("op |", _) $ x $ y) =
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   350
		let
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   351
			(* produces a theorem "(x' | y') = t'", where x', y', and t' are in CNF *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   352
			fun make_cnf_disj_thm (Const ("op &", _) $ x1 $ x2) y' =
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   353
				let
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   354
					val thm1 = make_cnf_disj_thm x1 y'
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   355
					val thm2 = make_cnf_disj_thm x2 y'
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   356
				in
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   357
					make_cnf_disj_conj_l OF [thm1, thm2]  (* ((x1 & x2) | y') = ((x1 | y')' & (x2 | y')') *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   358
				end
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   359
			  | make_cnf_disj_thm x' (Const ("op &", _) $ y1 $ y2) =
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   360
				let
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   361
					val thm1 = make_cnf_disj_thm x' y1
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   362
					val thm2 = make_cnf_disj_thm x' y2
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   363
				in
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   364
					make_cnf_disj_conj_r OF [thm1, thm2]  (* (x' | (y1 & y2)) = ((x' | y1)' & (x' | y2)') *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   365
				end
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   366
			  | make_cnf_disj_thm x' y' =
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   367
				inst_thm thy [HOLogic.mk_disj (x', y')] iff_refl  (* (x' | y') = (x' | y') *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   368
			val thm1     = make_cnf_thm_from_nnf x
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   369
			val thm2     = make_cnf_thm_from_nnf y
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   370
			val x'       = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   371
			val y'       = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm2
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   372
			val disj_thm = disj_cong OF [thm1, thm2]  (* (x | y) = (x' | y') *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   373
		in
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   374
			iff_trans OF [disj_thm, make_cnf_disj_thm x' y']
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   375
		end
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   376
	  | make_cnf_thm_from_nnf t =
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   377
		inst_thm thy [t] iff_refl
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   378
	(* convert 't' to NNF first *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   379
	val nnf_thm  = make_nnf_thm thy t
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   380
	val nnf      = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) nnf_thm
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   381
	(* then simplify wrt. True/False (this should preserve NNF) *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   382
	val simp_thm = simp_True_False_thm thy nnf
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   383
	val simp     = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) simp_thm
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   384
	(* finally, convert to CNF (this should preserve the simplification) *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   385
	val cnf_thm  = make_cnf_thm_from_nnf simp
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   386
in
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   387
	iff_trans OF [iff_trans OF [nnf_thm, simp_thm], cnf_thm]
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   388
end;
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   389
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   390
(* ------------------------------------------------------------------------- *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   391
(*            CNF transformation by introducing new literals                 *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   392
(* ------------------------------------------------------------------------- *)
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   393
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   394
(* ------------------------------------------------------------------------- *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   395
(* make_cnfx_thm: given any HOL term 't', produces a theorem t = t', where   *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   396
(*      t' is almost in conjunction normal form, except that conjunctions    *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   397
(*      and existential quantifiers may be nested.  (Use e.g. 'REPEAT_DETERM *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   398
(*      (etac exE i ORELSE etac conjE i)' afterwards to normalize.)  May     *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   399
(*      introduce new (existentially bound) literals.  Note: the current     *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   400
(*      implementation calls 'make_nnf_thm', causing an exponential blowup   *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   401
(*      in the case of nested equivalences.                                  *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   402
(* ------------------------------------------------------------------------- *)
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   403
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   404
(* Theory.theory -> Term.term -> Thm.thm *)
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   405
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   406
fun make_cnfx_thm thy t =
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   407
let
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   408
	val var_id = ref 0  (* properly initialized below *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   409
	(* unit -> Term.term *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   410
	fun new_free () =
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   411
		Free ("cnfx_" ^ string_of_int (inc var_id), HOLogic.boolT)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   412
	(* Term.term -> Thm.thm *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   413
	fun make_cnfx_thm_from_nnf (Const ("op &", _) $ x $ y) =
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   414
		let
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   415
			val thm1 = make_cnfx_thm_from_nnf x
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   416
			val thm2 = make_cnfx_thm_from_nnf y
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   417
		in
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   418
			conj_cong OF [thm1, thm2]
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   419
		end
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   420
	  | make_cnfx_thm_from_nnf (Const ("op |", _) $ x $ y) =
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   421
		if is_clause x andalso is_clause y then
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   422
			inst_thm thy [HOLogic.mk_disj (x, y)] iff_refl
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   423
		else if is_literal y orelse is_literal x then let
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   424
			(* produces a theorem "(x' | y') = t'", where x', y', and t' are *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   425
			(* almost in CNF, and x' or y' is a literal                      *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   426
			fun make_cnfx_disj_thm (Const ("op &", _) $ x1 $ x2) y' =
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   427
				let
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   428
					val thm1 = make_cnfx_disj_thm x1 y'
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   429
					val thm2 = make_cnfx_disj_thm x2 y'
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   430
				in
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   431
					make_cnf_disj_conj_l OF [thm1, thm2]  (* ((x1 & x2) | y') = ((x1 | y')' & (x2 | y')') *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   432
				end
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   433
			  | make_cnfx_disj_thm x' (Const ("op &", _) $ y1 $ y2) =
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   434
				let
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   435
					val thm1 = make_cnfx_disj_thm x' y1
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   436
					val thm2 = make_cnfx_disj_thm x' y2
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   437
				in
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   438
					make_cnf_disj_conj_r OF [thm1, thm2]  (* (x' | (y1 & y2)) = ((x' | y1)' & (x' | y2)') *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   439
				end
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   440
			  | make_cnfx_disj_thm (Const ("Ex", _) $ x') y' =
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   441
				let
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   442
					val thm1 = inst_thm thy [x', y'] make_cnfx_disj_ex_l   (* ((Ex x') | y') = (Ex (x' | y')) *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   443
					val var  = new_free ()
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   444
					val thm2 = make_cnfx_disj_thm (betapply (x', var)) y'  (* (x' | y') = body' *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   445
					val thm3 = forall_intr (cterm_of thy var) thm2         (* !!v. (x' | y') = body' *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   446
					val thm4 = strip_shyps (thm3 COMP allI)                (* ALL v. (x' | y') = body' *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   447
					val thm5 = strip_shyps (thm4 RS make_cnfx_ex_cong)     (* (EX v. (x' | y')) = (EX v. body') *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   448
				in
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   449
					iff_trans OF [thm1, thm5]  (* ((Ex x') | y') = (Ex v. body') *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   450
				end
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   451
			  | make_cnfx_disj_thm x' (Const ("Ex", _) $ y') =
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   452
				let
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   453
					val thm1 = inst_thm thy [x', y'] make_cnfx_disj_ex_r   (* (x' | (Ex y')) = (Ex (x' | y')) *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   454
					val var  = new_free ()
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   455
					val thm2 = make_cnfx_disj_thm x' (betapply (y', var))  (* (x' | y') = body' *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   456
					val thm3 = forall_intr (cterm_of thy var) thm2         (* !!v. (x' | y') = body' *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   457
					val thm4 = strip_shyps (thm3 COMP allI)                (* ALL v. (x' | y') = body' *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   458
					val thm5 = strip_shyps (thm4 RS make_cnfx_ex_cong)     (* (EX v. (x' | y')) = (EX v. body') *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   459
				in
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   460
					iff_trans OF [thm1, thm5]  (* (x' | (Ex y')) = (EX v. body') *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   461
				end
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   462
			  | make_cnfx_disj_thm x' y' =
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   463
				inst_thm thy [HOLogic.mk_disj (x', y')] iff_refl  (* (x' | y') = (x' | y') *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   464
			val thm1     = make_cnfx_thm_from_nnf x
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   465
			val thm2     = make_cnfx_thm_from_nnf y
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   466
			val x'       = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   467
			val y'       = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm2
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   468
			val disj_thm = disj_cong OF [thm1, thm2]  (* (x | y) = (x' | y') *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   469
		in
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   470
			iff_trans OF [disj_thm, make_cnfx_disj_thm x' y']
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   471
		end else let  (* neither 'x' nor 'y' is a literal: introduce a fresh variable *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   472
			val thm1 = inst_thm thy [x, y] make_cnfx_newlit     (* (x | y) = EX v. (x | v) & (y | ~v) *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   473
			val var  = new_free ()
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   474
			val body = HOLogic.mk_conj (HOLogic.mk_disj (x, var), HOLogic.mk_disj (y, HOLogic.Not $ var))
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   475
			val thm2 = make_cnfx_thm_from_nnf body              (* (x | v) & (y | ~v) = body' *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   476
			val thm3 = forall_intr (cterm_of thy var) thm2      (* !!v. (x | v) & (y | ~v) = body' *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   477
			val thm4 = strip_shyps (thm3 COMP allI)             (* ALL v. (x | v) & (y | ~v) = body' *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   478
			val thm5 = strip_shyps (thm4 RS make_cnfx_ex_cong)  (* (EX v. (x | v) & (y | ~v)) = (EX v. body') *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   479
		in
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   480
			iff_trans OF [thm1, thm5]
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   481
		end
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   482
	  | make_cnfx_thm_from_nnf t =
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   483
		inst_thm thy [t] iff_refl
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   484
	(* convert 't' to NNF first *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   485
	val nnf_thm  = make_nnf_thm thy t
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   486
	val nnf      = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) nnf_thm
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   487
	(* then simplify wrt. True/False (this should preserve NNF) *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   488
	val simp_thm = simp_True_False_thm thy nnf
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   489
	val simp     = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) simp_thm
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   490
	(* initialize var_id, in case the term already contains variables of the form "cnfx_<int>" *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   491
	val _        = (var_id := fold (fn free => fn max =>
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   492
		let
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   493
			val (name, _) = dest_Free free
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   494
			val idx       = if String.isPrefix "cnfx_" name then
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   495
					(Int.fromString o String.extract) (name, String.size "cnfx_", NONE)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   496
				else
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   497
					NONE
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   498
		in
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   499
			Int.max (max, getOpt (idx, 0))
29265
5b4247055bd7 moved old add_term_vars, add_term_frees etc. to structure OldTerm;
wenzelm
parents: 26341
diff changeset
   500
		end) (OldTerm.term_frees simp) 0)
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   501
	(* finally, convert to definitional CNF (this should preserve the simplification) *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   502
	val cnfx_thm = make_cnfx_thm_from_nnf simp
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   503
in
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   504
	iff_trans OF [iff_trans OF [nnf_thm, simp_thm], cnfx_thm]
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   505
end;
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   506
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   507
(* ------------------------------------------------------------------------- *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   508
(*                                  Tactics                                  *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   509
(* ------------------------------------------------------------------------- *)
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   510
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   511
(* ------------------------------------------------------------------------- *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   512
(* weakening_tac: removes the first hypothesis of the 'i'-th subgoal         *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   513
(* ------------------------------------------------------------------------- *)
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   514
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   515
(* int -> Tactical.tactic *)
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   516
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   517
fun weakening_tac i =
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   518
	dtac weakening_thm i THEN atac (i+1);
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   519
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   520
(* ------------------------------------------------------------------------- *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   521
(* cnf_rewrite_tac: converts all premises of the 'i'-th subgoal to CNF       *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   522
(*      (possibly causing an exponential blowup in the length of each        *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   523
(*      premise)                                                             *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   524
(* ------------------------------------------------------------------------- *)
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   525
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   526
(* int -> Tactical.tactic *)
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   527
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   528
fun cnf_rewrite_tac i =
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   529
	(* cut the CNF formulas as new premises *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   530
	METAHYPS (fn prems =>
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   531
		let
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   532
			val cnf_thms = map (fn pr => make_cnf_thm (theory_of_thm pr) ((HOLogic.dest_Trueprop o prop_of) pr)) prems
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   533
			val cut_thms = map (fn (th, pr) => cnftac_eq_imp OF [th, pr]) (cnf_thms ~~ prems)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   534
		in
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   535
			cut_facts_tac cut_thms 1
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   536
		end) i
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   537
	(* remove the original premises *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   538
	THEN SELECT_GOAL (fn thm =>
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   539
		let
21576
8c11b1ce2f05 simplified Logic.count_prems;
wenzelm
parents: 20547
diff changeset
   540
			val n = Logic.count_prems ((Term.strip_all_body o fst o Logic.dest_implies o prop_of) thm)
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   541
		in
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   542
			PRIMITIVE (funpow (n div 2) (Seq.hd o weakening_tac 1)) thm
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   543
		end) i;
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   544
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   545
(* ------------------------------------------------------------------------- *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   546
(* cnfx_rewrite_tac: converts all premises of the 'i'-th subgoal to CNF      *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   547
(*      (possibly introducing new literals)                                  *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   548
(* ------------------------------------------------------------------------- *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   549
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   550
(* int -> Tactical.tactic *)
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   551
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   552
fun cnfx_rewrite_tac i =
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   553
	(* cut the CNF formulas as new premises *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   554
	METAHYPS (fn prems =>
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   555
		let
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   556
			val cnfx_thms = map (fn pr => make_cnfx_thm (theory_of_thm pr) ((HOLogic.dest_Trueprop o prop_of) pr)) prems
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   557
			val cut_thms  = map (fn (th, pr) => cnftac_eq_imp OF [th, pr]) (cnfx_thms ~~ prems)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   558
		in
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   559
			cut_facts_tac cut_thms 1
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   560
		end) i
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   561
	(* remove the original premises *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   562
	THEN SELECT_GOAL (fn thm =>
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   563
		let
21576
8c11b1ce2f05 simplified Logic.count_prems;
wenzelm
parents: 20547
diff changeset
   564
			val n = Logic.count_prems ((Term.strip_all_body o fst o Logic.dest_implies o prop_of) thm)
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   565
		in
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   566
			PRIMITIVE (funpow (n div 2) (Seq.hd o weakening_tac 1)) thm
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   567
		end) i;
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   568
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17618
diff changeset
   569
end;  (* of structure *)