src/HOL/meson_lemmas.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/meson_lemmas.ML	Tue Sep 05 21:06:01 2000 +0200
@@ -0,0 +1,92 @@
+(*  Title:      HOL/meson_lemmas.ML
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1992  University of Cambridge
+
+Lemmas for Meson.
+*)
+
+(* "Axiom" of Choice, proved using the description operator *)
+
+Goal "ALL x. EX y. Q x y ==> EX f. ALL x. Q x (f x)";
+by (fast_tac (claset() addEs [selectI]) 1);
+qed "choice";
+
+
+(* Generation of contrapositives *)
+
+(*Inserts negated disjunct after removing the negation; P is a literal*)
+val [major,minor] = Goal "~P|Q ==> ((~P==>P) ==> Q)";
+by (rtac (major RS disjE) 1);
+by (rtac notE 1);
+by (etac minor 2);
+by (ALLGOALS assume_tac);
+qed "make_neg_rule";
+
+(*For Plaisted's "Postive refinement" of the MESON procedure*)
+Goal "~P|Q ==> (P ==> Q)";
+by (Blast_tac 1);
+qed "make_refined_neg_rule";
+
+(*P should be a literal*)
+val [major,minor] = Goal "P|Q ==> ((P==>~P) ==> Q)";
+by (rtac (major RS disjE) 1);
+by (rtac notE 1);
+by (etac minor 1);
+by (ALLGOALS assume_tac);
+qed "make_pos_rule";
+
+
+(* Generation of a goal clause -- put away the final literal *)
+
+val [major,minor] = Goal "~P ==> ((~P==>P) ==> False)";
+by (rtac notE 1);
+by (rtac minor 2);
+by (ALLGOALS (rtac major));
+qed "make_neg_goal";
+
+val [major,minor] = Goal "P ==> ((P==>~P) ==> False)";
+by (rtac notE 1);
+by (rtac minor 1);
+by (ALLGOALS (rtac major));
+qed "make_pos_goal";
+
+
+(* Lemmas for forward proof (like congruence rules) *)
+
+(*NOTE: could handle conjunctions (faster?) by
+    nf(th RS conjunct2) RS (nf(th RS conjunct1) RS conjI) *)
+val major::prems = Goal
+    "[| P'&Q';  P' ==> P;  Q' ==> Q |] ==> P&Q";
+by (rtac (major RS conjE) 1);
+by (rtac conjI 1);
+by (ALLGOALS (eresolve_tac prems));
+qed "conj_forward";
+
+val major::prems = Goal
+    "[| P'|Q';  P' ==> P;  Q' ==> Q |] ==> P|Q";
+by (rtac (major RS disjE) 1);
+by (ALLGOALS (dresolve_tac prems));
+by (ALLGOALS (eresolve_tac [disjI1,disjI2]));
+qed "disj_forward";
+
+(*Version for removal of duplicate literals*)
+val major::prems = Goal
+    "[| P'|Q';  P' ==> P;  [| Q'; P==>False |] ==> Q |] ==> P|Q";
+by (cut_facts_tac [major] 1);
+by (blast_tac (claset() addIs prems) 1);
+qed "disj_forward2";
+
+val major::prems = Goal
+    "[| ALL x. P'(x);  !!x. P'(x) ==> P(x) |] ==> ALL x. P(x)";
+by (rtac allI 1);
+by (resolve_tac prems 1);
+by (rtac (major RS spec) 1);
+qed "all_forward";
+
+val major::prems = Goal
+    "[| EX x. P'(x);  !!x. P'(x) ==> P(x) |] ==> EX x. P(x)";
+by (rtac (major RS exE) 1);
+by (rtac exI 1);
+by (eresolve_tac prems 1);
+qed "ex_forward";