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.48
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.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 *}