1 files changed, 99 insertions, 0 deletions
diff --git a/backends/hol4/divDefNoFixLib.sig b/backends/hol4/divDefNoFixLib.sig
new file mode 100644
index 00000000..eefc6ff7
--- /dev/null
+++ b/backends/hol4/divDefNoFixLib.sig
@@ -0,0 +1,99 @@
+(* **DEPRECATED**: see divDefLib
+
+   This library defines an older version of DefineDiv, which doesn't use
+   fixed-point operator and thus relies on more complex meta functions.
+
+   Define a (group of mutually recursive) function(s) which uses an error
+   monad and is potentially divergent.
+
+   We encode divergence in such a way that we don't have to prove that the
+   functions we define terminate *upon defining them*, and can do those proofs
+   in an extrinsic way later. It works as follows.
+
+   Let's say you want to define the following “even” and “odd” functions
+   which operate on *integers*:
+
+   {[
+     even (i : int) : bool result = if i = 0 then Return T else odd (i - 1) /\
+
+     odd (i : int) : bool result = if i = 0 then Return F else even (i - 1)
+   ]}
+
+   It is easy to prove that the functions terminate provided the input is >= 0,
+   but it would require to be able to define those functions in the first place!
+
+   {!DefineDev} consequently does the following.
+
+   It first defines versions of “even” and “odd” which use fuel:
+   {[
+     even___fuel (n : num) (i : int) : bool result =
+       case n of 0 => Diverge
+       | SUC m => if i = 0 then Return T else odd___fuel m (i - 1) /\
+
+     odd___fuel (n : num) (i : int) : bool result =
+       case n of 0 => Diverge
+       | SUC m => if i = 0 then Return F else even___fuel m (i - 1)
+   ]}
+
+   Those functions trivially terminate.
+
+   Then, provided we have the following auxiliary definition:
+   {[
+     is_diverge (r: 'a result) : bool = case r of Diverge => T | _ => F
+   ]}
+
+   we can define the following predicates, which tell us whether “even___fuel”
+   and “odd___fuel” terminate on some given inputs:
+   {[
+     even___P i n = ~(is_diverge (even___fuel n i)) /\
+
+     odd___P i n = ~(is_diverge (odd___fuel n i))
+   ]}
+
+   We can finally define “even” and “odd” as follows. We use the excluded
+   middle to test whether there exists some fuel on which the function
+   terminates: if there exists such fuel, we call the "___fuel" versions
+   of “even” and “odd” with it (we use the least upper bound, to be more
+   precise). Otherwise, we simply return “Diverge”.
+   {[
+     even i =
+       if (?n. even___P i n) then even___fuel ($LEAST (even___P i)) i
+       else Diverge /\
+
+     odd i =
+       if (?n. odd___P i n) then odd___fuel ($LEAST (odd___P i)) i
+       else Diverge
+   ]}
+
+   The definitions above happen to satisfy the rewriting theorem we want:
+   {[
+     even (i : int) : bool result = if i = 0 then Return T else odd (i - 1) /\
+
+     odd (i : int) : bool result = if i = 0 then Return F else even (i - 1)
+   ]}
+
+   Moreover, if we prove a lemma which states that they don't evaluate to
+   “Diverge” on some given inputs (trivial recursion if we take “i >= 0”
+   and reuse the rewriting theorem just above), then we effectively proved
+   that the functions terminate on those inputs.
+
+   Remark:
+   =======
+   {!DefineDiv} introduces all the auxiliary definitions we need and
+   automatically performs the proofs. A crucial intermediate lemma
+   we need in order to establish the last theorem is that the "___fuel"
+   versions of the functions are monotonic in the fuel.
+   More precisely:
+   {[
+     !n m. n <= m ==>
+       (!ls i. even___P ls i n ==> even___fuel n ls i n = even___fuel m ls i n) /\
+       (!ls i. odd___P ls i n ==> odd___fuel n ls i n = odd___fuel m ls i n)
+   ]}
+ *)
+
+signature divDefNoFixLib =
+sig
+  include Abbrev
+
+  val DefineDiv : term quotation -> thm list
+end