src/HOL/HOL.thy

 (*  Title:      HOL/HOL.thy
     Author:     Tobias Nipkow, Markus Wenzel, and Larry Paulson
 *)
 
-section {* The basis of Higher-Order Logic *}
+section \<open>The basis of Higher-Order Logic\<close>
 
 theory HOL
 imports Pure "~~/src/Tools/Code_Generator"
 keywords
   "try" "solve_direct" "quickcheck" "print_coercions" "print_claset"

     @{plugin quickcheck_full_exhaustive},
     @{plugin quickcheck_narrowing}]
 \<close>
 
 
-subsection {* Primitive logic *}
-
-subsubsection {* Core syntax *}
-
-setup {* Axclass.class_axiomatization (@{binding type}, []) *}
+subsection \<open>Primitive logic\<close>
+
+subsubsection \<open>Core syntax\<close>
+
+setup \<open>Axclass.class_axiomatization (@{binding type}, [])\<close>
 default_sort type
-setup {* Object_Logic.add_base_sort @{sort type} *}
+setup \<open>Object_Logic.add_base_sort @{sort type}\<close>
 
 axiomatization where fun_arity: "OFCLASS('a \<Rightarrow> 'b, type_class)"
 instance "fun" :: (type, type) type by (rule fun_arity)
 
 axiomatization where itself_arity: "OFCLASS('a itself, type_class)"

   All           :: "('a => bool) => bool"           (binder "ALL " 10)
   Ex            :: "('a => bool) => bool"           (binder "EX " 10)
   Ex1           :: "('a => bool) => bool"           (binder "EX! " 10)
 
 
-subsubsection {* Additional concrete syntax *}
+subsubsection \<open>Additional concrete syntax\<close>
 
 notation (output)
   eq  (infix "=" 50)
 
 abbreviation

 notation (xsymbols)
   iff  (infixr "\<longleftrightarrow>" 25)
 
 syntax "_The" :: "[pttrn, bool] => 'a"  ("(3THE _./ _)" [0, 10] 10)
 translations "THE x. P" == "CONST The (%x. P)"
-print_translation {*
+print_translation \<open>
   [(@{const_syntax The}, fn _ => fn [Abs abs] =>
       let val (x, t) = Syntax_Trans.atomic_abs_tr' abs
       in Syntax.const @{syntax_const "_The"} $ x $ t end)]
-*}  -- {* To avoid eta-contraction of body *}
+\<close>  -- \<open>To avoid eta-contraction of body\<close>
 
 nonterminal letbinds and letbind
 syntax
   "_bind"       :: "[pttrn, 'a] => letbind"              ("(2_ =/ _)" 10)
   ""            :: "letbind => letbinds"                 ("_")

   All  (binder "! " 10) and
   Ex  (binder "? " 10) and
   Ex1  (binder "?! " 10)
 
 
-subsubsection {* Axioms and basic definitions *}
+subsubsection \<open>Axioms and basic definitions\<close>
 
 axiomatization where
   refl: "t = (t::'a)" and
   subst: "s = t \<Longrightarrow> P s \<Longrightarrow> P t" and
   ext: "(!!x::'a. (f x ::'b) = g x) ==> (%x. f x) = (%x. g x)"
-    -- {*Extensionality is built into the meta-logic, and this rule expresses
+    -- \<open>Extensionality is built into the meta-logic, and this rule expresses
          a related property.  It is an eta-expanded version of the traditional
-         rule, and similar to the ABS rule of HOL*} and
+         rule, and similar to the ABS rule of HOL\<close> and
 
   the_eq_trivial: "(THE x. x = a) = (a::'a)"
 
 axiomatization where
   impI: "(P ==> Q) ==> P-->Q" and

 axiomatization undefined :: 'a
 
 class default = fixes default :: 'a
 
 
-subsection {* Fundamental rules *}
-
-subsubsection {* Equality *}
+subsection \<open>Fundamental rules\<close>
+
+subsubsection \<open>Equality\<close>
 
 lemma sym: "s = t ==> t = s"
   by (erule subst) (rule refl)
 
 lemma ssubst: "t = s ==> P s ==> P t"

 lemma meta_eq_to_obj_eq:
   assumes meq: "A == B"
   shows "A = B"
   by (unfold meq) (rule refl)
 
-text {* Useful with @{text erule} for proving equalities from known equalities. *}
+text \<open>Useful with @{text erule} for proving equalities from known equalities.\<close>
      (* a = b
         |   |
         c = d   *)
 lemma box_equals: "[| a=b;  a=c;  b=d |] ==> c=d"
 apply (rule trans)
 apply (rule trans)
 apply (rule sym)
 apply assumption+
 done
 
-text {* For calculational reasoning: *}
+text \<open>For calculational reasoning:\<close>
 
 lemma forw_subst: "a = b ==> P b ==> P a"
   by (rule ssubst)
 
 lemma back_subst: "P a ==> a = b ==> P b"
   by (rule subst)
 
 
