# HG changeset patch
# User chaieb
# Date 1181552771 -7200
# Node ID 26c978a475de554cac83fd4617457104ad6b459c
# Parent  df3a7e9ebadba81ee91ea17141bc4d6c1fe3d9b1
tuned  Proof and Document

diff -r df3a7e9ebadb -r 26c978a475de src/HOL/Complex/ex/MIR.thy
--- a/src/HOL/Complex/ex/MIR.thy	Mon Jun 11 11:06:04 2007 +0200
+++ b/src/HOL/Complex/ex/MIR.thy	Mon Jun 11 11:06:11 2007 +0200
@@ -98,8 +98,10 @@
   shows "(a dvd (x + t)) = (a dvd ((x+ c*d) + t))"
   using advdd  
 proof-
-  from advdd  have "\<forall>x.\<forall>k. (((a::int) dvd (x + t)) = (a dvd (x+k*d + t)))" 
-    by (rule dvd_modd_pinf)
+  {fix x k
+    from inf_period(3)[OF advdd, rule_format, where x=x and k="-k"]  
+    have " ((a::int) dvd (x + t)) = (a dvd (x+k*d + t))" by simp}
+  hence "\<forall>x.\<forall>k. ((a::int) dvd (x + t)) = (a dvd (x+k*d + t))"  by simp
   then show ?thesis by simp
 qed
 
@@ -1550,11 +1552,8 @@
 (auto simp del: simpfm.simps)
 
 
-
-    (**********************************************************************************)
-    (*******                             THE \<int>-PART                                 ***)
-    (**********************************************************************************)
-  (* Linearity for fm where Bound 0 ranges over \<int> *)
+text {* The @{text "\<int>"} Part *}
+text{* Linearity for fm where Bound 0 ranges over @{text "\<int>"} *}
 consts
   zsplit0 :: "num \<Rightarrow> int \<times> num" (* splits the bounded from the unbounded part*)
 recdef zsplit0 "measure num_size"
@@ -2060,11 +2059,16 @@
   ultimately show ?case by blast
 qed auto
 
+text{* 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*}
+
 consts 
-  plusinf:: "fm \<Rightarrow> fm" (* Virtual substitution of +\<infinity>*)
-  minusinf:: "fm \<Rightarrow> fm" (* Virtual substitution of -\<infinity>*)
-  \<delta> :: "fm \<Rightarrow> int" (* Compute lcm {d| N\<^isup>?\<^isup> Dvd c*x+t \<in> p}*)
-  d\<delta> :: "fm \<Rightarrow> int \<Rightarrow> bool" (* checks if a given l divides all the ds above*)
+  plusinf:: "fm \<Rightarrow> fm" 
+  minusinf:: "fm \<Rightarrow> fm"
+  \<delta> :: "fm \<Rightarrow> int" 
+  d\<delta> :: "fm \<Rightarrow> int \<Rightarrow> bool"
 
 recdef minusinf "measure size"
   "minusinf (And p q) = conj (minusinf p) (minusinf q)" 
