author wenzelm Mon, 22 Jun 2015 23:19:48 +0200 changeset 60560 ce7030d9191d parent 60559 48d7b203c0ea child 60561 85aed595feb4 child 60562 24af00b010cf
tuned proofs;
```--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Mon Jun 22 21:50:56 2015 +0200
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Mon Jun 22 23:19:48 2015 +0200
@@ -2,7 +2,7 @@
Author:     Amine Chaieb
*)

-section\<open>A formalization of Ferrante and Rackoff's procedure with polynomial parameters, see Paper in CALCULEMUS 2008\<close>
+section \<open>A formalization of Ferrante and Rackoff's procedure with polynomial parameters, see Paper in CALCULEMUS 2008\<close>

theory Parametric_Ferrante_Rackoff
imports
@@ -18,7 +18,7 @@
datatype tm = CP poly | Bound nat | Add tm tm | Mul poly tm
| Neg tm | Sub tm tm | CNP nat poly tm

-(* A size for poly to make inductive proofs simpler*)
+text \<open>A size for poly to make inductive proofs simpler.\<close>
primrec tmsize :: "tm \<Rightarrow> nat"
where
"tmsize (CP c) = polysize c"
@@ -29,8 +29,8 @@
| "tmsize (Mul c a) = 1 + polysize c + tmsize a"
| "tmsize (CNP n c a) = 3 + polysize c + tmsize a "

-(* Semantics of terms tm *)
-primrec Itm :: "'a::{field_char_0, field} list \<Rightarrow> 'a list \<Rightarrow> tm \<Rightarrow> 'a"
+text \<open>Semantics of terms tm.\<close>
+primrec Itm :: "'a::{field_char_0,field} list \<Rightarrow> 'a list \<Rightarrow> tm \<Rightarrow> 'a"
where
"Itm vs bs (CP c) = (Ipoly vs c)"
| "Itm vs bs (Bound n) = bs!n"
@@ -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" (* a tm is INDEPENDENT of Bound 0 *)
+primrec tmbound0 :: "tm \<Rightarrow> bool"  -- \<open>a tm is INDEPENDENT of Bound 0\<close>
where
"tmbound0 (CP c) = True"
| "tmbound0 (Bound n) = (n>0)"
@@ -74,9 +74,9 @@
assumes nb: "tmbound0 a"
shows "Itm vs (b#bs) a = Itm vs (b'#bs) a"
using nb
-  by (induct a rule: tm.induct,auto)
-
-primrec tmbound :: "nat \<Rightarrow> tm \<Rightarrow> bool" (* a tm is INDEPENDENT of Bound n *)
+  by (induct a rule: tm.induct) auto
+
+primrec tmbound :: "nat \<Rightarrow> tm \<Rightarrow> bool"  -- \<open>a tm is INDEPENDENT of Bound n\<close>
where
"tmbound n (CP c) = True"
| "tmbound n (Bound m) = (n \<noteq> m)"
@@ -146,8 +146,7 @@
lemma nth_length_exceeds: "n \<ge> length xs \<Longrightarrow> xs!n = []!(n - length xs)"
by (induct xs arbitrary: n) auto

-lemma removen_length:
-  "length (removen n xs) = (if n \<ge> length xs then length xs else length xs - 1)"
+lemma removen_length: "length (removen n xs) = (if n \<ge> length xs then length xs else length xs - 1)"
by (induct xs arbitrary: n, auto)

lemma removen_nth:
@@ -160,44 +159,45 @@
case Nil
then show ?case by simp
next
-  case (Cons x xs n m)
-  {
-    assume nxs: "n \<ge> length (x#xs)"
-    then have ?case using removen_same[OF nxs] by simp
-  }
-  moreover
-  {
-    assume nxs: "\<not> (n \<ge> length (x#xs))"
-    {
-      assume mln: "m < n"
-      then have ?case using Cons by (cases m) auto
-    }
-    moreover
-    {
-      assume mln: "\<not> (m < n)"
-      {
-        assume mxs: "m \<le> length (x#xs)"
-        then have ?case using Cons by (cases m) auto
-      }
-      moreover
-      {
-        assume mxs: "\<not> (m \<le> length (x#xs))"
-        have th: "length (removen n (x#xs)) = length xs"
-          using removen_length[where n="n" and xs="x#xs"] nxs by simp
-        with mxs have mxs':"m \<ge> length (removen n (x#xs))"
+  case (Cons x xs)
+  let ?l = "length (x # xs)"
+  consider "n \<ge> ?l" | "n < ?l" by arith
+  then show ?case
+  proof cases
+    case 1
+    then show ?thesis
+      using removen_same[OF 1] by simp
+  next
+    case 2
+    consider "m < n" | "m \<ge> n" by arith
+    then show ?thesis
+    proof cases
+      case 1
+      then show ?thesis
+        using Cons by (cases m) auto
+    next
+      case 2
+      consider "m \<le> ?l" | "m > ?l" by arith
+      then show ?thesis
+      proof cases
+        case 1
+        then show ?thesis
+          using Cons by (cases m) auto
+      next
+        case 2
+        have th: "length (removen n (x # xs)) = length xs"
+          using removen_length[where n = n and xs= "x # xs"] \<open>n < ?l\<close> by simp
+        with \<open>m > ?l\<close> have "m \<ge> length (removen n (x # xs))"
by auto
-        then have "(removen n (x#xs))!m = [] ! (m - length xs)"
-          using th nth_length_exceeds[OF mxs'] by auto
-        then have th: "(removen n (x#xs))!m = [] ! (m - (length (x#xs) - 1))"
+        from th nth_length_exceeds[OF this] have "(removen n (x # xs))!m = [] ! (m - length xs)"
+           by auto
+        then have "(removen n (x # xs))!m = [] ! (m - (length (x # xs) - 1))"
by auto
-        then have ?case
-          using nxs mln mxs by auto
-      }
-      ultimately have ?case by blast
-    }
-    ultimately have ?case by blast
-  }
-  ultimately show ?case by blast
+        then show ?thesis
+          using \<open>n < ?l\<close> \<open>m > ?l\<close> \<open>m > ?l\<close> by auto
+      qed
+    qed
+  qed
qed

lemma decrtm:
@@ -217,7 +217,7 @@
| "tmsubst0 t (Sub a b) = Sub (tmsubst0 t a) (tmsubst0 t b)"
| "tmsubst0 t (Mul i a) = Mul i (tmsubst0 t a)"

-lemma tmsubst0: "Itm vs (x#bs) (tmsubst0 t a) = Itm vs ((Itm vs (x#bs) t)#bs) a"
+lemma tmsubst0: "Itm vs (x # bs) (tmsubst0 t a) = Itm vs (Itm vs (x # bs) t # bs) a"
by (induct a rule: tm.induct) auto

lemma tmsubst0_nb: "tmbound0 t \<Longrightarrow> tmbound0 (tmsubst0 t a)"
@@ -256,7 +256,8 @@
lemma incrtm0_tmbound: "tmbound n t \<Longrightarrow> tmbound (Suc n) (incrtm0 t)"
by (induct t) auto

-(* Simplification *)
+
+text \<open>Simplification.\<close>

consts tmadd:: "tm \<times> tm \<Rightarrow> tm"
recdef tmadd "measure (\<lambda>(t,s). size t + size s)"
@@ -272,9 +273,13 @@

-  apply (case_tac "c1 +\<^sub>p c2 = 0\<^sub>p",case_tac "n1 \<le> n2", simp_all)
-  apply (case_tac "n1 = n2", simp_all add: field_simps)
+  apply (induct t s rule: tmadd.induct)
+  apply (case_tac "c1 +\<^sub>p c2 = 0\<^sub>p")
+  apply (case_tac "n1 \<le> n2")
+  apply simp_all
+  apply (case_tac "n1 = n2")
apply (simp only: distrib_left[symmetric])
done
@@ -311,7 +316,7 @@
by (induct t arbitrary: i rule: tmmul.induct) (auto simp add: Let_def)

lemma tmmul_allpolys_npoly[simp]:
-  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
+  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
shows "allpolys isnpoly t \<Longrightarrow> isnpoly c \<Longrightarrow> allpolys isnpoly (tmmul t c)"
by (induct t rule: tmmul.induct) (simp_all add: Let_def polymul_norm)

@@ -337,7 +342,7 @@
unfolding isnpoly_def by simp

lemma tmneg_allpolys_npoly[simp]:
-  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
+  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
shows "allpolys isnpoly t \<Longrightarrow> allpolys isnpoly (tmneg t)"
unfolding tmneg_def by auto

@@ -354,7 +359,7 @@
using tmsub_def by simp

lemma tmsub_allpolys_npoly[simp]:
-  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
+  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
shows "allpolys isnpoly t \<Longrightarrow> allpolys isnpoly s \<Longrightarrow> allpolys isnpoly (tmsub t s)"
unfolding tmsub_def by (simp add: isnpoly_def)

@@ -371,7 +376,7 @@
(let c' = polynate c in if c' = 0\<^sub>p then simptm t else tmadd (CNP n c' (CP 0\<^sub>p ), simptm t))"

lemma polynate_stupid:
-  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
+  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
shows "polynate t = 0\<^sub>p \<Longrightarrow> Ipoly bs t = (0::'a)"
apply (subst polynate[symmetric])
apply simp
@@ -390,17 +395,17 @@
by (induct t rule: simptm.induct) (auto simp add: Let_def)

lemma [simp]: "isnpoly 0\<^sub>p"
-  and [simp]: "isnpoly (C(1,1))"
+  and [simp]: "isnpoly (C (1, 1))"

lemma simptm_allpolys_npoly[simp]:
-  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
+  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
shows "allpolys isnpoly (simptm p)"
by (induct p rule: simptm.induct) (auto simp add: Let_def)

declare let_cong[fundef_cong del]

-fun split0 :: "tm \<Rightarrow> (poly \<times> tm)"
+fun split0 :: "tm \<Rightarrow> poly \<times> tm"
where
"split0 (Bound 0) = ((1)\<^sub>p, CP 0\<^sub>p)"
| "split0 (CNP 0 c t) = (let (c', t') = split0 t in (c +\<^sub>p c', t'))"
@@ -420,7 +425,7 @@
done

lemma split0:
-  "tmbound 0 (snd (split0 t)) \<and> (Itm vs bs (CNP 0 (fst (split0 t)) (snd (split0 t))) = Itm vs bs t)"
+  "tmbound 0 (snd (split0 t)) \<and> Itm vs bs (CNP 0 (fst (split0 t)) (snd (split0 t))) = Itm vs bs t"
apply (induct t rule: split0.induct)
apply simp
apply (simp add: Let_def split_def field_simps)
@@ -445,7 +450,7 @@
qed

lemma split0_nb0:
-  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
+  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
shows "split0 t = (c',t') \<Longrightarrow>  tmbound 0 t'"
proof -
fix c' t'
@@ -457,7 +462,7 @@
qed

lemma split0_nb0'[simp]:
-  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
+  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
shows "tmbound0 (snd (split0 t))"
using split0_nb0[of t "fst (split0 t)" "snd (split0 t)"]
@@ -485,13 +490,13 @@
by (induct p rule: split0.induct) (auto simp  add: isnpoly_def Let_def split_def)

lemma isnpoly_fst_split0:
-  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
+  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
shows "allpolys isnpoly p \<Longrightarrow> isnpoly (fst (split0 p))"
by (induct p rule: split0.induct)

-subsection\<open>Formulae\<close>
+subsection \<open>Formulae\<close>

datatype fm  =  T| F| Le tm | Lt tm | Eq tm | NEq tm|
NOT fm| And fm fm|  Or fm fm| Imp fm fm| Iff fm fm| E fm| A fm
@@ -514,7 +519,7 @@
by (induct p rule: fmsize.induct) simp_all

(* Semantics of formulae (fm) *)
-primrec Ifm ::"'a::{linordered_field} list \<Rightarrow> 'a list \<Rightarrow> fm \<Rightarrow> bool"
+primrec Ifm ::"'a::linordered_field list \<Rightarrow> 'a list \<Rightarrow> fm \<Rightarrow> bool"
where
"Ifm vs bs T = True"
| "Ifm vs bs F = False"
@@ -731,27 +736,27 @@
using bnd nb nle
proof (induct p arbitrary: bs m rule: fm.induct)
case (E p bs m)
-  { fix x
+  have "Ifm vs (removen (Suc m) (x#bs)) (decr (Suc m) p) = Ifm vs (x#bs) p" for x
+  proof -
from E
have bnd: "boundslt (length (x#bs)) p"
and nb: "bound (Suc m) p"
and nle: "Suc m < length (x#bs)"
by auto
-    from E(1)[OF bnd nb nle]
-    have "Ifm vs (removen (Suc m) (x#bs)) (decr (Suc m) p) = Ifm vs (x#bs) p" .
-  }
+    from E(1)[OF bnd nb nle] show ?thesis .
+  qed
then show ?case by auto
next
case (A p bs m)
-  { fix x
+  have "Ifm vs (removen (Suc m) (x#bs)) (decr (Suc m) p) = Ifm vs (x#bs) p" for x
+  proof -
from A
have bnd: "boundslt (length (x#bs)) p"
and nb: "bound (Suc m) p"
and nle: "Suc m < length (x#bs)"
by auto
-    from A(1)[OF bnd nb nle]
-    have "Ifm vs (removen (Suc m) (x#bs)) (decr (Suc m) p) = Ifm vs (x#bs) p" .
-  }
+    from A(1)[OF bnd nb nle] show ?thesis .
+  qed
then show ?case by auto
qed (auto simp add: decrtm removen_nth)

@@ -807,8 +812,9 @@
using nb nlm
proof (induct p arbitrary: bs n t rule: fm.induct)
case (E p bs n)
-  {
-    fix x
+  have "Ifm vs (x#bs) (subst (Suc n) (incrtm0 t) p) =
+        Ifm vs (x#bs[n:= Itm vs bs t]) p" for x
+  proof -
from E have bn: "boundslt (length (x#bs)) p"
by simp
from E have nlm: "Suc n \<le> length (x#bs)"
@@ -817,15 +823,15 @@
have "Ifm vs (x#bs) (subst (Suc n) (incrtm0 t) p) =
Ifm vs ((x#bs)[Suc n:= Itm vs (x#bs) (incrtm0 t)]) p"
by simp
-    then have "Ifm vs (x#bs) (subst (Suc n) (incrtm0 t) p) =
-        Ifm vs (x#bs[n:= Itm vs bs t]) p"
+    then show ?thesis
by (simp add: incrtm0[where x="x" and bs="bs" and t="t"])
-  }
+  qed
then show ?case by simp
next
case (A p bs n)
-  {
-    fix x
+  have "Ifm vs (x#bs) (subst (Suc n) (incrtm0 t) p) =
+        Ifm vs (x#bs[n:= Itm vs bs t]) p" for x
+  proof -
from A have bn: "boundslt (length (x#bs)) p"
by simp
from A have nlm: "Suc n \<le> length (x#bs)"
@@ -834,10 +840,9 @@
have "Ifm vs (x#bs) (subst (Suc n) (incrtm0 t) p) =
Ifm vs ((x#bs)[Suc n:= Itm vs (x#bs) (incrtm0 t)]) p"
by simp
-    then have "Ifm vs (x#bs) (subst (Suc n) (incrtm0 t) p) =
-        Ifm vs (x#bs[n:= Itm vs bs t]) p"
+    then show ?thesis
by (simp add: incrtm0[where x="x" and bs="bs" and t="t"])
-  }
+  qed
then show ?case by simp

@@ -894,7 +899,7 @@
lemma decr0_qf: "bound0 p \<Longrightarrow> qfree (decr0 p)"
by (induct p) simp_all

-fun isatom :: "fm \<Rightarrow> bool" (* test for atomicity *)
+fun isatom :: "fm \<Rightarrow> bool"  -- \<open>test for atomicity\<close>
where
"isatom T = True"
| "isatom F = True"
@@ -918,8 +923,13 @@
where "evaldjf f ps \<equiv> foldr (djf f) ps F"

lemma djf_Or: "Ifm vs bs (djf f p q) = Ifm vs bs (Or (f p) q)"
-    (cases "f p", simp_all add: Let_def djf_def)
+  apply (cases "q = T")
+  apply (cases "q = F")
+  apply (cases "f p")
+  apply (simp_all add: Let_def djf_def)
+  done

lemma evaldjf_ex: "Ifm vs bs (evaldjf f ps) \<longleftrightarrow> (\<exists>p \<in> set ps. Ifm vs bs (f p))"
by (induct ps) (simp_all add: evaldjf_def djf_Or)
@@ -927,12 +937,22 @@
lemma evaldjf_bound0:
assumes nb: "\<forall>x\<in> set xs. bound0 (f x)"
shows "bound0 (evaldjf f xs)"
-  using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f a", auto)
+  using nb
+  apply (induct xs)
+  apply (auto simp add: evaldjf_def djf_def Let_def)
+  apply (case_tac "f a")
+  apply auto
+  done

lemma evaldjf_qf:
assumes nb: "\<forall>x\<in> set xs. qfree (f x)"
shows "qfree (evaldjf f xs)"
-  using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f a", auto)
+  using nb
+  apply (induct xs)
+  apply (auto simp add: evaldjf_def djf_def Let_def)
+  apply (case_tac "f a")
+  apply auto
+  done

fun disjuncts :: "fm \<Rightarrow> fm list"
where
@@ -952,8 +972,8 @@
by (simp only: list_all_iff)
qed

-lemma disjuncts_qf: "qfree p \<Longrightarrow> \<forall>q\<in> set (disjuncts p). qfree q"
-proof-
+lemma disjuncts_qf: "qfree p \<Longrightarrow> \<forall>q \<in> set (disjuncts p). qfree q"
+proof -
assume qf: "qfree p"
then have "list_all qfree (disjuncts p)"
by (induct p rule: disjuncts.induct) auto
@@ -1026,7 +1046,7 @@
(yes, no) = partition bound0 cjs
in conj (decr0 (list_conj yes)) (f (list_conj no)))"

-lemma conjuncts_qf: "qfree p \<Longrightarrow> \<forall>q\<in> set (conjuncts p). qfree q"
+lemma conjuncts_qf: "qfree p \<Longrightarrow> \<forall>q \<in> set (conjuncts p). qfree q"
proof -
assume qf: "qfree p"
then have "list_all qfree (conjuncts p)"
@@ -1146,7 +1166,7 @@
definition "simpneq t = (let (c,s) = split0 (simptm t) in if c= 0\<^sub>p then neq s else NEq (CNP 0 c s))"

lemma simplt_islin[simp]:
-  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
+  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
shows "islin (simplt t)"
unfolding simplt_def
using split0_nb0'
@@ -1154,7 +1174,7 @@
islin_stupid allpolys_split0[OF simptm_allpolys_npoly])

lemma simple_islin[simp]:
-  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
+  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
shows "islin (simple t)"
unfolding simple_def
using split0_nb0'
@@ -1162,7 +1182,7 @@
islin_stupid allpolys_split0[OF simptm_allpolys_npoly] le_lin)

lemma simpeq_islin[simp]:
-  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
+  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
shows "islin (simpeq t)"
unfolding simpeq_def
using split0_nb0'
@@ -1170,7 +1190,7 @@
islin_stupid allpolys_split0[OF simptm_allpolys_npoly] eq_lin)

lemma simpneq_islin[simp]:
-  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
+  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
shows "islin (simpneq t)"
unfolding simpneq_def
using split0_nb0'
@@ -1181,7 +1201,7 @@
by (cases "split0 s") auto

lemma split0_npoly:
-  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
+  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
and n: "allpolys isnpoly t"
shows "isnpoly (fst (split0 t))"
and "allpolys isnpoly (snd (split0 t))"
@@ -1195,20 +1215,18 @@
have n: "allpolys isnpoly (simptm t)"
by simp
let ?t = "simptm t"
-  {
-    assume "fst (split0 ?t) = 0\<^sub>p"
-    then have ?thesis
+  show ?thesis
+  proof (cases "fst (split0 ?t) = 0\<^sub>p")
+    case True
+    then show ?thesis
using split0[of "simptm t" vs bs] lt[OF split0_npoly(2)[OF n], of vs bs]
by (simp add: simplt_def Let_def split_def lt)
-  }
-  moreover
-  {
-    assume "fst (split0 ?t) \<noteq> 0\<^sub>p"
-    then have ?thesis
-      using  split0[of "simptm t" vs bs]
+  next
+    case False
+    then show ?thesis
+      using split0[of "simptm t" vs bs]
by (simp add: simplt_def Let_def split_def)
-  }
-  ultimately show ?thesis by blast
+  qed
qed

lemma simple[simp]: "Ifm vs bs (simple t) = Ifm vs bs (Le t)"
@@ -1216,20 +1234,18 @@
have n: "allpolys isnpoly (simptm t)"
by simp
let ?t = "simptm t"
-  {
-    assume "fst (split0 ?t) = 0\<^sub>p"
-    then have ?thesis
+  show ?thesis
+  proof (cases "fst (split0 ?t) = 0\<^sub>p")
+    case True
+    then show ?thesis
using split0[of "simptm t" vs bs] le[OF split0_npoly(2)[OF n], of vs bs]
by (simp add: simple_def Let_def split_def le)
-  }
-  moreover
-  {
-    assume "fst (split0 ?t) \<noteq> 0\<^sub>p"
-    then have ?thesis
+  next
+    case False
+    then show ?thesis
using split0[of "simptm t" vs bs]
by (simp add: simple_def Let_def split_def)
-  }
-  ultimately show ?thesis by blast
+  qed
qed

lemma simpeq[simp]: "Ifm vs bs (simpeq t) = Ifm vs bs (Eq t)"
@@ -1237,19 +1253,17 @@
have n: "allpolys isnpoly (simptm t)"
by simp
let ?t = "simptm t"
-  {
-    assume "fst (split0 ?t) = 0\<^sub>p"
-    then have ?thesis
+  show ?thesis
+  proof (cases "fst (split0 ?t) = 0\<^sub>p")
+    case True
+    then show ?thesis
using split0[of "simptm t" vs bs] eq[OF split0_npoly(2)[OF n], of vs bs]
by (simp add: simpeq_def Let_def split_def)
-  }
-  moreover
-  {
-    assume "fst (split0 ?t) \<noteq> 0\<^sub>p"
-    then have ?thesis using  split0[of "simptm t" vs bs]
+  next
+    case False
+    then show ?thesis using  split0[of "simptm t" vs bs]
by (simp add: simpeq_def Let_def split_def)
-  }
-  ultimately show ?thesis by blast
+  qed
qed

lemma simpneq[simp]: "Ifm vs bs (simpneq t) = Ifm vs bs (NEq t)"
@@ -1257,19 +1271,17 @@
have n: "allpolys isnpoly (simptm t)"
by simp
let ?t = "simptm t"
-  {
-    assume "fst (split0 ?t) = 0\<^sub>p"
-    then have ?thesis
+  show ?thesis
+  proof (cases "fst (split0 ?t) = 0\<^sub>p")
+    case True
+    then show ?thesis
using split0[of "simptm t" vs bs] neq[OF split0_npoly(2)[OF n], of vs bs]
by (simp add: simpneq_def Let_def split_def)
-  }
-  moreover
-  {
-    assume "fst (split0 ?t) \<noteq> 0\<^sub>p"
-    then have ?thesis
+  next
+    case False
+    then show ?thesis
using split0[of "simptm t" vs bs] by (simp add: simpneq_def Let_def split_def)
-  }
-  ultimately show ?thesis by blast
+  qed
qed

lemma lt_nb: "tmbound0 t \<Longrightarrow> bound0 (lt t)"
@@ -1305,7 +1317,7 @@
done

lemma simplt_nb[simp]:
-  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
+  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
shows "tmbound0 t \<Longrightarrow> bound0 (simplt t)"
proof (simp add: simplt_def Let_def split_def)
assume nb: "tmbound0 t"
@@ -1326,7 +1338,7 @@
qed

lemma simple_nb[simp]:
-  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
+  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
shows "tmbound0 t \<Longrightarrow> bound0 (simple t)"
assume nb: "tmbound0 t"
@@ -1347,7 +1359,7 @@
qed

lemma simpeq_nb[simp]:
-  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
+  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
shows "tmbound0 t \<Longrightarrow> bound0 (simpeq t)"
proof (simp add: simpeq_def Let_def split_def)
assume nb: "tmbound0 t"
@@ -1368,7 +1380,7 @@
qed

lemma simpneq_nb[simp]:
-  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
+  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
shows "tmbound0 t \<Longrightarrow> bound0 (simpneq t)"
proof (simp add: simpneq_def Let_def split_def)
assume nb: "tmbound0 t"
@@ -1474,15 +1486,15 @@
by blast+
from cno_qf yes_qf have qf: "qfree (CJNB qe p)"
by (simp add: CJNB_def Let_def split_def)
-  {
-    fix bs
+  have "Ifm vs bs p = ((Ifm vs bs ?cyes) \<and> (Ifm vs bs ?cno))" for bs
+  proof -
from conjuncts have "Ifm vs bs p = (\<forall>q\<in> set ?cjs. Ifm vs bs q)"
by blast
also have "\<dots> = ((\<forall>q\<in> set ?yes. Ifm vs bs q) \<and> (\<forall>q\<in> set ?no. Ifm vs bs q))"
using partition_set[OF part] by auto
-    finally have "Ifm vs bs p = ((Ifm vs bs ?cyes) \<and> (Ifm vs bs ?cno))"
+    finally show ?thesis
using list_conj[of vs bs] by simp
-  }
+  qed
then have "Ifm vs bs (E p) = (\<exists>x. (Ifm vs (x#bs) ?cyes) \<and> (Ifm vs (x#bs) ?cno))"
by simp
also fix y have "\<dots> = (\<exists>x. (Ifm vs (y#bs) ?cyes) \<and> (Ifm vs (x#bs) ?cno))"
@@ -1526,7 +1538,7 @@
by (induct p arbitrary: bs rule: simpfm.induct) auto

lemma simpfm_bound0:
-  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
+  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
shows "bound0 p \<Longrightarrow> bound0 (simpfm p)"
by (induct p rule: simpfm.induct) auto

@@ -1551,12 +1563,20 @@
apply auto
done

-lemma neq_qf[simp]: "qfree (neq t)" by (simp add: neq_def)
-
-lemma simplt_qf[simp]: "qfree (simplt t)" by (simp add: simplt_def Let_def split_def)
-lemma simple_qf[simp]: "qfree (simple t)" by (simp add: simple_def Let_def split_def)
-lemma simpeq_qf[simp]: "qfree (simpeq t)" by (simp add: simpeq_def Let_def split_def)
-lemma simpneq_qf[simp]: "qfree (simpneq t)" by (simp add: simpneq_def Let_def split_def)
+lemma neq_qf[simp]: "qfree (neq t)"
+
+lemma simplt_qf[simp]: "qfree (simplt t)"
+  by (simp add: simplt_def Let_def split_def)
+
+lemma simple_qf[simp]: "qfree (simple t)"
+  by (simp add: simple_def Let_def split_def)
+
+lemma simpeq_qf[simp]: "qfree (simpeq t)"
+  by (simp add: simpeq_def Let_def split_def)
+
+lemma simpneq_qf[simp]: "qfree (simpneq t)"
+  by (simp add: simpneq_def Let_def split_def)

lemma simpfm_qf[simp]: "qfree p \<Longrightarrow> qfree (simpfm p)"
by (induct p rule: simpfm.induct) auto
@@ -1567,7 +1587,7 @@

lemma
-  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
+  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
shows "qfree p \<Longrightarrow> islin (simpfm p)"
by (induct p rule: simpfm.induct) (simp_all add: conj_lin disj_lin)

@@ -1596,13 +1616,13 @@
"prep (Imp p q) = prep (Or (NOT p) q)"
"prep (Iff p q) = disj (prep (And p q)) (prep (And (NOT p) (NOT q)))"
"prep p = p"

lemma prep: "Ifm vs bs (prep p) = Ifm vs bs p"
by (induct p arbitrary: bs rule: prep.induct) auto

-(* Generic quantifier elimination *)
+text \<open>Generic quantifier elimination.\<close>
function (sequential) qelim :: "fm \<Rightarrow> (fm \<Rightarrow> fm) \<Rightarrow> fm"
where
"qelim (E p) = (\<lambda>qe. DJ (CJNB qe) (qelim p qe))"
@@ -1613,7 +1633,7 @@
| "qelim (Imp p q) = (\<lambda>qe. imp (qelim p qe) (qelim q qe))"
| "qelim (Iff p q) = (\<lambda>qe. iff (qelim p qe) (qelim q qe))"
| "qelim p = (\<lambda>y. simpfm p)"
-by pat_completeness simp_all
+  by pat_completeness simp_all
termination by (relation "measure fmsize") auto

lemma qelim:
@@ -1625,7 +1645,7 @@

subsection \<open>Core Procedure\<close>

-fun minusinf:: "fm \<Rightarrow> fm" (* Virtual substitution of -\<infinity>*)
+fun minusinf:: "fm \<Rightarrow> fm"  -- \<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)"
@@ -1635,7 +1655,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" (* Virtual substitution of +\<infinity>*)
+fun plusinf:: "fm \<Rightarrow> fm"  -- \<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)"
@@ -1673,43 +1693,41 @@
let ?c = "Ipoly vs c"
fix y
let ?e = "Itm vs (y#bs) e"
-  have "?c = 0 \<or> ?c > 0 \<or> ?c < 0" by arith
-  moreover {
-    assume "?c = 0"
-    then have ?case
+  consider "?c = 0" | "?c > 0" | "?c < 0" by arith
+  then show ?case
+  proof cases
+    case 1
+    then show ?thesis
using eq[OF nc(2), of vs] eq[OF nc(1), of vs] by auto
-  }
-  moreover {
-    assume cp: "?c > 0"
-    {
-      fix x
-      assume xz: "x < -?e / ?c"
-      then have "?c * x < - ?e"
-        using pos_less_divide_eq[OF cp, where a="x" and b="-?e"]
+  next
+    case 2
+    have "Ifm vs (x#bs) (Eq (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (Eq (CNP 0 c e)))"
+      if "x < -?e / ?c" for x
+    proof -
+      from that have "?c * x < - ?e"
+        using pos_less_divide_eq[OF \<open>?c > 0\<close>, where a="x" and b="-?e"]
then have "?c * x + ?e < 0"
by simp
-      then have "Ifm vs (x#bs) (Eq (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (Eq (CNP 0 c e)))"
+      then show ?thesis
using eqs tmbound0_I[OF nbe, where b="y" and b'="x" and vs=vs and bs=bs] by auto
-    }
-    then have ?case by auto
-  }
-  moreover {
-    assume cp: "?c < 0"
-    {
-      fix x
-      assume xz: "x < -?e / ?c"
-      then have "?c * x > - ?e"
-        using neg_less_divide_eq[OF cp, where a="x" and b="-?e"]
+    qed
+    then show ?thesis by auto
+  next
+    case 3
+    have "Ifm vs (x#bs) (Eq (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (Eq (CNP 0 c e)))"
+      if "x < -?e / ?c" for x
+    proof -
+      from that have "?c * x > - ?e"
+        using neg_less_divide_eq[OF \<open>?c < 0\<close>, where a="x" and b="-?e"]
then have "?c * x + ?e > 0"
by simp
-      then have "Ifm vs (x#bs) (Eq (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (Eq (CNP 0 c e)))"
+      then show ?thesis
using tmbound0_I[OF nbe, where b="y" and b'="x"] eqs by auto
-    }
-    then have ?case by auto
-  }
-  ultimately show ?case by blast
+    qed
+    then show ?thesis by auto
+  qed
next
case (4 c e)
then have nbe: "tmbound0 e"
@@ -1720,44 +1738,42 @@
let ?c = "Ipoly vs c"
fix y
let ?e = "Itm vs (y#bs) e"
-  have "?c=0 \<or> ?c > 0 \<or> ?c < 0"
+  consider "?c = 0" | "?c > 0" | "?c < 0"
by arith
-  moreover {
-    assume "?c = 0"
-    then have ?case
+  then show ?case
+  proof cases
+    case 1
+    then show ?thesis
using eqs by auto
-  }
-  moreover {
-    assume cp: "?c > 0"
-    {
-      fix x
-      assume xz: "x < -?e / ?c"
-      then have "?c * x < - ?e"
-        using pos_less_divide_eq[OF cp, where a="x" and b="-?e"]
+  next
+    case 2
+    have "Ifm vs (x#bs) (NEq (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (NEq (CNP 0 c e)))"
+      if "x < -?e / ?c" for x
+    proof -
+      from that have "?c * x < - ?e"
+        using pos_less_divide_eq[OF \<open>?c > 0\<close>, where a="x" and b="-?e"]
then have "?c * x + ?e < 0"
by simp
-      then have "Ifm vs (x#bs) (NEq (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (NEq (CNP 0 c e)))"
+      then show ?thesis
using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] by auto
-    }
-    then have ?case by auto
-  }
-  moreover {
-    assume cp: "?c < 0"
-    {
-      fix x
-      assume xz: "x < -?e / ?c"
-      then have "?c * x > - ?e"
-        using neg_less_divide_eq[OF cp, where a="x" and b="-?e"]
+    qed
+    then show ?thesis by auto
+  next
+    case 3
+    have "Ifm vs (x#bs) (NEq (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (NEq (CNP 0 c e)))"
+      if "x < -?e / ?c" for x
+    proof -
+      from that have "?c * x > - ?e"
+        using neg_less_divide_eq[OF \<open>?c < 0\<close>, where a="x" and b="-?e"]
then have "?c * x + ?e > 0"
by simp
-      then have "Ifm vs (x#bs) (NEq (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (NEq (CNP 0 c e)))"
+      then show ?thesis
using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] by auto
-    }
-    then have ?case by auto
-  }
-  ultimately show ?case by blast
+    qed
+    then show ?thesis by auto
+  qed
next
case (5 c e)
then have nbe: "tmbound0 e"
@@ -1770,42 +1786,40 @@
let ?c = "Ipoly vs c"
fix y
let ?e = "Itm vs (y#bs) e"
-  have "?c=0 \<or> ?c > 0 \<or> ?c < 0"
+  consider "?c = 0" | "?c > 0" | "?c < 0"
by arith
-  moreover {
-    assume "?c = 0"
-    then have ?case using eqs by auto
-  }
-  moreover {
-    assume cp: "?c > 0"
-    {
-      fix x
-      assume xz: "x < -?e / ?c"
-      then have "?c * x < - ?e"
-        using pos_less_divide_eq[OF cp, where a="x" and b="-?e"]
+  then show ?case
+  proof cases
+    case 1
+    then show ?thesis using eqs by auto
+  next
+    case 2
+    have "Ifm vs (x#bs) (Lt (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (Lt (CNP 0 c e)))"
+      if "x < -?e / ?c" for x
+    proof -
+      from that have "?c * x < - ?e"
+        using pos_less_divide_eq[OF \<open>?c > 0\<close>, where a="x" and b="-?e"]
then have "?c * x + ?e < 0" by simp
-      then have "Ifm vs (x#bs) (Lt (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (Lt (CNP 0 c e)))"
-        using tmbound0_I[OF nbe, where b="y" and b'="x"] cp eqs by auto
-    }
-    then have ?case by auto
-  }
-  moreover {
-    assume cp: "?c < 0"
-    {
-      fix x
-      assume xz: "x < -?e / ?c"
-      then have "?c * x > - ?e"
-        using neg_less_divide_eq[OF cp, where a="x" and b="-?e"]
+      then show ?thesis
+        using tmbound0_I[OF nbe, where b="y" and b'="x"] \<open>?c > 0\<close> eqs by auto
+    qed
+    then show ?thesis by auto
+  next
+    case 3
+    have "Ifm vs (x#bs) (Lt (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (Lt (CNP 0 c e)))"
+      if "x < -?e / ?c" for x
+    proof -
+      from that have "?c * x > - ?e"
+        using neg_less_divide_eq[OF \<open>?c < 0\<close>, where a="x" and b="-?e"]
then have "?c * x + ?e > 0"
by simp
-      then have "Ifm vs (x#bs) (Lt (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (Lt (CNP 0 c e)))"
-        using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] cp by auto
-    }
-    then have ?case by auto
-  }
-  ultimately show ?case by blast
+      then show ?thesis
+        using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] \<open>?c < 0\<close> by auto
+    qed
+    then show ?thesis by auto
+  qed
next
case (6 c e)
then have nbe: "tmbound0 e"
@@ -1818,44 +1832,42 @@
let ?c = "Ipoly vs c"
fix y
let ?e = "Itm vs (y#bs) e"
-  have "?c = 0 \<or> ?c > 0 \<or> ?c < 0" by arith
-  moreover {
-    assume "?c = 0"
-    then have ?case using eqs by auto
-  }
-  moreover {
-    assume cp: "?c > 0"
-    {
-      fix x
-      assume xz: "x < -?e / ?c"
-      then have "?c * x < - ?e"
-        using pos_less_divide_eq[OF cp, where a="x" and b="-?e"]
+  consider "?c = 0" | "?c > 0" | "?c < 0" by arith
+  then show ?case
+  proof cases
+    case 1
+    then show ?thesis using eqs by auto
+  next
+    case 2
+    have "Ifm vs (x#bs) (Le (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (Le (CNP 0 c e)))"
+      if "x < -?e / ?c" for x
+    proof -
+      from that have "?c * x < - ?e"
+        using pos_less_divide_eq[OF \<open>?c > 0\<close>, where a="x" and b="-?e"]
then have "?c * x + ?e < 0"
by simp
-      then have "Ifm vs (x#bs) (Le (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (Le (CNP 0 c e)))"
-        using tmbound0_I[OF nbe, where b="y" and b'="x"] cp eqs
+      then show ?thesis
+        using tmbound0_I[OF nbe, where b="y" and b'="x"] \<open>?c > 0\<close> eqs
by auto
-    }
-    then have ?case by auto
-  }
-  moreover {
-    assume cp: "?c < 0"
-    {
-      fix x
-      assume xz: "x < -?e / ?c"
-      then have "?c * x > - ?e"
-        using neg_less_divide_eq[OF cp, where a="x" and b="-?e"]
+    qed
+    then show ?thesis by auto
+  next
+    case 3
+    have "Ifm vs (x#bs) (Le (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (Le (CNP 0 c e)))"
+      if "x < -?e / ?c" for x
+    proof -
+      from that have "?c * x > - ?e"
+        using neg_less_divide_eq[OF \<open>?c < 0\<close>, where a="x" and b="-?e"]
then have "?c * x + ?e > 0"
by simp
-      then have "Ifm vs (x#bs) (Le (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (Le (CNP 0 c e)))"
-        using tmbound0_I[OF nbe, where b="y" and b'="x"] cp eqs
+      then show ?thesis
+        using tmbound0_I[OF nbe, where b="y" and b'="x"] \<open>?c < 0\<close> eqs
by auto
-    }
-    then have ?case by auto
-  }
-  ultimately show ?case by blast
+    qed
+    then show ?thesis by auto
+  qed
qed auto

lemma plusinf_inf:
@@ -2173,7 +2185,7 @@
and nmi: "\<not> (Ifm vs (x#bs) (plusinf p))"
and ex: "Ifm vs (x#bs) p" (is "?I x p")
shows "\<exists>(c, s) \<in> set (uset p). x \<le> - Itm vs (x#bs) s / Ipoly vs c"
-proof-
+proof -
have "\<exists>(c, s) \<in> set (uset p).
Ipoly vs c < 0 \<and> Ipoly vs c * x \<ge> - Itm vs (x#bs) s \<or>
Ipoly vs c > 0 \<and> Ipoly vs c * x \<le> - Itm vs (x#bs) s"
@@ -3379,7 +3391,7 @@
qed

lemma simpfm_lin:
-  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
+  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
shows "qfree p \<Longrightarrow> islin (simpfm p)"
by (induct p rule: simpfm.induct) (auto simp add: conj_lin disj_lin)

@@ -3704,7 +3716,7 @@
(auto simp add: msubsteq2_nb msubstltpos_nb msubstlepos_nb)

lemma msubstneg_nb:
-  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
+  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
and lp: "islin p"
and tnb: "tmbound0 t"
shows "bound0 (msubstneg p c t)"
@@ -3713,7 +3725,7 @@
(auto simp add: msubsteq2_nb msubstltneg_nb msubstleneg_nb)

lemma msubst2_nb:
-  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
+  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
and lp: "islin p"
and tnb: "tmbound0 t"
shows "bound0 (msubst2 p c t)"
@@ -4196,7 +4208,7 @@
Parametric_Ferrante_Rackoff.method true
\<close> "parametric QE for linear Arithmetic over fields, Version 2"

-lemma "\<exists>(x::'a::{linordered_field}). y \<noteq> -1 \<longrightarrow> (y + 1) * x < 0"
+lemma "\<exists>(x::'a::linordered_field). y \<noteq> -1 \<longrightarrow> (y + 1) * x < 0"
apply (frpar type: 'a pars: y)
apply (rule spec[where x=y])
@@ -4204,7 +4216,7 @@
apply simp
done

-lemma "\<exists>(x::'a::{linordered_field}). y \<noteq> -1 \<longrightarrow> (y + 1)*x < 0"
+lemma "\<exists>(x::'a::linordered_field). y \<noteq> -1 \<longrightarrow> (y + 1)*x < 0"
apply (frpar2 type: 'a pars: y)
apply (rule spec[where x=y])
@@ -4212,10 +4224,10 @@
apply simp
done

-text\<open>Collins/Jones Problem\<close>
+text \<open>Collins/Jones Problem\<close>
(*
lemma "\<exists>(r::'a::{linordered_field, number_ring}). 0 < r \<and> r < 1 \<and> 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \<and> (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0"
-proof-
+proof -
have "(\<exists>(r::'a::{linordered_field, number_ring}). 0 < r \<and> r < 1 \<and> 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \<and> (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0) \<longleftrightarrow> (\<exists>(r::'a::{linordered_field, number_ring}). 0 < r \<and> r < 1 \<and> 0 < 2 *(a^2 + b^2) - (3*(a^2 + b^2)) * r + (2*a)*r \<and> 2*(a^2 + b^2) - (3*(a^2 + b^2) - 4*a + 1)*r - 2*a < 0)" (is "?lhs \<longleftrightarrow> ?rhs")
have "?rhs"
@@ -4230,11 +4242,11 @@
oops
*)

-text\<open>Collins/Jones Problem\<close>
+text \<open>Collins/Jones Problem\<close>

(*
lemma "\<exists>(r::'a::{linordered_field, number_ring}). 0 < r \<and> r < 1 \<and> 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \<and> (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0"
-proof-
+proof -
have "(\<exists>(r::'a::{linordered_field, number_ring}). 0 < r \<and> r < 1 \<and> 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \<and> (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0) \<longleftrightarrow> (\<exists>(r::'a::{linordered_field, number_ring}). 0 < r \<and> r < 1 \<and> 0 < 2 *(a^2 + b^2) - (3*(a^2 + b^2)) * r + (2*a)*r \<and> 2*(a^2 + b^2) - (3*(a^2 + b^2) - 4*a + 1)*r - 2*a < 0)" (is "?lhs \<longleftrightarrow> ?rhs")