Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Rat.thy
changeset 82310 41f5266e5595
parent 81124 6ce0c8d59f5a 
--- a/src/HOL/Rat.thy	Wed Mar 19 22:18:52 2025 +0000
+++ b/src/HOL/Rat.thy	Fri Mar 21 10:45:56 2025 +0000
@@ -928,6 +928,12 @@
 lemma quotient_of_int [code abstract]: "quotient_of (Rat.of_int a) = (a, 1)"
   by (simp add: of_int_def of_int_rat quotient_of_Fract)
 
+lemma quotient_of_rat_of_int [simp]: "quotient_of (rat_of_int i) = (i, 1)"
+  using Rat.of_int_def quotient_of_int by force
+
+lemma quotient_of_rat_of_nat [simp]: "quotient_of (rat_of_nat i) = (int i, 1)"
+  by (metis of_int_of_nat_eq quotient_of_rat_of_int)
+
 lemma [code_unfold]: "numeral k = Rat.of_int (numeral k)"
   by (simp add: Rat.of_int_def)
isabelle