@@ -2317,7 +2321,6 @@
     qed
 qed (auto simp add: nth_pos2 numbound0_I[where bs="bs" and b="real(x - k*d)" and b'="real x"] simp del: real_of_int_mult real_of_int_diff)
 
-    (* Is'nt this beautiful?*)
 lemma minusinf_ex:
   assumes lin: "iszlfm p (real (a::int) #bs)"
   and exmi: "\<exists> (x::int). Ifm (real x#bs) (minusinf p)" (is "\<exists> x. ?P1 x")
@@ -2331,7 +2334,6 @@
   from minusinfinity [OF dpos th1 th2] exmi show ?thesis by blast
 qed
 
-    (*	And This ???*)
 lemma minusinf_bex:
   assumes lin: "iszlfm p (real (a::int) #bs)"
   shows "(\<exists> (x::int). Ifm (real x#bs) (minusinf p)) = 
@@ -2342,10 +2344,9 @@
   from \<delta> [OF lin] have dpos: "?d >0" by simp
   from \<delta> [OF lin] have alld: "d\<delta> p ?d" by simp
   from minusinf_repeats[OF alld lin] have th1:"\<forall> x k. ?P x = ?P (x - (k * ?d))" by simp
-  from minf_vee[OF dpos th1] show ?thesis by blast
+  from periodic_finite_ex[OF dpos th1] show ?thesis by blast
 qed
 
-    (* Lemmas for the correctness of \<sigma>\<rho> *)
 lemma dvd1_eq1: "x >0 \<Longrightarrow> (x::int) dvd 1 = (x = 1)" by auto
 
 consts 
@@ -2831,6 +2832,29 @@
   shows "\<forall> b\<in> set (\<beta> p). isint b bs"
 using lp by (induct p rule: iszlfm.induct) (auto simp add: isint_neg isint_sub)
 
+lemma cpmi_eq: "0 < D \<Longrightarrow> (EX z::int. ALL x. x < z --> (P x = P1 x))
+==> ALL x.~(EX (j::int) : {1..D}. EX (b::int) : B. P(b+j)) --> P (x) --> P (x - D) 
+==> (ALL (x::int). ALL (k::int). ((P1 x)= (P1 (x-k*D))))
+==> (EX (x::int). P(x)) = ((EX (j::int) : {1..D} . (P1(j))) | (EX (j::int) : {1..D}. EX (b::int) : B. P (b+j)))"
+apply(rule iffI)
+prefer 2
+apply(drule minusinfinity)
+apply assumption+
+apply(fastsimp)
+apply clarsimp
+apply(subgoal_tac "!!k. 0<=k \<Longrightarrow> !x. P x \<longrightarrow> P (x - k*D)")
+apply(frule_tac x = x and z=z in decr_lemma)
+apply(subgoal_tac "P1(x - (\<bar>x - z\<bar> + 1) * D)")
+prefer 2
+apply(subgoal_tac "0 <= (\<bar>x - z\<bar> + 1)")
+prefer 2 apply arith
+ apply fastsimp
+apply(drule (1)  periodic_finite_ex)
+apply blast
+apply(blast dest:decr_mult_lemma)
+done
+
+
 theorem cp_thm:
   assumes lp: "iszlfm p (a #bs)"
   and u: "d\<beta> p 1"
@@ -2861,8 +2885,8 @@
 
 
 consts 
-  \<rho> :: "fm \<Rightarrow> (num \<times> int) list" (* Compute the Reddy/Loveland Bset*)
-  \<sigma>\<rho>:: "fm \<Rightarrow> num \<times> int \<Rightarrow> fm" (* Performs the modified substitution of Reddy/Loveland*)
+  \<rho> :: "fm \<Rightarrow> (num \<times> int) list" (* Compute the Reddy and Loveland Bset*)
+  \<sigma>\<rho>:: "fm \<Rightarrow> num \<times> int \<Rightarrow> fm" (* Performs the modified substitution of Reddy and Loveland*)
   \<alpha>\<rho> :: "fm \<Rightarrow> (num\<times>int) list"
   a\<rho> :: "fm \<Rightarrow> int \<Rightarrow> fm"
 recdef \<rho> "measure size"
@@ -3476,14 +3500,9 @@
 using lp
 by (induct p rule: mirror.induct, simp_all add: split_def image_Un )
   
-
-
-    (********************************************************************)
-    (***                     THE \<real>-PART                               ***)
-    (********************************************************************)
-
-
-  (* Linearity for fm where Bound 0 ranges over \<real> *)
+text {* The @{text "\<real>"} part*}
+
+text{* Linearity for fm where Bound 0 ranges over @{text "\<real>"}*}
 consts
   isrlfm :: "fm \<Rightarrow> bool"   (* Linearity test for fm *)
 recdef isrlfm "measure size"
@@ -3506,8 +3525,6 @@
                         (Gt (CN 0 (-n) (Add (Neg s) (Add (Floor s) (C (j + 1)))))))))"
 
   (* splits the bounded from the unbounded part*)
-  (* FIXME: Abscence of simplification of formulae and numeral-terms 
-    here is also a problem!!!!! Redundancy!!!!!*)
 consts rsplit0 :: "num \<Rightarrow> (fm \<times> int \<times> num) list" 
 recdef rsplit0 "measure num_size"
   "rsplit0 (Bound 0) = [(T,1,C 0)]"
@@ -4994,9 +5011,7 @@
   ultimately show "?E" by blast
 qed
 
-    (********************************************************************)
-    (***                     THE OVERALL-PART                         ***)
-    (********************************************************************)
+text{* The overall Part *}
 
 lemma real_ex_int_real01:
   shows "(\<exists> (x::real). P x) = (\<exists> (i::int) (u::real). 0\<le> u \<and> u< 1 \<and> P (real i + u))"
@@ -5067,8 +5082,6 @@
 qed
 
     (* Implement the right hand sides of Cooper's theorem and Ferrante and Rackoff. *)
-  (* NOTE THAT THIS ONLY HOLDS IN THE CONTEXT OF THE MIXED THEORY!!! MAY BE SHOULD ALSO IMPLEMENT FERRANTE AND RACKOFF TO MAKE IT AVAILABLE AS SAND ALONE!!!! *)
-  (* SINCE x is constrained to be between 0 and 1, plusinf and minusinf will always evaluate to False !!!!! *)
 
 constdefs ferrack01:: "fm \<Rightarrow> fm"
   "ferrack01 p \<equiv> (let p' = rlfm(And (And (Ge(CN 0 1 (C 0))) (Lt (CN 0 1 (C (- 1))))) p);
diff -r df3a7e9ebadb -r 26c978a475de src/HOL/Complex/ex/ReflectedFerrack.thy
--- a/src/HOL/Complex/ex/ReflectedFerrack.thy	Mon Jun 11 11:06:04 2007 +0200
+++ b/src/HOL/Complex/ex/ReflectedFerrack.thy	Mon Jun 11 11:06:11 2007 +0200
@@ -5,7 +5,7 @@
 header {* Quatifier elimination for R(0,1,+,<) *}
 
 theory ReflectedFerrack
-  imports GCD Real 
+  imports GCD Real EfficientNat
   uses ("linreif.ML") ("linrtac.ML")
 begin
 
@@ -1759,7 +1759,7 @@
 lemma allpairs_set: "set (allpairs xs ys) = {(x,y). x\<in> set xs \<and> y \<in> set ys}"
 by (induct xs) auto
 
-    (* Implement the right hand sides of Cooper's theorem and Ferrante and Rackoff. *)
+    (* Implement the right hand side of Ferrante and Rackoff's Theorem. *)
 constdefs ferrack:: "fm \<Rightarrow> fm"
   "ferrack p \<equiv> (let p' = rlfm (simpfm p); mp = minusinf p'; pp = plusinf p'
                 in if (mp = T \<or> pp = T) then T else