open HolKernel boolLib bossLib Parse

val primitives_theory_name = "Primitives"
val _ = new_theory primitives_theory_name

(* SML declarations  *)
(* for example: *)
(*val th = save_thm("SKOLEM_AGAIN",SKOLEM_THM) *)

local open boolTheory integerTheory wordsTheory stringTheory in end

Datatype:
  error = Failure
End

Datatype:
  result = Return 'a | Fail error | Loop
End

Type M = ``: 'a result``

(* TODO: rename *)
val st_ex_bind_def = Define `
  (st_ex_bind : 'a M -> ('a -> 'b M) -> 'b M) x f =
    case x of
      Return y => f y
    | Fail e => Fail e
    | Loop => Loop`;

val st_ex_return_def = Define `
  (st_ex_return : 'a -> 'a M) x =
    Return x`;

Overload monad_bind[local] = ``st_ex_bind``
Overload monad_unitbind[local] = ``\x y. st_ex_bind x (\z. y)``
Overload monad_ignore_bind[local] = ``\x y. st_ex_bind x (\z. y)``
(*Overload ex_bind[local] = ``st_ex_bind`` *)
(* Overload ex_return[local] = ``st_ex_return`` *)
(*Overload failwith = ``raise_Fail``*)

(* Temporarily allow the monadic syntax *)
val _ = monadsyntax.temp_add_monadsyntax ();

val test1_def = Define `
  test1 (x : bool) = Return x`

val is_true_def = Define ‘
  is_true (x : bool) = if x then Return () else Fail Failure’

val test1_def = Define ‘
  test1 (x : bool) = Return x’

val test_monad_def = Define `
  test_monad v =
    do
      x <- Return v;
      Return x
    od`;


val test_monad2_def = Define `
  test_monad2 =
    do
      x <- Return T;
      Return x
    od`;

val test_monad3_def = Define `
  test_monad3 x =
    do
      is_true x;
      Return x
    od`;

(**
 *  Arithmetic
 *)

open intLib

val test_int1 = Define ‘int1 = 32’
val test_int2 = Define ‘int2 = -32’

Theorem INT_THM1:
  !(x y : int). x > 0 ==> y > 0 ==> x + y > 0
Proof
  ARITH_TAC
QED

Theorem INT_THM2:
  !(x : int). T
Proof
  rw[]
QED

val _ = prefer_int ()

val x = “-36217863217862718”

(* Deactivate notations for int *)
val _ = deprecate_int ()
open arithmeticTheory


val m = Hol_pp.print_apropos
val f = Hol_pp.print_find

(* Display types on/off: M-h C-t *)
(* Move back: M-h b *)

val _ = numLib.deprecate_num ()
val _ = numLib.prefer_num ()

Theorem NAT_THM1:
  !(n : num). n < n + 1
Proof
  Induct_on ‘n’ >> DECIDE_TAC
QED

Theorem NAT_THM2:
  !(n : num). n < n + (1 : num)
Proof
  gen_tac >>
  Induct_on ‘n’ >- (
    PURE_REWRITE_TAC [ADD, NUMERAL_DEF, BIT1, ALT_ZERO] >>
    PURE_REWRITE_TAC [prim_recTheory.LESS_0_0]) >>
  PURE_REWRITE_TAC [ADD] >>
  irule prim_recTheory.LESS_MONO >>
  asm_rewrite_tac []
QED


val x = “1278361286371286:num”


(********************** PRIMITIVES *)
val _ = prefer_int ()

val _ = new_type ("u32", 0)
val _ = new_type ("i32", 0)

(*val u32_min_def = Define ‘u32_min = (0:int)’*)
val u32_max_def = Define ‘u32_max = (4294967295:int)’

(* TODO: change that *)
val usize_max_def = Define ‘usize_max = (4294967295:int)’

val i32_min_def = Define ‘i32_min = (-2147483648:int)’
val i32_max_def = Define ‘i32_max = (2147483647:int)’

val _ = new_constant ("u32_to_int", “:u32 -> int”)
val _ = new_constant ("i32_to_int", “:i32 -> int”)

val _ = new_constant ("int_to_u32", “:int -> u32”)
val _ = new_constant ("int_to_i32", “:int -> i32”)


(* TODO: change to "...of..." *)
val u32_to_int_bounds =
  new_axiom (
    "u32_to_int_bounds",
    “!n. 0 <= u32_to_int n /\ u32_to_int n <= u32_max”)

val i32_to_int_bounds =
  new_axiom (
    "i32_to_int_bounds",
    “!n. i32_min <= i32_to_int n /\ i32_to_int n <= i32_max”)

val int_to_u32_id =
  new_axiom (
    "int_to_u32_id",
    “!n. 0 <= n /\ n <= u32_max ==>
     u32_to_int (int_to_u32 n) = n”)

val int_to_i32_id =
  new_axiom (
    "int_to_i32_id",
    “!n. i32_min <= n /\ n <= i32_max ==>
     i32_to_int (int_to_i32 n) = n”)

val mk_u32_def = Define
  ‘mk_u32 n =
    if 0 <= n /\ n <= u32_max then Return (int_to_u32 n)
    else Fail Failure’

