summaryrefslogtreecommitdiff
path: root/backends/hol4/divDefNoFixLib.sml
blob: 59319e6a300ba546a623e3fc6d7b21043c8e8317 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053
1054
1055
1056
1057
1058
1059
1060
1061
1062
1063
1064
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
1076
1077
1078
1079
1080
1081
1082
1083
1084
1085
1086
1087
1088
1089
1090
1091
1092
1093
1094
1095
1096
1097
1098
1099
1100
1101
1102
1103
1104
1105
1106
1107
1108
1109
1110
1111
1112
1113
1114
1115
1116
1117
1118
1119
1120
1121
1122
1123
1124
1125
1126
1127
1128
1129
1130
1131
1132
1133
1134
1135
1136
1137
1138
1139
1140
1141
1142
1143
1144
1145
1146
1147
1148
1149
1150
1151
1152
1153
1154
1155
1156
1157
1158
1159
1160
1161
1162
1163
1164
1165
1166
1167
1168
1169
1170
1171
1172
1173
1174
1175
1176
1177
1178
1179
1180
1181
1182
1183
1184
1185
1186
1187
1188
1189
1190
1191
1192
1193
1194
1195
1196
1197
1198
1199
1200
1201
1202
1203
(* **DEPRECATED**: see divDefLib *)

structure divDefNoFixLib :> divDefNoFixLib =
struct

open HolKernel boolLib bossLib Parse
open boolTheory arithmeticTheory integerTheory intLib listTheory stringTheory

open primitivesArithTheory primitivesBaseTacLib ilistTheory primitivesTheory
open primitivesLib

