From c6e9e51197833a8685c63e6c40d8eabf4e64c22d Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 15 May 2023 10:32:46 +0200
Subject: Make minor modifications

---
 backends/hol4/divDefLib.sig    | 26 ++++++++++++++++++++++++++
 backends/hol4/divDefScript.sml | 17 +++++++++--------
 2 files changed, 35 insertions(+), 8 deletions(-)

(limited to 'backends')

diff --git a/backends/hol4/divDefLib.sig b/backends/hol4/divDefLib.sig
index 51a09b9c..df879b4b 100644
--- a/backends/hol4/divDefLib.sig
+++ b/backends/hol4/divDefLib.sig
@@ -9,6 +9,32 @@
    divDefExampleTheory.
 
    For examples of how to use DefiveDiv, see divDefLibExampleScript.
+
+   Limitations: our encoding has limitations with regards to higher-order functions. More
+   precisely, the following definition wouldn't be accepted, because we don't know how
+   “MAP” would use ‘explore_tree’, meaning we can't prove the validity property required
+   by the fixed point upon defining ‘explore_tree’ and ‘explore_node’:
+
+   {[
+     Datatype tree:
+     | Leaf : int
+     | Node : tree list
+
+     explore_tree (t : tree) : tree =
+       case t of
+         Leaf i => Leaf i
+       | Node ns => Node (explore_node ns)
+
+     explore_node (ns : tree list) : tree list =
+       MAP explore_tree ns (* This is not supported *)
+   ]}
+
+   *However*, our encoding does allow defining a function ‘f’ *then* giving it
+   as argument to a higher-order function such as ‘MAP’.
+
+   Remark: "Partial recursive functions in higher-order logic", Alexander Krauss,
+   introduces an interesting approach by means of an inductive. It could be
+   interesting to try and compare.
  *)
 
 signature divDefLib =
diff --git a/backends/hol4/divDefScript.sml b/backends/hol4/divDefScript.sml
index c742fb1f..b80aa2bf 100644
--- a/backends/hol4/divDefScript.sml
+++ b/backends/hol4/divDefScript.sml
@@ -20,35 +20,36 @@ val _ = new_theory "divDef"
  *======================*)
 
 (* An auxiliary operator which uses some fuel *)
-val fix_fuel_def = Define ‘
+Definition fix_fuel_def:
   (fix_fuel (0 : num) (f : ('a -> 'b result) -> 'a -> 'b result) (x : 'a) : 'b result = Diverge) ∧
   (fix_fuel (SUC n) (f : ('a -> 'b result) -> 'a -> 'b result) (x : 'a) : 'b result = f (fix_fuel n f) x)
-’
+End
 
 (* An auxiliary predicate *)
-val fix_fuel_P_def = Define ‘
+Definition fix_fuel_P_def:
   fix_fuel_P f x n = ~(is_diverge (fix_fuel n f x))
-’
+End
 
 (* The fixed point operator *)
-val fix_def = Define ‘
+Definition fix_def:
   fix (f : ('a -> 'b result) -> 'a -> 'b result) (x : 'a) : 'b result =
     if (∃ n. fix_fuel_P f x n) then fix_fuel ($LEAST (fix_fuel_P f x)) f x else Diverge
-’
+End
 
 (* A validity condition.
 
    If a function body ‘f’ satisfies this condition, then we have the fixed point
    equation ‘fix f = f (fix f)’ (see [fix_fixed_eq]).
  *)
-val is_valid_fp_body_def = Define ‘
+Definition is_valid_fp_body_def:
   (is_valid_fp_body (0 : num) (f : ('a -> 'a result) -> 'a -> 'a result) = F) ∧
   
   (is_valid_fp_body (SUC n) (f : ('a -> 'a result) -> 'a -> 'a result) =
     ∀x. (∀g h. f g x = f h x) ∨
          (∃ h y. is_valid_fp_body n h ∧
                   ∀g. f g x = do z <- g y; h g z od))
-’
+End
+
 (*======================
  * Lemmas
  *======================*)
-- 
cgit v1.2.3