src/HOL/Num.thy
changeset 61799 4cf66f21b764
parent 61630 608520e0e8e2
child 61944 5d06ecfdb472
     1.1 --- a/src/HOL/Num.thy	Mon Dec 07 10:23:50 2015 +0100
     1.2 +++ b/src/HOL/Num.thy	Mon Dec 07 10:38:04 2015 +0100
     1.3 @@ -9,7 +9,7 @@
     1.4  imports BNF_Least_Fixpoint
     1.5  begin
     1.6  
     1.7 -subsection \<open>The @{text num} type\<close>
     1.8 +subsection \<open>The \<open>num\<close> type\<close>
     1.9  
    1.10  datatype num = One | Bit0 num | Bit1 num
    1.11  
    1.12 @@ -83,8 +83,8 @@
    1.13  
    1.14  text \<open>
    1.15    From now on, there are two possible models for @{typ num}:
    1.16 -  as positive naturals (rule @{text "num_induct"})
    1.17 -  and as digit representation (rules @{text "num.induct"}, @{text "num.cases"}).
    1.18 +  as positive naturals (rule \<open>num_induct\<close>)
    1.19 +  and as digit representation (rules \<open>num.induct\<close>, \<open>num.cases\<close>).
    1.20  \<close>
    1.21  
    1.22  
    1.23 @@ -177,7 +177,7 @@
    1.24  lemma le_num_One_iff: "x \<le> num.One \<longleftrightarrow> x = num.One"
    1.25  by (simp add: antisym_conv)
    1.26  
    1.27 -text \<open>Rules using @{text One} and @{text inc} as constructors\<close>
    1.28 +text \<open>Rules using \<open>One\<close> and \<open>inc\<close> as constructors\<close>
    1.29  
    1.30  lemma add_One: "x + One = inc x"
    1.31    by (simp add: num_eq_iff nat_of_num_add nat_of_num_inc)
    1.32 @@ -237,7 +237,7 @@
    1.33  
    1.34  text \<open>
    1.35    We embed binary representations into a generic algebraic
    1.36 -  structure using @{text numeral}.
    1.37 +  structure using \<open>numeral\<close>.
    1.38  \<close>
    1.39  
    1.40  class numeral = one + semigroup_add
    1.41 @@ -327,7 +327,7 @@
    1.42    @{const numeral} is a morphism.
    1.43  \<close>
    1.44  
    1.45 -subsubsection \<open>Structures with addition: class @{text numeral}\<close>
    1.46 +subsubsection \<open>Structures with addition: class \<open>numeral\<close>\<close>
    1.47  
    1.48  context numeral
    1.49  begin
    1.50 @@ -354,7 +354,7 @@
    1.51  end
    1.52  
    1.53  subsubsection \<open>
    1.54 -  Structures with negation: class @{text neg_numeral}
    1.55 +  Structures with negation: class \<open>neg_numeral\<close>
    1.56  \<close>
    1.57  
    1.58  class neg_numeral = numeral + group_add
    1.59 @@ -492,7 +492,7 @@
    1.60  end
    1.61  
    1.62  subsubsection \<open>
    1.63 -  Structures with multiplication: class @{text semiring_numeral}
    1.64 +  Structures with multiplication: class \<open>semiring_numeral\<close>
    1.65  \<close>
    1.66  
    1.67  class semiring_numeral = semiring + monoid_mult
    1.68 @@ -518,7 +518,7 @@
    1.69  end
    1.70  
    1.71  subsubsection \<open>
    1.72 -  Structures with a zero: class @{text semiring_1}
    1.73 +  Structures with a zero: class \<open>semiring_1\<close>
    1.74  \<close>
    1.75  
    1.76  context semiring_1
    1.77 @@ -548,7 +548,7 @@
    1.78    by (simp_all add: Let_def)
    1.79  
    1.80  subsubsection \<open>
    1.81 -  Equality: class @{text semiring_char_0}
    1.82 +  Equality: class \<open>semiring_char_0\<close>
    1.83  \<close>
    1.84  
    1.85  context semiring_char_0
    1.86 @@ -581,7 +581,7 @@
    1.87  end
    1.88  
    1.89  subsubsection \<open>
    1.90 -  Comparisons: class @{text linordered_semidom}
    1.91 +  Comparisons: class \<open>linordered_semidom\<close>
    1.92  \<close>
    1.93  
    1.94  text \<open>Could be perhaps more general than here.\<close>
    1.95 @@ -672,7 +672,7 @@
    1.96  end
    1.97  
    1.98  subsubsection \<open>
    1.99 -  Multiplication and negation: class @{text ring_1}
   1.100 +  Multiplication and negation: class \<open>ring_1\<close>
   1.101  \<close>
   1.102  
   1.103  context ring_1
   1.104 @@ -696,7 +696,7 @@
   1.105  end
   1.106  
   1.107  subsubsection \<open>
   1.108 -  Equality using @{text iszero} for rings with non-zero characteristic
   1.109 +  Equality using \<open>iszero\<close> for rings with non-zero characteristic
   1.110  \<close>
   1.111  
   1.112  context ring_1
   1.113 @@ -728,16 +728,15 @@
   1.114  lemma eq_iff_iszero_diff: "x = y \<longleftrightarrow> iszero (x - y)"
   1.115    unfolding iszero_def by (rule eq_iff_diff_eq_0)
   1.116  
   1.117 -text \<open>The @{text "eq_numeral_iff_iszero"} lemmas are not declared
   1.118 -@{text "[simp]"} by default, because for rings of characteristic zero,
   1.119 -better simp rules are possible. For a type like integers mod @{text
   1.120 -"n"}, type-instantiated versions of these rules should be added to the
   1.121 +text \<open>The \<open>eq_numeral_iff_iszero\<close> lemmas are not declared
   1.122 +\<open>[simp]\<close> by default, because for rings of characteristic zero,
   1.123 +better simp rules are possible. For a type like integers mod \<open>n\<close>, type-instantiated versions of these rules should be added to the
   1.124  simplifier, along with a type-specific rule for deciding propositions
   1.125 -of the form @{text "iszero (numeral w)"}.
   1.126 +of the form \<open>iszero (numeral w)\<close>.
   1.127  
   1.128  bh: Maybe it would not be so bad to just declare these as simp
   1.129  rules anyway? I should test whether these rules take precedence over
   1.130 -the @{text "ring_char_0"} rules in the simplifier.
   1.131 +the \<open>ring_char_0\<close> rules in the simplifier.
   1.132  \<close>
   1.133  
   1.134  lemma eq_numeral_iff_iszero:
   1.135 @@ -759,7 +758,7 @@
   1.136  end
   1.137  
   1.138  subsubsection \<open>
   1.139 -  Equality and negation: class @{text ring_char_0}
   1.140 +  Equality and negation: class \<open>ring_char_0\<close>
   1.141  \<close>
   1.142  
   1.143  class ring_char_0 = ring_1 + semiring_char_0
   1.144 @@ -835,7 +834,7 @@
   1.145  end
   1.146  
   1.147  subsubsection \<open>
   1.148 -  Structures with negation and order: class @{text linordered_idom}
   1.149 +  Structures with negation and order: class \<open>linordered_idom\<close>
   1.150  \<close>
   1.151  
   1.152  context linordered_idom
   1.153 @@ -1179,7 +1178,7 @@
   1.154  
   1.155  text \<open>
   1.156    For making a minimal simpset, one must include these default simprules.
   1.157 -  Also include @{text simp_thms}.
   1.158 +  Also include \<open>simp_thms\<close>.
   1.159  \<close>
   1.160  
   1.161  lemmas arith_simps =
   1.162 @@ -1209,11 +1208,11 @@
   1.163    eq_numeral_simps eq_neg_numeral_simps eq_numeral_extra
   1.164  
   1.165  lemma Let_numeral [simp]: "Let (numeral v) f = f (numeral v)"
   1.166 -  -- \<open>Unfold all @{text let}s involving constants\<close>
   1.167 +  \<comment> \<open>Unfold all \<open>let\<close>s involving constants\<close>
   1.168    unfolding Let_def ..
   1.169  
   1.170  lemma Let_neg_numeral [simp]: "Let (- numeral v) f = f (- numeral v)"
   1.171 -  -- \<open>Unfold all @{text let}s involving constants\<close>
   1.172 +  \<comment> \<open>Unfold all \<open>let\<close>s involving constants\<close>
   1.173    unfolding Let_def ..
   1.174  
   1.175  declaration \<open>