val u32_add_def = Define ‘u32_add x y = mk_u32 ((u32_to_int x) + (u32_to_int y))’

Theorem MK_U32_SUCCESS:
  !n. 0 <= n /\ n <= u32_max ==>
  mk_u32 n = Return (int_to_u32 n)
Proof
  rw[mk_u32_def]
QED

Theorem U32_ADD_EQ:
  !x y.
    u32_to_int x + u32_to_int y <= u32_max ==>
    ?z. u32_add x y = Return z /\ u32_to_int z = u32_to_int x + u32_to_int y
Proof
  rpt gen_tac >>
  rpt DISCH_TAC >>
  exists_tac “int_to_u32 (u32_to_int x + u32_to_int y)” >>
  imp_res_tac MK_U32_SUCCESS >>
  (* There is probably a better way of doing this *)
  sg ‘0 <= u32_to_int x’ >- (rw[u32_to_int_bounds]) >>
  sg ‘0 <= u32_to_int y’ >- (rw[u32_to_int_bounds]) >>
  fs [u32_add_def] >>
  irule int_to_u32_id >>
  fs[]
QED

val u32_sub_def = Define ‘u32_sub x y = mk_u32 ((u32_to_int x) - (u32_to_int y))’

Theorem U32_SUB_EQ:
  !x y.
    0 <= u32_to_int x - u32_to_int y ==>
    ?z. u32_sub x y = Return z /\ u32_to_int z = u32_to_int x - u32_to_int y
Proof
  rpt gen_tac >>
  rpt DISCH_TAC >>
  exists_tac “int_to_u32 (u32_to_int x - u32_to_int y)” >>
  imp_res_tac MK_U32_SUCCESS >>
  (* There is probably a better way of doing this *)
  sg ‘u32_to_int x − u32_to_int y ≤ u32_max’ >-(
    sg ‘u32_to_int x <= u32_max’ >- (rw[u32_to_int_bounds]) >>
    sg ‘0 <= u32_to_int y’ >- (rw[u32_to_int_bounds]) >>
    COOPER_TAC
  ) >>
  fs [u32_sub_def] >>
  irule int_to_u32_id >>
  fs[]
QED

val mk_i32_def = Define
  ‘mk_i32 n =
    if i32_min <= n /\ n <= i32_max then Return (int_to_i32 n)
    else Fail Failure’

val i32_add_def = Define ‘i32_add x y = mk_i32 ((i32_to_int x) + (i32_to_int y))’

Theorem MK_I32_SUCCESS:
  !n. i32_min <= n /\ n <= i32_max ==>
  mk_i32 n = Return (int_to_i32 n)
Proof
  rw[mk_i32_def]
QED

Theorem I32_ADD_EQ:
  !x y.
    i32_min <= i32_to_int x + i32_to_int y ==>
    i32_to_int x + i32_to_int y <= i32_max ==>
    ?z. i32_add x y = Return z /\ i32_to_int z = i32_to_int x + i32_to_int y
Proof
  rpt gen_tac >>
  rpt DISCH_TAC >>
  exists_tac “int_to_i32 (i32_to_int x + i32_to_int y)” >>
  imp_res_tac MK_I32_SUCCESS >>
  fs [i32_min_def, i32_add_def] >>
  irule int_to_i32_id >>
  fs[i32_min_def]
QED

open listTheory

val _ = new_type ("vec", 1)
val _ = new_constant ("vec_to_list", “:'a vec -> 'a list”)

val VEC_TO_LIST_NUM_BOUNDS =
  new_axiom (
    "VEC_TO_LIST_BOUNDS",
    “!v. let l = LENGTH (vec_to_list v) in
     (0:num) <= l /\ l <= (4294967295:num)”)

Theorem VEC_TO_LIST_INT_BOUNDS:
  !v. let l = int_of_num (LENGTH (vec_to_list v)) in
     0 <= l /\ l <= u32_max
Proof
  gen_tac >>
  rw [u32_max_def] >>
  assume_tac VEC_TO_LIST_NUM_BOUNDS >>
  fs[]
QED

val VEC_LEN_DEF = Define ‘vec_len v = int_to_u32 (int_of_num (LENGTH (vec_to_list v)))’

(*
(* Useless *)
Theorem VEC_LEN_BOUNDS:
  !v. u32_min <= u32_to_int (vec_len v) /\ u32_to_int (vec_len v) <= u32_max
Proof
  gen_tac >>
  qspec_then ‘v’ assume_tac VEC_TO_LIST_INT_BOUNDS >>
  fs[VEC_LEN_DEF] >>
  IMP_RES_TAC int_to_u32_id >>
  fs[]
QED
*)

(* The type parameters are ordered in alphabetical order *)
Datatype:
  test = Variant1 'b | Variant2 'a
End

Datatype:
  test2 = Variant1_1 'T2 | Variant2_1 'T1
End

Datatype:
  test2 = Variant1_2 'T1 | Variant2_2 'T2
End

(*
“Variant1_1 3”
“Variant1_2 3”

type_of “CONS 3”
*)

