1(* Title: Sequents/LK.thy 2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 3 Copyright 1993 University of Cambridge 4 5Axiom to express monotonicity (a variant of the deduction theorem). Makes the 6link between \<turnstile> and \<Longrightarrow>, needed for instance to prove imp_cong. 7 8Axiom left_cong allows the simplifier to use left-side formulas. Ideally it 9should be derived from lower-level axioms. 10 11CANNOT be added to LK0.thy because modal logic is built upon it, and 12various modal rules would become inconsistent. 13*) 14 15theory LK 16imports LK0 17begin 18 19axiomatization 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 26subsection \<open>Rewrite rules\<close> 27 28lemma 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 40lemma 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 50lemma not_simps: 51 "\<turnstile> \<not> False \<longleftrightarrow> True" 52 "\<turnstile> \<not> True \<longleftrightarrow> False" 53 by (fast add!: subst)+ 54 55lemma 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 64lemma 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 72lemma 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 82subsection \<open>Miniscoping: pushing quantifiers in\<close> 83 84text \<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 90text \<open>existential miniscoping\<close> 91lemma 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 100text \<open>universal miniscoping\<close> 101lemma 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 110text \<open>These are NOT supplied by default!\<close> 111lemma 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 117lemma P_iff_F: "\<turnstile> \<not> P \<Longrightarrow> \<turnstile> (P \<longleftrightarrow> False)" 118 apply (erule thinR [THEN cut]) 119 apply fast 120 done 121 122lemmas iff_reflection_F = P_iff_F [THEN iff_reflection] 123 124lemma P_iff_T: "\<turnstile> P \<Longrightarrow> \<turnstile> (P \<longleftrightarrow> True)" 125 apply (erule thinR [THEN cut]) 126 apply fast 127 done 128 129lemmas iff_reflection_T = P_iff_T [THEN iff_reflection] 130 131 132lemma 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 141subsection \<open>Named rewrite rules\<close> 142 143lemma 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 147lemmas conj_comms = conj_commute conj_left_commute 148 149lemma 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 153lemmas disj_comms = disj_commute disj_left_commute 154 155lemma 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 174lemma 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 187lemma 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 200lemma eq_sym_conv: "\<turnstile> x = y \<longleftrightarrow> y = x" 201 by (fast add!: subst) 202 203ML_file \<open>simpdata.ML\<close> 204setup \<open>map_theory_simpset (put_simpset LK_ss)\<close> 205setup \<open>Simplifier.method_setup []\<close> 206 207 208text \<open>To create substitution rules\<close> 209 210lemma eq_imp_subst: "\<turnstile> a = b \<Longrightarrow> $H, A(a), $G \<turnstile> $E, A(b), $F" 211 by simp 212 213lemma 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 223lemma if_cancel: "\<turnstile> (if P then x else x) = x" 224 apply (lem split_if) 225 apply fast 226 done 227 228lemma 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 235end 236