src/Sequents/LK.thy
author bulwahn
Tue Aug 31 08:00:53 2010 +0200 (2010-08-31)
changeset 38950 62578950e748
parent 30607 c3d1590debd8
child 41959 b460124855b8
permissions -rw-r--r--
storing options for prolog code generation in the theory
wenzelm@17481
     1
(*  Title:      LK/LK.ML
paulson@2073
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@2073
     3
    Copyright   1993  University of Cambridge
paulson@2073
     4
paulson@7094
     5
Axiom to express monotonicity (a variant of the deduction theorem).  Makes the
paulson@7094
     6
link between |- and ==>, needed for instance to prove imp_cong.
paulson@2073
     7
paulson@7117
     8
Axiom left_cong allows the simplifier to use left-side formulas.  Ideally it
paulson@7117
     9
should be derived from lower-level axioms.
paulson@7117
    10
paulson@7094
    11
CANNOT be added to LK0.thy because modal logic is built upon it, and
paulson@7094
    12
various modal rules would become inconsistent.
paulson@2073
    13
*)
paulson@2073
    14
wenzelm@17481
    15
theory LK
wenzelm@17481
    16
imports LK0
wenzelm@17481
    17
uses ("simpdata.ML")
wenzelm@17481
    18
begin
paulson@2073
    19
wenzelm@27149
    20
axiomatization where
wenzelm@27149
    21
  monotonic:  "($H |- P ==> $H |- Q) ==> $H, P |- Q" and
paulson@2073
    22
wenzelm@17481
    23
  left_cong:  "[| P == P';  |- P' ==> ($H |- $F) == ($H' |- $F') |]
wenzelm@17481
    24
               ==> (P, $H |- $F) == (P', $H' |- $F')"
paulson@2073
    25
wenzelm@27149
    26
wenzelm@27149
    27
subsection {* Rewrite rules *}
wenzelm@27149
    28
wenzelm@27149
    29
lemma conj_simps:
wenzelm@27149
    30
  "|- P & True <-> P"
wenzelm@27149
    31
  "|- True & P <-> P"
wenzelm@27149
    32
  "|- P & False <-> False"
wenzelm@27149
    33
  "|- False & P <-> False"
wenzelm@27149
    34
  "|- P & P <-> P"
wenzelm@27149
    35
  "|- P & P & Q <-> P & Q"
wenzelm@27149
    36
  "|- P & ~P <-> False"
wenzelm@27149
    37
  "|- ~P & P <-> False"
wenzelm@27149
    38
  "|- (P & Q) & R <-> P & (Q & R)"
wenzelm@27149
    39
  apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *})
wenzelm@27149
    40
  done
wenzelm@27149
    41
wenzelm@27149
    42
lemma disj_simps:
wenzelm@27149
    43
  "|- P | True <-> True"
wenzelm@27149
    44
  "|- True | P <-> True"
wenzelm@27149
    45
  "|- P | False <-> P"
wenzelm@27149
    46
  "|- False | P <-> P"
wenzelm@27149
    47
  "|- P | P <-> P"
wenzelm@27149
    48
  "|- P | P | Q <-> P | Q"
wenzelm@27149
    49
  "|- (P | Q) | R <-> P | (Q | R)"
wenzelm@27149
    50
  apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *})
wenzelm@27149
    51
  done
wenzelm@27149
    52
wenzelm@27149
    53
lemma not_simps:
wenzelm@27149
    54
  "|- ~ False <-> True"
wenzelm@27149
    55
  "|- ~ True <-> False"
wenzelm@27149
    56
  apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *})
wenzelm@27149
    57
  done
wenzelm@27149
    58
wenzelm@27149
    59
lemma imp_simps:
wenzelm@27149
    60
  "|- (P --> False) <-> ~P"
wenzelm@27149
    61
  "|- (P --> True) <-> True"
wenzelm@27149
    62
  "|- (False --> P) <-> True"
wenzelm@27149
    63
  "|- (True --> P) <-> P"
wenzelm@27149
    64
  "|- (P --> P) <-> True"
wenzelm@27149
    65
  "|- (P --> ~P) <-> ~P"
wenzelm@27149
    66
  apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *})
wenzelm@27149
    67
  done
wenzelm@27149
    68
wenzelm@27149
    69
lemma iff_simps:
wenzelm@27149
    70
  "|- (True <-> P) <-> P"
