src/Sequents/LK0.ML
author nipkow
Wed, 04 Aug 2004 11:25:08 +0200
changeset 15106 e8cef6993701
parent 9259 103acc345f75
child 17481 75166ebb619b
permissions -rw-r--r--
aded comment
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
7093
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
     1
(*  Title:      LK/LK0
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
     2
    ID:         $Id$
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
     4
    Copyright   1992  University of Cambridge
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
     5
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
     6
Tactics and lemmas for LK (thanks also to Philippe de Groote)  
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
     7
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
     8
Structural rules by Soren Heilmann
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
     9
*)
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    10
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    11
(** Structural Rules on formulas **)
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    12
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    13
(*contraction*)
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    14
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    15
Goal "$H |- $E, P, P, $F ==> $H |- $E, P, $F";
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    16
by (etac contRS 1);
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    17
qed "contR";
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    18
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    19
Goal "$H, P, P, $G |- $E ==> $H, P, $G |- $E";
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    20
by (etac contLS 1);
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    21
qed "contL";
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    22
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    23
(*thinning*)
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    24
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    25
Goal "$H |- $E, $F ==> $H |- $E, P, $F";
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    26
by (etac thinRS 1);
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    27
qed "thinR";
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    28
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    29
Goal "$H, $G |- $E ==> $H, P, $G |- $E";
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    30
by (etac thinLS 1);
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    31
qed "thinL";
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    32
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    33
(*exchange*)
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    34
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    35
Goal "$H |- $E, Q, P, $F ==> $H |- $E, P, Q, $F";
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    36
by (etac exchRS 1);
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    37
qed "exchR";
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    38
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    39
Goal "$H, Q, P, $G |- $E ==> $H, P, Q, $G |- $E";
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    40
by (etac exchLS 1);
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    41
qed "exchL";
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    42
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    43
(*Cut and thin, replacing the right-side formula*)
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    44
fun cutR_tac (sP: string) i = 
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    45
    res_inst_tac [ ("P",sP) ] cut i  THEN  rtac thinR i;
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    46
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    47
(*Cut and thin, replacing the left-side formula*)
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    48
fun cutL_tac (sP: string) i = 
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    49
    res_inst_tac [ ("P",sP) ] cut i  THEN  rtac thinL (i+1);
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    50
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    51
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    52
(** If-and-only-if rules **)
7122
87b233b31889 renamed ...thm_pack... to ...pack...
paulson
parents: 7093
diff changeset
    53
Goalw [iff_def] 
87b233b31889 renamed ...thm_pack... to ...pack...
paulson
parents: 7093
diff changeset
    54
    "[| $H,P |- $E,Q,$F;  $H,Q |- $E,P,$F |] ==> $H |- $E, P <-> Q, $F";
87b233b31889 renamed ...thm_pack... to ...pack...
paulson
parents: 7093
diff changeset
    55
by (REPEAT (ares_tac [conjR,impR] 1));
87b233b31889 renamed ...thm_pack... to ...pack...
paulson
parents: 7093
diff changeset
    56
qed "iffR";
87b233b31889 renamed ...thm_pack... to ...pack...
paulson
parents: 7093
diff changeset
    57
87b233b31889 renamed ...thm_pack... to ...pack...
paulson
parents: 7093
diff changeset
    58
Goalw [iff_def] 
87b233b31889 renamed ...thm_pack... to ...pack...
paulson
parents: 7093
diff changeset
    59
    "[| $H,$G |- $E,P,Q;  $H,Q,P,$G |- $E |] ==> $H, P <-> Q, $G |- $E";
87b233b31889 renamed ...thm_pack... to ...pack...
paulson
parents: 7093
diff changeset
    60
by (REPEAT (ares_tac [conjL,impL,basic] 1));
87b233b31889 renamed ...thm_pack... to ...pack...
paulson
parents: 7093
diff changeset
    61
qed "iffL";
87b233b31889 renamed ...thm_pack... to ...pack...
paulson
parents: 7093
diff changeset
    62
87b233b31889 renamed ...thm_pack... to ...pack...
paulson
parents: 7093
diff changeset
    63
Goal "$H |- $E, (P <-> P), $F";
87b233b31889 renamed ...thm_pack... to ...pack...
paulson
parents: 7093
diff changeset
    64
by (REPEAT (resolve_tac [iffR,basic] 1));
87b233b31889 renamed ...thm_pack... to ...pack...
paulson
parents: 7093
diff changeset
    65
qed "iff_refl";
7093
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    66
7122
87b233b31889 renamed ...thm_pack... to ...pack...
paulson
parents: 7093
diff changeset
    67
Goalw [True_def] "$H |- $E, True, $F";
87b233b31889 renamed ...thm_pack... to ...pack...
paulson
parents: 7093
diff changeset
    68
by (rtac impR 1);
87b233b31889 renamed ...thm_pack... to ...pack...
paulson
parents: 7093
diff changeset
    69
by (rtac basic 1);
87b233b31889 renamed ...thm_pack... to ...pack...
paulson
parents: 7093
diff changeset
    70
