1.1 --- a/src/HOL/ex/Reflected_Presburger.thy	Mon Jun 11 11:06:00 2007 +0200
     1.2 +++ b/src/HOL/ex/Reflected_Presburger.thy	Mon Jun 11 11:06:04 2007 +0200
     1.3 @@ -46,13 +46,16 @@
     1.4    by auto
     1.5  
     1.6  (* Periodicity of dvd *)
     1.7 +
     1.8  lemma dvd_period:
     1.9    assumes advdd: "(a::int) dvd d"
    1.10    shows "(a dvd (x + t)) = (a dvd ((x+ c*d) + t))"
    1.11    using advdd  
    1.12  proof-
    1.13 -  from advdd  have "\<forall>x.\<forall>k. (((a::int) dvd (x + t)) = (a dvd (x+k*d + t)))" 
    1.14 -    by (rule dvd_modd_pinf)
    1.15 +  {fix x k
    1.16 +    from inf_period(3)[OF advdd, rule_format, where x=x and k="-k"]  
    1.17 +    have " ((a::int) dvd (x + t)) = (a dvd (x+k*d + t))" by simp}
    1.18 +  hence "\<forall>x.\<forall>k. ((a::int) dvd (x + t)) = (a dvd (x+k*d + t))"  by simp
    1.19    then show ?thesis by simp
    1.20  qed
    1.21  
    1.22 @@ -637,7 +640,8 @@
    1.23    moreover 
    1.24    {assume i1: "abs i = 1"
    1.25        from zdvd_1_left[where m = "Inum bs a"] uminus_dvd_conv[where d="1" and t="Inum bs a"]
    1.26 -      have ?case using i1 by (cases "i=0", simp_all add: Let_def) arith}
    1.27 +      have ?case using i1 apply (cases "i=0", simp_all add: Let_def) 
    1.28 +	by (cases "i > 0", simp_all)}
    1.29    moreover   
    1.30    {assume inz: "i\<noteq>0" and cond: "abs i \<noteq> 1"
    1.31      {fix v assume "?sa = C v" hence ?case using sa[symmetric] inz cond
    1.32 @@ -656,7 +660,8 @@
    1.33    moreover 
    1.34    {assume i1: "abs i = 1"
    1.35        from zdvd_1_left[where m = "Inum bs a"] uminus_dvd_conv[where d="1" and t="Inum bs a"]
    1.36 -      have ?case using i1 by (cases "i=0", simp_all add: Let_def) arith}
    1.37 +      have ?case using i1 apply (cases "i=0", simp_all add: Let_def)
    1.38 +      apply (cases "i > 0", simp_all) done}
    1.39    moreover   
    1.40    {assume inz: "i\<noteq>0" and cond: "abs i \<noteq> 1"
    1.41      {fix v assume "?sa = C v" hence ?case using sa[symmetric] inz cond
    1.42 @@ -727,12 +732,6 @@
    1.43  by(induct p rule: qelim.induct) 
    1.44  (auto simp add: not disj conj iff imp not_qf disj_qf conj_qf imp_qf iff_qf 
    1.45    simpfm simpfm_qf simp del: simpfm.simps)
    1.46 -
    1.47 -
    1.48 -
    1.49 -    (**********************************************************************************)
    1.50 -    (*******                             THE \<int>-PART                                 ***)
    1.51 -    (**********************************************************************************)
    1.52    (* Linearity for fm where Bound 0 ranges over \<int> *)
    1.53  consts
    1.54    zsplit0 :: "num \<Rightarrow> int \<times> num" (* splits the bounded from the unbounded part*)
    1.55 @@ -1335,7 +1334,7 @@
    1.56    from \<delta> [OF lin] have dpos: "?d >0" by simp
    1.57    from \<delta> [OF lin] have alld: "d\<delta> p ?d" by simp
    1.58    from minusinf_repeats[OF alld lin] have th1:"\<forall> x k. ?P x = ?P (x - (k * ?d))" by simp
    1.59 -  from minf_vee[OF dpos th1] show ?thesis by blast
    1.60 +  from periodic_finite_ex[OF dpos th1] show ?thesis by blast
    1.61  qed
    1.62  
    1.63  
    1.64 @@ -1690,6 +1689,27 @@
    1.65      by auto
    1.66    from  \<beta>[OF lp u d dp nb2 px] show "?P (x -d )" .
    1.67  qed
    1.68 +lemma cpmi_eq: "0 < D \<Longrightarrow> (EX z::int. ALL x. x < z --> (P x = P1 x))
    1.69 +==> ALL x.~(EX (j::int) : {1..D}. EX (b::int) : B. P(b+j)) --> P (x) --> P (x - D) 
    1.70 +==> (ALL (x::int). ALL (k::int). ((P1 x)= (P1 (x-k*D))))
    1.71 +==> (EX (x::int). P(x)) = ((EX (j::int) : {1..D} . (P1(j))) | (EX (j::int) : {1..D}. EX (b::int) : B. P (b+j)))"
    1.72 +apply(rule iffI)
    1.73 +prefer 2
    1.74 +apply(drule minusinfinity)
    1.75 +apply assumption+
    1.76 +apply(fastsimp)
    1.77 +apply clarsimp
    1.78 +apply(subgoal_tac "!!k. 0<=k \<Longrightarrow> !x. P x \<longrightarrow> P (x - k*D)")
    1.79 +apply(frule_tac x = x and z=z in decr_lemma)
    1.80 +apply(subgoal_tac "P1(x - (\<bar>x - z\<bar> + 1) * D)")
    1.81 +prefer 2
    1.82 +apply(subgoal_tac "0 <= (\<bar>x - z\<bar> + 1)")
    1.83 +prefer 2 apply arith
    1.84 + apply fastsimp
    1.85 +apply(drule (1)  periodic_finite_ex)
    1.86 +apply blast
    1.87 +apply(blast dest:decr_mult_lemma)
    1.88 +done
    1.89  
    1.90  theorem cp_thm:
    1.91    assumes lp: "iszlfm p"
    1.92 @@ -1880,8 +1900,8 @@
    1.93  
    1.94  theorem mirqe: "(Ifm bbs bs (pa p) = Ifm bbs bs p) \<and> qfree (pa p)"
    1.95    using qelim_ci cooper prep by (auto simp add: pa_def)
    1.96 +declare zdvd_iff_zmod_eq_0 [code]
    1.97  
    1.98 -declare zdvd_iff_zmod_eq_0 [code] 
    1.99  code_module GeneratedCooper
   1.100  file "generated_cooper.ML"
   1.101  contains pa = "pa"