--- a/src/HOL/BNF_Cardinal_Order_Relation.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/BNF_Cardinal_Order_Relation.thy Mon Dec 07 10:38:04 2015 +0100
@@ -19,7 +19,7 @@
\item standard set-theoretic constructions: products,
sums, unions, lists, powersets, set-of finite sets operator;
\item finiteness and infiniteness (in particular, with the numeric cardinal operator
-for finite sets, @{text "card"}, from the theory @{text "Finite_Sets.thy"}).
+for finite sets, \<open>card\<close>, from the theory \<open>Finite_Sets.thy\<close>).
\end{itemize}
%
On the way, we define the canonical $\omega$ cardinal and finite cardinals. We also
@@ -37,8 +37,8 @@
subsection \<open>Cardinal orders\<close>
text\<open>A cardinal order in our setting shall be a well-order {\em minim} w.r.t. the
-order-embedding relation, @{text "\<le>o"} (which is the same as being {\em minimal} w.r.t. the
-strict order-embedding relation, @{text "<o"}), among all the well-orders on its field.\<close>
+order-embedding relation, \<open>\<le>o\<close> (which is the same as being {\em minimal} w.r.t. the
+strict order-embedding relation, \<open><o\<close>), among all the well-orders on its field.\<close>
definition card_order_on :: "'a set \<Rightarrow> 'a rel \<Rightarrow> bool"
where
@@ -59,9 +59,9 @@
text\<open>The existence of a cardinal relation on any given set (which will mean
that any set has a cardinal) follows from two facts:
\begin{itemize}
-\item Zermelo's theorem (proved in @{text "Zorn.thy"} as theorem @{text "well_order_on"}),
+\item Zermelo's theorem (proved in \<open>Zorn.thy\<close> as theorem \<open>well_order_on\<close>),
which states that on any given set there exists a well-order;
-\item The well-founded-ness of @{text "<o"}, ensuring that then there exists a minimal
+\item The well-founded-ness of \<open><o\<close>, ensuring that then there exists a minimal
such well-order, i.e., a cardinal order.
\end{itemize}
\<close>
@@ -348,7 +348,7 @@
text\<open>Here we embark in a long journey of simple results showing
that the standard set-theoretic operations are well-behaved w.r.t. the notion of
cardinal -- essentially, this means that they preserve the ``cardinal identity"
-@{text "=o"} and are monotonic w.r.t. @{text "\<le>o"}.
+\<open>=o\<close> and are monotonic w.r.t. \<open>\<le>o\<close>.
\<close>
lemma card_of_empty: "|{}| \<le>o |A|"
@@ -823,7 +823,7 @@
text\<open>Here we show that, for infinite sets, most set-theoretic constructions
do not increase the cardinality. The cornerstone for this is
-theorem @{text "Card_order_Times_same_infinite"}, which states that self-product
+theorem \<open>Card_order_Times_same_infinite\<close>, which states that self-product
does not increase cardinality -- the proof of this fact adapts a standard
set-theoretic argument, as presented, e.g., in the proof of theorem 1.5.11
at page 47 in @{cite "card-book"}. Then everything else follows fairly easily.\<close>
@@ -1144,9 +1144,9 @@
text\<open>The cardinal $\omega$, of natural numbers, shall be the standard non-strict
order relation on
-@{text "nat"}, that we abbreviate by @{text "natLeq"}. The finite cardinals
+\<open>nat\<close>, that we abbreviate by \<open>natLeq\<close>. The finite cardinals
shall be the restrictions of these relations to the numbers smaller than
-fixed numbers @{text "n"}, that we abbreviate by @{text "natLeq_on n"}.\<close>
+fixed numbers \<open>n\<close>, that we abbreviate by \<open>natLeq_on n\<close>.\<close>
definition "(natLeq::(nat * nat) set) \<equiv> {(x,y). x \<le> y}"
definition "(natLess::(nat * nat) set) \<equiv> {(x,y). x < y}"
@@ -1260,9 +1260,9 @@
subsection \<open>The successor of a cardinal\<close>
-text\<open>First we define @{text "isCardSuc r r'"}, the notion of @{text "r'"}
-being a successor cardinal of @{text "r"}. Although the definition does
-not require @{text "r"} to be a cardinal, only this case will be meaningful.\<close>
+text\<open>First we define \<open>isCardSuc r r'\<close>, the notion of \<open>r'\<close>
+being a successor cardinal of \<open>r\<close>. Although the definition does
+not require \<open>r\<close> to be a cardinal, only this case will be meaningful.\<close>
definition isCardSuc :: "'a rel \<Rightarrow> 'a set rel \<Rightarrow> bool"
where
@@ -1270,8 +1270,8 @@
Card_order r' \<and> r <o r' \<and>
(\<forall>(r''::'a set rel). Card_order r'' \<and> r <o r'' \<longrightarrow> r' \<le>o r'')"
-text\<open>Now we introduce the cardinal-successor operator @{text "cardSuc"},
-by picking {\em some} cardinal-order relation fulfilling @{text "isCardSuc"}.
+text\<open>Now we introduce the cardinal-successor operator \<open>cardSuc\<close>,
+by picking {\em some} cardinal-order relation fulfilling \<open>isCardSuc\<close>.
Again, the picked item shall be proved unique up to order-isomorphism.\<close>
definition cardSuc :: "'a rel \<Rightarrow> 'a set rel"
@@ -1312,8 +1312,8 @@
"Card_order r \<Longrightarrow> r \<le>o cardSuc r"
using cardSuc_greater ordLeq_iff_ordLess_or_ordIso by blast
-text\<open>The minimality property of @{text "cardSuc"} originally present in its definition
-is local to the type @{text "'a set rel"}, i.e., that of @{text "cardSuc r"}:\<close>
+text\<open>The minimality property of \<open>cardSuc\<close> originally present in its definition
+is local to the type \<open>'a set rel\<close>, i.e., that of \<open>cardSuc r\<close>:\<close>
lemma cardSuc_least_aux:
"\<lbrakk>Card_order (r::'a rel); Card_order (r'::'a set rel); r <o r'\<rbrakk> \<Longrightarrow> cardSuc r \<le>o r'"
--- a/src/HOL/BNF_Wellorder_Constructions.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/BNF_Wellorder_Constructions.thy Mon Dec 07 10:38:04 2015 +0100
@@ -14,11 +14,11 @@
text \<open>In this section, we study basic constructions on well-orders, such as restriction to
a set/order filter, copy via direct images, ordinal-like sum of disjoint well-orders,
and bounded square. We also define between well-orders
-the relations @{text "ordLeq"}, of being embedded (abbreviated @{text "\<le>o"}),
-@{text "ordLess"}, of being strictly embedded (abbreviated @{text "<o"}), and
-@{text "ordIso"}, of being isomorphic (abbreviated @{text "=o"}). We study the
+the relations \<open>ordLeq\<close>, of being embedded (abbreviated \<open>\<le>o\<close>),
+\<open>ordLess\<close>, of being strictly embedded (abbreviated \<open><o\<close>), and
+\<open>ordIso\<close>, of being isomorphic (abbreviated \<open>=o\<close>). We study the
connections between these relations, order filters, and the aforementioned constructions.
-A main result of this section is that @{text "<o"} is well-founded.\<close>
+A main result of this section is that \<open><o\<close> is well-founded.\<close>
subsection \<open>Restriction to a set\<close>
@@ -306,14 +306,14 @@
text \<open>We define three relations between well-orders:
\begin{itemize}
-\item @{text "ordLeq"}, of being embedded (abbreviated @{text "\<le>o"});
-\item @{text "ordLess"}, of being strictly embedded (abbreviated @{text "<o"});
-\item @{text "ordIso"}, of being isomorphic (abbreviated @{text "=o"}).
+\item \<open>ordLeq\<close>, of being embedded (abbreviated \<open>\<le>o\<close>);
+\item \<open>ordLess\<close>, of being strictly embedded (abbreviated \<open><o\<close>);
+\item \<open>ordIso\<close>, of being isomorphic (abbreviated \<open>=o\<close>).
\end{itemize}
%
The prefix "ord" and the index "o" in these names stand for "ordinal-like".
These relations shall be proved to be inter-connected in a similar fashion as the trio
-@{text "\<le>"}, @{text "<"}, @{text "="} associated to a total order on a set.
+\<open>\<le>\<close>, \<open><\<close>, \<open>=\<close> associated to a total order on a set.
\<close>
definition ordLeq :: "('a rel * 'a' rel) set"
@@ -347,10 +347,10 @@
shows "Well_order r \<and> Well_order r'"
using assms unfolding ordLeq_def by simp
-text\<open>Notice that the relations @{text "\<le>o"}, @{text "<o"}, @{text "=o"} connect well-orders
+text\<open>Notice that the relations \<open>\<le>o\<close>, \<open><o\<close>, \<open>=o\<close> connect well-orders
on potentially {\em distinct} types. However, some of the lemmas below, including the next one,
-restrict implicitly the type of these relations to @{text "(('a rel) * ('a rel)) set"} , i.e.,
-to @{text "'a rel rel"}.\<close>
+restrict implicitly the type of these relations to \<open>(('a rel) * ('a rel)) set\<close> , i.e.,
+to \<open>'a rel rel\<close>.\<close>
lemma ordLeq_reflexive:
"Well_order r \<Longrightarrow> r \<le>o r"
@@ -822,12 +822,12 @@
ultimately show ?thesis using assms ordLeq_total ordIso_symmetric by blast
qed
-subsection\<open>@{text "<o"} is well-founded\<close>
+subsection\<open>\<open><o\<close> is well-founded\<close>
-text \<open>Of course, it only makes sense to state that the @{text "<o"} is well-founded
-on the restricted type @{text "'a rel rel"}. We prove this by first showing that, for any set
+text \<open>Of course, it only makes sense to state that the \<open><o\<close> is well-founded
+on the restricted type \<open>'a rel rel\<close>. We prove this by first showing that, for any set
of well-orders all embedded in a fixed well-order, the function mapping each well-order
-in the set to an order filter of the fixed well-order is compatible w.r.t. to @{text "<o"} versus
+in the set to an order filter of the fixed well-order is compatible w.r.t. to \<open><o\<close> versus
{\em strict inclusion}; and we already know that strict inclusion of order filters is well-founded.\<close>
definition ord_to_filter :: "'a rel \<Rightarrow> 'a rel \<Rightarrow> 'a set"
@@ -885,8 +885,8 @@
subsection \<open>Copy via direct images\<close>
-text\<open>The direct image operator is the dual of the inverse image operator @{text "inv_image"}
-from @{text "Relation.thy"}. It is useful for transporting a well-order between
+text\<open>The direct image operator is the dual of the inverse image operator \<open>inv_image\<close>
+from \<open>Relation.thy\<close>. It is useful for transporting a well-order between
different types.\<close>
definition dir_image :: "'a rel \<Rightarrow> ('a \<Rightarrow> 'a') \<Rightarrow> 'a' rel"
@@ -1045,8 +1045,8 @@
subsection \<open>Bounded square\<close>
-text\<open>This construction essentially defines, for an order relation @{text "r"}, a lexicographic
-order @{text "bsqr r"} on @{text "(Field r) \<times> (Field r)"}, applying the
+text\<open>This construction essentially defines, for an order relation \<open>r\<close>, a lexicographic
+order \<open>bsqr r\<close> on \<open>(Field r) \<times> (Field r)\<close>, applying the
following criteria (in this order):
\begin{itemize}
\item compare the maximums;
--- a/src/HOL/BNF_Wellorder_Embedding.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/BNF_Wellorder_Embedding.thy Mon Dec 07 10:38:04 2015 +0100
@@ -60,13 +60,13 @@
text\<open>Standardly, a function is an embedding of a well-order in another if it injectively and
order-compatibly maps the former into an order filter of the latter.
-Here we opt for a more succinct definition (operator @{text "embed"}),
+Here we opt for a more succinct definition (operator \<open>embed\<close>),
asking that, for any element in the source, the function should be a bijection
between the set of strict lower bounds of that element
and the set of strict lower bounds of its image. (Later we prove equivalence with
-the standard definition -- lemma @{text "embed_iff_compat_inj_on_ofilter"}.)
-A {\em strict embedding} (operator @{text "embedS"}) is a non-bijective embedding
-and an isomorphism (operator @{text "iso"}) is a bijective embedding.\<close>
+the standard definition -- lemma \<open>embed_iff_compat_inj_on_ofilter\<close>.)
+A {\em strict embedding} (operator \<open>embedS\<close>) is a non-bijective embedding
+and an isomorphism (operator \<open>iso\<close>) is a bijective embedding.\<close>
definition embed :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> ('a \<Rightarrow> 'a') \<Rightarrow> bool"
where
@@ -151,7 +151,7 @@
using assms unfolding iso_def
by (auto simp add: comp_embed bij_betw_trans)
-text\<open>That @{text "embedS"} is also preserved by function composition shall be proved only later.\<close>
+text\<open>That \<open>embedS\<close> is also preserved by function composition shall be proved only later.\<close>
lemma embed_Field:
"\<lbrakk>Well_order r; embed r r' f\<rbrakk> \<Longrightarrow> f`(Field r) \<le> Field r'"
@@ -454,22 +454,22 @@
subsection \<open>Given any two well-orders, one can be embedded in the other\<close>
text\<open>Here is an overview of the proof of of this fact, stated in theorem
-@{text "wellorders_totally_ordered"}:
+\<open>wellorders_totally_ordered\<close>:
- Fix the well-orders @{text "r::'a rel"} and @{text "r'::'a' rel"}.
- Attempt to define an embedding @{text "f::'a \<Rightarrow> 'a'"} from @{text "r"} to @{text "r'"} in the
- natural way by well-order recursion ("hoping" that @{text "Field r"} turns out to be smaller
- than @{text "Field r'"}), but also record, at the recursive step, in a function
- @{text "g::'a \<Rightarrow> bool"}, the extra information of whether @{text "Field r'"}
+ Fix the well-orders \<open>r::'a rel\<close> and \<open>r'::'a' rel\<close>.
+ Attempt to define an embedding \<open>f::'a \<Rightarrow> 'a'\<close> from \<open>r\<close> to \<open>r'\<close> in the
+ natural way by well-order recursion ("hoping" that \<open>Field r\<close> turns out to be smaller
+ than \<open>Field r'\<close>), but also record, at the recursive step, in a function
+ \<open>g::'a \<Rightarrow> bool\<close>, the extra information of whether \<open>Field r'\<close>
gets exhausted or not.
- If @{text "Field r'"} does not get exhausted, then @{text "Field r"} is indeed smaller
- and @{text "f"} is the desired embedding from @{text "r"} to @{text "r'"}
- (lemma @{text "wellorders_totally_ordered_aux"}).
+ If \<open>Field r'\<close> does not get exhausted, then \<open>Field r\<close> is indeed smaller
+ and \<open>f\<close> is the desired embedding from \<open>r\<close> to \<open>r'\<close>
+ (lemma \<open>wellorders_totally_ordered_aux\<close>).
- Otherwise, it means that @{text "Field r'"} is the smaller one, and the inverse of
- (the "good" segment of) @{text "f"} is the desired embedding from @{text "r'"} to @{text "r"}
- (lemma @{text "wellorders_totally_ordered_aux2"}).
+ Otherwise, it means that \<open>Field r'\<close> is the smaller one, and the inverse of
+ (the "good" segment of) \<open>f\<close> is the desired embedding from \<open>r'\<close> to \<open>r\<close>
+ (lemma \<open>wellorders_totally_ordered_aux2\<close>).
\<close>
lemma wellorders_totally_ordered_aux:
--- a/src/HOL/BNF_Wellorder_Relation.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/BNF_Wellorder_Relation.thy Mon Dec 07 10:38:04 2015 +0100
@@ -117,10 +117,10 @@
text\<open>
We define the successor {\em of a set}, and not of an element (the latter is of course
-a particular case). Also, we define the maximum {\em of two elements}, @{text "max2"},
-and the minimum {\em of a set}, @{text "minim"} -- we chose these variants since we
+a particular case). Also, we define the maximum {\em of two elements}, \<open>max2\<close>,
+and the minimum {\em of a set}, \<open>minim\<close> -- we chose these variants since we
consider them the most useful for well-orders. The minimum is defined in terms of the
-auxiliary relational operator @{text "isMinim"}. Then, supremum and successor are
+auxiliary relational operator \<open>isMinim\<close>. Then, supremum and successor are
defined in terms of minimum as expected.
The minimum is only meaningful for non-empty sets, and the successor is only
meaningful for sets for which strict upper bounds exist.
--- a/src/HOL/Binomial.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Binomial.thy Mon Dec 07 10:38:04 2015 +0100
@@ -146,7 +146,7 @@
by (induct r rule: nat.induct) (auto simp add: fact_div_fact Suc_diff_Suc mult_le_mono)
qed
-lemma fact_numeral: --\<open>Evaluation for specific numerals\<close>
+lemma fact_numeral: \<comment>\<open>Evaluation for specific numerals\<close>
"fact (numeral k) = (numeral k) * (fact (pred_numeral k))"
by (metis fact.simps(2) numeral_eq_Suc of_nat_numeral)
@@ -230,7 +230,7 @@
by (auto split add: nat_diff_split)
-subsection \<open>Combinatorial theorems involving @{text "choose"}\<close>
+subsection \<open>Combinatorial theorems involving \<open>choose\<close>\<close>
text \<open>By Florian Kamm\"uller, tidied by LCP.\<close>
@@ -890,7 +890,7 @@
by (subst setsum_right_distrib, rule setsum.cong[OF refl], subst Suc_times_binomial)
(simp add: algebra_simps of_nat_mult)
also have "(\<Sum>i\<le>m. (-1 :: 'a) ^ i * of_nat ((m choose i))) = 0"
- using choose_alternating_sum[OF `m > 0`] by simp
+ using choose_alternating_sum[OF \<open>m > 0\<close>] by simp
finally show ?thesis by simp
qed simp
@@ -1266,7 +1266,7 @@
text\<open>Versions of the theorems above for the natural-number version of "choose"\<close>
lemma binomial_altdef_of_nat:
fixes n k :: nat
- and x :: "'a :: {field_char_0,field}" --\<open>the point is to constrain @{typ 'a}\<close>
+ and x :: "'a :: {field_char_0,field}" \<comment>\<open>the point is to constrain @{typ 'a}\<close>
assumes "k \<le> n"
shows "of_nat (n choose k) = (\<Prod>i<k. of_nat (n - i) / of_nat (k - i) :: 'a)"
using assms
@@ -1426,7 +1426,7 @@
finally show ?thesis ..
qed
-text\<open>The number of nat lists of length @{text m} summing to @{text N} is
+text\<open>The number of nat lists of length \<open>m\<close> summing to \<open>N\<close> is
@{term "(N + m - 1) choose N"}:\<close>
lemma card_length_listsum_rec:
@@ -1473,7 +1473,7 @@
finally show ?thesis .
qed
-lemma card_length_listsum: --"By Holden Lee, tidied by Tobias Nipkow"
+lemma card_length_listsum: \<comment>"By Holden Lee, tidied by Tobias Nipkow"
"card {l::nat list. size l = m \<and> listsum l = N} = (N + m - 1) choose N"
proof (cases m)
case 0 then show ?thesis
@@ -1483,7 +1483,7 @@
have m: "m\<ge>1" by (simp add: Suc)
then show ?thesis
proof (induct "N + m - 1" arbitrary: N m)
- case 0 -- "In the base case, the only solution is [0]."
+ case 0 \<comment> "In the base case, the only solution is [0]."
have [simp]: "{l::nat list. length l = Suc 0 \<and> (\<forall>n\<in>set l. n = 0)} = {[0]}"
by (auto simp: length_Suc_conv)
have "m=1 \<and> N=0" using 0 by linarith
@@ -1519,7 +1519,7 @@
qed
-lemma Suc_times_binomial_add: -- \<open>by Lukas Bulwahn\<close>
+lemma Suc_times_binomial_add: \<comment> \<open>by Lukas Bulwahn\<close>
"Suc a * (Suc (a + b) choose Suc a) = Suc b * (Suc (a + b) choose a)"
proof -
have dvd: "Suc a * (fact a * fact b) dvd fact (Suc (a + b))" for a b
--- a/src/HOL/Code_Evaluation.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Code_Evaluation.thy Mon Dec 07 10:38:04 2015 +0100
@@ -11,7 +11,7 @@
subsection \<open>Term representation\<close>
-subsubsection \<open>Terms and class @{text term_of}\<close>
+subsubsection \<open>Terms and class \<open>term_of\<close>\<close>
datatype (plugins only: code extraction) "term" = dummy_term
@@ -87,7 +87,7 @@
ML_file "~~/src/HOL/Tools/value.ML"
-subsection \<open>@{text term_of} instances\<close>
+subsection \<open>\<open>term_of\<close> instances\<close>
instantiation "fun" :: (typerep, typerep) term_of
begin
--- a/src/HOL/Complete_Lattices.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Complete_Lattices.thy Mon Dec 07 10:38:04 2015 +0100
@@ -81,7 +81,7 @@
text \<open>
Note: must use names @{const INFIMUM} and @{const SUPREMUM} here instead of
- @{text INF} and @{text SUP} to allow the following syntax coexist
+ \<open>INF\<close> and \<open>SUP\<close> to allow the following syntax coexist
with the plain constant names.
\<close>
@@ -110,7 +110,7 @@
print_translation \<open>
[Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax INFIMUM} @{syntax_const "_INF"},
Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax SUPREMUM} @{syntax_const "_SUP"}]
-\<close> -- \<open>to avoid eta-contraction of body\<close>
+\<close> \<comment> \<open>to avoid eta-contraction of body\<close>
subsection \<open>Abstract complete lattices\<close>
@@ -274,7 +274,7 @@
lemma INF_superset_mono:
"B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> f x \<sqsubseteq> g x) \<Longrightarrow> (\<Sqinter>x\<in>A. f x) \<sqsubseteq> (\<Sqinter>x\<in>B. g x)"
- -- \<open>The last inclusion is POSITIVE!\<close>
+ \<comment> \<open>The last inclusion is POSITIVE!\<close>
by (blast intro: INF_mono dest: subsetD)
lemma SUP_subset_mono:
@@ -926,14 +926,14 @@
text \<open>
\medskip A ``destruct'' rule -- every @{term X} in @{term C}
contains @{term A} as an element, but @{prop "A \<in> X"} can hold when
- @{prop "X \<in> C"} does not! This rule is analogous to @{text spec}.
+ @{prop "X \<in> C"} does not! This rule is analogous to \<open>spec\<close>.
\<close>
lemma InterD [elim, Pure.elim]: "A \<in> \<Inter>C \<Longrightarrow> X \<in> C \<Longrightarrow> A \<in> X"
by auto
lemma InterE [elim]: "A \<in> \<Inter>C \<Longrightarrow> (X \<notin> C \<Longrightarrow> R) \<Longrightarrow> (A \<in> X \<Longrightarrow> R) \<Longrightarrow> R"
- -- \<open>``Classical'' elimination rule -- does not require proving
+ \<comment> \<open>``Classical'' elimination rule -- does not require proving
@{prop "X \<in> C"}.\<close>
by (unfold Inter_eq) blast
@@ -977,7 +977,7 @@
"INTER \<equiv> INFIMUM"
text \<open>
- Note: must use name @{const INTER} here instead of @{text INT}
+ Note: must use name @{const INTER} here instead of \<open>INT\<close>
to allow the following syntax coexist with the plain constant name.
\<close>
@@ -1001,7 +1001,7 @@
print_translation \<open>
[Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax INTER} @{syntax_const "_INTER"}]
-\<close> -- \<open>to avoid eta-contraction of body\<close>
+\<close> \<comment> \<open>to avoid eta-contraction of body\<close>
lemma INTER_eq:
"(\<Inter>x\<in>A. B x) = {y. \<forall>x\<in>A. y \<in> B x}"
@@ -1021,7 +1021,7 @@
by auto
lemma INT_E [elim]: "b \<in> (\<Inter>x\<in>A. B x) \<Longrightarrow> (b \<in> B a \<Longrightarrow> R) \<Longrightarrow> (a \<notin> A \<Longrightarrow> R) \<Longrightarrow> R"
- -- \<open>"Classical" elimination -- by the Excluded Middle on @{prop "a\<in>A"}.\<close>
+ \<comment> \<open>"Classical" elimination -- by the Excluded Middle on @{prop "a\<in>A"}.\<close>
by (auto simp add: INF_def image_def)
lemma Collect_ball_eq: "{x. \<forall>y\<in>A. P x y} = (\<Inter>y\<in>A. {x. P x y})"
@@ -1068,7 +1068,7 @@
lemma INT_anti_mono:
"A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<subseteq> g x) \<Longrightarrow> (\<Inter>x\<in>B. f x) \<subseteq> (\<Inter>x\<in>A. g x)"
- -- \<open>The last inclusion is POSITIVE!\<close>
+ \<comment> \<open>The last inclusion is POSITIVE!\<close>
by (fact INF_superset_mono)
lemma Pow_INT_eq: "Pow (\<Inter>x\<in>A. B x) = (\<Inter>x\<in>A. Pow (B x))"
@@ -1102,7 +1102,7 @@
lemma UnionI [intro]:
"X \<in> C \<Longrightarrow> A \<in> X \<Longrightarrow> A \<in> \<Union>C"
- -- \<open>The order of the premises presupposes that @{term C} is rigid;
+ \<comment> \<open>The order of the premises presupposes that @{term C} is rigid;
@{term A} may be flexible.\<close>
by auto
@@ -1153,7 +1153,7 @@
"UNION \<equiv> SUPREMUM"
text \<open>
- Note: must use name @{const UNION} here instead of @{text UN}
+ Note: must use name @{const UNION} here instead of \<open>UN\<close>
to allow the following syntax coexist with the plain constant name.
\<close>
@@ -1177,7 +1177,7 @@
text \<open>
Note the difference between ordinary xsymbol syntax of indexed
- unions and intersections (e.g.\ @{text"\<Union>a\<^sub>1\<in>A\<^sub>1. B"})
+ unions and intersections (e.g.\ \<open>\<Union>a\<^sub>1\<in>A\<^sub>1. B\<close>)
and their \LaTeX\ rendition: @{term"\<Union>a\<^sub>1\<in>A\<^sub>1. B"}. The
former does not make the index expression a subscript of the
union/intersection symbol because this leads to problems with nested
@@ -1186,7 +1186,7 @@
print_translation \<open>
[Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax UNION} @{syntax_const "_UNION"}]
-\<close> -- \<open>to avoid eta-contraction of body\<close>
+\<close> \<comment> \<open>to avoid eta-contraction of body\<close>
lemma UNION_eq:
"(\<Union>x\<in>A. B x) = {y. \<exists>x\<in>A. y \<in> B x}"
@@ -1211,7 +1211,7 @@
using Union_iff [of _ "B ` A"] by simp
lemma UN_I [intro]: "a \<in> A \<Longrightarrow> b \<in> B a \<Longrightarrow> b \<in> (\<Union>x\<in>A. B x)"
- -- \<open>The order of the premises presupposes that @{term A} is rigid;
+ \<comment> \<open>The order of the premises presupposes that @{term A} is rigid;
@{term b} may be flexible.\<close>
by auto
@@ -1295,7 +1295,7 @@
by blast
lemma vimage_eq_UN: "f -` B = (\<Union>y\<in>B. f -` {y})"
- -- \<open>NOT suitable for rewriting\<close>
+ \<comment> \<open>NOT suitable for rewriting\<close>
by blast
lemma image_UN: "f ` UNION A B = (\<Union>x\<in>A. f ` B x)"
@@ -1322,19 +1322,19 @@
lemma UN_Un_distrib: "(\<Union>i\<in>I. A i \<union> B i) = (\<Union>i\<in>I. A i) \<union> (\<Union>i\<in>I. B i)"
by (rule sym) (rule SUP_sup_distrib)
-lemma Int_Inter_image: "(\<Inter>x\<in>C. A x \<inter> B x) = \<Inter>(A ` C) \<inter> \<Inter>(B ` C)" -- \<open>FIXME drop\<close>
+lemma Int_Inter_image: "(\<Inter>x\<in>C. A x \<inter> B x) = \<Inter>(A ` C) \<inter> \<Inter>(B ` C)" \<comment> \<open>FIXME drop\<close>
by (simp add: INT_Int_distrib)
-lemma Un_Union_image: "(\<Union>x\<in>C. A x \<union> B x) = \<Union>(A ` C) \<union> \<Union>(B ` C)" -- \<open>FIXME drop\<close>
- -- \<open>Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5:\<close>
- -- \<open>Union of a family of unions\<close>
+lemma Un_Union_image: "(\<Union>x\<in>C. A x \<union> B x) = \<Union>(A ` C) \<union> \<Union>(B ` C)" \<comment> \<open>FIXME drop\<close>
+ \<comment> \<open>Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5:\<close>
+ \<comment> \<open>Union of a family of unions\<close>
by (simp add: UN_Un_distrib)
lemma Un_INT_distrib: "B \<union> (\<Inter>i\<in>I. A i) = (\<Inter>i\<in>I. B \<union> A i)"
by (fact sup_INF)
lemma Int_UN_distrib: "B \<inter> (\<Union>i\<in>I. A i) = (\<Union>i\<in>I. B \<inter> A i)"
- -- \<open>Halmos, Naive Set Theory, page 35.\<close>
+ \<comment> \<open>Halmos, Naive Set Theory, page 35.\<close>
by (fact inf_SUP)
lemma Int_UN_distrib2: "(\<Union>i\<in>I. A i) \<inter> (\<Union>j\<in>J. B j) = (\<Union>i\<in>I. \<Union>j\<in>J. A i \<inter> B j)"
@@ -1516,7 +1516,7 @@
lemmas mem_simps =
insert_iff empty_iff Un_iff Int_iff Compl_iff Diff_iff
mem_Collect_eq UN_iff Union_iff INT_iff Inter_iff
- -- \<open>Each of these has ALREADY been added @{text "[simp]"} above.\<close>
+ \<comment> \<open>Each of these has ALREADY been added \<open>[simp]\<close> above.\<close>
end
--- a/src/HOL/Complex.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Complex.thy Mon Dec 07 10:38:04 2015 +0100
@@ -11,8 +11,8 @@
begin
text \<open>
-We use the @{text codatatype} command to define the type of complex numbers. This allows us to use
-@{text primcorec} to define complex functions by defining their real and imaginary result
+We use the \<open>codatatype\<close> command to define the type of complex numbers. This allows us to use
+\<open>primcorec\<close> to define complex functions by defining their real and imaginary result
separately.
\<close>
--- a/src/HOL/Deriv.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Deriv.thy Mon Dec 07 10:38:04 2015 +0100
@@ -444,7 +444,7 @@
text \<open>
This can not generally shown for @{const has_derivative}, as we need to approach the point from
-all directions. There is a proof in @{text Multivariate_Analysis} for @{text euclidean_space}.
+all directions. There is a proof in \<open>Multivariate_Analysis\<close> for \<open>euclidean_space\<close>.
\<close>
@@ -800,7 +800,7 @@
by (auto intro: has_derivative_imp_has_field_derivative has_derivative_inverse)
qed
-text \<open>Power of @{text "-1"}\<close>
+text \<open>Power of \<open>-1\<close>\<close>
lemma DERIV_inverse:
"x \<noteq> 0 \<Longrightarrow> ((\<lambda>x. inverse(x)) has_field_derivative - (inverse x ^ Suc (Suc 0))) (at x within s)"
@@ -1079,9 +1079,9 @@
text\<open>Rolle's Theorem.
If @{term f} is defined and continuous on the closed interval
- @{text "[a,b]"} and differentiable on the open interval @{text "(a,b)"},
+ \<open>[a,b]\<close> and differentiable on the open interval \<open>(a,b)\<close>,
and @{term "f(a) = f(b)"},
- then there exists @{text "x0 \<in> (a,b)"} such that @{term "f'(x0) = 0"}\<close>
+ then there exists \<open>x0 \<in> (a,b)\<close> such that @{term "f'(x0) = 0"}\<close>
theorem Rolle:
assumes lt: "a < b"
and eq: "f(a) = f(b)"
@@ -1101,7 +1101,7 @@
show ?thesis
proof cases
assume axb: "a < x & x < b"
- --\<open>@{term f} attains its maximum within the interval\<close>
+ \<comment>\<open>@{term f} attains its maximum within the interval\<close>
hence ax: "a<x" and xb: "x<b" by arith +
from lemma_interval [OF ax xb]
obtain d where d: "0<d" and bound: "\<forall>y. \<bar>x-y\<bar> < d \<longrightarrow> a \<le> y \<and> y \<le> b"
@@ -1111,7 +1111,7 @@
from differentiableD [OF dif [OF axb]]
obtain l where der: "DERIV f x :> l" ..
have "l=0" by (rule DERIV_local_max [OF der d bound'])
- --\<open>the derivative at a local maximum is zero\<close>
+ \<comment>\<open>the derivative at a local maximum is zero\<close>
thus ?thesis using ax xb der by auto
next
assume notaxb: "~ (a < x & x < b)"
@@ -1120,7 +1120,7 @@
show ?thesis
proof cases
assume ax'b: "a < x' & x' < b"
- --\<open>@{term f} attains its minimum within the interval\<close>
+ \<comment>\<open>@{term f} attains its minimum within the interval\<close>
hence ax': "a<x'" and x'b: "x'<b" by arith+
from lemma_interval [OF ax' x'b]
obtain d where d: "0<d" and bound: "\<forall>y. \<bar>x'-y\<bar> < d \<longrightarrow> a \<le> y \<and> y \<le> b"
@@ -1130,11 +1130,11 @@
from differentiableD [OF dif [OF ax'b]]
obtain l where der: "DERIV f x' :> l" ..
have "l=0" by (rule DERIV_local_min [OF der d bound'])
- --\<open>the derivative at a local minimum is zero\<close>
+ \<comment>\<open>the derivative at a local minimum is zero\<close>
thus ?thesis using ax' x'b der by auto
next
assume notax'b: "~ (a < x' & x' < b)"
- --\<open>@{term f} is constant througout the interval\<close>
+ \<comment>\<open>@{term f} is constant througout the interval\<close>
hence x'eqab: "x'=a | x'=b" using alex' x'leb by arith
hence fb_eq_fx': "f b = f x'" by (auto simp add: eq)
from dense [OF lt]
@@ -1162,7 +1162,7 @@
from differentiableD [OF dif [OF conjI [OF ar rb]]]
obtain l where der: "DERIV f r :> l" ..
have "l=0" by (rule DERIV_local_const [OF der d bound'])
- --\<open>the derivative of a constant function is zero\<close>
+ \<comment>\<open>the derivative of a constant function is zero\<close>
thus ?thesis using ar rb der by auto
qed
qed
--- a/src/HOL/Divides.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Divides.thy Mon Dec 07 10:38:04 2015 +0100
@@ -220,7 +220,7 @@
text \<open>Addition respects modular equivalence.\<close>
-lemma mod_add_left_eq: -- \<open>FIXME reorient\<close>
+lemma mod_add_left_eq: \<comment> \<open>FIXME reorient\<close>
"(a + b) mod c = (a mod c + b) mod c"
proof -
have "(a + b) mod c = (a div c * c + a mod c + b) mod c"
@@ -232,7 +232,7 @@
finally show ?thesis .
qed
-lemma mod_add_right_eq: -- \<open>FIXME reorient\<close>
+lemma mod_add_right_eq: \<comment> \<open>FIXME reorient\<close>
"(a + b) mod c = (a + b mod c) mod c"
proof -
have "(a + b) mod c = (a + (b div c * c + b mod c)) mod c"
@@ -244,7 +244,7 @@
finally show ?thesis .
qed
-lemma mod_add_eq: -- \<open>FIXME reorient\<close>
+lemma mod_add_eq: \<comment> \<open>FIXME reorient\<close>
"(a + b) mod c = (a mod c + b mod c) mod c"
by (rule trans [OF mod_add_left_eq mod_add_right_eq])
@@ -261,7 +261,7 @@
text \<open>Multiplication respects modular equivalence.\<close>
-lemma mod_mult_left_eq: -- \<open>FIXME reorient\<close>
+lemma mod_mult_left_eq: \<comment> \<open>FIXME reorient\<close>
"(a * b) mod c = ((a mod c) * b) mod c"
proof -
have "(a * b) mod c = ((a div c * c + a mod c) * b) mod c"
@@ -273,7 +273,7 @@
finally show ?thesis .
qed
-lemma mod_mult_right_eq: -- \<open>FIXME reorient\<close>
+lemma mod_mult_right_eq: \<comment> \<open>FIXME reorient\<close>
"(a * b) mod c = (a * (b mod c)) mod c"
proof -
have "(a * b) mod c = (a * (b div c * c + b mod c)) mod c"
@@ -285,7 +285,7 @@
finally show ?thesis .
qed
-lemma mod_mult_eq: -- \<open>FIXME reorient\<close>
+lemma mod_mult_eq: \<comment> \<open>FIXME reorient\<close>
"(a * b) mod c = ((a mod c) * (b mod c)) mod c"
by (rule trans [OF mod_mult_left_eq mod_mult_right_eq])
@@ -573,7 +573,7 @@
and divmod_step_def: "divmod_step l qr = (let (q, r) = qr
in if r \<ge> numeral l then (2 * q + 1, r - numeral l)
else (2 * q, r))"
- -- \<open>These are conceptually definitions but force generated code
+ \<comment> \<open>These are conceptually definitions but force generated code
to be monomorphic wrt. particular instances of this class which
yields a significant speedup.\<close>
@@ -733,7 +733,7 @@
with False show ?thesis by simp
qed
-text \<open>The division rewrite proper -- first, trivial results involving @{text 1}\<close>
+text \<open>The division rewrite proper -- first, trivial results involving \<open>1\<close>\<close>
lemma divmod_trivial [simp]:
"divmod Num.One Num.One = (numeral Num.One, 0)"
@@ -1428,7 +1428,7 @@
fix k
show "?A k"
proof (induct k)
- show "?A 0" by simp -- "by contradiction"
+ show "?A 0" by simp \<comment> "by contradiction"
next
fix n
assume ih: "?A n"
@@ -1638,7 +1638,7 @@
subsection \<open>Division on @{typ int}\<close>
-definition divmod_int_rel :: "int \<Rightarrow> int \<Rightarrow> int \<times> int \<Rightarrow> bool" -- \<open>definition of quotient and remainder\<close>
+definition divmod_int_rel :: "int \<Rightarrow> int \<Rightarrow> int \<times> int \<Rightarrow> bool" \<comment> \<open>definition of quotient and remainder\<close>
where "divmod_int_rel a b = (\<lambda>(q, r). a = b * q + r \<and>
(if 0 < b then 0 \<le> r \<and> r < b else if b < 0 then b < r \<and> r \<le> 0 else q = 0))"
@@ -1860,7 +1860,7 @@
apply (auto simp add: divmod_int_rel_def)
done
-text\<open>There is no @{text mod_neg_pos_trivial}.\<close>
+text\<open>There is no \<open>mod_neg_pos_trivial\<close>.\<close>
subsubsection \<open>Laws for div and mod with Unary Minus\<close>
@@ -2170,7 +2170,7 @@
declare split_zmod [of _ _ "numeral k", arith_split] for k
-subsubsection \<open>Computing @{text "div"} and @{text "mod"} with shifting\<close>
+subsubsection \<open>Computing \<open>div\<close> and \<open>mod\<close> with shifting\<close>
lemma pos_divmod_int_rel_mult_2:
assumes "0 \<le> b"
@@ -2272,8 +2272,8 @@
lemma div_nonpos_pos_le0: "[| (a::int) \<le> 0; b > 0 |] ==> a div b \<le> 0"
by (drule zdiv_mono1, auto)
-text\<open>Now for some equivalences of the form @{text"a div b >=< 0 \<longleftrightarrow> \<dots>"}
-conditional upon the sign of @{text a} or @{text b}. There are many more.
+text\<open>Now for some equivalences of the form \<open>a div b >=< 0 \<longleftrightarrow> \<dots>\<close>
+conditional upon the sign of \<open>a\<close> or \<open>b\<close>. There are many more.
They should all be simp rules unless that causes too much search.\<close>
lemma pos_imp_zdiv_nonneg_iff: "(0::int) < b ==> (0 \<le> a div b) = (0 \<le> a)"
@@ -2466,7 +2466,7 @@
power_mod
zminus_zmod zdiff_zmod_left zdiff_zmod_right
-text \<open>Distributive laws for function @{text nat}.\<close>
+text \<open>Distributive laws for function \<open>nat\<close>.\<close>
lemma nat_div_distrib: "0 \<le> x \<Longrightarrow> nat (x div y) = nat x div nat y"
apply (rule linorder_cases [of y 0])
--- a/src/HOL/Enum.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Enum.thy Mon Dec 07 10:38:04 2015 +0100
@@ -6,7 +6,7 @@
imports Map Groups_List
begin
-subsection \<open>Class @{text enum}\<close>
+subsection \<open>Class \<open>enum\<close>\<close>
class enum =
fixes enum :: "'a list"
@@ -16,7 +16,7 @@
and enum_distinct: "distinct enum"
assumes enum_all_UNIV: "enum_all P \<longleftrightarrow> Ball UNIV P"
assumes enum_ex_UNIV: "enum_ex P \<longleftrightarrow> Bex UNIV P"
- -- \<open>tailored towards simple instantiation\<close>
+ \<comment> \<open>tailored towards simple instantiation\<close>
begin
subclass finite proof
--- a/src/HOL/Equiv_Relations.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Equiv_Relations.thy Mon Dec 07 10:38:04 2015 +0100
@@ -23,10 +23,10 @@
using assms by (simp add: equiv_def)
text \<open>
- Suppes, Theorem 70: @{text r} is an equiv relation iff @{text "r\<inverse> O
- r = r"}.
+ Suppes, Theorem 70: \<open>r\<close> is an equiv relation iff \<open>r\<inverse> O
+ r = r\<close>.
- First half: @{text "equiv A r ==> r\<inverse> O r = r"}.
+ First half: \<open>equiv A r ==> r\<inverse> O r = r\<close>.
\<close>
lemma sym_trans_comp_subset:
@@ -59,7 +59,7 @@
lemma equiv_class_subset:
"equiv A r ==> (a, b) \<in> r ==> r``{a} \<subseteq> r``{b}"
- -- \<open>lemma for the next result\<close>
+ \<comment> \<open>lemma for the next result\<close>
by (unfold equiv_def trans_def sym_def) blast
theorem equiv_class_eq: "equiv A r ==> (a, b) \<in> r ==> r``{a} = r``{b}"
@@ -73,7 +73,7 @@
lemma subset_equiv_class:
"equiv A r ==> r``{b} \<subseteq> r``{a} ==> b \<in> A ==> (a,b) \<in> r"
- -- \<open>lemma for the next result\<close>
+ \<comment> \<open>lemma for the next result\<close>
by (unfold equiv_def refl_on_def) blast
lemma eq_equiv_class:
@@ -99,7 +99,7 @@
subsection \<open>Quotients\<close>
definition quotient :: "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> 'a set set" (infixl "'/'/" 90) where
- "A//r = (\<Union>x \<in> A. {r``{x}})" -- \<open>set of equiv classes\<close>
+ "A//r = (\<Union>x \<in> A. {r``{x}})" \<comment> \<open>set of equiv classes\<close>
lemma quotientI: "x \<in> A ==> r``{x} \<in> A//r"
by (unfold quotient_def) blast
@@ -209,13 +209,13 @@
lemma UN_constant_eq: "a \<in> A ==> \<forall>y \<in> A. f y = c ==> (\<Union>y \<in> A. f(y))=c"
- -- \<open>lemma required to prove @{text UN_equiv_class}\<close>
+ \<comment> \<open>lemma required to prove \<open>UN_equiv_class\<close>\<close>
by auto
lemma UN_equiv_class:
"equiv A r ==> f respects r ==> a \<in> A
==> (\<Union>x \<in> r``{a}. f x) = f a"
- -- \<open>Conversion rule\<close>
+ \<comment> \<open>Conversion rule\<close>
apply (rule equiv_class_self [THEN UN_constant_eq], assumption+)
apply (unfold equiv_def congruent_def sym_def)
apply (blast del: equalityI)
@@ -232,8 +232,8 @@
text \<open>
Sufficient conditions for injectiveness. Could weaken premises!
- major premise could be an inclusion; bcong could be @{text "!!y. y \<in>
- A ==> f y \<in> B"}.
+ major premise could be an inclusion; bcong could be \<open>!!y. y \<in>
+ A ==> f y \<in> B\<close>.
\<close>
lemma UN_equiv_class_inject:
@@ -310,8 +310,8 @@
lemma UN_UN_split_split_eq:
"(\<Union>(x1, x2) \<in> X. \<Union>(y1, y2) \<in> Y. A x1 x2 y1 y2) =
(\<Union>x \<in> X. \<Union>y \<in> Y. (\<lambda>(x1, x2). (\<lambda>(y1, y2). A x1 x2 y1 y2) y) x)"
- -- \<open>Allows a natural expression of binary operators,\<close>
- -- \<open>without explicit calls to @{text split}\<close>
+ \<comment> \<open>Allows a natural expression of binary operators,\<close>
+ \<comment> \<open>without explicit calls to \<open>split\<close>\<close>
by auto
lemma congruent2I:
@@ -319,8 +319,8 @@
==> (!!y z w. w \<in> A2 ==> (y,z) \<in> r1 ==> f y w = f z w)
==> (!!y z w. w \<in> A1 ==> (y,z) \<in> r2 ==> f w y = f w z)
==> congruent2 r1 r2 f"
- -- \<open>Suggested by John Harrison -- the two subproofs may be\<close>
- -- \<open>\emph{much} simpler than the direct proof.\<close>
+ \<comment> \<open>Suggested by John Harrison -- the two subproofs may be\<close>
+ \<comment> \<open>\emph{much} simpler than the direct proof.\<close>
apply (unfold congruent2_def equiv_def refl_on_def)
apply clarify
apply (blast intro: trans)
@@ -345,7 +345,7 @@
text \<open>Suggested by Florian Kammüller\<close>
lemma finite_quotient: "finite A ==> r \<subseteq> A \<times> A ==> finite (A//r)"
- -- \<open>recall @{thm equiv_type}\<close>
+ \<comment> \<open>recall @{thm equiv_type}\<close>
apply (rule finite_subset)
apply (erule_tac [2] finite_Pow_iff [THEN iffD2])
apply (unfold quotient_def)
@@ -435,7 +435,7 @@
definition part_equivp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
"part_equivp R \<longleftrightarrow> (\<exists>x. R x x) \<and> (\<forall>x y. R x y \<longleftrightarrow> R x x \<and> R y y \<and> R x = R y)"
- -- \<open>John-Harrison-style characterization\<close>
+ \<comment> \<open>John-Harrison-style characterization\<close>
lemma part_equivpI:
"(\<exists>x. R x x) \<Longrightarrow> symp R \<Longrightarrow> transp R \<Longrightarrow> part_equivp R"
@@ -484,7 +484,7 @@
text \<open>Total equivalences\<close>
definition equivp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
- "equivp R \<longleftrightarrow> (\<forall>x y. R x y = (R x = R y))" -- \<open>John-Harrison-style characterization\<close>
+ "equivp R \<longleftrightarrow> (\<forall>x y. R x y = (R x = R y))" \<comment> \<open>John-Harrison-style characterization\<close>
lemma equivpI:
"reflp R \<Longrightarrow> symp R \<Longrightarrow> transp R \<Longrightarrow> equivp R"
--- a/src/HOL/Fields.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Fields.thy Mon Dec 07 10:38:04 2015 +0100
@@ -29,7 +29,7 @@
end
-text\<open>Lemmas @{text divide_simps} move division to the outside and eliminates them on (in)equalities.\<close>
+text\<open>Lemmas \<open>divide_simps\<close> move division to the outside and eliminates them on (in)equalities.\<close>
named_theorems divide_simps "rewrite rules to eliminate divisions"
@@ -396,8 +396,7 @@
text \<open>Calculations with fractions\<close>
-text\<open>There is a whole bunch of simp-rules just for class @{text
-field} but none for class @{text field} and @{text nonzero_divides}
+text\<open>There is a whole bunch of simp-rules just for class \<open>field\<close> but none for class \<open>field\<close> and \<open>nonzero_divides\<close>
because the latter are covered by a simproc.\<close>
lemma mult_divide_mult_cancel_left:
@@ -736,7 +735,7 @@
finally show ?thesis .
qed
-text\<open>The following @{text field_simps} rules are necessary, as minus is always moved atop of
+text\<open>The following \<open>field_simps\<close> rules are necessary, as minus is always moved atop of
division but we want to get rid of division.\<close>
lemma pos_le_minus_divide_eq [field_simps]: "0 < c \<Longrightarrow> a \<le> - (b / c) \<longleftrightarrow> a * c \<le> - b"
@@ -771,9 +770,8 @@
"y \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> x / y \<le> w / z \<longleftrightarrow> (x * z - w * y) / (y * z) \<le> 0"
by (subst le_iff_diff_le_0) (simp add: diff_frac_eq )
-text\<open>Lemmas @{text sign_simps} is a first attempt to automate proofs
-of positivity/negativity needed for @{text field_simps}. Have not added @{text
-sign_simps} to @{text field_simps} because the former can lead to case
+text\<open>Lemmas \<open>sign_simps\<close> is a first attempt to automate proofs
+of positivity/negativity needed for \<open>field_simps\<close>. Have not added \<open>sign_simps\<close> to \<open>field_simps\<close> because the former can lead to case
explosions.\<close>
lemmas sign_simps = algebra_simps zero_less_mult_iff mult_less_0_iff
@@ -1006,7 +1004,7 @@
lemma one_divide_eq_0_iff [simp]: "1 / a = 0 \<longleftrightarrow> a = 0"
using zero_eq_1_divide_iff[of a] by simp
-text\<open>Simplify expressions such as @{text "0 < 1/x"} to @{text "0 < x"}\<close>
+text\<open>Simplify expressions such as \<open>0 < 1/x\<close> to \<open>0 < x\<close>\<close>
lemma zero_le_divide_1_iff [simp]:
"0 \<le> 1 / a \<longleftrightarrow> 0 \<le> a"
--- a/src/HOL/Finite_Set.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Finite_Set.thy Mon Dec 07 10:38:04 2015 +0100
@@ -27,7 +27,7 @@
declare [[simproc del: finite_Collect]]
lemma finite_induct [case_names empty insert, induct set: finite]:
- -- \<open>Discharging @{text "x \<notin> F"} entails extra work.\<close>
+ \<comment> \<open>Discharging \<open>x \<notin> F\<close> entails extra work.\<close>
assumes "finite F"
assumes "P {}"
and insert: "\<And>x F. finite F \<Longrightarrow> x \<notin> F \<Longrightarrow> P F \<Longrightarrow> P (insert x F)"
@@ -61,7 +61,7 @@
subsubsection \<open>Choice principles\<close>
-lemma ex_new_if_finite: -- "does not depend on def of finite at all"
+lemma ex_new_if_finite: \<comment> "does not depend on def of finite at all"
assumes "\<not> finite (UNIV :: 'a set)" and "finite A"
shows "\<exists>a::'a. a \<notin> A"
proof -
@@ -574,7 +574,7 @@
qed
-subsection \<open>Class @{text finite}\<close>
+subsection \<open>Class \<open>finite\<close>\<close>
class finite =
assumes finite_UNIV: "finite (UNIV :: 'a set)"
@@ -624,8 +624,8 @@
subsection \<open>A basic fold functional for finite sets\<close>
text \<open>The intended behaviour is
-@{text "fold f z {x\<^sub>1, ..., x\<^sub>n} = f x\<^sub>1 (\<dots> (f x\<^sub>n z)\<dots>)"}
-if @{text f} is ``left-commutative'':
+\<open>fold f z {x\<^sub>1, ..., x\<^sub>n} = f x\<^sub>1 (\<dots> (f x\<^sub>n z)\<dots>)\<close>
+if \<open>f\<close> is ``left-commutative'':
\<close>
locale comp_fun_commute =
@@ -656,7 +656,7 @@
text\<open>A tempting alternative for the definiens is
@{term "if finite A then THE y. fold_graph f z A y else e"}.
It allows the removal of finiteness assumptions from the theorems
-@{text fold_comm}, @{text fold_reindex} and @{text fold_distrib}.
+\<open>fold_comm\<close>, \<open>fold_reindex\<close> and \<open>fold_distrib\<close>.
The proofs become ugly. It is not worth the effort. (???)\<close>
lemma finite_imp_fold_graph: "finite A \<Longrightarrow> \<exists>x. fold_graph f z A x"
@@ -723,7 +723,7 @@
with assms show ?thesis by (simp add: fold_def)
qed
-text \<open>The base case for @{text fold}:\<close>
+text \<open>The base case for \<open>fold\<close>:\<close>
lemma (in -) fold_infinite [simp]:
assumes "\<not> finite A"
@@ -747,7 +747,7 @@
qed
declare (in -) empty_fold_graphE [rule del] fold_graph.intros [rule del]
- -- \<open>No more proofs involve these.\<close>
+ \<comment> \<open>No more proofs involve these.\<close>
lemma fold_fun_left_comm:
"finite A \<Longrightarrow> f x (fold f z A) = fold f (f x z) A"
@@ -884,7 +884,7 @@
end
-subsubsection \<open>Liftings to @{text comp_fun_commute} etc.\<close>
+subsubsection \<open>Liftings to \<open>comp_fun_commute\<close> etc.\<close>
lemma (in comp_fun_commute) comp_comp_fun_commute:
"comp_fun_commute (f \<circ> g)"
--- a/src/HOL/Fun.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Fun.thy Mon Dec 07 10:38:04 2015 +0100
@@ -22,7 +22,7 @@
lemma b_uniq_choice: "\<forall>x\<in>S. \<exists>!y. Q x y \<Longrightarrow> \<exists>f. \<forall>x\<in>S. Q x (f x)"
by (force intro: theI')
-subsection \<open>The Identity Function @{text id}\<close>
+subsection \<open>The Identity Function \<open>id\<close>\<close>
definition id :: "'a \<Rightarrow> 'a" where
"id = (\<lambda>x. x)"
@@ -40,7 +40,7 @@
constant id \<rightharpoonup> (Haskell) "id"
-subsection \<open>The Composition Operator @{text "f \<circ> g"}\<close>
+subsection \<open>The Composition Operator \<open>f \<circ> g\<close>\<close>
definition comp :: "('b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c" (infixl "o" 55) where
"f o g = (\<lambda>x. f (g x))"
@@ -103,7 +103,7 @@
constant comp \<rightharpoonup> (SML) infixl 5 "o" and (Haskell) infixr 9 "."
-subsection \<open>The Forward Composition Operator @{text fcomp}\<close>
+subsection \<open>The Forward Composition Operator \<open>fcomp\<close>\<close>
definition fcomp :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c" (infixl "\<circ>>" 60) where
"f \<circ>> g = (\<lambda>x. g (f x))"
@@ -141,10 +141,10 @@
subsection \<open>Injectivity and Bijectivity\<close>
-definition inj_on :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> bool" where -- "injective"
+definition inj_on :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> bool" where \<comment> "injective"
"inj_on f A \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>A. f x = f y \<longrightarrow> x = y)"
-definition bij_betw :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> bool" where -- "bijective"
+definition bij_betw :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> bool" where \<comment> "bijective"
"bij_betw f A B \<longleftrightarrow> inj_on f A \<and> f ` A = B"
text\<open>A common special case: functions injective, surjective or bijective over
@@ -153,7 +153,7 @@
abbreviation
"inj f \<equiv> inj_on f UNIV"
-abbreviation surj :: "('a \<Rightarrow> 'b) \<Rightarrow> bool" where -- "surjective"
+abbreviation surj :: "('a \<Rightarrow> 'b) \<Rightarrow> bool" where \<comment> "surjective"
"surj f \<equiv> (range f = UNIV)"
abbreviation
@@ -290,7 +290,7 @@
lemma linorder_injI:
assumes hyp: "\<And>x y. x < (y::'a::linorder) \<Longrightarrow> f x \<noteq> f y"
shows "inj f"
- -- \<open>Courtesy of Stephan Merz\<close>
+ \<comment> \<open>Courtesy of Stephan Merz\<close>
proof (rule inj_onI)
fix x y
assume f_eq: "f x = f y"
@@ -524,7 +524,7 @@
done
lemma inj_vimage_singleton: "inj f \<Longrightarrow> f -` {a} \<subseteq> {THE x. f x = a}"
- -- \<open>The inverse image of a singleton under an injective function
+ \<comment> \<open>The inverse image of a singleton under an injective function
is included in a singleton.\<close>
apply (auto simp add: inj_on_def)
apply (blast intro: the_equality [symmetric])
@@ -669,7 +669,7 @@
lemma fun_upd_eqD: "f(x := y) = g(x := z) \<Longrightarrow> y = z"
by(simp add: fun_eq_iff split: split_if_asm)
-subsection \<open>@{text override_on}\<close>
+subsection \<open>\<open>override_on\<close>\<close>
definition override_on :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> 'b" where
"override_on f g A = (\<lambda>a. if a \<in> A then g a else f a)"
@@ -684,7 +684,7 @@
by(simp add:override_on_def)
-subsection \<open>@{text swap}\<close>
+subsection \<open>\<open>swap\<close>\<close>
definition swap :: "'a \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)"
where
--- a/src/HOL/Fun_Def.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Fun_Def.thy Mon Dec 07 10:38:04 2015 +0100
@@ -223,7 +223,7 @@
lemma wf_pair_less[simp]: "wf pair_less"
by (auto simp: pair_less_def)
-text \<open>Introduction rules for @{text pair_less}/@{text pair_leq}\<close>
+text \<open>Introduction rules for \<open>pair_less\<close>/\<open>pair_leq\<close>\<close>
lemma pair_leqI1: "a < b \<Longrightarrow> ((a, s), (b, t)) \<in> pair_leq"
and pair_leqI2: "a \<le> b \<Longrightarrow> s \<le> t \<Longrightarrow> ((a, s), (b, t)) \<in> pair_leq"
and pair_lessI1: "a < b \<Longrightarrow> ((a, s), (b, t)) \<in> pair_less"
@@ -301,7 +301,7 @@
ML_file "Tools/Function/scnp_reconstruct.ML"
ML_file "Tools/Function/fun_cases.ML"
-ML_val -- "setup inactive"
+ML_val \<comment> "setup inactive"
\<open>
Context.theory_map (Function_Common.set_termination_prover
(K (ScnpReconstruct.decomp_scnp_tac [ScnpSolve.MAX, ScnpSolve.MIN, ScnpSolve.MS])))
--- a/src/HOL/GCD.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/GCD.thy Mon Dec 07 10:38:04 2015 +0100
@@ -417,7 +417,7 @@
by (auto intro: associated_eqI)
qed
-lemma dvd_Gcd: -- \<open>FIXME remove\<close>
+lemma dvd_Gcd: \<comment> \<open>FIXME remove\<close>
"\<forall>b\<in>A. a dvd b \<Longrightarrow> a dvd Gcd A"
by (blast intro: Gcd_greatest)
@@ -745,7 +745,7 @@
declare gcd_nat.simps [simp del]
text \<open>
- \medskip @{term "gcd m n"} divides @{text m} and @{text n}. The
+ \medskip @{term "gcd m n"} divides \<open>m\<close> and \<open>n\<close>. The
conjunctions don't seem provable separately.
\<close>
@@ -873,7 +873,7 @@
\<close>
lemma gcd_mult_distrib_nat: "(k::nat) * gcd m n = gcd (k * m) (k * n)"
- -- \<open>@{cite \<open>page 27\<close> davenport92}\<close>
+ \<comment> \<open>@{cite \<open>page 27\<close> davenport92}\<close>
apply (induct m n rule: gcd_nat_induct)
apply simp
apply (case_tac "k = 0")
--- a/src/HOL/Groebner_Basis.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Groebner_Basis.thy Mon Dec 07 10:38:04 2015 +0100
@@ -10,9 +10,9 @@
subsection \<open>Groebner Bases\<close>
-lemmas bool_simps = simp_thms(1-34) -- \<open>FIXME move to @{theory HOL}\<close>
+lemmas bool_simps = simp_thms(1-34) \<comment> \<open>FIXME move to @{theory HOL}\<close>
-lemma nnf_simps: -- \<open>FIXME shadows fact binding in @{theory HOL}\<close>
+lemma nnf_simps: \<comment> \<open>FIXME shadows fact binding in @{theory HOL}\<close>
"(\<not>(P \<and> Q)) = (\<not>P \<or> \<not>Q)" "(\<not>(P \<or> Q)) = (\<not>P \<and> \<not>Q)"
"(P \<longrightarrow> Q) = (\<not>P \<or> Q)"
"(P = Q) = ((P \<and> Q) \<or> (\<not>P \<and> \<not> Q))" "(\<not> \<not>(P)) = P"
--- a/src/HOL/Groups.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Groups.thy Mon Dec 07 10:38:04 2015 +0100
@@ -13,22 +13,22 @@
named_theorems ac_simps "associativity and commutativity simplification rules"
-text\<open>The rewrites accumulated in @{text algebra_simps} deal with the
+text\<open>The rewrites accumulated in \<open>algebra_simps\<close> deal with the
classical algebraic structures of groups, rings and family. They simplify
terms by multiplying everything out (in case of a ring) and bringing sums and
products into a canonical form (by ordered rewriting). As a result it decides
group and ring equalities but also helps with inequalities.
Of course it also works for fields, but it knows nothing about multiplicative
-inverses or division. This is catered for by @{text field_simps}.\<close>
+inverses or division. This is catered for by \<open>field_simps\<close>.\<close>
named_theorems algebra_simps "algebra simplification rules"
-text\<open>Lemmas @{text field_simps} multiply with denominators in (in)equations
+text\<open>Lemmas \<open>field_simps\<close> multiply with denominators in (in)equations
if they can be proved to be non-zero (for equations) or positive/negative
(for inequations). Can be too aggressive and is therefore separate from the
-more benign @{text algebra_simps}.\<close>
+more benign \<open>algebra_simps\<close>.\<close>
named_theorems field_simps "algebra simplification rules for fields"
@@ -110,7 +110,7 @@
Syntax_Phases.term_of_typ ctxt T
else raise Match);
in map tr' [@{const_syntax Groups.one}, @{const_syntax Groups.zero}] end;
-\<close> -- \<open>show types that are presumably too general\<close>
+\<close> \<comment> \<open>show types that are presumably too general\<close>
class plus =
fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "+" 65)
@@ -1383,10 +1383,10 @@
hide_fact (open) ab_diff_conv_add_uminus add_0 mult_1 ab_left_minus
-lemmas add_0 = add_0_left -- \<open>FIXME duplicate\<close>
-lemmas mult_1 = mult_1_left -- \<open>FIXME duplicate\<close>
-lemmas ab_left_minus = left_minus -- \<open>FIXME duplicate\<close>
-lemmas diff_diff_eq = diff_diff_add -- \<open>FIXME duplicate\<close>
+lemmas add_0 = add_0_left \<comment> \<open>FIXME duplicate\<close>
+lemmas mult_1 = mult_1_left \<comment> \<open>FIXME duplicate\<close>
+lemmas ab_left_minus = left_minus \<comment> \<open>FIXME duplicate\<close>
+lemmas diff_diff_eq = diff_diff_add \<comment> \<open>FIXME duplicate\<close>
subsection \<open>Tools setup\<close>
--- a/src/HOL/Groups_Big.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Groups_Big.thy Mon Dec 07 10:38:04 2015 +0100
@@ -67,7 +67,7 @@
lemma union_inter:
assumes "finite A" and "finite B"
shows "F g (A \<union> B) * F g (A \<inter> B) = F g A * F g B"
- -- \<open>The reversed orientation looks more natural, but LOOPS as a simprule!\<close>
+ \<comment> \<open>The reversed orientation looks more natural, but LOOPS as a simprule!\<close>
using assms proof (induct A)
case empty then show ?case by simp
next
@@ -478,19 +478,19 @@
end
text\<open>Now: lot's of fancy syntax. First, @{term "setsum (%x. e) A"} is
-written @{text"\<Sum>x\<in>A. e"}.\<close>
+written \<open>\<Sum>x\<in>A. e\<close>.\<close>
syntax
"_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add" ("(3SUM _:_./ _)" [0, 51, 10] 10)
syntax (xsymbols)
"_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add" ("(2\<Sum>_\<in>_./ _)" [0, 51, 10] 10)
-translations -- \<open>Beware of argument permutation!\<close>
+translations \<comment> \<open>Beware of argument permutation!\<close>
"SUM i:A. b" == "CONST setsum (%i. b) A"
"\<Sum>i\<in>A. b" == "CONST setsum (%i. b) A"
text\<open>Instead of @{term"\<Sum>x\<in>{x. P}. e"} we introduce the shorter
- @{text"\<Sum>x|P. e"}.\<close>
+ \<open>\<Sum>x|P. e\<close>.\<close>
syntax
"_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SUM _ |/ _./ _)" [0,0,10] 10)
@@ -857,7 +857,7 @@
lemma setsum_Un_nat: "finite A ==> finite B ==>
(setsum f (A Un B) :: nat) = setsum f A + setsum f B - setsum f (A Int B)"
- -- \<open>For the natural numbers, we have subtraction.\<close>
+ \<comment> \<open>For the natural numbers, we have subtraction.\<close>
by (subst setsum.union_inter [symmetric], auto simp add: algebra_simps)
lemma setsum_diff1_nat: "(setsum f (A - {a}) :: nat) =
@@ -1064,12 +1064,12 @@
syntax (xsymbols)
"_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult" ("(2\<Prod>_\<in>_./ _)" [0, 51, 10] 10)
-translations -- \<open>Beware of argument permutation!\<close>
+translations \<comment> \<open>Beware of argument permutation!\<close>
"PROD i:A. b" == "CONST setprod (%i. b) A"
"\<Prod>i\<in>A. b" == "CONST setprod (%i. b) A"
text\<open>Instead of @{term"\<Prod>x\<in>{x. P}. e"} we introduce the shorter
- @{text"\<Prod>x|P. e"}.\<close>
+ \<open>\<Prod>x|P. e\<close>.\<close>
syntax
"_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(4PROD _ |/ _./ _)" [0,0,10] 10)
--- a/src/HOL/Groups_List.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Groups_List.thy Mon Dec 07 10:38:04 2015 +0100
@@ -99,7 +99,7 @@
syntax (xsymbols)
"_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
-translations -- \<open>Beware of argument permutation!\<close>
+translations \<comment> \<open>Beware of argument permutation!\<close>
"SUM x<-xs. b" == "CONST listsum (CONST map (%x. b) xs)"
"\<Sum>x\<leftarrow>xs. b" == "CONST listsum (CONST map (%x. b) xs)"
@@ -179,7 +179,7 @@
"(\<Sum>x\<leftarrow>xs. 0) = 0"
by (induct xs) (simp_all add: distrib_right)
-text\<open>For non-Abelian groups @{text xs} needs to be reversed on one side:\<close>
+text\<open>For non-Abelian groups \<open>xs\<close> needs to be reversed on one side:\<close>
lemma (in ab_group_add) uminus_listsum_map:
"- listsum (map f xs) = listsum (map (uminus \<circ> f) xs)"
by (induct xs) simp_all
@@ -357,7 +357,7 @@
syntax (xsymbols)
"_listprod" :: "pttrn => 'a list => 'b => 'b" ("(3\<Prod>_\<leftarrow>_. _)" [0, 51, 10] 10)
-translations -- \<open>Beware of argument permutation!\<close>
+translations \<comment> \<open>Beware of argument permutation!\<close>
"PROD x<-xs. b" == "CONST listprod (CONST map (%x. b) xs)"
"\<Prod>x\<leftarrow>xs. b" == "CONST listprod (CONST map (%x. b) xs)"
--- a/src/HOL/HOL.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/HOL.thy Mon Dec 07 10:38:04 2015 +0100
@@ -125,7 +125,7 @@
[(@{const_syntax The}, fn _ => fn [Abs abs] =>
let val (x, t) = Syntax_Trans.atomic_abs_tr' abs
in Syntax.const @{syntax_const "_The"} $ x $ t end)]
-\<close> -- \<open>To avoid eta-contraction of body\<close>
+\<close> \<comment> \<open>To avoid eta-contraction of body\<close>
nonterminal letbinds and letbind
syntax
@@ -160,7 +160,7 @@
refl: "t = (t::'a)" and
subst: "s = t \<Longrightarrow> P s \<Longrightarrow> P t" and
ext: "(\<And>x::'a. (f x ::'b) = g x) \<Longrightarrow> (\<lambda>x. f x) = (\<lambda>x. g x)"
- -- \<open>Extensionality is built into the meta-logic, and this rule expresses
+ \<comment> \<open>Extensionality is built into the meta-logic, and this rule expresses
a related property. It is an eta-expanded version of the traditional
rule, and similar to the ABS rule of HOL\<close> and
@@ -219,7 +219,7 @@
shows "A = B"
by (unfold meq) (rule refl)
-text \<open>Useful with @{text erule} for proving equalities from known equalities.\<close>
+text \<open>Useful with \<open>erule\<close> for proving equalities from known equalities.\<close>
(* a = b
| |
c = d *)
@@ -241,13 +241,13 @@
subsubsection \<open>Congruence rules for application\<close>
-text \<open>Similar to @{text AP_THM} in Gordon's HOL.\<close>
+text \<open>Similar to \<open>AP_THM\<close> in Gordon's HOL.\<close>
lemma fun_cong: "(f :: 'a \<Rightarrow> 'b) = g \<Longrightarrow> f x = g x"
apply (erule subst)
apply (rule refl)
done
-text \<open>Similar to @{text AP_TERM} in Gordon's HOL and FOL's @{text subst_context}.\<close>
+text \<open>Similar to \<open>AP_TERM\<close> in Gordon's HOL and FOL's \<open>subst_context\<close>.\<close>
lemma arg_cong: "x = y \<Longrightarrow> f x = f y"
apply (erule subst)
apply (rule refl)
@@ -329,7 +329,7 @@
subsubsection \<open>False\<close>
text \<open>
- Depends upon @{text spec}; it is impossible to do propositional
+ Depends upon \<open>spec\<close>; it is impossible to do propositional
logic before quantifiers!
\<close>
@@ -968,7 +968,7 @@
lemma imp_conjL: "((P \<and> Q) \<longrightarrow> R) = (P \<longrightarrow> (Q \<longrightarrow> R))" by iprover
lemma imp_disjL: "((P \<or> Q) \<longrightarrow> R) = ((P \<longrightarrow> R) \<and> (Q \<longrightarrow> R))" by iprover
-text \<open>These two are specialized, but @{text imp_disj_not1} is useful in @{text "Auth/Yahalom"}.\<close>
+text \<open>These two are specialized, but \<open>imp_disj_not1\<close> is useful in \<open>Auth/Yahalom\<close>.\<close>
lemma imp_disj_not1: "(P \<longrightarrow> Q \<or> R) = (\<not> Q \<longrightarrow> P \<longrightarrow> R)" by blast
lemma imp_disj_not2: "(P \<longrightarrow> Q \<or> R) = (\<not> R \<longrightarrow> P \<longrightarrow> Q)" by blast
@@ -983,7 +983,7 @@
lemma not_imp: "(\<not> (P \<longrightarrow> Q)) = (P \<and> \<not> Q)" by blast
lemma not_iff: "(P \<noteq> Q) = (P = (\<not> Q))" by blast
lemma disj_not1: "(\<not> P \<or> Q) = (P \<longrightarrow> Q)" by blast
-lemma disj_not2: "(P \<or> \<not> Q) = (Q \<longrightarrow> P)" -- \<open>changes orientation :-(\<close>
+lemma disj_not2: "(P \<or> \<not> Q) = (Q \<longrightarrow> P)" \<comment> \<open>changes orientation :-(\<close>
by blast
lemma imp_conv_disj: "(P \<longrightarrow> Q) = ((\<not> P) \<or> Q)" by blast
@@ -991,8 +991,8 @@
lemma cases_simp: "((P \<longrightarrow> Q) \<and> (\<not> P \<longrightarrow> Q)) = Q"
- -- \<open>Avoids duplication of subgoals after @{text split_if}, when the true and false\<close>
- -- \<open>cases boil down to the same thing.\<close>
+ \<comment> \<open>Avoids duplication of subgoals after \<open>split_if\<close>, when the true and false\<close>
+ \<comment> \<open>cases boil down to the same thing.\<close>
by blast
lemma not_all: "(\<not> (\<forall>x. P x)) = (\<exists>x. \<not> P x)" by blast
@@ -1007,7 +1007,7 @@
lemma all_conj_distrib: "(\<forall>x. P x \<and> Q x) = ((\<forall>x. P x) \<and> (\<forall>x. Q x))" by iprover
text \<open>
- \medskip The @{text "\<and>"} congruence rule: not included by default!
+ \medskip The \<open>\<and>\<close> congruence rule: not included by default!
May slow rewrite proofs down by as much as 50\%\<close>
lemma conj_cong:
@@ -1018,7 +1018,7 @@
"(Q = Q') \<Longrightarrow> (Q' \<Longrightarrow> (P = P')) \<Longrightarrow> ((P \<and> Q) = (P' \<and> Q'))"
by iprover
-text \<open>The @{text "|"} congruence rule: not included by default!\<close>
+text \<open>The \<open>|\<close> congruence rule: not included by default!\<close>
lemma disj_cong:
"(P = P') \<Longrightarrow> (\<not> P' \<Longrightarrow> (Q = Q')) \<Longrightarrow> ((P \<or> Q) = (P' \<or> Q'))"
@@ -1057,11 +1057,11 @@
by (simplesubst split_if, blast)
lemma if_bool_eq_conj: "(if P then Q else R) = ((P \<longrightarrow> Q) \<and> (\<not> P \<longrightarrow> R))"
- -- \<open>This form is useful for expanding @{text "if"}s on the RIGHT of the @{text "\<Longrightarrow>"} symbol.\<close>
+ \<comment> \<open>This form is useful for expanding \<open>if\<close>s on the RIGHT of the \<open>\<Longrightarrow>\<close> symbol.\<close>
by (rule split_if)
lemma if_bool_eq_disj: "(if P then Q else R) = ((P \<and> Q) \<or> (\<not> P \<and> R))"
- -- \<open>And this form is useful for expanding @{text "if"}s on the LEFT.\<close>
+ \<comment> \<open>And this form is useful for expanding \<open>if\<close>s on the LEFT.\<close>
by (simplesubst split_if) blast
lemma Eq_TrueI: "P \<Longrightarrow> P \<equiv> True" by (unfold atomize_eq) iprover
@@ -1156,7 +1156,7 @@
simproc_setup defined_Ex ("\<exists>x. P x") = \<open>fn _ => Quantifier1.rearrange_ex\<close>
simproc_setup defined_All ("\<forall>x. P x") = \<open>fn _ => Quantifier1.rearrange_all\<close>
-text \<open>Simproc for proving @{text "(y = x) \<equiv> False"} from premise @{text "\<not> (x = y)"}:\<close>
+text \<open>Simproc for proving \<open>(y = x) \<equiv> False\<close> from premise \<open>\<not> (x = y)\<close>:\<close>
simproc_setup neq ("x = y") = \<open>fn _ =>
let
@@ -1261,7 +1261,7 @@
"\<And>P Q. (\<exists>x. P \<or> Q x) = (P \<or> (\<exists>x. Q x))"
"\<And>P Q. (\<exists>x. P x \<longrightarrow> Q) = ((\<forall>x. P x) \<longrightarrow> Q)"
"\<And>P Q. (\<exists>x. P \<longrightarrow> Q x) = (P \<longrightarrow> (\<exists>x. Q x))"
- -- \<open>Miniscoping: pushing in existential quantifiers.\<close>
+ \<comment> \<open>Miniscoping: pushing in existential quantifiers.\<close>
by (iprover | blast)+
lemma all_simps:
@@ -1271,7 +1271,7 @@
"\<And>P Q. (\<forall>x. P \<or> Q x) = (P \<or> (\<forall>x. Q x))"
"\<And>P Q. (\<forall>x. P x \<longrightarrow> Q) = ((\<exists>x. P x) \<longrightarrow> Q)"
"\<And>P Q. (\<forall>x. P \<longrightarrow> Q x) = (P \<longrightarrow> (\<forall>x. Q x))"
- -- \<open>Miniscoping: pushing in universal quantifiers.\<close>
+ \<comment> \<open>Miniscoping: pushing in universal quantifiers.\<close>
by (iprover | blast)+
lemmas [simp] =
@@ -1654,7 +1654,7 @@
ML_file "Tools/cnf.ML"
-section \<open>@{text NO_MATCH} simproc\<close>
+section \<open>\<open>NO_MATCH\<close> simproc\<close>
text \<open>
The simplification procedure can be used to avoid simplification of terms of a certain form
--- a/src/HOL/Hilbert_Choice.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Hilbert_Choice.thy Mon Dec 07 10:38:04 2015 +0100
@@ -28,7 +28,7 @@
[(@{const_syntax Eps}, fn _ => fn [Abs abs] =>
let val (x, t) = Syntax_Trans.atomic_abs_tr' abs
in Syntax.const @{syntax_const "_Eps"} $ x $ t end)]
-\<close> -- \<open>to avoid eta-contraction of body\<close>
+\<close> \<comment> \<open>to avoid eta-contraction of body\<close>
definition inv_into :: "'a set => ('a => 'b) => ('b => 'a)" where
"inv_into A f == %x. SOME y. y : A & f y = x"
@@ -39,19 +39,19 @@
subsection \<open>Hilbert's Epsilon-operator\<close>
-text\<open>Easier to apply than @{text someI} if the witness comes from an
+text\<open>Easier to apply than \<open>someI\<close> if the witness comes from an
existential formula\<close>
lemma someI_ex [elim?]: "\<exists>x. P x ==> P (SOME x. P x)"
apply (erule exE)
apply (erule someI)
done
-text\<open>Easier to apply than @{text someI} because the conclusion has only one
+text\<open>Easier to apply than \<open>someI\<close> because the conclusion has only one
occurrence of @{term P}.\<close>
lemma someI2: "[| P a; !!x. P x ==> Q x |] ==> Q (SOME x. P x)"
by (blast intro: someI)
-text\<open>Easier to apply than @{text someI2} if the witness comes from an
+text\<open>Easier to apply than \<open>someI2\<close> if the witness comes from an
existential formula\<close>
lemma someI2_ex: "[| \<exists>a. P a; !!x. P x ==> Q x |] ==> Q (SOME x. P x)"
@@ -294,20 +294,20 @@
text \<open>
Every infinite set contains a countable subset. More precisely we
- show that a set @{text S} is infinite if and only if there exists an
- injective function from the naturals into @{text S}.
+ show that a set \<open>S\<close> is infinite if and only if there exists an
+ injective function from the naturals into \<open>S\<close>.
The ``only if'' direction is harder because it requires the
construction of a sequence of pairwise different elements of an
- infinite set @{text S}. The idea is to construct a sequence of
- non-empty and infinite subsets of @{text S} obtained by successively
- removing elements of @{text S}.
+ infinite set \<open>S\<close>. The idea is to construct a sequence of
+ non-empty and infinite subsets of \<open>S\<close> obtained by successively
+ removing elements of \<open>S\<close>.
\<close>
lemma infinite_countable_subset:
assumes inf: "\<not> finite (S::'a set)"
shows "\<exists>f. inj (f::nat \<Rightarrow> 'a) \<and> range f \<subseteq> S"
- -- \<open>Courtesy of Stephan Merz\<close>
+ \<comment> \<open>Courtesy of Stephan Merz\<close>
proof -
def Sseq \<equiv> "rec_nat S (\<lambda>n T. T - {SOME e. e \<in> T})"
def pick \<equiv> "\<lambda>n. (SOME e. e \<in> Sseq n)"
@@ -325,7 +325,7 @@
qed
lemma infinite_iff_countable_subset: "\<not> finite S \<longleftrightarrow> (\<exists>f. inj (f::nat \<Rightarrow> 'a) \<and> range f \<subseteq> S)"
- -- \<open>Courtesy of Stephan Merz\<close>
+ \<comment> \<open>Courtesy of Stephan Merz\<close>
using finite_imageD finite_subset infinite_UNIV_char_0 infinite_countable_subset by auto
lemma image_inv_into_cancel:
@@ -703,7 +703,7 @@
done
-text \<open>\medskip Specialization to @{text GREATEST}.\<close>
+text \<open>\medskip Specialization to \<open>GREATEST\<close>.\<close>
lemma GreatestI: "P (k::nat) ==> \<forall>y. P y --> y < b ==> P (GREATEST x. P x)"
apply (simp add: Greatest_def)
--- a/src/HOL/Inductive.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Inductive.thy Mon Dec 07 10:38:04 2015 +0100
@@ -21,11 +21,11 @@
definition
lfp :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a" where
- "lfp f = Inf {u. f u \<le> u}" --\<open>least fixed point\<close>
+ "lfp f = Inf {u. f u \<le> u}" \<comment>\<open>least fixed point\<close>
definition
gfp :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a" where
- "gfp f = Sup {u. u \<le> f u}" --\<open>greatest fixed point\<close>
+ "gfp f = Sup {u. u \<le> f u}" \<comment>\<open>greatest fixed point\<close>
subsection\<open>Proof of Knaster-Tarski Theorem using @{term lfp}\<close>
@@ -101,7 +101,7 @@
using assms by (rule lfp_ordinal_induct)
-text\<open>Definition forms of @{text lfp_unfold} and @{text lfp_induct},
+text\<open>Definition forms of \<open>lfp_unfold\<close> and \<open>lfp_induct\<close>,
to control unfolding\<close>
lemma def_lfp_unfold: "[| h==lfp(f); mono(f) |] ==> h = f(h)"
@@ -230,7 +230,7 @@
apply (simp_all)
done
-text\<open>Definition forms of @{text gfp_unfold} and @{text coinduct},
+text\<open>Definition forms of \<open>gfp_unfold\<close> and \<open>coinduct\<close>,
to control unfolding\<close>
lemma def_gfp_unfold: "[| A==gfp(f); mono(f) |] ==> A = f(A)"
--- a/src/HOL/Int.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Int.thy Mon Dec 07 10:38:04 2015 +0100
@@ -198,7 +198,7 @@
for z1 z2 w :: int
-subsection \<open>Embedding of the Integers into any @{text ring_1}: @{text of_int}\<close>
+subsection \<open>Embedding of the Integers into any \<open>ring_1\<close>: \<open>of_int\<close>\<close>
context ring_1
begin
@@ -270,7 +270,7 @@
context linordered_idom
begin
-text\<open>Every @{text linordered_idom} has characteristic zero.\<close>
+text\<open>Every \<open>linordered_idom\<close> has characteristic zero.\<close>
subclass ring_char_0 ..
lemma of_int_le_iff [simp]:
@@ -364,7 +364,7 @@
apply simp
done
-subsection \<open>Magnitude of an Integer, as a Natural Number: @{text nat}\<close>
+subsection \<open>Magnitude of an Integer, as a Natural Number: \<open>nat\<close>\<close>
lift_definition nat :: "int \<Rightarrow> nat" is "\<lambda>(x, y). x - y"
by auto
@@ -525,9 +525,9 @@
by simp
text\<open>This version is proved for all ordered rings, not just integers!
- It is proved here because attribute @{text arith_split} is not available
- in theory @{text Rings}.
- But is it really better than just rewriting with @{text abs_if}?\<close>
+ It is proved here because attribute \<open>arith_split\<close> is not available
+ in theory \<open>Rings\<close>.
+ But is it really better than just rewriting with \<open>abs_if\<close>?\<close>
lemma abs_split [arith_split, no_atp]:
"P(abs(a::'a::linordered_idom)) = ((0 \<le> a --> P a) & (a < 0 --> P(-a)))"
by (force dest: order_less_le_trans simp add: abs_if linorder_not_less)
@@ -588,14 +588,14 @@
using assms by (rule nonneg_eq_int)
lemma Let_numeral [simp]: "Let (numeral v) f = f (numeral v)"
- -- \<open>Unfold all @{text let}s involving constants\<close>
- by (fact Let_numeral) -- \<open>FIXME drop\<close>
+ \<comment> \<open>Unfold all \<open>let\<close>s involving constants\<close>
+ by (fact Let_numeral) \<comment> \<open>FIXME drop\<close>
lemma Let_neg_numeral [simp]: "Let (- numeral v) f = f (- numeral v)"
- -- \<open>Unfold all @{text let}s involving constants\<close>
- by (fact Let_neg_numeral) -- \<open>FIXME drop\<close>
+ \<comment> \<open>Unfold all \<open>let\<close>s involving constants\<close>
+ by (fact Let_neg_numeral) \<comment> \<open>FIXME drop\<close>
-text \<open>Unfold @{text min} and @{text max} on numerals.\<close>
+text \<open>Unfold \<open>min\<close> and \<open>max\<close> on numerals.\<close>
lemmas max_number_of [simp] =
max_def [of "numeral u" "numeral v"]
@@ -1220,7 +1220,7 @@
lemmas divide_le_0_iff_numeral [simp, no_atp] = divide_le_0_iff [of "numeral w"] for w
-text \<open>Replaces @{text "inverse #nn"} by @{text "1/#nn"}. It looks
+text \<open>Replaces \<open>inverse #nn\<close> by \<open>1/#nn\<close>. It looks
strange, but then other simprocs simplify the quotient.\<close>
lemmas inverse_eq_divide_numeral [simp] =
@@ -1250,10 +1250,10 @@
lemmas minus_less_iff_numeral [no_atp] =
minus_less_iff [of _ "numeral v"] for v
--- \<open>FIXME maybe simproc\<close>
+\<comment> \<open>FIXME maybe simproc\<close>
-text \<open>Cancellation of constant factors in comparisons (@{text "<"} and @{text "\<le>"})\<close>
+text \<open>Cancellation of constant factors in comparisons (\<open><\<close> and \<open>\<le>\<close>)\<close>
lemmas mult_less_cancel_left_numeral [simp, no_atp] = mult_less_cancel_left [of "numeral v"] for v
lemmas mult_less_cancel_right_numeral [simp, no_atp] = mult_less_cancel_right [of _ "numeral v"] for v
@@ -1261,7 +1261,7 @@
lemmas mult_le_cancel_right_numeral [simp, no_atp] = mult_le_cancel_right [of _ "numeral v"] for v
-text \<open>Multiplying out constant divisors in comparisons (@{text "<"}, @{text "\<le>"} and @{text "="})\<close>
+text \<open>Multiplying out constant divisors in comparisons (\<open><\<close>, \<open>\<le>\<close> and \<open>=\<close>)\<close>
named_theorems divide_const_simps "simplification rules to simplify comparisons involving constant divisors"
@@ -1689,7 +1689,7 @@
lemmas zpower_numeral_even = power_numeral_even [where 'a=int]
lemmas zpower_numeral_odd = power_numeral_odd [where 'a=int]
-text \<open>De-register @{text "int"} as a quotient type:\<close>
+text \<open>De-register \<open>int\<close> as a quotient type:\<close>
lifting_update int.lifting
lifting_forget int.lifting
--- a/src/HOL/Isar_Examples/Basic_Logic.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Isar_Examples/Basic_Logic.thy Mon Dec 07 10:38:04 2015 +0100
@@ -172,9 +172,9 @@
proof
assume "A \<and> B"
then show "B \<and> A"
- proof -- \<open>rule \<open>conjE\<close> of \<open>A \<and> B\<close>\<close>
+ proof \<comment> \<open>rule \<open>conjE\<close> of \<open>A \<and> B\<close>\<close>
assume B A
- then show ?thesis .. -- \<open>rule \<open>conjI\<close> of \<open>B \<and> A\<close>\<close>
+ then show ?thesis .. \<comment> \<open>rule \<open>conjI\<close> of \<open>B \<and> A\<close>\<close>
qed
qed
@@ -202,7 +202,7 @@
from \<open>A \<and> B\<close> have B ..
from \<open>B\<close> \<open>A\<close> have "B \<and> A" ..
}
- then show ?thesis .. -- \<open>rule \<open>impI\<close>\<close>
+ then show ?thesis .. \<comment> \<open>rule \<open>impI\<close>\<close>
qed
text \<open>
@@ -253,7 +253,7 @@
proof
assume "P \<or> P"
then show P
- proof -- \<open>rule \<open>disjE\<close>: \smash{$\infer{\<open>C\<close>}{\<open>A \<or> B\<close> & \infer*{\<open>C\<close>}{[\<open>A\<close>]} & \infer*{\<open>C\<close>}{[\<open>B\<close>]}}$}\<close>
+ proof \<comment> \<open>rule \<open>disjE\<close>: \smash{$\infer{\<open>C\<close>}{\<open>A \<or> B\<close> & \infer*{\<open>C\<close>}{[\<open>A\<close>]} & \infer*{\<open>C\<close>}{[\<open>B\<close>]}}$}\<close>
assume P show P by fact
next
assume P show P by fact
@@ -322,7 +322,7 @@
proof
assume "\<exists>x. P (f x)"
then show "\<exists>y. P y"
- proof (rule exE) -- \<open>rule \<open>exE\<close>: \smash{$\infer{\<open>B\<close>}{\<open>\<exists>x. A(x)\<close> & \infer*{\<open>B\<close>}{[\<open>A(x)\<close>]_x}}$}\<close>
+ proof (rule exE) \<comment> \<open>rule \<open>exE\<close>: \smash{$\infer{\<open>B\<close>}{\<open>\<exists>x. A(x)\<close> & \infer*{\<open>B\<close>}{[\<open>A(x)\<close>]_x}}$}\<close>
fix a
assume "P (f a)" (is "P ?witness")
then show ?thesis by (rule exI [of P ?witness])
--- a/src/HOL/Isar_Examples/Expr_Compiler.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Isar_Examples/Expr_Compiler.thy Mon Dec 07 10:38:04 2015 +0100
@@ -157,7 +157,7 @@
next
case (Load adr)
from Cons show ?case
- by simp -- \<open>same as above\<close>
+ by simp \<comment> \<open>same as above\<close>
next
case (Apply fn)
have "exec ((Apply fn # xs) @ ys) s env =
@@ -187,7 +187,7 @@
finally show ?case .
next
case (Constant val s)
- show ?case by simp -- \<open>same as above\<close>
+ show ?case by simp \<comment> \<open>same as above\<close>
next
case (Binop fn e1 e2 s)
have "exec (compile (Binop fn e1 e2)) s env =
--- a/src/HOL/Isar_Examples/Fibonacci.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Isar_Examples/Fibonacci.thy Mon Dec 07 10:38:04 2015 +0100
@@ -52,7 +52,7 @@
lemma fib_add:
"fib (n + k + 1) = fib (k + 1) * fib (n + 1) + fib k * fib n"
(is "?P n")
- -- \<open>see @{cite \<open>page 280\<close> "Concrete-Math"}\<close>
+ \<comment> \<open>see @{cite \<open>page 280\<close> "Concrete-Math"}\<close>
proof (induct n rule: fib_induct)
show "?P 0" by simp
show "?P 1" by simp
--- a/src/HOL/Isar_Examples/Group.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Isar_Examples/Group.thy Mon Dec 07 10:38:04 2015 +0100
@@ -87,27 +87,27 @@
by (simp only: group_left_inverse)
note calculation = this
- -- \<open>first calculational step: init calculation register\<close>
+ \<comment> \<open>first calculational step: init calculation register\<close>
have "\<dots> = x * inverse x * x"
by (simp only: group_assoc)
note calculation = trans [OF calculation this]
- -- \<open>general calculational step: compose with transitivity rule\<close>
+ \<comment> \<open>general calculational step: compose with transitivity rule\<close>
have "\<dots> = 1 * x"
by (simp only: group_right_inverse)
note calculation = trans [OF calculation this]
- -- \<open>general calculational step: compose with transitivity rule\<close>
+ \<comment> \<open>general calculational step: compose with transitivity rule\<close>
have "\<dots> = x"
by (simp only: group_left_one)
note calculation = trans [OF calculation this]
- -- \<open>final calculational step: compose with transitivity rule \dots\<close>
+ \<comment> \<open>final calculational step: compose with transitivity rule \dots\<close>
from calculation
- -- \<open>\dots\ and pick up the final result\<close>
+ \<comment> \<open>\dots\ and pick up the final result\<close>
show ?thesis .
qed
--- a/src/HOL/Isar_Examples/Hoare.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Isar_Examples/Hoare.thy Mon Dec 07 10:38:04 2015 +0100
@@ -384,7 +384,7 @@
lemma Compl_Collect: "- Collect b = {x. \<not> b x}"
by blast
-lemmas AbortRule = SkipRule -- "dummy version"
+lemmas AbortRule = SkipRule \<comment> "dummy version"
ML_file "~~/src/HOL/Hoare/hoare_tac.ML"
--- a/src/HOL/Isar_Examples/Hoare_Ex.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Isar_Examples/Hoare_Ex.thy Mon Dec 07 10:38:04 2015 +0100
@@ -79,7 +79,7 @@
lemma
"Valid {s. x s = a} (Basic (\<lambda>s. x_update (x s) s)) {s. x s = n}"
- -- \<open>same statement without concrete syntax\<close>
+ \<comment> \<open>same statement without concrete syntax\<close>
oops
@@ -99,8 +99,8 @@
lemma "\<turnstile> \<lbrace>\<acute>M = \<acute>N\<rbrace> \<acute>M := \<acute>M + 1 \<lbrace>\<acute>M \<noteq> \<acute>N\<rbrace>"
proof -
have "m = n \<longrightarrow> m + 1 \<noteq> n" for m n :: nat
- -- \<open>inclusion of assertions expressed in ``pure'' logic,\<close>
- -- \<open>without mentioning the state space\<close>
+ \<comment> \<open>inclusion of assertions expressed in ``pure'' logic,\<close>
+ \<comment> \<open>without mentioning the state space\<close>
by simp
also have "\<turnstile> \<lbrace>\<acute>M + 1 \<noteq> \<acute>N\<rbrace> \<acute>M := \<acute>M + 1 \<lbrace>\<acute>M \<noteq> \<acute>N\<rbrace>"
by hoare
--- a/src/HOL/Isar_Examples/Structured_Statements.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Isar_Examples/Structured_Statements.thy Mon Dec 07 10:38:04 2015 +0100
@@ -152,9 +152,9 @@
have C
proof -
- show ?thesis when "A x" (is ?A) for x :: 'a -- \<open>abstract @{term x}\<close>
+ show ?thesis when "A x" (is ?A) for x :: 'a \<comment> \<open>abstract @{term x}\<close>
using that sorry
- show "?A a" -- \<open>concrete @{term a}\<close>
+ show "?A a" \<comment> \<open>concrete @{term a}\<close>
sorry
qed
end
--- a/src/HOL/Lattices.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Lattices.thy Mon Dec 07 10:38:04 2015 +0100
@@ -741,12 +741,12 @@
ML_file "Tools/boolean_algebra_cancel.ML"
simproc_setup boolean_algebra_cancel_sup ("sup a b::'a::boolean_algebra") =
- {* fn phi => fn ss => try Boolean_Algebra_Cancel.cancel_sup_conv *}
+ \<open>fn phi => fn ss => try Boolean_Algebra_Cancel.cancel_sup_conv\<close>
simproc_setup boolean_algebra_cancel_inf ("inf a b::'a::boolean_algebra") =
- {* fn phi => fn ss => try Boolean_Algebra_Cancel.cancel_inf_conv *}
+ \<open>fn phi => fn ss => try Boolean_Algebra_Cancel.cancel_inf_conv\<close>
-subsection \<open>@{text "min/max"} as special case of lattice\<close>
+subsection \<open>\<open>min/max\<close> as special case of lattice\<close>
context linorder
begin
@@ -1002,8 +1002,8 @@
by (simp add: sup_fun_def) iprover
text \<open>
- \medskip Classical introduction rule: no commitment to @{text A} vs
- @{text B}.
+ \medskip Classical introduction rule: no commitment to \<open>A\<close> vs
+ \<open>B\<close>.
\<close>
lemma sup1CI: "(\<not> B x \<Longrightarrow> A x) \<Longrightarrow> (A \<squnion> B) x"
--- a/src/HOL/Library/Float.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Library/Float.thy Mon Dec 07 10:38:04 2015 +0100
@@ -529,7 +529,7 @@
show "m = mantissa f * 2 ^ nat (exponent f - e)"
by linarith
show "e = exponent f - nat (exponent f - e)"
- using `e \<le> exponent f` by auto
+ using \<open>e \<le> exponent f\<close> by auto
qed
context
--- a/src/HOL/Library/Formal_Power_Series.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Library/Formal_Power_Series.thy Mon Dec 07 10:38:04 2015 +0100
@@ -476,7 +476,7 @@
qed simp_all
-subsection {* Subdegrees *}
+subsection \<open>Subdegrees\<close>
definition subdegree :: "('a::zero) fps \<Rightarrow> nat" where
"subdegree f = (if f = 0 then 0 else LEAST n. f$n \<noteq> 0)"
@@ -1467,7 +1467,7 @@
assume "Lcm A \<noteq> 0"
from unbounded obtain f where f: "f \<in> A" "subdegree (Lcm A) < subdegree f"
unfolding bdd_above_def by (auto simp: not_le)
- moreover from this and `Lcm A \<noteq> 0` have "subdegree f \<le> subdegree (Lcm A)"
+ moreover from this and \<open>Lcm A \<noteq> 0\<close> have "subdegree f \<le> subdegree (Lcm A)"
by (intro dvd_imp_subdegree_le) simp_all
ultimately show False by simp
qed
--- a/src/HOL/Lifting.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Lifting.thy Mon Dec 07 10:38:04 2015 +0100
@@ -55,7 +55,7 @@
by blast
lemma Quotient_rel:
- "R r r \<and> R s s \<and> Abs r = Abs s \<longleftrightarrow> R r s" -- \<open>orientation does not loop on rewriting\<close>
+ "R r r \<and> R s s \<and> Abs r = Abs s \<longleftrightarrow> R r s" \<comment> \<open>orientation does not loop on rewriting\<close>
using a unfolding Quotient_def
by blast
@@ -318,7 +318,7 @@
end
-text \<open>Generating transfer rules for a type defined with @{text "typedef"}.\<close>
+text \<open>Generating transfer rules for a type defined with \<open>typedef\<close>.\<close>
context
fixes Rep Abs A T
@@ -350,7 +350,7 @@
end
text \<open>Generating the correspondence rule for a constant defined with
- @{text "lift_definition"}.\<close>
+ \<open>lift_definition\<close>.\<close>
lemma Quotient_to_transfer:
assumes "Quotient R Abs Rep T" and "R c c" and "c' \<equiv> Abs c"
--- a/src/HOL/Limits.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Limits.thy Mon Dec 07 10:38:04 2015 +0100
@@ -279,7 +279,7 @@
assume "c \<noteq> 0" "Bseq (\<lambda>x. c * f x)"
find_theorems "Bfun (\<lambda>_. ?c) _"
from Bfun_const this(2) have "Bseq (\<lambda>x. inverse c * (c * f x))" by (rule Bseq_mult)
- with `c \<noteq> 0` show "Bseq f" by (simp add: divide_simps)
+ with \<open>c \<noteq> 0\<close> show "Bseq f" by (simp add: divide_simps)
qed (intro Bseq_mult Bfun_const)
lemma Bseq_subseq: "Bseq (f :: nat \<Rightarrow> 'a :: real_normed_vector) \<Longrightarrow> Bseq (\<lambda>x. f (g x))"
--- a/src/HOL/List.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/List.thy Mon Dec 07 10:38:04 2015 +0100
@@ -20,12 +20,12 @@
datatype_compat list
lemma [case_names Nil Cons, cases type: list]:
- -- \<open>for backward compatibility -- names of variables differ\<close>
+ \<comment> \<open>for backward compatibility -- names of variables differ\<close>
"(y = [] \<Longrightarrow> P) \<Longrightarrow> (\<And>a list. y = a # list \<Longrightarrow> P) \<Longrightarrow> P"
by (rule list.exhaust)
lemma [case_names Nil Cons, induct type: list]:
- -- \<open>for backward compatibility -- names of variables differ\<close>
+ \<comment> \<open>for backward compatibility -- names of variables differ\<close>
"P [] \<Longrightarrow> (\<And>a list. P list \<Longrightarrow> P (a # list)) \<Longrightarrow> P list"
by (rule list.induct)
@@ -42,7 +42,7 @@
lemmas set_simps = list.set (* legacy *)
syntax
- -- \<open>list Enumeration\<close>
+ \<comment> \<open>list Enumeration\<close>
"_list" :: "args => 'a list" ("[(_)]")
translations
@@ -78,7 +78,7 @@
"filter P (x # xs) = (if P x then x # filter P xs else filter P xs)"
syntax
- -- \<open>Special syntax for filter\<close>
+ \<comment> \<open>Special syntax for filter\<close>
"_filter" :: "[pttrn, 'a list, bool] => 'a list" ("(1[_<-_./ _])")
syntax (xsymbols)
"_filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])")
@@ -104,19 +104,19 @@
primrec drop:: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
drop_Nil: "drop n [] = []" |
drop_Cons: "drop n (x # xs) = (case n of 0 \<Rightarrow> x # xs | Suc m \<Rightarrow> drop m xs)"
- -- \<open>Warning: simpset does not contain this definition, but separate
- theorems for @{text "n = 0"} and @{text "n = Suc k"}\<close>
+ \<comment> \<open>Warning: simpset does not contain this definition, but separate
+ theorems for \<open>n = 0\<close> and \<open>n = Suc k\<close>\<close>
primrec take:: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
take_Nil:"take n [] = []" |
take_Cons: "take n (x # xs) = (case n of 0 \<Rightarrow> [] | Suc m \<Rightarrow> x # take m xs)"
- -- \<open>Warning: simpset does not contain this definition, but separate
- theorems for @{text "n = 0"} and @{text "n = Suc k"}\<close>
+ \<comment> \<open>Warning: simpset does not contain this definition, but separate
+ theorems for \<open>n = 0\<close> and \<open>n = Suc k\<close>\<close>
primrec (nonexhaustive) nth :: "'a list => nat => 'a" (infixl "!" 100) where
nth_Cons: "(x # xs) ! n = (case n of 0 \<Rightarrow> x | Suc k \<Rightarrow> xs ! k)"
- -- \<open>Warning: simpset does not contain this definition, but separate
- theorems for @{text "n = 0"} and @{text "n = Suc k"}\<close>
+ \<comment> \<open>Warning: simpset does not contain this definition, but separate
+ theorems for \<open>n = 0\<close> and \<open>n = Suc k\<close>\<close>
primrec list_update :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a list" where
"list_update [] i v = []" |
@@ -147,8 +147,8 @@
"zip xs [] = []" |
zip_Cons: "zip xs (y # ys) =
(case xs of [] => [] | z # zs => (z, y) # zip zs ys)"
- -- \<open>Warning: simpset does not contain this definition, but separate
- theorems for @{text "xs = []"} and @{text "xs = z # zs"}\<close>
+ \<comment> \<open>Warning: simpset does not contain this definition, but separate
+ theorems for \<open>xs = []\<close> and \<open>xs = z # zs\<close>\<close>
primrec product :: "'a list \<Rightarrow> 'b list \<Rightarrow> ('a \<times> 'b) list" where
"product [] _ = []" |
@@ -177,7 +177,7 @@
"find _ [] = None" |
"find P (x#xs) = (if P x then Some x else find P xs)"
-text \<open>In the context of multisets, @{text count_list} is equivalent to
+text \<open>In the context of multisets, \<open>count_list\<close> is equivalent to
@{term "count o mset"} and it it advisable to use the latter.\<close>
primrec count_list :: "'a list \<Rightarrow> 'a \<Rightarrow> nat" where
"count_list [] y = 0" |
@@ -225,8 +225,8 @@
replicate_Suc: "replicate (Suc n) x = x # replicate n x"
text \<open>
- Function @{text size} is overloaded for all datatypes. Users may
- refer to the list version as @{text length}.\<close>
+ Function \<open>size\<close> is overloaded for all datatypes. Users may
+ refer to the list version as \<open>length\<close>.\<close>
abbreviation length :: "'a list \<Rightarrow> nat" where
"length \<equiv> size"
@@ -367,23 +367,23 @@
subsubsection \<open>List comprehension\<close>
text\<open>Input syntax for Haskell-like list comprehension notation.
-Typical example: @{text"[(x,y). x \<leftarrow> xs, y \<leftarrow> ys, x \<noteq> y]"},
-the list of all pairs of distinct elements from @{text xs} and @{text ys}.
-The syntax is as in Haskell, except that @{text"|"} becomes a dot
-(like in Isabelle's set comprehension): @{text"[e. x \<leftarrow> xs, \<dots>]"} rather than
+Typical example: \<open>[(x,y). x \<leftarrow> xs, y \<leftarrow> ys, x \<noteq> y]\<close>,
+the list of all pairs of distinct elements from \<open>xs\<close> and \<open>ys\<close>.
+The syntax is as in Haskell, except that \<open>|\<close> becomes a dot
+(like in Isabelle's set comprehension): \<open>[e. x \<leftarrow> xs, \<dots>]\<close> rather than
\verb![e| x <- xs, ...]!.
The qualifiers after the dot are
\begin{description}
-\item[generators] @{text"p \<leftarrow> xs"},
- where @{text p} is a pattern and @{text xs} an expression of list type, or
-\item[guards] @{text"b"}, where @{text b} is a boolean expression.
+\item[generators] \<open>p \<leftarrow> xs\<close>,
+ where \<open>p\<close> is a pattern and \<open>xs\<close> an expression of list type, or
+\item[guards] \<open>b\<close>, where \<open>b\<close> is a boolean expression.
%\item[local bindings] @ {text"let x = e"}.
\end{description}
Just like in Haskell, list comprehension is just a shorthand. To avoid
misunderstandings, the translation into desugared form is not reversed
-upon output. Note that the translation of @{text"[e. x \<leftarrow> xs]"} is
+upon output. Note that the translation of \<open>[e. x \<leftarrow> xs]\<close> is
optmized to @{term"map (%x. e) xs"}.
It is easy to write short list comprehensions which stand for complex
@@ -801,8 +801,7 @@
subsubsection \<open>@{const length}\<close>
text \<open>
- Needs to come before @{text "@"} because of theorem @{text
- append_eq_append_conv}.
+ Needs to come before \<open>@\<close> because of theorem \<open>append_eq_append_conv\<close>.
\<close>
lemma length_append [simp]: "length (xs @ ys) = length xs + length ys"
@@ -926,7 +925,7 @@
\<close>
-subsubsection \<open>@{text "@"} -- append\<close>
+subsubsection \<open>\<open>@\<close> -- append\<close>
lemma append_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)"
by (induct xs) auto
@@ -1003,7 +1002,7 @@
by(cases ys) auto
-text \<open>Trivial rules for solving @{text "@"}-equations automatically.\<close>
+text \<open>Trivial rules for solving \<open>@\<close>-equations automatically.\<close>
lemma eq_Nil_appendI: "xs = ys ==> xs = [] @ ys"
by simp
@@ -1019,7 +1018,7 @@
text \<open>
Simplification procedure for all list equalities.
-Currently only tries to rearrange @{text "@"} to see if
+Currently only tries to rearrange \<open>@\<close> to see if
- both lists end in a singleton list,
- or both lists end in the same list.
\<close>
@@ -1258,7 +1257,7 @@
subsubsection \<open>@{const set}\<close>
-declare list.set[code_post] --"pretty output"
+declare list.set[code_post] \<comment>"pretty output"
lemma finite_set [iff]: "finite (set xs)"
by (induct xs) auto
@@ -2782,7 +2781,7 @@
subsubsection \<open>@{const fold} with natural argument order\<close>
-lemma fold_simps [code]: -- \<open>eta-expanded variant for generated code -- enables tail-recursion optimisation in Scala\<close>
+lemma fold_simps [code]: \<comment> \<open>eta-expanded variant for generated code -- enables tail-recursion optimisation in Scala\<close>
"fold f [] s = s"
"fold f (x # xs) s = fold f xs (f x s)"
by simp_all
@@ -2934,7 +2933,7 @@
lemma foldl_conv_fold: "foldl f s xs = fold (\<lambda>x s. f s x) xs s"
by (induct xs arbitrary: s) simp_all
-lemma foldr_conv_foldl: -- \<open>The ``Third Duality Theorem'' in Bird \& Wadler:\<close>
+lemma foldr_conv_foldl: \<comment> \<open>The ``Third Duality Theorem'' in Bird \& Wadler:\<close>
"foldr f xs a = foldl (\<lambda>x y. f y x) a (rev xs)"
by (simp add: foldr_conv_fold foldl_conv_fold)
@@ -2980,7 +2979,7 @@
subsubsection \<open>@{const upt}\<close>
lemma upt_rec[code]: "[i..<j] = (if i<j then i#[Suc i..<j] else [])"
--- \<open>simp does not terminate!\<close>
+\<comment> \<open>simp does not terminate!\<close>
by (induct j) auto
lemmas upt_rec_numeral[simp] = upt_rec[of "numeral m" "numeral n"] for m n
@@ -3000,14 +2999,14 @@
done
lemma upt_Suc_append: "i <= j ==> [i..<(Suc j)] = [i..<j]@[j]"
--- \<open>Only needed if @{text upt_Suc} is deleted from the simpset.\<close>
+\<comment> \<open>Only needed if \<open>upt_Suc\<close> is deleted from the simpset.\<close>
by simp
lemma upt_conv_Cons: "i < j ==> [i..<j] = i # [Suc i..<j]"
by (simp add: upt_rec)
lemma upt_add_eq_append: "i<=j ==> [i..<j+k] = [i..<j]@[j..<j+k]"
--- \<open>LOOPS as a simprule, since @{text "j <= j"}.\<close>
+\<comment> \<open>LOOPS as a simprule, since \<open>j <= j\<close>.\<close>
by (induct k) auto
lemma length_upt [simp]: "length [i..<j] = j - i"
@@ -3080,7 +3079,7 @@
done
lemma take_equalityI: "(\<forall>i. take i xs = take i ys) ==> xs = ys"
--- \<open>The famous take-lemma.\<close>
+\<comment> \<open>The famous take-lemma.\<close>
apply (drule_tac x = "max (length xs) (length ys)" in spec)
apply (simp add: le_max_iff_disj)
done
@@ -3110,7 +3109,7 @@
by (simp add: nth_Cons')
-subsubsection \<open>@{text upto}: interval-list on @{typ int}\<close>
+subsubsection \<open>\<open>upto\<close>: interval-list on @{typ int}\<close>
function upto :: "int \<Rightarrow> int \<Rightarrow> int list" ("(1[_../_])") where
"upto i j = (if i \<le> j then i # [i+1..j] else [])"
@@ -5155,14 +5154,14 @@
qed
-subsubsection \<open>@{text sorted_list_of_set}\<close>
+subsubsection \<open>\<open>sorted_list_of_set\<close>\<close>
text\<open>This function maps (finite) linearly ordered sets to sorted
lists. Warning: in most cases it is not a good idea to convert from
sets to lists but one should convert in the other direction (via
@{const set}).\<close>
-subsubsection \<open>@{text sorted_list_of_set}\<close>
+subsubsection \<open>\<open>sorted_list_of_set\<close>\<close>
text\<open>This function maps (finite) linearly ordered sets to sorted
lists. Warning: in most cases it is not a good idea to convert from
@@ -5230,7 +5229,7 @@
by (rule sorted_distinct_set_unique) simp_all
-subsubsection \<open>@{text lists}: the list-forming operator over sets\<close>
+subsubsection \<open>\<open>lists\<close>: the list-forming operator over sets\<close>
inductive_set
lists :: "'a set => 'a list set"
@@ -5277,7 +5276,7 @@
lemmas append_in_lists_conv [iff] = append_in_listsp_conv [to_set]
lemma in_listsp_conv_set: "(listsp A xs) = (\<forall>x \<in> set xs. A x)"
--- \<open>eliminate @{text listsp} in favour of @{text set}\<close>
+\<comment> \<open>eliminate \<open>listsp\<close> in favour of \<open>set\<close>\<close>
by (induct xs) auto
lemmas in_lists_conv_set [code_unfold] = in_listsp_conv_set [to_set]
@@ -5326,7 +5325,7 @@
subsubsection \<open>Lists as Cartesian products\<close>
-text\<open>@{text"set_Cons A Xs"}: the set of lists with head drawn from
+text\<open>\<open>set_Cons A Xs\<close>: the set of lists with head drawn from
@{term A} and tail drawn from @{term Xs}.\<close>
definition set_Cons :: "'a set \<Rightarrow> 'a list set \<Rightarrow> 'a list set" where
@@ -5350,7 +5349,7 @@
text\<open>These orderings preserve well-foundedness: shorter lists
precede longer lists. These ordering are not used in dictionaries.\<close>
-primrec -- \<open>The lexicographic ordering for lists of the specified length\<close>
+primrec \<comment> \<open>The lexicographic ordering for lists of the specified length\<close>
lexn :: "('a \<times> 'a) set \<Rightarrow> nat \<Rightarrow> ('a list \<times> 'a list) set" where
"lexn r 0 = {}" |
"lexn r (Suc n) =
@@ -5358,11 +5357,11 @@
{(xs, ys). length xs = Suc n \<and> length ys = Suc n}"
definition lex :: "('a \<times> 'a) set \<Rightarrow> ('a list \<times> 'a list) set" where
-"lex r = (\<Union>n. lexn r n)" -- \<open>Holds only between lists of the same length\<close>
+"lex r = (\<Union>n. lexn r n)" \<comment> \<open>Holds only between lists of the same length\<close>
definition lenlex :: "('a \<times> 'a) set => ('a list \<times> 'a list) set" where
"lenlex r = inv_image (less_than <*lex*> lex r) (\<lambda>xs. (length xs, xs))"
- -- \<open>Compares lists by their length and then lexicographically\<close>
+ \<comment> \<open>Compares lists by their length and then lexicographically\<close>
lemma wf_lexn: "wf r ==> wf (lexn r n)"
apply (induct n, simp, simp)
@@ -5486,7 +5485,7 @@
apply (rule_tac x="drop (Suc i) y" in exI)
by (simp add: Cons_nth_drop_Suc)
--- \<open>lexord is extension of partial ordering List.lex\<close>
+\<comment> \<open>lexord is extension of partial ordering List.lex\<close>
lemma lexord_lex: "(x,y) \<in> lex r = ((x,y) \<in> lexord r \<and> length x = length y)"
apply (rule_tac x = y in spec)
apply (induct_tac x, clarsimp)
@@ -6159,7 +6158,7 @@
[code_abbrev]: "member xs x \<longleftrightarrow> x \<in> set xs"
text \<open>
- Use @{text member} only for generating executable code. Otherwise use
+ Use \<open>member\<close> only for generating executable code. Otherwise use
@{prop "x \<in> set xs"} instead --- it is much easier to reason about.
\<close>
@@ -6184,8 +6183,8 @@
list_ex1_iff [code_abbrev]: "list_ex1 P xs \<longleftrightarrow> (\<exists>! x. x \<in> set xs \<and> P x)"
text \<open>
- Usually you should prefer @{text "\<forall>x\<in>set xs"}, @{text "\<exists>x\<in>set xs"}
- and @{text "\<exists>!x. x\<in>set xs \<and> _"} over @{const list_all}, @{const list_ex}
+ Usually you should prefer \<open>\<forall>x\<in>set xs\<close>, \<open>\<exists>x\<in>set xs\<close>
+ and \<open>\<exists>!x. x\<in>set xs \<and> _\<close> over @{const list_all}, @{const list_ex}
and @{const list_ex1} in specifications.
\<close>
@@ -6322,7 +6321,7 @@
"(\<exists>m\<le>n::nat. P m) \<longleftrightarrow> (\<exists>m \<in> {0..n}. P m)"
by auto
-text\<open>Bounded @{text LEAST} operator:\<close>
+text\<open>Bounded \<open>LEAST\<close> operator:\<close>
definition "Bleast S P = (LEAST x. x \<in> S \<and> P x)"
@@ -6422,8 +6421,8 @@
"map f (filter P xs) = map_filter (\<lambda>x. if P x then Some (f x) else None) xs"
by (simp add: map_filter_def)
-text \<open>Optimized code for @{text"\<forall>i\<in>{a..b::int}"} and @{text"\<forall>n:{a..<b::nat}"}
-and similiarly for @{text"\<exists>"}.\<close>
+text \<open>Optimized code for \<open>\<forall>i\<in>{a..b::int}\<close> and \<open>\<forall>n:{a..<b::nat}\<close>
+and similiarly for \<open>\<exists>\<close>.\<close>
definition all_interval_nat :: "(nat \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where
"all_interval_nat P i j \<longleftrightarrow> (\<forall>n \<in> {i..<j}. P n)"
--- a/src/HOL/MacLaurin.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/MacLaurin.thy Mon Dec 07 10:38:04 2015 +0100
@@ -209,7 +209,7 @@
f h = (\<Sum>m<n. diff m 0 / (fact m) * h ^ m) +
diff n t / (fact n) * h ^ n"
proof -
- txt "Transform @{text ABL'} into @{text derivative_intros} format."
+ txt "Transform \<open>ABL'\<close> into \<open>derivative_intros\<close> format."
note DERIV' = DERIV_chain'[OF _ DERIV[rule_format], THEN DERIV_cong]
from assms
have "\<exists>t>0. t < - h \<and>
--- a/src/HOL/Map.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Map.thy Mon Dec 07 10:38:04 2015 +0100
@@ -275,7 +275,7 @@
by (auto simp: map_comp_def split: option.splits)
-subsection \<open>@{text "++"}\<close>
+subsection \<open>\<open>++\<close>\<close>
lemma map_add_empty[simp]: "m ++ empty = m"
by(simp add: map_add_def)
@@ -640,7 +640,7 @@
by (auto simp add: ran_def)
-subsection \<open>@{text "map_le"}\<close>
+subsection \<open>\<open>map_le\<close>\<close>
lemma map_le_empty [simp]: "empty \<subseteq>\<^sub>m g"
by (simp add: map_le_def)
--- a/src/HOL/Meson.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Meson.thy Mon Dec 07 10:38:04 2015 +0100
@@ -22,14 +22,14 @@
and not_exD: "!!P. ~(\<exists>x. P(x)) ==> \<forall>x. ~P(x)"
by fast+
-text \<open>Removal of @{text "-->"} and @{text "<->"} (positive and
+text \<open>Removal of \<open>-->\<close> and \<open><->\<close> (positive and
negative occurrences)\<close>
lemma imp_to_disjD: "P-->Q ==> ~P | Q"
and not_impD: "~(P-->Q) ==> P & ~Q"
and iff_to_disjD: "P=Q ==> (~P | Q) & (~Q | P)"
and not_iffD: "~(P=Q) ==> (P | Q) & (~P | ~Q)"
- -- \<open>Much more efficient than @{prop "(P & ~Q) | (Q & ~P)"} for computing CNF\<close>
+ \<comment> \<open>Much more efficient than @{prop "(P & ~Q) | (Q & ~P)"} for computing CNF\<close>
and not_refl_disj_D: "x ~= x | P ==> P"
by fast+
@@ -46,8 +46,8 @@
text \<open>Disjunction\<close>
lemma disj_exD: "!!P Q. (\<exists>x. P(x)) | (\<exists>x. Q(x)) ==> \<exists>x. P(x) | Q(x)"
- -- \<open>DO NOT USE with forall-Skolemization: makes fewer schematic variables!!\<close>
- -- \<open>With ex-Skolemization, makes fewer Skolem constants\<close>
+ \<comment> \<open>DO NOT USE with forall-Skolemization: makes fewer schematic variables!!\<close>
+ \<comment> \<open>With ex-Skolemization, makes fewer Skolem constants\<close>
and disj_exD1: "!!P Q. (\<exists>x. P(x)) | Q ==> \<exists>x. P(x) | Q"
and disj_exD2: "!!P Q. P | (\<exists>x. Q(x)) ==> \<exists>x. P | Q(x)"
by fast+
@@ -75,7 +75,7 @@
lemma make_pos_rule: "P|Q ==> ((P==>~P) ==> Q)"
by blast
-text\<open>Versions of @{text make_neg_rule} and @{text make_pos_rule} that don't
+text\<open>Versions of \<open>make_neg_rule\<close> and \<open>make_pos_rule\<close> that don't
insert new assumptions, for ordinary resolution.\<close>
lemmas make_neg_rule' = make_refined_neg_rule
--- a/src/HOL/Nat.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Nat.thy Mon Dec 07 10:38:04 2015 +0100
@@ -18,12 +18,12 @@
ML_file "~~/src/Provers/Arith/fast_lin_arith.ML"
-subsection \<open>Type @{text ind}\<close>
+subsection \<open>Type \<open>ind\<close>\<close>
typedecl ind
axiomatization Zero_Rep :: ind and Suc_Rep :: "ind => ind" where
- -- \<open>the axiom of infinity in 2 parts\<close>
+ \<comment> \<open>the axiom of infinity in 2 parts\<close>
Suc_Rep_inject: "Suc_Rep x = Suc_Rep y ==> x = y" and
Suc_Rep_not_Zero_Rep: "Suc_Rep x \<noteq> Zero_Rep"
@@ -79,7 +79,7 @@
shows "P n"
using assms
apply (unfold Zero_nat_def Suc_def)
-apply (rule Rep_Nat_inverse [THEN subst]) -- \<open>types force good instantiation\<close>
+apply (rule Rep_Nat_inverse [THEN subst]) \<comment> \<open>types force good instantiation\<close>
apply (erule Nat_Rep_Nat [THEN Nat.induct])
apply (iprover elim: Nat_Abs_Nat_inverse [THEN subst])
done
@@ -96,7 +96,7 @@
apply (simp only: Suc_not_Zero)
done
--- \<open>Avoid name clashes by prefixing the output of @{text old_rep_datatype} with @{text old}.\<close>
+\<comment> \<open>Avoid name clashes by prefixing the output of \<open>old_rep_datatype\<close> with \<open>old\<close>.\<close>
setup \<open>Sign.mandatory_path "old"\<close>
old_rep_datatype "0 :: nat" Suc
@@ -107,7 +107,7 @@
setup \<open>Sign.parent_path\<close>
--- \<open>But erase the prefix for properties that are not generated by @{text free_constructors}.\<close>
+\<comment> \<open>But erase the prefix for properties that are not generated by \<open>free_constructors\<close>.\<close>
setup \<open>Sign.mandatory_path "nat"\<close>
declare
@@ -126,7 +126,7 @@
declare nat.sel[code del]
-hide_const (open) Nat.pred -- \<open>hide everything related to the selector\<close>
+hide_const (open) Nat.pred \<comment> \<open>hide everything related to the selector\<close>
hide_fact
nat.case_eq_if
nat.collapse
@@ -137,12 +137,12 @@
nat.split_sel_asm
lemma nat_exhaust [case_names 0 Suc, cases type: nat]:
- -- \<open>for backward compatibility -- names of variables differ\<close>
+ \<comment> \<open>for backward compatibility -- names of variables differ\<close>
"(y = 0 \<Longrightarrow> P) \<Longrightarrow> (\<And>nat. y = Suc nat \<Longrightarrow> P) \<Longrightarrow> P"
by (rule old.nat.exhaust)
lemma nat_induct [case_names 0 Suc, induct type: nat]:
- -- \<open>for backward compatibility -- names of variables differ\<close>
+ \<comment> \<open>for backward compatibility -- names of variables differ\<close>
fixes n
assumes "P 0" and "\<And>n. P n \<Longrightarrow> P (Suc n)"
shows "P n"
@@ -313,7 +313,7 @@
shows "m + k = n + k \<longleftrightarrow> m = n"
by (fact add_right_cancel)
-text \<open>Reasoning about @{text "m + 0 = 0"}, etc.\<close>
+text \<open>Reasoning about \<open>m + 0 = 0\<close>, etc.\<close>
lemma add_is_0 [iff]:
fixes m n :: nat
@@ -630,7 +630,7 @@
apply (blast dest: Suc_lessD)
done
-text \<open>Can be used with @{text less_Suc_eq} to get @{term "n = m | n < m"}\<close>
+text \<open>Can be used with \<open>less_Suc_eq\<close> to get @{term "n = m | n < m"}\<close>
lemma not_less_eq: "\<not> m < n \<longleftrightarrow> n < Suc m"
unfolding not_less less_Suc_eq_le ..
@@ -654,14 +654,14 @@
lemma Suc_leI: "m < n ==> Suc(m) \<le> n"
unfolding Suc_le_eq .
-text \<open>Stronger version of @{text Suc_leD}\<close>
+text \<open>Stronger version of \<open>Suc_leD\<close>\<close>
lemma Suc_le_lessD: "Suc m \<le> n ==> m < n"
unfolding Suc_le_eq .
lemma less_imp_le_nat: "m < n ==> m \<le> (n::nat)"
unfolding less_eq_Suc_le by (rule Suc_leD)
-text \<open>For instance, @{text "(Suc m < Suc n) = (Suc m \<le> n) = (m < n)"}\<close>
+text \<open>For instance, \<open>(Suc m < Suc n) = (Suc m \<le> n) = (m < n)\<close>\<close>
lemmas le_simps = less_imp_le_nat less_Suc_eq_le Suc_le_eq
@@ -673,7 +673,7 @@
lemma le_eq_less_or_eq: "(m \<le> (n::nat)) = (m < n | m=n)"
by (rule le_less)
-text \<open>Useful with @{text blast}.\<close>
+text \<open>Useful with \<open>blast\<close>.\<close>
lemma eq_imp_le: "(m::nat) = n ==> m \<le> n"
by auto
@@ -717,7 +717,7 @@
lemma neq0_conv[iff]: fixes n :: nat shows "(n \<noteq> 0) = (0 < n)"
by (cases n) simp_all
-text \<open>This theorem is useful with @{text blast}\<close>
+text \<open>This theorem is useful with \<open>blast\<close>\<close>
lemma gr0I: "((n::nat) = 0 ==> False) ==> 0 < n"
by (rule neq0_conv[THEN iffD1], iprover)
@@ -762,7 +762,7 @@
apply (induct j, simp_all)
done
-text \<open>Deleted @{text less_natE}; use @{text "less_imp_Suc_add RS exE"}\<close>
+text \<open>Deleted \<open>less_natE\<close>; use \<open>less_imp_Suc_add RS exE\<close>\<close>
lemma less_imp_Suc_add: "m < n ==> (\<exists>k. n = Suc (m + k))"
apply (induct n)
apply (simp_all add: order_le_less)
@@ -773,7 +773,7 @@
lemma le_Suc_ex: "(k::nat) \<le> l \<Longrightarrow> (\<exists>n. l = k + n)"
by (auto simp: less_Suc_eq_le[symmetric] dest: less_imp_Suc_add)
-text \<open>strict, in 1st argument; proof is by induction on @{text "k > 0"}\<close>
+text \<open>strict, in 1st argument; proof is by induction on \<open>k > 0\<close>\<close>
lemma mult_less_mono2: "(i::nat) < j ==> 0<k ==> k * i < k * j"
apply(auto simp: gr0_conv_Suc)
apply (induct_tac m)
@@ -786,7 +786,7 @@
by (induct m n rule: diff_induct) simp_all
-text\<open>The naturals form an ordered @{text semidom}\<close>
+text\<open>The naturals form an ordered \<open>semidom\<close>\<close>
instance nat :: linordered_semidom
proof
show "0 < (1::nat)" by simp
@@ -1015,9 +1015,9 @@
obtain n where "n = V x" by auto
moreover have "\<And>x. V x = n \<Longrightarrow> P x"
proof (induct n rule: infinite_descent0)
- case 0 -- "i.e. $V(x) = 0$"
+ case 0 \<comment> "i.e. $V(x) = 0$"
with A0 show "P x" by auto
- next -- "now $n>0$ and $P(x)$ does not hold for some $x$ with $V(x)=n$"
+ next \<comment> "now $n>0$ and $P(x)$ does not hold for some $x$ with $V(x)=n$"
case (smaller n)
then obtain x where vxn: "V x = n " and "V x > 0 \<and> \<not> P x" by auto
with A1 obtain y where "V y < V x \<and> \<not> P y" by auto
@@ -1040,8 +1040,8 @@
ultimately show "P x" by auto
qed
-text \<open>A [clumsy] way of lifting @{text "<"}
- monotonicity to @{text "\<le>"} monotonicity\<close>
+text \<open>A [clumsy] way of lifting \<open><\<close>
+ monotonicity to \<open>\<le>\<close> monotonicity\<close>
lemma less_mono_imp_le_mono:
"\<lbrakk> !!i j::nat. i < j \<Longrightarrow> f i < f j; i \<le> j \<rbrakk> \<Longrightarrow> f i \<le> ((f j)::nat)"
by (simp add: order_le_less) (blast)
@@ -1109,7 +1109,7 @@
lemma add_leE: "(m::nat) + k \<le> n ==> (m \<le> n ==> k \<le> n ==> R) ==> R"
by (blast dest: add_leD1 add_leD2)
-text \<open>needs @{text "!!k"} for @{text ac_simps} to work\<close>
+text \<open>needs \<open>!!k\<close> for \<open>ac_simps\<close> to work\<close>
lemma less_add_eq_less: "!!k::nat. k < l ==> m + l = k + n ==> m < n"
by (force simp del: add_Suc_right
simp add: less_iff_Suc_add add_Suc_right [symmetric] ac_simps)
@@ -1177,14 +1177,14 @@
lemma nat_diff_split:
"P(a - b::nat) = ((a<b --> P 0) & (ALL d. a = b + d --> P d))"
- -- \<open>elimination of @{text -} on @{text nat}\<close>
+ \<comment> \<open>elimination of \<open>-\<close> on \<open>nat\<close>\<close>
by (cases "a < b")
(auto simp add: diff_is_0_eq [THEN iffD2] diff_add_inverse
not_less le_less dest!: add_eq_self_zero add_eq_self_zero[OF sym])
lemma nat_diff_split_asm:
"P(a - b::nat) = (~ (a < b & ~ P 0 | (EX d. a = b + d & ~ P d)))"
- -- \<open>elimination of @{text -} on @{text nat} in assumptions\<close>
+ \<comment> \<open>elimination of \<open>-\<close> on \<open>nat\<close> in assumptions\<close>
by (auto split: nat_diff_split)
lemma Suc_pred': "0 < n ==> n = Suc(n - 1)"
@@ -1214,14 +1214,14 @@
lemma mult_le_mono2: "i \<le> (j::nat) ==> k * i \<le> k * j"
by (simp add: mult_left_mono)
-text \<open>@{text "\<le>"} monotonicity, BOTH arguments\<close>
+text \<open>\<open>\<le>\<close> monotonicity, BOTH arguments\<close>
lemma mult_le_mono: "i \<le> (j::nat) ==> k \<le> l ==> i * k \<le> j * l"
by (simp add: mult_mono)
lemma mult_less_mono1: "(i::nat) < j ==> 0 < k ==> i * k < j * k"
by (simp add: mult_strict_right_mono)
-text\<open>Differs from the standard @{text zero_less_mult_iff} in that
+text\<open>Differs from the standard \<open>zero_less_mult_iff\<close> in that
there are no negative numbers.\<close>
lemma nat_0_less_mult_iff [simp]: "(0 < (m::nat) * n) = (0 < m & 0 < n)"
apply (induct m)
@@ -1265,7 +1265,7 @@
lemma le_cube: "(m::nat) \<le> m * (m * m)"
by (cases m) (auto intro: le_add1)
-text \<open>Lemma for @{text gcd}\<close>
+text \<open>Lemma for \<open>gcd\<close>\<close>
lemma mult_eq_self_implies_10: "(m::nat) = m * n ==> n = 1 | m = 0"
apply (drule sym)
apply (rule disjCI)
@@ -1317,7 +1317,7 @@
notation (latex output)
compower ("(_\<^bsup>_\<^esup>)" [1000] 1000)
-text \<open>@{text "f ^^ n = f o ... o f"}, the n-fold composition of @{text f}\<close>
+text \<open>\<open>f ^^ n = f o ... o f\<close>, the n-fold composition of \<open>f\<close>\<close>
overloading
funpow == "compow :: nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a)"
@@ -1450,7 +1450,7 @@
by (intro gfp_upperbound) (simp del: funpow.simps)
qed
-subsection \<open>Embedding of the naturals into any @{text semiring_1}: @{term of_nat}\<close>
+subsection \<open>Embedding of the naturals into any \<open>semiring_1\<close>: @{term of_nat}\<close>
context semiring_1
begin
@@ -1477,7 +1477,7 @@
primrec of_nat_aux :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" where
"of_nat_aux inc 0 i = i"
-| "of_nat_aux inc (Suc n) i = of_nat_aux inc n (inc i)" -- \<open>tail recursive\<close>
+| "of_nat_aux inc (Suc n) i = of_nat_aux inc n (inc i)" \<comment> \<open>tail recursive\<close>
lemma of_nat_code:
"of_nat n = of_nat_aux (\<lambda>i. i + 1) n 0"
@@ -1545,7 +1545,7 @@
lemma of_nat_less_imp_less: "of_nat m < of_nat n \<Longrightarrow> m < n"
by simp
-text\<open>Every @{text linordered_semidom} has characteristic zero.\<close>
+text\<open>Every \<open>linordered_semidom\<close> has characteristic zero.\<close>
subclass semiring_char_0 proof
qed (auto intro!: injI simp add: eq_iff)
@@ -1685,7 +1685,7 @@
case True
then show ?thesis
by (induct n n' rule: less_Suc_induct [consumes 1]) (auto intro: mono)
-qed (insert \<open>n \<le> n'\<close>, auto) -- \<open>trivial for @{prop "n = n'"}\<close>
+qed (insert \<open>n \<le> n'\<close>, auto) \<comment> \<open>trivial for @{prop "n = n'"}\<close>
lemma lift_Suc_antimono_le:
assumes mono: "\<And>n. f n \<ge> f (Suc n)" and "n \<le> n'"
@@ -1694,7 +1694,7 @@
case True
then show ?thesis
by (induct n n' rule: less_Suc_induct [consumes 1]) (auto intro: mono)
-qed (insert \<open>n \<le> n'\<close>, auto) -- \<open>trivial for @{prop "n = n'"}\<close>
+qed (insert \<open>n \<le> n'\<close>, auto) \<comment> \<open>trivial for @{prop "n = n'"}\<close>
lemma lift_Suc_mono_less:
assumes mono: "\<And>n. f n < f (Suc n)" and "n < n'"
@@ -1750,13 +1750,13 @@
by arith
lemma le_diff_conv2: "k \<le> j ==> (i \<le> j-k) = (i+k \<le> (j::nat))"
- by (fact le_diff_conv2) -- \<open>FIXME delete\<close>
+ by (fact le_diff_conv2) \<comment> \<open>FIXME delete\<close>
lemma diff_diff_cancel [simp]: "i \<le> (n::nat) ==> n - (n - i) = i"
by arith
lemma le_add_diff: "k \<le> (n::nat) ==> m \<le> n + m - k"
- by (fact le_add_diff) -- \<open>FIXME delete\<close>
+ by (fact le_add_diff) \<comment> \<open>FIXME delete\<close>
(*Replaces the previous diff_less and le_diff_less, which had the stronger
second premise n\<le>m*)
@@ -1829,8 +1829,7 @@
lemmas add_diff_assoc2 = diff_add_assoc2[symmetric]
declare diff_diff_left [simp] add_diff_assoc [simp] add_diff_assoc2[simp]
-text\<open>At present we prove no analogue of @{text not_less_Least} or @{text
-Least_Suc}, since there appears to be no need.\<close>
+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>
text\<open>Lemmas for ex/Factorization\<close>
@@ -2015,7 +2014,7 @@
subsection \<open>Size of a datatype value\<close>
class size =
- fixes size :: "'a \<Rightarrow> nat" -- \<open>see further theory @{text Wellfounded}\<close>
+ fixes size :: "'a \<Rightarrow> nat" \<comment> \<open>see further theory \<open>Wellfounded\<close>\<close>
instantiation nat :: size
begin
--- a/src/HOL/Nitpick.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Nitpick.thy Mon Dec 07 10:38:04 2015 +0100
@@ -116,7 +116,7 @@
text \<open>
Auxiliary definitions used to provide an alternative representation for
-@{text rat} and @{text real}.
+\<open>rat\<close> and \<open>real\<close>.
\<close>
function nat_gcd :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
--- a/src/HOL/Num.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Num.thy Mon Dec 07 10:38:04 2015 +0100
@@ -9,7 +9,7 @@
imports BNF_Least_Fixpoint
begin
-subsection \<open>The @{text num} type\<close>
+subsection \<open>The \<open>num\<close> type\<close>
datatype num = One | Bit0 num | Bit1 num
@@ -83,8 +83,8 @@
text \<open>
From now on, there are two possible models for @{typ num}:
- as positive naturals (rule @{text "num_induct"})
- and as digit representation (rules @{text "num.induct"}, @{text "num.cases"}).
+ as positive naturals (rule \<open>num_induct\<close>)
+ and as digit representation (rules \<open>num.induct\<close>, \<open>num.cases\<close>).
\<close>
@@ -177,7 +177,7 @@
lemma le_num_One_iff: "x \<le> num.One \<longleftrightarrow> x = num.One"
by (simp add: antisym_conv)
-text \<open>Rules using @{text One} and @{text inc} as constructors\<close>
+text \<open>Rules using \<open>One\<close> and \<open>inc\<close> as constructors\<close>
lemma add_One: "x + One = inc x"
by (simp add: num_eq_iff nat_of_num_add nat_of_num_inc)
@@ -237,7 +237,7 @@
text \<open>
We embed binary representations into a generic algebraic
- structure using @{text numeral}.
+ structure using \<open>numeral\<close>.
\<close>
class numeral = one + semigroup_add
@@ -327,7 +327,7 @@
@{const numeral} is a morphism.
\<close>
-subsubsection \<open>Structures with addition: class @{text numeral}\<close>
+subsubsection \<open>Structures with addition: class \<open>numeral\<close>\<close>
context numeral
begin
@@ -354,7 +354,7 @@
end
subsubsection \<open>
- Structures with negation: class @{text neg_numeral}
+ Structures with negation: class \<open>neg_numeral\<close>
\<close>
class neg_numeral = numeral + group_add
@@ -492,7 +492,7 @@
end
subsubsection \<open>
- Structures with multiplication: class @{text semiring_numeral}
+ Structures with multiplication: class \<open>semiring_numeral\<close>
\<close>
class semiring_numeral = semiring + monoid_mult
@@ -518,7 +518,7 @@
end
subsubsection \<open>
- Structures with a zero: class @{text semiring_1}
+ Structures with a zero: class \<open>semiring_1\<close>
\<close>
context semiring_1
@@ -548,7 +548,7 @@
by (simp_all add: Let_def)
subsubsection \<open>
- Equality: class @{text semiring_char_0}
+ Equality: class \<open>semiring_char_0\<close>
\<close>
context semiring_char_0
@@ -581,7 +581,7 @@
end
subsubsection \<open>
- Comparisons: class @{text linordered_semidom}
+ Comparisons: class \<open>linordered_semidom\<close>
\<close>
text \<open>Could be perhaps more general than here.\<close>
@@ -672,7 +672,7 @@
end
subsubsection \<open>
- Multiplication and negation: class @{text ring_1}
+ Multiplication and negation: class \<open>ring_1\<close>
\<close>
context ring_1
@@ -696,7 +696,7 @@
end
subsubsection \<open>
- Equality using @{text iszero} for rings with non-zero characteristic
+ Equality using \<open>iszero\<close> for rings with non-zero characteristic
\<close>
context ring_1
@@ -728,16 +728,15 @@
lemma eq_iff_iszero_diff: "x = y \<longleftrightarrow> iszero (x - y)"
unfolding iszero_def by (rule eq_iff_diff_eq_0)
-text \<open>The @{text "eq_numeral_iff_iszero"} lemmas are not declared
-@{text "[simp]"} by default, because for rings of characteristic zero,
-better simp rules are possible. For a type like integers mod @{text
-"n"}, type-instantiated versions of these rules should be added to the
+text \<open>The \<open>eq_numeral_iff_iszero\<close> lemmas are not declared
+\<open>[simp]\<close> by default, because for rings of characteristic zero,
+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
simplifier, along with a type-specific rule for deciding propositions
-of the form @{text "iszero (numeral w)"}.
+of the form \<open>iszero (numeral w)\<close>.
bh: Maybe it would not be so bad to just declare these as simp
rules anyway? I should test whether these rules take precedence over
-the @{text "ring_char_0"} rules in the simplifier.
+the \<open>ring_char_0\<close> rules in the simplifier.
\<close>
lemma eq_numeral_iff_iszero:
@@ -759,7 +758,7 @@
end
subsubsection \<open>
- Equality and negation: class @{text ring_char_0}
+ Equality and negation: class \<open>ring_char_0\<close>
\<close>
class ring_char_0 = ring_1 + semiring_char_0
@@ -835,7 +834,7 @@
end
subsubsection \<open>
- Structures with negation and order: class @{text linordered_idom}
+ Structures with negation and order: class \<open>linordered_idom\<close>
\<close>
context linordered_idom
@@ -1179,7 +1178,7 @@
text \<open>
For making a minimal simpset, one must include these default simprules.
- Also include @{text simp_thms}.
+ Also include \<open>simp_thms\<close>.
\<close>
lemmas arith_simps =
@@ -1209,11 +1208,11 @@
eq_numeral_simps eq_neg_numeral_simps eq_numeral_extra
lemma Let_numeral [simp]: "Let (numeral v) f = f (numeral v)"
- -- \<open>Unfold all @{text let}s involving constants\<close>
+ \<comment> \<open>Unfold all \<open>let\<close>s involving constants\<close>
unfolding Let_def ..
lemma Let_neg_numeral [simp]: "Let (- numeral v) f = f (- numeral v)"
- -- \<open>Unfold all @{text let}s involving constants\<close>
+ \<comment> \<open>Unfold all \<open>let\<close>s involving constants\<close>
unfolding Let_def ..
declaration \<open>
--- a/src/HOL/Numeral_Simprocs.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Numeral_Simprocs.thy Mon Dec 07 10:38:04 2015 +0100
@@ -23,12 +23,12 @@
declare split_div [of _ _ "numeral k", arith_split] for k
declare split_mod [of _ _ "numeral k", arith_split] for k
-text \<open>For @{text combine_numerals}\<close>
+text \<open>For \<open>combine_numerals\<close>\<close>
lemma left_add_mult_distrib: "i*u + (j*u + k) = (i+j)*u + (k::nat)"
by (simp add: add_mult_distrib)
-text \<open>For @{text cancel_numerals}\<close>
+text \<open>For \<open>cancel_numerals\<close>\<close>
lemma nat_diff_add_eq1:
"j <= (i::nat) ==> ((i*u + m) - (j*u + n)) = (((i-j)*u + m) - n)"
@@ -62,7 +62,7 @@
"i <= (j::nat) ==> (i*u + m <= j*u + n) = (m <= (j-i)*u + n)"
by (auto split add: nat_diff_split simp add: add_mult_distrib)
-text \<open>For @{text cancel_numeral_factors}\<close>
+text \<open>For \<open>cancel_numeral_factors\<close>\<close>
lemma nat_mult_le_cancel1: "(0::nat) < k ==> (k*m <= k*n) = (m<=n)"
by auto
@@ -83,7 +83,7 @@
lemma nat_mult_dvd_cancel1: "0 < k \<Longrightarrow> (k*m) dvd (k*n::nat) = (m dvd n)"
by(auto)
-text \<open>For @{text cancel_factor}\<close>
+text \<open>For \<open>cancel_factor\<close>\<close>
lemmas nat_mult_le_cancel_disj = mult_le_cancel1
--- a/src/HOL/Option.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Option.thy Mon Dec 07 10:38:04 2015 +0100
@@ -15,12 +15,12 @@
datatype_compat option
lemma [case_names None Some, cases type: option]:
- -- \<open>for backward compatibility -- names of variables differ\<close>
+ \<comment> \<open>for backward compatibility -- names of variables differ\<close>
"(y = None \<Longrightarrow> P) \<Longrightarrow> (\<And>a. y = Some a \<Longrightarrow> P) \<Longrightarrow> P"
by (rule option.exhaust)
lemma [case_names None Some, induct type: option]:
- -- \<open>for backward compatibility -- names of variables differ\<close>
+ \<comment> \<open>for backward compatibility -- names of variables differ\<close>
"P None \<Longrightarrow> (\<And>option. P (Some option)) \<Longrightarrow> P option"
by (rule option.induct)
--- a/src/HOL/Order_Relation.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Order_Relation.thy Mon Dec 07 10:38:04 2015 +0100
@@ -180,9 +180,9 @@
subsubsection \<open>The upper and lower bounds operators\<close>
text\<open>Here we define upper (``above") and lower (``below") bounds operators.
-We think of @{text "r"} as a {\em non-strict} relation. The suffix ``S"
+We think of \<open>r\<close> as a {\em non-strict} relation. The suffix ``S"
at the names of some operators indicates that the bounds are strict -- e.g.,
-@{text "underS a"} is the set of all strict lower bounds of @{text "a"} (w.r.t. @{text "r"}).
+\<open>underS a\<close> is the set of all strict lower bounds of \<open>a\<close> (w.r.t. \<open>r\<close>).
Capitalization of the first letter in the name reminds that the operator acts on sets, rather
than on individual elements.\<close>
@@ -213,9 +213,9 @@
definition ofilter :: "'a rel \<Rightarrow> 'a set \<Rightarrow> bool"
where "ofilter r A \<equiv> (A \<le> Field r) \<and> (\<forall>a \<in> A. under r a \<le> A)"
-text\<open>Note: In the definitions of @{text "Above[S]"} and @{text "Under[S]"},
- we bounded comprehension by @{text "Field r"} in order to properly cover
- the case of @{text "A"} being empty.\<close>
+text\<open>Note: In the definitions of \<open>Above[S]\<close> and \<open>Under[S]\<close>,
+ we bounded comprehension by \<open>Field r\<close> in order to properly cover
+ the case of \<open>A\<close> being empty.\<close>
lemma underS_subset_under: "underS r a \<le> under r a"
by(auto simp add: underS_def under_def)
@@ -362,7 +362,7 @@
ultimately show ?thesis using R_def by blast
qed
-text \<open>The next lemma is a variation of @{text "wf_eq_minimal"} from Wellfounded,
+text \<open>The next lemma is a variation of \<open>wf_eq_minimal\<close> from Wellfounded,
allowing one to assume the set included in the field.\<close>
lemma wf_eq_minimal2:
--- a/src/HOL/Orderings.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Orderings.thy Mon Dec 07 10:38:04 2015 +0100
@@ -18,7 +18,7 @@
fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<preceq>" 50)
and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<prec>" 50)
assumes strict_iff_order: "a \<prec> b \<longleftrightarrow> a \<preceq> b \<and> a \<noteq> b"
- assumes refl: "a \<preceq> a" -- \<open>not @{text iff}: makes problems due to multiple (dual) interpretations\<close>
+ assumes refl: "a \<preceq> a" \<comment> \<open>not \<open>iff\<close>: makes problems due to multiple (dual) interpretations\<close>
and antisym: "a \<preceq> b \<Longrightarrow> b \<preceq> a \<Longrightarrow> a = b"
and trans: "a \<preceq> b \<Longrightarrow> b \<preceq> c \<Longrightarrow> a \<preceq> c"
begin
@@ -39,7 +39,7 @@
"a \<preceq> b \<longleftrightarrow> a \<prec> b \<or> a = b"
by (auto simp add: strict_iff_order refl)
-lemma irrefl: -- \<open>not @{text iff}: makes problems due to multiple (dual) interpretations\<close>
+lemma irrefl: \<comment> \<open>not \<open>iff\<close>: makes problems due to multiple (dual) interpretations\<close>
"\<not> a \<prec> a"
by (simp add: strict_iff_order)
@@ -127,7 +127,7 @@
text \<open>Reflexivity.\<close>
lemma eq_refl: "x = y \<Longrightarrow> x \<le> y"
- -- \<open>This form is useful with the classical reasoner.\<close>
+ \<comment> \<open>This form is useful with the classical reasoner.\<close>
by (erule ssubst) (rule order_refl)
lemma less_irrefl [iff]: "\<not> x < x"
@@ -198,7 +198,7 @@
text \<open>Reflexivity.\<close>
lemma le_less: "x \<le> y \<longleftrightarrow> x < y \<or> x = y"
- -- \<open>NOT suitable for iff, since it can cause PROOF FAILED.\<close>
+ \<comment> \<open>NOT suitable for iff, since it can cause PROOF FAILED.\<close>
by (fact order.order_iff_strict)
lemma le_imp_less_or_eq: "x \<le> y \<Longrightarrow> x < y \<or> x = y"
@@ -1360,7 +1360,7 @@
then show "P (LEAST x. P x)" and "(LEAST x. P x) \<le> k" by auto
qed
--- "The following 3 lemmas are due to Brian Huffman"
+\<comment> "The following 3 lemmas are due to Brian Huffman"
lemma LeastI_ex: "\<exists>x. P x \<Longrightarrow> P (Least P)"
by (erule exE) (erule LeastI)
--- a/src/HOL/Parity.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Parity.thy Mon Dec 07 10:38:04 2015 +0100
@@ -9,7 +9,7 @@
imports Nat_Transfer
begin
-subsection \<open>Ring structures with parity and @{text even}/@{text odd} predicates\<close>
+subsection \<open>Ring structures with parity and \<open>even\<close>/\<open>odd\<close> predicates\<close>
class semiring_parity = comm_semiring_1_cancel + numeral +
assumes odd_one [simp]: "\<not> 2 dvd 1"
--- a/src/HOL/Power.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Power.thy Mon Dec 07 10:38:04 2015 +0100
@@ -465,7 +465,7 @@
"of_nat x ^ n > 0 \<longleftrightarrow> x > 0 \<or> n = 0"
by (induct n) auto
-text\<open>Surely we can strengthen this? It holds for @{text "0<a<1"} too.\<close>
+text\<open>Surely we can strengthen this? It holds for \<open>0<a<1\<close> too.\<close>
lemma power_inject_exp [simp]:
"1 < a \<Longrightarrow> a ^ m = a ^ n \<longleftrightarrow> m = n"
by (force simp add: order_antisym power_le_imp_le_exp)
@@ -482,7 +482,7 @@
by (induct n)
(auto simp add: mult_strict_mono le_less_trans [of 0 a b])
-text\<open>Lemma for @{text power_strict_decreasing}\<close>
+text\<open>Lemma for \<open>power_strict_decreasing\<close>\<close>
lemma power_Suc_less:
"0 < a \<Longrightarrow> a < 1 \<Longrightarrow> a * a ^ n < a ^ n"
by (induct n)
@@ -501,7 +501,7 @@
done
qed
-text\<open>Proof resembles that of @{text power_strict_decreasing}\<close>
+text\<open>Proof resembles that of \<open>power_strict_decreasing\<close>\<close>
lemma power_decreasing [rule_format]:
"n \<le> N \<Longrightarrow> 0 \<le> a \<Longrightarrow> a \<le> 1 \<longrightarrow> a ^ N \<le> a ^ n"
proof (induct N)
@@ -518,7 +518,7 @@
"0 < a \<Longrightarrow> a < 1 \<Longrightarrow> a ^ Suc n < 1"
using power_strict_decreasing [of 0 "Suc n" a] by simp
-text\<open>Proof again resembles that of @{text power_strict_decreasing}\<close>
+text\<open>Proof again resembles that of \<open>power_strict_decreasing\<close>\<close>
lemma power_increasing [rule_format]:
"n \<le> N \<Longrightarrow> 1 \<le> a \<Longrightarrow> a ^ n \<le> a ^ N"
proof (induct N)
@@ -531,7 +531,7 @@
done
qed
-text\<open>Lemma for @{text power_strict_increasing}\<close>
+text\<open>Lemma for \<open>power_strict_increasing\<close>\<close>
lemma power_less_power_Suc:
"1 < a \<Longrightarrow> a ^ n < a * a ^ n"
by (induct n) (auto simp add: mult_strict_left_mono less_trans [OF zero_less_one])
@@ -795,7 +795,7 @@
"Suc 0 ^ n = Suc 0"
by simp
-text\<open>Valid for the naturals, but what if @{text"0<i<1"}?
+text\<open>Valid for the naturals, but what if \<open>0<i<1\<close>?
Premises cannot be weakened: consider the case where @{term "i=0"},
@{term "m=1"} and @{term "n=0"}.\<close>
lemma nat_power_less_imp_less:
--- a/src/HOL/Presburger.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Presburger.thy Mon Dec 07 10:38:04 2015 +0100
@@ -12,7 +12,7 @@
ML_file "Tools/Qelim/qelim.ML"
ML_file "Tools/Qelim/cooper_procedure.ML"
-subsection\<open>The @{text "-\<infinity>"} and @{text "+\<infinity>"} Properties\<close>
+subsection\<open>The \<open>-\<infinity>\<close> and \<open>+\<infinity>\<close> Properties\<close>
lemma minf:
"\<lbrakk>\<exists>(z ::'a::linorder).\<forall>x<z. P x = P' x; \<exists>z.\<forall>x<z. Q x = Q' x\<rbrakk>
@@ -176,7 +176,7 @@
thus "\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> (\<not>d dvd x+t) \<longrightarrow> (\<not>d dvd (x + D) + t)" by auto
qed blast
-subsection\<open>Cooper's Theorem @{text "-\<infinity>"} and @{text "+\<infinity>"} Version\<close>
+subsection\<open>Cooper's Theorem \<open>-\<infinity>\<close> and \<open>+\<infinity>\<close> Version\<close>
subsubsection\<open>First some trivial facts about periodic sets or predicates\<close>
lemma periodic_finite_ex:
@@ -209,7 +209,7 @@
qed
qed auto
-subsubsection\<open>The @{text "-\<infinity>"} Version\<close>
+subsubsection\<open>The \<open>-\<infinity>\<close> Version\<close>
lemma decr_lemma: "0 < (d::int) \<Longrightarrow> x - (abs(x-z)+1) * d < z"
by(induct rule: int_gr_induct,simp_all add:int_distrib)
@@ -277,7 +277,7 @@
ultimately show ?thesis by blast
qed
-subsubsection \<open>The @{text "+\<infinity>"} Version\<close>
+subsubsection \<open>The \<open>+\<infinity>\<close> Version\<close>
lemma plusinfinity:
assumes dpos: "(0::int) < d" and
@@ -372,7 +372,7 @@
shows "d dvd t \<equiv> - d dvd t" and "d dvd t \<equiv> d dvd - t"
by simp_all
-text \<open>\bigskip Theorems for transforming predicates on nat to predicates on @{text int}\<close>
+text \<open>\bigskip Theorems for transforming predicates on nat to predicates on \<open>int\<close>\<close>
lemma zdiff_int_split: "P (int (x - y)) =
((y \<le> x \<longrightarrow> P (int x - int y)) \<and> (x < y \<longrightarrow> P 0))"
--- a/src/HOL/Product_Type.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Product_Type.thy Mon Dec 07 10:38:04 2015 +0100
@@ -15,7 +15,7 @@
free_constructors case_bool for True | False
by auto
-text \<open>Avoid name clashes by prefixing the output of @{text old_rep_datatype} with @{text old}.\<close>
+text \<open>Avoid name clashes by prefixing the output of \<open>old_rep_datatype\<close> with \<open>old\<close>.\<close>
setup \<open>Sign.mandatory_path "old"\<close>
@@ -23,7 +23,7 @@
setup \<open>Sign.parent_path\<close>
-text \<open>But erase the prefix for properties that are not generated by @{text free_constructors}.\<close>
+text \<open>But erase the prefix for properties that are not generated by \<open>free_constructors\<close>.\<close>
setup \<open>Sign.mandatory_path "bool"\<close>
@@ -35,7 +35,7 @@
setup \<open>Sign.parent_path\<close>
declare case_split [cases type: bool]
- -- "prefer plain propositional version"
+ \<comment> "prefer plain propositional version"
lemma
shows [code]: "HOL.equal False P \<longleftrightarrow> \<not> P"
@@ -57,7 +57,7 @@
| class_instance "bool" :: "equal" \<rightharpoonup> (Haskell) -
-subsection \<open>The @{text unit} type\<close>
+subsection \<open>The \<open>unit\<close> type\<close>
typedef unit = "{True}"
by auto
@@ -82,7 +82,7 @@
free_constructors case_unit for "()"
by auto
-text \<open>Avoid name clashes by prefixing the output of @{text old_rep_datatype} with @{text old}.\<close>
+text \<open>Avoid name clashes by prefixing the output of \<open>old_rep_datatype\<close> with \<open>old\<close>.\<close>
setup \<open>Sign.mandatory_path "old"\<close>
@@ -90,7 +90,7 @@
setup \<open>Sign.parent_path\<close>
-text \<open>But erase the prefix for properties that are not generated by @{text free_constructors}.\<close>
+text \<open>But erase the prefix for properties that are not generated by \<open>free_constructors\<close>.\<close>
setup \<open>Sign.mandatory_path "unit"\<close>
@@ -108,7 +108,7 @@
by (rule triv_forall_equality)
text \<open>
- This rewrite counters the effect of simproc @{text unit_eq} on @{term
+ This rewrite counters the effect of simproc \<open>unit_eq\<close> on @{term
[source] "%u::unit. f u"}, replacing it by @{term [source]
f} rather than by @{term [source] "%u. f ()"}.
\<close>
@@ -253,7 +253,7 @@
by (simp add: Pair_def Abs_prod_inject)
qed
-text \<open>Avoid name clashes by prefixing the output of @{text old_rep_datatype} with @{text old}.\<close>
+text \<open>Avoid name clashes by prefixing the output of \<open>old_rep_datatype\<close> with \<open>old\<close>.\<close>
setup \<open>Sign.mandatory_path "old"\<close>
@@ -262,7 +262,7 @@
setup \<open>Sign.parent_path\<close>
-text \<open>But erase the prefix for properties that are not generated by @{text free_constructors}.\<close>
+text \<open>But erase the prefix for properties that are not generated by \<open>free_constructors\<close>.\<close>
setup \<open>Sign.mandatory_path "prod"\<close>
@@ -282,7 +282,7 @@
declare prod.split_asm [no_atp]
text \<open>
- @{thm [source] prod.split} could be declared as @{text "[split]"}
+ @{thm [source] prod.split} could be declared as \<open>[split]\<close>
done after the Splitter has been speeded up significantly;
precompute the constants involved and don't do anything unless the
current goal contains one of those constants.
@@ -314,9 +314,9 @@
"\<lambda>(x, y, zs). b" \<rightleftharpoons> "CONST case_prod (\<lambda>x (y, zs). b)"
"\<lambda>(x, y). b" \<rightleftharpoons> "CONST case_prod (\<lambda>x y. b)"
"_abs (CONST Pair x y) t" \<rightharpoonup> "\<lambda>(x, y). t"
- -- \<open>This rule accommodates tuples in @{text "case C \<dots> (x, y) \<dots> \<Rightarrow> \<dots>"}:
- The @{text "(x, y)"} is parsed as @{text "Pair x y"} because it is @{text logic},
- not @{text pttrn}.\<close>
+ \<comment> \<open>This rule accommodates tuples in \<open>case C \<dots> (x, y) \<dots> \<Rightarrow> \<dots>\<close>:
+ The \<open>(x, y)\<close> is parsed as \<open>Pair x y\<close> because it is \<open>logic\<close>,
+ not \<open>pttrn\<close>.\<close>
text \<open>print @{term "case_prod f"} as @{term "\<lambda>(x, y). f x y"} and
@{term "case_prod (\<lambda>x. f x)"} as @{term "\<lambda>(x, y). f x y"}\<close>
@@ -457,7 +457,7 @@
by (simp add: fun_eq_iff split: prod.split)
lemma case_prod_eta: "(\<lambda>(x, y). f (x, y)) = f"
- -- \<open>Subsumes the old @{text split_Pair} when @{term f} is the identity function.\<close>
+ \<comment> \<open>Subsumes the old \<open>split_Pair\<close> when @{term f} is the identity function.\<close>
by (simp add: fun_eq_iff split: prod.split)
lemma case_prod_comp: "(case x of (a, b) \<Rightarrow> (f \<circ> g) a b) = f (g (fst x)) (snd x)"
@@ -483,8 +483,8 @@
text \<open>
The rule @{thm [source] split_paired_all} does not work with the
Simplifier because it also affects premises in congrence rules,
- where this can lead to premises of the form @{text "!!a b. ... =
- ?P(a, b)"} which cannot be solved by reflexivity.
+ where this can lead to premises of the form \<open>!!a b. ... =
+ ?P(a, b)\<close> which cannot be solved by reflexivity.
\<close>
lemmas split_tupled_all = split_paired_all unit_all_eq2
@@ -518,22 +518,21 @@
setup \<open>map_theory_claset (fn ctxt => ctxt addSbefore ("split_all_tac", split_all_tac))\<close>
lemma split_paired_All [simp, no_atp]: "(ALL x. P x) = (ALL a b. P (a, b))"
- -- \<open>@{text "[iff]"} is not a good idea because it makes @{text blast} loop\<close>
+ \<comment> \<open>\<open>[iff]\<close> is not a good idea because it makes \<open>blast\<close> loop\<close>
by fast
lemma split_paired_Ex [simp, no_atp]: "(EX x. P x) = (EX a b. P (a, b))"
by fast
lemma split_paired_The [no_atp]: "(THE x. P x) = (THE (a, b). P (a, b))"
- -- \<open>Can't be added to simpset: loops!\<close>
+ \<comment> \<open>Can't be added to simpset: loops!\<close>
by (simp add: case_prod_eta)
text \<open>
Simplification procedure for @{thm [source] cond_case_prod_eta}. Using
@{thm [source] case_prod_eta} as a rewrite rule is not general enough,
and using @{thm [source] cond_case_prod_eta} directly would render some
- existing proofs very inefficient; similarly for @{text
- prod.case_eq_if}.
+ existing proofs very inefficient; similarly for \<open>prod.case_eq_if\<close>.
\<close>
ML \<open>
@@ -590,8 +589,8 @@
text \<open>
\medskip @{const case_prod} used as a logical connective or set former.
- \medskip These rules are for use with @{text blast}; could instead
- call @{text simp} using @{thm [source] prod.split} as rewrite.\<close>
+ \medskip These rules are for use with \<open>blast\<close>; could instead
+ call \<open>simp\<close> using @{thm [source] prod.split} as rewrite.\<close>
lemma case_prodI2:
"\<And>p. (\<And>a b. p = (a, b) \<Longrightarrow> c a b) \<Longrightarrow> case p of (a, b) \<Rightarrow> c a b"
@@ -631,10 +630,10 @@
"\<And>p. (\<And>a b. p = (a, b) \<Longrightarrow> z \<in> c a b) \<Longrightarrow> z \<in> (case p of (a, b) \<Rightarrow> c a b)"
by (simp only: split_tupled_all) simp
-declare mem_case_prodI [intro!] -- \<open>postponed to maintain traditional declaration order!\<close>
-declare case_prodI2' [intro!] -- \<open>postponed to maintain traditional declaration order!\<close>
-declare case_prodI2 [intro!] -- \<open>postponed to maintain traditional declaration order!\<close>
-declare case_prodI [intro!] -- \<open>postponed to maintain traditional declaration order!\<close>
+declare mem_case_prodI [intro!] \<comment> \<open>postponed to maintain traditional declaration order!\<close>
+declare case_prodI2' [intro!] \<comment> \<open>postponed to maintain traditional declaration order!\<close>
+declare case_prodI2 [intro!] \<comment> \<open>postponed to maintain traditional declaration order!\<close>
+declare case_prodI [intro!] \<comment> \<open>postponed to maintain traditional declaration order!\<close>
lemma mem_case_prodE [elim!]:
assumes "z \<in> case_prod c p"
@@ -666,7 +665,7 @@
by (rule ext) fast
lemma split_part [simp]: "(%(a,b). P & Q a b) = (%ab. P & case_prod Q ab)"
- -- \<open>Allows simplifications of nested splits in case of independent predicates.\<close>
+ \<comment> \<open>Allows simplifications of nested splits in case of independent predicates.\<close>
by (rule ext) blast
(* Do NOT make this a simp rule as it
@@ -1027,7 +1026,7 @@
"[| c: Sigma A B;
!!x y.[| x:A; y:B(x); c=(x,y) |] ==> P
|] ==> P"
- -- \<open>The general elimination rule.\<close>
+ \<comment> \<open>The general elimination rule.\<close>
by (unfold Sigma_def) blast
text \<open>
@@ -1105,7 +1104,7 @@
lemma UN_Times_distrib:
"(\<Union>(a, b)\<in>A \<times> B. E a \<times> F b) = UNION A E \<times> UNION B F"
- -- \<open>Suggested by Pierre Chartier\<close>
+ \<comment> \<open>Suggested by Pierre Chartier\<close>
by blast
lemma split_paired_Ball_Sigma [simp, no_atp]:
--- a/src/HOL/Quickcheck_Narrowing.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Quickcheck_Narrowing.thy Mon Dec 07 10:38:04 2015 +0100
@@ -155,9 +155,9 @@
where
"all f = (case narrowing (100 :: integer) of Narrowing_cons ty cs => Universal ty (\<lambda>t. f (conv cs t)) (partial_term_of (TYPE('a))))"
-subsubsection \<open>class @{text is_testable}\<close>
+subsubsection \<open>class \<open>is_testable\<close>\<close>
-text \<open>The class @{text is_testable} ensures that all necessary type instances are generated.\<close>
+text \<open>The class \<open>is_testable\<close> ensures that all necessary type instances are generated.\<close>
class is_testable
@@ -319,7 +319,7 @@
(Generated'_Code.Const \"Groups.uminus'_class.uminus\" (mkFunT t t))
(mkNumber (- i)); } in mkNumber)"
-subsection \<open>The @{text find_unused_assms} command\<close>
+subsection \<open>The \<open>find_unused_assms\<close> command\<close>
ML_file "Tools/Quickcheck/find_unused_assms.ML"
--- a/src/HOL/Quickcheck_Random.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Quickcheck_Random.thy Mon Dec 07 10:38:04 2015 +0100
@@ -18,7 +18,7 @@
code_printing
constant catch_match \<rightharpoonup> (Quickcheck) "((_) handle Match => _)"
-subsection \<open>The @{text random} class\<close>
+subsection \<open>The \<open>random\<close> class\<close>
class random = typerep +
fixes random :: "natural \<Rightarrow> Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
@@ -213,8 +213,8 @@
code_printing
constant random_fun_aux \<rightharpoonup> (Quickcheck) "Random'_Generators.random'_fun"
- -- \<open>With enough criminal energy this can be abused to derive @{prop False};
- for this reason we use a distinguished target @{text Quickcheck}
+ \<comment> \<open>With enough criminal energy this can be abused to derive @{prop False};
+ for this reason we use a distinguished target \<open>Quickcheck\<close>
not spoiling the regular trusted code generation\<close>
code_reserved Quickcheck Random_Generators
--- a/src/HOL/Quotient.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Quotient.thy Mon Dec 07 10:38:04 2015 +0100
@@ -64,7 +64,7 @@
by blast
lemma Quotient3_rel:
- "R r r \<and> R s s \<and> Abs r = Abs s \<longleftrightarrow> R r s" -- \<open>orientation does not loop on rewriting\<close>
+ "R r r \<and> R s s \<and> Abs r = Abs s \<longleftrightarrow> R r s" \<comment> \<open>orientation does not loop on rewriting\<close>
using a
unfolding Quotient3_def
by blast
@@ -196,7 +196,7 @@
In the following theorem R1 can be instantiated with anything,
but we know some of the types of the Rep and Abs functions;
so by solving Quotient assumptions we can get a unique R1 that
- will be provable; which is why we need to use @{text apply_rsp} and
+ will be provable; which is why we need to use \<open>apply_rsp\<close> and
not the primed version\<close>
lemma apply_rspQ3:
@@ -392,7 +392,7 @@
using a unfolding Quotient3_def Bex_def in_respects id_apply comp_def map_fun_def
by metis
-subsection \<open>@{text Bex1_rel} quantifier\<close>
+subsection \<open>\<open>Bex1_rel\<close> quantifier\<close>
definition
Bex1_rel :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
--- a/src/HOL/Random.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Random.thy Mon Dec 07 10:38:04 2015 +0100
@@ -136,7 +136,7 @@
qed
-subsection \<open>@{text ML} interface\<close>
+subsection \<open>\<open>ML\<close> interface\<close>
code_reflect Random_Engine
functions range select select_weight
--- a/src/HOL/Rat.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Rat.thy Mon Dec 07 10:38:04 2015 +0100
@@ -244,7 +244,7 @@
with Fract \<open>q = Fract a b\<close> \<open>b > 0\<close> \<open>coprime a b\<close> show C by blast
qed
-subsubsection \<open>Function @{text normalize}\<close>
+subsubsection \<open>Function \<open>normalize\<close>\<close>
lemma Fract_coprime: "Fract (a div gcd a b) (b div gcd a b) = Fract a b"
proof (cases "b = 0")
--- a/src/HOL/Real.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Real.thy Mon Dec 07 10:38:04 2015 +0100
@@ -1401,7 +1401,7 @@
done
-text\<open>Similar results are proved in @{text Fields}\<close>
+text\<open>Similar results are proved in \<open>Fields\<close>\<close>
lemma real_less_half_sum: "x < y ==> x < (x+y) / (2::real)"
by auto
@@ -1488,7 +1488,7 @@
moreover have "j * b < 1 + i"
proof -
have "real_of_int (j * b) < real_of_int i + 1"
- using `a < 1 + real_of_int i` `real_of_int j * real_of_int b \<le> a` by force
+ using \<open>a < 1 + real_of_int i\<close> \<open>real_of_int j * real_of_int b \<le> a\<close> by force
thus "j * b < 1 + i"
by linarith
qed
--- a/src/HOL/Real_Vector_Spaces.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy Mon Dec 07 10:38:04 2015 +0100
@@ -264,7 +264,7 @@
by metis
-subsection \<open>Embedding of the Reals into any @{text real_algebra_1}:
+subsection \<open>Embedding of the Reals into any \<open>real_algebra_1\<close>:
@{term of_real}\<close>
definition
@@ -927,7 +927,7 @@
"norm (of_real b - of_real a :: 'a::real_normed_algebra_1) \<le> \<bar>b - a\<bar>"
by (metis norm_of_real of_real_diff order_refl)
-text\<open>Despite a superficial resemblance, @{text norm_eq_1} is not relevant.\<close>
+text\<open>Despite a superficial resemblance, \<open>norm_eq_1\<close> is not relevant.\<close>
lemma square_norm_one:
fixes x :: "'a::real_normed_div_algebra"
assumes "x^2 = 1" shows "norm x = 1"
@@ -1222,17 +1222,17 @@
subsection \<open>Extra type constraints\<close>
-text \<open>Only allow @{term "open"} in class @{text topological_space}.\<close>
+text \<open>Only allow @{term "open"} in class \<open>topological_space\<close>.\<close>
setup \<open>Sign.add_const_constraint
(@{const_name "open"}, SOME @{typ "'a::topological_space set \<Rightarrow> bool"})\<close>
-text \<open>Only allow @{term dist} in class @{text metric_space}.\<close>
+text \<open>Only allow @{term dist} in class \<open>metric_space\<close>.\<close>
setup \<open>Sign.add_const_constraint
(@{const_name dist}, SOME @{typ "'a::metric_space \<Rightarrow> 'a \<Rightarrow> real"})\<close>
-text \<open>Only allow @{term norm} in class @{text real_normed_vector}.\<close>
+text \<open>Only allow @{term norm} in class \<open>real_normed_vector\<close>.\<close>
setup \<open>Sign.add_const_constraint
(@{const_name norm}, SOME @{typ "'a::real_normed_vector \<Rightarrow> real"})\<close>
@@ -1731,7 +1731,7 @@
show "\<forall>e>0. \<exists>M. \<forall>m\<ge>M. \<forall>n>m. dist (f m) (f n) < e"
proof (intro allI impI)
fix e :: real assume e: "e > 0"
- with `Cauchy f` obtain M where "\<And>m n. m \<ge> M \<Longrightarrow> n \<ge> M \<Longrightarrow> dist (f m) (f n) < e"
+ with \<open>Cauchy f\<close> obtain M where "\<And>m n. m \<ge> M \<Longrightarrow> n \<ge> M \<Longrightarrow> dist (f m) (f n) < e"
unfolding Cauchy_def by blast
thus "\<exists>M. \<forall>m\<ge>M. \<forall>n>m. dist (f m) (f n) < e" by (intro exI[of _ M]) force
qed
--- a/src/HOL/Record.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Record.thy Mon Dec 07 10:38:04 2015 +0100
@@ -18,14 +18,14 @@
text \<open>
Records are isomorphic to compound tuple types. To implement
efficient records, we make this isomorphism explicit. Consider the
- record access/update simplification @{text "alpha (beta_update f
- rec) = alpha rec"} for distinct fields alpha and beta of some record
- rec with n fields. There are @{text "n ^ 2"} such theorems, which
+ record access/update simplification \<open>alpha (beta_update f
+ rec) = alpha rec\<close> for distinct fields alpha and beta of some record
+ rec with n fields. There are \<open>n ^ 2\<close> such theorems, which
prohibits storage of all of them for large n. The rules can be
proved on the fly by case decomposition and simplification in O(n)
time. By creating O(n) isomorphic-tuple types while defining the
record, however, we can prove the access/update simplification in
- @{text "O(log(n)^2)"} time.
+ \<open>O(log(n)^2)\<close> time.
The O(n) cost of case decomposition is not because O(n) steps are
taken, but rather because the resulting rule must contain O(n) new
@@ -34,39 +34,36 @@
access/update theorems.
Record types are defined as isomorphic to tuple types. For instance,
- a record type with fields @{text "'a"}, @{text "'b"}, @{text "'c"}
- and @{text "'d"} might be introduced as isomorphic to @{text "'a \<times>
- ('b \<times> ('c \<times> 'd))"}. If we balance the tuple tree to @{text "('a \<times>
- 'b) \<times> ('c \<times> 'd)"} then accessors can be defined by converting to the
+ a record type with fields \<open>'a\<close>, \<open>'b\<close>, \<open>'c\<close>
+ and \<open>'d\<close> might be introduced as isomorphic to \<open>'a \<times>
+ ('b \<times> ('c \<times> 'd))\<close>. If we balance the tuple tree to \<open>('a \<times>
+ 'b) \<times> ('c \<times> 'd)\<close> then accessors can be defined by converting to the
underlying type then using O(log(n)) fst or snd operations.
- Updators can be defined similarly, if we introduce a @{text
- "fst_update"} and @{text "snd_update"} function. Furthermore, we can
+ Updators can be defined similarly, if we introduce a \<open>fst_update\<close> and \<open>snd_update\<close> function. Furthermore, we can
prove the access/update theorem in O(log(n)) steps by using simple
- rewrites on fst, snd, @{text "fst_update"} and @{text "snd_update"}.
+ rewrites on fst, snd, \<open>fst_update\<close> and \<open>snd_update\<close>.
The catch is that, although O(log(n)) steps were taken, the
underlying type we converted to is a tuple tree of size
O(n). Processing this term type wastes performance. We avoid this
for large n by taking each subtree of size K and defining a new type
isomorphic to that tuple subtree. A record can now be defined as
- isomorphic to a tuple tree of these O(n/K) new types, or, if @{text
- "n > K*K"}, we can repeat the process, until the record can be
+ isomorphic to a tuple tree of these O(n/K) new types, or, if \<open>n > K*K\<close>, we can repeat the process, until the record can be
defined in terms of a tuple tree of complexity less than the
constant K.
If we prove the access/update theorem on this type with the
- analogous steps to the tuple tree, we consume @{text "O(log(n)^2)"}
- time as the intermediate terms are @{text "O(log(n))"} in size and
+ analogous steps to the tuple tree, we consume \<open>O(log(n)^2)\<close>
+ time as the intermediate terms are \<open>O(log(n))\<close> in size and
the types needed have size bounded by K. To enable this analogous
- traversal, we define the functions seen below: @{text
- "iso_tuple_fst"}, @{text "iso_tuple_snd"}, @{text "iso_tuple_fst_update"}
- and @{text "iso_tuple_snd_update"}. These functions generalise tuple
+ traversal, we define the functions seen below: \<open>iso_tuple_fst\<close>, \<open>iso_tuple_snd\<close>, \<open>iso_tuple_fst_update\<close>
+ and \<open>iso_tuple_snd_update\<close>. These functions generalise tuple
operations by taking a parameter that encapsulates a tuple
isomorphism. The rewrites needed on these functions now need an
additional assumption which is that the isomorphism works.
These rewrites are typically used in a structured way. They are here
- presented as the introduction rule @{text "isomorphic_tuple.intros"}
+ presented as the introduction rule \<open>isomorphic_tuple.intros\<close>
rather than as a rewrite rule set. The introduction form is an
optimisation, as net matching can be performed at one term location
for each step rather than the simplifier searching the term for
--- a/src/HOL/Relation.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Relation.thy Mon Dec 07 10:38:04 2015 +0100
@@ -57,11 +57,11 @@
type_synonym 'a rel = "('a * 'a) set"
-lemma subrelI: -- \<open>Version of @{thm [source] subsetI} for binary relations\<close>
+lemma subrelI: \<comment> \<open>Version of @{thm [source] subsetI} for binary relations\<close>
"(\<And>x y. (x, y) \<in> r \<Longrightarrow> (x, y) \<in> s) \<Longrightarrow> r \<subseteq> s"
by auto
-lemma lfp_induct2: -- \<open>Version of @{thm [source] lfp_induct} for binary relations\<close>
+lemma lfp_induct2: \<comment> \<open>Version of @{thm [source] lfp_induct} for binary relations\<close>
"(a, b) \<in> lfp f \<Longrightarrow> mono f \<Longrightarrow>
(\<And>a b. (a, b) \<in> f (lfp f \<inter> {(x, y). P x y}) \<Longrightarrow> P a b) \<Longrightarrow> P a b"
using lfp_induct_set [of "(a, b)" f "case_prod P"] by auto
@@ -150,7 +150,7 @@
"refl_on A r \<longleftrightarrow> r \<subseteq> A \<times> A \<and> (\<forall>x\<in>A. (x, x) \<in> r)"
abbreviation refl :: "'a rel \<Rightarrow> bool"
-where -- \<open>reflexivity over a type\<close>
+where \<comment> \<open>reflexivity over a type\<close>
"refl \<equiv> refl_on UNIV"
definition reflp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
@@ -380,7 +380,7 @@
by (simp add: trans_def transp_def)
abbreviation transP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
-where -- \<open>FIXME drop\<close>
+where \<comment> \<open>FIXME drop\<close>
"transP r \<equiv> trans {(x, y). r x y}"
lemma transI:
@@ -494,7 +494,7 @@
by (simp add: refl_on_def)
lemma antisym_Id: "antisym Id"
- -- \<open>A strange result, since @{text Id} is also symmetric.\<close>
+ \<comment> \<open>A strange result, since \<open>Id\<close> is also symmetric.\<close>
by (simp add: antisym_def)
lemma sym_Id: "sym Id"
@@ -533,7 +533,7 @@
lemma Id_onE [elim!]:
"c : Id_on A ==> (!!x. x : A ==> c = (x, x) ==> P) ==> P"
- -- \<open>The general elimination rule.\<close>
+ \<comment> \<open>The general elimination rule.\<close>
by (unfold Id_on_def) (iprover elim!: UN_E singletonE)
lemma Id_on_iff: "((x, y) : Id_on A) = (x = y & x : A)"
@@ -715,7 +715,7 @@
by (fact converseD [to_pred])
lemma converseE [elim!]:
- -- \<open>More general than @{text converseD}, as it ``splits'' the member of the relation.\<close>
+ \<comment> \<open>More general than \<open>converseD\<close>, as it ``splits'' the member of the relation.\<close>
"yx \<in> r\<inverse> \<Longrightarrow> (\<And>x y. yx = (y, x) \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> P) \<Longrightarrow> P"
by (cases yx) (simp, erule converse.cases, iprover)
@@ -1008,7 +1008,7 @@
by (unfold Image_def) (iprover elim!: CollectE bexE)
lemma rev_ImageI: "a : A ==> (a, b) : r ==> b : r `` A"
- -- \<open>This version's more effective when we already have the required @{text a}\<close>
+ \<comment> \<open>This version's more effective when we already have the required \<open>a\<close>\<close>
by blast
lemma Image_empty [simp]: "R``{} = {}"
@@ -1037,7 +1037,7 @@
by (iprover intro!: subsetI elim!: ImageE dest!: subsetD SigmaD2)
lemma Image_eq_UN: "r``B = (\<Union>y\<in> B. r``{y})"
- -- \<open>NOT suitable for rewriting\<close>
+ \<comment> \<open>NOT suitable for rewriting\<close>
by blast
lemma Image_mono: "r' \<subseteq> r ==> A' \<subseteq> A ==> (r' `` A') \<subseteq> (r `` A)"
--- a/src/HOL/Rings.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Rings.thy Mon Dec 07 10:38:04 2015 +0100
@@ -18,7 +18,7 @@
assumes distrib_left[algebra_simps]: "a * (b + c) = a * b + a * c"
begin
-text\<open>For the @{text combine_numerals} simproc\<close>
+text\<open>For the \<open>combine_numerals\<close> simproc\<close>
lemma combine_common_factor:
"a * e + (b * e + c) = (a + b) * e + c"
by (simp add: distrib_right ac_simps)
@@ -890,7 +890,7 @@
by (erule is_unitE [of _ c]) (simp add: dvd_mult_unit_iff)
lemmas unit_dvd_iff = mult_unit_dvd_iff div_unit_dvd_iff
- dvd_mult_unit_iff dvd_div_unit_iff -- \<open>FIXME consider fact collection\<close>
+ dvd_mult_unit_iff dvd_div_unit_iff \<comment> \<open>FIXME consider fact collection\<close>
lemma unit_mult_div_div [simp]:
"is_unit a \<Longrightarrow> b * (1 div a) = b div a"
@@ -1298,7 +1298,7 @@
lemma mult_nonpos_nonneg: "a \<le> 0 \<Longrightarrow> 0 \<le> b \<Longrightarrow> a * b \<le> 0"
using mult_right_mono [of a 0 b] by simp
-text \<open>Legacy - use @{text mult_nonpos_nonneg}\<close>
+text \<open>Legacy - use \<open>mult_nonpos_nonneg\<close>\<close>
lemma mult_nonneg_nonpos2: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> b * a \<le> 0"
by (drule mult_right_mono [of b 0], auto)
@@ -1374,7 +1374,7 @@
lemma mult_neg_pos: "a < 0 \<Longrightarrow> 0 < b \<Longrightarrow> a * b < 0"
using mult_strict_right_mono [of a 0 b] by simp
-text \<open>Legacy - use @{text mult_neg_pos}\<close>
+text \<open>Legacy - use \<open>mult_neg_pos\<close>\<close>
lemma mult_pos_neg2: "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> b * a < 0"
by (drule mult_strict_right_mono [of b 0], auto)
@@ -1627,7 +1627,7 @@
done
text\<open>Cancellation laws for @{term "c*a < c*b"} and @{term "a*c < b*c"},
- also with the relations @{text "\<le>"} and equality.\<close>
+ also with the relations \<open>\<le>\<close> and equality.\<close>
text\<open>These ``disjunction'' versions produce two cases when the comparison is
an assumption, but effectively four when the comparison is a goal.\<close>
--- a/src/HOL/SMT.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/SMT.thy Mon Dec 07 10:38:04 2015 +0100
@@ -123,8 +123,8 @@
subsection \<open>Integer division and modulo for Z3\<close>
text \<open>
-The following Z3-inspired definitions are overspecified for the case where @{text "l = 0"}. This
-Schönheitsfehler is corrected in the @{text div_as_z3div} and @{text mod_as_z3mod} theorems.
+The following Z3-inspired definitions are overspecified for the case where \<open>l = 0\<close>. This
+Schönheitsfehler is corrected in the \<open>div_as_z3div\<close> and \<open>mod_as_z3mod\<close> theorems.
\<close>
definition z3div :: "int \<Rightarrow> int \<Rightarrow> int" where
@@ -182,15 +182,15 @@
text \<open>
The current configuration can be printed by the command
-@{text smt_status}, which shows the values of most options.
+\<open>smt_status\<close>, which shows the values of most options.
\<close>
subsection \<open>General configuration options\<close>
text \<open>
-The option @{text smt_solver} can be used to change the target SMT
-solver. The possible values can be obtained from the @{text smt_status}
+The option \<open>smt_solver\<close> can be used to change the target SMT
+solver. The possible values can be obtained from the \<open>smt_status\<close>
command.
\<close>
@@ -258,7 +258,7 @@
subsection \<open>Certificates\<close>
text \<open>
-By setting the option @{text smt_certificates} to the name of a file,
+By setting the option \<open>smt_certificates\<close> to the name of a file,
all following applications of an SMT solver a cached in that file.
Any further application of the same SMT solver (using the very same
configuration) re-uses the cached certificate instead of invoking the
@@ -266,7 +266,7 @@
The filename should be given as an explicit path. It is good
practice to use the name of the current theory (with ending
-@{text ".certs"} instead of @{text ".thy"}) as the certificates file.
+\<open>.certs\<close> instead of \<open>.thy\<close>) as the certificates file.
Certificate files should be used at most once in a certain theory context,
to avoid race conditions with other concurrent accesses.
\<close>
@@ -274,11 +274,11 @@
declare [[smt_certificates = ""]]
text \<open>
-The option @{text smt_read_only_certificates} controls whether only
+The option \<open>smt_read_only_certificates\<close> controls whether only
stored certificates are should be used or invocation of an SMT solver
-is allowed. When set to @{text true}, no SMT solver will ever be
+is allowed. When set to \<open>true\<close>, no SMT solver will ever be
invoked and only the existing certificates found in the configured
-cache are used; when set to @{text false} and there is no cached
+cache are used; when set to \<open>false\<close> and there is no cached
certificate for some proposition, then the configured SMT solver is
invoked.
\<close>
@@ -290,7 +290,7 @@
text \<open>
The SMT method, when applied, traces important information. To
-make it entirely silent, set the following option to @{text false}.
+make it entirely silent, set the following option to \<open>false\<close>.
\<close>
declare [[smt_verbose = true]]
@@ -298,7 +298,7 @@
text \<open>
For tracing the generated problem file given to the SMT solver as
well as the returned result of the solver, the option
-@{text smt_trace} should be set to @{text true}.
+\<open>smt_trace\<close> should be set to \<open>true\<close>.
\<close>
declare [[smt_trace = false]]
@@ -309,9 +309,9 @@
text \<open>
Several prof rules of Z3 are not very well documented. There are two
lemma groups which can turn failing Z3 proof reconstruction attempts
-into succeeding ones: the facts in @{text z3_rule} are tried prior to
+into succeeding ones: the facts in \<open>z3_rule\<close> are tried prior to
any implemented reconstruction procedure for all uncertain Z3 proof
-rules; the facts in @{text z3_simp} are only fed to invocations of
+rules; the facts in \<open>z3_simp\<close> are only fed to invocations of
the simplifier when reconstructing theory-specific proof steps.
\<close>
--- a/src/HOL/Series.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Series.thy Mon Dec 07 10:38:04 2015 +0100
@@ -384,7 +384,7 @@
lemma summable_minus_iff:
fixes f :: "nat \<Rightarrow> 'a::real_normed_vector"
shows "summable (\<lambda>n. - f n) \<longleftrightarrow> summable f"
- by (auto dest: summable_minus) --\<open>used two ways, hence must be outside the context above\<close>
+ by (auto dest: summable_minus) \<comment>\<open>used two ways, hence must be outside the context above\<close>
context
--- a/src/HOL/Set.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Set.thy Mon Dec 07 10:38:04 2015 +0100
@@ -10,8 +10,8 @@
typedecl 'a set
-axiomatization Collect :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set" -- "comprehension"
- and member :: "'a \<Rightarrow> 'a set \<Rightarrow> bool" -- "membership"
+axiomatization Collect :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set" \<comment> "comprehension"
+ and member :: "'a \<Rightarrow> 'a set \<Rightarrow> bool" \<comment> "membership"
where
mem_Collect_eq [iff, code_unfold]: "member a (Collect P) = P a"
and Collect_mem_eq [simp]: "Collect (\<lambda>x. member x A) = A"
@@ -21,7 +21,7 @@
member ("(_/ : _)" [51, 51] 50)
abbreviation not_member where
- "not_member x A \<equiv> ~ (x : A)" -- "non-membership"
+ "not_member x A \<equiv> ~ (x : A)" \<comment> "non-membership"
notation
not_member ("op ~:") and
@@ -58,8 +58,8 @@
by simp
text \<open>
-Simproc for pulling @{text "x=t"} in @{text "{x. \<dots> & x=t & \<dots>}"}
-to the front (and similarly for @{text "t=x"}):
+Simproc for pulling \<open>x=t\<close> in \<open>{x. \<dots> & x=t & \<dots>}\<close>
+to the front (and similarly for \<open>t=x\<close>):
\<close>
simproc_setup defined_Collect ("{x. P x & Q x}") = \<open>
@@ -176,10 +176,10 @@
supset_eq ("(_/ \<supseteq> _)" [51, 51] 50)
definition Ball :: "'a set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" where
- "Ball A P \<longleftrightarrow> (\<forall>x. x \<in> A \<longrightarrow> P x)" -- "bounded universal quantifiers"
+ "Ball A P \<longleftrightarrow> (\<forall>x. x \<in> A \<longrightarrow> P x)" \<comment> "bounded universal quantifiers"
definition Bex :: "'a set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" where
- "Bex A P \<longleftrightarrow> (\<exists>x. x \<in> A \<and> P x)" -- "bounded existential quantifiers"
+ "Bex A P \<longleftrightarrow> (\<exists>x. x \<in> A \<and> P x)" \<comment> "bounded existential quantifiers"
syntax
"_Ball" :: "pttrn => 'a set => bool => bool" ("(3ALL _:_./ _)" [0, 0, 10] 10)
@@ -267,9 +267,8 @@
text \<open>
- \medskip Translate between @{text "{e | x1...xn. P}"} and @{text
- "{u. EX x1..xn. u = e & P}"}; @{text "{y. EX x1..xn. y = e & P}"} is
- only translated if @{text "[0..n] subset bvs(e)"}.
+ \medskip Translate between \<open>{e | x1...xn. P}\<close> and \<open>{u. EX x1..xn. u = e & P}\<close>; \<open>{y. EX x1..xn. y = e & P}\<close> is
+ only translated if \<open>[0..n] subset bvs(e)\<close>.
\<close>
syntax
@@ -295,7 +294,7 @@
print_translation \<open>
[Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax Ball} @{syntax_const "_Ball"},
Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax Bex} @{syntax_const "_Bex"}]
-\<close> -- \<open>to avoid eta-contraction of body\<close>
+\<close> \<comment> \<open>to avoid eta-contraction of body\<close>
print_translation \<open>
let
@@ -383,12 +382,12 @@
by (unfold Ball_def) blast
lemma bexI [intro]: "P x ==> x:A ==> EX x:A. P x"
- -- \<open>Normally the best argument order: @{prop "P x"} constrains the
+ \<comment> \<open>Normally the best argument order: @{prop "P x"} constrains the
choice of @{prop "x:A"}.\<close>
by (unfold Bex_def) blast
lemma rev_bexI [intro?]: "x:A ==> P x ==> EX x:A. P x"
- -- \<open>The best argument order when there is only one @{prop "x:A"}.\<close>
+ \<comment> \<open>The best argument order when there is only one @{prop "x:A"}.\<close>
by (unfold Bex_def) blast
lemma bexCI: "(ALL x:A. ~P x ==> P a) ==> a:A ==> EX x:A. P x"
@@ -398,11 +397,11 @@
by (unfold Bex_def) blast
lemma ball_triv [simp]: "(ALL x:A. P) = ((EX x. x:A) --> P)"
- -- \<open>Trival rewrite rule.\<close>
+ \<comment> \<open>Trival rewrite rule.\<close>
by (simp add: Ball_def)
lemma bex_triv [simp]: "(EX x:A. P) = ((EX x. x:A) & P)"
- -- \<open>Dual form for existentials.\<close>
+ \<comment> \<open>Dual form for existentials.\<close>
by (simp add: Bex_def)
lemma bex_triv_one_point1 [simp]: "(EX x:A. x = a) = (a:A)"
@@ -465,18 +464,18 @@
by (simp add: less_eq_set_def le_fun_def)
text \<open>
- \medskip Map the type @{text "'a set => anything"} to just @{typ
+ \medskip Map the type \<open>'a set => anything\<close> to just @{typ
'a}; for overloading constants whose first argument has type @{typ
"'a set"}.
\<close>
lemma subsetD [elim, intro?]: "A \<subseteq> B ==> c \<in> A ==> c \<in> B"
by (simp add: less_eq_set_def le_fun_def)
- -- \<open>Rule in Modus Ponens style.\<close>
+ \<comment> \<open>Rule in Modus Ponens style.\<close>
lemma rev_subsetD [intro?]: "c \<in> A ==> A \<subseteq> B ==> c \<in> B"
- -- \<open>The same, with reversed premises for use with @{text erule} --
- cf @{text rev_mp}.\<close>
+ \<comment> \<open>The same, with reversed premises for use with \<open>erule\<close> --
+ cf \<open>rev_mp\<close>.\<close>
by (rule subsetD)
text \<open>
@@ -484,7 +483,7 @@
\<close>
lemma subsetCE [elim]: "A \<subseteq> B ==> (c \<notin> A ==> P) ==> (c \<in> B ==> P) ==> P"
- -- \<open>Classical elimination rule.\<close>
+ \<comment> \<open>Classical elimination rule.\<close>
by (auto simp add: less_eq_set_def le_fun_def)
lemma subset_eq: "A \<le> B = (\<forall>x\<in>A. x \<in> B)" by blast
@@ -518,7 +517,7 @@
subsubsection \<open>Equality\<close>
lemma subset_antisym [intro!]: "A \<subseteq> B ==> B \<subseteq> A ==> A = B"
- -- \<open>Anti-symmetry of the subset relation.\<close>
+ \<comment> \<open>Anti-symmetry of the subset relation.\<close>
by (iprover intro: set_eqI subsetD)
text \<open>
@@ -533,8 +532,7 @@
by simp
text \<open>
- \medskip Be careful when adding this to the claset as @{text
- subset_empty} is in the simpset: @{prop "A = {}"} goes to @{prop "{}
+ \medskip Be careful when adding this to the claset as \<open>subset_empty\<close> is in the simpset: @{prop "A = {}"} goes to @{prop "{}
\<subseteq> A"} and @{prop "A \<subseteq> {}"} and then back to @{prop "A = {}"}!
\<close>
@@ -565,14 +563,14 @@
by simp
lemma empty_subsetI [iff]: "{} \<subseteq> A"
- -- \<open>One effect is to delete the ASSUMPTION @{prop "{} <= A"}\<close>
+ \<comment> \<open>One effect is to delete the ASSUMPTION @{prop "{} <= A"}\<close>
by blast
lemma equals0I: "(!!y. y \<in> A ==> False) ==> A = {}"
by blast
lemma equals0D: "A = {} ==> a \<notin> A"
- -- \<open>Use for reasoning about disjointness: @{text "A Int B = {}"}\<close>
+ \<comment> \<open>Use for reasoning about disjointness: \<open>A Int B = {}\<close>\<close>
by blast
lemma ball_empty [simp]: "Ball {} P = True"
@@ -594,7 +592,7 @@
lemma UNIV_I [simp]: "x : UNIV"
by (simp add: UNIV_def)
-declare UNIV_I [intro] -- \<open>unsafe makes it less likely to cause problems\<close>
+declare UNIV_I [intro] \<comment> \<open>unsafe makes it less likely to cause problems\<close>
lemma UNIV_witness [intro?]: "EX x. x : UNIV"
by simp
@@ -603,7 +601,7 @@
by (fact top_greatest) (* already simp *)
text \<open>
- \medskip Eta-contracting these two rules (to remove @{text P})
+ \medskip Eta-contracting these two rules (to remove \<open>P\<close>)
causes them to be ignored because of their interaction with
congruence rules.
\<close>
@@ -777,7 +775,7 @@
by (unfold insert_def) blast
lemma insertCI [intro!]: "(a~:B ==> a = b) ==> a: insert b B"
- -- \<open>Classical introduction rule.\<close>
+ \<comment> \<open>Classical introduction rule.\<close>
by auto
lemma subset_insert_iff: "(A \<subseteq> insert x B) = (if x:A then A - {x} \<subseteq> B else A \<subseteq> B)"
@@ -821,7 +819,7 @@
subsubsection \<open>Singletons, using insert\<close>
lemma singletonI [intro!]: "a : {a}"
- -- \<open>Redundant? But unlike @{text insertCI}, it proves the subgoal immediately!\<close>
+ \<comment> \<open>Redundant? But unlike \<open>insertCI\<close>, it proves the subgoal immediately!\<close>
by (rule insertI1)
lemma singletonD [dest!]: "b : {a} ==> b = a"
@@ -887,12 +885,12 @@
lemma rev_image_eqI:
"x \<in> A \<Longrightarrow> b = f x \<Longrightarrow> b \<in> f ` A"
- -- \<open>This version's more effective when we already have the
+ \<comment> \<open>This version's more effective when we already have the
required @{term x}.\<close>
by (rule image_eqI)
lemma imageE [elim!]:
- assumes "b \<in> (\<lambda>x. f x) ` A" -- \<open>The eta-expansion gives variable-name preservation.\<close>
+ assumes "b \<in> (\<lambda>x. f x) ` A" \<comment> \<open>The eta-expansion gives variable-name preservation.\<close>
obtains x where "b = f x" and "x \<in> A"
using assms by (unfold image_def) blast
@@ -910,13 +908,13 @@
lemma image_subsetI:
"(\<And>x. x \<in> A \<Longrightarrow> f x \<in> B) \<Longrightarrow> f ` A \<subseteq> B"
- -- \<open>Replaces the three steps @{text subsetI}, @{text imageE},
- @{text hypsubst}, but breaks too many existing proofs.\<close>
+ \<comment> \<open>Replaces the three steps \<open>subsetI\<close>, \<open>imageE\<close>,
+ \<open>hypsubst\<close>, but breaks too many existing proofs.\<close>
by blast
lemma image_subset_iff:
"f ` A \<subseteq> B \<longleftrightarrow> (\<forall>x\<in>A. f x \<in> B)"
- -- \<open>This rewrite rule would confuse users if made default.\<close>
+ \<comment> \<open>This rewrite rule would confuse users if made default.\<close>
by blast
lemma subset_imageE:
@@ -970,7 +968,7 @@
lemma image_Collect:
"f ` {x. P x} = {f x | x. P x}"
- -- \<open>NOT suitable as a default simprule: the RHS isn't simpler than the LHS,
+ \<comment> \<open>NOT suitable as a default simprule: the RHS isn't simpler than the LHS,
with its implicit quantifier and conjunction. Also image enjoys better
equational properties than does the RHS.\<close>
by blast
@@ -1011,7 +1009,7 @@
\<close>
abbreviation range :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b set"
-where -- "of function"
+where \<comment> "of function"
"range f \<equiv> f ` UNIV"
lemma range_eqI:
@@ -1035,9 +1033,9 @@
by auto
-subsubsection \<open>Some rules with @{text "if"}\<close>
-
-text\<open>Elimination of @{text"{x. \<dots> & x=t & \<dots>}"}.\<close>
+subsubsection \<open>Some rules with \<open>if\<close>\<close>
+
+text\<open>Elimination of \<open>{x. \<dots> & x=t & \<dots>}\<close>.\<close>
lemma Collect_conv_if: "{x. x=a & P x} = (if P a then {a} else {})"
by auto
@@ -1046,8 +1044,7 @@
by auto
text \<open>
- Rewrite rules for boolean case-splitting: faster than @{text
- "split_if [split]"}.
+ Rewrite rules for boolean case-splitting: faster than \<open>split_if [split]\<close>.
\<close>
lemma split_if_eq1: "((if Q then x else y) = b) = ((Q --> x = b) & (~ Q --> y = b))"
@@ -1057,8 +1054,7 @@
by (rule split_if)
text \<open>
- Split ifs on either side of the membership relation. Not for @{text
- "[simp]"} -- can cause goals to blow up!
+ Split ifs on either side of the membership relation. Not for \<open>[simp]\<close> -- can cause goals to blow up!
\<close>
lemma split_if_mem1: "((if Q then x else y) : b) = ((Q --> x : b) & (~ Q --> y : b))"
@@ -1139,7 +1135,7 @@
subsubsection \<open>Derived rules involving subsets.\<close>
-text \<open>@{text insert}.\<close>
+text \<open>\<open>insert\<close>.\<close>
lemma subset_insertI: "B \<subseteq> insert a B"
by (rule subsetI) (erule insertI2)
@@ -1186,10 +1182,10 @@
subsubsection \<open>Equalities involving union, intersection, inclusion, etc.\<close>
-text \<open>@{text "{}"}.\<close>
+text \<open>\<open>{}\<close>.\<close>
lemma Collect_const [simp]: "{s. P} = (if P then UNIV else {})"
- -- \<open>supersedes @{text "Collect_False_empty"}\<close>
+ \<comment> \<open>supersedes \<open>Collect_False_empty\<close>\<close>
by auto
lemma subset_empty [simp]: "(A \<subseteq> {}) = (A = {})"
@@ -1220,10 +1216,10 @@
by blast
-text \<open>\medskip @{text insert}.\<close>
+text \<open>\medskip \<open>insert\<close>.\<close>
lemma insert_is_Un: "insert a A = {a} Un A"
- -- \<open>NOT SUITABLE FOR REWRITING since @{text "{a} == insert a {}"}\<close>
+ \<comment> \<open>NOT SUITABLE FOR REWRITING since \<open>{a} == insert a {}\<close>\<close>
by blast
lemma insert_not_empty [simp]: "insert a A \<noteq> {}"
@@ -1233,8 +1229,8 @@
declare empty_not_insert [simp]
lemma insert_absorb: "a \<in> A ==> insert a A = A"
- -- \<open>@{text "[simp]"} causes recursive calls when there are nested inserts\<close>
- -- \<open>with \emph{quadratic} running time\<close>
+ \<comment> \<open>\<open>[simp]\<close> causes recursive calls when there are nested inserts\<close>
+ \<comment> \<open>with \emph{quadratic} running time\<close>
by blast
lemma insert_absorb2 [simp]: "insert x (insert x A) = insert x A"
@@ -1247,7 +1243,7 @@
by blast
lemma mk_disjoint_insert: "a \<in> A ==> \<exists>B. A = insert a B & a \<notin> B"
- -- \<open>use new @{text B} rather than @{text "A - {a}"} to avoid infinite unfolding\<close>
+ \<comment> \<open>use new \<open>B\<close> rather than \<open>A - {a}\<close> to avoid infinite unfolding\<close>
apply (rule_tac x = "A - {a}" in exI, blast)
done
@@ -1268,7 +1264,7 @@
by auto
-text \<open>\medskip @{text Int}\<close>
+text \<open>\medskip \<open>Int\<close>\<close>
lemma Int_absorb: "A \<inter> A = A"
by (fact inf_idem) (* already simp *)
@@ -1286,7 +1282,7 @@
by (fact inf_assoc)
lemmas Int_ac = Int_assoc Int_left_absorb Int_commute Int_left_commute
- -- \<open>Intersection is an AC-operator\<close>
+ \<comment> \<open>Intersection is an AC-operator\<close>
lemma Int_absorb1: "B \<subseteq> A ==> A \<inter> B = B"
by (fact inf_absorb2)
@@ -1328,7 +1324,7 @@
by blast
-text \<open>\medskip @{text Un}.\<close>
+text \<open>\medskip \<open>Un\<close>.\<close>
lemma Un_absorb: "A \<union> A = A"
by (fact sup_idem) (* already simp *)
@@ -1346,7 +1342,7 @@
by (fact sup_assoc)
lemmas Un_ac = Un_assoc Un_left_absorb Un_commute Un_left_commute
- -- \<open>Union is an AC-operator\<close>
+ \<comment> \<open>Union is an AC-operator\<close>
lemma Un_absorb1: "A \<subseteq> B ==> A \<union> B = B"
by (fact sup_absorb2)
@@ -1449,7 +1445,7 @@
by blast
lemma Un_Int_assoc_eq: "((A \<inter> B) \<union> C = A \<inter> (B \<union> C)) = (C \<subseteq> A)"
- -- \<open>Halmos, Naive Set Theory, page 16.\<close>
+ \<comment> \<open>Halmos, Naive Set Theory, page 16.\<close>
by blast
lemma Compl_UNIV_eq: "-UNIV = {}"
@@ -1470,7 +1466,7 @@
text \<open>\medskip Bounded quantifiers.
The following are not added to the default simpset because
- (a) they duplicate the body and (b) there are no similar rules for @{text Int}.\<close>
+ (a) they duplicate the body and (b) there are no similar rules for \<open>Int\<close>.\<close>
lemma ball_Un: "(\<forall>x \<in> A \<union> B. P x) = ((\<forall>x\<in>A. P x) & (\<forall>x\<in>B. P x))"
by blast
@@ -1509,11 +1505,11 @@
by blast
lemma Diff_insert: "A - insert a B = A - B - {a}"
- -- \<open>NOT SUITABLE FOR REWRITING since @{text "{a} == insert a 0"}\<close>
+ \<comment> \<open>NOT SUITABLE FOR REWRITING since \<open>{a} == insert a 0\<close>\<close>
by blast
lemma Diff_insert2: "A - insert a B = A - {a} - B"
- -- \<open>NOT SUITABLE FOR REWRITING since @{text "{a} == insert a 0"}\<close>
+ \<comment> \<open>NOT SUITABLE FOR REWRITING since \<open>{a} == insert a 0\<close>\<close>
by blast
lemma insert_Diff_if: "insert x A - B = (if x \<in> B then A - B else insert x (A - B))"
@@ -1591,7 +1587,7 @@
lemma UNIV_bool: "UNIV = {False, True}"
by (auto intro: bool_induct)
-text \<open>\medskip @{text Pow}\<close>
+text \<open>\medskip \<open>Pow\<close>\<close>
lemma Pow_empty [simp]: "Pow {} = {{}}"
by (auto simp add: Pow_def)
@@ -1764,7 +1760,7 @@
by blast
lemma vimage_insert: "f-`(insert a B) = (f-`{a}) Un (f-`B)"
- -- \<open>NOT suitable for rewriting because of the recurrence of @{term "{a}"}.\<close>
+ \<comment> \<open>NOT suitable for rewriting because of the recurrence of @{term "{a}"}.\<close>
by blast
lemma vimage_Diff: "f -` (A - B) = (f -` A) - (f -` B)"
@@ -1774,7 +1770,7 @@
by blast
lemma vimage_mono: "A \<subseteq> B ==> f -` A \<subseteq> f -` B"
- -- \<open>monotonicity\<close>
+ \<comment> \<open>monotonicity\<close>
by blast
lemma vimage_image_eq: "f -` (f ` A) = {y. EX x:A. f x = f y}"
@@ -1831,7 +1827,7 @@
lemma Least_mono:
"mono (f::'a::order => 'b::order) ==> EX x:S. ALL y:S. x <= y
==> (LEAST y. y : f ` S) = f (LEAST x. x : S)"
- -- \<open>Courtesy of Stephan Merz\<close>
+ \<comment> \<open>Courtesy of Stephan Merz\<close>
apply clarify
apply (erule_tac P = "%x. x : S" in LeastI2_order, fast)
apply (rule LeastI2_order)
--- a/src/HOL/Set_Interval.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Set_Interval.thy Mon Dec 07 10:38:04 2015 +0100
@@ -798,15 +798,15 @@
subsubsection \<open>Intervals and numerals\<close>
-lemma lessThan_nat_numeral: --\<open>Evaluation for specific numerals\<close>
+lemma lessThan_nat_numeral: \<comment>\<open>Evaluation for specific numerals\<close>
"lessThan (numeral k :: nat) = insert (pred_numeral k) (lessThan (pred_numeral k))"
by (simp add: numeral_eq_Suc lessThan_Suc)
-lemma atMost_nat_numeral: --\<open>Evaluation for specific numerals\<close>
+lemma atMost_nat_numeral: \<comment>\<open>Evaluation for specific numerals\<close>
"atMost (numeral k :: nat) = insert (numeral k) (atMost (pred_numeral k))"
by (simp add: numeral_eq_Suc atMost_Suc)
-lemma atLeastLessThan_nat_numeral: --\<open>Evaluation for specific numerals\<close>
+lemma atLeastLessThan_nat_numeral: \<comment>\<open>Evaluation for specific numerals\<close>
"atLeastLessThan m (numeral k :: nat) =
(if m \<le> (pred_numeral k) then insert (pred_numeral k) (atLeastLessThan m (pred_numeral k))
else {})"
@@ -1468,12 +1468,12 @@
the middle column shows the new (default) syntax, and the right column
shows a special syntax. The latter is only meaningful for latex output
and has to be activated explicitly by setting the print mode to
-@{text latex_sum} (e.g.\ via @{text "mode = latex_sum"} in
+\<open>latex_sum\<close> (e.g.\ via \<open>mode = latex_sum\<close> in
antiquotations). It is not the default \LaTeX\ output because it only
works well with italic-style formulae, not tt-style.
Note that for uniformity on @{typ nat} it is better to use
-@{term"\<Sum>x::nat=0..<n. e"} rather than @{text"\<Sum>x<n. e"}: @{text setsum} may
+@{term"\<Sum>x::nat=0..<n. e"} rather than \<open>\<Sum>x<n. e\<close>: \<open>setsum\<close> may
not provide all lemmas available for @{term"{m..<n}"} also in the
special form for @{term"{..<n}"}.\<close>
@@ -1697,7 +1697,7 @@
finally show ?case .
qed simp
-corollary power_diff_sumr2: --\<open>@{text COMPLEX_POLYFUN} in HOL Light\<close>
+corollary power_diff_sumr2: \<comment>\<open>\<open>COMPLEX_POLYFUN\<close> in HOL Light\<close>
fixes x :: "'a::{comm_ring,monoid_mult}"
shows "x^n - y^n = (x - y) * (\<Sum>i<n. y^(n - Suc i) * x^i)"
using diff_power_eq_setsum[of x "n - 1" y]
--- a/src/HOL/String.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/String.thy Mon Dec 07 10:38:04 2015 +0100
@@ -115,7 +115,7 @@
by (simp add: nibble_of_nat_def)
datatype char = Char nibble nibble
- -- "Note: canonical order of character encoding coincides with standard term ordering"
+ \<comment> "Note: canonical order of character encoding coincides with standard term ordering"
syntax
"_Char" :: "str_position => char" ("CHR _")
@@ -281,7 +281,7 @@
with Char show ?thesis by (simp add: nat_of_char_def add.commute)
qed
-code_datatype Char -- \<open>drop case certificate for char\<close>
+code_datatype Char \<comment> \<open>drop case certificate for char\<close>
lemma case_char_code [code]:
"case_char f c = (let n = nat_of_char c in f (nibble_of_nat (n div 16)) (nibble_of_nat n))"
--- a/src/HOL/Sum_Type.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Sum_Type.thy Mon Dec 07 10:38:04 2015 +0100
@@ -90,7 +90,7 @@
| Inr projr
by (erule sumE, assumption) (auto dest: Inl_inject Inr_inject simp add: Inl_not_Inr)
-text \<open>Avoid name clashes by prefixing the output of @{text old_rep_datatype} with @{text old}.\<close>
+text \<open>Avoid name clashes by prefixing the output of \<open>old_rep_datatype\<close> with \<open>old\<close>.\<close>
setup \<open>Sign.mandatory_path "old"\<close>
@@ -104,7 +104,7 @@
setup \<open>Sign.parent_path\<close>
-text \<open>But erase the prefix for properties that are not generated by @{text free_constructors}.\<close>
+text \<open>But erase the prefix for properties that are not generated by \<open>free_constructors\<close>.\<close>
setup \<open>Sign.mandatory_path "sum"\<close>
@@ -206,7 +206,7 @@
definition Plus :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a + 'b) set" (infixr "<+>" 65) where
"A <+> B = Inl ` A \<union> Inr ` B"
-hide_const (open) Plus --"Valuable identifier"
+hide_const (open) Plus \<comment>"Valuable identifier"
lemma InlI [intro!]: "a \<in> A \<Longrightarrow> Inl a \<in> A <+> B"
by (simp add: Plus_def)
--- a/src/HOL/Taylor.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Taylor.thy Mon Dec 07 10:38:04 2015 +0100
@@ -9,7 +9,7 @@
begin
text \<open>
-We use MacLaurin and the translation of the expansion point @{text c} to @{text 0}
+We use MacLaurin and the translation of the expansion point \<open>c\<close> to \<open>0\<close>
to prove Taylor's theorem.
\<close>
--- a/src/HOL/Topological_Spaces.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Topological_Spaces.thy Mon Dec 07 10:38:04 2015 +0100
@@ -644,7 +644,7 @@
assume "d \<noteq> c"
from t1_space[OF this] obtain U where "open U" "d \<in> U" "c \<notin> U" by blast
from this assms have "eventually (\<lambda>x. f x \<in> U) F" unfolding tendsto_def by blast
- hence "eventually (\<lambda>x. f x \<noteq> c) F" by eventually_elim (insert `c \<notin> U`, blast)
+ hence "eventually (\<lambda>x. f x \<noteq> c) F" by eventually_elim (insert \<open>c \<notin> U\<close>, blast)
with assms(2) show False unfolding frequently_def by contradiction
qed
@@ -795,7 +795,7 @@
definition
monoseq :: "(nat \<Rightarrow> 'a::order) \<Rightarrow> bool" where
- --\<open>Definition of monotonicity.
+ \<comment>\<open>Definition of monotonicity.
The use of disjunction here complicates proofs considerably.
One alternative is to add a Boolean argument to indicate the direction.
Another is to develop the notions of increasing and decreasing first.\<close>
@@ -815,7 +815,7 @@
definition
subseq :: "(nat \<Rightarrow> nat) \<Rightarrow> bool" where
- --\<open>Definition of subsequence\<close>
+ \<comment>\<open>Definition of subsequence\<close>
"subseq f \<longleftrightarrow> (\<forall>m. \<forall>n>m. f m < f n)"
lemma incseq_SucI:
@@ -1641,7 +1641,7 @@
begin
definition compact :: "'a set \<Rightarrow> bool" where
- compact_eq_heine_borel: -- "This name is used for backwards compatibility"
+ compact_eq_heine_borel: \<comment> "This name is used for backwards compatibility"
"compact S \<longleftrightarrow> (\<forall>C. (\<forall>c\<in>C. open c) \<and> S \<subseteq> \<Union>C \<longrightarrow> (\<exists>D\<subseteq>C. finite D \<and> S \<subseteq> \<Union>D))"
lemma compactI:
--- a/src/HOL/Transcendental.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Transcendental.thy Mon Dec 07 10:38:04 2015 +0100
@@ -41,7 +41,7 @@
lemma root_test_convergence:
fixes f :: "nat \<Rightarrow> 'a::banach"
- assumes f: "(\<lambda>n. root n (norm (f n))) ----> x" -- "could be weakened to lim sup"
+ assumes f: "(\<lambda>n. root n (norm (f n))) ----> x" \<comment> "could be weakened to lim sup"
assumes "x < 1"
shows "summable f"
proof -
@@ -1459,7 +1459,7 @@
assumes ln_one [simp]: "ln 1 = 0"
definition powr :: "['a,'a] => 'a::ln" (infixr "powr" 80)
- -- \<open>exponentation via ln and exp\<close>
+ \<comment> \<open>exponentation via ln and exp\<close>
where [code del]: "x powr a \<equiv> if x = 0 then 0 else exp(a * ln x)"
lemma powr_0 [simp]: "0 powr z = 0"
@@ -2084,7 +2084,7 @@
definition log :: "[real,real] => real"
- -- \<open>logarithm of @{term x} to base @{term a}\<close>
+ \<comment> \<open>logarithm of @{term x} to base @{term a}\<close>
where "log a x = ln x / ln a"
@@ -3519,7 +3519,7 @@
using sin_ge_zero [of "x-pi"]
by (simp add: sin_diff)
-text \<open>FIXME: This proof is almost identical to lemma @{text cos_is_zero}.
+text \<open>FIXME: This proof is almost identical to lemma \<open>cos_is_zero\<close>.
It should be possible to factor out some of the common parts.\<close>
lemma cos_total: "\<lbrakk>-1 \<le> y; y \<le> 1\<rbrakk> \<Longrightarrow> EX! x. 0 \<le> x & x \<le> pi & (cos x = y)"
@@ -3855,7 +3855,7 @@
qed
lemma cos_one_2pi_int: "cos(x) = 1 \<longleftrightarrow> (\<exists>n::int. x = n * 2*pi)"
- apply auto --\<open>FIXME simproc bug\<close>
+ apply auto \<comment>\<open>FIXME simproc bug\<close>
apply (auto simp: cos_one_2pi)
apply (metis of_int_of_nat_eq)
apply (metis mult_minus_right of_int_minus of_int_of_nat_eq)
@@ -5573,7 +5573,7 @@
then have wnz: "\<And>w. w \<noteq> 0 \<Longrightarrow> (\<Sum>i\<le>n. c (Suc i) * w^i) = 0"
using Suc by auto
then have "(\<lambda>h. \<Sum>i\<le>n. c (Suc i) * h^i) -- 0 --> 0"
- by (simp cong: LIM_cong) --\<open>the case @{term"w=0"} by continuity\<close>
+ by (simp cong: LIM_cong) \<comment>\<open>the case @{term"w=0"} by continuity\<close>
then have "(\<Sum>i\<le>n. c (Suc i) * 0^i) = 0"
using isCont_polynom [of 0 "\<lambda>i. c (Suc i)" n] LIM_unique
by (force simp add: Limits.isCont_iff)
--- a/src/HOL/Transitive_Closure.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Transitive_Closure.thy Mon Dec 07 10:38:04 2015 +0100
@@ -12,9 +12,9 @@
ML_file "~~/src/Provers/trancl.ML"
text \<open>
- @{text rtrancl} is reflexive/transitive closure,
- @{text trancl} is transitive closure,
- @{text reflcl} is reflexive closure.
+ \<open>rtrancl\<close> is reflexive/transitive closure,
+ \<open>trancl\<close> is transitive closure,
+ \<open>reflcl\<close> is reflexive closure.
These postfix operators have \emph{maximum priority}, forcing their
operands to be atomic.
@@ -86,17 +86,17 @@
by (auto simp add: fun_eq_iff)
lemma r_into_rtrancl [intro]: "!!p. p \<in> r ==> p \<in> r^*"
- -- \<open>@{text rtrancl} of @{text r} contains @{text r}\<close>
+ \<comment> \<open>\<open>rtrancl\<close> of \<open>r\<close> contains \<open>r\<close>\<close>
apply (simp only: split_tupled_all)
apply (erule rtrancl_refl [THEN rtrancl_into_rtrancl])
done
lemma r_into_rtranclp [intro]: "r x y ==> r^** x y"
- -- \<open>@{text rtrancl} of @{text r} contains @{text r}\<close>
+ \<comment> \<open>\<open>rtrancl\<close> of \<open>r\<close> contains \<open>r\<close>\<close>
by (erule rtranclp.rtrancl_refl [THEN rtranclp.rtrancl_into_rtrancl])
lemma rtranclp_mono: "r \<le> s ==> r^** \<le> s^**"
- -- \<open>monotonicity of @{text rtrancl}\<close>
+ \<comment> \<open>monotonicity of \<open>rtrancl\<close>\<close>
apply (rule predicate2I)
apply (erule rtranclp.induct)
apply (rule_tac [2] rtranclp.rtrancl_into_rtrancl, blast+)
@@ -157,7 +157,7 @@
obtains
(base) "a = b"
| (step) y where "(a, y) : r^*" and "(y, b) : r"
- -- \<open>elimination of @{text rtrancl} -- by induction on a special formula\<close>
+ \<comment> \<open>elimination of \<open>rtrancl\<close> -- by induction on a special formula\<close>
apply (subgoal_tac "(a::'a) = b | (EX y. (a,y) : r^* & (y,b) : r)")
apply (rule_tac [2] major [THEN rtrancl_induct])
prefer 2 apply blast
@@ -347,7 +347,7 @@
by (simp only: split_tupled_all) (erule r_into_trancl)
text \<open>
- \medskip Conversions between @{text trancl} and @{text rtrancl}.
+ \medskip Conversions between \<open>trancl\<close> and \<open>rtrancl\<close>.
\<close>
lemma tranclp_into_rtranclp: "r^++ a b ==> r^** a b"
@@ -362,7 +362,7 @@
lemmas rtrancl_into_trancl1 = rtranclp_into_tranclp1 [to_set]
lemma rtranclp_into_tranclp2: "[| r a b; r^** b c |] ==> r^++ a c"
- -- \<open>intro rule from @{text r} and @{text rtrancl}\<close>
+ \<comment> \<open>intro rule from \<open>r\<close> and \<open>rtrancl\<close>\<close>
apply (erule rtranclp.cases)
apply iprover
apply (rule rtranclp_trans [THEN rtranclp_into_tranclp1])
@@ -371,7 +371,7 @@
lemmas rtrancl_into_trancl2 = rtranclp_into_tranclp2 [to_set]
-text \<open>Nice induction rule for @{text trancl}\<close>
+text \<open>Nice induction rule for \<open>trancl\<close>\<close>
lemma tranclp_induct [consumes 1, case_names base step, induct pred: tranclp]:
assumes a: "r^++ a b"
and cases: "!!y. r a y ==> P y"
@@ -394,7 +394,7 @@
and cases: "!!x y. r x y ==> P x y"
"!!x y z. [| r^++ x y; P x y; r^++ y z; P y z |] ==> P x z"
shows "P x y"
- -- \<open>Another induction rule for trancl, incorporating transitivity\<close>
+ \<comment> \<open>Another induction rule for trancl, incorporating transitivity\<close>
by (iprover intro: major [THEN tranclp_induct] cases)
lemmas trancl_trans_induct = tranclp_trans_induct [to_set]
@@ -594,7 +594,7 @@
lemma trancl_insert:
"(insert (y, x) r)^+ = r^+ \<union> {(a, b). (a, y) \<in> r^* \<and> (x, b) \<in> r^*}"
- -- \<open>primitive recursion for @{text trancl} over finite relations\<close>
+ \<comment> \<open>primitive recursion for \<open>trancl\<close> over finite relations\<close>
apply (rule equalityI)
apply (rule subsetI)
apply (simp only: split_tupled_all)
@@ -627,7 +627,7 @@
by auto
-text \<open>@{text Domain} and @{text Range}\<close>
+text \<open>\<open>Domain\<close> and \<open>Range\<close>\<close>
lemma Domain_rtrancl [simp]: "Domain (R^*) = UNIV"
by blast
@@ -671,7 +671,7 @@
apply (auto simp add: finite_Field)
done
-text \<open>More about converse @{text rtrancl} and @{text trancl}, should
+text \<open>More about converse \<open>rtrancl\<close> and \<open>trancl\<close>, should
be merged with main body.\<close>
lemma single_valued_confluent:
@@ -720,7 +720,7 @@
subsection \<open>The power operation on relations\<close>
-text \<open>@{text "R ^^ n = R O ... O R"}, the n-fold composition of @{text R}\<close>
+text \<open>\<open>R ^^ n = R O ... O R\<close>, the n-fold composition of \<open>R\<close>\<close>
overloading
relpow == "compow :: nat \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set"
--- a/src/HOL/Typedef.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Typedef.thy Mon Dec 07 10:38:04 2015 +0100
@@ -14,7 +14,7 @@
assumes Rep: "Rep x \<in> A"
and Rep_inverse: "Abs (Rep x) = x"
and Abs_inverse: "y \<in> A \<Longrightarrow> Rep (Abs y) = y"
- -- \<open>This will be axiomatized for each typedef!\<close>
+ \<comment> \<open>This will be axiomatized for each typedef!\<close>
begin
lemma Rep_inject: "Rep x = Rep y \<longleftrightarrow> x = y"
--- a/src/HOL/Wellfounded.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Wellfounded.thy Mon Dec 07 10:38:04 2015 +0100
@@ -233,7 +233,7 @@
apply (rule_tac x = "{z. z:Q & (z,y) : r^*}" in allE)
apply assumption
apply (erule_tac V = "ALL Q. (EX x. x : Q) --> P Q" for P in thin_rl)
- --\<open>essential for speed\<close>
+ \<comment>\<open>essential for speed\<close>
txt\<open>Blast with new substOccur fails\<close>
apply (fast intro: converse_rtrancl_into_rtrancl)
done
@@ -375,7 +375,7 @@
qed
qed
-lemma wf_comp_self: "wf R = wf (R O R)" -- \<open>special case\<close>
+lemma wf_comp_self: "wf R = wf (R O R)" \<comment> \<open>special case\<close>
by (rule wf_union_merge [where S = "{}", simplified])
@@ -384,7 +384,7 @@
text \<open>Bachmair and Dershowitz 1986, Lemma 2. [Provided by Tjark Weber]\<close>
lemma qc_wf_relto_iff:
- assumes "R O S \<subseteq> (R \<union> S)\<^sup>* O R" -- \<open>R quasi-commutes over S\<close>
+ assumes "R O S \<subseteq> (R \<union> S)\<^sup>* O R" \<comment> \<open>R quasi-commutes over S\<close>
shows "wf (S\<^sup>* O R O S\<^sup>*) \<longleftrightarrow> wf R" (is "wf ?S \<longleftrightarrow> _")
proof
assume "wf ?S"
--- a/src/HOL/Wfrec.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Wfrec.thy Mon Dec 07 10:38:04 2015 +0100
@@ -79,11 +79,11 @@
finally show "wfrec R F x = F (wfrec R F) x" .
qed
-subsection \<open>Wellfoundedness of @{text same_fst}\<close>
+subsection \<open>Wellfoundedness of \<open>same_fst\<close>\<close>
definition same_fst :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> ('b \<times> 'b) set) \<Rightarrow> (('a \<times> 'b) \<times> ('a \<times> 'b)) set" where
"same_fst P R = {((x', y'), (x, y)) . x' = x \<and> P x \<and> (y',y) \<in> R x}"
- --\<open>For @{const wfrec} declarations where the first n parameters
+ \<comment>\<open>For @{const wfrec} declarations where the first n parameters
stay unchanged in the recursive call.\<close>
lemma same_fstI [intro!]: "P x \<Longrightarrow> (y', y) \<in> R x \<Longrightarrow> ((x, y'), (x, y)) \<in> same_fst P R"
--- a/src/HOL/Word/Bit_Comparison.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Word/Bit_Comparison.thy Mon Dec 07 10:38:04 2015 +0100
@@ -137,7 +137,7 @@
with 3 have "bin BIT bit = 0" by simp
then have "bin = 0" and "\<not> bit"
by (auto simp add: Bit_def split: if_splits) arith
- then show ?thesis using 0 1 `y < 2 ^ n`
+ then show ?thesis using 0 1 \<open>y < 2 ^ n\<close>
by simp
next
case (Suc m)
@@ -170,7 +170,7 @@
with 3 have "bin BIT bit = 0" by simp
then have "bin = 0" and "\<not> bit"
by (auto simp add: Bit_def split: if_splits) arith
- then show ?thesis using 0 1 `y < 2 ^ n`
+ then show ?thesis using 0 1 \<open>y < 2 ^ n\<close>
by simp
next
case (Suc m)
--- a/src/HOL/Word/Bit_Representation.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Word/Bit_Representation.thy Mon Dec 07 10:38:04 2015 +0100
@@ -2,13 +2,13 @@
Author: Jeremy Dawson, NICTA
*)
-section {* Integers as implict bit strings *}
+section \<open>Integers as implict bit strings\<close>
theory Bit_Representation
imports Misc_Numeric
begin
-subsection {* Constructors and destructors for binary integers *}
+subsection \<open>Constructors and destructors for binary integers\<close>
definition Bit :: "int \<Rightarrow> bool \<Rightarrow> int" (infixl "BIT" 90)
where
@@ -270,7 +270,7 @@
bin_nth_numeral_simps
-subsection {* Truncating binary integers *}
+subsection \<open>Truncating binary integers\<close>
definition bin_sign :: "int \<Rightarrow> int"
where
@@ -750,7 +750,7 @@
[THEN rco_lem [THEN fun_cong], unfolded o_def]
-subsection {* Splitting and concatenation *}
+subsection \<open>Splitting and concatenation\<close>
primrec bin_split :: "nat \<Rightarrow> int \<Rightarrow> int \<times> int" where
Z: "bin_split 0 w = (w, 0)"
--- a/src/HOL/Word/Bits.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Word/Bits.thy Mon Dec 07 10:38:04 2015 +0100
@@ -2,7 +2,7 @@
Author: Author: Brian Huffman, PSU and Gerwin Klein, NICTA
*)
-section {* Syntactic classes for bitwise operations *}
+section \<open>Syntactic classes for bitwise operations\<close>
theory Bits
imports Main
@@ -14,15 +14,15 @@
and bitOR :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "OR" 59)
and bitXOR :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "XOR" 59)
-text {*
+text \<open>
We want the bitwise operations to bind slightly weaker
- than @{text "+"} and @{text "-"}, but @{text "~~"} to
- bind slightly stronger than @{text "*"}.
-*}
+ than \<open>+\<close> and \<open>-\<close>, but \<open>~~\<close> to
+ bind slightly stronger than \<open>*\<close>.
+\<close>
-text {*
+text \<open>
Testing and shifting operations.
-*}
+\<close>
class bits = bit +
fixes test_bit :: "'a \<Rightarrow> nat \<Rightarrow> bool" (infixl "!!" 100)
--- a/src/HOL/Word/Bits_Bit.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Word/Bits_Bit.thy Mon Dec 07 10:38:04 2015 +0100
@@ -2,7 +2,7 @@
Author: Author: Brian Huffman, PSU and Gerwin Klein, NICTA
*)
-section {* Bit operations in $\cal Z_2$ *}
+section \<open>Bit operations in $\cal Z_2$\<close>
theory Bits_Bit
imports Bits "~~/src/HOL/Library/Bit"
--- a/src/HOL/Word/Bits_Int.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Word/Bits_Int.thy Mon Dec 07 10:38:04 2015 +0100
@@ -6,13 +6,13 @@
and converting them to and from lists of bools.
*)
-section {* Bitwise Operations on Binary Integers *}
+section \<open>Bitwise Operations on Binary Integers\<close>
theory Bits_Int
imports Bits Bit_Representation
begin
-subsection {* Logical operations *}
+subsection \<open>Logical operations\<close>
text "bit-wise logical operations on the int type"
@@ -43,7 +43,7 @@
end
-subsubsection {* Basic simplification rules *}
+subsubsection \<open>Basic simplification rules\<close>
lemma int_not_BIT [simp]:
"NOT (w BIT b) = (NOT w) BIT (\<not> b)"
@@ -88,7 +88,7 @@
"(x BIT b) XOR (y BIT c) = (x XOR y) BIT ((b \<or> c) \<and> \<not> (b \<and> c))"
unfolding int_xor_def by auto
-subsubsection {* Binary destructors *}
+subsubsection \<open>Binary destructors\<close>
lemma bin_rest_NOT [simp]: "bin_rest (NOT x) = NOT (bin_rest x)"
by (cases x rule: bin_exhaust, simp)
@@ -121,7 +121,7 @@
"!!x. bin_nth (NOT x) n = (~ bin_nth x n)"
by (induct n) auto
-subsubsection {* Derived properties *}
+subsubsection \<open>Derived properties\<close>
lemma int_xor_minus1 [simp]: "(-1::int) XOR x = NOT x"
by (auto simp add: bin_eq_iff bin_nth_ops)
@@ -219,10 +219,10 @@
declare bin_ops_comm [simp] bbw_assocs [simp]
*)
-subsubsection {* Simplification with numerals *}
+subsubsection \<open>Simplification with numerals\<close>
-text {* Cases for @{text "0"} and @{text "-1"} are already covered by
- other simp rules. *}
+text \<open>Cases for \<open>0\<close> and \<open>-1\<close> are already covered by
+ other simp rules.\<close>
lemma bin_rl_eqI: "\<lbrakk>bin_rest x = bin_rest y; bin_last x = bin_last y\<rbrakk> \<Longrightarrow> x = y"
by (metis (mono_tags) BIT_eq_iff bin_ex_rl bin_last_BIT bin_rest_BIT)
@@ -235,8 +235,8 @@
"bin_last (- numeral (Num.BitM w))"
by (simp only: BIT_bin_simps [symmetric] bin_last_BIT)
-text {* FIXME: The rule sets below are very large (24 rules for each
- operator). Is there a simpler way to do this? *}
+text \<open>FIXME: The rule sets below are very large (24 rules for each
+ operator). Is there a simpler way to do this?\<close>
lemma int_and_numerals [simp]:
"numeral (Num.Bit0 x) AND numeral (Num.Bit0 y) = (numeral x AND numeral y) BIT False"
@@ -319,7 +319,7 @@
"- numeral (Num.Bit1 x) XOR (1::int) = - numeral (Num.Bit0 (x + Num.One))"
by (rule bin_rl_eqI, simp, simp)+
-subsubsection {* Interactions with arithmetic *}
+subsubsection \<open>Interactions with arithmetic\<close>
lemma plus_and_or [rule_format]:
"ALL y::int. (x AND y) + (x OR y) = x + y"
@@ -358,7 +358,7 @@
apply (case_tac bit, auto)
done
-subsubsection {* Truncating results of bit-wise operations *}
+subsubsection \<open>Truncating results of bit-wise operations\<close>
lemma bin_trunc_ao:
"!!x y. (bintrunc n x) AND (bintrunc n y) = bintrunc n (x AND y)"
@@ -382,7 +382,7 @@
lemmas bin_trunc_and = bin_trunc_ao(1) [THEN bintr_bintr_i]
lemmas bin_trunc_or = bin_trunc_ao(2) [THEN bintr_bintr_i]
-subsection {* Setting and clearing bits *}
+subsection \<open>Setting and clearing bits\<close>
(** nth bit, set/clear **)
@@ -480,7 +480,7 @@
by (simp add: numeral_eq_Suc)
-subsection {* Splitting and concatenation *}
+subsection \<open>Splitting and concatenation\<close>
definition bin_rcat :: "nat \<Rightarrow> int list \<Rightarrow> int"
where
@@ -619,7 +619,7 @@
apply (simp add: Bit_def mod_mult_mult1 p1mod22k)
done
-subsection {* Miscellaneous lemmas *}
+subsection \<open>Miscellaneous lemmas\<close>
lemma nth_2p_bin:
"bin_nth (2 ^ n) m = (m = n)"
--- a/src/HOL/Word/Bool_List_Representation.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Word/Bool_List_Representation.thy Mon Dec 07 10:38:04 2015 +0100
@@ -29,7 +29,7 @@
unfolding map2_def by auto
-subsection {* Operations on lists of booleans *}
+subsection \<open>Operations on lists of booleans\<close>
primrec bl_to_bin_aux :: "bool list \<Rightarrow> int \<Rightarrow> int"
where
@@ -66,10 +66,10 @@
subsection "Arithmetic in terms of bool lists"
-text {*
+text \<open>
Arithmetic operations in terms of the reversed bool list,
assuming input list(s) the same length, and don't extend them.
-*}
+\<close>
primrec rbl_succ :: "bool list => bool list"
where
@@ -83,14 +83,14 @@
primrec rbl_add :: "bool list => bool list => bool list"
where
- -- "result is length of first arg, second arg may be longer"
+ \<comment> "result is length of first arg, second arg may be longer"
Nil: "rbl_add Nil x = Nil"
| Cons: "rbl_add (y # ys) x = (let ws = rbl_add ys (tl x) in
(y ~= hd x) # (if hd x & y then rbl_succ ws else ws))"
primrec rbl_mult :: "bool list => bool list => bool list"
where
- -- "result is length of first arg, second arg may be longer"
+ \<comment> "result is length of first arg, second arg may be longer"
Nil: "rbl_mult Nil x = Nil"
| Cons: "rbl_mult (y # ys) x = (let ws = False # rbl_mult ys x in
if y then rbl_add ws x else ws)"
@@ -129,7 +129,7 @@
bin_to_bl_aux (n - 1) (numeral w) (True # bl)"
by (cases n) auto
-text {* Link between bin and bool list. *}
+text \<open>Link between bin and bool list.\<close>
lemma bl_to_bin_aux_append:
"bl_to_bin_aux (bs @ cs) w = bl_to_bin_aux cs (bl_to_bin_aux bs w)"
@@ -1118,14 +1118,14 @@
proof (induct n nw w cs arbitrary: v bs rule: bin_rsplit_aux.induct)
case (1 n m w cs v bs) show ?case
proof (cases "m = 0")
- case True then show ?thesis using `length bs = length cs` by simp
+ case True then show ?thesis using \<open>length bs = length cs\<close> by simp
next
case False
- from "1.hyps" `m \<noteq> 0` `n \<noteq> 0` have hyp: "\<And>v bs. length bs = Suc (length cs) \<Longrightarrow>
+ from "1.hyps" \<open>m \<noteq> 0\<close> \<open>n \<noteq> 0\<close> have hyp: "\<And>v bs. length bs = Suc (length cs) \<Longrightarrow>
length (bin_rsplit_aux n (m - n) v bs) =
length (bin_rsplit_aux n (m - n) (fst (bin_split n w)) (snd (bin_split n w) # cs))"
by auto
- show ?thesis using `length bs = length cs` `n \<noteq> 0`
+ show ?thesis using \<open>length bs = length cs\<close> \<open>n \<noteq> 0\<close>
by (auto simp add: bin_rsplit_aux_simp_alt Let_def bin_rsplit_len
split: prod.split)
qed
@@ -1140,7 +1140,7 @@
done
-text {* Even more bit operations *}
+text \<open>Even more bit operations\<close>
instantiation int :: bitss
begin
--- a/src/HOL/Word/Misc_Numeric.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Word/Misc_Numeric.thy Mon Dec 07 10:38:04 2015 +0100
@@ -2,7 +2,7 @@
Author: Jeremy Dawson, NICTA
*)
-section {* Useful Numerical Lemmas *}
+section \<open>Useful Numerical Lemmas\<close>
theory Misc_Numeric
imports Main
--- a/src/HOL/Word/Misc_Typedef.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Word/Misc_Typedef.thy Mon Dec 07 10:38:04 2015 +0100
@@ -4,7 +4,7 @@
Consequences of type definition theorems, and of extended type definition.
*)
-section {* Type Definition Theorems *}
+section \<open>Type Definition Theorems\<close>
theory Misc_Typedef
imports Main
--- a/src/HOL/Word/Type_Length.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Word/Type_Length.thy Mon Dec 07 10:38:04 2015 +0100
@@ -2,24 +2,24 @@
Author: John Matthews, Galois Connections, Inc., copyright 2006
*)
-section {* Assigning lengths to types by typeclasses *}
+section \<open>Assigning lengths to types by typeclasses\<close>
theory Type_Length
imports "~~/src/HOL/Library/Numeral_Type"
begin
-text {*
+text \<open>
The aim of this is to allow any type as index type, but to provide a
default instantiation for numeral types. This independence requires
- some duplication with the definitions in @{text "Numeral_Type"}.
-*}
+ some duplication with the definitions in \<open>Numeral_Type\<close>.
+\<close>
class len0 =
fixes len_of :: "'a itself \<Rightarrow> nat"
-text {*
+text \<open>
Some theorems are only true on words with length greater 0.
-*}
+\<close>
class len = len0 +
assumes len_gt_0 [iff]: "0 < len_of TYPE ('a)"
--- a/src/HOL/Word/Word.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Word/Word.thy Mon Dec 07 10:38:04 2015 +0100
@@ -2,7 +2,7 @@
Author: Jeremy Dawson and Gerwin Klein, NICTA
*)
-section {* A type of finite bit strings *}
+section \<open>A type of finite bit strings\<close>
theory Word
imports
@@ -14,9 +14,9 @@
Word_Miscellaneous
begin
-text {* See @{file "Examples/WordExamples.thy"} for examples. *}
-
-subsection {* Type definition *}
+text \<open>See @{file "Examples/WordExamples.thy"} for examples.\<close>
+
+subsection \<open>Type definition\<close>
typedef (overloaded) 'a word = "{(0::int) ..< 2 ^ len_of TYPE('a::len0)}"
morphisms uint Abs_word by auto
@@ -45,8 +45,8 @@
definition word_of_int :: "int \<Rightarrow> 'a::len0 word"
where
- -- {* representation of words using unsigned or signed bins,
- only difference in these is the type class *}
+ \<comment> \<open>representation of words using unsigned or signed bins,
+ only difference in these is the type class\<close>
"word_of_int k = Abs_word (k mod 2 ^ len_of TYPE('a))"
lemma uint_word_of_int:
@@ -67,11 +67,11 @@
qed
-subsection {* Type conversions and casting *}
+subsection \<open>Type conversions and casting\<close>
definition sint :: "'a::len word \<Rightarrow> int"
where
- -- {* treats the most-significant-bit as a sign bit *}
+ \<comment> \<open>treats the most-significant-bit as a sign bit\<close>
sint_uint: "sint w = sbintrunc (len_of TYPE ('a) - 1) (uint w)"
definition unat :: "'a::len0 word \<Rightarrow> nat"
@@ -80,7 +80,7 @@
definition uints :: "nat \<Rightarrow> int set"
where
- -- "the sets of integers representing the words"
+ \<comment> "the sets of integers representing the words"
"uints n = range (bintrunc n)"
definition sints :: "nat \<Rightarrow> int set"
@@ -105,7 +105,7 @@
definition scast :: "'a::len word \<Rightarrow> 'b::len word"
where
- -- "cast a word to a different length"
+ \<comment> "cast a word to a different length"
"scast w = word_of_int (sint w)"
definition ucast :: "'a::len0 word \<Rightarrow> 'b::len0 word"
@@ -135,7 +135,7 @@
definition source_size :: "('a::len0 word \<Rightarrow> 'b) \<Rightarrow> nat"
where
- -- "whether a cast (or other) function is to a longer or shorter length"
+ \<comment> "whether a cast (or other) function is to a longer or shorter length"
[code del]: "source_size c = (let arb = undefined; x = c arb in size arb)"
definition target_size :: "('a \<Rightarrow> 'b::len0 word) \<Rightarrow> nat"
@@ -171,7 +171,7 @@
"case x of (XCONST of_int :: 'a) y => b" => "CONST word_int_case (%y. b) x"
-subsection {* Correspondence relation for theorem transfer *}
+subsection \<open>Correspondence relation for theorem transfer\<close>
definition cr_word :: "int \<Rightarrow> 'a::len0 word \<Rightarrow> bool"
where
@@ -189,7 +189,7 @@
setup_lifting Quotient_word reflp_word
-text {* TODO: The next lemma could be generated automatically. *}
+text \<open>TODO: The next lemma could be generated automatically.\<close>
lemma uint_transfer [transfer_rule]:
"(rel_fun pcr_word op =) (bintrunc (len_of TYPE('a)))
@@ -198,7 +198,7 @@
by (simp add: no_bintr_alt1 uint_word_of_int)
-subsection {* Basic code generation setup *}
+subsection \<open>Basic code generation setup\<close>
definition Word :: "int \<Rightarrow> 'a::len0 word"
where
@@ -241,7 +241,7 @@
no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
-subsection {* Type-definition locale instantiations *}
+subsection \<open>Type-definition locale instantiations\<close>
lemmas uint_0 = uint_nonnegative (* FIXME duplicate *)
lemmas uint_lt = uint_bounded (* FIXME duplicate *)
@@ -279,7 +279,7 @@
by (fact td_ext_ubin)
-subsection {* Arithmetic operations *}
+subsection \<open>Arithmetic operations\<close>
lift_definition word_succ :: "'a::len0 word \<Rightarrow> 'a word" is "\<lambda>x. x + 1"
by (metis bintr_ariths(6))
@@ -317,7 +317,7 @@
end
-text {* Legacy theorems: *}
+text \<open>Legacy theorems:\<close>
lemma word_arith_wis [code]: shows
word_add_def: "a + b = word_of_int (uint a + uint b)" and
@@ -372,7 +372,7 @@
"a udvd b = (EX n>=0. uint b = n * uint a)"
-subsection {* Ordering *}
+subsection \<open>Ordering\<close>
instantiation word :: (len0) linorder
begin
@@ -397,7 +397,7 @@
"(x <s y) = (x <=s y & x ~= y)"
-subsection {* Bit-wise operations *}
+subsection \<open>Bit-wise operations\<close>
instantiation word :: (len0) bits
begin
@@ -433,7 +433,7 @@
definition shiftr1 :: "'a word \<Rightarrow> 'a word"
where
- -- "shift right as unsigned or as signed, ie logical or arithmetic"
+ \<comment> "shift right as unsigned or as signed, ie logical or arithmetic"
"shiftr1 w = word_of_int (bin_rest (uint w))"
definition
@@ -474,7 +474,7 @@
"clearBit w n = set_bit w n False"
-subsection {* Shift operations *}
+subsection \<open>Shift operations\<close>
definition sshiftr1 :: "'a :: len word => 'a word"
where
@@ -505,7 +505,7 @@
"slice n w = slice1 (size w - n) w"
-subsection {* Rotation *}
+subsection \<open>Rotation\<close>
definition rotater1 :: "'a list => 'a list"
where
@@ -530,7 +530,7 @@
else word_rotl (nat (- i)) w)"
-subsection {* Split and cat operations *}
+subsection \<open>Split and cat operations\<close>
definition word_cat :: "'a :: len0 word => 'b :: len0 word => 'c :: len0 word"
where
@@ -552,14 +552,14 @@
"word_rsplit w =
map word_of_int (bin_rsplit (len_of TYPE ('b)) (len_of TYPE ('a), uint w))"
-definition max_word :: "'a::len word" -- "Largest representable machine integer."
+definition max_word :: "'a::len word" \<comment> "Largest representable machine integer."
where
"max_word = word_of_int (2 ^ len_of TYPE('a) - 1)"
lemmas of_nth_def = word_set_bits_def (* FIXME duplicate *)
-subsection {* Theorems about typedefs *}
+subsection \<open>Theorems about typedefs\<close>
lemma sint_sbintrunc':
"sint (word_of_int bin :: 'a word) =
@@ -805,7 +805,7 @@
unfolding word_size by (rule order_trans [OF _ sint_ge])
-subsection {* Testing bits *}
+subsection \<open>Testing bits\<close>
lemma test_bit_eq_iff: "(test_bit (u::'a::len0 word) = test_bit v) = (u = v)"
unfolding word_test_bit_def by (simp add: bin_nth_eq_iff)
@@ -1188,7 +1188,7 @@
lemmas word_log_defs = word_and_def word_or_def word_xor_def word_not_def
-subsection {* Word Arithmetic *}
+subsection \<open>Word Arithmetic\<close>
lemma word_less_alt: "(a < b) = (uint a < uint b)"
by (fact word_less_def)
@@ -1292,7 +1292,7 @@
(* now, to get the weaker results analogous to word_div/mod_def *)
-subsection {* Transferring goals from words to ints *}
+subsection \<open>Transferring goals from words to ints\<close>
lemma word_ths:
shows
@@ -1368,7 +1368,7 @@
by (rule_tac x="uint x" in exI) simp
-subsection {* Order on fixed-length words *}
+subsection \<open>Order on fixed-length words\<close>
lemma word_zero_le [simp] :
"0 <= (y :: 'a :: len0 word)"
@@ -1438,9 +1438,9 @@
moreover from assms have "0 \<noteq> uint w" by (simp add: uint_0_iff)
ultimately have "1 \<le> uint w" by arith
from uint_lt2p [of w] have "uint w - 1 < 2 ^ len_of TYPE('a)" by arith
- with `1 \<le> uint w` have "(uint w - 1) mod 2 ^ len_of TYPE('a) = uint w - 1"
+ with \<open>1 \<le> uint w\<close> have "(uint w - 1) mod 2 ^ len_of TYPE('a) = uint w - 1"
by (auto intro: mod_pos_pos_trivial)
- with `1 \<le> uint w` have "nat ((uint w - 1) mod 2 ^ len_of TYPE('a)) = nat (uint w) - 1"
+ with \<open>1 \<le> uint w\<close> have "nat ((uint w - 1) mod 2 ^ len_of TYPE('a)) = nat (uint w) - 1"
by auto
then show ?thesis
by (simp only: unat_def int_word_uint word_arith_wis mod_diff_right_eq [symmetric])
@@ -1458,7 +1458,7 @@
using uint_ge_0 [of y] uint_lt2p [of x] by arith
-subsection {* Conditions for the addition (etc) of two words to overflow *}
+subsection \<open>Conditions for the addition (etc) of two words to overflow\<close>
lemma uint_add_lem:
"(uint x + uint y < 2 ^ len_of TYPE('a)) =
@@ -1503,7 +1503,7 @@
using mod_sub_if_z [of "uint a" _ "uint b"] by (simp add: uint_word_ariths)
-subsection {* Definition of @{text uint_arith} *}
+subsection \<open>Definition of \<open>uint_arith\<close>\<close>
lemma word_of_int_inverse:
"word_of_int r = a \<Longrightarrow> 0 <= r \<Longrightarrow> r < 2 ^ len_of TYPE('a) \<Longrightarrow>
@@ -1541,7 +1541,7 @@
by auto
(* uint_arith_tac: reduce to arithmetic on int, try to solve by arith *)
-ML {*
+ML \<open>
fun uint_arith_simpset ctxt =
ctxt addsimps @{thms uint_arith_simps}
delsimps @{thms word_uint.Rep_inject}
@@ -1570,14 +1570,14 @@
end
fun uint_arith_tac ctxt = SELECT_GOAL (EVERY (uint_arith_tacs ctxt))
-*}
+\<close>
method_setup uint_arith =
- {* Scan.succeed (SIMPLE_METHOD' o uint_arith_tac) *}
+ \<open>Scan.succeed (SIMPLE_METHOD' o uint_arith_tac)\<close>
"solving word arithmetic via integers and arith"
-subsection {* More on overflows and monotonicity *}
+subsection \<open>More on overflows and monotonicity\<close>
lemma no_plus_overflow_uint_size:
"((x :: 'a :: len0 word) <= x + y) = (uint x + uint y < 2 ^ size x)"
@@ -1803,7 +1803,7 @@
word_pred_rbl word_mult_rbl word_add_rbl)
-subsection {* Arithmetic type class instantiations *}
+subsection \<open>Arithmetic type class instantiations\<close>
lemmas word_le_0_iff [simp] =
word_zero_le [THEN leD, THEN linorder_antisym_conv1]
@@ -1820,13 +1820,13 @@
using word_ubin.norm_eq_iff [where 'a='a, of "numeral bin" 0]
by (simp add: iszero_def [symmetric])
-text {* Use @{text iszero} to simplify equalities between word numerals. *}
+text \<open>Use \<open>iszero\<close> to simplify equalities between word numerals.\<close>
lemmas word_eq_numeral_iff_iszero [simp] =
eq_numeral_iff_iszero [where 'a="'a::len word"]
-subsection {* Word and nat *}
+subsection \<open>Word and nat\<close>
lemma td_ext_unat [OF refl]:
"n = len_of TYPE ('a :: len) \<Longrightarrow>
@@ -2017,7 +2017,7 @@
unfolding uint_nat by (simp add : unat_mod zmod_int)
-subsection {* Definition of @{text unat_arith} tactic *}
+subsection \<open>Definition of \<open>unat_arith\<close> tactic\<close>
lemma unat_split:
fixes x::"'a::len word"
@@ -2043,7 +2043,7 @@
(* unat_arith_tac: tactic to reduce word arithmetic to nat,
try to solve via arith *)
-ML {*
+ML \<open>
fun unat_arith_simpset ctxt =
ctxt addsimps @{thms unat_arith_simps}
delsimps @{thms word_unat.Rep_inject}
@@ -2070,10 +2070,10 @@
end
fun unat_arith_tac ctxt = SELECT_GOAL (EVERY (unat_arith_tacs ctxt))
-*}
+\<close>
method_setup unat_arith =
- {* Scan.succeed (SIMPLE_METHOD' o unat_arith_tac) *}
+ \<open>Scan.succeed (SIMPLE_METHOD' o unat_arith_tac)\<close>
"solving word arithmetic via natural numbers and arith"
lemma no_plus_overflow_unat_size:
@@ -2202,7 +2202,7 @@
done
-subsection {* Cardinality, finiteness of set of words *}
+subsection \<open>Cardinality, finiteness of set of words\<close>
instance word :: (len0) finite
by standard (simp add: type_definition.univ [OF type_definition_word])
@@ -2215,7 +2215,7 @@
unfolding word_size by (rule card_word)
-subsection {* Bitwise Operations on Words *}
+subsection \<open>Bitwise Operations on Words\<close>
lemmas bin_log_bintrs = bin_trunc_not bin_trunc_xor bin_trunc_and bin_trunc_or
@@ -2254,7 +2254,7 @@
"- numeral a XOR - numeral b = word_of_int (- numeral a XOR - numeral b)"
by (transfer, rule refl)+
-text {* Special cases for when one of the arguments equals 1. *}
+text \<open>Special cases for when one of the arguments equals 1.\<close>
lemma word_bitwise_1_simps [simp]:
"NOT (1::'a::len0 word) = -2"
@@ -2272,7 +2272,7 @@
"- numeral a XOR 1 = word_of_int (- numeral a XOR 1)"
by (transfer, simp)+
-text {* Special cases for when one of the arguments equals -1. *}
+text \<open>Special cases for when one of the arguments equals -1.\<close>
lemma word_bitwise_m1_simps [simp]:
"NOT (-1::'a::len0 word) = 0"
@@ -2759,7 +2759,7 @@
done
-subsection {* Shifting, Rotating, and Splitting Words *}
+subsection \<open>Shifting, Rotating, and Splitting Words\<close>
lemma shiftl1_wi [simp]: "shiftl1 (word_of_int w) = word_of_int (w BIT False)"
unfolding shiftl1_def
@@ -2923,7 +2923,7 @@
done
-subsubsection {* shift functions in terms of lists of bools *}
+subsubsection \<open>shift functions in terms of lists of bools\<close>
lemmas bshiftr1_numeral [simp] =
bshiftr1_def [where w="numeral w", unfolded to_bl_numeral] for w
@@ -3215,7 +3215,7 @@
done
-subsubsection {* Mask *}
+subsubsection \<open>Mask\<close>
lemma nth_mask [OF refl, simp]:
"m = mask n \<Longrightarrow> test_bit m i = (i < n & i < size m)"
@@ -3350,7 +3350,7 @@
by (clarsimp simp: and_mask_wi word_of_int_power_hom bintr_ariths)
-subsubsection {* Revcast *}
+subsubsection \<open>Revcast\<close>
lemmas revcast_def' = revcast_def [simplified]
lemmas revcast_def'' = revcast_def' [simplified word_size]
@@ -3382,7 +3382,7 @@
by (fact revcast_ucast [THEN word_rev_gal'])
--- "linking revcast and cast via shift"
+\<comment> "linking revcast and cast via shift"
lemmas wsst_TYs = source_size target_size word_size
@@ -3465,7 +3465,7 @@
rc2 [simplified rev_shiftr revcast_ucast [symmetric]]
-subsubsection {* Slices *}
+subsubsection \<open>Slices\<close>
lemma slice1_no_bin [simp]:
"slice1 n (numeral w :: 'b word) = of_bl (takefill False n (bin_to_bl (len_of TYPE('b :: len0)) (numeral w)))"
@@ -3488,7 +3488,7 @@
lemmas slice_take = slice_take' [unfolded word_size]
--- "shiftr to a word of the same size is just slice,
+\<comment> "shiftr to a word of the same size is just slice,
slice is just shiftr then ucast"
lemmas shiftr_slice = trans [OF shiftr_bl [THEN meta_eq_to_obj_eq] slice_take [symmetric]]
@@ -3573,8 +3573,8 @@
lemmas sym_notr =
not_iff [THEN iffD2, THEN not_sym, THEN not_iff [THEN iffD1]]
--- {* problem posed by TPHOLs referee:
- criterion for overflow of addition of signed integers *}
+\<comment> \<open>problem posed by TPHOLs referee:
+ criterion for overflow of addition of signed integers\<close>
lemma sofl_test:
"(sint (x :: 'a :: len word) + sint y = sint (x + y)) =
@@ -3605,7 +3605,7 @@
done
-subsection {* Split and cat *}
+subsection \<open>Split and cat\<close>
lemmas word_split_bin' = word_split_def
lemmas word_cat_bin' = word_cat_def
@@ -3711,7 +3711,7 @@
apply (rule refl conjI)+
done
--- "keep quantifiers for use in simplification"
+\<comment> "keep quantifiers for use in simplification"
lemma test_bit_split':
"word_split c = (a, b) --> (ALL n m. b !! n = (n < size b & c !! n) &
a !! m = (m < size a & c !! (m + size b)))"
@@ -3742,13 +3742,13 @@
apply (fastforce intro ! : word_eqI simp add : word_size)
done
--- {* this odd result is analogous to @{text "ucast_id"},
- result to the length given by the result type *}
+\<comment> \<open>this odd result is analogous to \<open>ucast_id\<close>,
+ result to the length given by the result type\<close>
lemma word_cat_id: "word_cat a b = b"
unfolding word_cat_bin' by (simp add: word_ubin.inverse_norm)
--- "limited hom result"
+\<comment> "limited hom result"
lemma word_cat_hom:
"len_of TYPE('a::len0) <= len_of TYPE('b::len0) + len_of TYPE ('c::len0)
\<Longrightarrow>
@@ -3771,7 +3771,7 @@
lemmas word_cat_split_size = sym [THEN [2] word_cat_split_alt [symmetric]]
-subsubsection {* Split and slice *}
+subsubsection \<open>Split and slice\<close>
lemma split_slices:
"word_split w = (u, v) \<Longrightarrow> u = slice (size v) w & v = slice 0 w"
@@ -3816,9 +3816,9 @@
lemmas word_split_bl_no_bin [simp] =
word_split_bl_eq [where c="numeral c", unfolded to_bl_numeral] for c
-text {* this odd result arises from the fact that the statement of the
+text \<open>this odd result arises from the fact that the statement of the
result implies that the decoded words are of the same type,
- and therefore of the same length, as the original word *}
+ and therefore of the same length, as the original word\<close>
lemma word_rsplit_same: "word_rsplit w = [w]"
unfolding word_rsplit_def by (simp add : bin_rsplit_all)
@@ -3892,7 +3892,7 @@
trans [OF nth_rev_alt [THEN test_bit_cong]
test_bit_rsplit [OF refl asm_rl diff_Suc_less]]
--- "lazy way of expressing that u and v, and su and sv, have same types"
+\<comment> "lazy way of expressing that u and v, and su and sv, have same types"
lemma word_rsplit_len_indep [OF refl refl refl refl]:
"[u,v] = p \<Longrightarrow> [su,sv] = q \<Longrightarrow> word_rsplit u = su \<Longrightarrow>
word_rsplit v = sv \<Longrightarrow> length su = length sv"
@@ -3975,7 +3975,7 @@
done
-subsection {* Rotation *}
+subsection \<open>Rotation\<close>
lemmas rotater_0' [simp] = rotater_def [where n = "0", simplified]
@@ -3997,7 +3997,7 @@
rotate_eq_mod
-subsubsection {* Rotation of list to right *}
+subsubsection \<open>Rotation of list to right\<close>
lemma rotate1_rl': "rotater1 (l @ [a]) = a # l"
unfolding rotater1_def by (cases l) auto
@@ -4072,7 +4072,7 @@
lemmas rotater_add = rotater_eqs (2)
-subsubsection {* map, map2, commuting with rotate(r) *}
+subsubsection \<open>map, map2, commuting with rotate(r)\<close>
lemma butlast_map:
"xs ~= [] \<Longrightarrow> butlast (map f xs) = map f (butlast xs)"
@@ -4147,7 +4147,7 @@
by (induct n) (auto intro!: lth)
--- "corresponding equalities for word rotation"
+\<comment> "corresponding equalities for word rotation"
lemma to_bl_rotl:
"to_bl (word_rotl n w) = rotate n (to_bl w)"
@@ -4248,7 +4248,7 @@
lemmas word_roti_conv_mod = word_roti_conv_mod' [unfolded word_size]
-subsubsection {* "Word rotation commutes with bit-wise operations *}
+subsubsection \<open>"Word rotation commutes with bit-wise operations\<close>
(* using locale to not pollute lemma namespace *)
locale word_rotate
@@ -4328,7 +4328,7 @@
declare word_roti_def [simp]
-subsection {* Maximum machine word *}
+subsection \<open>Maximum machine word\<close>
lemma word_int_cases:
obtains n where "(x ::'a::len0 word) = word_of_int n" and "0 \<le> n" and "n < 2^len_of TYPE('a)"
@@ -4630,7 +4630,7 @@
done
-subsection {* Recursion combinator for words *}
+subsection \<open>Recursion combinator for words\<close>
definition word_rec :: "'a \<Rightarrow> ('b::len word \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b word \<Rightarrow> 'a"
where
--- a/src/HOL/Word/WordBitwise.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Word/WordBitwise.thy Mon Dec 07 10:38:04 2015 +0100
@@ -9,7 +9,7 @@
begin
-text {* Helper constants used in defining addition *}
+text \<open>Helper constants used in defining addition\<close>
definition
xor3 :: "bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool"
@@ -39,9 +39,9 @@
"xor3 a b False = (a \<noteq> b)"
by (simp_all add: xor3_def)
-text {* Breaking up word equalities into equalities on their
+text \<open>Breaking up word equalities into equalities on their
bit lists. Equalities are generated and manipulated in the
-reverse order to to_bl. *}
+reverse order to to_bl.\<close>
lemma word_eq_rbl_eq:
"(x = y) = (rev (to_bl x) = rev (to_bl y))"
@@ -322,7 +322,7 @@
using word_rbl_mul_induct[where xs="rev (to_bl x)" and y=y]
by (simp add: word_size)
-text {* Breaking up inequalities into bitlist properties. *}
+text \<open>Breaking up inequalities into bitlist properties.\<close>
definition
"rev_bl_order F xs ys =
@@ -449,8 +449,8 @@
apply auto
done
-text {* Lemmas for unpacking rev (to_bl n) for numerals n and also
-for irreducible values and expressions. *}
+text \<open>Lemmas for unpacking rev (to_bl n) for numerals n and also
+for irreducible values and expressions.\<close>
lemma rev_bin_to_bl_simps:
"rev (bin_to_bl 0 x) = []"
@@ -494,9 +494,9 @@
"\<lbrakk> i = x; x < j; [x + 1 ..< j] = xs \<rbrakk> \<Longrightarrow> [i ..< j] = (x # xs)"
by (simp_all add: upt_eq_Nil_conv upt_eq_Cons_conv)
-text {* Tactic definition *}
+text \<open>Tactic definition\<close>
-ML {*
+ML \<open>
structure Word_Bitwise_Tac =
struct
@@ -617,10 +617,10 @@
end
-*}
+\<close>
method_setup word_bitwise =
- {* Scan.succeed (fn ctxt => Method.SIMPLE_METHOD (Word_Bitwise_Tac.tac ctxt 1)) *}
+ \<open>Scan.succeed (fn ctxt => Method.SIMPLE_METHOD (Word_Bitwise_Tac.tac ctxt 1))\<close>
"decomposer for word equalities and inequalities into bit propositions"
end
--- a/src/HOL/Word/Word_Miscellaneous.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Word/Word_Miscellaneous.thy Mon Dec 07 10:38:04 2015 +0100
@@ -2,7 +2,7 @@
Author: Miscellaneous
*)
-section {* Miscellaneous lemmas, of at least doubtful value *}
+section \<open>Miscellaneous lemmas, of at least doubtful value\<close>
theory Word_Miscellaneous
imports Main "~~/src/HOL/Library/Bit" Misc_Numeric
@@ -67,7 +67,7 @@
apply (erule y)
done
--- "simplifications for specific word lengths"
+\<comment> "simplifications for specific word lengths"
lemmas n2s_ths [THEN eq_reflection] = add_2_eq_Suc add_2_eq_Suc'
lemmas s2n_ths = n2s_ths [symmetric]
--- a/src/HOL/Zorn.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Zorn.thy Mon Dec 07 10:38:04 2015 +0100
@@ -17,7 +17,7 @@
subsubsection \<open>Results that do not require an order\<close>
-text \<open>Let @{text P} be a binary predicate on the set @{text A}.\<close>
+text \<open>Let \<open>P\<close> be a binary predicate on the set \<open>A\<close>.\<close>
locale pred_on =
fixes A :: "'a set"
and P :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<sqsubset>" 50)
@@ -464,7 +464,7 @@
shows "\<exists>m\<in>Field r. \<forall>a\<in>Field r. (m, a) \<in> r \<longrightarrow> a = m"
proof -
have "Preorder r" using po by (simp add: partial_order_on_def)
---\<open>Mirror r in the set of subsets below (wrt r) elements of A\<close>
+\<comment>\<open>Mirror r in the set of subsets below (wrt r) elements of A\<close>
let ?B = "%x. r\<inverse> `` {x}" let ?S = "?B ` Field r"
{
fix C assume 1: "C \<subseteq> ?S" and 2: "\<forall>A\<in>C. \<forall>B\<in>C. A \<subseteq> B \<or> B \<subseteq> A"
@@ -607,7 +607,7 @@
theorem well_ordering: "\<exists>r::'a rel. Well_order r \<and> Field r = UNIV"
proof -
--- \<open>The initial segment relation on well-orders:\<close>
+\<comment> \<open>The initial segment relation on well-orders:\<close>
let ?WO = "{r::'a rel. Well_order r}"
def I \<equiv> "init_seg_of \<inter> ?WO \<times> ?WO"
have I_init: "I \<subseteq> init_seg_of" by (auto simp: I_def)
@@ -619,7 +619,7 @@
hence 0: "Partial_order I"
by (auto simp: partial_order_on_def preorder_on_def antisym_def antisym_init_seg_of refl_on_def
trans_def I_def elim!: trans_init_seg_of)
--- \<open>I-chains have upper bounds in ?WO wrt I: their Union\<close>
+\<comment> \<open>I-chains have upper bounds in ?WO wrt I: their Union\<close>
{ fix R assume "R \<in> Chains I"
hence Ris: "R \<in> Chains init_seg_of" using mono_Chains [OF I_init] by blast
have subch: "chain\<^sub>\<subseteq> R" using \<open>R : Chains I\<close> I_init
@@ -648,13 +648,13 @@
unfolding I_def by blast
}
hence 1: "\<forall>R \<in> Chains I. \<exists>u\<in>Field I. \<forall>r\<in>R. (r, u) \<in> I" by (subst FI) blast
---\<open>Zorn's Lemma yields a maximal well-order m:\<close>
+\<comment>\<open>Zorn's Lemma yields a maximal well-order m:\<close>
then obtain m::"'a rel" where "Well_order m" and
max: "\<forall>r. Well_order r \<and> (m, r) \<in> I \<longrightarrow> r = m"
using Zorns_po_lemma[OF 0 1] unfolding FI by fastforce
---\<open>Now show by contradiction that m covers the whole type:\<close>
+\<comment>\<open>Now show by contradiction that m covers the whole type:\<close>
{ fix x::'a assume "x \<notin> Field m"
---\<open>We assume that x is not covered and extend m at the top with x\<close>
+\<comment>\<open>We assume that x is not covered and extend m at the top with x\<close>
have "m \<noteq> {}"
proof
assume "m = {}"
@@ -666,14 +666,14 @@
hence "Field m \<noteq> {}" by(auto simp:Field_def)
moreover have "wf (m - Id)" using \<open>Well_order m\<close>
by (simp add: well_order_on_def)
---\<open>The extension of m by x:\<close>
+\<comment>\<open>The extension of m by x:\<close>
let ?s = "{(a, x) | a. a \<in> Field m}"
let ?m = "insert (x, x) m \<union> ?s"
have Fm: "Field ?m = insert x (Field m)"
by (auto simp: Field_def)
have "Refl m" and "trans m" and "antisym m" and "Total m" and "wf (m - Id)"
using \<open>Well_order m\<close> by (simp_all add: order_on_defs)
---\<open>We show that the extension is a well-order\<close>
+\<comment>\<open>We show that the extension is a well-order\<close>
have "Refl ?m" using \<open>Refl m\<close> Fm unfolding refl_on_def by blast
moreover have "trans ?m" using \<open>trans m\<close> and \<open>x \<notin> Field m\<close>
unfolding trans_def Field_def by blast
@@ -689,11 +689,11 @@
unfolding Un_Diff Field_def by (auto intro: wf_Un)
qed
ultimately have "Well_order ?m" by (simp add: order_on_defs)
---\<open>We show that the extension is above m\<close>
+\<comment>\<open>We show that the extension is above m\<close>
moreover have "(m, ?m) \<in> I" using \<open>Well_order ?m\<close> and \<open>Well_order m\<close> and \<open>x \<notin> Field m\<close>
by (fastforce simp: I_def init_seg_of_def Field_def)
ultimately
---\<open>This contradicts maximality of m:\<close>
+\<comment>\<open>This contradicts maximality of m:\<close>
have False using max and \<open>x \<notin> Field m\<close> unfolding Field_def by blast
}
hence "Field m = UNIV" by auto