# HG changeset patch
# User wenzelm
# Date 1006796057 -3600
# Node ID 2c76042c3b06941fad81ec3013d844c3b275b332
# Parent  b344486c33e2800fe4fd8bd55708d11fd82bb5a0
moved lemmas to theory Hilbert_Choice;

diff -r b344486c33e2 -r 2c76042c3b06 src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Mon Nov 26 18:33:57 2001 +0100
+++ b/src/HOL/Tools/meson.ML	Mon Nov 26 18:34:17 2001 +0100
@@ -13,61 +13,24 @@
 
 local
 
- (*Prove theorems using fast_tac*)
- fun prove_fun s =
-     prove_goal (the_context ()) s
-          (fn prems => [ cut_facts_tac prems 1, Fast_tac 1 ]);
-
- (**** Negation Normal Form ****)
-
- (*** de Morgan laws ***)
-
- val not_conjD = prove_fun "~(P&Q) ==> ~P | ~Q";
- val not_disjD = prove_fun "~(P|Q) ==> ~P & ~Q";
- val not_notD = prove_fun "~~P ==> P";
- val not_allD = prove_fun  "~(ALL x. P(x)) ==> EX x. ~P(x)";
- val not_exD = prove_fun   "~(EX x. P(x)) ==> ALL x. ~P(x)";
-
-
- (*** Removal of --> and <-> (positive and negative occurrences) ***)
-
- val imp_to_disjD = prove_fun "P-->Q ==> ~P | Q";
- val not_impD = prove_fun   "~(P-->Q) ==> P & ~Q";
-
- val iff_to_disjD = prove_fun "P=Q ==> (~P | Q) & (~Q | P)";
-
- (*Much more efficient than (P & ~Q) | (Q & ~P) for computing CNF*)
- val not_iffD = prove_fun "~(P=Q) ==> (P | Q) & (~P | ~Q)";
-
-
- (**** Pulling out the existential quantifiers ****)
-
- (*** Conjunction ***)
-
- val conj_exD1 = prove_fun "(EX x. P(x)) & Q ==> EX x. P(x) & Q";
- val conj_exD2 = prove_fun "P & (EX x. Q(x)) ==> EX x. P & Q(x)";
-
- (*** Disjunction ***)
-
- (*DO NOT USE with forall-Skolemization: makes fewer schematic variables!!
-   With ex-Skolemization, makes fewer Skolem constants*)
- val disj_exD = prove_fun "(EX x. P(x)) | (EX x. Q(x)) ==> EX x. P(x) | Q(x)";
-
- val disj_exD1 = prove_fun "(EX x. P(x)) | Q ==> EX x. P(x) | Q";
- val disj_exD2 = prove_fun "P | (EX x. Q(x)) ==> EX x. P | Q(x)";
-
-
-
- (***** Generating clauses for the Meson Proof Procedure *****)
-
- (*** Disjunctions ***)
-
- val disj_assoc = prove_fun "(P|Q)|R ==> P|(Q|R)";
-
- val disj_comm = prove_fun "P|Q ==> Q|P";
-
- val disj_FalseD1 = prove_fun "False|P ==> P";
- val disj_FalseD2 = prove_fun "P|False ==> P";
+ val not_conjD = thm "meson_not_conjD";
+ val not_disjD = thm "meson_not_disjD";
+ val not_notD = thm "meson_not_notD";
+ val not_allD = thm "meson_not_allD";
+ val not_exD = thm "meson_not_exD";
+ val imp_to_disjD = thm "meson_imp_to_disjD";
+ val not_impD = thm "meson_not_impD";
+ val iff_to_disjD = thm "meson_iff_to_disjD";
+ val not_iffD = thm "meson_not_iffD";
+ val conj_exD1 = thm "meson_conj_exD1";
+ val conj_exD2 = thm "meson_conj_exD2";
+ val disj_exD = thm "meson_disj_exD";
+ val disj_exD1 = thm "meson_disj_exD1";
+ val disj_exD2 = thm "meson_disj_exD2";
+ val disj_assoc = thm "meson_disj_assoc";
+ val disj_comm = thm "meson_disj_comm";
+ val disj_FalseD1 = thm "meson_disj_FalseD1";
+ val disj_FalseD2 = thm "meson_disj_FalseD2";
 
 
  (**** Operators for forward proof ****)