Stream: Beginner Questions

Topic: No code equation for interpretation, unless it is global

view this post on Zulip David Wang (Dec 12 2023 at 15:46):

Hello,

I have a locale form_syntax, which defines a function free_vars.
I have defined the necessary lemmas and functions to instantiate form_syntax. I cannot find a way to instantiate it within a context or sub-locale, while getting Isabelle to generate executable code. What works is the following:

(* define a few lemmas and functions *)
global_interpretation ta_forms: form_syntax ta_subst ta_vars ta_consts t_vars ent
  defines fv = ta_forms.free_vars
  using ta_subst_leaves_consts ta_subst_comp
        ta_subst_assoc t_vars_eq_ta_vars
  by unfold_locales auto
 value "fv (Atom (predAtm (Pred ''1234'') [term.VAR (Var ''123'')]))"

What I want to do is something like:

locale impl
begin
<define the assumed lemmas and functions>
end

context impl
begin
<be able to call the functions defined in 'form_syntax' here>
end

What does not work:

locale ta_forms
begin
(* define functions and lemmas needed for form_syntax *)
end
sublocale ta_forms ⊆ form_syntax ta_subst ta_vars ta_consts t_vars ent
  defines free_vars = free_vars
  using ta_subst_leaves_consts ta_subst_comp
        ta_subst_assoc t_vars_eq_ta_vars
  by unfold_locales auto

context ta_forms
begin
value "free_vars (Atom (predAtm (Pred ''1234'') [term.VAR (Var ''123'')]))"
(* no code equation *)
end

Last updated: Apr 27 2024 at 16:16 UTC