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.5  
     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.12  
    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.28  
    1.29  text \<open>For calculational reasoning:\<close>
    1.30  
    1.31 @@ -246,25 +246,25 @@
    1.32  
    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.41  
    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.50  
    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.58  
    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.66  
    1.67  ML \<open>fun cong_tac ctxt = Cong_Tac.cong_tac ctxt @{thm cong}\<close>
    1.68  
    1.69 @@ -295,7 +295,7 @@
    1.70  
    1.71  subsubsection \<open>True\<close>
    1.72  
    1.73 -lemma TrueI: "True"
    1.74 +lemma TrueI: True
    1.75    unfolding True_def by (rule refl)
    1.76  
    1.77  lemma eqTrueI: "P \<Longrightarrow> P = True"
    1.78 @@ -307,14 +307,16 @@
    1.79  
    1.80  subsubsection \<open>Universal quantifier\<close>
    1.81  
    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.87  
    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.97  
    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.106  
   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.112  
   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.120  
   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.130  
   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.135  
   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.141  
   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.151  
   1.152  
   1.153  subsubsection \<open>Conjunction\<close>
   1.154  
   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.160  
   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.166  
   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.172  
   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.186  
   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.193  
   1.194  
   1.195  subsubsection \<open>Disjunction\<close>
   1.196  
   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.202  
   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.208  
   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.220  
   1.221  
   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.239  
   1.240  lemmas ccontr = FalseE [THEN classical]
   1.241  
   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.257  
   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.269  
   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.277  
   1.278  
   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.286  
   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.296  
   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.310  
   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.320  
   1.321  
   1.322  subsubsection \<open>Classical intro rules for disjunction and existential quantifiers\<close>
   1.323  
   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.332  
   1.333  lemma excluded_middle: "\<not> P \<or> P"
   1.334 -by (iprover intro: disjCI)
   1.335 +  by (iprover intro: disjCI)
   1.336  
   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.355  
   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.369  
   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.389  
   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.401  
   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.409  
   1.410  
   1.411  subsubsection \<open>Intuitionistic Reasoning\<close>
   1.412 @@ -650,7 +636,7 @@
   1.413  subsubsection \<open>Atomizing meta-level connectives\<close>
   1.414  
   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.418  
   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.423  
   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.432  
   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.437  
   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.459  
   1.460  ML \<open>
   1.461    structure Blast = Blast
   1.462 @@ -862,27 +848,29 @@
   1.463  
   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.470  
   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.478  
   1.479  lemma theI': "\<exists>!x. P x \<Longrightarrow> P (THE x. P x)"
   1.480    by (blast intro: theI)
   1.481  
   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.489  
   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.497  
   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.503  
   1.504 -lemma disj_absorb: "(A \<or> A) = A"
   1.505 +lemma disj_absorb: "A \<or> A \<longleftrightarrow> A"
   1.506    by blast
   1.507  
   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.511  
   1.512 -lemma conj_absorb: "(A \<and> A) = A"
   1.513 +lemma conj_absorb: "A \<and> A \<longleftrightarrow> A"
   1.514    by blast
   1.515  
   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.519  
   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.526 +
   1.527  lemma neq_commute: "a \<noteq> b \<longleftrightarrow> b \<noteq> a" by iprover
   1.528  
   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.536  
   1.537  lemmas conj_ac = conj_commute conj_left_commute conj_assoc
   1.538  
   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.546  
   1.547  lemmas disj_ac = disj_commute disj_left_commute disj_assoc
   1.548  
   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.553  
   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.558  
   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.562  
   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.568  
   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.573  
   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.577  
   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.594  
   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.597  
   1.598  
   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.604  
   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.615  
   1.616  declare All_def [no_atp]
   1.617  
   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.622  
   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.627  
   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.632  
   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.637  
   1.638  text \<open>The \<open>|\<close> congruence rule: not included by default!\<close>
   1.639  
   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.644  
   1.645  
   1.646 -text \<open>\medskip if-then-else rules\<close>
   1.647 +text \<open>\<^medskip> if-then-else rules\<close>
   1.648  
   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.652  
   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.656  
   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.660  
   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.664  
   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.673  
   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.677  
   1.678  lemmas if_splits [no_atp] = if_split if_split_asm
   1.679  
   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.683  
   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.687  
   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.693  
   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.698  
   1.699 -text \<open>\medskip let rules for simproc\<close>
   1.700 +text \<open>\<^medskip> let rules for simproc\<close>
   1.701  
   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.707  
   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.712  
   1.713  lemma simp_impliesI:
   1.714    assumes PQ: "(PROP P \<Longrightarrow> PROP Q)"
   1.715 @@ -1098,8 +1086,8 @@
   1.716  
   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.727  
   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.753  
   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.758  
   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.763  
   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.767  
   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.802  
   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.913  
   1.914  lemma True_implies_equals: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
   1.915  proof
   1.916 @@ -1254,9 +1242,10 @@
   1.917  
   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.927  
   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.932  
   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.959  
   1.960  ML \<open>val HOL_ss = simpset_of @{context}\<close>
   1.961  
   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.972  
   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.981  
   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.986  
   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.993  
   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 [3] x = x in fun_cong, simp_all)
  1.1012 +   apply (rule allI)
  1.1013 +   apply (case_tac "xa = x")
  1.1014 +    apply (drule_tac [3] x = x in fun_cong)
  1.1015 +    apply simp_all
  1.1016    done
  1.1017  
  1.1018  lemmas eq_sym_conv = eq_commute
  1.1019  
  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.1032 +
  1.1033  
  1.1034  subsection \<open>Basic ML bindings\<close>
  1.1035  
  1.1036 @@ -1659,12 +1652,15 @@
  1.1037  section \<open>\<open>NO_MATCH\<close> simproc\<close>
  1.1038  
  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.1044  
  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.1048  
  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.1052  
  1.1053  declare [[coercion_args NO_MATCH - -]]
  1.1054  
  1.1055 @@ -1678,24 +1674,26 @@
  1.1056  
  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.1062  
  1.1063  
  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.1070  
  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.1075  
  1.1076  lemma ASSUMPTION_cong[cong]: "ASSUMPTION A = ASSUMPTION A"
  1.1077 -by (rule refl)
  1.1078 +  by (rule refl)
  1.1079  
  1.1080  lemma ASSUMPTION_I: "A \<Longrightarrow> ASSUMPTION A"
  1.1081 -by(simp add: ASSUMPTION_def)
  1.1082 +  by (simp add: ASSUMPTION_def)
  1.1083  
  1.1084  lemma ASSUMPTION_D: "ASSUMPTION A \<Longrightarrow> A"
  1.1085 -by(simp add: ASSUMPTION_def)
  1.1086 +  by (simp add: ASSUMPTION_def)
  1.1087  
  1.1088  setup \<open>
  1.1089  let
  1.1090 @@ -1712,12 +1710,10 @@
  1.1091  
  1.1092  subsubsection \<open>Generic code generator preprocessor setup\<close>
  1.1093  
  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.1098  
  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.1103  
  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.1112  
  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.1120  
  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.1128  
  1.1129  text \<open>More about @{typ prop}\<close>
  1.1130  
  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.1137  
  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.1142  
  1.1143  declare Trueprop_code [symmetric, code_post]
  1.1144 @@ -1806,21 +1805,21 @@
  1.1145  instantiation itself :: (type) equal
  1.1146  begin
  1.1147  
  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.1152  
  1.1153 -instance proof
  1.1154 -qed (fact equal_itself_def)
  1.1155 +instance
  1.1156 +  by standard (fact equal_itself_def)
  1.1157  
  1.1158  end
  1.1159  
  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.1164  
  1.1165  setup \<open>Sign.add_const_constraint (@{const_name equal}, SOME @{typ "'a::type \<Rightarrow> 'a \<Rightarrow> bool"})\<close>
  1.1166  
  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.1176  
  1.1177 -text \<open>using built-in Haskell equality\<close>
  1.1178 -
  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.1184  
  1.1185 -text \<open>undefined\<close>
  1.1186 -
  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.1193  
  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.1197  
  1.1198  
  1.1199  subsection \<open>Preprocessing for the predicate compiler\<close>