src/HOL/HOL.thy
 changeset 63575 b9bd9e61fd63 parent 63561 fba08009ff3e child 63909 cc15bd7c5396
1.1 --- a/src/HOL/HOL.thy	Mon Aug 01 13:51:17 2016 +0200
1.2 +++ b/src/HOL/HOL.thy	Mon Aug 01 22:11:29 2016 +0200
1.3 @@ -218,20 +218,20 @@
1.4    by (rule trans [OF _ sym])
1.6  lemma meta_eq_to_obj_eq:
1.7 -  assumes meq: "A \<equiv> B"
1.8 +  assumes "A \<equiv> B"
1.9    shows "A = B"
1.10 -  by (unfold meq) (rule refl)
1.11 +  unfolding assms by (rule refl)
1.13  text \<open>Useful with \<open>erule\<close> for proving equalities from known equalities.\<close>
1.14       (* a = b
1.15          |   |
1.16          c = d   *)
1.17  lemma box_equals: "\<lbrakk>a = b; a = c; b = d\<rbrakk> \<Longrightarrow> c = d"
1.18 -apply (rule trans)
1.19 -apply (rule trans)
1.20 -apply (rule sym)
1.21 -apply assumption+
1.22 -done
1.23 +  apply (rule trans)
1.24 +   apply (rule trans)
1.25 +    apply (rule sym)
1.26 +    apply assumption+
1.27 +  done
1.29  text \<open>For calculational reasoning:\<close>
1.31 @@ -246,25 +246,25 @@
1.33  text \<open>Similar to \<open>AP_THM\<close> in Gordon's HOL.\<close>
1.34  lemma fun_cong: "(f :: 'a \<Rightarrow> 'b) = g \<Longrightarrow> f x = g x"
1.35 -apply (erule subst)
1.36 -apply (rule refl)
1.37 -done
1.38 +  apply (erule subst)
1.39 +  apply (rule refl)
1.40 +  done
1.42  text \<open>Similar to \<open>AP_TERM\<close> in Gordon's HOL and FOL's \<open>subst_context\<close>.\<close>
1.43  lemma arg_cong: "x = y \<Longrightarrow> f x = f y"
1.44 -apply (erule subst)
1.45 -apply (rule refl)
1.46 -done
1.47 +  apply (erule subst)
1.48 +  apply (rule refl)
1.49 +  done
1.51  lemma arg_cong2: "\<lbrakk>a = b; c = d\<rbrakk> \<Longrightarrow> f a c = f b d"
1.52 -apply (erule ssubst)+
1.53 -apply (rule refl)
1.54 -done
1.55 +  apply (erule ssubst)+
1.56 +  apply (rule refl)
1.57 +  done
1.59  lemma cong: "\<lbrakk>f = g; (x::'a) = y\<rbrakk> \<Longrightarrow> f x = g y"
1.60 -apply (erule subst)+
1.61 -apply (rule refl)
1.62 -done
1.63 +  apply (erule subst)+
1.64 +  apply (rule refl)
1.65 +  done
1.67  ML \<open>fun cong_tac ctxt = Cong_Tac.cong_tac ctxt @{thm cong}\<close>
1.69 @@ -295,7 +295,7 @@
1.71  subsubsection \<open>True\<close>
1.73 -lemma TrueI: "True"
1.74 +lemma TrueI: True
1.75    unfolding True_def by (rule refl)
1.77  lemma eqTrueI: "P \<Longrightarrow> P = True"
1.78 @@ -307,14 +307,16 @@
1.80  subsubsection \<open>Universal quantifier\<close>
1.82 -lemma allI: assumes "\<And>x::'a. P x" shows "\<forall>x. P x"
1.83 +lemma allI:
1.84 +  assumes "\<And>x::'a. P x"
1.85 +  shows "\<forall>x. P x"
1.86    unfolding All_def by (iprover intro: ext eqTrueI assms)
1.88  lemma spec: "\<forall>x::'a. P x \<Longrightarrow> P x"
1.89 -apply (unfold All_def)
1.90 -apply (rule eqTrueE)
1.91 -apply (erule fun_cong)
1.92 -done
1.93 +  apply (unfold All_def)
1.94 +  apply (rule eqTrueE)
1.95 +  apply (erule fun_cong)
1.96 +  done
1.98  lemma allE:
1.99    assumes major: "\<forall>x. P x"
1.100 @@ -380,24 +382,24 @@
1.101  lemma impE:
1.102    assumes "P \<longrightarrow> Q" P "Q \<Longrightarrow> R"
1.103    shows R
1.104 -by (iprover intro: assms mp)
1.105 +  by (iprover intro: assms mp)
1.107 -(* Reduces Q to P \<longrightarrow> Q, allowing substitution in P. *)
1.108 +text \<open>Reduces \<open>Q\<close> to \<open>P \<longrightarrow> Q\<close>, allowing substitution in \<open>P\<close>.\<close>
1.109  lemma rev_mp: "\<lbrakk>P; P \<longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
1.110 -by (iprover intro: mp)
1.111 +  by (iprover intro: mp)
1.113  lemma contrapos_nn:
1.114    assumes major: "\<not> Q"
1.115 -      and minor: "P \<Longrightarrow> Q"
1.116 +    and minor: "P \<Longrightarrow> Q"
1.117    shows "\<not> P"
1.118 -by (iprover intro: notI minor major [THEN notE])
1.119 +  by (iprover intro: notI minor major [THEN notE])
1.121 -(*not used at all, but we already have the other 3 combinations *)
1.122 +text \<open>Not used at all, but we already have the other 3 combinations.\<close>
1.123  lemma contrapos_pn:
1.124    assumes major: "Q"
1.125 -      and minor: "P \<Longrightarrow> \<not> Q"
1.126 +    and minor: "P \<Longrightarrow> \<not> Q"
1.127    shows "\<not> P"
1.128 -by (iprover intro: notI minor major notE)
1.129 +  by (iprover intro: notI minor major notE)
1.131  lemma not_sym: "t \<noteq> s \<Longrightarrow> s \<noteq> t"
1.132    by (erule contrapos_nn) (erule sym)
1.133 @@ -409,69 +411,56 @@
1.134  subsubsection \<open>Existential quantifier\<close>
1.136  lemma exI: "P x \<Longrightarrow> \<exists>x::'a. P x"
1.137 -apply (unfold Ex_def)
1.138 -apply (iprover intro: allI allE impI mp)
1.139 -done
1.140 +  unfolding Ex_def by (iprover intro: allI allE impI mp)
1.142  lemma exE:
1.143    assumes major: "\<exists>x::'a. P x"
1.144 -      and minor: "\<And>x. P x \<Longrightarrow> Q"
1.145 +    and minor: "\<And>x. P x \<Longrightarrow> Q"
1.146    shows "Q"
1.147 -apply (rule major [unfolded Ex_def, THEN spec, THEN mp])
1.148 -apply (iprover intro: impI [THEN allI] minor)
1.149 -done
1.150 +  by (rule major [unfolded Ex_def, THEN spec, THEN mp]) (iprover intro: impI [THEN allI] minor)
1.153  subsubsection \<open>Conjunction\<close>
1.155  lemma conjI: "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> P \<and> Q"
1.156 -apply (unfold and_def)
1.157 -apply (iprover intro: impI [THEN allI] mp)
1.158 -done
1.159 +  unfolding and_def by (iprover intro: impI [THEN allI] mp)
1.161  lemma conjunct1: "\<lbrakk>P \<and> Q\<rbrakk> \<Longrightarrow> P"
1.162 -apply (unfold and_def)
1.163 -apply (iprover intro: impI dest: spec mp)
1.164 -done
1.165 +  unfolding and_def by (iprover intro: impI dest: spec mp)
1.167  lemma conjunct2: "\<lbrakk>P \<and> Q\<rbrakk> \<Longrightarrow> Q"
1.168 -apply (unfold and_def)
1.169 -apply (iprover intro: impI dest: spec mp)
1.170 -done
1.171 +  unfolding and_def by (iprover intro: impI dest: spec mp)
1.173  lemma conjE:
1.174    assumes major: "P \<and> Q"
1.175 -      and minor: "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> R"
1.176 +    and minor: "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> R"
1.177    shows R
1.178 -apply (rule minor)
1.179 -apply (rule major [THEN conjunct1])
1.180 -apply (rule major [THEN conjunct2])
1.181 -done
1.182 +  apply (rule minor)
1.183 +   apply (rule major [THEN conjunct1])
1.184 +  apply (rule major [THEN conjunct2])
1.185 +  done
1.187  lemma context_conjI:
1.188 -  assumes P "P \<Longrightarrow> Q" shows "P \<and> Q"
1.189 -by (iprover intro: conjI assms)
1.190 +  assumes P "P \<Longrightarrow> Q"
1.191 +  shows "P \<and> Q"
1.192 +  by (iprover intro: conjI assms)
1.195  subsubsection \<open>Disjunction\<close>
1.197  lemma disjI1: "P \<Longrightarrow> P \<or> Q"
1.198 -apply (unfold or_def)
1.199 -apply (iprover intro: allI impI mp)
1.200 -done
1.201 +  unfolding or_def by (iprover intro: allI impI mp)
1.203  lemma disjI2: "Q \<Longrightarrow> P \<or> Q"
1.204 -apply (unfold or_def)
1.205 -apply (iprover intro: allI impI mp)
1.206 -done
1.207 +  unfolding or_def by (iprover intro: allI impI mp)
1.209  lemma disjE:
1.210    assumes major: "P \<or> Q"
1.211 -      and minorP: "P \<Longrightarrow> R"
1.212 -      and minorQ: "Q \<Longrightarrow> R"
1.213 +    and minorP: "P \<Longrightarrow> R"
1.214 +    and minorQ: "Q \<Longrightarrow> R"
1.215    shows R
1.216 -by (iprover intro: minorP minorQ impI
1.217 -                 major [unfolded or_def, THEN spec, THEN mp, THEN mp])
1.218 +  by (iprover intro: minorP minorQ impI
1.219 +      major [unfolded or_def, THEN spec, THEN mp, THEN mp])
1.222  subsubsection \<open>Classical logic\<close>
1.223 @@ -479,37 +468,37 @@
1.224  lemma classical:
1.225    assumes prem: "\<not> P \<Longrightarrow> P"
1.226    shows P
1.227 -apply (rule True_or_False [THEN disjE, THEN eqTrueE])
1.228 -apply assumption
1.229 -apply (rule notI [THEN prem, THEN eqTrueI])
1.230 -apply (erule subst)
1.231 -apply assumption
1.232 -done
1.233 +  apply (rule True_or_False [THEN disjE, THEN eqTrueE])
1.234 +   apply assumption
1.235 +  apply (rule notI [THEN prem, THEN eqTrueI])
1.236 +  apply (erule subst)
1.237 +  apply assumption
1.238 +  done
1.240  lemmas ccontr = FalseE [THEN classical]
1.242 -(*notE with premises exchanged; it discharges \<not> R so that it can be used to
1.243 -  make elimination rules*)
1.244 +text \<open>\<open>notE\<close> with premises exchanged; it discharges \<open>\<not> R\<close> so that it can be used to
1.245 +  make elimination rules.\<close>
1.246  lemma rev_notE:
1.247    assumes premp: P
1.248 -      and premnot: "\<not> R \<Longrightarrow> \<not> P"
1.249 +    and premnot: "\<not> R \<Longrightarrow> \<not> P"
1.250    shows R
1.251 -apply (rule ccontr)
1.252 -apply (erule notE [OF premnot premp])
1.253 -done
1.254 +  apply (rule ccontr)
1.255 +  apply (erule notE [OF premnot premp])
1.256 +  done
1.258 -(*Double negation law*)
1.259 +text \<open>Double negation law.\<close>
1.260  lemma notnotD: "\<not>\<not> P \<Longrightarrow> P"
1.261 -apply (rule classical)
1.262 -apply (erule notE)
1.263 -apply assumption
1.264 -done
1.265 +  apply (rule classical)
1.266 +  apply (erule notE)
1.267 +  apply assumption
1.268 +  done
1.270  lemma contrapos_pp:
1.271    assumes p1: Q
1.272 -      and p2: "\<not> P \<Longrightarrow> \<not> Q"
1.273 +    and p2: "\<not> P \<Longrightarrow> \<not> Q"
1.274    shows P
1.275 -by (iprover intro: classical p1 p2 notE)
1.276 +  by (iprover intro: classical p1 p2 notE)
1.279  subsubsection \<open>Unique existence\<close>
1.280 @@ -517,90 +506,87 @@
1.281  lemma ex1I:
1.282    assumes "P a" "\<And>x. P x \<Longrightarrow> x = a"
1.283    shows "\<exists>!x. P x"
1.284 -by (unfold Ex1_def, iprover intro: assms exI conjI allI impI)
1.285 +  unfolding Ex1_def by (iprover intro: assms exI conjI allI impI)
1.287 -text\<open>Sometimes easier to use: the premises have no shared variables.  Safe!\<close>
1.288 +text \<open>Sometimes easier to use: the premises have no shared variables. Safe!\<close>
1.289  lemma ex_ex1I:
1.290    assumes ex_prem: "\<exists>x. P x"
1.291 -      and eq: "\<And>x y. \<lbrakk>P x; P y\<rbrakk> \<Longrightarrow> x = y"
1.292 +    and eq: "\<And>x y. \<lbrakk>P x; P y\<rbrakk> \<Longrightarrow> x = y"
1.293    shows "\<exists>!x. P x"
1.294 -by (iprover intro: ex_prem [THEN exE] ex1I eq)
1.295 +  by (iprover intro: ex_prem [THEN exE] ex1I eq)
1.297  lemma ex1E:
1.298    assumes major: "\<exists>!x. P x"
1.299 -      and minor: "\<And>x. \<lbrakk>P x; \<forall>y. P y \<longrightarrow> y = x\<rbrakk> \<Longrightarrow> R"
1.300 +    and minor: "\<And>x. \<lbrakk>P x; \<forall>y. P y \<longrightarrow> y = x\<rbrakk> \<Longrightarrow> R"
1.301    shows R
1.302 -apply (rule major [unfolded Ex1_def, THEN exE])
1.303 -apply (erule conjE)
1.304 -apply (iprover intro: minor)
1.305 -done
1.306 +  apply (rule major [unfolded Ex1_def, THEN exE])
1.307 +  apply (erule conjE)
1.308 +  apply (iprover intro: minor)
1.309 +  done
1.311  lemma ex1_implies_ex: "\<exists>!x. P x \<Longrightarrow> \<exists>x. P x"
1.312 -apply (erule ex1E)
1.313 -apply (rule exI)
1.314 -apply assumption
1.315 -done
1.316 +  apply (erule ex1E)
1.317 +  apply (rule exI)
1.318 +  apply assumption
1.319 +  done
1.322  subsubsection \<open>Classical intro rules for disjunction and existential quantifiers\<close>
1.324  lemma disjCI:
1.325 -  assumes "\<not> Q \<Longrightarrow> P" shows "P \<or> Q"
1.326 -apply (rule classical)
1.327 -apply (iprover intro: assms disjI1 disjI2 notI elim: notE)
1.328 -done
1.329 +  assumes "\<not> Q \<Longrightarrow> P"
1.330 +  shows "P \<or> Q"
1.331 +  by (rule classical) (iprover intro: assms disjI1 disjI2 notI elim: notE)
1.333  lemma excluded_middle: "\<not> P \<or> P"
1.334 -by (iprover intro: disjCI)
1.335 +  by (iprover intro: disjCI)
1.337  text \<open>
1.338    case distinction as a natural deduction rule.
1.339 -  Note that @{term "\<not> P"} is the second case, not the first
1.340 +  Note that \<open>\<not> P\<close> is the second case, not the first.
1.341  \<close>
1.342  lemma case_split [case_names True False]:
1.343    assumes prem1: "P \<Longrightarrow> Q"
1.344 -      and prem2: "\<not> P \<Longrightarrow> Q"
1.345 +    and prem2: "\<not> P \<Longrightarrow> Q"
1.346    shows Q
1.347 -apply (rule excluded_middle [THEN disjE])
1.348 -apply (erule prem2)
1.349 -apply (erule prem1)
1.350 -done
1.351 +  apply (rule excluded_middle [THEN disjE])
1.352 +   apply (erule prem2)
1.353 +  apply (erule prem1)
1.354 +  done
1.356 -(*Classical implies (\<longrightarrow>) elimination. *)
1.357 +text \<open>Classical implies (\<open>\<longrightarrow>\<close>) elimination.\<close>
1.358  lemma impCE:
1.359    assumes major: "P \<longrightarrow> Q"
1.360 -      and minor: "\<not> P \<Longrightarrow> R" "Q \<Longrightarrow> R"
1.361 +    and minor: "\<not> P \<Longrightarrow> R" "Q \<Longrightarrow> R"
1.362    shows R
1.363 -apply (rule excluded_middle [of P, THEN disjE])
1.364 -apply (iprover intro: minor major [THEN mp])+
1.365 -done
1.366 +  apply (rule excluded_middle [of P, THEN disjE])
1.367 +   apply (iprover intro: minor major [THEN mp])+
1.368 +  done
1.370 -(*This version of \<longrightarrow> elimination works on Q before P.  It works best for
1.371 -  those cases in which P holds "almost everywhere".  Can't install as
1.372 -  default: would break old proofs.*)
1.373 +text \<open>
1.374 +  This version of \<open>\<longrightarrow>\<close> elimination works on \<open>Q\<close> before \<open>P\<close>.  It works best for
1.375 +  those cases in which \<open>P\<close> holds "almost everywhere".  Can't install as
1.376 +  default: would break old proofs.
1.377 +\<close>
1.378  lemma impCE':
1.379    assumes major: "P \<longrightarrow> Q"
1.380 -      and minor: "Q \<Longrightarrow> R" "\<not> P \<Longrightarrow> R"
1.381 +    and minor: "Q \<Longrightarrow> R" "\<not> P \<Longrightarrow> R"
1.382    shows R
1.383 -apply (rule excluded_middle [of P, THEN disjE])
1.384 -apply (iprover intro: minor major [THEN mp])+
1.385 -done
1.386 +  apply (rule excluded_middle [of P, THEN disjE])
1.387 +   apply (iprover intro: minor major [THEN mp])+
1.388 +  done
1.390 -(*Classical <-> elimination. *)
1.391 +text \<open>Classical \<open>\<longleftrightarrow>\<close> elimination.\<close>
1.392  lemma iffCE:
1.393    assumes major: "P = Q"
1.394 -      and minor: "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> R" "\<lbrakk>\<not> P; \<not> Q\<rbrakk> \<Longrightarrow> R"
1.395 +    and minor: "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> R" "\<lbrakk>\<not> P; \<not> Q\<rbrakk> \<Longrightarrow> R"
1.396    shows R
1.397 -apply (rule major [THEN iffE])
1.398 -apply (iprover intro: minor elim: impCE notE)
1.399 -done
1.400 +  by (rule major [THEN iffE]) (iprover intro: minor elim: impCE notE)
1.402  lemma exCI:
1.403    assumes "\<forall>x. \<not> P x \<Longrightarrow> P a"
1.404    shows "\<exists>x. P x"
1.405 -apply (rule ccontr)
1.406 -apply (iprover intro: assms exI allI notI notE [of "\<exists>x. P x"])
1.407 -done
1.408 +  by (rule ccontr) (iprover intro: assms exI allI notI notE [of "\<exists>x. P x"])
1.411  subsubsection \<open>Intuitionistic Reasoning\<close>
1.412 @@ -650,7 +636,7 @@
1.413  subsubsection \<open>Atomizing meta-level connectives\<close>
1.415  axiomatization where
1.416 -  eq_reflection: "x = y \<Longrightarrow> x \<equiv> y" (*admissible axiom*)
1.417 +  eq_reflection: "x = y \<Longrightarrow> x \<equiv> y"  \<comment> \<open>admissible axiom\<close>
1.419  lemma atomize_all [atomize]: "(\<And>x. P x) \<equiv> Trueprop (\<forall>x. P x)"
1.420  proof
1.421 @@ -731,9 +717,9 @@
1.422  subsubsection \<open>Sledgehammer setup\<close>
1.424  text \<open>
1.425 -Theorems blacklisted to Sledgehammer. These theorems typically produce clauses
1.426 -that are prolific (match too many equality or membership literals) and relate to
1.427 -seldom-used facts. Some duplicate other rules.
1.428 +  Theorems blacklisted to Sledgehammer. These theorems typically produce clauses
1.429 +  that are prolific (match too many equality or membership literals) and relate to
1.430 +  seldom-used facts. Some duplicate other rules.
1.431  \<close>
1.433  named_theorems no_atp "theorems that should be filtered out by Sledgehammer"
1.434 @@ -830,18 +816,18 @@
1.435  lemmas [intro?] = ext
1.436    and [elim?] = ex1_implies_ex
1.438 -(*Better then ex1E for classical reasoner: needs no quantifier duplication!*)
1.439 +text \<open>Better than \<open>ex1E\<close> for classical reasoner: needs no quantifier duplication!\<close>
1.440  lemma alt_ex1E [elim!]:
1.441    assumes major: "\<exists>!x. P x"
1.442 -      and prem: "\<And>x. \<lbrakk> P x; \<forall>y y'. P y \<and> P y' \<longrightarrow> y = y' \<rbrakk> \<Longrightarrow> R"
1.443 +    and prem: "\<And>x. \<lbrakk>P x; \<forall>y y'. P y \<and> P y' \<longrightarrow> y = y'\<rbrakk> \<Longrightarrow> R"
1.444    shows R
1.445 -apply (rule ex1E [OF major])
1.446 -apply (rule prem)
1.447 -apply assumption
1.448 -apply (rule allI)+
1.449 -apply (tactic \<open>eresolve_tac @{context} [Classical.dup_elim @{context} @{thm allE}] 1\<close>)
1.450 -apply iprover
1.451 -done
1.452 +  apply (rule ex1E [OF major])
1.453 +  apply (rule prem)
1.454 +   apply assumption
1.455 +  apply (rule allI)+
1.456 +  apply (tactic \<open>eresolve_tac @{context} [Classical.dup_elim @{context} @{thm allE}] 1\<close>)
1.457 +  apply iprover
1.458 +  done
1.460  ML \<open>
1.461    structure Blast = Blast
1.462 @@ -862,27 +848,29 @@
1.464  lemma the_equality [intro]:
1.465    assumes "P a"
1.466 -      and "\<And>x. P x \<Longrightarrow> x = a"
1.467 +    and "\<And>x. P x \<Longrightarrow> x = a"
1.468    shows "(THE x. P x) = a"
1.469    by (blast intro: assms trans [OF arg_cong [where f=The] the_eq_trivial])
1.471  lemma theI:
1.472 -  assumes "P a" and "\<And>x. P x \<Longrightarrow> x = a"
1.473 +  assumes "P a"
1.474 +    and "\<And>x. P x \<Longrightarrow> x = a"
1.475    shows "P (THE x. P x)"
1.476 -by (iprover intro: assms the_equality [THEN ssubst])
1.477 +  by (iprover intro: assms the_equality [THEN ssubst])
1.479  lemma theI': "\<exists>!x. P x \<Longrightarrow> P (THE x. P x)"
1.480    by (blast intro: theI)
1.482 -(*Easier to apply than theI: only one occurrence of P*)
1.483 +text \<open>Easier to apply than \<open>theI\<close>: only one occurrence of \<open>P\<close>.\<close>
1.484  lemma theI2:
1.485    assumes "P a" "\<And>x. P x \<Longrightarrow> x = a" "\<And>x. P x \<Longrightarrow> Q x"
1.486    shows "Q (THE x. P x)"
1.487 -by (iprover intro: assms theI)
1.488 +  by (iprover intro: assms theI)
1.490 -lemma the1I2: assumes "\<exists>!x. P x" "\<And>x. P x \<Longrightarrow> Q x" shows "Q (THE x. P x)"
1.491 -by(iprover intro:assms(2) theI2[where P=P and Q=Q] ex1E[OF assms(1)]
1.492 -           elim:allE impE)
1.493 +lemma the1I2:
1.494 +  assumes "\<exists>!x. P x" "\<And>x. P x \<Longrightarrow> Q x"
1.495 +  shows "Q (THE x. P x)"
1.496 +  by (iprover intro: assms(2) theI2[where P=P and Q=Q] ex1E[OF assms(1)] elim: allE impE)
1.498  lemma the1_equality [elim?]: "\<lbrakk>\<exists>!x. P x; P a\<rbrakk> \<Longrightarrow> (THE x. P x) = a"
1.499    by blast
1.500 @@ -929,136 +917,136 @@
1.501      "\<And>P. (\<forall>x. t = x \<longrightarrow> P x) = P t"
1.502    by (blast, blast, blast, blast, blast, iprover+)
1.504 -lemma disj_absorb: "(A \<or> A) = A"
1.505 +lemma disj_absorb: "A \<or> A \<longleftrightarrow> A"
1.506    by blast
1.508 -lemma disj_left_absorb: "(A \<or> (A \<or> B)) = (A \<or> B)"
1.509 +lemma disj_left_absorb: "A \<or> (A \<or> B) \<longleftrightarrow> A \<or> B"
1.510    by blast
1.512 -lemma conj_absorb: "(A \<and> A) = A"
1.513 +lemma conj_absorb: "A \<and> A \<longleftrightarrow> A"
1.514    by blast
1.516 -lemma conj_left_absorb: "(A \<and> (A \<and> B)) = (A \<and> B)"
1.517 +lemma conj_left_absorb: "A \<and> (A \<and> B) \<longleftrightarrow> A \<and> B"
1.518    by blast
1.520  lemma eq_ac:
1.521    shows eq_commute: "a = b \<longleftrightarrow> b = a"
1.522      and iff_left_commute: "(P \<longleftrightarrow> (Q \<longleftrightarrow> R)) \<longleftrightarrow> (Q \<longleftrightarrow> (P \<longleftrightarrow> R))"
1.523 -    and iff_assoc: "((P \<longleftrightarrow> Q) \<longleftrightarrow> R) \<longleftrightarrow> (P \<longleftrightarrow> (Q \<longleftrightarrow> R))" by (iprover, blast+)
1.524 +    and iff_assoc: "((P \<longleftrightarrow> Q) \<longleftrightarrow> R) \<longleftrightarrow> (P \<longleftrightarrow> (Q \<longleftrightarrow> R))"
1.525 +  by (iprover, blast+)
1.527  lemma neq_commute: "a \<noteq> b \<longleftrightarrow> b \<noteq> a" by iprover
1.529  lemma conj_comms:
1.530 -  shows conj_commute: "(P \<and> Q) = (Q \<and> P)"
1.531 -    and conj_left_commute: "(P \<and> (Q \<and> R)) = (Q \<and> (P \<and> R))" by iprover+
1.532 -lemma conj_assoc: "((P \<and> Q) \<and> R) = (P \<and> (Q \<and> R))" by iprover
1.533 +  shows conj_commute: "P \<and> Q \<longleftrightarrow> Q \<and> P"
1.534 +    and conj_left_commute: "P \<and> (Q \<and> R) \<longleftrightarrow> Q \<and> (P \<and> R)" by iprover+
1.535 +lemma conj_assoc: "(P \<and> Q) \<and> R \<longleftrightarrow> P \<and> (Q \<and> R)" by iprover
1.537  lemmas conj_ac = conj_commute conj_left_commute conj_assoc
1.539  lemma disj_comms:
1.540 -  shows disj_commute: "(P \<or> Q) = (Q \<or> P)"
1.541 -    and disj_left_commute: "(P \<or> (Q \<or> R)) = (Q \<or> (P \<or> R))" by iprover+
1.542 -lemma disj_assoc: "((P \<or> Q) \<or> R) = (P \<or> (Q \<or> R))" by iprover
1.543 +  shows disj_commute: "P \<or> Q \<longleftrightarrow> Q \<or> P"
1.544 +    and disj_left_commute: "P \<or> (Q \<or> R) \<longleftrightarrow> Q \<or> (P \<or> R)" by iprover+
1.545 +lemma disj_assoc: "(P \<or> Q) \<or> R \<longleftrightarrow> P \<or> (Q \<or> R)" by iprover
1.547  lemmas disj_ac = disj_commute disj_left_commute disj_assoc
1.549 -lemma conj_disj_distribL: "(P \<and> (Q \<or> R)) = (P \<and> Q \<or> P \<and> R)" by iprover
1.550 -lemma conj_disj_distribR: "((P \<or> Q) \<and> R) = (P \<and> R \<or> Q \<and> R)" by iprover
1.551 +lemma conj_disj_distribL: "P \<and> (Q \<or> R) \<longleftrightarrow> P \<and> Q \<or> P \<and> R" by iprover
1.552 +lemma conj_disj_distribR: "(P \<or> Q) \<and> R \<longleftrightarrow> P \<and> R \<or> Q \<and> R" by iprover
1.554 -lemma disj_conj_distribL: "(P \<or> (Q \<and> R)) = ((P \<or> Q) \<and> (P \<or> R))" by iprover
1.555 -lemma disj_conj_distribR: "((P \<and> Q) \<or> R) = ((P \<or> R) \<and> (Q \<or> R))" by iprover
1.556 +lemma disj_conj_distribL: "P \<or> (Q \<and> R) \<longleftrightarrow> (P \<or> Q) \<and> (P \<or> R)" by iprover
1.557 +lemma disj_conj_distribR: "(P \<and> Q) \<or> R \<longleftrightarrow> (P \<or> R) \<and> (Q \<or> R)" by iprover
1.559  lemma imp_conjR: "(P \<longrightarrow> (Q \<and> R)) = ((P \<longrightarrow> Q) \<and> (P \<longrightarrow> R))" by iprover
1.560  lemma imp_conjL: "((P \<and> Q) \<longrightarrow> R) = (P \<longrightarrow> (Q \<longrightarrow> R))" by iprover
1.561  lemma imp_disjL: "((P \<or> Q) \<longrightarrow> R) = ((P \<longrightarrow> R) \<and> (Q \<longrightarrow> R))" by iprover
1.563  text \<open>These two are specialized, but \<open>imp_disj_not1\<close> is useful in \<open>Auth/Yahalom\<close>.\<close>
1.564 -lemma imp_disj_not1: "(P \<longrightarrow> Q \<or> R) = (\<not> Q \<longrightarrow> P \<longrightarrow> R)" by blast
1.565 -lemma imp_disj_not2: "(P \<longrightarrow> Q \<or> R) = (\<not> R \<longrightarrow> P \<longrightarrow> Q)" by blast
1.566 +lemma imp_disj_not1: "(P \<longrightarrow> Q \<or> R) \<longleftrightarrow> (\<not> Q \<longrightarrow> P \<longrightarrow> R)" by blast
1.567 +lemma imp_disj_not2: "(P \<longrightarrow> Q \<or> R) \<longleftrightarrow> (\<not> R \<longrightarrow> P \<longrightarrow> Q)" by blast
1.569 -lemma imp_disj1: "((P \<longrightarrow> Q) \<or> R) = (P \<longrightarrow> Q \<or> R)" by blast
1.570 -lemma imp_disj2: "(Q \<or> (P \<longrightarrow> R)) = (P \<longrightarrow> Q \<or> R)" by blast
1.571 +lemma imp_disj1: "((P \<longrightarrow> Q) \<or> R) \<longleftrightarrow> (P \<longrightarrow> Q \<or> R)" by blast
1.572 +lemma imp_disj2: "(Q \<or> (P \<longrightarrow> R)) \<longleftrightarrow> (P \<longrightarrow> Q \<or> R)" by blast
1.574 -lemma imp_cong: "(P = P') \<Longrightarrow> (P' \<Longrightarrow> (Q = Q')) \<Longrightarrow> ((P \<longrightarrow> Q) = (P' \<longrightarrow> Q'))"
1.575 +lemma imp_cong: "(P = P') \<Longrightarrow> (P' \<Longrightarrow> (Q = Q')) \<Longrightarrow> ((P \<longrightarrow> Q) \<longleftrightarrow> (P' \<longrightarrow> Q'))"
1.576    by iprover
1.578 -lemma de_Morgan_disj: "(\<not> (P \<or> Q)) = (\<not> P \<and> \<not> Q)" by iprover
1.579 -lemma de_Morgan_conj: "(\<not> (P \<and> Q)) = (\<not> P \<or> \<not> Q)" by blast
1.580 -lemma not_imp: "(\<not> (P \<longrightarrow> Q)) = (P \<and> \<not> Q)" by blast
1.581 -lemma not_iff: "(P \<noteq> Q) = (P = (\<not> Q))" by blast
1.582 -lemma disj_not1: "(\<not> P \<or> Q) = (P \<longrightarrow> Q)" by blast
1.583 -lemma disj_not2: "(P \<or> \<not> Q) = (Q \<longrightarrow> P)"  \<comment> \<open>changes orientation :-(\<close>
1.584 -  by blast
1.585 -lemma imp_conv_disj: "(P \<longrightarrow> Q) = ((\<not> P) \<or> Q)" by blast
1.586 +lemma de_Morgan_disj: "\<not> (P \<or> Q) \<longleftrightarrow> \<not> P \<and> \<not> Q" by iprover
1.587 +lemma de_Morgan_conj: "\<not> (P \<and> Q) \<longleftrightarrow> \<not> P \<or> \<not> Q" by blast
1.588 +lemma not_imp: "\<not> (P \<longrightarrow> Q) \<longleftrightarrow> P \<and> \<not> Q" by blast
1.589 +lemma not_iff: "P \<noteq> Q \<longleftrightarrow> (P \<longleftrightarrow> \<not> Q)" by blast
1.590 +lemma disj_not1: "\<not> P \<or> Q \<longleftrightarrow> (P \<longrightarrow> Q)" by blast
1.591 +lemma disj_not2: "P \<or> \<not> Q \<longleftrightarrow> (Q \<longrightarrow> P)" by blast  \<comment> \<open>changes orientation :-(\<close>
1.592 +lemma imp_conv_disj: "(P \<longrightarrow> Q) \<longleftrightarrow> (\<not> P) \<or> Q" by blast
1.593  lemma disj_imp: "P \<or> Q \<longleftrightarrow> \<not> P \<longrightarrow> Q" by blast
1.595 -lemma iff_conv_conj_imp: "(P = Q) = ((P \<longrightarrow> Q) \<and> (Q \<longrightarrow> P))" by iprover
1.596 +lemma iff_conv_conj_imp: "(P \<longleftrightarrow> Q) \<longleftrightarrow> (P \<longrightarrow> Q) \<and> (Q \<longrightarrow> P)" by iprover
1.599 -lemma cases_simp: "((P \<longrightarrow> Q) \<and> (\<not> P \<longrightarrow> Q)) = Q"
1.600 +lemma cases_simp: "(P \<longrightarrow> Q) \<and> (\<not> P \<longrightarrow> Q) \<longleftrightarrow> Q"
1.601    \<comment> \<open>Avoids duplication of subgoals after \<open>if_split\<close>, when the true and false\<close>
1.602    \<comment> \<open>cases boil down to the same thing.\<close>
1.603    by blast
1.605 -lemma not_all: "(\<not> (\<forall>x. P x)) = (\<exists>x. \<not> P x)" by blast
1.606 -lemma imp_all: "((\<forall>x. P x) \<longrightarrow> Q) = (\<exists>x. P x \<longrightarrow> Q)" by blast
1.607 -lemma not_ex: "(\<not> (\<exists>x. P x)) = (\<forall>x. \<not> P x)" by iprover
1.608 -lemma imp_ex: "((\<exists>x. P x) \<longrightarrow> Q) = (\<forall>x. P x \<longrightarrow> Q)" by iprover
1.609 -lemma all_not_ex: "(\<forall>x. P x) = (\<not> (\<exists>x. \<not> P x ))" by blast
1.610 +lemma not_all: "\<not> (\<forall>x. P x) \<longleftrightarrow> (\<exists>x. \<not> P x)" by blast
1.611 +lemma imp_all: "((\<forall>x. P x) \<longrightarrow> Q) \<longleftrightarrow> (\<exists>x. P x \<longrightarrow> Q)" by blast
1.612 +lemma not_ex: "\<not> (\<exists>x. P x) \<longleftrightarrow> (\<forall>x. \<not> P x)" by iprover
1.613 +lemma imp_ex: "((\<exists>x. P x) \<longrightarrow> Q) \<longleftrightarrow> (\<forall>x. P x \<longrightarrow> Q)" by iprover
1.614 +lemma all_not_ex: "(\<forall>x. P x) \<longleftrightarrow> \<not> (\<exists>x. \<not> P x)" by blast
1.616  declare All_def [no_atp]
1.618 -lemma ex_disj_distrib: "(\<exists>x. P x \<or> Q x) = ((\<exists>x. P x) \<or> (\<exists>x. Q x))" by iprover
1.619 -lemma all_conj_distrib: "(\<forall>x. P x \<and> Q x) = ((\<forall>x. P x) \<and> (\<forall>x. Q x))" by iprover
1.620 +lemma ex_disj_distrib: "(\<exists>x. P x \<or> Q x) \<longleftrightarrow> (\<exists>x. P x) \<or> (\<exists>x. Q x)" by iprover
1.621 +lemma all_conj_distrib: "(\<forall>x. P x \<and> Q x) \<longleftrightarrow> (\<forall>x. P x) \<and> (\<forall>x. Q x)" by iprover
1.623  text \<open>
1.624 -  \medskip The \<open>\<and>\<close> congruence rule: not included by default!
1.625 +  \<^medskip> The \<open>\<and>\<close> congruence rule: not included by default!
1.626    May slow rewrite proofs down by as much as 50\%\<close>
1.628 -lemma conj_cong:
1.629 -    "(P = P') \<Longrightarrow> (P' \<Longrightarrow> (Q = Q')) \<Longrightarrow> ((P \<and> Q) = (P' \<and> Q'))"
1.630 +lemma conj_cong: "P = P' \<Longrightarrow> (P' \<Longrightarrow> Q = Q') \<Longrightarrow> (P \<and> Q) = (P' \<and> Q')"
1.631    by iprover
1.633 -lemma rev_conj_cong:
1.634 -    "(Q = Q') \<Longrightarrow> (Q' \<Longrightarrow> (P = P')) \<Longrightarrow> ((P \<and> Q) = (P' \<and> Q'))"
1.635 +lemma rev_conj_cong: "Q = Q' \<Longrightarrow> (Q' \<Longrightarrow> P = P') \<Longrightarrow> (P \<and> Q) = (P' \<and> Q')"
1.636    by iprover
1.638  text \<open>The \<open>|\<close> congruence rule: not included by default!\<close>
1.640 -lemma disj_cong:
1.641 -    "(P = P') \<Longrightarrow> (\<not> P' \<Longrightarrow> (Q = Q')) \<Longrightarrow> ((P \<or> Q) = (P' \<or> Q'))"
1.642 +lemma disj_cong: "P = P' \<Longrightarrow> (\<not> P' \<Longrightarrow> Q = Q') \<Longrightarrow> (P \<or> Q) = (P' \<or> Q')"
1.643    by blast
1.646 -text \<open>\medskip if-then-else rules\<close>
1.647 +text \<open>\<^medskip> if-then-else rules\<close>
1.649  lemma if_True [code]: "(if True then x else y) = x"
1.650 -  by (unfold If_def) blast
1.651 +  unfolding If_def by blast
1.653  lemma if_False [code]: "(if False then x else y) = y"
1.654 -  by (unfold If_def) blast
1.655 +  unfolding If_def by blast
1.657  lemma if_P: "P \<Longrightarrow> (if P then x else y) = x"
1.658 -  by (unfold If_def) blast
1.659 +  unfolding If_def by blast
1.661  lemma if_not_P: "\<not> P \<Longrightarrow> (if P then x else y) = y"
1.662 -  by (unfold If_def) blast
1.663 +  unfolding If_def by blast
1.665  lemma if_split: "P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))"
1.666    apply (rule case_split [of Q])
1.667     apply (simplesubst if_P)
1.668 -    prefer 3 apply (simplesubst if_not_P, blast+)
1.669 +    prefer 3
1.670 +    apply (simplesubst if_not_P)
1.671 +     apply blast+
1.672    done
1.674  lemma if_split_asm: "P (if Q then x else y) = (\<not> ((Q \<and> \<not> P x) \<or> (\<not> Q \<and> \<not> P y)))"
1.675 -by (simplesubst if_split, blast)
1.676 +  by (simplesubst if_split) blast
1.678  lemmas if_splits [no_atp] = if_split if_split_asm
1.680  lemma if_cancel: "(if c then x else x) = x"
1.681 -by (simplesubst if_split, blast)
1.682 +  by (simplesubst if_split) blast
1.684  lemma if_eq_cancel: "(if x = y then y else x) = x"
1.685 -by (simplesubst if_split, blast)
1.686 +  by (simplesubst if_split) blast
1.688  lemma if_bool_eq_conj: "(if P then Q else R) = ((P \<longrightarrow> Q) \<and> (\<not> P \<longrightarrow> R))"
1.689    \<comment> \<open>This form is useful for expanding \<open>if\<close>s on the RIGHT of the \<open>\<Longrightarrow>\<close> symbol.\<close>
1.690 @@ -1068,10 +1056,10 @@
1.691    \<comment> \<open>And this form is useful for expanding \<open>if\<close>s on the LEFT.\<close>
1.692    by (simplesubst if_split) blast
1.694 -lemma Eq_TrueI: "P \<Longrightarrow> P \<equiv> True" by (unfold atomize_eq) iprover
1.695 -lemma Eq_FalseI: "\<not> P \<Longrightarrow> P \<equiv> False" by (unfold atomize_eq) iprover
1.696 +lemma Eq_TrueI: "P \<Longrightarrow> P \<equiv> True" unfolding atomize_eq by iprover
1.697 +lemma Eq_FalseI: "\<not> P \<Longrightarrow> P \<equiv> False" unfolding atomize_eq by iprover
1.699 -text \<open>\medskip let rules for simproc\<close>
1.700 +text \<open>\<^medskip> let rules for simproc\<close>
1.702  lemma Let_folded: "f x \<equiv> g x \<Longrightarrow> Let x f \<equiv> Let x g"
1.703    by (unfold Let_def)
1.704 @@ -1085,8 +1073,8 @@
1.705    its premise.
1.706  \<close>
1.708 -definition simp_implies :: "[prop, prop] \<Rightarrow> prop"  (infixr "=simp=>" 1) where
1.709 -  "simp_implies \<equiv> op \<Longrightarrow>"
1.710 +definition simp_implies :: "prop \<Rightarrow> prop \<Rightarrow> prop"  (infixr "=simp=>" 1)
1.711 +  where "simp_implies \<equiv> op \<Longrightarrow>"
1.713  lemma simp_impliesI:
1.714    assumes PQ: "(PROP P \<Longrightarrow> PROP Q)"
1.715 @@ -1098,8 +1086,8 @@
1.717  lemma simp_impliesE:
1.718    assumes PQ: "PROP P =simp=> PROP Q"
1.719 -  and P: "PROP P"
1.720 -  and QR: "PROP Q \<Longrightarrow> PROP R"
1.721 +    and P: "PROP P"
1.722 +    and QR: "PROP Q \<Longrightarrow> PROP R"
1.723    shows "PROP R"
1.724    apply (rule QR)
1.725    apply (rule PQ [unfolded simp_implies_def])
1.726 @@ -1108,18 +1096,19 @@
1.728  lemma simp_implies_cong:
1.729    assumes PP' :"PROP P \<equiv> PROP P'"
1.730 -  and P'QQ': "PROP P' \<Longrightarrow> (PROP Q \<equiv> PROP Q')"
1.731 +    and P'QQ': "PROP P' \<Longrightarrow> (PROP Q \<equiv> PROP Q')"
1.732    shows "(PROP P =simp=> PROP Q) \<equiv> (PROP P' =simp=> PROP Q')"
1.733 -proof (unfold simp_implies_def, rule equal_intr_rule)
1.734 +  unfolding simp_implies_def
1.735 +proof (rule equal_intr_rule)
1.736    assume PQ: "PROP P \<Longrightarrow> PROP Q"
1.737 -  and P': "PROP P'"
1.738 +    and P': "PROP P'"
1.739    from PP' [symmetric] and P' have "PROP P"
1.740      by (rule equal_elim_rule1)
1.741    then have "PROP Q" by (rule PQ)
1.742    with P'QQ' [OF P'] show "PROP Q'" by (rule equal_elim_rule1)
1.743  next
1.744    assume P'Q': "PROP P' \<Longrightarrow> PROP Q'"
1.745 -  and P: "PROP P"
1.746 +    and P: "PROP P"
1.747    from PP' and P have P': "PROP P'" by (rule equal_elim_rule1)
1.748    then have "PROP Q'" by (rule P'Q')
1.749    with P'QQ' [OF P', symmetric] show "PROP Q"
1.750 @@ -1141,12 +1130,10 @@
1.751    shows "(\<exists>x. P x) = (\<exists>x. Q x)"
1.752    using assms by blast
1.754 -lemma all_comm:
1.755 -  "(\<forall>x y. P x y) = (\<forall>y x. P x y)"
1.756 +lemma all_comm: "(\<forall>x y. P x y) = (\<forall>y x. P x y)"
1.757    by blast
1.759 -lemma ex_comm:
1.760 -  "(\<exists>x y. P x y) = (\<exists>y x. P x y)"
1.761 +lemma ex_comm: "(\<exists>x y. P x y) = (\<exists>y x. P x y)"
1.762    by blast
1.764  ML_file "Tools/simpdata.ML"
1.765 @@ -1163,79 +1150,80 @@
1.766  text \<open>Simproc for proving \<open>(y = x) \<equiv> False\<close> from premise \<open>\<not> (x = y)\<close>:\<close>
1.768  simproc_setup neq ("x = y") = \<open>fn _ =>
1.769 -let
1.770 -  val neq_to_EQ_False = @{thm not_sym} RS @{thm Eq_FalseI};
1.771 -  fun is_neq eq lhs rhs thm =
1.772 -    (case Thm.prop_of thm of
1.773 -      _ \$ (Not \$ (eq' \$ l' \$ r')) =>
1.774 -        Not = HOLogic.Not andalso eq' = eq andalso
1.775 -        r' aconv lhs andalso l' aconv rhs
1.776 -    | _ => false);
1.777 -  fun proc ss ct =
1.778 -    (case Thm.term_of ct of
1.779 -      eq \$ lhs \$ rhs =>
1.780 -        (case find_first (is_neq eq lhs rhs) (Simplifier.prems_of ss) of
1.781 -          SOME thm => SOME (thm RS neq_to_EQ_False)
1.782 -        | NONE => NONE)
1.783 -     | _ => NONE);
1.784 -in proc end;
1.785 +  let
1.786 +    val neq_to_EQ_False = @{thm not_sym} RS @{thm Eq_FalseI};
1.787 +    fun is_neq eq lhs rhs thm =
1.788 +      (case Thm.prop_of thm of
1.789 +        _ \$ (Not \$ (eq' \$ l' \$ r')) =>
1.790 +          Not = HOLogic.Not andalso eq' = eq andalso
1.791 +          r' aconv lhs andalso l' aconv rhs
1.792 +      | _ => false);
1.793 +    fun proc ss ct =
1.794 +      (case Thm.term_of ct of
1.795 +        eq \$ lhs \$ rhs =>
1.796 +          (case find_first (is_neq eq lhs rhs) (Simplifier.prems_of ss) of
1.797 +            SOME thm => SOME (thm RS neq_to_EQ_False)
1.798 +          | NONE => NONE)
1.799 +       | _ => NONE);
1.800 +  in proc end;
1.801  \<close>
1.803  simproc_setup let_simp ("Let x f") = \<open>
1.804 -let
1.805 -  fun count_loose (Bound i) k = if i >= k then 1 else 0
1.806 -    | count_loose (s \$ t) k = count_loose s k + count_loose t k
1.807 -    | count_loose (Abs (_, _, t)) k = count_loose  t (k + 1)
1.808 -    | count_loose _ _ = 0;
1.809 -  fun is_trivial_let (Const (@{const_name Let}, _) \$ x \$ t) =
1.810 -    (case t of
1.811 -      Abs (_, _, t') => count_loose t' 0 <= 1
1.812 -    | _ => true);
1.813 -in
1.814 -  fn _ => fn ctxt => fn ct =>
1.815 -    if is_trivial_let (Thm.term_of ct)
1.816 -    then SOME @{thm Let_def} (*no or one ocurrence of bound variable*)
1.817 -    else
1.818 -      let (*Norbert Schirmer's case*)
1.819 -        val t = Thm.term_of ct;
1.820 -        val ([t'], ctxt') = Variable.import_terms false [t] ctxt;
1.821 -      in
1.822 -        Option.map (hd o Variable.export ctxt' ctxt o single)
1.823 -          (case t' of Const (@{const_name Let},_) \$ x \$ f => (* x and f are already in normal form *)
1.824 -            if is_Free x orelse is_Bound x orelse is_Const x
1.825 -            then SOME @{thm Let_def}
1.826 -            else
1.827 -              let
1.828 -                val n = case f of (Abs (x, _, _)) => x | _ => "x";
1.829 -                val cx = Thm.cterm_of ctxt x;
1.830 -                val xT = Thm.typ_of_cterm cx;
1.831 -                val cf = Thm.cterm_of ctxt f;
1.832 -                val fx_g = Simplifier.rewrite ctxt (Thm.apply cf cx);
1.833 -                val (_ \$ _ \$ g) = Thm.prop_of fx_g;
1.834 -                val g' = abstract_over (x, g);
1.835 -                val abs_g'= Abs (n, xT, g');
1.836 -              in
1.837 -                if g aconv g' then
1.838 -                  let
1.839 -                    val rl =
1.840 -                      infer_instantiate ctxt [(("f", 0), cf), (("x", 0), cx)] @{thm Let_unfold};
1.841 -                  in SOME (rl OF [fx_g]) end
1.842 -                else if (Envir.beta_eta_contract f) aconv (Envir.beta_eta_contract abs_g')
1.843 -                then NONE (*avoid identity conversion*)
1.844 -                else
1.845 -                  let
1.846 -                    val g'x = abs_g' \$ x;
1.847 -                    val g_g'x = Thm.symmetric (Thm.beta_conversion false (Thm.cterm_of ctxt g'x));
1.848 -                    val rl =
1.849 -                      @{thm Let_folded} |> infer_instantiate ctxt
1.850 -                        [(("f", 0), Thm.cterm_of ctxt f),
1.851 -                         (("x", 0), cx),
1.852 -                         (("g", 0), Thm.cterm_of ctxt abs_g')];
1.853 -                  in SOME (rl OF [Thm.transitive fx_g g_g'x]) end
1.854 -              end
1.855 -          | _ => NONE)
1.856 -      end
1.857 -end\<close>
1.858 +  let
1.859 +    fun count_loose (Bound i) k = if i >= k then 1 else 0
1.860 +      | count_loose (s \$ t) k = count_loose s k + count_loose t k
1.861 +      | count_loose (Abs (_, _, t)) k = count_loose  t (k + 1)
1.862 +      | count_loose _ _ = 0;
1.863 +    fun is_trivial_let (Const (@{const_name Let}, _) \$ x \$ t) =
1.864 +      (case t of
1.865 +        Abs (_, _, t') => count_loose t' 0 <= 1
1.866 +      | _ => true);
1.867 +  in
1.868 +    fn _ => fn ctxt => fn ct =>
1.869 +      if is_trivial_let (Thm.term_of ct)
1.870 +      then SOME @{thm Let_def} (*no or one ocurrence of bound variable*)
1.871 +      else
1.872 +        let (*Norbert Schirmer's case*)
1.873 +          val t = Thm.term_of ct;
1.874 +          val ([t'], ctxt') = Variable.import_terms false [t] ctxt;
1.875 +        in
1.876 +          Option.map (hd o Variable.export ctxt' ctxt o single)
1.877 +            (case t' of Const (@{const_name Let},_) \$ x \$ f => (* x and f are already in normal form *)
1.878 +              if is_Free x orelse is_Bound x orelse is_Const x
1.879 +              then SOME @{thm Let_def}
1.880 +              else
1.881 +                let
1.882 +                  val n = case f of (Abs (x, _, _)) => x | _ => "x";
1.883 +                  val cx = Thm.cterm_of ctxt x;
1.884 +                  val xT = Thm.typ_of_cterm cx;
1.885 +                  val cf = Thm.cterm_of ctxt f;
1.886 +                  val fx_g = Simplifier.rewrite ctxt (Thm.apply cf cx);
1.887 +                  val (_ \$ _ \$ g) = Thm.prop_of fx_g;
1.888 +                  val g' = abstract_over (x, g);
1.889 +                  val abs_g'= Abs (n, xT, g');
1.890 +                in
1.891 +                  if g aconv g' then
1.892 +                    let
1.893 +                      val rl =
1.894 +                        infer_instantiate ctxt [(("f", 0), cf), (("x", 0), cx)] @{thm Let_unfold};
1.895 +                    in SOME (rl OF [fx_g]) end
1.896 +                  else if (Envir.beta_eta_contract f) aconv (Envir.beta_eta_contract abs_g')
1.897 +                  then NONE (*avoid identity conversion*)
1.898 +                  else
1.899 +                    let
1.900 +                      val g'x = abs_g' \$ x;
1.901 +                      val g_g'x = Thm.symmetric (Thm.beta_conversion false (Thm.cterm_of ctxt g'x));
1.902 +                      val rl =
1.903 +                        @{thm Let_folded} |> infer_instantiate ctxt
1.904 +                          [(("f", 0), Thm.cterm_of ctxt f),
1.905 +                           (("x", 0), cx),
1.906 +                           (("g", 0), Thm.cterm_of ctxt abs_g')];
1.907 +                    in SOME (rl OF [Thm.transitive fx_g g_g'x]) end
1.908 +                end
1.909 +            | _ => NONE)
1.910 +        end
1.911 +  end
1.912 +\<close>
1.914  lemma True_implies_equals: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
1.915  proof
1.916 @@ -1254,9 +1242,10 @@
1.918  (* This is not made a simp rule because it does not improve any proofs
1.919     but slows some AFP entries down by 5% (cpu time). May 2015 *)
1.920 -lemma implies_False_swap: "NO_MATCH (Trueprop False) P \<Longrightarrow>
1.921 -  (False \<Longrightarrow> PROP P \<Longrightarrow> PROP Q) \<equiv> (PROP P \<Longrightarrow> False \<Longrightarrow> PROP Q)"
1.922 -by(rule swap_prems_eq)
1.923 +lemma implies_False_swap:
1.924 +  "NO_MATCH (Trueprop False) P \<Longrightarrow>
1.925 +    (False \<Longrightarrow> PROP P \<Longrightarrow> PROP Q) \<equiv> (PROP P \<Longrightarrow> False \<Longrightarrow> PROP Q)"
1.926 +  by (rule swap_prems_eq)
1.928  lemma ex_simps:
1.929    "\<And>P Q. (\<exists>x. P x \<and> Q)   = ((\<exists>x. P x) \<and> Q)"
1.930 @@ -1279,19 +1268,19 @@
1.931    by (iprover | blast)+
1.933  lemmas [simp] =
1.934 -  triv_forall_equality (*prunes params*)
1.935 -  True_implies_equals implies_True_equals (*prune True in asms*)
1.936 -  False_implies_equals (*prune False in asms*)
1.937 +  triv_forall_equality  \<comment> \<open>prunes params\<close>
1.938 +  True_implies_equals implies_True_equals  \<comment> \<open>prune \<open>True\<close> in asms\<close>
1.939 +  False_implies_equals  \<comment> \<open>prune \<open>False\<close> in asms\<close>
1.940    if_True
1.941    if_False
1.942    if_cancel
1.943    if_eq_cancel
1.944 -  imp_disjL
1.945 -  (*In general it seems wrong to add distributive laws by default: they
1.946 -    might cause exponential blow-up.  But imp_disjL has been in for a while
1.947 +  imp_disjL \<comment>
1.948 +   \<open>In general it seems wrong to add distributive laws by default: they
1.949 +    might cause exponential blow-up.  But \<open>imp_disjL\<close> has been in for a while
1.950      and cannot be removed without affecting existing proofs.  Moreover,
1.951 -    rewriting by "(P \<or> Q \<longrightarrow> R) = ((P \<longrightarrow> R) \<and> (Q \<longrightarrow> R))" might be justified on the
1.952 -    grounds that it allows simplification of R in the two cases.*)
1.953 +    rewriting by \<open>(P \<or> Q \<longrightarrow> R) = ((P \<longrightarrow> R) \<and> (Q \<longrightarrow> R))\<close> might be justified on the
1.954 +    grounds that it allows simplification of \<open>R\<close> in the two cases.\<close>
1.955    conj_assoc
1.956    disj_assoc
1.957    de_Morgan_conj
1.958 @@ -1314,15 +1303,15 @@
1.960  ML \<open>val HOL_ss = simpset_of @{context}\<close>
1.962 -text \<open>Simplifies @{term x} assuming @{prop c} and @{term y} assuming @{prop "\<not> c"}\<close>
1.963 +text \<open>Simplifies \<open>x\<close> assuming \<open>c\<close> and \<open>y\<close> assuming \<open>\<not> c\<close>.\<close>
1.964  lemma if_cong:
1.965    assumes "b = c"
1.966 -      and "c \<Longrightarrow> x = u"
1.967 -      and "\<not> c \<Longrightarrow> y = v"
1.968 +    and "c \<Longrightarrow> x = u"
1.969 +    and "\<not> c \<Longrightarrow> y = v"
1.970    shows "(if b then x else y) = (if c then u else v)"
1.971    using assms by simp
1.973 -text \<open>Prevents simplification of x and y:
1.974 +text \<open>Prevents simplification of \<open>x\<close> and \<open>y\<close>:
1.975    faster and allows the execution of functional programs.\<close>
1.976  lemma if_weak_cong [cong]:
1.977    assumes "b = c"
1.978 @@ -1341,11 +1330,10 @@
1.979    shows "(t \<equiv> u) \<equiv> (t \<equiv> u')"
1.980    using assms by simp
1.982 -lemma if_distrib:
1.983 -  "f (if c then x else y) = (if c then f x else f y)"
1.984 +lemma if_distrib: "f (if c then x else y) = (if c then f x else f y)"
1.985    by simp
1.987 -text\<open>As a simplification rule, it replaces all function equalities by
1.988 +text \<open>As a simplification rule, it replaces all function equalities by
1.989    first-order equalities.\<close>
1.990  lemma fun_eq_iff: "f = g \<longleftrightarrow> (\<forall>x. f x = g x)"
1.991    by auto
1.992 @@ -1578,27 +1566,32 @@
1.994  lemma choice_eq: "(\<forall>x. \<exists>!y. P x y) = (\<exists>!f. \<forall>x. P x (f x))"
1.995    apply (rule iffI)
1.996 -  apply (rule_tac a = "\<lambda>x. THE y. P x y" in ex1I)
1.997 -  apply (fast dest!: theI')
1.998 -  apply (fast intro: the1_equality [symmetric])
1.999 +   apply (rule_tac a = "\<lambda>x. THE y. P x y" in ex1I)
1.1000 +    apply (fast dest!: theI')
1.1001 +   apply (fast intro: the1_equality [symmetric])
1.1002    apply (erule ex1E)
1.1003    apply (rule allI)
1.1004    apply (rule ex1I)
1.1005 -  apply (erule spec)
1.1006 +   apply (erule spec)
1.1007    apply (erule_tac x = "\<lambda>z. if z = x then y else f z" in allE)
1.1008    apply (erule impE)
1.1009 -  apply (rule allI)
1.1010 -  apply (case_tac "xa = x")
1.1011 -  apply (drule_tac  x = x in fun_cong, simp_all)
1.1012 +   apply (rule allI)
1.1013 +   apply (case_tac "xa = x")
1.1014 +    apply (drule_tac  x = x in fun_cong)
1.1015 +    apply simp_all
1.1016    done
1.1018  lemmas eq_sym_conv = eq_commute
1.1020  lemma nnf_simps:
1.1021 -  "(\<not>(P \<and> Q)) = (\<not> P \<or> \<not> Q)" "(\<not> (P \<or> Q)) = (\<not> P \<and> \<not>Q)" "(P \<longrightarrow> Q) = (\<not>P \<or> Q)"
1.1022 -  "(P = Q) = ((P \<and> Q) \<or> (\<not>P \<and> \<not> Q))" "(\<not>(P = Q)) = ((P \<and> \<not> Q) \<or> (\<not>P \<and> Q))"
1.1023 -  "(\<not> \<not>(P)) = P"
1.1024 -by blast+
1.1025 +  "(\<not> (P \<and> Q)) = (\<not> P \<or> \<not> Q)"
1.1026 +  "(\<not> (P \<or> Q)) = (\<not> P \<and> \<not> Q)"
1.1027 +  "(P \<longrightarrow> Q) = (\<not> P \<or> Q)"
1.1028 +  "(P = Q) = ((P \<and> Q) \<or> (\<not> P \<and> \<not> Q))"
1.1029 +  "(\<not> (P = Q)) = ((P \<and> \<not> Q) \<or> (\<not> P \<and> Q))"
1.1030 +  "(\<not> \<not> P) = P"
1.1031 +  by blast+
1.1034  subsection \<open>Basic ML bindings\<close>
1.1036 @@ -1659,12 +1652,15 @@
1.1037  section \<open>\<open>NO_MATCH\<close> simproc\<close>
1.1039  text \<open>
1.1040 - The simplification procedure can be used to avoid simplification of terms of a certain form
1.1041 +  The simplification procedure can be used to avoid simplification of terms
1.1042 +  of a certain form.
1.1043  \<close>
1.1045 -definition NO_MATCH :: "'a \<Rightarrow> 'b \<Rightarrow> bool" where "NO_MATCH pat val \<equiv> True"
1.1046 +definition NO_MATCH :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
1.1047 +  where "NO_MATCH pat val \<equiv> True"
1.1049 -lemma NO_MATCH_cong[cong]: "NO_MATCH pat val = NO_MATCH pat val" by (rule refl)
1.1050 +lemma NO_MATCH_cong[cong]: "NO_MATCH pat val = NO_MATCH pat val"
1.1051 +  by (rule refl)
1.1053  declare [[coercion_args NO_MATCH - -]]
1.1055 @@ -1678,24 +1674,26 @@
1.1057  text \<open>
1.1058    This setup ensures that a rewrite rule of the form @{term "NO_MATCH pat val \<Longrightarrow> t"}
1.1059 -  is only applied, if the pattern @{term pat} does not match the value @{term val}.
1.1060 +  is only applied, if the pattern \<open>pat\<close> does not match the value \<open>val\<close>.
1.1061  \<close>
1.1064 -text\<open>Tagging a premise of a simp rule with ASSUMPTION forces the simplifier
1.1065 -not to simplify the argument and to solve it by an assumption.\<close>
1.1066 +text\<open>
1.1067 +  Tagging a premise of a simp rule with ASSUMPTION forces the simplifier
1.1068 +  not to simplify the argument and to solve it by an assumption.
1.1069 +\<close>
1.1071 -definition ASSUMPTION :: "bool \<Rightarrow> bool" where
1.1072 -"ASSUMPTION A \<equiv> A"
1.1073 +definition ASSUMPTION :: "bool \<Rightarrow> bool"
1.1074 +  where "ASSUMPTION A \<equiv> A"
1.1076  lemma ASSUMPTION_cong[cong]: "ASSUMPTION A = ASSUMPTION A"
1.1077 -by (rule refl)
1.1078 +  by (rule refl)
1.1080  lemma ASSUMPTION_I: "A \<Longrightarrow> ASSUMPTION A"
1.1081 -by(simp add: ASSUMPTION_def)
1.1082 +  by (simp add: ASSUMPTION_def)
1.1084  lemma ASSUMPTION_D: "ASSUMPTION A \<Longrightarrow> A"
1.1085 -by(simp add: ASSUMPTION_def)
1.1086 +  by (simp add: ASSUMPTION_def)
1.1088  setup \<open>
1.1089  let
1.1090 @@ -1712,12 +1710,10 @@
1.1092  subsubsection \<open>Generic code generator preprocessor setup\<close>
1.1094 -lemma conj_left_cong:
1.1095 -  "P \<longleftrightarrow> Q \<Longrightarrow> P \<and> R \<longleftrightarrow> Q \<and> R"
1.1096 +lemma conj_left_cong: "P \<longleftrightarrow> Q \<Longrightarrow> P \<and> R \<longleftrightarrow> Q \<and> R"
1.1097    by (fact arg_cong)
1.1099 -lemma disj_left_cong:
1.1100 -  "P \<longleftrightarrow> Q \<Longrightarrow> P \<or> R \<longleftrightarrow> Q \<or> R"
1.1101 +lemma disj_left_cong: "P \<longleftrightarrow> Q \<Longrightarrow> P \<or> R \<longleftrightarrow> Q \<or> R"
1.1102    by (fact arg_cong)
1.1104  setup \<open>
1.1105 @@ -1772,29 +1768,32 @@
1.1106    shows "False \<and> P \<longleftrightarrow> False"
1.1107      and "True \<and> P \<longleftrightarrow> P"
1.1108      and "P \<and> False \<longleftrightarrow> False"
1.1109 -    and "P \<and> True \<longleftrightarrow> P" by simp_all
1.1110 +    and "P \<and> True \<longleftrightarrow> P"
1.1111 +  by simp_all
1.1113  lemma [code]:
1.1114    shows "False \<or> P \<longleftrightarrow> P"
1.1115      and "True \<or> P \<longleftrightarrow> True"
1.1116      and "P \<or> False \<longleftrightarrow> P"
1.1117 -    and "P \<or> True \<longleftrightarrow> True" by simp_all
1.1118 +    and "P \<or> True \<longleftrightarrow> True"
1.1119 +  by simp_all
1.1121  lemma [code]:
1.1122    shows "(False \<longrightarrow> P) \<longleftrightarrow> True"
1.1123      and "(True \<longrightarrow> P) \<longleftrightarrow> P"
1.1124      and "(P \<longrightarrow> False) \<longleftrightarrow> \<not> P"
1.1125 -    and "(P \<longrightarrow> True) \<longleftrightarrow> True" by simp_all
1.1126 +    and "(P \<longrightarrow> True) \<longleftrightarrow> True"
1.1127 +  by simp_all
1.1129  text \<open>More about @{typ prop}\<close>
1.1131  lemma [code nbe]:
1.1132    shows "(True \<Longrightarrow> PROP Q) \<equiv> PROP Q"
1.1133      and "(PROP Q \<Longrightarrow> True) \<equiv> Trueprop True"
1.1134 -    and "(P \<Longrightarrow> R) \<equiv> Trueprop (P \<longrightarrow> R)" by (auto intro!: equal_intr_rule)
1.1135 +    and "(P \<Longrightarrow> R) \<equiv> Trueprop (P \<longrightarrow> R)"
1.1136 +  by (auto intro!: equal_intr_rule)
1.1138 -lemma Trueprop_code [code]:
1.1139 -  "Trueprop True \<equiv> Code_Generator.holds"
1.1140 +lemma Trueprop_code [code]: "Trueprop True \<equiv> Code_Generator.holds"
1.1141    by (auto intro!: equal_intr_rule holds)
1.1143  declare Trueprop_code [symmetric, code_post]
1.1144 @@ -1806,21 +1805,21 @@
1.1145  instantiation itself :: (type) equal
1.1146  begin
1.1148 -definition equal_itself :: "'a itself \<Rightarrow> 'a itself \<Rightarrow> bool" where
1.1149 -  "equal_itself x y \<longleftrightarrow> x = y"
1.1150 +definition equal_itself :: "'a itself \<Rightarrow> 'a itself \<Rightarrow> bool"
1.1151 +  where "equal_itself x y \<longleftrightarrow> x = y"
1.1153 -instance proof
1.1154 -qed (fact equal_itself_def)
1.1155 +instance
1.1156 +  by standard (fact equal_itself_def)
1.1158  end
1.1160 -lemma equal_itself_code [code]:
1.1161 -  "equal TYPE('a) TYPE('a) \<longleftrightarrow> True"
1.1162 +lemma equal_itself_code [code]: "equal TYPE('a) TYPE('a) \<longleftrightarrow> True"
1.1163    by (simp add: equal)
1.1165  setup \<open>Sign.add_const_constraint (@{const_name equal}, SOME @{typ "'a::type \<Rightarrow> 'a \<Rightarrow> bool"})\<close>
1.1167 -lemma equal_alias_cert: "OFCLASS('a, equal_class) \<equiv> ((op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool) \<equiv> equal)" (is "?ofclass \<equiv> ?equal")
1.1168 +lemma equal_alias_cert: "OFCLASS('a, equal_class) \<equiv> ((op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool) \<equiv> equal)"
1.1169 +  (is "?ofclass \<equiv> ?equal")
1.1170  proof
1.1171    assume "PROP ?ofclass"
1.1172    show "PROP ?equal"
1.1173 @@ -1900,15 +1899,13 @@
1.1174    code_module Pure \<rightharpoonup>
1.1175      (SML) HOL and (OCaml) HOL and (Haskell) HOL and (Scala) HOL
1.1177 -text \<open>using built-in Haskell equality\<close>
1.1179 +text \<open>Using built-in Haskell equality.\<close>
1.1180  code_printing
1.1181    type_class equal \<rightharpoonup> (Haskell) "Eq"
1.1182  | constant HOL.equal \<rightharpoonup> (Haskell) infix 4 "=="
1.1183  | constant HOL.eq \<rightharpoonup> (Haskell) infix 4 "=="
1.1185 -text \<open>undefined\<close>
1.1187 +text \<open>\<open>undefined\<close>\<close>
1.1188  code_printing
1.1189    constant undefined \<rightharpoonup>
1.1190      (SML) "!(raise/ Fail/ \"undefined\")"
1.1191 @@ -1956,7 +1953,7 @@
1.1192    and nitpick_choice_spec "choice specification of constants as needed by Nitpick"
1.1194  declare if_bool_eq_conj [nitpick_unfold, no_atp]
1.1195 -        if_bool_eq_disj [no_atp]
1.1196 +  and if_bool_eq_disj [no_atp]
1.1199  subsection \<open>Preprocessing for the predicate compiler\<close>