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
     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 (* "Axiom" of Choice, proved using the description operator *)
    10 
    11 Goal "ALL x. EX y. Q x y ==> EX f. ALL x. Q x (f x)";
    12 by (fast_tac (claset() addEs [someI]) 1);
    13 qed "choice";
    14 
    15 
    16 (* Generation of contrapositives *)
    17 
    18 (*Inserts negated disjunct after removing the negation; P is a literal*)
    19 val [major,minor] = Goal "~P|Q ==> ((~P==>P) ==> Q)";
    20 by (rtac (major RS disjE) 1);
    21 by (rtac notE 1);
    22 by (etac minor 2);
    23 by (ALLGOALS assume_tac);
    24 qed "make_neg_rule";
    25 
    26 (*For Plaisted's "Postive refinement" of the MESON procedure*)
    27 Goal "~P|Q ==> (P ==> Q)";
    28 by (Blast_tac 1);
    29 qed "make_refined_neg_rule";
    30 
    31 (*P should be a literal*)
    32 val [major,minor] = Goal "P|Q ==> ((P==>~P) ==> Q)";
    33 by (rtac (major RS disjE) 1);
    34 by (rtac notE 1);
    35 by (etac minor 1);
    36 by (ALLGOALS assume_tac);
    37 qed "make_pos_rule";
    38 
    39 
    40 (* Generation of a goal clause -- put away the final literal *)
    41 
    42 val [major,minor] = Goal "~P ==> ((~P==>P) ==> False)";
    43 by (rtac notE 1);
    44 by (rtac minor 2);
    45 by (ALLGOALS (rtac major));
    46 qed "make_neg_goal";
    47 
    48 val [major,minor] = Goal "P ==> ((P==>~P) ==> False)";
    49 by (rtac notE 1);
    50 by (rtac minor 1);
    51 by (ALLGOALS (rtac major));
    52 qed "make_pos_goal";
    53 
    54 
    55 (* Lemmas for forward proof (like congruence rules) *)
    56 
    57 (*NOTE: could handle conjunctions (faster?) by
    58     nf(th RS conjunct2) RS (nf(th RS conjunct1) RS conjI) *)
    59 val major::prems = Goal
    60     "[| P'&Q';  P' ==> P;  Q' ==> Q |] ==> P&Q";
    61 by (rtac (major RS conjE) 1);
    62 by (rtac conjI 1);
    63 by (ALLGOALS (eresolve_tac prems));
    64 qed "conj_forward";
    65 
    66 val major::prems = Goal
    67     "[| P'|Q';  P' ==> P;  Q' ==> Q |] ==> P|Q";
    68 by (rtac (major RS disjE) 1);
    69 by (ALLGOALS (dresolve_tac prems));
    70 by (ALLGOALS (eresolve_tac [disjI1,disjI2]));
    71 qed "disj_forward";
    72 
    73 (*Version for removal of duplicate literals*)
    74 val major::prems = Goal
    75     "[| P'|Q';  P' ==> P;  [| Q'; P==>False |] ==> Q |] ==> P|Q";
    76 by (cut_facts_tac [major] 1);
    77 by (blast_tac (claset() addIs prems) 1);
    78 qed "disj_forward2";
    79 
    80 val major::prems = Goal
    81     "[| ALL x. P'(x);  !!x. P'(x) ==> P(x) |] ==> ALL x. P(x)";
    82 by (rtac allI 1);
    83 by (resolve_tac prems 1);
    84 by (rtac (major RS spec) 1);
    85 qed "all_forward";
    86 
    87 val major::prems = Goal
    88     "[| EX x. P'(x);  !!x. P'(x) ==> P(x) |] ==> EX x. P(x)";
    89 by (rtac (major RS exE) 1);
    90 by (rtac exI 1);
    91 by (eresolve_tac prems 1);
    92 qed "ex_forward";