Theory Typed_Substitution_Lifting_Example

theory Typed_Substitution_Lifting_Example
  imports
    Typed_Substitution_Lifting
    Typed_Substitution_Example
    Abstract_Substitution.Substitution_Lifting_Example
begin

text ‹All property locales have corresponding lifting locales›


locale nonground_typing_lifting =
   typed_subst_stability_lifting where 
   sub_welltyped = sub_welltyped and base_welltyped = "welltyped ℱ"
for ℱ :: "('f, 'ty) fun_types" and sub_welltyped :: "('v ⇒ 'ty) ⇒ 'sub ⇒ 'ty' ⇒ bool"

locale example_typing_lifting =
  fixes ℱ :: "('f, 'ty) fun_types"
begin

sublocale equation:
  nonground_typing_lifting where
  base_vars = vars_term and base_subst = subst_apply_term and base_is_ground = is_ground and
  map = "λf. map_prod f f" and to_set = set_prod and comp_subst = subst_compose and 
  id_subst = Var and sub_vars = vars_term and sub_subst = subst_apply_term and
  sub_is_ground = is_ground and sub_welltyped = "welltyped ℱ" and apply_subst = apply_subst and
  subst_update = fun_upd
  by unfold_locales

text ‹Lifted lemmas and definitions›
thm
  equation.is_welltyped_def
  equation.welltyped_subst_stability

term equation.is_welltyped

text ‹We can lift multiple levels›

sublocale equation_set:
  nonground_typing_lifting where
  base_vars = vars_term and base_subst = subst_apply_term and base_is_ground = is_ground and
  map = fimage and to_set = fset and comp_subst = subst_compose and id_subst = Var and
  sub_vars = equation_subst.vars and sub_subst = equation_subst.subst and
  sub_is_ground = equation_subst.is_ground and sub_welltyped = equation.welltyped and
  apply_subst = apply_subst and subst_update = fun_upd
  by unfold_locales

text ‹Lifted lemmas and definitions›
thm
  equation_set.is_welltyped_def
  equation_set.welltyped_subst_stability

term equation_set.is_welltyped

end

text ‹Interpretation with unit as type›
global_interpretation example_typing_lifting "λ_. ([], ())" .

end