src/HOL/Decision_Procs/Cooper.thy

 (*********************************************************************************)
 
 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"
 | "num_size (Neg a) = 1 + num_size a"
 | "num_size (Add a b) = 1 + num_size a + num_size b"

   T| F| Lt num| Le num| Gt num| Ge num| Eq num| NEq num| Dvd int num| NDvd int num|
   NOT fm| And fm fm|  Or fm fm| Imp fm fm| Iff fm fm| E fm| A fm
   | 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"
 | "fmsize (Or p q) = 1 + fmsize p + fmsize q"
 | "fmsize (Imp p q) = 3 + fmsize p + fmsize q"

 | "fmsize p = 1"
 
 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"
 | "Ifm bbs bs (Lt a) \<longleftrightarrow> Inum bs a < 0"
 | "Ifm bbs bs (Gt a) \<longleftrightarrow> Inum bs a > 0"

 
 lemma prep: "Ifm bbs bs (prep p) = Ifm bbs bs p"
   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"
 | "qfree (NOT p) \<longleftrightarrow> qfree p"
 | "qfree (And p q) \<longleftrightarrow> qfree p \<and> qfree q"

 | "qfree p \<longleftrightarrow> True"
 
 
 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"
 | "numbound0 (CN n i a) \<longleftrightarrow> n > 0 \<and> numbound0 a"
 | "numbound0 (Neg a) \<longleftrightarrow> numbound0 a"

 lemma numbound0_I:
   assumes nb: "numbound0 a"
   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"
 | "bound0 (Lt a) \<longleftrightarrow> numbound0 a"
 | "bound0 (Le a) \<longleftrightarrow> numbound0 a"

 
 lemma numsubst0_I':
   "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"
 | "subst0 t (Lt a) = Lt (numsubst0 t a)"
 | "subst0 t (Le a) = Le (numsubst0 t a)"

   using nb by (induct p rule: decr.induct) (simp_all add: gr0_conv_Suc decrnum)
 
 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"
 | "isatom (Lt a) \<longleftrightarrow> True"
 | "isatom (Le a) \<longleftrightarrow> True"

   using qe_inv DJ_qe[OF qe_inv]
   by (induct p rule: qelim.induct)
     (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>
-
-fun zsplit0 :: "num \<Rightarrow> int \<times> num"  -- \<open>splits the bounded from the unbounded part\<close>
+text \<open>Linearity for fm where Bound 0 ranges over \<open>\<int>\<close>\<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))"
 | "zsplit0 (CN n i a) =
     (let (i', a') =  zsplit0 a

     by (simp add: distrib_left)
   finally show ?case using th th2
     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"
   "iszlfm (Eq  (CN 0 c e)) \<longleftrightarrow> c > 0 \<and> numbound0 e"
   "iszlfm (NEq (CN 0 c e)) \<longleftrightarrow> c > 0 \<and> numbound0 e"

   "iszlfm p \<longleftrightarrow> isatom p \<and> bound0 p"
 
 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)"
   "zlfm (Imp p q) = Or (zlfm (NOT p)) (zlfm q)"
   "zlfm (Iff p q) = Or (And (zlfm p) (zlfm q)) (And (zlfm (NOT p)) (zlfm (NOT q)))"

     with Ia 4 dvd_minus_iff[of "abs j" "?c*i + ?N ?r"] show ?thesis
       by (simp add: Let_def split_def)
   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)"
   "minusinf (Eq  (CN 0 c e)) = F"
   "minusinf (NEq (CN 0 c e)) = T"

   "minusinf p = p"
 
 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)"
   "plusinf (Eq  (CN 0 c e)) = F"
   "plusinf (NEq (CN 0 c e)) = T"

   "plusinf (Le  (CN 0 c e)) = F"
   "plusinf (Gt  (CN 0 c e)) = T"
   "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)"
   "\<delta> (Dvd i (CN 0 c e)) = i"
   "\<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)"
   "d_\<delta> (Dvd i (CN 0 c e)) = (\<lambda>d. i dvd d)"
   "d_\<delta> (NDvd i (CN 0 c e)) = (\<lambda>d. i dvd d)"

   from th th' dp show ?case
     by simp
 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))"
   "a_\<beta> (Eq  (CN 0 c e)) = (\<lambda>k. Eq (CN 0 1 (Mul (k div c) e)))"
   "a_\<beta> (NEq (CN 0 c e)) = (\<lambda>k. NEq (CN 0 1 (Mul (k div c) e)))"

   "a_\<beta> (Ge  (CN 0 c e)) = (\<lambda>k. Ge (CN 0 1 (Mul (k div c) e)))"
   "a_\<beta> (Dvd i (CN 0 c e)) =(\<lambda>k. Dvd ((k div c)*i) (CN 0 1 (Mul (k div c) e)))"
   "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))"
   "d_\<beta> (Eq  (CN 0 c e)) = (\<lambda>k. c dvd k)"
   "d_\<beta> (NEq (CN 0 c e)) = (\<lambda>k. c dvd k)"

   "d_\<beta> (Ge  (CN 0 c e)) = (\<lambda>k. c dvd k)"
   "d_\<beta> (Dvd i (CN 0 c e)) =(\<lambda>k. c dvd k)"
   "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)"
   "\<zeta> (Eq  (CN 0 c e)) = c"
   "\<zeta> (NEq (CN 0 c e)) = c"

   "mirror (Ge  (CN 0 c e)) = Le (CN 0 c (Neg e))"
   "mirror (Dvd i (CN 0 c e)) = Dvd i (CN 0 c (Neg e))"
   "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
   shows "x > 0 \<Longrightarrow> x dvd 1 \<longleftrightarrow> x = 1"
   by simp