-subsubsection {* Congruence rules for application *}
-
-text {* Similar to @{text AP_THM} in Gordon's HOL. *}
+subsubsection \<open>Congruence rules for application\<close>
+
+text \<open>Similar to @{text AP_THM} in Gordon's HOL.\<close>
 lemma fun_cong: "(f::'a=>'b) = g ==> f(x)=g(x)"
 apply (erule subst)
 apply (rule refl)
 done
 
-text {* Similar to @{text AP_TERM} in Gordon's HOL and FOL's @{text subst_context}. *}
+text \<open>Similar to @{text AP_TERM} in Gordon's HOL and FOL's @{text subst_context}.\<close>
 lemma arg_cong: "x=y ==> f(x)=f(y)"
 apply (erule subst)
 apply (rule refl)
 done
 

 lemma cong: "[| f = g; (x::'a) = y |] ==> f x = g y"
 apply (erule subst)+
 apply (rule refl)
 done
 
-ML {* fun cong_tac ctxt = Cong_Tac.cong_tac ctxt @{thm cong} *}
-
-
-subsubsection {* Equality of booleans -- iff *}
+ML \<open>fun cong_tac ctxt = Cong_Tac.cong_tac ctxt @{thm cong}\<close>
+
+
+subsubsection \<open>Equality of booleans -- iff\<close>
 
 lemma iffI: assumes "P ==> Q" and "Q ==> P" shows "P=Q"
   by (iprover intro: iff [THEN mp, THEN mp] impI assms)
 
 lemma iffD2: "[| P=Q; Q |] ==> P"

     and minor: "[| P --> Q; Q --> P |] ==> R"
   shows R
   by (iprover intro: minor impI major [THEN iffD2] major [THEN iffD1])
 
 
-subsubsection {*True*}
+subsubsection \<open>True\<close>
 
 lemma TrueI: "True"
   unfolding True_def by (rule refl)
 
 lemma eqTrueI: "P ==> P = True"

 
 lemma eqTrueE: "P = True ==> P"
   by (erule iffD2) (rule TrueI)
 
 
-subsubsection {*Universal quantifier*}
+subsubsection \<open>Universal quantifier\<close>
 
 lemma allI: assumes "!!x::'a. P(x)" shows "ALL x. P(x)"
   unfolding All_def by (iprover intro: ext eqTrueI assms)
 
 lemma spec: "ALL x::'a. P(x) ==> P(x)"

     and minor: "[| P(x); ALL x. P(x) |] ==> R"
   shows R
   by (iprover intro: minor major major [THEN spec])
 
 
-subsubsection {* False *}
-
-text {*
+subsubsection \<open>False\<close>
+
+text \<open>
   Depends upon @{text spec}; it is impossible to do propositional
   logic before quantifiers!
-*}
+\<close>
 
 lemma FalseE: "False ==> P"
   apply (unfold False_def)
   apply (erule spec)
   done
 
 lemma False_neq_True: "False = True ==> P"
   by (erule eqTrueE [THEN FalseE])
 
 
-subsubsection {* Negation *}
+subsubsection \<open>Negation\<close>
 
 lemma notI:
   assumes "P ==> False"
   shows "~P"
   apply (unfold not_def)

 
 lemma notI2: "(P \<Longrightarrow> \<not> Pa) \<Longrightarrow> (P \<Longrightarrow> Pa) \<Longrightarrow> \<not> P"
   by (erule notE [THEN notI]) (erule meta_mp)
 
 
-subsubsection {*Implication*}
+subsubsection \<open>Implication\<close>
 
 lemma impE:
   assumes "P-->Q" "P" "Q ==> R"
   shows "R"
 by (iprover intro: assms mp)

 
 lemma eq_neq_eq_imp_neq: "[| x = a ; a ~= b; b = y |] ==> x ~= y"
   by (erule subst, erule ssubst, assumption)
 
 
-subsubsection {*Existential quantifier*}
+subsubsection \<open>Existential quantifier\<close>
 
 lemma exI: "P x ==> EX x::'a. P x"
 apply (unfold Ex_def)
 apply (iprover intro: allI allE impI mp)
 done

 apply (rule major [unfolded Ex_def, THEN spec, THEN mp])
 apply (iprover intro: impI [THEN allI] minor)
 done
 
 
-subsubsection {*Conjunction*}
+subsubsection \<open>Conjunction\<close>
 
 lemma conjI: "[| P; Q |] ==> P&Q"
 apply (unfold and_def)
 apply (iprover intro: impI [THEN allI] mp)
 done

 lemma context_conjI:
   assumes "P" "P ==> Q" shows "P & Q"
 by (iprover intro: conjI assms)
 
 
-subsubsection {*Disjunction*}
+subsubsection \<open>Disjunction\<close>
 
 lemma disjI1: "P ==> P|Q"
 apply (unfold or_def)
 apply (iprover intro: allI impI mp)
 done

   shows "R"
 by (iprover intro: minorP minorQ impI
                  major [unfolded or_def, THEN spec, THEN mp, THEN mp])
 
 
-subsubsection {*Classical logic*}
+subsubsection \<open>Classical logic\<close>
 
 lemma classical:
   assumes prem: "~P ==> P"
   shows "P"
 apply (rule True_or_False [THEN disjE, THEN eqTrueE])

       and p2: "~P ==> ~Q"
   shows "P"
 by (iprover intro: classical p1 p2 notE)
 
 
-subsubsection {*Unique existence*}
+subsubsection \<open>Unique existence\<close>
 
 lemma ex1I:
   assumes "P a" "!!x. P(x) ==> x=a"
   shows "EX! x. P(x)"
 by (unfold Ex1_def, iprover intro: assms exI conjI allI impI)
 
-text{*Sometimes easier to use: the premises have no shared variables.  Safe!*}
+text\<open>Sometimes easier to use: the premises have no shared variables.  Safe!\<close>
 lemma ex_ex1I:
   assumes ex_prem: "EX x. P(x)"
       and eq: "!!x y. [| P(x); P(y) |] ==> x=y"
   shows "EX! x. P(x)"
 by (iprover intro: ex_prem [THEN exE] ex1I eq)

 apply (rule exI)
 apply assumption
 done
 
 
-subsubsection {*Classical intro rules for disjunction and existential quantifiers*}
+subsubsection \<open>Classical intro rules for disjunction and existential quantifiers\<close>
 
 lemma disjCI:
   assumes "~Q ==> P" shows "P|Q"
 apply (rule classical)
 apply (iprover intro: assms disjI1 disjI2 notI elim: notE)
 done
 
 lemma excluded_middle: "~P | P"
 by (iprover intro: disjCI)
 
-text {*
+text \<open>
   case distinction as a natural deduction rule.
   Note that @{term "~P"} is the second case, not the first
-*}
+\<close>
 lemma case_split [case_names True False]:
   assumes prem1: "P ==> Q"
       and prem2: "~P ==> Q"
   shows "Q"
 apply (rule excluded_middle [THEN disjE])

 apply (rule ccontr)
 apply (iprover intro: assms exI allI notI notE [of "\<exists>x. P x"])
 done
 
 
-subsubsection {* Intuitionistic Reasoning *}
+subsubsection \<open>Intuitionistic Reasoning\<close>
 
 lemma impE':
   assumes 1: "P --> Q"
     and 2: "Q ==> R"
     and 3: "P --> Q ==> P"

 lemmas [trans] = trans
   and [sym] = sym not_sym
   and [Pure.elim?] = iffD1 iffD2 impE
 
 
-subsubsection {* Atomizing meta-level connectives *}
+subsubsection \<open>Atomizing meta-level connectives\<close>
 
 axiomatization where
   eq_reflection: "x = y \<Longrightarrow> x \<equiv> y" (*admissible axiom*)
 
 lemma atomize_all [atomize]: "(!!x. P x) == Trueprop (ALL x. P x)"

 qed
 
 lemma atomize_eq [atomize, code]: "(x == y) == Trueprop (x = y)"
 proof
   assume "x == y"
-  show "x = y" by (unfold `x == y`) (rule refl)
+  show "x = y" by (unfold \<open>x == y\<close>) (rule refl)
 next
   assume "x = y"
   then show "x == y" by (rule eq_reflection)
 qed
 

 
 lemmas [symmetric, rulify] = atomize_all atomize_imp
   and [symmetric, defn] = atomize_all atomize_imp atomize_eq
 
 
-subsubsection {* Atomizing elimination rules *}
+subsubsection \<open>Atomizing elimination rules\<close>
 
 lemma atomize_exL[atomize_elim]: "(!!x. P x ==> Q) == ((EX x. P x) ==> Q)"
   by rule iprover+
 
 lemma atomize_conjL[atomize_elim]: "(A ==> B ==> C) == (A & B ==> C)"

   by rule iprover+
 
 lemma atomize_elimL[atomize_elim]: "(!!B. (A ==> B) ==> B) == Trueprop A" ..
 
 
-subsection {* Package setup *}
+subsection \<open>Package setup\<close>
 
 ML_file "Tools/hologic.ML"
 
 
-subsubsection {* Sledgehammer setup *}
-
-text {*
+subsubsection \<open>Sledgehammer setup\<close>
+
+text \<open>
 Theorems blacklisted to Sledgehammer. These theorems typically produce clauses
 that are prolific (match too many equality or membership literals) and relate to
 seldom-used facts. Some duplicate other rules.
-*}
+\<close>
 
 named_theorems no_atp "theorems that should be filtered out by Sledgehammer"
 
 
-subsubsection {* Classical Reasoner setup *}
+subsubsection \<open>Classical Reasoner setup\<close>
 
 lemma imp_elim: "P --> Q ==> (~ R ==> P) ==> (Q ==> R) ==> R"
   by (rule classical) iprover
 
 lemma swap: "~ P ==> (~ R ==> P) ==> R"
   by (rule classical) iprover
 
 lemma thin_refl:
   "\<And>X. \<lbrakk> x=x; PROP W \<rbrakk> \<Longrightarrow> PROP W" .
 
-ML {*
+ML \<open>
 structure Hypsubst = Hypsubst
 (
   val dest_eq = HOLogic.dest_eq
   val dest_Trueprop = HOLogic.dest_Trueprop
   val dest_imp = HOLogic.dest_imp

   val hyp_subst_tacs = [Hypsubst.hyp_subst_tac]
 );
 
 structure Basic_Classical: BASIC_CLASSICAL = Classical;
 open Basic_Classical;
-*}
-
-setup {*
+\<close>
+
+setup \<open>
   (*prevent substitution on bool*)
   let
     fun non_bool_eq (@{const_name HOL.eq}, Type (_, [T, _])) = T <> @{typ bool}
       | non_bool_eq _ = false;
     fun hyp_subst_tac' ctxt =

         then Hypsubst.hyp_subst_tac ctxt i
         else no_tac);
   in
     Context_Rules.addSWrapper (fn ctxt => fn tac => hyp_subst_tac' ctxt ORELSE' tac)
   end
-*}
+\<close>
 
 declare iffI [intro!]
   and notI [intro!]
   and impI [intro!]
   and disjCI [intro!]

   and exI [intro]
 
 declare exE [elim!]
   allE [elim]
 
