Improved statements of is_int_thm

binghe · Jul 24, 2023 · b449637 · b449637
1 parent 5f06cfc
commit b449637
Showing 1 changed file with 7 additions and 1 deletion.
diff --git a/src/real/intrealScript.sml b/src/real/intrealScript.sml
@@ -549,7 +549,7 @@ Proof
  >> METIS_TAC [REAL_LT_IMP_NE, INT_FLOOR_BOUNDS, real_of_int_add]
 QED
 
-Theorem is_int_thm :
+Theorem is_int_thm_lemma[local] :
     !x. is_int x <=> real_of_int (INT_FLOOR x) = real_of_int (INT_CEILING x)
 Proof
     Q.X_GEN_TAC ‘x’
@@ -562,6 +562,12 @@ Proof
  >> rw [INT_LT_ADDR]
 QED
 
+Theorem is_int_thm :
+    !x. is_int x <=> INT_FLOOR x = INT_CEILING x
+Proof
+    rw [is_int_thm_lemma, real_of_int_11]
+QED
+
 Theorem INT_CEILING_ADD_NUM :
     INT_CEILING (x + &n) = INT_CEILING x + &n /\
     INT_CEILING (&n + x) = INT_CEILING x + &n