1594 with assms have cp: "c > 0" and nb: "numbound0 e" by simp_all |
1594 with assms have cp: "c > 0" and nb: "numbound0 e" by simp_all |
1595 have "?I ?u (Lt (CN 0 c e)) \<longleftrightarrow> real_of_int c * (?t / ?n) + ?N x e < 0" |
1595 have "?I ?u (Lt (CN 0 c e)) \<longleftrightarrow> real_of_int c * (?t / ?n) + ?N x e < 0" |
1596 using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp |
1596 using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp |
1597 also have "\<dots> \<longleftrightarrow> ?n * (real_of_int c * (?t / ?n)) + ?n*(?N x e) < 0" |
1597 also have "\<dots> \<longleftrightarrow> ?n * (real_of_int c * (?t / ?n)) + ?n*(?N x e) < 0" |
1598 by (simp only: pos_less_divide_eq[OF np, where a="real_of_int c *(?t/?n) + (?N x e)" |
1598 by (simp only: pos_less_divide_eq[OF np, where a="real_of_int c *(?t/?n) + (?N x e)" |
1599 and b="0", simplified divide_zero_left]) (simp only: algebra_simps) |
1599 and b="0", simplified div_0]) (simp only: algebra_simps) |
1600 also have "\<dots> \<longleftrightarrow> real_of_int c * ?t + ?n * (?N x e) < 0" using np by simp |
1600 also have "\<dots> \<longleftrightarrow> real_of_int c * ?t + ?n * (?N x e) < 0" using np by simp |
1601 finally show ?case using nbt nb by (simp add: algebra_simps) |
1601 finally show ?case using nbt nb by (simp add: algebra_simps) |
1602 next |
1602 next |
1603 case (6 c e) |
1603 case (6 c e) |
1604 with assms have cp: "c > 0" and nb: "numbound0 e" by simp_all |
1604 with assms have cp: "c > 0" and nb: "numbound0 e" by simp_all |
1605 have "?I ?u (Le (CN 0 c e)) \<longleftrightarrow> real_of_int c * (?t / ?n) + ?N x e \<le> 0" |
1605 have "?I ?u (Le (CN 0 c e)) \<longleftrightarrow> real_of_int c * (?t / ?n) + ?N x e \<le> 0" |
1606 using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp |
1606 using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp |
1607 also have "\<dots> = (?n*(real_of_int c *(?t/?n)) + ?n*(?N x e) \<le> 0)" |
1607 also have "\<dots> = (?n*(real_of_int c *(?t/?n)) + ?n*(?N x e) \<le> 0)" |
1608 by (simp only: pos_le_divide_eq[OF np, where a="real_of_int c *(?t/?n) + (?N x e)" |
1608 by (simp only: pos_le_divide_eq[OF np, where a="real_of_int c *(?t/?n) + (?N x e)" |
1609 and b="0", simplified divide_zero_left]) (simp only: algebra_simps) |
1609 and b="0", simplified div_0]) (simp only: algebra_simps) |
1610 also have "\<dots> = (real_of_int c *?t + ?n* (?N x e) \<le> 0)" using np by simp |
1610 also have "\<dots> = (real_of_int c *?t + ?n* (?N x e) \<le> 0)" using np by simp |
1611 finally show ?case using nbt nb by (simp add: algebra_simps) |
1611 finally show ?case using nbt nb by (simp add: algebra_simps) |
1612 next |
1612 next |
1613 case (7 c e) |
1613 case (7 c e) |
1614 with assms have cp: "c >0" and nb: "numbound0 e" by simp_all |
1614 with assms have cp: "c >0" and nb: "numbound0 e" by simp_all |
1615 have "?I ?u (Gt (CN 0 c e)) \<longleftrightarrow> real_of_int c *(?t / ?n) + ?N x e > 0" |
1615 have "?I ?u (Gt (CN 0 c e)) \<longleftrightarrow> real_of_int c *(?t / ?n) + ?N x e > 0" |
1616 using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp |
1616 using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp |
1617 also have "\<dots> \<longleftrightarrow> ?n * (real_of_int c * (?t / ?n)) + ?n * ?N x e > 0" |
1617 also have "\<dots> \<longleftrightarrow> ?n * (real_of_int c * (?t / ?n)) + ?n * ?N x e > 0" |
1618 by (simp only: pos_divide_less_eq[OF np, where a="real_of_int c *(?t/?n) + (?N x e)" |
1618 by (simp only: pos_divide_less_eq[OF np, where a="real_of_int c *(?t/?n) + (?N x e)" |
1619 and b="0", simplified divide_zero_left]) (simp only: algebra_simps) |
1619 and b="0", simplified div_0]) (simp only: algebra_simps) |
1620 also have "\<dots> \<longleftrightarrow> real_of_int c * ?t + ?n * ?N x e > 0" using np by simp |
1620 also have "\<dots> \<longleftrightarrow> real_of_int c * ?t + ?n * ?N x e > 0" using np by simp |
1621 finally show ?case using nbt nb by (simp add: algebra_simps) |
1621 finally show ?case using nbt nb by (simp add: algebra_simps) |
1622 next |
1622 next |
1623 case (8 c e) |
1623 case (8 c e) |
1624 with assms have cp: "c > 0" and nb: "numbound0 e" by simp_all |
1624 with assms have cp: "c > 0" and nb: "numbound0 e" by simp_all |
1625 have "?I ?u (Ge (CN 0 c e)) \<longleftrightarrow> real_of_int c * (?t / ?n) + ?N x e \<ge> 0" |
1625 have "?I ?u (Ge (CN 0 c e)) \<longleftrightarrow> real_of_int c * (?t / ?n) + ?N x e \<ge> 0" |
1626 using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp |
1626 using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp |
1627 also have "\<dots> \<longleftrightarrow> ?n * (real_of_int c * (?t / ?n)) + ?n * ?N x e \<ge> 0" |
1627 also have "\<dots> \<longleftrightarrow> ?n * (real_of_int c * (?t / ?n)) + ?n * ?N x e \<ge> 0" |
1628 by (simp only: pos_divide_le_eq[OF np, where a="real_of_int c *(?t/?n) + (?N x e)" |
1628 by (simp only: pos_divide_le_eq[OF np, where a="real_of_int c *(?t/?n) + (?N x e)" |
1629 and b="0", simplified divide_zero_left]) (simp only: algebra_simps) |
1629 and b="0", simplified div_0]) (simp only: algebra_simps) |
1630 also have "\<dots> \<longleftrightarrow> real_of_int c * ?t + ?n * ?N x e \<ge> 0" using np by simp |
1630 also have "\<dots> \<longleftrightarrow> real_of_int c * ?t + ?n * ?N x e \<ge> 0" using np by simp |
1631 finally show ?case using nbt nb by (simp add: algebra_simps) |
1631 finally show ?case using nbt nb by (simp add: algebra_simps) |
1632 next |
1632 next |
1633 case (3 c e) |
1633 case (3 c e) |
1634 with assms have cp: "c > 0" and nb: "numbound0 e" by simp_all |
1634 with assms have cp: "c > 0" and nb: "numbound0 e" by simp_all |
1635 from np have np: "real_of_int n \<noteq> 0" by simp |
1635 from np have np: "real_of_int n \<noteq> 0" by simp |
1636 have "?I ?u (Eq (CN 0 c e)) \<longleftrightarrow> real_of_int c * (?t / ?n) + ?N x e = 0" |
1636 have "?I ?u (Eq (CN 0 c e)) \<longleftrightarrow> real_of_int c * (?t / ?n) + ?N x e = 0" |
1637 using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp |
1637 using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp |
1638 also have "\<dots> \<longleftrightarrow> ?n * (real_of_int c * (?t / ?n)) + ?n * ?N x e = 0" |
1638 also have "\<dots> \<longleftrightarrow> ?n * (real_of_int c * (?t / ?n)) + ?n * ?N x e = 0" |
1639 by (simp only: nonzero_eq_divide_eq[OF np, where a="real_of_int c *(?t/?n) + (?N x e)" |
1639 by (simp only: nonzero_eq_divide_eq[OF np, where a="real_of_int c *(?t/?n) + (?N x e)" |
1640 and b="0", simplified divide_zero_left]) (simp only: algebra_simps) |
1640 and b="0", simplified div_0]) (simp only: algebra_simps) |
1641 also have "\<dots> \<longleftrightarrow> real_of_int c * ?t + ?n * ?N x e = 0" using np by simp |
1641 also have "\<dots> \<longleftrightarrow> real_of_int c * ?t + ?n * ?N x e = 0" using np by simp |
1642 finally show ?case using nbt nb by (simp add: algebra_simps) |
1642 finally show ?case using nbt nb by (simp add: algebra_simps) |
1643 next |
1643 next |
1644 case (4 c e) with assms have cp: "c >0" and nb: "numbound0 e" by simp_all |
1644 case (4 c e) with assms have cp: "c >0" and nb: "numbound0 e" by simp_all |
1645 from np have np: "real_of_int n \<noteq> 0" by simp |
1645 from np have np: "real_of_int n \<noteq> 0" by simp |
1646 have "?I ?u (NEq (CN 0 c e)) \<longleftrightarrow> real_of_int c * (?t / ?n) + ?N x e \<noteq> 0" |
1646 have "?I ?u (NEq (CN 0 c e)) \<longleftrightarrow> real_of_int c * (?t / ?n) + ?N x e \<noteq> 0" |
1647 using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp |
1647 using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp |
1648 also have "\<dots> \<longleftrightarrow> ?n * (real_of_int c * (?t / ?n)) + ?n * ?N x e \<noteq> 0" |
1648 also have "\<dots> \<longleftrightarrow> ?n * (real_of_int c * (?t / ?n)) + ?n * ?N x e \<noteq> 0" |
1649 by (simp only: nonzero_eq_divide_eq[OF np, where a="real_of_int c *(?t/?n) + (?N x e)" |
1649 by (simp only: nonzero_eq_divide_eq[OF np, where a="real_of_int c *(?t/?n) + (?N x e)" |
1650 and b="0", simplified divide_zero_left]) (simp only: algebra_simps) |
1650 and b="0", simplified div_0]) (simp only: algebra_simps) |
1651 also have "\<dots> \<longleftrightarrow> real_of_int c * ?t + ?n * ?N x e \<noteq> 0" using np by simp |
1651 also have "\<dots> \<longleftrightarrow> real_of_int c * ?t + ?n * ?N x e \<noteq> 0" using np by simp |
1652 finally show ?case using nbt nb by (simp add: algebra_simps) |
1652 finally show ?case using nbt nb by (simp add: algebra_simps) |
1653 qed(simp_all add: nbt numbound0_I[where bs ="bs" and b="(Inum (x#bs) t)/ real_of_int n" and b'="x"]) |
1653 qed(simp_all add: nbt numbound0_I[where bs ="bs" and b="(Inum (x#bs) t)/ real_of_int n" and b'="x"]) |
1654 |
1654 |
1655 lemma uset_l: |
1655 lemma uset_l: |