src/HOL/Decision_Procs/MIR.thy
changeset 68270 2bc921b2159b
parent 67613 ce654b0e6d69
child 69064 5840724b1d71
     1.1 --- a/src/HOL/Decision_Procs/MIR.thy	Thu May 24 22:28:26 2018 +0200
     1.2 +++ b/src/HOL/Decision_Procs/MIR.thy	Thu May 24 09:26:26 2018 +0000
     1.3 @@ -999,7 +999,7 @@
     1.4            using real_of_int_div[OF gpdd] th2 gp0 by simp
     1.5          finally have "?lhs = Inum bs t / real_of_int n" by simp
     1.6          then have ?thesis using nnz g1 g'1 by (simp add: simp_num_pair_def) }
     1.7 -      ultimately have ?thesis by blast }
     1.8 +      ultimately have ?thesis by auto }
     1.9      ultimately have ?thesis by blast }
    1.10    ultimately show ?thesis by blast
    1.11  qed
    1.12 @@ -1031,7 +1031,7 @@
    1.13          have "n div ?g' >0" by simp
    1.14          hence ?thesis using assms g1 g'1
    1.15            by(auto simp add: simp_num_pair_def Let_def reducecoeffh_numbound0)}
    1.16 -      ultimately have ?thesis by blast }
    1.17 +      ultimately have ?thesis by auto }
    1.18      ultimately have ?thesis by blast }
    1.19    ultimately show ?thesis by blast
    1.20  qed
    1.21 @@ -1171,7 +1171,7 @@
    1.22          using rdvd_reduce[OF gpdd gpdgp g'p, where t="?t", simplified div_self[OF gp0]]
    1.23            th2[symmetric] by simp
    1.24        finally have ?thesis by simp  }
    1.25 -    ultimately have ?thesis by blast
    1.26 +    ultimately have ?thesis by auto
    1.27    }
    1.28    ultimately show ?thesis by blast
    1.29  qed
    1.30 @@ -3397,7 +3397,7 @@
    1.31      ((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) Un
    1.32      (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) Un
    1.33      (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0} (\<lambda> (p,n,s). set (?ff (p,n,s)))))"
    1.34 -    using int_cases[rule_format] by blast
    1.35 +    by (auto split: if_splits)
    1.36    also have "\<dots> =
    1.37      ((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). set [(p,0,Floor s)])) Un
    1.38     (UNION {(p,n,s). (p,n,s)\<in> ?SS a\<and>n>0} (\<lambda>(p,n,s). set(map(?f(p,n,s)) [0..n]))) Un
    1.39 @@ -3411,12 +3411,14 @@
    1.40    also have "\<dots> =
    1.41      ((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). {(p,0,Floor s)})) Un
    1.42      (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). {?f(p,n,s) j| j. j\<in> {0 .. n}})) Un
    1.43 -    (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0} (\<lambda> (p,n,s).  {?f(p,n,s) j| j. j\<in> {n .. 0}})))" by blast
    1.44 +    (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0} (\<lambda> (p,n,s).  {?f(p,n,s) j| j. j\<in> {n .. 0}})))"
    1.45 +    by blast
    1.46    finally
    1.47    have FS: "?SS (Floor a) =
    1.48      ((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). {(p,0,Floor s)})) Un
    1.49      (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). {?f(p,n,s) j| j. j\<in> {0 .. n}})) Un
    1.50 -    (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0} (\<lambda> (p,n,s).  {?f(p,n,s) j| j. j\<in> {n .. 0}})))"    by blast
    1.51 +    (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0} (\<lambda> (p,n,s).  {?f(p,n,s) j| j. j\<in> {n .. 0}})))"
    1.52 +    by blast
    1.53    show ?case
    1.54    proof(simp only: FS, clarsimp simp del: Ifm.simps Inum.simps, -)
    1.55      fix p n s
    1.56 @@ -3552,7 +3554,7 @@
    1.57      ((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) Un
    1.58      (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) Un
    1.59      (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0} (\<lambda> (p,n,s). set (?ff (p,n,s)))))"
    1.60 -    using int_cases[rule_format] by blast
    1.61 +    by (auto split: if_splits)
    1.62    also have "\<dots> =
    1.63      ((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). set [(p,0,Floor s)])) Un
    1.64      (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). set (map (?f(p,n,s)) [0..n]))) Un