Theory Functional_Substitution_Lifting_Example

theory Functional_Substitution_Lifting_Example ✐‹contributor ‹Balazs Toth››
  imports
    Functional_Substitution_Lifting
    Functional_Substitution_Example
begin

text ‹Lifting of properties from term to equations (modelled as pairs)›

type_synonym ('f,'v) equation = "('f, 'v) term × ('f, 'v) term"

text ‹All property locales have corresponding lifting locales›
locale lifting_term_subst_properties =
  based_functional_substitution_lifting where
  id_subst = Var and comp_subst = subst_compose and base_subst = subst_apply_term and
  base_vars = "vars_term :: ('f, 'v) term ⇒ 'v set" +
  finite_variables_lifting where id_subst = Var and comp_subst = subst_compose

global_interpretation equation_subst:
  lifting_term_subst_properties where
  sub_vars = vars_term and sub_subst = subst_apply_term and map = "λf. map_prod f f" and
  to_set = set_prod
  by unfold_locales fastforce+

text ‹Lifted lemmas and defintions›
thm
  equation_subst.subst_reduntant_upd
  equation_subst.subst_reduntant_if
  equation_subst.vars_subst_subset

  equation_subst.vars_def
  equation_subst.subst_def

text ‹We can lift multiple levels›
global_interpretation equation_set_subst:
  lifting_term_subst_properties where
  sub_vars = equation_subst.vars and sub_subst = equation_subst.subst and map = fimage and 
  to_set = fset
  by unfold_locales (auto simp: rev_image_eqI)

text ‹Lifted lemmas and defintions›
thm
  equation_set_subst.subst_reduntant_upd
  equation_set_subst.subst_reduntant_if
  equation_set_subst.vars_subst_subset

  equation_set_subst.vars_def
  equation_set_subst.subst_def

end