--- a/src/HOL/Decision_Procs/Approximation.thy Thu Nov 05 10:39:49 2015 +0100
+++ b/src/HOL/Decision_Procs/Approximation.thy Thu Nov 05 10:39:59 2015 +0100
@@ -18,7 +18,7 @@
section "Horner Scheme"
-subsection \<open>Define auxiliary helper @{text horner} function\<close>
+subsection \<open>Define auxiliary helper \<open>horner\<close> function\<close>
primrec horner :: "(nat \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> real \<Rightarrow> real" where
"horner F G 0 i k x = 0" |
--- a/src/HOL/Decision_Procs/Commutative_Ring_Complete.thy Thu Nov 05 10:39:49 2015 +0100
+++ b/src/HOL/Decision_Procs/Commutative_Ring_Complete.thy Thu Nov 05 10:39:59 2015 +0100
@@ -101,7 +101,7 @@
by (cases x) auto
qed
-text \<open>mkPX conserves normalizedness (@{text "_cn"})\<close>
+text \<open>mkPX conserves normalizedness (\<open>_cn\<close>)\<close>
lemma mkPX_cn:
assumes "x \<noteq> 0"
and "isnorm P"
--- a/src/HOL/Decision_Procs/Cooper.thy Thu Nov 05 10:39:49 2015 +0100
+++ b/src/HOL/Decision_Procs/Cooper.thy Thu Nov 05 10:39:59 2015 +0100
@@ -18,7 +18,7 @@
datatype num = C int | Bound nat | CN nat int num | Neg num | Add num num| Sub num num
| Mul int num
-primrec num_size :: "num \<Rightarrow> nat" -- \<open>A size for num to make inductive proofs simpler\<close>
+primrec num_size :: "num \<Rightarrow> nat" \<comment> \<open>A size for num to make inductive proofs simpler\<close>
where
"num_size (C c) = 1"
| "num_size (Bound n) = 1"
@@ -44,7 +44,7 @@
| Closed nat | NClosed nat
-fun fmsize :: "fm \<Rightarrow> nat" -- \<open>A size for fm\<close>
+fun fmsize :: "fm \<Rightarrow> nat" \<comment> \<open>A size for fm\<close>
where
"fmsize (NOT p) = 1 + fmsize p"
| "fmsize (And p q) = 1 + fmsize p + fmsize q"
@@ -60,7 +60,7 @@
lemma fmsize_pos: "fmsize p > 0"
by (induct p rule: fmsize.induct) simp_all
-primrec Ifm :: "bool list \<Rightarrow> int list \<Rightarrow> fm \<Rightarrow> bool" -- \<open>Semantics of formulae (fm)\<close>
+primrec Ifm :: "bool list \<Rightarrow> int list \<Rightarrow> fm \<Rightarrow> bool" \<comment> \<open>Semantics of formulae (fm)\<close>
where
"Ifm bbs bs T \<longleftrightarrow> True"
| "Ifm bbs bs F \<longleftrightarrow> False"
@@ -113,7 +113,7 @@
by (induct p arbitrary: bs rule: prep.induct) auto
-fun qfree :: "fm \<Rightarrow> bool" -- \<open>Quantifier freeness\<close>
+fun qfree :: "fm \<Rightarrow> bool" \<comment> \<open>Quantifier freeness\<close>
where
"qfree (E p) \<longleftrightarrow> False"
| "qfree (A p) \<longleftrightarrow> False"
@@ -127,7 +127,7 @@
text \<open>Boundedness and substitution\<close>
-primrec numbound0 :: "num \<Rightarrow> bool" -- \<open>a num is INDEPENDENT of Bound 0\<close>
+primrec numbound0 :: "num \<Rightarrow> bool" \<comment> \<open>a num is INDEPENDENT of Bound 0\<close>
where
"numbound0 (C c) \<longleftrightarrow> True"
| "numbound0 (Bound n) \<longleftrightarrow> n > 0"
@@ -142,7 +142,7 @@
shows "Inum (b # bs) a = Inum (b' # bs) a"
using nb by (induct a rule: num.induct) (auto simp add: gr0_conv_Suc)
-primrec bound0 :: "fm \<Rightarrow> bool" -- \<open>A Formula is independent of Bound 0\<close>
+primrec bound0 :: "fm \<Rightarrow> bool" \<comment> \<open>A Formula is independent of Bound 0\<close>
where
"bound0 T \<longleftrightarrow> True"
| "bound0 F \<longleftrightarrow> True"
@@ -188,7 +188,7 @@
"numbound0 a \<Longrightarrow> Inum (b#bs) (numsubst0 a t) = Inum ((Inum (b'#bs) a)#bs) t"
by (induct t rule: numsubst0.induct) (auto simp: nth_Cons' numbound0_I[where b="b" and b'="b'"])
-primrec subst0:: "num \<Rightarrow> fm \<Rightarrow> fm" -- \<open>substitue a num into a formula for Bound 0\<close>
+primrec subst0:: "num \<Rightarrow> fm \<Rightarrow> fm" \<comment> \<open>substitue a num into a formula for Bound 0\<close>
where
"subst0 t T = T"
| "subst0 t F = F"
@@ -254,7 +254,7 @@
lemma decr_qf: "bound0 p \<Longrightarrow> qfree (decr p)"
by (induct p) simp_all
-fun isatom :: "fm \<Rightarrow> bool" -- \<open>test for atomicity\<close>
+fun isatom :: "fm \<Rightarrow> bool" \<comment> \<open>test for atomicity\<close>
where
"isatom T \<longleftrightarrow> True"
| "isatom F \<longleftrightarrow> True"
@@ -856,9 +856,9 @@
(auto simp add: not disj conj iff imp not_qf disj_qf conj_qf imp_qf iff_qf
simpfm simpfm_qf simp del: simpfm.simps)
-text \<open>Linearity for fm where Bound 0 ranges over @{text "\<int>"}\<close>
+text \<open>Linearity for fm where Bound 0 ranges over \<open>\<int>\<close>\<close>
-fun zsplit0 :: "num \<Rightarrow> int \<times> num" -- \<open>splits the bounded from the unbounded part\<close>
+fun zsplit0 :: "num \<Rightarrow> int \<times> num" \<comment> \<open>splits the bounded from the unbounded part\<close>
where
"zsplit0 (C c) = (0, C c)"
| "zsplit0 (Bound n) = (if n = 0 then (1, C 0) else (0, Bound n))"
@@ -989,7 +989,7 @@
by simp
qed
-consts iszlfm :: "fm \<Rightarrow> bool" -- \<open>Linearity test for fm\<close>
+consts iszlfm :: "fm \<Rightarrow> bool" \<comment> \<open>Linearity test for fm\<close>
recdef iszlfm "measure size"
"iszlfm (And p q) \<longleftrightarrow> iszlfm p \<and> iszlfm q"
"iszlfm (Or p q) \<longleftrightarrow> iszlfm p \<and> iszlfm q"
@@ -1006,7 +1006,7 @@
lemma zlin_qfree: "iszlfm p \<Longrightarrow> qfree p"
by (induct p rule: iszlfm.induct) auto
-consts zlfm :: "fm \<Rightarrow> fm" -- \<open>Linearity transformation for fm\<close>
+consts zlfm :: "fm \<Rightarrow> fm" \<comment> \<open>Linearity transformation for fm\<close>
recdef zlfm "measure fmsize"
"zlfm (And p q) = And (zlfm p) (zlfm q)"
"zlfm (Or p q) = Or (zlfm p) (zlfm q)"
@@ -1258,7 +1258,7 @@
qed
qed auto
-consts minusinf :: "fm \<Rightarrow> fm" -- \<open>Virtual substitution of @{text "-\<infinity>"}\<close>
+consts minusinf :: "fm \<Rightarrow> fm" \<comment> \<open>Virtual substitution of \<open>-\<infinity>\<close>\<close>
recdef minusinf "measure size"
"minusinf (And p q) = And (minusinf p) (minusinf q)"
"minusinf (Or p q) = Or (minusinf p) (minusinf q)"
@@ -1273,7 +1273,7 @@
lemma minusinf_qfree: "qfree p \<Longrightarrow> qfree (minusinf p)"
by (induct p rule: minusinf.induct) auto
-consts plusinf :: "fm \<Rightarrow> fm" -- \<open>Virtual substitution of @{text "+\<infinity>"}\<close>
+consts plusinf :: "fm \<Rightarrow> fm" \<comment> \<open>Virtual substitution of \<open>+\<infinity>\<close>\<close>
recdef plusinf "measure size"
"plusinf (And p q) = And (plusinf p) (plusinf q)"
"plusinf (Or p q) = Or (plusinf p) (plusinf q)"
@@ -1285,7 +1285,7 @@
"plusinf (Ge (CN 0 c e)) = T"
"plusinf p = p"
-consts \<delta> :: "fm \<Rightarrow> int" -- \<open>Compute @{text "lcm {d| N\<^sup>? Dvd c*x+t \<in> p}"}\<close>
+consts \<delta> :: "fm \<Rightarrow> int" \<comment> \<open>Compute \<open>lcm {d| N\<^sup>? Dvd c*x+t \<in> p}\<close>\<close>
recdef \<delta> "measure size"
"\<delta> (And p q) = lcm (\<delta> p) (\<delta> q)"
"\<delta> (Or p q) = lcm (\<delta> p) (\<delta> q)"
@@ -1293,7 +1293,7 @@
"\<delta> (NDvd i (CN 0 c e)) = i"
"\<delta> p = 1"
-consts d_\<delta> :: "fm \<Rightarrow> int \<Rightarrow> bool" -- \<open>check if a given l divides all the ds above\<close>
+consts d_\<delta> :: "fm \<Rightarrow> int \<Rightarrow> bool" \<comment> \<open>check if a given l divides all the ds above\<close>
recdef d_\<delta> "measure size"
"d_\<delta> (And p q) = (\<lambda>d. d_\<delta> p d \<and> d_\<delta> q d)"
"d_\<delta> (Or p q) = (\<lambda>d. d_\<delta> p d \<and> d_\<delta> q d)"
@@ -1354,7 +1354,7 @@
qed simp_all
-consts a_\<beta> :: "fm \<Rightarrow> int \<Rightarrow> fm" -- \<open>adjust the coefficients of a formula\<close>
+consts a_\<beta> :: "fm \<Rightarrow> int \<Rightarrow> fm" \<comment> \<open>adjust the coefficients of a formula\<close>
recdef a_\<beta> "measure size"
"a_\<beta> (And p q) = (\<lambda>k. And (a_\<beta> p k) (a_\<beta> q k))"
"a_\<beta> (Or p q) = (\<lambda>k. Or (a_\<beta> p k) (a_\<beta> q k))"
@@ -1368,7 +1368,7 @@
"a_\<beta> (NDvd i (CN 0 c e))=(\<lambda>k. NDvd ((k div c)*i) (CN 0 1 (Mul (k div c) e)))"
"a_\<beta> p = (\<lambda>k. p)"
-consts d_\<beta> :: "fm \<Rightarrow> int \<Rightarrow> bool" -- \<open>test if all coeffs c of c divide a given l\<close>
+consts d_\<beta> :: "fm \<Rightarrow> int \<Rightarrow> bool" \<comment> \<open>test if all coeffs c of c divide a given l\<close>
recdef d_\<beta> "measure size"
"d_\<beta> (And p q) = (\<lambda>k. (d_\<beta> p k) \<and> (d_\<beta> q k))"
"d_\<beta> (Or p q) = (\<lambda>k. (d_\<beta> p k) \<and> (d_\<beta> q k))"
@@ -1382,7 +1382,7 @@
"d_\<beta> (NDvd i (CN 0 c e))=(\<lambda>k. c dvd k)"
"d_\<beta> p = (\<lambda>k. True)"
-consts \<zeta> :: "fm \<Rightarrow> int" -- \<open>computes the lcm of all coefficients of x\<close>
+consts \<zeta> :: "fm \<Rightarrow> int" \<comment> \<open>computes the lcm of all coefficients of x\<close>
recdef \<zeta> "measure size"
"\<zeta> (And p q) = lcm (\<zeta> p) (\<zeta> q)"
"\<zeta> (Or p q) = lcm (\<zeta> p) (\<zeta> q)"
@@ -1434,7 +1434,7 @@
"mirror (NDvd i (CN 0 c e)) = NDvd i (CN 0 c (Neg e))"
"mirror p = p"
-text \<open>Lemmas for the correctness of @{text "\<sigma>_\<rho>"}\<close>
+text \<open>Lemmas for the correctness of \<open>\<sigma>_\<rho>\<close>\<close>
lemma dvd1_eq1:
fixes x :: int
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Thu Nov 05 10:39:49 2015 +0100
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Thu Nov 05 10:39:59 2015 +0100
@@ -32,7 +32,7 @@
lemma gather_start [no_atp]: "(\<exists>x. P x) \<equiv> (\<exists>x. (\<forall>y \<in> {}. y < x) \<and> (\<forall>y\<in> {}. x < y) \<and> P x)"
by simp
-text\<open>Theorems for @{text "\<exists>z. \<forall>x. x < z \<longrightarrow> (P x \<longleftrightarrow> P\<^sub>-\<^sub>\<infinity>)"}\<close>
+text\<open>Theorems for \<open>\<exists>z. \<forall>x. x < z \<longrightarrow> (P x \<longleftrightarrow> P\<^sub>-\<^sub>\<infinity>)\<close>\<close>
lemma minf_lt[no_atp]: "\<exists>z . \<forall>x. x < z \<longrightarrow> (x < t \<longleftrightarrow> True)" by auto
lemma minf_gt[no_atp]: "\<exists>z . \<forall>x. x < z \<longrightarrow> (t < x \<longleftrightarrow> False)"
by (simp add: not_less) (rule exI[where x="t"], auto simp add: less_le)
@@ -44,7 +44,7 @@
lemma minf_neq[no_atp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (x \<noteq> t \<longleftrightarrow> True)" by auto
lemma minf_P[no_atp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (P \<longleftrightarrow> P)" by blast
-text\<open>Theorems for @{text "\<exists>z. \<forall>x. x < z \<longrightarrow> (P x \<longleftrightarrow> P\<^sub>+\<^sub>\<infinity>)"}\<close>
+text\<open>Theorems for \<open>\<exists>z. \<forall>x. x < z \<longrightarrow> (P x \<longleftrightarrow> P\<^sub>+\<^sub>\<infinity>)\<close>\<close>
lemma pinf_gt[no_atp]: "\<exists>z. \<forall>x. z < x \<longrightarrow> (t < x \<longleftrightarrow> True)" by auto
lemma pinf_lt[no_atp]: "\<exists>z. \<forall>x. z < x \<longrightarrow> (x < t \<longleftrightarrow> False)"
by (simp add: not_less) (rule exI[where x="t"], auto simp add: less_le)
@@ -452,7 +452,7 @@
lemma ge_ex[no_atp]: "\<exists>y. x \<sqsubseteq> y"
using gt_ex by auto
-text \<open>Theorems for @{text "\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> (P x \<longleftrightarrow> P\<^sub>+\<^sub>\<infinity>)"}\<close>
+text \<open>Theorems for \<open>\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> (P x \<longleftrightarrow> P\<^sub>+\<^sub>\<infinity>)\<close>\<close>
lemma pinf_conj[no_atp]:
assumes ex1: "\<exists>z1. \<forall>x. z1 \<sqsubset> x \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
and ex2: "\<exists>z2. \<forall>x. z2 \<sqsubset> x \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
@@ -516,7 +516,7 @@
using lt_ex by auto
-text \<open>Theorems for @{text "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (P x \<longleftrightarrow> P\<^sub>-\<^sub>\<infinity>)"}\<close>
+text \<open>Theorems for \<open>\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (P x \<longleftrightarrow> P\<^sub>-\<^sub>\<infinity>)\<close>\<close>
lemma minf_conj[no_atp]:
assumes ex1: "\<exists>z1. \<forall>x. x \<sqsubset> z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
and ex2: "\<exists>z2. \<forall>x. x \<sqsubset> z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
--- a/src/HOL/Decision_Procs/Ferrack.thy Thu Nov 05 10:39:49 2015 +0100
+++ b/src/HOL/Decision_Procs/Ferrack.thy Thu Nov 05 10:39:59 2015 +0100
@@ -7,7 +7,7 @@
"~~/src/HOL/Library/Code_Target_Numeral" "~~/src/HOL/Library/Old_Recdef"
begin
-section \<open>Quantifier elimination for @{text "\<real> (0, 1, +, <)"}\<close>
+section \<open>Quantifier elimination for \<open>\<real> (0, 1, +, <)\<close>\<close>
(*********************************************************************************)
(**** SHADOW SYNTAX AND SEMANTICS ****)
--- a/src/HOL/Decision_Procs/MIR.thy Thu Nov 05 10:39:49 2015 +0100
+++ b/src/HOL/Decision_Procs/MIR.thy Thu Nov 05 10:39:59 2015 +0100
@@ -7,7 +7,7 @@
"~~/src/HOL/Library/Code_Target_Numeral" "~~/src/HOL/Library/Old_Recdef"
begin
-section \<open>Quantifier elimination for @{text "\<real> (0, 1, +, floor, <)"}\<close>
+section \<open>Quantifier elimination for \<open>\<real> (0, 1, +, floor, <)\<close>\<close>
declare real_of_int_floor_cancel [simp del]
@@ -1450,8 +1450,8 @@
by (induct p rule: qelim.induct) (auto simp del: simpfm.simps)
-text \<open>The @{text "\<int>"} Part\<close>
-text\<open>Linearity for fm where Bound 0 ranges over @{text "\<int>"}\<close>
+text \<open>The \<open>\<int>\<close> Part\<close>
+text\<open>Linearity for fm where Bound 0 ranges over \<open>\<int>\<close>\<close>
function zsplit0 :: "num \<Rightarrow> int \<times> num" (* splits the bounded from the unbounded part*) where
"zsplit0 (C c) = (0,C c)"
@@ -1955,10 +1955,10 @@
ultimately show ?case by blast
qed auto
-text\<open>plusinf : Virtual substitution of @{text "+\<infinity>"}
- minusinf: Virtual substitution of @{text "-\<infinity>"}
- @{text "\<delta>"} Compute lcm @{text "d| Dvd d c*x+t \<in> p"}
- @{text "d_\<delta>"} checks if a given l divides all the ds above\<close>
+text\<open>plusinf : Virtual substitution of \<open>+\<infinity>\<close>
+ minusinf: Virtual substitution of \<open>-\<infinity>\<close>
+ \<open>\<delta>\<close> Compute lcm \<open>d| Dvd d c*x+t \<in> p\<close>
+ \<open>d_\<delta>\<close> checks if a given l divides all the ds above\<close>
fun minusinf:: "fm \<Rightarrow> fm" where
"minusinf (And p q) = conj (minusinf p) (minusinf q)"
@@ -3294,9 +3294,9 @@
using lp
by (induct p rule: mirror.induct) (simp_all add: split_def image_Un)
-text \<open>The @{text "\<real>"} part\<close>
-
-text\<open>Linearity for fm where Bound 0 ranges over @{text "\<real>"}\<close>
+text \<open>The \<open>\<real>\<close> part\<close>
+
+text\<open>Linearity for fm where Bound 0 ranges over \<open>\<real>\<close>\<close>
consts
isrlfm :: "fm \<Rightarrow> bool" (* Linearity test for fm *)
recdef isrlfm "measure size"
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Thu Nov 05 10:39:49 2015 +0100
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Thu Nov 05 10:39:59 2015 +0100
@@ -60,7 +60,7 @@
| "tmboundslt n (Sub a b) = (tmboundslt n a \<and> tmboundslt n b)"
| "tmboundslt n (Mul i a) = tmboundslt n a"
-primrec tmbound0 :: "tm \<Rightarrow> bool" -- \<open>a tm is INDEPENDENT of Bound 0\<close>
+primrec tmbound0 :: "tm \<Rightarrow> bool" \<comment> \<open>a tm is INDEPENDENT of Bound 0\<close>
where
"tmbound0 (CP c) = True"
| "tmbound0 (Bound n) = (n>0)"
@@ -76,7 +76,7 @@
using nb
by (induct a rule: tm.induct) auto
-primrec tmbound :: "nat \<Rightarrow> tm \<Rightarrow> bool" -- \<open>a tm is INDEPENDENT of Bound n\<close>
+primrec tmbound :: "nat \<Rightarrow> tm \<Rightarrow> bool" \<comment> \<open>a tm is INDEPENDENT of Bound n\<close>
where
"tmbound n (CP c) = True"
| "tmbound n (Bound m) = (n \<noteq> m)"
@@ -626,7 +626,7 @@
| "boundslt n (E p) = boundslt (Suc n) p"
| "boundslt n (A p) = boundslt (Suc n) p"
-fun bound0:: "fm \<Rightarrow> bool" -- \<open>a Formula is independent of Bound 0\<close>
+fun bound0:: "fm \<Rightarrow> bool" \<comment> \<open>a Formula is independent of Bound 0\<close>
where
"bound0 T = True"
| "bound0 F = True"
@@ -647,7 +647,7 @@
using bp tmbound0_I[where b="b" and bs="bs" and b'="b'"]
by (induct p rule: bound0.induct) auto
-primrec bound:: "nat \<Rightarrow> fm \<Rightarrow> bool" -- \<open>a Formula is independent of Bound n\<close>
+primrec bound:: "nat \<Rightarrow> fm \<Rightarrow> bool" \<comment> \<open>a Formula is independent of Bound n\<close>
where
"bound m T = True"
| "bound m F = True"
@@ -897,7 +897,7 @@
lemma decr0_qf: "bound0 p \<Longrightarrow> qfree (decr0 p)"
by (induct p) simp_all
-fun isatom :: "fm \<Rightarrow> bool" -- \<open>test for atomicity\<close>
+fun isatom :: "fm \<Rightarrow> bool" \<comment> \<open>test for atomicity\<close>
where
"isatom T = True"
| "isatom F = True"
@@ -1643,7 +1643,7 @@
subsection \<open>Core Procedure\<close>
-fun minusinf:: "fm \<Rightarrow> fm" -- \<open>Virtual substitution of -\<infinity>\<close>
+fun minusinf:: "fm \<Rightarrow> fm" \<comment> \<open>Virtual substitution of -\<infinity>\<close>
where
"minusinf (And p q) = conj (minusinf p) (minusinf q)"
| "minusinf (Or p q) = disj (minusinf p) (minusinf q)"
@@ -1653,7 +1653,7 @@
| "minusinf (Le (CNP 0 c e)) = disj (conj (eq (CP c)) (le e)) (lt (CP (~\<^sub>p c)))"
| "minusinf p = p"
-fun plusinf:: "fm \<Rightarrow> fm" -- \<open>Virtual substitution of +\<infinity>\<close>
+fun plusinf:: "fm \<Rightarrow> fm" \<comment> \<open>Virtual substitution of +\<infinity>\<close>
where
"plusinf (And p q) = conj (plusinf p) (plusinf q)"
| "plusinf (Or p q) = disj (plusinf p) (plusinf q)"
--- a/src/HOL/Decision_Procs/Polynomial_List.thy Thu Nov 05 10:39:49 2015 +0100
+++ b/src/HOL/Decision_Procs/Polynomial_List.thy Thu Nov 05 10:39:59 2015 +0100
@@ -81,15 +81,15 @@
obtains q where "poly p2 = poly (p1 *** q)"
using assms by (auto simp add: divides_def)
--- \<open>order of a polynomial\<close>
+\<comment> \<open>order of a polynomial\<close>
definition (in ring_1) order :: "'a \<Rightarrow> 'a list \<Rightarrow> nat"
where "order a p = (SOME n. ([-a, 1] %^ n) divides p \<and> \<not> (([-a, 1] %^ (Suc n)) divides p))"
--- \<open>degree of a polynomial\<close>
+\<comment> \<open>degree of a polynomial\<close>
definition (in semiring_0) degree :: "'a list \<Rightarrow> nat"
where "degree p = length (pnormalize p) - 1"
--- \<open>squarefree polynomials --- NB with respect to real roots only\<close>
+\<comment> \<open>squarefree polynomials --- NB with respect to real roots only\<close>
definition (in ring_1) rsquarefree :: "'a list \<Rightarrow> bool"
where "rsquarefree p \<longleftrightarrow> poly p \<noteq> poly [] \<and> (\<forall>a. order a p = 0 \<or> order a p = 1)"
--- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Thu Nov 05 10:39:49 2015 +0100
+++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Thu Nov 05 10:39:59 2015 +0100
@@ -30,7 +30,7 @@
| "polysize (Pw p n) = 1 + polysize p"
| "polysize (CN c n p) = 4 + polysize c + polysize p"
-primrec polybound0:: "poly \<Rightarrow> bool" -- \<open>a poly is INDEPENDENT of Bound 0\<close>
+primrec polybound0:: "poly \<Rightarrow> bool" \<comment> \<open>a poly is INDEPENDENT of Bound 0\<close>
where
"polybound0 (C c) \<longleftrightarrow> True"
| "polybound0 (Bound n) \<longleftrightarrow> n > 0"
@@ -41,7 +41,7 @@
| "polybound0 (Pw p n) \<longleftrightarrow> polybound0 p"
| "polybound0 (CN c n p) \<longleftrightarrow> n \<noteq> 0 \<and> polybound0 c \<and> polybound0 p"
-primrec polysubst0:: "poly \<Rightarrow> poly \<Rightarrow> poly" -- \<open>substitute a poly into a poly for Bound 0\<close>
+primrec polysubst0:: "poly \<Rightarrow> poly \<Rightarrow> poly" \<comment> \<open>substitute a poly into a poly for Bound 0\<close>
where
"polysubst0 t (C c) = C c"
| "polysubst0 t (Bound n) = (if n = 0 then t else Bound n)"
--- a/src/HOL/Decision_Procs/ex/Approximation_Quickcheck_Ex.thy Thu Nov 05 10:39:49 2015 +0100
+++ b/src/HOL/Decision_Procs/ex/Approximation_Quickcheck_Ex.thy Thu Nov 05 10:39:59 2015 +0100
@@ -31,7 +31,7 @@
shows "x > 1 \<Longrightarrow> x \<le> 2 ^ 20 * log 2 x + 1 \<and> (sin x)\<^sup>2 + (cos x)\<^sup>2 = 1"
using [[quickcheck_approximation_custom_seed = 1]]
using [[quickcheck_approximation_epsilon = 0.00000001]]
- --\<open>avoids spurious counterexamples in approximate computation of @{term "(sin x)\<^sup>2 + (cos x)\<^sup>2"}
+ \<comment>\<open>avoids spurious counterexamples in approximate computation of @{term "(sin x)\<^sup>2 + (cos x)\<^sup>2"}
and therefore avoids expensive failing attempts for certification\<close>
quickcheck[approximation, expect=counterexample, size=20]
oops