# HG changeset patch # User wenzelm # Date 1446716399 -3600 # Node ID 5197a2ecb65850a97df9463e70274c98a4636a71 # Parent a9599d3d761002c1877775ed1bfee705f56dd706 isabelle update_cartouches -c -t; diff -r a9599d3d7610 -r 5197a2ecb658 src/HOL/Decision_Procs/Approximation.thy --- 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 \Define auxiliary helper @{text horner} function\ +subsection \Define auxiliary helper \horner\ function\ primrec horner :: "(nat \ nat) \ (nat \ nat \ nat) \ nat \ nat \ nat \ real \ real" where "horner F G 0 i k x = 0" | diff -r a9599d3d7610 -r 5197a2ecb658 src/HOL/Decision_Procs/Commutative_Ring_Complete.thy --- 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 \mkPX conserves normalizedness (@{text "_cn"})\ +text \mkPX conserves normalizedness (\_cn\)\ lemma mkPX_cn: assumes "x \ 0" and "isnorm P" diff -r a9599d3d7610 -r 5197a2ecb658 src/HOL/Decision_Procs/Cooper.thy --- 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 \ nat" -- \A size for num to make inductive proofs simpler\ +primrec num_size :: "num \ nat" \ \A size for num to make inductive proofs simpler\ where "num_size (C c) = 1" | "num_size (Bound n) = 1" @@ -44,7 +44,7 @@ | Closed nat | NClosed nat -fun fmsize :: "fm \ nat" -- \A size for fm\ +fun fmsize :: "fm \ nat" \ \A size for fm\ 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 \ int list \ fm \ bool" -- \Semantics of formulae (fm)\ +primrec Ifm :: "bool list \ int list \ fm \ bool" \ \Semantics of formulae (fm)\ where "Ifm bbs bs T \ True" | "Ifm bbs bs F \ False" @@ -113,7 +113,7 @@ by (induct p arbitrary: bs rule: prep.induct) auto -fun qfree :: "fm \ bool" -- \Quantifier freeness\ +fun qfree :: "fm \ bool" \ \Quantifier freeness\ where "qfree (E p) \ False" | "qfree (A p) \ False" @@ -127,7 +127,7 @@ text \Boundedness and substitution\ -primrec numbound0 :: "num \ bool" -- \a num is INDEPENDENT of Bound 0\ +primrec numbound0 :: "num \ bool" \ \a num is INDEPENDENT of Bound 0\ where "numbound0 (C c) \ True" | "numbound0 (Bound n) \ 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 \ bool" -- \A Formula is independent of Bound 0\ +primrec bound0 :: "fm \ bool" \ \A Formula is independent of Bound 0\ where "bound0 T \ True" | "bound0 F \ True" @@ -188,7 +188,7 @@ "numbound0 a \ 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 \ fm \ fm" -- \substitue a num into a formula for Bound 0\ +primrec subst0:: "num \ fm \ fm" \ \substitue a num into a formula for Bound 0\ where "subst0 t T = T" | "subst0 t F = F" @@ -254,7 +254,7 @@ lemma decr_qf: "bound0 p \ qfree (decr p)" by (induct p) simp_all -fun isatom :: "fm \ bool" -- \test for atomicity\ +fun isatom :: "fm \ bool" \ \test for atomicity\ where "isatom T \ True" | "isatom F \ 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 \Linearity for fm where Bound 0 ranges over @{text "\"}\ +text \Linearity for fm where Bound 0 ranges over \\\\ -fun zsplit0 :: "num \ int \ num" -- \splits the bounded from the unbounded part\ +fun zsplit0 :: "num \ int \ num" \ \splits the bounded from the unbounded part\ 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 \ bool" -- \Linearity test for fm\ +consts iszlfm :: "fm \ bool" \ \Linearity test for fm\ recdef iszlfm "measure size" "iszlfm (And p q) \ iszlfm p \ iszlfm q" "iszlfm (Or p q) \ iszlfm p \ iszlfm q" @@ -1006,7 +1006,7 @@ lemma zlin_qfree: "iszlfm p \ qfree p" by (induct p rule: iszlfm.induct) auto -consts zlfm :: "fm \ fm" -- \Linearity transformation for fm\ +consts zlfm :: "fm \ fm" \ \Linearity transformation for fm\ 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 \ fm" -- \Virtual substitution of @{text "-\"}\ +consts minusinf :: "fm \ fm" \ \Virtual substitution of \-\\\ 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 \ qfree (minusinf p)" by (induct p rule: minusinf.induct) auto -consts plusinf :: "fm \ fm" -- \Virtual substitution of @{text "+\"}\ +consts plusinf :: "fm \ fm" \ \Virtual substitution of \+\\\ 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 \ :: "fm \ int" -- \Compute @{text "lcm {d| N\<^sup>? Dvd c*x+t \ p}"}\ +consts \ :: "fm \ int" \ \Compute \lcm {d| N\<^sup>? Dvd c*x+t \ p}\\ recdef \ "measure size" "\ (And p q) = lcm (\ p) (\ q)" "\ (Or p q) = lcm (\ p) (\ q)" @@ -1293,7 +1293,7 @@ "\ (NDvd i (CN 0 c e)) = i" "\ p = 1" -consts d_\ :: "fm \ int \ bool" -- \check if a given l divides all the ds above\ +consts d_\ :: "fm \ int \ bool" \ \check if a given l divides all the ds above\ recdef d_\ "measure size" "d_\ (And p q) = (\d. d_\ p d \ d_\ q d)" "d_\ (Or p q) = (\d. d_\ p d \ d_\ q d)" @@ -1354,7 +1354,7 @@ qed simp_all -consts a_\ :: "fm \ int \ fm" -- \adjust the coefficients of a formula\ +consts a_\ :: "fm \ int \ fm" \ \adjust the coefficients of a formula\ recdef a_\ "measure size" "a_\ (And p q) = (\k. And (a_\ p k) (a_\ q k))" "a_\ (Or p q) = (\k. Or (a_\ p k) (a_\ q k))" @@ -1368,7 +1368,7 @@ "a_\ (NDvd i (CN 0 c e))=(\k. NDvd ((k div c)*i) (CN 0 1 (Mul (k div c) e)))" "a_\ p = (\k. p)" -consts d_\ :: "fm \ int \ bool" -- \test if all coeffs c of c divide a given l\ +consts d_\ :: "fm \ int \ bool" \ \test if all coeffs c of c divide a given l\ recdef d_\ "measure size" "d_\ (And p q) = (\k. (d_\ p k) \ (d_\ q k))" "d_\ (Or p q) = (\k. (d_\ p k) \ (d_\ q k))" @@ -1382,7 +1382,7 @@ "d_\ (NDvd i (CN 0 c e))=(\k. c dvd k)" "d_\ p = (\k. True)" -consts \ :: "fm \ int" -- \computes the lcm of all coefficients of x\ +consts \ :: "fm \ int" \ \computes the lcm of all coefficients of x\ recdef \ "measure size" "\ (And p q) = lcm (\ p) (\ q)" "\ (Or p q) = lcm (\ p) (\ q)" @@ -1434,7 +1434,7 @@ "mirror (NDvd i (CN 0 c e)) = NDvd i (CN 0 c (Neg e))" "mirror p = p" -text \Lemmas for the correctness of @{text "\_\"}\ +text \Lemmas for the correctness of \\_\\\ lemma dvd1_eq1: fixes x :: int diff -r a9599d3d7610 -r 5197a2ecb658 src/HOL/Decision_Procs/Dense_Linear_Order.thy --- 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]: "(\x. P x) \ (\x. (\y \ {}. y < x) \ (\y\ {}. x < y) \ P x)" by simp -text\Theorems for @{text "\z. \x. x < z \ (P x \ P\<^sub>-\<^sub>\)"}\ +text\Theorems for \\z. \x. x < z \ (P x \ P\<^sub>-\<^sub>\)\\ lemma minf_lt[no_atp]: "\z . \x. x < z \ (x < t \ True)" by auto lemma minf_gt[no_atp]: "\z . \x. x < z \ (t < x \ 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]: "\z. \x. x < z \ (x \ t \ True)" by auto lemma minf_P[no_atp]: "\z. \x. x < z \ (P \ P)" by blast -text\Theorems for @{text "\z. \x. x < z \ (P x \ P\<^sub>+\<^sub>\)"}\ +text\Theorems for \\z. \x. x < z \ (P x \ P\<^sub>+\<^sub>\)\\ lemma pinf_gt[no_atp]: "\z. \x. z < x \ (t < x \ True)" by auto lemma pinf_lt[no_atp]: "\z. \x. z < x \ (x < t \ 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]: "\y. x \ y" using gt_ex by auto -text \Theorems for @{text "\z. \x. z \ x \ (P x \ P\<^sub>+\<^sub>\)"}\ +text \Theorems for \\z. \x. z \ x \ (P x \ P\<^sub>+\<^sub>\)\\ lemma pinf_conj[no_atp]: assumes ex1: "\z1. \x. z1 \ x \ (P1 x \ P1')" and ex2: "\z2. \x. z2 \ x \ (P2 x \ P2')" @@ -516,7 +516,7 @@ using lt_ex by auto -text \Theorems for @{text "\z. \x. x \ z \ (P x \ P\<^sub>-\<^sub>\)"}\ +text \Theorems for \\z. \x. x \ z \ (P x \ P\<^sub>-\<^sub>\)\\ lemma minf_conj[no_atp]: assumes ex1: "\z1. \x. x \ z1 \ (P1 x \ P1')" and ex2: "\z2. \x. x \ z2 \ (P2 x \ P2')" diff -r a9599d3d7610 -r 5197a2ecb658 src/HOL/Decision_Procs/Ferrack.thy --- 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 \Quantifier elimination for @{text "\ (0, 1, +, <)"}\ +section \Quantifier elimination for \\ (0, 1, +, <)\\ (*********************************************************************************) (**** SHADOW SYNTAX AND SEMANTICS ****) diff -r a9599d3d7610 -r 5197a2ecb658 src/HOL/Decision_Procs/MIR.thy --- 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 \Quantifier elimination for @{text "\ (0, 1, +, floor, <)"}\ +section \Quantifier elimination for \\ (0, 1, +, floor, <)\\ declare real_of_int_floor_cancel [simp del] @@ -1450,8 +1450,8 @@ by (induct p rule: qelim.induct) (auto simp del: simpfm.simps) -text \The @{text "\"} Part\ -text\Linearity for fm where Bound 0 ranges over @{text "\"}\ +text \The \\\ Part\ +text\Linearity for fm where Bound 0 ranges over \\\\ function zsplit0 :: "num \ int \ 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\plusinf : Virtual substitution of @{text "+\"} - minusinf: Virtual substitution of @{text "-\"} - @{text "\"} Compute lcm @{text "d| Dvd d c*x+t \ p"} - @{text "d_\"} checks if a given l divides all the ds above\ +text\plusinf : Virtual substitution of \+\\ + minusinf: Virtual substitution of \-\\ + \\\ Compute lcm \d| Dvd d c*x+t \ p\ + \d_\\ checks if a given l divides all the ds above\ fun minusinf:: "fm \ 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 \The @{text "\"} part\ - -text\Linearity for fm where Bound 0 ranges over @{text "\"}\ +text \The \\\ part\ + +text\Linearity for fm where Bound 0 ranges over \\\\ consts isrlfm :: "fm \ bool" (* Linearity test for fm *) recdef isrlfm "measure size" diff -r a9599d3d7610 -r 5197a2ecb658 src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy --- 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 \ tmboundslt n b)" | "tmboundslt n (Mul i a) = tmboundslt n a" -primrec tmbound0 :: "tm \ bool" -- \a tm is INDEPENDENT of Bound 0\ +primrec tmbound0 :: "tm \ bool" \ \a tm is INDEPENDENT of Bound 0\ 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 \ tm \ bool" -- \a tm is INDEPENDENT of Bound n\ +primrec tmbound :: "nat \ tm \ bool" \ \a tm is INDEPENDENT of Bound n\ where "tmbound n (CP c) = True" | "tmbound n (Bound m) = (n \ m)" @@ -626,7 +626,7 @@ | "boundslt n (E p) = boundslt (Suc n) p" | "boundslt n (A p) = boundslt (Suc n) p" -fun bound0:: "fm \ bool" -- \a Formula is independent of Bound 0\ +fun bound0:: "fm \ bool" \ \a Formula is independent of Bound 0\ 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 \ fm \ bool" -- \a Formula is independent of Bound n\ +primrec bound:: "nat \ fm \ bool" \ \a Formula is independent of Bound n\ where "bound m T = True" | "bound m F = True" @@ -897,7 +897,7 @@ lemma decr0_qf: "bound0 p \ qfree (decr0 p)" by (induct p) simp_all -fun isatom :: "fm \ bool" -- \test for atomicity\ +fun isatom :: "fm \ bool" \ \test for atomicity\ where "isatom T = True" | "isatom F = True" @@ -1643,7 +1643,7 @@ subsection \Core Procedure\ -fun minusinf:: "fm \ fm" -- \Virtual substitution of -\\ +fun minusinf:: "fm \ fm" \ \Virtual substitution of -\\ 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 \ fm" -- \Virtual substitution of +\\ +fun plusinf:: "fm \ fm" \ \Virtual substitution of +\\ where "plusinf (And p q) = conj (plusinf p) (plusinf q)" | "plusinf (Or p q) = disj (plusinf p) (plusinf q)" diff -r a9599d3d7610 -r 5197a2ecb658 src/HOL/Decision_Procs/Polynomial_List.thy --- 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) --- \order of a polynomial\ +\ \order of a polynomial\ definition (in ring_1) order :: "'a \ 'a list \ nat" where "order a p = (SOME n. ([-a, 1] %^ n) divides p \ \ (([-a, 1] %^ (Suc n)) divides p))" --- \degree of a polynomial\ +\ \degree of a polynomial\ definition (in semiring_0) degree :: "'a list \ nat" where "degree p = length (pnormalize p) - 1" --- \squarefree polynomials --- NB with respect to real roots only\ +\ \squarefree polynomials --- NB with respect to real roots only\ definition (in ring_1) rsquarefree :: "'a list \ bool" where "rsquarefree p \ poly p \ poly [] \ (\a. order a p = 0 \ order a p = 1)" diff -r a9599d3d7610 -r 5197a2ecb658 src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy --- 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 \ bool" -- \a poly is INDEPENDENT of Bound 0\ +primrec polybound0:: "poly \ bool" \ \a poly is INDEPENDENT of Bound 0\ where "polybound0 (C c) \ True" | "polybound0 (Bound n) \ n > 0" @@ -41,7 +41,7 @@ | "polybound0 (Pw p n) \ polybound0 p" | "polybound0 (CN c n p) \ n \ 0 \ polybound0 c \ polybound0 p" -primrec polysubst0:: "poly \ poly \ poly" -- \substitute a poly into a poly for Bound 0\ +primrec polysubst0:: "poly \ poly \ poly" \ \substitute a poly into a poly for Bound 0\ where "polysubst0 t (C c) = C c" | "polysubst0 t (Bound n) = (if n = 0 then t else Bound n)" diff -r a9599d3d7610 -r 5197a2ecb658 src/HOL/Decision_Procs/ex/Approximation_Quickcheck_Ex.thy --- 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 \ x \ 2 ^ 20 * log 2 x + 1 \ (sin x)\<^sup>2 + (cos x)\<^sup>2 = 1" using [[quickcheck_approximation_custom_seed = 1]] using [[quickcheck_approximation_epsilon = 0.00000001]] - --\avoids spurious counterexamples in approximate computation of @{term "(sin x)\<^sup>2 + (cos x)\<^sup>2"} + \\avoids spurious counterexamples in approximate computation of @{term "(sin x)\<^sup>2 + (cos x)\<^sup>2"} and therefore avoids expensive failing attempts for certification\ quickcheck[approximation, expect=counterexample, size=20] oops