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