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.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
```