# HG changeset patch
# User haftmann
# Date 1617885498 0
# Node ID 7cb3fefef79e7badc1820f4c9ed01419f9019df7
# Parent  fc72e5ebf9de4e1537cefe98206a1272ac0ff7a3
confluent preprocessing for floats in presence of target language numerals

diff -r fc72e5ebf9de -r 7cb3fefef79e src/HOL/Decision_Procs/Approximation.thy
--- 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
 
diff -r fc72e5ebf9de -r 7cb3fefef79e src/HOL/Library/Code_Target_Numeral_Float.thy
--- /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
diff -r fc72e5ebf9de -r 7cb3fefef79e src/HOL/ROOT
--- 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