src/HOL/Tools/meson.ML
 changeset 12299 2c76042c3b06 parent 10821 dcb75538f542 child 13105 3d1e7a199bdc
equal inserted replaced
12298:b344486c33e2 12299:2c76042c3b06
`    11 FUNCTION nodups -- if done to goal clauses too!`
`    11 FUNCTION nodups -- if done to goal clauses too!`
`    12 *)`
`    12 *)`
`    13 `
`    13 `
`    14 local`
`    14 local`
`    15 `
`    15 `
`    16  (*Prove theorems using fast_tac*)`
`    16  val not_conjD = thm "meson_not_conjD";`
`    17  fun prove_fun s =`
`    17  val not_disjD = thm "meson_not_disjD";`
`    18      prove_goal (the_context ()) s`
`    18  val not_notD = thm "meson_not_notD";`
`    19           (fn prems => [ cut_facts_tac prems 1, Fast_tac 1 ]);`
`    19  val not_allD = thm "meson_not_allD";`
`    20 `
`    20  val not_exD = thm "meson_not_exD";`
`    21  (**** Negation Normal Form ****)`
`    21  val imp_to_disjD = thm "meson_imp_to_disjD";`
`    22 `
`    22  val not_impD = thm "meson_not_impD";`
`    23  (*** de Morgan laws ***)`
`    23  val iff_to_disjD = thm "meson_iff_to_disjD";`
`    24 `
`    24  val not_iffD = thm "meson_not_iffD";`
`    25  val not_conjD = prove_fun "~(P&Q) ==> ~P | ~Q";`
`    25  val conj_exD1 = thm "meson_conj_exD1";`
`    26  val not_disjD = prove_fun "~(P|Q) ==> ~P & ~Q";`
`    26  val conj_exD2 = thm "meson_conj_exD2";`
`    27  val not_notD = prove_fun "~~P ==> P";`
`    27  val disj_exD = thm "meson_disj_exD";`
`    28  val not_allD = prove_fun  "~(ALL x. P(x)) ==> EX x. ~P(x)";`
`    28  val disj_exD1 = thm "meson_disj_exD1";`
`    29  val not_exD = prove_fun   "~(EX x. P(x)) ==> ALL x. ~P(x)";`
`    29  val disj_exD2 = thm "meson_disj_exD2";`
`    30 `
`    30  val disj_assoc = thm "meson_disj_assoc";`
`    31 `
`    31  val disj_comm = thm "meson_disj_comm";`
`    32  (*** Removal of --> and <-> (positive and negative occurrences) ***)`
`    32  val disj_FalseD1 = thm "meson_disj_FalseD1";`
`    33 `
`    33  val disj_FalseD2 = thm "meson_disj_FalseD2";`
`    34  val imp_to_disjD = prove_fun "P-->Q ==> ~P | Q";`
`       `
`    35  val not_impD = prove_fun   "~(P-->Q) ==> P & ~Q";`
`       `
`    36 `
`       `
`    37  val iff_to_disjD = prove_fun "P=Q ==> (~P | Q) & (~Q | P)";`
`       `
`    38 `
`       `
`    39  (*Much more efficient than (P & ~Q) | (Q & ~P) for computing CNF*)`
`       `
`    40  val not_iffD = prove_fun "~(P=Q) ==> (P | Q) & (~P | ~Q)";`
`       `
`    41 `
`       `
`    42 `
`       `
`    43  (**** Pulling out the existential quantifiers ****)`
`       `
`    44 `
`       `
`    45  (*** Conjunction ***)`
`       `
`    46 `
`       `
`    47  val conj_exD1 = prove_fun "(EX x. P(x)) & Q ==> EX x. P(x) & Q";`
`       `
`    48  val conj_exD2 = prove_fun "P & (EX x. Q(x)) ==> EX x. P & Q(x)";`
`       `
`    49 `
`       `
`    50  (*** Disjunction ***)`
`       `
`    51 `
`       `
`    52  (*DO NOT USE with forall-Skolemization: makes fewer schematic variables!!`
`       `
`    53    With ex-Skolemization, makes fewer Skolem constants*)`
`       `
`    54  val disj_exD = prove_fun "(EX x. P(x)) | (EX x. Q(x)) ==> EX x. P(x) | Q(x)";`
`       `
`    55 `
`       `
`    56  val disj_exD1 = prove_fun "(EX x. P(x)) | Q ==> EX x. P(x) | Q";`
`       `
`    57  val disj_exD2 = prove_fun "P | (EX x. Q(x)) ==> EX x. P | Q(x)";`
`       `
`    58 `
`       `
`    59 `
`       `
`    60 `
`       `
`    61  (***** Generating clauses for the Meson Proof Procedure *****)`
`       `
`    62 `
`       `
`    63  (*** Disjunctions ***)`
`       `
`    64 `
`       `
`    65  val disj_assoc = prove_fun "(P|Q)|R ==> P|(Q|R)";`
`       `
`    66 `
`       `
`    67  val disj_comm = prove_fun "P|Q ==> Q|P";`
`       `
`    68 `
`       `
`    69  val disj_FalseD1 = prove_fun "False|P ==> P";`
`       `
`    70  val disj_FalseD2 = prove_fun "P|False ==> P";`
`       `
`    71 `
`    34 `
`    72 `
`    35 `
`    73  (**** Operators for forward proof ****)`
`    36  (**** Operators for forward proof ****)`
`    74 `
`    37 `
`    75  (*raises exception if no rules apply -- unlike RL*)`
`    38  (*raises exception if no rules apply -- unlike RL*)`