Structure alist_treeLib

(* Code to recall that some partial functions (of type 'a -> 'b option)
can be represented as sorted alists, and derive a fast conversion on
applications of those functions. *)

signature alist_treeLib = sig

include Abbrev

(* Syntax *)
val alookup_tm : term;
val option_choice_tm : term;
val repr_tm : term;

(* The repr set type *)
type 'a alist_reprs

(*
   Representations of partial functions using sorted trees.
   Requires a relation R and a theorem that shows
   it is irreflexive and transitive. The destructor maps terms
   of the domain type to some type that can be sorted in ML.
   The conversion must prove R x y for any x, y where x is
   sorted before y by the destructor and comparison.
*)
val mk_alist_reprs : thm -> conv -> (term -> 'a)
    -> (('a * 'a) -> order) -> 'a alist_reprs

(*
   The representation set contains representations of various
   partial functions, initially none.
*)
val peek_functions_in_rs : 'a alist_reprs -> term list

(*
   Adds a function's representation.

   Requires a theorem f = rhs with a valid rhs.
   A valid rhs is:
     - ALOOKUP xs
     - a function g in the repr set.
     - option_choice_f of two valid rhs values
*)
val add_alist_repr : 'a alist_reprs -> thm -> unit

(*
   Converts f x to a concrete value (SOME y/NONE)
   for functions f in the repr set.
*)
val reprs_conv : 'a alist_reprs -> conv

end

HOL 4, Kananaskis-14