src/HOL/Decision_Procs/MIR.thy
 changeset 64240 eabf80376aab parent 63600 d0fa16751d14 child 64246 15d1ee6e847b
equal inserted replaced
64239:de5cd9217d4c 64240:eabf80376aab
`  4410   from 5 have cp: "c >0" and nb: "numbound0 e" by simp_all`
`  4410   from 5 have cp: "c >0" and nb: "numbound0 e" by simp_all`
`  4411   have "?I ?u (Lt (CN 0 c e)) = (real_of_int c *(?t/?n) + (?N x e) < 0)"`
`  4411   have "?I ?u (Lt (CN 0 c e)) = (real_of_int c *(?t/?n) + (?N x e) < 0)"`
`  4412     using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp`
`  4412     using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp`
`  4413   also have "\<dots> = (?n*(real_of_int c *(?t/?n)) + ?n*(?N x e) < 0)"`
`  4413   also have "\<dots> = (?n*(real_of_int c *(?t/?n)) + ?n*(?N x e) < 0)"`
`  4414     by (simp only: pos_less_divide_eq[OF np, where a="real_of_int c *(?t/?n) + (?N x e)"`
`  4414     by (simp only: pos_less_divide_eq[OF np, where a="real_of_int c *(?t/?n) + (?N x e)"`
`  4415       and b="0", simplified divide_zero_left]) (simp only: algebra_simps)`
`  4415       and b="0", simplified div_0]) (simp only: algebra_simps)`
`  4416   also have "\<dots> = (real_of_int c *?t + ?n* (?N x e) < 0)"`
`  4416   also have "\<dots> = (real_of_int c *?t + ?n* (?N x e) < 0)"`
`  4417     using np by simp`
`  4417     using np by simp`
`  4418   finally show ?case using nbt nb by (simp add: algebra_simps)`
`  4418   finally show ?case using nbt nb by (simp add: algebra_simps)`
`  4419 next`
`  4419 next`
`  4420   case (6 c e)`
`  4420   case (6 c e)`
`  4421   from 6 have cp: "c >0" and nb: "numbound0 e" by simp_all`
`  4421   from 6 have cp: "c >0" and nb: "numbound0 e" by simp_all`
`  4422   have "?I ?u (Le (CN 0 c e)) = (real_of_int c *(?t/?n) + (?N x e) \<le> 0)"`
`  4422   have "?I ?u (Le (CN 0 c e)) = (real_of_int c *(?t/?n) + (?N x e) \<le> 0)"`
`  4423     using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp`
`  4423     using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp`
`  4424   also have "\<dots> = (?n*(real_of_int c *(?t/?n)) + ?n*(?N x e) \<le> 0)"`
`  4424   also have "\<dots> = (?n*(real_of_int c *(?t/?n)) + ?n*(?N x e) \<le> 0)"`
`  4425     by (simp only: pos_le_divide_eq[OF np, where a="real_of_int c *(?t/?n) + (?N x e)"`
`  4425     by (simp only: pos_le_divide_eq[OF np, where a="real_of_int c *(?t/?n) + (?N x e)"`
`  4426       and b="0", simplified divide_zero_left]) (simp only: algebra_simps)`
`  4426       and b="0", simplified div_0]) (simp only: algebra_simps)`
`  4427   also have "\<dots> = (real_of_int c *?t + ?n* (?N x e) \<le> 0)"`
`  4427   also have "\<dots> = (real_of_int c *?t + ?n* (?N x e) \<le> 0)"`
`  4428     using np by simp`
`  4428     using np by simp`
`  4429   finally show ?case using nbt nb by (simp add: algebra_simps)`
`  4429   finally show ?case using nbt nb by (simp add: algebra_simps)`
`  4430 next`
`  4430 next`
`  4431   case (7 c e)`
`  4431   case (7 c e)`
`  4432   from 7 have cp: "c >0" and nb: "numbound0 e" by simp_all`
`  4432   from 7 have cp: "c >0" and nb: "numbound0 e" by simp_all`
`  4433   have "?I ?u (Gt (CN 0 c e)) = (real_of_int c *(?t/?n) + (?N x e) > 0)"`
`  4433   have "?I ?u (Gt (CN 0 c e)) = (real_of_int c *(?t/?n) + (?N x e) > 0)"`
`  4434     using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp`
`  4434     using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp`
`  4435   also have "\<dots> = (?n*(real_of_int c *(?t/?n)) + ?n*(?N x e) > 0)"`
`  4435   also have "\<dots> = (?n*(real_of_int c *(?t/?n)) + ?n*(?N x e) > 0)"`
`  4436     by (simp only: pos_divide_less_eq[OF np, where a="real_of_int c *(?t/?n) + (?N x e)"`
`  4436     by (simp only: pos_divide_less_eq[OF np, where a="real_of_int c *(?t/?n) + (?N x e)"`
`  4437       and b="0", simplified divide_zero_left]) (simp only: algebra_simps)`
`  4437       and b="0", simplified div_0]) (simp only: algebra_simps)`
`  4438   also have "\<dots> = (real_of_int c *?t + ?n* (?N x e) > 0)"`
`  4438   also have "\<dots> = (real_of_int c *?t + ?n* (?N x e) > 0)"`
`  4439     using np by simp`
`  4439     using np by simp`
`  4440   finally show ?case using nbt nb by (simp add: algebra_simps)`
`  4440   finally show ?case using nbt nb by (simp add: algebra_simps)`
`  4441 next`
`  4441 next`
`  4442   case (8 c e)`
`  4442   case (8 c e)`
`  4443   from 8 have cp: "c >0" and nb: "numbound0 e" by simp_all`
`  4443   from 8 have cp: "c >0" and nb: "numbound0 e" by simp_all`
`  4444   have "?I ?u (Ge (CN 0 c e)) = (real_of_int c *(?t/?n) + (?N x e) \<ge> 0)"`
`  4444   have "?I ?u (Ge (CN 0 c e)) = (real_of_int c *(?t/?n) + (?N x e) \<ge> 0)"`
`  4445     using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp`
`  4445     using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp`
`  4446   also have "\<dots> = (?n*(real_of_int c *(?t/?n)) + ?n*(?N x e) \<ge> 0)"`
`  4446   also have "\<dots> = (?n*(real_of_int c *(?t/?n)) + ?n*(?N x e) \<ge> 0)"`
`  4447     by (simp only: pos_divide_le_eq[OF np, where a="real_of_int c *(?t/?n) + (?N x e)"`
`  4447     by (simp only: pos_divide_le_eq[OF np, where a="real_of_int c *(?t/?n) + (?N x e)"`
`  4448       and b="0", simplified divide_zero_left]) (simp only: algebra_simps)`
`  4448       and b="0", simplified div_0]) (simp only: algebra_simps)`
`  4449   also have "\<dots> = (real_of_int c *?t + ?n* (?N x e) \<ge> 0)"`
`  4449   also have "\<dots> = (real_of_int c *?t + ?n* (?N x e) \<ge> 0)"`
`  4450     using np by simp`
`  4450     using np by simp`
`  4451   finally show ?case using nbt nb by (simp add: algebra_simps)`
`  4451   finally show ?case using nbt nb by (simp add: algebra_simps)`
`  4452 next`
`  4452 next`
`  4453   case (3 c e)`
`  4453   case (3 c e)`
`  4455   from np have np: "real_of_int n \<noteq> 0" by simp`
`  4455   from np have np: "real_of_int n \<noteq> 0" by simp`
`  4456   have "?I ?u (Eq (CN 0 c e)) = (real_of_int c *(?t/?n) + (?N x e) = 0)"`
`  4456   have "?I ?u (Eq (CN 0 c e)) = (real_of_int c *(?t/?n) + (?N x e) = 0)"`
`  4457     using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp`
`  4457     using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp`
`  4458   also have "\<dots> = (?n*(real_of_int c *(?t/?n)) + ?n*(?N x e) = 0)"`
`  4458   also have "\<dots> = (?n*(real_of_int c *(?t/?n)) + ?n*(?N x e) = 0)"`
`  4459     by (simp only: nonzero_eq_divide_eq[OF np, where a="real_of_int c *(?t/?n) + (?N x e)"`
`  4459     by (simp only: nonzero_eq_divide_eq[OF np, where a="real_of_int c *(?t/?n) + (?N x e)"`
`  4460       and b="0", simplified divide_zero_left]) (simp only: algebra_simps)`
`  4460       and b="0", simplified div_0]) (simp only: algebra_simps)`
`  4461   also have "\<dots> = (real_of_int c *?t + ?n* (?N x e) = 0)"`
`  4461   also have "\<dots> = (real_of_int c *?t + ?n* (?N x e) = 0)"`
`  4462     using np by simp`
`  4462     using np by simp`
`  4463   finally show ?case using nbt nb by (simp add: algebra_simps)`
`  4463   finally show ?case using nbt nb by (simp add: algebra_simps)`
`  4464 next`
`  4464 next`
`  4465   case (4 c e)`
`  4465   case (4 c e)`
`  4467   from np have np: "real_of_int n \<noteq> 0" by simp`
`  4467   from np have np: "real_of_int n \<noteq> 0" by simp`
`  4468   have "?I ?u (NEq (CN 0 c e)) = (real_of_int c *(?t/?n) + (?N x e) \<noteq> 0)"`
`  4468   have "?I ?u (NEq (CN 0 c e)) = (real_of_int c *(?t/?n) + (?N x e) \<noteq> 0)"`
`  4469     using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp`
`  4469     using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp`
`  4470   also have "\<dots> = (?n*(real_of_int c *(?t/?n)) + ?n*(?N x e) \<noteq> 0)"`
`  4470   also have "\<dots> = (?n*(real_of_int c *(?t/?n)) + ?n*(?N x e) \<noteq> 0)"`
`  4471     by (simp only: nonzero_eq_divide_eq[OF np, where a="real_of_int c *(?t/?n) + (?N x e)"`
`  4471     by (simp only: nonzero_eq_divide_eq[OF np, where a="real_of_int c *(?t/?n) + (?N x e)"`
`  4472       and b="0", simplified divide_zero_left]) (simp only: algebra_simps)`
`  4472       and b="0", simplified div_0]) (simp only: algebra_simps)`
`  4473   also have "\<dots> = (real_of_int c *?t + ?n* (?N x e) \<noteq> 0)"`
`  4473   also have "\<dots> = (real_of_int c *?t + ?n* (?N x e) \<noteq> 0)"`
`  4474     using np by simp`
`  4474     using np by simp`
`  4475   finally show ?case using nbt nb by (simp add: algebra_simps)`
`  4475   finally show ?case using nbt nb by (simp add: algebra_simps)`
`  4476 qed(simp_all add: nbt numbound0_I[where bs ="bs" and b="(Inum (x#bs) t)/ real_of_int n" and b'="x"])`
`  4476 qed(simp_all add: nbt numbound0_I[where bs ="bs" and b="(Inum (x#bs) t)/ real_of_int n" and b'="x"])`
`  4477 `
`  4477 `