src/Sequents/LK.thy
author wenzelm
Thu, 07 Apr 2016 20:51:52 +0200
changeset 62908 d7009a515733
parent 61386 0a29a984a91b
child 63530 045490f55f69
permissions -rw-r--r--
clarified mode of ROOT.ML files;
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
61386
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
     6
link between \<turnstile> and \<Longrightarrow>, 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
61386
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    20
  monotonic:  "($H \<turnstile> P \<Longrightarrow> $H \<turnstile> Q) \<Longrightarrow> $H, P \<turnstile> Q" and
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    21
61386
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    22
  left_cong:  "\<lbrakk>P == P';  \<turnstile> P' \<Longrightarrow> ($H \<turnstile> $F) \<equiv> ($H' \<turnstile> $F')\<rbrakk>
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    23
               \<Longrightarrow> (P, $H \<turnstile> $F) \<equiv> (P', $H' \<turnstile> $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
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 60754
diff changeset
    26
subsection \<open>Rewrite rules\<close>
27149
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:
61386
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    29
  "\<turnstile> P \<and> True \<longleftrightarrow> P"
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    30
  "\<turnstile> True \<and> P \<longleftrightarrow> P"
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    31
  "\<turnstile> P \<and> False \<longleftrightarrow> False"
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    32
  "\<turnstile> False \<and> P \<longleftrightarrow> False"
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    33
  "\<turnstile> P \<and> P \<longleftrightarrow> P"
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    34
  "\<turnstile> P \<and> P \<and> Q \<longleftrightarrow> P \<and> Q"
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    35
  "\<turnstile> P \<and> \<not> P \<longleftrightarrow> False"
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    36
  "\<turnstile> \<not> P \<and> P \<longleftrightarrow> False"
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    37
  "\<turnstile> (P \<and> Q) \<and> R \<longleftrightarrow> P \<and> (Q \<and> R)"
55228
901a6696cdd8 misc tuning and modernization;
wenzelm
parents: 51717
diff changeset
    38
  by (fast add!: subst)+
27149
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 21428
diff changeset
    39
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 21428
diff changeset
    40
lemma disj_simps:
61386
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    41
  "\<turnstile> P \<or> True \<longleftrightarrow> True"
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    42
  "\<turnstile> True \<or> P \<longleftrightarrow> True"
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    43
  "\<turnstile> P \<or> False \<longleftrightarrow> P"
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    44
  "\<turnstile> False \<or> P \<longleftrightarrow> P"
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    45
  "\<turnstile> P \<or> P \<longleftrightarrow> P"
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    46
  "\<turnstile> P \<or> P \<or> Q \<longleftrightarrow> P \<or> Q"
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    47
  "\<turnstile> (P \<or> Q) \<or> R \<longleftrightarrow> P \<or> (Q \<or> R)"
55228
901a6696cdd8 misc tuning and modernization;
wenzelm
parents: 51717
diff changeset
    48
  by (fast add!: subst)+
27149
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 21428
diff changeset
    49
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 21428
diff changeset
    50
lemma not_simps:
61386
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    51
  "\<turnstile> \<not> False \<longleftrightarrow> True"
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    52
  "\<turnstile> \<not> True \<longleftrightarrow> False"
55228
901a6696cdd8 misc tuning and modernization;
wenzelm
parents: 51717
diff changeset
    53
  by (fast add!: subst)+
27149
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 21428
diff changeset
    54
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 21428
diff changeset
    55
lemma imp_simps:
61386
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    56
  "\<turnstile> (P \<longrightarrow> False) \<longleftrightarrow> \<not> P"
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    57
  "\<turnstile> (P \<longrightarrow> True) \<longleftrightarrow> True"
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    58
  "\<turnstile> (False \<longrightarrow> P) \<longleftrightarrow> True"
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    59
  "\<turnstile> (True \<longrightarrow> P) \<longleftrightarrow> P"
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    60
  "\<turnstile> (P \<longrightarrow> P) \<longleftrightarrow> True"
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    61
  "\<turnstile> (P \<longrightarrow> \<not> P) \<longleftrightarrow> \<not> P"
55228
901a6696cdd8 misc tuning and modernization;
wenzelm
parents: 51717
diff changeset
    62
  by (fast add!: subst)+
27149
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 21428
diff changeset
    63
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 21428
diff changeset
    64
lemma iff_simps:
61386
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    65
  "\<turnstile> (True \<longleftrightarrow> P) \<longleftrightarrow> P"
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    66
  "\<turnstile> (P \<longleftrightarrow> True) \<longleftrightarrow> P"
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    67
  "\<turnstile> (P \<longleftrightarrow> P) \<longleftrightarrow> True"
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    68
  "\<turnstile> (False \<longleftrightarrow> P) \<longleftrightarrow> \<not> P"
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    69
  "\<turnstile> (P \<longleftrightarrow> False) \<longleftrightarrow> \<not> P"
55228
901a6696cdd8 misc tuning and modernization;
wenzelm
parents: 51717
diff changeset
    70
  by (fast add!: subst)+
27149
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 21428
diff changeset
    71
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 21428
diff changeset
    72
lemma quant_simps:
61386
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    73
  "\<And>P. \<turnstile> (\<forall>x. P) \<longleftrightarrow> P"
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    74
  "\<And>P. \<turnstile> (\<forall>x. x = t \<longrightarrow> P(x)) \<longleftrightarrow> P(t)"
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    75
  "\<And>P. \<turnstile> (\<forall>x. t = x \<longrightarrow> P(x)) \<longleftrightarrow> P(t)"
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    76
  "\<And>P. \<turnstile> (\<exists>x. P) \<longleftrightarrow> P"
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    77
  "\<And>P. \<turnstile> (\<exists>x. x = t \<and> P(x)) \<longleftrightarrow> P(t)"
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    78
  "\<And>P. \<turnstile> (\<exists>x. t = x \<and> P(x)) \<longleftrightarrow> P(t)"
55228
901a6696cdd8 misc tuning and modernization;
wenzelm
parents: 51717
diff changeset
    79
  by (fast add!: subst)+
27149
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 21428
diff changeset
    80
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 21428
diff changeset
    81
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 60754
diff changeset
    82
subsection \<open>Miniscoping: pushing quantifiers in\<close>
27149
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 21428
diff changeset
    83
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 60754
diff changeset
    84
text \<open>
61385
538100cc4399 more symbols;
wenzelm
parents: 60770
diff changeset
    85
  We do NOT distribute of \<forall> over \<and>, or dually that of \<exists> over \<or>
27149
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 21428
diff changeset
    86
  Baaz and Leitsch, On Skolemization and Proof Complexity (1994)
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 21428
diff changeset
    87
  show that this step can increase proof length!
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 60754
diff changeset
    88
\<close>
27149
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 21428
diff changeset
    89
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 60754
diff changeset
    90
text \<open>existential miniscoping\<close>
27149
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 21428
diff changeset
    91
lemma ex_simps:
61386
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    92
  "\<And>P Q. \<turnstile> (\<exists>x. P(x) \<and> Q) \<longleftrightarrow> (\<exists>x. P(x)) \<and> Q"
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    93
  "\<And>P Q. \<turnstile> (\<exists>x. P \<and> Q(x)) \<longleftrightarrow> P \<and> (\<exists>x. Q(x))"
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    94
  "\<And>P Q. \<turnstile> (\<exists>x. P(x) \<or> Q) \<longleftrightarrow> (\<exists>x. P(x)) \<or> Q"
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    95
  "\<And>P Q. \<turnstile> (\<exists>x. P \<or> Q(x)) \<longleftrightarrow> P \<or> (\<exists>x. Q(x))"
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    96
  "\<And>P Q. \<turnstile> (\<exists>x. P(x) \<longrightarrow> Q) \<longleftrightarrow> (\<forall>x. P(x)) \<longrightarrow> Q"
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    97
  "\<And>P Q. \<turnstile> (\<exists>x. P \<longrightarrow> Q(x)) \<longleftrightarrow> P \<longrightarrow> (\<exists>x. Q(x))"
55228
901a6696cdd8 misc tuning and modernization;
wenzelm
parents: 51717
diff changeset
    98
  by (fast add!: subst)+
27149
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 21428
diff changeset
    99
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 60754
diff changeset
   100
text \<open>universal miniscoping\<close>
27149
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 21428
diff changeset
   101
lemma all_simps:
61386
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
   102
  "\<And>P Q. \<turnstile> (\<forall>x. P(x) \<and> Q) \<longleftrightarrow> (\<forall>x. P(x)) \<and> Q"
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
   103
  "\<And>P Q. \<turnstile> (\<forall>x. P \<and> Q(x)) \<longleftrightarrow> P \<and> (\<forall>x. Q(x))"
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
   104
  "\<And>P Q. \<turnstile> (\<forall>x. P(x) \<longrightarrow> Q) \<longleftrightarrow> (\<exists>x. P(x)) \<longrightarrow> Q"
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
   105
  "\<And>P Q. \<turnstile> (\<forall>x. P \<longrightarrow> Q(x)) \<longleftrightarrow> P \<longrightarrow> (\<forall>x. Q(x))"
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
   106
  "\<And>P Q. \<turnstile> (\<forall>x. P(x) \<or> Q) \<longleftrightarrow> (\<forall>x. P(x)) \<or> Q"
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
   107
  "\<And>P Q. \<turnstile> (\<forall>x. P \<or> Q(x)) \<longleftrightarrow> P \<or> (\<forall>x. Q(x))"
55228
901a6696cdd8 misc tuning and modernization;
wenzelm
parents: 51717
diff changeset
   108
  by (fast add!: subst)+
27149
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 21428
diff changeset
   109
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 60754
diff changeset
   110
text \<open>These are NOT supplied by default!\<close>
27149
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 21428
diff changeset
   111
lemma distrib_simps:
61386
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
   112
  "\<turnstile> P \<and> (Q \<or> R) \<longleftrightarrow> P \<and> Q \<or> P \<and> R"
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
   113
  "\<turnstile> (Q \<or> R) \<and> P \<longleftrightarrow> Q \<and> P \<or> R \<and> P"
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
   114
  "\<turnstile> (P \<or> Q \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> R) \<and> (Q \<longrightarrow> R)"
55228
901a6696cdd8 misc tuning and modernization;
wenzelm
parents: 51717
diff changeset
   115
  by (fast add!: subst)+
27149
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 21428
diff changeset
   116
61386
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
   117
lemma P_iff_F: "\<turnstile> \<not> P \<Longrightarrow> \<turnstile> (P \<longleftrightarrow> False)"
27149
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 21428
diff changeset
   118
  apply (erule thinR [THEN cut])
55228
901a6696cdd8 misc tuning and modernization;
wenzelm
parents: 51717
diff changeset
   119
  apply fast
27149
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 21428
diff changeset
   120
  done
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 21428
diff changeset
   121
45602
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 42795
diff changeset
   122
lemmas iff_reflection_F = P_iff_F [THEN iff_reflection]
27149
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 21428
diff changeset
   123
61386
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
   124
lemma P_iff_T: "\<turnstile> P \<Longrightarrow> \<turnstile> (P \<longleftrightarrow> True)"
27149
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 21428
diff changeset
   125
  apply (erule thinR [THEN cut])
55228
901a6696cdd8 misc tuning and modernization;
wenzelm
parents: 51717
diff changeset
   126
  apply fast
27149
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 21428
diff changeset
   127
  done
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 21428
diff changeset
   128
45602
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 42795
diff changeset
   129
lemmas iff_reflection_T = P_iff_T [THEN iff_reflection]
27149
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 21428
diff changeset
   130
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 21428
diff changeset
   131
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 21428
diff changeset
   132
lemma LK_extra_simps:
61386
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
   133
  "\<turnstile> P \<or> \<not> P"
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
   134
  "\<turnstile> \<not> P \<or> P"
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
   135
  "\<turnstile> \<not> \<not> P \<longleftrightarrow> P"
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
   136
  "\<turnstile> (\<not> P \<longrightarrow> P) \<longleftrightarrow> P"
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
   137
  "\<turnstile> (\<not> P \<longleftrightarrow> \<not> Q) \<longleftrightarrow> (P \<longleftrightarrow> Q)"
55228
901a6696cdd8 misc tuning and modernization;
wenzelm
parents: 51717
diff changeset
   138
  by (fast add!: subst)+
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
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 60754
diff changeset
   141
subsection \<open>Named rewrite rules\<close>
27149
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 21428
diff changeset
   142
61386
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
   143
lemma conj_commute: "\<turnstile> P \<and> Q \<longleftrightarrow> Q \<and> P"
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
   144
  and conj_left_commute: "\<turnstile> P \<and> (Q \<and> R) \<longleftrightarrow> Q \<and> (P \<and> R)"
55228
901a6696cdd8 misc tuning and modernization;
wenzelm
parents: 51717
diff changeset
   145
  by (fast add!: subst)+
27149
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 21428
diff changeset
   146
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 21428
diff changeset
   147
lemmas conj_comms = conj_commute conj_left_commute
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 21428
diff changeset
   148
61386
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
   149
lemma disj_commute: "\<turnstile> P \<or> Q \<longleftrightarrow> Q \<or> P"
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
   150
  and disj_left_commute: "\<turnstile> P \<or> (Q \<or> R) \<longleftrightarrow> Q \<or> (P \<or> R)"
55228
901a6696cdd8 misc tuning and modernization;
wenzelm
parents: 51717
diff changeset
   151
  by (fast add!: subst)+
27149
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
lemmas disj_comms = disj_commute disj_left_commute
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 21428
diff changeset
   154
61386
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
   155
lemma conj_disj_distribL: "\<turnstile> P \<and> (Q \<or> R) \<longleftrightarrow> (P \<and> Q \<or> P \<and> R)"
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
   156
  and conj_disj_distribR: "\<turnstile> (P \<or> Q) \<and> R \<longleftrightarrow> (P \<and> R \<or> Q \<and> R)"
27149
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 21428
diff changeset
   157
61386
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
   158
  and disj_conj_distribL: "\<turnstile> P \<or> (Q \<and> R) \<longleftrightarrow> (P \<or> Q) \<and> (P \<or> R)"
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
   159
  and disj_conj_distribR: "\<turnstile> (P \<and> Q) \<or> R \<longleftrightarrow> (P \<or> R) \<and> (Q \<or> R)"
27149
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 21428
diff changeset
   160
61386
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
   161
  and imp_conj_distrib: "\<turnstile> (P \<longrightarrow> (Q \<and> R)) \<longleftrightarrow> (P \<longrightarrow> Q) \<and> (P \<longrightarrow> R)"
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
   162
  and imp_conj: "\<turnstile> ((P \<and> Q) \<longrightarrow> R)  \<longleftrightarrow> (P \<longrightarrow> (Q \<longrightarrow> R))"
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
   163
  and imp_disj: "\<turnstile> (P \<or> Q \<longrightarrow> R)  \<longleftrightarrow> (P \<longrightarrow> R) \<and> (Q \<longrightarrow> R)"
27149
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 21428
diff changeset
   164
61386
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
   165
  and imp_disj1: "\<turnstile> (P \<longrightarrow> Q) \<or> R \<longleftrightarrow> (P \<longrightarrow> Q \<or> R)"
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
   166
  and imp_disj2: "\<turnstile> Q \<or> (P \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> Q \<or> R)"
27149
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 21428
diff changeset
   167
61386
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
   168
  and de_Morgan_disj: "\<turnstile> (\<not> (P \<or> Q)) \<longleftrightarrow> (\<not> P \<and> \<not> Q)"
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
   169
  and de_Morgan_conj: "\<turnstile> (\<not> (P \<and> Q)) \<longleftrightarrow> (\<not> P \<or> \<not> Q)"
27149
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 21428
diff changeset
   170
61386
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
   171
  and not_iff: "\<turnstile> \<not> (P \<longleftrightarrow> Q) \<longleftrightarrow> (P \<longleftrightarrow> \<not> Q)"
55228
901a6696cdd8 misc tuning and modernization;
wenzelm
parents: 51717
diff changeset
   172
  by (fast add!: subst)+
27149
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 21428
diff changeset
   173
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 21428
diff changeset
   174
lemma imp_cong:
61386
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
   175
  assumes p1: "\<turnstile> P \<longleftrightarrow> P'"
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
   176
    and p2: "\<turnstile> P' \<Longrightarrow> \<turnstile> Q \<longleftrightarrow> Q'"
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
   177
  shows "\<turnstile> (P \<longrightarrow> Q) \<longleftrightarrow> (P' \<longrightarrow> Q')"
55233
3229614ca9c5 method_setup "lem";
wenzelm
parents: 55230
diff changeset
   178
  apply (lem p1)
55228
901a6696cdd8 misc tuning and modernization;
wenzelm
parents: 51717
diff changeset
   179
  apply safe
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 60754
diff changeset
   180
   apply (tactic \<open>
60754
02924903a6fd prefer tactics with explicit context;
wenzelm
parents: 59498
diff changeset
   181
     REPEAT (resolve_tac @{context} @{thms cut} 1 THEN
27149
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 21428
diff changeset
   182
       DEPTH_SOLVE_1
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 55233
diff changeset
   183
         (resolve_tac @{context} [@{thm thinL}, @{thm thinR}, @{thm p2} COMP @{thm monotonic}] 1) THEN
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 60754
diff changeset
   184
           Cla.safe_tac @{context} 1)\<close>)
27149
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 conj_cong:
61386
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
   188
  assumes p1: "\<turnstile> P \<longleftrightarrow> P'"
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
   189
    and p2: "\<turnstile> P' \<Longrightarrow> \<turnstile> Q \<longleftrightarrow> Q'"
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
   190
  shows "\<turnstile> (P \<and> Q) \<longleftrightarrow> (P' \<and> Q')"
55233
3229614ca9c5 method_setup "lem";
wenzelm
parents: 55230
diff changeset
   191
  apply (lem p1)
55228
901a6696cdd8 misc tuning and modernization;
wenzelm
parents: 51717
diff changeset
   192
  apply safe
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 60754
diff changeset
   193
   apply (tactic \<open>
60754
02924903a6fd prefer tactics with explicit context;
wenzelm
parents: 59498
diff changeset
   194
     REPEAT (resolve_tac @{context} @{thms cut} 1 THEN
27149
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 21428
diff changeset
   195
       DEPTH_SOLVE_1
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 55233
diff changeset
   196
         (resolve_tac @{context} [@{thm thinL}, @{thm thinR}, @{thm p2} COMP @{thm monotonic}] 1) THEN
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 60754
diff changeset
   197
           Cla.safe_tac @{context} 1)\<close>)
27149
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
61386
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
   200
lemma eq_sym_conv: "\<turnstile> x = y \<longleftrightarrow> y = x"
55228
901a6696cdd8 misc tuning and modernization;
wenzelm
parents: 51717
diff changeset
   201
  by (fast add!: subst)
27149
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 21428
diff changeset
   202
48891
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 45602
diff changeset
   203
ML_file "simpdata.ML"
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 60754
diff changeset
   204
setup \<open>map_theory_simpset (put_simpset LK_ss)\<close>
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 60754
diff changeset
   205
setup \<open>Simplifier.method_setup []\<close>
17481
75166ebb619b converted to Isar theory format;
wenzelm
parents: 7117
diff changeset
   206
27149
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 21428
diff changeset
   207
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 60754
diff changeset
   208
text \<open>To create substition rules\<close>
27149
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 21428
diff changeset
   209
61386
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
   210
lemma eq_imp_subst: "\<turnstile> a = b \<Longrightarrow> $H, A(a), $G \<turnstile> $E, A(b), $F"
55230
cb5ef74b32f9 proper Simplifier method setup;
wenzelm
parents: 55228
diff changeset
   211
  by simp
27149
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 21428
diff changeset
   212
61386
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
   213
lemma split_if: "\<turnstile> P(if Q then x else y) \<longleftrightarrow> ((Q \<longrightarrow> P(x)) \<and> (\<not> Q \<longrightarrow> P(y)))"
27149
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 21428
diff changeset
   214
  apply (rule_tac P = Q in cut)
55230
cb5ef74b32f9 proper Simplifier method setup;
wenzelm
parents: 55228
diff changeset
   215
   prefer 2
cb5ef74b32f9 proper Simplifier method setup;
wenzelm
parents: 55228
diff changeset
   216
   apply (simp add: if_P)
61385
538100cc4399 more symbols;
wenzelm
parents: 60770
diff changeset
   217
  apply (rule_tac P = "\<not> Q" in cut)
55230
cb5ef74b32f9 proper Simplifier method setup;
wenzelm
parents: 55228
diff changeset
   218
   prefer 2
cb5ef74b32f9 proper Simplifier method setup;
wenzelm
parents: 55228
diff changeset
   219
   apply (simp add: if_not_P)
55228
901a6696cdd8 misc tuning and modernization;
wenzelm
parents: 51717
diff changeset
   220
  apply fast
27149
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 21428
diff changeset
   221
  done
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 21428
diff changeset
   222
61386
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
   223
lemma if_cancel: "\<turnstile> (if P then x else x) = x"
55233
3229614ca9c5 method_setup "lem";
wenzelm
parents: 55230
diff changeset
   224
  apply (lem split_if)
55228
901a6696cdd8 misc tuning and modernization;
wenzelm
parents: 51717
diff changeset
   225
  apply fast
27149
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 21428
diff changeset
   226
  done
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 21428
diff changeset
   227
61386
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
   228
lemma if_eq_cancel: "\<turnstile> (if x = y then y else x) = x"
55233
3229614ca9c5 method_setup "lem";
wenzelm
parents: 55230
diff changeset
   229
  apply (lem split_if)
55228
901a6696cdd8 misc tuning and modernization;
wenzelm
parents: 51717
diff changeset
   230
  apply safe
27149
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 21428
diff changeset
   231
  apply (rule symL)
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 21428
diff changeset
   232
  apply (rule basic)
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
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   235
end