src/HOL/Decision_Procs/MIR.thy
changeset 64240 eabf80376aab
parent 63600 d0fa16751d14
child 64246 15d1ee6e847b
equal deleted 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