isabelle update_cartouches -c -t;
authorwenzelm
Thu Nov 05 10:39:59 2015 +0100 (2015-11-05)
changeset 615865197a2ecb658
parent 61585 a9599d3d7610
child 61587 c3974cd2d381
isabelle update_cartouches -c -t;
src/HOL/Decision_Procs/Approximation.thy
src/HOL/Decision_Procs/Commutative_Ring_Complete.thy
src/HOL/Decision_Procs/Cooper.thy
src/HOL/Decision_Procs/Dense_Linear_Order.thy
src/HOL/Decision_Procs/Ferrack.thy
src/HOL/Decision_Procs/MIR.thy
src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
src/HOL/Decision_Procs/Polynomial_List.thy
src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
src/HOL/Decision_Procs/ex/Approximation_Quickcheck_Ex.thy
     1.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Thu Nov 05 10:39:49 2015 +0100
     1.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Thu Nov 05 10:39:59 2015 +0100
     1.3 @@ -18,7 +18,7 @@
     1.4  
     1.5  section "Horner Scheme"
     1.6  
     1.7 -subsection \<open>Define auxiliary helper @{text horner} function\<close>
     1.8 +subsection \<open>Define auxiliary helper \<open>horner\<close> function\<close>
     1.9  
    1.10  primrec horner :: "(nat \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> real \<Rightarrow> real" where
    1.11  "horner F G 0 i k x       = 0" |
     2.1 --- a/src/HOL/Decision_Procs/Commutative_Ring_Complete.thy	Thu Nov 05 10:39:49 2015 +0100
     2.2 +++ b/src/HOL/Decision_Procs/Commutative_Ring_Complete.thy	Thu Nov 05 10:39:59 2015 +0100
     2.3 @@ -101,7 +101,7 @@
     2.4      by (cases x) auto
     2.5  qed
     2.6  
     2.7 -text \<open>mkPX conserves normalizedness (@{text "_cn"})\<close>
     2.8 +text \<open>mkPX conserves normalizedness (\<open>_cn\<close>)\<close>
     2.9  lemma mkPX_cn:
    2.10    assumes "x \<noteq> 0"
    2.11      and "isnorm P"
     3.1 --- a/src/HOL/Decision_Procs/Cooper.thy	Thu Nov 05 10:39:49 2015 +0100
     3.2 +++ b/src/HOL/Decision_Procs/Cooper.thy	Thu Nov 05 10:39:59 2015 +0100
     3.3 @@ -18,7 +18,7 @@
     3.4  datatype num = C int | Bound nat | CN nat int num | Neg num | Add num num| Sub num num
     3.5    | Mul int num
     3.6  
     3.7 -primrec num_size :: "num \<Rightarrow> nat" -- \<open>A size for num to make inductive proofs simpler\<close>
     3.8 +primrec num_size :: "num \<Rightarrow> nat" \<comment> \<open>A size for num to make inductive proofs simpler\<close>
     3.9  where
    3.10    "num_size (C c) = 1"
    3.11  | "num_size (Bound n) = 1"
    3.12 @@ -44,7 +44,7 @@
    3.13    | Closed nat | NClosed nat
    3.14  
    3.15  
    3.16 -fun fmsize :: "fm \<Rightarrow> nat"  -- \<open>A size for fm\<close>
    3.17 +fun fmsize :: "fm \<Rightarrow> nat"  \<comment> \<open>A size for fm\<close>
    3.18  where
    3.19    "fmsize (NOT p) = 1 + fmsize p"
    3.20  | "fmsize (And p q) = 1 + fmsize p + fmsize q"
    3.21 @@ -60,7 +60,7 @@
    3.22  lemma fmsize_pos: "fmsize p > 0"
    3.23    by (induct p rule: fmsize.induct) simp_all
    3.24  
    3.25 -primrec Ifm :: "bool list \<Rightarrow> int list \<Rightarrow> fm \<Rightarrow> bool"  -- \<open>Semantics of formulae (fm)\<close>
    3.26 +primrec Ifm :: "bool list \<Rightarrow> int list \<Rightarrow> fm \<Rightarrow> bool"  \<comment> \<open>Semantics of formulae (fm)\<close>
    3.27  where
    3.28    "Ifm bbs bs T \<longleftrightarrow> True"
    3.29  | "Ifm bbs bs F \<longleftrightarrow> False"
    3.30 @@ -113,7 +113,7 @@
    3.31    by (induct p arbitrary: bs rule: prep.induct) auto
    3.32  
    3.33  
    3.34 -fun qfree :: "fm \<Rightarrow> bool"  -- \<open>Quantifier freeness\<close>
    3.35 +fun qfree :: "fm \<Rightarrow> bool"  \<comment> \<open>Quantifier freeness\<close>
    3.36  where
    3.37    "qfree (E p) \<longleftrightarrow> False"
    3.38  | "qfree (A p) \<longleftrightarrow> False"
    3.39 @@ -127,7 +127,7 @@
    3.40  
    3.41  text \<open>Boundedness and substitution\<close>
    3.42  
    3.43 -primrec numbound0 :: "num \<Rightarrow> bool"  -- \<open>a num is INDEPENDENT of Bound 0\<close>
    3.44 +primrec numbound0 :: "num \<Rightarrow> bool"  \<comment> \<open>a num is INDEPENDENT of Bound 0\<close>
    3.45  where
    3.46    "numbound0 (C c) \<longleftrightarrow> True"
    3.47  | "numbound0 (Bound n) \<longleftrightarrow> n > 0"
    3.48 @@ -142,7 +142,7 @@
    3.49    shows "Inum (b # bs) a = Inum (b' # bs) a"
    3.50    using nb by (induct a rule: num.induct) (auto simp add: gr0_conv_Suc)
    3.51  
    3.52 -primrec bound0 :: "fm \<Rightarrow> bool" -- \<open>A Formula is independent of Bound 0\<close>
    3.53 +primrec bound0 :: "fm \<Rightarrow> bool" \<comment> \<open>A Formula is independent of Bound 0\<close>
    3.54  where
    3.55    "bound0 T \<longleftrightarrow> True"
    3.56  | "bound0 F \<longleftrightarrow> True"
    3.57 @@ -188,7 +188,7 @@
    3.58    "numbound0 a \<Longrightarrow> Inum (b#bs) (numsubst0 a t) = Inum ((Inum (b'#bs) a)#bs) t"
    3.59    by (induct t rule: numsubst0.induct) (auto simp: nth_Cons' numbound0_I[where b="b" and b'="b'"])
    3.60  
    3.61 -primrec subst0:: "num \<Rightarrow> fm \<Rightarrow> fm"  -- \<open>substitue a num into a formula for Bound 0\<close>
    3.62 +primrec subst0:: "num \<Rightarrow> fm \<Rightarrow> fm"  \<comment> \<open>substitue a num into a formula for Bound 0\<close>
    3.63  where
    3.64    "subst0 t T = T"
    3.65  | "subst0 t F = F"
    3.66 @@ -254,7 +254,7 @@
    3.67  lemma decr_qf: "bound0 p \<Longrightarrow> qfree (decr p)"
    3.68    by (induct p) simp_all
    3.69  
    3.70 -fun isatom :: "fm \<Rightarrow> bool"  -- \<open>test for atomicity\<close>
    3.71 +fun isatom :: "fm \<Rightarrow> bool"  \<comment> \<open>test for atomicity\<close>
    3.72  where
    3.73    "isatom T \<longleftrightarrow> True"
    3.74  | "isatom F \<longleftrightarrow> True"
    3.75 @@ -856,9 +856,9 @@
    3.76      (auto simp add: not disj conj iff imp not_qf disj_qf conj_qf imp_qf iff_qf
    3.77        simpfm simpfm_qf simp del: simpfm.simps)
    3.78  
    3.79 -text \<open>Linearity for fm where Bound 0 ranges over @{text "\<int>"}\<close>
    3.80 +text \<open>Linearity for fm where Bound 0 ranges over \<open>\<int>\<close>\<close>
    3.81  
    3.82 -fun zsplit0 :: "num \<Rightarrow> int \<times> num"  -- \<open>splits the bounded from the unbounded part\<close>
    3.83 +fun zsplit0 :: "num \<Rightarrow> int \<times> num"  \<comment> \<open>splits the bounded from the unbounded part\<close>
    3.84  where
    3.85    "zsplit0 (C c) = (0, C c)"
    3.86  | "zsplit0 (Bound n) = (if n = 0 then (1, C 0) else (0, Bound n))"
    3.87 @@ -989,7 +989,7 @@
    3.88      by simp
    3.89  qed
    3.90  
    3.91 -consts iszlfm :: "fm \<Rightarrow> bool"  -- \<open>Linearity test for fm\<close>
    3.92 +consts iszlfm :: "fm \<Rightarrow> bool"  \<comment> \<open>Linearity test for fm\<close>
    3.93  recdef iszlfm "measure size"
    3.94    "iszlfm (And p q) \<longleftrightarrow> iszlfm p \<and> iszlfm q"
    3.95    "iszlfm (Or p q) \<longleftrightarrow> iszlfm p \<and> iszlfm q"
    3.96 @@ -1006,7 +1006,7 @@
    3.97  lemma zlin_qfree: "iszlfm p \<Longrightarrow> qfree p"
    3.98    by (induct p rule: iszlfm.induct) auto
    3.99  
   3.100 -consts zlfm :: "fm \<Rightarrow> fm"  -- \<open>Linearity transformation for fm\<close>
   3.101 +consts zlfm :: "fm \<Rightarrow> fm"  \<comment> \<open>Linearity transformation for fm\<close>
   3.102  recdef zlfm "measure fmsize"
   3.103    "zlfm (And p q) = And (zlfm p) (zlfm q)"
   3.104    "zlfm (Or p q) = Or (zlfm p) (zlfm q)"
   3.105 @@ -1258,7 +1258,7 @@
   3.106    qed
   3.107  qed auto
   3.108  
   3.109 -consts minusinf :: "fm \<Rightarrow> fm" -- \<open>Virtual substitution of @{text "-\<infinity>"}\<close>
   3.110 +consts minusinf :: "fm \<Rightarrow> fm" \<comment> \<open>Virtual substitution of \<open>-\<infinity>\<close>\<close>
   3.111  recdef minusinf "measure size"
   3.112    "minusinf (And p q) = And (minusinf p) (minusinf q)"
   3.113    "minusinf (Or p q) = Or (minusinf p) (minusinf q)"
   3.114 @@ -1273,7 +1273,7 @@
   3.115  lemma minusinf_qfree: "qfree p \<Longrightarrow> qfree (minusinf p)"
   3.116    by (induct p rule: minusinf.induct) auto
   3.117  
   3.118 -consts plusinf :: "fm \<Rightarrow> fm"  -- \<open>Virtual substitution of @{text "+\<infinity>"}\<close>
   3.119 +consts plusinf :: "fm \<Rightarrow> fm"  \<comment> \<open>Virtual substitution of \<open>+\<infinity>\<close>\<close>
   3.120  recdef plusinf "measure size"
   3.121    "plusinf (And p q) = And (plusinf p) (plusinf q)"
   3.122    "plusinf (Or p q) = Or (plusinf p) (plusinf q)"
   3.123 @@ -1285,7 +1285,7 @@
   3.124    "plusinf (Ge  (CN 0 c e)) = T"
   3.125    "plusinf p = p"
   3.126  
   3.127 -consts \<delta> :: "fm \<Rightarrow> int"  -- \<open>Compute @{text "lcm {d| N\<^sup>? Dvd c*x+t \<in> p}"}\<close>
   3.128 +consts \<delta> :: "fm \<Rightarrow> int"  \<comment> \<open>Compute \<open>lcm {d| N\<^sup>? Dvd c*x+t \<in> p}\<close>\<close>
   3.129  recdef \<delta> "measure size"
   3.130    "\<delta> (And p q) = lcm (\<delta> p) (\<delta> q)"
   3.131    "\<delta> (Or p q) = lcm (\<delta> p) (\<delta> q)"
   3.132 @@ -1293,7 +1293,7 @@
   3.133    "\<delta> (NDvd i (CN 0 c e)) = i"
   3.134    "\<delta> p = 1"
   3.135  
   3.136 -consts d_\<delta> :: "fm \<Rightarrow> int \<Rightarrow> bool"  -- \<open>check if a given l divides all the ds above\<close>
   3.137 +consts d_\<delta> :: "fm \<Rightarrow> int \<Rightarrow> bool"  \<comment> \<open>check if a given l divides all the ds above\<close>
   3.138  recdef d_\<delta> "measure size"
   3.139    "d_\<delta> (And p q) = (\<lambda>d. d_\<delta> p d \<and> d_\<delta> q d)"
   3.140    "d_\<delta> (Or p q) = (\<lambda>d. d_\<delta> p d \<and> d_\<delta> q d)"
   3.141 @@ -1354,7 +1354,7 @@
   3.142  qed simp_all
   3.143  
   3.144  
   3.145 -consts a_\<beta> :: "fm \<Rightarrow> int \<Rightarrow> fm"  -- \<open>adjust the coefficients of a formula\<close>
   3.146 +consts a_\<beta> :: "fm \<Rightarrow> int \<Rightarrow> fm"  \<comment> \<open>adjust the coefficients of a formula\<close>
   3.147  recdef a_\<beta> "measure size"
   3.148    "a_\<beta> (And p q) = (\<lambda>k. And (a_\<beta> p k) (a_\<beta> q k))"
   3.149    "a_\<beta> (Or p q) = (\<lambda>k. Or (a_\<beta> p k) (a_\<beta> q k))"
   3.150 @@ -1368,7 +1368,7 @@
   3.151    "a_\<beta> (NDvd i (CN 0 c e))=(\<lambda>k. NDvd ((k div c)*i) (CN 0 1 (Mul (k div c) e)))"
   3.152    "a_\<beta> p = (\<lambda>k. p)"
   3.153  
   3.154 -consts d_\<beta> :: "fm \<Rightarrow> int \<Rightarrow> bool"  -- \<open>test if all coeffs c of c divide a given l\<close>
   3.155 +consts d_\<beta> :: "fm \<Rightarrow> int \<Rightarrow> bool"  \<comment> \<open>test if all coeffs c of c divide a given l\<close>
   3.156  recdef d_\<beta> "measure size"
   3.157    "d_\<beta> (And p q) = (\<lambda>k. (d_\<beta> p k) \<and> (d_\<beta> q k))"
   3.158    "d_\<beta> (Or p q) = (\<lambda>k. (d_\<beta> p k) \<and> (d_\<beta> q k))"
   3.159 @@ -1382,7 +1382,7 @@
   3.160    "d_\<beta> (NDvd i (CN 0 c e))=(\<lambda>k. c dvd k)"
   3.161    "d_\<beta> p = (\<lambda>k. True)"
   3.162  
   3.163 -consts \<zeta> :: "fm \<Rightarrow> int"  -- \<open>computes the lcm of all coefficients of x\<close>
   3.164 +consts \<zeta> :: "fm \<Rightarrow> int"  \<comment> \<open>computes the lcm of all coefficients of x\<close>
   3.165  recdef \<zeta> "measure size"
   3.166    "\<zeta> (And p q) = lcm (\<zeta> p) (\<zeta> q)"
   3.167    "\<zeta> (Or p q) = lcm (\<zeta> p) (\<zeta> q)"
   3.168 @@ -1434,7 +1434,7 @@
   3.169    "mirror (NDvd i (CN 0 c e)) = NDvd i (CN 0 c (Neg e))"
   3.170    "mirror p = p"
   3.171  
   3.172 -text \<open>Lemmas for the correctness of @{text "\<sigma>_\<rho>"}\<close>
   3.173 +text \<open>Lemmas for the correctness of \<open>\<sigma>_\<rho>\<close>\<close>
   3.174  
   3.175  lemma dvd1_eq1:
   3.176    fixes x :: int
     4.1 --- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Thu Nov 05 10:39:49 2015 +0100
     4.2 +++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Thu Nov 05 10:39:59 2015 +0100
     4.3 @@ -32,7 +32,7 @@
     4.4  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)"
     4.5    by simp
     4.6  
     4.7 -text\<open>Theorems for @{text "\<exists>z. \<forall>x. x < z \<longrightarrow> (P x \<longleftrightarrow> P\<^sub>-\<^sub>\<infinity>)"}\<close>
     4.8 +text\<open>Theorems for \<open>\<exists>z. \<forall>x. x < z \<longrightarrow> (P x \<longleftrightarrow> P\<^sub>-\<^sub>\<infinity>)\<close>\<close>
     4.9  lemma minf_lt[no_atp]:  "\<exists>z . \<forall>x. x < z \<longrightarrow> (x < t \<longleftrightarrow> True)" by auto
    4.10  lemma minf_gt[no_atp]: "\<exists>z . \<forall>x. x < z \<longrightarrow>  (t < x \<longleftrightarrow>  False)"
    4.11    by (simp add: not_less) (rule exI[where x="t"], auto simp add: less_le)
    4.12 @@ -44,7 +44,7 @@
    4.13  lemma minf_neq[no_atp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (x \<noteq> t \<longleftrightarrow> True)" by auto
    4.14  lemma minf_P[no_atp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (P \<longleftrightarrow> P)" by blast
    4.15  
    4.16 -text\<open>Theorems for @{text "\<exists>z. \<forall>x. x < z \<longrightarrow> (P x \<longleftrightarrow> P\<^sub>+\<^sub>\<infinity>)"}\<close>
    4.17 +text\<open>Theorems for \<open>\<exists>z. \<forall>x. x < z \<longrightarrow> (P x \<longleftrightarrow> P\<^sub>+\<^sub>\<infinity>)\<close>\<close>
    4.18  lemma pinf_gt[no_atp]:  "\<exists>z. \<forall>x. z < x \<longrightarrow> (t < x \<longleftrightarrow> True)" by auto
    4.19  lemma pinf_lt[no_atp]: "\<exists>z. \<forall>x. z < x \<longrightarrow>  (x < t \<longleftrightarrow>  False)"
    4.20    by (simp add: not_less) (rule exI[where x="t"], auto simp add: less_le)
    4.21 @@ -452,7 +452,7 @@
    4.22  lemma ge_ex[no_atp]: "\<exists>y. x \<sqsubseteq> y"
    4.23    using gt_ex by auto
    4.24  
    4.25 -text \<open>Theorems for @{text "\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> (P x \<longleftrightarrow> P\<^sub>+\<^sub>\<infinity>)"}\<close>
    4.26 +text \<open>Theorems for \<open>\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> (P x \<longleftrightarrow> P\<^sub>+\<^sub>\<infinity>)\<close>\<close>
    4.27  lemma pinf_conj[no_atp]:
    4.28    assumes ex1: "\<exists>z1. \<forall>x. z1 \<sqsubset> x \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
    4.29      and ex2: "\<exists>z2. \<forall>x. z2 \<sqsubset> x \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
    4.30 @@ -516,7 +516,7 @@
    4.31    using lt_ex by auto
    4.32  
    4.33  
    4.34 -text \<open>Theorems for @{text "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (P x \<longleftrightarrow> P\<^sub>-\<^sub>\<infinity>)"}\<close>
    4.35 +text \<open>Theorems for \<open>\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (P x \<longleftrightarrow> P\<^sub>-\<^sub>\<infinity>)\<close>\<close>
    4.36  lemma minf_conj[no_atp]:
    4.37    assumes ex1: "\<exists>z1. \<forall>x. x \<sqsubset> z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
    4.38      and ex2: "\<exists>z2. \<forall>x. x \<sqsubset> z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
     5.1 --- a/src/HOL/Decision_Procs/Ferrack.thy	Thu Nov 05 10:39:49 2015 +0100
     5.2 +++ b/src/HOL/Decision_Procs/Ferrack.thy	Thu Nov 05 10:39:59 2015 +0100
     5.3 @@ -7,7 +7,7 @@
     5.4    "~~/src/HOL/Library/Code_Target_Numeral" "~~/src/HOL/Library/Old_Recdef"
     5.5  begin
     5.6  
     5.7 -section \<open>Quantifier elimination for @{text "\<real> (0, 1, +, <)"}\<close>
     5.8 +section \<open>Quantifier elimination for \<open>\<real> (0, 1, +, <)\<close>\<close>
     5.9  
    5.10    (*********************************************************************************)
    5.11    (****                            SHADOW SYNTAX AND SEMANTICS                  ****)
     6.1 --- a/src/HOL/Decision_Procs/MIR.thy	Thu Nov 05 10:39:49 2015 +0100
     6.2 +++ b/src/HOL/Decision_Procs/MIR.thy	Thu Nov 05 10:39:59 2015 +0100
     6.3 @@ -7,7 +7,7 @@
     6.4    "~~/src/HOL/Library/Code_Target_Numeral" "~~/src/HOL/Library/Old_Recdef"
     6.5  begin
     6.6  
     6.7 -section \<open>Quantifier elimination for @{text "\<real> (0, 1, +, floor, <)"}\<close>
     6.8 +section \<open>Quantifier elimination for \<open>\<real> (0, 1, +, floor, <)\<close>\<close>
     6.9  
    6.10  declare real_of_int_floor_cancel [simp del]
    6.11  
    6.12 @@ -1450,8 +1450,8 @@
    6.13    by (induct p rule: qelim.induct) (auto simp del: simpfm.simps)
    6.14  
    6.15  
    6.16 -text \<open>The @{text "\<int>"} Part\<close>
    6.17 -text\<open>Linearity for fm where Bound 0 ranges over @{text "\<int>"}\<close>
    6.18 +text \<open>The \<open>\<int>\<close> Part\<close>
    6.19 +text\<open>Linearity for fm where Bound 0 ranges over \<open>\<int>\<close>\<close>
    6.20  
    6.21  function zsplit0 :: "num \<Rightarrow> int \<times> num" (* splits the bounded from the unbounded part*) where
    6.22    "zsplit0 (C c) = (0,C c)"
    6.23 @@ -1955,10 +1955,10 @@
    6.24    ultimately show ?case by blast
    6.25  qed auto
    6.26  
    6.27 -text\<open>plusinf : Virtual substitution of @{text "+\<infinity>"}
    6.28 -       minusinf: Virtual substitution of @{text "-\<infinity>"}
    6.29 -       @{text "\<delta>"} Compute lcm @{text "d| Dvd d  c*x+t \<in> p"}
    6.30 -       @{text "d_\<delta>"} checks if a given l divides all the ds above\<close>
    6.31 +text\<open>plusinf : Virtual substitution of \<open>+\<infinity>\<close>
    6.32 +       minusinf: Virtual substitution of \<open>-\<infinity>\<close>
    6.33 +       \<open>\<delta>\<close> Compute lcm \<open>d| Dvd d  c*x+t \<in> p\<close>
    6.34 +       \<open>d_\<delta>\<close> checks if a given l divides all the ds above\<close>
    6.35  
    6.36  fun minusinf:: "fm \<Rightarrow> fm" where
    6.37    "minusinf (And p q) = conj (minusinf p) (minusinf q)" 
    6.38 @@ -3294,9 +3294,9 @@
    6.39    using lp
    6.40    by (induct p rule: mirror.induct) (simp_all add: split_def image_Un)
    6.41    
    6.42 -text \<open>The @{text "\<real>"} part\<close>
    6.43 -
    6.44 -text\<open>Linearity for fm where Bound 0 ranges over @{text "\<real>"}\<close>
    6.45 +text \<open>The \<open>\<real>\<close> part\<close>
    6.46 +
    6.47 +text\<open>Linearity for fm where Bound 0 ranges over \<open>\<real>\<close>\<close>
    6.48  consts
    6.49    isrlfm :: "fm \<Rightarrow> bool"   (* Linearity test for fm *)
    6.50  recdef isrlfm "measure size"
     7.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Thu Nov 05 10:39:49 2015 +0100
     7.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Thu Nov 05 10:39:59 2015 +0100
     7.3 @@ -60,7 +60,7 @@
     7.4  | "tmboundslt n (Sub a b) = (tmboundslt n a \<and> tmboundslt n b)"
     7.5  | "tmboundslt n (Mul i a) = tmboundslt n a"
     7.6  
     7.7 -primrec tmbound0 :: "tm \<Rightarrow> bool"  -- \<open>a tm is INDEPENDENT of Bound 0\<close>
     7.8 +primrec tmbound0 :: "tm \<Rightarrow> bool"  \<comment> \<open>a tm is INDEPENDENT of Bound 0\<close>
     7.9  where
    7.10    "tmbound0 (CP c) = True"
    7.11  | "tmbound0 (Bound n) = (n>0)"
    7.12 @@ -76,7 +76,7 @@
    7.13    using nb
    7.14    by (induct a rule: tm.induct) auto
    7.15  
    7.16 -primrec tmbound :: "nat \<Rightarrow> tm \<Rightarrow> bool"  -- \<open>a tm is INDEPENDENT of Bound n\<close>
    7.17 +primrec tmbound :: "nat \<Rightarrow> tm \<Rightarrow> bool"  \<comment> \<open>a tm is INDEPENDENT of Bound n\<close>
    7.18  where
    7.19    "tmbound n (CP c) = True"
    7.20  | "tmbound n (Bound m) = (n \<noteq> m)"
    7.21 @@ -626,7 +626,7 @@
    7.22  | "boundslt n (E p) = boundslt (Suc n) p"
    7.23  | "boundslt n (A p) = boundslt (Suc n) p"
    7.24  
    7.25 -fun bound0:: "fm \<Rightarrow> bool"  -- \<open>a Formula is independent of Bound 0\<close>
    7.26 +fun bound0:: "fm \<Rightarrow> bool"  \<comment> \<open>a Formula is independent of Bound 0\<close>
    7.27  where
    7.28    "bound0 T = True"
    7.29  | "bound0 F = True"
    7.30 @@ -647,7 +647,7 @@
    7.31    using bp tmbound0_I[where b="b" and bs="bs" and b'="b'"]
    7.32    by (induct p rule: bound0.induct) auto
    7.33  
    7.34 -primrec bound:: "nat \<Rightarrow> fm \<Rightarrow> bool"  -- \<open>a Formula is independent of Bound n\<close>
    7.35 +primrec bound:: "nat \<Rightarrow> fm \<Rightarrow> bool"  \<comment> \<open>a Formula is independent of Bound n\<close>
    7.36  where
    7.37    "bound m T = True"
    7.38  | "bound m F = True"
    7.39 @@ -897,7 +897,7 @@
    7.40  lemma decr0_qf: "bound0 p \<Longrightarrow> qfree (decr0 p)"
    7.41    by (induct p) simp_all
    7.42  
    7.43 -fun isatom :: "fm \<Rightarrow> bool"  -- \<open>test for atomicity\<close>
    7.44 +fun isatom :: "fm \<Rightarrow> bool"  \<comment> \<open>test for atomicity\<close>
    7.45  where
    7.46    "isatom T = True"
    7.47  | "isatom F = True"
    7.48 @@ -1643,7 +1643,7 @@
    7.49  
    7.50  subsection \<open>Core Procedure\<close>
    7.51  
    7.52 -fun minusinf:: "fm \<Rightarrow> fm"  -- \<open>Virtual substitution of -\<infinity>\<close>
    7.53 +fun minusinf:: "fm \<Rightarrow> fm"  \<comment> \<open>Virtual substitution of -\<infinity>\<close>
    7.54  where
    7.55    "minusinf (And p q) = conj (minusinf p) (minusinf q)"
    7.56  | "minusinf (Or p q) = disj (minusinf p) (minusinf q)"
    7.57 @@ -1653,7 +1653,7 @@
    7.58  | "minusinf (Le  (CNP 0 c e)) = disj (conj (eq (CP c)) (le e)) (lt (CP (~\<^sub>p c)))"
    7.59  | "minusinf p = p"
    7.60  
    7.61 -fun plusinf:: "fm \<Rightarrow> fm"  -- \<open>Virtual substitution of +\<infinity>\<close>
    7.62 +fun plusinf:: "fm \<Rightarrow> fm"  \<comment> \<open>Virtual substitution of +\<infinity>\<close>
    7.63  where
    7.64    "plusinf (And p q) = conj (plusinf p) (plusinf q)"
    7.65  | "plusinf (Or p q) = disj (plusinf p) (plusinf q)"
     8.1 --- a/src/HOL/Decision_Procs/Polynomial_List.thy	Thu Nov 05 10:39:49 2015 +0100
     8.2 +++ b/src/HOL/Decision_Procs/Polynomial_List.thy	Thu Nov 05 10:39:59 2015 +0100
     8.3 @@ -81,15 +81,15 @@
     8.4    obtains q where "poly p2 = poly (p1 *** q)"
     8.5    using assms by (auto simp add: divides_def)
     8.6  
     8.7 --- \<open>order of a polynomial\<close>
     8.8 +\<comment> \<open>order of a polynomial\<close>
     8.9  definition (in ring_1) order :: "'a \<Rightarrow> 'a list \<Rightarrow> nat"
    8.10    where "order a p = (SOME n. ([-a, 1] %^ n) divides p \<and> \<not> (([-a, 1] %^ (Suc n)) divides p))"
    8.11  
    8.12 --- \<open>degree of a polynomial\<close>
    8.13 +\<comment> \<open>degree of a polynomial\<close>
    8.14  definition (in semiring_0) degree :: "'a list \<Rightarrow> nat"
    8.15    where "degree p = length (pnormalize p) - 1"
    8.16  
    8.17 --- \<open>squarefree polynomials --- NB with respect to real roots only\<close>
    8.18 +\<comment> \<open>squarefree polynomials --- NB with respect to real roots only\<close>
    8.19  definition (in ring_1) rsquarefree :: "'a list \<Rightarrow> bool"
    8.20    where "rsquarefree p \<longleftrightarrow> poly p \<noteq> poly [] \<and> (\<forall>a. order a p = 0 \<or> order a p = 1)"
    8.21  
     9.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Thu Nov 05 10:39:49 2015 +0100
     9.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Thu Nov 05 10:39:59 2015 +0100
     9.3 @@ -30,7 +30,7 @@
     9.4  | "polysize (Pw p n) = 1 + polysize p"
     9.5  | "polysize (CN c n p) = 4 + polysize c + polysize p"
     9.6  
     9.7 -primrec polybound0:: "poly \<Rightarrow> bool" -- \<open>a poly is INDEPENDENT of Bound 0\<close>
     9.8 +primrec polybound0:: "poly \<Rightarrow> bool" \<comment> \<open>a poly is INDEPENDENT of Bound 0\<close>
     9.9  where
    9.10    "polybound0 (C c) \<longleftrightarrow> True"
    9.11  | "polybound0 (Bound n) \<longleftrightarrow> n > 0"
    9.12 @@ -41,7 +41,7 @@
    9.13  | "polybound0 (Pw p n) \<longleftrightarrow> polybound0 p"
    9.14  | "polybound0 (CN c n p) \<longleftrightarrow> n \<noteq> 0 \<and> polybound0 c \<and> polybound0 p"
    9.15  
    9.16 -primrec polysubst0:: "poly \<Rightarrow> poly \<Rightarrow> poly" -- \<open>substitute a poly into a poly for Bound 0\<close>
    9.17 +primrec polysubst0:: "poly \<Rightarrow> poly \<Rightarrow> poly" \<comment> \<open>substitute a poly into a poly for Bound 0\<close>
    9.18  where
    9.19    "polysubst0 t (C c) = C c"
    9.20  | "polysubst0 t (Bound n) = (if n = 0 then t else Bound n)"
    10.1 --- a/src/HOL/Decision_Procs/ex/Approximation_Quickcheck_Ex.thy	Thu Nov 05 10:39:49 2015 +0100
    10.2 +++ b/src/HOL/Decision_Procs/ex/Approximation_Quickcheck_Ex.thy	Thu Nov 05 10:39:59 2015 +0100
    10.3 @@ -31,7 +31,7 @@
    10.4    shows "x > 1 \<Longrightarrow> x \<le> 2 ^ 20 * log 2 x + 1 \<and> (sin x)\<^sup>2 + (cos x)\<^sup>2 = 1"
    10.5    using [[quickcheck_approximation_custom_seed = 1]]
    10.6    using [[quickcheck_approximation_epsilon = 0.00000001]]
    10.7 -    --\<open>avoids spurious counterexamples in approximate computation of @{term "(sin x)\<^sup>2 + (cos x)\<^sup>2"}
    10.8 +    \<comment>\<open>avoids spurious counterexamples in approximate computation of @{term "(sin x)\<^sup>2 + (cos x)\<^sup>2"}
    10.9        and therefore avoids expensive failing attempts for certification\<close>
   10.10    quickcheck[approximation, expect=counterexample, size=20]
   10.11    oops