1(* Title: ZF/Induct/PropLog.thy 2 Author: Tobias Nipkow & Lawrence C Paulson 3 Copyright 1993 University of Cambridge 4*) 5 6section \<open>Meta-theory of propositional logic\<close> 7 8theory PropLog imports ZF begin 9 10text \<open> 11 Datatype definition of propositional logic formulae and inductive 12 definition of the propositional tautologies. 13 14 Inductive definition of propositional logic. Soundness and 15 completeness w.r.t.\ truth-tables. 16 17 Prove: If \<open>H |= p\<close> then \<open>G |= p\<close> where \<open>G \<in> 18 Fin(H)\<close> 19\<close> 20 21 22subsection \<open>The datatype of propositions\<close> 23 24consts 25 propn :: i 26 27datatype propn = 28 Fls 29 | Var ("n \<in> nat") (\<open>#_\<close> [100] 100) 30 | Imp ("p \<in> propn", "q \<in> propn") (infixr \<open>=>\<close> 90) 31 32 33subsection \<open>The proof system\<close> 34 35consts thms :: "i => i" 36 37abbreviation 38 thms_syntax :: "[i,i] => o" (infixl \<open>|-\<close> 50) 39 where "H |- p == p \<in> thms(H)" 40 41inductive 42 domains "thms(H)" \<subseteq> "propn" 43 intros 44 H: "[| p \<in> H; p \<in> propn |] ==> H |- p" 45 K: "[| p \<in> propn; q \<in> propn |] ==> H |- p=>q=>p" 46 S: "[| p \<in> propn; q \<in> propn; r \<in> propn |] 47 ==> H |- (p=>q=>r) => (p=>q) => p=>r" 48 DN: "p \<in> propn ==> H |- ((p=>Fls) => Fls) => p" 49 MP: "[| H |- p=>q; H |- p; p \<in> propn; q \<in> propn |] ==> H |- q" 50 type_intros "propn.intros" 51 52declare propn.intros [simp] 53 54 55subsection \<open>The semantics\<close> 56 57subsubsection \<open>Semantics of propositional logic.\<close> 58 59consts 60 is_true_fun :: "[i,i] => i" 61primrec 62 "is_true_fun(Fls, t) = 0" 63 "is_true_fun(Var(v), t) = (if v \<in> t then 1 else 0)" 64 "is_true_fun(p=>q, t) = (if is_true_fun(p,t) = 1 then is_true_fun(q,t) else 1)" 65 66definition 67 is_true :: "[i,i] => o" where 68 "is_true(p,t) == is_true_fun(p,t) = 1" 69 \<comment> \<open>this definition is required since predicates can't be recursive\<close> 70 71lemma is_true_Fls [simp]: "is_true(Fls,t) \<longleftrightarrow> False" 72 by (simp add: is_true_def) 73 74lemma is_true_Var [simp]: "is_true(#v,t) \<longleftrightarrow> v \<in> t" 75 by (simp add: is_true_def) 76 77lemma is_true_Imp [simp]: "is_true(p=>q,t) \<longleftrightarrow> (is_true(p,t)\<longrightarrow>is_true(q,t))" 78 by (simp add: is_true_def) 79 80 81subsubsection \<open>Logical consequence\<close> 82 83text \<open> 84 For every valuation, if all elements of \<open>H\<close> are true then so 85 is \<open>p\<close>. 86\<close> 87 88definition 89 logcon :: "[i,i] => o" (infixl \<open>|=\<close> 50) where 90 "H |= p == \<forall>t. (\<forall>q \<in> H. is_true(q,t)) \<longrightarrow> is_true(p,t)" 91 92 93text \<open> 94 A finite set of hypotheses from \<open>t\<close> and the \<open>Var\<close>s in 95 \<open>p\<close>. 96\<close> 97 98consts 99 hyps :: "[i,i] => i" 100primrec 101 "hyps(Fls, t) = 0" 102 "hyps(Var(v), t) = (if v \<in> t then {#v} else {#v=>Fls})" 103 "hyps(p=>q, t) = hyps(p,t) \<union> hyps(q,t)" 104 105 106 107subsection \<open>Proof theory of propositional logic\<close> 108 109lemma thms_mono: "G \<subseteq> H ==> thms(G) \<subseteq> thms(H)" 110 apply (unfold thms.defs) 111 apply (rule lfp_mono) 112 apply (rule thms.bnd_mono)+ 113 apply (assumption | rule univ_mono basic_monos)+ 114 done 115 116lemmas thms_in_pl = thms.dom_subset [THEN subsetD] 117 118inductive_cases ImpE: "p=>q \<in> propn" 119 120lemma thms_MP: "[| H |- p=>q; H |- p |] ==> H |- q" 121 \<comment> \<open>Stronger Modus Ponens rule: no typechecking!\<close> 122 apply (rule thms.MP) 123 apply (erule asm_rl thms_in_pl thms_in_pl [THEN ImpE])+ 124 done 125 126lemma thms_I: "p \<in> propn ==> H |- p=>p" 127 \<comment> \<open>Rule is called \<open>I\<close> for Identity Combinator, not for Introduction.\<close> 128 apply (rule thms.S [THEN thms_MP, THEN thms_MP]) 129 apply (rule_tac [5] thms.K) 130 apply (rule_tac [4] thms.K) 131 apply simp_all 132 done 133 134 135subsubsection \<open>Weakening, left and right\<close> 136 137lemma weaken_left: "[| G \<subseteq> H; G|-p |] ==> H|-p" 138 \<comment> \<open>Order of premises is convenient with \<open>THEN\<close>\<close> 139 by (erule thms_mono [THEN subsetD]) 140 141lemma weaken_left_cons: "H |- p ==> cons(a,H) |- p" 142 by (erule subset_consI [THEN weaken_left]) 143 144lemmas weaken_left_Un1 = Un_upper1 [THEN weaken_left] 145lemmas weaken_left_Un2 = Un_upper2 [THEN weaken_left] 146 147lemma weaken_right: "[| H |- q; p \<in> propn |] ==> H |- p=>q" 148 by (simp_all add: thms.K [THEN thms_MP] thms_in_pl) 149 150 151subsubsection \<open>The deduction theorem\<close> 152 153theorem deduction: "[| cons(p,H) |- q; p \<in> propn |] ==> H |- p=>q" 154 apply (erule thms.induct) 155 apply (blast intro: thms_I thms.H [THEN weaken_right]) 156 apply (blast intro: thms.K [THEN weaken_right]) 157 apply (blast intro: thms.S [THEN weaken_right]) 158 apply (blast intro: thms.DN [THEN weaken_right]) 159 apply (blast intro: thms.S [THEN thms_MP [THEN thms_MP]]) 160 done 161 162 163subsubsection \<open>The cut rule\<close> 164 165lemma cut: "[| H|-p; cons(p,H) |- q |] ==> H |- q" 166 apply (rule deduction [THEN thms_MP]) 167 apply (simp_all add: thms_in_pl) 168 done 169 170lemma thms_FlsE: "[| H |- Fls; p \<in> propn |] ==> H |- p" 171 apply (rule thms.DN [THEN thms_MP]) 172 apply (rule_tac [2] weaken_right) 173 apply (simp_all add: propn.intros) 174 done 175 176lemma thms_notE: "[| H |- p=>Fls; H |- p; q \<in> propn |] ==> H |- q" 177 by (erule thms_MP [THEN thms_FlsE]) 178 179 180subsubsection \<open>Soundness of the rules wrt truth-table semantics\<close> 181 182theorem soundness: "H |- p ==> H |= p" 183 apply (unfold logcon_def) 184 apply (induct set: thms) 185 apply auto 186 done 187 188 189subsection \<open>Completeness\<close> 190 191subsubsection \<open>Towards the completeness proof\<close> 192 193lemma Fls_Imp: "[| H |- p=>Fls; q \<in> propn |] ==> H |- p=>q" 194 apply (frule thms_in_pl) 195 apply (rule deduction) 196 apply (rule weaken_left_cons [THEN thms_notE]) 197 apply (blast intro: thms.H elim: ImpE)+ 198 done 199 200lemma Imp_Fls: "[| H |- p; H |- q=>Fls |] ==> H |- (p=>q)=>Fls" 201 apply (frule thms_in_pl) 202 apply (frule thms_in_pl [of concl: "q=>Fls"]) 203 apply (rule deduction) 204 apply (erule weaken_left_cons [THEN thms_MP]) 205 apply (rule consI1 [THEN thms.H, THEN thms_MP]) 206 apply (blast intro: weaken_left_cons elim: ImpE)+ 207 done 208 209lemma hyps_thms_if: 210 "p \<in> propn ==> hyps(p,t) |- (if is_true(p,t) then p else p=>Fls)" 211 \<comment> \<open>Typical example of strengthening the induction statement.\<close> 212 apply simp 213 apply (induct_tac p) 214 apply (simp_all add: thms_I thms.H) 215 apply (safe elim!: Fls_Imp [THEN weaken_left_Un1] Fls_Imp [THEN weaken_left_Un2]) 216 apply (blast intro: weaken_left_Un1 weaken_left_Un2 weaken_right Imp_Fls)+ 217 done 218 219lemma logcon_thms_p: "[| p \<in> propn; 0 |= p |] ==> hyps(p,t) |- p" 220 \<comment> \<open>Key lemma for completeness; yields a set of assumptions satisfying \<open>p\<close>\<close> 221 apply (drule hyps_thms_if) 222 apply (simp add: logcon_def) 223 done 224 225text \<open> 226 For proving certain theorems in our new propositional logic. 227\<close> 228 229lemmas propn_SIs = propn.intros deduction 230 and propn_Is = thms_in_pl thms.H thms.H [THEN thms_MP] 231 232text \<open> 233 The excluded middle in the form of an elimination rule. 234\<close> 235 236lemma thms_excluded_middle: 237 "[| p \<in> propn; q \<in> propn |] ==> H |- (p=>q) => ((p=>Fls)=>q) => q" 238 apply (rule deduction [THEN deduction]) 239 apply (rule thms.DN [THEN thms_MP]) 240 apply (best intro!: propn_SIs intro: propn_Is)+ 241 done 242 243lemma thms_excluded_middle_rule: 244 "[| cons(p,H) |- q; cons(p=>Fls,H) |- q; p \<in> propn |] ==> H |- q" 245 \<comment> \<open>Hard to prove directly because it requires cuts\<close> 246 apply (rule thms_excluded_middle [THEN thms_MP, THEN thms_MP]) 247 apply (blast intro!: propn_SIs intro: propn_Is)+ 248 done 249 250 251subsubsection \<open>Completeness -- lemmas for reducing the set of assumptions\<close> 252 253text \<open> 254 For the case \<^prop>\<open>hyps(p,t)-cons(#v,Y) |- p\<close> we also have \<^prop>\<open>hyps(p,t)-{#v} \<subseteq> hyps(p, t-{v})\<close>. 255\<close> 256 257lemma hyps_Diff: 258 "p \<in> propn ==> hyps(p, t-{v}) \<subseteq> cons(#v=>Fls, hyps(p,t)-{#v})" 259 by (induct set: propn) auto 260 261text \<open> 262 For the case \<^prop>\<open>hyps(p,t)-cons(#v => Fls,Y) |- p\<close> we also have 263 \<^prop>\<open>hyps(p,t)-{#v=>Fls} \<subseteq> hyps(p, cons(v,t))\<close>. 264\<close> 265 266lemma hyps_cons: 267 "p \<in> propn ==> hyps(p, cons(v,t)) \<subseteq> cons(#v, hyps(p,t)-{#v=>Fls})" 268 by (induct set: propn) auto 269 270text \<open>Two lemmas for use with \<open>weaken_left\<close>\<close> 271 272lemma cons_Diff_same: "B-C \<subseteq> cons(a, B-cons(a,C))" 273 by blast 274 275lemma cons_Diff_subset2: "cons(a, B-{c}) - D \<subseteq> cons(a, B-cons(c,D))" 276 by blast 277 278text \<open> 279 The set \<^term>\<open>hyps(p,t)\<close> is finite, and elements have the form 280 \<^term>\<open>#v\<close> or \<^term>\<open>#v=>Fls\<close>; could probably prove the stronger 281 \<^prop>\<open>hyps(p,t) \<in> Fin(hyps(p,0) \<union> hyps(p,nat))\<close>. 282\<close> 283 284lemma hyps_finite: "p \<in> propn ==> hyps(p,t) \<in> Fin(\<Union>v \<in> nat. {#v, #v=>Fls})" 285 by (induct set: propn) auto 286 287lemmas Diff_weaken_left = Diff_mono [OF _ subset_refl, THEN weaken_left] 288 289text \<open> 290 Induction on the finite set of assumptions \<^term>\<open>hyps(p,t0)\<close>. We 291 may repeatedly subtract assumptions until none are left! 292\<close> 293 294lemma completeness_0_lemma [rule_format]: 295 "[| p \<in> propn; 0 |= p |] ==> \<forall>t. hyps(p,t) - hyps(p,t0) |- p" 296 apply (frule hyps_finite) 297 apply (erule Fin_induct) 298 apply (simp add: logcon_thms_p Diff_0) 299 txt \<open>inductive step\<close> 300 apply safe 301 txt \<open>Case \<^prop>\<open>hyps(p,t)-cons(#v,Y) |- p\<close>\<close> 302 apply (rule thms_excluded_middle_rule) 303 apply (erule_tac [3] propn.intros) 304 apply (blast intro: cons_Diff_same [THEN weaken_left]) 305 apply (blast intro: cons_Diff_subset2 [THEN weaken_left] 306 hyps_Diff [THEN Diff_weaken_left]) 307 txt \<open>Case \<^prop>\<open>hyps(p,t)-cons(#v => Fls,Y) |- p\<close>\<close> 308 apply (rule thms_excluded_middle_rule) 309 apply (erule_tac [3] propn.intros) 310 apply (blast intro: cons_Diff_subset2 [THEN weaken_left] 311 hyps_cons [THEN Diff_weaken_left]) 312 apply (blast intro: cons_Diff_same [THEN weaken_left]) 313 done 314 315 316subsubsection \<open>Completeness theorem\<close> 317 318lemma completeness_0: "[| p \<in> propn; 0 |= p |] ==> 0 |- p" 319 \<comment> \<open>The base case for completeness\<close> 320 apply (rule Diff_cancel [THEN subst]) 321 apply (blast intro: completeness_0_lemma) 322 done 323 324lemma logcon_Imp: "[| cons(p,H) |= q |] ==> H |= p=>q" 325 \<comment> \<open>A semantic analogue of the Deduction Theorem\<close> 326 by (simp add: logcon_def) 327 328lemma completeness: 329 "H \<in> Fin(propn) ==> p \<in> propn \<Longrightarrow> H |= p \<Longrightarrow> H |- p" 330 apply (induct arbitrary: p set: Fin) 331 apply (safe intro!: completeness_0) 332 apply (rule weaken_left_cons [THEN thms_MP]) 333 apply (blast intro!: logcon_Imp propn.intros) 334 apply (blast intro: propn_Is) 335 done 336 337theorem thms_iff: "H \<in> Fin(propn) ==> H |- p \<longleftrightarrow> H |= p \<and> p \<in> propn" 338 by (blast intro: soundness completeness thms_in_pl) 339 340end 341