src/HOL/ex/Reflected_Presburger.thy
 changeset 25515 32a5f675a85d parent 25162 ad4d5365d9d8 child 25592 e8ddaf6bf5df
equal 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"])`
`  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`