From 8a5c5e4ae0cab0ab627c25ece59453a8e4bd4b64 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 12 May 2023 20:17:26 +0200
Subject: Cleanup the files of the HOL4 backend

---
 backends/hol4/divDefProto2Script.sml | 566 -----------------------------------
 1 file changed, 566 deletions(-)
 delete mode 100644 backends/hol4/divDefProto2Script.sml

(limited to 'backends/hol4/divDefProto2Script.sml')

diff --git a/backends/hol4/divDefProto2Script.sml b/backends/hol4/divDefProto2Script.sml
deleted file mode 100644
index 9efe835b..00000000
--- a/backends/hol4/divDefProto2Script.sml
+++ /dev/null
@@ -1,566 +0,0 @@
-(* 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 "divDefProto2"
-
-(*
- * 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 (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))
-’
-
-(* Auxiliary lemma.
-   We generalize the goal of fix_fuel_mono in the case the fuel is non-empty
-   (this allows us to unfold definitions like ‘fix_fuel’ once, and reveal
-   a first intermediate function).
-
-   Important: the structure of the proof is induction over ‘n’ then ‘N’.
- *)
-Theorem fix_fuel_mono_aux:
-  ∀n.
-    ∀N M g f. is_valid_fp_body M f ⇒
-      is_valid_fp_body N g ⇒
-      ∀x. ~(is_diverge (g (fix_fuel n f) x)) ⇒
-       ∀m. n ≤ m ⇒
-         g (fix_fuel n f) x = g (fix_fuel m f) x
-Proof
-  Induct_on ‘n’ >>
-  Induct_on ‘N’ >- fs [is_valid_fp_body_def]
-  >-(  
-    rw [] >>
-    fs [is_valid_fp_body_def, is_diverge_def] >>
-    first_x_assum (qspec_assume ‘x’) >>
-    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’) >>
-    fs [] >>
-    ntac 3 (pop_assum ignore_tac) >>
-    fs [bind_def] >>
-    fs [fix_fuel_def])
-  >-(fs [is_valid_fp_body_def]) >>
-  rw [] >>
-  qpat_assum ‘is_valid_fp_body (SUC N) g’ mp_tac >>
-  pure_rewrite_tac [is_valid_fp_body_def] >>
-  fs [is_diverge_def] >>
-  rw [] >>
-  first_x_assum (qspec_assume ‘x’) >>
-  rw []
-  >-((* Case 1: the continuation doesn't matter *) fs []) >>
-  (* Case 2: the continuation *does* matter (i.e., there is a recursive call *)
-  (* Use the validity property with the different continuations *)
-  fs [] >> pop_assum ignore_tac >>
-  fs [bind_def, fix_fuel_def] >>
-  Cases_on ‘m’ >- int_tac >>
-  fs [fix_fuel_def] >>
-  (* *)
-  last_x_assum (qspecl_assume [‘M’, ‘M’, ‘f’, ‘f’]) >>
-  gvs [] >>
-  first_x_assum (qspec_assume ‘y’) >>
-  Cases_on ‘f (fix_fuel n f) y’ >> fs [] >>
-  first_x_assum (qspec_assume ‘n'’) >> gvs [] >> Cases_on ‘f (fix_fuel n' f) y’ >> fs [] >>
-  (* *)  
-  first_assum (qspecl_assume [‘M’, ‘h’, ‘f’]) >>
-  gvs []
-QED
-
-Theorem fix_fuel_mono:
-  ∀N f. is_valid_fp_body N f ⇒
-    ∀n x. fix_fuel_P f x n ⇒
-     ∀ m. n ≤ m ⇒
-       fix_fuel n f x = fix_fuel m f x
-Proof
-  rw [] >>
-  Cases_on ‘n’
-  >-(fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def]) >>
-  fs [fix_fuel_P_def, fix_fuel_def] >> rw [] >>
-  qspecl_assume [‘n'’, ‘N’, ‘N’, ‘f’, ‘f’] fix_fuel_mono_aux >>
-  Cases_on ‘m’ >- fs [] >>
-  gvs [fix_fuel_def]
-QED
-
-(* TODO: remove? *)
-Theorem fix_fuel_mono_least:
-  ∀N f. is_valid_fp_body N 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 [] >>
-  conj_tac
-  >- (spose_not_then assume_tac >> fs [not_le_eq_gt]) >>
-  metis_tac []
-QED
-
-Theorem fix_fuel_eq_fix:
-  ∀N f. is_valid_fp_body N f ⇒
-    ∀n x. fix_fuel_P f x n ⇒
-      fix_fuel n f x = fix f x
-Proof
-  fs [fix_def] >>
-  rw [] >>
-  imp_res_tac fix_fuel_mono_least >>
-  fs [fix_fuel_P_def, is_diverge_def] >>
-  case_tac >> fs []
-QED
-
-Theorem fix_fuel_P_least:
-  ∀f n x. fix_fuel n f x ≠ Diverge ⇒ fix_fuel_P f x ($LEAST (fix_fuel_P f x))
-Proof
-  rw [] >>
-  qspec_assume ‘fix_fuel_P f x’ whileTheory.LEAST_EXISTS_IMP >>
-  (* Prove the premise *)
-  pop_assum sg_premise_tac
-  >-(fs [fix_fuel_P_def, is_diverge_def] >> qexists ‘n’ >> fs [] >> case_tac >> fs []) >>
-  rw []
-QED
-
-(* If ‘g (fix f) x’ doesn't diverge, we can exhibit some fuel *)
-Theorem fix_not_diverge_implies_fix_fuel_aux:
-  ∀N M g f. is_valid_fp_body M f ⇒
-    is_valid_fp_body N g ⇒
-     ∀x. g (fix f) x ≠ Diverge ⇒
-       ∃n. g (fix f) x = g (fix_fuel n f) x ∧
-         ∀m. n ≤ m ⇒ g (fix_fuel m f) x = g (fix_fuel n f) x
-Proof
-  Induct_on ‘N’
-  >-(fs [is_valid_fp_body_def]) >>
-  rw [is_valid_fp_body_def] >>
-  first_x_assum (qspec_assume ‘x’) >> rw []
-  >-(first_assum (qspecl_assume [‘fix f’, ‘fix_fuel 0 f’]) >> fs []) >>
-  (* Use the validity hypothesis *)
-  fs [] >> pop_assum ignore_tac >>
-  (* Use the induction hypothesis *)
-  last_x_assum (qspecl_assume [‘M’, ‘h’, ‘f’]) >> gvs [] >>
-  (* Case disjunction on ‘fix f ÿ’*)
-  Cases_on ‘fix f y’ >> fs [bind_def] >~ [‘fix f y = Fail _’]
-  >-(
-    (* Fail case: easy, the call to ‘h’ is ignored *)
-    fs [fix_def] >> pop_assum mp_tac >> rw [] >>
-    qexists ‘$LEAST (fix_fuel_P f y)’ >>
-    fs [] >>
-    (* Use the monotonicity property for ‘f’ *)
-    rw [] >>
-    qspecl_assume [‘M’, ‘f’] fix_fuel_mono >> gvs [] >>
-    first_x_assum (qspecl_assume [‘$LEAST (fix_fuel_P f y)’, ‘y’]) >> gvs [] >>
-    fs [fix_fuel_P_def, is_diverge_def] >> gvs [] >>
-    first_x_assum (qspecl_assume [‘m’]) >> gvs [] >>
-    first_x_assum (fn th => assume_tac (GSYM th)) >> fs []
-    ) >>
-  (* Return case: we must take the maximum of the fuel for ‘f’ and ‘h’, and use
-     the monotonicity property *)
-  fs [fix_def] >> pop_assum mp_tac >> rw [] >>
-  first_x_assum (qspec_assume ‘a’) >> gvs [] >>
-  qexists ‘MAX ($LEAST (fix_fuel_P f y)) n'’ >> fs [] >>
-  (* Use the monotonicity properties *)
-  (* Instantiate the Monotonicity property for ‘f’ (the induction hypothesis gives
-     the one for ‘h’) *)
-  qspecl_assume [‘M’, ‘f’] fix_fuel_mono >> gvs [] >>
-  first_x_assum (qspecl_assume [‘$LEAST (fix_fuel_P f y)’, ‘y’]) >> gvs [] >>
-  fs [fix_fuel_P_def, is_diverge_def] >> gvs [] >>
-  first_x_assum (qspecl_assume [‘MAX ($LEAST (fix_fuel_P f y)) n'’]) >> gvs [] >>
-  first_x_assum (fn th => assume_tac (GSYM th)) >> fs [] >>
-  (* Prove the monotonicity property for ‘do z <- fix f y; h (fix f) z’ *)
-  rw [] >>
-  (* First, one of the ‘fix_fuel ... f y’ doesn't use the proper fuel *)
-  sg ‘fix_fuel ($LEAST (fix_fuel_P f y)) f y = Return a’
-  >-(
-    qspecl_assume [‘f’, ‘MAX ($LEAST (fix_fuel_P f y)) n'’, ‘y’] fix_fuel_P_least >>
-    gvs [fix_fuel_P_def, is_diverge_def] >>
-    Cases_on ‘fix_fuel ($LEAST (fix_fuel_P f y)) f y’ >> fs [] >>
-    (* Use the monotonicity property - there are two goals here *)
-    qspecl_assume [‘M’, ‘f’] fix_fuel_mono >> gvs [] >>
-    first_x_assum (qspecl_assume [‘$LEAST (fix_fuel_P f y)’, ‘y’]) >> gvs [] >>
-    fs [fix_fuel_P_def, is_diverge_def] >> gvs [] >>
-    first_x_assum (qspecl_assume [‘MAX ($LEAST (fix_fuel_P f y)) n'’]) >> gvs []) >>
-  (* Instantiate the monotonicity property for ‘f’ *)
-  qspecl_assume [‘M’, ‘f’] fix_fuel_mono >> gvs [] >>
-  first_x_assum (qspecl_assume [‘$LEAST (fix_fuel_P f y)’, ‘y’]) >> gvs [] >>
-  gvs [fix_fuel_P_def, is_diverge_def] >> gvs [] >>
-  first_x_assum (qspecl_assume [‘m’]) >> gvs [] >>
-  first_x_assum (fn th => assume_tac (GSYM th)) >> fs []
-QED
-
-(* If ‘g (fix f) x’ doesn't diverge, we can exhibit some fuel *)
-Theorem fix_not_diverge_implies_fix_fuel:
-  ∀N f. is_valid_fp_body N f ⇒
-     ∀x. f (fix f) x ≠ Diverge ⇒
-       ∃n. f (fix f) x = f (fix_fuel n f) x
-Proof
-  metis_tac [fix_not_diverge_implies_fix_fuel_aux]
-QED    
-
-Theorem fix_fixed_diverges:
-  ∀N f. is_valid_fp_body N f ⇒ ∀x. ~(∃ n. fix_fuel_P f x n) ⇒ fix f x = f (fix f) x
-Proof
-  (* We do the proof by contraposition: if ‘f (fix f) x’ doesn't diverge, we
-     can exhibit some fuel (lemma [fix_not_diverge_implies_fix_fuel]) *)
-  rw [fix_def] >>
-  imp_res_tac fix_not_diverge_implies_fix_fuel >>
-  pop_assum (qspec_assume ‘x’) >>
-  fs [fix_fuel_P_def, is_diverge_def] >>
-  (* Case analysis: we have to prove that the ‘Return’ and ‘Fail’ cases lead
-     to a contradiction *)
-  Cases_on ‘f (fix f) x’ >> gvs [] >>
-  first_x_assum (qspec_assume ‘SUC n’) >> fs [fix_fuel_def] >>
-  pop_assum mp_tac >> case_tac >> fs []
-QED
-
-(* If ‘g (fix_fuel n f) x’ doesn't diverge, then it is equal to ‘g (fix f) x’ *)
-Theorem fix_fuel_not_diverge_eq_fix_aux:
-  ∀N M g f. is_valid_fp_body M f ⇒
-    is_valid_fp_body N g ⇒
-     ∀n x. g (fix_fuel n f) x ≠ Diverge ⇒
-       g (fix f) x = g (fix_fuel n f) x
-Proof
-  Induct_on ‘N’
-  >-(fs [is_valid_fp_body_def]) >>
-  rw [is_valid_fp_body_def] >>
-  first_x_assum (qspec_assume ‘x’) >> rw []
-  >-(first_assum (qspecl_assume [‘fix f’, ‘fix_fuel 0 f’]) >> fs []) >>
-  (* Use the validity hypothesis *)
-  fs [] >> pop_assum ignore_tac >>
-  (* For ‘fix f y = fix_fuel n f y’: use the monotonicity property *)
-  sg ‘fix_fuel_P f y n’
-  >-(Cases_on ‘fix_fuel n f y’ >> fs [fix_fuel_P_def, is_diverge_def, bind_def]) >>
-  sg ‘fix f y = fix_fuel n f y’ >-(metis_tac [fix_fuel_eq_fix])>>
-  (* Case disjunction on the call to ‘f’ *)
-  Cases_on ‘fix_fuel n f y’ >> gvs [bind_def] >>
-  (* We have to prove that: ‘h (fix f) a = h (fix_fuel n f) a’: use the induction hypothesis *)
-  metis_tac []
-QED
-
-Theorem fix_fuel_not_diverge_eq_fix:
-  ∀N f. is_valid_fp_body N f ⇒
-     ∀n x. f (fix_fuel n f) x ≠ Diverge ⇒
-       f (fix f) x = f (fix_fuel n f) x
-Proof
-  metis_tac [fix_fuel_not_diverge_eq_fix_aux]
-QED
-
-Theorem fix_fixed_terminates:
-  ∀N f. is_valid_fp_body N f ⇒ ∀x n. fix_fuel_P f x n ⇒ fix f x = f (fix f) x
-Proof
-  (* The proof simply uses the lemma [fix_fuel_not_diverge_eq_fix] *)
-  rw [fix_fuel_P_def, is_diverge_def, fix_def] >> case_tac >> fs [] >>
-  (* We can prove that ‘fix_fuel ($LEAST ...) f x ≠ Diverge’ *)
-  qspecl_assume [‘f’, ‘n’, ‘x’] fix_fuel_P_least >>
-  pop_assum sg_premise_tac >-(Cases_on ‘fix_fuel n f x’ >> fs []) >>
-  fs [fix_fuel_P_def, is_diverge_def] >>
-  (* *)
-  Cases_on ‘($LEAST (fix_fuel_P f x))’ >> fs [fix_fuel_def] >>
-  irule (GSYM fix_fuel_not_diverge_eq_fix) >>
-  Cases_on ‘f (fix_fuel n'' f) x’ >> fs [] >> metis_tac []
-QED
-
-Theorem fix_fixed_eq:
-  ∀N f. is_valid_fp_body N 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 >>
-  metis_tac []
-QED  
-
-(*======================
- * Example 1: nth
- *======================*)
-Datatype:
-  list_t =
-    ListCons 't list_t
-  | ListNil
-End
-
-(* We use this version of the body to prove that the body is valid *)
-val nth_body_def = Define ‘
-  nth_body (f : (('t list_t # u32) + 't) -> (('t list_t # u32) + 't) result)
-    (x : (('t list_t # u32) + 't)) :
-    (('t list_t # u32) + 't) result =
-    (* Destruct the input. We need this to call the proper function in case
-       of mutually recursive definitions, but also to eliminate arguments
-       which correspond to the output value (the input type is the same
-       as the output type). *)
-    case x of
-    | INL x => (
-      let (ls, i) = x in
-      case ls of
-      | ListCons x tl =>
-        if u32_to_int i = (0:int)
-        then Return (INR x)
-        else
-          do
-          i0 <- u32_sub i (int_to_u32 1);
-          r <- f (INL (tl, i0));
-          (* Eliminate the invalid outputs. This is not necessary here,
-             but it is in the case of non tail call recursive calls. *)
-          case r of
-          | INL _ => Fail Failure
-          | INR i1 => Return (INR i1)
-          od
-      | ListNil => Fail Failure)
-    | INR _ => Fail Failure
-’
-
-(* We first prove the theorem with ‘SUC (SUC n)’ where ‘n’ is a variable
-   to prevent this quantity from being rewritten to 2 *)
-Theorem nth_body_is_valid_aux:
-  is_valid_fp_body (SUC (SUC n)) nth_body
-Proof
-  pure_once_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 ‘x'’ >> fs [] >>
-  Cases_on ‘q’ >> fs [] >>
-  Cases_on ‘u32_to_int r = 0’ >> fs [] >>
-  Cases_on ‘u32_sub r (int_to_u32 1)’ >> fs [] >>
-  disj2_tac >>
-  (* This is hard *)
-  qexists ‘\g x. case x of | INL _ => Fail Failure | INR i1 => Return (INR i1)’ >>
-  qexists ‘INL (l, a)’ >>
-  conj_tac
-  >-(
-    (* Prove that the body of h is valid *)
-    pure_once_rewrite_tac [is_valid_fp_body_def] >>
-    (* *)
-    fs []) >>
-  gen_tac >>
-  (* Explore all paths *)
-  Cases_on ‘g (INL (l,a))’ >> fs [] >>
-  Cases_on ‘a'’ >> fs []
-QED
-
-Theorem nth_body_is_valid:
-  is_valid_fp_body (SUC (SUC 0)) nth_body
-Proof
-  irule nth_body_is_valid_aux
-QED
-
-val nth_raw_def = Define ‘
-  nth (ls : 't list_t) (i : u32) =
-    case fix nth_body (INL (ls, i)) of
-    | Fail e => Fail e
-    | Diverge => Diverge
-    | Return r =>
-      case r of
-      | INL _ => Fail Failure
-      | INR x => Return x
-’
-
-(* Rewrite the goal once, and on the left part of the goal seen as an application *)
-fun pure_once_rewrite_left_tac ths =
-  CONV_TAC (PATH_CONV "l" (PURE_ONCE_REWRITE_CONV ths))
-
-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 - the rewrite must only be applied *on the left* of the equality, in the goal *)
-  pure_once_rewrite_left_tac [HO_MATCH_MP fix_fixed_eq nth_body_is_valid] >>
-  (* Expand the body definition *)
-  pure_rewrite_tac [nth_body_def] >>
-  (* Explore all the paths - maybe we can be smarter, but this is fast and really easy *)
-  fs [bind_def] >>
-  Cases_on ‘ls’ >> fs [] >>
-  Cases_on ‘u32_to_int i = 0’ >> fs [] >>
-  Cases_on ‘u32_sub i (int_to_u32 1)’ >> fs [] >>
-  Cases_on ‘fix nth_body (INL (l,a))’ >> fs [] >>
-  Cases_on ‘a'’ >> fs []
-QED
-
-(*======================
- * Example 2: even, odd
- *======================*)
-
-val even_odd_body_def = Define ‘
-  even_odd_body
-    (f : (int + int + bool) -> (int + int + bool) result)
-    (x : int + int + bool) : (int + int + bool) result =
-    case x of
-    | INL i =>
-      (* Even *)
-      if i = 0 then Return (INR (INR T))
-      else
-        (case f (INR (INL (i - 1))) of
-         | Fail e => Fail e
-         | Diverge => Diverge
-         | Return r =>
-           (* Eliminate the unwanted results *)
-           case r of
-           | INL _ => Fail Failure
-           | INR (INL _) => Fail Failure
-           | INR (INR b) => Return (INR (INR b))
-           )
-    | INR x =>
-      case x of
-      | INL i =>
-        (* Odd *)
-        if i = 0 then Return (INR (INR F))
-        else
-          (case f (INL (i - 1)) of
-           | Fail e => Fail e
-           | Diverge => Diverge
-           | Return r =>
-             (* Eliminate the unwanted results *)
-             case r of
-             | INL _ => Fail Failure
-             | INR (INL _) => Fail Failure
-             | INR (INR b) => Return (INR (INR b))
-             )
-      | INR _ =>
-        (* This case is for the return value *)
-        Fail Failure
-’
-
-Theorem even_odd_body_is_valid_aux:
-  is_valid_fp_body (SUC (SUC n)) even_odd_body
-Proof
-  pure_once_rewrite_tac [is_valid_fp_body_def] >>
-  gen_tac >>
-  (* Expand *)
-  fs [even_odd_body_def, bind_def] >>
-  (* TODO: automate this *)
-  Cases_on ‘x’ >> fs []
-  >-(
-    Cases_on ‘x' = 0’ >> fs [] >>
-    (* Recursive call *)
-    disj2_tac >>
-    qexists ‘\g x. case x of | INL _ => Fail Failure | INR (INL _) => Fail Failure | INR (INR i1) => Return (INR (INR i1))’ >>
-    qexists ‘INR (INL (x' − 1))’ >>
-    conj_tac
-    >-(pure_once_rewrite_tac [is_valid_fp_body_def] >> fs []) >>
-    fs []) >>
-  Cases_on ‘y’ >> fs []  >>
-  Cases_on ‘x = 0’ >> fs []  >>
-  (* Recursive call *)
-  disj2_tac >>
-  qexists ‘\g x. case x of | INL _ => Fail Failure | INR (INL _) => Fail Failure | INR (INR i1) => Return (INR (INR i1))’ >>
-  qexists ‘INL (x − 1)’ >>
-  conj_tac
-  >-(pure_once_rewrite_tac [is_valid_fp_body_def] >> fs []) >>
-  fs []
-QED
-
-Theorem even_odd_body_is_valid:
-  is_valid_fp_body (SUC (SUC 0)) even_odd_body
-Proof
-  irule even_odd_body_is_valid_aux
-QED
-
-val even_raw_def = Define ‘
-  even (i : int) =
-    case fix even_odd_body (INL i) of
-    | Fail e => Fail e
-    | Diverge => Diverge
-    | Return r =>
-      case r of
-      | INL _ => Fail Failure
-      | INR (INL _) => Fail Failure
-      | INR (INR b) => Return b
-’
-
-val odd_raw_def = Define ‘
-  odd (i : int) =
-    case fix even_odd_body (INR (INL i)) of
-    | Fail e => Fail e
-    | Diverge => Diverge
-    | Return r =>
-      case r of
-      | INL _ => Fail Failure
-      | INR (INL _) => Fail Failure
-      | INR (INR b) => Return b
-’
-
-Theorem even_def:
-  ∀i. even (i : int) : bool result =
-    if i = 0 then Return T else odd (i - 1)
-Proof
-  gen_tac >>
-  (* Expand the definition *)
-  pure_once_rewrite_tac [even_raw_def] >>
-  (* Use the fixed-point equality *)
-  pure_once_rewrite_left_tac [HO_MATCH_MP fix_fixed_eq even_odd_body_is_valid] >>
-  (* Expand the body definition *)
-  pure_rewrite_tac [even_odd_body_def] >>
-  (* Expand all the definitions from the group *)
-  pure_rewrite_tac [even_raw_def, odd_raw_def] >>
-  (* Explore all the paths - maybe we can be smarter, but this is fast and really easy *)
-  fs [bind_def] >>
-  Cases_on ‘i = 0’ >> fs [] >>
-  Cases_on ‘fix even_odd_body (INR (INL (i − 1)))’ >> fs [] >>
-  Cases_on ‘a’ >> fs [] >>
-  Cases_on ‘y’ >> fs []
-QED
-
-Theorem odd_def:
-  ∀i. odd (i : int) : bool result =
-    if i = 0 then Return F else even (i - 1)
-Proof
-  gen_tac >>
-  (* Expand the definition *)
-  pure_once_rewrite_tac [odd_raw_def] >>
-  (* Use the fixed-point equality *)
-  pure_once_rewrite_left_tac [HO_MATCH_MP fix_fixed_eq even_odd_body_is_valid] >>
-  (* Expand the body definition *)
-  pure_rewrite_tac [even_odd_body_def] >>
-  (* Expand all the definitions from the group *)
-  pure_rewrite_tac [even_raw_def, odd_raw_def] >>
-  (* Explore all the paths - maybe we can be smarter, but this is fast and really easy *)
-  fs [bind_def] >>
-  Cases_on ‘i = 0’ >> fs [] >>
-  Cases_on ‘fix even_odd_body (INL (i − 1))’ >> fs [] >>
-  Cases_on ‘a’ >> fs [] >>
-  Cases_on ‘y’ >> fs []
-QED
-
-val _ = export_theory ()
-- 
cgit v1.2.3