src/HOL/ex/Reflected_Presburger.thy
changeset 25515 32a5f675a85d
parent 25162 ad4d5365d9d8
child 25592 e8ddaf6bf5df
equal deleted inserted replaced
25514:4b508bb31a6c 25515:32a5f675a85d
  1335       hence "\<exists> (l::int). c*x - c * (k*d) +?e = i*l"
  1335       hence "\<exists> (l::int). c*x - c * (k*d) +?e = i*l"
  1336 	by blast
  1336 	by blast
  1337       thus "i dvd c*x - c*(k*d) + Inum (x # bs) e" by (simp add: dvd_def)
  1337       thus "i dvd c*x - c*(k*d) + Inum (x # bs) e" by (simp add: dvd_def)
  1338     qed
  1338     qed
  1339 qed (auto simp add: gr0_conv_Suc numbound0_I[where bs="bs" and b="x - k*d" and b'="x"])
  1339 qed (auto simp add: gr0_conv_Suc numbound0_I[where bs="bs" and b="x - k*d" and b'="x"])
  1340 
       
  1341     (* Is'nt this beautiful?*)
       
  1342 lemma minusinf_ex:
       
  1343   assumes lin: "iszlfm p" and u: "d\<beta> p 1"
       
  1344   and exmi: "\<exists> (x::int). Ifm bbs (x#bs) (minusinf p)" (is "\<exists> x. ?P1 x")
       
  1345   shows "\<exists> (x::int). Ifm bbs (x#bs) p" (is "\<exists> x. ?P x")
       
  1346 proof-
       
  1347   let ?d = "\<delta> p"
       
  1348   from \<delta> [OF lin] have dpos: "?d >0" by simp
       
  1349   from \<delta> [OF lin] have alld: "d\<delta> p ?d" by simp
       
  1350   from minusinf_repeats[OF alld lin] have th1:"\<forall> x k. ?P1 x = ?P1 (x - (k * ?d))" by simp
       
  1351   from minusinf_inf[OF lin u] have th2:"\<exists> z. \<forall> x. x<z \<longrightarrow> (?P x = ?P1 x)" by blast
       
  1352   from minusinfinity [OF dpos th1 th2] exmi show ?thesis by blast
       
  1353 qed
       
  1354 
       
  1355     (*	And This ???*)
       
  1356 lemma minusinf_bex:
       
  1357   assumes lin: "iszlfm p"
       
  1358   shows "(\<exists> (x::int). Ifm bbs (x#bs) (minusinf p)) = 
       
  1359          (\<exists> (x::int)\<in> {1..\<delta> p}. Ifm bbs (x#bs) (minusinf p))"
       
  1360   (is "(\<exists> x. ?P x) = _")
       
  1361 proof-
       
  1362   let ?d = "\<delta> p"
       
  1363   from \<delta> [OF lin] have dpos: "?d >0" by simp
       
  1364   from \<delta> [OF lin] have alld: "d\<delta> p ?d" by simp
       
  1365   from minusinf_repeats[OF alld lin] have th1:"\<forall> x k. ?P x = ?P (x - (k * ?d))" by simp
       
  1366   from periodic_finite_ex[OF dpos th1] show ?thesis by blast
       
  1367 qed
       
  1368 
       
  1369 
  1340 
  1370 lemma mirror\<alpha>\<beta>:
  1341 lemma mirror\<alpha>\<beta>:
  1371   assumes lp: "iszlfm p"
  1342   assumes lp: "iszlfm p"
  1372   shows "(Inum (i#bs)) ` set (\<alpha> p) = (Inum (i#bs)) ` set (\<beta> (mirror p))"
  1343   shows "(Inum (i#bs)) ` set (\<alpha> p) = (Inum (i#bs)) ` set (\<beta> (mirror p))"
  1373 using lp
  1344 using lp