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