[isabelle] Creating cterms with automatic type inference from several distinct terms in Isabelle/ML



Dear All,

I would like to understand if there exists a canonical method for creating
cterms with automatic type inference from several distinct terms in
Isabelle/ML, given that some of these distinct terms are supplied by the
user.  Unfortunately, given that some of the consts that are used in the
terms provided by the user are not known in advance, the methods that I am
aware of do not seem to be directly applicable or may, potentially, result
in certain malpractices.

For example, I would like to perform an automatic type inference and create
a certified term in the context of the following (significantly) simplified
use case:

ML ‹

val A = @{term "A::'al⇒'ar⇒bool"};
val B = @{term "B::'bl⇒'br⇒bool"};
val RF = @{term rel_fun} (*in the use case, RF can represent an arbitrary
const accepting an arbitrary number of arguments, as supplied by the user*)

val uterm = RF $ A $ B;
(* fails because type inference is not applicable: *)
val cterm = Thm.cterm_of @{context} uterm;

›

Of course, the default names of the 'TFree' types that are generated for
rel_fun in the example above are not suitable when $ is used for combining
terms. *It is very important to note that **in my use case **RF is provided
by the user and, therefore, it may be different from rel_fun.*

I am aware of two methods that can be used for the solution of the problem.
However, these methods do not seem to be ideal for my application, given
that the consts are provided by the user:
1. Provide "tailor-made" type inference for each const, similar to the
methodology used in hologic.ml, e.g. HOLogic.mk_eq. Unfortunately, in my
use case, functions like HOLogic.mk_eq need to be generated 'on the fly'
based on the user input. This solution seems to require an investment of a
certain amount of effort.
2. Define terms as strings and use Syntax.read_term to generate terms from
the strings. This solution does not seem to be safe, although, its
implementation is almost trivial.

I provide a code that demonstrates the methods that I am referring to in
the clauses above after my signature. However, please note that the code is
merely an example that is meant for the demonstration of the problem and it
does not contain (almost) any parts of the intended solution. Therefore,
please ignore various malpractices that are not related to the problem (in
particular, the code does not provide guarantees that unique names are used
and omits all error checks).

*Lastly, I would like to provide a summary of the question : *

   - If there is a canonical method for combining arbitrary terms with type
   inference that is different from the methods suggested in clauses 1 and 2
   above, then I would highly appreciate if you could let me know about it. If
   such a method does not exist, then I would like to know whether the
   solution in clause 2 above is considered to be a standard practice or not.

Thank you

ML ‹

(* -------------------------------------------- *)
(* auxiliary functions - provided for completeness *)

fun delete_elem _ [] = []
  | delete_elem a (x::xs) =
    if (a = x) then (delete_elem a xs) else x::(delete_elem a xs);

(* remove duplicates from a list *)
fun remdups [] = []
  | remdups (x::xs) = x::(remdups (delete_elem x xs));

(* get unique free type variables *)
fun get_unique_tfree t =
  remdups(
    rev(
      fold_atyps
        (fn t => fn ts => case t of TFree td => (TFree td)::ts | _ => ts) t
[]
      )
    );

val A = @{term "A::'al⇒'ar⇒bool"};
val B = @{term "B::'bl⇒'br⇒bool"};

(* -------------------------------------------- *)


(*

Solution 1: the solution was inferred from the method suggested in section
3.2
(and other sections) in the document "The Isabelle Cookbook"
(May 28, 2015 draft) by Christian Urban. According to this solution,
a tailor-made type inference procedure needs to be provided for each const.
Of course, for many existing standard consts this functionality has
already been provided in hologic.ML (e.g. HOLogic.mk_eq).

The solution is difficult to implement because the consts are
supplied by the user. Therefore, functions similar to HOLogic.mk_eq need to
be
generated 'on the fly'. Effectively, this would require the development of
the functionality
that would enable automatic generation of a significant part of the content
of hologic.ml.

*)

val boolT = Type ("HOL.bool", []);
fun rel_fun_const (A, B, C, D) =
  Const
    (\<^const_name>‹BNF_Def.rel_fun›,
    (A --> B --> boolT) -->
    (C --> D --> boolT) -->
    (A --> C) -->
    (B --> D) -->
    boolT);

fun get_types_rel_fun fts gts = (nth fts 0, nth fts 1, nth gts 0, nth gts
1);

fun mk_rel_fun (R1, R2) =
  (
  (get_types_rel_fun
  (R1 |> type_of |> get_unique_tfree)
  (R2 |> type_of |> get_unique_tfree)) |> rel_fun_const
  )
  $ R1 $ R2;

val cterm = Thm.cterm_of @{context} (mk_rel_fun (A, B));

(*
Solution 2: inferred from the code on page 118 in
the document "The Isabelle/Isar Implementation" by Makarius Wenzel.

Can be implemented with ease, but requires the construction of terms
from strings. I am not certain if this is considered to be a standard
practice.
*)
val ctxt' = @{context} |> Variable.declare_term A |> Variable.declare_term
B;
val uterm' = Syntax.read_term ctxt' "BNF_Def.rel_fun A B";
val cterm' = Thm.cterm_of @{context} uterm';

›

-- 
Please accept my apologies for posting anonymously. This is done to protect
my privacy. I can make my identity and my real contact details available
upon request in private communication under the condition that they are not
to be mentioned on the mailing list.



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.