qed "TrueR";
7093
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    71
7122
87b233b31889 renamed ...thm_pack... to ...pack...
paulson
parents: 7093
diff changeset
    72
(*Descriptions*)
87b233b31889 renamed ...thm_pack... to ...pack...
paulson
parents: 7093
diff changeset
    73
val [p1,p2] = Goal
87b233b31889 renamed ...thm_pack... to ...pack...
paulson
parents: 7093
diff changeset
    74
    "[| $H |- $E, P(a), $F;  !!x. $H, P(x) |- $E, x=a, $F |] \
87b233b31889 renamed ...thm_pack... to ...pack...
paulson
parents: 7093
diff changeset
    75
\    ==> $H |- $E, (THE x. P(x)) = a, $F";
87b233b31889 renamed ...thm_pack... to ...pack...
paulson
parents: 7093
diff changeset
    76
by (rtac cut 1);
87b233b31889 renamed ...thm_pack... to ...pack...
paulson
parents: 7093
diff changeset
    77
by (rtac p2 2);
87b233b31889 renamed ...thm_pack... to ...pack...
paulson
parents: 7093
diff changeset
    78
by (rtac The 1 THEN rtac thinR 1 THEN rtac exchRS 1 THEN rtac p1 1);
87b233b31889 renamed ...thm_pack... to ...pack...
paulson
parents: 7093
diff changeset
    79
by (rtac thinR 1 THEN rtac exchRS 1 THEN rtac p2 1);
87b233b31889 renamed ...thm_pack... to ...pack...
paulson
parents: 7093
diff changeset
    80
qed "the_equality";
7093
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    81
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    82
(** Weakened quantifier rules.  Incomplete, they let the search terminate.**)
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    83
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    84
Goal "$H, P(x), $G |- $E ==> $H, ALL x. P(x), $G |- $E";
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    85
by (rtac allL 1);
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    86
by (etac thinL 1);
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    87
qed "allL_thin";
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    88
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    89
Goal "$H |- $E, P(x), $F ==> $H |- $E, EX x. P(x), $F";
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    90
by (rtac exR 1);
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    91
by (etac thinR 1);
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    92
qed "exR_thin";
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    93
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    94
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    95
(*The rules of LK*)
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    96
val prop_pack = empty_pack add_safes 
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    97
                [basic, refl, TrueR, FalseL, 
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    98
		 conjL, conjR, disjL, disjR, impL, impR, 
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    99
                 notL, notR, iffL, iffR];
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   100
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   101
val LK_pack = prop_pack add_safes   [allR, exL] 
7122
87b233b31889 renamed ...thm_pack... to ...pack...
paulson
parents: 7093
diff changeset
   102
                        add_unsafes [allL_thin, exR_thin, the_equality];
7093
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   103
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   104
val LK_dup_pack = prop_pack add_safes   [allR, exL] 
7122
87b233b31889 renamed ...thm_pack... to ...pack...
paulson
parents: 7093
diff changeset
   105
                            add_unsafes [allL, exR, the_equality];
7093
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   106
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   107
7122
87b233b31889 renamed ...thm_pack... to ...pack...
paulson
parents: 7093
diff changeset
   108
pack_ref() := LK_pack;
7093
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   109
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   110
fun lemma_tac th i = 
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   111
    rtac (thinR RS cut) i THEN REPEAT (rtac thinL i) THEN rtac th i;
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   112
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   113
val [major,minor] = goal thy 
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   114
    "[| $H |- $E, $F, P --> Q;  $H |- $E, $F, P |] ==> $H |- $E, Q, $F";
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   115
by (rtac (thinRS RS cut) 1 THEN rtac major 1);
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   116
by (Step_tac 1);
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   117
by (rtac thinR 1 THEN rtac minor 1);
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   118
qed "mp_R";
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   119
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   120
val [major,minor] = goal thy 
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   121
    "[| $H, $G |- $E, P --> Q;  $H, $G, Q |- $E |] ==> $H, P, $G |- $E";
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   122
by (rtac (thinL RS cut) 1 THEN rtac major 1);
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   123
by (Step_tac 1);
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   124
by (rtac thinL 1 THEN rtac minor 1);
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   125
qed "mp_L";
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   126
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   127
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   128
(** Two rules to generate left- and right- rules from implications **)
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   129
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   130
val [major,minor] = goal thy 
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   131
    "[| |- P --> Q;  $H |- $E, $F, P |] ==> $H |- $E, Q, $F";
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   132
by (rtac mp_R 1);
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   133
by (rtac minor 2);
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   134
by (rtac thinRS 1 THEN rtac (major RS thinLS) 1);
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   135
qed "R_of_imp";
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   136
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   137
val [major,minor] = goal thy 
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   138
    "[| |- P --> Q;  $H, $G, Q |- $E |] ==> $H, P, $G |- $E";
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   139
by (rtac mp_L 1);
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   140
by (rtac minor 2);
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   141
by (rtac thinRS 1 THEN rtac (major RS thinLS) 1);
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   142
qed "L_of_imp";
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   143
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   144
(*Can be used to create implications in a subgoal*)
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   145
val [prem] = goal thy 
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   146
    "[| $H, $G |- $E, $F, P --> Q |] ==> $H, P, $G |- $E, Q, $F";
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   147
by (rtac mp_L 1);
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   148
by (rtac basic 2);
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   149
by (rtac thinR 1 THEN rtac prem 1);
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   150
qed "backwards_impR";
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   151
9259
103acc345f75 removal of batch style, and tidying
paulson
parents: 7122
diff changeset
   152