(* TODO: argument order, we must also omit arguments in new type *)
Datatype:
  list_t =
    ListCons 't list_t
  | ListNil
End

val list_nth_mut_loop_loop_fwd_def = Define ‘
  list_nth_mut_loop_loop_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);
      list_nth_mut_loop_loop_fwd tl i0
      od
  | ListNil => 
    Fail Failure
’

(*
CoInductive coind:
 !x y. coind x /\ coind y ==> coind (x + y)
End
*)

(*
(* This generates inconsistent theorems *)
CoInductive loop:
 !x. loop x = if x then loop x else 0
End

CoInductive loop:
 !(x : int). loop x = if x > 0 then loop (x - 1) else 0
End
*)

(* This terminates *)
val list_nth_mut_loop_loop_fwd_def = Define ‘
  list_nth_mut_loop_loop_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);
      list_nth_mut_loop_loop_fwd tl i0
      od
  | ListNil => 
    Fail Failure
’

(* This is sort of a coinductive definition.

   This can be justified:
   - we first define a version [nth_fuel] which uses fuel (and is thus terminating)
   - we define the predicate P:
     P ls i n = case nth_fuel n ls i of Return _ => T |  _ => F
   - we then use [LEAST] (least upper bound for natural numbers) to define nth as:
     “nth ls i = if (?n. P n) then nth_fuel (LEAST (P ls i)) ls i else Fail Loop ”
   - we finally prove that nth satisfies the proper equation.

     We would need the following intermediate lemma:
     !n.
       n < LEAST (P ls i) ==> nth_fuel n ls i = Fail _ /\
       n >= LEAST (P ls i) ==> nth_fuel n ls i = nth_fuel (LEAST P ls i) ls i
     
 *)
val _ = new_constant ("nth", “:'t list_t -> u32 -> 't result”)
val nth_def = new_axiom ("nth_def", “
 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
 ”)


(*** Examples of proofs on [nth] *)
val list_t_v_def = Define ‘
  list_t_v ListNil = [] /\
  list_t_v (ListCons x tl) = x :: list_t_v tl
’

(* TODO: move *)
open dep_rewrite
open integerTheory

Theorem INT_OF_NUM_INJ:
  !n m. &n = &m ==> n = m
Proof
  rpt strip_tac >>
  fs [Num]
QED

Theorem NUM_SUB_1_EQ:
  !i. 0 <= i - 1 ==> Num i = SUC (Num (i-1))
Proof
  rpt strip_tac >>
  (* 0 <= i *)
  sg ‘0 <= i’ >- COOPER_TAC >>
  (* Get rid of the SUC *)
  sg ‘SUC (Num (i - 1)) = 1 + Num (i - 1)’ >-(rw [ADD]) >>
  rw [] >>
  (* Convert to integers*)
  irule INT_OF_NUM_INJ >>
  imp_res_tac (GSYM INT_OF_NUM) >>
  (* Associativity of & *)
  PURE_REWRITE_TAC [GSYM INT_ADD] >>
  fs []
QED

(* TODO:
   - list all the integer variables, and insert bounds in the assumptions
   - replace u32_min by 0?
   - i - 1
   - auto lookup of spec lemmas
*)

(* Add a list of theorems in the assumptions - TODO: move *)
fun ASSUME_TACL (thms : thm list) : tactic =
  let
    (* TODO: use MAP_EVERY *)
    fun t thms =
      case thms of
        [] => ALL_TAC
      | thm :: thms => ASSUME_TAC thm >> t thms
  in
  t thms
  end

(* Drop/forget a theorem.

   To be used in conjunction with {!pop_assum} for instance.
 *)
fun DROP_TAC (_ : thm) : tactic = ALL_TAC

(* The map from integer type to bounds lemmas *)
val integer_bounds_lemmas =
  Redblackmap.fromList String.compare
  [
    ("u32", u32_to_int_bounds),
    ("i32", i32_to_int_bounds)
  ]

(* The map from integer type to conversion lemmas *)
val integer_conversion_lemmas =
  Redblackmap.fromList String.compare
  [
    ("u32", int_to_u32_id),
    ("i32", int_to_i32_id)
  ]

val integer_conversion_lemmas_list =
  map snd (Redblackmap.listItems integer_conversion_lemmas)

(* Not sure how term nets work, nor how we are supposed to convert Term.term
   to mlibTerm.term.

   TODO: it seems we need to explore the term and convert everything to strings.
 *)
fun term_to_mlib_term (t : term) : mlibTerm.term =
  mlibTerm.string_to_term (term_to_string t)

(*
(* The lhs of the conclusion of the integer conversion lemmas - we use this for
   pattern matching *)
val integer_conversion_lhs_concls =
  let
    val thms = map snd (Redblackmap.listItems integer_conversion_lemmas);
    val concls = map (lhs o concl o UNDISCH_ALL o SPEC_ALL) thms;
  in concls end
*)

