Theory Higher_Order_Terms.Nterm

chapter ‹Terms with explicit bound variable names›

theory Nterm
imports Term_Class
begin

text ‹
  The ‹nterm› type is similar to @{typ term}, but removes the distinction between bound and free
  variables. Instead, there are only named variables.
›

datatype nterm =
  Nconst name |
  Nvar name |
  Nabs name nterm ("Λ⇩n _. _" [0, 50] 50) |
  Napp nterm nterm (infixl "$⇩n" 70)

derive linorder nterm

instantiation nterm :: pre_term begin

definition app_nterm where
"app_nterm t u = t $⇩n u"

fun unapp_nterm where
"unapp_nterm (t $⇩n u) = Some (t, u)" |
"unapp_nterm _ = None"

definition const_nterm where
"const_nterm = Nconst"

fun unconst_nterm where
"unconst_nterm (Nconst name) = Some name" |
"unconst_nterm _ = None"

definition free_nterm where
"free_nterm = Nvar"

fun unfree_nterm where
"unfree_nterm (Nvar name) = Some name" |
"unfree_nterm _ = None"

fun frees_nterm :: "nterm ⇒ name fset" where
"frees_nterm (Nvar x) = {| x |}" |
"frees_nterm (t⇩1 $⇩n t⇩2) = frees_nterm t⇩1 |∪| frees_nterm t⇩2" |
"frees_nterm (Λ⇩n x. t) = frees_nterm t - {| x |}" |
"frees_nterm (Nconst _) = {||}"

fun subst_nterm :: "nterm ⇒ (name, nterm) fmap ⇒ nterm" where
"subst_nterm (Nvar s) env = (case fmlookup env s of Some t ⇒ t | None ⇒ Nvar s)" |
"subst_nterm (t⇩1 $⇩n t⇩2) env = subst_nterm t⇩1 env $⇩n subst_nterm t⇩2 env" |
"subst_nterm (Λ⇩n x. t) env = (Λ⇩n x. subst_nterm t (fmdrop x env))" |
"subst_nterm t env = t"

fun consts_nterm :: "nterm ⇒ name fset" where
"consts_nterm (Nconst x) = {| x |}" |
"consts_nterm (t⇩1 $⇩n t⇩2) = consts_nterm t⇩1 |∪| consts_nterm t⇩2" |
"consts_nterm (Nabs _ t) = consts_nterm t" |
"consts_nterm (Nvar _) = {||}"

instance
by standard
   (auto
      simp: app_nterm_def const_nterm_def free_nterm_def
      elim: unapp_nterm.elims unconst_nterm.elims unfree_nterm.elims
      split: option.splits)

end

instantiation nterm :: "term" begin

definition abs_pred_nterm :: "(nterm ⇒ bool) ⇒ nterm ⇒ bool" where
[code del]: "abs_pred P t ⟷ (∀t' x. t = (Λ⇩n x. t') ⟶ P t' ⟶ P t)"

instance proof (standard, goal_cases)
  case (1 P t)
  then show ?case
    by (induction t) (auto simp: abs_pred_nterm_def const_nterm_def free_nterm_def app_nterm_def)
next
  case 3
  show ?case
    unfolding abs_pred_nterm_def
    apply auto
    apply (subst fmdrop_comm)
    by auto
next
  case 4
  show ?case
    unfolding abs_pred_nterm_def
    apply auto
    apply (erule_tac x = "fmdrop x env⇩1" in allE)
    apply (erule_tac x = "fmdrop x env⇩2" in allE)
    by (auto simp: fdisjnt_alt_def)
next
  case 5
  show ?case
    unfolding abs_pred_nterm_def
    apply clarify
    subgoal for t' x env
      apply (erule allE[where x = "fmdrop x env"])
      by auto
    done
next
  case 6
  show ?case
    unfolding abs_pred_nterm_def
    apply clarify
    subgoal premises prems[rule_format] for t x env
      unfolding consts_nterm.simps subst_nterm.simps frees_nterm.simps
      apply (subst prems)
      unfolding fmimage_drop fmdom_drop
      apply (rule arg_cong[where f = "(|∪|) (consts t)"])
      apply (rule arg_cong[where f = ffUnion])
      apply (rule arg_cong[where f = "λx. consts |`| fmimage env x"])
      by auto
    done
qed (auto simp: abs_pred_nterm_def)

end

lemma no_abs_abs[simp]: "¬ no_abs (Λ⇩n x. t)"
by (subst no_abs.simps) (auto simp: term_cases_def)

end