Goal "|-P&Q ==> |-P";
103acc345f75 removal of batch style, and tidying
paulson
parents: 7122
diff changeset
   153
by (etac (thinR RS cut) 1);
103acc345f75 removal of batch style, and tidying
paulson
parents: 7122
diff changeset
   154
by (Fast_tac 1);		
103acc345f75 removal of batch style, and tidying
paulson
parents: 7122
diff changeset
   155
qed "conjunct1";
7093
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   156
9259
103acc345f75 removal of batch style, and tidying
paulson
parents: 7122
diff changeset
   157
Goal "|-P&Q ==> |-Q";
103acc345f75 removal of batch style, and tidying
paulson
parents: 7122
diff changeset
   158
by (etac (thinR RS cut) 1);
103acc345f75 removal of batch style, and tidying
paulson
parents: 7122
diff changeset
   159
by (Fast_tac 1);		
103acc345f75 removal of batch style, and tidying
paulson
parents: 7122
diff changeset
   160
qed "conjunct2";
7093
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   161
9259
103acc345f75 removal of batch style, and tidying
paulson
parents: 7122
diff changeset
   162
Goal "|- (ALL x. P(x)) ==> |- P(x)";
103acc345f75 removal of batch style, and tidying
paulson
parents: 7122
diff changeset
   163
by (etac (thinR RS cut) 1);
103acc345f75 removal of batch style, and tidying
paulson
parents: 7122
diff changeset
   164
by (Fast_tac 1);		
103acc345f75 removal of batch style, and tidying
paulson
parents: 7122
diff changeset
   165
qed "spec";
7093
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   166
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   167
(** Equality **)
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   168
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   169
Goal "|- a=b --> b=a";
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   170
by (safe_tac (LK_pack add_safes [subst]) 1);
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   171
qed "sym";
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   172
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   173
Goal "|- a=b --> b=c --> a=c";
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   174
by (safe_tac (LK_pack add_safes [subst]) 1);
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   175
qed "trans";
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   176
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   177
(* Symmetry of equality in hypotheses *)
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   178
bind_thm ("symL", sym RS L_of_imp);
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   179
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   180
(* Symmetry of equality in hypotheses *)
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   181
bind_thm ("symR", sym RS R_of_imp);
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   182
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   183
Goal "[| $H|- $E, $F, a=b;  $H|- $E, $F, b=c |] ==> $H|- $E, a=c, $F";
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   184
by (rtac (trans RS R_of_imp RS mp_R) 1);
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   185
by (ALLGOALS assume_tac);
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   186
qed "transR";
7122
87b233b31889 renamed ...thm_pack... to ...pack...
paulson
parents: 7093
diff changeset
   187
87b233b31889 renamed ...thm_pack... to ...pack...
paulson
parents: 7093
diff changeset
   188
87b233b31889 renamed ...thm_pack... to ...pack...
paulson
parents: 7093
diff changeset
   189
(* Two theorms for rewriting only one instance of a definition:
87b233b31889 renamed ...thm_pack... to ...pack...
paulson
parents: 7093
diff changeset
   190
   the first for definitions of formulae and the second for terms *)
87b233b31889 renamed ...thm_pack... to ...pack...
paulson
parents: 7093
diff changeset
   191
87b233b31889 renamed ...thm_pack... to ...pack...
paulson
parents: 7093
diff changeset
   192
val prems = goal thy "(A == B) ==> |- A <-> B";
87b233b31889 renamed ...thm_pack... to ...pack...
paulson
parents: 7093
diff changeset
   193
by (rewrite_goals_tac prems);
87b233b31889 renamed ...thm_pack... to ...pack...
paulson
parents: 7093
diff changeset
   194
by (rtac iff_refl 1);
87b233b31889 renamed ...thm_pack... to ...pack...
paulson
parents: 7093
diff changeset
   195
qed "def_imp_iff";
87b233b31889 renamed ...thm_pack... to ...pack...
paulson
parents: 7093
diff changeset
   196
87b233b31889 renamed ...thm_pack... to ...pack...
paulson
parents: 7093
diff changeset
   197
val prems = goal thy "(A == B) ==> |- A = B";
87b233b31889 renamed ...thm_pack... to ...pack...
paulson
parents: 7093
diff changeset
   198
by (rewrite_goals_tac prems);
87b233b31889 renamed ...thm_pack... to ...pack...
paulson
parents: 7093
diff changeset
   199
by (rtac refl 1);
87b233b31889 renamed ...thm_pack... to ...pack...
paulson
parents: 7093
diff changeset
   200
qed "meta_eq_to_obj_eq";