src/HOL/meson_lemmas.ML
 author nipkow Fri, 24 Nov 2000 16:49:27 +0100 changeset 10519 ade64af4c57c parent 9970 dfe4747c8318 child 11460 e5fb885bfe3a permissions -rw-r--r--
hide many names from Datatype_Universe.
```
(*  Title:      HOL/meson_lemmas.ML
ID:         \$Id\$
Author:     Lawrence C Paulson, Cambridge University Computer Laboratory

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 [someI]) 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";
```