# HG changeset patch
# User chaieb
# Date 1196624322 3600
# Node ID 32a5f675a85df680500dfb2c50e253a00dc086d2
# Parent 4b508bb31a6c1981552f9a6065737327467344fa
Eliminated unused theorems minusinf_ex and minusinf_bex
diff r 4b508bb31a6c r 32a5f675a85d src/HOL/ex/Reflected_Presburger.thy
 a/src/HOL/ex/Reflected_Presburger.thy Fri Nov 30 20:13:08 2007 +0100
+++ b/src/HOL/ex/Reflected_Presburger.thy Sun Dec 02 20:38:42 2007 +0100
@@ 1338,35 +1338,6 @@
qed
qed (auto simp add: gr0_conv_Suc numbound0_I[where bs="bs" and b="x  k*d" and b'="x"])
 (* Is'nt this beautiful?*)
lemma minusinf_ex:
 assumes lin: "iszlfm p" and u: "d\ p 1"
 and exmi: "\ (x::int). Ifm bbs (x#bs) (minusinf p)" (is "\ x. ?P1 x")
 shows "\ (x::int). Ifm bbs (x#bs) p" (is "\ x. ?P x")
proof
 let ?d = "\ p"
 from \ [OF lin] have dpos: "?d >0" by simp
 from \ [OF lin] have alld: "d\ p ?d" by simp
 from minusinf_repeats[OF alld lin] have th1:"\ x k. ?P1 x = ?P1 (x  (k * ?d))" by simp
 from minusinf_inf[OF lin u] have th2:"\ z. \ x. x (?P x = ?P1 x)" by blast
 from minusinfinity [OF dpos th1 th2] exmi show ?thesis by blast
qed

 (* And This ???*)
lemma minusinf_bex:
 assumes lin: "iszlfm p"
 shows "(\ (x::int). Ifm bbs (x#bs) (minusinf p)) =
 (\ (x::int)\ {1..\ p}. Ifm bbs (x#bs) (minusinf p))"
 (is "(\ x. ?P x) = _")
proof
 let ?d = "\ p"
 from \ [OF lin] have dpos: "?d >0" by simp
 from \ [OF lin] have alld: "d\ p ?d" by simp
 from minusinf_repeats[OF alld lin] have th1:"\ x k. ?P x = ?P (x  (k * ?d))" by simp
 from periodic_finite_ex[OF dpos th1] show ?thesis by blast
qed


lemma mirror\\:
assumes lp: "iszlfm p"
shows "(Inum (i#bs)) ` set (\ p) = (Inum (i#bs)) ` set (\ (mirror p))"