wenzelm@27149
    71
  "|- (P <-> True) <-> P"
wenzelm@27149
    72
  "|- (P <-> P) <-> True"
wenzelm@27149
    73
  "|- (False <-> P) <-> ~P"
wenzelm@27149
    74
  "|- (P <-> False) <-> ~P"
wenzelm@27149
    75
  apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *})
wenzelm@27149
    76
  done
wenzelm@27149
    77
wenzelm@27149
    78
lemma quant_simps:
wenzelm@27149
    79
  "!!P. |- (ALL x. P) <-> P"
wenzelm@27149
    80
  "!!P. |- (ALL x. x=t --> P(x)) <-> P(t)"
wenzelm@27149
    81
  "!!P. |- (ALL x. t=x --> P(x)) <-> P(t)"
wenzelm@27149
    82
  "!!P. |- (EX x. P) <-> P"
wenzelm@27149
    83
  "!!P. |- (EX x. x=t & P(x)) <-> P(t)"
wenzelm@27149
    84
  "!!P. |- (EX x. t=x & P(x)) <-> P(t)"
wenzelm@27149
    85
  apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *})
wenzelm@27149
    86
  done
wenzelm@27149
    87
wenzelm@27149
    88
wenzelm@27149
    89
subsection {* Miniscoping: pushing quantifiers in *}
wenzelm@27149
    90
wenzelm@27149
    91
text {*
wenzelm@27149
    92
  We do NOT distribute of ALL over &, or dually that of EX over |
wenzelm@27149
    93
  Baaz and Leitsch, On Skolemization and Proof Complexity (1994)
wenzelm@27149
    94
  show that this step can increase proof length!
wenzelm@27149
    95
*}
wenzelm@27149
    96
wenzelm@27149
    97
text {*existential miniscoping*}
wenzelm@27149
    98
lemma ex_simps:
wenzelm@27149
    99
  "!!P Q. |- (EX x. P(x) & Q) <-> (EX x. P(x)) & Q"
wenzelm@27149
   100
  "!!P Q. |- (EX x. P & Q(x)) <-> P & (EX x. Q(x))"
wenzelm@27149
   101
  "!!P Q. |- (EX x. P(x) | Q) <-> (EX x. P(x)) | Q"
wenzelm@27149
   102
  "!!P Q. |- (EX x. P | Q(x)) <-> P | (EX x. Q(x))"
wenzelm@27149
   103
  "!!P Q. |- (EX x. P(x) --> Q) <-> (ALL x. P(x)) --> Q"
wenzelm@27149
   104
  "!!P Q. |- (EX x. P --> Q(x)) <-> P --> (EX x. Q(x))"
wenzelm@27149
   105
  apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *})
wenzelm@27149
   106
  done
wenzelm@27149
   107
wenzelm@27149
   108
text {*universal miniscoping*}
wenzelm@27149
   109
lemma all_simps:
wenzelm@27149
   110
  "!!P Q. |- (ALL x. P(x) & Q) <-> (ALL x. P(x)) & Q"
wenzelm@27149
   111
  "!!P Q. |- (ALL x. P & Q(x)) <-> P & (ALL x. Q(x))"
wenzelm@27149
   112
  "!!P Q. |- (ALL x. P(x) --> Q) <-> (EX x. P(x)) --> Q"
wenzelm@27149
   113
  "!!P Q. |- (ALL x. P --> Q(x)) <-> P --> (ALL x. Q(x))"
wenzelm@27149
   114
  "!!P Q. |- (ALL x. P(x) | Q) <-> (ALL x. P(x)) | Q"
wenzelm@27149
   115
  "!!P Q. |- (ALL x. P | Q(x)) <-> P | (ALL x. Q(x))"
wenzelm@27149
   116
  apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *})
wenzelm@27149
   117
  done
wenzelm@27149
   118
wenzelm@27149
   119
text {*These are NOT supplied by default!*}
wenzelm@27149
   120
lemma distrib_simps:
wenzelm@27149
   121
  "|- P & (Q | R) <-> P&Q | P&R"
wenzelm@27149
   122
  "|- (Q | R) & P <-> Q&P | R&P"
wenzelm@27149
   123
  "|- (P | Q --> R) <-> (P --> R) & (Q --> R)"
wenzelm@27149
   124
  apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *})
wenzelm@27149
   125
  done
wenzelm@27149
   126
wenzelm@27149
   127
