1.1 --- a/src/HOL/ex/Reflected_Presburger.thy	Fri Nov 30 20:13:08 2007 +0100
     1.2 +++ b/src/HOL/ex/Reflected_Presburger.thy	Sun Dec 02 20:38:42 2007 +0100
     1.3 @@ -1338,35 +1338,6 @@
     1.4      qed
     1.5  qed (auto simp add: gr0_conv_Suc numbound0_I[where bs="bs" and b="x - k*d" and b'="x"])
     1.6  
     1.7 -    (* Is'nt this beautiful?*)
     1.8 -lemma minusinf_ex:
     1.9 -  assumes lin: "iszlfm p" and u: "d\<beta> p 1"
    1.10 -  and exmi: "\<exists> (x::int). Ifm bbs (x#bs) (minusinf p)" (is "\<exists> x. ?P1 x")
    1.11 -  shows "\<exists> (x::int). Ifm bbs (x#bs) p" (is "\<exists> x. ?P x")
    1.12 -proof-
    1.13 -  let ?d = "\<delta> p"
    1.14 -  from \<delta> [OF lin] have dpos: "?d >0" by simp
    1.15 -  from \<delta> [OF lin] have alld: "d\<delta> p ?d" by simp
    1.16 -  from minusinf_repeats[OF alld lin] have th1:"\<forall> x k. ?P1 x = ?P1 (x - (k * ?d))" by simp
    1.17 -  from minusinf_inf[OF lin u] have th2:"\<exists> z. \<forall> x. x<z \<longrightarrow> (?P x = ?P1 x)" by blast
    1.18 -  from minusinfinity [OF dpos th1 th2] exmi show ?thesis by blast
    1.19 -qed
    1.20 -
    1.21 -    (*	And This ???*)
    1.22 -lemma minusinf_bex:
    1.23 -  assumes lin: "iszlfm p"
    1.24 -  shows "(\<exists> (x::int). Ifm bbs (x#bs) (minusinf p)) = 
    1.25 -         (\<exists> (x::int)\<in> {1..\<delta> p}. Ifm bbs (x#bs) (minusinf p))"
    1.26 -  (is "(\<exists> x. ?P x) = _")
    1.27 -proof-
    1.28 -  let ?d = "\<delta> p"
    1.29 -  from \<delta> [OF lin] have dpos: "?d >0" by simp
    1.30 -  from \<delta> [OF lin] have alld: "d\<delta> p ?d" by simp
    1.31 -  from minusinf_repeats[OF alld lin] have th1:"\<forall> x k. ?P x = ?P (x - (k * ?d))" by simp
    1.32 -  from periodic_finite_ex[OF dpos th1] show ?thesis by blast
    1.33 -qed
    1.34 -
    1.35 -
    1.36  lemma mirror\<alpha>\<beta>:
    1.37    assumes lp: "iszlfm p"
    1.38    shows "(Inum (i#bs)) ` set (\<alpha> p) = (Inum (i#bs)) ` set (\<beta> (mirror p))"