1(* Title: HOL/HOL.thy 2 Author: Tobias Nipkow, Markus Wenzel, and Larry Paulson 3*) 4 5section \<open>The basis of Higher-Order Logic\<close> 6 7theory HOL 8imports Pure Tools.Code_Generator 9keywords 10 "try" "solve_direct" "quickcheck" "print_coercions" "print_claset" 11 "print_induct_rules" :: diag and 12 "quickcheck_params" :: thy_decl 13begin 14 15ML_file \<open>~~/src/Tools/misc_legacy.ML\<close> 16ML_file \<open>~~/src/Tools/try.ML\<close> 17ML_file \<open>~~/src/Tools/quickcheck.ML\<close> 18ML_file \<open>~~/src/Tools/solve_direct.ML\<close> 19ML_file \<open>~~/src/Tools/IsaPlanner/zipper.ML\<close> 20ML_file \<open>~~/src/Tools/IsaPlanner/isand.ML\<close> 21ML_file \<open>~~/src/Tools/IsaPlanner/rw_inst.ML\<close> 22ML_file \<open>~~/src/Provers/hypsubst.ML\<close> 23ML_file \<open>~~/src/Provers/splitter.ML\<close> 24ML_file \<open>~~/src/Provers/classical.ML\<close> 25ML_file \<open>~~/src/Provers/blast.ML\<close> 26ML_file \<open>~~/src/Provers/clasimp.ML\<close> 27ML_file \<open>~~/src/Tools/eqsubst.ML\<close> 28ML_file \<open>~~/src/Provers/quantifier1.ML\<close> 29ML_file \<open>~~/src/Tools/atomize_elim.ML\<close> 30ML_file \<open>~~/src/Tools/cong_tac.ML\<close> 31ML_file \<open>~~/src/Tools/intuitionistic.ML\<close> setup \<open>Intuitionistic.method_setup \<^binding>\<open>iprover\<close>\<close> 32ML_file \<open>~~/src/Tools/project_rule.ML\<close> 33ML_file \<open>~~/src/Tools/subtyping.ML\<close> 34ML_file \<open>~~/src/Tools/case_product.ML\<close> 35 36 37ML \<open>Plugin_Name.declare_setup \<^binding>\<open>extraction\<close>\<close> 38 39ML \<open> 40 Plugin_Name.declare_setup \<^binding>\<open>quickcheck_random\<close>; 41 Plugin_Name.declare_setup \<^binding>\<open>quickcheck_exhaustive\<close>; 42 Plugin_Name.declare_setup \<^binding>\<open>quickcheck_bounded_forall\<close>; 43 Plugin_Name.declare_setup \<^binding>\<open>quickcheck_full_exhaustive\<close>; 44 Plugin_Name.declare_setup \<^binding>\<open>quickcheck_narrowing\<close>; 45\<close> 46ML \<open> 47 Plugin_Name.define_setup \<^binding>\<open>quickcheck\<close> 48 [\<^plugin>\<open>quickcheck_exhaustive\<close>, 49 \<^plugin>\<open>quickcheck_random\<close>, 50 \<^plugin>\<open>quickcheck_bounded_forall\<close>, 51 \<^plugin>\<open>quickcheck_full_exhaustive\<close>, 52 \<^plugin>\<open>quickcheck_narrowing\<close>] 53\<close> 54 55 56subsection \<open>Primitive logic\<close> 57 58text \<open> 59The definition of the logic is based on Mike Gordon's technical report @{cite "Gordon-TR68"} that 60describes the first implementation of HOL. However, there are a number of differences. 61In particular, we start with the definite description operator and introduce Hilbert's \<open>\<epsilon>\<close> operator 62only much later. Moreover, axiom \<open>(P \<longrightarrow> Q) \<longrightarrow> (Q \<longrightarrow> P) \<longrightarrow> (P = Q)\<close> is derived from the other 63axioms. The fact that this axiom is derivable was first noticed by Bruno Barras (for Mike Gordon's 64line of HOL systems) and later independently by Alexander Maletzky (for Isabelle/HOL). 65\<close> 66 67subsubsection \<open>Core syntax\<close> 68 69setup \<open>Axclass.class_axiomatization (\<^binding>\<open>type\<close>, [])\<close> 70default_sort type 71setup \<open>Object_Logic.add_base_sort \<^sort>\<open>type\<close>\<close> 72 73setup \<open>Proofterm.set_preproc (Proof_Rewrite_Rules.standard_preproc [])\<close> 74 75axiomatization where fun_arity: "OFCLASS('a \<Rightarrow> 'b, type_class)" 76instance "fun" :: (type, type) type by (rule fun_arity) 77 78axiomatization where itself_arity: "OFCLASS('a itself, type_class)" 79instance itself :: (type) type by (rule itself_arity) 80 81typedecl bool 82 83judgment Trueprop :: "bool \<Rightarrow> prop" ("(_)" 5) 84 85axiomatization implies :: "[bool, bool] \<Rightarrow> bool" (infixr "\<longrightarrow>" 25) 86 and eq :: "['a, 'a] \<Rightarrow> bool" 87 and The :: "('a \<Rightarrow> bool) \<Rightarrow> 'a" 88 89notation (input) 90 eq (infixl "=" 50) 91notation (output) 92 eq (infix "=" 50) 93 94text \<open>The input syntax for \<open>eq\<close> is more permissive than the output syntax 95because of the large amount of material that relies on infixl.\<close> 96 97subsubsection \<open>Defined connectives and quantifiers\<close> 98 99definition True :: bool 100 where "True \<equiv> ((\<lambda>x::bool. x) = (\<lambda>x. x))" 101 102definition All :: "('a \<Rightarrow> bool) \<Rightarrow> bool" (binder "\<forall>" 10) 103 where "All P \<equiv> (P = (\<lambda>x. True))" 104 105definition Ex :: "('a \<Rightarrow> bool) \<Rightarrow> bool" (binder "\<exists>" 10) 106 where "Ex P \<equiv> \<forall>Q. (\<forall>x. P x \<longrightarrow> Q) \<longrightarrow> Q" 107 108definition False :: bool 109 where "False \<equiv> (\<forall>P. P)" 110 111definition Not :: "bool \<Rightarrow> bool" ("\<not> _" [40] 40) 112 where not_def: "\<not> P \<equiv> P \<longrightarrow> False" 113 114definition conj :: "[bool, bool] \<Rightarrow> bool" (infixr "\<and>" 35) 115 where and_def: "P \<and> Q \<equiv> \<forall>R. (P \<longrightarrow> Q \<longrightarrow> R) \<longrightarrow> R" 116 117definition disj :: "[bool, bool] \<Rightarrow> bool" (infixr "\<or>" 30) 118 where or_def: "P \<or> Q \<equiv> \<forall>R. (P \<longrightarrow> R) \<longrightarrow> (Q \<longrightarrow> R) \<longrightarrow> R" 119 120definition Ex1 :: "('a \<Rightarrow> bool) \<Rightarrow> bool" 121 where "Ex1 P \<equiv> \<exists>x. P x \<and> (\<forall>y. P y \<longrightarrow> y = x)" 122 123 124subsubsection \<open>Additional concrete syntax\<close> 125 126syntax (ASCII) 127 "_Ex1" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool" ("(3EX! _./ _)" [0, 10] 10) 128syntax (input) 129 "_Ex1" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool" ("(3?! _./ _)" [0, 10] 10) 130syntax "_Ex1" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool" ("(3\<exists>!_./ _)" [0, 10] 10) 131translations "\<exists>!x. P" \<rightleftharpoons> "CONST Ex1 (\<lambda>x. P)" 132 133print_translation \<open> 134 [Syntax_Trans.preserve_binder_abs_tr' \<^const_syntax>\<open>Ex1\<close> \<^syntax_const>\<open>_Ex1\<close>] 135\<close> \<comment> \<open>to avoid eta-contraction of body\<close> 136 137 138syntax 139 "_Not_Ex" :: "idts \<Rightarrow> bool \<Rightarrow> bool" ("(3\<nexists>_./ _)" [0, 10] 10) 140 "_Not_Ex1" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool" ("(3\<nexists>!_./ _)" [0, 10] 10) 141translations 142 "\<nexists>x. P" \<rightleftharpoons> "\<not> (\<exists>x. P)" 143 "\<nexists>!x. P" \<rightleftharpoons> "\<not> (\<exists>!x. P)" 144 145 146abbreviation not_equal :: "['a, 'a] \<Rightarrow> bool" (infix "\<noteq>" 50) 147 where "x \<noteq> y \<equiv> \<not> (x = y)" 148 149notation (ASCII) 150 Not ("~ _" [40] 40) and 151 conj (infixr "&" 35) and 152 disj (infixr "|" 30) and 153 implies (infixr "-->" 25) and 154 not_equal (infix "~=" 50) 155 156abbreviation (iff) 157 iff :: "[bool, bool] \<Rightarrow> bool" (infixr "\<longleftrightarrow>" 25) 158 where "A \<longleftrightarrow> B \<equiv> A = B" 159 160syntax "_The" :: "[pttrn, bool] \<Rightarrow> 'a" ("(3THE _./ _)" [0, 10] 10) 161translations "THE x. P" \<rightleftharpoons> "CONST The (\<lambda>x. P)" 162print_translation \<open> 163 [(\<^const_syntax>\<open>The\<close>, fn _ => fn [Abs abs] => 164 let val (x, t) = Syntax_Trans.atomic_abs_tr' abs 165 in Syntax.const \<^syntax_const>\<open>_The\<close> $ x $ t end)] 166\<close> \<comment> \<open>To avoid eta-contraction of body\<close> 167 168nonterminal letbinds and letbind 169syntax 170 "_bind" :: "[pttrn, 'a] \<Rightarrow> letbind" ("(2_ =/ _)" 10) 171 "" :: "letbind \<Rightarrow> letbinds" ("_") 172 "_binds" :: "[letbind, letbinds] \<Rightarrow> letbinds" ("_;/ _") 173 "_Let" :: "[letbinds, 'a] \<Rightarrow> 'a" ("(let (_)/ in (_))" [0, 10] 10) 174 175nonterminal case_syn and cases_syn 176syntax 177 "_case_syntax" :: "['a, cases_syn] \<Rightarrow> 'b" ("(case _ of/ _)" 10) 178 "_case1" :: "['a, 'b] \<Rightarrow> case_syn" ("(2_ \<Rightarrow>/ _)" 10) 179 "" :: "case_syn \<Rightarrow> cases_syn" ("_") 180 "_case2" :: "[case_syn, cases_syn] \<Rightarrow> cases_syn" ("_/ | _") 181syntax (ASCII) 182 "_case1" :: "['a, 'b] \<Rightarrow> case_syn" ("(2_ =>/ _)" 10) 183 184notation (ASCII) 185 All (binder "ALL " 10) and 186 Ex (binder "EX " 10) 187 188notation (input) 189 All (binder "! " 10) and 190 Ex (binder "? " 10) 191 192 193subsubsection \<open>Axioms and basic definitions\<close> 194 195axiomatization where 196 refl: "t = (t::'a)" and 197 subst: "s = t \<Longrightarrow> P s \<Longrightarrow> P t" and 198 ext: "(\<And>x::'a. (f x ::'b) = g x) \<Longrightarrow> (\<lambda>x. f x) = (\<lambda>x. g x)" 199 \<comment> \<open>Extensionality is built into the meta-logic, and this rule expresses 200 a related property. It is an eta-expanded version of the traditional 201 rule, and similar to the ABS rule of HOL\<close> and 202 203 the_eq_trivial: "(THE x. x = a) = (a::'a)" 204 205axiomatization where 206 impI: "(P \<Longrightarrow> Q) \<Longrightarrow> P \<longrightarrow> Q" and 207 mp: "\<lbrakk>P \<longrightarrow> Q; P\<rbrakk> \<Longrightarrow> Q" and 208 209 True_or_False: "(P = True) \<or> (P = False)" 210 211definition If :: "bool \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" ("(if (_)/ then (_)/ else (_))" [0, 0, 10] 10) 212 where "If P x y \<equiv> (THE z::'a. (P = True \<longrightarrow> z = x) \<and> (P = False \<longrightarrow> z = y))" 213 214definition Let :: "'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b" 215 where "Let s f \<equiv> f s" 216 217translations 218 "_Let (_binds b bs) e" \<rightleftharpoons> "_Let b (_Let bs e)" 219 "let x = a in e" \<rightleftharpoons> "CONST Let a (\<lambda>x. e)" 220 221axiomatization undefined :: 'a 222 223class default = fixes default :: 'a 224 225 226subsection \<open>Fundamental rules\<close> 227 228subsubsection \<open>Equality\<close> 229 230lemma sym: "s = t \<Longrightarrow> t = s" 231 by (erule subst) (rule refl) 232 233lemma ssubst: "t = s \<Longrightarrow> P s \<Longrightarrow> P t" 234 by (drule sym) (erule subst) 235 236lemma trans: "\<lbrakk>r = s; s = t\<rbrakk> \<Longrightarrow> r = t" 237 by (erule subst) 238 239lemma trans_sym [Pure.elim?]: "r = s \<Longrightarrow> t = s \<Longrightarrow> r = t" 240 by (rule trans [OF _ sym]) 241 242lemma meta_eq_to_obj_eq: 243 assumes "A \<equiv> B" 244 shows "A = B" 245 unfolding assms by (rule refl) 246 247text \<open>Useful with \<open>erule\<close> for proving equalities from known equalities.\<close> 248 (* a = b 249 | | 250 c = d *) 251lemma box_equals: "\<lbrakk>a = b; a = c; b = d\<rbrakk> \<Longrightarrow> c = d" 252 apply (rule trans) 253 apply (rule trans) 254 apply (rule sym) 255 apply assumption+ 256 done 257 258text \<open>For calculational reasoning:\<close> 259 260lemma forw_subst: "a = b \<Longrightarrow> P b \<Longrightarrow> P a" 261 by (rule ssubst) 262 263lemma back_subst: "P a \<Longrightarrow> a = b \<Longrightarrow> P b" 264 by (rule subst) 265 266 267subsubsection \<open>Congruence rules for application\<close> 268 269text \<open>Similar to \<open>AP_THM\<close> in Gordon's HOL.\<close> 270lemma fun_cong: "(f :: 'a \<Rightarrow> 'b) = g \<Longrightarrow> f x = g x" 271 apply (erule subst) 272 apply (rule refl) 273 done 274 275text \<open>Similar to \<open>AP_TERM\<close> in Gordon's HOL and FOL's \<open>subst_context\<close>.\<close> 276lemma arg_cong: "x = y \<Longrightarrow> f x = f y" 277 apply (erule subst) 278 apply (rule refl) 279 done 280 281lemma arg_cong2: "\<lbrakk>a = b; c = d\<rbrakk> \<Longrightarrow> f a c = f b d" 282 apply (erule ssubst)+ 283 apply (rule refl) 284 done 285 286lemma cong: "\<lbrakk>f = g; (x::'a) = y\<rbrakk> \<Longrightarrow> f x = g y" 287 apply (erule subst)+ 288 apply (rule refl) 289 done 290 291ML \<open>fun cong_tac ctxt = Cong_Tac.cong_tac ctxt @{thm cong}\<close> 292 293 294subsubsection \<open>Equality of booleans -- iff\<close> 295 296lemma iffD2: "\<lbrakk>P = Q; Q\<rbrakk> \<Longrightarrow> P" 297 by (erule ssubst) 298 299lemma rev_iffD2: "\<lbrakk>Q; P = Q\<rbrakk> \<Longrightarrow> P" 300 by (erule iffD2) 301 302lemma iffD1: "Q = P \<Longrightarrow> Q \<Longrightarrow> P" 303 by (drule sym) (rule iffD2) 304 305lemma rev_iffD1: "Q \<Longrightarrow> Q = P \<Longrightarrow> P" 306 by (drule sym) (rule rev_iffD2) 307 308lemma iffE: 309 assumes major: "P = Q" 310 and minor: "\<lbrakk>P \<longrightarrow> Q; Q \<longrightarrow> P\<rbrakk> \<Longrightarrow> R" 311 shows R 312 by (iprover intro: minor impI major [THEN iffD2] major [THEN iffD1]) 313 314 315subsubsection \<open>True (1)\<close> 316 317lemma TrueI: True 318 unfolding True_def by (rule refl) 319 320lemma eqTrueE: "P = True \<Longrightarrow> P" 321 by (erule iffD2) (rule TrueI) 322 323 324subsubsection \<open>Universal quantifier (1)\<close> 325 326lemma spec: "\<forall>x::'a. P x \<Longrightarrow> P x" 327 apply (unfold All_def) 328 apply (rule eqTrueE) 329 apply (erule fun_cong) 330 done 331 332lemma allE: 333 assumes major: "\<forall>x. P x" 334 and minor: "P x \<Longrightarrow> R" 335 shows R 336 by (iprover intro: minor major [THEN spec]) 337 338lemma all_dupE: 339 assumes major: "\<forall>x. P x" 340 and minor: "\<lbrakk>P x; \<forall>x. P x\<rbrakk> \<Longrightarrow> R" 341 shows R 342 by (iprover intro: minor major major [THEN spec]) 343 344 345subsubsection \<open>False\<close> 346 347text \<open> 348 Depends upon \<open>spec\<close>; it is impossible to do propositional 349 logic before quantifiers! 350\<close> 351 352lemma FalseE: "False \<Longrightarrow> P" 353 apply (unfold False_def) 354 apply (erule spec) 355 done 356 357lemma False_neq_True: "False = True \<Longrightarrow> P" 358 by (erule eqTrueE [THEN FalseE]) 359 360 361subsubsection \<open>Negation\<close> 362 363lemma notI: 364 assumes "P \<Longrightarrow> False" 365 shows "\<not> P" 366 apply (unfold not_def) 367 apply (iprover intro: impI assms) 368 done 369 370lemma False_not_True: "False \<noteq> True" 371 apply (rule notI) 372 apply (erule False_neq_True) 373 done 374 375lemma True_not_False: "True \<noteq> False" 376 apply (rule notI) 377 apply (drule sym) 378 apply (erule False_neq_True) 379 done 380 381lemma notE: "\<lbrakk>\<not> P; P\<rbrakk> \<Longrightarrow> R" 382 apply (unfold not_def) 383 apply (erule mp [THEN FalseE]) 384 apply assumption 385 done 386 387lemma notI2: "(P \<Longrightarrow> \<not> Pa) \<Longrightarrow> (P \<Longrightarrow> Pa) \<Longrightarrow> \<not> P" 388 by (erule notE [THEN notI]) (erule meta_mp) 389 390 391subsubsection \<open>Implication\<close> 392 393lemma impE: 394 assumes "P \<longrightarrow> Q" P "Q \<Longrightarrow> R" 395 shows R 396 by (iprover intro: assms mp) 397 398text \<open>Reduces \<open>Q\<close> to \<open>P \<longrightarrow> Q\<close>, allowing substitution in \<open>P\<close>.\<close> 399lemma rev_mp: "\<lbrakk>P; P \<longrightarrow> Q\<rbrakk> \<Longrightarrow> Q" 400 by (iprover intro: mp) 401 402lemma contrapos_nn: 403 assumes major: "\<not> Q" 404 and minor: "P \<Longrightarrow> Q" 405 shows "\<not> P" 406 by (iprover intro: notI minor major [THEN notE]) 407 408text \<open>Not used at all, but we already have the other 3 combinations.\<close> 409lemma contrapos_pn: 410 assumes major: "Q" 411 and minor: "P \<Longrightarrow> \<not> Q" 412 shows "\<not> P" 413 by (iprover intro: notI minor major notE) 414 415lemma not_sym: "t \<noteq> s \<Longrightarrow> s \<noteq> t" 416 by (erule contrapos_nn) (erule sym) 417 418lemma eq_neq_eq_imp_neq: "\<lbrakk>x = a; a \<noteq> b; b = y\<rbrakk> \<Longrightarrow> x \<noteq> y" 419 by (erule subst, erule ssubst, assumption) 420 421 422subsubsection \<open>Disjunction (1)\<close> 423 424lemma disjE: 425 assumes major: "P \<or> Q" 426 and minorP: "P \<Longrightarrow> R" 427 and minorQ: "Q \<Longrightarrow> R" 428 shows R 429 by (iprover intro: minorP minorQ impI 430 major [unfolded or_def, THEN spec, THEN mp, THEN mp]) 431 432 433subsubsection \<open>Derivation of \<open>iffI\<close>\<close> 434 435text \<open>In an intuitionistic version of HOL \<open>iffI\<close> needs to be an axiom.\<close> 436 437lemma iffI: 438 assumes "P \<Longrightarrow> Q" and "Q \<Longrightarrow> P" 439 shows "P = Q" 440proof (rule disjE[OF True_or_False[of P]]) 441 assume 1: "P = True" 442 note Q = assms(1)[OF eqTrueE[OF this]] 443 from 1 show ?thesis 444 proof (rule ssubst) 445 from True_or_False[of Q] show "True = Q" 446 proof (rule disjE) 447 assume "Q = True" 448 thus ?thesis by(rule sym) 449 next 450 assume "Q = False" 451 with Q have False by (rule rev_iffD1) 452 thus ?thesis by (rule FalseE) 453 qed 454 qed 455next 456 assume 2: "P = False" 457 thus ?thesis 458 proof (rule ssubst) 459 from True_or_False[of Q] show "False = Q" 460 proof (rule disjE) 461 assume "Q = True" 462 from 2 assms(2)[OF eqTrueE[OF this]] have False by (rule iffD1) 463 thus ?thesis by (rule FalseE) 464 next 465 assume "Q = False" 466 thus ?thesis by(rule sym) 467 qed 468 qed 469qed 470 471 472subsubsection \<open>True (2)\<close> 473 474lemma eqTrueI: "P \<Longrightarrow> P = True" 475 by (iprover intro: iffI TrueI) 476 477 478subsubsection \<open>Universal quantifier (2)\<close> 479 480lemma allI: 481 assumes "\<And>x::'a. P x" 482 shows "\<forall>x. P x" 483 unfolding All_def by (iprover intro: ext eqTrueI assms) 484 485 486subsubsection \<open>Existential quantifier\<close> 487 488lemma exI: "P x \<Longrightarrow> \<exists>x::'a. P x" 489 unfolding Ex_def by (iprover intro: allI allE impI mp) 490 491lemma exE: 492 assumes major: "\<exists>x::'a. P x" 493 and minor: "\<And>x. P x \<Longrightarrow> Q" 494 shows "Q" 495 by (rule major [unfolded Ex_def, THEN spec, THEN mp]) (iprover intro: impI [THEN allI] minor) 496 497 498subsubsection \<open>Conjunction\<close> 499 500lemma conjI: "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> P \<and> Q" 501 unfolding and_def by (iprover intro: impI [THEN allI] mp) 502 503lemma conjunct1: "\<lbrakk>P \<and> Q\<rbrakk> \<Longrightarrow> P" 504 unfolding and_def by (iprover intro: impI dest: spec mp) 505 506lemma conjunct2: "\<lbrakk>P \<and> Q\<rbrakk> \<Longrightarrow> Q" 507 unfolding and_def by (iprover intro: impI dest: spec mp) 508 509lemma conjE: 510 assumes major: "P \<and> Q" 511 and minor: "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> R" 512 shows R 513 apply (rule minor) 514 apply (rule major [THEN conjunct1]) 515 apply (rule major [THEN conjunct2]) 516 done 517 518lemma context_conjI: 519 assumes P "P \<Longrightarrow> Q" 520 shows "P \<and> Q" 521 by (iprover intro: conjI assms) 522 523 524subsubsection \<open>Disjunction (2)\<close> 525 526lemma disjI1: "P \<Longrightarrow> P \<or> Q" 527 unfolding or_def by (iprover intro: allI impI mp) 528 529lemma disjI2: "Q \<Longrightarrow> P \<or> Q" 530 unfolding or_def by (iprover intro: allI impI mp) 531 532 533subsubsection \<open>Classical logic\<close> 534 535lemma classical: 536 assumes prem: "\<not> P \<Longrightarrow> P" 537 shows P 538 apply (rule True_or_False [THEN disjE, THEN eqTrueE]) 539 apply assumption 540 apply (rule notI [THEN prem, THEN eqTrueI]) 541 apply (erule subst) 542 apply assumption 543 done 544 545lemmas ccontr = FalseE [THEN classical] 546 547text \<open>\<open>notE\<close> with premises exchanged; it discharges \<open>\<not> R\<close> so that it can be used to 548 make elimination rules.\<close> 549lemma rev_notE: 550 assumes premp: P 551 and premnot: "\<not> R \<Longrightarrow> \<not> P" 552 shows R 553 apply (rule ccontr) 554 apply (erule notE [OF premnot premp]) 555 done 556 557text \<open>Double negation law.\<close> 558lemma notnotD: "\<not>\<not> P \<Longrightarrow> P" 559 apply (rule classical) 560 apply (erule notE) 561 apply assumption 562 done 563 564lemma contrapos_pp: 565 assumes p1: Q 566 and p2: "\<not> P \<Longrightarrow> \<not> Q" 567 shows P 568 by (iprover intro: classical p1 p2 notE) 569 570 571subsubsection \<open>Unique existence\<close> 572 573lemma ex1I: 574 assumes "P a" "\<And>x. P x \<Longrightarrow> x = a" 575 shows "\<exists>!x. P x" 576 unfolding Ex1_def by (iprover intro: assms exI conjI allI impI) 577 578text \<open>Sometimes easier to use: the premises have no shared variables. Safe!\<close> 579lemma ex_ex1I: 580 assumes ex_prem: "\<exists>x. P x" 581 and eq: "\<And>x y. \<lbrakk>P x; P y\<rbrakk> \<Longrightarrow> x = y" 582 shows "\<exists>!x. P x" 583 by (iprover intro: ex_prem [THEN exE] ex1I eq) 584 585lemma ex1E: 586 assumes major: "\<exists>!x. P x" 587 and minor: "\<And>x. \<lbrakk>P x; \<forall>y. P y \<longrightarrow> y = x\<rbrakk> \<Longrightarrow> R" 588 shows R 589 apply (rule major [unfolded Ex1_def, THEN exE]) 590 apply (erule conjE) 591 apply (iprover intro: minor) 592 done 593 594lemma ex1_implies_ex: "\<exists>!x. P x \<Longrightarrow> \<exists>x. P x" 595 apply (erule ex1E) 596 apply (rule exI) 597 apply assumption 598 done 599 600 601subsubsection \<open>Classical intro rules for disjunction and existential quantifiers\<close> 602 603lemma disjCI: 604 assumes "\<not> Q \<Longrightarrow> P" 605 shows "P \<or> Q" 606 by (rule classical) (iprover intro: assms disjI1 disjI2 notI elim: notE) 607 608lemma excluded_middle: "\<not> P \<or> P" 609 by (iprover intro: disjCI) 610 611text \<open> 612 case distinction as a natural deduction rule. 613 Note that \<open>\<not> P\<close> is the second case, not the first. 614\<close> 615lemma case_split [case_names True False]: 616 assumes prem1: "P \<Longrightarrow> Q" 617 and prem2: "\<not> P \<Longrightarrow> Q" 618 shows Q 619 apply (rule excluded_middle [THEN disjE]) 620 apply (erule prem2) 621 apply (erule prem1) 622 done 623 624text \<open>Classical implies (\<open>\<longrightarrow>\<close>) elimination.\<close> 625lemma impCE: 626 assumes major: "P \<longrightarrow> Q" 627 and minor: "\<not> P \<Longrightarrow> R" "Q \<Longrightarrow> R" 628 shows R 629 apply (rule excluded_middle [of P, THEN disjE]) 630 apply (iprover intro: minor major [THEN mp])+ 631 done 632 633text \<open> 634 This version of \<open>\<longrightarrow>\<close> elimination works on \<open>Q\<close> before \<open>P\<close>. It works best for 635 those cases in which \<open>P\<close> holds "almost everywhere". Can't install as 636 default: would break old proofs. 637\<close> 638lemma impCE': 639 assumes major: "P \<longrightarrow> Q" 640 and minor: "Q \<Longrightarrow> R" "\<not> P \<Longrightarrow> R" 641 shows R 642 apply (rule excluded_middle [of P, THEN disjE]) 643 apply (iprover intro: minor major [THEN mp])+ 644 done 645 646text \<open>Classical \<open>\<longleftrightarrow>\<close> elimination.\<close> 647lemma iffCE: 648 assumes major: "P = Q" 649 and minor: "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> R" "\<lbrakk>\<not> P; \<not> Q\<rbrakk> \<Longrightarrow> R" 650 shows R 651 by (rule major [THEN iffE]) (iprover intro: minor elim: impCE notE) 652 653lemma exCI: 654 assumes "\<forall>x. \<not> P x \<Longrightarrow> P a" 655 shows "\<exists>x. P x" 656 by (rule ccontr) (iprover intro: assms exI allI notI notE [of "\<exists>x. P x"]) 657 658 659subsubsection \<open>Intuitionistic Reasoning\<close> 660 661lemma impE': 662 assumes 1: "P \<longrightarrow> Q" 663 and 2: "Q \<Longrightarrow> R" 664 and 3: "P \<longrightarrow> Q \<Longrightarrow> P" 665 shows R 666proof - 667 from 3 and 1 have P . 668 with 1 have Q by (rule impE) 669 with 2 show R . 670qed 671 672lemma allE': 673 assumes 1: "\<forall>x. P x" 674 and 2: "P x \<Longrightarrow> \<forall>x. P x \<Longrightarrow> Q" 675 shows Q 676proof - 677 from 1 have "P x" by (rule spec) 678 from this and 1 show Q by (rule 2) 679qed 680 681lemma notE': 682 assumes 1: "\<not> P" 683 and 2: "\<not> P \<Longrightarrow> P" 684 shows R 685proof - 686 from 2 and 1 have P . 687 with 1 show R by (rule notE) 688qed 689 690lemma TrueE: "True \<Longrightarrow> P \<Longrightarrow> P" . 691lemma notFalseE: "\<not> False \<Longrightarrow> P \<Longrightarrow> P" . 692 693lemmas [Pure.elim!] = disjE iffE FalseE conjE exE TrueE notFalseE 694 and [Pure.intro!] = iffI conjI impI TrueI notI allI refl 695 and [Pure.elim 2] = allE notE' impE' 696 and [Pure.intro] = exI disjI2 disjI1 697 698lemmas [trans] = trans 699 and [sym] = sym not_sym 700 and [Pure.elim?] = iffD1 iffD2 impE 701 702 703subsubsection \<open>Atomizing meta-level connectives\<close> 704 705axiomatization where 706 eq_reflection: "x = y \<Longrightarrow> x \<equiv> y" \<comment> \<open>admissible axiom\<close> 707 708lemma atomize_all [atomize]: "(\<And>x. P x) \<equiv> Trueprop (\<forall>x. P x)" 709proof 710 assume "\<And>x. P x" 711 then show "\<forall>x. P x" .. 712next 713 assume "\<forall>x. P x" 714 then show "\<And>x. P x" by (rule allE) 715qed 716 717lemma atomize_imp [atomize]: "(A \<Longrightarrow> B) \<equiv> Trueprop (A \<longrightarrow> B)" 718proof 719 assume r: "A \<Longrightarrow> B" 720 show "A \<longrightarrow> B" by (rule impI) (rule r) 721next 722 assume "A \<longrightarrow> B" and A 723 then show B by (rule mp) 724qed 725 726lemma atomize_not: "(A \<Longrightarrow> False) \<equiv> Trueprop (\<not> A)" 727proof 728 assume r: "A \<Longrightarrow> False" 729 show "\<not> A" by (rule notI) (rule r) 730next 731 assume "\<not> A" and A 732 then show False by (rule notE) 733qed 734 735lemma atomize_eq [atomize, code]: "(x \<equiv> y) \<equiv> Trueprop (x = y)" 736proof 737 assume "x \<equiv> y" 738 show "x = y" by (unfold \<open>x \<equiv> y\<close>) (rule refl) 739next 740 assume "x = y" 741 then show "x \<equiv> y" by (rule eq_reflection) 742qed 743 744lemma atomize_conj [atomize]: "(A &&& B) \<equiv> Trueprop (A \<and> B)" 745proof 746 assume conj: "A &&& B" 747 show "A \<and> B" 748 proof (rule conjI) 749 from conj show A by (rule conjunctionD1) 750 from conj show B by (rule conjunctionD2) 751 qed 752next 753 assume conj: "A \<and> B" 754 show "A &&& B" 755 proof - 756 from conj show A .. 757 from conj show B .. 758 qed 759qed 760 761lemmas [symmetric, rulify] = atomize_all atomize_imp 762 and [symmetric, defn] = atomize_all atomize_imp atomize_eq 763 764 765subsubsection \<open>Atomizing elimination rules\<close> 766 767lemma atomize_exL[atomize_elim]: "(\<And>x. P x \<Longrightarrow> Q) \<equiv> ((\<exists>x. P x) \<Longrightarrow> Q)" 768 by rule iprover+ 769 770lemma atomize_conjL[atomize_elim]: "(A \<Longrightarrow> B \<Longrightarrow> C) \<equiv> (A \<and> B \<Longrightarrow> C)" 771 by rule iprover+ 772 773lemma atomize_disjL[atomize_elim]: "((A \<Longrightarrow> C) \<Longrightarrow> (B \<Longrightarrow> C) \<Longrightarrow> C) \<equiv> ((A \<or> B \<Longrightarrow> C) \<Longrightarrow> C)" 774 by rule iprover+ 775 776lemma atomize_elimL[atomize_elim]: "(\<And>B. (A \<Longrightarrow> B) \<Longrightarrow> B) \<equiv> Trueprop A" .. 777 778 779subsection \<open>Package setup\<close> 780 781ML_file \<open>Tools/hologic.ML\<close> 782ML_file \<open>Tools/rewrite_hol_proof.ML\<close> 783 784setup \<open>Proofterm.set_preproc (Proof_Rewrite_Rules.standard_preproc Rewrite_HOL_Proof.rews)\<close> 785 786 787subsubsection \<open>Sledgehammer setup\<close> 788 789text \<open> 790 Theorems blacklisted to Sledgehammer. These theorems typically produce clauses 791 that are prolific (match too many equality or membership literals) and relate to 792 seldom-used facts. Some duplicate other rules. 793\<close> 794 795named_theorems no_atp "theorems that should be filtered out by Sledgehammer" 796 797 798subsubsection \<open>Classical Reasoner setup\<close> 799 800lemma imp_elim: "P \<longrightarrow> Q \<Longrightarrow> (\<not> R \<Longrightarrow> P) \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R" 801 by (rule classical) iprover 802 803lemma swap: "\<not> P \<Longrightarrow> (\<not> R \<Longrightarrow> P) \<Longrightarrow> R" 804 by (rule classical) iprover 805 806lemma thin_refl: "\<lbrakk>x = x; PROP W\<rbrakk> \<Longrightarrow> PROP W" . 807 808ML \<open> 809structure Hypsubst = Hypsubst 810( 811 val dest_eq = HOLogic.dest_eq 812 val dest_Trueprop = HOLogic.dest_Trueprop 813 val dest_imp = HOLogic.dest_imp 814 val eq_reflection = @{thm eq_reflection} 815 val rev_eq_reflection = @{thm meta_eq_to_obj_eq} 816 val imp_intr = @{thm impI} 817 val rev_mp = @{thm rev_mp} 818 val subst = @{thm subst} 819 val sym = @{thm sym} 820 val thin_refl = @{thm thin_refl}; 821); 822open Hypsubst; 823 824structure Classical = Classical 825( 826 val imp_elim = @{thm imp_elim} 827 val not_elim = @{thm notE} 828 val swap = @{thm swap} 829 val classical = @{thm classical} 830 val sizef = Drule.size_of_thm 831 val hyp_subst_tacs = [Hypsubst.hyp_subst_tac] 832); 833 834structure Basic_Classical: BASIC_CLASSICAL = Classical; 835open Basic_Classical; 836\<close> 837 838setup \<open> 839 (*prevent substitution on bool*) 840 let 841 fun non_bool_eq (\<^const_name>\<open>HOL.eq\<close>, Type (_, [T, _])) = T <> \<^typ>\<open>bool\<close> 842 | non_bool_eq _ = false; 843 fun hyp_subst_tac' ctxt = 844 SUBGOAL (fn (goal, i) => 845 if Term.exists_Const non_bool_eq goal 846 then Hypsubst.hyp_subst_tac ctxt i 847 else no_tac); 848 in 849 Context_Rules.addSWrapper (fn ctxt => fn tac => hyp_subst_tac' ctxt ORELSE' tac) 850 end 851\<close> 852 853declare iffI [intro!] 854 and notI [intro!] 855 and impI [intro!] 856 and disjCI [intro!] 857 and conjI [intro!] 858 and TrueI [intro!] 859 and refl [intro!] 860 861declare iffCE [elim!] 862 and FalseE [elim!] 863 and impCE [elim!] 864 and disjE [elim!] 865 and conjE [elim!] 866 867declare ex_ex1I [intro!] 868 and allI [intro!] 869 and exI [intro] 870 871declare exE [elim!] 872 allE [elim] 873 874ML \<open>val HOL_cs = claset_of \<^context>\<close> 875 876lemma contrapos_np: "\<not> Q \<Longrightarrow> (\<not> P \<Longrightarrow> Q) \<Longrightarrow> P" 877 apply (erule swap) 878 apply (erule (1) meta_mp) 879 done 880 881declare ex_ex1I [rule del, intro! 2] 882 and ex1I [intro] 883 884declare ext [intro] 885 886lemmas [intro?] = ext 887 and [elim?] = ex1_implies_ex 888 889text \<open>Better than \<open>ex1E\<close> for classical reasoner: needs no quantifier duplication!\<close> 890lemma alt_ex1E [elim!]: 891 assumes major: "\<exists>!x. P x" 892 and prem: "\<And>x. \<lbrakk>P x; \<forall>y y'. P y \<and> P y' \<longrightarrow> y = y'\<rbrakk> \<Longrightarrow> R" 893 shows R 894 apply (rule ex1E [OF major]) 895 apply (rule prem) 896 apply assumption 897 apply (rule allI)+ 898 apply (tactic \<open>eresolve_tac \<^context> [Classical.dup_elim \<^context> @{thm allE}] 1\<close>) 899 apply iprover 900 done 901 902ML \<open> 903 structure Blast = Blast 904 ( 905 structure Classical = Classical 906 val Trueprop_const = dest_Const \<^const>\<open>Trueprop\<close> 907 val equality_name = \<^const_name>\<open>HOL.eq\<close> 908 val not_name = \<^const_name>\<open>Not\<close> 909 val notE = @{thm notE} 910 val ccontr = @{thm ccontr} 911 val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac 912 ); 913 val blast_tac = Blast.blast_tac; 914\<close> 915 916 917subsubsection \<open>THE: definite description operator\<close> 918 919lemma the_equality [intro]: 920 assumes "P a" 921 and "\<And>x. P x \<Longrightarrow> x = a" 922 shows "(THE x. P x) = a" 923 by (blast intro: assms trans [OF arg_cong [where f=The] the_eq_trivial]) 924 925lemma theI: 926 assumes "P a" 927 and "\<And>x. P x \<Longrightarrow> x = a" 928 shows "P (THE x. P x)" 929 by (iprover intro: assms the_equality [THEN ssubst]) 930 931lemma theI': "\<exists>!x. P x \<Longrightarrow> P (THE x. P x)" 932 by (blast intro: theI) 933 934text \<open>Easier to apply than \<open>theI\<close>: only one occurrence of \<open>P\<close>.\<close> 935lemma theI2: 936 assumes "P a" "\<And>x. P x \<Longrightarrow> x = a" "\<And>x. P x \<Longrightarrow> Q x" 937 shows "Q (THE x. P x)" 938 by (iprover intro: assms theI) 939 940lemma the1I2: 941 assumes "\<exists>!x. P x" "\<And>x. P x \<Longrightarrow> Q x" 942 shows "Q (THE x. P x)" 943 by (iprover intro: assms(2) theI2[where P=P and Q=Q] ex1E[OF assms(1)] elim: allE impE) 944 945lemma the1_equality [elim?]: "\<lbrakk>\<exists>!x. P x; P a\<rbrakk> \<Longrightarrow> (THE x. P x) = a" 946 by blast 947 948lemma the_sym_eq_trivial: "(THE y. x = y) = x" 949 by blast 950 951 952subsubsection \<open>Simplifier\<close> 953 954lemma eta_contract_eq: "(\<lambda>s. f s) = f" .. 955 956lemma simp_thms: 957 shows not_not: "(\<not> \<not> P) = P" 958 and Not_eq_iff: "((\<not> P) = (\<not> Q)) = (P = Q)" 959 and 960 "(P \<noteq> Q) = (P = (\<not> Q))" 961 "(P \<or> \<not>P) = True" "(\<not> P \<or> P) = True" 962 "(x = x) = True" 963 and not_True_eq_False [code]: "(\<not> True) = False" 964 and not_False_eq_True [code]: "(\<not> False) = True" 965 and 966 "(\<not> P) \<noteq> P" "P \<noteq> (\<not> P)" 967 "(True = P) = P" 968 and eq_True: "(P = True) = P" 969 and "(False = P) = (\<not> P)" 970 and eq_False: "(P = False) = (\<not> P)" 971 and 972 "(True \<longrightarrow> P) = P" "(False \<longrightarrow> P) = True" 973 "(P \<longrightarrow> True) = True" "(P \<longrightarrow> P) = True" 974 "(P \<longrightarrow> False) = (\<not> P)" "(P \<longrightarrow> \<not> P) = (\<not> P)" 975 "(P \<and> True) = P" "(True \<and> P) = P" 976 "(P \<and> False) = False" "(False \<and> P) = False" 977 "(P \<and> P) = P" "(P \<and> (P \<and> Q)) = (P \<and> Q)" 978 "(P \<and> \<not> P) = False" "(\<not> P \<and> P) = False" 979 "(P \<or> True) = True" "(True \<or> P) = True" 980 "(P \<or> False) = P" "(False \<or> P) = P" 981 "(P \<or> P) = P" "(P \<or> (P \<or> Q)) = (P \<or> Q)" and 982 "(\<forall>x. P) = P" "(\<exists>x. P) = P" "\<exists>x. x = t" "\<exists>x. t = x" 983 and 984 "\<And>P. (\<exists>x. x = t \<and> P x) = P t" 985 "\<And>P. (\<exists>x. t = x \<and> P x) = P t" 986 "\<And>P. (\<forall>x. x = t \<longrightarrow> P x) = P t" 987 "\<And>P. (\<forall>x. t = x \<longrightarrow> P x) = P t" 988 "(\<forall>x. x \<noteq> t) = False" "(\<forall>x. t \<noteq> x) = False" 989 by (blast, blast, blast, blast, blast, iprover+) 990 991lemma disj_absorb: "A \<or> A \<longleftrightarrow> A" 992 by blast 993 994lemma disj_left_absorb: "A \<or> (A \<or> B) \<longleftrightarrow> A \<or> B" 995 by blast 996 997lemma conj_absorb: "A \<and> A \<longleftrightarrow> A" 998 by blast 999 1000lemma conj_left_absorb: "A \<and> (A \<and> B) \<longleftrightarrow> A \<and> B" 1001 by blast 1002 1003lemma eq_ac: 1004 shows eq_commute: "a = b \<longleftrightarrow> b = a" 1005 and iff_left_commute: "(P \<longleftrightarrow> (Q \<longleftrightarrow> R)) \<longleftrightarrow> (Q \<longleftrightarrow> (P \<longleftrightarrow> R))" 1006 and iff_assoc: "((P \<longleftrightarrow> Q) \<longleftrightarrow> R) \<longleftrightarrow> (P \<longleftrightarrow> (Q \<longleftrightarrow> R))" 1007 by (iprover, blast+) 1008 1009lemma neq_commute: "a \<noteq> b \<longleftrightarrow> b \<noteq> a" by iprover 1010 1011lemma conj_comms: 1012 shows conj_commute: "P \<and> Q \<longleftrightarrow> Q \<and> P" 1013 and conj_left_commute: "P \<and> (Q \<and> R) \<longleftrightarrow> Q \<and> (P \<and> R)" by iprover+ 1014lemma conj_assoc: "(P \<and> Q) \<and> R \<longleftrightarrow> P \<and> (Q \<and> R)" by iprover 1015 1016lemmas conj_ac = conj_commute conj_left_commute conj_assoc 1017 1018lemma disj_comms: 1019 shows disj_commute: "P \<or> Q \<longleftrightarrow> Q \<or> P" 1020 and disj_left_commute: "P \<or> (Q \<or> R) \<longleftrightarrow> Q \<or> (P \<or> R)" by iprover+ 1021lemma disj_assoc: "(P \<or> Q) \<or> R \<longleftrightarrow> P \<or> (Q \<or> R)" by iprover 1022 1023lemmas disj_ac = disj_commute disj_left_commute disj_assoc 1024 1025lemma conj_disj_distribL: "P \<and> (Q \<or> R) \<longleftrightarrow> P \<and> Q \<or> P \<and> R" by iprover 1026lemma conj_disj_distribR: "(P \<or> Q) \<and> R \<longleftrightarrow> P \<and> R \<or> Q \<and> R" by iprover 1027 1028lemma disj_conj_distribL: "P \<or> (Q \<and> R) \<longleftrightarrow> (P \<or> Q) \<and> (P \<or> R)" by iprover 1029lemma disj_conj_distribR: "(P \<and> Q) \<or> R \<longleftrightarrow> (P \<or> R) \<and> (Q \<or> R)" by iprover 1030 1031lemma imp_conjR: "(P \<longrightarrow> (Q \<and> R)) = ((P \<longrightarrow> Q) \<and> (P \<longrightarrow> R))" by iprover 1032lemma imp_conjL: "((P \<and> Q) \<longrightarrow> R) = (P \<longrightarrow> (Q \<longrightarrow> R))" by iprover 1033lemma imp_disjL: "((P \<or> Q) \<longrightarrow> R) = ((P \<longrightarrow> R) \<and> (Q \<longrightarrow> R))" by iprover 1034 1035text \<open>These two are specialized, but \<open>imp_disj_not1\<close> is useful in \<open>Auth/Yahalom\<close>.\<close> 1036lemma imp_disj_not1: "(P \<longrightarrow> Q \<or> R) \<longleftrightarrow> (\<not> Q \<longrightarrow> P \<longrightarrow> R)" by blast 1037lemma imp_disj_not2: "(P \<longrightarrow> Q \<or> R) \<longleftrightarrow> (\<not> R \<longrightarrow> P \<longrightarrow> Q)" by blast 1038 1039lemma imp_disj1: "((P \<longrightarrow> Q) \<or> R) \<longleftrightarrow> (P \<longrightarrow> Q \<or> R)" by blast 1040lemma imp_disj2: "(Q \<or> (P \<longrightarrow> R)) \<longleftrightarrow> (P \<longrightarrow> Q \<or> R)" by blast 1041 1042lemma imp_cong: "(P = P') \<Longrightarrow> (P' \<Longrightarrow> (Q = Q')) \<Longrightarrow> ((P \<longrightarrow> Q) \<longleftrightarrow> (P' \<longrightarrow> Q'))" 1043 by iprover 1044 1045lemma de_Morgan_disj: "\<not> (P \<or> Q) \<longleftrightarrow> \<not> P \<and> \<not> Q" by iprover 1046lemma de_Morgan_conj: "\<not> (P \<and> Q) \<longleftrightarrow> \<not> P \<or> \<not> Q" by blast 1047lemma not_imp: "\<not> (P \<longrightarrow> Q) \<longleftrightarrow> P \<and> \<not> Q" by blast 1048lemma not_iff: "P \<noteq> Q \<longleftrightarrow> (P \<longleftrightarrow> \<not> Q)" by blast 1049lemma disj_not1: "\<not> P \<or> Q \<longleftrightarrow> (P \<longrightarrow> Q)" by blast 1050lemma disj_not2: "P \<or> \<not> Q \<longleftrightarrow> (Q \<longrightarrow> P)" by blast \<comment> \<open>changes orientation :-(\<close> 1051lemma imp_conv_disj: "(P \<longrightarrow> Q) \<longleftrightarrow> (\<not> P) \<or> Q" by blast 1052lemma disj_imp: "P \<or> Q \<longleftrightarrow> \<not> P \<longrightarrow> Q" by blast 1053 1054lemma iff_conv_conj_imp: "(P \<longleftrightarrow> Q) \<longleftrightarrow> (P \<longrightarrow> Q) \<and> (Q \<longrightarrow> P)" by iprover 1055 1056 1057lemma cases_simp: "(P \<longrightarrow> Q) \<and> (\<not> P \<longrightarrow> Q) \<longleftrightarrow> Q" 1058 \<comment> \<open>Avoids duplication of subgoals after \<open>if_split\<close>, when the true and false\<close> 1059 \<comment> \<open>cases boil down to the same thing.\<close> 1060 by blast 1061 1062lemma not_all: "\<not> (\<forall>x. P x) \<longleftrightarrow> (\<exists>x. \<not> P x)" by blast 1063lemma imp_all: "((\<forall>x. P x) \<longrightarrow> Q) \<longleftrightarrow> (\<exists>x. P x \<longrightarrow> Q)" by blast 1064lemma not_ex: "\<not> (\<exists>x. P x) \<longleftrightarrow> (\<forall>x. \<not> P x)" by iprover 1065lemma imp_ex: "((\<exists>x. P x) \<longrightarrow> Q) \<longleftrightarrow> (\<forall>x. P x \<longrightarrow> Q)" by iprover 1066lemma all_not_ex: "(\<forall>x. P x) \<longleftrightarrow> \<not> (\<exists>x. \<not> P x)" by blast 1067 1068declare All_def [no_atp] 1069 1070lemma ex_disj_distrib: "(\<exists>x. P x \<or> Q x) \<longleftrightarrow> (\<exists>x. P x) \<or> (\<exists>x. Q x)" by iprover 1071lemma all_conj_distrib: "(\<forall>x. P x \<and> Q x) \<longleftrightarrow> (\<forall>x. P x) \<and> (\<forall>x. Q x)" by iprover 1072 1073text \<open> 1074 \<^medskip> The \<open>\<and>\<close> congruence rule: not included by default! 1075 May slow rewrite proofs down by as much as 50\%\<close> 1076 1077lemma conj_cong: "P = P' \<Longrightarrow> (P' \<Longrightarrow> Q = Q') \<Longrightarrow> (P \<and> Q) = (P' \<and> Q')" 1078 by iprover 1079 1080lemma rev_conj_cong: "Q = Q' \<Longrightarrow> (Q' \<Longrightarrow> P = P') \<Longrightarrow> (P \<and> Q) = (P' \<and> Q')" 1081 by iprover 1082 1083text \<open>The \<open>|\<close> congruence rule: not included by default!\<close> 1084 1085lemma disj_cong: "P = P' \<Longrightarrow> (\<not> P' \<Longrightarrow> Q = Q') \<Longrightarrow> (P \<or> Q) = (P' \<or> Q')" 1086 by blast 1087 1088 1089text \<open>\<^medskip> if-then-else rules\<close> 1090 1091lemma if_True [code]: "(if True then x else y) = x" 1092 unfolding If_def by blast 1093 1094lemma if_False [code]: "(if False then x else y) = y" 1095 unfolding If_def by blast 1096 1097lemma if_P: "P \<Longrightarrow> (if P then x else y) = x" 1098 unfolding If_def by blast 1099 1100lemma if_not_P: "\<not> P \<Longrightarrow> (if P then x else y) = y" 1101 unfolding If_def by blast 1102 1103lemma if_split: "P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))" 1104 apply (rule case_split [of Q]) 1105 apply (simplesubst if_P) 1106 prefer 3 1107 apply (simplesubst if_not_P) 1108 apply blast+ 1109 done 1110 1111lemma if_split_asm: "P (if Q then x else y) = (\<not> ((Q \<and> \<not> P x) \<or> (\<not> Q \<and> \<not> P y)))" 1112 by (simplesubst if_split) blast 1113 1114lemmas if_splits [no_atp] = if_split if_split_asm 1115 1116lemma if_cancel: "(if c then x else x) = x" 1117 by (simplesubst if_split) blast 1118 1119lemma if_eq_cancel: "(if x = y then y else x) = x" 1120 by (simplesubst if_split) blast 1121 1122lemma if_bool_eq_conj: "(if P then Q else R) = ((P \<longrightarrow> Q) \<and> (\<not> P \<longrightarrow> R))" 1123 \<comment> \<open>This form is useful for expanding \<open>if\<close>s on the RIGHT of the \<open>\<Longrightarrow>\<close> symbol.\<close> 1124 by (rule if_split) 1125 1126lemma if_bool_eq_disj: "(if P then Q else R) = ((P \<and> Q) \<or> (\<not> P \<and> R))" 1127 \<comment> \<open>And this form is useful for expanding \<open>if\<close>s on the LEFT.\<close> 1128 by (simplesubst if_split) blast 1129 1130lemma Eq_TrueI: "P \<Longrightarrow> P \<equiv> True" unfolding atomize_eq by iprover 1131lemma Eq_FalseI: "\<not> P \<Longrightarrow> P \<equiv> False" unfolding atomize_eq by iprover 1132 1133text \<open>\<^medskip> let rules for simproc\<close> 1134 1135lemma Let_folded: "f x \<equiv> g x \<Longrightarrow> Let x f \<equiv> Let x g" 1136 by (unfold Let_def) 1137 1138lemma Let_unfold: "f x \<equiv> g \<Longrightarrow> Let x f \<equiv> g" 1139 by (unfold Let_def) 1140 1141text \<open> 1142 The following copy of the implication operator is useful for 1143 fine-tuning congruence rules. It instructs the simplifier to simplify 1144 its premise. 1145\<close> 1146 1147definition simp_implies :: "prop \<Rightarrow> prop \<Rightarrow> prop" (infixr "=simp=>" 1) 1148 where "simp_implies \<equiv> (\<Longrightarrow>)" 1149 1150lemma simp_impliesI: 1151 assumes PQ: "(PROP P \<Longrightarrow> PROP Q)" 1152 shows "PROP P =simp=> PROP Q" 1153 apply (unfold simp_implies_def) 1154 apply (rule PQ) 1155 apply assumption 1156 done 1157 1158lemma simp_impliesE: 1159 assumes PQ: "PROP P =simp=> PROP Q" 1160 and P: "PROP P" 1161 and QR: "PROP Q \<Longrightarrow> PROP R" 1162 shows "PROP R" 1163 apply (rule QR) 1164 apply (rule PQ [unfolded simp_implies_def]) 1165 apply (rule P) 1166 done 1167 1168lemma simp_implies_cong: 1169 assumes PP' :"PROP P \<equiv> PROP P'" 1170 and P'QQ': "PROP P' \<Longrightarrow> (PROP Q \<equiv> PROP Q')" 1171 shows "(PROP P =simp=> PROP Q) \<equiv> (PROP P' =simp=> PROP Q')" 1172 unfolding simp_implies_def 1173proof (rule equal_intr_rule) 1174 assume PQ: "PROP P \<Longrightarrow> PROP Q" 1175 and P': "PROP P'" 1176 from PP' [symmetric] and P' have "PROP P" 1177 by (rule equal_elim_rule1) 1178 then have "PROP Q" by (rule PQ) 1179 with P'QQ' [OF P'] show "PROP Q'" by (rule equal_elim_rule1) 1180next 1181 assume P'Q': "PROP P' \<Longrightarrow> PROP Q'" 1182 and P: "PROP P" 1183 from PP' and P have P': "PROP P'" by (rule equal_elim_rule1) 1184 then have "PROP Q'" by (rule P'Q') 1185 with P'QQ' [OF P', symmetric] show "PROP Q" 1186 by (rule equal_elim_rule1) 1187qed 1188 1189lemma uncurry: 1190 assumes "P \<longrightarrow> Q \<longrightarrow> R" 1191 shows "P \<and> Q \<longrightarrow> R" 1192 using assms by blast 1193 1194lemma iff_allI: 1195 assumes "\<And>x. P x = Q x" 1196 shows "(\<forall>x. P x) = (\<forall>x. Q x)" 1197 using assms by blast 1198 1199lemma iff_exI: 1200 assumes "\<And>x. P x = Q x" 1201 shows "(\<exists>x. P x) = (\<exists>x. Q x)" 1202 using assms by blast 1203 1204lemma all_comm: "(\<forall>x y. P x y) = (\<forall>y x. P x y)" 1205 by blast 1206 1207lemma ex_comm: "(\<exists>x y. P x y) = (\<exists>y x. P x y)" 1208 by blast 1209 1210ML_file \<open>Tools/simpdata.ML\<close> 1211ML \<open>open Simpdata\<close> 1212 1213setup \<open> 1214 map_theory_simpset (put_simpset HOL_basic_ss) #> 1215 Simplifier.method_setup Splitter.split_modifiers 1216\<close> 1217 1218simproc_setup defined_Ex ("\<exists>x. P x") = \<open>K Quantifier1.rearrange_ex\<close> 1219simproc_setup defined_All ("\<forall>x. P x") = \<open>K Quantifier1.rearrange_all\<close> 1220 1221text \<open>Simproc for proving \<open>(y = x) \<equiv> False\<close> from premise \<open>\<not> (x = y)\<close>:\<close> 1222 1223simproc_setup neq ("x = y") = \<open>fn _ => 1224 let 1225 val neq_to_EQ_False = @{thm not_sym} RS @{thm Eq_FalseI}; 1226 fun is_neq eq lhs rhs thm = 1227 (case Thm.prop_of thm of 1228 _ $ (Not $ (eq' $ l' $ r')) => 1229 Not = HOLogic.Not andalso eq' = eq andalso 1230 r' aconv lhs andalso l' aconv rhs 1231 | _ => false); 1232 fun proc ss ct = 1233 (case Thm.term_of ct of 1234 eq $ lhs $ rhs => 1235 (case find_first (is_neq eq lhs rhs) (Simplifier.prems_of ss) of 1236 SOME thm => SOME (thm RS neq_to_EQ_False) 1237 | NONE => NONE) 1238 | _ => NONE); 1239 in proc end 1240\<close> 1241 1242simproc_setup let_simp ("Let x f") = \<open> 1243 let 1244 fun count_loose (Bound i) k = if i >= k then 1 else 0 1245 | count_loose (s $ t) k = count_loose s k + count_loose t k 1246 | count_loose (Abs (_, _, t)) k = count_loose t (k + 1) 1247 | count_loose _ _ = 0; 1248 fun is_trivial_let (Const (\<^const_name>\<open>Let\<close>, _) $ x $ t) = 1249 (case t of 1250 Abs (_, _, t') => count_loose t' 0 <= 1 1251 | _ => true); 1252 in 1253 fn _ => fn ctxt => fn ct => 1254 if is_trivial_let (Thm.term_of ct) 1255 then SOME @{thm Let_def} (*no or one ocurrence of bound variable*) 1256 else 1257 let (*Norbert Schirmer's case*) 1258 val t = Thm.term_of ct; 1259 val (t', ctxt') = yield_singleton (Variable.import_terms false) t ctxt; 1260 in 1261 Option.map (hd o Variable.export ctxt' ctxt o single) 1262 (case t' of Const (\<^const_name>\<open>Let\<close>,_) $ x $ f => (* x and f are already in normal form *) 1263 if is_Free x orelse is_Bound x orelse is_Const x 1264 then SOME @{thm Let_def} 1265 else 1266 let 1267 val n = case f of (Abs (x, _, _)) => x | _ => "x"; 1268 val cx = Thm.cterm_of ctxt x; 1269 val xT = Thm.typ_of_cterm cx; 1270 val cf = Thm.cterm_of ctxt f; 1271 val fx_g = Simplifier.rewrite ctxt (Thm.apply cf cx); 1272 val (_ $ _ $ g) = Thm.prop_of fx_g; 1273 val g' = abstract_over (x, g); 1274 val abs_g'= Abs (n, xT, g'); 1275 in 1276 if g aconv g' then 1277 let 1278 val rl = 1279 infer_instantiate ctxt [(("f", 0), cf), (("x", 0), cx)] @{thm Let_unfold}; 1280 in SOME (rl OF [fx_g]) end 1281 else if (Envir.beta_eta_contract f) aconv (Envir.beta_eta_contract abs_g') 1282 then NONE (*avoid identity conversion*) 1283 else 1284 let 1285 val g'x = abs_g' $ x; 1286 val g_g'x = Thm.symmetric (Thm.beta_conversion false (Thm.cterm_of ctxt g'x)); 1287 val rl = 1288 @{thm Let_folded} |> infer_instantiate ctxt 1289 [(("f", 0), Thm.cterm_of ctxt f), 1290 (("x", 0), cx), 1291 (("g", 0), Thm.cterm_of ctxt abs_g')]; 1292 in SOME (rl OF [Thm.transitive fx_g g_g'x]) end 1293 end 1294 | _ => NONE) 1295 end 1296 end 1297\<close> 1298 1299lemma True_implies_equals: "(True \<Longrightarrow> PROP P) \<equiv> PROP P" 1300proof 1301 assume "True \<Longrightarrow> PROP P" 1302 from this [OF TrueI] show "PROP P" . 1303next 1304 assume "PROP P" 1305 then show "PROP P" . 1306qed 1307 1308lemma implies_True_equals: "(PROP P \<Longrightarrow> True) \<equiv> Trueprop True" 1309 by standard (intro TrueI) 1310 1311lemma False_implies_equals: "(False \<Longrightarrow> P) \<equiv> Trueprop True" 1312 by standard simp_all 1313 1314(* This is not made a simp rule because it does not improve any proofs 1315 but slows some AFP entries down by 5% (cpu time). May 2015 *) 1316lemma implies_False_swap: 1317 "NO_MATCH (Trueprop False) P \<Longrightarrow> 1318 (False \<Longrightarrow> PROP P \<Longrightarrow> PROP Q) \<equiv> (PROP P \<Longrightarrow> False \<Longrightarrow> PROP Q)" 1319 by (rule swap_prems_eq) 1320 1321lemma ex_simps: 1322 "\<And>P Q. (\<exists>x. P x \<and> Q) = ((\<exists>x. P x) \<and> Q)" 1323 "\<And>P Q. (\<exists>x. P \<and> Q x) = (P \<and> (\<exists>x. Q x))" 1324 "\<And>P Q. (\<exists>x. P x \<or> Q) = ((\<exists>x. P x) \<or> Q)" 1325 "\<And>P Q. (\<exists>x. P \<or> Q x) = (P \<or> (\<exists>x. Q x))" 1326 "\<And>P Q. (\<exists>x. P x \<longrightarrow> Q) = ((\<forall>x. P x) \<longrightarrow> Q)" 1327 "\<And>P Q. (\<exists>x. P \<longrightarrow> Q x) = (P \<longrightarrow> (\<exists>x. Q x))" 1328 \<comment> \<open>Miniscoping: pushing in existential quantifiers.\<close> 1329 by (iprover | blast)+ 1330 1331lemma all_simps: 1332 "\<And>P Q. (\<forall>x. P x \<and> Q) = ((\<forall>x. P x) \<and> Q)" 1333 "\<And>P Q. (\<forall>x. P \<and> Q x) = (P \<and> (\<forall>x. Q x))" 1334 "\<And>P Q. (\<forall>x. P x \<or> Q) = ((\<forall>x. P x) \<or> Q)" 1335 "\<And>P Q. (\<forall>x. P \<or> Q x) = (P \<or> (\<forall>x. Q x))" 1336 "\<And>P Q. (\<forall>x. P x \<longrightarrow> Q) = ((\<exists>x. P x) \<longrightarrow> Q)" 1337 "\<And>P Q. (\<forall>x. P \<longrightarrow> Q x) = (P \<longrightarrow> (\<forall>x. Q x))" 1338 \<comment> \<open>Miniscoping: pushing in universal quantifiers.\<close> 1339 by (iprover | blast)+ 1340 1341lemmas [simp] = 1342 triv_forall_equality \<comment> \<open>prunes params\<close> 1343 True_implies_equals implies_True_equals \<comment> \<open>prune \<open>True\<close> in asms\<close> 1344 False_implies_equals \<comment> \<open>prune \<open>False\<close> in asms\<close> 1345 if_True 1346 if_False 1347 if_cancel 1348 if_eq_cancel 1349 imp_disjL \<comment> \<open>In general it seems wrong to add distributive laws by default: they 1350 might cause exponential blow-up. But \<open>imp_disjL\<close> has been in for a while 1351 and cannot be removed without affecting existing proofs. Moreover, 1352 rewriting by \<open>(P \<or> Q \<longrightarrow> R) = ((P \<longrightarrow> R) \<and> (Q \<longrightarrow> R))\<close> might be justified on the 1353 grounds that it allows simplification of \<open>R\<close> in the two cases.\<close> 1354 conj_assoc 1355 disj_assoc 1356 de_Morgan_conj 1357 de_Morgan_disj 1358 imp_disj1 1359 imp_disj2 1360 not_imp 1361 disj_not1 1362 not_all 1363 not_ex 1364 cases_simp 1365 the_eq_trivial 1366 the_sym_eq_trivial 1367 ex_simps 1368 all_simps 1369 simp_thms 1370 1371lemmas [cong] = imp_cong simp_implies_cong 1372lemmas [split] = if_split 1373 1374ML \<open>val HOL_ss = simpset_of \<^context>\<close> 1375 1376text \<open>Simplifies \<open>x\<close> assuming \<open>c\<close> and \<open>y\<close> assuming \<open>\<not> c\<close>.\<close> 1377lemma if_cong: 1378 assumes "b = c" 1379 and "c \<Longrightarrow> x = u" 1380 and "\<not> c \<Longrightarrow> y = v" 1381 shows "(if b then x else y) = (if c then u else v)" 1382 using assms by simp 1383 1384text \<open>Prevents simplification of \<open>x\<close> and \<open>y\<close>: 1385 faster and allows the execution of functional programs.\<close> 1386lemma if_weak_cong [cong]: 1387 assumes "b = c" 1388 shows "(if b then x else y) = (if c then x else y)" 1389 using assms by (rule arg_cong) 1390 1391text \<open>Prevents simplification of t: much faster\<close> 1392lemma let_weak_cong: 1393 assumes "a = b" 1394 shows "(let x = a in t x) = (let x = b in t x)" 1395 using assms by (rule arg_cong) 1396 1397text \<open>To tidy up the result of a simproc. Only the RHS will be simplified.\<close> 1398lemma eq_cong2: 1399 assumes "u = u'" 1400 shows "(t \<equiv> u) \<equiv> (t \<equiv> u')" 1401 using assms by simp 1402 1403lemma if_distrib: "f (if c then x else y) = (if c then f x else f y)" 1404 by simp 1405 1406lemma if_distribR: "(if b then f else g) x = (if b then f x else g x)" 1407 by simp 1408 1409lemma all_if_distrib: "(\<forall>x. if x = a then P x else Q x) \<longleftrightarrow> P a \<and> (\<forall>x. x\<noteq>a \<longrightarrow> Q x)" 1410 by auto 1411 1412lemma ex_if_distrib: "(\<exists>x. if x = a then P x else Q x) \<longleftrightarrow> P a \<or> (\<exists>x. x\<noteq>a \<and> Q x)" 1413 by auto 1414 1415lemma if_if_eq_conj: "(if P then if Q then x else y else y) = (if P \<and> Q then x else y)" 1416 by simp 1417 1418text \<open>As a simplification rule, it replaces all function equalities by 1419 first-order equalities.\<close> 1420lemma fun_eq_iff: "f = g \<longleftrightarrow> (\<forall>x. f x = g x)" 1421 by auto 1422 1423 1424subsubsection \<open>Generic cases and induction\<close> 1425 1426text \<open>Rule projections:\<close> 1427ML \<open> 1428structure Project_Rule = Project_Rule 1429( 1430 val conjunct1 = @{thm conjunct1} 1431 val conjunct2 = @{thm conjunct2} 1432 val mp = @{thm mp} 1433); 1434\<close> 1435 1436context 1437begin 1438 1439qualified definition "induct_forall P \<equiv> \<forall>x. P x" 1440qualified definition "induct_implies A B \<equiv> A \<longrightarrow> B" 1441qualified definition "induct_equal x y \<equiv> x = y" 1442qualified definition "induct_conj A B \<equiv> A \<and> B" 1443qualified definition "induct_true \<equiv> True" 1444qualified definition "induct_false \<equiv> False" 1445 1446lemma induct_forall_eq: "(\<And>x. P x) \<equiv> Trueprop (induct_forall (\<lambda>x. P x))" 1447 by (unfold atomize_all induct_forall_def) 1448 1449lemma induct_implies_eq: "(A \<Longrightarrow> B) \<equiv> Trueprop (induct_implies A B)" 1450 by (unfold atomize_imp induct_implies_def) 1451 1452lemma induct_equal_eq: "(x \<equiv> y) \<equiv> Trueprop (induct_equal x y)" 1453 by (unfold atomize_eq induct_equal_def) 1454 1455lemma induct_conj_eq: "(A &&& B) \<equiv> Trueprop (induct_conj A B)" 1456 by (unfold atomize_conj induct_conj_def) 1457 1458lemmas induct_atomize' = induct_forall_eq induct_implies_eq induct_conj_eq 1459lemmas induct_atomize = induct_atomize' induct_equal_eq 1460lemmas induct_rulify' [symmetric] = induct_atomize' 1461lemmas induct_rulify [symmetric] = induct_atomize 1462lemmas induct_rulify_fallback = 1463 induct_forall_def induct_implies_def induct_equal_def induct_conj_def 1464 induct_true_def induct_false_def 1465 1466lemma induct_forall_conj: "induct_forall (\<lambda>x. induct_conj (A x) (B x)) = 1467 induct_conj (induct_forall A) (induct_forall B)" 1468 by (unfold induct_forall_def induct_conj_def) iprover 1469 1470lemma induct_implies_conj: "induct_implies C (induct_conj A B) = 1471 induct_conj (induct_implies C A) (induct_implies C B)" 1472 by (unfold induct_implies_def induct_conj_def) iprover 1473 1474lemma induct_conj_curry: "(induct_conj A B \<Longrightarrow> PROP C) \<equiv> (A \<Longrightarrow> B \<Longrightarrow> PROP C)" 1475proof 1476 assume r: "induct_conj A B \<Longrightarrow> PROP C" 1477 assume ab: A B 1478 show "PROP C" by (rule r) (simp add: induct_conj_def ab) 1479next 1480 assume r: "A \<Longrightarrow> B \<Longrightarrow> PROP C" 1481 assume ab: "induct_conj A B" 1482 show "PROP C" by (rule r) (simp_all add: ab [unfolded induct_conj_def]) 1483qed 1484 1485lemmas induct_conj = induct_forall_conj induct_implies_conj induct_conj_curry 1486 1487lemma induct_trueI: "induct_true" 1488 by (simp add: induct_true_def) 1489 1490text \<open>Method setup.\<close> 1491 1492ML_file \<open>~~/src/Tools/induct.ML\<close> 1493ML \<open> 1494structure Induct = Induct 1495( 1496 val cases_default = @{thm case_split} 1497 val atomize = @{thms induct_atomize} 1498 val rulify = @{thms induct_rulify'} 1499 val rulify_fallback = @{thms induct_rulify_fallback} 1500 val equal_def = @{thm induct_equal_def} 1501 fun dest_def (Const (\<^const_name>\<open>induct_equal\<close>, _) $ t $ u) = SOME (t, u) 1502 | dest_def _ = NONE 1503 fun trivial_tac ctxt = match_tac ctxt @{thms induct_trueI} 1504) 1505\<close> 1506 1507ML_file \<open>~~/src/Tools/induction.ML\<close> 1508 1509declaration \<open> 1510 fn _ => Induct.map_simpset (fn ss => ss 1511 addsimprocs 1512 [Simplifier.make_simproc \<^context> "swap_induct_false" 1513 {lhss = [\<^term>\<open>induct_false \<Longrightarrow> PROP P \<Longrightarrow> PROP Q\<close>], 1514 proc = fn _ => fn _ => fn ct => 1515 (case Thm.term_of ct of 1516 _ $ (P as _ $ \<^const>\<open>induct_false\<close>) $ (_ $ Q $ _) => 1517 if P <> Q then SOME Drule.swap_prems_eq else NONE 1518 | _ => NONE)}, 1519 Simplifier.make_simproc \<^context> "induct_equal_conj_curry" 1520 {lhss = [\<^term>\<open>induct_conj P Q \<Longrightarrow> PROP R\<close>], 1521 proc = fn _ => fn _ => fn ct => 1522 (case Thm.term_of ct of 1523 _ $ (_ $ P) $ _ => 1524 let 1525 fun is_conj (\<^const>\<open>induct_conj\<close> $ P $ Q) = 1526 is_conj P andalso is_conj Q 1527 | is_conj (Const (\<^const_name>\<open>induct_equal\<close>, _) $ _ $ _) = true 1528 | is_conj \<^const>\<open>induct_true\<close> = true 1529 | is_conj \<^const>\<open>induct_false\<close> = true 1530 | is_conj _ = false 1531 in if is_conj P then SOME @{thm induct_conj_curry} else NONE end 1532 | _ => NONE)}] 1533 |> Simplifier.set_mksimps (fn ctxt => 1534 Simpdata.mksimps Simpdata.mksimps_pairs ctxt #> 1535 map (rewrite_rule ctxt (map Thm.symmetric @{thms induct_rulify_fallback})))) 1536\<close> 1537 1538text \<open>Pre-simplification of induction and cases rules\<close> 1539 1540lemma [induct_simp]: "(\<And>x. induct_equal x t \<Longrightarrow> PROP P x) \<equiv> PROP P t" 1541 unfolding induct_equal_def 1542proof 1543 assume r: "\<And>x. x = t \<Longrightarrow> PROP P x" 1544 show "PROP P t" by (rule r [OF refl]) 1545next 1546 fix x 1547 assume "PROP P t" "x = t" 1548 then show "PROP P x" by simp 1549qed 1550 1551lemma [induct_simp]: "(\<And>x. induct_equal t x \<Longrightarrow> PROP P x) \<equiv> PROP P t" 1552 unfolding induct_equal_def 1553proof 1554 assume r: "\<And>x. t = x \<Longrightarrow> PROP P x" 1555 show "PROP P t" by (rule r [OF refl]) 1556next 1557 fix x 1558 assume "PROP P t" "t = x" 1559 then show "PROP P x" by simp 1560qed 1561 1562lemma [induct_simp]: "(induct_false \<Longrightarrow> P) \<equiv> Trueprop induct_true" 1563 unfolding induct_false_def induct_true_def 1564 by (iprover intro: equal_intr_rule) 1565 1566lemma [induct_simp]: "(induct_true \<Longrightarrow> PROP P) \<equiv> PROP P" 1567 unfolding induct_true_def 1568proof 1569 assume "True \<Longrightarrow> PROP P" 1570 then show "PROP P" using TrueI . 1571next 1572 assume "PROP P" 1573 then show "PROP P" . 1574qed 1575 1576lemma [induct_simp]: "(PROP P \<Longrightarrow> induct_true) \<equiv> Trueprop induct_true" 1577 unfolding induct_true_def 1578 by (iprover intro: equal_intr_rule) 1579 1580lemma [induct_simp]: "(\<And>x::'a::{}. induct_true) \<equiv> Trueprop induct_true" 1581 unfolding induct_true_def 1582 by (iprover intro: equal_intr_rule) 1583 1584lemma [induct_simp]: "induct_implies induct_true P \<equiv> P" 1585 by (simp add: induct_implies_def induct_true_def) 1586 1587lemma [induct_simp]: "x = x \<longleftrightarrow> True" 1588 by (rule simp_thms) 1589 1590end 1591 1592ML_file \<open>~~/src/Tools/induct_tacs.ML\<close> 1593 1594 1595subsubsection \<open>Coherent logic\<close> 1596 1597ML_file \<open>~~/src/Tools/coherent.ML\<close> 1598ML \<open> 1599structure Coherent = Coherent 1600( 1601 val atomize_elimL = @{thm atomize_elimL}; 1602 val atomize_exL = @{thm atomize_exL}; 1603 val atomize_conjL = @{thm atomize_conjL}; 1604 val atomize_disjL = @{thm atomize_disjL}; 1605 val operator_names = [\<^const_name>\<open>HOL.disj\<close>, \<^const_name>\<open>HOL.conj\<close>, \<^const_name>\<open>Ex\<close>]; 1606); 1607\<close> 1608 1609 1610subsubsection \<open>Reorienting equalities\<close> 1611 1612ML \<open> 1613signature REORIENT_PROC = 1614sig 1615 val add : (term -> bool) -> theory -> theory 1616 val proc : morphism -> Proof.context -> cterm -> thm option 1617end; 1618 1619structure Reorient_Proc : REORIENT_PROC = 1620struct 1621 structure Data = Theory_Data 1622 ( 1623 type T = ((term -> bool) * stamp) list; 1624 val empty = []; 1625 val extend = I; 1626 fun merge data : T = Library.merge (eq_snd (op =)) data; 1627 ); 1628 fun add m = Data.map (cons (m, stamp ())); 1629 fun matches thy t = exists (fn (m, _) => m t) (Data.get thy); 1630 1631 val meta_reorient = @{thm eq_commute [THEN eq_reflection]}; 1632 fun proc phi ctxt ct = 1633 let 1634 val thy = Proof_Context.theory_of ctxt; 1635 in 1636 case Thm.term_of ct of 1637 (_ $ t $ u) => if matches thy u then NONE else SOME meta_reorient 1638 | _ => NONE 1639 end; 1640end; 1641\<close> 1642 1643 1644subsection \<open>Other simple lemmas and lemma duplicates\<close> 1645 1646lemma all_cong1: "(\<And>x. P x = P' x) \<Longrightarrow> (\<forall>x. P x) = (\<forall>x. P' x)" 1647 by auto 1648 1649lemma ex_cong1: "(\<And>x. P x = P' x) \<Longrightarrow> (\<exists>x. P x) = (\<exists>x. P' x)" 1650 by auto 1651 1652lemma all_cong: "(\<And>x. Q x \<Longrightarrow> P x = P' x) \<Longrightarrow> (\<forall>x. Q x \<longrightarrow> P x) = (\<forall>x. Q x \<longrightarrow> P' x)" 1653 by auto 1654 1655lemma ex_cong: "(\<And>x. Q x \<Longrightarrow> P x = P' x) \<Longrightarrow> (\<exists>x. Q x \<and> P x) = (\<exists>x. Q x \<and> P' x)" 1656 by auto 1657 1658lemma ex1_eq [iff]: "\<exists>!x. x = t" "\<exists>!x. t = x" 1659 by blast+ 1660 1661lemma choice_eq: "(\<forall>x. \<exists>!y. P x y) = (\<exists>!f. \<forall>x. P x (f x))" 1662 apply (rule iffI) 1663 apply (rule_tac a = "\<lambda>x. THE y. P x y" in ex1I) 1664 apply (fast dest!: theI') 1665 apply (fast intro: the1_equality [symmetric]) 1666 apply (erule ex1E) 1667 apply (rule allI) 1668 apply (rule ex1I) 1669 apply (erule spec) 1670 apply (erule_tac x = "\<lambda>z. if z = x then y else f z" in allE) 1671 apply (erule impE) 1672 apply (rule allI) 1673 apply (case_tac "xa = x") 1674 apply (drule_tac [3] x = x in fun_cong) 1675 apply simp_all 1676 done 1677 1678lemmas eq_sym_conv = eq_commute 1679 1680lemma nnf_simps: 1681 "(\<not> (P \<and> Q)) = (\<not> P \<or> \<not> Q)" 1682 "(\<not> (P \<or> Q)) = (\<not> P \<and> \<not> Q)" 1683 "(P \<longrightarrow> Q) = (\<not> P \<or> Q)" 1684 "(P = Q) = ((P \<and> Q) \<or> (\<not> P \<and> \<not> Q))" 1685 "(\<not> (P = Q)) = ((P \<and> \<not> Q) \<or> (\<not> P \<and> Q))" 1686 "(\<not> \<not> P) = P" 1687 by blast+ 1688 1689 1690subsection \<open>Basic ML bindings\<close> 1691 1692ML \<open> 1693val FalseE = @{thm FalseE} 1694val Let_def = @{thm Let_def} 1695val TrueI = @{thm TrueI} 1696val allE = @{thm allE} 1697val allI = @{thm allI} 1698val all_dupE = @{thm all_dupE} 1699val arg_cong = @{thm arg_cong} 1700val box_equals = @{thm box_equals} 1701val ccontr = @{thm ccontr} 1702val classical = @{thm classical} 1703val conjE = @{thm conjE} 1704val conjI = @{thm conjI} 1705val conjunct1 = @{thm conjunct1} 1706val conjunct2 = @{thm conjunct2} 1707val disjCI = @{thm disjCI} 1708val disjE = @{thm disjE} 1709val disjI1 = @{thm disjI1} 1710val disjI2 = @{thm disjI2} 1711val eq_reflection = @{thm eq_reflection} 1712val ex1E = @{thm ex1E} 1713val ex1I = @{thm ex1I} 1714val ex1_implies_ex = @{thm ex1_implies_ex} 1715val exE = @{thm exE} 1716val exI = @{thm exI} 1717val excluded_middle = @{thm excluded_middle} 1718val ext = @{thm ext} 1719val fun_cong = @{thm fun_cong} 1720val iffD1 = @{thm iffD1} 1721val iffD2 = @{thm iffD2} 1722val iffI = @{thm iffI} 1723val impE = @{thm impE} 1724val impI = @{thm impI} 1725val meta_eq_to_obj_eq = @{thm meta_eq_to_obj_eq} 1726val mp = @{thm mp} 1727val notE = @{thm notE} 1728val notI = @{thm notI} 1729val not_all = @{thm not_all} 1730val not_ex = @{thm not_ex} 1731val not_iff = @{thm not_iff} 1732val not_not = @{thm not_not} 1733val not_sym = @{thm not_sym} 1734val refl = @{thm refl} 1735val rev_mp = @{thm rev_mp} 1736val spec = @{thm spec} 1737val ssubst = @{thm ssubst} 1738val subst = @{thm subst} 1739val sym = @{thm sym} 1740val trans = @{thm trans} 1741\<close> 1742 1743locale cnf 1744begin 1745 1746lemma clause2raw_notE: "\<lbrakk>P; \<not>P\<rbrakk> \<Longrightarrow> False" by auto 1747lemma clause2raw_not_disj: "\<lbrakk>\<not> P; \<not> Q\<rbrakk> \<Longrightarrow> \<not> (P \<or> Q)" by auto 1748lemma clause2raw_not_not: "P \<Longrightarrow> \<not>\<not> P" by auto 1749 1750lemma iff_refl: "(P::bool) = P" by auto 1751lemma iff_trans: "[| (P::bool) = Q; Q = R |] ==> P = R" by auto 1752lemma conj_cong: "[| P = P'; Q = Q' |] ==> (P \<and> Q) = (P' \<and> Q')" by auto 1753lemma disj_cong: "[| P = P'; Q = Q' |] ==> (P \<or> Q) = (P' \<or> Q')" by auto 1754 1755lemma make_nnf_imp: "[| (\<not>P) = P'; Q = Q' |] ==> (P \<longrightarrow> Q) = (P' \<or> Q')" by auto 1756lemma make_nnf_iff: "[| P = P'; (\<not>P) = NP; Q = Q'; (\<not>Q) = NQ |] ==> (P = Q) = ((P' \<or> NQ) \<and> (NP \<or> Q'))" by auto 1757lemma make_nnf_not_false: "(\<not>False) = True" by auto 1758lemma make_nnf_not_true: "(\<not>True) = False" by auto 1759lemma make_nnf_not_conj: "[| (\<not>P) = P'; (\<not>Q) = Q' |] ==> (\<not>(P \<and> Q)) = (P' \<or> Q')" by auto 1760lemma make_nnf_not_disj: "[| (\<not>P) = P'; (\<not>Q) = Q' |] ==> (\<not>(P \<or> Q)) = (P' \<and> Q')" by auto 1761lemma make_nnf_not_imp: "[| P = P'; (\<not>Q) = Q' |] ==> (\<not>(P \<longrightarrow> Q)) = (P' \<and> Q')" by auto 1762lemma make_nnf_not_iff: "[| P = P'; (\<not>P) = NP; Q = Q'; (\<not>Q) = NQ |] ==> (\<not>(P = Q)) = ((P' \<or> Q') \<and> (NP \<or> NQ))" by auto 1763lemma make_nnf_not_not: "P = P' ==> (\<not>\<not>P) = P'" by auto 1764 1765lemma simp_TF_conj_True_l: "[| P = True; Q = Q' |] ==> (P \<and> Q) = Q'" by auto 1766lemma simp_TF_conj_True_r: "[| P = P'; Q = True |] ==> (P \<and> Q) = P'" by auto 1767lemma simp_TF_conj_False_l: "P = False ==> (P \<and> Q) = False" by auto 1768lemma simp_TF_conj_False_r: "Q = False ==> (P \<and> Q) = False" by auto 1769lemma simp_TF_disj_True_l: "P = True ==> (P \<or> Q) = True" by auto 1770lemma simp_TF_disj_True_r: "Q = True ==> (P \<or> Q) = True" by auto 1771lemma simp_TF_disj_False_l: "[| P = False; Q = Q' |] ==> (P \<or> Q) = Q'" by auto 1772lemma simp_TF_disj_False_r: "[| P = P'; Q = False |] ==> (P \<or> Q) = P'" by auto 1773 1774lemma make_cnf_disj_conj_l: "[| (P \<or> R) = PR; (Q \<or> R) = QR |] ==> ((P \<and> Q) \<or> R) = (PR \<and> QR)" by auto 1775lemma make_cnf_disj_conj_r: "[| (P \<or> Q) = PQ; (P \<or> R) = PR |] ==> (P \<or> (Q \<and> R)) = (PQ \<and> PR)" by auto 1776 1777lemma make_cnfx_disj_ex_l: "((\<exists>(x::bool). P x) \<or> Q) = (\<exists>x. P x \<or> Q)" by auto 1778lemma make_cnfx_disj_ex_r: "(P \<or> (\<exists>(x::bool). Q x)) = (\<exists>x. P \<or> Q x)" by auto 1779lemma make_cnfx_newlit: "(P \<or> Q) = (\<exists>x. (P \<or> x) \<and> (Q \<or> \<not>x))" by auto 1780lemma make_cnfx_ex_cong: "(\<forall>(x::bool). P x = Q x) \<Longrightarrow> (\<exists>x. P x) = (\<exists>x. Q x)" by auto 1781 1782lemma weakening_thm: "[| P; Q |] ==> Q" by auto 1783 1784lemma cnftac_eq_imp: "[| P = Q; P |] ==> Q" by auto 1785 1786end 1787 1788ML_file \<open>Tools/cnf.ML\<close> 1789 1790 1791section \<open>\<open>NO_MATCH\<close> simproc\<close> 1792 1793text \<open> 1794 The simplification procedure can be used to avoid simplification of terms 1795 of a certain form. 1796\<close> 1797 1798definition NO_MATCH :: "'a \<Rightarrow> 'b \<Rightarrow> bool" 1799 where "NO_MATCH pat val \<equiv> True" 1800 1801lemma NO_MATCH_cong[cong]: "NO_MATCH pat val = NO_MATCH pat val" 1802 by (rule refl) 1803 1804declare [[coercion_args NO_MATCH - -]] 1805 1806simproc_setup NO_MATCH ("NO_MATCH pat val") = \<open>fn _ => fn ctxt => fn ct => 1807 let 1808 val thy = Proof_Context.theory_of ctxt 1809 val dest_binop = Term.dest_comb #> apfst (Term.dest_comb #> snd) 1810 val m = Pattern.matches thy (dest_binop (Thm.term_of ct)) 1811 in if m then NONE else SOME @{thm NO_MATCH_def} end 1812\<close> 1813 1814text \<open> 1815 This setup ensures that a rewrite rule of the form \<^term>\<open>NO_MATCH pat val \<Longrightarrow> t\<close> 1816 is only applied, if the pattern \<open>pat\<close> does not match the value \<open>val\<close>. 1817\<close> 1818 1819 1820text\<open> 1821 Tagging a premise of a simp rule with ASSUMPTION forces the simplifier 1822 not to simplify the argument and to solve it by an assumption. 1823\<close> 1824 1825definition ASSUMPTION :: "bool \<Rightarrow> bool" 1826 where "ASSUMPTION A \<equiv> A" 1827 1828lemma ASSUMPTION_cong[cong]: "ASSUMPTION A = ASSUMPTION A" 1829 by (rule refl) 1830 1831lemma ASSUMPTION_I: "A \<Longrightarrow> ASSUMPTION A" 1832 by (simp add: ASSUMPTION_def) 1833 1834lemma ASSUMPTION_D: "ASSUMPTION A \<Longrightarrow> A" 1835 by (simp add: ASSUMPTION_def) 1836 1837setup \<open> 1838let 1839 val asm_sol = mk_solver "ASSUMPTION" (fn ctxt => 1840 resolve_tac ctxt [@{thm ASSUMPTION_I}] THEN' 1841 resolve_tac ctxt (Simplifier.prems_of ctxt)) 1842in 1843 map_theory_simpset (fn ctxt => Simplifier.addSolver (ctxt,asm_sol)) 1844end 1845\<close> 1846 1847 1848subsection \<open>Code generator setup\<close> 1849 1850subsubsection \<open>Generic code generator preprocessor setup\<close> 1851 1852lemma conj_left_cong: "P \<longleftrightarrow> Q \<Longrightarrow> P \<and> R \<longleftrightarrow> Q \<and> R" 1853 by (fact arg_cong) 1854 1855lemma disj_left_cong: "P \<longleftrightarrow> Q \<Longrightarrow> P \<or> R \<longleftrightarrow> Q \<or> R" 1856 by (fact arg_cong) 1857 1858setup \<open> 1859 Code_Preproc.map_pre (put_simpset HOL_basic_ss) #> 1860 Code_Preproc.map_post (put_simpset HOL_basic_ss) #> 1861 Code_Simp.map_ss (put_simpset HOL_basic_ss #> 1862 Simplifier.add_cong @{thm conj_left_cong} #> 1863 Simplifier.add_cong @{thm disj_left_cong}) 1864\<close> 1865 1866 1867subsubsection \<open>Equality\<close> 1868 1869class equal = 1870 fixes equal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" 1871 assumes equal_eq: "equal x y \<longleftrightarrow> x = y" 1872begin 1873 1874lemma equal: "equal = (=)" 1875 by (rule ext equal_eq)+ 1876 1877lemma equal_refl: "equal x x \<longleftrightarrow> True" 1878 unfolding equal by rule+ 1879 1880lemma eq_equal: "(=) \<equiv> equal" 1881 by (rule eq_reflection) (rule ext, rule ext, rule sym, rule equal_eq) 1882 1883end 1884 1885declare eq_equal [symmetric, code_post] 1886declare eq_equal [code] 1887 1888setup \<open> 1889 Code_Preproc.map_pre (fn ctxt => 1890 ctxt addsimprocs 1891 [Simplifier.make_simproc \<^context> "equal" 1892 {lhss = [\<^term>\<open>HOL.eq\<close>], 1893 proc = fn _ => fn _ => fn ct => 1894 (case Thm.term_of ct of 1895 Const (_, Type (\<^type_name>\<open>fun\<close>, [Type _, _])) => SOME @{thm eq_equal} 1896 | _ => NONE)}]) 1897\<close> 1898 1899 1900subsubsection \<open>Generic code generator foundation\<close> 1901 1902text \<open>Datatype \<^typ>\<open>bool\<close>\<close> 1903 1904code_datatype True False 1905 1906lemma [code]: 1907 shows "False \<and> P \<longleftrightarrow> False" 1908 and "True \<and> P \<longleftrightarrow> P" 1909 and "P \<and> False \<longleftrightarrow> False" 1910 and "P \<and> True \<longleftrightarrow> P" 1911 by simp_all 1912 1913lemma [code]: 1914 shows "False \<or> P \<longleftrightarrow> P" 1915 and "True \<or> P \<longleftrightarrow> True" 1916 and "P \<or> False \<longleftrightarrow> P" 1917 and "P \<or> True \<longleftrightarrow> True" 1918 by simp_all 1919 1920lemma [code]: 1921 shows "(False \<longrightarrow> P) \<longleftrightarrow> True" 1922 and "(True \<longrightarrow> P) \<longleftrightarrow> P" 1923 and "(P \<longrightarrow> False) \<longleftrightarrow> \<not> P" 1924 and "(P \<longrightarrow> True) \<longleftrightarrow> True" 1925 by simp_all 1926 1927text \<open>More about \<^typ>\<open>prop\<close>\<close> 1928 1929lemma [code nbe]: 1930 shows "(True \<Longrightarrow> PROP Q) \<equiv> PROP Q" 1931 and "(PROP Q \<Longrightarrow> True) \<equiv> Trueprop True" 1932 and "(P \<Longrightarrow> R) \<equiv> Trueprop (P \<longrightarrow> R)" 1933 by (auto intro!: equal_intr_rule) 1934 1935lemma Trueprop_code [code]: "Trueprop True \<equiv> Code_Generator.holds" 1936 by (auto intro!: equal_intr_rule holds) 1937 1938declare Trueprop_code [symmetric, code_post] 1939 1940text \<open>Equality\<close> 1941 1942declare simp_thms(6) [code nbe] 1943 1944instantiation itself :: (type) equal 1945begin 1946 1947definition equal_itself :: "'a itself \<Rightarrow> 'a itself \<Rightarrow> bool" 1948 where "equal_itself x y \<longleftrightarrow> x = y" 1949 1950instance 1951 by standard (fact equal_itself_def) 1952 1953end 1954 1955lemma equal_itself_code [code]: "equal TYPE('a) TYPE('a) \<longleftrightarrow> True" 1956 by (simp add: equal) 1957 1958setup \<open>Sign.add_const_constraint (\<^const_name>\<open>equal\<close>, SOME \<^typ>\<open>'a::type \<Rightarrow> 'a \<Rightarrow> bool\<close>)\<close> 1959 1960lemma equal_alias_cert: "OFCLASS('a, equal_class) \<equiv> (((=) :: 'a \<Rightarrow> 'a \<Rightarrow> bool) \<equiv> equal)" 1961 (is "?ofclass \<equiv> ?equal") 1962proof 1963 assume "PROP ?ofclass" 1964 show "PROP ?equal" 1965 by (tactic \<open>ALLGOALS (resolve_tac \<^context> [Thm.unconstrainT @{thm eq_equal}])\<close>) 1966 (fact \<open>PROP ?ofclass\<close>) 1967next 1968 assume "PROP ?equal" 1969 show "PROP ?ofclass" proof 1970 qed (simp add: \<open>PROP ?equal\<close>) 1971qed 1972 1973setup \<open>Sign.add_const_constraint (\<^const_name>\<open>equal\<close>, SOME \<^typ>\<open>'a::equal \<Rightarrow> 'a \<Rightarrow> bool\<close>)\<close> 1974 1975setup \<open>Nbe.add_const_alias @{thm equal_alias_cert}\<close> 1976 1977text \<open>Cases\<close> 1978 1979lemma Let_case_cert: 1980 assumes "CASE \<equiv> (\<lambda>x. Let x f)" 1981 shows "CASE x \<equiv> f x" 1982 using assms by simp_all 1983 1984setup \<open> 1985 Code.declare_case_global @{thm Let_case_cert} #> 1986 Code.declare_undefined_global \<^const_name>\<open>undefined\<close> 1987\<close> 1988 1989declare [[code abort: undefined]] 1990 1991 1992subsubsection \<open>Generic code generator target languages\<close> 1993 1994text \<open>type \<^typ>\<open>bool\<close>\<close> 1995 1996code_printing 1997 type_constructor bool \<rightharpoonup> 1998 (SML) "bool" and (OCaml) "bool" and (Haskell) "Bool" and (Scala) "Boolean" 1999| constant True \<rightharpoonup> 2000 (SML) "true" and (OCaml) "true" and (Haskell) "True" and (Scala) "true" 2001| constant False \<rightharpoonup> 2002 (SML) "false" and (OCaml) "false" and (Haskell) "False" and (Scala) "false" 2003 2004code_reserved SML 2005 bool true false 2006 2007code_reserved OCaml 2008 bool 2009 2010code_reserved Scala 2011 Boolean 2012 2013code_printing 2014 constant Not \<rightharpoonup> 2015 (SML) "not" and (OCaml) "not" and (Haskell) "not" and (Scala) "'! _" 2016| constant HOL.conj \<rightharpoonup> 2017 (SML) infixl 1 "andalso" and (OCaml) infixl 3 "&&" and (Haskell) infixr 3 "&&" and (Scala) infixl 3 "&&" 2018| constant HOL.disj \<rightharpoonup> 2019 (SML) infixl 0 "orelse" and (OCaml) infixl 2 "||" and (Haskell) infixl 2 "||" and (Scala) infixl 1 "||" 2020| constant HOL.implies \<rightharpoonup> 2021 (SML) "!(if (_)/ then (_)/ else true)" 2022 and (OCaml) "!(if (_)/ then (_)/ else true)" 2023 and (Haskell) "!(if (_)/ then (_)/ else True)" 2024 and (Scala) "!(if ((_))/ (_)/ else true)" 2025| constant If \<rightharpoonup> 2026 (SML) "!(if (_)/ then (_)/ else (_))" 2027 and (OCaml) "!(if (_)/ then (_)/ else (_))" 2028 and (Haskell) "!(if (_)/ then (_)/ else (_))" 2029 and (Scala) "!(if ((_))/ (_)/ else (_))" 2030 2031code_reserved SML 2032 not 2033 2034code_reserved OCaml 2035 not 2036 2037code_identifier 2038 code_module Pure \<rightharpoonup> 2039 (SML) HOL and (OCaml) HOL and (Haskell) HOL and (Scala) HOL 2040 2041text \<open>Using built-in Haskell equality.\<close> 2042code_printing 2043 type_class equal \<rightharpoonup> (Haskell) "Eq" 2044| constant HOL.equal \<rightharpoonup> (Haskell) infix 4 "==" 2045| constant HOL.eq \<rightharpoonup> (Haskell) infix 4 "==" 2046 2047text \<open>\<open>undefined\<close>\<close> 2048code_printing 2049 constant undefined \<rightharpoonup> 2050 (SML) "!(raise/ Fail/ \"undefined\")" 2051 and (OCaml) "failwith/ \"undefined\"" 2052 and (Haskell) "error/ \"undefined\"" 2053 and (Scala) "!sys.error(\"undefined\")" 2054 2055 2056subsubsection \<open>Evaluation and normalization by evaluation\<close> 2057 2058method_setup eval = \<open> 2059 let 2060 fun eval_tac ctxt = 2061 let val conv = Code_Runtime.dynamic_holds_conv ctxt 2062 in 2063 CONVERSION (Conv.params_conv ~1 (K (Conv.concl_conv ~1 conv)) ctxt) THEN' 2064 resolve_tac ctxt [TrueI] 2065 end 2066 in 2067 Scan.succeed (SIMPLE_METHOD' o eval_tac) 2068 end 2069\<close> "solve goal by evaluation" 2070 2071method_setup normalization = \<open> 2072 Scan.succeed (fn ctxt => 2073 SIMPLE_METHOD' 2074 (CHANGED_PROP o 2075 (CONVERSION (Nbe.dynamic_conv ctxt) 2076 THEN_ALL_NEW (TRY o resolve_tac ctxt [TrueI])))) 2077\<close> "solve goal by normalization" 2078 2079 2080subsection \<open>Counterexample Search Units\<close> 2081 2082subsubsection \<open>Quickcheck\<close> 2083 2084quickcheck_params [size = 5, iterations = 50] 2085 2086 2087subsubsection \<open>Nitpick setup\<close> 2088 2089named_theorems nitpick_unfold "alternative definitions of constants as needed by Nitpick" 2090 and nitpick_simp "equational specification of constants as needed by Nitpick" 2091 and nitpick_psimp "partial equational specification of constants as needed by Nitpick" 2092 and nitpick_choice_spec "choice specification of constants as needed by Nitpick" 2093 2094declare if_bool_eq_conj [nitpick_unfold, no_atp] 2095 and if_bool_eq_disj [no_atp] 2096 2097 2098subsection \<open>Preprocessing for the predicate compiler\<close> 2099 2100named_theorems code_pred_def "alternative definitions of constants for the Predicate Compiler" 2101 and code_pred_inline "inlining definitions for the Predicate Compiler" 2102 and code_pred_simp "simplification rules for the optimisations in the Predicate Compiler" 2103 2104 2105subsection \<open>Legacy tactics and ML bindings\<close> 2106 2107ML \<open> 2108 (* combination of (spec RS spec RS ...(j times) ... spec RS mp) *) 2109 local 2110 fun wrong_prem (Const (\<^const_name>\<open>All\<close>, _) $ Abs (_, _, t)) = wrong_prem t 2111 | wrong_prem (Bound _) = true 2112 | wrong_prem _ = false; 2113 val filter_right = filter (not o wrong_prem o HOLogic.dest_Trueprop o hd o Thm.prems_of); 2114 fun smp i = funpow i (fn m => filter_right ([spec] RL m)) [mp]; 2115 in 2116 fun smp_tac ctxt j = EVERY' [dresolve_tac ctxt (smp j), assume_tac ctxt]; 2117 end; 2118 2119 local 2120 val nnf_ss = 2121 simpset_of (put_simpset HOL_basic_ss \<^context> addsimps @{thms simp_thms nnf_simps}); 2122 in 2123 fun nnf_conv ctxt = Simplifier.rewrite (put_simpset nnf_ss ctxt); 2124 end 2125\<close> 2126 2127hide_const (open) eq equal 2128 2129end 2130