summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/Decision_Procs/MIR.thy

changeset 63600 | d0fa16751d14 |

parent 62342 | 1cf129590be8 |

child 64240 | eabf80376aab |

equal
deleted
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 |