(*
val integer_conversion_concls_net =
  let
    val maplets = map (fn x => fst (dest_eq x) |-> ()) integer_conversion_concls;

    val maplets = map (fn x => fst (mlibTerm.dest_eq x) |-> ()) integer_conversion_concls;
    val maplets = map (fn x => fst (mlibThm.dest_unit_eq x) |-> ()) integer_conversion_concls;
    val parameters = { fifo=false };
  in mlibTermnet.from_maplets parameters maplets end

mlibTerm.string_to_term (term_to_string “u32_to_int (int_to_u32 n) = n”)
term_to_quote

SIMP_CONV
mlibThm.dest_thm u32_to_int_bounds
mlibThm.dest_unit u32_to_int_bounds
*)

(* The integer types *)
val integer_types_names =
  Redblackset.fromList String.compare
  (map fst (Redblackmap.listItems integer_bounds_lemmas))

val all_integer_bounds = [
  u32_max_def,
  i32_min_def,
  i32_max_def
]

(* Small utility: compute the set of assumptions in the context.

   We isolate this code in a utility in order to be able to improve it:
   for now we simply put all the assumptions in a set, but in the future
   we might want to split the assumptions which are conjunctions in order
   to be more precise.
 *)
fun compute_asms_set ((asms,g) : goal) : term Redblackset.set =
  Redblackset.fromList Term.compare asms

(* See {!assume_bounds_for_all_int_vars}.

   This tactic is in charge of adding assumptions for one variable.
 *)

fun assume_bounds_for_int_var
  (asms_set: term Redblackset.set) (var : string) (ty : string) :
  tactic =
  let
    (* Lookup the lemma to apply *)
    val lemma = Redblackmap.find (integer_bounds_lemmas, ty);
    (* Instantiate the lemma *)
    val ty_t = mk_type (ty, []);
    val var_t = mk_var (var, ty_t);
    val lemma = SPEC var_t lemma;
    (* Split the theorem into a list of conjuncts.

       The bounds are typically a conjunction:
       {[
         ⊢ 0 ≤ u32_to_int x ∧ u32_to_int x ≤ u32_max: thm
       ]}
     *)
    val lemmas = CONJUNCTS lemma;
    (* Filter the conjuncts: some of them might already be in the context,
       we don't want to introduce them again, as it would pollute it.
     *)
    val lemmas = filter (fn lem => not (Redblackset.member (asms_set, concl lem))) lemmas;
   in
  (* Introduce the assumptions in the context *)
  ASSUME_TACL lemmas
  end

(* Destruct if possible a term of the shape: [x y],
   where [x] is not a comb.

   Returns [(x, y)]
 *)
fun dest_single_comb (t : term) : (term * term) option =
  case strip_comb t of
    (x, [y]) => SOME (x, y)
  | _ => NONE

(** Destruct if possible a term of the shape: [x (y z)].
    Returns [(x, y, z)]
 *)
fun dest_single_comb_twice (t : term) : (term * term * term) option =
  case dest_single_comb t of
    NONE => NONE
  | SOME (x, y) =>
    case dest_single_comb y of
      NONE => NONE
    | SOME (y, z) => SOME (x, y, z)

(* A utility map to lookup integer conversion lemmas *)
val integer_conversion_pat_map =
  let
    val thms = map snd (Redblackmap.listItems integer_conversion_lemmas);
    val tl = map (lhs o concl o UNDISCH_ALL o SPEC_ALL) thms;
    val tl = map (valOf o dest_single_comb_twice) tl;
    val tl = map (fn (x, y, _) => (x, y)) tl;
    val m = Redblackmap.fromList Term.compare tl
  in m end

(* Introduce bound assumptions for all the machine integers in the context.

   Exemple:
   ========
   If there is “x : u32” in the input set, then we introduce:
   {[
     0 <= u32_to_int x
     u32_to_int x <= u32_max
   ]}
 *)
fun assume_bounds_for_all_int_vars (asms, g) =
  let
    (* Compute the set of integer variables in the context *)
    val vars = free_varsl (g :: asms);
    (* Compute the set of assumptions already present in the context *)
    val asms_set = compute_asms_set (asms, g);
    (* Filter the variables to keep only the ones with type machine integer,
       decompose the types at the same time *)
    fun decompose_var (v : term) : (string * string) =
      let
        val (v, ty) = dest_var v;
        val {Args=args, Thy=thy, Tyop=ty} = dest_thy_type ty;
        val _ = assert null args;
        val _ = assert (fn thy => thy = primitives_theory_name) thy;
        val _ = assert (fn ty => Redblackset.member (integer_types_names, ty)) ty;
      in (v, ty) end;
    val vars = mapfilter decompose_var vars; 
    (* Add assumptions for one variable *)
    fun add_var_asm (v, ty) : tactic =
      assume_bounds_for_int_var asms_set v ty;    
    (* Add assumptions for all the variables *)
    (* TODO: use MAP_EVERY *)
    fun add_vars_asm vl : tactic =
      case vl of
        [] => ALL_TAC
      | v :: vl =>
        add_var_asm v >> add_vars_asm vl;
  in
    add_vars_asm vars (asms, g)
  end

(*
dest_thy_type “:u32”
val massage : tactic = assume_bounds_for_all_int_vars
val vl = vars
val (v::vl) = vl
*)

