confluent preprocessing for floats in presence of target language numerals
authorhaftmann
Thu, 08 Apr 2021 12:38:18 +0000
changeset 73802 7cb3fefef79e
parent 73801 fc72e5ebf9de
child 73804 c54a9395ad96
confluent preprocessing for floats in presence of target language numerals
src/HOL/Decision_Procs/Approximation.thy
src/HOL/Library/Code_Target_Numeral_Float.thy
src/HOL/ROOT
--- a/src/HOL/Decision_Procs/Approximation.thy	Wed Apr 07 15:46:06 2021 +0000
+++ b/src/HOL/Decision_Procs/Approximation.thy	Thu Apr 08 12:38:18 2021 +0000
@@ -1,11 +1,11 @@
- (* Author:     Johannes Hoelzl, TU Muenchen
+(* Author:     Johannes Hoelzl, TU Muenchen
    Coercions removed by Dmitriy Traytel *)
 
 theory Approximation
 imports
   Complex_Main
-  "HOL-Library.Code_Target_Numeral"
   Approximation_Bounds
+  "HOL-Library.Code_Target_Numeral_Float"
 keywords "approximate" :: diag
 begin
 
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Code_Target_Numeral_Float.thy	Thu Apr 08 12:38:18 2021 +0000
@@ -0,0 +1,16 @@
+(*  Title:      HOL/Library/Code_Target_Numeral_Float.thy
+    Author:     Florian Haftmann, TU Muenchen
+*)
+
+section \<open>Preprocessor setup for floats implemented by target language numerals\<close>
+
+theory Code_Target_Numeral_Float
+imports Float Code_Target_Numeral
+begin
+
+lemma numeral_float_computation_unfold [code_computation_unfold]:
+  \<open>numeral k = Float (int_of_integer (Code_Numeral.positive k)) 0\<close>
+  \<open>- numeral k = Float (int_of_integer (Code_Numeral.negative k)) 0\<close>
+  by (simp_all add: Float.compute_float_numeral Float.compute_float_neg_numeral)
+
+end
--- a/src/HOL/ROOT	Wed Apr 07 15:46:06 2021 +0000
+++ b/src/HOL/ROOT	Thu Apr 08 12:38:18 2021 +0000
@@ -73,6 +73,7 @@
     Code_Prolog
     Code_Real_Approx_By_Float
     Code_Target_Numeral
+    Code_Target_Numeral_Float
     DAList
     DAList_Multiset
     RBT_Mapping