# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1447430380 0
# Node ID 90c65a81125771c5010c66e49614a297d392f521
# Parent  415e816d3f37fe3f5a65a9836d873b0e2b691a2b
MIR decision procedure again working

diff -r 415e816d3f37 -r 90c65a811257 src/HOL/Decision_Procs/MIR.thy
--- 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
 
diff -r 415e816d3f37 -r 90c65a811257 src/HOL/Decision_Procs/mir_tac.ML
--- 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;