(*
val (asms, g) = top_goal ()
fun bounds_for_ints_in_list (vars : (string * hol_type) list) : tactic =
  foldl
  FAIL_TAC ""
val var = "x"
val ty = "u32"

val asms_set = Redblackset.fromList Term.compare asms;

val x = “1: int”
val ty = "u32"

val thm = lemma
*)

(* Given a theorem of the shape:
   {[
     A0, ..., An ⊢ B0 ==> ... ==> Bm ==> concl
   ]}

   Rewrite it so that it has the shape:
   {[
     ⊢ (A0 /\ ... /\ An /\ B0 /\ ... /\ Bm) ==> concl
   ]}
 *)
fun thm_to_conj_implies (thm : thm) : thm =
  let
    (* Discharge all the assumptions *)
    val thm = DISCH_ALL thm;
    (* Rewrite the implications as one conjunction *)
    val thm = PURE_REWRITE_RULE [GSYM satTheory.AND_IMP] thm;
  in thm end

(* If the current goal is [asms ⊢ g], and given a lemma of the form
   [⊢ H ==> C], do the following:
   - attempt to prove [asms ⊢ H] using the given tactic
   - if it succeeds, call the theorem tactic with the theorem [asms ⊢ C]
   
   If the lemma is not an implication, we directly call the theorem tactic.
 *)
fun prove_premise_then_apply (prove_hyp: tactic) (then_tac: thm_tactic) (thm : thm)  : tactic =
  let
    val c = concl thm;
    (* First case: there is a premise to prove *)
    fun prove_premise_then (h : term) =
      SUBGOAL_THEN h (fn h_thm => then_tac (MP thm h_thm)) >- prove_hyp;
    (* Second case: no premise to prove *)
    val no_prove_premise_then = then_tac thm;
  in
    if is_imp c then prove_premise_then (fst (dest_imp c)) else no_prove_premise_then
  end

(* Call a function on all the subterms of a term *)
fun dep_apply_in_subterms
  (f : string Redblackset.set -> term -> unit)
  (bound_vars : string Redblackset.set)
  (t : term) : unit =
  let
    val dep = dep_apply_in_subterms f;
    val _ = f bound_vars t;
  in
  case dest_term t of
    VAR (name, ty) => ()
  | CONST {Name=name, Thy=thy, Ty=ty} => ()
  | COMB (app, arg) =>
    let
      val _ = dep bound_vars app;
      val _ = dep bound_vars arg;
    in () end
  | LAMB (bvar, body) =>
    let
      val (varname, ty) = dest_var bvar;
      val bound_vars = Redblackset.add (bound_vars, varname);
      val _ = dep bound_vars body;
    in () end
  end

(* Attempt to instantiate a rewrite theorem.

   Remark: this theorem should be of the form:
   H ⊢ x = y
   
   (without quantified variables).
   
   **REMARK**: the function raises a HOL_ERR exception if it fails.
   
   [forbid_vars]: forbid substituting with those vars (typically because
   they are bound elsewhere).
*)
fun instantiate_dep_rewrite (forbid_vars : string Redblackset.set) (th : thm) (t : term) : thm =
  let
      (* Retrieve the lhs of the conclusion of the theorem *)
      val l = lhs (concl th);
      (* Match this lhs with the term *)
      val (var_s, ty_s) = match_term l t;
      (* Check that we are allowed to perform the substitution *)
      val free_vars = free_varsl (map (fn {redex=_, residue=x} => x) var_s);
      val free_vars = map (fst o dest_var) free_vars;
      val free_vars = Redblackset.fromList String.compare free_vars;
      val _ = assert Redblackset.isEmpty (Redblackset.intersection (free_vars, forbid_vars));
  in
    (* Perform the substitution *)
    INST var_s (INST_TYPE ty_s th)
  end

(*
val forbid_vars = Redblackset.empty String.compare
val t = “u32_to_int (int_to_u32 x)”
val t = “u32_to_int (int_to_u32 3)”
val th = (UNDISCH_ALL o SPEC_ALL) int_to_u32_id
*)

fun instantiate_dep_rewrites (th : thm) (t : term) : thm list =
  let
    val th = (UNDISCH_ALL o SPEC_ALL) th;
    (* We use a map when storing the theorems, to avoid storing the same theorem twice *)
    val inst_thms: (term, thm) Redblackmap.dict ref = ref (Redblackmap.mkDict Term.compare);
    fun try_instantiate bvars t =
      let
        val inst_th = instantiate_dep_rewrite bvars th t;
      in
        inst_thms := Redblackmap.insert (!inst_thms, lhs (concl inst_th), inst_th)
      end
      handle HOL_ERR _ => ();
    (* Explore the term *)
    val _ = dep_apply_in_subterms try_instantiate (Redblackset.empty String.compare) t;
  in
    map snd (Redblackmap.listItems (!inst_thms))
  end

(*
val t = “!x. u32_to_int (int_to_u32 x) = u32_to_int (int_to_u32 y)”
val th = int_to_u32_id

val thms = instantiate_dep_rewrites int_to_u32_id
  “!x. u32_to_int (int_to_u32 x) = u32_to_int (int_to_u32 y)”
*)

