src/HOL/Decision_Procs/MIR.thy
 changeset 63600 d0fa16751d14 parent 62342 1cf129590be8 child 64240 eabf80376aab
equal inserted replaced
63599:f560147710fb 63600:d0fa16751d14
`  1524   have th': "(real_of_int ?nt)*(real_of_int x) = real_of_int (?nt * x)" by simp`
`  1524   have th': "(real_of_int ?nt)*(real_of_int x) = real_of_int (?nt * x)" by simp`
`  1525   have "?I x (Floor t) = ?I x (Floor (CN 0 ?nt ?at))" using th2 by simp`
`  1525   have "?I x (Floor t) = ?I x (Floor (CN 0 ?nt ?at))" using th2 by simp`
`  1526   also have "\<dots> = real_of_int \<lfloor>real_of_int ?nt * real_of_int x + ?I x ?at\<rfloor>" by simp`
`  1526   also have "\<dots> = real_of_int \<lfloor>real_of_int ?nt * real_of_int x + ?I x ?at\<rfloor>" by simp`
`  1527   also have "\<dots> = real_of_int \<lfloor>?I x ?at + real_of_int (?nt * x)\<rfloor>" by (simp add: ac_simps)`
`  1527   also have "\<dots> = real_of_int \<lfloor>?I x ?at + real_of_int (?nt * x)\<rfloor>" by (simp add: ac_simps)`
`  1528   also have "\<dots> = real_of_int (\<lfloor>?I x ?at\<rfloor> + (?nt * x))"`
`  1528   also have "\<dots> = real_of_int (\<lfloor>?I x ?at\<rfloor> + (?nt * x))"`
`  1529     using floor_add_of_int[of "?I x ?at" "?nt * x"] by simp`
`  1529     by (simp add: of_int_mult[symmetric] del: of_int_mult)`
`  1530   also have "\<dots> = real_of_int (?nt)*(real_of_int x) + real_of_int \<lfloor>?I x ?at\<rfloor>" by (simp add: ac_simps)`
`  1530   also have "\<dots> = real_of_int (?nt)*(real_of_int x) + real_of_int \<lfloor>?I x ?at\<rfloor>" by (simp add: ac_simps)`
`  1531   finally have "?I x (Floor t) = ?I x (CN 0 n a)" using th by simp`
`  1531   finally have "?I x (Floor t) = ?I x (CN 0 n a)" using th by simp`
`  1532   with na show ?case by simp`
`  1532   with na show ?case by simp`
`  1533 qed`
`  1533 qed`
`  1534 `
`  1534 `