src/HOL/Library/Extended_Nat.thy
changeset 60500 903bb1495239
parent 59582 0fbed69ff081
child 60636 ee18efe9b246
     1.1 --- a/src/HOL/Library/Extended_Nat.thy	Wed Jun 17 10:57:11 2015 +0200
     1.2 +++ b/src/HOL/Library/Extended_Nat.thy	Wed Jun 17 11:03:05 2015 +0200
     1.3 @@ -3,7 +3,7 @@
     1.4      Contributions: David Trachtenherz, TU Muenchen
     1.5  *)
     1.6  
     1.7 -section {* Extended natural numbers (i.e. with infinity) *}
     1.8 +section \<open>Extended natural numbers (i.e. with infinity)\<close>
     1.9  
    1.10  theory Extended_Nat
    1.11  imports Main Countable
    1.12 @@ -18,16 +18,16 @@
    1.13  notation (HTML output)
    1.14    infinity  ("\<infinity>")
    1.15  
    1.16 -subsection {* Type definition *}
    1.17 +subsection \<open>Type definition\<close>
    1.18  
    1.19 -text {*
    1.20 +text \<open>
    1.21    We extend the standard natural numbers by a special value indicating
    1.22    infinity.
    1.23 -*}
    1.24 +\<close>
    1.25  
    1.26  typedef enat = "UNIV :: nat option set" ..
    1.27  
    1.28 -text {* TODO: introduce enat as coinductive datatype, enat is just @{const of_nat} *}
    1.29 +text \<open>TODO: introduce enat as coinductive datatype, enat is just @{const of_nat}\<close>
    1.30  
    1.31  definition enat :: "nat \<Rightarrow> enat" where
    1.32    "enat n = Abs_enat (Some n)"
    1.33 @@ -70,7 +70,7 @@
    1.34    where "the_enat (enat n) = n"
    1.35  
    1.36  
    1.37 -subsection {* Constructors and numbers *}
    1.38 +subsection \<open>Constructors and numbers\<close>
    1.39  
    1.40  instantiation enat :: "{zero, one}"
    1.41  begin
    1.42 @@ -141,7 +141,7 @@
    1.43  lemma enat_eSuc_iff: "enat y = eSuc x \<longleftrightarrow> (\<exists>n. y = Suc n \<and> enat n = x)"
    1.44    by (cases y) (auto simp: enat_0 eSuc_enat[symmetric])
    1.45  
    1.46 -subsection {* Addition *}
    1.47 +subsection \<open>Addition\<close>
    1.48  
    1.49  instantiation enat :: comm_monoid_add
    1.50  begin
    1.51 @@ -186,7 +186,7 @@
    1.52  lemma iadd_is_0: "(m + n = (0::enat)) = (m = 0 \<and> n = 0)"
    1.53    by (cases m, cases n, simp_all add: zero_enat_def)
    1.54  
    1.55 -subsection {* Multiplication *}
    1.56 +subsection \<open>Multiplication\<close>
    1.57  
    1.58  instantiation enat :: comm_semiring_1
    1.59  begin
    1.60 @@ -254,7 +254,7 @@
    1.61    by (auto simp add: times_enat_def zero_enat_def split: enat.split)
    1.62  
    1.63  
    1.64 -subsection {* Numerals *}
    1.65 +subsection \<open>Numerals\<close>
    1.66  
    1.67  lemma numeral_eq_enat:
    1.68    "numeral k = enat (numeral k)"
    1.69 @@ -273,7 +273,7 @@
    1.70  lemma eSuc_numeral [simp]: "eSuc (numeral k) = numeral (k + Num.One)"
    1.71    by (simp only: eSuc_plus_1 numeral_plus_one)
    1.72  
    1.73 -subsection {* Subtraction *}
    1.74 +subsection \<open>Subtraction\<close>
    1.75  
    1.76  instantiation enat :: minus
    1.77  begin
    1.78 @@ -316,7 +316,7 @@
    1.79  
    1.80  (*lemmas idiff_self_eq_0_enat = idiff_self_eq_0[unfolded zero_enat_def]*)
    1.81  
    1.82 -subsection {* Ordering *}
    1.83 +subsection \<open>Ordering\<close>
    1.84  
    1.85  instantiation enat :: linordered_ab_semigroup_add
    1.86  begin
    1.87 @@ -499,7 +499,7 @@
    1.88  qed
    1.89  
    1.90  
    1.91 -subsection {* Cancellation simprocs *}
    1.92 +subsection \<open>Cancellation simprocs\<close>
    1.93  
    1.94  lemma enat_add_left_cancel: "a + b = a + c \<longleftrightarrow> a = (\<infinity>::enat) \<or> b = c"
    1.95    unfolding plus_enat_def by (simp split: enat.split)
    1.96 @@ -510,7 +510,7 @@
    1.97  lemma enat_add_left_cancel_less: "a + b < a + c \<longleftrightarrow> a \<noteq> (\<infinity>::enat) \<and> b < c"
    1.98    unfolding plus_enat_def by (simp split: enat.split)
    1.99  
   1.100 -ML {*
   1.101 +ML \<open>
   1.102  structure Cancel_Enat_Common =
   1.103  struct
   1.104    (* copied from src/HOL/Tools/nat_numeral_simprocs.ML *)
   1.105 @@ -557,25 +557,25 @@
   1.106    val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} @{typ enat}
   1.107    fun simp_conv _ _ = SOME @{thm enat_add_left_cancel_less}
   1.108  )
   1.109 -*}
   1.110 +\<close>
   1.111  
   1.112  simproc_setup enat_eq_cancel
   1.113    ("(l::enat) + m = n" | "(l::enat) = m + n") =
   1.114 -  {* fn phi => fn ctxt => fn ct => Eq_Enat_Cancel.proc ctxt (Thm.term_of ct) *}
   1.115 +  \<open>fn phi => fn ctxt => fn ct => Eq_Enat_Cancel.proc ctxt (Thm.term_of ct)\<close>
   1.116  
   1.117  simproc_setup enat_le_cancel
   1.118    ("(l::enat) + m \<le> n" | "(l::enat) \<le> m + n") =
   1.119 -  {* fn phi => fn ctxt => fn ct => Le_Enat_Cancel.proc ctxt (Thm.term_of ct) *}
   1.120 +  \<open>fn phi => fn ctxt => fn ct => Le_Enat_Cancel.proc ctxt (Thm.term_of ct)\<close>
   1.121  
   1.122  simproc_setup enat_less_cancel
   1.123    ("(l::enat) + m < n" | "(l::enat) < m + n") =
   1.124 -  {* fn phi => fn ctxt => fn ct => Less_Enat_Cancel.proc ctxt (Thm.term_of ct) *}
   1.125 +  \<open>fn phi => fn ctxt => fn ct => Less_Enat_Cancel.proc ctxt (Thm.term_of ct)\<close>
   1.126  
   1.127 -text {* TODO: add regression tests for these simprocs *}
   1.128 +text \<open>TODO: add regression tests for these simprocs\<close>
   1.129  
   1.130 -text {* TODO: add simprocs for combining and cancelling numerals *}
   1.131 +text \<open>TODO: add simprocs for combining and cancelling numerals\<close>
   1.132  
   1.133 -subsection {* Well-ordering *}
   1.134 +subsection \<open>Well-ordering\<close>
   1.135  
   1.136  lemma less_enatE:
   1.137    "[| n < enat m; !!k. n = enat k ==> k < m ==> P |] ==> P"
   1.138 @@ -613,7 +613,7 @@
   1.139    show "P n" by (blast intro: enat_less_induct hyp)
   1.140  qed
   1.141  
   1.142 -subsection {* Complete Lattice *}
   1.143 +subsection \<open>Complete Lattice\<close>
   1.144  
   1.145  instantiation enat :: complete_lattice
   1.146  begin
   1.147 @@ -647,7 +647,7 @@
   1.148  
   1.149  instance enat :: complete_linorder ..
   1.150  
   1.151 -subsection {* Traditional theorem names *}
   1.152 +subsection \<open>Traditional theorem names\<close>
   1.153  
   1.154  lemmas enat_defs = zero_enat_def one_enat_def eSuc_def
   1.155    plus_enat_def less_eq_enat_def less_enat_def