--- a/src/HOL/Decision_Procs/MIR.thy Fri Nov 13 16:17:30 2015 +0100
+++ b/src/HOL/Decision_Procs/MIR.thy Fri Nov 13 15:59:40 2015 +0000
@@ -3452,7 +3452,7 @@
ultimately have "?I (?p (p',n',s') j) \<longrightarrow> (?N (Floor a) = ?N ((Add (Floor s') (C j))))"
by blast
with s_def n0 p_def nb nf have ?ths by auto}
- ultimately show ?ths by auto
+ ultimately show ?ths by fastforce
qed
next
case (3 a b) then show ?case
@@ -5647,13 +5647,17 @@
end;
\<close>
+lemmas iff_real_of_int = of_int_eq_iff [where 'a = real, symmetric]
+ of_int_less_iff [where 'a = real, symmetric]
+ of_int_le_iff [where 'a = real, symmetric]
+
ML_file "mir_tac.ML"
method_setup mir = \<open>
Scan.lift (Args.mode "no_quantify") >>
(fn q => fn ctxt => SIMPLE_METHOD' (Mir_Tac.mir_tac ctxt (not q)))
\<close> "decision procedure for MIR arithmetic"
-(*FIXME
+
lemma "\<forall>x::real. (\<lfloor>x\<rfloor> = \<lceil>x\<rceil> \<longleftrightarrow> (x = real_of_int \<lfloor>x\<rfloor>))"
by mir
@@ -5668,6 +5672,6 @@
lemma "\<forall>(x::real) (y::real). \<lfloor>x\<rfloor> = \<lfloor>y\<rfloor> \<longrightarrow> 0 \<le> abs (y - x) \<and> abs (y - x) \<le> 1"
by mir
-*)
+
end
--- a/src/HOL/Decision_Procs/mir_tac.ML Fri Nov 13 16:17:30 2015 +0100
+++ b/src/HOL/Decision_Procs/mir_tac.ML Fri Nov 13 15:59:40 2015 +0000
@@ -11,9 +11,8 @@
struct
val mir_ss =
-let val ths = [@{thm "of_int_eq_iff"}, @{thm "of_int_less_iff"}, @{thm "of_int_le_iff"}]
-in simpset_of (@{context} delsimps ths addsimps (map (fn th => th RS sym) ths))
-end;
+ simpset_of (@{context} delsimps [@{thm "of_int_eq_iff"}, @{thm "of_int_less_iff"}, @{thm "of_int_le_iff"}]
+ addsimps @{thms "iff_real_of_int"});
val nT = HOLogic.natT;
val nat_arith = [@{thm diff_nat_numeral}];
@@ -30,8 +29,7 @@
@{thm "divide_divide_eq_left"}, @{thm "times_divide_eq_right"},
@{thm "times_divide_eq_left"}, @{thm "divide_divide_eq_right"},
@{thm uminus_add_conv_diff [symmetric]}, @{thm "minus_divide_left"}]
-val comp_ths = ths @ comp_arith @ @{thms simp_thms};
-
+val comp_ths = distinct Thm.eq_thm (ths @ comp_arith @ @{thms simp_thms});
val mod_div_equality' = @{thm "mod_div_equality'"};
val mod_add_eq = @{thm "mod_add_eq"} RS sym;