Theory IsaFoR_Ground_Term_Compatibility

theory IsaFoR_Ground_Term_Compatibility
  imports
    IsaFoR_Nonground_Context
    Abstract_Substitution.Noop_Substitution
begin

interpretation ground: nonground_term where
  comp_subst = noop_comp_subst and id_subst = noop_id_subst and term_vars = noop_vars and
  subst_update = noop_subst_update and apply_subst = noop_apply_subst and
  term_subst = noop_subst and subst_updates = noop_subst_updates and term_to_ground = id and
  term_from_ground = id and term_is_ground = noop_is_ground
  by unfold_locales (use unit.is_right_invertible_def in simp_all)

interpretation ground: nonground_term_with_context where
  comp_subst = noop_comp_subst and id_subst = noop_id_subst and term_vars = noop_vars and
  subst_update = noop_subst_update and apply_subst = noop_apply_subst and
  term_subst = noop_subst and subst_updates = noop_subst_updates and term_to_ground = id and
  term_from_ground = id and apply_context = apply_ground_context and hole = □ and 
  compose_context = "(∘c)" and map_context = map_args_actxt and context_to_set = set2_actxt and
  ground_hole = □ and compose_ground_context = "(∘c)" and to_ground_context_map = map_args_actxt and 
  from_ground_context_map = map_args_actxt and ground_context_map = map_args_actxt and
  ground_context_to_set = set2_actxt and apply_ground_context = apply_ground_context and
  occurences = "λ_ _. 0" and term_is_ground = noop_is_ground
proof unfold_locales

  interpret grounding_lifting where
    comp_subst = noop_comp_subst and id_subst = noop_id_subst and sub_vars = noop_vars and
    apply_subst = noop_apply_subst and to_set = set2_actxt and sub_is_ground = noop_is_ground and
    sub_to_ground = id and sub_from_ground = id and sub_subst = noop_subst and
    map = map_args_actxt and to_ground_map  = map_args_actxt and from_ground_map = map_args_actxt and
    ground_map  = map_args_actxt and to_set_ground = set2_actxt
    by unfold_locales (auto simp: noop_vars_def)

  fix c c' and t :: "'f gterm" and f :: "'f gterm ⇒ 'f gterm" and σ and x :: 'v

  show "ground.from_ground c⟨t⟩G = (to_ground c)⟨ground.from_ground t⟩G"
    by (simp add: to_ground_def)

  show "ground.from_ground c⟨t⟩G = (from_ground c)⟨ground.from_ground t⟩G"
    by (simp add: from_ground_def)

  show "ground.is_ground c⟨t⟩G ⟷ is_ground c  ∧ ground.is_ground t"
    by (simp add: is_ground_def noop_is_ground_def)

  show "map_args_actxt f (c ∘c c') = map_args_actxt f c ∘c map_args_actxt f c'"
    by (induction c) simp_all

  show "from_ground (c ∘c c') = from_ground c ∘c from_ground c'"
    by (simp add: from_ground_def)

  show "ground.vars c⟨t⟩G = vars c ∪ ground.vars t"
    by (simp add: vars_def noop_vars_def)

  show "noop_subst c⟨t⟩G σ = (subst c σ)⟨noop_subst t σ⟩G"
    by (simp add: subst_def noop_subst_def)

  show "x ∈ ground.vars t ⟹ ∃c. t = c⟨ground.Var x⟩G"
    by (simp add: noop_vars_def)

  show "⋀γ cG tG. noop_subst t γ = cG⟨tG⟩G  ⟹
         (∃c t'. t = c⟨t'⟩G ∧ noop_subst t' γ = tG ∧ local.subst c γ = cG) ∨ 
         (∃c cG' x. t = c⟨ground.Var x⟩G ∧ cG = local.subst c γ ∘c cG')"
    by (simp add: subst_def noop_subst_def)

  show "⟦∃t. ¬ ground.is_ground t; ground.is_ground t⟧ ⟹ 0 = Suc 0"
    by (simp add: noop_vars_def)

  show "x ∈ ground.vars t ⟷ (0::nat) < 0"
    by (simp add: noop_vars_def)
qed simp_all

end