src/HOL/Decision_Procs/Cooper.thy
changeset 49962 a8cc904a6820
parent 48891 c0eafbd55de3
child 50252 4aa34bd43228
     1.1 --- a/src/HOL/Decision_Procs/Cooper.thy	Fri Oct 19 10:46:42 2012 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Cooper.thy	Fri Oct 19 15:12:52 2012 +0200
     1.3 @@ -413,7 +413,7 @@
     1.4  apply (case_tac "c1+c2 = 0",case_tac "n1 \<le> n2", simp_all)
     1.5   apply (case_tac "n1 = n2")
     1.6    apply(simp_all add: algebra_simps)
     1.7 -apply(simp add: left_distrib[symmetric])
     1.8 +apply(simp add: distrib_right[symmetric])
     1.9  done
    1.10  
    1.11  lemma numadd_nb: "\<lbrakk> numbound0 t ; numbound0 s\<rbrakk> \<Longrightarrow> numbound0 (numadd (t,s))"
    1.12 @@ -727,7 +727,7 @@
    1.13        by (simp add: Let_def split_def)
    1.14      from abj 3 m0 have th2: "(?I x (CN 0 ?j ?b) = ?I x a) \<and> ?N ?b" by blast
    1.15      from th have "?I x (CN 0 n a') = ?I x (CN 0 (i+?j) ?b)" by simp
    1.16 -    also from th2 have "\<dots> = ?I x (CN 0 i (CN 0 ?j ?b))" by (simp add: left_distrib)
    1.17 +    also from th2 have "\<dots> = ?I x (CN 0 i (CN 0 ?j ?b))" by (simp add: distrib_right)
    1.18    finally have "?I x (CN 0 n a') = ?I  x (CN 0 i a)" using th2 by simp
    1.19    with th2 th have ?case using m0 by blast} 
    1.20  ultimately show ?case by blast
    1.21 @@ -754,7 +754,7 @@
    1.22    with bluddy abjt have th3: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast
    1.23    from abjs 5 have th2: "(?I x (CN 0 ?ns ?as) = ?I x s) \<and> ?N ?as" by blast
    1.24    from th3[simplified] th2[simplified] th[simplified] show ?case 
    1.25 -    by (simp add: left_distrib)
    1.26 +    by (simp add: distrib_right)
    1.27  next
    1.28    case (6 s t n a)
    1.29    let ?ns = "fst (zsplit0 s)"
    1.30 @@ -779,7 +779,7 @@
    1.31      by (simp add: Let_def split_def)
    1.32    from abj 7 have th2: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast
    1.33    hence "?I x (Mul i t) = i * ?I x (CN 0 ?nt ?at)" by simp
    1.34 -  also have "\<dots> = ?I x (CN 0 (i*?nt) (Mul i ?at))" by (simp add: right_distrib)
    1.35 +  also have "\<dots> = ?I x (CN 0 (i*?nt) (Mul i ?at))" by (simp add: distrib_left)
    1.36    finally show ?case using th th2 by simp
    1.37  qed
    1.38