Theory MIR
theory MIR
imports Complex_Main Dense_Linear_Order DP_Library
"HOL-Library.Code_Target_Numeral" "HOL-Library.Old_Recdef"
begin
section ‹Prelude›
abbreviation (input) UNION :: "'a set ⇒ ('a ⇒ 'b set) ⇒ 'b set"
where "UNION A f ≡ ⋃ (f ` A)"
section ‹Quantifier elimination for ‹ℝ (0, 1, +, floor, <)››
declare of_int_floor_cancel [simp del]
lemma myle:
fixes a b :: "'a::{ordered_ab_group_add}"
shows "(a ≤ b) = (0 ≤ b - a)"
by (metis add_0_left add_le_cancel_right diff_add_cancel)
lemma myless:
fixes a b :: "'a::{ordered_ab_group_add}"
shows "(a < b) = (0 < b - a)"
by (metis le_iff_diff_le_0 less_le_not_le myle)
lemmas dvd_period = zdvd_period
definition rdvd:: "real ⇒ real ⇒ bool" (infixl "rdvd" 50)
where "x rdvd y ⟷ (∃k::int. y = x * real_of_int k)"
lemma int_rdvd_real:
"real_of_int (i::int) rdvd x = (i dvd ⌊x⌋ ∧ real_of_int ⌊x⌋ = x)" (is "?l = ?r")
proof
assume "?l"
hence th: "∃ k. x=real_of_int (i*k)" by (simp add: rdvd_def)
hence th': "real_of_int ⌊x⌋ = x" by (auto simp del: of_int_mult)
with th have "∃ k. real_of_int ⌊x⌋ = real_of_int (i*k)" by simp
hence "∃k. ⌊x⌋ = i*k" by presburger
thus ?r using th' by (simp add: dvd_def)
next
assume "?r" hence "(i::int) dvd ⌊x::real⌋" ..
hence "∃k. real_of_int ⌊x⌋ = real_of_int (i*k)"
by (metis (no_types) dvd_def)
thus ?l using ‹?r› by (simp add: rdvd_def)
qed
lemma int_rdvd_iff: "(real_of_int (i::int) rdvd real_of_int t) = (i dvd t)"
by (auto simp add: rdvd_def dvd_def) (rule_tac x="k" in exI, simp only: of_int_mult[symmetric])
lemma rdvd_abs1: "(¦real_of_int d¦ rdvd t) = (real_of_int (d ::int) rdvd t)"
proof
assume d: "real_of_int d rdvd t"
from d int_rdvd_real have d2: "d dvd ⌊t⌋" and ti: "real_of_int ⌊t⌋ = t"
by auto
from iffD2[OF abs_dvd_iff] d2 have "¦d¦ dvd ⌊t⌋" by blast
with ti int_rdvd_real[symmetric] have "real_of_int ¦d¦ rdvd t" by blast
thus "¦real_of_int d¦ rdvd t" by simp
next
assume "¦real_of_int d¦ rdvd t" hence "real_of_int ¦d¦ rdvd t" by simp
with int_rdvd_real[where i="¦d¦" and x="t"]
have d2: "¦d¦ dvd ⌊t⌋" and ti: "real_of_int ⌊t⌋ = t"
by auto
from iffD1[OF abs_dvd_iff] d2 have "d dvd ⌊t⌋" by blast
with ti int_rdvd_real[symmetric] show "real_of_int d rdvd t" by blast
qed
lemma rdvd_minus: "(real_of_int (d::int) rdvd t) = (real_of_int d rdvd -t)"
apply (auto simp add: rdvd_def)
apply (rule_tac x="-k" in exI, simp)
apply (rule_tac x="-k" in exI, simp)
done
lemma rdvd_left_0_eq: "(0 rdvd t) = (t=0)"
by (auto simp add: rdvd_def)
lemma rdvd_mult:
assumes knz: "k≠0"
shows "(real_of_int (n::int) * real_of_int (k::int) rdvd x * real_of_int k) = (real_of_int n rdvd x)"
using knz by (simp add: rdvd_def)