val case_result_same_eq = prove (
  “!(r : 'a result).
    (case r of
       Return x => Return x
     | Fail e => Fail e
     | Diverge => Diverge) = r”,
  rw [] >> CASE_TAC)

(*
val ty = id_ty
strip_arrows ty
*)

(* TODO: move *)
fun list_mk_arrow (tys : hol_type list) (ret_ty : hol_type) : hol_type =
  foldr (fn (ty, aty) => ty --> aty) ret_ty tys

(* TODO: move *)
fun strip_arrows (ty : hol_type) : hol_type list * hol_type =
  let
    val (ty0, ty1) = dom_rng ty
    val (tys, ret) = strip_arrows ty1
  in
    (ty0::tys, ret)
  end
  handle HOL_ERR _ => ([], ty)

(* Small utilities *)
val current_goal : term option ref = ref NONE

(* Save a goal in {!current_goal} then prove it.

   This way if the proof fails we can easily retrieve the goal for debugging
   purposes.
 *)
fun save_goal_and_prove (g, tac) : thm =
  let
    val _ = current_goal := SOME g
  in
    prove (g, tac)
  end
  

(*val def_qt = ‘
(nth_fuel (n : num) (ls : 't list_t) (i : u32) : 't result =
  case n of
  | 0 => Loop
  | SUC n => 
    do 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_fuel n tl i0
        od
    | ListNil => 
      Fail Failure
    od)
’*)

val num_zero_tm = “0:num”
val num_suc_tm = “SUC: num -> num
val num_ty = “:num”

val fuel_def_suffix = "___fuel" (* TODO: name collisions *)
val fuel_var_name = "$n" (* TODO: name collisions *)
val fuel_var = mk_var (fuel_var_name, num_ty)
val fuel_var0 = fuel_var
val fuel_var1 = mk_var ("$m", “:num”) (* TODO: name collisions *)
val fuel_vars_le = “^fuel_var0 <= ^fuel_var1

val fuel_predicate_suffix = "___P" (* TODO: name collisions *)
val expand_suffix = "___E" (* TODO: name collisions *)

val bool_ty = “:bool”

val alpha_tyvar : hol_type = “:'a”
val beta_tyvar : hol_type = “:'b”

val is_diverge_tm = “is_diverge: 'a result -> bool
val diverge_tm = “Diverge : 'a result

val least_tm = “$LEAST”
val le_tm = (fst o strip_comb) “x:num <= y:num
val true_tm = “T”
val false_tm = “F”

val measure_tm = “measure: ('a -> num) -> 'a -> 'a -> bool

fun mk_diverge_tm (ty : hol_type) : term =
  let
    val diverge_ty = mk_thy_type {Thy="primitives", Tyop="result", Args = [ty] }
    val diverge_tm = mk_thy_const { Thy="primitives", Name="Diverge", Ty=diverge_ty }
  in
    diverge_tm
  end

(* Small utility: we sometimes need to generate a termination measure for
   the fuel definitions.

   We derive a measure for a type which is simply the sum of the tuples
   of the input types of the functions.

   For instance, for even and odd we have:
   {[
     even___fuel : num -> int -> bool result
     odd___fuel  : num -> int -> bool result
   ]}

   So the type would be:
   {[
     (num # int) + (num # int)
   ]}

   Note that generally speaking we expect a type of the shape (the “:num”
   on the left is for the fuel):
   {[
     (num # ...) + (num # ...) + ... + (num # ...)
   ]}

   The decreasing measure is simply given by a function which matches over
   its argument to return the fuel, whatever the case.
 *)
fun mk_termination_measure_from_ty (ty : hol_type) : term =
  let
    val dtys = map pairSyntax.strip_prod (sumSyntax.strip_sum ty)
    (* For every tuple, create a match to extract the num *)
    fun mk_case_of_tuple (tys : hol_type list) : (term * term) =
      case tys of
        [] => failwith "mk_termination_measure_from_ty: empty list of types"
      | [num_ty] =>
        (* No need for a case *)
        let val var = genvar num_ty in (var, var) end
      | num_ty :: rem_tys =>
        let
          val scrut_var = genvar (pairSyntax.list_mk_prod tys)
          val var = genvar num_ty
          val rem_var = genvar (pairSyntax.list_mk_prod rem_tys)
          val pats = [(pairSyntax.mk_pair (var, rem_var), var)]
          val case_tm = TypeBase.mk_case (scrut_var, pats)
        in
          (scrut_var, case_tm)
        end
     val tuple_cases = map mk_case_of_tuple dtys

    (* For every sum, create a match to extract one of the tuples *)
    fun mk_sum_case ((tuple_var, tuple_case), (nvar, case_end)) =
      let
        val left_pat = sumSyntax.mk_inl (tuple_var, type_of nvar)
        val right_pat = sumSyntax.mk_inr (nvar, type_of tuple_var)
        val scrut = genvar (sumSyntax.mk_sum (type_of tuple_var, type_of nvar))
        val pats = [(left_pat, tuple_case), (right_pat, case_end)]
        val case_tm = TypeBase.mk_case (scrut, pats)
      in
        (scrut, case_tm)
      end
    val tuple_cases = rev tuple_cases
    val (nvar, case_end) = hd tuple_cases
    val tuple_cases = tl tuple_cases
    val (scrut, case_tm) = foldl mk_sum_case (nvar, case_end) tuple_cases

    (* Create the function *)
    val abs_tm = mk_abs (scrut, case_tm)
    
    (* Add the “measure term” *)
    val tm = inst [alpha_tyvar |-> type_of scrut] measure_tm
    val tm = mk_comb (tm, abs_tm)
  in
    tm
  end

(*
val ty = “: (num # 'a) + (num # 'b) + (num # 'c)”

val tys = hd dtys
val num_ty::rem_tys = tys

val (tuple_var, tuple_case) = hd tuple_cases
*)

(* Get the smallest id which make the names unique (or to be more precise:
   such that the names don't correspond to already defined constants).

   We do this for {!mk_fuel_defs}: for some reason, the termination proof
   fails if we try to reuse the same names as before.
 *)
fun get_smallest_unique_id_for_names (names : string list) : string =
  let
    (* Not trying to be smart here *)
    val i : int option ref = ref NONE
    fun get_i () = case !i of NONE => "" | SOME i => int_to_string i
    fun incr_i () =
      i := (case !i of NONE => SOME 0 | SOME i => SOME (i+1))
    val continue = ref true
    fun name_is_ok (name : string) : bool =
      not (is_const (Parse.parse_in_context [] [QUOTE (name ^ get_i ())]))
      handle HOL_ERR _ => false
    val _ =
      while !continue do (
        let val _ = (continue := not (forall name_is_ok names)) in
        if !continue then incr_i () else () end
      )
  in
    get_i ()
  end

fun mk_fuel_defs (def_tms : term list) : thm list =
  let
    (* Retrieve the identifiers.

       Ex.: def_tm = “even (n : int) : bool result = if i = 0 then Return T else odd (i - 1))”
       We want to retrive: id = “even”
     *)
    val ids = map (fst o strip_comb o lhs) def_tms

    (* In the definitions, replace the identifiers by new identifiers which use
       fuel.

       Ex.:
       def_fuel_tm = “
         even___fuel (fuel : nat) (n : int) : result bool =
           case fuel of 0 => Diverge
           | SUC fuel' => 
             if i = 0 then Return T else odd_fuel fuel' (i - 1))”
     *)
     val names = map ((fn s => s ^ fuel_def_suffix) o fst o dest_var) ids
     val index = get_smallest_unique_id_for_names names
     fun mk_fuel_id (id : term) : term =
       let
         val (id_str, ty) = dest_var id
         (* Note: we use symbols forbidden in the generation of code to
            prevent name collisions *)
         val fuel_id_str = id_str ^ fuel_def_suffix ^ index
         val fuel_id = mk_var (fuel_id_str, num_ty --> ty)
       in fuel_id end
     val fuel_ids = map mk_fuel_id ids

     val fuel_ids_with_fuel0 = map (fn id => mk_comb (id, fuel_var0)) fuel_ids
     val fuel_ids_with_fuel1 = map (fn id => mk_comb (id, fuel_var1)) fuel_ids

     (* Recurse through the terms and replace the calls *)
     val rwr_thms0 = map (ASSUME o mk_eq) (zip ids fuel_ids_with_fuel0)
     val rwr_thms1 = map (ASSUME o mk_eq) (zip ids fuel_ids_with_fuel1)

     fun mk_fuel_tm (def_tm : term) : term =
       let
         val (tm0, tm1) = dest_eq def_tm
         val tm0 = (rhs o concl o (PURE_REWRITE_CONV rwr_thms0)) tm0
         val tm1 = (rhs o concl o (PURE_REWRITE_CONV rwr_thms1)) tm1
       in mk_eq (tm0, tm1) end
     val fuel_tms = map mk_fuel_tm def_tms

     (* Add the case over the fuel *)
     fun add_fuel_case (tm : term) : term =
       let
         val (f, body) = dest_eq tm
         (* Create the “Diverge” term with the proper type *)
         val body_ty = type_of body
         val return_ty =
           case (snd o dest_type) body_ty of [ty] => ty
           | _ => failwith "unexpected"
         val diverge_tm = mk_diverge_tm return_ty
         (* Create the “SUC fuel” term *)
         val suc_tm = mk_comb (num_suc_tm, fuel_var1)
         val fuel_tm =
           TypeBase.mk_case (fuel_var0, [(num_zero_tm, diverge_tm), (suc_tm, body)])
       in mk_eq (f, fuel_tm) end
     val fuel_tms = map add_fuel_case fuel_tms

     (* Define the auxiliary definitions which use fuel *)
     val fuel_defs_conj = list_mk_conj fuel_tms
     (* The definition name *)
     val def_name = (fst o dest_var o hd) fuel_ids
     (* The tactic to prove the termination *)
     val rty = ref “:bool” (* This is useful for debugging *)
     fun prove_termination_tac (asms, g) =
       let
         val r_tm = (fst o dest_exists) g
         val _ = rty := type_of r_tm
         val ty = (hd o snd o dest_type) (!rty)
         val m_tm = mk_termination_measure_from_ty ty
       in
         WF_REL_TAC ‘^m_tm’ (asms, g)
       end

     (* Define the fuel definitions *)
     (*
       val temp_def = Hol_defn def_name ‘^fuel_defs_conj’
       Defn.tgoal temp_def
     *)
     val fuel_defs = tDefine def_name ‘^fuel_defs_conj’ prove_termination_tac
   in
     CONJUNCTS fuel_defs
   end

(*
val (fuel_tms, fuel_defs) = mk_fuel_defs def_tms
val fuel_def_tms = map (snd o strip_forall) ((strip_conj o concl) fuel_defs)
val (def_tm, fuel_def_tm) = hd (zip def_tms fuel_def_tms)
*)

fun mk_is_diverge_tm (fuel_tm : term) : term =
  case snd (dest_type (type_of fuel_tm)) of
    [ret_ty] => mk_comb (inst [alpha_tyvar |-> ret_ty] is_diverge_tm, fuel_tm)
   | _ => failwith "mk_is_diverge_tm: unexpected"

fun mk_fuel_predicate_defs (def_tm, fuel_def_tm) : thm =
  let
    (* From [even i] create the term [even_P i n], where [n] is the fuel *)
    val (id, args) = (strip_comb o lhs) def_tm
    val (id_str, id_ty) = dest_var id
    val (tys, ret_ty) = strip_arrows id_ty
    val tys = append tys [num_ty]
    val pred_ty = list_mk_arrow tys bool_ty
    val pred_id = mk_var (id_str ^ fuel_predicate_suffix, pred_ty)
    val pred_tm = list_mk_comb (pred_id, append args [fuel_var])

    (* Create the term ~is_diverge (even_fuel n i) *)
    val fuel_tm = lhs fuel_def_tm
    val not_is_diverge_tm = mk_neg (mk_is_diverge_tm fuel_tm)

    (* Create the term: even_P i n = ~(is_diverge (even_fuel n i) *)
    val pred_def_tm = mk_eq (pred_tm, not_is_diverge_tm)
  in
    (* Create the definition *)
    Define ‘^pred_def_tm’
  end

(*
val (def_tm, fuel_def_tm) = hd (zip def_tms fuel_def_tms)

val pred_defs = map mk_fuel_predicate_defs (zip def_tms fuel_def_tms)
*)

(* Tactic which makes progress in a proof by making a case disjunction (we use
   this to explore all the paths in a function body). *)
fun case_progress (asms, g) =
  let
    val scrut = (strip_all_cases_get_scrutinee o lhs) g
  in Cases_on ‘^scrut’ (asms, g) end  

(* Prove the fuel monotonicity properties.

   We want to prove a theorem of the shape:
   {[
     !n m.
       (!i. n <= m ==> even___P i n ==> even___fuel n i = even___fuel m i) /\
       (!i. n <= m ==> odd___P i n ==> odd___fuel n i = odd___fuel m i)
   ]}
*)
fun prove_fuel_mono (pred_defs : thm list) (fuel_defs : thm list) : thm =
  let
    val pred_tms = map (lhs o snd o strip_forall o concl) pred_defs
    val fuel_tms = map (lhs o snd o strip_forall o concl) fuel_defs
    val pred_fuel_tms = zip pred_tms fuel_tms
    (* Create a set containing the names of all the functions in the recursive group *)
    val rec_fun_set =
      Redblackset.fromList const_name_compare (map get_fun_name_from_app fuel_tms)
    (* Small tactic which rewrites the occurrences of recursive calls *)
    fun rewrite_rec_call (asms, g) =
      let
        val scrut = (strip_all_cases_get_scrutinee o lhs) g
        val fun_id = get_fun_name_from_app scrut (* This can fail *)
      in
        (* Check if the function is part of the group we are considering *)
        if Redblackset.member (rec_fun_set, fun_id) then
          let
             (* Yes: use the induction hypothesis *)
             fun apply_ind_hyp (ind_th : thm) : tactic =
               let
                  val th = SPEC_ALL ind_th
                  val th_pat = (lhs o snd o strip_imp o concl) th
                  val (var_s, ty_s) = match_term th_pat scrut
                  (* Note that in practice the type instantiation should be empty *)
                  val th = INST var_s (INST_TYPE ty_s th)
               in
                 assume_tac th
               end
          in
            (last_assum apply_ind_hyp >> fs []) (asms, g)
          end
        else all_tac (asms, g)
      end
      handle HOL_ERR _ => all_tac (asms, g)
    (* Generate terms of the shape:
       !i. n <= m ==> even___P i n ==> even___fuel n i = even___fuel m i
     *)
    fun mk_fuel_eq_tm (pred_tm, fuel_tm) : term =
      let
        (* Retrieve the variables which are not the fuel - for the quantifiers *)
        val vars = (tl o snd o strip_comb) fuel_tm
        (* Introduce the fuel term which uses “m” *)
        val m_fuel_tm = subst [fuel_var0 |-> fuel_var1] fuel_tm
        (* Introduce the equality *)
        val fuel_eq_tm = mk_eq (fuel_tm, m_fuel_tm)
        (* Introduce the implication with the _P pred *)
        val fuel_eq_tm = mk_imp (pred_tm, fuel_eq_tm)
        (* Introduce the “n <= m ==> ...” implication *)
        val fuel_eq_tm = mk_imp (fuel_vars_le, fuel_eq_tm)
        (* Quantify *)
        val fuel_eq_tm = list_mk_forall (vars, fuel_eq_tm)
      in
        fuel_eq_tm
      end
     val fuel_eq_tms = map mk_fuel_eq_tm pred_fuel_tms
     (* Create the conjunction *)
     val fuel_eq_tms = list_mk_conj fuel_eq_tms
     (* Qantify over the fuels *)
     val fuel_eq_tms = list_mk_forall ([fuel_var0, fuel_var1], fuel_eq_tms)
     (* The tactics for the proof *)
     val prove_tac =
       Induct_on ‘^fuel_var0’ >-(
         (* The ___P predicates are false: n is 0 *)
         fs pred_defs >>
         fs [is_diverge_def] >>
         pure_once_rewrite_tac fuel_defs >> fs []) >>
       (* Introduce n *)
       gen_tac >>
       (* Introduce m *)
       Cases_on ‘^fuel_var1’ >-(
         (* Contradiction: SUC n < 0 *)
         rw [] >> exfalso >> int_tac) >>
       fs pred_defs >>
       fs [is_diverge_def] >>
       pure_once_rewrite_tac fuel_defs >> fs [bind_def] >>
       (* Introduce in the context *)
       rpt gen_tac >>
       (* Split the goals - note that we prove one big goal for all the functions at once *)
       rpt strip_tac >>
       (* Instantiate the assumption: !m. n <= m ==> ~(...)
          with the proper m.
        *)
       last_x_assum imp_res_tac >>
       (* Make sure the induction hypothesis is always the last assumption *)
       last_x_assum assume_tac >>
       (* Split the goals *)
       rpt strip_tac >> fs [case_result_same_eq] >>
       (* Explore all the paths *)
       rpt (rewrite_rec_call >> case_progress >> fs [case_result_same_eq])
   in
     (* Prove *)
     save_goal_and_prove (fuel_eq_tms, prove_tac)
   end

(*
val fuel_mono_thm = prove_fuel_mono pred_defs fuel_defs

set_goal ([], fuel_eq_tms)
*)

(* Prove the property about the least upper bound.

   We want to prove theorems of the shape:
   {[
     (!n i. $LEAST (even___P i) <= n ==> even___fuel n i = even___fuel ($LEAST (even___P i)) i)
   ]}
   {[
     (!n i. $LEAST (odd___P i) <= n ==> odd___fuel n i = odd___fuel ($LEAST (odd___P i)) i)
   ]}

   TODO: merge with other functions? (prove_pred_imp_fuel_eq_raw_thms)
*)
fun prove_least_fuel_mono (pred_defs : thm list) (fuel_mono_thm : thm) : thm list =
  let
    val thl = (CONJUNCTS o SPECL [fuel_var0, fuel_var1]) fuel_mono_thm
    fun mk_least_fuel_thm (pred_def, mono_thm) : thm =
      let
        (* Retrieve the predicate, without the fuel *)
        val pred_tm = (lhs o snd o strip_forall o concl) pred_def
        val (pred_tm, args) = strip_comb pred_tm
        val args = rev (tl (rev args))
        val pred_tm = list_mk_comb (pred_tm, args)
        (* Add $LEAST *)
        val least_pred_tm = mk_comb (least_tm, pred_tm)
        (* Specialize all *)
        val vars = (fst o strip_forall o concl) mono_thm
        val th = SPECL vars mono_thm
        (* Substitute in the mono theorem *)
        val th = INST [fuel_var0 |-> least_pred_tm] th
        (* Symmetrize the equality *)
        val th = PURE_ONCE_REWRITE_RULE [EQ_SYM_EQ] th
        (* Quantify *)
        val th = GENL (fuel_var1 :: vars) th
      in
        th
      end
  in
    map mk_least_fuel_thm (zip pred_defs thl)
  end

(*
val (pred_def, mono_thm) = hd (zip pred_defs thl)
*)

(* Prove theorems of the shape:

   {[
     !n i. even___P i n ==> $LEAST (even___P i) <= n
   ]}

   TODO: merge with other functions? (prove_pred_imp_fuel_eq_raw_thms)
 *)
fun prove_least_pred_thms (pred_defs : thm list) : thm list =
  let
    fun prove_least_pred_thm (pred_def : thm) : thm =
      let
        val pred_tm = (lhs o snd o strip_forall o concl) pred_def
        val (pred_no_fuel_tm, args) = strip_comb pred_tm
        val args = rev (tl (rev args))
        val pred_no_fuel_tm = list_mk_comb (pred_no_fuel_tm, args)
        (* Make the “$LEAST (even___P i)” term *)
        val least_pred_tm = mk_comb (least_tm, pred_no_fuel_tm)
        (* Make the inequality *)
        val tm = list_mk_comb (le_tm, [least_pred_tm, fuel_var0])
        (* Add the implication *)
        val tm = mk_imp (pred_tm, tm)
        (* Quantify *)
        val tm = list_mk_forall (args, tm)
        val tm = mk_forall (fuel_var0, tm)
        (* Prove *)
        val prove_tac =
          rpt gen_tac >>
          disch_tac >>
          (* Use the "fundamental" property about $LEAST *)
          qspec_assume ‘^pred_no_fuel_tm’ whileTheory.LEAST_EXISTS_IMP >>
          (* Prove the premise *)
          pop_assum sg_premise_tac >- (exists_tac fuel_var0 >> fs []) >>
          rw [] >>
          (* Finish the proof by contraposition *)
          spose_not_then assume_tac >>
          fs [not_le_eq_gt]
      in
        save_goal_and_prove (tm, prove_tac)
      end
  in
    map prove_least_pred_thm pred_defs
  end


(*
val least_pred_thms = prove_least_pred_thms pred_defs

val least_pred_thm = hd least_pred_thms
*)

(* Prove theorems of the shape:

   {[
     !n i. even___P i n ==> even___P i ($LEAST (even___P i))
   ]}
*)
fun prove_pred_n_imp_pred_least_thms (pred_defs : thm list) : thm list =
  let
    fun prove_pred_n_imp_pred_least (pred_def : thm) : thm =
      let
        val pred_tm = (lhs o snd o strip_forall o concl) pred_def
        val (pred_no_fuel_tm, args) = strip_comb pred_tm
        val args = rev (tl (rev args))
        val pred_no_fuel_tm = list_mk_comb (pred_no_fuel_tm, args)
        (* Make the “$LEAST (even___P i)” term *)
        val least_pred_tm = mk_comb (least_tm, pred_no_fuel_tm)
        (* Make the “even___P i ($LEAST (even___P i))” *)
        val tm = subst [fuel_var0 |-> least_pred_tm] pred_tm
        (* Add the implication *)
        val tm = mk_imp (pred_tm, tm)
        (* Quantify *)
        val tm = list_mk_forall (args, tm)
        val tm = mk_forall (fuel_var0, tm)
        (* The proof tactic *)
        val prove_tac =
          rpt gen_tac >>
          disch_tac >>
          (* Use the "fundamental" property about $LEAST *)
          qspec_assume ‘^pred_no_fuel_tm’ whileTheory.LEAST_EXISTS_IMP >>
          (* Prove the premise *)
          pop_assum sg_premise_tac >- (exists_tac fuel_var0 >> fs []) >>
          rw []
      in
        save_goal_and_prove (tm, prove_tac)
      end
  in
    map prove_pred_n_imp_pred_least pred_defs
  end

(*
val (pred_def, mono_thm) = hd (zip pred_defs thl)
val least_fuel_mono_thms = prove_least_fuel_mono pred_defs fuel_defs fuel_mono_thm

val least_fuel_mono_thm = hd least_fuel_mono_thms
*)

(* Define the "raw" definitions:

   {[
     even i = if (?n. even___P i n) then even___P ($LEAST (even___P i)) i else Diverge
   ]}
 *)
fun define_raw_defs (def_tms : term list) (pred_defs : thm list) (fuel_defs : thm list) : thm list =
  let
    fun define_raw_def (def_tm, (pred_def, fuel_def)) : thm =
      let
        val app = lhs def_tm
        val pred_tm = (lhs o snd o strip_forall o concl) pred_def
        (* Make the “?n. even___P i n” term *)
        val exists_fuel_tm = mk_exists (fuel_var0, pred_tm)
        (* Make the “even___fuel ($LEAST (even___P i)) i” term *)
        val fuel_tm = (lhs o snd o strip_forall o concl) fuel_def
        val (pred_tm, args) = strip_comb pred_tm
        val args = rev (tl (rev args))
        val pred_tm = list_mk_comb (pred_tm, args)
        val least_pred_tm = mk_comb (least_tm, pred_tm)
        val fuel_tm = subst [fuel_var0 |-> least_pred_tm] fuel_tm
        (* Create the Diverge term *)
        val ret_ty = (hd o snd o dest_type) (type_of app)
        (* Create the “if then else” *)
        val body = TypeBase.mk_case (exists_fuel_tm, [(true_tm, fuel_tm), (false_tm, mk_diverge_tm ret_ty)])
        (* *)
        val raw_def_tm = mk_eq (app, body)
      in
        Define ‘^raw_def_tm’
      end
  in
    map define_raw_def (zip def_tms (zip pred_defs fuel_defs))
  end

(*
val raw_defs = define_raw_defs def_tms pred_defs fuel_defs
 *)

(* Prove theorems of the shape:

   !n i. even___P i n ==> even___fuel n i = even i
 *)
fun prove_pred_imp_fuel_eq_raw_defs
  (pred_defs : thm list)
  (fuel_def_tms : term list)
  (least_fuel_mono_thms : thm list)
  (least_pred_thms : thm list)
  (pred_n_imp_pred_least_thms : thm list)
  (raw_defs : thm list) :
  thm list =
  let
    fun prove_thm (pred_def,
                   (fuel_def_tm,
                    (least_fuel_mono_thm,
                     (least_pred_thm,
                      (pred_n_imp_pred_least_thm, raw_def))))) : thm =
      let
        (* Generate: “even___P i n” *)
        val pred_tm = (lhs o snd o strip_forall o concl) pred_def
        val (pred_no_fuel_tm, args) = strip_comb pred_tm
        val args = rev (tl (rev args))
        (* Generate: “even___fuel n i” *)
        val fuel_tm = lhs fuel_def_tm
        (* Generate: “even i” *)
        val raw_def_tm = (lhs o snd o strip_forall o concl) raw_def
        (* Generate: “even___fuel n i = even i” *)
        val tm = mk_eq (fuel_tm, raw_def_tm)
        (* Add the implication *)
        val tm = mk_imp (pred_tm, tm)
        (* Quantify *)
        val tm = list_mk_forall (args, tm)
        val tm = mk_forall (fuel_var0, tm)
        (* Prove *)
        val prove_tac =
          rpt gen_tac >>
          strip_tac >>
          fs raw_defs >>
          (* Case on ‘?n. even___P i n’ *)
          CASE_TAC >> fs [] >>
          (* Use the monotonicity property *)
          irule least_fuel_mono_thm >>
          imp_res_tac pred_n_imp_pred_least_thm >> fs [] >>
          irule least_pred_thm >> fs []
      in
        save_goal_and_prove (tm, prove_tac)
      end
  in
    map prove_thm (zip pred_defs (zip fuel_def_tms (zip least_fuel_mono_thms
                   (zip least_pred_thms (zip pred_n_imp_pred_least_thms raw_defs)))))
  end

(*
val pred_imp_fuel_eq_raw_defs =
  prove_pred_imp_fuel_eq_raw_defs
    pred_defs fuel_def_tms least_fuel_mono_thms least_pred_thms
    pred_n_imp_pred_least_thms raw_defs
 *)


(* Generate "expand" definitions of the following shape (we use them to
   hide the raw function bodies, to control the rewritings):

   {[
     even___expand even odd i : bool result =
       if i = 0 then Return T else odd (i - 1)
   ]}

   {[
     odd___expand even odd i : bool result =
       if i = 0 then Return F else even (i - 1)
   ]}

 *)
fun gen_expand_defs (def_tms : term list) =
  let
    (* Generate the variables for “even”, “odd”, etc. *)
    val fun_vars = map (fst o strip_comb o lhs) def_tms
    val fun_tys = map type_of fun_vars
    (* Generate the expansion *)
    fun mk_def (def_tm : term) : thm =
      let
        val (exp_fun, args) = (strip_comb o lhs) def_tm
        val (exp_fun_str, exp_fun_ty) = dest_var exp_fun
        val exp_fun_str = exp_fun_str ^ expand_suffix
        val exp_fun_ty = list_mk_arrow fun_tys exp_fun_ty
        val exp_fun = mk_var (exp_fun_str, exp_fun_ty)
        val exp_fun = list_mk_comb (exp_fun, fun_vars)
        val exp_fun = list_mk_comb (exp_fun, args)
        val tm = mk_eq (exp_fun, rhs def_tm)
      in
        Define ‘^tm’
      end
  in
    map mk_def def_tms
  end

(*
val def_tm = hd def_tms

val expand_defs = gen_expand_defs def_tms
*)

(* Small utility:

   Return the list:
   {[
     (“even___P i n”, “even i = even___expand even odd i”),
     ...
   ]}
   
 *)
fun mk_termination_diverge_tms
  (def_tms : term list)
  (pred_defs : thm list)
  (raw_defs : thm list)
  (expand_defs : thm list) :
  (term * term) list =
  let
    (* Create the substitution for the "expand" functions:
       {[
         even -> even
         odd -> odd
         ...
       ]}

       where on the left we have *variables* and on the right we have
       the "raw" definitions.
     *)
    fun mk_fun_subst (def_tm, raw_def) =
      let
        val var = (fst o strip_comb o lhs) def_tm
        val f = (fst o strip_comb o lhs o snd o strip_forall o concl) raw_def
      in
        (var |-> f)
      end
    val fun_subst = map mk_fun_subst (zip def_tms raw_defs)
  
    fun mk_tm (pred_def, (raw_def, expand_def)) :
      term * term =
      let
        (* “even___P i n” *)
        val pred_tm = (lhs o snd o strip_forall o concl) pred_def
        (* “even i = even___expand even odd i” *)
        val expand_tm = (lhs o snd o strip_forall o concl) expand_def
        val expand_tm = subst fun_subst expand_tm
        val fun_tm = (lhs o snd o strip_forall o concl) raw_def
        val fun_eq_tm = mk_eq (fun_tm, expand_tm)
      in (pred_tm, fun_eq_tm) end
  in
    map mk_tm (zip pred_defs (zip raw_defs expand_defs))
  end

(*
val term_div_tms =
  mk_termination_diverge_tms pred_defs raw_defs expand_defs
*)

(* Prove the termination lemmas:
   
   {[
     !i.
       (?n. even___P i n) ==>
         even i = even___expand even odd i
   ]}
 *)
fun prove_termination_thms
  (term_div_tms : (term * term) list)
  (fuel_defs : thm list)
  (pred_defs : thm list)
  (raw_defs : thm list)
  (expand_defs : thm list)
  (pred_n_imp_pred_least_thms : thm list)
  (pred_imp_fuel_eq_raw_defs : thm list)
  : thm list =
  let
    (* Create a map from functions in the recursive group to lemmas
       to apply *)
    fun mk_rec_fun_eq_pair (fuel_def, eq_th) =
      let
        val rfun = (get_fun_name_from_app o lhs o snd o strip_forall o concl) fuel_def
      in
        (rfun, eq_th)
      end
    val rec_fun_eq_map =
      Redblackmap.fromList const_name_compare (
        map mk_rec_fun_eq_pair
          (zip fuel_defs pred_imp_fuel_eq_raw_defs))

    (* Small tactic which rewrites the recursive calls *)
    fun rewrite_rec_call (asms, g) =
      let
        val scrut = (strip_all_cases_get_scrutinee o lhs) g
        val fun_id = get_fun_name_from_app scrut (* This can fail *)
        (* This can raise an exception - hence the handle at the end
           of the function *)
        val eq_th = Redblackmap.find (rec_fun_eq_map, fun_id)
        val eq_th = (UNDISCH_ALL o SPEC_ALL) eq_th
        (* Match the theorem *)
        val eq_th_tm = (lhs o concl) eq_th
        val (var_s, ty_s) = match_term eq_th_tm scrut
        val eq_th = INST var_s (INST_TYPE ty_s eq_th)
        val eq_th = thm_to_conj_implies eq_th
        (* Some tactics *)
        val premise_tac = fs pred_defs >> fs [is_diverge_def]
      in
        (* Apply the theorem, prove the premise, and rewrite *)
        (prove_premise_then premise_tac assume_tac eq_th >> fs []) (asms, g)
      end handle NotFound => all_tac (asms, g)
          | HOL_ERR _ => all_tac (asms, g) (* Getting the function name can also fail *)
  
    fun prove_one ((pred_tm, fun_eq_tm), pred_n_imp_pred_least_thm) :
      thm =
      let
        (* “?n. even___P i n” *)
        val pred_tm = mk_exists (fuel_var0, pred_tm)
        (* “even i = even___expand even odd i” *)
        val tm = fun_eq_tm
        (* Add the implication *)
        val tm = mk_imp (pred_tm, tm)
        (* Quantify *)
        val (_, args) = strip_comb (lhs fun_eq_tm)
        val tm = list_mk_forall (args, tm)

        (* Prove *)
        val prove_tac =
          rpt gen_tac >>
          disch_tac >>

          (* Expand the raw definition and get rid of the ‘?n ...’ *)
          pure_once_rewrite_tac raw_defs >>
          pure_asm_rewrite_tac [] >>

          (* Simplify *)
          fs [] >>

          (* Prove that: “even___P i $(LEAST ...)” *)
          imp_res_tac pred_n_imp_pred_least_thm >>

          (* We don't need the ‘even___P i n’ assumption anymore: we have a more
             precise one with the least upper bound *)
          last_x_assum ignore_tac >>

          (* Expand *)
          fs pred_defs >>
          fs [is_diverge_def] >>
          fs expand_defs >>

          (* We need to be a bit careful when expanding the definitions which use fuel:
             it can make the simplifier loop. *)
          rpt (pop_assum mp_tac) >>
          pure_once_rewrite_tac fuel_defs >>
          rpt disch_tac >>

          (* Expand the binds *)
          fs [bind_def, case_result_same_eq] >>

          (* Explore all the paths by doing case disjunctions *)
          rpt (rewrite_rec_call >> case_progress >> fs [case_result_same_eq])
      in
        save_goal_and_prove (tm, prove_tac)
      end
  in
    map prove_one
      (zip term_div_tms pred_n_imp_pred_least_thms)
  end

(*
val termination_thms =
  prove_termination_thms term_div_tms fuel_defs pred_defs
    raw_defs expand_defs pred_n_imp_pred_least_thms
    pred_imp_fuel_eq_raw_defs

val ((pred_tm, fun_eq_tm), pred_n_imp_pred_least_thm) = hd (zip term_div_tms pred_n_imp_pred_least_thms)
set_goal ([], tm)
*)

(* Prove the divergence lemmas:

   {[
     !i.
       (!n. ~even___P i n) ==>
        (!n. ~even___P i (SUC n)) ==>
         even i = even___expand even odd i
   ]}

   Note that the shape of the theorem is very precise: this helps for the proof.
   Also, by correctly ordering the assumptions, we make sure that by rewriting
   we don't convert one of the two to “T”.
 *)
fun prove_divergence_thms
  (term_div_tms : (term * term) list)
  (fuel_defs : thm list)
  (pred_defs : thm list)
  (raw_defs : thm list)
  (expand_defs : thm list)
  : thm list =
  let
    (* Create a set containing the names of all the functions in the recursive group *)
    fun get_rec_fun_id (fuel_def : thm) =
     (get_fun_name_from_app o lhs o snd o strip_forall o concl) fuel_def
    val rec_fun_set =
      Redblackset.fromList const_name_compare (
        map get_rec_fun_id raw_defs)

    (* Small tactic which rewrites the recursive calls *)
    fun rewrite_rec_call (asms, g) =
      let
        val scrut = (strip_all_cases_get_scrutinee o lhs) g
        val fun_id = get_fun_name_from_app scrut (* This can fail *)
      in
        (* Check if the function is part of the group we are considering *)
        if Redblackset.member (rec_fun_set, fun_id) then
          let
            (* Create a subgoal “odd i = Diverge” *)
            val ret_ty = (hd o snd o dest_type o type_of) scrut
            val g = mk_eq (scrut, mk_diverge_tm ret_ty)

            (* Create a subgoal: “?n. odd___P i n”.

               It is a bit cumbersome because we have to lookup the proper
               predicate (from “odd” we need to lookup “odd___P”) and we
               may have to perform substitutions... We hack a bit by using
               a conversion to rewrite “odd i” to a term which contains
               the “?n. odd___P i n” we are looking for.
             *)
            val exists_g = (rhs o concl) (PURE_REWRITE_CONV raw_defs scrut)
            val (_, exists_g, _) = TypeBase.dest_case exists_g
            (* The tactic to prove the subgoal *)
            val prove_sg_tac =
              pure_rewrite_tac raw_defs >>
              Cases_on ‘^exists_g’ >> pure_asm_rewrite_tac [] >> fs [] >>
              (* There must only remain the positive case (i.e., “?n. ...”):
                 we have a contradiction *)
              exfalso >>
              (* The end of the proof is done by opening the definitions *)
              pop_assum mp_tac >>
              fs pred_defs >> fs [is_diverge_def]
          in
            (SUBGOAL_THEN g assume_tac >- prove_sg_tac >> fs []) (asms, g)
          end
        else all_tac (asms, g) (* Nothing to do *)
      end handle HOL_ERR _ => all_tac (asms, g)
  
    fun prove_one (pred_tm, fun_eq_tm) :
      thm =
      let
        (* “!n. ~even___P i n” *)
        val neg_pred_tm = mk_neg pred_tm
        val pred_tm = mk_forall (fuel_var0, neg_pred_tm)
        val pred_suc_tm = subst [fuel_var0 |-> numSyntax.mk_suc fuel_var0] neg_pred_tm
        val pred_suc_tm = mk_forall (fuel_var0, pred_suc_tm)

        (* “even i = even___expand even odd i” *)
        val tm = fun_eq_tm

        (* Add the implications *)
        val tm = list_mk_imp ([pred_tm, pred_suc_tm], tm)

        (* Quantify *)
        val (_, args) = strip_comb (lhs fun_eq_tm)
        val tm = list_mk_forall (args, tm)

        (* Prove *)
        val prove_tac =
          rpt gen_tac >>

          pure_rewrite_tac raw_defs >>
          rpt disch_tac >>

          (* This allows to simplify the “?n. even___P i n” *)
          fs [] >>
          (* We don't need the last assumption anymore *)
          last_x_assum ignore_tac >>

          (* Expand *)
          fs pred_defs >> fs [is_diverge_def] >>
          fs expand_defs >>

          (* We need to be a bit careful when expanding the definitions which use fuel:
             it can make the simplifier loop.
           *)
          pop_assum mp_tac >>
          pure_once_rewrite_tac fuel_defs  >>
          rpt disch_tac >> fs [bind_def, case_result_same_eq] >>

          (* Evaluate all the paths *)
          rpt (rewrite_rec_call >> case_progress >> fs [case_result_same_eq])
      in
        save_goal_and_prove (tm, prove_tac)
      end
  in
    map prove_one term_div_tms
  end

(*
val (pred_tm, fun_eq_tm) = hd term_div_tms
set_goal ([], tm)

val divergence_thms =
  prove_divergence_thms
    term_div_tms
    fuel_defs
    pred_defs
    raw_defs
    expand_defs
*)

(* Prove the final lemmas:

   {[
     !i. even i = even___expand even odd i
   ]}

   Note that the shape of the theorem is very precise: this helps for the proof.
   Also, by correctly ordering the assumptions, we make sure that by rewriting
   we don't convert one of the two to “T”.
 *)
fun prove_final_eqs
  (term_div_tms : (term * term) list)
  (termination_thms : thm list)
  (divergence_thms : thm list)
  (raw_defs : thm list)
  : thm list =
  let
    fun prove_one ((pred_tm, fun_eq_tm), (termination_thm, divergence_thm)) : thm =
      let
        val (_, args) = strip_comb (lhs fun_eq_tm)
        val g = list_mk_forall (args, fun_eq_tm)
        (* We make a case disjunction of the subgoal: “exists n. even___P i n” *)
        val exists_g = (rhs o concl) (PURE_REWRITE_CONV raw_defs (lhs fun_eq_tm))
        val (_, exists_g, _) = TypeBase.dest_case exists_g
        val prove_tac =
          rpt gen_tac >>
          Cases_on ‘^exists_g’
          >-( (* Termination *)
             irule termination_thm >> pure_asm_rewrite_tac [])
          (* Divergence *)
          >> irule divergence_thm >> fs []
          
      in
        save_goal_and_prove (g, prove_tac)
      end    
  in
    map prove_one (zip term_div_tms (zip termination_thms divergence_thms))
  end

(*
val termination_thm = hd termination_thms
val divergence_thm = hd divergence_thms
set_goal ([], g)
*)

(* The final function: define potentially diverging functions in an error monad *)
fun DefineDiv (def_qt : term quotation) =
  let
    (* Parse the definitions.
    
       Example:
       {[
         (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))
       ]}
     *)
    val def_tms = (strip_conj o list_mk_conj o rev) (Defn.parse_quote def_qt)

    (* Generate definitions which use some fuel
    
       Example:
       {[
         even___fuel n i =
           case fuel of
             0 => Diverge
           | SUC fuel => 
             if i = 0 then Return T else odd_fuel (i - 1))
       ]}
     *)
     val fuel_defs = mk_fuel_defs def_tms

     (* Generate the predicate definitions.
     
        {[ even___P n i = = ~is_diverge (even___fuel n i) ]}
      *)
     val fuel_def_tms = map (snd o strip_forall o concl) fuel_defs
     val pred_defs = map mk_fuel_predicate_defs (zip def_tms fuel_def_tms)
     
     (* Prove the monotonicity property for the fuel, all at once

      *)
     val fuel_mono_thm = prove_fuel_mono pred_defs fuel_defs
     
     (* Prove the individual fuel functions - TODO: update

        {[
          !n i. $LEAST (even___P i) <= n ==> even___fuel n i = even___fuel ($LEAST (even___P i)) i
        ]}
      *)
     val least_fuel_mono_thms = prove_least_fuel_mono pred_defs fuel_mono_thm

     (*
       {[
         !n i. even___P i n ==> $LEAST (even___P i) <= n
       ]}
      *)
     val least_pred_thms = prove_least_pred_thms pred_defs

     (*
       {[
         !n i. even___P i n ==> even___P i ($LEAST (even___P i))
       ]}
      *)
     val pred_n_imp_pred_least_thms = prove_pred_n_imp_pred_least_thms pred_defs

     (*
       "Raw" definitions:

       {[
         even i = if (?n. even___P i n) then even___P ($LEAST (even___P i)) i else Diverge
       ]}
      *)
     val raw_defs = define_raw_defs def_tms pred_defs fuel_defs

     (*
       !n i. even___P i n ==> even___fuel n i = even i
      *)
     val pred_imp_fuel_eq_raw_defs =
       prove_pred_imp_fuel_eq_raw_defs
         pred_defs fuel_def_tms least_fuel_mono_thms
         least_pred_thms pred_n_imp_pred_least_thms raw_defs

     (* "Expand" definitions *)
     val expand_defs = gen_expand_defs def_tms

     (* Small utility *)
     val term_div_tms = mk_termination_diverge_tms def_tms pred_defs raw_defs expand_defs

     (* Termination theorems *)
     val termination_thms =
       prove_termination_thms term_div_tms fuel_defs pred_defs
         raw_defs expand_defs pred_n_imp_pred_least_thms pred_imp_fuel_eq_raw_defs

     (* Divergence theorems *)
     val divergence_thms =
       prove_divergence_thms term_div_tms fuel_defs pred_defs raw_defs expand_defs

     (* Final theorems:

        {[
          ∀i. even i = even___E even odd i,
          ⊢ ∀i. odd i = odd___E even odd i
        ]}
      *)
     val final_eqs = prove_final_eqs term_div_tms termination_thms divergence_thms raw_defs
     val final_eqs = map (PURE_REWRITE_RULE expand_defs) final_eqs
  in
    (* We return the final equations, which act as rewriting theorems *)
    final_eqs
  end

end