(* Attempt to apply dependent rewrites with a theorem *)
fun apply_dep_rewrites_tac (prove_premise : tactic) (then_tac : thm_tactic) (th : thm) : tactic =
  fn (asms, g) =>
    let
      (* Discharge the assumptions so that the goal is one single term *)
      val dg = list_mk_imp (asms, g)
      val thms = instantiate_dep_rewrites th dg;
      val thms = map thm_to_conj_implies thms;
      (* Apply each theorem *)
    in
      MAP_EVERY (prove_premise_then_apply prove_premise then_tac) thms (asms, g)
    end

(*
val (asms, g) = ([
  “u32_to_int z = u32_to_int i − u32_to_int (int_to_u32 1)”,
  “u32_to_int (int_to_u32 2) = 2”
], “T”)

apply_dep_rewrites_tac
  (FULL_SIMP_TAC simpLib.empty_ss all_integer_bounds >> COOPER_TAC)
  (fn th => FULL_SIMP_TAC simpLib.empty_ss [th])
  int_to_u32_id
*)

(* See {!rewrite_all_int_conversion_ids}.

   Small utility which takes care of one rewriting.

   TODO: we actually don't use it.
 *)
fun rewrite_int_conversion_id
  (asms_set: term Redblackset.set) (x : term) (ty : string) :
  tactic =
  let
    (* Lookup the theorem *)
    val lemma = Redblackmap.find (integer_conversion_lemmas, ty);
    (* Instantiate *)
    val lemma = SPEC x lemma;
    (* Rewrite the lemma. The lemma typically has the shape:
       ⊢ u32_min <= x /\ x <= u32_max ==> u32_to_int (int_to_u32 x) = x
       
       Make sure the lemma has the proper shape, attempt to prove the premise,
       then use the conclusion if it succeeds.
     *)
    val lemma = thm_to_conj_implies lemma;
    (* Retrieve the conclusion of the lemma - we do this to check if it is not
       already in the assumptions *)
    val c = concl (UNDISCH_ALL lemma);
    val already_in_asms = Redblackset.member (asms_set, c);
    (* Small utility: the tactic to prove the premise *)
    val prove_premise =
      (* We might need to unfold the bound definitions, in particular if the
         term is a constant (e.g.,  “3:int”) *)
      FULL_SIMP_TAC simpLib.empty_ss all_integer_bounds >>
      COOPER_TAC;
    (* Rewrite with a lemma, then assume it *)
    fun rewrite_then_assum (thm : thm) : tactic =
      FULL_SIMP_TAC simpLib.empty_ss [thm] >> assume_tac thm;
  in
    (* If the conclusion is not already in the assumptions, prove it, use
       it to rewrite the goal and add it in the assumptions, otherwise do nothing *)
    if already_in_asms then ALL_TAC
    else prove_premise_then_apply prove_premise rewrite_then_assum lemma
 end

(* Look for conversions from integers to machine integers and back.
   {[
     u32_to_int (int_to_u32 x)
   ]}

   Attempts to prove and apply equalities of the form:
   {[
     u32_to_int (int_to_u32 x) = x
   ]}
   
   **REMARK**: this function can fail, if it doesn't manage to prove the
   premises of the theorem to apply.
 *)
val rewrite_all_int_conversion_ids : tactic =
  (* We're not trying to be smart: we just try to rewrite with each theorem at
     a time *)
  let
    val prove_premise = FULL_SIMP_TAC simpLib.empty_ss all_integer_bounds >> COOPER_TAC;
    val then_tac = (fn th => FULL_SIMP_TAC simpLib.empty_ss [th]);
    val rewr_tac = apply_dep_rewrites_tac prove_premise then_tac;
  in
      MAP_EVERY rewr_tac integer_conversion_lemmas_list
  end

(* Massage a bit the goal, for instance by introducing integer bounds in the
   assumptions.
*)
val massage : tactic = assume_bounds_for_all_int_vars >> rewrite_all_int_conversion_ids