lemma P_iff_F: "|- ~P ==> |- (P <-> False)"
wenzelm@27149
   128
  apply (erule thinR [THEN cut])
wenzelm@27149
   129
  apply (tactic {* fast_tac LK_pack 1 *})
wenzelm@27149
   130
  done
wenzelm@27149
   131
wenzelm@27149
   132
lemmas iff_reflection_F = P_iff_F [THEN iff_reflection, standard]
wenzelm@27149
   133
wenzelm@27149
   134
lemma P_iff_T: "|- P ==> |- (P <-> True)"
wenzelm@27149
   135
  apply (erule thinR [THEN cut])
wenzelm@27149
   136
  apply (tactic {* fast_tac LK_pack 1 *})
wenzelm@27149
   137
  done
wenzelm@27149
   138
wenzelm@27149
   139
lemmas iff_reflection_T = P_iff_T [THEN iff_reflection, standard]
wenzelm@27149
   140
wenzelm@27149
   141
wenzelm@27149
   142
lemma LK_extra_simps:
wenzelm@27149
   143
  "|- P | ~P"
wenzelm@27149
   144
  "|- ~P | P"
wenzelm@27149
   145
  "|- ~ ~ P <-> P"
wenzelm@27149
   146
  "|- (~P --> P) <-> P"
wenzelm@27149
   147
  "|- (~P <-> ~Q) <-> (P<->Q)"
wenzelm@27149
   148
  apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *})
wenzelm@27149
   149
  done
wenzelm@27149
   150
wenzelm@27149
   151
wenzelm@27149
   152
subsection {* Named rewrite rules *}
wenzelm@27149
   153
wenzelm@27149
   154
lemma conj_commute: "|- P&Q <-> Q&P"
wenzelm@27149
   155
  and conj_left_commute: "|- P&(Q&R) <-> Q&(P&R)"
wenzelm@27149
   156
  apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *})
wenzelm@27149
   157
  done
wenzelm@27149
   158
wenzelm@27149
   159
lemmas conj_comms = conj_commute conj_left_commute
wenzelm@27149
   160
wenzelm@27149
   161
lemma disj_commute: "|- P|Q <-> Q|P"
wenzelm@27149
   162
  and disj_left_commute: "|- P|(Q|R) <-> Q|(P|R)"
wenzelm@27149
   163
  apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *})
wenzelm@27149
   164
  done
wenzelm@27149
   165
wenzelm@27149
   166
lemmas disj_comms = disj_commute disj_left_commute
wenzelm@27149
   167
wenzelm@27149
   168
lemma conj_disj_distribL: "|- P&(Q|R) <-> (P&Q | P&R)"
wenzelm@27149
   169
  and conj_disj_distribR: "|- (P|Q)&R <-> (P&R | Q&R)"
wenzelm@27149
   170
wenzelm@27149
   171
  and disj_conj_distribL: "|- P|(Q&R) <-> (P|Q) & (P|R)"
wenzelm@27149
   172
  and disj_conj_distribR: "|- (P&Q)|R <-> (P|R) & (Q|R)"
wenzelm@27149
   173
wenzelm@27149
   174
  and imp_conj_distrib: "|- (P --> (Q&R)) <-> (P-->Q) & (P-->R)"
wenzelm@27149
   175
  and imp_conj: "|- ((P&Q)-->R)   <-> (P --> (Q --> R))"
wenzelm@27149
   176
  and imp_disj: "|- (P|Q --> R)   <-> (P-->R) & (Q-->R)"
wenzelm@27149
   177
wenzelm@27149
   178
  and imp_disj1: "|- (P-->Q) | R <-> (P-->Q | R)"
wenzelm@27149
   179
  and imp_disj2: "|- Q | (P-->R) <-> (P-->Q | R)"
wenzelm@27149
   180
wenzelm@27149
   181
  and de_Morgan_disj: "|- (~(P | Q)) <-> (~P & ~Q)"
wenzelm@27149
   182
  and de_Morgan_conj: "|- (~(P & Q)) <-> (~P | ~Q)"
wenzelm@27149
   183
wenzelm@27149
   184
  and not_iff: "|- ~(P <-> Q) <-> (P <-> ~Q)"
wenzelm@27149
   185
  apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *})
wenzelm@27149
   186
  done
wenzelm@27149
   187
wenzelm@27149
   188
lemma imp_cong:
wenzelm@27149
   189
  assumes p1: "|- P <-> P'"
