src/HOL/meson_lemmas.ML
author oheimb
Wed Jan 31 10:15:55 2001 +0100 (2001-01-31)
changeset 11008 f7333f055ef6
parent 9970 dfe4747c8318
child 11460 e5fb885bfe3a
permissions -rw-r--r--
improved theory reference in comment
wenzelm@9869
     1
(*  Title:      HOL/meson_lemmas.ML
wenzelm@9869
     2
    ID:         $Id$
wenzelm@9869
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
wenzelm@9869
     4
    Copyright   1992  University of Cambridge
wenzelm@9869
     5
wenzelm@9869
     6
Lemmas for Meson.
wenzelm@9869
     7
*)
wenzelm@9869
     8
wenzelm@9869
     9
(* "Axiom" of Choice, proved using the description operator *)
wenzelm@9869
    10
wenzelm@9869
    11
Goal "ALL x. EX y. Q x y ==> EX f. ALL x. Q x (f x)";
paulson@9970
    12
by (fast_tac (claset() addEs [someI]) 1);
wenzelm@9869
    13
qed "choice";
wenzelm@9869
    14
wenzelm@9869
    15
wenzelm@9869
    16
(* Generation of contrapositives *)
wenzelm@9869
    17
wenzelm@9869
    18
(*Inserts negated disjunct after removing the negation; P is a literal*)
wenzelm@9869
    19
val [major,minor] = Goal "~P|Q ==> ((~P==>P) ==> Q)";
wenzelm@9869
    20
by (rtac (major RS disjE) 1);
wenzelm@9869
    21
by (rtac notE 1);
wenzelm@9869
    22
by (etac minor 2);
wenzelm@9869
    23
by (ALLGOALS assume_tac);
wenzelm@9869
    24
qed "make_neg_rule";
wenzelm@9869
    25
wenzelm@9869
    26
(*For Plaisted's "Postive refinement" of the MESON procedure*)
wenzelm@9869
    27
Goal "~P|Q ==> (P ==> Q)";
wenzelm@9869
    28
by (Blast_tac 1);
wenzelm@9869
    29
qed "make_refined_neg_rule";
wenzelm@9869
    30
wenzelm@9869
    31
(*P should be a literal*)
wenzelm@9869
    32
val [major,minor] = Goal "P|Q ==> ((P==>~P) ==> Q)";
wenzelm@9869
    33
by (rtac (major RS disjE) 1);
wenzelm@9869
    34
by (rtac notE 1);
wenzelm@9869
    35
by (etac minor 1);
wenzelm@9869
    36
by (ALLGOALS assume_tac);
wenzelm@9869
    37
qed "make_pos_rule";
wenzelm@9869
    38
wenzelm@9869
    39
wenzelm@9869
    40
(* Generation of a goal clause -- put away the final literal *)
wenzelm@9869
    41
wenzelm@9869
    42
val [major,minor] = Goal "~P ==> ((~P==>P) ==> False)";
wenzelm@9869
    43
by (rtac notE 1);
wenzelm@9869
    44
by (rtac minor 2);
wenzelm@9869
    45
by (ALLGOALS (rtac major));
wenzelm@9869
    46
qed "make_neg_goal";
wenzelm@9869
    47
wenzelm@9869
    48
val [major,minor] = Goal "P ==> ((P==>~P) ==> False)";
wenzelm@9869
    49
by (rtac notE 1);
wenzelm@9869
    50
by (rtac minor 1);
wenzelm@9869
    51
by (ALLGOALS (rtac major));
wenzelm@9869
    52
qed "make_pos_goal";
wenzelm@9869
    53
wenzelm@9869
    54
wenzelm@9869
    55
(* Lemmas for forward proof (like congruence rules) *)
wenzelm@9869
    56
wenzelm@9869
    57
(*NOTE: could handle conjunctions (faster?) by
wenzelm@9869
    58
    nf(th RS conjunct2) RS (nf(th RS conjunct1) RS conjI) *)
wenzelm@9869
    59
val major::prems = Goal
wenzelm@9869
    60
    "[| P'&Q';  P' ==> P;  Q' ==> Q |] ==> P&Q";
wenzelm@9869
    61
by (rtac (major RS conjE) 1);
wenzelm@9869
    62
by (rtac conjI 1);
wenzelm@9869
    63
by (ALLGOALS (eresolve_tac prems));
wenzelm@9869
    64
qed "conj_forward";
wenzelm@9869
    65
wenzelm@9869
    66
val major::prems = Goal
wenzelm@9869
    67
    "[| P'|Q';  P' ==> P;  Q' ==> Q |] ==> P|Q";
wenzelm@9869
    68
by (rtac (major RS disjE) 1);
wenzelm@9869
    69
by (ALLGOALS (dresolve_tac prems));
wenzelm@9869
    70
by (ALLGOALS (eresolve_tac [disjI1,disjI2]));
wenzelm@9869
    71
qed "disj_forward";
wenzelm@9869
    72
wenzelm@9869
    73
(*Version for removal of duplicate literals*)
wenzelm@9869
    74
val major::prems = Goal
wenzelm@9869
    75
    "[| P'|Q';  P' ==> P;  [| Q'; P==>False |] ==> Q |] ==> P|Q";
wenzelm@9869
    76
by (cut_facts_tac [major] 1);
wenzelm@9869
    77
by (blast_tac (claset() addIs prems) 1);
wenzelm@9869
    78
qed "disj_forward2";
wenzelm@9869
    79
wenzelm@9869
    80
val major::prems = Goal
wenzelm@9869
    81
    "[| ALL x. P'(x);  !!x. P'(x) ==> P(x) |] ==> ALL x. P(x)";
wenzelm@9869
    82
by (rtac allI 1);
wenzelm@9869
    83
by (resolve_tac prems 1);
wenzelm@9869
    84
by (rtac (major RS spec) 1);
wenzelm@9869
    85
qed "all_forward";
wenzelm@9869
    86
wenzelm@9869
    87
val major::prems = Goal
wenzelm@9869
    88
    "[| EX x. P'(x);  !!x. P'(x) ==> P(x) |] ==> EX x. P(x)";
wenzelm@9869
    89
by (rtac (major RS exE) 1);
wenzelm@9869
    90
by (rtac exI 1);
wenzelm@9869
    91
by (eresolve_tac prems 1);
wenzelm@9869
    92
qed "ex_forward";