(* Title: HOL/HOL.thy Author: Tobias Nipkow, Markus Wenzel, and Larry Paulson
*)
section \<open>The basis of Higher-Order Logic\<close>
theory HOL imports Pure Try0 Tools.Code_Generator
keywords "try""solve_direct""quickcheck""print_coercions""print_claset" "print_induct_rules" :: diag and "quickcheck_params" :: thy_decl
abbrevs "?<" = "\\<^sub>\\<^sub>1" begin
ML \<open>
val _ =
Try.tool_setup
{name = "try0", weight = 30, auto_option = \<^system_option>\<open>auto_methods\<close>,
body = fn auto => fst o Try0.generic_try0 (if auto then Try0.Auto_Try else Try0.Try) NONE Try0.empty_facts} \<close>
ML \<open>Plugin_Name.declare_setup \<^binding>\<open>extraction\<close>\<close>
text\<open>
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 \<open>(P \<longrightarrow> Q) \<longrightarrow> (Q \<longrightarrow> P) \<longrightarrow> (P = Q)\<close> 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). \<close>
subsubsection \<open>Core syntax\<close>
setup\<open>Axclass.class_axiomatization (\<^binding>\<open>type\<close>, [])\<close>
default_sort type setup\<open>Object_Logic.add_base_sort \<^sort>\<open>type\<close>\<close>
text\<open>The input syntax for \<open>eq\<close> is more permissive than the output syntax
because of the large amount of material that relies on infixl.\<close>
subsubsection \<open>Defined connectives and quantifiers\<close>
notation (ASCII)
Not (\<open>(\<open>open_block notation=\<open>prefix ~\<close>\<close>~ _)\<close> [40] 40) and
conj (infixr\<open>&\<close> 35) and
disj (infixr\<open>|\<close> 30) and
implies (infixr\<open>-->\<close> 25) and
not_equal (infix\<open>~=\<close> 50)
abbreviation (iff)
iff :: "[bool, bool] \ bool" (infixr \\\ 25) where"A \ B \ A = B"
syntax"_The" :: "[pttrn, bool] \ 'a" (\(\indent=3 notation=\binder THE\\THE _./ _)\ [0, 10] 10)
syntax_consts "_The"\<rightleftharpoons> The translations"THE x. P"\<rightleftharpoons> "CONST The (\<lambda>x. P)" print_translation\<open>
[(\<^const_syntax>\<open>The\<close>, fn ctxt => fn [Abs abs] => let val (x, t) = Syntax_Trans.atomic_abs_tr' ctxt abs inSyntax.const \<^syntax_const>\<open>_The\<close> $ x $ t end)] \<close> \<comment> \<open>To avoid eta-contraction of body\<close>
notation (ASCII)
All (binder\<open>ALL \<close> 10) and
Ex (binder\<open>EX \<close> 10)
notation (input)
All (binder\<open>! \<close> 10) and
Ex (binder\<open>? \<close> 10)
subsubsection \<open>Axioms and basic definitions\<close>
axiomatizationwhere
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)" \<comment> \<open>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\<close> and
the_eq_trivial: "(THE x. x = a) = (a::'a)"
axiomatizationwhere
impI: "(P \ Q) \ P \ Q" and
mp: "\P \ Q; P\ \ Q" and
True_or_False: "(P = True) \ (P = False)"
definitionIf :: "bool \ 'a \ 'a \ 'a" (\(\notation=\mixfix if expression\\if (_)/ then (_)/ else (_))\ [0, 0, 10] 10) where"If P x y \ (THE z::'a. (P = True \ z = x) \ (P = False \ z = y))"
definitionLet :: "'a \ ('a \ 'b) \ 'b" where"Let s f \ f s"
nonterminal letbinds and letbind
open_bundle let_syntax begin
syntax "_bind" :: "[pttrn, 'a] \ letbind" (\(\indent=2 notation=\mixfix let binding\\_ =/ _)\ 10) "" :: "letbind \ letbinds" (\_\) "_binds" :: "[letbind, letbinds] \ letbinds" (\_;/ _\) "_Let" :: "[letbinds, 'a] \ 'a" (\(\notation=\mixfix let expression\\let (_)/ in (_))\ [0, 10] 10)
syntax_consts "_bind""_binds""_Let"\<rightleftharpoons> Let translations "_Let (_binds b bs) e"\<rightleftharpoons> "_Let b (_Let bs e)" "let x = a in e"\<rightleftharpoons> "CONST Let a (\<lambda>x. e)"
end
axiomatization undefined :: 'a
class default = fixes default :: 'a
subsection \<open>Fundamental rules\<close>
subsubsection \<open>Equality\<close>
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])
text\<open>Useful with \<open>erule\<close> for proving equalities from known equalities.\<close> (* a = b | |
c = d *) lemma box_equals: "\a = b; a = c; b = d\ \ c = d" by (iprover intro: sym trans)
text\<open>For calculational reasoning:\<close>
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 \<open>Congruence rules for application\<close>
text\<open>Similar to \<open>AP_THM\<close> in Gordon's HOL.\<close> lemma fun_cong: "(f :: 'a \ 'b) = g \ f x = g x" by (iprover intro: refl elim: subst)
text\<open>Similar to \<open>AP_TERM\<close> in Gordon's HOL and FOL's \<open>subst_context\<close>.\<close> 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 arg_cong3: "\x = x'; y = y'; z = z'\ \ f x y z = f x' y' z'" by (iprover intro: refl elim: subst)
lemma arg_cong4: "\w = w'; x = x'; y = y'; z = z'\ \ f w x y z = f w' x' y' z'" by (iprover intro: refl elim: subst)
lemma cong: "\f = g; (x::'a) = y\ \ f x = g y" by (iprover intro: refl elim: subst)
ML \<open>fun cong_tac ctxt = Cong_Tac.cong_tac ctxt @{thm cong}\<close>
subsubsection \<open>Equality of booleans -- iff\<close>
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 \<open>True (1)\<close>
lemma TrueI: True unfolding True_def by (rule refl)
lemma impE: assumes"P \ Q" P "Q \ R" shows R by (iprover intro: assms mp)
text\<open>Reduces \<open>Q\<close> to \<open>P \<longrightarrow> Q\<close>, allowing substitution in \<open>P\<close>.\<close> 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 [THENnotE])
text\<open>Not used at all, but we already have the other 3 combinations.\<close> 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 \<open>Disjunction (1)\<close>
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 \<open>Derivation of \<open>iffI\<close>\<close>
text\<open>In an intuitionistic version of HOL \<open>iffI\<close> needs to be an axiom.\<close>
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 \<open>True (2)\<close>
lemma eqTrueI: "P \ P = True" by (iprover intro: iffI TrueI)
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 \<open>Conjunction\<close>
lemma conjI: "\P; Q\ \ P \ Q" unfolding and_def by (iprover intro: impI [THEN allI] 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 \<open>Disjunction (2)\<close>
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 \<open>Classical logic\<close>
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\<open>\<open>notE\<close> with premises exchanged; it discharges \<open>\<not> R\<close> so that it can be used to
make elimination rules.\<close> lemma rev_notE: assumes premp: P and premnot: "\ R \ \ P" shows R by (iprover intro: ccontr notE [OF premnot premp])
text\<open>Double negation law.\<close> 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 \<open>Unique existence\<close>
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\<open>Sometimes easier to use: the premises have no shared variables. Safe!\<close> 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 \<open>Classical intro rules for disjunction and existential quantifiers\<close>
lemma excluded_middle: "\ P \ P" by (iprover intro: disjCI)
text\<open> case distinction as a natural deduction rule. Note that \<open>\<not> P\<close> is the second case, not the first. \<close> 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\<open>Classical implies (\<open>\<longrightarrow>\<close>) elimination.\<close> 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\<open>
This version of \<open>\<longrightarrow>\<close> elimination works on \<open>Q\<close> before \<open>P\<close>. It works best for
those cases in which \<open>P\<close> holds "almost everywhere". Can't install as
default: would break old proofs. \<close> lemma impCE': assumes major: "P \ Q" and minor: "Q \ R" "\ P \ R" shows R using assms by (elim impCE)
text\<open>The analogous introduction rule for conjunction, above, is even constructive\<close> lemma context_disjE: assumes major: "P \ Q" and minor: "P \ R" "\P \ Q \ R" shows R by (iprover intro: disjE [OF major] disjE [OF excluded_middle] assms)
text\<open>Classical \<open>\<longleftrightarrow>\<close> elimination.\<close> 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"])
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
lemmanotE': 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
axiomatizationwhere
eq_reflection: "x = y \ x \ y" \ \admissible axiom\
lemma atomize_all [atomize]: "(\x. P x) \ Trueprop (\x. P x)" proof assume"\x. P x" thenshow"\x. P x" .. next assume"\x. P x" thenshow"\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 thenshow 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 thenshow False by (rule notE) 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
text\<open> Theorems blacklisted toSledgehammer. 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. \<close>
named_theorems no_atp "theorems that should be filtered out by Sledgehammer"
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 \<open> 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 = @{thmnotE}
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; \<close>
setup\<open> (*prevent substitution on bool*) let fun non_bool_eq \<^Const_>\<open>HOL.eq T\<close> = T <> \<^Type>\<open>bool\<close>
| non_bool_eq _ = false; fun hyp_subst_tac' ctxt =
SUBGOAL (fn (goal, i) => ifTerm.exists_subterm 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 \<close>
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 \<open>val HOL_cs = claset_of \<^context>\<close>
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\<open>Better than \<open>ex1E\<close> for classical reasoner: needs no quantifier duplication!\<close> 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\<open>P x\<close> \<section> \<section> by fast qed assumption
text\<open>And again using Uniq\<close> lemma alt_ex1E': assumes"\!x. P x" "\x. \P x; \\<^sub>\\<^sub>1x. P x\ \ R" shows R using assms unfolding Uniq_def by fast
lemma ex1_iff_ex_Uniq: "(\!x. P x) \ (\x. P x) \ (\\<^sub>\\<^sub>1x. P x)" unfolding Uniq_def by fast
ML \<open> structure Blast = Blast
( structure Classical = Classical
val Trueprop_const = dest_Const \<^Const>\<open>Trueprop\<close>
val equality_name = \<^const_name>\<open>HOL.eq\<close>
val not_name = \<^const_name>\<open>Not\<close>
val notE = @{thmnotE}
val ccontr = @{thm ccontr}
val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
);
val blast_tac = Blast.blast_tac; \<close>
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\<open>Easier to apply than \<open>theI\<close>: only one occurrence of \<open>P\<close>.\<close> 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': "\\\<^sub>\\<^sub>1x. 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 \<open>Simplifier\<close>
lemma eta_contract_eq: "(\s. f s) = f" ..
lemma subst_all: \<open>(\<And>x. x = a \<Longrightarrow> PROP P x) \<equiv> PROP P a\<close> \<open>(\<And>x. a = x \<Longrightarrow> PROP P x) \<equiv> PROP P a\<close> proof - show\<open>(\<And>x. x = a \<Longrightarrow> PROP P x) \<equiv> PROP P a\<close> proof (rule equal_intr_rule) assume *: \<open>\<And>x. x = a \<Longrightarrow> PROP P x\<close> show\<open>PROP P a\<close> by (rule *) (rule refl) next fix x assume\<open>PROP P a\<close> and \<open>x = a\<close> from\<open>x = a\<close> have \<open>x \<equiv> a\<close> by (rule eq_reflection) with\<open>PROP P a\<close> show \<open>PROP P x\<close> by simp qed show\<open>(\<And>x. a = x \<Longrightarrow> PROP P x) \<equiv> PROP P a\<close> proof (rule equal_intr_rule) assume *: \<open>\<And>x. a = x \<Longrightarrow> PROP P x\<close> show\<open>PROP P a\<close> by (rule *) (rule refl) next fix x assume\<open>PROP P a\<close> and \<open>a = x\<close> from\<open>a = x\<close> have \<open>a \<equiv> x\<close> by (rule eq_reflection) with\<open>PROP P a\<close> show \<open>PROP P x\<close> 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
text\<open>These two are specialized, but \<open>imp_disj_not1\<close> is useful in \<open>Auth/Yahalom\<close>.\<close> 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 cases_simp: "(P \ Q) \ (\ P \ Q) \ Q" \<comment> \<open>Avoids duplication of subgoals after \<open>if_split\<close>, when the true and false\<close> \<comment> \<open>cases boil down to the same thing.\<close> 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 lemma all_imp_conj_distrib: "(\x. P x \ Q x \ R x) \ (\x. P x \ Q x) \ (\x. P x \R x)" by iprover
text\<open> \<^medskip> The \<open>\<and>\<close> congruence rule: not included by default!
May slow rewrite proofs down by as much as 50\%\<close>
text\<open>The \<open>|\<close> congruence rule: not included by default!\<close>
lemma disj_cong: "P = P' \ (\ P' \ Q = Q') \ (P \ Q) = (P' \ Q')" by blast
text\<open>\<^medskip> if-then-else rules\<close>
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))" \<comment> \<open>This form is useful for expanding \<open>if\<close>s on the RIGHT of the \<open>\<Longrightarrow>\<close> symbol.\<close> by (rule if_split)
lemma if_bool_eq_disj: "(if P then Q else R) = ((P \ Q) \ (\ P \ R))" \<comment> \<open>And this form is useful for expanding \<open>if\<close>s on the LEFT.\<close> 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\<open>\<^medskip> let rules for simproc\<close>
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\<open>
The following copy of the implication operator is useful for
fine-tuning congruence rules. It instructs the simplifier to simplify
its premise. \<close>
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) thenhave"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) thenhave"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 \<open>Tools/simpdata.ML\<close>
ML \<open>open Simpdata\<close>
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\<open>Simproc for proving \<open>(y = x) \<equiv> False\<close> from premise \<open>\<not> (x = y)\<close>:\<close>
simproc_setup neq ("x = y") = \<open> let
val neq_to_EQ_False = @{thm not_sym} RS @{thm Eq_FalseI}; fun is_neq eq lhs rhs thm =
(caseThm.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 =
(caseThm.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 K proc end \<close>
simproc_setup let_simp ("Let x f") = \<open> 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_>\<open>Let _ _ for x t\<close> =
(case t of
Abs (_, _, t') => count_loose t' 0 <= 1
| _ => true); in
K (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_>\Let _ _ for 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 \<close>
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" thenshow"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)
simproc_setup eliminate_false_implies ("False \ PROP P") = \ let fun conv n = if n > 1 then
Conv.rewr_conv @{thm Pure.swap_prems_eq}
then_conv Conv.arg_conv (conv (n - 1))
then_conv Conv.rewr_conv @{thm HOL.implies_True_equals}
else
Conv.rewr_conv @{thm HOL.False_implies_equals} in
fn _ => fn _ => fn ct => let
val t = Thm.term_of ct
val n = length (Logic.strip_imp_prems t) in
(case Logic.strip_imp_concl t of \<^Const_>\<open>Trueprop for _\<close> => SOME (conv n ct)
| _ => NONE) end end \<close>
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))" \<comment> \<open>Miniscoping: pushing in existential quantifiers.\<close> 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))" \<comment> \<open>Miniscoping: pushing in universal quantifiers.\<close> by (iprover | blast)+
lemmas [simp] =
triv_forall_equality \<comment> \<open>prunes params\<close>
True_implies_equals implies_True_equals \<comment> \<open>prune \<open>True\<close> in asms\<close>
False_implies_equals \<comment> \<open>prune \<open>False\<close> in asms\<close>
if_True
if_False
if_cancel
if_eq_cancel
imp_disjL \<comment> \<open>In general it seems wrong to add distributive laws by default: they
might cause exponential blow-up. But \<open>imp_disjL\<close> has been in for a while and cannot be removed without affecting existing proofs. Moreover,
rewriting by\<open>(P \<or> Q \<longrightarrow> R) = ((P \<longrightarrow> R) \<and> (Q \<longrightarrow> R))\<close> might be justified on the
grounds that it allows simplification of \<open>R\<close> in the two cases.\<close>
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
ML \<open>val HOL_ss = simpset_of \<^context>\<close>
text\<open>Simplifies \<open>x\<close> assuming \<open>c\<close> and \<open>y\<close> assuming \<open>\<not> c\<close>.\<close> 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\<open>Prevents simplification of \<open>x\<close> and \<open>y\<close>:
faster and allows the execution of functional programs.\<close> 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\<open>Prevents simplification of t: much faster\<close> 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\<open>To tidy up the result of a simproc. Only the RHS will be simplified.\<close> 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\<open>As a simplification rule, it replaces all function equalities by
first-order equalities.\<close> lemma fun_eq_iff: "f = g \ (\x. f x = g x)" by auto
subsubsection \<open>Generic cases and induction\<close>
text\<open>Rule projections:\<close>
ML \<open> structure Project_Rule = Project_Rule
(
val conjunct1 = @{thm conjunct1}
val conjunct2 = @{thm conjunct2}
val mp = @{thm mp}
); \<close>
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)
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
text\<open>Pre-simplification of induction and cases rules\<close>
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" thenshow"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" thenshow"PROP P x"by simp qed
ML \<open> signature REORIENT_PROC =
sig
val add : (term -> bool) -> theory -> theory
val proc : Simplifier.proc 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 ctxt ct = let
val thy = Proof_Context.theory_of ctxt; in caseThm.term_of ct of
(_ $ t $ u) => if matches thy u then NONE else SOME meta_reorient
| _ => NONE end; end; \<close>
subsection \<open>Other simple lemmas and lemma duplicates\<close>
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 thenhave *: "\x. P x (THE y. P x y)" by (best intro: theI') show ?rhs by (rule ex1I) (use L * in\<open>fast+\<close>) next fix x assume R: ?rhs thenobtain 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
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
