src/HOL/Nat.thy
changeset 61799 4cf66f21b764
parent 61649 268d88ec9087
child 62217 527488dc8b90
     1.1 --- a/src/HOL/Nat.thy	Mon Dec 07 10:23:50 2015 +0100
     1.2 +++ b/src/HOL/Nat.thy	Mon Dec 07 10:38:04 2015 +0100
     1.3 @@ -18,12 +18,12 @@
     1.4  ML_file "~~/src/Provers/Arith/fast_lin_arith.ML"
     1.5  
     1.6  
     1.7 -subsection \<open>Type @{text ind}\<close>
     1.8 +subsection \<open>Type \<open>ind\<close>\<close>
     1.9  
    1.10  typedecl ind
    1.11  
    1.12  axiomatization Zero_Rep :: ind and Suc_Rep :: "ind => ind" where
    1.13 -  -- \<open>the axiom of infinity in 2 parts\<close>
    1.14 +  \<comment> \<open>the axiom of infinity in 2 parts\<close>
    1.15    Suc_Rep_inject:       "Suc_Rep x = Suc_Rep y ==> x = y" and
    1.16    Suc_Rep_not_Zero_Rep: "Suc_Rep x \<noteq> Zero_Rep"
    1.17  
    1.18 @@ -79,7 +79,7 @@
    1.19    shows "P n"
    1.20  using assms
    1.21  apply (unfold Zero_nat_def Suc_def)
    1.22 -apply (rule Rep_Nat_inverse [THEN subst]) -- \<open>types force good instantiation\<close>
    1.23 +apply (rule Rep_Nat_inverse [THEN subst]) \<comment> \<open>types force good instantiation\<close>
    1.24  apply (erule Nat_Rep_Nat [THEN Nat.induct])
    1.25  apply (iprover elim: Nat_Abs_Nat_inverse [THEN subst])
    1.26  done
    1.27 @@ -96,7 +96,7 @@
    1.28    apply (simp only: Suc_not_Zero)
    1.29    done
    1.30  
    1.31 --- \<open>Avoid name clashes by prefixing the output of @{text old_rep_datatype} with @{text old}.\<close>
    1.32 +\<comment> \<open>Avoid name clashes by prefixing the output of \<open>old_rep_datatype\<close> with \<open>old\<close>.\<close>
    1.33  setup \<open>Sign.mandatory_path "old"\<close>
    1.34  
    1.35  old_rep_datatype "0 :: nat" Suc
    1.36 @@ -107,7 +107,7 @@
    1.37  
    1.38  setup \<open>Sign.parent_path\<close>
    1.39  
    1.40 --- \<open>But erase the prefix for properties that are not generated by @{text free_constructors}.\<close>
    1.41 +\<comment> \<open>But erase the prefix for properties that are not generated by \<open>free_constructors\<close>.\<close>
    1.42  setup \<open>Sign.mandatory_path "nat"\<close>
    1.43  
    1.44  declare
    1.45 @@ -126,7 +126,7 @@
    1.46  
    1.47  declare nat.sel[code del]
    1.48  
    1.49 -hide_const (open) Nat.pred -- \<open>hide everything related to the selector\<close>
    1.50 +hide_const (open) Nat.pred \<comment> \<open>hide everything related to the selector\<close>
    1.51  hide_fact
    1.52    nat.case_eq_if
    1.53    nat.collapse
    1.54 @@ -137,12 +137,12 @@
    1.55    nat.split_sel_asm
    1.56  
    1.57  lemma nat_exhaust [case_names 0 Suc, cases type: nat]:
    1.58 -  -- \<open>for backward compatibility -- names of variables differ\<close>
    1.59 +  \<comment> \<open>for backward compatibility -- names of variables differ\<close>
    1.60    "(y = 0 \<Longrightarrow> P) \<Longrightarrow> (\<And>nat. y = Suc nat \<Longrightarrow> P) \<Longrightarrow> P"
    1.61  by (rule old.nat.exhaust)
    1.62  
    1.63  lemma nat_induct [case_names 0 Suc, induct type: nat]:
    1.64 -  -- \<open>for backward compatibility -- names of variables differ\<close>
    1.65 +  \<comment> \<open>for backward compatibility -- names of variables differ\<close>
    1.66    fixes n
    1.67    assumes "P 0" and "\<And>n. P n \<Longrightarrow> P (Suc n)"
    1.68    shows "P n"
    1.69 @@ -313,7 +313,7 @@
    1.70    shows "m + k = n + k \<longleftrightarrow> m = n"
    1.71    by (fact add_right_cancel)
    1.72  
    1.73 -text \<open>Reasoning about @{text "m + 0 = 0"}, etc.\<close>
    1.74 +text \<open>Reasoning about \<open>m + 0 = 0\<close>, etc.\<close>
    1.75  
    1.76  lemma add_is_0 [iff]:
    1.77    fixes m n :: nat
    1.78 @@ -630,7 +630,7 @@
    1.79    apply (blast dest: Suc_lessD)
    1.80    done
    1.81  
    1.82 -text \<open>Can be used with @{text less_Suc_eq} to get @{term "n = m | n < m"}\<close>
    1.83 +text \<open>Can be used with \<open>less_Suc_eq\<close> to get @{term "n = m | n < m"}\<close>
    1.84  lemma not_less_eq: "\<not> m < n \<longleftrightarrow> n < Suc m"
    1.85    unfolding not_less less_Suc_eq_le ..
    1.86  
    1.87 @@ -654,14 +654,14 @@
    1.88  lemma Suc_leI: "m < n ==> Suc(m) \<le> n"
    1.89    unfolding Suc_le_eq .
    1.90  
    1.91 -text \<open>Stronger version of @{text Suc_leD}\<close>
    1.92 +text \<open>Stronger version of \<open>Suc_leD\<close>\<close>
    1.93  lemma Suc_le_lessD: "Suc m \<le> n ==> m < n"
    1.94    unfolding Suc_le_eq .
    1.95  
    1.96  lemma less_imp_le_nat: "m < n ==> m \<le> (n::nat)"
    1.97    unfolding less_eq_Suc_le by (rule Suc_leD)
    1.98  
    1.99 -text \<open>For instance, @{text "(Suc m < Suc n) = (Suc m \<le> n) = (m < n)"}\<close>
   1.100 +text \<open>For instance, \<open>(Suc m < Suc n) = (Suc m \<le> n) = (m < n)\<close>\<close>
   1.101  lemmas le_simps = less_imp_le_nat less_Suc_eq_le Suc_le_eq
   1.102  
   1.103  
   1.104 @@ -673,7 +673,7 @@
   1.105  lemma le_eq_less_or_eq: "(m \<le> (n::nat)) = (m < n | m=n)"
   1.106    by (rule le_less)
   1.107  
   1.108 -text \<open>Useful with @{text blast}.\<close>
   1.109 +text \<open>Useful with \<open>blast\<close>.\<close>
   1.110  lemma eq_imp_le: "(m::nat) = n ==> m \<le> n"
   1.111    by auto
   1.112  
   1.113 @@ -717,7 +717,7 @@
   1.114  lemma neq0_conv[iff]: fixes n :: nat shows "(n \<noteq> 0) = (0 < n)"
   1.115  by (cases n) simp_all
   1.116  
   1.117 -text \<open>This theorem is useful with @{text blast}\<close>
   1.118 +text \<open>This theorem is useful with \<open>blast\<close>\<close>
   1.119  lemma gr0I: "((n::nat) = 0 ==> False) ==> 0 < n"
   1.120  by (rule neq0_conv[THEN iffD1], iprover)
   1.121  
   1.122 @@ -762,7 +762,7 @@
   1.123    apply (induct j, simp_all)
   1.124    done
   1.125  
   1.126 -text \<open>Deleted @{text less_natE}; use @{text "less_imp_Suc_add RS exE"}\<close>
   1.127 +text \<open>Deleted \<open>less_natE\<close>; use \<open>less_imp_Suc_add RS exE\<close>\<close>
   1.128  lemma less_imp_Suc_add: "m < n ==> (\<exists>k. n = Suc (m + k))"
   1.129    apply (induct n)
   1.130    apply (simp_all add: order_le_less)
   1.131 @@ -773,7 +773,7 @@
   1.132  lemma le_Suc_ex: "(k::nat) \<le> l \<Longrightarrow> (\<exists>n. l = k + n)"
   1.133    by (auto simp: less_Suc_eq_le[symmetric] dest: less_imp_Suc_add)
   1.134  
   1.135 -text \<open>strict, in 1st argument; proof is by induction on @{text "k > 0"}\<close>
   1.136 +text \<open>strict, in 1st argument; proof is by induction on \<open>k > 0\<close>\<close>
   1.137  lemma mult_less_mono2: "(i::nat) < j ==> 0<k ==> k * i < k * j"
   1.138  apply(auto simp: gr0_conv_Suc)
   1.139  apply (induct_tac m)
   1.140 @@ -786,7 +786,7 @@
   1.141  by (induct m n rule: diff_induct) simp_all
   1.142  
   1.143  
   1.144 -text\<open>The naturals form an ordered @{text semidom}\<close>
   1.145 +text\<open>The naturals form an ordered \<open>semidom\<close>\<close>
   1.146  instance nat :: linordered_semidom
   1.147  proof
   1.148    show "0 < (1::nat)" by simp
   1.149 @@ -1015,9 +1015,9 @@
   1.150    obtain n where "n = V x" by auto
   1.151    moreover have "\<And>x. V x = n \<Longrightarrow> P x"
   1.152    proof (induct n rule: infinite_descent0)
   1.153 -    case 0 -- "i.e. $V(x) = 0$"
   1.154 +    case 0 \<comment> "i.e. $V(x) = 0$"
   1.155      with A0 show "P x" by auto
   1.156 -  next -- "now $n>0$ and $P(x)$ does not hold for some $x$ with $V(x)=n$"
   1.157 +  next \<comment> "now $n>0$ and $P(x)$ does not hold for some $x$ with $V(x)=n$"
   1.158      case (smaller n)
   1.159      then obtain x where vxn: "V x = n " and "V x > 0 \<and> \<not> P x" by auto
   1.160      with A1 obtain y where "V y < V x \<and> \<not> P y" by auto
   1.161 @@ -1040,8 +1040,8 @@
   1.162    ultimately show "P x" by auto
   1.163  qed
   1.164  
   1.165 -text \<open>A [clumsy] way of lifting @{text "<"}
   1.166 -  monotonicity to @{text "\<le>"} monotonicity\<close>
   1.167 +text \<open>A [clumsy] way of lifting \<open><\<close>
   1.168 +  monotonicity to \<open>\<le>\<close> monotonicity\<close>
   1.169  lemma less_mono_imp_le_mono:
   1.170    "\<lbrakk> !!i j::nat. i < j \<Longrightarrow> f i < f j; i \<le> j \<rbrakk> \<Longrightarrow> f i \<le> ((f j)::nat)"
   1.171  by (simp add: order_le_less) (blast)
   1.172 @@ -1109,7 +1109,7 @@
   1.173  lemma add_leE: "(m::nat) + k \<le> n ==> (m \<le> n ==> k \<le> n ==> R) ==> R"
   1.174  by (blast dest: add_leD1 add_leD2)
   1.175  
   1.176 -text \<open>needs @{text "!!k"} for @{text ac_simps} to work\<close>
   1.177 +text \<open>needs \<open>!!k\<close> for \<open>ac_simps\<close> to work\<close>
   1.178  lemma less_add_eq_less: "!!k::nat. k < l ==> m + l = k + n ==> m < n"
   1.179  by (force simp del: add_Suc_right
   1.180      simp add: less_iff_Suc_add add_Suc_right [symmetric] ac_simps)
   1.181 @@ -1177,14 +1177,14 @@
   1.182  
   1.183  lemma nat_diff_split:
   1.184    "P(a - b::nat) = ((a<b --> P 0) & (ALL d. a = b + d --> P d))"
   1.185 -    -- \<open>elimination of @{text -} on @{text nat}\<close>
   1.186 +    \<comment> \<open>elimination of \<open>-\<close> on \<open>nat\<close>\<close>
   1.187  by (cases "a < b")
   1.188    (auto simp add: diff_is_0_eq [THEN iffD2] diff_add_inverse
   1.189      not_less le_less dest!: add_eq_self_zero add_eq_self_zero[OF sym])
   1.190  
   1.191  lemma nat_diff_split_asm:
   1.192    "P(a - b::nat) = (~ (a < b & ~ P 0 | (EX d. a = b + d & ~ P d)))"
   1.193 -    -- \<open>elimination of @{text -} on @{text nat} in assumptions\<close>
   1.194 +    \<comment> \<open>elimination of \<open>-\<close> on \<open>nat\<close> in assumptions\<close>
   1.195  by (auto split: nat_diff_split)
   1.196  
   1.197  lemma Suc_pred': "0 < n ==> n = Suc(n - 1)"
   1.198 @@ -1214,14 +1214,14 @@
   1.199  lemma mult_le_mono2: "i \<le> (j::nat) ==> k * i \<le> k * j"
   1.200  by (simp add: mult_left_mono)
   1.201  
   1.202 -text \<open>@{text "\<le>"} monotonicity, BOTH arguments\<close>
   1.203 +text \<open>\<open>\<le>\<close> monotonicity, BOTH arguments\<close>
   1.204  lemma mult_le_mono: "i \<le> (j::nat) ==> k \<le> l ==> i * k \<le> j * l"
   1.205  by (simp add: mult_mono)
   1.206  
   1.207  lemma mult_less_mono1: "(i::nat) < j ==> 0 < k ==> i * k < j * k"
   1.208  by (simp add: mult_strict_right_mono)
   1.209  
   1.210 -text\<open>Differs from the standard @{text zero_less_mult_iff} in that
   1.211 +text\<open>Differs from the standard \<open>zero_less_mult_iff\<close> in that
   1.212        there are no negative numbers.\<close>
   1.213  lemma nat_0_less_mult_iff [simp]: "(0 < (m::nat) * n) = (0 < m & 0 < n)"
   1.214    apply (induct m)
   1.215 @@ -1265,7 +1265,7 @@
   1.216  lemma le_cube: "(m::nat) \<le> m * (m * m)"
   1.217    by (cases m) (auto intro: le_add1)
   1.218  
   1.219 -text \<open>Lemma for @{text gcd}\<close>
   1.220 +text \<open>Lemma for \<open>gcd\<close>\<close>
   1.221  lemma mult_eq_self_implies_10: "(m::nat) = m * n ==> n = 1 | m = 0"
   1.222    apply (drule sym)
   1.223    apply (rule disjCI)
   1.224 @@ -1317,7 +1317,7 @@
   1.225  notation (latex output)
   1.226    compower ("(_\<^bsup>_\<^esup>)" [1000] 1000)
   1.227  
   1.228 -text \<open>@{text "f ^^ n = f o ... o f"}, the n-fold composition of @{text f}\<close>
   1.229 +text \<open>\<open>f ^^ n = f o ... o f\<close>, the n-fold composition of \<open>f\<close>\<close>
   1.230  
   1.231  overloading
   1.232    funpow == "compow :: nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a)"
   1.233 @@ -1450,7 +1450,7 @@
   1.234      by (intro gfp_upperbound) (simp del: funpow.simps)
   1.235  qed
   1.236  
   1.237 -subsection \<open>Embedding of the naturals into any @{text semiring_1}: @{term of_nat}\<close>
   1.238 +subsection \<open>Embedding of the naturals into any \<open>semiring_1\<close>: @{term of_nat}\<close>
   1.239  
   1.240  context semiring_1
   1.241  begin
   1.242 @@ -1477,7 +1477,7 @@
   1.243  
   1.244  primrec of_nat_aux :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" where
   1.245    "of_nat_aux inc 0 i = i"
   1.246 -| "of_nat_aux inc (Suc n) i = of_nat_aux inc n (inc i)" -- \<open>tail recursive\<close>
   1.247 +| "of_nat_aux inc (Suc n) i = of_nat_aux inc n (inc i)" \<comment> \<open>tail recursive\<close>
   1.248  
   1.249  lemma of_nat_code:
   1.250    "of_nat n = of_nat_aux (\<lambda>i. i + 1) n 0"
   1.251 @@ -1545,7 +1545,7 @@
   1.252  lemma of_nat_less_imp_less: "of_nat m < of_nat n \<Longrightarrow> m < n"
   1.253    by simp
   1.254  
   1.255 -text\<open>Every @{text linordered_semidom} has characteristic zero.\<close>
   1.256 +text\<open>Every \<open>linordered_semidom\<close> has characteristic zero.\<close>
   1.257  
   1.258  subclass semiring_char_0 proof
   1.259  qed (auto intro!: injI simp add: eq_iff)
   1.260 @@ -1685,7 +1685,7 @@
   1.261    case True
   1.262    then show ?thesis
   1.263      by (induct n n' rule: less_Suc_induct [consumes 1]) (auto intro: mono)
   1.264 -qed (insert \<open>n \<le> n'\<close>, auto) -- \<open>trivial for @{prop "n = n'"}\<close>
   1.265 +qed (insert \<open>n \<le> n'\<close>, auto) \<comment> \<open>trivial for @{prop "n = n'"}\<close>
   1.266  
   1.267  lemma lift_Suc_antimono_le:
   1.268    assumes mono: "\<And>n. f n \<ge> f (Suc n)" and "n \<le> n'"
   1.269 @@ -1694,7 +1694,7 @@
   1.270    case True
   1.271    then show ?thesis
   1.272      by (induct n n' rule: less_Suc_induct [consumes 1]) (auto intro: mono)
   1.273 -qed (insert \<open>n \<le> n'\<close>, auto) -- \<open>trivial for @{prop "n = n'"}\<close>
   1.274 +qed (insert \<open>n \<le> n'\<close>, auto) \<comment> \<open>trivial for @{prop "n = n'"}\<close>
   1.275  
   1.276  lemma lift_Suc_mono_less:
   1.277    assumes mono: "\<And>n. f n < f (Suc n)" and "n < n'"
   1.278 @@ -1750,13 +1750,13 @@
   1.279  by arith
   1.280  
   1.281  lemma le_diff_conv2: "k \<le> j ==> (i \<le> j-k) = (i+k \<le> (j::nat))"
   1.282 -  by (fact le_diff_conv2) -- \<open>FIXME delete\<close>
   1.283 +  by (fact le_diff_conv2) \<comment> \<open>FIXME delete\<close>
   1.284  
   1.285  lemma diff_diff_cancel [simp]: "i \<le> (n::nat) ==> n - (n - i) = i"
   1.286  by arith
   1.287  
   1.288  lemma le_add_diff: "k \<le> (n::nat) ==> m \<le> n + m - k"
   1.289 -  by (fact le_add_diff) -- \<open>FIXME delete\<close>
   1.290 +  by (fact le_add_diff) \<comment> \<open>FIXME delete\<close>
   1.291  
   1.292  (*Replaces the previous diff_less and le_diff_less, which had the stronger
   1.293    second premise n\<le>m*)
   1.294 @@ -1829,8 +1829,7 @@
   1.295  lemmas add_diff_assoc2 = diff_add_assoc2[symmetric]
   1.296  declare diff_diff_left [simp]  add_diff_assoc [simp] add_diff_assoc2[simp]
   1.297  
   1.298 -text\<open>At present we prove no analogue of @{text not_less_Least} or @{text
   1.299 -Least_Suc}, since there appears to be no need.\<close>
   1.300 +text\<open>At present we prove no analogue of \<open>not_less_Least\<close> or \<open>Least_Suc\<close>, since there appears to be no need.\<close>
   1.301  
   1.302  text\<open>Lemmas for ex/Factorization\<close>
   1.303  
   1.304 @@ -2015,7 +2014,7 @@
   1.305  subsection \<open>Size of a datatype value\<close>
   1.306  
   1.307  class size =
   1.308 -  fixes size :: "'a \<Rightarrow> nat" -- \<open>see further theory @{text Wellfounded}\<close>
   1.309 +  fixes size :: "'a \<Rightarrow> nat" \<comment> \<open>see further theory \<open>Wellfounded\<close>\<close>
   1.310  
   1.311  instantiation nat :: size
   1.312  begin