-ML {* val HOL_cs = claset_of @{context} *}
+ML \<open>val HOL_cs = claset_of @{context}\<close>
 
 lemma contrapos_np: "~ Q ==> (~ P ==> Q) ==> P"
   apply (erule swap)
   apply (erule (1) meta_mp)
   done

   shows R
 apply (rule ex1E [OF major])
 apply (rule prem)
 apply assumption
 apply (rule allI)+
-apply (tactic {* eresolve_tac @{context} [Classical.dup_elim @{context} @{thm allE}] 1 *})
+apply (tactic \<open>eresolve_tac @{context} [Classical.dup_elim @{context} @{thm allE}] 1\<close>)
 apply iprover
 done
 
-ML {*
+ML \<open>
   structure Blast = Blast
   (
     structure Classical = Classical
     val Trueprop_const = dest_Const @{const Trueprop}
     val equality_name = @{const_name HOL.eq}

     val notE = @{thm notE}
     val ccontr = @{thm ccontr}
     val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
   );
   val blast_tac = Blast.blast_tac;
-*}
-
-
-subsubsection {*THE: definite description operator*}
+\<close>
+
+
+subsubsection \<open>THE: definite description operator\<close>
 
 lemma the_equality [intro]:
   assumes "P a"
       and "!!x. P x ==> x=a"
   shows "(THE x. P x) = a"

 
 lemma the_sym_eq_trivial: "(THE y. x=y) = x"
   by blast
 
 
