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