# HG changeset patch # User wenzelm # Date 1515767266 -3600 # Node ID 4a4c14b2480084ad4f0da12450548822d67030b9 # Parent dbaa38bd223a380e8cd3fe22bf35c2a42884a552 prefer formal comments; diff -r dbaa38bd223a -r 4a4c14b24800 src/HOL/Library/Bourbaki_Witt_Fixpoint.thy --- a/src/HOL/Library/Bourbaki_Witt_Fixpoint.thy Fri Jan 12 14:43:06 2018 +0100 +++ b/src/HOL/Library/Bourbaki_Witt_Fixpoint.thy Fri Jan 12 15:27:46 2018 +0100 @@ -357,7 +357,7 @@ by (blast intro: ChainsI dest: in_ChainsD) lemma fixp_above_Kleene_iter: - assumes "\M \ Chains leq. finite M" (* convenient but surely not necessary *) + assumes "\M \ Chains leq. finite M" \ \convenient but surely not necessary\ assumes "(f ^^ Suc k) a = (f ^^ k) a" shows "fixp_above a = (f ^^ k) a" proof(rule leq_antisym) diff -r dbaa38bd223a -r 4a4c14b24800 src/HOL/Library/DAList_Multiset.thy --- a/src/HOL/Library/DAList_Multiset.thy Fri Jan 12 14:43:06 2018 +0100 +++ b/src/HOL/Library/DAList_Multiset.thy Fri Jan 12 15:27:46 2018 +0100 @@ -372,8 +372,7 @@ end -(* we cannot use (\a n. (+) (a * n)) for folding, since * is not defined - in comm_monoid_add *) +\ \we cannot use \\a n. (+) (a * n)\ for folding, since \( * )\ is not defined in \comm_monoid_add\\ lemma sum_mset_Bag[code]: "sum_mset (Bag ms) = DAList_Multiset.fold (\a n. (((+) a) ^^ n)) 0 ms" unfolding sum_mset.eq_fold apply (rule comp_fun_commute.DAList_Multiset_fold) @@ -381,8 +380,7 @@ apply (auto simp: ac_simps) done -(* we cannot use (\a n. ( * ) (a ^ n)) for folding, since ^ is not defined - in comm_monoid_mult *) +\ \we cannot use \\a n. ( * ) (a ^ n)\ for folding, since \(^)\ is not defined in \comm_monoid_mult\\ lemma prod_mset_Bag[code]: "prod_mset (Bag ms) = DAList_Multiset.fold (\a n. ((( * ) a) ^^ n)) 1 ms" unfolding prod_mset.eq_fold apply (rule comp_fun_commute.DAList_Multiset_fold) diff -r dbaa38bd223a -r 4a4c14b24800 src/HOL/Library/Extended_Nonnegative_Real.thy --- a/src/HOL/Library/Extended_Nonnegative_Real.thy Fri Jan 12 14:43:06 2018 +0100 +++ b/src/HOL/Library/Extended_Nonnegative_Real.thy Fri Jan 12 15:27:46 2018 +0100 @@ -181,7 +181,7 @@ by (intro cSUP_upper bdd_above_image_mono assms) (auto simp: mono_def) qed -(*These generalise their counterparts in Nat.linordered_semidom_class*) +\ \These generalise their counterparts in \Nat.linordered_semidom_class\\ lemma of_nat_less[simp]: "m < n \ of_nat m < (of_nat n::'a::{linordered_nonzero_semiring, semiring_char_0})" by (auto simp: less_le) diff -r dbaa38bd223a -r 4a4c14b24800 src/HOL/Library/Extended_Real.thy --- a/src/HOL/Library/Extended_Real.thy Fri Jan 12 14:43:06 2018 +0100 +++ b/src/HOL/Library/Extended_Real.thy Fri Jan 12 15:27:46 2018 +0100 @@ -4091,7 +4091,7 @@ subsubsection \Tests for code generator\ -(* A small list of simple arithmetic expressions *) +text \A small list of simple arithmetic expressions.\ value "- \ :: ereal" value "\-\\ :: ereal" diff -r dbaa38bd223a -r 4a4c14b24800 src/HOL/Library/FSet.thy --- a/src/HOL/Library/FSet.thy Fri Jan 12 14:43:06 2018 +0100 +++ b/src/HOL/Library/FSet.thy Fri Jan 12 15:27:46 2018 +0100 @@ -1204,7 +1204,7 @@ subsection \Advanced relator customization\ -(* Set vs. sum relators: *) +text \Set vs. sum relators:\ lemma rel_set_rel_sum[simp]: "rel_set (rel_sum \ \) A1 A2 \ diff -r dbaa38bd223a -r 4a4c14b24800 src/HOL/Library/Infinite_Set.thy --- a/src/HOL/Library/Infinite_Set.thy Fri Jan 12 14:43:06 2018 +0100 +++ b/src/HOL/Library/Infinite_Set.thy Fri Jan 12 15:27:46 2018 +0100 @@ -188,7 +188,7 @@ lemma MOST_ge_nat: "MOST n::nat. m \ n" by (simp add: cofinite_eq_sequentially) -(* legacy names *) +\ \legacy names\ lemma Inf_many_def: "Inf_many P \ infinite {x. P x}" by (fact frequently_cofinite) lemma Alm_all_def: "Alm_all P \ \ (INFM x. \ P x)" by simp lemma INFM_iff_infinite: "(INFM x. P x) \ infinite {x. P x}" by (fact frequently_cofinite) diff -r dbaa38bd223a -r 4a4c14b24800 src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy --- a/src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy Fri Jan 12 14:43:06 2018 +0100 +++ b/src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy Fri Jan 12 15:27:46 2018 +0100 @@ -28,7 +28,8 @@ section\Linear temporal logic\ -(* Propositional connectives: *) +text \Propositional connectives:\ + abbreviation (input) IMPL (infix "impl" 60) where "\ impl \ \ \ xs. \ xs \ \ xs" @@ -55,7 +56,8 @@ lemma non_not[simp]: "not (not \) = \" by simp -(* Temporal (LTL) connectives: *) +text \Temporal (LTL) connectives:\ + fun holds where "holds P xs \ P (shd xs)" fun nxt where "nxt \ xs = \ (stl xs)" @@ -76,7 +78,7 @@ coinductive alw for \ where alw: "\\ xs; alw \ (stl xs)\ \ alw \ xs" -(* weak until: *) +\ \weak until:\ coinductive UNTIL (infix "until" 60) for \ \ where base: "\ xs \ (\ until \) xs" | @@ -377,7 +379,7 @@ thus ?L by (induct rule: sset_induct) (simp_all add: ev.base ev.step) qed -(* LTL as a program logic: *) +text \LTL as a program logic:\ lemma alw_invar: assumes "\ xs" and "alw (\ impl nxt \) xs" shows "alw \ xs" diff -r dbaa38bd223a -r 4a4c14b24800 src/HOL/Library/Permutations.thy --- a/src/HOL/Library/Permutations.thy Fri Jan 12 14:43:06 2018 +0100 +++ b/src/HOL/Library/Permutations.thy Fri Jan 12 15:27:46 2018 +0100 @@ -1054,7 +1054,7 @@ qed qed -(* Prove image_mset_eq_implies_permutes *) +\ \Prove \image_mset_eq_implies_permutes\ ...\ lemma image_mset_eq_implies_permutes: fixes f :: "'a \ 'b" assumes "finite A" @@ -1114,7 +1114,7 @@ lemma mset_set_upto_eq_mset_upto: "mset_set {.. \... and derive the existing property:\ lemma mset_eq_permutation: fixes xs ys :: "'a list" assumes mset_eq: "mset xs = mset ys" diff -r dbaa38bd223a -r 4a4c14b24800 src/HOL/Library/RBT_Impl.thy --- a/src/HOL/Library/RBT_Impl.thy Fri Jan 12 14:43:06 2018 +0100 +++ b/src/HOL/Library/RBT_Impl.thy Fri Jan 12 15:27:46 2018 +0100 @@ -1081,8 +1081,7 @@ "fold f (Branch c lt k v rt) x = fold f rt (f k v (fold f lt x))" by(simp_all) -(* fold with continuation predicate *) - +\ \fold with continuation predicate\ fun foldi :: "('c \ bool) \ ('a \ 'b \ 'c \ 'c) \ ('a :: linorder, 'b) rbt \ 'c \ 'c" where "foldi c f Empty s = s" | diff -r dbaa38bd223a -r 4a4c14b24800 src/HOL/Library/RBT_Set.thy --- a/src/HOL/Library/RBT_Set.thy Fri Jan 12 14:43:06 2018 +0100 +++ b/src/HOL/Library/RBT_Set.thy Fri Jan 12 15:27:46 2018 +0100 @@ -126,14 +126,15 @@ subsection \folding over non empty trees and selecting the minimal and maximal element\ -(** concrete **) +subsubsection \concrete\ -(* The concrete part is here because it's probably not general enough to be moved to RBT_Impl *) +text \The concrete part is here because it's probably not general enough to be moved to \RBT_Impl\\ definition rbt_fold1_keys :: "('a \ 'a \ 'a) \ ('a::linorder, 'b) RBT_Impl.rbt \ 'a" where "rbt_fold1_keys f t = List.fold f (tl(RBT_Impl.keys t)) (hd(RBT_Impl.keys t))" -(* minimum *) + +paragraph \minimum\ definition rbt_min :: "('a::linorder, unit) RBT_Impl.rbt \ 'a" where "rbt_min t = rbt_fold1_keys min t" @@ -229,7 +230,8 @@ Min.set_eq_fold [symmetric] Min_eqI rbt_min_opt_in_set) qed -(* maximum *) + +paragraph \maximum\ definition rbt_max :: "('a::linorder, unit) RBT_Impl.rbt \ 'a" where "rbt_max t = rbt_fold1_keys max t" @@ -331,7 +333,7 @@ qed -(** abstract **) +subsubsection \abstract\ context includes rbt.lifting begin lift_definition fold1_keys :: "('a \ 'a \ 'a) \ ('a::linorder, 'b) rbt \ 'a" @@ -351,7 +353,8 @@ by (auto simp: fold1_keys_def_alt set_keys fold_def_alt non_empty_keys set_eq_fold [symmetric]) qed -(* minimum *) + +paragraph \minimum\ lift_definition r_min :: "('a :: linorder, unit) rbt \ 'a" is rbt_min . @@ -388,7 +391,8 @@ done qed -(* maximum *) + +paragraph \maximum\ lift_definition r_max :: "('a :: linorder, unit) rbt \ 'a" is rbt_max . diff -r dbaa38bd223a -r 4a4c14b24800 src/HOL/Library/Stream.thy --- a/src/HOL/Library/Stream.thy Fri Jan 12 14:43:06 2018 +0100 +++ b/src/HOL/Library/Stream.thy Fri Jan 12 15:27:46 2018 +0100 @@ -21,7 +21,7 @@ context begin -(*for code generation only*) +\ \for code generation only\ qualified definition smember :: "'a \ 'a stream \ bool" where [code_abbrev]: "smember x s \ x \ sset s" diff -r dbaa38bd223a -r 4a4c14b24800 src/HOL/Word/Bits_Int.thy --- a/src/HOL/Word/Bits_Int.thy Fri Jan 12 14:43:06 2018 +0100 +++ b/src/HOL/Word/Bits_Int.thy Fri Jan 12 15:27:46 2018 +0100 @@ -609,7 +609,7 @@ apply (auto simp: Bit_B0_2t [symmetric]) done -(*for use when simplifying with bin_nth_Bit*) +\ \for use when simplifying with \bin_nth_Bit\\ lemma ex_eq_or: "(\m. n = Suc m \ (m = k \ P m)) \ n = Suc k \ (\m. n = Suc m \ P m)" by auto diff -r dbaa38bd223a -r 4a4c14b24800 src/HOL/Word/Bool_List_Representation.thy --- a/src/HOL/Word/Bool_List_Representation.thy Fri Jan 12 14:43:06 2018 +0100 +++ b/src/HOL/Word/Bool_List_Representation.thy Fri Jan 12 15:27:46 2018 +0100 @@ -839,7 +839,7 @@ lemmas rsplit_aux_simp1s = rsplit_aux_simps [THEN th_if_simp1] lemmas rsplit_aux_simp2ls = rsplit_aux_simps [THEN th_if_simp2] -(* these safe to [simp add] as require calculating m - n *) +\ \these safe to \[simp add]\ as require calculating \m - n\\ lemmas bin_rsplit_aux_simp2s [simp] = rsplit_aux_simp2ls [unfolded Let_def] lemmas rbscl = bin_rsplit_aux_simp2s (2) diff -r dbaa38bd223a -r 4a4c14b24800 src/HOL/Word/Misc_Typedef.thy --- a/src/HOL/Word/Misc_Typedef.thy Fri Jan 12 14:43:06 2018 +0100 +++ b/src/HOL/Word/Misc_Typedef.thy Fri Jan 12 15:27:46 2018 +0100 @@ -147,15 +147,16 @@ lemma fns5: "Rep \ fa \ Abs = fr \ fr \ norm = fr \ norm \ fr = fr" by (fold eq_norm') auto -(* following give conditions for converses to td_fns1 - the condition (norm \ fr \ norm = fr \ norm) says that - fr takes normalised arguments to normalised results, - (norm \ fr \ norm = norm \ fr) says that fr - takes norm-equivalent arguments to norm-equivalent results, - (fr \ norm = fr) says that fr - takes norm-equivalent arguments to the same result, and - (norm \ fr = fr) says that fr takes any argument to a normalised result - *) +text \ + following give conditions for converses to \td_fns1\ + \<^item> the condition \norm \ fr \ norm = fr \ norm\ says that + \fr\ takes normalised arguments to normalised results + \<^item> \norm \ fr \ norm = norm \ fr\ says that \fr\ + takes norm-equivalent arguments to norm-equivalent results + \<^item> \fr \ norm = fr\ says that \fr\ + takes norm-equivalent arguments to the same result + \<^item> \norm \ fr = fr\ says that \fr\ takes any argument to a normalised result +\ lemma fns2: "Abs \ fr \ Rep = fa \ norm \ fr \ norm = fr \ norm \ Rep \ fa = fr \ Rep" apply (fold eq_norm') apply safe diff -r dbaa38bd223a -r 4a4c14b24800 src/HOL/Word/Word.thy --- a/src/HOL/Word/Word.thy Fri Jan 12 14:43:06 2018 +0100 +++ b/src/HOL/Word/Word.thy Fri Jan 12 15:27:46 2018 +0100 @@ -527,10 +527,12 @@ 2 ^ (len_of TYPE('a) - 1))" using td_ext_sbin [where ?'a = 'a] by (simp add: no_sbintr_alt2) -(* We do sint before sbin, before sint is the user version - and interpretations do not produce thm duplicates. I.e. - we get the name word_sint.Rep_eqD, but not word_sbin.Req_eqD, - because the latter is the same thm as the former *) +text \ + We do \sint\ before \sbin\, before \sint\ is the user version + and interpretations do not produce thm duplicates. I.e. + we get the name \word_sint.Rep_eqD\, but not \word_sbin.Req_eqD\, + because the latter is the same thm as the former. +\ interpretation word_sint: td_ext "sint ::'a::len word \ int" @@ -765,7 +767,7 @@ apply (auto simp add: nth_sbintr) done -(* type definitions theorem for in terms of equivalent bool list *) +\ \type definitions theorem for in terms of equivalent bool list\ lemma td_bl: "type_definition (to_bl :: 'a::len0 word \ bool list) @@ -862,7 +864,7 @@ for x :: "'a::len0 word" by (rule trans [OF bin_bl_bin word_ubin.norm_Rep]) -(* naturals *) +\ \naturals\ lemma uints_unats: "uints n = int ` unats n" apply (unfold unats_def uints_num) apply safe @@ -898,8 +900,10 @@ word_of_int (sbintrunc (len_of TYPE('a::len) - 1) (numeral x))" by (simp only: word_sbin.Abs_norm word_numeral_alt) -(** cast - note, no arg for new length, as it's determined by type of result, - thus in "cast w = w, the type means cast to length of w! **) +text \ + \cast\ -- note, no arg for new length, as it's determined by type of result, + thus in \cast w = w\, the type means cast to length of \w\! +\ lemma ucast_id: "ucast w = w" by (auto simp: ucast_def) @@ -914,8 +918,7 @@ by (simp add: ucast_def test_bit_bin word_ubin.eq_norm nth_bintr word_size) (fast elim!: bin_nth_uint_imp) -(* for literal u(s)cast *) - +\ \literal u(s)cast\ lemma ucast_bintr [simp]: "ucast (numeral w :: 'a::len0 word) = word_of_int (bintrunc (len_of TYPE('a)) (numeral w))" @@ -1171,7 +1174,7 @@ lemma ucast_1 [simp]: "ucast (1::'a::len word) = 1" by (simp add: ucast_def) -(* now, to get the weaker results analogous to word_div/mod_def *) +\ \now, to get the weaker results analogous to \word_div\/\mod_def\\ subsection \Transferring goals from words to ints\ @@ -1244,7 +1247,7 @@ "word_succ (- 1) = 0 \ word_succ 0 = 1 \ word_pred 0 = - 1 \ word_pred 1 = 0" by (simp_all add: word_succ_p1 word_pred_m1) -(* alternative approach to lifting arithmetic equalities *) +\ \alternative approach to lifting arithmetic equalities\ lemma word_of_int_Ex: "\y. x = word_of_int y" by (rule_tac x="uint x" in exI) simp @@ -1421,11 +1424,11 @@ word_uint.Rep_inject [symmetric] uint_sub_if' uint_plus_if' -(* use this to stop, eg, 2 ^ len_of TYPE(32) being simplified *) +\ \use this to stop, eg. \2 ^ len_of TYPE(32)\ being simplified\ lemma power_False_cong: "False \ a ^ b = c ^ d" by auto -(* uint_arith_tac: reduce to arithmetic on int, try to solve by arith *) +\ \\uint_arith_tac\: reduce to arithmetic on int, try to solve by arith\ ML \ fun uint_arith_simpset ctxt = ctxt addsimps @{thms uint_arith_simps} @@ -1641,7 +1644,7 @@ apply simp done -(* links with rbl operations *) +\ \links with \rbl\ operations\ lemma word_succ_rbl: "to_bl w = bl \ to_bl (word_succ w) = rev (rbl_succ (rev bl))" apply (unfold word_succ_def) apply clarify @@ -1690,8 +1693,10 @@ lemma word_of_int_nat: "0 \ x \ word_of_int x = of_nat (nat x)" by (simp add: word_of_int) -(* note that iszero_def is only for class comm_semiring_1_cancel, - which requires word length >= 1, ie 'a::len word *) +text \ + note that \iszero_def\ is only for class \comm_semiring_1_cancel\, + which requires word length \\ 1\, ie \'a::len word\ +\ lemma iszero_word_no [simp]: "iszero (numeral bin :: 'a::len word) = iszero (bintrunc (len_of TYPE('a)) (numeral bin))" @@ -1907,8 +1912,7 @@ word_unat.Rep_inject [symmetric] unat_sub_if' unat_plus_if' unat_div unat_mod -(* unat_arith_tac: tactic to reduce word arithmetic to nat, - try to solve via arith *) +\ \\unat_arith_tac\: tactic to reduce word arithmetic to \nat\, try to solve via \arith\\ ML \ fun unat_arith_simpset ctxt = ctxt addsimps @{thms unat_arith_simps} @@ -2087,14 +2091,13 @@ lemmas bin_log_bintrs = bin_trunc_not bin_trunc_xor bin_trunc_and bin_trunc_or -(* following definitions require both arithmetic and bit-wise word operations *) - -(* to get word_no_log_defs from word_log_defs, using bin_log_bintrs *) +\ \following definitions require both arithmetic and bit-wise word operations\ + +\ \to get \word_no_log_defs\ from \word_log_defs\, using \bin_log_bintrs\\ lemmas wils1 = bin_log_bintrs [THEN word_ubin.norm_eq_iff [THEN iffD1], folded word_ubin.eq_norm, THEN eq_reflection] -(* the binary operations only *) -(* BH: why is this needed? *) +\ \the binary operations only\ (* BH: why is this needed? *) lemmas word_log_binary_defs = word_and_def word_or_def word_xor_def @@ -2201,9 +2204,7 @@ lemma nth_minus1 [simp]: "(-1 :: 'a::len0 word) !! n \ n < len_of TYPE('a)" by transfer simp -(* get from commutativity, associativity etc of int_and etc - to same for word_and etc *) - +\ \get from commutativity, associativity etc of \int_and\ etc to same for \word_and etc\\ lemmas bwsimps = wi_hom_add word_wi_log_defs @@ -2670,9 +2671,11 @@ apply (auto simp add: nth_shiftr1) done -(* see paper page 10, (1), (2), shiftr1_def is of the form of (1), - where f (ie bin_rest) takes normal arguments to normal results, - thus we get (2) from (1) *) +text \ + see paper page 10, (1), (2), \shiftr1_def\ is of the form of (1), + where \f\ (ie \bin_rest\) takes normal arguments to normal results, + thus we get (2) from (1) +\ lemma uint_shiftr1: "uint (shiftr1 w) = bin_rest (uint w)" apply (unfold shiftr1_def word_ubin.eq_norm bin_rest_trunc_i) @@ -2774,7 +2777,7 @@ for w :: "'a::len word" by (simp add: shiftl1_bl word_rep_drop drop_Suc drop_Cons') (fast intro!: Suc_leI) -(* Generalized version of bl_shiftl1. Maybe this one should replace it? *) +\ \Generalized version of \bl_shiftl1\. Maybe this one should replace it?\ lemma bl_shiftl1': "to_bl (shiftl1 w) = tl (to_bl w @ [False])" by (simp add: shiftl1_bl word_rep_drop drop_Suc del: drop_append) @@ -2788,7 +2791,7 @@ for w :: "'a::len word" by (simp add: shiftr1_bl word_rep_drop len_gt_0 [THEN Suc_leI]) -(* Generalized version of bl_shiftr1. Maybe this one should replace it? *) +\ \Generalized version of \bl_shiftr1\. Maybe this one should replace it?\ lemma bl_shiftr1': "to_bl (shiftr1 w) = butlast (False # to_bl w)" apply (rule word_bl.Abs_inverse') apply (simp del: butlast.simps) @@ -2909,7 +2912,7 @@ apply (clarsimp simp add: shiftl_bl word_size test_bit_of_bl nth_append) done -(* note - the following results use 'a::len word < number_ring *) +\ \note -- the following results use \'a::len word < number_ring\\ lemma shiftl1_2t: "shiftl1 w = 2 * w" for w :: "'a::len word" @@ -3719,7 +3722,7 @@ lemmas length_word_rsplit_exp_size' = refl [THEN length_word_rsplit_exp_size] -(* alternative proof of word_rcat_rsplit *) +\ \alternative proof of \word_rcat_rsplit\\ lemmas tdle = times_div_less_eq_dividend lemmas dtle = xtr4 [OF tdle mult.commute] @@ -4047,7 +4050,7 @@ subsubsection \"Word rotation commutes with bit-wise operations\ -(* using locale to not pollute lemma namespace *) +\ \using locale to not pollute lemma namespace\ locale word_rotate begin diff -r dbaa38bd223a -r 4a4c14b24800 src/HOL/Word/Word_Miscellaneous.thy --- a/src/HOL/Word/Word_Miscellaneous.thy Fri Jan 12 14:43:06 2018 +0100 +++ b/src/HOL/Word/Word_Miscellaneous.thy Fri Jan 12 15:27:46 2018 +0100 @@ -95,8 +95,7 @@ lemma if_same_eq_not: "(If p x y = (\ If p u v)) = (if p then x = (\ u) else y = (\ v))" by auto -(* note - if_Cons can cause blowup in the size, if p is complex, - so make a simproc *) +\ \note -- \if_Cons\ can cause blowup in the size, if \p\ is complex, so make a simproc\ lemma if_Cons: "(if p then x # xs else y # ys) = If p x y # If p xs ys" by auto