author | paulson |
Tue, 11 May 2004 10:48:00 +0200 | |
changeset 14733 | 3eda95792083 |
parent 11460 | e5fb885bfe3a |
permissions | -rw-r--r-- |
9869 | 1 |
(* Title: HOL/meson_lemmas.ML |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1992 University of Cambridge |
|
5 |
||
6 |
Lemmas for Meson. |
|
7 |
*) |
|
8 |
||
9 |
(* Generation of contrapositives *) |
|
10 |
||
14733
3eda95792083
conversion to clauses for ordinary resolution rather than ME
paulson
parents:
11460
diff
changeset
|
11 |
(*Inserts negated disjunct after removing the negation; P is a literal. |
3eda95792083
conversion to clauses for ordinary resolution rather than ME
paulson
parents:
11460
diff
changeset
|
12 |
Model elimination requires assuming the negation of every attempted subgoal, |
3eda95792083
conversion to clauses for ordinary resolution rather than ME
paulson
parents:
11460
diff
changeset
|
13 |
hence the negated disjuncts.*) |
9869 | 14 |
val [major,minor] = Goal "~P|Q ==> ((~P==>P) ==> Q)"; |
15 |
by (rtac (major RS disjE) 1); |
|
16 |
by (rtac notE 1); |
|
17 |
by (etac minor 2); |
|
18 |
by (ALLGOALS assume_tac); |
|
19 |
qed "make_neg_rule"; |
|
20 |
||
21 |
(*For Plaisted's "Postive refinement" of the MESON procedure*) |
|
22 |
Goal "~P|Q ==> (P ==> Q)"; |
|
23 |
by (Blast_tac 1); |
|
24 |
qed "make_refined_neg_rule"; |
|
25 |
||
26 |
(*P should be a literal*) |
|
27 |
val [major,minor] = Goal "P|Q ==> ((P==>~P) ==> Q)"; |
|
28 |
by (rtac (major RS disjE) 1); |
|
29 |
by (rtac notE 1); |
|
30 |
by (etac minor 1); |
|
31 |
by (ALLGOALS assume_tac); |
|
32 |
qed "make_pos_rule"; |
|
33 |
||
14733
3eda95792083
conversion to clauses for ordinary resolution rather than ME
paulson
parents:
11460
diff
changeset
|
34 |
(** Versions of make_neg_rule and make_pos_rule that don't insert new |
3eda95792083
conversion to clauses for ordinary resolution rather than ME
paulson
parents:
11460
diff
changeset
|
35 |
assumptions, for ordinary resolution. **) |
3eda95792083
conversion to clauses for ordinary resolution rather than ME
paulson
parents:
11460
diff
changeset
|
36 |
|
3eda95792083
conversion to clauses for ordinary resolution rather than ME
paulson
parents:
11460
diff
changeset
|
37 |
val make_neg_rule' = make_refined_neg_rule; |
3eda95792083
conversion to clauses for ordinary resolution rather than ME
paulson
parents:
11460
diff
changeset
|
38 |
|
3eda95792083
conversion to clauses for ordinary resolution rather than ME
paulson
parents:
11460
diff
changeset
|
39 |
Goal "[|P|Q; ~P|] ==> Q"; |
3eda95792083
conversion to clauses for ordinary resolution rather than ME
paulson
parents:
11460
diff
changeset
|
40 |
by (Blast_tac 1); |
3eda95792083
conversion to clauses for ordinary resolution rather than ME
paulson
parents:
11460
diff
changeset
|
41 |
qed "make_pos_rule'"; |
9869 | 42 |
|
43 |
(* Generation of a goal clause -- put away the final literal *) |
|
44 |
||
45 |
val [major,minor] = Goal "~P ==> ((~P==>P) ==> False)"; |
|
46 |
by (rtac notE 1); |
|
47 |
by (rtac minor 2); |
|
48 |
by (ALLGOALS (rtac major)); |
|
49 |
qed "make_neg_goal"; |
|
50 |
||
51 |
val [major,minor] = Goal "P ==> ((P==>~P) ==> False)"; |
|
52 |
by (rtac notE 1); |
|
53 |
by (rtac minor 1); |
|
54 |
by (ALLGOALS (rtac major)); |
|
55 |
qed "make_pos_goal"; |
|
56 |
||
57 |
||
58 |
(* Lemmas for forward proof (like congruence rules) *) |
|
59 |
||
60 |
(*NOTE: could handle conjunctions (faster?) by |
|
61 |
nf(th RS conjunct2) RS (nf(th RS conjunct1) RS conjI) *) |
|
62 |
val major::prems = Goal |
|
63 |
"[| P'&Q'; P' ==> P; Q' ==> Q |] ==> P&Q"; |
|
64 |
by (rtac (major RS conjE) 1); |
|
65 |
by (rtac conjI 1); |
|
66 |
by (ALLGOALS (eresolve_tac prems)); |
|
67 |
qed "conj_forward"; |
|
68 |
||
69 |
val major::prems = Goal |
|
70 |
"[| P'|Q'; P' ==> P; Q' ==> Q |] ==> P|Q"; |
|
71 |
by (rtac (major RS disjE) 1); |
|
72 |
by (ALLGOALS (dresolve_tac prems)); |
|
73 |
by (ALLGOALS (eresolve_tac [disjI1,disjI2])); |
|
74 |
qed "disj_forward"; |
|
75 |
||
76 |
(*Version for removal of duplicate literals*) |
|
77 |
val major::prems = Goal |
|
78 |
"[| P'|Q'; P' ==> P; [| Q'; P==>False |] ==> Q |] ==> P|Q"; |
|
79 |
by (cut_facts_tac [major] 1); |
|
80 |
by (blast_tac (claset() addIs prems) 1); |
|
81 |
qed "disj_forward2"; |
|
82 |
||
83 |
val major::prems = Goal |
|
84 |
"[| ALL x. P'(x); !!x. P'(x) ==> P(x) |] ==> ALL x. P(x)"; |
|
85 |
by (rtac allI 1); |
|
86 |
by (resolve_tac prems 1); |
|
87 |
by (rtac (major RS spec) 1); |
|
88 |
qed "all_forward"; |
|
89 |
||
90 |
val major::prems = Goal |
|
91 |
"[| EX x. P'(x); !!x. P'(x) ==> P(x) |] ==> EX x. P(x)"; |
|
92 |
by (rtac (major RS exE) 1); |
|
93 |
by (rtac exI 1); |
|
94 |
by (eresolve_tac prems 1); |
|
95 |
qed "ex_forward"; |