-subsubsection {* Simplifier *}
+subsubsection \<open>Simplifier\<close>
 
 lemma eta_contract_eq: "(%s. f s) = f" ..
 
 lemma simp_thms:
   shows not_not: "(~ ~ P) = P"

 
 lemma imp_conjR: "(P --> (Q&R)) = ((P-->Q) & (P-->R))" by iprover
 lemma imp_conjL: "((P&Q) -->R)  = (P --> (Q --> R))" by iprover
 lemma imp_disjL: "((P|Q) --> R) = ((P-->R)&(Q-->R))" by iprover
 
-text {* These two are specialized, but @{text imp_disj_not1} is useful in @{text "Auth/Yahalom"}. *}
+text \<open>These two are specialized, but @{text imp_disj_not1} is useful in @{text "Auth/Yahalom"}.\<close>
 lemma imp_disj_not1: "(P --> Q | R) = (~Q --> P --> R)" by blast
 lemma imp_disj_not2: "(P --> Q | R) = (~R --> P --> Q)" by blast
 
 lemma imp_disj1: "((P-->Q)|R) = (P--> Q|R)" by blast
 lemma imp_disj2: "(Q|(P-->R)) = (P--> Q|R)" by blast

 lemma de_Morgan_disj: "(~(P | Q)) = (~P & ~Q)" by iprover
 lemma de_Morgan_conj: "(~(P & Q)) = (~P | ~Q)" by blast
 lemma not_imp: "(~(P --> Q)) = (P & ~Q)" by blast
 lemma not_iff: "(P~=Q) = (P = (~Q))" by blast
 lemma disj_not1: "(~P | Q) = (P --> Q)" by blast