Theorem nth_lem:
  !(ls : 't list_t) (i : u32).
    u32_to_int i < int_of_num (LENGTH (list_t_v ls)) ==>
    case nth ls i of
    | Return x => x = EL (Num (u32_to_int i)) (list_t_v ls)
    | Fail _ => F
    | Loop => F
Proof
  Induct_on ‘ls’ >> fs [list_t_v_def, HD] >~ [‘ListNil’] >>
  rpt strip_tac >> massage >>
  PURE_ONCE_REWRITE_TAC [nth_def] >> rw [] >-(intLib.COOPER_TAC) >>
  (* TODO: we need specialized tactics here - first: subgoal *)
  sg ‘0 <= u32_to_int i - u32_to_int (int_to_u32 1)’ >-(
    massage >> COOPER_TAC
  ) >>
  (* TODO: automate (should be in a massage) *)
  imp_res_tac U32_SUB_EQ >> fs [st_ex_bind_def, list_t_v_def] >> rw [] >>
  massage >> fs [] >> rw [] >>
  (* Finish the proof by recursion *)
  (* TODO: automate (it should be in massage) *)
  qspec_then ‘u32_to_int z’ imp_res_tac NUM_SUB_1_EQ >> rw [] >> rfs [] >>
  (* TODO: automate this: we should be able to analyze the ‘nth ls z’,
     notice there is a quantified assumption in the context,
     and instantiate it properly.

     Remark: we can apply the resulting theorem only after rewriting it.
     Possibility:
     - do some default rewriting and try to apply it
     - if it fails, simply add it in the assumptions for the user
   *)
  pop_last_assum (qspec_then ‘z’ assume_tac) >> rfs [] >>
  pop_assum irule >>
  COOPER_TAC
QED

(***
 * Example of how to get rid of the fuel in practice
 *)
val nth_fuel_def = Define ‘
 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 is_loop_def = Define ‘is_loop r = case r of Loop => T | _ => F’
 
val nth_fuel_P_def = Define ‘
  nth_fuel_P ls i n = ~is_loop (nth_fuel n ls i)
’

Theorem nth_fuel_mono:
  !n m ls i.
    n <= m ==>
    if is_loop (nth_fuel n ls i) then T
    else nth_fuel n ls i = nth_fuel m ls i
Proof
  Induct_on ‘n’ >- (
    rpt gen_tac >>
    DISCH_TAC >>
    PURE_ONCE_REWRITE_TAC [nth_fuel_def] >>
    rw[is_loop_def]
  ) >>
  (* Interesting case *)
  rpt gen_tac >>
  DISCH_TAC >>
  CASE_TAC >>
  Cases_on ‘m’ >- (
    (* Contradiction: SUC n < 0 *)
    sg ‘SUC n = 0’ >- decide_tac >>
    fs [is_loop_def]
  ) >>
  fs [is_loop_def] >>
  pop_assum mp_tac >>
  PURE_ONCE_REWRITE_TAC [nth_fuel_def] >>
  fs [] >>
  DISCH_TAC >>
  (* We just have to explore all the paths: we can have dedicated tactics for that
     (we need to do case analysis) *)
  Cases_on ‘ls’ >> fs [] >>
  Cases_on ‘u32_to_int (i :u32) = (0 :int)’ >> fs [] >>
  fs [st_ex_bind_def] >>
  Cases_on ‘u32_sub (i :u32) (int_to_u32 (1 :int))’ >> fs [] >>
  (* Apply the induction hypothesis *)
  first_x_assum (qspecl_then [‘n'’, ‘l’, ‘a’] assume_tac) >>
  first_x_assum imp_res_tac >>
  pop_assum mp_tac >>
  CASE_TAC
QED

Theorem nth_fuel_P_mono:
  !n m ls i.
    n <= m ==>
    nth_fuel_P ls i n ==>
    nth_fuel n ls i = nth_fuel m ls i
Proof
  rpt gen_tac >> rpt DISCH_TAC >>
  fs [nth_fuel_P_def] >>
  imp_res_tac nth_fuel_mono >>
  pop_assum (qspecl_then [‘ls’, ‘i’] assume_tac) >>
  pop_assum mp_tac >> CASE_TAC >> fs []
QED

Theorem nth_fuel_least_fail_mono:
  !n ls i.
    n < $LEAST (nth_fuel_P ls i) ==>
    nth_fuel n ls i = Loop
Proof
  rpt gen_tac >>
  disch_tac >>
  imp_res_tac whileTheory.LESS_LEAST >>
  fs [nth_fuel_P_def, is_loop_def] >>
  pop_assum mp_tac >>
  CASE_TAC
QED

Theorem nth_fuel_least_success_mono:
  !n ls i.
    $LEAST (nth_fuel_P ls i) <= n ==>
    nth_fuel n ls i = nth_fuel ($LEAST (nth_fuel_P ls i)) ls i
Proof
  rpt gen_tac >>
  disch_tac >>
  (* Case disjunction on whether there exists a fuel such that it terminates *)
  Cases_on ‘?m. nth_fuel_P ls i m’ >- (
    (* Terminates *)
    irule EQ_SYM >>
    irule nth_fuel_P_mono >> fs [] >>
    (* Prove that calling with the least upper bound of fuel succeeds *)    
    qspec_then ‘nth_fuel_P (ls :α list_t) (i :u32)’ imp_res_tac whileTheory.LEAST_EXISTS_IMP
  ) >>
  (* Doesn't terminate *)
  fs [] >>
  sg ‘~(nth_fuel_P ls i n)’ >- fs [] >>
  sg ‘~(nth_fuel_P ls i ($LEAST (nth_fuel_P ls i)))’ >- fs [] >>
  fs [nth_fuel_P_def, is_loop_def] >>
  pop_assum mp_tac >> CASE_TAC >>
  pop_assum mp_tac >>
  pop_assum mp_tac >> CASE_TAC
QED

val nth_def_raw = Define ‘
  nth ls i =
    if (?n. nth_fuel_P ls i n) then nth_fuel ($LEAST (nth_fuel_P ls i)) ls i
    else Loop
’

(* This makes the proofs easier, in that it helps us control the context *)
val nth_expand_def = Define ‘
  nth_expand nth ls i =
    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
’             

(* Prove the important theorems *)
Theorem nth_def_terminates:
  !ls i.
  (?n. nth_fuel_P ls i n) ==>
  nth ls i =
    nth_expand nth ls i
Proof
  rpt strip_tac >>
  fs [nth_expand_def] >>
  PURE_ONCE_REWRITE_TAC [nth_def_raw] >>
  (* Prove that the least upper bound is <= n *)
  sg ‘$LEAST (nth_fuel_P ls i) <= n’ >-(
    qspec_then ‘nth_fuel_P (ls :α list_t) (i :u32)’ imp_res_tac whileTheory.LEAST_EXISTS_IMP >>
    spose_not_then assume_tac >> fs []
  ) >>
  (* Use the monotonicity theorem - TODO: ? *)
  imp_res_tac nth_fuel_least_success_mono >>
  (* Rewrite only on the left - TODO: easy way ?? *)
  qspecl_then [‘$LEAST (nth_fuel_P ls i)’, ‘ls’, ‘i’] assume_tac nth_fuel_def >>
  (* TODO: how to discard assumptions?? *)
  fs [] >> pop_assum (fn _ => fs []) >>
  (* Cases on the least upper bound *)
  Cases_on ‘$LEAST (nth_fuel_P ls i)’ >> rw [] >- (
    (* The bound is equal to 0: contradiction *)
    sg ‘nth_fuel 0 ls i = Loop’ >- (PURE_ONCE_REWRITE_TAC [nth_fuel_def] >> rw []) >>
    fs [nth_fuel_P_def, is_loop_def]
  ) >>
  (* Bound not equal to 0 *)
  fs [nth_fuel_P_def, is_loop_def] >>
  (* Explore all the paths *)
  fs [st_ex_bind_def] >>
  Cases_on ‘ls’ >> rw [] >> fs [] >>
  Cases_on ‘u32_sub i (int_to_u32 1)’ >> rw [] >> fs [] >>
  (* Recursive call: use monotonicity - we have an assumption which eliminates the Loop case *)
  Cases_on ‘nth_fuel n' l a’ >> rw [] >> fs [] >>
  (sg ‘nth_fuel_P l a n'’ >- fs [nth_fuel_P_def, is_loop_def]) >>
  (sg ‘$LEAST (nth_fuel_P l a) <= n'’ >-(
   qspec_then ‘nth_fuel_P l a’ imp_res_tac whileTheory.LEAST_EXISTS_IMP >>
   spose_not_then assume_tac >> fs [])) >>
  imp_res_tac nth_fuel_least_success_mono >> fs []
QED

(* Prove the important theorems *)
Theorem nth_def_loop:
  !ls i.
  (!n. ~nth_fuel_P ls i n) ==>
  nth ls i =
    nth_expand nth ls i
Proof
  rpt gen_tac >>
  PURE_ONCE_REWRITE_TAC [nth_def_raw] >>
  strip_tac >> rw[] >>
  (* Non-terminating case *)
  sg ‘∀n. ¬nth_fuel_P ls i (SUC n)’ >- rw [] >>
  fs [nth_fuel_P_def, is_loop_def] >>
  pop_assum mp_tac >>
  PURE_ONCE_REWRITE_TAC [nth_fuel_def] >>
  rw [] >>  
  fs [nth_expand_def] >>
  (* Evaluate all the paths *)
  fs [st_ex_bind_def] >>
  Cases_on ‘ls’ >> rw [] >> fs [] >>
  Cases_on ‘u32_sub i (int_to_u32 1)’ >> rw [] >> fs [] >>
  (* Use the definition of nth *)
  rw [nth_def_raw] >>
  first_x_assum (qspec_then ‘$LEAST (nth_fuel_P l a)’ assume_tac) >>
  Cases_on ‘nth_fuel ($LEAST (nth_fuel_P l a)) l a’ >> fs []
QED

(* The final theorem *)
Theorem nth_def:
  !ls i.
  nth ls i =
    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 >>
  Cases_on ‘?n. nth_fuel_P ls i n’ >-(
    assume_tac nth_def_terminates >>
    fs [nth_expand_def] >>
    pop_assum irule >>
    metis_tac []) >>
  fs [] >> imp_res_tac nth_def_loop >> fs [nth_expand_def]
QED

(*

Je viens de finir ma petite expérimentation avec le fuel : ça marche bien. Par exemple, si je pose les définitions suivantes :
Datatype:
  result = Return 'a | Fail error | Loop
End

(* Omitting some definitions like the bind *)

val _ = Define ‘
 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 _ = Define 'is_loop r = case r of Loop => T | _ => F'
 
val _ = Define 'nth_fuel_P ls i n = ~is_loop (nth_fuel n ls i)'

(* $LEAST returns the least upper bound for a predicate (if it exists - otherwise it returns an arbitrary number) *)
val _ = Define ‘
  nth ls i =
    if (?n. nth_fuel_P ls i n) then nth_fuel ($LEAST (nth_fuel_P ls i)) ls i
    else Loop
’
J'arrive à montrer (c'est un chouïa technique) :
Theorem nth_def:
  !ls i.
  nth ls i =
    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

*)