*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] Creating cterms with automatic type inference from several distinct terms in Isabelle/ML*From*: mailing-list anonymous <mailing.list.anonymous at gmail.com>*Date*: Wed, 1 May 2019 02:06:09 +0300

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.

**Follow-Ups**:

- Next by Date: Re: [isabelle] Export files generated by code_export to hard drive
- Next by Thread: Re: [isabelle] Creating cterms with automatic type inference from several distinct terms in Isabelle/ML
- Cl-isabelle-users May 2019 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list