(* Title: HOL/HOL.thy Author: Tobias Nipkow, Markus Wenzel, and Larry Paulson *) section ‹The basis of Higher-Order Logic› theory HOL imports Pure Tools.Code_Generator keywords "try" "solve_direct" "quickcheck" "print_coercions" "print_claset" "print_induct_rules" :: diag and "quickcheck_params" :: thy_decl abbrevs "?<" = "∃⇩_{≤}⇩_{1}" begin ML_file ‹~~/src/Tools/misc_legacy.ML› ML_file ‹~~/src/Tools/try.ML› ML_file ‹~~/src/Tools/quickcheck.ML› ML_file ‹~~/src/Tools/solve_direct.ML› ML_file ‹~~/src/Tools/IsaPlanner/zipper.ML› ML_file ‹~~/src/Tools/IsaPlanner/isand.ML› ML_file ‹~~/src/Tools/IsaPlanner/rw_inst.ML› ML_file ‹~~/src/Provers/hypsubst.ML› ML_file ‹~~/src/Provers/splitter.ML› ML_file ‹~~/src/Provers/classical.ML› ML_file ‹~~/src/Provers/blast.ML› ML_file ‹~~/src/Provers/clasimp.ML› ML_file ‹~~/src/Tools/eqsubst.ML› ML_file ‹~~/src/Provers/quantifier1.ML› ML_file ‹~~/src/Tools/atomize_elim.ML› ML_file ‹~~/src/Tools/cong_tac.ML› ML_file ‹~~/src/Tools/intuitionistic.ML› setup ‹Intuitionistic.method_setup \<^binding>‹iprover›› ML_file ‹~~/src/Tools/project_rule.ML› ML_file ‹~~/src/Tools/subtyping.ML› ML_file ‹~~/src/Tools/case_product.ML› ML ‹Plugin_Name.declare_setup \<^binding>‹extraction›› ML ‹ Plugin_Name.declare_setup \<^binding>‹quickcheck_random›; Plugin_Name.declare_setup \<^binding>‹quickcheck_exhaustive›; Plugin_Name.declare_setup \<^binding>‹quickcheck_bounded_forall›; Plugin_Name.declare_setup \<^binding>‹quickcheck_full_exhaustive›; Plugin_Name.declare_setup \<^binding>‹quickcheck_narrowing›; › ML ‹ Plugin_Name.define_setup \<^binding>‹quickcheck› [\<^plugin>‹quickcheck_exhaustive›, \<^plugin>‹quickcheck_random›, \<^plugin>‹quickcheck_bounded_forall›, \<^plugin>‹quickcheck_full_exhaustive›, \<^plugin>‹quickcheck_narrowing›] › subsection ‹Primitive logic› text ‹ The definition of the logic is based on Mike Gordon's technical report @{cite "Gordon-TR68"} that describes the first implementation of HOL. However, there are a number of differences. In particular, we start with the definite description operator and introduce Hilbert's ‹ε› operator only much later. Moreover, axiom ‹(P ⟶ Q) ⟶ (Q ⟶ P) ⟶ (P = Q)› is derived from the other axioms. The fact that this axiom is derivable was first noticed by Bruno Barras (for Mike Gordon's line of HOL systems) and later independently by Alexander Maletzky (for Isabelle/HOL). › subsubsection ‹Core syntax› setup ‹Axclass.class_axiomatization (\<^binding>‹type›, [])› default_sort type setup ‹Object_Logic.add_base_sort \<^sort>‹type›› setup ‹Proofterm.set_preproc (Proof_Rewrite_Rules.standard_preproc [])› axiomatization where fun_arity: "OFCLASS('a ⇒ 'b, type_class)" instance "fun" :: (type, type) type by (rule fun_arity) axiomatization where itself_arity: "OFCLASS('a itself, type_class)" instance itself :: (type) type by (rule itself_arity) typedecl bool judgment Trueprop :: "bool ⇒ prop" ("(_)" 5) axiomatization implies :: "[bool, bool] ⇒ bool" (infixr "⟶" 25) and eq :: "['a, 'a] ⇒ bool" and The :: "('a ⇒ bool) ⇒ 'a" notation (input) eq (infixl "=" 50) notation (output) eq (infix "=" 50) text ‹The input syntax for ‹eq› is more permissive than the output syntax because of the large amount of material that relies on infixl.› subsubsection ‹Defined connectives and quantifiers› definition True :: bool where "True ≡ ((λx::bool. x) = (λx. x))" definition All :: "('a ⇒ bool) ⇒ bool" (binder "∀" 10) where "All P ≡ (P = (λx. True))" definition Ex :: "('a ⇒ bool) ⇒ bool" (binder "∃" 10) where "Ex P ≡ ∀Q. (∀x. P x ⟶ Q) ⟶ Q" definition False :: bool where "False ≡ (∀P. P)" definition Not :: "bool ⇒ bool" ("¬ _" [40] 40) where not_def: "¬ P ≡ P ⟶ False" definition conj :: "[bool, bool] ⇒ bool" (infixr "∧" 35) where and_def: "P ∧ Q ≡ ∀R. (P ⟶ Q ⟶ R) ⟶ R" definition disj :: "[bool, bool] ⇒ bool" (infixr "∨" 30) where or_def: "P ∨ Q ≡ ∀R. (P ⟶ R) ⟶ (Q ⟶ R) ⟶ R" definition Uniq :: "('a ⇒ bool) ⇒ bool" where "Uniq P ≡ (∀x y. P x ⟶ P y ⟶ y = x)" definition Ex1 :: "('a ⇒ bool) ⇒ bool" where "Ex1 P ≡ ∃x. P x ∧ (∀y. P y ⟶ y = x)" subsubsection ‹Additional concrete syntax› syntax (ASCII) "_Uniq" :: "pttrn ⇒ bool ⇒ bool" ("(4?< _./ _)" [0, 10] 10) syntax "_Uniq" :: "pttrn ⇒ bool ⇒ bool" ("(2∃⇩_{≤}⇩_{1}_./ _)" [0, 10] 10) translations "∃⇩_{≤}⇩_{1}x. P" ⇌ "CONST Uniq (λx. P)" print_translation ‹ [Syntax_Trans.preserve_binder_abs_tr' \<^const_syntax>‹Uniq› \<^syntax_const>‹_Uniq›] › ― ‹to avoid eta-contraction of body› syntax (ASCII) "_Ex1" :: "pttrn ⇒ bool ⇒ bool" ("(3EX! _./ _)" [0, 10] 10) syntax (input) "_Ex1" :: "pttrn ⇒ bool ⇒ bool" ("(3?! _./ _)" [0, 10] 10) syntax "_Ex1" :: "pttrn ⇒ bool ⇒ bool" ("(3∃!_./ _)" [0, 10] 10) translations "∃!x. P" ⇌ "CONST Ex1 (λx. P)" print_translation ‹ [Syntax_Trans.preserve_binder_abs_tr' \<^const_syntax>‹Ex1› \<^syntax_const>‹_Ex1›] › ― ‹to avoid eta-contraction of body› syntax "_Not_Ex" :: "idts ⇒ bool ⇒ bool" ("(3∄_./ _)" [0, 10] 10) "_Not_Ex1" :: "pttrn ⇒ bool ⇒ bool" ("(3∄!_./ _)" [0, 10] 10) translations "∄x. P" ⇌ "¬ (∃x. P)" "∄!x. P" ⇌ "¬ (∃!x. P)" abbreviation not_equal :: "['a, 'a] ⇒ bool" (infix "≠" 50) where "x ≠ y ≡ ¬ (x = y)" notation (ASCII) Not ("~ _" [40] 40) and conj (infixr "&" 35) and disj (infixr "|" 30) and implies (infixr "-->" 25) and not_equal (infix "~=" 50) abbreviation (iff) iff :: "[bool, bool] ⇒ bool" (infixr "⟷" 25) where "A ⟷ B ≡ A = B" syntax "_The" :: "[pttrn, bool] ⇒ 'a" ("(3THE _./ _)" [0, 10] 10) translations "THE x. P" ⇌ "CONST The (λx. P)" print_translation ‹ [(\<^const_syntax>‹The›, fn _ => fn [Abs abs] => let val (x, t) = Syntax_Trans.atomic_abs_tr' abs in Syntax.const \<^syntax_const>‹_The› $ x $ t end)] › ― ‹To avoid eta-contraction of body› nonterminal letbinds and letbind syntax "_bind" :: "[pttrn, 'a] ⇒ letbind" ("(2_ =/ _)" 10) "" :: "letbind ⇒ letbinds" ("_") "_binds" :: "[letbind, letbinds] ⇒ letbinds" ("_;/ _") "_Let" :: "[letbinds, 'a] ⇒ 'a" ("(let (_)/ in (_))" [0, 10] 10) nonterminal case_syn and cases_syn syntax "_case_syntax" :: "['a, cases_syn] ⇒ 'b" ("(case _ of/ _)" 10) "_case1" :: "['a, 'b] ⇒ case_syn" ("(2_ ⇒/ _)" 10) "" :: "case_syn ⇒ cases_syn" ("_") "_case2" :: "[case_syn, cases_syn] ⇒ cases_syn" ("_/ | _") syntax (ASCII) "_case1" :: "['a, 'b] ⇒ case_syn" ("(2_ =>/ _)" 10) notation (ASCII) All (binder "ALL " 10) and Ex (binder "EX " 10) notation (input) All (binder "! " 10) and Ex (binder "? " 10) subsubsection ‹Axioms and basic definitions› axiomatization where refl: "t = (t::'a)" and subst: "s = t ⟹ P s ⟹ P t" and ext: "(⋀x::'a. (f x ::'b) = g x) ⟹ (λx. f x) = (λx. g x)" ― ‹Extensionality is built into the meta-logic, and this rule expresses a related property. It is an eta-expanded version of the traditional rule, and similar to the ABS rule of HOL› and the_eq_trivial: "(THE x. x = a) = (a::'a)" axiomatization where impI: "(P ⟹ Q) ⟹ P ⟶ Q" and mp: "⟦P ⟶ Q; P⟧ ⟹ Q" and True_or_False: "(P = True) ∨ (P = False)" definition If :: "bool ⇒ 'a ⇒ 'a ⇒ 'a" ("(if (_)/ then (_)/ else (_))" [0, 0, 10] 10) where "If P x y ≡ (THE z::'a. (P = True ⟶ z = x) ∧ (P = False ⟶ z = y))" definition Let :: "'a ⇒ ('a ⇒ 'b) ⇒ 'b" where "Let s f ≡ f s" translations "_Let (_binds b bs) e" ⇌ "_Let b (_Let bs e)" "let x = a in e" ⇌ "CONST Let a (λx. e)" axiomatization undefined :: 'a class default = fixes default :: 'a subsection ‹Fundamental rules› subsubsection ‹Equality› lemma sym: "s = t ⟹ t = s" by (erule subst) (rule refl) lemma ssubst: "t = s ⟹ P s ⟹ P t" by (drule sym) (erule subst) lemma trans: "⟦r = s; s = t⟧ ⟹ r = t" by (erule subst) lemma trans_sym [Pure.elim?]: "r = s ⟹ t = s ⟹ r = t" by (rule trans [OF _ sym]) lemma meta_eq_to_obj_eq: assumes "A ≡ B" shows "A = B" unfolding assms by (rule refl) text ‹Useful with ‹erule› for proving equalities from known equalities.› (* a = b | | c = d *) lemma box_equals: "⟦a = b; a = c; b = d⟧ ⟹ c = d" by (iprover intro: sym trans) text ‹For calculational reasoning:› lemma forw_subst: "a = b ⟹ P b ⟹ P a" by (rule ssubst) lemma back_subst: "P a ⟹ a = b ⟹ P b" by (rule subst) subsubsection ‹Congruence rules for application› text ‹Similar to ‹AP_THM› in Gordon's HOL.› lemma fun_cong: "(f :: 'a ⇒ 'b) = g ⟹ f x = g x" by (iprover intro: refl elim: subst) text ‹Similar to ‹AP_TERM› in Gordon's HOL and FOL's ‹subst_context›.› lemma arg_cong: "x = y ⟹ f x = f y" by (iprover intro: refl elim: subst) lemma arg_cong2: "⟦a = b; c = d⟧ ⟹ f a c = f b d" by (iprover intro: refl elim: subst) lemma cong: "⟦f = g; (x::'a) = y⟧ ⟹ f x = g y" by (iprover intro: refl elim: subst) ML ‹fun cong_tac ctxt = Cong_Tac.cong_tac ctxt @{thm cong}› subsubsection ‹Equality of booleans -- iff› lemma iffD2: "⟦P = Q; Q⟧ ⟹ P" by (erule ssubst) lemma rev_iffD2: "⟦Q; P = Q⟧ ⟹ P" by (erule iffD2) lemma iffD1: "Q = P ⟹ Q ⟹ P" by (drule sym) (rule iffD2) lemma rev_iffD1: "Q ⟹ Q = P ⟹ P" by (drule sym) (rule rev_iffD2) lemma iffE: assumes major: "P = Q" and minor: "⟦P ⟶ Q; Q ⟶ P⟧ ⟹ R" shows R by (iprover intro: minor impI major [THEN iffD2] major [THEN iffD1]) subsubsection ‹True (1)› lemma TrueI: True unfolding True_def by (rule refl) lemma eqTrueE: "P = True ⟹ P" by (erule iffD2) (rule TrueI) subsubsection ‹Universal quantifier (1)› lemma spec: "∀x::'a. P x ⟹ P x" unfolding All_def by (iprover intro: eqTrueE fun_cong) lemma allE: assumes major: "∀x. P x" and minor: "P x ⟹ R" shows R by (iprover intro: minor major [THEN spec]) lemma all_dupE: assumes major: "∀x. P x" and minor: "⟦P x; ∀x. P x⟧ ⟹ R" shows R by (iprover intro: minor major major [THEN spec]) subsubsection ‹False› text ‹ Depends upon ‹spec›; it is impossible to do propositional logic before quantifiers! › lemma FalseE: "False ⟹ P" unfolding False_def by (erule spec) lemma False_neq_True: "False = True ⟹ P" by (erule eqTrueE [THEN FalseE]) subsubsection ‹Negation› lemma notI: assumes "P ⟹ False" shows "¬ P" unfolding not_def by (iprover intro: impI assms) lemma False_not_True: "False ≠ True" by (iprover intro: notI elim: False_neq_True) lemma True_not_False: "True ≠ False" by (iprover intro: notI dest: sym elim: False_neq_True) lemma notE: "⟦¬ P; P⟧ ⟹ R" unfolding not_def by (iprover intro: mp [THEN FalseE]) subsubsection ‹Implication› lemma impE: assumes "P ⟶ Q" P "Q ⟹ R" shows R by (iprover intro: assms mp) text ‹Reduces ‹Q› to ‹P ⟶ Q›, allowing substitution in ‹P›.› lemma rev_mp: "⟦P; P ⟶ Q⟧ ⟹ Q" by (rule mp) lemma contrapos_nn: assumes major: "¬ Q" and minor: "P ⟹ Q" shows "¬ P" by (iprover intro: notI minor major [THEN notE]) text ‹Not used at all, but we already have the other 3 combinations.› lemma contrapos_pn: assumes major: "Q" and minor: "P ⟹ ¬ Q" shows "¬ P" by (iprover intro: notI minor major notE) lemma not_sym: "t ≠ s ⟹ s ≠ t" by (erule contrapos_nn) (erule sym) lemma eq_neq_eq_imp_neq: "⟦x = a; a ≠ b; b = y⟧ ⟹ x ≠ y" by (erule subst, erule ssubst, assumption) subsubsection ‹Disjunction (1)› lemma disjE: assumes major: "P ∨ Q" and minorP: "P ⟹ R" and minorQ: "Q ⟹ R" shows R by (iprover intro: minorP minorQ impI major [unfolded or_def, THEN spec, THEN mp, THEN mp]) subsubsection ‹Derivation of ‹iffI›› text ‹In an intuitionistic version of HOL ‹iffI› needs to be an axiom.› lemma iffI: assumes "P ⟹ Q" and "Q ⟹ P" shows "P = Q" proof (rule disjE[OF True_or_False[of P]]) assume 1: "P = True" note Q = assms(1)[OF eqTrueE[OF this]] from 1 show ?thesis proof (rule ssubst) from True_or_False[of Q] show "True = Q" proof (rule disjE) assume "Q = True" thus ?thesis by(rule sym) next assume "Q = False" with Q have False by (rule rev_iffD1) thus ?thesis by (rule FalseE) qed qed next assume 2: "P = False" thus ?thesis proof (rule ssubst) from True_or_False[of Q] show "False = Q" proof (rule disjE) assume "Q = True" from 2 assms(2)[OF eqTrueE[OF this]] have False by (rule iffD1) thus ?thesis by (rule FalseE) next assume "Q = False" thus ?thesis by(rule sym) qed qed qed subsubsection ‹True (2)› lemma eqTrueI: "P ⟹ P = True" by (iprover intro: iffI TrueI) subsubsection ‹Universal quantifier (2)› lemma allI: assumes "⋀x::'a. P x" shows "∀x. P x" unfolding All_def by (iprover intro: ext eqTrueI assms) subsubsection ‹Existential quantifier› lemma exI: "P x ⟹ ∃x::'a. P x" unfolding Ex_def by (iprover intro: allI allE impI mp) lemma exE: assumes major: "∃x::'a. P x" and minor: "⋀x. P x ⟹ Q" shows "Q" by (rule major [unfolded Ex_def, THEN spec, THEN mp]) (iprover intro: impI [THEN allI] minor) subsubsection ‹Conjunction› lemma conjI: "⟦P; Q⟧ ⟹ P ∧ Q" unfolding and_def by (iprover intro: impI [THEN allI] mp) lemma conjunct1: "⟦P ∧ Q⟧ ⟹ P" unfolding and_def by (iprover intro: impI dest: spec mp) lemma conjunct2: "⟦P ∧ Q⟧ ⟹ Q" unfolding and_def by (iprover intro: impI dest: spec mp) lemma conjE: assumes major: "P ∧ Q" and minor: "⟦P; Q⟧ ⟹ R" shows R proof (rule minor) show P by (rule major [THEN conjunct1]) show Q by (rule major [THEN conjunct2]) qed lemma context_conjI: assumes P "P ⟹ Q" shows "P ∧ Q" by (iprover intro: conjI assms) subsubsection ‹Disjunction (2)› lemma disjI1: "P ⟹ P ∨ Q" unfolding or_def by (iprover intro: allI impI mp) lemma disjI2: "Q ⟹ P ∨ Q" unfolding or_def by (iprover intro: allI impI mp) subsubsection ‹Classical logic› lemma classical: assumes "¬ P ⟹ P" shows P proof (rule True_or_False [THEN disjE]) show P if "P = True" using that by (iprover intro: eqTrueE) show P if "P = False" proof (intro notI assms) assume P with that show False by (iprover elim: subst) qed qed lemmas ccontr = FalseE [THEN classical] text ‹‹notE› with premises exchanged; it discharges ‹¬ R› so that it can be used to make elimination rules.› lemma rev_notE: assumes premp: P and premnot: "¬ R ⟹ ¬ P" shows R by (iprover intro: ccontr notE [OF premnot premp]) text ‹Double negation law.› lemma notnotD: "¬¬ P ⟹ P" by (iprover intro: ccontr notE ) lemma contrapos_pp: assumes p1: Q and p2: "¬ P ⟹ ¬ Q" shows P by (iprover intro: classical p1 p2 notE) subsubsection ‹Unique existence› lemma Uniq_I [intro?]: assumes "⋀x y. ⟦P x; P y⟧ ⟹ y = x" shows "Uniq P" unfolding Uniq_def by (iprover intro: assms allI impI) lemma Uniq_D [dest?]: "⟦Uniq P; P a; P b⟧ ⟹ a=b" unfolding Uniq_def by (iprover dest: spec mp) lemma ex1I: assumes "P a" "⋀x. P x ⟹ x = a" shows "∃!x. P x" unfolding Ex1_def by (iprover intro: assms exI conjI allI impI) text ‹Sometimes easier to use: the premises have no shared variables. Safe!› lemma ex_ex1I: assumes ex_prem: "∃x. P x" and eq: "⋀x y. ⟦P x; P y⟧ ⟹ x = y" shows "∃!x. P x" by (iprover intro: ex_prem [THEN exE] ex1I eq) lemma ex1E: assumes major: "∃!x. P x" and minor: "⋀x. ⟦P x; ∀y. P y ⟶ y = x⟧ ⟹ R" shows R proof (rule major [unfolded Ex1_def, THEN exE]) show "⋀x. P x ∧ (∀y. P y ⟶ y = x) ⟹ R" by (iprover intro: minor elim: conjE) qed lemma ex1_implies_ex: "∃!x. P x ⟹ ∃x. P x" by (iprover intro: exI elim: ex1E) subsubsection ‹Classical intro rules for disjunction and existential quantifiers› lemma disjCI: assumes "¬ Q ⟹ P" shows "P ∨ Q" by (rule classical) (iprover intro: assms disjI1 disjI2 notI elim: notE) lemma excluded_middle: "¬ P ∨ P" by (iprover intro: disjCI) text ‹ case distinction as a natural deduction rule. Note that ‹¬ P› is the second case, not the first. › lemma case_split [case_names True False]: assumes "P ⟹ Q" "¬ P ⟹ Q" shows Q using excluded_middle [of P] by (iprover intro: assms elim: disjE) text ‹Classical implies (‹⟶›) elimination.› lemma impCE: assumes major: "P ⟶ Q" and minor: "¬ P ⟹ R" "Q ⟹ R" shows R using excluded_middle [of P] by (iprover intro: minor major [THEN mp] elim: disjE)+ text ‹ This version of ‹⟶› elimination works on ‹Q› before ‹P›. It works best for those cases in which ‹P› holds "almost everywhere". Can't install as default: would break old proofs. › lemma impCE': assumes major: "P ⟶ Q" and minor: "Q ⟹ R" "¬ P ⟹ R" shows R using assms by (elim impCE) text ‹Classical ‹⟷› elimination.› lemma iffCE: assumes major: "P = Q" and minor: "⟦P; Q⟧ ⟹ R" "⟦¬ P; ¬ Q⟧ ⟹ R" shows R by (rule major [THEN iffE]) (iprover intro: minor elim: impCE notE) lemma exCI: assumes "∀x. ¬ P x ⟹ P a" shows "∃x. P x" by (rule ccontr) (iprover intro: assms exI allI notI notE [of "∃x. P x"]) subsubsection ‹Intuitionistic Reasoning› lemma impE': assumes 1: "P ⟶ Q" and 2: "Q ⟹ R" and 3: "P ⟶ Q ⟹ P" shows R proof - from 3 and 1 have P . with 1 have Q by (rule impE) with 2 show R . qed lemma allE': assumes 1: "∀x. P x" and 2: "P x ⟹ ∀x. P x ⟹ Q" shows Q proof - from 1 have "P x" by (rule spec) from this and 1 show Q by (rule 2) qed lemma notE': assumes 1: "¬ P" and 2: "¬ P ⟹ P" shows R proof - from 2 and 1 have P . with 1 show R by (rule notE) qed lemma TrueE: "True ⟹ P ⟹ P" . lemma notFalseE: "¬ False ⟹ P ⟹ P" . lemmas [Pure.elim!] = disjE iffE FalseE conjE exE TrueE notFalseE and [Pure.intro!] = iffI conjI impI TrueI notI allI refl and [Pure.elim 2] = allE notE' impE' and [Pure.intro] = exI disjI2 disjI1 lemmas [trans] = trans and [sym] = sym not_sym and [Pure.elim?] = iffD1 iffD2 impE subsubsection ‹Atomizing meta-level connectives› axiomatization where eq_reflection: "x = y ⟹ x ≡ y" ― ‹admissible axiom› lemma atomize_all [atomize]: "(⋀x. P x) ≡ Trueprop (∀x. P x)" proof assume "⋀x. P x" then show "∀x. P x" .. next assume "∀x. P x" then show "⋀x. P x" by (rule allE) qed lemma atomize_imp [atomize]: "(A ⟹ B) ≡ Trueprop (A ⟶ B)" proof assume r: "A ⟹ B" show "A ⟶ B" by (rule impI) (rule r) next assume "A ⟶ B" and A then show B by (rule mp) qed lemma atomize_not: "(A ⟹ False) ≡ Trueprop (¬ A)" proof assume r: "A ⟹ False" show "¬ A" by (rule notI) (rule r) next assume "¬ A" and A then show False by (rule notE) qed lemma atomize_eq [atomize, code]: "(x ≡ y) ≡ Trueprop (x = y)" proof assume "x ≡ y" show "x = y" by (unfold ‹x ≡ y›) (rule refl) next assume "x = y" then show "x ≡ y" by (rule eq_reflection) qed lemma atomize_conj [atomize]: "(A &&& B) ≡ Trueprop (A ∧ B)" proof assume conj: "A &&& B" show "A ∧ B" proof (rule conjI) from conj show A by (rule conjunctionD1) from conj show B by (rule conjunctionD2) qed next assume conj: "A ∧ B" show "A &&& B" proof - from conj show A .. from conj show B .. qed qed lemmas [symmetric, rulify] = atomize_all atomize_imp and [symmetric, defn] = atomize_all atomize_imp atomize_eq subsubsection ‹Atomizing elimination rules› lemma atomize_exL[atomize_elim]: "(⋀x. P x ⟹ Q) ≡ ((∃x. P x) ⟹ Q)" by rule iprover+ lemma atomize_conjL[atomize_elim]: "(A ⟹ B ⟹ C) ≡ (A ∧ B ⟹ C)" by rule iprover+ lemma atomize_disjL[atomize_elim]: "((A ⟹ C) ⟹ (B ⟹ C) ⟹ C) ≡ ((A ∨ B ⟹ C) ⟹ C)" by rule iprover+ lemma atomize_elimL[atomize_elim]: "(⋀B. (A ⟹ B) ⟹ B) ≡ Trueprop A" .. subsection ‹Package setup› ML_file ‹Tools/hologic.ML› ML_file ‹Tools/rewrite_hol_proof.ML› setup ‹Proofterm.set_preproc (Proof_Rewrite_Rules.standard_preproc Rewrite_HOL_Proof.rews)› subsubsection ‹Sledgehammer setup› text ‹ Theorems blacklisted to Sledgehammer. These theorems typically produce clauses that are prolific (match too many equality or membership literals) and relate to seldom-used facts. Some duplicate other rules. › named_theorems no_atp "theorems that should be filtered out by Sledgehammer" subsubsection ‹Classical Reasoner setup› lemma imp_elim: "P ⟶ Q ⟹ (¬ R ⟹ P) ⟹ (Q ⟹ R) ⟹ R" by (rule classical) iprover lemma swap: "¬ P ⟹ (¬ R ⟹ P) ⟹ R" by (rule classical) iprover lemma thin_refl: "⟦x = x; PROP W⟧ ⟹ PROP W" . ML ‹ structure Hypsubst = Hypsubst ( val dest_eq = HOLogic.dest_eq val dest_Trueprop = HOLogic.dest_Trueprop val dest_imp = HOLogic.dest_imp val eq_reflection = @{thm eq_reflection} val rev_eq_reflection = @{thm meta_eq_to_obj_eq} val imp_intr = @{thm impI} val rev_mp = @{thm rev_mp} val subst = @{thm subst} val sym = @{thm sym} val thin_refl = @{thm thin_refl}; ); open Hypsubst; structure Classical = Classical ( val imp_elim = @{thm imp_elim} val not_elim = @{thm notE} val swap = @{thm swap} val classical = @{thm classical} val sizef = Drule.size_of_thm val hyp_subst_tacs = [Hypsubst.hyp_subst_tac] ); structure Basic_Classical: BASIC_CLASSICAL = Classical; open Basic_Classical; › setup ‹ (*prevent substitution on bool*) let fun non_bool_eq (\<^const_name>‹HOL.eq›, Type (_, [T, _])) = T <> \<^typ>‹bool› | non_bool_eq _ = false; fun hyp_subst_tac' ctxt = SUBGOAL (fn (goal, i) => if Term.exists_Const non_bool_eq goal then Hypsubst.hyp_subst_tac ctxt i else no_tac); in Context_Rules.addSWrapper (fn ctxt => fn tac => hyp_subst_tac' ctxt ORELSE' tac) end › declare iffI [intro!] and notI [intro!] and impI [intro!] and disjCI [intro!] and conjI [intro!] and TrueI [intro!] and refl [intro!] declare iffCE [elim!] and FalseE [elim!] and impCE [elim!] and disjE [elim!] and conjE [elim!] declare ex_ex1I [intro!] and allI [intro!] and exI [intro] declare exE [elim!] allE [elim] ML ‹val HOL_cs = claset_of \<^context>› lemma contrapos_np: "¬ Q ⟹ (¬ P ⟹ Q) ⟹ P" by (erule swap) declare ex_ex1I [rule del, intro! 2] and ex1I [intro] declare ext [intro] lemmas [intro?] = ext and [elim?] = ex1_implies_ex text ‹Better than ‹ex1E› for classical reasoner: needs no quantifier duplication!› lemma alt_ex1E [elim!]: assumes major: "∃!x. P x" and minor: "⋀x. ⟦P x; ∀y y'. P y ∧ P y' ⟶ y = y'⟧ ⟹ R" shows R proof (rule ex1E [OF major minor]) show "∀y y'. P y ∧ P y' ⟶ y = y'" if "P x" and §: "∀y. P y ⟶ y = x" for x using ‹P x› § § by fast qed assumption text ‹And again using Uniq› lemma alt_ex1E': assumes "∃!x. P x" "⋀x. ⟦P x; ∃⇩_{≤}⇩_{1}x. P x⟧ ⟹ R" shows R using assms unfolding Uniq_def by fast lemma ex1_iff_ex_Uniq: "(∃!x. P x) ⟷ (∃x. P x) ∧ (∃⇩_{≤}⇩_{1}x. P x)" unfolding Uniq_def by fast ML ‹ structure Blast = Blast ( structure Classical = Classical val Trueprop_const = dest_Const \<^Const>‹Trueprop› val equality_name = \<^const_name>‹HOL.eq› val not_name = \<^const_name>‹Not› val notE = @{thm notE} val ccontr = @{thm ccontr} val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac ); val blast_tac = Blast.blast_tac; › subsubsection ‹THE: definite description operator› lemma the_equality [intro]: assumes "P a" and "⋀x. P x ⟹ x = a" shows "(THE x. P x) = a" by (blast intro: assms trans [OF arg_cong [where f=The] the_eq_trivial]) lemma theI: assumes "P a" and "⋀x. P x ⟹ x = a" shows "P (THE x. P x)" by (iprover intro: assms the_equality [THEN ssubst]) lemma theI': "∃!x. P x ⟹ P (THE x. P x)" by (blast intro: theI) text ‹Easier to apply than ‹theI›: only one occurrence of ‹P›.› lemma theI2: assumes "P a" "⋀x. P x ⟹ x = a" "⋀x. P x ⟹ Q x" shows "Q (THE x. P x)" by (iprover intro: assms theI) lemma the1I2: assumes "∃!x. P x" "⋀x. P x ⟹ Q x" shows "Q (THE x. P x)" by (iprover intro: assms(2) theI2[where P=P and Q=Q] ex1E[OF assms(1)] elim: allE impE) lemma the1_equality [elim?]: "⟦∃!x. P x; P a⟧ ⟹ (THE x. P x) = a" by blast lemma the1_equality': "⟦∃⇩_{≤}⇩_{1}x. P x; P a⟧ ⟹ (THE x. P x) = a" unfolding Uniq_def by blast lemma the_sym_eq_trivial: "(THE y. x = y) = x" by blast subsubsection ‹Simplifier› lemma eta_contract_eq: "(λs. f s) = f" .. lemma subst_all: ‹(⋀x. x = a ⟹ PROP P x) ≡ PROP P a› ‹(⋀x. a = x ⟹ PROP P x) ≡ PROP P a› proof - show ‹(⋀x. x = a ⟹ PROP P x) ≡ PROP P a› proof (rule equal_intr_rule) assume *: ‹⋀x. x = a ⟹ PROP P x› show ‹PROP P a› by (rule *) (rule refl) next fix x assume ‹PROP P a› and ‹x = a› from ‹x = a› have ‹x ≡ a› by (rule eq_reflection) with ‹PROP P a› show ‹PROP P x› by simp qed show ‹(⋀x. a = x ⟹ PROP P x) ≡ PROP P a› proof (rule equal_intr_rule) assume *: ‹⋀x. a = x ⟹ PROP P x› show ‹PROP P a› by (rule *) (rule refl) next fix x assume ‹PROP P a› and ‹a = x› from ‹a = x› have ‹a ≡ x› by (rule eq_reflection) with ‹PROP P a› show ‹PROP P x› by simp qed qed lemma simp_thms: shows not_not: "(¬ ¬ P) = P" and Not_eq_iff: "((¬ P) = (¬ Q)) = (P = Q)" and "(P ≠ Q) = (P = (¬ Q))" "(P ∨ ¬P) = True" "(¬ P ∨ P) = True" "(x = x) = True" and not_True_eq_False [code]: "(¬ True) = False" and not_False_eq_True [code]: "(¬ False) = True" and "(¬ P) ≠ P" "P ≠ (¬ P)" "(True = P) = P" and eq_True: "(P = True) = P" and "(False = P) = (¬ P)" and eq_False: "(P = False) = (¬ P)" and "(True ⟶ P) = P" "(False ⟶ P) = True" "(P ⟶ True) = True" "(P ⟶ P) = True" "(P ⟶ False) = (¬ P)" "(P ⟶ ¬ P) = (¬ P)" "(P ∧ True) = P" "(True ∧ P) = P" "(P ∧ False) = False" "(False ∧ P) = False" "(P ∧ P) = P" "(P ∧ (P ∧ Q)) = (P ∧ Q)" "(P ∧ ¬ P) = False" "(¬ P ∧ P) = False" "(P ∨ True) = True" "(True ∨ P) = True" "(P ∨ False) = P" "(False ∨ P) = P" "(P ∨ P) = P" "(P ∨ (P ∨ Q)) = (P ∨ Q)" and "(∀x. P) = P" "(∃x. P) = P" "∃x. x = t" "∃x. t = x" and "⋀P. (∃x. x = t ∧ P x) = P t" "⋀P. (∃x. t = x ∧ P x) = P t" "⋀P. (∀x. x = t ⟶ P x) = P t" "⋀P. (∀x. t = x ⟶ P x) = P t" "(∀x. x ≠ t) = False" "(∀x. t ≠ x) = False" by (blast, blast, blast, blast, blast, iprover+) lemma disj_absorb: "A ∨ A ⟷ A" by blast lemma disj_left_absorb: "A ∨ (A ∨ B) ⟷ A ∨ B" by blast lemma conj_absorb: "A ∧ A ⟷ A" by blast lemma conj_left_absorb: "A ∧ (A ∧ B) ⟷ A ∧ B" by blast lemma eq_ac: shows eq_commute: "a = b ⟷ b = a" and iff_left_commute: "(P ⟷ (Q ⟷ R)) ⟷ (Q ⟷ (P ⟷ R))" and iff_assoc: "((P ⟷ Q) ⟷ R) ⟷ (P ⟷ (Q ⟷ R))" by (iprover, blast+) lemma neq_commute: "a ≠ b ⟷ b ≠ a" by iprover lemma conj_comms: shows conj_commute: "P ∧ Q ⟷ Q ∧ P" and conj_left_commute: "P ∧ (Q ∧ R) ⟷ Q ∧ (P ∧ R)" by iprover+ lemma conj_assoc: "(P ∧ Q) ∧ R ⟷ P ∧ (Q ∧ R)" by iprover lemmas conj_ac = conj_commute conj_left_commute conj_assoc lemma disj_comms: shows disj_commute: "P ∨ Q ⟷ Q ∨ P" and disj_left_commute: "P ∨ (Q ∨ R) ⟷ Q ∨ (P ∨ R)" by iprover+ lemma disj_assoc: "(P ∨ Q) ∨ R ⟷ P ∨ (Q ∨ R)" by iprover lemmas disj_ac = disj_commute disj_left_commute disj_assoc lemma conj_disj_distribL: "P ∧ (Q ∨ R) ⟷ P ∧ Q ∨ P ∧ R" by iprover lemma conj_disj_distribR: "(P ∨ Q) ∧ R ⟷ P ∧ R ∨ Q ∧ R" by iprover lemma disj_conj_distribL: "P ∨ (Q ∧ R) ⟷ (P ∨ Q) ∧ (P ∨ R)" by iprover lemma disj_conj_distribR: "(P ∧ Q) ∨ R ⟷ (P ∨ R) ∧ (Q ∨ R)" by iprover lemma imp_conjR: "(P ⟶ (Q ∧ R)) = ((P ⟶ Q) ∧ (P ⟶ R))" by iprover lemma imp_conjL: "((P ∧ Q) ⟶ R) = (P ⟶ (Q ⟶ R))" by iprover lemma imp_disjL: "((P ∨ Q) ⟶ R) = ((P ⟶ R) ∧ (Q ⟶ R))" by iprover text ‹These two are specialized, but ‹imp_disj_not1› is useful in ‹Auth/Yahalom›.› lemma imp_disj_not1: "(P ⟶ Q ∨ R) ⟷ (¬ Q ⟶ P ⟶ R)" by blast lemma imp_disj_not2: "(P ⟶ Q ∨ R) ⟷ (¬ R ⟶ P ⟶ Q)" by blast lemma imp_disj1: "((P ⟶ Q) ∨ R) ⟷ (P ⟶ Q ∨ R)" by blast lemma imp_disj2: "(Q ∨ (P ⟶ R)) ⟷ (P ⟶ Q ∨ R)" by blast lemma imp_cong: "(P = P') ⟹ (P' ⟹ (Q = Q')) ⟹ ((P ⟶ Q) ⟷ (P' ⟶ Q'))" by iprover lemma de_Morgan_disj: "¬ (P ∨ Q) ⟷ ¬ P ∧ ¬ Q" by iprover lemma de_Morgan_conj: "¬ (P ∧ Q) ⟷ ¬ P ∨ ¬ Q" by blast lemma not_imp: "¬ (P ⟶ Q) ⟷ P ∧ ¬ Q" by blast lemma not_iff: "P ≠ Q ⟷ (P ⟷ ¬ Q)" by blast lemma disj_not1: "¬ P ∨ Q ⟷ (P ⟶ Q)" by blast lemma disj_not2: "P ∨ ¬ Q ⟷ (Q ⟶ P)" by blast ― ‹changes orientation :-(› lemma imp_conv_disj: "(P ⟶ Q) ⟷ (¬ P) ∨ Q" by blast lemma disj_imp: "P ∨ Q ⟷ ¬ P ⟶ Q" by blast lemma iff_conv_conj_imp: "(P ⟷ Q) ⟷ (P ⟶ Q) ∧ (Q ⟶ P)" by iprover lemma cases_simp: "(P ⟶ Q) ∧ (¬ P ⟶ Q) ⟷ Q" ― ‹Avoids duplication of subgoals after ‹if_split›, when the true and false› ― ‹cases boil down to the same thing.› by blast lemma not_all: "¬ (∀x. P x) ⟷ (∃x. ¬ P x)" by blast lemma imp_all: "((∀x. P x) ⟶ Q) ⟷ (∃x. P x ⟶ Q)" by blast lemma not_ex: "¬ (∃x. P x) ⟷ (∀x. ¬ P x)" by iprover lemma imp_ex: "((∃x. P x) ⟶ Q) ⟷ (∀x. P x ⟶ Q)" by iprover lemma all_not_ex: "(∀x. P x) ⟷ ¬ (∃x. ¬ P x)" by blast declare All_def [no_atp] lemma ex_disj_distrib: "(∃x. P x ∨ Q x) ⟷ (∃x. P x) ∨ (∃x. Q x)" by iprover lemma all_conj_distrib: "(∀x. P x ∧ Q x) ⟷ (∀x. P x) ∧ (∀x. Q x)" by iprover text ‹ ┉ The ‹∧› congruence rule: not included by default! May slow rewrite proofs down by as much as 50\%› lemma conj_cong: "P = P' ⟹ (P' ⟹ Q = Q') ⟹ (P ∧ Q) = (P' ∧ Q')" by iprover lemma rev_conj_cong: "Q = Q' ⟹ (Q' ⟹ P = P') ⟹ (P ∧ Q) = (P' ∧ Q')" by iprover text ‹The ‹|› congruence rule: not included by default!› lemma disj_cong: "P = P' ⟹ (¬ P' ⟹ Q = Q') ⟹ (P ∨ Q) = (P' ∨ Q')" by blast text ‹┉ if-then-else rules› lemma if_True [code]: "(if True then x else y) = x" unfolding If_def by blast lemma if_False [code]: "(if False then x else y) = y" unfolding If_def by blast lemma if_P: "P ⟹ (if P then x else y) = x" unfolding If_def by blast lemma if_not_P: "¬ P ⟹ (if P then x else y) = y" unfolding If_def by blast lemma if_split: "P (if Q then x else y) = ((Q ⟶ P x) ∧ (¬ Q ⟶ P y))" proof (rule case_split [of Q]) show ?thesis if Q using that by (simplesubst if_P) blast+ show ?thesis if "¬ Q" using that by (simplesubst if_not_P) blast+ qed lemma if_split_asm: "P (if Q then x else y) = (¬ ((Q ∧ ¬ P x) ∨ (¬ Q ∧ ¬ P y)))" by (simplesubst if_split) blast lemmas if_splits [no_atp] = if_split if_split_asm lemma if_cancel: "(if c then x else x) = x" by (simplesubst if_split) blast lemma if_eq_cancel: "(if x = y then y else x) = x" by (simplesubst if_split) blast lemma if_bool_eq_conj: "(if P then Q else R) = ((P ⟶ Q) ∧ (¬ P ⟶ R))" ― ‹This form is useful for expanding ‹if›s on the RIGHT of the ‹⟹› symbol.› by (rule if_split) lemma if_bool_eq_disj: "(if P then Q else R) = ((P ∧ Q) ∨ (¬ P ∧ R))" ― ‹And this form is useful for expanding ‹if›s on the LEFT.› by (simplesubst if_split) blast lemma Eq_TrueI: "P ⟹ P ≡ True" unfolding atomize_eq by iprover lemma Eq_FalseI: "¬ P ⟹ P ≡ False" unfolding atomize_eq by iprover text ‹┉ let rules for simproc› lemma Let_folded: "f x ≡ g x ⟹ Let x f ≡ Let x g" by (unfold Let_def) lemma Let_unfold: "f x ≡ g ⟹ Let x f ≡ g" by (unfold Let_def) text ‹ The following copy of the implication operator is useful for fine-tuning congruence rules. It instructs the simplifier to simplify its premise. › definition simp_implies :: "prop ⇒ prop ⇒ prop" (infixr "=simp=>" 1) where "simp_implies ≡ (⟹)" lemma simp_impliesI: assumes PQ: "(PROP P ⟹ PROP Q)" shows "PROP P =simp=> PROP Q" unfolding simp_implies_def by (iprover intro: PQ) lemma simp_impliesE: assumes PQ: "PROP P =simp=> PROP Q" and P: "PROP P" and QR: "PROP Q ⟹ PROP R" shows "PROP R" by (iprover intro: QR P PQ [unfolded simp_implies_def]) lemma simp_implies_cong: assumes PP' :"PROP P ≡ PROP P'" and P'QQ': "PROP P' ⟹ (PROP Q ≡ PROP Q')" shows "(PROP P =simp=> PROP Q) ≡ (PROP P' =simp=> PROP Q')" unfolding simp_implies_def proof (rule equal_intr_rule) assume PQ: "PROP P ⟹ PROP Q" and P': "PROP P'" from PP' [symmetric] and P' have "PROP P" by (rule equal_elim_rule1) then have "PROP Q" by (rule PQ) with P'QQ' [OF P'] show "PROP Q'" by (rule equal_elim_rule1) next assume P'Q': "PROP P' ⟹ PROP Q'" and P: "PROP P" from PP' and P have P': "PROP P'" by (rule equal_elim_rule1) then have "PROP Q'" by (rule P'Q') with P'QQ' [OF P', symmetric] show "PROP Q" by (rule equal_elim_rule1) qed lemma uncurry: assumes "P ⟶ Q ⟶ R" shows "P ∧ Q ⟶ R" using assms by blast lemma iff_allI: assumes "⋀x. P x = Q x" shows "(∀x. P x) = (∀x. Q x)" using assms by blast lemma iff_exI: assumes "⋀x. P x = Q x" shows "(∃x. P x) = (∃x. Q x)" using assms by blast lemma all_comm: "(∀x y. P x y) = (∀y x. P x y)" by blast lemma ex_comm: "(∃x y. P x y) = (∃y x. P x y)" by blast ML_file ‹Tools/simpdata.ML› ML ‹open Simpdata› setup ‹ map_theory_simpset (put_simpset HOL_basic_ss) #> Simplifier.method_setup Splitter.split_modifiers › simproc_setup defined_Ex ("∃x. P x") = ‹K Quantifier1.rearrange_Ex› simproc_setup defined_All ("∀x. P x") = ‹K Quantifier1.rearrange_All› simproc_setup defined_all("⋀x. PROP P x") = ‹K Quantifier1.rearrange_all› text ‹Simproc for proving ‹(y = x) ≡ False› from premise ‹¬ (x = y)›:› simproc_setup neq ("x = y") = ‹fn _ => let val neq_to_EQ_False = @{thm not_sym} RS @{thm Eq_FalseI}; fun is_neq eq lhs rhs thm = (case Thm.prop_of thm of _ $ (Not $ (eq' $ l' $ r')) => Not = HOLogic.Not andalso eq' = eq andalso r' aconv lhs andalso l' aconv rhs | _ => false); fun proc ss ct = (case Thm.term_of ct of eq $ lhs $ rhs => (case find_first (is_neq eq lhs rhs) (Simplifier.prems_of ss) of SOME thm => SOME (thm RS neq_to_EQ_False) | NONE => NONE) | _ => NONE); in proc end › simproc_setup let_simp ("Let x f") = ‹ let fun count_loose (Bound i) k = if i >= k then 1 else 0 | count_loose (s $ t) k = count_loose s k + count_loose t k | count_loose (Abs (_, _, t)) k = count_loose t (k + 1) | count_loose _ _ = 0; fun is_trivial_let (Const (\<^const_name>‹Let›, _) $ x $ t) = (case t of Abs (_, _, t') => count_loose t' 0 <= 1 | _ => true); in fn _ => fn ctxt => fn ct => if is_trivial_let (Thm.term_of ct) then SOME @{thm Let_def} (*no or one ocurrence of bound variable*) else let (*Norbert Schirmer's case*) val t = Thm.term_of ct; val (t', ctxt') = yield_singleton (Variable.import_terms false) t ctxt; in Option.map (hd o Variable.export ctxt' ctxt o single) (case t' of Const (\<^const_name>‹Let›,_) $ x $ f => (* x and f are already in normal form *) if is_Free x orelse is_Bound x orelse is_Const x then SOME @{thm Let_def} else let val n = case f of (Abs (x, _, _)) => x | _ => "x"; val cx = Thm.cterm_of ctxt x; val xT = Thm.typ_of_cterm cx; val cf = Thm.cterm_of ctxt f; val fx_g = Simplifier.rewrite ctxt (Thm.apply cf cx); val (_ $ _ $ g) = Thm.prop_of fx_g; val g' = abstract_over (x, g); val abs_g'= Abs (n, xT, g'); in if g aconv g' then let val rl = infer_instantiate ctxt [(("f", 0), cf), (("x", 0), cx)] @{thm Let_unfold}; in SOME (rl OF [fx_g]) end else if (Envir.beta_eta_contract f) aconv (Envir.beta_eta_contract abs_g') then NONE (*avoid identity conversion*) else let val g'x = abs_g' $ x; val g_g'x = Thm.symmetric (Thm.beta_conversion false (Thm.cterm_of ctxt g'x)); val rl = @{thm Let_folded} |> infer_instantiate ctxt [(("f", 0), Thm.cterm_of ctxt f), (("x", 0), cx), (("g", 0), Thm.cterm_of ctxt abs_g')]; in SOME (rl OF [Thm.transitive fx_g g_g'x]) end end | _ => NONE) end end › lemma True_implies_equals: "(True ⟹ PROP P) ≡ PROP P" proof assume "True ⟹ PROP P" from this [OF TrueI] show "PROP P" . next assume "PROP P" then show "PROP P" . qed lemma implies_True_equals: "(PROP P ⟹ True) ≡ Trueprop True" by standard (intro TrueI) lemma False_implies_equals: "(False ⟹ P) ≡ Trueprop True" by standard simp_all (* It seems that making this a simp rule is slower than using the simproc below *) lemma implies_False_swap: "(False ⟹ PROP P ⟹ PROP Q) ≡ (PROP P ⟹ False ⟹ PROP Q)" by (rule swap_prems_eq) ML ‹ fun eliminate_false_implies ct = let val (prems, concl) = Logic.strip_horn (Thm.term_of ct) fun go n = if n > 1 then Conv.rewr_conv @{thm Pure.swap_prems_eq} then_conv Conv.arg_conv (go (n - 1)) then_conv Conv.rewr_conv @{thm HOL.implies_True_equals} else Conv.rewr_conv @{thm HOL.False_implies_equals} in case concl of Const (@{const_name HOL.Trueprop}, _) $ _ => SOME (go (length prems) ct) | _ => NONE end › simproc_setup eliminate_false_implies ("False ⟹ PROP P") = ‹K (K eliminate_false_implies)› lemma ex_simps: "⋀P Q. (∃x. P x ∧ Q) = ((∃x. P x) ∧ Q)" "⋀P Q. (∃x. P ∧ Q x) = (P ∧ (∃x. Q x))" "⋀P Q. (∃x. P x ∨ Q) = ((∃x. P x) ∨ Q)" "⋀P Q. (∃x. P ∨ Q x) = (P ∨ (∃x. Q x))" "⋀P Q. (∃x. P x ⟶ Q) = ((∀x. P x) ⟶ Q)" "⋀P Q. (∃x. P ⟶ Q x) = (P ⟶ (∃x. Q x))" ― ‹Miniscoping: pushing in existential quantifiers.› by (iprover | blast)+ lemma all_simps: "⋀P Q. (∀x. P x ∧ Q) = ((∀x. P x) ∧ Q)" "⋀P Q. (∀x. P ∧ Q x) = (P ∧ (∀x. Q x))" "⋀P Q. (∀x. P x ∨ Q) = ((∀x. P x) ∨ Q)" "⋀P Q. (∀x. P ∨ Q x) = (P ∨ (∀x. Q x))" "⋀P Q. (∀x. P x ⟶ Q) = ((∃x. P x) ⟶ Q)" "⋀P Q. (∀x. P ⟶ Q x) = (P ⟶ (∀x. Q x))" ― ‹Miniscoping: pushing in universal quantifiers.› by (iprover | blast)+ lemmas [simp] = triv_forall_equality ― ‹prunes params› True_implies_equals implies_True_equals ― ‹prune ‹True› in asms› False_implies_equals ― ‹prune ‹False› in asms› if_True if_False if_cancel if_eq_cancel imp_disjL ― ‹In general it seems wrong to add distributive laws by default: they might cause exponential blow-up. But ‹imp_disjL› has been in for a while and cannot be removed without affecting existing proofs. Moreover, rewriting by ‹(P ∨ Q ⟶ R) = ((P ⟶ R) ∧ (Q ⟶ R))› might be justified on the grounds that it allows simplification of ‹R› in the two cases.› conj_assoc disj_assoc de_Morgan_conj de_Morgan_disj imp_disj1 imp_disj2 not_imp disj_not1 not_all not_ex cases_simp the_eq_trivial the_sym_eq_trivial ex_simps all_simps simp_thms subst_all lemmas [cong] = imp_cong simp_implies_cong lemmas [split] = if_split ML ‹val HOL_ss = simpset_of \<^context>› text ‹Simplifies ‹x› assuming ‹c› and ‹y› assuming ‹¬ c›.› lemma if_cong: assumes "b = c" and "c ⟹ x = u" and "¬ c ⟹ y = v" shows "(if b then x else y) = (if c then u else v)" using assms by simp text ‹Prevents simplification of ‹x› and ‹y›: faster and allows the execution of functional programs.› lemma if_weak_cong [cong]: assumes "b = c" shows "(if b then x else y) = (if c then x else y)" using assms by (rule arg_cong) text ‹Prevents simplification of t: much faster› lemma let_weak_cong: assumes "a = b" shows "(let x = a in t x) = (let x = b in t x)" using assms by (rule arg_cong) text ‹To tidy up the result of a simproc. Only the RHS will be simplified.› lemma eq_cong2: assumes "u = u'" shows "(t ≡ u) ≡ (t ≡ u')" using assms by simp lemma if_distrib: "f (if c then x else y) = (if c then f x else f y)" by simp lemma if_distribR: "(if b then f else g) x = (if b then f x else g x)" by simp lemma all_if_distrib: "(∀x. if x = a then P x else Q x) ⟷ P a ∧ (∀x. x≠a ⟶ Q x)" by auto lemma ex_if_distrib: "(∃x. if x = a then P x else Q x) ⟷ P a ∨ (∃x. x≠a ∧ Q x)" by auto lemma if_if_eq_conj: "(if P then if Q then x else y else y) = (if P ∧ Q then x else y)" by simp text ‹As a simplification rule, it replaces all function equalities by first-order equalities.› lemma fun_eq_iff: "f = g ⟷ (∀x. f x = g x)" by auto subsubsection ‹Generic cases and induction› text ‹Rule projections:› ML ‹ structure Project_Rule = Project_Rule ( val conjunct1 = @{thm conjunct1} val conjunct2 = @{thm conjunct2} val mp = @{thm mp} ); › context begin qualified definition "induct_forall P ≡ ∀x. P x" qualified definition "induct_implies A B ≡ A ⟶ B" qualified definition "induct_equal x y ≡ x = y" qualified definition "induct_conj A B ≡ A ∧ B" qualified definition "induct_true ≡ True" qualified definition "induct_false ≡ False" lemma induct_forall_eq: "(⋀x. P x) ≡ Trueprop (induct_forall (λx. P x))" by (unfold atomize_all induct_forall_def) lemma induct_implies_eq: "(A ⟹ B) ≡ Trueprop (induct_implies A B)" by (unfold atomize_imp induct_implies_def) lemma induct_equal_eq: "(x ≡ y) ≡ Trueprop (induct_equal x y)" by (unfold atomize_eq induct_equal_def) lemma induct_conj_eq: "(A &&& B) ≡ Trueprop (induct_conj A B)" by (unfold atomize_conj induct_conj_def) lemmas induct_atomize' = induct_forall_eq induct_implies_eq induct_conj_eq lemmas induct_atomize = induct_atomize' induct_equal_eq lemmas induct_rulify' [symmetric] = induct_atomize' lemmas induct_rulify [symmetric] = induct_atomize lemmas induct_rulify_fallback = induct_forall_def induct_implies_def induct_equal_def induct_conj_def induct_true_def induct_false_def lemma induct_forall_conj: "induct_forall (λx. induct_conj (A x) (B x)) = induct_conj (induct_forall A) (induct_forall B)" by (unfold induct_forall_def induct_conj_def) iprover lemma induct_implies_conj: "induct_implies C (induct_conj A B) = induct_conj (induct_implies C A) (induct_implies C B)" by (unfold induct_implies_def induct_conj_def) iprover lemma induct_conj_curry: "(induct_conj A B ⟹ PROP C) ≡ (A ⟹ B ⟹ PROP C)" proof assume r: "induct_conj A B ⟹ PROP C" assume ab: A B show "PROP C" by (rule r) (simp add: induct_conj_def ab) next assume r: "A ⟹ B ⟹ PROP C" assume ab: "induct_conj A B" show "PROP C" by (rule r) (simp_all add: ab [unfolded induct_conj_def]) qed lemmas induct_conj = induct_forall_conj induct_implies_conj induct_conj_curry lemma induct_trueI: "induct_true" by (simp add: induct_true_def) text ‹Method setup.› ML_file ‹~~/src/Tools/induct.ML› ML ‹ structure Induct = Induct ( val cases_default = @{thm case_split} val atomize = @{thms induct_atomize} val rulify = @{thms induct_rulify'} val rulify_fallback = @{thms induct_rulify_fallback} val equal_def = @{thm induct_equal_def} fun dest_def (Const (\<^const_name>‹induct_equal›, _) $ t $ u) = SOME (t, u) | dest_def _ = NONE fun trivial_tac ctxt = match_tac ctxt @{thms induct_trueI} ) › ML_file ‹~~/src/Tools/induction.ML› declaration ‹ fn _ => Induct.map_simpset (fn ss => ss addsimprocs [Simplifier.make_simproc \<^context> "swap_induct_false" {lhss = [\<^term>‹induct_false ⟹ PROP P ⟹ PROP Q›], proc = fn _ => fn _ => fn ct => (case Thm.term_of ct of _ $ (P as _ $ \<^Const_>‹induct_false›) $ (_ $ Q $ _) => if P <> Q then SOME Drule.swap_prems_eq else NONE | _ => NONE)}, Simplifier.make_simproc \<^context> "induct_equal_conj_curry" {lhss = [\<^term>‹induct_conj P Q ⟹ PROP R›], proc = fn _ => fn _ => fn ct => (case Thm.term_of ct of _ $ (_ $ P) $ _ => let fun is_conj \<^Const_>‹induct_conj for P Q› = is_conj P andalso is_conj Q | is_conj \<^Const_>‹induct_equal _ for _ _› = true | is_conj \<^Const_>‹induct_true› = true | is_conj \<^Const_>‹induct_false› = true | is_conj _ = false in if is_conj P then SOME @{thm induct_conj_curry} else NONE end | _ => NONE)}] |> Simplifier.set_mksimps (fn ctxt => Simpdata.mksimps Simpdata.mksimps_pairs ctxt #> map (rewrite_rule ctxt (map Thm.symmetric @{thms induct_rulify_fallback})))) › text ‹Pre-simplification of induction and cases rules› lemma [induct_simp]: "(⋀x. induct_equal x t ⟹ PROP P x) ≡ PROP P t" unfolding induct_equal_def proof assume r: "⋀x. x = t ⟹ PROP P x" show "PROP P t" by (rule r [OF refl]) next fix x assume "PROP P t" "x = t" then show "PROP P x" by simp qed lemma [induct_simp]: "(⋀x. induct_equal t x ⟹ PROP P x) ≡ PROP P t" unfolding induct_equal_def proof assume r: "⋀x. t = x ⟹ PROP P x" show "PROP P t" by (rule r [OF refl]) next fix x assume "PROP P t" "t = x" then show "PROP P x" by simp qed lemma [induct_simp]: "(induct_false ⟹ P) ≡ Trueprop induct_true" unfolding induct_false_def induct_true_def by (iprover intro: equal_intr_rule) lemma [induct_simp]: "(induct_true ⟹ PROP P) ≡ PROP P" unfolding induct_true_def proof assume "True ⟹ PROP P" then show "PROP P" using TrueI . next assume "PROP P" then show "PROP P" . qed lemma [induct_simp]: "(PROP P ⟹ induct_true) ≡ Trueprop induct_true" unfolding induct_true_def by (iprover intro: equal_intr_rule) lemma [induct_simp]: "(⋀x::'a::{}. induct_true) ≡ Trueprop induct_true" unfolding induct_true_def by (iprover intro: equal_intr_rule) lemma [induct_simp]: "induct_implies induct_true P ≡ P" by (simp add: induct_implies_def induct_true_def) lemma [induct_simp]: "x = x ⟷ True" by (rule simp_thms) end ML_file ‹~~/src/Tools/induct_tacs.ML› subsubsection ‹Coherent logic› ML_file ‹~~/src/Tools/coherent.ML› ML ‹ structure Coherent = Coherent ( val atomize_elimL = @{thm atomize_elimL}; val atomize_exL = @{thm atomize_exL}; val atomize_conjL = @{thm atomize_conjL}; val atomize_disjL = @{thm atomize_disjL}; val operator_names = [\<^const_name>‹HOL.disj›, \<^const_name>‹HOL.conj›, \<^const_name>‹Ex›]; ); › subsubsection ‹Reorienting equalities› ML ‹ signature REORIENT_PROC = sig val add : (term -> bool) -> theory -> theory val proc : morphism -> Proof.context -> cterm -> thm option end; structure Reorient_Proc : REORIENT_PROC = struct structure Data = Theory_Data ( type T = ((term -> bool) * stamp) list; val empty = []; fun merge data : T = Library.merge (eq_snd (op =)) data; ); fun add m = Data.map (cons (m, stamp ())); fun matches thy t = exists (fn (m, _) => m t) (Data.get thy); val meta_reorient = @{thm eq_commute [THEN eq_reflection]}; fun proc phi ctxt ct = let val thy = Proof_Context.theory_of ctxt; in case Thm.term_of ct of (_ $ t $ u) => if matches thy u then NONE else SOME meta_reorient | _ => NONE end; end; › subsection ‹Other simple lemmas and lemma duplicates› lemma eq_iff_swap: "(x = y ⟷ P) ⟹ (y = x ⟷ P)" by blast lemma all_cong1: "(⋀x. P x = P' x) ⟹ (∀x. P x) = (∀x. P' x)" by auto lemma ex_cong1: "(⋀x. P x = P' x) ⟹ (∃x. P x) = (∃x. P' x)" by auto lemma all_cong: "(⋀x. Q x ⟹ P x = P' x) ⟹ (∀x. Q x ⟶ P x) = (∀x. Q x ⟶ P' x)" by auto lemma ex_cong: "(⋀x. Q x ⟹ P x = P' x) ⟹ (∃x. Q x ∧ P x) = (∃x. Q x ∧ P' x)" by auto lemma ex1_eq [iff]: "∃!x. x = t" "∃!x. t = x" by blast+ lemma choice_eq: "(∀x. ∃!y. P x y) = (∃!f. ∀x. P x (f x))" (is "?lhs = ?rhs") proof (intro iffI allI) assume L: ?lhs then have §: "∀x. P x (THE y. P x y)" by (best intro: theI') show ?rhs by (rule ex1I) (use L § in ‹fast+›) next fix x assume R: ?rhs then obtain f where f: "∀x. P x (f x)" and f1: "⋀y. (∀x. P x (y x)) ⟹ y = f" by (blast elim: ex1E) show "∃!y. P x y" proof (rule ex1I) show "P x (f x)" using f by blast show "y = f x" if "P x y" for y proof - have "P z (if z = x then y else f z)" for z using f that by (auto split: if_split) with f1 [of "λz. if z = x then y else f z"] f show ?thesis by (auto simp add: split: if_split_asm dest: fun_cong) qed qed qed lemmas eq_sym_conv = eq_commute lemma nnf_simps: "(¬ (P ∧ Q)) = (¬ P ∨ ¬ Q)" "(¬ (P ∨ Q)) = (¬ P ∧ ¬ Q)" "(P ⟶ Q) = (¬ P ∨ Q)" "(P = Q) = ((P ∧ Q) ∨ (¬ P ∧ ¬ Q))" "(¬ (P = Q)) = ((P ∧ ¬ Q) ∨ (¬ P ∧ Q))" "(¬ ¬ P) = P" by blast+ subsection ‹Basic ML bindings› ML ‹ val FalseE = @{thm FalseE} val Let_def = @{thm Let_def} val TrueI = @{thm TrueI} val allE = @{thm allE} val allI = @{thm allI} val all_dupE = @{thm all_dupE} val arg_cong = @{thm arg_cong} val box_equals = @{thm box_equals} val ccontr = @{thm ccontr} val classical = @{thm classical} val conjE = @{thm conjE} val conjI = @{thm conjI} val conjunct1 = @{thm conjunct1} val conjunct2 = @{thm conjunct2} val disjCI = @{thm disjCI} val disjE = @{thm disjE} val disjI1 = @{thm disjI1} val disjI2 = @{thm disjI2} val eq_reflection = @{thm eq_reflection} val ex1E = @{thm ex1E} val ex1I = @{thm ex1I} val ex1_implies_ex = @{thm ex1_implies_ex} val exE = @{thm exE} val exI = @{thm exI} val excluded_middle = @{thm excluded_middle} val ext = @{thm ext} val fun_cong = @{thm fun_cong} val iffD1 = @{thm iffD1} val iffD2 = @{thm iffD2} val iffI = @{thm iffI} val impE = @{thm impE} val impI = @{thm impI} val meta_eq_to_obj_eq = @{thm meta_eq_to_obj_eq} val mp = @{thm mp} val notE = @{thm notE} val notI = @{thm notI} val not_all = @{thm not_all} val not_ex = @{thm not_ex} val not_iff = @{thm not_iff} val not_not = @{thm not_not} val not_sym = @{thm not_sym} val refl = @{thm refl} val rev_mp = @{thm rev_mp} val spec = @{thm spec} val ssubst = @{thm ssubst} val subst = @{thm subst} val sym = @{thm sym} val trans = @{thm trans} › locale cnf begin lemma clause2raw_notE: "⟦P; ¬P⟧ ⟹ False" by auto lemma clause2raw_not_disj: "⟦¬ P; ¬ Q⟧ ⟹ ¬ (P ∨ Q)" by auto lemma clause2raw_not_not: "P ⟹ ¬¬ P" by auto lemma iff_refl: "(P::bool) = P" by auto lemma iff_trans: "[| (P::bool) = Q; Q = R |] ==> P = R" by auto lemma conj_cong: "[| P = P'; Q = Q' |] ==> (P ∧ Q) = (P' ∧ Q')" by auto lemma disj_cong: "[| P = P'; Q = Q' |] ==> (P ∨ Q) = (P' ∨ Q')" by auto lemma make_nnf_imp: "[| (¬P) = P'; Q = Q' |] ==> (P ⟶ Q) = (P' ∨ Q')" by auto lemma make_nnf_iff: "[| P = P'; (¬P) = NP; Q = Q'; (¬Q) = NQ |] ==> (P = Q) = ((P' ∨ NQ) ∧ (NP ∨ Q'))" by auto lemma make_nnf_not_false: "(¬False) = True" by auto lemma make_nnf_not_true: "(¬True) = False" by auto lemma make_nnf_not_conj: "[| (¬P) = P'; (¬Q) = Q' |] ==> (¬(P ∧ Q)) = (P' ∨ Q')" by auto lemma make_nnf_not_disj: "[| (¬P) = P'; (¬Q) = Q' |] ==> (¬(P ∨ Q)) = (P' ∧ Q')" by auto lemma make_nnf_not_imp: "[| P = P'; (¬Q) = Q' |] ==> (¬(P ⟶ Q)) = (P' ∧ Q')" by auto lemma make_nnf_not_iff: "[| P = P'; (¬P) = NP; Q = Q'; (¬Q) = NQ |] ==> (¬(P = Q)) = ((P' ∨ Q') ∧ (NP ∨ NQ))" by auto lemma make_nnf_not_not: "P = P' ==> (¬¬P) = P'" by auto lemma simp_TF_conj_True_l: "[| P = True; Q = Q' |] ==> (P ∧ Q) = Q'" by auto lemma simp_TF_conj_True_r: "[| P = P'; Q = True |] ==> (P ∧ Q) = P'" by auto lemma simp_TF_conj_False_l: "P = False ==> (P ∧ Q) = False" by auto lemma simp_TF_conj_False_r: "Q = False ==> (P ∧ Q) = False" by auto lemma simp_TF_disj_True_l: "P = True ==> (P ∨ Q) = True" by auto lemma simp_TF_disj_True_r: "Q = True ==> (P ∨ Q) = True" by auto lemma simp_TF_disj_False_l: "[| P = False; Q = Q' |] ==> (P ∨ Q) = Q'" by auto lemma simp_TF_disj_False_r: "[| P = P'; Q = False |] ==> (P ∨ Q) = P'" by auto lemma make_cnf_disj_conj_l: "[| (P ∨ R) = PR; (Q ∨ R) = QR |] ==> ((P ∧ Q) ∨ R) = (PR ∧ QR)" by auto lemma make_cnf_disj_conj_r: "[| (P ∨ Q) = PQ; (P ∨ R) = PR |] ==> (P ∨ (Q ∧ R)) = (PQ ∧ PR)" by auto lemma make_cnfx_disj_ex_l: "((∃(x::bool). P x) ∨ Q) = (∃x. P x ∨ Q)" by auto lemma make_cnfx_disj_ex_r: "(P ∨ (∃(x::bool). Q x)) = (∃x. P ∨ Q x)" by auto lemma make_cnfx_newlit: "(P ∨ Q) = (∃x. (P ∨ x) ∧ (Q ∨ ¬x))" by auto lemma make_cnfx_ex_cong: "(∀(x::bool). P x = Q x) ⟹ (∃x. P x) = (∃x. Q x)" by auto lemma weakening_thm: "[| P; Q |] ==> Q" by auto lemma cnftac_eq_imp: "[| P = Q; P |] ==> Q" by auto end ML_file ‹Tools/cnf.ML› section ‹‹NO_MATCH› simproc› text ‹ The simplification procedure can be used to avoid simplification of terms of a certain form. › definition NO_MATCH :: "'a ⇒ 'b ⇒ bool" where "NO_MATCH pat val ≡ True" lemma NO_MATCH_cong[cong]: "NO_MATCH pat val = NO_MATCH pat val" by (rule refl) declare [[coercion_args NO_MATCH - -]] simproc_setup NO_MATCH ("NO_MATCH pat val") = ‹fn _ => fn ctxt => fn ct => let val thy = Proof_Context.theory_of ctxt val dest_binop = Term.dest_comb #> apfst (Term.dest_comb #> snd) val m = Pattern.matches thy (dest_binop (Thm.term_of ct)) in if m then NONE else SOME @{thm NO_MATCH_def} end › text ‹ This setup ensures that a rewrite rule of the form \<^term>‹NO_MATCH pat val ⟹ t› is only applied, if the pattern ‹pat› does not match the value ‹val›. › text‹ Tagging a premise of a simp rule with ASSUMPTION forces the simplifier not to simplify the argument and to solve it by an assumption. › definition ASSUMPTION :: "bool ⇒ bool" where "ASSUMPTION A ≡ A" lemma ASSUMPTION_cong[cong]: "ASSUMPTION A = ASSUMPTION A" by (rule refl) lemma ASSUMPTION_I: "A ⟹ ASSUMPTION A" by (simp add: ASSUMPTION_def) lemma ASSUMPTION_D: "ASSUMPTION A ⟹ A" by (simp add: ASSUMPTION_def) setup ‹ let val asm_sol = mk_solver "ASSUMPTION" (fn ctxt => resolve_tac ctxt [@{thm ASSUMPTION_I}] THEN' resolve_tac ctxt (Simplifier.prems_of ctxt)) in map_theory_simpset (fn ctxt => Simplifier.addSolver (ctxt,asm_sol)) end › subsection ‹Code generator setup› subsubsection ‹Generic code generator preprocessor setup› lemma conj_left_cong: "P ⟷ Q ⟹ P ∧ R ⟷ Q ∧ R" by (fact arg_cong) lemma disj_left_cong: "P ⟷ Q ⟹ P ∨ R ⟷ Q ∨ R" by (fact arg_cong) setup ‹ Code_Preproc.map_pre (put_simpset HOL_basic_ss) #> Code_Preproc.map_post (put_simpset HOL_basic_ss) #> Code_Simp.map_ss (put_simpset HOL_basic_ss #> Simplifier.add_cong @{thm conj_left_cong} #> Simplifier.add_cong @{thm disj_left_cong}) › subsubsection ‹Equality› class equal = fixes equal :: "'a ⇒ 'a ⇒ bool" assumes equal_eq: "equal x y ⟷ x = y" begin lemma equal: "equal = (=)" by (rule ext equal_eq)+ lemma equal_refl: "equal x x ⟷ True" unfolding equal by rule+ lemma eq_equal: "(=) ≡ equal" by (rule eq_reflection) (rule ext, rule ext, rule sym, rule equal_eq) end declare eq_equal [symmetric, code_post] declare eq_equal [code] setup ‹ Code_Preproc.map_pre (fn ctxt => ctxt addsimprocs [Simplifier.make_simproc \<^context> "equal" {lhss = [\<^term>‹HOL.eq›], proc = fn _ => fn _ => fn ct => (case Thm.term_of ct of Const (_, Type (\<^type_name>‹fun›, [Type _, _])) => SOME @{thm eq_equal} | _ => NONE)}]) › subsubsection ‹Generic code generator foundation› text ‹Datatype \<^typ>‹bool›› code_datatype True False lemma [code]: shows "False ∧ P ⟷ False" and "True ∧ P ⟷ P" and "P ∧ False ⟷ False" and "P ∧ True ⟷ P" by simp_all lemma [code]: shows "False ∨ P ⟷ P" and "True ∨ P ⟷ True" and "P ∨ False ⟷ P" and "P ∨ True ⟷ True" by simp_all lemma [code]: shows "(False ⟶ P) ⟷ True" and "(True ⟶ P) ⟷ P" and "(P ⟶ False) ⟷ ¬ P" and "(P ⟶ True) ⟷ True" by simp_all text ‹More about \<^typ>‹prop›› lemma [code nbe]: shows "(True ⟹ PROP Q) ≡ PROP Q" and "(PROP Q ⟹ True) ≡ Trueprop True" and "(P ⟹ R) ≡ Trueprop (P ⟶ R)" by (auto intro!: equal_intr_rule) lemma Trueprop_code [code]: "Trueprop True ≡ Code_Generator.holds" by (auto intro!: equal_intr_rule holds) declare Trueprop_code [symmetric, code_post] text ‹Equality› declare simp_thms(6) [code nbe] instantiation itself :: (type) equal begin definition equal_itself :: "'a itself ⇒ 'a itself ⇒ bool" where "equal_itself x y ⟷ x = y" instance by standard (fact equal_itself_def) end lemma equal_itself_code [code]: "equal TYPE('a) TYPE('a) ⟷ True" by (simp add: equal) setup ‹Sign.add_const_constraint (\<^const_name>‹equal›, SOME \<^typ>‹'a::type ⇒ 'a ⇒ bool›)› lemma equal_alias_cert: "OFCLASS('a, equal_class) ≡ (((=) :: 'a ⇒ 'a ⇒ bool) ≡ equal)" (is "?ofclass ≡ ?equal") proof assume "PROP ?ofclass" show "PROP ?equal" by (tactic ‹ALLGOALS (resolve_tac \<^context> [Thm.unconstrainT @{thm eq_equal}])›) (fact ‹PROP ?ofclass›) next assume "PROP ?equal" show "PROP ?ofclass" proof qed (simp add: ‹PROP ?equal›) qed setup ‹Sign.add_const_constraint (\<^const_name>‹equal›, SOME \<^typ>‹'a::equal ⇒ 'a ⇒ bool›)› setup ‹Nbe.add_const_alias @{thm equal_alias_cert}› text ‹Cases› lemma Let_case_cert: assumes "CASE ≡ (λx. Let x f)" shows "CASE x ≡ f x" using assms by simp_all setup ‹ Code.declare_case_global @{thm Let_case_cert} #> Code.declare_undefined_global \<^const_name>‹undefined› › declare [[code abort: undefined]] subsubsection ‹Generic code generator target languages› text ‹type \<^typ>‹bool›› code_printing type_constructor bool ⇀ (SML) "bool" and (OCaml) "bool" and (Haskell) "Bool" and (Scala) "Boolean" | constant True ⇀ (SML) "true" and (OCaml) "true" and (Haskell) "True" and (Scala) "true" | constant False ⇀ (SML) "false" and (OCaml) "false" and (Haskell) "False" and (Scala) "false" code_reserved SML bool true false code_reserved OCaml bool code_reserved Scala Boolean code_printing constant Not ⇀ (SML) "not" and (OCaml) "not" and (Haskell) "not" and (Scala) "'! _" | constant HOL.conj ⇀ (SML) infixl 1 "andalso" and (OCaml) infixl 3 "&&" and (Haskell) infixr 3 "&&" and (Scala) infixl 3 "&&" | constant HOL.disj ⇀ (SML) infixl 0 "orelse" and (OCaml) infixl 2 "||" and (Haskell) infixl 2 "||" and (Scala) infixl 1 "||" | constant HOL.implies ⇀ (SML) "!(if (_)/ then (_)/ else true)" and (OCaml) "!(if (_)/ then (_)/ else true)" and (Haskell) "!(if (_)/ then (_)/ else True)" and (Scala) "!(if ((_))/ (_)/ else true)" | constant If ⇀ (SML) "!(if (_)/ then (_)/ else (_))" and (OCaml) "!(if (_)/ then (_)/ else (_))" and (Haskell) "!(if (_)/ then (_)/ else (_))" and (Scala) "!(if ((_))/ (_)/ else (_))" code_reserved SML not code_reserved OCaml not code_identifier code_module Pure ⇀ (SML) HOL and (OCaml) HOL and (Haskell) HOL and (Scala) HOL text ‹Using built-in Haskell equality.› code_printing type_class equal ⇀ (Haskell) "Eq" | constant HOL.equal ⇀ (Haskell) infix 4 "==" | constant HOL.eq ⇀ (Haskell) infix 4 "==" text ‹‹undefined›› code_printing constant undefined ⇀ (SML) "!(raise/ Fail/ \"undefined\")" and (OCaml) "failwith/ \"undefined\"" and (Haskell) "error/ \"undefined\"" and (Scala) "!sys.error(\"undefined\")" subsubsection ‹Evaluation and normalization by evaluation› method_setup eval = ‹ let fun eval_tac ctxt = let val conv = Code_Runtime.dynamic_holds_conv in CONVERSION (Conv.params_conv ~1 (Conv.concl_conv ~1 o conv) ctxt) THEN' resolve_tac ctxt [TrueI] end in Scan.succeed (SIMPLE_METHOD' o eval_tac) end › "solve goal by evaluation" method_setup normalization = ‹ Scan.succeed (fn ctxt => SIMPLE_METHOD' (CHANGED_PROP o (CONVERSION (Nbe.dynamic_conv ctxt) THEN_ALL_NEW (TRY o resolve_tac ctxt [TrueI])))) › "solve goal by normalization" subsection ‹Counterexample Search Units› subsubsection ‹Quickcheck› quickcheck_params [size = 5, iterations = 50] subsubsection ‹Nitpick setup› named_theorems nitpick_unfold "alternative definitions of constants as needed by Nitpick" and nitpick_simp "equational specification of constants as needed by Nitpick" and nitpick_psimp "partial equational specification of constants as needed by Nitpick" and nitpick_choice_spec "choice specification of constants as needed by Nitpick" declare if_bool_eq_conj [nitpick_unfold, no_atp] and if_bool_eq_disj [no_atp] subsection ‹Preprocessing for the predicate compiler› named_theorems code_pred_def "alternative definitions of constants for the Predicate Compiler" and code_pred_inline "inlining definitions for the Predicate Compiler" and code_pred_simp "simplification rules for the optimisations in the Predicate Compiler" subsection ‹Legacy tactics and ML bindings› ML ‹ (* combination of (spec RS spec RS ...(j times) ... spec RS mp) *) local fun wrong_prem (Const (\<^const_name>‹All›, _) $ Abs (_, _, t)) = wrong_prem t | wrong_prem (Bound _) = true | wrong_prem _ = false; val filter_right = filter (not o wrong_prem o HOLogic.dest_Trueprop o hd o Thm.prems_of); fun smp i = funpow i (fn m => filter_right ([spec] RL m)) [mp]; in fun smp_tac ctxt j = EVERY' [dresolve_tac ctxt (smp j), assume_tac ctxt]; end; local val nnf_ss = simpset_of (put_simpset HOL_basic_ss \<^context> addsimps @{thms simp_thms nnf_simps}); in fun nnf_conv ctxt = Simplifier.rewrite (put_simpset nnf_ss ctxt); end › hide_const (open) eq equal end