wenzelm@27149
   190
    and p2: "|- P' ==> |- Q <-> Q'"
wenzelm@27149
   191
  shows "|- (P-->Q) <-> (P'-->Q')"
wenzelm@27149
   192
  apply (tactic {* lemma_tac @{thm p1} 1 *})
wenzelm@27149
   193
  apply (tactic {* safe_tac LK_pack 1 *})
wenzelm@27149
   194
   apply (tactic {*
wenzelm@27149
   195
     REPEAT (rtac @{thm cut} 1 THEN
wenzelm@27149
   196
       DEPTH_SOLVE_1
wenzelm@27149
   197
         (resolve_tac [@{thm thinL}, @{thm thinR}, @{thm p2} COMP @{thm monotonic}] 1) THEN
wenzelm@27149
   198
           safe_tac LK_pack 1) *})
wenzelm@27149
   199
  done
wenzelm@27149
   200
wenzelm@27149
   201
lemma conj_cong:
wenzelm@27149
   202
  assumes p1: "|- P <-> P'"
wenzelm@27149
   203
    and p2: "|- P' ==> |- Q <-> Q'"
wenzelm@27149
   204
  shows "|- (P&Q) <-> (P'&Q')"
wenzelm@27149
   205
  apply (tactic {* lemma_tac @{thm p1} 1 *})
wenzelm@27149
   206
  apply (tactic {* safe_tac LK_pack 1 *})
wenzelm@27149
   207
   apply (tactic {*
wenzelm@27149
   208
     REPEAT (rtac @{thm cut} 1 THEN
wenzelm@27149
   209
       DEPTH_SOLVE_1
wenzelm@27149
   210
         (resolve_tac [@{thm thinL}, @{thm thinR}, @{thm p2} COMP @{thm monotonic}] 1) THEN
wenzelm@27149
   211
           safe_tac LK_pack 1) *})
wenzelm@27149
   212
  done
wenzelm@27149
   213
wenzelm@27149
   214
lemma eq_sym_conv: "|- (x=y) <-> (y=x)"
wenzelm@27149
   215
  apply (tactic {* fast_tac (LK_pack add_safes @{thms subst}) 1 *})
wenzelm@27149
   216
  done
wenzelm@27149
   217
wenzelm@17481
   218
use "simpdata.ML"
wenzelm@17481
   219
wenzelm@27149
   220
wenzelm@27149
   221
text {* To create substition rules *}
wenzelm@27149
   222
wenzelm@27149
   223
lemma eq_imp_subst: "|- a=b ==> $H, A(a), $G |- $E, A(b), $F"
wenzelm@27149
   224
  apply (tactic {* asm_simp_tac LK_basic_ss 1 *})
wenzelm@27149
   225
  done
wenzelm@27149
   226
wenzelm@27149
   227
lemma split_if: "|- P(if Q then x else y) <-> ((Q --> P(x)) & (~Q --> P(y)))"
wenzelm@27149
   228
  apply (rule_tac P = Q in cut)
wenzelm@30607
   229
   apply (tactic {* simp_tac (@{simpset} addsimps @{thms if_P}) 2 *})
wenzelm@27149
   230
  apply (rule_tac P = "~Q" in cut)
wenzelm@30607
   231
   apply (tactic {* simp_tac (@{simpset} addsimps @{thms if_not_P}) 2 *})
wenzelm@27149
   232
  apply (tactic {* fast_tac LK_pack 1 *})
wenzelm@27149
   233
  done
wenzelm@27149
   234
wenzelm@27149
   235
lemma if_cancel: "|- (if P then x else x) = x"
wenzelm@27149
   236
  apply (tactic {* lemma_tac @{thm split_if} 1 *})
wenzelm@27149
   237
  apply (tactic {* fast_tac LK_pack 1 *})
wenzelm@27149
   238
  done
wenzelm@27149
   239
wenzelm@27149
   240
lemma if_eq_cancel: "|- (if x=y then y else x) = x"
wenzelm@27149
   241
  apply (tactic {* lemma_tac @{thm split_if} 1 *})
wenzelm@27149
   242
  apply (tactic {* safe_tac LK_pack 1 *})
wenzelm@27149
   243
  apply (rule symL)
wenzelm@27149
   244
  apply (rule basic)
wenzelm@27149
   245
  done
wenzelm@27149
   246
paulson@2073
   247
end