clasohm@923: (* Title: HOL/HOL.thy wenzelm@11750: Author: Tobias Nipkow, Markus Wenzel, and Larry Paulson wenzelm@11750: *) clasohm@923: wenzelm@58889: section {* The basis of Higher-Order Logic *} clasohm@923: nipkow@15131: theory HOL haftmann@30929: imports Pure "~~/src/Tools/Code_Generator" wenzelm@46950: keywords wenzelm@52432: "try" "solve_direct" "quickcheck" "print_coercions" "print_claset" wenzelm@52432: "print_induct_rules" :: diag and haftmann@47657: "quickcheck_params" :: thy_decl nipkow@15131: begin wenzelm@2260: wenzelm@48891: ML_file "~~/src/Tools/misc_legacy.ML" wenzelm@48891: ML_file "~~/src/Tools/try.ML" wenzelm@48891: ML_file "~~/src/Tools/quickcheck.ML" wenzelm@48891: ML_file "~~/src/Tools/solve_direct.ML" wenzelm@48891: ML_file "~~/src/Tools/IsaPlanner/zipper.ML" wenzelm@48891: ML_file "~~/src/Tools/IsaPlanner/isand.ML" wenzelm@48891: ML_file "~~/src/Tools/IsaPlanner/rw_inst.ML" wenzelm@48891: ML_file "~~/src/Provers/hypsubst.ML" wenzelm@48891: ML_file "~~/src/Provers/splitter.ML" wenzelm@48891: ML_file "~~/src/Provers/classical.ML" wenzelm@48891: ML_file "~~/src/Provers/blast.ML" wenzelm@48891: ML_file "~~/src/Provers/clasimp.ML" wenzelm@48891: ML_file "~~/src/Tools/eqsubst.ML" wenzelm@48891: ML_file "~~/src/Provers/quantifier1.ML" wenzelm@48891: ML_file "~~/src/Tools/atomize_elim.ML" wenzelm@48891: ML_file "~~/src/Tools/cong_tac.ML" wenzelm@58826: ML_file "~~/src/Tools/intuitionistic.ML" setup \Intuitionistic.method_setup @{binding iprover}\ wenzelm@48891: ML_file "~~/src/Tools/project_rule.ML" wenzelm@48891: ML_file "~~/src/Tools/subtyping.ML" wenzelm@48891: ML_file "~~/src/Tools/case_product.ML" wenzelm@48891: wenzelm@30165: wenzelm@58659: ML \Plugin_Name.declare_setup @{binding extraction}\ wenzelm@58659: wenzelm@58659: ML \ wenzelm@58659: Plugin_Name.declare_setup @{binding quickcheck_random}; wenzelm@58659: Plugin_Name.declare_setup @{binding quickcheck_exhaustive}; wenzelm@58659: Plugin_Name.declare_setup @{binding quickcheck_bounded_forall}; wenzelm@58659: Plugin_Name.declare_setup @{binding quickcheck_full_exhaustive}; wenzelm@58659: Plugin_Name.declare_setup @{binding quickcheck_narrowing}; wenzelm@58659: \ wenzelm@58659: ML \ wenzelm@58659: Plugin_Name.define_setup @{binding quickcheck} wenzelm@58659: [@{plugin quickcheck_exhaustive}, wenzelm@58659: @{plugin quickcheck_random}, wenzelm@58659: @{plugin quickcheck_bounded_forall}, wenzelm@58659: @{plugin quickcheck_full_exhaustive}, wenzelm@58659: @{plugin quickcheck_narrowing}] wenzelm@58659: \ wenzelm@58659: wenzelm@58659: wenzelm@11750: subsection {* Primitive logic *} wenzelm@11750: wenzelm@11750: subsubsection {* Core syntax *} wenzelm@2260: wenzelm@56941: setup {* Axclass.class_axiomatization (@{binding type}, []) *} wenzelm@36452: default_sort type wenzelm@35625: setup {* Object_Logic.add_base_sort @{sort type} *} haftmann@25460: wenzelm@55383: axiomatization where fun_arity: "OFCLASS('a \ 'b, type_class)" wenzelm@55383: instance "fun" :: (type, type) type by (rule fun_arity) wenzelm@55383: wenzelm@55383: axiomatization where itself_arity: "OFCLASS('a itself, type_class)" wenzelm@55383: instance itself :: (type) type by (rule itself_arity) haftmann@25460: wenzelm@7357: typedecl bool clasohm@923: wenzelm@11750: judgment wenzelm@11750: Trueprop :: "bool => prop" ("(_)" 5) clasohm@923: wenzelm@46973: axiomatization wenzelm@46973: implies :: "[bool, bool] => bool" (infixr "-->" 25) and wenzelm@46973: eq :: "['a, 'a] => bool" (infixl "=" 50) and wenzelm@46973: The :: "('a => bool) => 'a" wenzelm@46973: wenzelm@11750: consts wenzelm@7357: True :: bool wenzelm@7357: False :: bool haftmann@38547: Not :: "bool => bool" ("~ _" [40] 40) haftmann@38795: haftmann@38795: conj :: "[bool, bool] => bool" (infixr "&" 35) haftmann@38795: disj :: "[bool, bool] => bool" (infixr "|" 30) haftmann@38555: wenzelm@7357: All :: "('a => bool) => bool" (binder "ALL " 10) wenzelm@7357: Ex :: "('a => bool) => bool" (binder "EX " 10) wenzelm@7357: Ex1 :: "('a => bool) => bool" (binder "EX! " 10) clasohm@923: wenzelm@19656: wenzelm@11750: subsubsection {* Additional concrete syntax *} wenzelm@2260: wenzelm@21210: notation (output) haftmann@38864: eq (infix "=" 50) wenzelm@19656: wenzelm@19656: abbreviation wenzelm@21404: not_equal :: "['a, 'a] => bool" (infixl "~=" 50) where wenzelm@19656: "x ~= y == ~ (x = y)" wenzelm@19656: wenzelm@21210: notation (output) wenzelm@19656: not_equal (infix "~=" 50) wenzelm@19656: wenzelm@21210: notation (xsymbols) wenzelm@21404: Not ("\ _" [40] 40) and haftmann@38864: conj (infixr "\" 35) and haftmann@38864: disj (infixr "\" 30) and haftmann@38864: implies (infixr "\" 25) and nipkow@50360: not_equal (infixl "\" 50) nipkow@50360: nipkow@50360: notation (xsymbols output) wenzelm@19656: not_equal (infix "\" 50) wenzelm@19656: wenzelm@21210: notation (HTML output) wenzelm@21404: Not ("\ _" [40] 40) and haftmann@38864: conj (infixr "\" 35) and haftmann@38864: disj (infixr "\" 30) and wenzelm@19656: not_equal (infix "\" 50) wenzelm@19656: wenzelm@19656: abbreviation (iff) wenzelm@21404: iff :: "[bool, bool] => bool" (infixr "<->" 25) where wenzelm@19656: "A <-> B == A = B" wenzelm@19656: wenzelm@21210: notation (xsymbols) wenzelm@19656: iff (infixr "\" 25) wenzelm@19656: wenzelm@46973: syntax "_The" :: "[pttrn, bool] => 'a" ("(3THE _./ _)" [0, 10] 10) wenzelm@46973: translations "THE x. P" == "CONST The (%x. P)" wenzelm@46125: print_translation {* wenzelm@52143: [(@{const_syntax The}, fn _ => fn [Abs abs] => wenzelm@46125: let val (x, t) = Syntax_Trans.atomic_abs_tr' abs wenzelm@46125: in Syntax.const @{syntax_const "_The"} $ x $ t end)] wenzelm@46125: *} -- {* To avoid eta-contraction of body *} clasohm@923: wenzelm@46125: nonterminal letbinds and letbind clasohm@923: syntax wenzelm@7357: "_bind" :: "[pttrn, 'a] => letbind" ("(2_ =/ _)" 10) wenzelm@7357: "" :: "letbind => letbinds" ("_") wenzelm@7357: "_binds" :: "[letbind, letbinds] => letbinds" ("_;/ _") huffman@36363: "_Let" :: "[letbinds, 'a] => 'a" ("(let (_)/ in (_))" [0, 10] 10) clasohm@923: wenzelm@46125: nonterminal case_syn and cases_syn wenzelm@46125: syntax wenzelm@46125: "_case_syntax" :: "['a, cases_syn] => 'b" ("(case _ of/ _)" 10) wenzelm@46125: "_case1" :: "['a, 'b] => case_syn" ("(2_ =>/ _)" 10) wenzelm@46125: "" :: "case_syn => cases_syn" ("_") wenzelm@46125: "_case2" :: "[case_syn, cases_syn] => cases_syn" ("_/ | _") wenzelm@42057: syntax (xsymbols) wenzelm@46125: "_case1" :: "['a, 'b] => case_syn" ("(2_ \/ _)" 10) nipkow@13763: wenzelm@21524: notation (xsymbols) wenzelm@21524: All (binder "\" 10) and wenzelm@21524: Ex (binder "\" 10) and wenzelm@21524: Ex1 (binder "\!" 10) wenzelm@2372: wenzelm@21524: notation (HTML output) wenzelm@21524: All (binder "\" 10) and wenzelm@21524: Ex (binder "\" 10) and wenzelm@21524: Ex1 (binder "\!" 10) wenzelm@6340: wenzelm@21524: notation (HOL) wenzelm@21524: All (binder "! " 10) and wenzelm@21524: Ex (binder "? " 10) and wenzelm@21524: Ex1 (binder "?! " 10) wenzelm@7238: wenzelm@7238: wenzelm@11750: subsubsection {* Axioms and basic definitions *} wenzelm@2260: wenzelm@46973: axiomatization where wenzelm@46973: refl: "t = (t::'a)" and wenzelm@46973: subst: "s = t \ P s \ P t" and wenzelm@46973: ext: "(!!x::'a. (f x ::'b) = g x) ==> (%x. f x) = (%x. g x)" paulson@15380: -- {*Extensionality is built into the meta-logic, and this rule expresses paulson@15380: a related property. It is an eta-expanded version of the traditional wenzelm@46973: rule, and similar to the ABS rule of HOL*} and paulson@6289: wenzelm@11432: the_eq_trivial: "(THE x. x = a) = (a::'a)" clasohm@923: wenzelm@46973: axiomatization where wenzelm@46973: impI: "(P ==> Q) ==> P-->Q" and wenzelm@46973: mp: "[| P-->Q; P |] ==> Q" and paulson@15380: wenzelm@46973: iff: "(P-->Q) --> (Q-->P) --> (P=Q)" and wenzelm@46973: True_or_False: "(P=True) | (P=False)" paulson@15380: clasohm@923: defs wenzelm@7357: True_def: "True == ((%x::bool. x) = (%x. x))" wenzelm@7357: All_def: "All(P) == (P = (%x. True))" paulson@11451: Ex_def: "Ex(P) == !Q. (!x. P x --> Q) --> Q" wenzelm@7357: False_def: "False == (!P. P)" wenzelm@7357: not_def: "~ P == P-->False" wenzelm@7357: and_def: "P & Q == !R. (P-->Q-->R) --> R" wenzelm@7357: or_def: "P | Q == !R. (P-->R) --> (Q-->R) --> R" wenzelm@7357: Ex1_def: "Ex1(P) == ? x. P(x) & (! y. P(y) --> y=x)" clasohm@923: wenzelm@46973: definition If :: "bool \ 'a \ 'a \ 'a" ("(if (_)/ then (_)/ else (_))" [0, 0, 10] 10) wenzelm@46973: where "If P x y \ (THE z::'a. (P=True --> z=x) & (P=False --> z=y))" clasohm@923: wenzelm@46973: definition Let :: "'a \ ('a \ 'b) \ 'b" wenzelm@46973: where "Let s f \ f s" haftmann@38525: haftmann@38525: translations haftmann@38525: "_Let (_binds b bs) e" == "_Let b (_Let bs e)" haftmann@38525: "let x = a in e" == "CONST Let a (%x. e)" haftmann@38525: wenzelm@46973: axiomatization undefined :: 'a haftmann@22481: wenzelm@46973: class default = fixes default :: 'a wenzelm@4868: wenzelm@11750: haftmann@20944: subsection {* Fundamental rules *} haftmann@20944: haftmann@20973: subsubsection {* Equality *} haftmann@20944: wenzelm@18457: lemma sym: "s = t ==> t = s" wenzelm@18457: by (erule subst) (rule refl) paulson@15411: wenzelm@18457: lemma ssubst: "t = s ==> P s ==> P t" wenzelm@18457: by (drule sym) (erule subst) paulson@15411: paulson@15411: lemma trans: "[| r=s; s=t |] ==> r=t" wenzelm@18457: by (erule subst) paulson@15411: wenzelm@40715: lemma trans_sym [Pure.elim?]: "r = s ==> t = s ==> r = t" wenzelm@40715: by (rule trans [OF _ sym]) wenzelm@40715: wenzelm@58826: lemma meta_eq_to_obj_eq: haftmann@20944: assumes meq: "A == B" haftmann@20944: shows "A = B" haftmann@20944: by (unfold meq) (rule refl) paulson@15411: wenzelm@21502: text {* Useful with @{text erule} for proving equalities from known equalities. *} haftmann@20944: (* a = b paulson@15411: | | paulson@15411: c = d *) paulson@15411: lemma box_equals: "[| a=b; a=c; b=d |] ==> c=d" paulson@15411: apply (rule trans) paulson@15411: apply (rule trans) paulson@15411: apply (rule sym) paulson@15411: apply assumption+ paulson@15411: done paulson@15411: nipkow@15524: text {* For calculational reasoning: *} nipkow@15524: nipkow@15524: lemma forw_subst: "a = b ==> P b ==> P a" nipkow@15524: by (rule ssubst) nipkow@15524: nipkow@15524: lemma back_subst: "P a ==> a = b ==> P b" nipkow@15524: by (rule subst) nipkow@15524: paulson@15411: wenzelm@32733: subsubsection {* Congruence rules for application *} paulson@15411: wenzelm@32733: text {* Similar to @{text AP_THM} in Gordon's HOL. *} paulson@15411: lemma fun_cong: "(f::'a=>'b) = g ==> f(x)=g(x)" paulson@15411: apply (erule subst) paulson@15411: apply (rule refl) paulson@15411: done paulson@15411: wenzelm@32733: text {* Similar to @{text AP_TERM} in Gordon's HOL and FOL's @{text subst_context}. *} paulson@15411: lemma arg_cong: "x=y ==> f(x)=f(y)" paulson@15411: apply (erule subst) paulson@15411: apply (rule refl) paulson@15411: done paulson@15411: paulson@15655: lemma arg_cong2: "\ a = b; c = d \ \ f a c = f b d" paulson@15655: apply (erule ssubst)+ paulson@15655: apply (rule refl) paulson@15655: done paulson@15655: wenzelm@32733: lemma cong: "[| f = g; (x::'a) = y |] ==> f x = g y" paulson@15411: apply (erule subst)+ paulson@15411: apply (rule refl) paulson@15411: done paulson@15411: wenzelm@58956: ML {* fun cong_tac ctxt = Cong_Tac.cong_tac ctxt @{thm cong} *} paulson@15411: wenzelm@32733: wenzelm@32733: subsubsection {* Equality of booleans -- iff *} paulson@15411: wenzelm@21504: lemma iffI: assumes "P ==> Q" and "Q ==> P" shows "P=Q" wenzelm@21504: by (iprover intro: iff [THEN mp, THEN mp] impI assms) paulson@15411: paulson@15411: lemma iffD2: "[| P=Q; Q |] ==> P" wenzelm@18457: by (erule ssubst) paulson@15411: paulson@15411: lemma rev_iffD2: "[| Q; P=Q |] ==> P" wenzelm@18457: by (erule iffD2) paulson@15411: wenzelm@21504: lemma iffD1: "Q = P \ Q \ P" wenzelm@21504: by (drule sym) (rule iffD2) wenzelm@21504: wenzelm@21504: lemma rev_iffD1: "Q \ Q = P \ P" wenzelm@21504: by (drule sym) (rule rev_iffD2) paulson@15411: paulson@15411: lemma iffE: paulson@15411: assumes major: "P=Q" wenzelm@21504: and minor: "[| P --> Q; Q --> P |] ==> R" wenzelm@18457: shows R wenzelm@18457: by (iprover intro: minor impI major [THEN iffD2] major [THEN iffD1]) paulson@15411: paulson@15411: haftmann@20944: subsubsection {*True*} paulson@15411: paulson@15411: lemma TrueI: "True" wenzelm@21504: unfolding True_def by (rule refl) paulson@15411: wenzelm@21504: lemma eqTrueI: "P ==> P = True" wenzelm@18457: by (iprover intro: iffI TrueI) paulson@15411: wenzelm@21504: lemma eqTrueE: "P = True ==> P" wenzelm@21504: by (erule iffD2) (rule TrueI) paulson@15411: paulson@15411: haftmann@20944: subsubsection {*Universal quantifier*} paulson@15411: wenzelm@21504: lemma allI: assumes "!!x::'a. P(x)" shows "ALL x. P(x)" wenzelm@21504: unfolding All_def by (iprover intro: ext eqTrueI assms) paulson@15411: paulson@15411: lemma spec: "ALL x::'a. P(x) ==> P(x)" paulson@15411: apply (unfold All_def) paulson@15411: apply (rule eqTrueE) paulson@15411: apply (erule fun_cong) paulson@15411: done paulson@15411: paulson@15411: lemma allE: paulson@15411: assumes major: "ALL x. P(x)" wenzelm@21504: and minor: "P(x) ==> R" wenzelm@21504: shows R wenzelm@21504: by (iprover intro: minor major [THEN spec]) paulson@15411: paulson@15411: lemma all_dupE: paulson@15411: assumes major: "ALL x. P(x)" wenzelm@21504: and minor: "[| P(x); ALL x. P(x) |] ==> R" wenzelm@21504: shows R wenzelm@21504: by (iprover intro: minor major major [THEN spec]) paulson@15411: paulson@15411: wenzelm@21504: subsubsection {* False *} wenzelm@21504: wenzelm@21504: text {* wenzelm@21504: Depends upon @{text spec}; it is impossible to do propositional wenzelm@21504: logic before quantifiers! wenzelm@21504: *} paulson@15411: paulson@15411: lemma FalseE: "False ==> P" wenzelm@21504: apply (unfold False_def) wenzelm@21504: apply (erule spec) wenzelm@21504: done paulson@15411: wenzelm@21504: lemma False_neq_True: "False = True ==> P" wenzelm@21504: by (erule eqTrueE [THEN FalseE]) paulson@15411: paulson@15411: wenzelm@21504: subsubsection {* Negation *} paulson@15411: paulson@15411: lemma notI: wenzelm@21504: assumes "P ==> False" paulson@15411: shows "~P" wenzelm@21504: apply (unfold not_def) wenzelm@21504: apply (iprover intro: impI assms) wenzelm@21504: done paulson@15411: paulson@15411: lemma False_not_True: "False ~= True" wenzelm@21504: apply (rule notI) wenzelm@21504: apply (erule False_neq_True) wenzelm@21504: done paulson@15411: paulson@15411: lemma True_not_False: "True ~= False" wenzelm@21504: apply (rule notI) wenzelm@21504: apply (drule sym) wenzelm@21504: apply (erule False_neq_True) wenzelm@21504: done paulson@15411: paulson@15411: lemma notE: "[| ~P; P |] ==> R" wenzelm@21504: apply (unfold not_def) wenzelm@21504: apply (erule mp [THEN FalseE]) wenzelm@21504: apply assumption wenzelm@21504: done paulson@15411: wenzelm@21504: lemma notI2: "(P \ \ Pa) \ (P \ Pa) \ \ P" wenzelm@21504: by (erule notE [THEN notI]) (erule meta_mp) paulson@15411: paulson@15411: haftmann@20944: subsubsection {*Implication*} paulson@15411: paulson@15411: lemma impE: paulson@15411: assumes "P-->Q" "P" "Q ==> R" paulson@15411: shows "R" wenzelm@23553: by (iprover intro: assms mp) paulson@15411: paulson@15411: (* Reduces Q to P-->Q, allowing substitution in P. *) paulson@15411: lemma rev_mp: "[| P; P --> Q |] ==> Q" nipkow@17589: by (iprover intro: mp) paulson@15411: paulson@15411: lemma contrapos_nn: paulson@15411: assumes major: "~Q" paulson@15411: and minor: "P==>Q" paulson@15411: shows "~P" nipkow@17589: by (iprover intro: notI minor major [THEN notE]) paulson@15411: paulson@15411: (*not used at all, but we already have the other 3 combinations *) paulson@15411: lemma contrapos_pn: paulson@15411: assumes major: "Q" paulson@15411: and minor: "P ==> ~Q" paulson@15411: shows "~P" nipkow@17589: by (iprover intro: notI minor major notE) paulson@15411: paulson@15411: lemma not_sym: "t ~= s ==> s ~= t" haftmann@21250: by (erule contrapos_nn) (erule sym) haftmann@21250: haftmann@21250: lemma eq_neq_eq_imp_neq: "[| x = a ; a ~= b; b = y |] ==> x ~= y" haftmann@21250: by (erule subst, erule ssubst, assumption) paulson@15411: paulson@15411: haftmann@20944: subsubsection {*Existential quantifier*} paulson@15411: paulson@15411: lemma exI: "P x ==> EX x::'a. P x" paulson@15411: apply (unfold Ex_def) nipkow@17589: apply (iprover intro: allI allE impI mp) paulson@15411: done paulson@15411: paulson@15411: lemma exE: paulson@15411: assumes major: "EX x::'a. P(x)" paulson@15411: and minor: "!!x. P(x) ==> Q" paulson@15411: shows "Q" paulson@15411: apply (rule major [unfolded Ex_def, THEN spec, THEN mp]) nipkow@17589: apply (iprover intro: impI [THEN allI] minor) paulson@15411: done paulson@15411: paulson@15411: haftmann@20944: subsubsection {*Conjunction*} paulson@15411: paulson@15411: lemma conjI: "[| P; Q |] ==> P&Q" paulson@15411: apply (unfold and_def) nipkow@17589: apply (iprover intro: impI [THEN allI] mp) paulson@15411: done paulson@15411: paulson@15411: lemma conjunct1: "[| P & Q |] ==> P" paulson@15411: apply (unfold and_def) nipkow@17589: apply (iprover intro: impI dest: spec mp) paulson@15411: done paulson@15411: paulson@15411: lemma conjunct2: "[| P & Q |] ==> Q" paulson@15411: apply (unfold and_def) nipkow@17589: apply (iprover intro: impI dest: spec mp) paulson@15411: done paulson@15411: paulson@15411: lemma conjE: paulson@15411: assumes major: "P&Q" paulson@15411: and minor: "[| P; Q |] ==> R" paulson@15411: shows "R" paulson@15411: apply (rule minor) paulson@15411: apply (rule major [THEN conjunct1]) paulson@15411: apply (rule major [THEN conjunct2]) paulson@15411: done paulson@15411: paulson@15411: lemma context_conjI: wenzelm@23553: assumes "P" "P ==> Q" shows "P & Q" wenzelm@23553: by (iprover intro: conjI assms) paulson@15411: paulson@15411: haftmann@20944: subsubsection {*Disjunction*} paulson@15411: paulson@15411: lemma disjI1: "P ==> P|Q" paulson@15411: apply (unfold or_def) nipkow@17589: apply (iprover intro: allI impI mp) paulson@15411: done paulson@15411: paulson@15411: lemma disjI2: "Q ==> P|Q" paulson@15411: apply (unfold or_def) nipkow@17589: apply (iprover intro: allI impI mp) paulson@15411: done paulson@15411: paulson@15411: lemma disjE: paulson@15411: assumes major: "P|Q" paulson@15411: and minorP: "P ==> R" paulson@15411: and minorQ: "Q ==> R" paulson@15411: shows "R" nipkow@17589: by (iprover intro: minorP minorQ impI paulson@15411: major [unfolded or_def, THEN spec, THEN mp, THEN mp]) paulson@15411: paulson@15411: haftmann@20944: subsubsection {*Classical logic*} paulson@15411: paulson@15411: lemma classical: paulson@15411: assumes prem: "~P ==> P" paulson@15411: shows "P" paulson@15411: apply (rule True_or_False [THEN disjE, THEN eqTrueE]) paulson@15411: apply assumption paulson@15411: apply (rule notI [THEN prem, THEN eqTrueI]) paulson@15411: apply (erule subst) paulson@15411: apply assumption paulson@15411: done paulson@15411: wenzelm@45607: lemmas ccontr = FalseE [THEN classical] paulson@15411: paulson@15411: (*notE with premises exchanged; it discharges ~R so that it can be used to paulson@15411: make elimination rules*) paulson@15411: lemma rev_notE: paulson@15411: assumes premp: "P" paulson@15411: and premnot: "~R ==> ~P" paulson@15411: shows "R" paulson@15411: apply (rule ccontr) paulson@15411: apply (erule notE [OF premnot premp]) paulson@15411: done paulson@15411: paulson@15411: (*Double negation law*) paulson@15411: lemma notnotD: "~~P ==> P" paulson@15411: apply (rule classical) paulson@15411: apply (erule notE) paulson@15411: apply assumption paulson@15411: done paulson@15411: paulson@15411: lemma contrapos_pp: paulson@15411: assumes p1: "Q" paulson@15411: and p2: "~P ==> ~Q" paulson@15411: shows "P" nipkow@17589: by (iprover intro: classical p1 p2 notE) paulson@15411: paulson@15411: haftmann@20944: subsubsection {*Unique existence*} paulson@15411: paulson@15411: lemma ex1I: wenzelm@23553: assumes "P a" "!!x. P(x) ==> x=a" paulson@15411: shows "EX! x. P(x)" wenzelm@23553: by (unfold Ex1_def, iprover intro: assms exI conjI allI impI) paulson@15411: paulson@15411: text{*Sometimes easier to use: the premises have no shared variables. Safe!*} paulson@15411: lemma ex_ex1I: paulson@15411: assumes ex_prem: "EX x. P(x)" paulson@15411: and eq: "!!x y. [| P(x); P(y) |] ==> x=y" paulson@15411: shows "EX! x. P(x)" nipkow@17589: by (iprover intro: ex_prem [THEN exE] ex1I eq) paulson@15411: paulson@15411: lemma ex1E: paulson@15411: assumes major: "EX! x. P(x)" paulson@15411: and minor: "!!x. [| P(x); ALL y. P(y) --> y=x |] ==> R" paulson@15411: shows "R" paulson@15411: apply (rule major [unfolded Ex1_def, THEN exE]) paulson@15411: apply (erule conjE) nipkow@17589: apply (iprover intro: minor) paulson@15411: done paulson@15411: paulson@15411: lemma ex1_implies_ex: "EX! x. P x ==> EX x. P x" paulson@15411: apply (erule ex1E) paulson@15411: apply (rule exI) paulson@15411: apply assumption paulson@15411: done paulson@15411: paulson@15411: haftmann@20944: subsubsection {*Classical intro rules for disjunction and existential quantifiers*} paulson@15411: paulson@15411: lemma disjCI: paulson@15411: assumes "~Q ==> P" shows "P|Q" paulson@15411: apply (rule classical) wenzelm@23553: apply (iprover intro: assms disjI1 disjI2 notI elim: notE) paulson@15411: done paulson@15411: paulson@15411: lemma excluded_middle: "~P | P" nipkow@17589: by (iprover intro: disjCI) paulson@15411: haftmann@20944: text {* haftmann@20944: case distinction as a natural deduction rule. haftmann@20944: Note that @{term "~P"} is the second case, not the first haftmann@20944: *} wenzelm@27126: lemma case_split [case_names True False]: paulson@15411: assumes prem1: "P ==> Q" paulson@15411: and prem2: "~P ==> Q" paulson@15411: shows "Q" paulson@15411: apply (rule excluded_middle [THEN disjE]) paulson@15411: apply (erule prem2) paulson@15411: apply (erule prem1) paulson@15411: done wenzelm@27126: paulson@15411: (*Classical implies (-->) elimination. *) paulson@15411: lemma impCE: paulson@15411: assumes major: "P-->Q" paulson@15411: and minor: "~P ==> R" "Q ==> R" paulson@15411: shows "R" paulson@15411: apply (rule excluded_middle [of P, THEN disjE]) nipkow@17589: apply (iprover intro: minor major [THEN mp])+ paulson@15411: done paulson@15411: paulson@15411: (*This version of --> elimination works on Q before P. It works best for paulson@15411: those cases in which P holds "almost everywhere". Can't install as paulson@15411: default: would break old proofs.*) paulson@15411: lemma impCE': paulson@15411: assumes major: "P-->Q" paulson@15411: and minor: "Q ==> R" "~P ==> R" paulson@15411: shows "R" paulson@15411: apply (rule excluded_middle [of P, THEN disjE]) nipkow@17589: apply (iprover intro: minor major [THEN mp])+ paulson@15411: done paulson@15411: paulson@15411: (*Classical <-> elimination. *) paulson@15411: lemma iffCE: paulson@15411: assumes major: "P=Q" paulson@15411: and minor: "[| P; Q |] ==> R" "[| ~P; ~Q |] ==> R" paulson@15411: shows "R" paulson@15411: apply (rule major [THEN iffE]) nipkow@17589: apply (iprover intro: minor elim: impCE notE) paulson@15411: done paulson@15411: paulson@15411: lemma exCI: paulson@15411: assumes "ALL x. ~P(x) ==> P(a)" paulson@15411: shows "EX x. P(x)" paulson@15411: apply (rule ccontr) wenzelm@23553: apply (iprover intro: assms exI allI notI notE [of "\x. P x"]) paulson@15411: done paulson@15411: paulson@15411: wenzelm@12386: subsubsection {* Intuitionistic Reasoning *} wenzelm@12386: wenzelm@12386: lemma impE': wenzelm@12937: assumes 1: "P --> Q" wenzelm@12937: and 2: "Q ==> R" wenzelm@12937: and 3: "P --> Q ==> P" wenzelm@12937: shows R wenzelm@12386: proof - wenzelm@12386: from 3 and 1 have P . wenzelm@12386: with 1 have Q by (rule impE) wenzelm@12386: with 2 show R . wenzelm@12386: qed wenzelm@12386: wenzelm@12386: lemma allE': wenzelm@12937: assumes 1: "ALL x. P x" wenzelm@12937: and 2: "P x ==> ALL x. P x ==> Q" wenzelm@12937: shows Q wenzelm@12386: proof - wenzelm@12386: from 1 have "P x" by (rule spec) wenzelm@12386: from this and 1 show Q by (rule 2) wenzelm@12386: qed wenzelm@12386: wenzelm@12937: lemma notE': wenzelm@12937: assumes 1: "~ P" wenzelm@12937: and 2: "~ P ==> P" wenzelm@12937: shows R wenzelm@12386: proof - wenzelm@12386: from 2 and 1 have P . wenzelm@12386: with 1 show R by (rule notE) wenzelm@12386: qed wenzelm@12386: dixon@22444: lemma TrueE: "True ==> P ==> P" . dixon@22444: lemma notFalseE: "~ False ==> P ==> P" . dixon@22444: dixon@22467: lemmas [Pure.elim!] = disjE iffE FalseE conjE exE TrueE notFalseE wenzelm@15801: and [Pure.intro!] = iffI conjI impI TrueI notI allI refl wenzelm@15801: and [Pure.elim 2] = allE notE' impE' wenzelm@15801: and [Pure.intro] = exI disjI2 disjI1 wenzelm@12386: wenzelm@12386: lemmas [trans] = trans wenzelm@12386: and [sym] = sym not_sym wenzelm@15801: and [Pure.elim?] = iffD1 iffD2 impE wenzelm@11750: wenzelm@11438: wenzelm@11750: subsubsection {* Atomizing meta-level connectives *} wenzelm@11750: haftmann@28513: axiomatization where haftmann@28513: eq_reflection: "x = y \ x \ y" (*admissible axiom*) haftmann@28513: wenzelm@11750: lemma atomize_all [atomize]: "(!!x. P x) == Trueprop (ALL x. P x)" wenzelm@12003: proof wenzelm@9488: assume "!!x. P x" wenzelm@23389: then show "ALL x. P x" .. wenzelm@9488: next wenzelm@9488: assume "ALL x. P x" wenzelm@23553: then show "!!x. P x" by (rule allE) wenzelm@9488: qed wenzelm@9488: wenzelm@11750: lemma atomize_imp [atomize]: "(A ==> B) == Trueprop (A --> B)" wenzelm@12003: proof wenzelm@9488: assume r: "A ==> B" wenzelm@10383: show "A --> B" by (rule impI) (rule r) wenzelm@9488: next wenzelm@9488: assume "A --> B" and A wenzelm@23553: then show B by (rule mp) wenzelm@9488: qed wenzelm@9488: paulson@14749: lemma atomize_not: "(A ==> False) == Trueprop (~A)" paulson@14749: proof paulson@14749: assume r: "A ==> False" paulson@14749: show "~A" by (rule notI) (rule r) paulson@14749: next paulson@14749: assume "~A" and A wenzelm@23553: then show False by (rule notE) paulson@14749: qed paulson@14749: haftmann@39566: lemma atomize_eq [atomize, code]: "(x == y) == Trueprop (x = y)" wenzelm@12003: proof wenzelm@10432: assume "x == y" wenzelm@23553: show "x = y" by (unfold `x == y`) (rule refl) wenzelm@10432: next wenzelm@10432: assume "x = y" wenzelm@23553: then show "x == y" by (rule eq_reflection) wenzelm@10432: qed wenzelm@10432: wenzelm@28856: lemma atomize_conj [atomize]: "(A &&& B) == Trueprop (A & B)" wenzelm@12003: proof wenzelm@28856: assume conj: "A &&& B" wenzelm@19121: show "A & B" wenzelm@19121: proof (rule conjI) wenzelm@19121: from conj show A by (rule conjunctionD1) wenzelm@19121: from conj show B by (rule conjunctionD2) wenzelm@19121: qed wenzelm@11953: next wenzelm@19121: assume conj: "A & B" wenzelm@28856: show "A &&& B" wenzelm@19121: proof - wenzelm@19121: from conj show A .. wenzelm@19121: from conj show B .. wenzelm@11953: qed wenzelm@11953: qed wenzelm@11953: wenzelm@12386: lemmas [symmetric, rulify] = atomize_all atomize_imp wenzelm@18832: and [symmetric, defn] = atomize_all atomize_imp atomize_eq wenzelm@12386: wenzelm@11750: krauss@26580: subsubsection {* Atomizing elimination rules *} krauss@26580: krauss@26580: lemma atomize_exL[atomize_elim]: "(!!x. P x ==> Q) == ((EX x. P x) ==> Q)" krauss@26580: by rule iprover+ krauss@26580: krauss@26580: lemma atomize_conjL[atomize_elim]: "(A ==> B ==> C) == (A & B ==> C)" krauss@26580: by rule iprover+ krauss@26580: krauss@26580: lemma atomize_disjL[atomize_elim]: "((A ==> C) ==> (B ==> C) ==> C) == ((A | B ==> C) ==> C)" krauss@26580: by rule iprover+ krauss@26580: krauss@26580: lemma atomize_elimL[atomize_elim]: "(!!B. (A ==> B) ==> B) == Trueprop A" .. krauss@26580: krauss@26580: haftmann@20944: subsection {* Package setup *} haftmann@20944: wenzelm@51314: ML_file "Tools/hologic.ML" wenzelm@51314: wenzelm@51314: blanchet@35828: subsubsection {* Sledgehammer setup *} blanchet@35828: blanchet@35828: text {* blanchet@35828: Theorems blacklisted to Sledgehammer. These theorems typically produce clauses blanchet@35828: that are prolific (match too many equality or membership literals) and relate to blanchet@35828: seldom-used facts. Some duplicate other rules. blanchet@35828: *} blanchet@35828: wenzelm@57963: named_theorems no_atp "theorems that should be filtered out by Sledgehammer" blanchet@35828: blanchet@35828: wenzelm@11750: subsubsection {* Classical Reasoner setup *} wenzelm@9529: wenzelm@26411: lemma imp_elim: "P --> Q ==> (~ R ==> P) ==> (Q ==> R) ==> R" wenzelm@26411: by (rule classical) iprover wenzelm@26411: wenzelm@26411: lemma swap: "~ P ==> (~ R ==> P) ==> R" wenzelm@26411: by (rule classical) iprover wenzelm@26411: haftmann@20944: lemma thin_refl: haftmann@20944: "\X. \ x=x; PROP W \ \ PROP W" . haftmann@20944: haftmann@21151: ML {* wenzelm@42799: structure Hypsubst = Hypsubst wenzelm@42799: ( wenzelm@21218: val dest_eq = HOLogic.dest_eq haftmann@21151: val dest_Trueprop = HOLogic.dest_Trueprop haftmann@21151: val dest_imp = HOLogic.dest_imp wenzelm@26411: val eq_reflection = @{thm eq_reflection} wenzelm@26411: val rev_eq_reflection = @{thm meta_eq_to_obj_eq} wenzelm@26411: val imp_intr = @{thm impI} wenzelm@26411: val rev_mp = @{thm rev_mp} wenzelm@26411: val subst = @{thm subst} wenzelm@26411: val sym = @{thm sym} wenzelm@22129: val thin_refl = @{thm thin_refl}; wenzelm@42799: ); wenzelm@21671: open Hypsubst; haftmann@21151: wenzelm@42799: structure Classical = Classical wenzelm@42799: ( wenzelm@26411: val imp_elim = @{thm imp_elim} wenzelm@26411: val not_elim = @{thm notE} wenzelm@26411: val swap = @{thm swap} wenzelm@26411: val classical = @{thm classical} haftmann@21151: val sizef = Drule.size_of_thm haftmann@21151: val hyp_subst_tacs = [Hypsubst.hyp_subst_tac] wenzelm@42799: ); haftmann@21151: wenzelm@58826: structure Basic_Classical: BASIC_CLASSICAL = Classical; wenzelm@33308: open Basic_Classical; wenzelm@43560: *} wenzelm@22129: haftmann@21009: setup {* wenzelm@35389: (*prevent substitution on bool*) wenzelm@58826: let wenzelm@58826: fun non_bool_eq (@{const_name HOL.eq}, Type (_, [T, _])) = T <> @{typ bool} wenzelm@58826: | non_bool_eq _ = false; wenzelm@58826: fun hyp_subst_tac' ctxt = wenzelm@58826: SUBGOAL (fn (goal, i) => wenzelm@58826: if Term.exists_Const non_bool_eq goal wenzelm@58826: then Hypsubst.hyp_subst_tac ctxt i wenzelm@58826: else no_tac); wenzelm@58826: in wenzelm@58826: Context_Rules.addSWrapper (fn ctxt => fn tac => hyp_subst_tac' ctxt ORELSE' tac) wenzelm@58826: end haftmann@21009: *} haftmann@21009: haftmann@21009: declare iffI [intro!] haftmann@21009: and notI [intro!] haftmann@21009: and impI [intro!] haftmann@21009: and disjCI [intro!] haftmann@21009: and conjI [intro!] haftmann@21009: and TrueI [intro!] haftmann@21009: and refl [intro!] haftmann@21009: haftmann@21009: declare iffCE [elim!] haftmann@21009: and FalseE [elim!] haftmann@21009: and impCE [elim!] haftmann@21009: and disjE [elim!] haftmann@21009: and conjE [elim!] haftmann@21009: haftmann@21009: declare ex_ex1I [intro!] haftmann@21009: and allI [intro!] haftmann@21009: and exI [intro] haftmann@21009: haftmann@21009: declare exE [elim!] haftmann@21009: allE [elim] haftmann@21009: wenzelm@51687: ML {* val HOL_cs = claset_of @{context} *} mengj@19162: wenzelm@20223: lemma contrapos_np: "~ Q ==> (~ P ==> Q) ==> P" wenzelm@20223: apply (erule swap) wenzelm@20223: apply (erule (1) meta_mp) wenzelm@20223: done wenzelm@10383: wenzelm@18689: declare ex_ex1I [rule del, intro! 2] wenzelm@18689: and ex1I [intro] wenzelm@18689: paulson@41865: declare ext [intro] paulson@41865: wenzelm@12386: lemmas [intro?] = ext wenzelm@12386: and [elim?] = ex1_implies_ex wenzelm@11977: haftmann@20944: (*Better then ex1E for classical reasoner: needs no quantifier duplication!*) haftmann@20973: lemma alt_ex1E [elim!]: haftmann@20944: assumes major: "\!x. P x" haftmann@20944: and prem: "\x. \ P x; \y y'. P y \ P y' \ y = y' \ \ R" haftmann@20944: shows R haftmann@20944: apply (rule ex1E [OF major]) haftmann@20944: apply (rule prem) wenzelm@59499: apply assumption wenzelm@59499: apply (rule allI)+ wenzelm@59498: apply (tactic {* eresolve_tac @{context} [Classical.dup_elim NONE @{thm allE}] 1 *}) wenzelm@22129: apply iprover wenzelm@22129: done haftmann@20944: haftmann@21151: ML {* wenzelm@42477: structure Blast = Blast wenzelm@42477: ( wenzelm@42477: structure Classical = Classical wenzelm@42802: val Trueprop_const = dest_Const @{const Trueprop} wenzelm@42477: val equality_name = @{const_name HOL.eq} wenzelm@42477: val not_name = @{const_name Not} wenzelm@42477: val notE = @{thm notE} wenzelm@42477: val ccontr = @{thm ccontr} wenzelm@42477: val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac wenzelm@42477: ); wenzelm@42477: val blast_tac = Blast.blast_tac; haftmann@20944: *} haftmann@20944: haftmann@20944: lp15@59504: subsubsection {*THE: definite description operator*} lp15@59504: lp15@59504: lemma the_equality [intro]: lp15@59504: assumes "P a" lp15@59504: and "!!x. P x ==> x=a" lp15@59504: shows "(THE x. P x) = a" lp15@59504: by (blast intro: assms trans [OF arg_cong [where f=The] the_eq_trivial]) lp15@59504: lp15@59504: lemma theI: lp15@59504: assumes "P a" and "!!x. P x ==> x=a" lp15@59504: shows "P (THE x. P x)" lp15@59504: by (iprover intro: assms the_equality [THEN ssubst]) lp15@59504: lp15@59504: lemma theI': "EX! x. P x ==> P (THE x. P x)" lp15@59504: by (blast intro: theI) lp15@59504: lp15@59504: (*Easier to apply than theI: only one occurrence of P*) lp15@59504: lemma theI2: lp15@59504: assumes "P a" "!!x. P x ==> x=a" "!!x. P x ==> Q x" lp15@59504: shows "Q (THE x. P x)" lp15@59504: by (iprover intro: assms theI) lp15@59504: lp15@59504: lemma the1I2: assumes "EX! x. P x" "\x. P x \ Q x" shows "Q (THE x. P x)" lp15@59504: by(iprover intro:assms(2) theI2[where P=P and Q=Q] ex1E[OF assms(1)] lp15@59504: elim:allE impE) lp15@59504: lp15@59504: lemma the1_equality [elim?]: "[| EX!x. P x; P a |] ==> (THE x. P x) = a" lp15@59504: by blast lp15@59504: lp15@59504: lemma the_sym_eq_trivial: "(THE y. x=y) = x" lp15@59504: by blast lp15@59504: lp15@59504: haftmann@20944: subsubsection {* Simplifier *} wenzelm@12281: wenzelm@12281: lemma eta_contract_eq: "(%s. f s) = f" .. wenzelm@12281: wenzelm@12281: lemma simp_thms: wenzelm@12937: shows not_not: "(~ ~ P) = P" nipkow@15354: and Not_eq_iff: "((~P) = (~Q)) = (P = Q)" wenzelm@12937: and berghofe@12436: "(P ~= Q) = (P = (~Q))" berghofe@12436: "(P | ~P) = True" "(~P | P) = True" wenzelm@12281: "(x = x) = True" haftmann@32068: and not_True_eq_False [code]: "(\ True) = False" haftmann@32068: and not_False_eq_True [code]: "(\ False) = True" haftmann@20944: and berghofe@12436: "(~P) ~= P" "P ~= (~P)" haftmann@20944: "(True=P) = P" haftmann@20944: and eq_True: "(P = True) = P" haftmann@20944: and "(False=P) = (~P)" haftmann@20944: and eq_False: "(P = False) = (\ P)" haftmann@20944: and wenzelm@12281: "(True --> P) = P" "(False --> P) = True" wenzelm@12281: "(P --> True) = True" "(P --> P) = True" wenzelm@12281: "(P --> False) = (~P)" "(P --> ~P) = (~P)" wenzelm@12281: "(P & True) = P" "(True & P) = P" wenzelm@12281: "(P & False) = False" "(False & P) = False" wenzelm@12281: "(P & P) = P" "(P & (P & Q)) = (P & Q)" wenzelm@12281: "(P & ~P) = False" "(~P & P) = False" wenzelm@12281: "(P | True) = True" "(True | P) = True" wenzelm@12281: "(P | False) = P" "(False | P) = P" berghofe@12436: "(P | P) = P" "(P | (P | Q)) = (P | Q)" and wenzelm@12281: "(ALL x. P) = P" "(EX x. P) = P" "EX x. x=t" "EX x. t=x" nipkow@31166: and wenzelm@12281: "!!P. (EX x. x=t & P(x)) = P(t)" wenzelm@12281: "!!P. (EX x. t=x & P(x)) = P(t)" wenzelm@12281: "!!P. (ALL x. x=t --> P(x)) = P(t)" wenzelm@12937: "!!P. (ALL x. t=x --> P(x)) = P(t)" nipkow@17589: by (blast, blast, blast, blast, blast, iprover+) wenzelm@13421: paulson@14201: lemma disj_absorb: "(A | A) = A" paulson@14201: by blast paulson@14201: paulson@14201: lemma disj_left_absorb: "(A | (A | B)) = (A | B)" paulson@14201: by blast paulson@14201: paulson@14201: lemma conj_absorb: "(A & A) = A" paulson@14201: by blast paulson@14201: paulson@14201: lemma conj_left_absorb: "(A & (A & B)) = (A & B)" paulson@14201: by blast paulson@14201: wenzelm@12281: lemma eq_ac: haftmann@57512: shows eq_commute: "a = b \ b = a" haftmann@57512: and iff_left_commute: "(P \ (Q \ R)) \ (Q \ (P \ R))" haftmann@57512: and iff_assoc: "((P \ Q) \ R) \ (P \ (Q \ R))" by (iprover, blast+) haftmann@57512: lemma neq_commute: "a \ b \ b \ a" by iprover wenzelm@12281: wenzelm@12281: lemma conj_comms: wenzelm@12937: shows conj_commute: "(P&Q) = (Q&P)" nipkow@17589: and conj_left_commute: "(P&(Q&R)) = (Q&(P&R))" by iprover+ nipkow@17589: lemma conj_assoc: "((P&Q)&R) = (P&(Q&R))" by iprover wenzelm@12281: paulson@19174: lemmas conj_ac = conj_commute conj_left_commute conj_assoc paulson@19174: wenzelm@12281: lemma disj_comms: wenzelm@12937: shows disj_commute: "(P|Q) = (Q|P)" nipkow@17589: and disj_left_commute: "(P|(Q|R)) = (Q|(P|R))" by iprover+ nipkow@17589: lemma disj_assoc: "((P|Q)|R) = (P|(Q|R))" by iprover wenzelm@12281: paulson@19174: lemmas disj_ac = disj_commute disj_left_commute disj_assoc paulson@19174: nipkow@17589: lemma conj_disj_distribL: "(P&(Q|R)) = (P&Q | P&R)" by iprover nipkow@17589: lemma conj_disj_distribR: "((P|Q)&R) = (P&R | Q&R)" by iprover wenzelm@12281: nipkow@17589: lemma disj_conj_distribL: "(P|(Q&R)) = ((P|Q) & (P|R))" by iprover nipkow@17589: lemma disj_conj_distribR: "((P&Q)|R) = ((P|R) & (Q|R))" by iprover wenzelm@12281: nipkow@17589: lemma imp_conjR: "(P --> (Q&R)) = ((P-->Q) & (P-->R))" by iprover nipkow@17589: lemma imp_conjL: "((P&Q) -->R) = (P --> (Q --> R))" by iprover nipkow@17589: lemma imp_disjL: "((P|Q) --> R) = ((P-->R)&(Q-->R))" by iprover wenzelm@12281: wenzelm@12281: text {* These two are specialized, but @{text imp_disj_not1} is useful in @{text "Auth/Yahalom"}. *} wenzelm@12281: lemma imp_disj_not1: "(P --> Q | R) = (~Q --> P --> R)" by blast wenzelm@12281: lemma imp_disj_not2: "(P --> Q | R) = (~R --> P --> Q)" by blast wenzelm@12281: wenzelm@12281: lemma imp_disj1: "((P-->Q)|R) = (P--> Q|R)" by blast wenzelm@12281: lemma imp_disj2: "(Q|(P-->R)) = (P--> Q|R)" by blast wenzelm@12281: haftmann@21151: lemma imp_cong: "(P = P') ==> (P' ==> (Q = Q')) ==> ((P --> Q) = (P' --> Q'))" haftmann@21151: by iprover haftmann@21151: nipkow@17589: lemma de_Morgan_disj: "(~(P | Q)) = (~P & ~Q)" by iprover wenzelm@12281: lemma de_Morgan_conj: "(~(P & Q)) = (~P | ~Q)" by blast wenzelm@12281: lemma not_imp: "(~(P --> Q)) = (P & ~Q)" by blast wenzelm@12281: lemma not_iff: "(P~=Q) = (P = (~Q))" by blast wenzelm@12281: lemma disj_not1: "(~P | Q) = (P --> Q)" by blast wenzelm@12281: lemma disj_not2: "(P | ~Q) = (Q --> P)" -- {* changes orientation :-( *} wenzelm@12281: by blast wenzelm@12281: lemma imp_conv_disj: "(P --> Q) = ((~P) | Q)" by blast wenzelm@12281: nipkow@17589: lemma iff_conv_conj_imp: "(P = Q) = ((P --> Q) & (Q --> P))" by iprover wenzelm@12281: wenzelm@12281: wenzelm@12281: lemma cases_simp: "((P --> Q) & (~P --> Q)) = Q" wenzelm@12281: -- {* Avoids duplication of subgoals after @{text split_if}, when the true and false *} wenzelm@12281: -- {* cases boil down to the same thing. *} wenzelm@12281: by blast wenzelm@12281: wenzelm@12281: lemma not_all: "(~ (! x. P(x))) = (? x.~P(x))" by blast wenzelm@12281: lemma imp_all: "((! x. P x) --> Q) = (? x. P x --> Q)" by blast nipkow@17589: lemma not_ex: "(~ (? x. P(x))) = (! x.~P(x))" by iprover nipkow@17589: lemma imp_ex: "((? x. P x) --> Q) = (! x. P x --> Q)" by iprover chaieb@23403: lemma all_not_ex: "(ALL x. P x) = (~ (EX x. ~ P x ))" by blast wenzelm@12281: blanchet@35828: declare All_def [no_atp] paulson@24286: nipkow@17589: lemma ex_disj_distrib: "(? x. P(x) | Q(x)) = ((? x. P(x)) | (? x. Q(x)))" by iprover nipkow@17589: lemma all_conj_distrib: "(!x. P(x) & Q(x)) = ((! x. P(x)) & (! x. Q(x)))" by iprover wenzelm@12281: wenzelm@12281: text {* wenzelm@12281: \medskip The @{text "&"} congruence rule: not included by default! wenzelm@12281: May slow rewrite proofs down by as much as 50\% *} wenzelm@12281: wenzelm@12281: lemma conj_cong: wenzelm@12281: "(P = P') ==> (P' ==> (Q = Q')) ==> ((P & Q) = (P' & Q'))" nipkow@17589: by iprover wenzelm@12281: wenzelm@12281: lemma rev_conj_cong: wenzelm@12281: "(Q = Q') ==> (Q' ==> (P = P')) ==> ((P & Q) = (P' & Q'))" nipkow@17589: by iprover wenzelm@12281: wenzelm@12281: text {* The @{text "|"} congruence rule: not included by default! *} wenzelm@12281: wenzelm@12281: lemma disj_cong: wenzelm@12281: "(P = P') ==> (~P' ==> (Q = Q')) ==> ((P | Q) = (P' | Q'))" wenzelm@12281: by blast wenzelm@12281: wenzelm@12281: wenzelm@12281: text {* \medskip if-then-else rules *} wenzelm@12281: haftmann@32068: lemma if_True [code]: "(if True then x else y) = x" haftmann@38525: by (unfold If_def) blast wenzelm@12281: haftmann@32068: lemma if_False [code]: "(if False then x else y) = y" haftmann@38525: by (unfold If_def) blast wenzelm@12281: wenzelm@12281: lemma if_P: "P ==> (if P then x else y) = x" haftmann@38525: by (unfold If_def) blast wenzelm@12281: wenzelm@12281: lemma if_not_P: "~P ==> (if P then x else y) = y" haftmann@38525: by (unfold If_def) blast wenzelm@12281: wenzelm@12281: lemma split_if: "P (if Q then x else y) = ((Q --> P(x)) & (~Q --> P(y)))" wenzelm@12281: apply (rule case_split [of Q]) paulson@15481: apply (simplesubst if_P) paulson@15481: prefer 3 apply (simplesubst if_not_P, blast+) wenzelm@12281: done wenzelm@12281: wenzelm@12281: lemma split_if_asm: "P (if Q then x else y) = (~((Q & ~P x) | (~Q & ~P y)))" paulson@15481: by (simplesubst split_if, blast) wenzelm@12281: blanchet@35828: lemmas if_splits [no_atp] = split_if split_if_asm wenzelm@12281: wenzelm@12281: lemma if_cancel: "(if c then x else x) = x" paulson@15481: by (simplesubst split_if, blast) wenzelm@12281: wenzelm@12281: lemma if_eq_cancel: "(if x = y then y else x) = x" paulson@15481: by (simplesubst split_if, blast) wenzelm@12281: blanchet@41792: lemma if_bool_eq_conj: blanchet@41792: "(if P then Q else R) = ((P-->Q) & (~P-->R))" wenzelm@19796: -- {* This form is useful for expanding @{text "if"}s on the RIGHT of the @{text "==>"} symbol. *} wenzelm@12281: by (rule split_if) wenzelm@12281: wenzelm@12281: lemma if_bool_eq_disj: "(if P then Q else R) = ((P&Q) | (~P&R))" wenzelm@19796: -- {* And this form is useful for expanding @{text "if"}s on the LEFT. *} lp15@59504: by (simplesubst split_if) blast wenzelm@12281: nipkow@17589: lemma Eq_TrueI: "P ==> P == True" by (unfold atomize_eq) iprover nipkow@17589: lemma Eq_FalseI: "~P ==> P == False" by (unfold atomize_eq) iprover wenzelm@12281: schirmer@15423: text {* \medskip let rules for simproc *} schirmer@15423: schirmer@15423: lemma Let_folded: "f x \ g x \ Let x f \ Let x g" schirmer@15423: by (unfold Let_def) schirmer@15423: schirmer@15423: lemma Let_unfold: "f x \ g \ Let x f \ g" schirmer@15423: by (unfold Let_def) schirmer@15423: berghofe@16633: text {* ballarin@16999: The following copy of the implication operator is useful for ballarin@16999: fine-tuning congruence rules. It instructs the simplifier to simplify ballarin@16999: its premise. berghofe@16633: *} berghofe@16633: haftmann@35416: definition simp_implies :: "[prop, prop] => prop" (infixr "=simp=>" 1) where haftmann@37767: "simp_implies \ op ==>" berghofe@16633: wenzelm@18457: lemma simp_impliesI: berghofe@16633: assumes PQ: "(PROP P \ PROP Q)" berghofe@16633: shows "PROP P =simp=> PROP Q" berghofe@16633: apply (unfold simp_implies_def) berghofe@16633: apply (rule PQ) berghofe@16633: apply assumption berghofe@16633: done berghofe@16633: berghofe@16633: lemma simp_impliesE: wenzelm@25388: assumes PQ: "PROP P =simp=> PROP Q" berghofe@16633: and P: "PROP P" berghofe@16633: and QR: "PROP Q \ PROP R" berghofe@16633: shows "PROP R" berghofe@16633: apply (rule QR) berghofe@16633: apply (rule PQ [unfolded simp_implies_def]) berghofe@16633: apply (rule P) berghofe@16633: done berghofe@16633: berghofe@16633: lemma simp_implies_cong: berghofe@16633: assumes PP' :"PROP P == PROP P'" berghofe@16633: and P'QQ': "PROP P' ==> (PROP Q == PROP Q')" berghofe@16633: shows "(PROP P =simp=> PROP Q) == (PROP P' =simp=> PROP Q')" berghofe@16633: proof (unfold simp_implies_def, rule equal_intr_rule) berghofe@16633: assume PQ: "PROP P \ PROP Q" berghofe@16633: and P': "PROP P'" berghofe@16633: from PP' [symmetric] and P' have "PROP P" berghofe@16633: by (rule equal_elim_rule1) wenzelm@23553: then have "PROP Q" by (rule PQ) berghofe@16633: with P'QQ' [OF P'] show "PROP Q'" by (rule equal_elim_rule1) berghofe@16633: next berghofe@16633: assume P'Q': "PROP P' \ PROP Q'" berghofe@16633: and P: "PROP P" berghofe@16633: from PP' and P have P': "PROP P'" by (rule equal_elim_rule1) wenzelm@23553: then have "PROP Q'" by (rule P'Q') berghofe@16633: with P'QQ' [OF P', symmetric] show "PROP Q" berghofe@16633: by (rule equal_elim_rule1) berghofe@16633: qed berghofe@16633: haftmann@20944: lemma uncurry: haftmann@20944: assumes "P \ Q \ R" haftmann@20944: shows "P \ Q \ R" wenzelm@23553: using assms by blast haftmann@20944: haftmann@20944: lemma iff_allI: haftmann@20944: assumes "\x. P x = Q x" haftmann@20944: shows "(\x. P x) = (\x. Q x)" wenzelm@23553: using assms by blast haftmann@20944: haftmann@20944: lemma iff_exI: haftmann@20944: assumes "\x. P x = Q x" haftmann@20944: shows "(\x. P x) = (\x. Q x)" wenzelm@23553: using assms by blast haftmann@20944: haftmann@20944: lemma all_comm: haftmann@20944: "(\x y. P x y) = (\y x. P x y)" haftmann@20944: by blast haftmann@20944: haftmann@20944: lemma ex_comm: haftmann@20944: "(\x y. P x y) = (\y x. P x y)" haftmann@20944: by blast haftmann@20944: wenzelm@48891: ML_file "Tools/simpdata.ML" wenzelm@21671: ML {* open Simpdata *} wenzelm@42455: wenzelm@58826: setup {* wenzelm@58826: map_theory_simpset (put_simpset HOL_basic_ss) #> wenzelm@58826: Simplifier.method_setup Splitter.split_modifiers wenzelm@58826: *} wenzelm@42455: wenzelm@42459: simproc_setup defined_Ex ("EX x. P x") = {* fn _ => Quantifier1.rearrange_ex *} wenzelm@42459: simproc_setup defined_All ("ALL x. P x") = {* fn _ => Quantifier1.rearrange_all *} wenzelm@21671: wenzelm@24035: text {* Simproc for proving @{text "(y = x) == False"} from premise @{text "~(x = y)"}: *} wenzelm@24035: wenzelm@24035: simproc_setup neq ("x = y") = {* fn _ => wenzelm@24035: let wenzelm@24035: val neq_to_EQ_False = @{thm not_sym} RS @{thm Eq_FalseI}; wenzelm@24035: fun is_neq eq lhs rhs thm = wenzelm@24035: (case Thm.prop_of thm of wenzelm@24035: _ $ (Not $ (eq' $ l' $ r')) => wenzelm@24035: Not = HOLogic.Not andalso eq' = eq andalso wenzelm@24035: r' aconv lhs andalso l' aconv rhs wenzelm@24035: | _ => false); wenzelm@24035: fun proc ss ct = wenzelm@24035: (case Thm.term_of ct of wenzelm@24035: eq $ lhs $ rhs => wenzelm@43597: (case find_first (is_neq eq lhs rhs) (Simplifier.prems_of ss) of wenzelm@24035: SOME thm => SOME (thm RS neq_to_EQ_False) wenzelm@24035: | NONE => NONE) wenzelm@24035: | _ => NONE); wenzelm@24035: in proc end; wenzelm@24035: *} wenzelm@24035: wenzelm@24035: simproc_setup let_simp ("Let x f") = {* wenzelm@24035: let wenzelm@24035: val (f_Let_unfold, x_Let_unfold) = wenzelm@59582: let val [(_ $ (f $ x) $ _)] = Thm.prems_of @{thm Let_unfold} wenzelm@59628: in apply2 (Thm.cterm_of @{context}) (f, x) end wenzelm@24035: val (f_Let_folded, x_Let_folded) = wenzelm@59582: let val [(_ $ (f $ x) $ _)] = Thm.prems_of @{thm Let_folded} wenzelm@59628: in apply2 (Thm.cterm_of @{context}) (f, x) end; wenzelm@24035: val g_Let_folded = wenzelm@59582: let val [(_ $ _ $ (g $ _))] = Thm.prems_of @{thm Let_folded} wenzelm@59628: in Thm.cterm_of @{context} g end; haftmann@28741: fun count_loose (Bound i) k = if i >= k then 1 else 0 haftmann@28741: | count_loose (s $ t) k = count_loose s k + count_loose t k haftmann@28741: | count_loose (Abs (_, _, t)) k = count_loose t (k + 1) haftmann@28741: | count_loose _ _ = 0; haftmann@28741: fun is_trivial_let (Const (@{const_name Let}, _) $ x $ t) = wenzelm@59628: (case t of wenzelm@59628: Abs (_, _, t') => count_loose t' 0 <= 1 wenzelm@59628: | _ => true); wenzelm@59628: in wenzelm@59628: fn _ => fn ctxt => fn ct => wenzelm@59628: if is_trivial_let (Thm.term_of ct) wenzelm@59628: then SOME @{thm Let_def} (*no or one ocurrence of bound variable*) wenzelm@59628: else wenzelm@59628: let (*Norbert Schirmer's case*) wenzelm@59628: val t = Thm.term_of ct; wenzelm@59628: val ([t'], ctxt') = Variable.import_terms false [t] ctxt; wenzelm@59628: in wenzelm@59628: Option.map (hd o Variable.export ctxt' ctxt o single) wenzelm@59628: (case t' of Const (@{const_name Let},_) $ x $ f => (* x and f are already in normal form *) wenzelm@59628: if is_Free x orelse is_Bound x orelse is_Const x wenzelm@59628: then SOME @{thm Let_def} wenzelm@59628: else wenzelm@59628: let wenzelm@59628: val n = case f of (Abs (x, _, _)) => x | _ => "x"; wenzelm@59628: val cx = Thm.cterm_of ctxt x; wenzelm@59628: val xT = Thm.typ_of_cterm cx; wenzelm@59628: val cf = Thm.cterm_of ctxt f; wenzelm@59628: val fx_g = Simplifier.rewrite ctxt (Thm.apply cf cx); wenzelm@59628: val (_ $ _ $ g) = Thm.prop_of fx_g; wenzelm@59628: val g' = abstract_over (x, g); wenzelm@59628: val abs_g'= Abs (n, xT, g'); wenzelm@59628: in wenzelm@59628: if g aconv g' then wenzelm@59628: let wenzelm@59628: val rl = wenzelm@59628: cterm_instantiate [(f_Let_unfold, cf), (x_Let_unfold, cx)] @{thm Let_unfold}; wenzelm@59628: in SOME (rl OF [fx_g]) end wenzelm@59628: else if (Envir.beta_eta_contract f) aconv (Envir.beta_eta_contract abs_g') wenzelm@59628: then NONE (*avoid identity conversion*) wenzelm@59628: else wenzelm@59628: let wenzelm@59628: val g'x = abs_g' $ x; wenzelm@59628: val g_g'x = Thm.symmetric (Thm.beta_conversion false (Thm.cterm_of ctxt g'x)); wenzelm@59628: val rl = wenzelm@59628: @{thm Let_folded} |> cterm_instantiate wenzelm@59628: [(f_Let_folded, Thm.cterm_of ctxt f), wenzelm@59628: (x_Let_folded, cx), wenzelm@59628: (g_Let_folded, Thm.cterm_of ctxt abs_g')]; wenzelm@59628: in SOME (rl OF [Thm.transitive fx_g g_g'x]) end wenzelm@59628: end wenzelm@59628: | _ => NONE) wenzelm@59628: end haftmann@28741: end *} wenzelm@24035: haftmann@21151: lemma True_implies_equals: "(True \ PROP P) \ PROP P" haftmann@21151: proof wenzelm@23389: assume "True \ PROP P" wenzelm@23389: from this [OF TrueI] show "PROP P" . haftmann@21151: next haftmann@21151: assume "PROP P" wenzelm@23389: then show "PROP P" . haftmann@21151: qed haftmann@21151: nipkow@59864: lemma implies_True_equals: "(PROP P \ True) \ Trueprop True" nipkow@59864: by default (intro TrueI) nipkow@59864: nipkow@59864: lemma False_implies_equals: "(False \ P) \ Trueprop True" nipkow@59864: by default simp_all nipkow@59864: haftmann@21151: lemma ex_simps: haftmann@21151: "!!P Q. (EX x. P x & Q) = ((EX x. P x) & Q)" haftmann@21151: "!!P Q. (EX x. P & Q x) = (P & (EX x. Q x))" haftmann@21151: "!!P Q. (EX x. P x | Q) = ((EX x. P x) | Q)" haftmann@21151: "!!P Q. (EX x. P | Q x) = (P | (EX x. Q x))" haftmann@21151: "!!P Q. (EX x. P x --> Q) = ((ALL x. P x) --> Q)" haftmann@21151: "!!P Q. (EX x. P --> Q x) = (P --> (EX x. Q x))" haftmann@21151: -- {* Miniscoping: pushing in existential quantifiers. *} haftmann@21151: by (iprover | blast)+ haftmann@21151: haftmann@21151: lemma all_simps: haftmann@21151: "!!P Q. (ALL x. P x & Q) = ((ALL x. P x) & Q)" haftmann@21151: "!!P Q. (ALL x. P & Q x) = (P & (ALL x. Q x))" haftmann@21151: "!!P Q. (ALL x. P x | Q) = ((ALL x. P x) | Q)" haftmann@21151: "!!P Q. (ALL x. P | Q x) = (P | (ALL x. Q x))" haftmann@21151: "!!P Q. (ALL x. P x --> Q) = ((EX x. P x) --> Q)" haftmann@21151: "!!P Q. (ALL x. P --> Q x) = (P --> (ALL x. Q x))" haftmann@21151: -- {* Miniscoping: pushing in universal quantifiers. *} haftmann@21151: by (iprover | blast)+ paulson@15481: wenzelm@21671: lemmas [simp] = wenzelm@21671: triv_forall_equality (*prunes params*) wenzelm@21671: True_implies_equals (*prune asms `True'*) wenzelm@21671: if_True wenzelm@21671: if_False wenzelm@21671: if_cancel wenzelm@21671: if_eq_cancel wenzelm@21671: imp_disjL haftmann@20973: (*In general it seems wrong to add distributive laws by default: they haftmann@20973: might cause exponential blow-up. But imp_disjL has been in for a while haftmann@20973: and cannot be removed without affecting existing proofs. Moreover, haftmann@20973: rewriting by "(P|Q --> R) = ((P-->R)&(Q-->R))" might be justified on the haftmann@20973: grounds that it allows simplification of R in the two cases.*) wenzelm@21671: conj_assoc wenzelm@21671: disj_assoc wenzelm@21671: de_Morgan_conj wenzelm@21671: de_Morgan_disj wenzelm@21671: imp_disj1 wenzelm@21671: imp_disj2 wenzelm@21671: not_imp wenzelm@21671: disj_not1 wenzelm@21671: not_all wenzelm@21671: not_ex wenzelm@21671: cases_simp wenzelm@21671: the_eq_trivial wenzelm@21671: the_sym_eq_trivial wenzelm@21671: ex_simps wenzelm@21671: all_simps wenzelm@21671: simp_thms wenzelm@21671: wenzelm@21671: lemmas [cong] = imp_cong simp_implies_cong wenzelm@21671: lemmas [split] = split_if haftmann@20973: wenzelm@51717: ML {* val HOL_ss = simpset_of @{context} *} haftmann@20973: haftmann@20944: text {* Simplifies x assuming c and y assuming ~c *} haftmann@20944: lemma if_cong: haftmann@20944: assumes "b = c" haftmann@20944: and "c \ x = u" haftmann@20944: and "\ c \ y = v" haftmann@20944: shows "(if b then x else y) = (if c then u else v)" haftmann@38525: using assms by simp haftmann@20944: haftmann@20944: text {* Prevents simplification of x and y: haftmann@20944: faster and allows the execution of functional programs. *} haftmann@20944: lemma if_weak_cong [cong]: haftmann@20944: assumes "b = c" haftmann@20944: shows "(if b then x else y) = (if c then x else y)" wenzelm@23553: using assms by (rule arg_cong) haftmann@20944: haftmann@20944: text {* Prevents simplification of t: much faster *} haftmann@20944: lemma let_weak_cong: haftmann@20944: assumes "a = b" haftmann@20944: shows "(let x = a in t x) = (let x = b in t x)" wenzelm@23553: using assms by (rule arg_cong) haftmann@20944: haftmann@20944: text {* To tidy up the result of a simproc. Only the RHS will be simplified. *} haftmann@20944: lemma eq_cong2: haftmann@20944: assumes "u = u'" haftmann@20944: shows "(t \ u) \ (t \ u')" wenzelm@23553: using assms by simp haftmann@20944: haftmann@20944: lemma if_distrib: haftmann@20944: "f (if c then x else y) = (if c then f x else f y)" haftmann@20944: by simp haftmann@20944: haftmann@44277: text{*As a simplification rule, it replaces all function equalities by haftmann@44277: first-order equalities.*} haftmann@44277: lemma fun_eq_iff: "f = g \ (\x. f x = g x)" haftmann@44277: by auto haftmann@44277: wenzelm@17459: haftmann@20944: subsubsection {* Generic cases and induction *} wenzelm@17459: haftmann@20944: text {* Rule projections: *} haftmann@20944: ML {* wenzelm@32172: structure Project_Rule = Project_Rule wenzelm@25388: ( wenzelm@27126: val conjunct1 = @{thm conjunct1} wenzelm@27126: val conjunct2 = @{thm conjunct2} wenzelm@27126: val mp = @{thm mp} wenzelm@59929: ); wenzelm@17459: *} wenzelm@17459: wenzelm@59940: context wenzelm@59940: begin wenzelm@59940: wenzelm@59940: restricted definition "induct_forall P \ \x. P x" wenzelm@59940: restricted definition "induct_implies A B \ A \ B" wenzelm@59940: restricted definition "induct_equal x y \ x = y" wenzelm@59940: restricted definition "induct_conj A B \ A \ B" wenzelm@59940: restricted definition "induct_true \ True" wenzelm@59940: restricted definition "induct_false \ False" haftmann@35416: wenzelm@59929: lemma induct_forall_eq: "(\x. P x) \ Trueprop (induct_forall (\x. P x))" wenzelm@18457: by (unfold atomize_all induct_forall_def) wenzelm@11824: wenzelm@59929: lemma induct_implies_eq: "(A \ B) \ Trueprop (induct_implies A B)" wenzelm@18457: by (unfold atomize_imp induct_implies_def) wenzelm@11824: wenzelm@59929: lemma induct_equal_eq: "(x \ y) \ Trueprop (induct_equal x y)" wenzelm@18457: by (unfold atomize_eq induct_equal_def) wenzelm@18457: wenzelm@59929: lemma induct_conj_eq: "(A &&& B) \ Trueprop (induct_conj A B)" wenzelm@18457: by (unfold atomize_conj induct_conj_def) wenzelm@18457: berghofe@34908: lemmas induct_atomize' = induct_forall_eq induct_implies_eq induct_conj_eq berghofe@34908: lemmas induct_atomize = induct_atomize' induct_equal_eq wenzelm@45607: lemmas induct_rulify' [symmetric] = induct_atomize' wenzelm@45607: lemmas induct_rulify [symmetric] = induct_atomize wenzelm@18457: lemmas induct_rulify_fallback = wenzelm@18457: induct_forall_def induct_implies_def induct_equal_def induct_conj_def berghofe@34908: induct_true_def induct_false_def wenzelm@18457: wenzelm@11989: lemma induct_forall_conj: "induct_forall (\x. induct_conj (A x) (B x)) = wenzelm@11989: induct_conj (induct_forall A) (induct_forall B)" nipkow@17589: by (unfold induct_forall_def induct_conj_def) iprover wenzelm@11824: wenzelm@11989: lemma induct_implies_conj: "induct_implies C (induct_conj A B) = wenzelm@11989: induct_conj (induct_implies C A) (induct_implies C B)" nipkow@17589: by (unfold induct_implies_def induct_conj_def) iprover wenzelm@11989: wenzelm@59929: lemma induct_conj_curry: "(induct_conj A B \ PROP C) \ (A \ B \ PROP C)" berghofe@13598: proof wenzelm@59929: assume r: "induct_conj A B \ PROP C" wenzelm@59929: assume ab: A B wenzelm@59929: show "PROP C" by (rule r) (simp add: induct_conj_def ab) berghofe@13598: next wenzelm@59929: assume r: "A \ B \ PROP C" wenzelm@59929: assume ab: "induct_conj A B" wenzelm@59929: show "PROP C" by (rule r) (simp_all add: ab [unfolded induct_conj_def]) berghofe@13598: qed wenzelm@11824: wenzelm@11989: lemmas induct_conj = induct_forall_conj induct_implies_conj induct_conj_curry wenzelm@11824: berghofe@34908: lemma induct_trueI: "induct_true" berghofe@34908: by (simp add: induct_true_def) wenzelm@11824: wenzelm@11824: text {* Method setup. *} wenzelm@11824: wenzelm@58826: ML_file "~~/src/Tools/induct.ML" wenzelm@11824: ML {* wenzelm@32171: structure Induct = Induct wenzelm@27126: ( wenzelm@27126: val cases_default = @{thm case_split} wenzelm@27126: val atomize = @{thms induct_atomize} berghofe@34908: val rulify = @{thms induct_rulify'} wenzelm@27126: val rulify_fallback = @{thms induct_rulify_fallback} berghofe@34988: val equal_def = @{thm induct_equal_def} berghofe@34908: fun dest_def (Const (@{const_name induct_equal}, _) $ t $ u) = SOME (t, u) berghofe@34908: | dest_def _ = NONE wenzelm@58957: fun trivial_tac ctxt = match_tac ctxt @{thms induct_trueI} wenzelm@27126: ) wenzelm@11824: *} wenzelm@11824: wenzelm@48891: ML_file "~~/src/Tools/induction.ML" nipkow@45014: wenzelm@59940: declaration {* wenzelm@59940: fn _ => Induct.map_simpset (fn ss => ss berghofe@34908: addsimprocs wenzelm@38715: [Simplifier.simproc_global @{theory} "swap_induct_false" berghofe@34908: ["induct_false ==> PROP P ==> PROP Q"] wenzelm@51717: (fn _ => berghofe@34908: (fn _ $ (P as _ $ @{const induct_false}) $ (_ $ Q $ _) => berghofe@34908: if P <> Q then SOME Drule.swap_prems_eq else NONE berghofe@34908: | _ => NONE)), wenzelm@38715: Simplifier.simproc_global @{theory} "induct_equal_conj_curry" berghofe@34908: ["induct_conj P Q ==> PROP R"] wenzelm@51717: (fn _ => berghofe@34908: (fn _ $ (_ $ P) $ _ => berghofe@34908: let berghofe@34908: fun is_conj (@{const induct_conj} $ P $ Q) = berghofe@34908: is_conj P andalso is_conj Q berghofe@34908: | is_conj (Const (@{const_name induct_equal}, _) $ _ $ _) = true berghofe@34908: | is_conj @{const induct_true} = true berghofe@34908: | is_conj @{const induct_false} = true berghofe@34908: | is_conj _ = false berghofe@34908: in if is_conj P then SOME @{thm induct_conj_curry} else NONE end wenzelm@45625: | _ => NONE))] wenzelm@54742: |> Simplifier.set_mksimps (fn ctxt => wenzelm@54742: Simpdata.mksimps Simpdata.mksimps_pairs ctxt #> wenzelm@59940: map (rewrite_rule ctxt (map Thm.symmetric @{thms induct_rulify_fallback})))) berghofe@34908: *} berghofe@34908: berghofe@34908: text {* Pre-simplification of induction and cases rules *} berghofe@34908: wenzelm@59929: lemma [induct_simp]: "(\x. induct_equal x t \ PROP P x) \ PROP P t" berghofe@34908: unfolding induct_equal_def berghofe@34908: proof wenzelm@59929: assume r: "\x. x = t \ PROP P x" wenzelm@59929: show "PROP P t" by (rule r [OF refl]) berghofe@34908: next wenzelm@59929: fix x wenzelm@59929: assume "PROP P t" "x = t" berghofe@34908: then show "PROP P x" by simp berghofe@34908: qed berghofe@34908: wenzelm@59929: lemma [induct_simp]: "(\x. induct_equal t x \ PROP P x) \ PROP P t" berghofe@34908: unfolding induct_equal_def berghofe@34908: proof wenzelm@59929: assume r: "\x. t = x \ PROP P x" wenzelm@59929: show "PROP P t" by (rule r [OF refl]) berghofe@34908: next wenzelm@59929: fix x wenzelm@59929: assume "PROP P t" "t = x" berghofe@34908: then show "PROP P x" by simp berghofe@34908: qed berghofe@34908: wenzelm@59929: lemma [induct_simp]: "(induct_false \ P) \ Trueprop induct_true" berghofe@34908: unfolding induct_false_def induct_true_def berghofe@34908: by (iprover intro: equal_intr_rule) berghofe@34908: wenzelm@59929: lemma [induct_simp]: "(induct_true \ PROP P) \ PROP P" berghofe@34908: unfolding induct_true_def berghofe@34908: proof wenzelm@59929: assume "True \ PROP P" wenzelm@59929: then show "PROP P" using TrueI . berghofe@34908: next berghofe@34908: assume "PROP P" berghofe@34908: then show "PROP P" . berghofe@34908: qed berghofe@34908: wenzelm@59929: lemma [induct_simp]: "(PROP P \ induct_true) \ Trueprop induct_true" berghofe@34908: unfolding induct_true_def berghofe@34908: by (iprover intro: equal_intr_rule) berghofe@34908: wenzelm@59929: lemma [induct_simp]: "(\x. induct_true) \ Trueprop induct_true" berghofe@34908: unfolding induct_true_def berghofe@34908: by (iprover intro: equal_intr_rule) berghofe@34908: wenzelm@59929: lemma [induct_simp]: "induct_implies induct_true P \ P" berghofe@34908: by (simp add: induct_implies_def induct_true_def) berghofe@34908: wenzelm@59929: lemma [induct_simp]: "x = x \ True" berghofe@34908: by (rule simp_thms) berghofe@34908: wenzelm@59940: end wenzelm@18457: wenzelm@48891: ML_file "~~/src/Tools/induct_tacs.ML" wenzelm@27126: haftmann@20944: berghofe@28325: subsubsection {* Coherent logic *} berghofe@28325: wenzelm@55632: ML_file "~~/src/Tools/coherent.ML" berghofe@28325: ML {* wenzelm@32734: structure Coherent = Coherent berghofe@28325: ( wenzelm@55632: val atomize_elimL = @{thm atomize_elimL}; wenzelm@55632: val atomize_exL = @{thm atomize_exL}; wenzelm@55632: val atomize_conjL = @{thm atomize_conjL}; wenzelm@55632: val atomize_disjL = @{thm atomize_disjL}; wenzelm@55632: val operator_names = [@{const_name HOL.disj}, @{const_name HOL.conj}, @{const_name Ex}]; berghofe@28325: ); berghofe@28325: *} berghofe@28325: berghofe@28325: huffman@31024: subsubsection {* Reorienting equalities *} huffman@31024: huffman@31024: ML {* huffman@31024: signature REORIENT_PROC = huffman@31024: sig huffman@31024: val add : (term -> bool) -> theory -> theory wenzelm@51717: val proc : morphism -> Proof.context -> cterm -> thm option huffman@31024: end; huffman@31024: wenzelm@33523: structure Reorient_Proc : REORIENT_PROC = huffman@31024: struct wenzelm@33523: structure Data = Theory_Data huffman@31024: ( wenzelm@33523: type T = ((term -> bool) * stamp) list; wenzelm@33523: val empty = []; huffman@31024: val extend = I; wenzelm@33523: fun merge data : T = Library.merge (eq_snd op =) data; wenzelm@33523: ); wenzelm@33523: fun add m = Data.map (cons (m, stamp ())); wenzelm@33523: fun matches thy t = exists (fn (m, _) => m t) (Data.get thy); huffman@31024: huffman@31024: val meta_reorient = @{thm eq_commute [THEN eq_reflection]}; wenzelm@51717: fun proc phi ctxt ct = huffman@31024: let wenzelm@42361: val thy = Proof_Context.theory_of ctxt; huffman@31024: in huffman@31024: case Thm.term_of ct of wenzelm@33523: (_ $ t $ u) => if matches thy u then NONE else SOME meta_reorient huffman@31024: | _ => NONE huffman@31024: end; huffman@31024: end; huffman@31024: *} huffman@31024: huffman@31024: haftmann@20944: subsection {* Other simple lemmas and lemma duplicates *} haftmann@20944: haftmann@20944: lemma ex1_eq [iff]: "EX! x. x = t" "EX! x. t = x" haftmann@20944: by blast+ haftmann@20944: haftmann@20944: lemma choice_eq: "(ALL x. EX! y. P x y) = (EX! f. ALL x. P x (f x))" haftmann@20944: apply (rule iffI) haftmann@20944: apply (rule_tac a = "%x. THE y. P x y" in ex1I) haftmann@20944: apply (fast dest!: theI') huffman@44921: apply (fast intro: the1_equality [symmetric]) haftmann@20944: apply (erule ex1E) haftmann@20944: apply (rule allI) haftmann@20944: apply (rule ex1I) haftmann@20944: apply (erule spec) haftmann@20944: apply (erule_tac x = "%z. if z = x then y else f z" in allE) haftmann@20944: apply (erule impE) haftmann@20944: apply (rule allI) wenzelm@27126: apply (case_tac "xa = x") haftmann@20944: apply (drule_tac [3] x = x in fun_cong, simp_all) haftmann@20944: done haftmann@20944: haftmann@22218: lemmas eq_sym_conv = eq_commute haftmann@22218: chaieb@23037: lemma nnf_simps: wenzelm@58826: "(\(P \ Q)) = (\ P \ \ Q)" "(\ (P \ Q)) = (\ P \ \Q)" "(P \ Q) = (\P \ Q)" wenzelm@58826: "(P = Q) = ((P \ Q) \ (\P \ \ Q))" "(\(P = Q)) = ((P \ \ Q) \ (\P \ Q))" chaieb@23037: "(\ \(P)) = P" chaieb@23037: by blast+ chaieb@23037: wenzelm@21671: subsection {* Basic ML bindings *} wenzelm@21671: wenzelm@21671: ML {* wenzelm@22129: val FalseE = @{thm FalseE} wenzelm@22129: val Let_def = @{thm Let_def} wenzelm@22129: val TrueI = @{thm TrueI} wenzelm@22129: val allE = @{thm allE} wenzelm@22129: val allI = @{thm allI} wenzelm@22129: val all_dupE = @{thm all_dupE} wenzelm@22129: val arg_cong = @{thm arg_cong} wenzelm@22129: val box_equals = @{thm box_equals} wenzelm@22129: val ccontr = @{thm ccontr} wenzelm@22129: val classical = @{thm classical} wenzelm@22129: val conjE = @{thm conjE} wenzelm@22129: val conjI = @{thm conjI} wenzelm@22129: val conjunct1 = @{thm conjunct1} wenzelm@22129: val conjunct2 = @{thm conjunct2} wenzelm@22129: val disjCI = @{thm disjCI} wenzelm@22129: val disjE = @{thm disjE} wenzelm@22129: val disjI1 = @{thm disjI1} wenzelm@22129: val disjI2 = @{thm disjI2} wenzelm@22129: val eq_reflection = @{thm eq_reflection} wenzelm@22129: val ex1E = @{thm ex1E} wenzelm@22129: val ex1I = @{thm ex1I} wenzelm@22129: val ex1_implies_ex = @{thm ex1_implies_ex} wenzelm@22129: val exE = @{thm exE} wenzelm@22129: val exI = @{thm exI} wenzelm@22129: val excluded_middle = @{thm excluded_middle} wenzelm@22129: val ext = @{thm ext} wenzelm@22129: val fun_cong = @{thm fun_cong} wenzelm@22129: val iffD1 = @{thm iffD1} wenzelm@22129: val iffD2 = @{thm iffD2} wenzelm@22129: val iffI = @{thm iffI} wenzelm@22129: val impE = @{thm impE} wenzelm@22129: val impI = @{thm impI} wenzelm@22129: val meta_eq_to_obj_eq = @{thm meta_eq_to_obj_eq} wenzelm@22129: val mp = @{thm mp} wenzelm@22129: val notE = @{thm notE} wenzelm@22129: val notI = @{thm notI} wenzelm@22129: val not_all = @{thm not_all} wenzelm@22129: val not_ex = @{thm not_ex} wenzelm@22129: val not_iff = @{thm not_iff} wenzelm@22129: val not_not = @{thm not_not} wenzelm@22129: val not_sym = @{thm not_sym} wenzelm@22129: val refl = @{thm refl} wenzelm@22129: val rev_mp = @{thm rev_mp} wenzelm@22129: val spec = @{thm spec} wenzelm@22129: val ssubst = @{thm ssubst} wenzelm@22129: val subst = @{thm subst} wenzelm@22129: val sym = @{thm sym} wenzelm@22129: val trans = @{thm trans} wenzelm@21671: *} wenzelm@21671: wenzelm@55239: ML_file "Tools/cnf.ML" wenzelm@55239: wenzelm@21671: hoelzl@58775: section {* @{text NO_MATCH} simproc *} hoelzl@58775: hoelzl@58775: text {* hoelzl@58775: The simplification procedure can be used to avoid simplification of terms of a certain form hoelzl@58775: *} hoelzl@58775: hoelzl@59779: definition NO_MATCH :: "'a \ 'b \ bool" where "NO_MATCH pat val \ True" hoelzl@58830: hoelzl@59779: lemma NO_MATCH_cong[cong]: "NO_MATCH pat val = NO_MATCH pat val" by (rule refl) hoelzl@58775: hoelzl@58830: declare [[coercion_args NO_MATCH - -]] hoelzl@58830: hoelzl@59779: simproc_setup NO_MATCH ("NO_MATCH pat val") = {* fn _ => fn ctxt => fn ct => hoelzl@58775: let hoelzl@58775: val thy = Proof_Context.theory_of ctxt hoelzl@58775: val dest_binop = Term.dest_comb #> apfst (Term.dest_comb #> snd) hoelzl@58775: val m = Pattern.matches thy (dest_binop (Thm.term_of ct)) hoelzl@58775: in if m then NONE else SOME @{thm NO_MATCH_def} end hoelzl@58775: *} hoelzl@58775: hoelzl@58775: text {* hoelzl@59779: This setup ensures that a rewrite rule of the form @{term "NO_MATCH pat val \ t"} hoelzl@58775: is only applied, if the pattern @{term pat} does not match the value @{term val}. hoelzl@58775: *} hoelzl@58775: hoelzl@58775: haftmann@30929: subsection {* Code generator setup *} haftmann@30929: haftmann@31151: subsubsection {* Generic code generator preprocessor setup *} haftmann@31151: haftmann@53146: lemma conj_left_cong: haftmann@53146: "P \ Q \ P \ R \ Q \ R" haftmann@53146: by (fact arg_cong) haftmann@53146: haftmann@53146: lemma disj_left_cong: haftmann@53146: "P \ Q \ P \ R \ Q \ R" haftmann@53146: by (fact arg_cong) haftmann@53146: haftmann@31151: setup {* wenzelm@58826: Code_Preproc.map_pre (put_simpset HOL_basic_ss) #> wenzelm@58826: Code_Preproc.map_post (put_simpset HOL_basic_ss) #> wenzelm@58826: Code_Simp.map_ss (put_simpset HOL_basic_ss #> wenzelm@58826: Simplifier.add_cong @{thm conj_left_cong} #> wenzelm@58826: Simplifier.add_cong @{thm disj_left_cong}) haftmann@31151: *} haftmann@31151: haftmann@53146: haftmann@30929: subsubsection {* Equality *} haftmann@24844: haftmann@38857: class equal = haftmann@38857: fixes equal :: "'a \ 'a \ bool" haftmann@38857: assumes equal_eq: "equal x y \ x = y" haftmann@26513: begin haftmann@26513: bulwahn@45231: lemma equal: "equal = (op =)" haftmann@38857: by (rule ext equal_eq)+ haftmann@28346: haftmann@38857: lemma equal_refl: "equal x x \ True" haftmann@38857: unfolding equal by rule+ haftmann@28346: haftmann@38857: lemma eq_equal: "(op =) \ equal" haftmann@38857: by (rule eq_reflection) (rule ext, rule ext, rule sym, rule equal_eq) haftmann@30929: haftmann@26513: end haftmann@26513: haftmann@38857: declare eq_equal [symmetric, code_post] haftmann@38857: declare eq_equal [code] haftmann@30966: haftmann@31151: setup {* wenzelm@51717: Code_Preproc.map_pre (fn ctxt => wenzelm@51717: ctxt addsimprocs [Simplifier.simproc_global_i @{theory} "equal" [@{term HOL.eq}] wenzelm@51717: (fn _ => fn Const (_, Type ("fun", [Type _, _])) => SOME @{thm eq_equal} | _ => NONE)]) haftmann@31151: *} haftmann@31151: haftmann@30966: haftmann@30929: subsubsection {* Generic code generator foundation *} haftmann@30929: haftmann@39421: text {* Datatype @{typ bool} *} haftmann@30929: haftmann@30929: code_datatype True False haftmann@30929: haftmann@30929: lemma [code]: haftmann@33185: shows "False \ P \ False" haftmann@33185: and "True \ P \ P" haftmann@33185: and "P \ False \ False" haftmann@33185: and "P \ True \ P" by simp_all haftmann@30929: haftmann@30929: lemma [code]: haftmann@33185: shows "False \ P \ P" haftmann@33185: and "True \ P \ True" haftmann@33185: and "P \ False \ P" haftmann@33185: and "P \ True \ True" by simp_all haftmann@30929: haftmann@33185: lemma [code]: haftmann@33185: shows "(False \ P) \ True" haftmann@33185: and "(True \ P) \ P" haftmann@33185: and "(P \ False) \ \ P" haftmann@33185: and "(P \ True) \ True" by simp_all haftmann@30929: haftmann@39421: text {* More about @{typ prop} *} haftmann@39421: haftmann@39421: lemma [code nbe]: wenzelm@58826: shows "(True \ PROP Q) \ PROP Q" haftmann@39421: and "(PROP Q \ True) \ Trueprop True" haftmann@39421: and "(P \ R) \ Trueprop (P \ R)" by (auto intro!: equal_intr_rule) haftmann@39421: haftmann@39421: lemma Trueprop_code [code]: haftmann@39421: "Trueprop True \ Code_Generator.holds" haftmann@39421: by (auto intro!: equal_intr_rule holds) haftmann@39421: haftmann@39421: declare Trueprop_code [symmetric, code_post] haftmann@39421: haftmann@39421: text {* Equality *} haftmann@39421: haftmann@39421: declare simp_thms(6) [code nbe] haftmann@39421: haftmann@38857: instantiation itself :: (type) equal haftmann@31132: begin haftmann@31132: haftmann@38857: definition equal_itself :: "'a itself \ 'a itself \ bool" where haftmann@38857: "equal_itself x y \ x = y" haftmann@31132: haftmann@31132: instance proof haftmann@38857: qed (fact equal_itself_def) haftmann@31132: haftmann@31132: end haftmann@31132: haftmann@38857: lemma equal_itself_code [code]: haftmann@38857: "equal TYPE('a) TYPE('a) \ True" haftmann@38857: by (simp add: equal) haftmann@31132: wenzelm@58826: setup {* Sign.add_const_constraint (@{const_name equal}, SOME @{typ "'a\type \ 'a \ bool"}) *} haftmann@31956: haftmann@38857: lemma equal_alias_cert: "OFCLASS('a, equal_class) \ ((op = :: 'a \ 'a \ bool) \ equal)" (is "?ofclass \ ?equal") haftmann@31956: proof haftmann@31956: assume "PROP ?ofclass" haftmann@38857: show "PROP ?equal" wenzelm@59498: by (tactic {* ALLGOALS (resolve_tac @{context} [Thm.unconstrainT @{thm eq_equal}]) *}) haftmann@31956: (fact `PROP ?ofclass`) haftmann@31956: next haftmann@38857: assume "PROP ?equal" haftmann@31956: show "PROP ?ofclass" proof haftmann@38857: qed (simp add: `PROP ?equal`) haftmann@31956: qed haftmann@31956: wenzelm@58826: setup {* Sign.add_const_constraint (@{const_name equal}, SOME @{typ "'a\equal \ 'a \ bool"}) *} wenzelm@58826: wenzelm@58826: setup {* Nbe.add_const_alias @{thm equal_alias_cert} *} haftmann@30929: haftmann@30929: text {* Cases *} haftmann@30929: haftmann@30929: lemma Let_case_cert: haftmann@30929: assumes "CASE \ (\x. Let x f)" haftmann@30929: shows "CASE x \ f x" haftmann@30929: using assms by simp_all haftmann@30929: haftmann@30929: setup {* wenzelm@58826: Code.add_case @{thm Let_case_cert} #> wenzelm@58826: Code.add_undefined @{const_name undefined} haftmann@30929: *} haftmann@30929: haftmann@54890: declare [[code abort: undefined]] haftmann@30929: haftmann@38972: haftmann@30929: subsubsection {* Generic code generator target languages *} haftmann@30929: haftmann@38972: text {* type @{typ bool} *} haftmann@30929: haftmann@52435: code_printing haftmann@52435: type_constructor bool \ haftmann@52435: (SML) "bool" and (OCaml) "bool" and (Haskell) "Bool" and (Scala) "Boolean" haftmann@52435: | constant True \ haftmann@52435: (SML) "true" and (OCaml) "true" and (Haskell) "True" and (Scala) "true" haftmann@52435: | constant False \ wenzelm@58826: (SML) "false" and (OCaml) "false" and (Haskell) "False" and (Scala) "false" haftmann@34294: haftmann@30929: code_reserved SML haftmann@52435: bool true false haftmann@30929: haftmann@30929: code_reserved OCaml haftmann@52435: bool haftmann@30929: haftmann@34294: code_reserved Scala haftmann@34294: Boolean haftmann@34294: haftmann@52435: code_printing haftmann@52435: constant Not \ haftmann@52435: (SML) "not" and (OCaml) "not" and (Haskell) "not" and (Scala) "'! _" haftmann@52435: | constant HOL.conj \ haftmann@52435: (SML) infixl 1 "andalso" and (OCaml) infixl 3 "&&" and (Haskell) infixr 3 "&&" and (Scala) infixl 3 "&&" haftmann@52435: | constant HOL.disj \ haftmann@52435: (SML) infixl 0 "orelse" and (OCaml) infixl 2 "||" and (Haskell) infixl 2 "||" and (Scala) infixl 1 "||" haftmann@52435: | constant HOL.implies \ haftmann@52435: (SML) "!(if (_)/ then (_)/ else true)" haftmann@52435: and (OCaml) "!(if (_)/ then (_)/ else true)" haftmann@52435: and (Haskell) "!(if (_)/ then (_)/ else True)" haftmann@52435: and (Scala) "!(if ((_))/ (_)/ else true)" haftmann@52435: | constant If \ haftmann@52435: (SML) "!(if (_)/ then (_)/ else (_))" haftmann@52435: and (OCaml) "!(if (_)/ then (_)/ else (_))" haftmann@52435: and (Haskell) "!(if (_)/ then (_)/ else (_))" haftmann@52435: and (Scala) "!(if ((_))/ (_)/ else (_))" haftmann@52435: haftmann@52435: code_reserved SML haftmann@52435: not haftmann@52435: haftmann@52435: code_reserved OCaml haftmann@52435: not haftmann@52435: haftmann@52435: code_identifier haftmann@52435: code_module Pure \ haftmann@52435: (SML) HOL and (OCaml) HOL and (Haskell) HOL and (Scala) HOL haftmann@39026: haftmann@30929: text {* using built-in Haskell equality *} haftmann@30929: haftmann@52435: code_printing haftmann@52435: type_class equal \ (Haskell) "Eq" haftmann@52435: | constant HOL.equal \ (Haskell) infix 4 "==" haftmann@52435: | constant HOL.eq \ (Haskell) infix 4 "==" haftmann@30929: haftmann@30929: text {* undefined *} haftmann@30929: haftmann@52435: code_printing haftmann@52435: constant undefined \ haftmann@52435: (SML) "!(raise/ Fail/ \"undefined\")" haftmann@52435: and (OCaml) "failwith/ \"undefined\"" haftmann@52435: and (Haskell) "error/ \"undefined\"" haftmann@52435: and (Scala) "!sys.error(\"undefined\")" haftmann@52435: haftmann@30929: haftmann@30929: subsubsection {* Evaluation and normalization by evaluation *} haftmann@30929: haftmann@55757: method_setup eval = {* wenzelm@58826: let wenzelm@58826: fun eval_tac ctxt = wenzelm@58826: let val conv = Code_Runtime.dynamic_holds_conv ctxt wenzelm@58839: in wenzelm@58839: CONVERSION (Conv.params_conv ~1 (K (Conv.concl_conv ~1 conv)) ctxt) THEN' wenzelm@59498: resolve_tac ctxt [TrueI] wenzelm@58839: end wenzelm@58826: in wenzelm@58826: Scan.succeed (SIMPLE_METHOD' o eval_tac) wenzelm@58826: end haftmann@55757: *} "solve goal by evaluation" haftmann@30929: haftmann@30929: method_setup normalization = {* wenzelm@46190: Scan.succeed (fn ctxt => wenzelm@46190: SIMPLE_METHOD' wenzelm@46190: (CHANGED_PROP o haftmann@55757: (CONVERSION (Nbe.dynamic_conv ctxt) wenzelm@59498: THEN_ALL_NEW (TRY o resolve_tac ctxt [TrueI])))) haftmann@30929: *} "solve goal by normalization" haftmann@30929: wenzelm@31902: haftmann@33084: subsection {* Counterexample Search Units *} haftmann@33084: haftmann@30929: subsubsection {* Quickcheck *} haftmann@30929: haftmann@33084: quickcheck_params [size = 5, iterations = 50] haftmann@33084: haftmann@30929: haftmann@33084: subsubsection {* Nitpick setup *} blanchet@30309: wenzelm@59028: named_theorems nitpick_unfold "alternative definitions of constants as needed by Nitpick" wenzelm@59028: and nitpick_simp "equational specification of constants as needed by Nitpick" wenzelm@59028: and nitpick_psimp "partial equational specification of constants as needed by Nitpick" wenzelm@59028: and nitpick_choice_spec "choice specification of constants as needed by Nitpick" wenzelm@30980: blanchet@41792: declare if_bool_eq_conj [nitpick_unfold, no_atp] blanchet@41792: if_bool_eq_disj [no_atp] blanchet@41792: blanchet@29863: haftmann@33084: subsection {* Preprocessing for the predicate compiler *} haftmann@33084: wenzelm@59028: named_theorems code_pred_def "alternative definitions of constants for the Predicate Compiler" wenzelm@59028: and code_pred_inline "inlining definitions for the Predicate Compiler" wenzelm@59028: and code_pred_simp "simplification rules for the optimisations in the Predicate Compiler" haftmann@33084: haftmann@33084: haftmann@22839: subsection {* Legacy tactics and ML bindings *} wenzelm@21671: wenzelm@21671: ML {* wenzelm@58826: (* combination of (spec RS spec RS ...(j times) ... spec RS mp) *) wenzelm@58826: local wenzelm@58826: fun wrong_prem (Const (@{const_name All}, _) $ Abs (_, _, t)) = wrong_prem t wenzelm@58826: | wrong_prem (Bound _) = true wenzelm@58826: | wrong_prem _ = false; wenzelm@58826: val filter_right = filter (not o wrong_prem o HOLogic.dest_Trueprop o hd o Thm.prems_of); wenzelm@58826: in wenzelm@58826: fun smp i = funpow i (fn m => filter_right ([spec] RL m)) ([mp]); wenzelm@59498: fun smp_tac ctxt j = EVERY' [dresolve_tac ctxt (smp j), assume_tac ctxt]; wenzelm@58826: end; haftmann@22839: wenzelm@58826: local wenzelm@58826: val nnf_ss = wenzelm@58826: simpset_of (put_simpset HOL_basic_ss @{context} addsimps @{thms simp_thms nnf_simps}); wenzelm@58826: in wenzelm@58826: fun nnf_conv ctxt = Simplifier.rewrite (put_simpset nnf_ss ctxt); wenzelm@58826: end wenzelm@21671: *} wenzelm@21671: haftmann@38866: hide_const (open) eq equal haftmann@38866: kleing@14357: end