src/HOL/HOL.thy
changeset 60758 d8d85a8172b5
parent 60183 4cd4c204578c
child 60759 36d9f215c982
     1.1 --- a/src/HOL/HOL.thy	Sat Jul 18 21:44:18 2015 +0200
     1.2 +++ b/src/HOL/HOL.thy	Sat Jul 18 22:58:50 2015 +0200
     1.3 @@ -2,7 +2,7 @@
     1.4      Author:     Tobias Nipkow, Markus Wenzel, and Larry Paulson
     1.5  *)
     1.6  
     1.7 -section {* The basis of Higher-Order Logic *}
     1.8 +section \<open>The basis of Higher-Order Logic\<close>
     1.9  
    1.10  theory HOL
    1.11  imports Pure "~~/src/Tools/Code_Generator"
    1.12 @@ -53,13 +53,13 @@
    1.13  \<close>
    1.14  
    1.15  
    1.16 -subsection {* Primitive logic *}
    1.17 +subsection \<open>Primitive logic\<close>
    1.18  
    1.19 -subsubsection {* Core syntax *}
    1.20 +subsubsection \<open>Core syntax\<close>
    1.21  
    1.22 -setup {* Axclass.class_axiomatization (@{binding type}, []) *}
    1.23 +setup \<open>Axclass.class_axiomatization (@{binding type}, [])\<close>
    1.24  default_sort type
    1.25 -setup {* Object_Logic.add_base_sort @{sort type} *}
    1.26 +setup \<open>Object_Logic.add_base_sort @{sort type}\<close>
    1.27  
    1.28  axiomatization where fun_arity: "OFCLASS('a \<Rightarrow> 'b, type_class)"
    1.29  instance "fun" :: (type, type) type by (rule fun_arity)
    1.30 @@ -90,7 +90,7 @@
    1.31    Ex1           :: "('a => bool) => bool"           (binder "EX! " 10)
    1.32  
    1.33  
    1.34 -subsubsection {* Additional concrete syntax *}
    1.35 +subsubsection \<open>Additional concrete syntax\<close>
    1.36  
    1.37  notation (output)
    1.38    eq  (infix "=" 50)
    1.39 @@ -127,11 +127,11 @@
    1.40  
    1.41  syntax "_The" :: "[pttrn, bool] => 'a"  ("(3THE _./ _)" [0, 10] 10)
    1.42  translations "THE x. P" == "CONST The (%x. P)"
    1.43 -print_translation {*
    1.44 +print_translation \<open>
    1.45    [(@{const_syntax The}, fn _ => fn [Abs abs] =>
    1.46        let val (x, t) = Syntax_Trans.atomic_abs_tr' abs
    1.47        in Syntax.const @{syntax_const "_The"} $ x $ t end)]
    1.48 -*}  -- {* To avoid eta-contraction of body *}
    1.49 +\<close>  -- \<open>To avoid eta-contraction of body\<close>
    1.50  
    1.51  nonterminal letbinds and letbind
    1.52  syntax
    1.53 @@ -165,15 +165,15 @@
    1.54    Ex1  (binder "?! " 10)
    1.55  
    1.56  
    1.57 -subsubsection {* Axioms and basic definitions *}
    1.58 +subsubsection \<open>Axioms and basic definitions\<close>
    1.59  
    1.60  axiomatization where
    1.61    refl: "t = (t::'a)" and
    1.62    subst: "s = t \<Longrightarrow> P s \<Longrightarrow> P t" and
    1.63    ext: "(!!x::'a. (f x ::'b) = g x) ==> (%x. f x) = (%x. g x)"
    1.64 -    -- {*Extensionality is built into the meta-logic, and this rule expresses
    1.65 +    -- \<open>Extensionality is built into the meta-logic, and this rule expresses
    1.66           a related property.  It is an eta-expanded version of the traditional
    1.67 -         rule, and similar to the ABS rule of HOL*} and
    1.68 +         rule, and similar to the ABS rule of HOL\<close> and
    1.69  
    1.70    the_eq_trivial: "(THE x. x = a) = (a::'a)"
    1.71  
    1.72 @@ -209,9 +209,9 @@
    1.73  class default = fixes default :: 'a
    1.74  
    1.75  
    1.76 -subsection {* Fundamental rules *}
    1.77 +subsection \<open>Fundamental rules\<close>
    1.78  
    1.79 -subsubsection {* Equality *}
    1.80 +subsubsection \<open>Equality\<close>
    1.81  
    1.82  lemma sym: "s = t ==> t = s"
    1.83    by (erule subst) (rule refl)
    1.84 @@ -230,7 +230,7 @@
    1.85    shows "A = B"
    1.86    by (unfold meq) (rule refl)
    1.87  
    1.88 -text {* Useful with @{text erule} for proving equalities from known equalities. *}
    1.89 +text \<open>Useful with @{text erule} for proving equalities from known equalities.\<close>
    1.90       (* a = b
    1.91          |   |
    1.92          c = d   *)
    1.93 @@ -241,7 +241,7 @@
    1.94  apply assumption+
    1.95  done
    1.96  
    1.97 -text {* For calculational reasoning: *}
    1.98 +text \<open>For calculational reasoning:\<close>
    1.99  
   1.100  lemma forw_subst: "a = b ==> P b ==> P a"
   1.101    by (rule ssubst)
   1.102 @@ -250,15 +250,15 @@
   1.103    by (rule subst)
   1.104  
   1.105  
   1.106 -subsubsection {* Congruence rules for application *}
   1.107 +subsubsection \<open>Congruence rules for application\<close>
   1.108  
   1.109 -text {* Similar to @{text AP_THM} in Gordon's HOL. *}
   1.110 +text \<open>Similar to @{text AP_THM} in Gordon's HOL.\<close>
   1.111  lemma fun_cong: "(f::'a=>'b) = g ==> f(x)=g(x)"
   1.112  apply (erule subst)
   1.113  apply (rule refl)
   1.114  done
   1.115  
   1.116 -text {* Similar to @{text AP_TERM} in Gordon's HOL and FOL's @{text subst_context}. *}
   1.117 +text \<open>Similar to @{text AP_TERM} in Gordon's HOL and FOL's @{text subst_context}.\<close>
   1.118  lemma arg_cong: "x=y ==> f(x)=f(y)"
   1.119  apply (erule subst)
   1.120  apply (rule refl)
   1.121 @@ -274,10 +274,10 @@
   1.122  apply (rule refl)
   1.123  done
   1.124  
   1.125 -ML {* fun cong_tac ctxt = Cong_Tac.cong_tac ctxt @{thm cong} *}
   1.126 +ML \<open>fun cong_tac ctxt = Cong_Tac.cong_tac ctxt @{thm cong}\<close>
   1.127  
   1.128  
   1.129 -subsubsection {* Equality of booleans -- iff *}
   1.130 +subsubsection \<open>Equality of booleans -- iff\<close>
   1.131  
   1.132  lemma iffI: assumes "P ==> Q" and "Q ==> P" shows "P=Q"
   1.133    by (iprover intro: iff [THEN mp, THEN mp] impI assms)
   1.134 @@ -301,7 +301,7 @@
   1.135    by (iprover intro: minor impI major [THEN iffD2] major [THEN iffD1])
   1.136  
   1.137  
   1.138 -subsubsection {*True*}
   1.139 +subsubsection \<open>True\<close>
   1.140  
   1.141  lemma TrueI: "True"
   1.142    unfolding True_def by (rule refl)
   1.143 @@ -313,7 +313,7 @@
   1.144    by (erule iffD2) (rule TrueI)
   1.145  
   1.146  
   1.147 -subsubsection {*Universal quantifier*}
   1.148 +subsubsection \<open>Universal quantifier\<close>
   1.149  
   1.150  lemma allI: assumes "!!x::'a. P(x)" shows "ALL x. P(x)"
   1.151    unfolding All_def by (iprover intro: ext eqTrueI assms)
   1.152 @@ -337,12 +337,12 @@
   1.153    by (iprover intro: minor major major [THEN spec])
   1.154  
   1.155  
   1.156 -subsubsection {* False *}
   1.157 +subsubsection \<open>False\<close>
   1.158  
   1.159 -text {*
   1.160 +text \<open>
   1.161    Depends upon @{text spec}; it is impossible to do propositional
   1.162    logic before quantifiers!
   1.163 -*}
   1.164 +\<close>
   1.165  
   1.166  lemma FalseE: "False ==> P"
   1.167    apply (unfold False_def)
   1.168 @@ -353,7 +353,7 @@
   1.169    by (erule eqTrueE [THEN FalseE])
   1.170  
   1.171  
   1.172 -subsubsection {* Negation *}
   1.173 +subsubsection \<open>Negation\<close>
   1.174  
   1.175  lemma notI:
   1.176    assumes "P ==> False"
   1.177 @@ -383,7 +383,7 @@
   1.178    by (erule notE [THEN notI]) (erule meta_mp)
   1.179  
   1.180  
   1.181 -subsubsection {*Implication*}
   1.182 +subsubsection \<open>Implication\<close>
   1.183  
   1.184  lemma impE:
   1.185    assumes "P-->Q" "P" "Q ==> R"
   1.186 @@ -414,7 +414,7 @@
   1.187    by (erule subst, erule ssubst, assumption)
   1.188  
   1.189  
   1.190 -subsubsection {*Existential quantifier*}
   1.191 +subsubsection \<open>Existential quantifier\<close>
   1.192  
   1.193  lemma exI: "P x ==> EX x::'a. P x"
   1.194  apply (unfold Ex_def)
   1.195 @@ -430,7 +430,7 @@
   1.196  done
   1.197  
   1.198  
   1.199 -subsubsection {*Conjunction*}
   1.200 +subsubsection \<open>Conjunction\<close>
   1.201  
   1.202  lemma conjI: "[| P; Q |] ==> P&Q"
   1.203  apply (unfold and_def)
   1.204 @@ -461,7 +461,7 @@
   1.205  by (iprover intro: conjI assms)
   1.206  
   1.207  
   1.208 -subsubsection {*Disjunction*}
   1.209 +subsubsection \<open>Disjunction\<close>
   1.210  
   1.211  lemma disjI1: "P ==> P|Q"
   1.212  apply (unfold or_def)
   1.213 @@ -482,7 +482,7 @@
   1.214                   major [unfolded or_def, THEN spec, THEN mp, THEN mp])
   1.215  
   1.216  
   1.217 -subsubsection {*Classical logic*}
   1.218 +subsubsection \<open>Classical logic\<close>
   1.219  
   1.220  lemma classical:
   1.221    assumes prem: "~P ==> P"
   1.222 @@ -520,14 +520,14 @@
   1.223  by (iprover intro: classical p1 p2 notE)
   1.224  
   1.225  
   1.226 -subsubsection {*Unique existence*}
   1.227 +subsubsection \<open>Unique existence\<close>
   1.228  
   1.229  lemma ex1I:
   1.230    assumes "P a" "!!x. P(x) ==> x=a"
   1.231    shows "EX! x. P(x)"
   1.232  by (unfold Ex1_def, iprover intro: assms exI conjI allI impI)
   1.233  
   1.234 -text{*Sometimes easier to use: the premises have no shared variables.  Safe!*}
   1.235 +text\<open>Sometimes easier to use: the premises have no shared variables.  Safe!\<close>
   1.236  lemma ex_ex1I:
   1.237    assumes ex_prem: "EX x. P(x)"
   1.238        and eq: "!!x y. [| P(x); P(y) |] ==> x=y"
   1.239 @@ -550,7 +550,7 @@
   1.240  done
   1.241  
   1.242  
   1.243 -subsubsection {*Classical intro rules for disjunction and existential quantifiers*}
   1.244 +subsubsection \<open>Classical intro rules for disjunction and existential quantifiers\<close>
   1.245  
   1.246  lemma disjCI:
   1.247    assumes "~Q ==> P" shows "P|Q"
   1.248 @@ -561,10 +561,10 @@
   1.249  lemma excluded_middle: "~P | P"
   1.250  by (iprover intro: disjCI)
   1.251  
   1.252 -text {*
   1.253 +text \<open>
   1.254    case distinction as a natural deduction rule.
   1.255    Note that @{term "~P"} is the second case, not the first
   1.256 -*}
   1.257 +\<close>
   1.258  lemma case_split [case_names True False]:
   1.259    assumes prem1: "P ==> Q"
   1.260        and prem2: "~P ==> Q"
   1.261 @@ -611,7 +611,7 @@
   1.262  done
   1.263  
   1.264  
   1.265 -subsubsection {* Intuitionistic Reasoning *}
   1.266 +subsubsection \<open>Intuitionistic Reasoning\<close>
   1.267  
   1.268  lemma impE':
   1.269    assumes 1: "P --> Q"
   1.270 @@ -655,7 +655,7 @@
   1.271    and [Pure.elim?] = iffD1 iffD2 impE
   1.272  
   1.273  
   1.274 -subsubsection {* Atomizing meta-level connectives *}
   1.275 +subsubsection \<open>Atomizing meta-level connectives\<close>
   1.276  
   1.277  axiomatization where
   1.278    eq_reflection: "x = y \<Longrightarrow> x \<equiv> y" (*admissible axiom*)
   1.279 @@ -690,7 +690,7 @@
   1.280  lemma atomize_eq [atomize, code]: "(x == y) == Trueprop (x = y)"
   1.281  proof
   1.282    assume "x == y"
   1.283 -  show "x = y" by (unfold `x == y`) (rule refl)
   1.284 +  show "x = y" by (unfold \<open>x == y\<close>) (rule refl)
   1.285  next
   1.286    assume "x = y"
   1.287    then show "x == y" by (rule eq_reflection)
   1.288 @@ -717,7 +717,7 @@
   1.289    and [symmetric, defn] = atomize_all atomize_imp atomize_eq
   1.290  
   1.291  
   1.292 -subsubsection {* Atomizing elimination rules *}
   1.293 +subsubsection \<open>Atomizing elimination rules\<close>
   1.294  
   1.295  lemma atomize_exL[atomize_elim]: "(!!x. P x ==> Q) == ((EX x. P x) ==> Q)"
   1.296    by rule iprover+
   1.297 @@ -731,23 +731,23 @@
   1.298  lemma atomize_elimL[atomize_elim]: "(!!B. (A ==> B) ==> B) == Trueprop A" ..
   1.299  
   1.300  
   1.301 -subsection {* Package setup *}
   1.302 +subsection \<open>Package setup\<close>
   1.303  
   1.304  ML_file "Tools/hologic.ML"
   1.305  
   1.306  
   1.307 -subsubsection {* Sledgehammer setup *}
   1.308 +subsubsection \<open>Sledgehammer setup\<close>
   1.309  
   1.310 -text {*
   1.311 +text \<open>
   1.312  Theorems blacklisted to Sledgehammer. These theorems typically produce clauses
   1.313  that are prolific (match too many equality or membership literals) and relate to
   1.314  seldom-used facts. Some duplicate other rules.
   1.315 -*}
   1.316 +\<close>
   1.317  
   1.318  named_theorems no_atp "theorems that should be filtered out by Sledgehammer"
   1.319  
   1.320  
   1.321 -subsubsection {* Classical Reasoner setup *}
   1.322 +subsubsection \<open>Classical Reasoner setup\<close>
   1.323  
   1.324  lemma imp_elim: "P --> Q ==> (~ R ==> P) ==> (Q ==> R) ==> R"
   1.325    by (rule classical) iprover
   1.326 @@ -758,7 +758,7 @@
   1.327  lemma thin_refl:
   1.328    "\<And>X. \<lbrakk> x=x; PROP W \<rbrakk> \<Longrightarrow> PROP W" .
   1.329  
   1.330 -ML {*
   1.331 +ML \<open>
   1.332  structure Hypsubst = Hypsubst
   1.333  (
   1.334    val dest_eq = HOLogic.dest_eq
   1.335 @@ -786,9 +786,9 @@
   1.336  
   1.337  structure Basic_Classical: BASIC_CLASSICAL = Classical;
   1.338  open Basic_Classical;
   1.339 -*}
   1.340 +\<close>
   1.341  
   1.342 -setup {*
   1.343 +setup \<open>
   1.344    (*prevent substitution on bool*)
   1.345    let
   1.346      fun non_bool_eq (@{const_name HOL.eq}, Type (_, [T, _])) = T <> @{typ bool}
   1.347 @@ -801,7 +801,7 @@
   1.348    in
   1.349      Context_Rules.addSWrapper (fn ctxt => fn tac => hyp_subst_tac' ctxt ORELSE' tac)
   1.350    end
   1.351 -*}
   1.352 +\<close>
   1.353  
   1.354  declare iffI [intro!]
   1.355    and notI [intro!]
   1.356 @@ -824,7 +824,7 @@
   1.357  declare exE [elim!]
   1.358    allE [elim]
   1.359  
   1.360 -ML {* val HOL_cs = claset_of @{context} *}
   1.361 +ML \<open>val HOL_cs = claset_of @{context}\<close>
   1.362  
   1.363  lemma contrapos_np: "~ Q ==> (~ P ==> Q) ==> P"
   1.364    apply (erule swap)
   1.365 @@ -848,11 +848,11 @@
   1.366  apply (rule prem)
   1.367  apply assumption
   1.368  apply (rule allI)+
   1.369 -apply (tactic {* eresolve_tac @{context} [Classical.dup_elim @{context} @{thm allE}] 1 *})
   1.370 +apply (tactic \<open>eresolve_tac @{context} [Classical.dup_elim @{context} @{thm allE}] 1\<close>)
   1.371  apply iprover
   1.372  done
   1.373  
   1.374 -ML {*
   1.375 +ML \<open>
   1.376    structure Blast = Blast
   1.377    (
   1.378      structure Classical = Classical
   1.379 @@ -864,10 +864,10 @@
   1.380      val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
   1.381    );
   1.382    val blast_tac = Blast.blast_tac;
   1.383 -*}
   1.384 +\<close>
   1.385  
   1.386  
   1.387 -subsubsection {*THE: definite description operator*}
   1.388 +subsubsection \<open>THE: definite description operator\<close>
   1.389  
   1.390  lemma the_equality [intro]:
   1.391    assumes "P a"
   1.392 @@ -900,7 +900,7 @@
   1.393    by blast
   1.394  
   1.395  
   1.396 -subsubsection {* Simplifier *}
   1.397 +subsubsection \<open>Simplifier\<close>
   1.398  
   1.399  lemma eta_contract_eq: "(%s. f s) = f" ..
   1.400  
   1.401 @@ -980,7 +980,7 @@
   1.402  lemma imp_conjL: "((P&Q) -->R)  = (P --> (Q --> R))" by iprover
   1.403  lemma imp_disjL: "((P|Q) --> R) = ((P-->R)&(Q-->R))" by iprover
   1.404  
   1.405 -text {* These two are specialized, but @{text imp_disj_not1} is useful in @{text "Auth/Yahalom"}. *}
   1.406 +text \<open>These two are specialized, but @{text imp_disj_not1} is useful in @{text "Auth/Yahalom"}.\<close>
   1.407  lemma imp_disj_not1: "(P --> Q | R) = (~Q --> P --> R)" by blast
   1.408  lemma imp_disj_not2: "(P --> Q | R) = (~R --> P --> Q)" by blast
   1.409  
   1.410 @@ -995,7 +995,7 @@
   1.411  lemma not_imp: "(~(P --> Q)) = (P & ~Q)" by blast
   1.412  lemma not_iff: "(P~=Q) = (P = (~Q))" by blast
   1.413  lemma disj_not1: "(~P | Q) = (P --> Q)" by blast
   1.414 -lemma disj_not2: "(P | ~Q) = (Q --> P)"  -- {* changes orientation :-( *}
   1.415 +lemma disj_not2: "(P | ~Q) = (Q --> P)"  -- \<open>changes orientation :-(\<close>
   1.416    by blast
   1.417  lemma imp_conv_disj: "(P --> Q) = ((~P) | Q)" by blast
   1.418  
   1.419 @@ -1003,8 +1003,8 @@
   1.420  
   1.421  
   1.422  lemma cases_simp: "((P --> Q) & (~P --> Q)) = Q"
   1.423 -  -- {* Avoids duplication of subgoals after @{text split_if}, when the true and false *}
   1.424 -  -- {* cases boil down to the same thing. *}
   1.425 +  -- \<open>Avoids duplication of subgoals after @{text split_if}, when the true and false\<close>
   1.426 +  -- \<open>cases boil down to the same thing.\<close>
   1.427    by blast
   1.428  
   1.429  lemma not_all: "(~ (! x. P(x))) = (? x.~P(x))" by blast
   1.430 @@ -1018,9 +1018,9 @@
   1.431  lemma ex_disj_distrib: "(? x. P(x) | Q(x)) = ((? x. P(x)) | (? x. Q(x)))" by iprover
   1.432  lemma all_conj_distrib: "(!x. P(x) & Q(x)) = ((! x. P(x)) & (! x. Q(x)))" by iprover
   1.433  
   1.434 -text {*
   1.435 +text \<open>
   1.436    \medskip The @{text "&"} congruence rule: not included by default!
   1.437 -  May slow rewrite proofs down by as much as 50\% *}
   1.438 +  May slow rewrite proofs down by as much as 50\%\<close>
   1.439  
   1.440  lemma conj_cong:
   1.441      "(P = P') ==> (P' ==> (Q = Q')) ==> ((P & Q) = (P' & Q'))"
   1.442 @@ -1030,14 +1030,14 @@
   1.443      "(Q = Q') ==> (Q' ==> (P = P')) ==> ((P & Q) = (P' & Q'))"
   1.444    by iprover
   1.445  
   1.446 -text {* The @{text "|"} congruence rule: not included by default! *}
   1.447 +text \<open>The @{text "|"} congruence rule: not included by default!\<close>
   1.448  
   1.449  lemma disj_cong:
   1.450      "(P = P') ==> (~P' ==> (Q = Q')) ==> ((P | Q) = (P' | Q'))"
   1.451    by blast
   1.452  
   1.453  
   1.454 -text {* \medskip if-then-else rules *}
   1.455 +text \<open>\medskip if-then-else rules\<close>
   1.456  
   1.457  lemma if_True [code]: "(if True then x else y) = x"
   1.458    by (unfold If_def) blast
   1.459 @@ -1070,17 +1070,17 @@
   1.460  
   1.461  lemma if_bool_eq_conj:
   1.462  "(if P then Q else R) = ((P-->Q) & (~P-->R))"
   1.463 -  -- {* This form is useful for expanding @{text "if"}s on the RIGHT of the @{text "==>"} symbol. *}
   1.464 +  -- \<open>This form is useful for expanding @{text "if"}s on the RIGHT of the @{text "==>"} symbol.\<close>
   1.465    by (rule split_if)
   1.466  
   1.467  lemma if_bool_eq_disj: "(if P then Q else R) = ((P&Q) | (~P&R))"
   1.468 -  -- {* And this form is useful for expanding @{text "if"}s on the LEFT. *}
   1.469 +  -- \<open>And this form is useful for expanding @{text "if"}s on the LEFT.\<close>
   1.470    by (simplesubst split_if) blast
   1.471  
   1.472  lemma Eq_TrueI: "P ==> P == True" by (unfold atomize_eq) iprover
   1.473  lemma Eq_FalseI: "~P ==> P == False" by (unfold atomize_eq) iprover
   1.474  
   1.475 -text {* \medskip let rules for simproc *}
   1.476 +text \<open>\medskip let rules for simproc\<close>
   1.477  
   1.478  lemma Let_folded: "f x \<equiv> g x \<Longrightarrow>  Let x f \<equiv> Let x g"
   1.479    by (unfold Let_def)
   1.480 @@ -1088,11 +1088,11 @@
   1.481  lemma Let_unfold: "f x \<equiv> g \<Longrightarrow>  Let x f \<equiv> g"
   1.482    by (unfold Let_def)
   1.483  
   1.484 -text {*
   1.485 +text \<open>
   1.486    The following copy of the implication operator is useful for
   1.487    fine-tuning congruence rules.  It instructs the simplifier to simplify
   1.488    its premise.
   1.489 -*}
   1.490 +\<close>
   1.491  
   1.492  definition simp_implies :: "[prop, prop] => prop"  (infixr "=simp=>" 1) where
   1.493    "simp_implies \<equiv> op ==>"
   1.494 @@ -1159,19 +1159,19 @@
   1.495    by blast
   1.496  
   1.497  ML_file "Tools/simpdata.ML"
   1.498 -ML {* open Simpdata *}
   1.499 +ML \<open>open Simpdata\<close>
   1.500  
   1.501 -setup {*
   1.502 +setup \<open>
   1.503    map_theory_simpset (put_simpset HOL_basic_ss) #>
   1.504    Simplifier.method_setup Splitter.split_modifiers
   1.505 -*}
   1.506 +\<close>
   1.507  
   1.508 -simproc_setup defined_Ex ("EX x. P x") = {* fn _ => Quantifier1.rearrange_ex *}
   1.509 -simproc_setup defined_All ("ALL x. P x") = {* fn _ => Quantifier1.rearrange_all *}
   1.510 +simproc_setup defined_Ex ("EX x. P x") = \<open>fn _ => Quantifier1.rearrange_ex\<close>
   1.511 +simproc_setup defined_All ("ALL x. P x") = \<open>fn _ => Quantifier1.rearrange_all\<close>
   1.512  
   1.513 -text {* Simproc for proving @{text "(y = x) == False"} from premise @{text "~(x = y)"}: *}
   1.514 +text \<open>Simproc for proving @{text "(y = x) == False"} from premise @{text "~(x = y)"}:\<close>
   1.515  
   1.516 -simproc_setup neq ("x = y") = {* fn _ =>
   1.517 +simproc_setup neq ("x = y") = \<open>fn _ =>
   1.518  let
   1.519    val neq_to_EQ_False = @{thm not_sym} RS @{thm Eq_FalseI};
   1.520    fun is_neq eq lhs rhs thm =
   1.521 @@ -1188,9 +1188,9 @@
   1.522          | NONE => NONE)
   1.523       | _ => NONE);
   1.524  in proc end;
   1.525 -*}
   1.526 +\<close>
   1.527  
   1.528 -simproc_setup let_simp ("Let x f") = {*
   1.529 +simproc_setup let_simp ("Let x f") = \<open>
   1.530  let
   1.531    val (f_Let_unfold, x_Let_unfold) =
   1.532      let val [(_ $ (f $ x) $ _)] = Thm.prems_of @{thm Let_unfold}
   1.533 @@ -1253,7 +1253,7 @@
   1.534                end
   1.535            | _ => NONE)
   1.536        end
   1.537 -end *}
   1.538 +end\<close>
   1.539  
   1.540  lemma True_implies_equals: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
   1.541  proof
   1.542 @@ -1283,7 +1283,7 @@
   1.543    "!!P Q. (EX x. P | Q x)   = (P | (EX x. Q x))"
   1.544    "!!P Q. (EX x. P x --> Q) = ((ALL x. P x) --> Q)"
   1.545    "!!P Q. (EX x. P --> Q x) = (P --> (EX x. Q x))"
   1.546 -  -- {* Miniscoping: pushing in existential quantifiers. *}
   1.547 +  -- \<open>Miniscoping: pushing in existential quantifiers.\<close>
   1.548    by (iprover | blast)+
   1.549  
   1.550  lemma all_simps:
   1.551 @@ -1293,7 +1293,7 @@
   1.552    "!!P Q. (ALL x. P | Q x)   = (P | (ALL x. Q x))"
   1.553    "!!P Q. (ALL x. P x --> Q) = ((EX x. P x) --> Q)"
   1.554    "!!P Q. (ALL x. P --> Q x) = (P --> (ALL x. Q x))"
   1.555 -  -- {* Miniscoping: pushing in universal quantifiers. *}
   1.556 +  -- \<open>Miniscoping: pushing in universal quantifiers.\<close>
   1.557    by (iprover | blast)+
   1.558  
   1.559  lemmas [simp] =
   1.560 @@ -1330,9 +1330,9 @@
   1.561  lemmas [cong] = imp_cong simp_implies_cong
   1.562  lemmas [split] = split_if
   1.563  
   1.564 -ML {* val HOL_ss = simpset_of @{context} *}
   1.565 +ML \<open>val HOL_ss = simpset_of @{context}\<close>
   1.566  
   1.567 -text {* Simplifies x assuming c and y assuming ~c *}
   1.568 +text \<open>Simplifies x assuming c and y assuming ~c\<close>
   1.569  lemma if_cong:
   1.570    assumes "b = c"
   1.571        and "c \<Longrightarrow> x = u"
   1.572 @@ -1340,20 +1340,20 @@
   1.573    shows "(if b then x else y) = (if c then u else v)"
   1.574    using assms by simp
   1.575  
   1.576 -text {* Prevents simplification of x and y:
   1.577 -  faster and allows the execution of functional programs. *}
   1.578 +text \<open>Prevents simplification of x and y:
   1.579 +  faster and allows the execution of functional programs.\<close>
   1.580  lemma if_weak_cong [cong]:
   1.581    assumes "b = c"
   1.582    shows "(if b then x else y) = (if c then x else y)"
   1.583    using assms by (rule arg_cong)
   1.584  
   1.585 -text {* Prevents simplification of t: much faster *}
   1.586 +text \<open>Prevents simplification of t: much faster\<close>
   1.587  lemma let_weak_cong:
   1.588    assumes "a = b"
   1.589    shows "(let x = a in t x) = (let x = b in t x)"
   1.590    using assms by (rule arg_cong)
   1.591  
   1.592 -text {* To tidy up the result of a simproc.  Only the RHS will be simplified. *}
   1.593 +text \<open>To tidy up the result of a simproc.  Only the RHS will be simplified.\<close>
   1.594  lemma eq_cong2:
   1.595    assumes "u = u'"
   1.596    shows "(t \<equiv> u) \<equiv> (t \<equiv> u')"
   1.597 @@ -1363,23 +1363,23 @@
   1.598    "f (if c then x else y) = (if c then f x else f y)"
   1.599    by simp
   1.600  
   1.601 -text{*As a simplification rule, it replaces all function equalities by
   1.602 -  first-order equalities.*}
   1.603 +text\<open>As a simplification rule, it replaces all function equalities by
   1.604 +  first-order equalities.\<close>
   1.605  lemma fun_eq_iff: "f = g \<longleftrightarrow> (\<forall>x. f x = g x)"
   1.606    by auto
   1.607  
   1.608  
   1.609 -subsubsection {* Generic cases and induction *}
   1.610 +subsubsection \<open>Generic cases and induction\<close>
   1.611  
   1.612 -text {* Rule projections: *}
   1.613 -ML {*
   1.614 +text \<open>Rule projections:\<close>
   1.615 +ML \<open>
   1.616  structure Project_Rule = Project_Rule
   1.617  (
   1.618    val conjunct1 = @{thm conjunct1}
   1.619    val conjunct2 = @{thm conjunct2}
   1.620    val mp = @{thm mp}
   1.621  );
   1.622 -*}
   1.623 +\<close>
   1.624  
   1.625  context
   1.626  begin
   1.627 @@ -1435,10 +1435,10 @@
   1.628  lemma induct_trueI: "induct_true"
   1.629    by (simp add: induct_true_def)
   1.630  
   1.631 -text {* Method setup. *}
   1.632 +text \<open>Method setup.\<close>
   1.633  
   1.634  ML_file "~~/src/Tools/induct.ML"
   1.635 -ML {*
   1.636 +ML \<open>
   1.637  structure Induct = Induct
   1.638  (
   1.639    val cases_default = @{thm case_split}
   1.640 @@ -1450,11 +1450,11 @@
   1.641      | dest_def _ = NONE
   1.642    fun trivial_tac ctxt = match_tac ctxt @{thms induct_trueI}
   1.643  )
   1.644 -*}
   1.645 +\<close>
   1.646  
   1.647  ML_file "~~/src/Tools/induction.ML"
   1.648  
   1.649 -declaration {*
   1.650 +declaration \<open>
   1.651    fn _ => Induct.map_simpset (fn ss => ss
   1.652      addsimprocs
   1.653        [Simplifier.simproc_global @{theory} "swap_induct_false"
   1.654 @@ -1479,9 +1479,9 @@
   1.655      |> Simplifier.set_mksimps (fn ctxt =>
   1.656          Simpdata.mksimps Simpdata.mksimps_pairs ctxt #>
   1.657          map (rewrite_rule ctxt (map Thm.symmetric @{thms induct_rulify_fallback}))))
   1.658 -*}
   1.659 +\<close>
   1.660  
   1.661 -text {* Pre-simplification of induction and cases rules *}
   1.662 +text \<open>Pre-simplification of induction and cases rules\<close>
   1.663  
   1.664  lemma [induct_simp]: "(\<And>x. induct_equal x t \<Longrightarrow> PROP P x) \<equiv> PROP P t"
   1.665    unfolding induct_equal_def
   1.666 @@ -1538,10 +1538,10 @@
   1.667  ML_file "~~/src/Tools/induct_tacs.ML"
   1.668  
   1.669  
   1.670 -subsubsection {* Coherent logic *}
   1.671 +subsubsection \<open>Coherent logic\<close>
   1.672  
   1.673  ML_file "~~/src/Tools/coherent.ML"
   1.674 -ML {*
   1.675 +ML \<open>
   1.676  structure Coherent = Coherent
   1.677  (
   1.678    val atomize_elimL = @{thm atomize_elimL};
   1.679 @@ -1550,12 +1550,12 @@
   1.680    val atomize_disjL = @{thm atomize_disjL};
   1.681    val operator_names = [@{const_name HOL.disj}, @{const_name HOL.conj}, @{const_name Ex}];
   1.682  );
   1.683 -*}
   1.684 +\<close>
   1.685  
   1.686  
   1.687 -subsubsection {* Reorienting equalities *}
   1.688 +subsubsection \<open>Reorienting equalities\<close>
   1.689  
   1.690 -ML {*
   1.691 +ML \<open>
   1.692  signature REORIENT_PROC =
   1.693  sig
   1.694    val add : (term -> bool) -> theory -> theory
   1.695 @@ -1584,10 +1584,10 @@
   1.696        | _ => NONE
   1.697      end;
   1.698  end;
   1.699 -*}
   1.700 +\<close>
   1.701  
   1.702  
   1.703 -subsection {* Other simple lemmas and lemma duplicates *}
   1.704 +subsection \<open>Other simple lemmas and lemma duplicates\<close>
   1.705  
   1.706  lemma ex1_eq [iff]: "EX! x. x = t" "EX! x. t = x"
   1.707    by blast+
   1.708 @@ -1616,9 +1616,9 @@
   1.709    "(\<not> \<not>(P)) = P"
   1.710  by blast+
   1.711  
   1.712 -subsection {* Basic ML bindings *}
   1.713 +subsection \<open>Basic ML bindings\<close>
   1.714  
   1.715 -ML {*
   1.716 +ML \<open>
   1.717  val FalseE = @{thm FalseE}
   1.718  val Let_def = @{thm Let_def}
   1.719  val TrueI = @{thm TrueI}
   1.720 @@ -1667,16 +1667,16 @@
   1.721  val subst = @{thm subst}
   1.722  val sym = @{thm sym}
   1.723  val trans = @{thm trans}
   1.724 -*}
   1.725 +\<close>
   1.726  
   1.727  ML_file "Tools/cnf.ML"
   1.728  
   1.729  
   1.730 -section {* @{text NO_MATCH} simproc *}
   1.731 +section \<open>@{text NO_MATCH} simproc\<close>
   1.732  
   1.733 -text {*
   1.734 +text \<open>
   1.735   The simplification procedure can be used to avoid simplification of terms of a certain form
   1.736 -*}
   1.737 +\<close>
   1.738  
   1.739  definition NO_MATCH :: "'a \<Rightarrow> 'b \<Rightarrow> bool" where "NO_MATCH pat val \<equiv> True"
   1.740  
   1.741 @@ -1684,23 +1684,23 @@
   1.742  
   1.743  declare [[coercion_args NO_MATCH - -]]
   1.744  
   1.745 -simproc_setup NO_MATCH ("NO_MATCH pat val") = {* fn _ => fn ctxt => fn ct =>
   1.746 +simproc_setup NO_MATCH ("NO_MATCH pat val") = \<open>fn _ => fn ctxt => fn ct =>
   1.747    let
   1.748      val thy = Proof_Context.theory_of ctxt
   1.749      val dest_binop = Term.dest_comb #> apfst (Term.dest_comb #> snd)
   1.750      val m = Pattern.matches thy (dest_binop (Thm.term_of ct))
   1.751    in if m then NONE else SOME @{thm NO_MATCH_def} end
   1.752 -*}
   1.753 +\<close>
   1.754  
   1.755 -text {*
   1.756 +text \<open>
   1.757    This setup ensures that a rewrite rule of the form @{term "NO_MATCH pat val \<Longrightarrow> t"}
   1.758    is only applied, if the pattern @{term pat} does not match the value @{term val}.
   1.759 -*}
   1.760 +\<close>
   1.761  
   1.762  
   1.763 -subsection {* Code generator setup *}
   1.764 +subsection \<open>Code generator setup\<close>
   1.765  
   1.766 -subsubsection {* Generic code generator preprocessor setup *}
   1.767 +subsubsection \<open>Generic code generator preprocessor setup\<close>
   1.768  
   1.769  lemma conj_left_cong:
   1.770    "P \<longleftrightarrow> Q \<Longrightarrow> P \<and> R \<longleftrightarrow> Q \<and> R"
   1.771 @@ -1710,16 +1710,16 @@
   1.772    "P \<longleftrightarrow> Q \<Longrightarrow> P \<or> R \<longleftrightarrow> Q \<or> R"
   1.773    by (fact arg_cong)
   1.774  
   1.775 -setup {*
   1.776 +setup \<open>
   1.777    Code_Preproc.map_pre (put_simpset HOL_basic_ss) #>
   1.778    Code_Preproc.map_post (put_simpset HOL_basic_ss) #>
   1.779    Code_Simp.map_ss (put_simpset HOL_basic_ss #>
   1.780    Simplifier.add_cong @{thm conj_left_cong} #>
   1.781    Simplifier.add_cong @{thm disj_left_cong})
   1.782 -*}
   1.783 +\<close>
   1.784  
   1.785  
   1.786 -subsubsection {* Equality *}
   1.787 +subsubsection \<open>Equality\<close>
   1.788  
   1.789  class equal =
   1.790    fixes equal :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   1.791 @@ -1740,16 +1740,16 @@
   1.792  declare eq_equal [symmetric, code_post]
   1.793  declare eq_equal [code]
   1.794  
   1.795 -setup {*
   1.796 +setup \<open>
   1.797    Code_Preproc.map_pre (fn ctxt =>
   1.798      ctxt addsimprocs [Simplifier.simproc_global_i @{theory} "equal" [@{term HOL.eq}]
   1.799        (fn _ => fn Const (_, Type ("fun", [Type _, _])) => SOME @{thm eq_equal} | _ => NONE)])
   1.800 -*}
   1.801 +\<close>
   1.802  
   1.803  
   1.804 -subsubsection {* Generic code generator foundation *}
   1.805 +subsubsection \<open>Generic code generator foundation\<close>
   1.806  
   1.807 -text {* Datatype @{typ bool} *}
   1.808 +text \<open>Datatype @{typ bool}\<close>
   1.809  
   1.810  code_datatype True False
   1.811  
   1.812 @@ -1771,7 +1771,7 @@
   1.813      and "(P \<longrightarrow> False) \<longleftrightarrow> \<not> P"
   1.814      and "(P \<longrightarrow> True) \<longleftrightarrow> True" by simp_all
   1.815  
   1.816 -text {* More about @{typ prop} *}
   1.817 +text \<open>More about @{typ prop}\<close>
   1.818  
   1.819  lemma [code nbe]:
   1.820    shows "(True \<Longrightarrow> PROP Q) \<equiv> PROP Q"
   1.821 @@ -1784,7 +1784,7 @@
   1.822  
   1.823  declare Trueprop_code [symmetric, code_post]
   1.824  
   1.825 -text {* Equality *}
   1.826 +text \<open>Equality\<close>
   1.827  
   1.828  declare simp_thms(6) [code nbe]
   1.829  
   1.830 @@ -1803,42 +1803,42 @@
   1.831    "equal TYPE('a) TYPE('a) \<longleftrightarrow> True"
   1.832    by (simp add: equal)
   1.833  
   1.834 -setup {* Sign.add_const_constraint (@{const_name equal}, SOME @{typ "'a\<Colon>type \<Rightarrow> 'a \<Rightarrow> bool"}) *}
   1.835 +setup \<open>Sign.add_const_constraint (@{const_name equal}, SOME @{typ "'a\<Colon>type \<Rightarrow> 'a \<Rightarrow> bool"})\<close>
   1.836  
   1.837  lemma equal_alias_cert: "OFCLASS('a, equal_class) \<equiv> ((op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool) \<equiv> equal)" (is "?ofclass \<equiv> ?equal")
   1.838  proof
   1.839    assume "PROP ?ofclass"
   1.840    show "PROP ?equal"
   1.841 -    by (tactic {* ALLGOALS (resolve_tac @{context} [Thm.unconstrainT @{thm eq_equal}]) *})
   1.842 -      (fact `PROP ?ofclass`)
   1.843 +    by (tactic \<open>ALLGOALS (resolve_tac @{context} [Thm.unconstrainT @{thm eq_equal}])\<close>)
   1.844 +      (fact \<open>PROP ?ofclass\<close>)
   1.845  next
   1.846    assume "PROP ?equal"
   1.847    show "PROP ?ofclass" proof
   1.848 -  qed (simp add: `PROP ?equal`)
   1.849 +  qed (simp add: \<open>PROP ?equal\<close>)
   1.850  qed
   1.851  
   1.852 -setup {* Sign.add_const_constraint (@{const_name equal}, SOME @{typ "'a\<Colon>equal \<Rightarrow> 'a \<Rightarrow> bool"}) *}
   1.853 +setup \<open>Sign.add_const_constraint (@{const_name equal}, SOME @{typ "'a\<Colon>equal \<Rightarrow> 'a \<Rightarrow> bool"})\<close>
   1.854  
   1.855 -setup {* Nbe.add_const_alias @{thm equal_alias_cert} *}
   1.856 +setup \<open>Nbe.add_const_alias @{thm equal_alias_cert}\<close>
   1.857  
   1.858 -text {* Cases *}
   1.859 +text \<open>Cases\<close>
   1.860  
   1.861  lemma Let_case_cert:
   1.862    assumes "CASE \<equiv> (\<lambda>x. Let x f)"
   1.863    shows "CASE x \<equiv> f x"
   1.864    using assms by simp_all
   1.865  
   1.866 -setup {*
   1.867 +setup \<open>
   1.868    Code.add_case @{thm Let_case_cert} #>
   1.869    Code.add_undefined @{const_name undefined}
   1.870 -*}
   1.871 +\<close>
   1.872  
   1.873  declare [[code abort: undefined]]
   1.874  
   1.875  
   1.876 -subsubsection {* Generic code generator target languages *}
   1.877 +subsubsection \<open>Generic code generator target languages\<close>
   1.878  
   1.879 -text {* type @{typ bool} *}
   1.880 +text \<open>type @{typ bool}\<close>
   1.881  
   1.882  code_printing
   1.883    type_constructor bool \<rightharpoonup>
   1.884 @@ -1885,14 +1885,14 @@
   1.885    code_module Pure \<rightharpoonup>
   1.886      (SML) HOL and (OCaml) HOL and (Haskell) HOL and (Scala) HOL
   1.887  
   1.888 -text {* using built-in Haskell equality *}
   1.889 +text \<open>using built-in Haskell equality\<close>
   1.890  
   1.891  code_printing
   1.892    type_class equal \<rightharpoonup> (Haskell) "Eq"
   1.893  | constant HOL.equal \<rightharpoonup> (Haskell) infix 4 "=="
   1.894  | constant HOL.eq \<rightharpoonup> (Haskell) infix 4 "=="
   1.895  
   1.896 -text {* undefined *}
   1.897 +text \<open>undefined\<close>
   1.898  
   1.899  code_printing
   1.900    constant undefined \<rightharpoonup>
   1.901 @@ -1902,9 +1902,9 @@
   1.902      and (Scala) "!sys.error(\"undefined\")"
   1.903  
   1.904  
   1.905 -subsubsection {* Evaluation and normalization by evaluation *}
   1.906 +subsubsection \<open>Evaluation and normalization by evaluation\<close>
   1.907  
   1.908 -method_setup eval = {*
   1.909 +method_setup eval = \<open>
   1.910    let
   1.911      fun eval_tac ctxt =
   1.912        let val conv = Code_Runtime.dynamic_holds_conv ctxt
   1.913 @@ -1915,25 +1915,25 @@
   1.914    in
   1.915      Scan.succeed (SIMPLE_METHOD' o eval_tac)
   1.916    end
   1.917 -*} "solve goal by evaluation"
   1.918 +\<close> "solve goal by evaluation"
   1.919  
   1.920 -method_setup normalization = {*
   1.921 +method_setup normalization = \<open>
   1.922    Scan.succeed (fn ctxt =>
   1.923      SIMPLE_METHOD'
   1.924        (CHANGED_PROP o
   1.925          (CONVERSION (Nbe.dynamic_conv ctxt)
   1.926            THEN_ALL_NEW (TRY o resolve_tac ctxt [TrueI]))))
   1.927 -*} "solve goal by normalization"
   1.928 +\<close> "solve goal by normalization"
   1.929  
   1.930  
   1.931 -subsection {* Counterexample Search Units *}
   1.932 +subsection \<open>Counterexample Search Units\<close>
   1.933  
   1.934 -subsubsection {* Quickcheck *}
   1.935 +subsubsection \<open>Quickcheck\<close>
   1.936  
   1.937  quickcheck_params [size = 5, iterations = 50]
   1.938  
   1.939  
   1.940 -subsubsection {* Nitpick setup *}
   1.941 +subsubsection \<open>Nitpick setup\<close>
   1.942  
   1.943  named_theorems nitpick_unfold "alternative definitions of constants as needed by Nitpick"
   1.944    and nitpick_simp "equational specification of constants as needed by Nitpick"
   1.945 @@ -1944,16 +1944,16 @@
   1.946          if_bool_eq_disj [no_atp]
   1.947  
   1.948  
   1.949 -subsection {* Preprocessing for the predicate compiler *}
   1.950 +subsection \<open>Preprocessing for the predicate compiler\<close>
   1.951  
   1.952  named_theorems code_pred_def "alternative definitions of constants for the Predicate Compiler"
   1.953    and code_pred_inline "inlining definitions for the Predicate Compiler"
   1.954    and code_pred_simp "simplification rules for the optimisations in the Predicate Compiler"
   1.955  
   1.956  
   1.957 -subsection {* Legacy tactics and ML bindings *}
   1.958 +subsection \<open>Legacy tactics and ML bindings\<close>
   1.959  
   1.960 -ML {*
   1.961 +ML \<open>
   1.962    (* combination of (spec RS spec RS ...(j times) ... spec RS mp) *)
   1.963    local
   1.964      fun wrong_prem (Const (@{const_name All}, _) $ Abs (_, _, t)) = wrong_prem t
   1.965 @@ -1971,7 +1971,7 @@
   1.966    in
   1.967      fun nnf_conv ctxt = Simplifier.rewrite (put_simpset nnf_ss ctxt);
   1.968    end
   1.969 -*}
   1.970 +\<close>
   1.971  
   1.972  hide_const (open) eq equal
   1.973