1(* Title: FOL/FOL.thy 2 Author: Lawrence C Paulson and Markus Wenzel 3*) 4 5section \<open>Classical first-order logic\<close> 6 7theory FOL 8imports IFOL 9keywords "print_claset" "print_induct_rules" :: diag 10begin 11 12ML_file \<open>~~/src/Provers/classical.ML\<close> 13ML_file \<open>~~/src/Provers/blast.ML\<close> 14ML_file \<open>~~/src/Provers/clasimp.ML\<close> 15 16 17subsection \<open>The classical axiom\<close> 18 19axiomatization where 20 classical: \<open>(\<not> P \<Longrightarrow> P) \<Longrightarrow> P\<close> 21 22 23subsection \<open>Lemmas and proof tools\<close> 24 25lemma ccontr: \<open>(\<not> P \<Longrightarrow> False) \<Longrightarrow> P\<close> 26 by (erule FalseE [THEN classical]) 27 28 29subsubsection \<open>Classical introduction rules for \<open>\<or>\<close> and \<open>\<exists>\<close>\<close> 30 31lemma disjCI: \<open>(\<not> Q \<Longrightarrow> P) \<Longrightarrow> P \<or> Q\<close> 32 apply (rule classical) 33 apply (assumption | erule meta_mp | rule disjI1 notI)+ 34 apply (erule notE disjI2)+ 35 done 36 37text \<open>Introduction rule involving only \<open>\<exists>\<close>\<close> 38lemma ex_classical: 39 assumes r: \<open>\<not> (\<exists>x. P(x)) \<Longrightarrow> P(a)\<close> 40 shows \<open>\<exists>x. P(x)\<close> 41 apply (rule classical) 42 apply (rule exI, erule r) 43 done 44 45text \<open>Version of above, simplifying \<open>\<not>\<exists>\<close> to \<open>\<forall>\<not>\<close>.\<close> 46lemma exCI: 47 assumes r: \<open>\<forall>x. \<not> P(x) \<Longrightarrow> P(a)\<close> 48 shows \<open>\<exists>x. P(x)\<close> 49 apply (rule ex_classical) 50 apply (rule notI [THEN allI, THEN r]) 51 apply (erule notE) 52 apply (erule exI) 53 done 54 55lemma excluded_middle: \<open>\<not> P \<or> P\<close> 56 apply (rule disjCI) 57 apply assumption 58 done 59 60lemma case_split [case_names True False]: 61 assumes r1: \<open>P \<Longrightarrow> Q\<close> 62 and r2: \<open>\<not> P \<Longrightarrow> Q\<close> 63 shows \<open>Q\<close> 64 apply (rule excluded_middle [THEN disjE]) 65 apply (erule r2) 66 apply (erule r1) 67 done 68 69ML \<open> 70 fun case_tac ctxt a fixes = 71 Rule_Insts.res_inst_tac ctxt [((("P", 0), Position.none), a)] fixes @{thm case_split}; 72\<close> 73 74method_setup case_tac = \<open> 75 Args.goal_spec -- Scan.lift (Args.embedded_inner_syntax -- Parse.for_fixes) >> 76 (fn (quant, (s, fixes)) => fn ctxt => SIMPLE_METHOD'' quant (case_tac ctxt s fixes)) 77\<close> "case_tac emulation (dynamic instantiation!)" 78 79 80subsection \<open>Special elimination rules\<close> 81 82text \<open>Classical implies (\<open>\<longrightarrow>\<close>) elimination.\<close> 83lemma impCE: 84 assumes major: \<open>P \<longrightarrow> Q\<close> 85 and r1: \<open>\<not> P \<Longrightarrow> R\<close> 86 and r2: \<open>Q \<Longrightarrow> R\<close> 87 shows \<open>R\<close> 88 apply (rule excluded_middle [THEN disjE]) 89 apply (erule r1) 90 apply (rule r2) 91 apply (erule major [THEN mp]) 92 done 93 94text \<open> 95 This version of \<open>\<longrightarrow>\<close> elimination works on \<open>Q\<close> before \<open>P\<close>. It works best for those cases in which P holds ``almost everywhere''. 96 Can't install as default: would break old proofs. 97\<close> 98lemma impCE': 99 assumes major: \<open>P \<longrightarrow> Q\<close> 100 and r1: \<open>Q \<Longrightarrow> R\<close> 101 and r2: \<open>\<not> P \<Longrightarrow> R\<close> 102 shows \<open>R\<close> 103 apply (rule excluded_middle [THEN disjE]) 104 apply (erule r2) 105 apply (rule r1) 106 apply (erule major [THEN mp]) 107 done 108 109text \<open>Double negation law.\<close> 110lemma notnotD: \<open>\<not> \<not> P \<Longrightarrow> P\<close> 111 apply (rule classical) 112 apply (erule notE) 113 apply assumption 114 done 115 116lemma contrapos2: \<open>\<lbrakk>Q; \<not> P \<Longrightarrow> \<not> Q\<rbrakk> \<Longrightarrow> P\<close> 117 apply (rule classical) 118 apply (drule (1) meta_mp) 119 apply (erule (1) notE) 120 done 121 122 123subsubsection \<open>Tactics for implication and contradiction\<close> 124 125text \<open> 126 Classical \<open>\<longleftrightarrow>\<close> elimination. Proof substitutes \<open>P = Q\<close> in 127 \<open>\<not> P \<Longrightarrow> \<not> Q\<close> and \<open>P \<Longrightarrow> Q\<close>. 128\<close> 129lemma iffCE: 130 assumes major: \<open>P \<longleftrightarrow> Q\<close> 131 and r1: \<open>\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> R\<close> 132 and r2: \<open>\<lbrakk>\<not> P; \<not> Q\<rbrakk> \<Longrightarrow> R\<close> 133 shows \<open>R\<close> 134 apply (rule major [unfolded iff_def, THEN conjE]) 135 apply (elim impCE) 136 apply (erule (1) r2) 137 apply (erule (1) notE)+ 138 apply (erule (1) r1) 139 done 140 141 142(*Better for fast_tac: needs no quantifier duplication!*) 143lemma alt_ex1E: 144 assumes major: \<open>\<exists>! x. P(x)\<close> 145 and r: \<open>\<And>x. \<lbrakk>P(x); \<forall>y y'. P(y) \<and> P(y') \<longrightarrow> y = y'\<rbrakk> \<Longrightarrow> R\<close> 146 shows \<open>R\<close> 147 using major 148proof (rule ex1E) 149 fix x 150 assume * : \<open>\<forall>y. P(y) \<longrightarrow> y = x\<close> 151 assume \<open>P(x)\<close> 152 then show \<open>R\<close> 153 proof (rule r) 154 { 155 fix y y' 156 assume \<open>P(y)\<close> and \<open>P(y')\<close> 157 with * have \<open>x = y\<close> and \<open>x = y'\<close> 158 by - (tactic "IntPr.fast_tac \<^context> 1")+ 159 then have \<open>y = y'\<close> by (rule subst) 160 } note r' = this 161 show \<open>\<forall>y y'. P(y) \<and> P(y') \<longrightarrow> y = y'\<close> 162 by (intro strip, elim conjE) (rule r') 163 qed 164qed 165 166lemma imp_elim: \<open>P \<longrightarrow> Q \<Longrightarrow> (\<not> R \<Longrightarrow> P) \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R\<close> 167 by (rule classical) iprover 168 169lemma swap: \<open>\<not> P \<Longrightarrow> (\<not> R \<Longrightarrow> P) \<Longrightarrow> R\<close> 170 by (rule classical) iprover 171 172 173section \<open>Classical Reasoner\<close> 174 175ML \<open> 176structure Cla = Classical 177( 178 val imp_elim = @{thm imp_elim} 179 val not_elim = @{thm notE} 180 val swap = @{thm swap} 181 val classical = @{thm classical} 182 val sizef = size_of_thm 183 val hyp_subst_tacs = [hyp_subst_tac] 184); 185 186structure Basic_Classical: BASIC_CLASSICAL = Cla; 187open Basic_Classical; 188\<close> 189 190(*Propositional rules*) 191lemmas [intro!] = refl TrueI conjI disjCI impI notI iffI 192 and [elim!] = conjE disjE impCE FalseE iffCE 193ML \<open>val prop_cs = claset_of \<^context>\<close> 194 195(*Quantifier rules*) 196lemmas [intro!] = allI ex_ex1I 197 and [intro] = exI 198 and [elim!] = exE alt_ex1E 199 and [elim] = allE 200ML \<open>val FOL_cs = claset_of \<^context>\<close> 201 202ML \<open> 203 structure Blast = Blast 204 ( 205 structure Classical = Cla 206 val Trueprop_const = dest_Const \<^const>\<open>Trueprop\<close> 207 val equality_name = \<^const_name>\<open>eq\<close> 208 val not_name = \<^const_name>\<open>Not\<close> 209 val notE = @{thm notE} 210 val ccontr = @{thm ccontr} 211 val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac 212 ); 213 val blast_tac = Blast.blast_tac; 214\<close> 215 216 217lemma ex1_functional: \<open>\<lbrakk>\<exists>! z. P(a,z); P(a,b); P(a,c)\<rbrakk> \<Longrightarrow> b = c\<close> 218 by blast 219 220text \<open>Elimination of \<open>True\<close> from assumptions:\<close> 221lemma True_implies_equals: \<open>(True \<Longrightarrow> PROP P) \<equiv> PROP P\<close> 222proof 223 assume \<open>True \<Longrightarrow> PROP P\<close> 224 from this and TrueI show \<open>PROP P\<close> . 225next 226 assume \<open>PROP P\<close> 227 then show \<open>PROP P\<close> . 228qed 229 230lemma uncurry: \<open>P \<longrightarrow> Q \<longrightarrow> R \<Longrightarrow> P \<and> Q \<longrightarrow> R\<close> 231 by blast 232 233lemma iff_allI: \<open>(\<And>x. P(x) \<longleftrightarrow> Q(x)) \<Longrightarrow> (\<forall>x. P(x)) \<longleftrightarrow> (\<forall>x. Q(x))\<close> 234 by blast 235 236lemma iff_exI: \<open>(\<And>x. P(x) \<longleftrightarrow> Q(x)) \<Longrightarrow> (\<exists>x. P(x)) \<longleftrightarrow> (\<exists>x. Q(x))\<close> 237 by blast 238 239lemma all_comm: \<open>(\<forall>x y. P(x,y)) \<longleftrightarrow> (\<forall>y x. P(x,y))\<close> 240 by blast 241 242lemma ex_comm: \<open>(\<exists>x y. P(x,y)) \<longleftrightarrow> (\<exists>y x. P(x,y))\<close> 243 by blast 244 245 246 247subsection \<open>Classical simplification rules\<close> 248 249text \<open> 250 Avoids duplication of subgoals after \<open>expand_if\<close>, when the true and 251 false cases boil down to the same thing. 252\<close> 253 254lemma cases_simp: \<open>(P \<longrightarrow> Q) \<and> (\<not> P \<longrightarrow> Q) \<longleftrightarrow> Q\<close> 255 by blast 256 257 258subsubsection \<open>Miniscoping: pushing quantifiers in\<close> 259 260text \<open> 261 We do NOT distribute of \<open>\<forall>\<close> over \<open>\<and>\<close>, or dually that of 262 \<open>\<exists>\<close> over \<open>\<or>\<close>. 263 264 Baaz and Leitsch, On Skolemization and Proof Complexity (1994) show that 265 this step can increase proof length! 266\<close> 267 268text \<open>Existential miniscoping.\<close> 269lemma int_ex_simps: 270 \<open>\<And>P Q. (\<exists>x. P(x) \<and> Q) \<longleftrightarrow> (\<exists>x. P(x)) \<and> Q\<close> 271 \<open>\<And>P Q. (\<exists>x. P \<and> Q(x)) \<longleftrightarrow> P \<and> (\<exists>x. Q(x))\<close> 272 \<open>\<And>P Q. (\<exists>x. P(x) \<or> Q) \<longleftrightarrow> (\<exists>x. P(x)) \<or> Q\<close> 273 \<open>\<And>P Q. (\<exists>x. P \<or> Q(x)) \<longleftrightarrow> P \<or> (\<exists>x. Q(x))\<close> 274 by iprover+ 275 276text \<open>Classical rules.\<close> 277lemma cla_ex_simps: 278 \<open>\<And>P Q. (\<exists>x. P(x) \<longrightarrow> Q) \<longleftrightarrow> (\<forall>x. P(x)) \<longrightarrow> Q\<close> 279 \<open>\<And>P Q. (\<exists>x. P \<longrightarrow> Q(x)) \<longleftrightarrow> P \<longrightarrow> (\<exists>x. Q(x))\<close> 280 by blast+ 281 282lemmas ex_simps = int_ex_simps cla_ex_simps 283 284text \<open>Universal miniscoping.\<close> 285lemma int_all_simps: 286 \<open>\<And>P Q. (\<forall>x. P(x) \<and> Q) \<longleftrightarrow> (\<forall>x. P(x)) \<and> Q\<close> 287 \<open>\<And>P Q. (\<forall>x. P \<and> Q(x)) \<longleftrightarrow> P \<and> (\<forall>x. Q(x))\<close> 288 \<open>\<And>P Q. (\<forall>x. P(x) \<longrightarrow> Q) \<longleftrightarrow> (\<exists> x. P(x)) \<longrightarrow> Q\<close> 289 \<open>\<And>P Q. (\<forall>x. P \<longrightarrow> Q(x)) \<longleftrightarrow> P \<longrightarrow> (\<forall>x. Q(x))\<close> 290 by iprover+ 291 292text \<open>Classical rules.\<close> 293lemma cla_all_simps: 294 \<open>\<And>P Q. (\<forall>x. P(x) \<or> Q) \<longleftrightarrow> (\<forall>x. P(x)) \<or> Q\<close> 295 \<open>\<And>P Q. (\<forall>x. P \<or> Q(x)) \<longleftrightarrow> P \<or> (\<forall>x. Q(x))\<close> 296 by blast+ 297 298lemmas all_simps = int_all_simps cla_all_simps 299 300 301subsubsection \<open>Named rewrite rules proved for IFOL\<close> 302 303lemma imp_disj1: \<open>(P \<longrightarrow> Q) \<or> R \<longleftrightarrow> (P \<longrightarrow> Q \<or> R)\<close> by blast 304lemma imp_disj2: \<open>Q \<or> (P \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> Q \<or> R)\<close> by blast 305 306lemma de_Morgan_conj: \<open>(\<not> (P \<and> Q)) \<longleftrightarrow> (\<not> P \<or> \<not> Q)\<close> by blast 307 308lemma not_imp: \<open>\<not> (P \<longrightarrow> Q) \<longleftrightarrow> (P \<and> \<not> Q)\<close> by blast 309lemma not_iff: \<open>\<not> (P \<longleftrightarrow> Q) \<longleftrightarrow> (P \<longleftrightarrow> \<not> Q)\<close> by blast 310 311lemma not_all: \<open>(\<not> (\<forall>x. P(x))) \<longleftrightarrow> (\<exists>x. \<not> P(x))\<close> by blast 312lemma imp_all: \<open>((\<forall>x. P(x)) \<longrightarrow> Q) \<longleftrightarrow> (\<exists>x. P(x) \<longrightarrow> Q)\<close> by blast 313 314 315lemmas meta_simps = 316 triv_forall_equality \<comment> \<open>prunes params\<close> 317 True_implies_equals \<comment> \<open>prune asms \<open>True\<close>\<close> 318 319lemmas IFOL_simps = 320 refl [THEN P_iff_T] conj_simps disj_simps not_simps 321 imp_simps iff_simps quant_simps 322 323lemma notFalseI: \<open>\<not> False\<close> by iprover 324 325lemma cla_simps_misc: 326 \<open>\<not> (P \<and> Q) \<longleftrightarrow> \<not> P \<or> \<not> Q\<close> 327 \<open>P \<or> \<not> P\<close> 328 \<open>\<not> P \<or> P\<close> 329 \<open>\<not> \<not> P \<longleftrightarrow> P\<close> 330 \<open>(\<not> P \<longrightarrow> P) \<longleftrightarrow> P\<close> 331 \<open>(\<not> P \<longleftrightarrow> \<not> Q) \<longleftrightarrow> (P \<longleftrightarrow> Q)\<close> by blast+ 332 333lemmas cla_simps = 334 de_Morgan_conj de_Morgan_disj imp_disj1 imp_disj2 335 not_imp not_all not_ex cases_simp cla_simps_misc 336 337 338ML_file \<open>simpdata.ML\<close> 339 340simproc_setup defined_Ex (\<open>\<exists>x. P(x)\<close>) = \<open>fn _ => Quantifier1.rearrange_ex\<close> 341simproc_setup defined_All (\<open>\<forall>x. P(x)\<close>) = \<open>fn _ => Quantifier1.rearrange_all\<close> 342 343ML \<open> 344(*intuitionistic simprules only*) 345val IFOL_ss = 346 put_simpset FOL_basic_ss \<^context> 347 addsimps @{thms meta_simps IFOL_simps int_ex_simps int_all_simps} 348 addsimprocs [\<^simproc>\<open>defined_All\<close>, \<^simproc>\<open>defined_Ex\<close>] 349 |> Simplifier.add_cong @{thm imp_cong} 350 |> simpset_of; 351 352(*classical simprules too*) 353val FOL_ss = 354 put_simpset IFOL_ss \<^context> 355 addsimps @{thms cla_simps cla_ex_simps cla_all_simps} 356 |> simpset_of; 357\<close> 358 359setup \<open> 360 map_theory_simpset (put_simpset FOL_ss) #> 361 Simplifier.method_setup Splitter.split_modifiers 362\<close> 363 364ML_file \<open>~~/src/Tools/eqsubst.ML\<close> 365 366 367subsection \<open>Other simple lemmas\<close> 368 369lemma [simp]: \<open>((P \<longrightarrow> R) \<longleftrightarrow> (Q \<longrightarrow> R)) \<longleftrightarrow> ((P \<longleftrightarrow> Q) \<or> R)\<close> 370 by blast 371 372lemma [simp]: \<open>((P \<longrightarrow> Q) \<longleftrightarrow> (P \<longrightarrow> R)) \<longleftrightarrow> (P \<longrightarrow> (Q \<longleftrightarrow> R))\<close> 373 by blast 374 375lemma not_disj_iff_imp: \<open>\<not> P \<or> Q \<longleftrightarrow> (P \<longrightarrow> Q)\<close> 376 by blast 377 378 379subsubsection \<open>Monotonicity of implications\<close> 380 381lemma conj_mono: \<open>\<lbrakk>P1 \<longrightarrow> Q1; P2 \<longrightarrow> Q2\<rbrakk> \<Longrightarrow> (P1 \<and> P2) \<longrightarrow> (Q1 \<and> Q2)\<close> 382 by fast (*or (IntPr.fast_tac 1)*) 383 384lemma disj_mono: \<open>\<lbrakk>P1 \<longrightarrow> Q1; P2 \<longrightarrow> Q2\<rbrakk> \<Longrightarrow> (P1 \<or> P2) \<longrightarrow> (Q1 \<or> Q2)\<close> 385 by fast (*or (IntPr.fast_tac 1)*) 386 387lemma imp_mono: \<open>\<lbrakk>Q1 \<longrightarrow> P1; P2 \<longrightarrow> Q2\<rbrakk> \<Longrightarrow> (P1 \<longrightarrow> P2) \<longrightarrow> (Q1 \<longrightarrow> Q2)\<close> 388 by fast (*or (IntPr.fast_tac 1)*) 389 390lemma imp_refl: \<open>P \<longrightarrow> P\<close> 391 by (rule impI) 392 393text \<open>The quantifier monotonicity rules are also intuitionistically valid.\<close> 394lemma ex_mono: \<open>(\<And>x. P(x) \<longrightarrow> Q(x)) \<Longrightarrow> (\<exists>x. P(x)) \<longrightarrow> (\<exists>x. Q(x))\<close> 395 by blast 396 397lemma all_mono: \<open>(\<And>x. P(x) \<longrightarrow> Q(x)) \<Longrightarrow> (\<forall>x. P(x)) \<longrightarrow> (\<forall>x. Q(x))\<close> 398 by blast 399 400 401subsection \<open>Proof by cases and induction\<close> 402 403text \<open>Proper handling of non-atomic rule statements.\<close> 404 405context 406begin 407 408qualified definition \<open>induct_forall(P) \<equiv> \<forall>x. P(x)\<close> 409qualified definition \<open>induct_implies(A, B) \<equiv> A \<longrightarrow> B\<close> 410qualified definition \<open>induct_equal(x, y) \<equiv> x = y\<close> 411qualified definition \<open>induct_conj(A, B) \<equiv> A \<and> B\<close> 412 413lemma induct_forall_eq: \<open>(\<And>x. P(x)) \<equiv> Trueprop(induct_forall(\<lambda>x. P(x)))\<close> 414 unfolding atomize_all induct_forall_def . 415 416lemma induct_implies_eq: \<open>(A \<Longrightarrow> B) \<equiv> Trueprop(induct_implies(A, B))\<close> 417 unfolding atomize_imp induct_implies_def . 418 419lemma induct_equal_eq: \<open>(x \<equiv> y) \<equiv> Trueprop(induct_equal(x, y))\<close> 420 unfolding atomize_eq induct_equal_def . 421 422lemma induct_conj_eq: \<open>(A &&& B) \<equiv> Trueprop(induct_conj(A, B))\<close> 423 unfolding atomize_conj induct_conj_def . 424 425lemmas induct_atomize = induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq 426lemmas induct_rulify [symmetric] = induct_atomize 427lemmas induct_rulify_fallback = 428 induct_forall_def induct_implies_def induct_equal_def induct_conj_def 429 430text \<open>Method setup.\<close> 431 432ML_file \<open>~~/src/Tools/induct.ML\<close> 433ML \<open> 434 structure Induct = Induct 435 ( 436 val cases_default = @{thm case_split} 437 val atomize = @{thms induct_atomize} 438 val rulify = @{thms induct_rulify} 439 val rulify_fallback = @{thms induct_rulify_fallback} 440 val equal_def = @{thm induct_equal_def} 441 fun dest_def _ = NONE 442 fun trivial_tac _ _ = no_tac 443 ); 444\<close> 445 446declare case_split [cases type: o] 447 448end 449 450ML_file \<open>~~/src/Tools/case_product.ML\<close> 451 452 453hide_const (open) eq 454 455end 456