Start working on a version of divDefLib which uses fixed point combinators

2 files changed, 983 insertions, 0 deletions

diff --git a/backends/hol4/divDefProtoScript.sml b/backends/hol4/divDefProtoScript.sml
new file mode 100644
index 00000000..64d4b9f0
--- /dev/null
+++ b/backends/hol4/divDefProtoScript.sml
@@ -0,0 +1,773 @@
+(* Prototype: divDefLib but with general combinators *)
+
+open HolKernel boolLib bossLib Parse
+open boolTheory arithmeticTheory integerTheory intLib listTheory stringTheory
+
+open primitivesArithTheory primitivesBaseTacLib ilistTheory primitivesTheory
+open primitivesLib
+
+val _ = new_theory "divDefProto"
+
+(*
+ * Test with a general validity predicate.
+ *
+ * TODO: this works! Cleanup.
+ *)
+val fix_fuel_def = Define ‘
+  (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)
+’
+
+val fix_fuel_P_def = Define ‘
+  fix_fuel_P f x n = ~(is_diverge (fix_fuel n f x))
+’
+
+val fix_def = Define ‘
+  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
+’
+
+val is_valid_fp_body_def = Define ‘
+  is_valid_fp_body (f : ('a -> 'b result) -> 'a -> 'b result) =
+    ∀x. (∀g h. f g x = f h x) ∨ (∃ y. ∀g. f g x = g y)
+’
+
+Theorem fix_fuel_mono:
+  ∀f. is_valid_fp_body f ⇒
+    ∀n x. fix_fuel_P f x n ⇒
+     ∀ m. n ≤ m ⇒
+       fix_fuel n f x = fix_fuel m f x
+Proof
+  ntac 2 strip_tac >>
+  Induct_on ‘n’ >> rpt strip_tac
+  >- (fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def]) >>
+  Cases_on ‘m’ >- int_tac >> fs [] >>
+    fs [is_valid_fp_body_def] >>
+  fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def] >>
+
+  (* Use the validity property *)
+  last_x_assum (qspec_assume ‘x’) >>
+  (* This makes a case disjunction on the validity property *)
+  rw []
+  >-((* Case 1: the continuation doesn't matter *) fs []) >>
+  (* Case 2: the continuation *does* matter (i.e., there is a recursive call *)
+  (* Instantiate the validity property with the different continuations *)
+  first_assum (qspec_assume ‘fix_fuel n f’) >>
+  first_assum (qspec_assume ‘fix_fuel n' f’) >>
+  last_assum (qspec_assume ‘y’) >>
+  fs []
+QED
+
+(* TODO: remove? *)
+Theorem fix_fuel_mono_least:
+  ∀f. is_valid_fp_body f ⇒
+    ∀n x. fix_fuel_P f x n ⇒
+      fix_fuel n f x = fix_fuel ($LEAST (fix_fuel_P f x)) f x
+Proof
+  rw [] >>
+  pure_once_rewrite_tac [EQ_SYM_EQ] >>
+  irule fix_fuel_mono >> fs [] >>
+  (* Use the "fundamental" property about $LEAST *)
+  qspec_assume ‘fix_fuel_P f x’ whileTheory.LEAST_EXISTS_IMP >>
+  (* Prove the premise *)
+  pop_assum sg_premise_tac >- metis_tac [] >> fs [] >>
+  spose_not_then assume_tac >>
+  fs [not_le_eq_gt]
+QED
+
+Theorem fix_fixed_diverges:
+  ∀f. is_valid_fp_body f ⇒ ∀x. ~(∃ n. fix_fuel_P f x n) ⇒ fix f x = f (fix f) x
+Proof
+  rw [fix_def] >>
+  (* Case disjunction on the validity hypothesis *)
+  fs [is_valid_fp_body_def] >>
+  last_x_assum (qspec_assume ‘x’) >>
+  rw []
+  >- (
+    last_assum (qspec_assume ‘SUC n’) >>
+    fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def] >>
+    first_assum (qspecl_assume [‘fix f’, ‘fix_fuel n f’]) >>
+    Cases_on ‘f (fix_fuel n f) x’ >> fs []
+  ) >>
+  first_assum (qspec_assume ‘fix f’) >> fs [] >>
+  fs [fix_def] >>
+  (* Case disjunction on the ‘∃n. ...’ *)
+  rw [] >>
+  (* Use the hypothesis that there is no fuel s.t. ... *)
+  last_assum (qspec_assume ‘SUC n’) >>
+  fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def] >>
+  first_assum (qspec_assume ‘fix_fuel n f’) >>
+  Cases_on ‘fix_fuel n f y’ >> fs []
+QED
+
+(* TODO: I think we can merge this with the theorem below *)
+Theorem fix_fixed_termination_rec_case:
+  ∀x y n m.
+  is_valid_fp_body f ⇒
+  (∀g. f g x = g y) ⇒
+  fix_fuel_P f x n ⇒
+  fix_fuel_P f y m ⇒
+  fix_fuel n f x = fix_fuel m f y
+Proof
+  rw [] >>
+  Cases_on ‘n’ >- fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def] >>
+  pure_asm_rewrite_tac [fix_fuel_def] >>
+  sg ‘fix_fuel_P f y n'’ >- rfs [fix_fuel_P_def, is_diverge_def, fix_fuel_def] >>
+  imp_res_tac fix_fuel_mono_least >>
+  fs []
+QED
+
+Theorem fix_fixed_termination_rec_case:
+  ∀ x y n m.
+  is_valid_fp_body f ⇒
+  (∀g. f g x = g y) ⇒
+  fix_fuel_P f x n ⇒
+  fix_fuel_P f y m ⇒
+  fix_fuel ($LEAST (fix_fuel_P f x)) f x =
+  fix_fuel ($LEAST (fix_fuel_P f y)) f y
+Proof
+  rw [] >>
+  imp_res_tac fix_fuel_mono_least >>
+  irule fix_fixed_termination_rec_case >>
+  fs [] >>
+  (* TODO: factorize *)
+  qspec_assume ‘fix_fuel_P f x’ whileTheory.LEAST_EXISTS_IMP >>
+  pop_assum sg_premise_tac >- metis_tac [] >>
+  qspec_assume ‘fix_fuel_P f y’ whileTheory.LEAST_EXISTS_IMP >>
+  pop_assum sg_premise_tac >- metis_tac [] >>
+  rw []
+QED
+
+Theorem fix_fixed_terminates:
+  ∀f. is_valid_fp_body f ⇒ ∀x n. fix_fuel_P f x n ⇒ fix f x = f (fix f) x
+Proof
+  rpt strip_tac >>
+  (* Case disjunction on the validity hypothesis - we don't want to consume it *)
+  last_assum mp_tac >>
+  pure_rewrite_tac [is_valid_fp_body_def] >> rpt strip_tac >>
+  pop_assum (qspec_assume ‘x’) >>
+  rw []
+  >-( (* No recursive call *)
+    fs [fix_def] >> rw [] >> fs [] >>
+    imp_res_tac fix_fuel_mono_least >>
+    Cases_on ‘$LEAST (fix_fuel_P f x)’ >> fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def]
+  ) >>
+  (* There exists a recursive call *)
+  SUBGOAL_THEN “∃m. fix_fuel_P f y m” assume_tac >-(
+    Cases_on ‘n’ >>
+    fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def] >>
+    metis_tac []
+  ) >>
+  fs [fix_def] >> rw [] >> fs [] >>
+  irule fix_fixed_termination_rec_case >>
+  fs [] >>
+  metis_tac []
+QED
+
+Theorem fix_fixed_eq:
+  ∀f. is_valid_fp_body f ⇒ ∀x. fix f x = f (fix f) x
+Proof
+  rw [] >>
+  Cases_on ‘∃n. fix_fuel_P f x n’
+  >- (irule fix_fixed_terminates >> metis_tac []) >>
+  irule fix_fixed_diverges >>
+  fs []
+QED  
+
+(* Testing on an example *)
+Datatype:
+  list_t =
+    ListCons 't list_t
+  | ListNil
+End
+
+val nth_body_def = Define ‘
+  nth_body (f : ('t list_t # u32) -> 't result) (x : ('t list_t # u32)) : 't result =
+    let (ls, i) = x in
+    case ls of
+    | ListCons x tl =>
+      if u32_to_int i = (0:int)
+      then (Return x)
+      else
+        do
+        i0 <- u32_sub i (int_to_u32 1);
+        f (tl, i0)
+        od
+    | ListNil => Fail Failure
+’
+
+(* TODO: move *)
+Theorem is_valid_suffice:
+  ∃y. ∀g. g x = g y
+Proof
+  metis_tac []
+QED
+
+(* The general proof of is_valid_fp_body *)
+Theorem nth_body_is_valid:
+  is_valid_fp_body nth_body
+Proof
+  pure_rewrite_tac [is_valid_fp_body_def] >>
+  gen_tac >>
+  (* TODO: automate this *)
+  Cases_on ‘x’ >> fs [] >>
+  (* Expand *)
+  fs [nth_body_def, bind_def] >>
+  (* Explore all paths *)
+  Cases_on ‘q’ >> fs [is_valid_suffice] >>
+  Cases_on ‘u32_to_int r = 0’ >> fs [is_valid_suffice] >>
+  Cases_on ‘u32_sub r (int_to_u32 1)’ >> fs [is_valid_suffice]
+QED
+
+val nth_raw_def = Define ‘
+  nth (ls : 't list_t) (i : u32) = fix nth_body (ls, i)
+’
+
+Theorem nth_def:
+  ∀ls i. nth (ls : 't list_t) (i : u32) : 't result =
+    case ls of
+    | ListCons x tl =>
+      if u32_to_int i = (0:int)
+      then (Return x)
+      else
+        do
+        i0 <- u32_sub i (int_to_u32 1);
+        nth tl i0
+        od
+    | ListNil => Fail Failure
+Proof
+  rpt strip_tac >>
+  (* Expand the raw definition *)
+  pure_rewrite_tac [nth_raw_def] >>
+  (* Use the fixed-point equality *)
+  sg ‘fix nth_body (ls,i) = nth_body (fix nth_body) (ls,i)’
+  >- simp_tac bool_ss [HO_MATCH_MP fix_fixed_eq nth_body_is_valid] >>
+  pure_asm_rewrite_tac [] >>
+  (* Expand the body definition *)
+  qspecl_assume [‘fix nth_body’, ‘(ls, i)’] nth_body_def >>
+  pure_asm_rewrite_tac [LET_THM] >>
+  simp_tac arith_ss []
+QED
+
+(************************** FAILED TESTS *)
+
+(*
+Datatype:
+  fresult = FReturn 'b | FFail error | FRec 'a
+End
+
+(* TODO: monad converter from fresult to result + rewrite rules *)
+val fres_to_res_def = Define ‘
+  fres_to_res (f : 'a -> 'b result) (r : ('a, 'b) fresult) : 'b result =
+    case r of
+    | FReturn x => Return x
+    | FFail e => Fail e
+    | FRec y => f y
+’
+
+val fixa_fuel_def = Define ‘
+  (fixa_fuel (0 : num) (f : 'a -> ('a, 'b) fresult) (x : 'a) : 'b result = Diverge) ∧
+  (fixa_fuel (SUC n) (f : 'a -> ('a, 'b) fresult) (x : 'a) : 'b result =
+    fres_to_res (fixa_fuel n f) (f x))
+’
+
+val fixa_fuel_P_def = Define ‘
+  fixa_fuel_P f x n = ~(is_diverge (fixa_fuel n f x))
+’
+
+val fixa_def = Define ‘
+  fixa (f : 'a -> ('a, 'b) fresult) (x : 'a) : 'b result =
+    if (∃ n. fixa_fuel_P f x n) then fixa_fuel ($LEAST (fixa_fuel_P f x)) f x else Diverge
+’
+
+Theorem fixa_fuel_mono:
+  ∀n m. n <= m ⇒ (∀f x. fixa_fuel_P f x n ⇒ fixa_fuel n f x = fixa_fuel m f x)
+Proof
+  Induct_on ‘n’ >> rpt strip_tac
+  >- (fs [fixa_fuel_P_def, is_diverge_def, fixa_fuel_def, fres_to_res_def]) >>
+  Cases_on ‘m’ >- int_tac >> fs [] >>
+  last_x_assum imp_res_tac >>
+  fs [fixa_fuel_P_def, is_diverge_def, fixa_fuel_def, fres_to_res_def] >>
+  Cases_on ‘f x’ >> fs []
+QED
+
+(* TODO: remove ? *)
+Theorem fixa_fuel_P_least:
+  ∀f x n. fixa_fuel_P f x n ⇒ fixa_fuel_P f x ($LEAST (fixa_fuel_P f x))
+Proof
+  rw [] >>
+  (* Use the "fundamental" property about $LEAST *)
+  qspec_assume ‘fixa_fuel_P f x’ whileTheory.LEAST_EXISTS_IMP >>
+  (* Prove the premise *)
+  pop_assum sg_premise_tac >- metis_tac [] >>
+  rw []
+QED
+
+Theorem fixa_fuel_mono_least:
+  ∀n f x. fixa_fuel_P f x n ⇒ fixa_fuel n f x = fixa_fuel ($LEAST (fixa_fuel_P f x)) f x
+Proof
+  rw [] >>
+  (* Use the "fundamental" property about $LEAST *)
+  qspec_assume ‘fixa_fuel_P f x’ whileTheory.LEAST_EXISTS_IMP >>
+  (* Prove the premise *)
+  pop_assum sg_premise_tac >- metis_tac [] >>
+  (* Prove that $LEAST ... ≤ n *)
+  sg ‘n >= $LEAST (fixa_fuel_P f x)’ >-(
+    spose_not_then assume_tac >>
+    fs [not_ge_eq_lt]) >>
+  pure_once_rewrite_tac [EQ_SYM_EQ] >>
+  irule fixa_fuel_mono >>
+  fs []
+QED
+
+Theorem fixa_fixed_eq:
+  ∀f x. fixa f x = fres_to_res (fixa f) (f x)
+Proof
+  rw [fixa_def, fres_to_res_def]
+  >- (
+    (* Termination case *)
+    imp_res_tac fixa_fuel_P_least >>
+    Cases_on ‘$LEAST (fixa_fuel_P f x)’ >>
+    fs [fixa_fuel_P_def, is_diverge_def, fixa_fuel_def, fres_to_res_def] >>
+    Cases_on ‘f x’ >> fs [] >>
+    rw [] >> fs [] >>
+    irule fixa_fuel_mono_least >>
+    fs [fixa_fuel_P_def, is_diverge_def, fixa_fuel_def]) >>
+  (* Divergence case *)
+  fs [fres_to_res_def] >>
+  sg ‘∀n. ~(fixa_fuel_P f x (SUC n))’ >- fs [] >>
+  Cases_on ‘f x’ >> fs [] >>
+  fs [fixa_fuel_P_def, is_diverge_def, fixa_fuel_def, fres_to_res_def]  >>
+  rw []
+QED
+
+val fix_fuel_def = Define ‘
+  (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)
+’
+
+val fix_fuel_P_def = Define ‘
+  fix_fuel_P f x n = ~(is_diverge (fix_fuel n f x))
+’
+
+val fix_def = Define ‘
+  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
+’
+
+Theorem fixa_fuel_eq_fix_fuel:
+  ∀n (f : 'a -> ('a, 'b) fresult) (x : 'a).
+    fixa_fuel n f x = fix_fuel n (\g y. fres_to_res g (f y)) x
+Proof
+  Induct_on ‘n’ >> rw [fixa_fuel_def, fix_fuel_def, fres_to_res_def]
+QED
+
+Theorem fixa_fuel_P_eq_fix_fuel_P:
+  ∀(f : 'a -> ('a, 'b) fresult) (x : 'a).
+    fixa_fuel_P f x = fix_fuel_P (\g y. fres_to_res g (f y)) x
+Proof
+  rw [] >> irule EQ_EXT >> rw [] >>
+  qspecl_assume [‘x'’, ‘f’, ‘x’] fixa_fuel_eq_fix_fuel >>
+  fs [fixa_fuel_P_def, fix_fuel_P_def]  
+QED
+
+Theorem fixa_fuel_eq_fix_fuel:
+  ∀(f : 'a -> ('a, 'b) fresult) (x : 'a).
+    fixa f x = fix (\g y. fres_to_res g (f y)) x
+Proof
+  rw [fixa_def, fix_def, fixa_fuel_P_eq_fix_fuel_P, fixa_fuel_eq_fix_fuel]
+QED
+
+(*
+  The annoying thing is that to make this work, we need to rewrite the
+  body by swapping matches, which is not easy to automate.
+*)
+
+(*
+f x =
+  case _ of
+  | _ => Fail e
+  | _ => Return x
+  | _ => f y
+
+f x (g : ('a, 'b) result => 'c)
+
+f x (fres_to_res g) = f x g
+
+*)
+
+(*
+val fix_fuel_def = Define ‘
+  (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)
+’
+
+val fix_fuel_P_def = Define ‘
+  fix_fuel_P f x n = ~(is_diverge (fix_fuel n f x))
+’
+*)
+
+
+(*
+val is_valid_FP_body_def = Define ‘
+  is_valid_FP_body (f : (('a, 'b) fresult -> 'c) -> ('a, 'b) fresult -> 'c) =
+    ∃ (fa: (('a, 'b) fresult -> ('a, 'b) fresult) -> ('a, 'b) fresult -> ('a, 'b) fresult).
+      ∀ (g : ('a, 'b) fresult -> 'c) x.
+        f g x = g (fa (\x. x) x)
+
+val fix_fuel_def = Define ‘
+  (fix_fuel (0 : num) (f : (('a, 'b) fresult -> 'b result) -> ('a, 'b) fresult -> 'b result) (x : ('a, 'b) fresult) : 'b result = Diverge) ∧
+  (fix_fuel (SUC n) (f : (('a, 'b) fresult -> 'b result) -> ('a, 'b) fresult -> 'b result) (x : ('a, 'b) fresult) : 'b result = f (fix_fuel n f) x)
+’
+
+val fix_fuel_P_def = Define ‘
+  fix_fuel_P f x n = ~(is_diverge (fix_fuel n f x))
+’
+
+val fix_def = Define ‘
+  fix f x : 'b result =
+    if (∃ n. fix_fuel_P f x n) then fix_fuel ($LEAST (fix_fuel_P f x)) f x else Diverge
+
+
+Theorem fix_fuel_mono:
+  ∀f. is_valid_FP_body f ⇒
+  ∀n m. n <= m ⇒ (∀x. fix_fuel_P f x n ⇒ fix_fuel n f x = fix_fuel m f x)
+Proof
+  strip_tac >> strip_tac >>
+  Induct_on ‘n’ >> rpt strip_tac
+  >- (fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def]) >>
+  fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def] >>
+  Cases_on ‘m’ >- int_tac >>
+  fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def] >>
+  fs [is_valid_FP_body] >>
+  last_x_assum (qspec_assume ‘fix_fuel n f’) >>
+  fs []
+QED
+
+’*)
+
+(*
+ * Test with a validity predicate which gives monotonicity.
+
+   TODO: not enough to prove the fixed-point equation.
+ *)
+val fix_fuel_def = Define ‘
+  (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)
+’
+
+val fix_fuel_P_def = Define ‘
+  fix_fuel_P f x n = ~(is_diverge (fix_fuel n f x))
+’
+
+val fix_def = Define ‘
+  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
+’
+
+Theorem fix_eq:
+  fix f = \x. if (∃ n. fix_fuel_P f x n) then fix_fuel ($LEAST (fix_fuel_P f x)) f x else Diverge
+Proof
+  irule EQ_EXT >> fs [fix_def]
+QED
+
+val is_valid_fp_body_def = Define ‘
+  is_valid_fp_body (f : ('a -> 'b result) -> 'a -> 'b result) =
+    ∀n m. n ≤ m ⇒ ∀x. fix_fuel_P f x n ⇒ fix_fuel n f x = fix_fuel m f x
+’
+
+Theorem fix_fuel_mono_least:
+  ∀f. is_valid_fp_body f ⇒
+    ∀n x. fix_fuel_P f x n ⇒ fix_fuel n f x = fix_fuel ($LEAST (fix_fuel_P f x)) f x
+Proof
+  rw [] >>
+  (* Use the "fundamental" property about $LEAST *)
+  qspec_assume ‘fix_fuel_P f x’ whileTheory.LEAST_EXISTS_IMP >>
+  (* Prove the premise *)
+  pop_assum sg_premise_tac >- metis_tac [] >> fs [] >>
+  (* Prove that $LEAST ... ≤ n *)
+  sg ‘n >= $LEAST (fix_fuel_P f x)’ >-(
+    spose_not_then assume_tac >>
+    fs [not_ge_eq_lt]) >>
+  pure_once_rewrite_tac [EQ_SYM_EQ] >>
+  (* Finish by using the monotonicity property *)
+  fs [is_valid_fp_body_def]
+QED
+
+
+(* TODO: remove ? *)
+Theorem fix_fuel_P_least:
+  ∀f x n. fix_fuel_P f x n ⇒ fix_fuel_P f x ($LEAST (fix_fuel_P f x))
+Proof
+  rw [] >>
+  (* Use the "fundamental" property about $LEAST *)
+  qspec_assume ‘fix_fuel_P f x’ whileTheory.LEAST_EXISTS_IMP >>
+  (* Prove the premise *)
+  pop_assum sg_premise_tac >- metis_tac [] >>
+  rw []
+QED
+
+(*Theorem test:
+  fix_fuel_P f x (SUC n) ⇒
+  (∀m. n ≤ m ⇒ f (fix_fuel n f) x = f (fix_fuel m f) x) ⇒
+  f (fix_fuel n f) x = f (fix f) x
+Proof
+  rw [] >>
+  spose_not_then assume_tac >>
+  fs [fix_eq]
+*)
+Theorem fix_fixed_eq:
+  ∀f. is_valid_fp_body f ⇒ ∀x. fix f x = f (fix f) x
+Proof
+  rw [fix_def] >> CASE_TAC >> fs []
+  >- (
+    (* Termination case *)
+    sg ‘$LEAST (fix_fuel_P f x) <= n’ >- cheat >>
+    imp_res_tac fix_fuel_P_least >>
+    Cases_on ‘$LEAST (fix_fuel_P f x)’ >>
+    fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def] >>
+    Cases_on ‘n’ >>
+    fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def] >>
+    (* Use the validity assumption *)
+    fs [is_valid_fp_body_def] >>
+  
+(*    last_x_assum imp_res_tac >> *)
+    last_assum (qspecl_assume [‘SUC n'’, ‘SUC n''’]) >> fs [] >>
+    pop_assum imp_res_tac >>
+    pop_assum (qspec_assume ‘x’) >>
+    pop_assum sg_premise_tac >- fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def] >>
+    
+    fs [fix_fuel_def] >>
+
+    
+    fs [fix_fuel_P_def] >>
+    rfs [fix_fuel_P_def, is_diverge_def, fix_fuel_def] >>
+    
+    fs [fix_eq] >>
+
+    Cases_on ‘fix_fuel n' f x’ >> fs [] >>
+    last_assum (qspecl_then [‘n'’, ‘’
+    f (fix_fuel n' f) x >>
+
+    Cases_on ‘f x’ >> fs [] >>
+    rw [] >> fs [] >>
+    irule fix_fuel_mono_least >>
+    fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def]) >>
+  (* Divergence case *)
+  fs [fres_to_res_def] >>
+  sg ‘∀n. ~(fix_fuel_P f x (SUC n))’ >- fs [] >>
+  Cases_on ‘f x’ >> fs [] >>
+  fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def]  >>
+  rw []
+QED
+
+
+(* A slightly weaker and more precise validity criteria.
+
+   We simply extracted the part of the inductive proof that we can't prove without
+   knowing ‘f’.
+ *)
+val is_valid_fp_body_weak_def = Define ‘
+   is_valid_fp_body_weak f =
+   ∀n m x.
+   ((∀x. fix_fuel_P f x n ⇒ fix_fuel n f x = fix_fuel m f x) ⇒
+    n ≤ m ⇒
+    fix_fuel_P f x (SUC n) ⇒
+    fix_fuel (SUC n) f x = fix_fuel (SUC m) f x)
+’
+
+Theorem is_valid_fp_body_weak_imp_is_valid:
+  ∀f. is_valid_fp_body_weak f ⇒ is_valid_fp_body f
+Proof
+  rpt strip_tac >> fs [is_valid_fp_body_def] >>
+  Induct_on ‘n’ >- fs [fix_fuel_P_def, fix_fuel_def, is_diverge_def] >>
+  Cases_on ‘m’ >> fs [] >>
+  fs [is_valid_fp_body_weak_def]
+QED
+
+(* Testing on an example *)
+Datatype:
+  list_t =
+    ListCons 't list_t
+  | ListNil
+End
+
+val nth_body_def = Define ‘
+  nth_body (f : ('t list_t # u32) -> 't result) (x : ('t list_t # u32)) : 't result =
+    let (ls, i) = x in
+    case ls of
+    | ListCons x tl =>
+      if u32_to_int i = (0:int)
+      then (Return x)
+      else
+        do
+        i0 <- u32_sub i (int_to_u32 1);
+        f (tl, i0)
+        od
+    | ListNil => (Fail Failure)
+’ 
+
+(* The general proof of is_valid_fp_body. We isolate a more precise property below. *)
+Theorem nth_body_is_valid:
+  is_valid_fp_body nth_body
+Proof
+  pure_rewrite_tac [is_valid_fp_body_def] >>
+  Induct_on ‘n’ >- fs [fix_fuel_P_def, fix_fuel_def, is_diverge_def] >>
+  Cases_on ‘m’ >- fs [] >>
+  rpt strip_tac >>
+  (* TODO: here *)
+  last_assum imp_res_tac >>
+  (* TODO: here? *)
+  fs [fix_fuel_def, nth_body_def, fix_fuel_P_def, is_diverge_def, bind_def] >>
+  Cases_on ‘x’ >> fs [] >> (* TODO: automate this *)
+  (* Explore all paths *)
+  Cases_on ‘q’ >> fs [] >>
+  Cases_on ‘u32_to_int r = 0’ >> fs [] >>
+  Cases_on ‘u32_sub r (int_to_u32 1)’ >> fs []
+QED
+
+
+Theorem nth_body_is_valid_weak:
+  is_valid_fp_body_weak nth_body
+Proof
+  pure_rewrite_tac [is_valid_fp_body_weak_def] >>
+  rpt strip_tac >>
+  (* TODO: automate this - we may need to destruct a variable number of times *)
+  Cases_on ‘x’ >> fs [] >>
+  (* Expand all *)
+  fs [fix_fuel_def, nth_body_def, fix_fuel_P_def, is_diverge_def, bind_def] >>
+  (* Explore all paths *)
+  Cases_on ‘q’ >> fs [] >>
+  Cases_on ‘u32_to_int r = 0’ >> fs [] >>
+  Cases_on ‘u32_sub r (int_to_u32 1)’ >> fs []
+QED
+
+(*
+ * Test with a more general validity predicate.
+ *)
+(* We need to control the way calls to the continuation are performed, so
+   that we can inspect the inputs (otherwise we can't prove anything).
+ *)
+val is_valid_FP_body_def = Define ‘
+  is_valid_FP_body (f : (('a, 'b) fresult -> 'c) -> 'a -> 'c) =
+    ∃ (fa: (('a, 'b) fresult -> ('a, 'b) fresult) -> 'a -> ('a, 'b) fresult).
+      ∀ (g : ('a, 'b) fresult -> 'c) x.
+        f g x = g (fa (\x. x) x)
+’
+
+
+val fix_fuel_def = Define ‘
+  (fix_fuel (0 : num) (f : (('a, 'b) fresult -> 'b result) -> 'a -> 'b result) (x : 'a) : 'b result = Diverge) ∧
+  (fix_fuel (SUC n) (f : (('a, 'b) fresult -> 'b result) -> 'a -> 'b result) (x : 'a) : 'b result =
+    f (fres_to_res (fix_fuel n f)) x)
+’
+
+val fix_fuel_P_def = Define ‘
+  fix_fuel_P f x n = ~(is_diverge (fix_fuel n f x))
+’
+
+val fix_def = Define ‘
+  fix f x : 'b result =
+    if (∃ n. fix_fuel_P f x n) then fix_fuel ($LEAST (fix_fuel_P f x)) f x else Diverge
+’
+
+Theorem fix_fuel_mono:
+  ∀f. is_valid_FP_body f ⇒
+  ∀n m. n <= m ⇒ (∀x. fix_fuel_P f x n ⇒ fix_fuel n f x = fix_fuel m f x)
+Proof
+  strip_tac >> strip_tac >>
+  Induct_on ‘n’ >> rpt strip_tac
+  >- (fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def]) >>
+  fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def, fres_to_res_def] >>
+  Cases_on ‘m’ >- int_tac >>
+  fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def] >>
+  fs [is_valid_FP_body_def, fres_to_res_def] >>
+  CASE_TAC >>
+  last_x_assum (qspec_assume ‘fres_to_res (fix_fuel n f)’) >>
+  fs [fres_to_res_def]
+QED
+
+(* Tests *)
+
+
+
+Datatype:
+  list_t =
+    ListCons 't list_t
+  | ListNil
+End
+
+(*
+val def_qt = ‘
+  nth_mut_fwd (ls : 't list_t) (i : u32) : 't result =
+  case ls of
+  | ListCons x tl =>
+    if u32_to_int i = (0:int)
+    then Return x
+    else
+      do
+      i0 <- u32_sub i (int_to_u32 1);
+      nth_mut_fwd tl i0
+      od
+  | ListNil =>
+    Fail Failure
+’
+*)
+
+val nth_body_def = Define ‘
+  nth_body (f : ('t list_t # u32, 't) fresult -> 'c) (ls : 't list_t, i : u32) : 'c =
+    case ls of
+    | ListCons x tl =>
+      if u32_to_int i = (0:int)
+      then f (FReturn x)
+      else
+        do
+        i0 <- u32_sub i (int_to_u32 1);
+        f (FRec (tl, i0))
+        od
+    | ListNil => f (FFail Failure)
+’
+
+Theorem nth_body_is_valid_FP_body:
+  is_valid_FP_body nth_body
+Proof
+  fs [is_valid_FP_body_def] >>
+  exists_tac “nth_body” >>
+QED
+
+“nth_body”
+
+(* TODO: abbreviation for ‘(\g y. fres_to_res g (f y))’ *)
+Theorem fix_fixed_eq:
+  ∀f x. fix (\g y. fres_to_res g (f y)) x =
+     (f x)
+    fres_to_res (\g y. fres_to_res g (f y))
+
+
+
+(*
+TODO: can't prove that
+
+Theorem fix_fuel_mono:
+  ∀n m. n <= m ⇒ (∀f x. fix_fuel_P f x n ⇒ fix_fuel n f x = fix_fuel m f x)
+Proof
+  Induct_on ‘n’ >> rpt strip_tac
+  >- (fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def]) >>
+  fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def] >>
+  Cases_on ‘m’ >- int_tac >>
+  fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def] >>
+
+  sg ‘fix_fuel n f = fix_fuel n' f’ >>
+
+  last_x_assum imp_res_tac >>
+  pop_assum (qspecl_assume [‘x’, ‘f’]) >>
+
+Theorem fix_def_eq:
+  ∀f x. fix f x = f (fix f) x
+Proof
+  
+*)
+*)
+
+
+val _ = export_theory ()
diff --git a/backends/hol4/divDefProtoTheory.sig b/backends/hol4/divDefProtoTheory.sig
new file mode 100644
index 00000000..6e4e5950
--- /dev/null
+++ b/backends/hol4/divDefProtoTheory.sig
@@ -0,0 +1,210 @@
+signature divDefProtoTheory =
+sig
+  type thm = Thm.thm
+  
+  (*  Definitions  *)
+    val fix_def : thm
+    val fix_fuel_P_def : thm
+    val fix_fuel_def : thm
+    val is_valid_fp_body_def : thm
+    val list_t_TY_DEF : thm
+    val list_t_case_def : thm
+    val list_t_size_def : thm
+    val nth_body_def : thm
+  
+  (*  Theorems  *)
+    val datatype_list_t : thm
+    val fix_fixed_diverges : thm
+    val fix_fixed_eq : thm
+    val fix_fixed_terminates : thm
+    val fix_fixed_termination_rec_case : thm
+    val fix_fuel_compute : thm
+    val fix_fuel_mono : thm
+    val fix_fuel_mono_least : thm
+    val is_valid_suffice : thm
+    val list_t_11 : thm
+    val list_t_Axiom : thm
+    val list_t_case_cong : thm
+    val list_t_case_eq : thm
+    val list_t_distinct : thm
+    val list_t_induction : thm
+    val list_t_nchotomy : thm
+    val nth_body_is_valid : thm
+    val nth_def : thm
+  
+  val divDefProto_grammars : type_grammar.grammar * term_grammar.grammar
+(*
+   [primitives] Parent theory of "divDefProto"
+   
+   [fix_def]  Definition
+      
+      ⊢ ∀f x.
+          fix f x =
+          if ∃n. fix_fuel_P f x n then
+            fix_fuel ($LEAST (fix_fuel_P f x)) f x
+          else Diverge
+   
+   [fix_fuel_P_def]  Definition
+      
+      ⊢ ∀f x n. fix_fuel_P f x n ⇔ ¬is_diverge (fix_fuel n f x)
+   
+   [fix_fuel_def]  Definition
+      
+      ⊢ (∀f x. fix_fuel 0 f x = Diverge) ∧
+        ∀n f x. fix_fuel (SUC n) f x = f (fix_fuel n f) x
+   
+   [is_valid_fp_body_def]  Definition
+      
+      ⊢ ∀f. is_valid_fp_body f ⇔
+            ∀x. (∀g h. f g x = f h x) ∨ ∃y. ∀g. f g x = g y
+   
+   [list_t_TY_DEF]  Definition
+      
+      ⊢ ∃rep.
+          TYPE_DEFINITION
+            (λa0'.
+                 ∀ $var$('list_t').
+                   (∀a0'.
+                      (∃a0 a1.
+                         a0' =
+                         (λa0 a1.
+                              ind_type$CONSTR 0 a0
+                                (ind_type$FCONS a1 (λn. ind_type$BOTTOM)))
+                           a0 a1 ∧ $var$('list_t') a1) ∨
+                      a0' =
+                      ind_type$CONSTR (SUC 0) ARB (λn. ind_type$BOTTOM) ⇒
+                      $var$('list_t') a0') ⇒
+                   $var$('list_t') a0') rep
+   
+   [list_t_case_def]  Definition
+      
+      ⊢ (∀a0 a1 f v. list_t_CASE (ListCons a0 a1) f v = f a0 a1) ∧
+        ∀f v. list_t_CASE ListNil f v = v
+   
+   [list_t_size_def]  Definition
+      
+      ⊢ (∀f a0 a1.
+           list_t_size f (ListCons a0 a1) = 1 + (f a0 + list_t_size f a1)) ∧
+        ∀f. list_t_size f ListNil = 0
+   
+   [nth_body_def]  Definition
+      
+      ⊢ ∀f x.
+          nth_body f x =
+          (let
+             (ls,i) = x
+           in
+             case ls of
+               ListCons x tl =>
+                 if u32_to_int i = 0 then Return x
+                 else do i0 <- u32_sub i (int_to_u32 1); f (tl,i0) od
+             | ListNil => Fail Failure)
+   
+   [datatype_list_t]  Theorem
+      
+      ⊢ DATATYPE (list_t ListCons ListNil)
+   
+   [fix_fixed_diverges]  Theorem
+      
+      ⊢ ∀f. is_valid_fp_body f ⇒
+            ∀x. ¬(∃n. fix_fuel_P f x n) ⇒ fix f x = f (fix f) x
+   
+   [fix_fixed_eq]  Theorem
+      
+      ⊢ ∀f. is_valid_fp_body f ⇒ ∀x. fix f x = f (fix f) x
+   
+   [fix_fixed_terminates]  Theorem
+      
+      ⊢ ∀f. is_valid_fp_body f ⇒
+            ∀x n. fix_fuel_P f x n ⇒ fix f x = f (fix f) x
+   
+   [fix_fixed_termination_rec_case]  Theorem
+      
+      ⊢ ∀x y n m.
+          is_valid_fp_body f ⇒
+          (∀g. f g x = g y) ⇒
+          fix_fuel_P f x n ⇒
+          fix_fuel_P f y m ⇒
+          fix_fuel ($LEAST (fix_fuel_P f x)) f x =
+          fix_fuel ($LEAST (fix_fuel_P f y)) f y
+   
+   [fix_fuel_compute]  Theorem
+      
+      ⊢ (∀f x. fix_fuel 0 f x = Diverge) ∧
+        (∀n f x.
+           fix_fuel (NUMERAL (BIT1 n)) f x =
+           f (fix_fuel (NUMERAL (BIT1 n) − 1) f) x) ∧
+        ∀n f x.
+          fix_fuel (NUMERAL (BIT2 n)) f x =
+          f (fix_fuel (NUMERAL (BIT1 n)) f) x
+   
+   [fix_fuel_mono]  Theorem
+      
+      ⊢ ∀f. is_valid_fp_body f ⇒
+            ∀n x.
+              fix_fuel_P f x n ⇒
+              ∀m. n ≤ m ⇒ fix_fuel n f x = fix_fuel m f x
+   
+   [fix_fuel_mono_least]  Theorem
+      
+      ⊢ ∀f. is_valid_fp_body f ⇒
+            ∀n x.
+              fix_fuel_P f x n ⇒
+              fix_fuel n f x = fix_fuel ($LEAST (fix_fuel_P f x)) f x
+   
+   [is_valid_suffice]  Theorem
+      
+      ⊢ ∃y. ∀g. g x = g y
+   
+   [list_t_11]  Theorem
+      
+      ⊢ ∀a0 a1 a0' a1'.
+          ListCons a0 a1 = ListCons a0' a1' ⇔ a0 = a0' ∧ a1 = a1'
+   
+   [list_t_Axiom]  Theorem
+      
+      ⊢ ∀f0 f1. ∃fn.
+          (∀a0 a1. fn (ListCons a0 a1) = f0 a0 a1 (fn a1)) ∧
+          fn ListNil = f1
+   
+   [list_t_case_cong]  Theorem
+      
+      ⊢ ∀M M' f v.
+          M = M' ∧ (∀a0 a1. M' = ListCons a0 a1 ⇒ f a0 a1 = f' a0 a1) ∧
+          (M' = ListNil ⇒ v = v') ⇒
+          list_t_CASE M f v = list_t_CASE M' f' v'
+   
+   [list_t_case_eq]  Theorem
+      
+      ⊢ list_t_CASE x f v = v' ⇔
+        (∃t l. x = ListCons t l ∧ f t l = v') ∨ x = ListNil ∧ v = v'
+   
+   [list_t_distinct]  Theorem
+      
+      ⊢ ∀a1 a0. ListCons a0 a1 ≠ ListNil
+   
+   [list_t_induction]  Theorem
+      
+      ⊢ ∀P. (∀l. P l ⇒ ∀t. P (ListCons t l)) ∧ P ListNil ⇒ ∀l. P l
+   
+   [list_t_nchotomy]  Theorem
+      
+      ⊢ ∀ll. (∃t l. ll = ListCons t l) ∨ ll = ListNil
+   
+   [nth_body_is_valid]  Theorem
+      
+      ⊢ is_valid_fp_body nth_body
+   
+   [nth_def]  Theorem
+      
+      ⊢ ∀ls i.
+          nth ls i =
+          case ls of
+            ListCons x tl =>
+              if u32_to_int i = 0 then Return x
+              else do i0 <- u32_sub i (int_to_u32 1); nth tl i0 od
+          | ListNil => Fail Failure
+   
+   
+*)
+end