-lemma disj_not2: "(P | ~Q) = (Q --> P)"  -- {* changes orientation :-( *}
+lemma disj_not2: "(P | ~Q) = (Q --> P)"  -- \<open>changes orientation :-(\<close>
   by blast
 lemma imp_conv_disj: "(P --> Q) = ((~P) | Q)" by blast
 
 lemma iff_conv_conj_imp: "(P = Q) = ((P --> Q) & (Q --> P))" by iprover
 
 
 lemma cases_simp: "((P --> Q) & (~P --> Q)) = Q"
-  -- {* Avoids duplication of subgoals after @{text split_if}, when the true and false *}
-  -- {* cases boil down to the same thing. *}
+  -- \<open>Avoids duplication of subgoals after @{text split_if}, when the true and false\<close>
+  -- \<open>cases boil down to the same thing.\<close>
   by blast
 
 lemma not_all: "(~ (! x. P(x))) = (? x.~P(x))" by blast
 lemma imp_all: "((! x. P x) --> Q) = (? x. P x --> Q)" by blast
 lemma not_ex: "(~ (? x. P(x))) = (! x.~P(x))" by iprover

 declare All_def [no_atp]
 
 lemma ex_disj_distrib: "(? x. P(x) | Q(x)) = ((? x. P(x)) | (? x. Q(x)))" by iprover
 lemma all_conj_distrib: "(!x. P(x) & Q(x)) = ((! x. P(x)) & (! x. Q(x)))" by iprover
 
-text {*
+text \<open>
   \medskip The @{text "&"} congruence rule: not included by default!
-  May slow rewrite proofs down by as much as 50\% *}
+  May slow rewrite proofs down by as much as 50\%\<close>
 
 lemma conj_cong:
     "(P = P') ==> (P' ==> (Q = Q')) ==> ((P & Q) = (P' & Q'))"
   by iprover
 
 lemma rev_conj_cong:
     "(Q = Q') ==> (Q' ==> (P = P')) ==> ((P & Q) = (P' & Q'))"
   by iprover
 
-text {* The @{text "|"} congruence rule: not included by default! *}
+text \<open>The @{text "|"} congruence rule: not included by default!\<close>
 
 lemma disj_cong:
     "(P = P') ==> (~P' ==> (Q = Q')) ==> ((P | Q) = (P' | Q'))"
   by blast
 
 
-text {* \medskip if-then-else rules *}
+text \<open>\medskip if-then-else rules\<close>
 
 lemma if_True [code]: "(if True then x else y) = x"
   by (unfold If_def) blast
 
 lemma if_False [code]: "(if False then x else y) = y"

 lemma if_eq_cancel: "(if x = y then y else x) = x"
 by (simplesubst split_if, blast)
 
 lemma if_bool_eq_conj:
 "(if P then Q else R) = ((P-->Q) & (~P-->R))"
-  -- {* This form is useful for expanding @{text "if"}s on the RIGHT of the @{text "==>"} symbol. *}
+  -- \<open>This form is useful for expanding @{text "if"}s on the RIGHT of the @{text "==>"} symbol.\<close>
   by (rule split_if)
 
 lemma if_bool_eq_disj: "(if P then Q else R) = ((P&Q) | (~P&R))"
-  -- {* And this form is useful for expanding @{text "if"}s on the LEFT. *}
+  -- \<open>And this form is useful for expanding @{text "if"}s on the LEFT.\<close>
   by (simplesubst split_if) blast
 
 lemma Eq_TrueI: "P ==> P == True" by (unfold atomize_eq) iprover
 lemma Eq_FalseI: "~P ==> P == False" by (unfold atomize_eq) iprover
 
-text {* \medskip let rules for simproc *}
+text \<open>\medskip let rules for simproc\<close>
 
 lemma Let_folded: "f x \<equiv> g x \<Longrightarrow>  Let x f \<equiv> Let x g"
   by (unfold Let_def)
 
 lemma Let_unfold: "f x \<equiv> g \<Longrightarrow>  Let x f \<equiv> g"
   by (unfold Let_def)
 
-text {*
+text \<open>
   The following copy of the implication operator is useful for
   fine-tuning congruence rules.  It instructs the simplifier to simplify
   its premise.
-*}
+\<close>
 
 definition simp_implies :: "[prop, prop] => prop"  (infixr "=simp=>" 1) where
   "simp_implies \<equiv> op ==>"
 
 lemma simp_impliesI:

 lemma ex_comm:
   "(\<exists>x y. P x y) = (\<exists>y x. P x y)"
   by blast
 
 ML_file "Tools/simpdata.ML"
-ML {* open Simpdata *}
-
-setup {*
+ML \<open>open Simpdata\<close>
+
+setup \<open>
   map_theory_simpset (put_simpset HOL_basic_ss) #>
   Simplifier.method_setup Splitter.split_modifiers
-*}
-
-simproc_setup defined_Ex ("EX x. P x") = {* fn _ => Quantifier1.rearrange_ex *}
-simproc_setup defined_All ("ALL x. P x") = {* fn _ => Quantifier1.rearrange_all *}
-
-text {* Simproc for proving @{text "(y = x) == False"} from premise @{text "~(x = y)"}: *}
-
-simproc_setup neq ("x = y") = {* fn _ =>
+\<close>
+
+simproc_setup defined_Ex ("EX x. P x") = \<open>fn _ => Quantifier1.rearrange_ex\<close>
+simproc_setup defined_All ("ALL x. P x") = \<open>fn _ => Quantifier1.rearrange_all\<close>
+
+text \<open>Simproc for proving @{text "(y = x) == False"} from premise @{text "~(x = y)"}:\<close>
+
+simproc_setup neq ("x = y") = \<open>fn _ =>
 let
   val neq_to_EQ_False = @{thm not_sym} RS @{thm Eq_FalseI};
   fun is_neq eq lhs rhs thm =
     (case Thm.prop_of thm of
       _ $ (Not $ (eq' $ l' $ r')) =>

         (case find_first (is_neq eq lhs rhs) (Simplifier.prems_of ss) of
           SOME thm => SOME (thm RS neq_to_EQ_False)
         | NONE => NONE)
      | _ => NONE);
 in proc end;
-*}
-
-simproc_setup let_simp ("Let x f") = {*
+\<close>
+
+simproc_setup let_simp ("Let x f") = \<open>
 let
   val (f_Let_unfold, x_Let_unfold) =
     let val [(_ $ (f $ x) $ _)] = Thm.prems_of @{thm Let_unfold}
     in apply2 (Thm.cterm_of @{context}) (f, x) end
   val (f_Let_folded, x_Let_folded) =

                          (g_Let_folded, Thm.cterm_of ctxt abs_g')];
                   in SOME (rl OF [Thm.transitive fx_g g_g'x]) end
               end
           | _ => NONE)
       end
-end *}
+end\<close>
 
 lemma True_implies_equals: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
 proof
   assume "True \<Longrightarrow> PROP P"
   from this [OF TrueI] show "PROP P" .

   "!!P Q. (EX x. P & Q x)   = (P & (EX x. Q x))"
   "!!P Q. (EX x. P x | Q)   = ((EX x. P x) | Q)"
   "!!P Q. (EX x. P | Q x)   = (P | (EX x. Q x))"
   "!!P Q. (EX x. P x --> Q) = ((ALL x. P x) --> Q)"
   "!!P Q. (EX x. P --> Q x) = (P --> (EX x. Q x))"
-  -- {* Miniscoping: pushing in existential quantifiers. *}
+  -- \<open>Miniscoping: pushing in existential quantifiers.\<close>
   by (iprover | blast)+
 
 lemma all_simps:
   "!!P Q. (ALL x. P x & Q)   = ((ALL x. P x) & Q)"
   "!!P Q. (ALL x. P & Q x)   = (P & (ALL x. Q x))"
   "!!P Q. (ALL x. P x | Q)   = ((ALL x. P x) | Q)"
   "!!P Q. (ALL x. P | Q x)   = (P | (ALL x. Q x))"
   "!!P Q. (ALL x. P x --> Q) = ((EX x. P x) --> Q)"
   "!!P Q. (ALL x. P --> Q x) = (P --> (ALL x. Q x))"
-  -- {* Miniscoping: pushing in universal quantifiers. *}
+  -- \<open>Miniscoping: pushing in universal quantifiers.\<close>
   by (iprover | blast)+
 
 lemmas [simp] =
   triv_forall_equality (*prunes params*)
   True_implies_equals implies_True_equals (*prune True in asms*)

   simp_thms
 
 lemmas [cong] = imp_cong simp_implies_cong
 lemmas [split] = split_if
 
-ML {* val HOL_ss = simpset_of @{context} *}
-
-text {* Simplifies x assuming c and y assuming ~c *}
+ML \<open>val HOL_ss = simpset_of @{context}\<close>
+
+text \<open>Simplifies x assuming c and y assuming ~c\<close>
 lemma if_cong:
   assumes "b = c"
       and "c \<Longrightarrow> x = u"
       and "\<not> c \<Longrightarrow> y = v"
   shows "(if b then x else y) = (if c then u else v)"
   using assms by simp
 
-text {* Prevents simplification of x and y:
-  faster and allows the execution of functional programs. *}
+text \<open>Prevents simplification of x and y:
+  faster and allows the execution of functional programs.\<close>
 lemma if_weak_cong [cong]:
   assumes "b = c"
   shows "(if b then x else y) = (if c then x else y)"
   using assms by (rule arg_cong)
 
-text {* Prevents simplification of t: much faster *}
+text \<open>Prevents simplification of t: much faster\<close>
 lemma let_weak_cong:
   assumes "a = b"
   shows "(let x = a in t x) = (let x = b in t x)"
   using assms by (rule arg_cong)
 
-text {* To tidy up the result of a simproc.  Only the RHS will be simplified. *}
+text \<open>To tidy up the result of a simproc.  Only the RHS will be simplified.\<close>
 lemma eq_cong2:
   assumes "u = u'"
   shows "(t \<equiv> u) \<equiv> (t \<equiv> u')"
   using assms by simp
 
 lemma if_distrib:
   "f (if c then x else y) = (if c then f x else f y)"
   by simp
 
-text{*As a simplification rule, it replaces all function equalities by
-  first-order equalities.*}
+text\<open>As a simplification rule, it replaces all function equalities by
+  first-order equalities.\<close>
 lemma fun_eq_iff: "f = g \<longleftrightarrow> (\<forall>x. f x = g x)"
   by auto
 
 
-subsubsection {* Generic cases and induction *}
-
-text {* Rule projections: *}
-ML {*
+subsubsection \<open>Generic cases and induction\<close>
+
+text \<open>Rule projections:\<close>
+ML \<open>
 structure Project_Rule = Project_Rule
 (
   val conjunct1 = @{thm conjunct1}
   val conjunct2 = @{thm conjunct2}
   val mp = @{thm mp}
 );
-*}
+\<close>
 
 context
 begin
 
 qualified definition "induct_forall P \<equiv> \<forall>x. P x"

 lemmas induct_conj = induct_forall_conj induct_implies_conj induct_conj_curry
 
 lemma induct_trueI: "induct_true"
   by (simp add: induct_true_def)
 
-text {* Method setup. *}
+text \<open>Method setup.\<close>
 
 ML_file "~~/src/Tools/induct.ML"
-ML {*
+ML \<open>
 structure Induct = Induct
 (
   val cases_default = @{thm case_split}
   val atomize = @{thms induct_atomize}
   val rulify = @{thms induct_rulify'}

   val equal_def = @{thm induct_equal_def}
   fun dest_def (Const (@{const_name induct_equal}, _) $ t $ u) = SOME (t, u)
     | dest_def _ = NONE
   fun trivial_tac ctxt = match_tac ctxt @{thms induct_trueI}
 )
-*}
+\<close>
 
 ML_file "~~/src/Tools/induction.ML"
 
-declaration {*
+declaration \<open>
   fn _ => Induct.map_simpset (fn ss => ss
     addsimprocs
       [Simplifier.simproc_global @{theory} "swap_induct_false"
          ["induct_false ==> PROP P ==> PROP Q"]
          (fn _ =>

                 in if is_conj P then SOME @{thm induct_conj_curry} else NONE end
               | _ => NONE))]
     |> Simplifier.set_mksimps (fn ctxt =>
         Simpdata.mksimps Simpdata.mksimps_pairs ctxt #>
         map (rewrite_rule ctxt (map Thm.symmetric @{thms induct_rulify_fallback}))))
-*}
-
-text {* Pre-simplification of induction and cases rules *}
+\<close>
+
+text \<open>Pre-simplification of induction and cases rules\<close>
 
 lemma [induct_simp]: "(\<And>x. induct_equal x t \<Longrightarrow> PROP P x) \<equiv> PROP P t"
   unfolding induct_equal_def
 proof
   assume r: "\<And>x. x = t \<Longrightarrow> PROP P x"

 end
 
 ML_file "~~/src/Tools/induct_tacs.ML"
 
 
-subsubsection {* Coherent logic *}
+subsubsection \<open>Coherent logic\<close>
 
 ML_file "~~/src/Tools/coherent.ML"
-ML {*
+ML \<open>
 structure Coherent = Coherent
 (
   val atomize_elimL = @{thm atomize_elimL};
   val atomize_exL = @{thm atomize_exL};
   val atomize_conjL = @{thm atomize_conjL};
   val atomize_disjL = @{thm atomize_disjL};
   val operator_names = [@{const_name HOL.disj}, @{const_name HOL.conj}, @{const_name Ex}];
 );
-*}
-
-
-subsubsection {* Reorienting equalities *}
-
-ML {*
+\<close>
+
+
+subsubsection \<open>Reorienting equalities\<close>
+
+ML \<open>
 signature REORIENT_PROC =
 sig
   val add : (term -> bool) -> theory -> theory
   val proc : morphism -> Proof.context -> cterm -> thm option
 end;

       case Thm.term_of ct of
         (_ $ t $ u) => if matches thy u then NONE else SOME meta_reorient
       | _ => NONE
     end;
 end;
-*}
-
-
-subsection {* Other simple lemmas and lemma duplicates *}
+\<close>
+
+
+subsection \<open>Other simple lemmas and lemma duplicates\<close>
 
 lemma ex1_eq [iff]: "EX! x. x = t" "EX! x. t = x"
   by blast+
 
 lemma choice_eq: "(ALL x. EX! y. P x y) = (EX! f. ALL x. P x (f x))"

   "(\<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)"
   "(P = Q) = ((P \<and> Q) \<or> (\<not>P \<and> \<not> Q))" "(\<not>(P = Q)) = ((P \<and> \<not> Q) \<or> (\<not>P \<and> Q))"
   "(\<not> \<not>(P)) = P"
 by blast+
 
-subsection {* Basic ML bindings *}
-
-ML {*
+subsection \<open>Basic ML bindings\<close>
+
+ML \<open>
 val FalseE = @{thm FalseE}
 val Let_def = @{thm Let_def}
 val TrueI = @{thm TrueI}
 val allE = @{thm allE}
 val allI = @{thm allI}

 val spec = @{thm spec}
 val ssubst = @{thm ssubst}
 val subst = @{thm subst}
 val sym = @{thm sym}
 val trans = @{thm trans}
-*}
+\<close>
 
 ML_file "Tools/cnf.ML"
 
 
-section {* @{text NO_MATCH} simproc *}
-
-text {*
+section \<open>@{text NO_MATCH} simproc\<close>
+
+text \<open>
  The simplification procedure can be used to avoid simplification of terms of a certain form
-*}
+\<close>
 
 definition NO_MATCH :: "'a \<Rightarrow> 'b \<Rightarrow> bool" where "NO_MATCH pat val \<equiv> True"
 
 lemma NO_MATCH_cong[cong]: "NO_MATCH pat val = NO_MATCH pat val" by (rule refl)
 
 declare [[coercion_args NO_MATCH - -]]
 
-simproc_setup NO_MATCH ("NO_MATCH pat val") = {* fn _ => fn ctxt => fn ct =>
+simproc_setup NO_MATCH ("NO_MATCH pat val") = \<open>fn _ => fn ctxt => fn ct =>
   let
     val thy = Proof_Context.theory_of ctxt
     val dest_binop = Term.dest_comb #> apfst (Term.dest_comb #> snd)
     val m = Pattern.matches thy (dest_binop (Thm.term_of ct))
   in if m then NONE else SOME @{thm NO_MATCH_def} end
-*}
-
-text {*
+\<close>
+
+text \<open>
   This setup ensures that a rewrite rule of the form @{term "NO_MATCH pat val \<Longrightarrow> t"}
   is only applied, if the pattern @{term pat} does not match the value @{term val}.
-*}
-
-
-subsection {* Code generator setup *}
-
-subsubsection {* Generic code generator preprocessor setup *}
+\<close>
+
+
+subsection \<open>Code generator setup\<close>
+
+subsubsection \<open>Generic code generator preprocessor setup\<close>
 
 lemma conj_left_cong:
   "P \<longleftrightarrow> Q \<Longrightarrow> P \<and> R \<longleftrightarrow> Q \<and> R"
   by (fact arg_cong)
 
 lemma disj_left_cong:
   "P \<longleftrightarrow> Q \<Longrightarrow> P \<or> R \<longleftrightarrow> Q \<or> R"
   by (fact arg_cong)
 
-setup {*
+setup \<open>
   Code_Preproc.map_pre (put_simpset HOL_basic_ss) #>
   Code_Preproc.map_post (put_simpset HOL_basic_ss) #>
   Code_Simp.map_ss (put_simpset HOL_basic_ss #>
   Simplifier.add_cong @{thm conj_left_cong} #>
   Simplifier.add_cong @{thm disj_left_cong})
-*}
-
-
-subsubsection {* Equality *}
+\<close>
+
+
+subsubsection \<open>Equality\<close>
 
 class equal =
   fixes equal :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   assumes equal_eq: "equal x y \<longleftrightarrow> x = y"
 begin

 end
 
 declare eq_equal [symmetric, code_post]
 declare eq_equal [code]
 
-setup {*
+setup \<open>
   Code_Preproc.map_pre (fn ctxt =>
     ctxt addsimprocs [Simplifier.simproc_global_i @{theory} "equal" [@{term HOL.eq}]
       (fn _ => fn Const (_, Type ("fun", [Type _, _])) => SOME @{thm eq_equal} | _ => NONE)])
-*}
-
-
-subsubsection {* Generic code generator foundation *}
-
-text {* Datatype @{typ bool} *}
+\<close>
+
+
+subsubsection \<open>Generic code generator foundation\<close>
+
+text \<open>Datatype @{typ bool}\<close>
 
 code_datatype True False
 
 lemma [code]:
   shows "False \<and> P \<longleftrightarrow> False"

   shows "(False \<longrightarrow> P) \<longleftrightarrow> True"
     and "(True \<longrightarrow> P) \<longleftrightarrow> P"
     and "(P \<longrightarrow> False) \<longleftrightarrow> \<not> P"
     and "(P \<longrightarrow> True) \<longleftrightarrow> True" by simp_all
 
-text {* More about @{typ prop} *}
+text \<open>More about @{typ prop}\<close>
 
 lemma [code nbe]:
   shows "(True \<Longrightarrow> PROP Q) \<equiv> PROP Q"
     and "(PROP Q \<Longrightarrow> True) \<equiv> Trueprop True"
     and "(P \<Longrightarrow> R) \<equiv> Trueprop (P \<longrightarrow> R)" by (auto intro!: equal_intr_rule)

   "Trueprop True \<equiv> Code_Generator.holds"
   by (auto intro!: equal_intr_rule holds)
 
 declare Trueprop_code [symmetric, code_post]
 
-text {* Equality *}
+text \<open>Equality\<close>
 
 declare simp_thms(6) [code nbe]
 
 instantiation itself :: (type) equal
 begin

 
 lemma equal_itself_code [code]:
   "equal TYPE('a) TYPE('a) \<longleftrightarrow> True"
   by (simp add: equal)
 
-setup {* Sign.add_const_constraint (@{const_name equal}, SOME @{typ "'a\<Colon>type \<Rightarrow> 'a \<Rightarrow> bool"}) *}
+setup \<open>Sign.add_const_constraint (@{const_name equal}, SOME @{typ "'a\<Colon>type \<Rightarrow> 'a \<Rightarrow> bool"})\<close>
 
 lemma equal_alias_cert: "OFCLASS('a, equal_class) \<equiv> ((op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool) \<equiv> equal)" (is "?ofclass \<equiv> ?equal")
 proof
   assume "PROP ?ofclass"
   show "PROP ?equal"
-    by (tactic {* ALLGOALS (resolve_tac @{context} [Thm.unconstrainT @{thm eq_equal}]) *})
-      (fact `PROP ?ofclass`)
+    by (tactic \<open>ALLGOALS (resolve_tac @{context} [Thm.unconstrainT @{thm eq_equal}])\<close>)
+      (fact \<open>PROP ?ofclass\<close>)
 next
   assume "PROP ?equal"
   show "PROP ?ofclass" proof
-  qed (simp add: `PROP ?equal`)
+  qed (simp add: \<open>PROP ?equal\<close>)
 qed
 
-setup {* Sign.add_const_constraint (@{const_name equal}, SOME @{typ "'a\<Colon>equal \<Rightarrow> 'a \<Rightarrow> bool"}) *}
-
-setup {* Nbe.add_const_alias @{thm equal_alias_cert} *}
-
-text {* Cases *}
+setup \<open>Sign.add_const_constraint (@{const_name equal}, SOME @{typ "'a\<Colon>equal \<Rightarrow> 'a \<Rightarrow> bool"})\<close>
+
+setup \<open>Nbe.add_const_alias @{thm equal_alias_cert}\<close>
+
+text \<open>Cases\<close>
 
 lemma Let_case_cert:
   assumes "CASE \<equiv> (\<lambda>x. Let x f)"
   shows "CASE x \<equiv> f x"
   using assms by simp_all
 
-setup {*
+setup \<open>
   Code.add_case @{thm Let_case_cert} #>
   Code.add_undefined @{const_name undefined}
-*}
+\<close>
 
 declare [[code abort: undefined]]
 
 
-subsubsection {* Generic code generator target languages *}
-
-text {* type @{typ bool} *}
+subsubsection \<open>Generic code generator target languages\<close>
+
+text \<open>type @{typ bool}\<close>
 
 code_printing
   type_constructor bool \<rightharpoonup>
     (SML) "bool" and (OCaml) "bool" and (Haskell) "Bool" and (Scala) "Boolean"
 | constant True \<rightharpoonup>

 
 code_identifier
   code_module Pure \<rightharpoonup>
     (SML) HOL and (OCaml) HOL and (Haskell) HOL and (Scala) HOL
 
-text {* using built-in Haskell equality *}
+text \<open>using built-in Haskell equality\<close>
 
 code_printing
   type_class equal \<rightharpoonup> (Haskell) "Eq"
 | constant HOL.equal \<rightharpoonup> (Haskell) infix 4 "=="
 | constant HOL.eq \<rightharpoonup> (Haskell) infix 4 "=="
 
-text {* undefined *}
+text \<open>undefined\<close>
 
 code_printing
   constant undefined \<rightharpoonup>
     (SML) "!(raise/ Fail/ \"undefined\")"
     and (OCaml) "failwith/ \"undefined\""
     and (Haskell) "error/ \"undefined\""
     and (Scala) "!sys.error(\"undefined\")"
 
 
-subsubsection {* Evaluation and normalization by evaluation *}
-
-method_setup eval = {*
+subsubsection \<open>Evaluation and normalization by evaluation\<close>
+
+method_setup eval = \<open>
   let
     fun eval_tac ctxt =
       let val conv = Code_Runtime.dynamic_holds_conv ctxt
       in
         CONVERSION (Conv.params_conv ~1 (K (Conv.concl_conv ~1 conv)) ctxt) THEN'
         resolve_tac ctxt [TrueI]
       end
   in
     Scan.succeed (SIMPLE_METHOD' o eval_tac)
   end
-*} "solve goal by evaluation"
-
-method_setup normalization = {*
+\<close> "solve goal by evaluation"
+
+method_setup normalization = \<open>
   Scan.succeed (fn ctxt =>
     SIMPLE_METHOD'
       (CHANGED_PROP o
         (CONVERSION (Nbe.dynamic_conv ctxt)
           THEN_ALL_NEW (TRY o resolve_tac ctxt [TrueI]))))
-*} "solve goal by normalization"
-
-
-subsection {* Counterexample Search Units *}
-
-subsubsection {* Quickcheck *}
+\<close> "solve goal by normalization"
+
+
+subsection \<open>Counterexample Search Units\<close>
+
+subsubsection \<open>Quickcheck\<close>
 
 quickcheck_params [size = 5, iterations = 50]
 
 
-subsubsection {* Nitpick setup *}
+subsubsection \<open>Nitpick setup\<close>
 
 named_theorems nitpick_unfold "alternative definitions of constants as needed by Nitpick"
   and nitpick_simp "equational specification of constants as needed by Nitpick"
   and nitpick_psimp "partial equational specification of constants as needed by Nitpick"
   and nitpick_choice_spec "choice specification of constants as needed by Nitpick"
 
 declare if_bool_eq_conj [nitpick_unfold, no_atp]
         if_bool_eq_disj [no_atp]
 
 
-subsection {* Preprocessing for the predicate compiler *}
+subsection \<open>Preprocessing for the predicate compiler\<close>
 
 named_theorems code_pred_def "alternative definitions of constants for the Predicate Compiler"
   and code_pred_inline "inlining definitions for the Predicate Compiler"
   and code_pred_simp "simplification rules for the optimisations in the Predicate Compiler"
 
 
-subsection {* Legacy tactics and ML bindings *}
-
-ML {*
+subsection \<open>Legacy tactics and ML bindings\<close>
+
+ML \<open>
   (* combination of (spec RS spec RS ...(j times) ... spec RS mp) *)
   local
     fun wrong_prem (Const (@{const_name All}, _) $ Abs (_, _, t)) = wrong_prem t
       | wrong_prem (Bound _) = true
       | wrong_prem _ = false;

     val nnf_ss =
       simpset_of (put_simpset HOL_basic_ss @{context} addsimps @{thms simp_thms nnf_simps});
   in
     fun nnf_conv ctxt = Simplifier.rewrite (put_simpset nnf_ss ctxt);
   end
-*}
+\<close>
 
 hide_const (open) eq equal
 
 end