prefer formal comments;
authorwenzelm
Fri Jan 12 15:27:46 2018 +0100 (19 months ago)
changeset 674084a4c14b24800
parent 67407 dbaa38bd223a
child 67409 060efe532189
prefer formal comments;
src/HOL/Library/Bourbaki_Witt_Fixpoint.thy
src/HOL/Library/DAList_Multiset.thy
src/HOL/Library/Extended_Nonnegative_Real.thy
src/HOL/Library/Extended_Real.thy
src/HOL/Library/FSet.thy
src/HOL/Library/Infinite_Set.thy
src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy
src/HOL/Library/Permutations.thy
src/HOL/Library/RBT_Impl.thy
src/HOL/Library/RBT_Set.thy
src/HOL/Library/Stream.thy
src/HOL/Word/Bits_Int.thy
src/HOL/Word/Bool_List_Representation.thy
src/HOL/Word/Misc_Typedef.thy
src/HOL/Word/Word.thy
src/HOL/Word/Word_Miscellaneous.thy
     1.1 --- a/src/HOL/Library/Bourbaki_Witt_Fixpoint.thy	Fri Jan 12 14:43:06 2018 +0100
     1.2 +++ b/src/HOL/Library/Bourbaki_Witt_Fixpoint.thy	Fri Jan 12 15:27:46 2018 +0100
     1.3 @@ -357,7 +357,7 @@
     1.4  by (blast intro: ChainsI dest: in_ChainsD)
     1.5  
     1.6  lemma fixp_above_Kleene_iter:
     1.7 -  assumes "\<forall>M \<in> Chains leq. finite M" (* convenient but surely not necessary *)
     1.8 +  assumes "\<forall>M \<in> Chains leq. finite M"  \<comment> \<open>convenient but surely not necessary\<close>
     1.9    assumes "(f ^^ Suc k) a = (f ^^ k) a"
    1.10    shows "fixp_above a = (f ^^ k) a"
    1.11  proof(rule leq_antisym)
     2.1 --- a/src/HOL/Library/DAList_Multiset.thy	Fri Jan 12 14:43:06 2018 +0100
     2.2 +++ b/src/HOL/Library/DAList_Multiset.thy	Fri Jan 12 15:27:46 2018 +0100
     2.3 @@ -372,8 +372,7 @@
     2.4  
     2.5  end
     2.6  
     2.7 -(* we cannot use (\<lambda>a n. (+) (a * n)) for folding, since * is not defined
     2.8 -   in comm_monoid_add *)
     2.9 +\<comment> \<open>we cannot use \<open>\<lambda>a n. (+) (a * n)\<close> for folding, since \<open>( * )\<close> is not defined in \<open>comm_monoid_add\<close>\<close>
    2.10  lemma sum_mset_Bag[code]: "sum_mset (Bag ms) = DAList_Multiset.fold (\<lambda>a n. (((+) a) ^^ n)) 0 ms"
    2.11    unfolding sum_mset.eq_fold
    2.12    apply (rule comp_fun_commute.DAList_Multiset_fold)
    2.13 @@ -381,8 +380,7 @@
    2.14    apply (auto simp: ac_simps)
    2.15    done
    2.16  
    2.17 -(* we cannot use (\<lambda>a n. ( * ) (a ^ n)) for folding, since ^ is not defined
    2.18 -   in comm_monoid_mult *)
    2.19 +\<comment> \<open>we cannot use \<open>\<lambda>a n. ( * ) (a ^ n)\<close> for folding, since \<open>(^)\<close> is not defined in \<open>comm_monoid_mult\<close>\<close>
    2.20  lemma prod_mset_Bag[code]: "prod_mset (Bag ms) = DAList_Multiset.fold (\<lambda>a n. ((( * ) a) ^^ n)) 1 ms"
    2.21    unfolding prod_mset.eq_fold
    2.22    apply (rule comp_fun_commute.DAList_Multiset_fold)
     3.1 --- a/src/HOL/Library/Extended_Nonnegative_Real.thy	Fri Jan 12 14:43:06 2018 +0100
     3.2 +++ b/src/HOL/Library/Extended_Nonnegative_Real.thy	Fri Jan 12 15:27:46 2018 +0100
     3.3 @@ -181,7 +181,7 @@
     3.4      by (intro cSUP_upper bdd_above_image_mono assms) (auto simp: mono_def)
     3.5  qed
     3.6  
     3.7 -(*These generalise their counterparts in Nat.linordered_semidom_class*)
     3.8 +\<comment> \<open>These generalise their counterparts in \<open>Nat.linordered_semidom_class\<close>\<close>
     3.9  lemma of_nat_less[simp]:
    3.10    "m < n \<Longrightarrow> of_nat m < (of_nat n::'a::{linordered_nonzero_semiring, semiring_char_0})"
    3.11    by (auto simp: less_le)
     4.1 --- a/src/HOL/Library/Extended_Real.thy	Fri Jan 12 14:43:06 2018 +0100
     4.2 +++ b/src/HOL/Library/Extended_Real.thy	Fri Jan 12 15:27:46 2018 +0100
     4.3 @@ -4091,7 +4091,7 @@
     4.4  
     4.5  subsubsection \<open>Tests for code generator\<close>
     4.6  
     4.7 -(* A small list of simple arithmetic expressions *)
     4.8 +text \<open>A small list of simple arithmetic expressions.\<close>
     4.9  
    4.10  value "- \<infinity> :: ereal"
    4.11  value "\<bar>-\<infinity>\<bar> :: ereal"
     5.1 --- a/src/HOL/Library/FSet.thy	Fri Jan 12 14:43:06 2018 +0100
     5.2 +++ b/src/HOL/Library/FSet.thy	Fri Jan 12 15:27:46 2018 +0100
     5.3 @@ -1204,7 +1204,7 @@
     5.4  
     5.5  subsection \<open>Advanced relator customization\<close>
     5.6  
     5.7 -(* Set vs. sum relators: *)
     5.8 +text \<open>Set vs. sum relators:\<close>
     5.9  
    5.10  lemma rel_set_rel_sum[simp]:
    5.11  "rel_set (rel_sum \<chi> \<phi>) A1 A2 \<longleftrightarrow>
     6.1 --- a/src/HOL/Library/Infinite_Set.thy	Fri Jan 12 14:43:06 2018 +0100
     6.2 +++ b/src/HOL/Library/Infinite_Set.thy	Fri Jan 12 15:27:46 2018 +0100
     6.3 @@ -188,7 +188,7 @@
     6.4  lemma MOST_ge_nat: "MOST n::nat. m \<le> n"
     6.5    by (simp add: cofinite_eq_sequentially)
     6.6  
     6.7 -(* legacy names *)
     6.8 +\<comment> \<open>legacy names\<close>
     6.9  lemma Inf_many_def: "Inf_many P \<longleftrightarrow> infinite {x. P x}" by (fact frequently_cofinite)
    6.10  lemma Alm_all_def: "Alm_all P \<longleftrightarrow> \<not> (INFM x. \<not> P x)" by simp
    6.11  lemma INFM_iff_infinite: "(INFM x. P x) \<longleftrightarrow> infinite {x. P x}" by (fact frequently_cofinite)
     7.1 --- a/src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy	Fri Jan 12 14:43:06 2018 +0100
     7.2 +++ b/src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy	Fri Jan 12 15:27:46 2018 +0100
     7.3 @@ -28,7 +28,8 @@
     7.4  
     7.5  section\<open>Linear temporal logic\<close>
     7.6  
     7.7 -(* Propositional connectives: *)
     7.8 +text \<open>Propositional connectives:\<close>
     7.9 +
    7.10  abbreviation (input) IMPL (infix "impl" 60)
    7.11  where "\<phi> impl \<psi> \<equiv> \<lambda> xs. \<phi> xs \<longrightarrow> \<psi> xs"
    7.12  
    7.13 @@ -55,7 +56,8 @@
    7.14  
    7.15  lemma non_not[simp]: "not (not \<phi>) = \<phi>" by simp
    7.16  
    7.17 -(* Temporal (LTL) connectives: *)
    7.18 +text \<open>Temporal (LTL) connectives:\<close>
    7.19 +
    7.20  fun holds where "holds P xs \<longleftrightarrow> P (shd xs)"
    7.21  fun nxt where "nxt \<phi> xs = \<phi> (stl xs)"
    7.22  
    7.23 @@ -76,7 +78,7 @@
    7.24  coinductive alw for \<phi> where
    7.25  alw: "\<lbrakk>\<phi> xs; alw \<phi> (stl xs)\<rbrakk> \<Longrightarrow> alw \<phi> xs"
    7.26  
    7.27 -(* weak until: *)
    7.28 +\<comment> \<open>weak until:\<close>
    7.29  coinductive UNTIL (infix "until" 60) for \<phi> \<psi> where
    7.30  base: "\<psi> xs \<Longrightarrow> (\<phi> until \<psi>) xs"
    7.31  |
    7.32 @@ -377,7 +379,7 @@
    7.33    thus ?L by (induct rule: sset_induct) (simp_all add: ev.base ev.step)
    7.34  qed
    7.35  
    7.36 -(* LTL as a program logic: *)
    7.37 +text \<open>LTL as a program logic:\<close>
    7.38  lemma alw_invar:
    7.39  assumes "\<phi> xs" and "alw (\<phi> impl nxt \<phi>) xs"
    7.40  shows "alw \<phi> xs"
     8.1 --- a/src/HOL/Library/Permutations.thy	Fri Jan 12 14:43:06 2018 +0100
     8.2 +++ b/src/HOL/Library/Permutations.thy	Fri Jan 12 15:27:46 2018 +0100
     8.3 @@ -1054,7 +1054,7 @@
     8.4    qed
     8.5  qed
     8.6  
     8.7 -(* Prove image_mset_eq_implies_permutes *)
     8.8 +\<comment> \<open>Prove \<open>image_mset_eq_implies_permutes\<close> ...\<close>
     8.9  lemma image_mset_eq_implies_permutes:
    8.10    fixes f :: "'a \<Rightarrow> 'b"
    8.11    assumes "finite A"
    8.12 @@ -1114,7 +1114,7 @@
    8.13  lemma mset_set_upto_eq_mset_upto: "mset_set {..<n} = mset [0..<n]"
    8.14    by (induct n) (auto simp: add.commute lessThan_Suc)
    8.15  
    8.16 -(* and derive the existing property: *)
    8.17 +\<comment> \<open>... and derive the existing property:\<close>
    8.18  lemma mset_eq_permutation:
    8.19    fixes xs ys :: "'a list"
    8.20    assumes mset_eq: "mset xs = mset ys"
     9.1 --- a/src/HOL/Library/RBT_Impl.thy	Fri Jan 12 14:43:06 2018 +0100
     9.2 +++ b/src/HOL/Library/RBT_Impl.thy	Fri Jan 12 15:27:46 2018 +0100
     9.3 @@ -1081,8 +1081,7 @@
     9.4    "fold f (Branch c lt k v rt) x = fold f rt (f k v (fold f lt x))"
     9.5  by(simp_all)
     9.6  
     9.7 -(* fold with continuation predicate *)
     9.8 -
     9.9 +\<comment> \<open>fold with continuation predicate\<close>
    9.10  fun foldi :: "('c \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a :: linorder, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c" 
    9.11    where
    9.12    "foldi c f Empty s = s" |
    10.1 --- a/src/HOL/Library/RBT_Set.thy	Fri Jan 12 14:43:06 2018 +0100
    10.2 +++ b/src/HOL/Library/RBT_Set.thy	Fri Jan 12 15:27:46 2018 +0100
    10.3 @@ -126,14 +126,15 @@
    10.4  
    10.5  subsection \<open>folding over non empty trees and selecting the minimal and maximal element\<close>
    10.6  
    10.7 -(** concrete **)
    10.8 +subsubsection \<open>concrete\<close>
    10.9  
   10.10 -(* The concrete part is here because it's probably not general enough to be moved to RBT_Impl *)
   10.11 +text \<open>The concrete part is here because it's probably not general enough to be moved to \<open>RBT_Impl\<close>\<close>
   10.12  
   10.13  definition rbt_fold1_keys :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a::linorder, 'b) RBT_Impl.rbt \<Rightarrow> 'a" 
   10.14    where "rbt_fold1_keys f t = List.fold f (tl(RBT_Impl.keys t)) (hd(RBT_Impl.keys t))"
   10.15  
   10.16 -(* minimum *)
   10.17 +
   10.18 +paragraph \<open>minimum\<close>
   10.19  
   10.20  definition rbt_min :: "('a::linorder, unit) RBT_Impl.rbt \<Rightarrow> 'a" 
   10.21    where "rbt_min t = rbt_fold1_keys min t"
   10.22 @@ -229,7 +230,8 @@
   10.23        Min.set_eq_fold [symmetric] Min_eqI rbt_min_opt_in_set)
   10.24  qed
   10.25  
   10.26 -(* maximum *)
   10.27 +
   10.28 +paragraph \<open>maximum\<close>
   10.29  
   10.30  definition rbt_max :: "('a::linorder, unit) RBT_Impl.rbt \<Rightarrow> 'a" 
   10.31    where "rbt_max t = rbt_fold1_keys max t"
   10.32 @@ -331,7 +333,7 @@
   10.33  qed
   10.34  
   10.35  
   10.36 -(** abstract **)
   10.37 +subsubsection \<open>abstract\<close>
   10.38  
   10.39  context includes rbt.lifting begin
   10.40  lift_definition fold1_keys :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a::linorder, 'b) rbt \<Rightarrow> 'a"
   10.41 @@ -351,7 +353,8 @@
   10.42      by (auto simp: fold1_keys_def_alt set_keys fold_def_alt non_empty_keys set_eq_fold [symmetric])
   10.43  qed
   10.44  
   10.45 -(* minimum *)
   10.46 +
   10.47 +paragraph \<open>minimum\<close>
   10.48  
   10.49  lift_definition r_min :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_min .
   10.50  
   10.51 @@ -388,7 +391,8 @@
   10.52      done
   10.53  qed
   10.54  
   10.55 -(* maximum *)
   10.56 +
   10.57 +paragraph \<open>maximum\<close>
   10.58  
   10.59  lift_definition r_max :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_max .
   10.60  
    11.1 --- a/src/HOL/Library/Stream.thy	Fri Jan 12 14:43:06 2018 +0100
    11.2 +++ b/src/HOL/Library/Stream.thy	Fri Jan 12 15:27:46 2018 +0100
    11.3 @@ -21,7 +21,7 @@
    11.4  context
    11.5  begin
    11.6  
    11.7 -(*for code generation only*)
    11.8 +\<comment> \<open>for code generation only\<close>
    11.9  qualified definition smember :: "'a \<Rightarrow> 'a stream \<Rightarrow> bool" where
   11.10    [code_abbrev]: "smember x s \<longleftrightarrow> x \<in> sset s"
   11.11  
    12.1 --- a/src/HOL/Word/Bits_Int.thy	Fri Jan 12 14:43:06 2018 +0100
    12.2 +++ b/src/HOL/Word/Bits_Int.thy	Fri Jan 12 15:27:46 2018 +0100
    12.3 @@ -609,7 +609,7 @@
    12.4      apply (auto simp: Bit_B0_2t [symmetric])
    12.5    done
    12.6  
    12.7 -(*for use when simplifying with bin_nth_Bit*)
    12.8 +\<comment> \<open>for use when simplifying with \<open>bin_nth_Bit\<close>\<close>
    12.9  lemma ex_eq_or: "(\<exists>m. n = Suc m \<and> (m = k \<or> P m)) \<longleftrightarrow> n = Suc k \<or> (\<exists>m. n = Suc m \<and> P m)"
   12.10    by auto
   12.11  
    13.1 --- a/src/HOL/Word/Bool_List_Representation.thy	Fri Jan 12 14:43:06 2018 +0100
    13.2 +++ b/src/HOL/Word/Bool_List_Representation.thy	Fri Jan 12 15:27:46 2018 +0100
    13.3 @@ -839,7 +839,7 @@
    13.4  lemmas rsplit_aux_simp1s = rsplit_aux_simps [THEN th_if_simp1]
    13.5  
    13.6  lemmas rsplit_aux_simp2ls = rsplit_aux_simps [THEN th_if_simp2]
    13.7 -(* these safe to [simp add] as require calculating m - n *)
    13.8 +\<comment> \<open>these safe to \<open>[simp add]\<close> as require calculating \<open>m - n\<close>\<close>
    13.9  lemmas bin_rsplit_aux_simp2s [simp] = rsplit_aux_simp2ls [unfolded Let_def]
   13.10  lemmas rbscl = bin_rsplit_aux_simp2s (2)
   13.11  
    14.1 --- a/src/HOL/Word/Misc_Typedef.thy	Fri Jan 12 14:43:06 2018 +0100
    14.2 +++ b/src/HOL/Word/Misc_Typedef.thy	Fri Jan 12 15:27:46 2018 +0100
    14.3 @@ -147,15 +147,16 @@
    14.4  lemma fns5: "Rep \<circ> fa \<circ> Abs = fr \<Longrightarrow> fr \<circ> norm = fr \<and> norm \<circ> fr = fr"
    14.5    by (fold eq_norm') auto
    14.6  
    14.7 -(* following give conditions for converses to td_fns1
    14.8 -  the condition (norm \<circ> fr \<circ> norm = fr \<circ> norm) says that
    14.9 -  fr takes normalised arguments to normalised results,
   14.10 -  (norm \<circ> fr \<circ> norm = norm \<circ> fr) says that fr
   14.11 -  takes norm-equivalent arguments to norm-equivalent results,
   14.12 -  (fr \<circ> norm = fr) says that fr
   14.13 -  takes norm-equivalent arguments to the same result, and
   14.14 -  (norm \<circ> fr = fr) says that fr takes any argument to a normalised result
   14.15 -  *)
   14.16 +text \<open>
   14.17 +  following give conditions for converses to \<open>td_fns1\<close>
   14.18 +  \<^item> the condition \<open>norm \<circ> fr \<circ> norm = fr \<circ> norm\<close> says that
   14.19 +    \<open>fr\<close> takes normalised arguments to normalised results
   14.20 +  \<^item> \<open>norm \<circ> fr \<circ> norm = norm \<circ> fr\<close> says that \<open>fr\<close>
   14.21 +    takes norm-equivalent arguments to norm-equivalent results
   14.22 +  \<^item> \<open>fr \<circ> norm = fr\<close> says that \<open>fr\<close>
   14.23 +    takes norm-equivalent arguments to the same result
   14.24 +  \<^item> \<open>norm \<circ> fr = fr\<close> says that \<open>fr\<close> takes any argument to a normalised result
   14.25 +\<close>
   14.26  lemma fns2: "Abs \<circ> fr \<circ> Rep = fa \<Longrightarrow> norm \<circ> fr \<circ> norm = fr \<circ> norm \<longleftrightarrow> Rep \<circ> fa = fr \<circ> Rep"
   14.27    apply (fold eq_norm')
   14.28    apply safe
    15.1 --- a/src/HOL/Word/Word.thy	Fri Jan 12 14:43:06 2018 +0100
    15.2 +++ b/src/HOL/Word/Word.thy	Fri Jan 12 15:27:46 2018 +0100
    15.3 @@ -527,10 +527,12 @@
    15.4           2 ^ (len_of TYPE('a) - 1))"
    15.5    using td_ext_sbin [where ?'a = 'a] by (simp add: no_sbintr_alt2)
    15.6  
    15.7 -(* We do sint before sbin, before sint is the user version
    15.8 -   and interpretations do not produce thm duplicates. I.e.
    15.9 -   we get the name word_sint.Rep_eqD, but not word_sbin.Req_eqD,
   15.10 -   because the latter is the same thm as the former *)
   15.11 +text \<open>
   15.12 +  We do \<open>sint\<close> before \<open>sbin\<close>, before \<open>sint\<close> is the user version
   15.13 +  and interpretations do not produce thm duplicates. I.e.
   15.14 +  we get the name \<open>word_sint.Rep_eqD\<close>, but not \<open>word_sbin.Req_eqD\<close>,
   15.15 +  because the latter is the same thm as the former.
   15.16 +\<close>
   15.17  interpretation word_sint:
   15.18    td_ext
   15.19      "sint ::'a::len word \<Rightarrow> int"
   15.20 @@ -765,7 +767,7 @@
   15.21    apply (auto simp add: nth_sbintr)
   15.22    done
   15.23  
   15.24 -(* type definitions theorem for in terms of equivalent bool list *)
   15.25 +\<comment> \<open>type definitions theorem for in terms of equivalent bool list\<close>
   15.26  lemma td_bl:
   15.27    "type_definition
   15.28      (to_bl :: 'a::len0 word \<Rightarrow> bool list)
   15.29 @@ -862,7 +864,7 @@
   15.30    for x :: "'a::len0 word"
   15.31    by (rule trans [OF bin_bl_bin word_ubin.norm_Rep])
   15.32  
   15.33 -(* naturals *)
   15.34 +\<comment> \<open>naturals\<close>
   15.35  lemma uints_unats: "uints n = int ` unats n"
   15.36    apply (unfold unats_def uints_num)
   15.37    apply safe
   15.38 @@ -898,8 +900,10 @@
   15.39      word_of_int (sbintrunc (len_of TYPE('a::len) - 1) (numeral x))"
   15.40    by (simp only: word_sbin.Abs_norm word_numeral_alt)
   15.41  
   15.42 -(** cast - note, no arg for new length, as it's determined by type of result,
   15.43 -  thus in "cast w = w, the type means cast to length of w! **)
   15.44 +text \<open>
   15.45 +  \<open>cast\<close> -- note, no arg for new length, as it's determined by type of result,
   15.46 +  thus in \<open>cast w = w\<close>, the type means cast to length of \<open>w\<close>!
   15.47 +\<close>
   15.48  
   15.49  lemma ucast_id: "ucast w = w"
   15.50    by (auto simp: ucast_def)
   15.51 @@ -914,8 +918,7 @@
   15.52    by (simp add: ucast_def test_bit_bin word_ubin.eq_norm nth_bintr word_size)
   15.53      (fast elim!: bin_nth_uint_imp)
   15.54  
   15.55 -(* for literal u(s)cast *)
   15.56 -
   15.57 +\<comment> \<open>literal u(s)cast\<close>
   15.58  lemma ucast_bintr [simp]:
   15.59    "ucast (numeral w :: 'a::len0 word) =
   15.60      word_of_int (bintrunc (len_of TYPE('a)) (numeral w))"
   15.61 @@ -1171,7 +1174,7 @@
   15.62  lemma ucast_1 [simp]: "ucast (1::'a::len word) = 1"
   15.63    by (simp add: ucast_def)
   15.64  
   15.65 -(* now, to get the weaker results analogous to word_div/mod_def *)
   15.66 +\<comment> \<open>now, to get the weaker results analogous to \<open>word_div\<close>/\<open>mod_def\<close>\<close>
   15.67  
   15.68  
   15.69  subsection \<open>Transferring goals from words to ints\<close>
   15.70 @@ -1244,7 +1247,7 @@
   15.71    "word_succ (- 1) = 0 \<and> word_succ 0 = 1 \<and> word_pred 0 = - 1 \<and> word_pred 1 = 0"
   15.72    by (simp_all add: word_succ_p1 word_pred_m1)
   15.73  
   15.74 -(* alternative approach to lifting arithmetic equalities *)
   15.75 +\<comment> \<open>alternative approach to lifting arithmetic equalities\<close>
   15.76  lemma word_of_int_Ex: "\<exists>y. x = word_of_int y"
   15.77    by (rule_tac x="uint x" in exI) simp
   15.78  
   15.79 @@ -1421,11 +1424,11 @@
   15.80    word_uint.Rep_inject [symmetric]
   15.81    uint_sub_if' uint_plus_if'
   15.82  
   15.83 -(* use this to stop, eg, 2 ^ len_of TYPE(32) being simplified *)
   15.84 +\<comment> \<open>use this to stop, eg. \<open>2 ^ len_of TYPE(32)\<close> being simplified\<close>
   15.85  lemma power_False_cong: "False \<Longrightarrow> a ^ b = c ^ d"
   15.86    by auto
   15.87  
   15.88 -(* uint_arith_tac: reduce to arithmetic on int, try to solve by arith *)
   15.89 +\<comment> \<open>\<open>uint_arith_tac\<close>: reduce to arithmetic on int, try to solve by arith\<close>
   15.90  ML \<open>
   15.91  fun uint_arith_simpset ctxt =
   15.92    ctxt addsimps @{thms uint_arith_simps}
   15.93 @@ -1641,7 +1644,7 @@
   15.94    apply simp
   15.95    done
   15.96  
   15.97 -(* links with rbl operations *)
   15.98 +\<comment> \<open>links with \<open>rbl\<close> operations\<close>
   15.99  lemma word_succ_rbl: "to_bl w = bl \<Longrightarrow> to_bl (word_succ w) = rev (rbl_succ (rev bl))"
  15.100    apply (unfold word_succ_def)
  15.101    apply clarify
  15.102 @@ -1690,8 +1693,10 @@
  15.103  lemma word_of_int_nat: "0 \<le> x \<Longrightarrow> word_of_int x = of_nat (nat x)"
  15.104    by (simp add: word_of_int)
  15.105  
  15.106 -(* note that iszero_def is only for class comm_semiring_1_cancel,
  15.107 -   which requires word length >= 1, ie 'a::len word *)
  15.108 +text \<open>
  15.109 +  note that \<open>iszero_def\<close> is only for class \<open>comm_semiring_1_cancel\<close>,
  15.110 +  which requires word length \<open>\<ge> 1\<close>, ie \<open>'a::len word\<close>
  15.111 +\<close>
  15.112  lemma iszero_word_no [simp]:
  15.113    "iszero (numeral bin :: 'a::len word) =
  15.114      iszero (bintrunc (len_of TYPE('a)) (numeral bin))"
  15.115 @@ -1907,8 +1912,7 @@
  15.116    word_unat.Rep_inject [symmetric]
  15.117    unat_sub_if' unat_plus_if' unat_div unat_mod
  15.118  
  15.119 -(* unat_arith_tac: tactic to reduce word arithmetic to nat,
  15.120 -   try to solve via arith *)
  15.121 +\<comment> \<open>\<open>unat_arith_tac\<close>: tactic to reduce word arithmetic to \<open>nat\<close>, try to solve via \<open>arith\<close>\<close>
  15.122  ML \<open>
  15.123  fun unat_arith_simpset ctxt =
  15.124    ctxt addsimps @{thms unat_arith_simps}
  15.125 @@ -2087,14 +2091,13 @@
  15.126  
  15.127  lemmas bin_log_bintrs = bin_trunc_not bin_trunc_xor bin_trunc_and bin_trunc_or
  15.128  
  15.129 -(* following definitions require both arithmetic and bit-wise word operations *)
  15.130 -
  15.131 -(* to get word_no_log_defs from word_log_defs, using bin_log_bintrs *)
  15.132 +\<comment> \<open>following definitions require both arithmetic and bit-wise word operations\<close>
  15.133 +
  15.134 +\<comment> \<open>to get \<open>word_no_log_defs\<close> from \<open>word_log_defs\<close>, using \<open>bin_log_bintrs\<close>\<close>
  15.135  lemmas wils1 = bin_log_bintrs [THEN word_ubin.norm_eq_iff [THEN iffD1],
  15.136    folded word_ubin.eq_norm, THEN eq_reflection]
  15.137  
  15.138 -(* the binary operations only *)
  15.139 -(* BH: why is this needed? *)
  15.140 +\<comment> \<open>the binary operations only\<close>  (* BH: why is this needed? *)
  15.141  lemmas word_log_binary_defs =
  15.142    word_and_def word_or_def word_xor_def
  15.143  
  15.144 @@ -2201,9 +2204,7 @@
  15.145  lemma nth_minus1 [simp]: "(-1 :: 'a::len0 word) !! n \<longleftrightarrow> n < len_of TYPE('a)"
  15.146    by transfer simp
  15.147  
  15.148 -(* get from commutativity, associativity etc of int_and etc
  15.149 -  to same for word_and etc *)
  15.150 -
  15.151 +\<comment> \<open>get from commutativity, associativity etc of \<open>int_and\<close> etc to same for \<open>word_and etc\<close>\<close>
  15.152  lemmas bwsimps =
  15.153    wi_hom_add
  15.154    word_wi_log_defs
  15.155 @@ -2670,9 +2671,11 @@
  15.156     apply (auto simp add: nth_shiftr1)
  15.157    done
  15.158  
  15.159 -(* see paper page 10, (1), (2), shiftr1_def is of the form of (1),
  15.160 -  where f (ie bin_rest) takes normal arguments to normal results,
  15.161 -  thus we get (2) from (1) *)
  15.162 +text \<open>
  15.163 +  see paper page 10, (1), (2), \<open>shiftr1_def\<close> is of the form of (1),
  15.164 +  where \<open>f\<close> (ie \<open>bin_rest\<close>) takes normal arguments to normal results,
  15.165 +  thus we get (2) from (1)
  15.166 +\<close>
  15.167  
  15.168  lemma uint_shiftr1: "uint (shiftr1 w) = bin_rest (uint w)"
  15.169    apply (unfold shiftr1_def word_ubin.eq_norm bin_rest_trunc_i)
  15.170 @@ -2774,7 +2777,7 @@
  15.171    for w :: "'a::len word"
  15.172    by (simp add: shiftl1_bl word_rep_drop drop_Suc drop_Cons') (fast intro!: Suc_leI)
  15.173  
  15.174 -(* Generalized version of bl_shiftl1. Maybe this one should replace it? *)
  15.175 +\<comment> \<open>Generalized version of \<open>bl_shiftl1\<close>. Maybe this one should replace it?\<close>
  15.176  lemma bl_shiftl1': "to_bl (shiftl1 w) = tl (to_bl w @ [False])"
  15.177    by (simp add: shiftl1_bl word_rep_drop drop_Suc del: drop_append)
  15.178  
  15.179 @@ -2788,7 +2791,7 @@
  15.180    for w :: "'a::len word"
  15.181    by (simp add: shiftr1_bl word_rep_drop len_gt_0 [THEN Suc_leI])
  15.182  
  15.183 -(* Generalized version of bl_shiftr1. Maybe this one should replace it? *)
  15.184 +\<comment> \<open>Generalized version of \<open>bl_shiftr1\<close>. Maybe this one should replace it?\<close>
  15.185  lemma bl_shiftr1': "to_bl (shiftr1 w) = butlast (False # to_bl w)"
  15.186    apply (rule word_bl.Abs_inverse')
  15.187     apply (simp del: butlast.simps)
  15.188 @@ -2909,7 +2912,7 @@
  15.189    apply (clarsimp simp add: shiftl_bl word_size test_bit_of_bl nth_append)
  15.190    done
  15.191  
  15.192 -(* note - the following results use 'a::len word < number_ring *)
  15.193 +\<comment> \<open>note -- the following results use \<open>'a::len word < number_ring\<close>\<close>
  15.194  
  15.195  lemma shiftl1_2t: "shiftl1 w = 2 * w"
  15.196    for w :: "'a::len word"
  15.197 @@ -3719,7 +3722,7 @@
  15.198  
  15.199  lemmas length_word_rsplit_exp_size' = refl [THEN length_word_rsplit_exp_size]
  15.200  
  15.201 -(* alternative proof of word_rcat_rsplit *)
  15.202 +\<comment> \<open>alternative proof of \<open>word_rcat_rsplit\<close>\<close>
  15.203  lemmas tdle = times_div_less_eq_dividend
  15.204  lemmas dtle = xtr4 [OF tdle mult.commute]
  15.205  
  15.206 @@ -4047,7 +4050,7 @@
  15.207  
  15.208  subsubsection \<open>"Word rotation commutes with bit-wise operations\<close>
  15.209  
  15.210 -(* using locale to not pollute lemma namespace *)
  15.211 +\<comment> \<open>using locale to not pollute lemma namespace\<close>
  15.212  locale word_rotate
  15.213  begin
  15.214  
    16.1 --- a/src/HOL/Word/Word_Miscellaneous.thy	Fri Jan 12 14:43:06 2018 +0100
    16.2 +++ b/src/HOL/Word/Word_Miscellaneous.thy	Fri Jan 12 15:27:46 2018 +0100
    16.3 @@ -95,8 +95,7 @@
    16.4  lemma if_same_eq_not: "(If p x y = (\<not> If p u v)) = (if p then x = (\<not> u) else y = (\<not> v))"
    16.5    by auto
    16.6  
    16.7 -(* note - if_Cons can cause blowup in the size, if p is complex,
    16.8 -  so make a simproc *)
    16.9 +\<comment> \<open>note -- \<open>if_Cons\<close> can cause blowup in the size, if \<open>p\<close> is complex, so make a simproc\<close>
   16.10  lemma if_Cons: "(if p then x # xs else y # ys) = If p x y # If p xs ys"
   16.11    by auto
   16.12