Session Higher_Order_Terms

Theory Term_Utils

theory Term_Utils
imports
  "HOL-Library.Finite_Map"
  "HOL-Library.Monad_Syntax"
  "HOL-Library.State_Monad"
begin

fun map2 where
"map2 f (x # xs) (y # ys) = f x y # map2 f xs ys" |
"map2 _ _ _ = []"

lemma map2_elemE:
  assumes "z  set (map2 f xs ys)"
  obtains x y where "x  set xs" "y  set ys" "z = f x y"
using assms by (induct f xs ys rule: map2.induct) auto

lemma map2_elemE1:
  assumes "length xs = length ys" "x  set xs"
  obtains y where "y  set ys" "f x y  set (map2 f xs ys)"
using assms by (induct xs ys rule: list_induct2) auto

lemma map2_elemE2:
  assumes "length xs = length ys" "y  set ys"
  obtains x where "x  set xs" "f x y  set (map2 f xs ys)"
using assms by (induct xs ys rule: list_induct2) auto

lemma map2_cong[fundef_cong]:
  assumes "xs1 = xs2" "ys1 = ys2"
  assumes fg: "x y. x  set xs1  y  set ys1  f x y = g x y"
  shows "map2 f xs1 ys1 = map2 g xs2 ys2"
proof -
  have "map2 f xs1 ys1 = map2 g xs1 ys1"
    using fg
    by (induction f xs1 ys1 rule: map2.induct) auto
  with assms show ?thesis
    by simp
qed

lemma option_bindE:
  assumes "x  f = Some a"
  obtains x' where "x = Some x'"  "f x' = Some a"
using assms
by (cases x) auto

lemma rel_option_bind[intro]:
  assumes "rel_option R x y" "a b. R a b  rel_option R (f a) (g b)"
  shows "rel_option R (x  f) (y  g)"
using assms(1) proof (cases rule: option.rel_cases)
  case None
  thus ?thesis
    by simp
next
  case (Some a b)
  thus ?thesis
    using assms(2) by simp
qed

lemma list_split:
  assumes "n < length xs"
  obtains xs1 xs2 where "xs = xs1 @ xs2" "n = length xs2" "0 < length xs1"
proof
  let ?xs1 = "take (length xs - n) xs"
  let ?xs2 = "drop (length xs - n) xs"

  show "xs = ?xs1 @ ?xs2"
    by simp
  show "n = length ?xs2" "0 < length ?xs1"
    using assms by auto
qed

context
  includes fset.lifting
begin

lemma ffUnion_alt_def: "x |∈| ffUnion A  fBex A (λX. x |∈| X)"
by transfer blast

lemma funion_image_bind_eq: "ffUnion (f |`| M) = fbind M f"
by transfer auto

lemma fbind_funion: "fbind (M |∪| N) f = fbind M f |∪| fbind N f"
by transfer' auto

lemma ffUnion_least: "fBall A (λX. X |⊆| C)  ffUnion A |⊆| C"
by transfer blast

lemma fbind_iff: "x |∈| fbind S f  (s. x |∈| f s  s |∈| S)"
  by transfer' auto

lemma fBall_pred_weaken: "(x. x |∈| M  P x  Q x)  fBall M P  fBall M Q"
by auto

end

lemma fmmap_fmupd[simp]:
  "fmmap f (fmupd k v m) = fmupd k (f v) (fmmap f m)"
apply (rule fmap_ext)
by auto

definition fmlookup_default :: "('a, 'b) fmap  ('a  'b)  'a  'b" where
"fmlookup_default m f x = (case fmlookup m x of None  f x | Some b  b)"

end

Theory Find_First

theory Find_First
imports
  "HOL-Library.Finite_Map"
  "List-Index.List_Index"
begin

fun find_first :: "'a  'a list  nat option" where
"find_first _ [] = None" |
"find_first x (y # ys) = (if x = y then Some 0 else map_option Suc (find_first x ys))"

lemma find_first_correct:
  assumes "find_first x xs = Some i"
  shows "i < length xs" "xs ! i = x" "x  set (take i xs)"
using assms
proof (induction xs arbitrary: i)
  case (Cons y ys)
  { case 1 with Cons show ?case by (cases "x = y") auto }
  { case 2 with Cons show ?case by (cases "x = y") auto }
  { case 3 with Cons show ?case by (cases "x = y") auto }
qed auto

lemma find_first_none: "x  set xs  find_first x xs = None"
by (induct xs) auto

lemma find_first_some_strong:
  assumes "x  set (take n xs)" "n  length xs"
  obtains i where "find_first x xs = Some i" "i < n"
using assms
proof (induction xs arbitrary: thesis n)
  case (Cons y ys)
  show ?case
    proof (cases "x = y")
      case True
      show ?thesis
        proof (rule Cons.prems)
          show "find_first x (y # ys) = Some 0"
            unfolding x = y by simp
        next
          show "0 < n"
            using Cons by (metis length_pos_if_in_set length_take min.absorb2)
          qed
    next
      case False
      show ?thesis
        proof (rule Cons.IH)
          fix i
          assume "find_first x ys = Some i" "i < n - 1"
          with False have "find_first x (y # ys) = Some (Suc i)" "Suc i < n"
            using False by auto
          thus thesis
            using Cons by metis
        next
          show "x  set (take (n - 1) ys)"
            using Cons False by (metis empty_iff list.set(1) set_ConsD take_Cons')
        next
          show "n - 1  length ys"
            using Cons by (metis One_nat_def le_diff_conv list.size(4))
        qed
    qed
qed simp

lemma find_first_some:
  assumes "x  set xs"
  obtains i where "find_first x xs = Some i" "i < length xs"
using assms
by (metis order_refl take_all find_first_some_strong)

lemma find_first_some_index: "i < length xs  distinct xs  find_first (xs ! i) xs = Some i"
proof (induction xs arbitrary: i)
  case (Cons x xs)
  show ?case
    proof (cases "i = 0")
      case False
      have "find_first ((x # xs) ! i) (x # xs) = map_option Suc (Some (i - 1))"
        using Cons False by auto
      also have " = Some i"
        using False by auto
      finally show ?thesis .
    qed simp
qed auto

lemma find_first_append:
  "find_first x (ys @ zs) =
    (case find_first x ys of None  map_option (λi. i + length ys) (find_first x zs) | Some a  Some a)"
by (induct ys) (auto simp: option.map_comp comp_def map_option.identity split: option.splits)

lemma find_first_first:
  assumes "i < length xs" "x  set (take i xs)" "xs ! i = x"
  shows "find_first x xs = Some i"
proof -
  let ?ys = "take i xs"
  let ?zs = "drop i xs"

  have "?zs ! 0 = x"
    using assms by simp
  hence "find_first x ?zs = Some 0"
    using assms by (cases ?zs) auto
  moreover have "find_first x ?ys = None"
    using assms by (simp add: find_first_none)
  ultimately have "find_first x (?ys @ ?zs) = Some i"
    unfolding find_first_append
    using assms by simp
  thus ?thesis
    using assms by simp
qed

lemma find_first_prefix:
  assumes "find_first x xs = Some i" "i < n"
  shows "find_first x (take n xs) = Some i"
proof (rule find_first_first)
  show "i < length (take n xs)"
    using assms by (simp add: find_first_correct)
next
  have "x  set (take i xs)"
    using assms by (simp add: find_first_correct)
  with assms show "x  set (take i (take n xs))"
    by (simp add: min.absorb1)
next
  show "take n xs ! i = x"
    using assms by (simp add: find_first_correct)
qed

lemma find_first_later:
  assumes "i < length xs" "j < length xs" "i < j"
  assumes "xs ! i = x" "xs ! j = x"
  shows "find_first x xs  Some j"
proof (cases "x  set (take i xs)")
  case True
  then obtain k where "find_first x xs = Some k" "k < i"
    using assms by (auto elim: find_first_some_strong)
  thus ?thesis
    using assms by simp
next
  case False
  hence "find_first x xs = Some i"
    using assms by (simp add: find_first_first)
  thus ?thesis
    using assms by simp
qed

lemma find_first_in_map:
  assumes "length xs  length ys" "find_first n xs = Some i"
  shows "fmlookup (fmap_of_list (zip xs ys)) n = Some (ys ! i)"
using assms proof (induction xs arbitrary: ys i)
  case (Cons x xs)
  then obtain y ys' where "ys = y # ys'"
    by (metis Skolem_list_nth le_0_eq length_greater_0_conv less_nat_zero_code list.set_cases listrel_Cons1 listrel_iff_nth nth_mem)
  with Cons show ?case
    by (cases "x = n") auto
qed auto

fun common_prefix where
"common_prefix (x # xs) (y # ys) = (if x = y then x # common_prefix xs ys else [])" |
"common_prefix _ _ = []"

lemma common_prefix_find:
  assumes "z  set (common_prefix xs ys)"
  shows "find_first z xs = find_first z ys"
using assms
by (induct xs ys rule: common_prefix.induct) auto

lemma find_first_insert_nth_eq:
  assumes "n  length xs" "x  set (take n xs)"
  shows "find_first x (insert_nth n x xs) = Some n"
using assms
  by (auto simp: find_first_append find_first_none split: option.splits)

lemma insert_nth_induct:
  fixes P :: "nat  'a  'a list  bool"
    and a0 :: "nat"
    and a1 :: "'a"
    and a2 :: "'a list"
  assumes "x xs. P 0 x xs"
    and "n x y ys. P n x ys  P (Suc n) x (y # ys)"
    and "n x. P (Suc n) x []"
  shows "P a0 a1 a2"
using assms
apply induction_schema
apply pat_completeness
apply lexicographic_order
done

lemma find_first_insert_nth_neq:
  assumes "x  y"
  shows "find_first x (insert_nth n y xs) = map_option (λi. if i < n then i else Suc i) (find_first x xs)"
using assms
proof (induction n y xs rule: insert_nth_induct)
  case 2
  note insert_nth_take_drop[simp del]
  show ?case
    apply auto
    apply (subst 2)
    apply (rule 2)
    unfolding option.map_comp
    apply (rule option.map_cong0)
    by auto
qed auto

end

Theory Name

chapter ‹Names as a unique datatype›

theory Name
imports Main
begin

text ‹
  I would like to model names as @{typ string}s. Unfortunately, there is no default order on lists,
  as there could be multiple reasonable implementations: e.g.\ lexicographic and point-wise.
  For both choices, users can import the corresponding instantiation.

  In Isabelle, only at most one implementation of a given type class for a given type may be present
  in the same theory. Consequently, I avoided importing a list ordering from the library, because it
  may cause conflicts with users who use another ordering. The general approach for these situations
  is to introduce a type copy.

  The full flexibility of strings (i.e.\ string manipulations) is only required where fresh names
  are being produced. Otherwise, only a linear order on terms is needed. Conveniently, Sternagel and
  Thiemann @{cite sternagel2015deriving} provide tooling to automatically generate such a
  lexicographic order.
›

datatype name = Name (as_string: string)

― ‹Mostly copied from List_Lexorder›

instantiation name :: ord
begin

definition less_name where
"xs < ys  (as_string xs, as_string ys)  lexord {(u, v). (of_char u :: nat) < of_char v}"

definition less_eq_name where
"(xs :: name)  ys  xs < ys  xs = ys"

instance ..

end

instance name :: order
proof
  fix xs :: "name"
  show "xs  xs" by (simp add: less_eq_name_def)
next
  fix xs ys zs :: "name"
  assume "xs  ys" and "ys  zs"
  then show "xs  zs"
    apply (auto simp add: less_eq_name_def less_name_def)
    apply (rule lexord_trans)
    apply (auto intro: transI)
    done
next
  fix xs ys :: "name"
  assume "xs  ys" and "ys  xs"
  then show "xs = ys"
    apply (auto simp add: less_eq_name_def less_name_def)
    apply (rule lexord_irreflexive [THEN notE])
    defer
    apply (rule lexord_trans)
    apply (auto intro: transI)
    done
next
  fix xs ys :: "name"
  show "xs < ys  xs  ys  ¬ ys  xs"
    apply (auto simp add: less_name_def less_eq_name_def)
    defer
    apply (rule lexord_irreflexive [THEN notE])
    apply auto
    apply (rule lexord_irreflexive [THEN notE])
    defer
    apply (rule lexord_trans)
    apply (auto intro: transI)
    done
qed

instance name :: linorder
proof
  fix xs ys :: "name"
  have "(as_string xs, as_string ys)  lexord {(u, v). (of_char u::nat) < of_char v}  xs = ys  (as_string ys, as_string xs)  lexord {(u, v). (of_char u::nat) < of_char v}"
    by (metis (no_types, lifting) case_prodI lexord_linear linorder_neqE_nat mem_Collect_eq name.expand of_char_eq_iff)
  then show "xs  ys  ys  xs"
    by (auto simp add: less_eq_name_def less_name_def)
qed

lemma less_name_code[code]:
  "Name xs < Name []  False"
  "Name [] < Name (x # xs)  True"
  "Name (x # xs) < Name (y # ys)  (of_char x::nat) < of_char y  x = y  Name xs < Name ys"
unfolding less_name_def by auto

lemma le_name_code[code]:
  "Name (x # xs)  Name []  False"
  "Name []  Name (x # xs)  True"
  "Name (x # xs)  Name (y # ys)  (of_char x::nat) < of_char y  x = y  Name xs  Name ys"
unfolding less_eq_name_def less_name_def by auto

context begin

qualified definition append :: "name  name  name" where
"append v1 v2 = Name (as_string v1 @ as_string v2)"

lemma name_append_less:
  assumes "xs  Name []"
  shows "append ys xs > ys"
proof -
  have "Name (ys @ xs) > Name ys" if "xs  []" for xs ys
    using that
    proof (induction ys)
      case Nil
      thus ?case
        unfolding less_name_def
        by (cases xs) auto
    next
      case (Cons y ys)
      thus ?case
        unfolding less_name_def
        by auto
    qed
  with assms show ?thesis
    unfolding append_def
    by (cases xs, cases ys) auto
qed

end

end

Theory Fresh_Monad

chapter ‹A monad for generating fresh names›

theory Fresh_Monad
imports
  "HOL-Library.State_Monad"
  Term_Utils
begin

text ‹
  Generation of fresh names in general can be thought of as picking a string that is not an element
  of a (finite) set of already existing names. For Isabelle, the ‹Nominal› framework
  @{cite urban2008nominal and urban2013nominal} provides support for reasoning over fresh names, but
  unfortunately, its definitions are not executable.

  Instead, I chose to model generation of fresh names as a monad based on @{type state}. With this,
  it becomes possible to write programs using do›-notation. This is implemented abstractly as a
  @{command locale} that expects two operations:

   next› expects a value and generates a larger value, according to @{class linorder}
   arb› produces any value, similarly to @{const undefined}, but executable
›

locale fresh =
  fixes "next" :: "'a::linorder  'a" and arb :: 'a
  assumes next_ge: "next x > x"
begin

abbreviation update_next :: "('a, unit) state" where
"update_next  State_Monad.update next"

lemma update_next_strict_mono[simp, intro]: "strict_mono_state update_next"
using next_ge by (auto intro: update_strict_mono)

lemma update_next_mono[simp, intro]: "mono_state update_next"
by (rule strict_mono_implies_mono) (rule update_next_strict_mono)

definition create :: "('a, 'a) state" where
"create = update_next  (λ_. State_Monad.get)"

lemma create_alt_def[code]: "create = State (λa. (next a, next a))"
unfolding create_def State_Monad.update_def State_Monad.get_def State_Monad.set_def State_Monad.bind_def
by simp

abbreviation fresh_in :: "'a set  'a  bool" where
"fresh_in S s  Ball S ((≥) s)"

lemma next_ge_all: "finite S  fresh_in S s  next s  S"
by (metis antisym less_imp_le less_irrefl next_ge)

definition Next :: "'a set  'a" where
"Next S = (if S = {} then arb else next (Max S))"

lemma Next_ge_max: "finite S  S  {}  Next S > Max S"
unfolding Next_def using next_ge by simp

lemma Next_not_member_subset: "finite S'  S  S'  Next S'  S"
unfolding Next_def using next_ge
by (metis Max_ge Max_mono empty_iff finite_subset leD less_le_trans subset_empty)

lemma Next_not_member: "finite S  Next S  S"
by (rule Next_not_member_subset) auto

lemma Next_geq_not_member: "finite S  s  Next S  s  S"
unfolding Next_def using next_ge
by (metis (full_types) Max_ge all_not_in_conv leD le_less_trans)

lemma next_not_member: "finite S  s  Next S  next s  S"
by (meson Next_geq_not_member less_imp_le next_ge order_trans)

lemma create_mono[simp, intro]: "mono_state create"
unfolding create_def
by (auto intro: bind_mono_strong)

lemma create_strict_mono[simp, intro]: "strict_mono_state create"
unfolding create_def
by (rule bind_strict_mono_strong2) auto

abbreviation run_fresh where
"run_fresh m S  fst (run_state m (Next S))"

abbreviation fresh_fin :: "'a fset  'a  bool" where
"fresh_fin S s  fBall S ((≥) s)"

context includes fset.lifting begin

lemma next_ge_fall: "fresh_fin S s  next s |∉| S"
by (transfer fixing: "next") (rule next_ge_all)

lift_definition fNext :: "'a fset  'a" is Next .

lemma fNext_ge_max: "S  {||}  fNext S > fMax S"
by transfer (rule Next_ge_max)

lemma next_not_fmember: "s  fNext S  next s |∉| S"
by transfer (rule next_not_member)

lemma fNext_geq_not_member: "s  fNext S  s |∉| S"
by transfer (rule Next_geq_not_member)

lemma fNext_not_member: "fNext S |∉| S"
by transfer (rule Next_not_member)

lemma fNext_not_member_subset: "S |⊆| S'  fNext S' |∉| S"
by transfer (rule Next_not_member_subset)

abbreviation frun_fresh where
"frun_fresh m S  fst (run_state m (fNext S))"

end

end

end

Theory Fresh_Class

section ‹Fresh monad operations as class operations›

theory Fresh_Class
imports
  Fresh_Monad
  Name
begin

text ‹
  The @{const fresh} locale allows arbitrary instantiations. However, this may be inconvenient to
  use. The following class serves as a global instantiation that can be used without interpretation.
  The arb› parameter of the locale redirects to @{const default}.

  Some instantiations are provided. For @{typ name}s, underscores are appended to generate a fresh
  name.
›

class fresh = linorder + default +
  fixes "next" :: "'a  'a"
  assumes next_ge: "next x > x"

global_interpretation Fresh_Monad.fresh "next" default
  defines fresh_create = create
      and fresh_Next = Next
      and fresh_fNext = fNext
      and fresh_frun = frun_fresh
      and fresh_run = run_fresh
proof
  show "x < next x" for x by (rule next_ge)
qed

lemma [code]: "fresh_frun m S = fst (run_state m (fresh_fNext S))"
by (simp add: fresh_fNext_def fresh_frun_def)

lemma [code]: "fresh_run m S = fst (run_state m (fresh_Next S))"
by (simp add: fresh_Next_def fresh_run_def)

instantiation nat :: fresh begin

definition default_nat :: nat where
"default_nat = 0"

definition next_nat where
"next_nat = Suc"

instance
by intro_classes (auto simp: next_nat_def)

end

instantiation char :: default
begin

definition default_char :: char where
"default_char = CHR ''_''"

instance ..

end

instantiation name :: fresh begin

definition default_name where
"default_name = Name ''_''"

definition next_name where
"next_name xs = Name.append xs default"

instance proof
  fix v :: name
  show "v < next v"
    unfolding next_name_def default_name_def
    by (rule name_append_less) simp
qed

end

export_code
  fresh_create fresh_Next fresh_fNext fresh_frun fresh_run
  checking Scala? SML?

end

Theory Term_Class

chapter ‹Terms›

theory Term_Class
imports
  Datatype_Order_Generator.Order_Generator
  Name
  Term_Utils
  "HOL-Library.Disjoint_FSets"
begin

hide_type (open) "term"

section ‹A simple term type, modelled after Pure's term› type›

datatype "term" =
  Const name |
  Free name |
  Abs "term" ("Λ _" [71] 71) |
  Bound nat |
  App "term" "term" (infixl "$" 70)

derive linorder "term"

section ‹A type class describing terms›

text ‹
  The type class is split into two parts, ‹pre-terms› and ‹terms›. The only difference is that
  terms assume more axioms about substitution (see below).

  A term must provide the following generic constructors that behave like regular free constructors:

   const :: name ⇒ τ›
   free :: name ⇒ τ›
   app :: τ ⇒ τ ⇒ τ›

text ‹
  Conversely, there are also three corresponding destructors that could be defined in terms of
  Hilbert's choice operator. However, I have instead opted to let instances define destructors
  directly, which is simpler for execution purposes.

  Besides the generic constructors, terms may also contain other constructors. Those are abstractly
  called ‹abstractions›, even though that name is not entirely accurate (bound variables may also
  fall under this).

  Additionally, there must be operations that compute the list of all free variables (frees›),
  constants (consts›), and substitutions (subst›). Pre-terms only assume some basic properties of
  substitution on the generic constructors.

  Most importantly, substitution is not specified for environments containing terms with free
  variables. Term types are not required to implement α›-renaming to prevent capturing of
  variables.
›

class pre_term = size +
  fixes
    frees :: "'a  name fset" and
    subst :: "'a  (name, 'a) fmap  'a" and
    "consts" :: "'a  name fset"
  fixes
    app :: "'a  'a  'a" and unapp :: "'a  ('a × 'a) option"
  fixes
    const :: "name  'a" and unconst :: "'a  name option"
  fixes
    free :: "name  'a" and unfree :: "'a  name option"
  assumes unapp_app[simp]: "unapp (app u1 u2) = Some (u1, u2)"
  assumes app_unapp[dest]: "unapp u = Some (u1, u2)  u = app u1 u2"
  assumes app_size[simp]: "size (app u1 u2) = size u1 + size u2 + 1"
  assumes unconst_const[simp]: "unconst (const name) = Some name"
  assumes const_unconst[dest]: "unconst u = Some name  u = const name"
  assumes unfree_free[simp]: "unfree (free name) = Some name"
  assumes free_unfree[dest]: "unfree u = Some name  u = free name"
  assumes app_const_distinct: "app u1 u2  const name"
  assumes app_free_distinct: "app u1 u2  free name"
  assumes free_const_distinct: "free name1  const name2"
  assumes frees_const[simp]: "frees (const name) = fempty"
  assumes frees_free[simp]: "frees (free name) = {| name |}"
  assumes frees_app[simp]: "frees (app u1 u2) = frees u1 |∪| frees u2"
  assumes consts_free[simp]: "consts (free name) = fempty"
  assumes consts_const[simp]: "consts (const name) = {| name |}"
  assumes consts_app[simp]: "consts (app u1 u2) = consts u1 |∪| consts u2"
  assumes subst_app[simp]: "subst (app u1 u2) env = app (subst u1 env) (subst u2 env)"
  assumes subst_const[simp]: "subst (const name) env = const name"
  assumes subst_free[simp]: "subst (free name) env = (case fmlookup env name of Some t  t | _  free name)"
  assumes free_inject: "free name1 = free name2  name1 = name2"
  assumes const_inject: "const name1 = const name2  name1 = name2"
  assumes app_inject: "app u1 u2 = app u3 u4  u1 = u3  u2 = u4"

instantiation "term" :: pre_term begin

definition app_term where
"app_term t u = t $ u"

fun unapp_term where
"unapp_term (t $ u) = Some (t, u)" |
"unapp_term _ = None"

definition const_term where
"const_term = Const"

fun unconst_term where
"unconst_term (Const name) = Some name" |
"unconst_term _ = None"

definition free_term where
"free_term = Free"

fun unfree_term where
"unfree_term (Free name) = Some name" |
"unfree_term _ = None"

fun frees_term :: "term  name fset" where
"frees_term (Free x) = {| x |}" |
"frees_term (t1 $ t2) = frees_term t1 |∪| frees_term t2" |
"frees_term (Λ t) = frees_term t" |
"frees_term _ = {||}"

fun subst_term :: "term  (name, term) fmap  term" where
"subst_term (Free s) env = (case fmlookup env s of Some t  t | None  Free s)" |
"subst_term (t1 $ t2) env = subst_term t1 env $ subst_term t2 env" |
"subst_term (Λ t) env = Λ subst_term t env" |
"subst_term t env = t"

fun consts_term :: "term  name fset" where
"consts_term (Const x) = {| x |}" |
"consts_term (t1 $ t2) = consts_term t1 |∪| consts_term t2" |
"consts_term (Λ t) = consts_term t" |
"consts_term _ = {||}"

instance
  by standard
      (auto
        simp: app_term_def const_term_def free_term_def
        elim: unapp_term.elims unconst_term.elims unfree_term.elims
        split: option.splits)

end

context pre_term begin

definition freess :: "'a list  name fset" where
"freess = ffUnion  fset_of_list  map frees"

lemma freess_cons[simp]: "freess (x # xs) = frees x |∪| freess xs"
unfolding freess_def by simp

lemma freess_single: "freess [x] = frees x"
unfolding freess_def by simp

lemma freess_empty[simp]: "freess [] = {||}"
unfolding freess_def by simp

lemma freess_app[simp]: "freess (xs @ ys) = freess xs |∪| freess ys"
unfolding freess_def by simp

lemma freess_subset: "set xs  set ys  freess xs |⊆| freess ys"
unfolding freess_def comp_apply
by (intro ffunion_mono fset_of_list_subset) auto

abbreviation id_env :: "(name, 'a) fmap  bool" where
"id_env  fmpred (λx y. y = free x)"

definition closed_except :: "'a  name fset  bool" where
"closed_except t S  frees t |⊆| S"

abbreviation closed :: "'a  bool" where
"closed t  closed_except t {||}"

lemmas term_inject = free_inject const_inject app_inject

lemmas term_distinct[simp] =
  app_const_distinct app_const_distinct[symmetric]
  app_free_distinct app_free_distinct[symmetric]
  free_const_distinct free_const_distinct[symmetric]

lemma app_size1: "size u1 < size (app u1 u2)"
by simp

lemma app_size2: "size u2 < size (app u1 u2)"
by simp

lemma unx_some_lemmas:
  "unapp u = Some x  unconst u = None"
  "unapp u = Some x  unfree u = None"
  "unconst u = Some y  unapp u = None"
  "unconst u = Some y  unfree u = None"
  "unfree u = Some z  unconst u = None"
  "unfree u = Some z  unapp u = None"
subgoal by (metis app_unapp const_unconst app_const_distinct not_None_eq surj_pair)
subgoal by (metis app_free_distinct app_unapp free_unfree option.exhaust surj_pair)
subgoal by (metis app_unapp const_unconst app_const_distinct old.prod.exhaust option.distinct(1) option.expand option.sel)
subgoal by (metis const_unconst free_const_distinct free_unfree option.exhaust)
subgoal by (metis const_unconst free_const_distinct free_unfree option.exhaust)
subgoal by (metis app_free_distinct app_unapp free_unfree not_Some_eq surj_pair)
done

lemma unx_none_simps[simp]:
  "unapp (const name) = None"
  "unapp (free name) = None"
  "unconst (app t u) = None"
  "unconst (free name) = None"
  "unfree (const name) = None"
  "unfree (app t u) = None"
subgoal by (metis app_unapp app_const_distinct not_None_eq surj_pair)
subgoal by (metis app_free_distinct app_unapp option.exhaust surj_pair)
subgoal by (metis const_unconst app_const_distinct option.distinct(1) option.expand option.sel)
subgoal by (metis const_unconst free_const_distinct option.exhaust)
subgoal by (metis free_const_distinct free_unfree option.exhaust)
subgoal by (metis app_free_distinct free_unfree not_Some_eq)
done

lemma term_cases:
  obtains (free) name where "t = free name"
        | (const) name where "t = const name"
        | (app) u1 u2 where "t = app u1 u2"
        | (other) "unfree t = None" "unapp t = None" "unconst t = None"
apply (cases "unfree t")
apply (cases "unconst t")
apply (cases "unapp t")
subgoal by auto
subgoal for x by (cases x) auto
subgoal by auto
subgoal by auto
done

definition is_const where
"is_const t  (unconst t  None)"

definition const_name where
"const_name t = (case unconst t of Some name  name)"

lemma is_const_simps[simp]:
  "is_const (const name)"
  "¬ is_const (app t u)"
  "¬ is_const (free name)"
unfolding is_const_def by simp+

lemma const_name_simps[simp]:
  "const_name (const name) = name"
  "is_const t  const (const_name t) = t"
unfolding const_name_def is_const_def by auto

definition is_free where
"is_free t  (unfree t  None)"

definition free_name where
"free_name t = (case unfree t of Some name  name)"

lemma is_free_simps[simp]:
  "is_free (free name)"
  "¬ is_free (const name)"
  "¬ is_free (app t u)"
unfolding is_free_def by simp+

lemma free_name_simps[simp]:
  "free_name (free name) = name"
  "is_free t  free (free_name t) = t"
unfolding free_name_def is_free_def by auto

definition is_app where
"is_app t  (unapp t  None)"

definition left where
"left t = (case unapp t of Some (l, _)  l)"

definition right where
"right t = (case unapp t of Some (_, r)  r)"

lemma app_simps[simp]:
  "¬ is_app (const name)"
  "¬ is_app (free name)"
  "is_app (app t u)"
unfolding is_app_def by simp+

lemma left_right_simps[simp]:
  "left (app l r) = l"
  "right (app l r) = r"
  "is_app t  app (left t) (right t) = t"
unfolding is_app_def left_def right_def by auto

definition ids :: "'a  name fset" where
"ids t = frees t |∪| consts t"

lemma closed_except_const[simp]: "closed_except (const name) S"
unfolding closed_except_def by auto

abbreviation closed_env :: "(name, 'a) fmap  bool" where
"closed_env  fmpred (λ_. closed)"

lemma closed_except_self: "closed_except t (frees t)"
unfolding closed_except_def by simp

end

class "term" = pre_term + size +
  fixes
    abs_pred :: "('a  bool)  'a  bool"
  assumes
    raw_induct[case_names const free app abs]:
      "(name. P (const name)) 
        (name. P (free name)) 
        (t1 t2. P t1  P t2  P (app t1 t2)) 
        (t. abs_pred P t) 
        P t"
  assumes
    raw_subst_id: "abs_pred (λt. env. id_env env  subst t env = t) t" and
    raw_subst_drop: "abs_pred (λt. x |∉| frees t  (env. subst t (fmdrop x env) = subst t env)) t" and
    raw_subst_indep: "abs_pred (λt. env1 env2. closed_env env2  fdisjnt (fmdom env1) (fmdom env2)  subst t (env1 ++f env2) = subst (subst t env2) env1) t" and
    raw_subst_frees: "abs_pred (λt. env. closed_env env  frees (subst t env) = frees t |-| fmdom env) t" and
    raw_subst_consts': "abs_pred (λa. x. consts (subst a x) = consts a |∪| ffUnion (consts |`| fmimage x (frees a))) t" and
    abs_pred_trivI: "P t  abs_pred P t"
begin

lemma subst_id: "id_env env  subst t env = t"
proof (induction t arbitrary: env rule: raw_induct)
  case (abs t)
  show ?case
    by (rule raw_subst_id)
qed (auto split: option.splits)

lemma subst_drop: "x |∉| frees t  subst t (fmdrop x env) = subst t env"
proof (induction t arbitrary: env rule: raw_induct)
  case (abs t)
  show ?case
    by (rule raw_subst_drop)
qed (auto split: option.splits)

lemma subst_frees: "fmpred (λ_. closed) env  frees (subst t env) = frees t |-| fmdom env"
proof (induction t arbitrary: env rule: raw_induct)
  case (abs t)
  show ?case
    by (rule raw_subst_frees)
qed (auto split: option.splits simp: closed_except_def)

lemma subst_consts': "consts (subst t env) = consts t |∪| ffUnion (consts |`| fmimage env (frees t))"
proof (induction t arbitrary: env rule: raw_induct)
  case (free name)
  then show ?case
    by (auto
          split: option.splits
          simp: ffUnion_alt_def fmlookup_ran_iff fmlookup_image_iff fmlookup_dom_iff
          intro!: fBexI)
next
  case (abs t)
  show ?case
    by (rule raw_subst_consts')
qed (auto simp: funion_image_bind_eq finter_funion_distrib fbind_funion)

fun match :: "term  'a  (name, 'a) fmap option" where
"match (t1 $ t2) u = do {
  (u1, u2)  unapp u;
  env1  match t1 u1;
  env2  match t2 u2;
  Some (env1 ++f env2)
}" |
"match (Const name) u =
  (case unconst u of
    None  None
  | Some name'  if name = name' then Some fmempty else None)" |
"match (Free name) u = Some (fmap_of_list [(name, u)])" |
"match (Bound n) u = None" |
"match (Abs t) u = None"

lemma match_simps[simp]:
  "match (t1 $ t2) (app u1 u2) = do {
    env1  match t1 u1;
    env2  match t2 u2;
    Some (env1 ++f env2)
  }"
  "match (Const name) (const name') = (if name = name' then Some fmempty else None)"
by auto

lemma match_some_induct[consumes 1, case_names app const free]:
  assumes "match t u = Some env"
  assumes "t1 t2 u1 u2 env1 env2. P t1 u1 env1  match t1 u1 = Some env1  P t2 u2 env2  match t2 u2 = Some env2  P (t1 $ t2) (app u1 u2) (env1 ++f env2)"
  assumes "name. P (Const name) (const name) fmempty"
  assumes "name u. P (Free name) u (fmupd name u fmempty)"
  shows "P t u env"
using assms
by (induction t u arbitrary: env rule: match.induct)
   (auto split: option.splits if_splits elim!: option_bindE)

lemma match_dom: "match p t = Some env  fmdom env = frees p"
by (induction p arbitrary: t env)
   (fastforce split: option.splits if_splits elim: option_bindE)+

lemma match_vars: "match p t = Some env  fmpred (λ_ u. frees u |⊆| frees t) env"
proof (induction p t env rule: match_some_induct)
  case (app t1 t2 u1 u2 env1 env2)
  show ?case
    apply rule
    using app
    by (fastforce intro: fmpred_mono_strong)+
qed auto

lemma match_appE_split:
  assumes "match (t1 $ t2) u = Some env"
  obtains u1 u2 env1 env2 where
    "u = app u1 u2" "match t1 u1 = Some env1" "match t2 u2 = Some env2" "env = env1 ++f env2"
using assms
by (auto split: option.splits elim!: option_bindE)

lemma subst_consts:
  assumes "consts t |⊆| S" "fmpred (λ_ u. consts u |⊆| S) env"
  shows "consts (subst t env) |⊆| S"
apply (subst subst_consts')
using assms by (auto intro!: ffUnion_least)

lemma subst_empty[simp]: "subst t fmempty = t"
by (auto simp: subst_id)

lemma subst_drop_fset: "fdisjnt S (frees t)  subst t (fmdrop_fset S env) = subst t env"
by (induct S) (auto simp: subst_drop fdisjnt_alt_def)

lemma subst_restrict:
  assumes "frees t |⊆| M"
  shows "subst t (fmrestrict_fset M env) = subst t env"
proof -
  have *: "fmrestrict_fset M env = fmdrop_fset (fmdom env - M) env"
    by (rule fmap_ext) auto

  show ?thesis
    apply (subst *)
    apply (subst subst_drop_fset)
    unfolding fdisjnt_alt_def
    using assms by auto
qed

corollary subst_restrict'[simp]: "subst t (fmrestrict_fset (frees t) env) = subst t env"
by (simp add: subst_restrict)

corollary subst_cong:
  assumes "x. x |∈| frees t  fmlookup Γ1 x = fmlookup Γ2 x"
  shows "subst t Γ1 = subst t Γ2"
proof -
  have "fmrestrict_fset (frees t) Γ1 = fmrestrict_fset (frees t) Γ2"
    apply (rule fmap_ext)
    using assms by simp
  thus ?thesis
    by (metis subst_restrict')
qed

corollary subst_add_disjnt:
  assumes "fdisjnt (frees t) (fmdom env1)"
  shows "subst t (env1 ++f env2) = subst t env2"
proof -
  have "subst t (env1 ++f env2) = subst t (fmrestrict_fset (frees t) (env1 ++f env2))"
    by (metis subst_restrict')
  also have " = subst t (fmrestrict_fset (frees t) env1 ++f fmrestrict_fset (frees t) env2)"
    by simp
  also have " = subst t (fmempty ++f fmrestrict_fset (frees t) env2)"
    unfolding fmfilter_alt_defs
    apply (subst fmfilter_false)
    using assms
    by (auto simp: fdisjnt_alt_def intro: fmdomI)
  also have " = subst t (fmrestrict_fset (frees t) env2)"
    by simp
  also have " = subst t env2"
    by simp
  finally show ?thesis .
qed

corollary subst_add_shadowed_env:
  assumes "frees t |⊆| fmdom env2"
  shows "subst t (env1 ++f env2) = subst t env2"
proof -
  have "subst t (env1 ++f env2) = subst t (fmdrop_fset (fmdom env2) env1 ++f env2)"
    by (subst fmadd_drop_left_dom) rule
  also have " = subst t (fmrestrict_fset (frees t) (fmdrop_fset (fmdom env2) env1 ++f env2))"
    by (metis subst_restrict')
  also have " = subst t (fmrestrict_fset (frees t) (fmdrop_fset (fmdom env2) env1) ++f fmrestrict_fset (frees t) env2)"
    by simp
  also have " = subst t (fmempty ++f fmrestrict_fset (frees t) env2)"
    unfolding fmfilter_alt_defs
    using fsubsetD[OF assms]
    by auto
  also have " = subst t env2"
    by simp
  finally show ?thesis .
qed

corollary subst_restrict_closed: "closed_except t S  subst t (fmrestrict_fset S env) = subst t env"
by (metis subst_restrict closed_except_def)

lemma subst_closed_except_id:
  assumes "closed_except t S" "fdisjnt (fmdom env) S"
  shows "subst t env = t"
using assms
by (metis fdisjnt_subset_right fmdom_drop_fset fminus_cancel fmrestrict_fset_dom
          fmrestrict_fset_null closed_except_def subst_drop_fset subst_empty)

lemma subst_closed_except_preserved:
  assumes "closed_except t S" "fdisjnt (fmdom env) S"
  shows "closed_except (subst t env) S"
using assms
by (metis subst_closed_except_id)

corollary subst_closed_id: "closed t  subst t env = t"
by (simp add: subst_closed_except_id fdisjnt_alt_def)

corollary subst_closed_preserved: "closed t  closed (subst t env)"
by (simp add: subst_closed_except_preserved fdisjnt_alt_def)


context begin

private lemma subst_indep0:
  assumes "closed_env env2" "fdisjnt (fmdom env1) (fmdom env2)"
  shows "subst t (env1 ++f env2) = subst (subst t env2) env1"
using assms proof (induction t arbitrary: env1 env2 rule: raw_induct)
  case (free name)
  show ?case
    using ‹closed_env env2
    by (cases rule: fmpred_cases[where x = name]) (auto simp: subst_closed_id)
next
  case (abs t)
  show ?case
    by (rule raw_subst_indep)
qed auto

lemma subst_indep:
  assumes "closed_env Γ'"
  shows "subst t (Γ ++f Γ') = subst (subst t Γ') Γ"
proof -
  have "subst t (Γ ++f Γ') = subst t (fmrestrict_fset (frees t) (Γ ++f Γ'))"
    by (metis subst_restrict')
  also have " = subst t (fmrestrict_fset (frees t) Γ ++f Γ')"
    by (smt fmlookup_add fmlookup_restrict_fset subst_cong)
  also have " = subst t (fmrestrict_fset (frees t |-| fmdom Γ') Γ ++f Γ')"
    by (rule subst_cong) (simp add: fmfilter_alt_defs(5))
  also have " = subst (subst t Γ') (fmrestrict_fset (frees t |-| fmdom Γ') Γ)"
    apply (rule subst_indep0[OF assms])
    using fmdom_restrict_fset
    unfolding fdisjnt_alt_def
    by auto
  also have " = subst (subst t Γ') (fmrestrict_fset (frees (subst t Γ')) Γ)"
    using assms by (auto simp: subst_frees)
  also have " = subst (subst t Γ') Γ"
    by simp
  finally show ?thesis .
qed

lemma subst_indep':
  assumes "closed_env Γ'" "fdisjnt (fmdom Γ') (fmdom Γ)"
  shows "subst t (Γ' ++f Γ) = subst (subst t Γ') Γ"
using assms by (metis subst_indep fmadd_disjnt)

lemma subst_twice:
  assumes "Γ' f Γ" "closed_env Γ'"
  shows "subst (subst t Γ') Γ = subst t Γ"
proof -
  have "subst (subst t Γ') Γ = subst t (Γ ++f Γ')"
    apply (rule subst_indep[symmetric])
    apply fact
    done
  also have " = subst t Γ"
    apply (rule subst_cong)
    using Γ' f Γ unfolding fmsubset_alt_def
    by fastforce
  finally show ?thesis .
qed

end

fun matchs :: "term list  'a list  (name, 'a) fmap option" where
"matchs [] [] = Some fmempty" |
"matchs (t # ts) (u # us) = do { env1  match t u; env2  matchs ts us; Some (env1 ++f env2) }" |
"matchs _ _ = None"

lemmas matchs_induct = matchs.induct[case_names empty cons]

context begin

private lemma matchs_alt_def0:
  assumes "length ps = length vs"
  shows "map_option (λenv. m ++f env) (matchs ps vs) = map_option (foldl (++f) m) (those (map2 match ps vs))"
using assms proof (induction arbitrary: m rule: list_induct2)
  case (Cons x xs y ys)
  show ?case
    proof (cases "match x y")
      case x_y: Some
      show ?thesis
        proof (cases "matchs xs ys")
          case None
          with x_y Cons show ?thesis
            by simp
        next
          case Some
          with x_y show ?thesis
            apply simp
            using Cons(2) apply simp
            apply (subst option.map_comp)
            by (auto cong: map_option_cong)
        qed
    qed simp
qed simp

lemma matchs_alt_def:
  assumes "length ps = length vs"
  shows "matchs ps vs = map_option (foldl (++f) fmempty) (those (map2 match ps vs))"
by (subst matchs_alt_def0[where m = fmempty, simplified, symmetric, OF assms])
   (simp add: option.map_ident)

end

lemma matchs_neq_length_none[simp]: "length xs  length ys  matchs xs ys = None"
by (induct xs ys rule: matchs.induct) fastforce+

corollary matchs_some_eq_length: "matchs xs ys = Some env  length xs = length ys"
by (metis option.distinct(1) matchs_neq_length_none)

lemma matchs_app[simp]:
  assumes "length xs2 = length ys2"
  shows "matchs (xs1 @ xs2) (ys1 @ ys2) =
          matchs xs1 ys1  (λenv1. matchs xs2 ys2  (λenv2. Some (env1 ++f env2)))"
using assms
by (induct xs1 ys1 rule: matchs.induct) fastforce+

corollary matchs_appI:
  assumes "matchs xs ys = Some env1" "matchs xs' ys' = Some env2"
  shows "matchs (xs @ xs') (ys @ ys') = Some (env1 ++f env2)"
using assms
by (metis (no_types, lifting) Option.bind_lunit matchs_app matchs_some_eq_length)

corollary matchs_dom:
  assumes "matchs ps ts = Some env"
  shows "fmdom env = freess ps"
using assms
by (induction ps ts arbitrary: env rule: matchs_induct)
   (auto simp: match_dom elim!: option_bindE)

fun find_match :: "(term × 'a) list  'a  ((name, 'a) fmap × term × 'a) option" where
"find_match [] _ = None" |
"find_match ((pat, rhs) # cs) t =
  (case match pat t of
    Some env  Some (env, pat, rhs)
  | None  find_match cs t)"

lemma find_match_map:
  "find_match (map (λ(pat, t). (pat, f pat t)) cs) t =
    map_option (λ(env, pat, rhs). (env, pat, f pat rhs)) (find_match cs t)"
by (induct cs) (auto split: option.splits)

lemma find_match_elem:
  assumes "find_match cs t = Some (env, pat, rhs)"
  shows "(pat, rhs)  set cs" "match pat t = Some env"
using assms
by (induct cs) (auto split: option.splits)

lemma match_subst_closed:
  assumes "match pat t = Some env" "closed_except rhs (frees pat)" "closed t"
  shows "closed (subst rhs env)"
using assms
by (smt fminusE fmpred_iff fset_mp fsubsetI closed_except_def match_vars match_dom subst_frees)

fun rewrite_step :: "(term × 'a)  'a  'a option" where
"rewrite_step (t1, t2) u = map_option (subst t2) (match t1 u)"

abbreviation rewrite_step' :: "(term × 'a)  'a  'a  bool" ("_/ / _ / _" [50,0,50] 50) where
"r  t  u  rewrite_step r t = Some u"

lemma rewrite_step_closed:
  assumes "frees t2 |⊆| frees t1" "(t1, t2)  u  u'" "closed u"
  shows "closed u'"
proof -
  from assms obtain env where *: "match t1 u = Some env"
    by auto
  then have "closed (subst t2 env)"
    apply (rule match_subst_closed[where pat = t1 and t = u])
    using assms unfolding closed_except_def by auto
  with * show ?thesis
    using assms by auto
qed

definition matches :: "'a  'a  bool" (infix "" 50) where
"t  u  (env. subst t env = u)"

lemma matchesI[intro]: "subst t env = u  t  u"
unfolding matches_def by auto

lemma matchesE[elim]:
  assumes "t  u"
  obtains env where "subst t env = u"
using assms unfolding matches_def by blast

definition overlapping :: "'a  'a  bool" where
"overlapping s t  (u. s  u  t  u)"

lemma overlapping_refl: "overlapping t t"
unfolding overlapping_def matches_def by blast

lemma overlapping_sym: "overlapping t u  overlapping u t"
unfolding overlapping_def by auto

lemma overlappingI[intro]: "s  u  t  u  overlapping s t"
unfolding overlapping_def by auto

lemma overlappingE[elim]:
  assumes "overlapping s t"
  obtains u where "s  u" "t  u"
using assms unfolding overlapping_def by blast

abbreviation "non_overlapping s t  ¬ overlapping s t"

corollary non_overlapping_implies_neq: "non_overlapping t u  t  u"
by (metis overlapping_refl)

end

inductive rewrite_first :: "(term × 'a::term) list  'a  'a  bool" where
match: "match pat t = Some env  rewrite_first ((pat, rhs) # _) t (subst rhs env)" |
nomatch: "match pat t = None  rewrite_first cs t t'  rewrite_first ((pat, _) # cs) t t'"

code_pred (modes: i ⇒ i ⇒ o ⇒ bool) rewrite_first .

lemma rewrite_firstE:
  assumes "rewrite_first cs t t'"
  obtains pat rhs env where "(pat, rhs)  set cs" "match pat t = Some env" "t' = subst rhs env"
using assms by induction auto

text ‹
  This doesn't follow from @{thm [source] find_match_elem}, because @{const rewrite_first} requires
  the first match, not just any.
›

lemma find_match_rewrite_first:
  assumes "find_match cs t = Some (env, pat, rhs)"
  shows "rewrite_first cs t (subst rhs env)"
using assms proof (induction cs)
  case (Cons c cs)
  obtain pat0 rhs0 where "c = (pat0, rhs0)"
    by fastforce
  thus ?case
    using Cons
    by (cases "match pat0 t") (auto intro: rewrite_first.intros)
qed simp

definition term_cases :: "(name  'b)  (name  'b)  ('a  'a  'b)  'b  'a::term  'b" where
"term_cases if_const if_free if_app otherwise t =
  (case unconst t of
    Some name  if_const name |
    None  (case unfree t of
      Some name  if_free name |
      None 
        (case unapp t of
          Some (t, u)  if_app t u
        | None  otherwise)))"

lemma term_cases_cong[fundef_cong]:
  assumes "t = u" "otherwise1 = otherwise2"
  assumes "(name. t = const name  if_const1 name = if_const2 name)"
  assumes "(name. t = free name  if_free1 name = if_free2 name)"
  assumes "(u1 u2. t = app u1 u2  if_app1 u1 u2 = if_app2 u1 u2)"
  shows "term_cases if_const1 if_free1 if_app1 otherwise1 t = term_cases if_const2 if_free2 if_app2 otherwise2 u"
using assms
unfolding term_cases_def
by (auto split: option.splits)

lemma term_cases[simp]:
  "term_cases if_const if_free if_app otherwise (const name) = if_const name"
  "term_cases if_const if_free if_app otherwise (free name) = if_free name"
  "term_cases if_const if_free if_app otherwise (app t u) = if_app t u"
unfolding term_cases_def
by (auto split: option.splits)

lemma term_cases_template:
  assumes "x. f x = term_cases if_const if_free if_app otherwise x"
  shows "f (const name) = if_const name"
    and "f (free name) = if_free name"
    and "f (app t u) = if_app t u"
unfolding assms by (rule term_cases)+

context "term" begin

function (sequential) strip_comb :: "'a  'a × 'a list" where
[simp del]: "strip_comb t =
  (case unapp t of
    Some (t, u) 
      (let (f, args) = strip_comb t in (f, args @ [u]))
  | None  (t, []))"
by pat_completeness auto

(* FIXME why is this not automatic? *)
termination
  apply (relation "measure size")
  apply rule
  apply auto
  done

lemma strip_comb_simps[simp]:
  "strip_comb (app t u) = (let (f, args) = strip_comb t in (f, args @ [u]))"
  "unapp t = None  strip_comb t = (t, [])"
by (subst strip_comb.simps; auto)+

lemma strip_comb_induct[case_names app no_app]:
  assumes "x y. P x  P (app x y)"
  assumes "t. unapp t = None  P t"
  shows "P t"
proof (rule strip_comb.induct, goal_cases)
  case (1 t)
  show ?case
    proof (cases "unapp t")
      case None
      with assms show ?thesis by metis
    next
      case (Some a)
      then show ?thesis
        apply (cases a)
        using 1 assms by auto
    qed
qed

lemma strip_comb_size: "t'  set (snd (strip_comb t))  size t' < size t"
by (induction t rule: strip_comb_induct) (auto split: prod.splits)

lemma sstrip_comb_termination[termination_simp]:
  "(f, ts) = strip_comb t  t'  set ts  size t' < size t"
by (metis snd_conv strip_comb_size)

lemma strip_comb_empty: "snd (strip_comb t) = []  fst (strip_comb t) = t"
by (induction t rule: strip_comb_induct) (auto split: prod.splits)

lemma strip_comb_app: "fst (strip_comb (app t u)) = fst (strip_comb t)"
by (simp split: prod.splits)

primrec list_comb :: "'a  'a list  'a" where
"list_comb f [] = f" |
"list_comb f (t # ts) = list_comb (app f t) ts"

lemma list_comb_app[simp]: "list_comb f (xs @ ys) = list_comb (list_comb f xs) ys"
by (induct xs arbitrary: f) auto

corollary list_comb_snoc: "app (list_comb f xs) y = list_comb f (xs @ [y])"
by simp

lemma list_comb_size[simp]: "size (list_comb f xs) = size f + size_list size xs"
by (induct xs arbitrary: f) auto

lemma subst_list_comb: "subst (list_comb f xs) env = list_comb (subst f env) (map (λt. subst t env) xs)"
by (induct xs arbitrary: f) auto

abbreviation const_list_comb :: "name  'a list  'a" (infixl "$$" 70) where
"const_list_comb name  list_comb (const name)"

lemma list_strip_comb[simp]: "list_comb (fst (strip_comb t)) (snd (strip_comb t)) = t"
by (induction t rule: strip_comb_induct) (auto split: prod.splits)

lemma strip_list_comb: "strip_comb (list_comb f ys) = (fst (strip_comb f), snd (strip_comb f) @ ys)"
by (induct ys arbitrary: f) (auto simp: split_beta)

lemma strip_list_comb_const: "strip_comb (name $$ xs) = (const name, xs)"
by (simp add: strip_list_comb)

lemma frees_list_comb[simp]: "frees (list_comb t xs) = frees t |∪| freess xs"
by (induct xs arbitrary: t) (auto simp: freess_def)

lemma consts_list_comb: "consts (list_comb f xs) = consts f |∪| ffUnion (fset_of_list (map consts xs))"
by (induct xs arbitrary: f) auto

lemma ids_list_comb: "ids (list_comb f xs) = ids f |∪| ffUnion (fset_of_list (map ids xs))"
unfolding ids_def frees_list_comb consts_list_comb freess_def
apply auto
apply (smt fbind_iff finsert_absorb finsert_fsubset funion_image_bind_eq inf_sup_ord(3))
apply (metis fbind_iff funionCI funion_image_bind_eq)
by (smt fbind_iff funionE funion_image_bind_eq)

lemma frees_strip_comb: "frees t = frees (fst (strip_comb t)) |∪| freess (snd (strip_comb t))"
by (metis list_strip_comb frees_list_comb)

lemma list_comb_cases':
  obtains (app) "is_app (list_comb f xs)"
        | (empty) "list_comb f xs = f" "xs = []"
by (induction xs arbitrary: f) auto

(* FIXME case names? *)
lemma list_comb_cases[consumes 1]:
  assumes "t = list_comb f xs"
  obtains (head) "t = f" "xs = []"
        | (app) u v where "t = app u v"
using assms by (metis list_comb_cases' left_right_simps(3))

end

fun left_nesting :: "'a::term  nat" where
[simp del]: "left_nesting t = term_cases (λ_. 0) (λ_. 0) (λt u. Suc (left_nesting t)) 0 t"

lemmas left_nesting_simps[simp] = term_cases_template[OF left_nesting.simps]

lemma list_comb_nesting[simp]: "left_nesting (list_comb f xs) = left_nesting f + length xs"
by (induct xs arbitrary: f) auto

lemma list_comb_cond_inj:
  assumes "list_comb f xs = list_comb g ys" "left_nesting f = left_nesting g"
  shows "xs = ys" "f = g"
using assms proof (induction xs arbitrary: f g ys)
  case Nil
  fix f g :: 'a
  fix ys
  assume prems: "list_comb f [] = list_comb g ys" "left_nesting f = left_nesting g"

  hence "left_nesting f = left_nesting g + length ys"
    by simp
  with prems show "[] = ys" "f = g"
    by simp+
next
  case (Cons x xs)
  fix f g ys
  assume prems: "list_comb f (x # xs) = list_comb g ys" "left_nesting f = left_nesting g"

  hence "left_nesting (list_comb f (x # xs)) = left_nesting (list_comb g ys)"
    by simp
  hence "Suc (left_nesting f + length xs) = left_nesting g + length ys"
    by simp
  with prems have "length ys = Suc (length xs)"
    by linarith
  then obtain z zs where "ys = z # zs"
    by (metis length_Suc_conv)

  thus "x # xs = ys" "f = g"
    using prems Cons[where ys = zs and f = "app f x" and g = "app g z"]
    by (auto dest: app_inject)
qed

lemma list_comb_inj_second: "inj (list_comb f)"
by (metis injI list_comb_cond_inj)

lemma list_comb_semi_inj:
  assumes "length xs = length ys"
  assumes "list_comb f xs = list_comb g ys"
  shows "xs = ys" "f = g"
proof -
  from assms have "left_nesting (list_comb f xs) = left_nesting (list_comb g ys)"
    by simp
  with assms have "left_nesting f = left_nesting g"
    unfolding list_comb_nesting by simp
  with assms show "xs = ys" "f = g"
    by (metis list_comb_cond_inj)+
qed

fun no_abs :: "'a::term  bool" where
[simp del]: "no_abs t = term_cases (λ_. True) (λ_. True) (λt u. no_abs t  no_abs u) False t"

lemmas no_abs_simps[simp] = term_cases_template[OF no_abs.simps]

lemma no_abs_induct[consumes 1, case_names free const app, induct pred: no_abs]:
  assumes "no_abs t"
  assumes "name. P (free name)"
  assumes "name. P (const name)"
  assumes "t1 t2. P t1  no_abs t1  P t2  no_abs t2  P (app t1 t2)"
  shows "P t"
using assms(1) proof (induction rule: no_abs.induct)
  case (1 t)
  show ?case
    proof (cases rule: pre_term_class.term_cases[where t = t])
      case (free name)
      then show ?thesis
        using assms by auto
    next
      case (const name)
      then show ?thesis
        using assms by auto
    next
      case (app u1 u2)
      with assms have "P u1" "P u2"
        using 1 by auto
      with assms ‹no_abs t show ?thesis
        unfolding t = _ by auto
    next
      case other
      then show ?thesis
        using ‹no_abs t
        apply (subst (asm) no_abs.simps)
        apply (subst (asm) term_cases_def)
        by simp
    qed
qed

lemma no_abs_cases[consumes 1, cases pred: no_abs]:
  assumes "no_abs t"
  obtains (free) name where "t = free name"
        | (const) name where "t = const name"
        | (app) t1 t2 where "t = app t1 t2" "no_abs t1" "no_abs t2"
proof (cases rule: pre_term_class.term_cases[where t = t])
  case (app u1 u2)
  show ?thesis
    apply (rule that(3))
    apply fact
    using ‹no_abs t unfolding t = _ by auto
next
  case other
  then have False
    using ‹no_abs t
    apply (subst (asm) no_abs.simps)
    by (auto simp: term_cases_def)
  then show ?thesis ..
qed

definition is_abs :: "'a::term  bool" where
"is_abs t = term_cases (λ_. False) (λ_. False) (λ_ _. False) True t"

lemmas is_abs_simps[simp] = term_cases_template[OF is_abs_def]

definition abs_ish :: "term list  'a::term  bool" where
"abs_ish pats rhs  pats  []  is_abs rhs"

locale simple_syntactic_and =
  fixes P :: "'a::term  bool"
  assumes app: "P (app t u)  P t  P u"
begin

context
  notes app[simp]
begin

lemma list_comb: "P (list_comb f xs)  P f  list_all P xs"
by (induction xs arbitrary: f) auto

corollary list_combE:
  assumes "P (list_comb f xs)"
  shows "P f" "x  set xs  P x"
using assms
by (auto simp: list_comb list_all_iff)

lemma match:
  assumes "match pat t = Some env" "P t"
  shows "fmpred (λ_. P) env"
using assms
by (induction pat t env rule: match_some_induct) auto

lemma matchs:
  assumes "matchs pats ts = Some env" "list_all P ts"
  shows "fmpred (λ_. P) env"
using assms
by (induction pats ts arbitrary: env rule: matchs.induct) (auto elim!: option_bindE intro: match)

end

end

locale subst_syntactic_and = simple_syntactic_and +
  assumes subst: "P t  fmpred (λ_. P) env  P (subst t env)"
begin

lemma rewrite_step:
  assumes "(lhs, rhs)  t  t'" "P t" "P rhs"
  shows "P t'"
using assms by (auto intro: match subst)

end

locale simple_syntactic_or =
  fixes P :: "'a::term  bool"
  assumes app: "P (app t u)  P t  P u"
begin

context
  notes app[simp]
begin

lemma list_comb: "P (list_comb f xs)  P f  list_ex P xs"
by (induction xs arbitrary: f) auto

lemma match:
  assumes "match pat t = Some env" "¬ P t"
  shows "fmpred (λ_ t. ¬ P t) env"
using assms
by (induction pat t env rule: match_some_induct) auto

end

sublocale neg: simple_syntactic_and "λt. ¬ P t"
by standard (auto simp: app)

end

global_interpretation no_abs: simple_syntactic_and no_abs
by standard simp

global_interpretation closed: simple_syntactic_and "λt. closed_except t S" for S
by standard (simp add: closed_except_def)

global_interpretation closed: subst_syntactic_and closed
by standard (rule subst_closed_preserved)

corollary closed_list_comb: "closed (name $$ args)  list_all closed args"
by (simp add: closed.list_comb)

locale term_struct_rel =
  fixes P :: "'a::term  'b::term  bool"
  assumes P_t_const: "P t (const name)  t = const name"
  assumes P_const_const: "P (const name) (const name)"
  assumes P_t_app: "P t (app u1 u2)  t1 t2. t = app t1 t2  P t1 u1  P t2 u2"
  assumes P_app_app: "P t1 u1  P t2 u2  P (app t1 t2) (app u1 u2)"
begin

abbreviation P_env :: "('k, 'a) fmap  ('k, 'b) fmap  bool" where
"P_env  fmrel P"

lemma related_match:
  assumes "match x u = Some env" "P t u"
  obtains env' where "match x t = Some env'" "P_env env' env"
using assms proof (induction x u env arbitrary: t thesis rule: match_some_induct)
  case (app v1 v2 w1 w2 env1 env2)
  obtain u1 u2 where "t = app u1 u2" "P u1 w1" "P u2 w2"
    using P_t_app[OF P t (app w1 w2)] by auto
  with app obtain env1' env2'
    where "match v1 u1 = Some env1'" "P_env env1' env1"
      and "match v2 u2 = Some env2'" "P_env env2' env2"
    by metis
  hence "match (v1 $ v2) (app u1 u2) = Some (env1' ++f env2')"
    by simp

  show ?case
    proof (rule app.prems)
      show "match (v1 $ v2) t = Some (env1' ++f env2')"
        unfolding t = _ by fact
    next
      show "P_env (env1' ++f env2') (env1 ++f env2)"
        by rule fact+
    qed
qed (auto split: option.splits if_splits dest: P_t_const)

lemma list_combI:
  assumes "list_all2 P us1 us2" "P t1 t2"
  shows "P (list_comb t1 us1) (list_comb t2 us2)"
using assms
by (induction arbitrary: t1 t2 rule: list.rel_induct) (auto intro: P_app_app)

lemma list_combE:
  assumes "P t (name $$ args)"
  obtains args' where "t = name $$ args'" "list_all2 P args' args"
using assms proof (induction args arbitrary: t thesis rule: rev_induct)
  case Nil
  hence "P t (const name)"
    by simp
  hence "t = const name"
    using P_t_const by auto
  with Nil show ?case
    by simp
next
  case (snoc x xs)
  hence "P t (app (name $$ xs) x)"
    by simp
  obtain t' y where "t = app t' y" "P t' (name $$ xs)" "P y x"
    using P_t_app[OF P t (app (name $$ xs) x)] by auto
  with snoc obtain ys where "t' = name $$ ys" "list_all2 P ys xs"
    by blast
  show ?case
    proof (rule snoc.prems)
      show "t = name $$ (ys @ [y])"
        unfolding t = app t' y t' = name $$ ys
        by simp
    next
      have "list_all2 P [y] [x]"
        using P y x by simp
      thus "list_all2 P (ys @ [y]) (xs @ [x])"
        using ‹list_all2 P ys xs
        by (metis list_all2_appendI)
    qed
qed

end

locale term_struct_rel_strong = term_struct_rel +
  assumes P_const_t: "P (const name) t  t = const name"
  assumes P_app_t: "P (app u1 u2) t  t1 t2. t = app t1 t2  P u1 t1  P u2 t2"
begin

lemma unconst_rel: "P t u  unconst t = unconst u"
by (metis P_const_t P_t_const const_name_simps(2) is_const_def unconst_const)

lemma unapp_rel: "P t u  rel_option (rel_prod P P) (unapp t) (unapp u)"
by (smt P_app_t P_t_app is_app_def left_right_simps(3) option.rel_sel option.sel option.simps(3) rel_prod_inject unapp_app)

lemma match_rel:
  assumes "P t u"
  shows "rel_option P_env (match p t) (match p u)"
using assms proof (induction p arbitrary: t u)
  case (Const name)
  thus ?case
    by (auto split: option.splits simp: unconst_rel)
next
  case (App p1 p2)
  hence "rel_option (rel_prod P P) (unapp t) (unapp u)"
    by (metis unapp_rel)
  thus ?case
    using App
    by cases (auto split: option.splits intro!: rel_option_bind)
qed auto

lemma find_match_rel:
  assumes "list_all2 (rel_prod (=) P) cs cs'" "P t t'"
  shows "rel_option (rel_prod P_env (rel_prod (=) P)) (find_match cs t) (find_match cs' t')"
using assms proof induction
  case (Cons x xs y ys)
  moreover obtain px tx py ty where "x = (px, tx)" "y = (py, ty)"
    by (cases x, cases y) auto
  moreover note match_rel[OF Cons(4), where p = px]
  ultimately show ?case
    by (auto elim: option.rel_cases)
qed auto

end

fun convert_term :: "'a::term  'b::term" where
[simp del]: "convert_term t = term_cases const free (λt u. app (convert_term t) (convert_term u)) undefined t"

lemmas convert_term_simps[simp] = term_cases_template[OF convert_term.simps]

lemma convert_term_id:
  assumes "no_abs t"
  shows "convert_term t = t"
using assms by induction auto

lemma convert_term_no_abs:
  assumes "no_abs t"
  shows "no_abs (convert_term t)"
using assms by induction auto

lemma convert_term_inj:
  assumes "no_abs t" "no_abs t'" "convert_term t = convert_term t'"
  shows "t = t'"
using assms proof (induction t arbitrary: t')
  case (free name)
  then show ?case
    by cases (auto dest: term_inject)
next
  case (const name)
  then show ?case
    by cases (auto dest: term_inject)
next
  case (app t1 t2)
  from ‹no_abs t' show ?case
    apply cases
    using app by (auto dest: term_inject)
qed

lemma convert_term_idem:
  assumes "no_abs t"
  shows "convert_term (convert_term t) = convert_term t"
using assms by (induction t) auto

lemma convert_term_frees[simp]:
  assumes "no_abs t"
  shows "frees (convert_term t) = frees t"
using assms by induction auto

lemma convert_term_consts[simp]:
  assumes "no_abs t"
  shows "consts (convert_term t) = consts t"
using assms by induction auto

text ‹
  The following lemma does not generalize to when @{prop ‹match t u = None›}. Assume matching
  return @{const None}, because the pattern is an application and the object is a term satisfying
  @{const is_abs}. Now, @{const convert_term} applied to the object will produce @{const undefined}.
  Of course we don't know anything about that and whether or not that matches. A workaround would
  be to require implementations of @{class term} to prove @{prop t. is_abs t}, such that
  @{const convert_term} could use that instead of @{const undefined}. This seems to be too much of a
  special case in order to be useful.
›

lemma convert_term_match:
  assumes "match t u = Some env"
  shows "match t (convert_term u) = Some (fmmap convert_term env)"
using assms by (induction t u env rule: match_some_induct) auto

section ‹Related work›

text ‹
  Schmidt-Schau{\ss} and Siekmann @{cite schmidt1988unification} discuss the concept of
  ‹unification algebras›. They generalize terms to ‹objects› and substitutions to ‹mappings›.
  A unification problem can be rephrased to finding a mapping such that a set of objects are mapped
  to the same object. The advantage of this generalization is that other -- superficially unrelated
  -- problems like solving algebraic equations or querying logic programs can be seen as unification
  problems.

  In particular, the authors note that among the similarities of such problems are that ``objects
  [have] variables'' whose ``names do not matter'' and ``there exists an operation like substituting
  objects into variables''. The major difference between this formalization and their work is that I
  use concrete types for variables and mappings. Otherwise, some similarities to here can be found.

  Eder @{cite eder1985properties} discusses properties of substitutions with a special focus on a
  partial ordering between substitutions. However, Eder constructs and uses a concrete type of
  first-order terms, similarly to Sternagel and Thiemann @{cite sternagel2018terms}.

  Williams @{cite williams1991instantiation} defines substitutions as elements in a monoid.
  In this setting, instantiations can be represented as ‹monoid actions›. Williams then proceeds to
  define -- for arbitrary sets of terms and variables -- the notion of ‹instantiation systems,›
  heavily drawing on notation from Schmidt-Schau{\ss} and Siekmann. Some of the presented axioms
  are also present in this formalization, as are some theorems that have a direct correspondence.
›

end

Theory Term

section ‹Instantiation of class term› for type term›

theory Term
imports Term_Class
begin

instantiation "term" :: "term" begin

text ‹
  All of these definitions need to be marked as code del›; otherwise the code generator will
  attempt to generate these, which will fail because they are not executable.
›

definition abs_pred_term :: "(term  bool)  term  bool" where
[code del]: "abs_pred P t 
  (x. t = Bound x  P t) 
  (t'. t = Λ t'  P t'  P t)"

instance proof (standard, goal_cases)
  case (1 P t)
  then show ?case
    by (induction t) (auto simp: abs_pred_term_def const_term_def free_term_def app_term_def)
qed (auto simp: abs_pred_term_def)

end

lemma is_const_free[simp]: "¬ is_const (Free name)"
unfolding is_const_def by simp

lemma is_free_app[simp]: "¬ is_free (t $ u)"
unfolding is_free_def by simp

lemma is_free_free[simp]: "is_free (Free name)"
unfolding is_free_def by simp

lemma is_const_const[simp]: "is_const (Const name)"
unfolding is_const_def by simp

lemma list_comb_free: "is_free (list_comb f xs)  is_free f"
apply (induction xs arbitrary: f)
apply auto
subgoal premises prems
  apply (insert prems(1)[OF prems(2)])
  unfolding app_term_def
  by simp
done

lemma const_list_comb_free[simp]: "¬ is_free (name $$ args)"
by (fastforce dest: list_comb_free simp: const_term_def)

corollary const_list_comb_neq_free[simp]: "name $$ args  free name'"
by (metis const_list_comb_free is_free_simps(1))

declare const_list_comb_neq_free[symmetric, simp]

lemma match_list_comb_list_comb_eq_lengths[simp]:
  assumes "length ps = length vs"
  shows "match (list_comb f ps) (list_comb g vs) =
    (case match f g of
      Some env 
        (case those (map2 match ps vs) of
          Some envs  Some (foldl (++f) env envs)
        | None  None)
    | None  None)"
using assms
by (induction ps vs arbitrary: f g rule: list_induct2) (auto split: option.splits simp: app_term_def)

lemma matchs_match_list_comb[simp]: "match (name $$ xs) (name $$ ys) = matchs xs ys"
proof (induction xs arbitrary: ys rule: rev_induct)
  case Nil
  show ?case
    by (cases ys rule: rev_cases) (auto simp: const_term_def)
next
  case (snoc x xs)
  note snoc0 = snoc
  have "match (name $$ xs $ x) (name $$ ys) = matchs (xs @ [x]) ys"
    proof (cases ys rule: rev_cases)
      case (snoc zs z)
      show ?thesis
        unfolding snoc using snoc0
        by simp
    qed auto
  thus ?case
    by (simp add: app_term_def)
qed

fun bounds :: "term  nat fset" where
"bounds (Bound i) = {| i |}" |
"bounds (t1 $ t2) = bounds t1 |∪| bounds t2" |
"bounds (Λ t) = (λi. i - 1) |`| (bounds t - {| 0 |})" |
"bounds _ = {||}"

definition shift_nat :: "nat  int  nat" where
[simp]: "shift_nat n k = (if k  0 then n + nat k else n - nat ¦k¦)"

fun incr_bounds :: "int  nat  term  term" where
"incr_bounds inc lev (Bound i) = (if i  lev then Bound (shift_nat i inc) else Bound i)" |
"incr_bounds inc lev (Λ u) = Λ incr_bounds inc (lev + 1) u" |
"incr_bounds inc lev (t1 $ t2) = incr_bounds inc lev t1 $ incr_bounds inc lev t2" |
"incr_bounds _ _ t = t"

lemma incr_bounds_frees[simp]: "frees (incr_bounds n k t) = frees t"
by (induction n k t rule: incr_bounds.induct) auto

lemma incr_bounds_zero[simp]: "incr_bounds 0 i t = t"
by (induct t arbitrary: i) auto

fun replace_bound :: "nat  term  term  term" where
"replace_bound lev (Bound i) t = (if i < lev then Bound i else if i = lev then incr_bounds (int lev) 0 t else Bound (i - 1))" |
"replace_bound lev (t1 $ t2) t = replace_bound lev t1 t $ replace_bound lev t2 t" |
"replace_bound lev (Λ u) t = Λ replace_bound (lev + 1) u t" |
"replace_bound _ t _ = t"

abbreviation β_reduce :: "term  term  term" ("_ [_]β") where
"t [u]β  replace_bound 0 t u"

lemma replace_bound_frees: "frees (replace_bound n t t') |⊆| frees t |∪| frees t'"
by (induction n t t' rule: replace_bound.induct) auto

lemma replace_bound_eq:
  assumes "i |∉| bounds t"
  shows "replace_bound i t t' = incr_bounds (-1) (i + 1) t"
using assms
by (induct t arbitrary: i) force+

fun wellformed' :: "nat  term  bool" where
"wellformed' n (t1 $ t2)  wellformed' n t1  wellformed' n t2" |
"wellformed' n (Bound n')  n' < n" |
"wellformed' n (Λ t)  wellformed' (n + 1) t" |
"wellformed' _ _  True"

lemma wellformed_inc:
  assumes "wellformed' k t" "k  n"
  shows "wellformed' n t"
using assms
by (induct t arbitrary: k n) auto

abbreviation wellformed :: "term  bool" where
"wellformed  wellformed' 0"

lemma wellformed'_replace_bound_eq:
  assumes "wellformed' n t" "k  n"
  shows "replace_bound k t u = t"
using assms
by (induction t arbitrary: n k) auto

lemma wellformed_replace_bound_eq: "wellformed t  replace_bound k t u = t"
by (rule wellformed'_replace_bound_eq) simp+

lemma incr_bounds_eq: "n  k  wellformed' k t  incr_bounds i n t = t"
by (induct t arbitrary: k n) force+

lemma incr_bounds_subst:
  assumes "t. t  fmran' env  wellformed t"
  shows "incr_bounds i n (subst t env) = subst (incr_bounds i n t) env"
proof (induction t arbitrary: n)
  case (Free name)
  show ?case
    proof (cases "fmlookup env name")
      case (Some t)
      hence "wellformed t"
        using assms by (auto intro: fmran'I)
      hence "incr_bounds i n t = t"
        by (subst incr_bounds_eq) auto
      with Some show ?thesis
        by simp
    qed auto
qed auto

lemma incr_bounds_wellformed:
  assumes "wellformed' m u"
  shows "wellformed' (k + m) (incr_bounds (int k) n u)"
using assms
by (induct u arbitrary: n m) force+

lemma replace_bound_wellformed:
  assumes "wellformed u" "wellformed' (Suc k) t" "i  k"
  shows "wellformed' k (replace_bound i t u)"
using assms
apply (induction t arbitrary: i k)
apply auto
using incr_bounds_wellformed[where m = 0, simplified]
using wellformed_inc by blast

lemma subst_wellformed:
  assumes "wellformed' n t" "fmpred (λ_. wellformed) env"
  shows "wellformed' n (subst t env)"
using assms
by (induction t arbitrary: n) (auto split: option.splits intro: wellformed_inc)

global_interpretation wellformed: simple_syntactic_and "wellformed' n" for n
by standard (auto simp: app_term_def)

global_interpretation wellformed: subst_syntactic_and wellformed
by standard (auto intro: subst_wellformed)

lemma match_list_combE:
  assumes "match (name $$ xs) t = Some env"
  obtains ys where "t = name $$ ys" "matchs xs ys = Some env"
proof -
  from assms that show thesis
    proof (induction xs arbitrary: t env thesis rule: rev_induct)
      case Nil
      from Nil(1) show ?case
        apply (auto simp: const_term_def split: option.splits if_splits)
        using Nil(2)[where ys = "[]"]
        by auto
    next
      case (snoc x xs)
      obtain t' y where "t = app t' y"
        using ‹match _ t = Some env
        by (auto simp: app_term_def elim!: option_bindE)
      from snoc(2) obtain env1 env2
        where "match (name $$ xs) t' = Some env1" "match x y = Some env2" "env = env1 ++f env2"
        unfolding t = _ by (fastforce simp: app_term_def elim: option_bindE)

      with snoc obtain ys where "t' = name $$ ys" "matchs xs ys = Some env1"
        by blast

      show ?case
        proof (rule snoc(3))
          show "t = name $$ (ys @ [y])"
            unfolding t = _ t' = _
            by simp
        next
          have "matchs [x] [y] = Some env2"
            using ‹match x y = _ by simp
          thus "matchs (xs @ [x]) (ys @ [y]) = Some env"
            unfolding env = _ using ‹matchs xs ys = _
            by simp
        qed
    qed
qed

lemma left_nesting_neq_match:
  "left_nesting f  left_nesting g  is_const (fst (strip_comb f))  match f g = None"
proof (induction f arbitrary: g)
  case (Const x)
  then show ?case
    apply (auto split: option.splits)
    apply (fold const_term_def)
    apply auto
    done
next
  case (App f1 f2)
  then have f1_g: "Suc (left_nesting f1)  left_nesting g" and f1: "is_const (fst (strip_comb f1))"
    apply (fold app_term_def)
    by (auto split: prod.splits)
  show ?case
    proof (cases "unapp g")
      case (Some g')
      obtain g1 g2 where "g' = (g1, g2)"
        by (cases g') auto
      with Some have "g = app g1 g2"
        by auto
      with f1_g have "left_nesting f1  left_nesting g1"
        by simp
      with f1 App have "match f1 g1 = None"
        by simp
      then show ?thesis
        unfolding g' = _ g = _
        by simp
    qed simp
qed auto

context begin

private lemma match_list_comb_list_comb_none_structure:
  assumes "length ps = length vs" "left_nesting f  left_nesting g"
  assumes "is_const (fst (strip_comb f))"
  shows "match (list_comb f ps) (list_comb g vs) = None"
using assms
by (induction ps vs arbitrary: f g rule: list_induct2) (auto simp: split_beta left_nesting_neq_match)

lemma match_list_comb_list_comb_some:
  assumes "match (list_comb f ps) (list_comb g vs) = Some env" "left_nesting f = left_nesting g"
  assumes "is_const (fst (strip_comb f))"
  shows "match f g  None" "length ps = length vs"
proof -
  have "match f g  None  length ps = length vs"
    proof (cases rule: linorder_cases[where y = "length vs" and x = "length ps"])
      assume "length ps = length vs"
      thus ?thesis
        using assms
        proof (induction ps vs arbitrary: f g env rule: list_induct2)
          case (Cons p ps v vs)
          have "match (app f p) (app g v)  None  length ps = length vs"
            proof (rule Cons)
              show "is_const (fst (strip_comb (app f p)))"
                using Cons by (simp add: split_beta)
            next
              show "left_nesting (app f p) = left_nesting (app g v)"
                using Cons by simp
            next
              show "match (list_comb (app f p) ps) (list_comb (app g v) vs) = Some env"
                using Cons by simp
            qed
          thus ?case
            unfolding app_term_def
            by (auto elim: match.elims option_bindE)
        qed auto
    next
      assume "length ps < length vs"
      then obtain vs1 vs2 where "vs = vs1 @ vs2" "length ps = length vs2" "0 < length vs1"
        by (auto elim: list_split)

      have "match (list_comb f ps) (list_comb (list_comb g vs1) vs2) = None"
        proof (rule match_list_comb_list_comb_none_structure)
          show "left_nesting f  left_nesting (list_comb g vs1)"
            using assms(2) 0 < length vs1 by simp
        qed fact+
      hence "match (list_comb f ps) (list_comb g vs) = None"
        unfolding vs = _ by simp
      hence False
        using assms by auto
      thus ?thesis ..
    next
      assume "length vs < length ps"
      then obtain ps1 ps2 where "ps = ps1 @ ps2" "length ps2 = length vs" "0 < length ps1"
        by (auto elim: list_split)

      have "match (list_comb (list_comb f ps1) ps2) (list_comb g vs) = None"
        proof (rule match_list_comb_list_comb_none_structure)
          show "left_nesting (list_comb f ps1)  left_nesting g"
            using assms 0 < length ps1 by simp
        next
          show "is_const (fst (strip_comb (list_comb f ps1)))"
            using assms by (simp add: strip_list_comb)
        qed fact
      hence "match (list_comb f ps) (list_comb g vs) = None"
        unfolding ps = _ by simp
      hence False
        using assms by auto
      thus ?thesis ..
    qed
  thus "match f g  None" "length ps = length vs"
    by simp+
qed

end

lemma match_list_comb_list_comb_none_name[simp]:
  assumes "name  name'"
  shows "match (name $$ ps) (name' $$ vs) = None"
proof (rule ccontr)
  assume "match (name $$ ps) (name' $$ vs)  None"
  then obtain env where *: "match (name $$ ps) (name' $$ vs) = Some env"
    by blast
  hence "match (const name) (const name' :: 'a)  None"
    by (rule match_list_comb_list_comb_some) (simp add: is_const_def)+
  hence "name = name'"
    unfolding const_term_def
    by (simp split: if_splits)
  thus False
    using assms by blast
qed

lemma match_list_comb_list_comb_none_length[simp]:
  assumes "length ps  length vs"
  shows "match (name $$ ps) (name' $$ vs) = None"
proof (rule ccontr)
  assume "match (name $$ ps) (name' $$ vs)  None"
  then obtain env where "match (name $$ ps) (name' $$ vs) = Some env"
    by blast
  hence "length ps = length vs"
    by (rule match_list_comb_list_comb_some) (simp add: is_const_def)+
  thus False
    using assms by blast
qed

context term_struct_rel begin

corollary related_matchs:
  assumes "matchs ps ts2 = Some env2" "list_all2 P ts1 ts2"
  obtains env1 where "matchs ps ts1 = Some env1" "P_env env1 env2"
proof -
  fix name ― ‹dummy›

  from assms have "match (name $$ ps) (name $$ ts2) = Some env2"
    by simp
  moreover have "P (name $$ ts1) (name $$ ts2)"
    using assms by (auto intro: P_const_const list_combI)
  ultimately obtain env1 where "match (name $$ ps) (name $$ ts1) = Some env1" "P_env env1 env2"
    by (metis related_match)
  hence "matchs ps ts1 = Some env1"
    by simp

  show thesis
    by (rule that) fact+
qed

end

end

Theory Pats

chapter ‹Wellformedness of patterns›

theory Pats
imports Term
begin

text ‹
  The @{class term} class already defines a generic definition of ‹matching› a ‹pattern› with a
  term. Importantly, the type of patterns is neither generic, nor a dedicated pattern type; instead,
  it is @{typ term} itself.

  Patterns are a proper subset of terms, with the restriction that no abstractions may occur and
  there must be at most a single occurrence of any variable (usually known as ‹linearity›).
  The first restriction can be modelled in a datatype, the second cannot. Consequently, I define a
  predicate that captures both properties.

  Using linearity, many more generic properties can be proved, for example that substituting the
  environment produced by matching yields the matched term.
›

fun linear :: "term  bool" where
"linear (Free _)  True" |
"linear (Const _)  True" |
"linear (t1 $ t2)  linear t1  linear t2  ¬ is_free t1  fdisjnt (frees t1) (frees t2)" |
"linear _  False"

lemmas linear_simps[simp] =
  linear.simps(2)[folded const_term_def]
  linear.simps(3)[folded app_term_def]

lemma linear_implies_no_abs: "linear t  no_abs t"
proof induction
  case Const
  then show ?case
    by (fold const_term_def free_term_def app_term_def) auto
next
  case Free
  then show ?case
    by (fold const_term_def free_term_def app_term_def) auto
next
  case App
  then show ?case
    by (fold const_term_def free_term_def app_term_def) auto
qed auto

fun linears :: "term list  bool" where
"linears []  True" |
"linears (t # ts)  linear t  fdisjnt (frees t) (freess ts)  linears ts"

lemma linears_butlastI[intro]: "linears ts  linears (butlast ts)"
proof (induction ts)
  case (Cons t ts)
  hence "linear t" "linears (butlast ts)"
    by simp+
  moreover have " fdisjnt (frees t) (freess (butlast ts))"
    proof (rule fdisjnt_subset_right)
      show "freess (butlast ts) |⊆| freess ts"
        by (rule freess_subset) (auto dest: in_set_butlastD)
    next
      show "fdisjnt (frees t) (freess ts)"
        using Cons by simp
    qed
  ultimately show ?case
    by simp
qed simp

lemma linears_appI[intro]:
  assumes "linears xs" "linears ys" "fdisjnt (freess xs) (freess ys)"
  shows "linears (xs @ ys)"
using assms proof (induction xs)
  case (Cons z zs)
  hence "linears zs"
    by simp+

  have "fdisjnt (frees z) (freess zs |∪| freess ys)"
    proof (rule fdisjnt_union_right)
      show "fdisjnt (frees z) (freess zs)"
        using ‹linears (z # zs) by simp
    next
      have "frees z |⊆| freess (z # zs)"
        unfolding freess_def by simp
      thus "fdisjnt (frees z) (freess ys)"
        by (rule fdisjnt_subset_left) fact
    qed

  moreover have "linears (zs @ ys)"
    proof (rule Cons)
      show "fdisjnt (freess zs) (freess ys)"
        using Cons
        by (auto intro: freess_subset fdisjnt_subset_left)
    qed fact+

  ultimately show ?case
    using Cons by auto
qed simp

lemma linears_linear: "linears ts  t  set ts  linear t"
by (induct ts) auto

lemma linears_singleI[intro]: "linear t  linears [t]"
by (simp add: freess_def fdisjnt_alt_def)

lemma linear_strip_comb: "linear t  linear (fst (strip_comb t))"
by (induction t rule: strip_comb_induct) (auto simp: split_beta)

lemma linears_strip_comb: "linear t  linears (snd (strip_comb t))"
proof (induction t rule: strip_comb_induct)
  case (app t1 t2)
  have "linears (snd (strip_comb t1) @ [t2])"
    proof (intro linears_appI linears_singleI)
      have "freess (snd (strip_comb t1)) |⊆| frees t1"
        by (subst frees_strip_comb) auto
      moreover have "fdisjnt (frees t1) (frees t2)"
        using app by auto
      ultimately have "fdisjnt (freess (snd (strip_comb t1))) (frees t2)"
        by (rule fdisjnt_subset_left)
      thus "fdisjnt (freess (snd (strip_comb t1))) (freess [t2])"
        by simp
    next
      show "linear t2" "linears (snd (strip_comb t1))"
        using app by auto
    qed
  thus ?case
    by (simp add: split_beta)
qed auto

lemma linears_appendD:
  assumes "linears (xs @ ys)"
  shows "linears xs" "linears ys" "fdisjnt (freess xs) (freess ys)"
using assms proof (induction xs)
  case (Cons x xs)
  assume "linears ((x # xs) @ ys)"

  hence "linears (x # (xs @ ys))"
    by simp
  hence "linears (xs @ ys)" "linear x" "fdisjnt (frees x) (freess (xs @ ys))"
    by auto
  hence "linears xs"
    using Cons by simp
  moreover have "fdisjnt (frees x) (freess xs)"
    proof (rule fdisjnt_subset_right)
      show "freess xs |⊆| freess (xs @ ys)" by simp
    qed fact
  ultimately show "linears (x # xs)"
    using ‹linear x by auto

  have "fdisjnt (freess xs) (freess ys)"
    by (rule Cons) fact
  moreover have "fdisjnt (frees x) (freess ys)"
    proof (rule fdisjnt_subset_right)
      show "freess ys |⊆| freess (xs @ ys)" by simp
    qed fact
  ultimately show "fdisjnt (freess (x # xs)) (freess ys)"
    unfolding fdisjnt_alt_def
    by auto
qed (auto simp: fdisjnt_alt_def)

lemma linear_list_comb:
  assumes "linear f" "linears xs" "fdisjnt (frees f) (freess xs)" "¬ is_free f"
  shows "linear (list_comb f xs)"
using assms
proof (induction xs arbitrary: f)
  case (Cons x xs)

  hence *: "fdisjnt (frees f) (frees x |∪| freess xs)"
    by simp

  have "linear (list_comb (f $ x) xs)"
    proof (rule Cons)
      have "linear x"
        using Cons by simp
      moreover have "fdisjnt (frees f) (frees x)"
        using * by (auto intro: fdisjnt_subset_right)
      ultimately show "linear (f $ x)"
        using assms Cons by simp
    next
      show "linears xs"
        using Cons by simp
    next
      have "fdisjnt (frees f) (freess xs)"
        using * by (auto intro: fdisjnt_subset_right)
      moreover have "fdisjnt (frees x) (freess xs)"
        using Cons by simp
      ultimately show "fdisjnt (frees (f $ x)) (freess xs)"
        by (auto intro: fdisjnt_union_left)
    qed auto
  thus ?case
    by (simp add: app_term_def)
qed auto

corollary linear_list_comb': "linears xs  linear (name $$ xs)"
by (auto intro: linear_list_comb simp: fdisjnt_alt_def)

lemma linear_strip_comb_cases[consumes 1]:
  assumes "linear pat"
  obtains (comb) s args where "strip_comb pat = (Const s, args)" "pat = s $$ args"
        | (free) s where "strip_comb pat = (Free s, [])" "pat = Free s"
using assms
proof (induction pat rule: strip_comb_induct)
  case (app t1 t2)
  show ?case
    proof (rule "app.IH")
      show "linear t1"
        using app by simp
    next
      fix s
      assume "strip_comb t1 = (Free s, [])"
      hence "t1 = Free s"
        by (metis fst_conv snd_conv strip_comb_empty)
      hence False
        using app by simp
      thus thesis
        by simp
    next
      fix s args
      assume "strip_comb t1 = (Const s, args)"
      with app show thesis
        by (fastforce simp add: strip_comb_app)
    qed
next
  case (no_app t)
  thus ?case
    by (cases t) (auto simp: const_term_def)
qed

lemma wellformed_linearI: "linear t  wellformed' n t"
by (induct t) auto

lemma pat_cases:
  obtains (free) s where "t = Free s"
        | (comb) name args where "linears args" "t = name $$ args"
        | (nonlinear) "¬ linear t"
proof (cases t)
  case Free
  thus thesis using free by simp
next
  case Bound
  thus thesis using nonlinear by simp
next
  case Abs
  thus thesis using nonlinear by simp
next
  case (Const name)
  have "linears []" by simp
  moreover have "t = name $$ []" unfolding Const by (simp add: const_term_def)
  ultimately show thesis
    by (rule comb)
next
  case (App u v)
  show thesis
    proof (cases "linear t")
      case False
      thus thesis using nonlinear by simp
    next
      case True
      thus thesis
        proof (cases rule: linear_strip_comb_cases)
          case free
          thus thesis using that by simp
        next
          case (comb name args)
          moreover hence "linears (snd (strip_comb t))"
            using True by (blast intro: linears_strip_comb)
          ultimately have "linears args"
            by simp
          thus thesis using that comb by simp
        qed
    qed
qed

corollary linear_pat_cases[consumes 1]:
  assumes "linear t"
  obtains (free) s where "t = Free s"
        | (comb) name args where "linears args" "t = name $$ args"
using assms
by (metis pat_cases)

lemma linear_pat_induct[consumes 1, case_names free comb]:
  assumes "linear t"
  assumes "s. P (Free s)"
  assumes "name args. linears args  (arg. arg  set args  P arg)  P (name $$ args)"
  shows "P t"
using wf_measure[of size] ‹linear t
proof (induction t)
  case (less t)

  show ?case
    using ‹linear t
    proof (cases rule: linear_pat_cases)
      case (free name)
      thus ?thesis
        using assms by simp
    next
      case (comb name args)
      show ?thesis
        proof (cases "args = []")
          case True
          thus ?thesis
            using assms comb by fastforce
        next
          case False
          show ?thesis
            unfolding t = _
            proof (rule assms)
              fix arg
              assume "arg  set args"

              then have "(arg, t)  measure size"
                unfolding t = _
                by (induction args) auto

              moreover have "linear arg"
                using arg  set args ‹linears args
                by (auto dest: linears_linear)

              ultimately show "P arg"
                using less by auto
            qed fact
        qed
    qed
qed

context begin

private lemma match_subst_correctness0:
  assumes "linear t"
  shows "case match t u of
          None  (env. subst (convert_term t) env  u) |
          Some env  subst (convert_term t) env = u"
using assms proof (induction t arbitrary: u)
  case Free
  show ?case
    unfolding match.simps
    by (fold free_term_def) auto
next
  case Const
  show ?case
    unfolding match.simps
    by (fold const_term_def) (auto split: option.splits)
next
  case (App t1 t2)
  hence linear: "linear t1" "linear t2" "fdisjnt (frees t1) (frees t2)"
    by simp+

  show ?case
    proof (cases "unapp u")
      case None
      then show ?thesis
        apply simp
        apply (fold app_term_def)
        apply simp
        using app_simps(3) is_app_def by blast
    next
      case (Some u')
      then obtain u1 u2 where u: "unapp u = Some (u1, u2)" by (cases u') auto
      hence "u = app u1 u2" by auto

      note 1 = App(1)[OF ‹linear t1, of u1]
      note 2 = App(2)[OF ‹linear t2, of u2]

      show ?thesis
        proof (cases "match t1 u1")
          case None
          then show ?thesis
            using u
            apply simp
            apply (fold app_term_def)
            using 1 by auto
        next
          case (Some env1)
          with 1 have s1: "subst (convert_term t1) env1 = u1" by simp
          show ?thesis
            proof (cases "match t2 u2")
              case None
              then show ?thesis
                using u
                apply simp
                apply (fold app_term_def)
                using 2 by auto
            next
              case (Some env2)
              with 2 have s2: "subst (convert_term t2) env2 = u2" by simp

              note match = ‹match t1 u1 = Some env1 ‹match t2 u2 = Some env2

              let ?env = "env1 ++f env2"
              from match have "frees t1 = fmdom env1" "frees t2 = fmdom env2"
                by (auto simp: match_dom)
              with linear have "env1 = fmrestrict_fset (frees t1) ?env" "env2 = fmrestrict_fset (frees t2) ?env"
                apply auto
                apply (auto simp: fmfilter_alt_defs)
                apply (subst fmfilter_false; auto simp: fdisjnt_alt_def intro: fmdomI)+
                done
              with s1 s2 have "subst (convert_term t1) ?env = u1" "subst (convert_term t2) ?env = u2"
                using linear
                by (metis subst_restrict' convert_term_frees linear_implies_no_abs)+

              then show ?thesis
                using match unfolding u = _
                apply simp
                apply (fold app_term_def)
                by simp
            qed
        qed
    qed
qed auto

lemma match_subst_some[simp]:
  "match t u = Some env  linear t  subst (convert_term t) env = u"
by (metis (mono_tags) match_subst_correctness0 option.simps(5))

lemma match_subst_none:
  "match t u = None  linear t  subst (convert_term t) env = u  False"
by (metis (mono_tags, lifting) match_subst_correctness0 option.simps(4))

end

(* FIXME inverse direction? *)

lemma match_matches: "match t u = Some env  linear t  t  u"
by (metis match_subst_some linear_implies_no_abs convert_term_id matchesI)

lemma overlapping_var1I: "overlapping (Free name) t"
proof (intro overlappingI matchesI)
  show "subst (Free name) (fmap_of_list [(name, t)]) = t"
    by simp
next
  show "subst t fmempty = t"
    by simp
qed

lemma overlapping_var2I: "overlapping t (Free name)"
proof (intro overlappingI matchesI)
  show "subst (Free name) (fmap_of_list [(name, t)]) = t"
    by simp
next
  show "subst t fmempty = t"
    by simp
qed

lemma non_overlapping_appI1: "non_overlapping t1 u1  non_overlapping (t1 $ t2) (u1 $ u2)"
unfolding overlapping_def matches_def by auto

lemma non_overlapping_appI2: "non_overlapping t2 u2  non_overlapping (t1 $ t2) (u1 $ u2)"
unfolding overlapping_def matches_def by auto

lemma non_overlapping_app_constI: "non_overlapping (t1 $ t2) (Const name)"
unfolding overlapping_def matches_def by simp

lemma non_overlapping_const_appI: "non_overlapping (Const name) (t1 $ t2)"
unfolding overlapping_def matches_def by simp

lemma non_overlapping_const_constI: "x  y  non_overlapping (Const x) (Const y)"
unfolding overlapping_def matches_def by simp

lemma match_overlapping:
  assumes "linear t1" "linear t2"
  assumes "match t1 u = Some env1" "match t2 u = Some env2"
  shows "overlapping t1 t2"
proof -
  define env1' where "env1' = (fmmap convert_term env1 :: (name, term) fmap)"
  define env2' where "env2' = (fmmap convert_term env2 :: (name, term) fmap)"
  from assms have "match t1 (convert_term u :: term) = Some env1'" "match t2 (convert_term u :: term) = Some env2'"
    unfolding env1'_def env2'_def
    by (metis convert_term_match)+
  with assms show ?thesis
    by (metis overlappingI match_matches)
qed

end

Theory 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 (t1 $n t2) = frees_nterm t1 |∪| frees_nterm t2" |
"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 (t1 $n t2) env = subst_nterm t1 env $n subst_nterm t2 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 (t1 $n t2) = consts_nterm t1 |∪| consts_nterm t2" |
"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 env1" in allE)
    apply (erule_tac x = "fmdrop x env2" 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

Theory Term_to_Nterm

chapter ‹Converting between term›s and nterm›s›

theory Term_to_Nterm
imports
  Fresh_Class
  Find_First
  Term
  Nterm
begin

section α›-equivalence›

inductive alpha_equiv :: "(name, name) fmap  nterm  nterm  bool" where
const: "alpha_equiv env (Nconst x) (Nconst x)" |
var1: "x |∉| fmdom env  x |∉| fmran env  alpha_equiv env (Nvar x) (Nvar x)" |
var2: "fmlookup env x = Some y  alpha_equiv env (Nvar x) (Nvar y)" |
abs: "alpha_equiv (fmupd x y env) n1 n2  alpha_equiv env (Λn x. n1) (Λn y. n2)" |
app: "alpha_equiv env n1 n2  alpha_equiv env m1 m2  alpha_equiv env (n1 $n m1) (n2 $n m2)"

code_pred alpha_equiv .

abbreviation alpha_eq :: "nterm  nterm  bool" (infixl "α" 50) where
"alpha_eq n1 n2  alpha_equiv fmempty n1 n2"

lemma alpha_equiv_refl[intro?]:
  assumes "fmpred (=) Γ"
  shows "alpha_equiv Γ t t"
using assms proof (induction t arbitrary: Γ)
  case Napp
  show ?case
    apply (rule alpha_equiv.app; rule Napp)
    using Napp.prems unfolding fdisjnt_alt_def by auto
qed (auto simp: fdisjnt_alt_def intro: alpha_equiv.intros)

corollary alpha_eq_refl: "alpha_eq t t"
by (auto intro: alpha_equiv_refl)

section ‹From @{typ term} to @{typ nterm}

fun term_to_nterm :: "name list  term  (name, nterm) state" where
"term_to_nterm _ (Const name) = State_Monad.return (Nconst name)" |
"term_to_nterm _ (Free name) = State_Monad.return (Nvar name)" |
"term_to_nterm Γ (Bound n) = State_Monad.return (Nvar (Γ ! n))" |
"term_to_nterm Γ (Λ t) = do {
  n  fresh_create;
  e  term_to_nterm (n # Γ) t;
  State_Monad.return (Λn n. e)
}" |
"term_to_nterm Γ (t1 $ t2) = do {
  e1  term_to_nterm Γ t1;
  e2  term_to_nterm Γ t2;
  State_Monad.return (e1 $n e2)
}"

lemmas term_to_nterm_induct = term_to_nterm.induct[case_names const free bound abs app]

lemma term_to_nterm:
  assumes "no_abs t"
  shows "fst (run_state (term_to_nterm Γ t) x) = convert_term t"
using assms
apply (induction arbitrary: x)
apply auto
by (auto simp: free_term_def free_nterm_def const_term_def const_nterm_def app_term_def app_nterm_def split_beta split: prod.splits)

definition term_to_nterm' :: "term  nterm" where
"term_to_nterm' t = frun_fresh (term_to_nterm [] t) (frees t)"

lemma term_to_nterm_mono: "mono_state (term_to_nterm Γ x)"
by (induction Γ x rule: term_to_nterm.induct) (auto intro: bind_mono_strong)

lemma term_to_nterm_vars0:
  assumes "wellformed' (length Γ) t"
  shows "frees (fst (run_state (term_to_nterm Γ t) s)) |⊆| frees t |∪| fset_of_list Γ"
using assms proof (induction Γ t arbitrary: s rule: term_to_nterm_induct)
  case (bound Γ i)
  hence "Γ ! i |∈| fset_of_list Γ"
    including fset.lifting by transfer auto
  thus ?case
    by (auto simp: State_Monad.return_def)
next
  case (abs Γ t)
  let ?x = "next s"

  from abs have "frees (fst (run_state (term_to_nterm (?x # Γ) t) ?x)) |⊆| frees t |∪| {|?x|} |∪| fset_of_list Γ"
    by simp
  thus ?case
    by (auto simp: create_alt_def split_beta)
qed (auto simp: split_beta)

corollary term_to_nterm_vars:
  assumes "wellformed t"
  shows "frees (fresh_frun (term_to_nterm [] t) F) |⊆| frees t"
proof -
  let  = "[]"
  from assms have "wellformed' (length ) t"
    by simp
  hence "frees (fst (run_state (term_to_nterm  t) (fNext F))) |⊆| (frees t |∪| fset_of_list )"
    by (rule term_to_nterm_vars0)
  thus ?thesis
    by (simp add: fresh_fNext_def fresh_frun_def)
qed

corollary term_to_nterm_closed: "closed t  wellformed t  closed (term_to_nterm' t)"
using term_to_nterm_vars[where F = "frees t" and t = t, simplified]
unfolding closed_except_def term_to_nterm'_def
by (simp add: fresh_frun_def)

lemma term_to_nterm_consts: "pred_state (λt'. consts t' = consts t) (term_to_nterm Γ t)"
apply (rule pred_stateI)
apply (induction t arbitrary: Γ)
apply (auto split: prod.splits)
done

section ‹From @{typ nterm} to @{typ term}

fun nterm_to_term :: "name list  nterm  term" where
"nterm_to_term Γ (Nconst name) = Const name" |
"nterm_to_term Γ (Nvar name) = (case find_first name Γ of Some n  Bound n | None  Free name)" |
"nterm_to_term Γ (t $n u) = nterm_to_term Γ t $ nterm_to_term Γ u" |
"nterm_to_term Γ (Λn x. t) = Λ nterm_to_term (x # Γ) t"

lemma nterm_to_term:
  assumes "no_abs t" "fdisjnt (fset_of_list Γ) (frees t)"
  shows "nterm_to_term Γ t = convert_term t"
using assms proof (induction arbitrary: Γ)
  case (free name)
  then show ?case
    apply simp
    apply (auto simp: free_nterm_def free_term_def fdisjnt_alt_def split: option.splits)
    apply (rule find_first_none)
    by (metis fset_of_list_elem)
next
  case (const name)
  show ?case
    apply simp
    by (simp add: const_nterm_def const_term_def)
next
  case (app t1 t2)
  then have "nterm_to_term Γ t1 = convert_term t1" "nterm_to_term Γ t2 = convert_term t2"
    by (auto simp: fdisjnt_alt_def finter_funion_distrib)
  then show ?case
    apply simp
    by (simp add: app_nterm_def app_term_def)
qed

abbreviation "nterm_to_term'  nterm_to_term []"

lemma nterm_to_term': "no_abs t  nterm_to_term' t = convert_term t"
by (auto simp: fdisjnt_alt_def nterm_to_term)

lemma nterm_to_term_frees[simp]: "frees (nterm_to_term Γ t) = frees t - fset_of_list Γ"
proof (induction t arbitrary: Γ)
  case (Nvar name)
  show ?case
    proof (cases "find_first name Γ")
      case None
      hence "name |∉| fset_of_list Γ"
        including fset.lifting
        by transfer (metis find_first_some option.distinct(1))
      with None show ?thesis
        by auto
    next
      case (Some u)
      hence "name |∈| fset_of_list Γ"
        including fset.lifting
        by transfer (metis find_first_none option.distinct(1))
      with Some show ?thesis
        by auto
    qed
  qed (auto split: option.splits)

section ‹Correctness›

text ‹Some proofs in this section have been contributed by Yu Zhang.›

lemma term_to_nterm_nterm_to_term0:
  assumes "wellformed' (length Γ) t" "fdisjnt (fset_of_list Γ) (frees t)" "distinct Γ"
  assumes "fBall (frees t |∪| fset_of_list Γ) (λx. x  s)"
  shows "nterm_to_term Γ (fst (run_state (term_to_nterm Γ t) s)) = t"
using assms proof (induction Γ t arbitrary: s rule: term_to_nterm_induct)
  case (free Γ name)
  hence "fdisjnt (fset_of_list Γ) {|name|}"
    by simp
  hence "name  set Γ"
    including fset.lifting by transfer' (simp add: disjnt_def)
  hence "find_first name Γ = None"
    by (rule find_first_none)
  thus ?case
    by (simp add: State_Monad.return_def)
next
  case (bound Γ i)
  thus ?case
    by (simp add: State_Monad.return_def find_first_some_index)
next
  case (app Γ t1 t2)
  have "fdisjnt (fset_of_list Γ) (frees t1)"
    apply (rule fdisjnt_subset_right[where N = "frees t1 |∪| frees t2"])
    using app by auto
  have "fdisjnt (fset_of_list Γ) (frees t2)"
    apply (rule fdisjnt_subset_right[where N = "frees t1 |∪| frees t2"])
    using app by auto

  have s: "s  snd (run_state (term_to_nterm Γ t1) s)"
    apply (rule state_io_relD[OF term_to_nterm_mono])
    apply (rule surjective_pairing)
    done

  show ?case
    apply (auto simp: split_beta)
    subgoal
      apply (rule app)
      subgoal using app by simp
      subgoal by fact
      subgoal by fact
      using app by auto
    subgoal
      apply (rule app)
      subgoal using app by simp
      subgoal by fact
      subgoal by fact
      using app s by force+
    done
next
  case (abs Γ t)

  have "next s |∉| frees t |∪| fset_of_list Γ"
    using abs(5)[simplified]
    by (rule next_ge_fall)

  have "nterm_to_term (next s # Γ) (fst (run_state (term_to_nterm (next s # Γ) t) (next s))) = t"
    proof (subst abs)
      show "wellformed' (length (next s # Γ)) t"
        using abs by auto
      show "fdisjnt (fset_of_list (next s # Γ)) (frees t)"
        apply simp
        apply (rule fdisjnt_insert)
        using ‹next s |∉| frees t |∪| fset_of_list Γ abs by auto
      show "distinct (next s # Γ)"
        apply simp
        apply rule
        using ‹next s |∉| frees t |∪| fset_of_list Γ apply (simp add: fset_of_list_elem)
        apply fact
        done
      show "fBall (frees t |∪| fset_of_list (next s # Γ)) (λx. x  next s)"
        using abs(5) apply simp
        apply (rule fBall_pred_weaken[where P = "λx. x  s"])
        subgoal
          apply simp
          by (meson dual_order.strict_implies_order dual_order.strict_trans2 fresh_class.next_ge)
        subgoal by assumption
        done
    qed auto

  thus ?case
    by (auto simp: split_beta create_alt_def)
qed (auto simp: State_Monad.return_def)

lemma term_to_nterm_nterm_to_term:
  assumes "wellformed t" "frees t |⊆| S"
  shows "nterm_to_term' (frun_fresh (term_to_nterm [] t) (S |∪| Q)) = t"
proof (rule term_to_nterm_nterm_to_term0)
  show "wellformed' (length []) t"
    using assms by simp
next
  show "fdisjnt (fset_of_list []) (frees t)"
    unfolding fdisjnt_alt_def by simp
next
  have "fBall (S |∪| Q) (λx. x < fresh.fNext next default (S |∪| Q))"
    by (metis fNext_geq_not_member fresh_fNext_def le_less_linear fBallI)
  hence "fBall (S |∪| Q) (λx. x  fresh.fNext next default (S |∪| Q))"
    by (meson fBall_pred_weaken less_eq_name_def)
  thus "fBall (frees t |∪| fset_of_list []) (λx. x  fresh.fNext next default (S |∪| Q))"
    using ‹frees t |⊆| S
    by auto
qed simp

corollary term_to_nterm_nterm_to_term_simple:
  assumes "wellformed t"
  shows "nterm_to_term' (term_to_nterm' t) = t"
unfolding term_to_nterm'_def using assms
by (metis order_refl sup.idem term_to_nterm_nterm_to_term)

lemma nterm_to_term_eq:
  assumes "frees u |⊆| fset_of_list (common_prefix Γ Γ')"
  shows "nterm_to_term Γ u = nterm_to_term Γ' u"
using assms
proof (induction u arbitrary: Γ Γ')
  case (Nvar name)
  hence "name  set (common_prefix Γ Γ')"
    unfolding frees_nterm.simps
    including fset.lifting
    by transfer' simp
  thus ?case
    by (auto simp: common_prefix_find)
next
  case (Nabs x t)
  hence *: "frees t - {|x|} |⊆| fset_of_list (common_prefix Γ Γ')"
    by simp

  show ?case
    apply simp
    apply (rule Nabs)
    using * Nabs by auto
qed auto

corollary nterm_to_term_eq_closed: "closed t  nterm_to_term Γ t = nterm_to_term Γ' t"
by (rule nterm_to_term_eq) (auto simp: closed_except_def)

lemma nterm_to_term_wellformed: "wellformed' (length Γ) (nterm_to_term Γ t)"
proof (induction t arbitrary: Γ)
  case (Nabs x t)
  hence "wellformed' (Suc (length Γ)) (nterm_to_term (x # Γ) t)"
    by (metis length_Cons)
  thus ?case
    by auto
qed (auto simp: find_first_correct split: option.splits)

corollary nterm_to_term_closed_wellformed: "closed t  wellformed (nterm_to_term Γ t)"
by (metis Ex_list_of_length nterm_to_term_eq_closed nterm_to_term_wellformed)

lemma nterm_to_term_term_to_nterm:
  assumes "frees t |⊆| fset_of_list Γ" "length Γ = length Γ'"
  shows "alpha_equiv (fmap_of_list (zip Γ Γ')) t (fst (run_state (term_to_nterm Γ' (nterm_to_term Γ t)) s))"
using assms proof (induction Γ t arbitrary: s Γ' rule:nterm_to_term.induct)
  case (4 Γ x t)
  show ?case
    apply (simp add: split_beta)
    apply (rule alpha_equiv.abs)
    using "4.IH"[where Γ' = "next s # Γ'"] "4.prems"
    by (fastforce simp: create_alt_def intro: alpha_equiv.intros)
qed
  (force split: option.splits intro: find_first_some intro!: alpha_equiv.intros
         simp: fset_of_list_elem find_first_in_map split_beta fdisjnt_alt_def)+

corollary nterm_to_term_term_to_nterm': "closed t  t α term_to_nterm' (nterm_to_term' t)"
unfolding term_to_nterm'_def closed_except_def
apply (rule nterm_to_term_term_to_nterm[where Γ = "[]" and Γ' = "[]", simplified])
by auto

context begin

private lemma term_to_nterm_alpha_equiv0:
  "length Γ1 = length Γ2  distinct Γ1  distinct Γ2  wellformed' (length Γ1) t1 
   fresh_fin (frees t1 |∪| fset_of_list Γ1) s1  fdisjnt (fset_of_list Γ1) (frees t1) 
   fresh_fin (frees t1 |∪| fset_of_list Γ2) s2  fdisjnt (fset_of_list Γ2) (frees t1) 
   alpha_equiv (fmap_of_list (zip Γ1 Γ2)) (fst( run_state (term_to_nterm Γ1 t1) s1)) (fst ( run_state (term_to_nterm Γ2 t1) s2))"
proof (induction Γ1 t1 arbitrary: Γ2 s1 s2 rule:term_to_nterm_induct)
  case (free Γ1 name)
  then have "name |∉| fmdom (fmap_of_list (zip Γ1 Γ2))"
    unfolding fdisjnt_alt_def
    by force
  moreover have "name |∉| fmran (fmap_of_list (zip Γ1 Γ2))"
    apply rule
    apply (subst (asm) fmran_of_list)
    apply (subst (asm) fset_of_list_map[symmetric])
    apply (subst (asm) distinct_clearjunk_id)
    subgoal
      apply (subst map_fst_zip)
      apply fact
      apply fact
      done
    apply (subst (asm) map_snd_zip)
    apply fact
    using free unfolding fdisjnt_alt_def
    by fastforce
  ultimately show ?case
    by (force intro:alpha_equiv.intros)
next
  case (abs Γ t)
  have *: "next s1 > s1" "next s2 > s2"
    using next_ge by force+
  with abs have "next s1  set Γ" "next s2  set Γ2"
    by (metis fBall_funion fset_of_list_elem next_ge_fall)+
  have "fresh_fin (frees t |∪| fset_of_list Γ) (next s1)"
       "fresh_fin (frees t |∪| fset_of_list Γ2) (next s2)"
    using * abs
    by (smt dual_order.trans fBall_pred_weaken frees_term.simps(3) less_imp_le)+
  have "fdisjnt (finsert (next s1) (fset_of_list Γ)) (frees t)"
       "fdisjnt (finsert (next s2) (fset_of_list Γ2)) (frees t)"
    unfolding fdisjnt_alt_def using abs frees_term.simps
    by (metis fdisjnt_alt_def finter_finsert_right funionCI inf_commute next_ge_fall)+
  have "wellformed' (Suc (length Γ2)) t"
    using wellformed'.simps abs
    by (metis Suc_eq_plus1)
  show ?case
    apply (auto simp: split_beta create_alt_def)
    apply rule
    apply (rule abs.IH[of _ "next s2 # Γ2", simplified])
    by (fact | rule)+
next
  case (app Γ1 t1 t2)
  hence "wellformed' (length Γ1) t1" "wellformed' (length Γ1) t2"
  and "fresh_fin (frees t1 |∪| fset_of_list Γ1) s1" "fresh_fin (frees t1 |∪| fset_of_list Γ2) s2"
  and "fdisjnt (fset_of_list Γ1) (frees t1)" "fdisjnt (fset_of_list Γ2) (frees t1)"
  and "fdisjnt (fset_of_list Γ1) (frees t2)" "fdisjnt (fset_of_list Γ2) (frees t2)"
    using app
    unfolding fdisjnt_alt_def
    by (auto simp: inf_sup_distrib1)
  have "s1  snd (run_state (term_to_nterm Γ1 t1) s1)" "s2  snd (run_state (term_to_nterm Γ2 t1) s2)"
    using term_to_nterm_mono
    by (simp add: state_io_rel_def)+
  hence "fresh_fin (frees t2 |∪| fset_of_list Γ1) (snd (run_state (term_to_nterm Γ1 t1) s1))"
    using ‹fresh_fin (frees (t1 $ t2) |∪| fset_of_list Γ1) s1
    by force

  have "fresh_fin (frees t2 |∪| fset_of_list Γ2) (snd (run_state (term_to_nterm Γ2 t1) s2))"
    apply rule
    using app frees_term.simps s2  _ dual_order.trans
    by (metis fbspec funion_iff)

  show ?case
    apply (auto simp: split_beta create_alt_def)
    apply (rule alpha_equiv.app)
    subgoal
      apply (rule app)
      apply (simp | fact)+
      done
    subgoal
      apply (rule app)
      apply (simp | fact)+
      done
    done
qed (force intro: alpha_equiv.intros simp: fmlookup_of_list in_set_zip)+

lemma term_to_nterm_alpha_equiv:
  assumes "length Γ1 = length Γ2" "distinct Γ1" "distinct Γ2" "closed t"
  assumes "wellformed' (length Γ1) t"
  assumes "fresh_fin (fset_of_list Γ1) s1" "fresh_fin (fset_of_list Γ2) s2"
  shows "alpha_equiv (fmap_of_list (zip Γ1 Γ2)) (fst (run_state (term_to_nterm Γ1 t) s1)) (fst (run_state (term_to_nterm Γ2 t) s2))"
  ― ‹An instantiated version of this lemma with @{prop Γ1 = []} and @{prop Γ2 = []}
      would not make sense because then it would just be a special case of
      @{thm [source=true] alpha_eq_refl}.›
using assms
by (simp add: fdisjnt_alt_def closed_except_def term_to_nterm_alpha_equiv0)

end

global_interpretation nrelated: term_struct_rel_strong "(λt n. t = nterm_to_term Γ n)" for Γ
proof (standard, goal_cases)
  case (5 name t)
  then show ?case by (cases t) (auto simp: const_term_def const_nterm_def split: option.splits)
next
  case (6 u1 u2 t)
  then show ?case by (cases t) (auto simp: app_term_def app_nterm_def split: option.splits)
qed (auto simp: const_term_def const_nterm_def app_term_def app_nterm_def)

lemma env_nrelated_closed:
  assumes "nrelated.P_env Γ env nenv" "closed_env nenv"
  shows "nrelated.P_env Γ' env nenv"
proof
  fix x
  from assms have "rel_option (λt n. t = nterm_to_term Γ n) (fmlookup env x) (fmlookup nenv x)"
    by auto
  thus "rel_option (λt n. t = nterm_to_term Γ' n) (fmlookup env x) (fmlookup nenv x)"
    using assms
    by (cases rule: option.rel_cases) (auto dest: fmdomI simp: nterm_to_term_eq_closed)
qed

lemma nrelated_subst:
  assumes "nrelated.P_env Γ env nenv" "closed_env nenv" "fdisjnt (fset_of_list Γ) (fmdom nenv)"
  shows "subst (nterm_to_term Γ t) env = nterm_to_term Γ (subst t nenv)"
using assms
proof (induction t arbitrary: Γ env nenv)
  case (Nvar name)
  thus ?case
    proof (cases rule: fmrel_cases[where x = name])
      case (some t1 t2)
      with Nvar have "name |∉| fset_of_list Γ"
        unfolding fdisjnt_alt_def by (auto dest: fmdomI)
      hence "find_first name Γ = None"
        including fset.lifting by transfer' (simp add: find_first_none)
      with some show ?thesis
        by auto
    qed (auto split: option.splits)
next
  case (Nabs x t)
  show ?case
    apply simp
    apply (subst subst_drop[symmetric, where x = x])
    subgoal by simp
    apply (rule Nabs)
    using Nabs unfolding fdisjnt_alt_def
    by (auto intro: env_nrelated_closed)
qed auto

lemma nterm_to_term_insert_dupl:
  assumes "y  set (take n Γ)" "n  length Γ"
  shows "nterm_to_term Γ t = incr_bounds (- 1) (Suc n) (nterm_to_term (insert_nth n y Γ) t)"
using assms
proof (induction t arbitrary: n Γ)
  case (Nvar name)
  show ?case
    proof (cases "y = name")
      case True
      with Nvar obtain i where "find_first name Γ = Some i" "i < n"
        by (auto elim: find_first_some_strong)

      hence "find_first name (take n Γ) = Some i"
        by (rule find_first_prefix)

      show ?thesis
        apply simp
        apply (subst ‹find_first name Γ = Some i)
        apply simp
        apply (subst find_first_append)
        apply (subst ‹find_first name (take n Γ) = Some i)
        apply simp
        using i < n by simp
    next
      case False
      show ?thesis
        apply (simp del: insert_nth_take_drop)
        apply (subst find_first_insert_nth_neq)
        subgoal using False by simp
        by (cases "find_first name Γ") auto
    qed
next
  case (Nabs x t)
  show ?case
    apply simp
    apply (subst Nabs(1)[where n = "Suc n"])
    using Nabs by auto
qed auto

lemma nterm_to_term_bounds_dupl:
  assumes "i < length Γ" "j < length Γ" "i < j"
  assumes "Γ ! i = Γ ! j"
  shows "j |∉| bounds (nterm_to_term Γ t)"
using assms
proof (induction t arbitrary: Γ i j)
  case (Nvar name)
  show ?case
    proof (cases "find_first name Γ")
      case (Some k)
      show ?thesis
        proof
          assume "j |∈| bounds (nterm_to_term Γ (Nvar name))"
          with Some have "find_first name Γ = Some j"
            by simp

          moreover have "find_first name Γ  Some j"
            proof (rule find_first_later)
              show "i < length Γ" "j < length Γ" "i < j"
                by fact+
            next
              show "Γ ! j = name"
                by (rule find_first_correct) fact
              thus "Γ ! i = name"
                using Nvar by simp
            qed

          ultimately show False
            by blast
        qed
    qed simp
next
  case (Nabs x t)
  show ?case
    proof
      assume "j |∈| bounds (nterm_to_term Γ (Λn x. t))"
      then obtain j' where "j' |∈| bounds (nterm_to_term (x # Γ) t)" "j' > 0" "j = j' - 1"
        by auto
      hence "Suc j |∈| bounds (nterm_to_term (x # Γ) t)"
        by simp

      moreover have "Suc j |∉| bounds (nterm_to_term (x # Γ) t)"
        proof (rule Nabs)
          show "Suc i < length (x # Γ)" "Suc j < length (x # Γ)" "Suc i < Suc j" "(x # Γ) ! Suc i = (x # Γ) ! Suc j"
            using Nabs by simp+
        qed

      ultimately show False
        by blast
    qed
  qed auto

fun subst_single :: "nterm  name  nterm  nterm" where
"subst_single (Nvar s) s' t' = (if s = s' then t' else Nvar s)" |
"subst_single (t1 $n t2) s' t' = subst_single t1 s' t' $n subst_single t2 s' t'" |
"subst_single (Λn x. t) s' t' = (Λn x. (if x = s' then t else subst_single t s' t'))" |
"subst_single t _ _ = t"

lemma subst_single_eq: "subst_single t s t' = subst t (fmap_of_list [(s, t')])"
proof (induction t)
  case (Nabs x t)
  then show ?case
    by (cases "x = s") (simp add: fmfilter_alt_defs)+
qed auto

lemma nterm_to_term_subst_replace_bound:
  assumes "closed u'" "n  length Γ" "x  set (take n Γ)"
  shows "nterm_to_term Γ (subst_single u x u') = replace_bound n (nterm_to_term (insert_nth n x Γ) u) (nterm_to_term Γ u')"
using assms
proof (induction u arbitrary: n Γ)
  case (Nvar name)
  note insert_nth_take_drop[simp del]
  show ?case
    proof (cases "name = x")
      case True
      thus ?thesis
        using Nvar
        apply (simp add: find_first_insert_nth_eq)
        apply (subst incr_bounds_eq[where k = 0])
        subgoal by simp
        apply (rule nterm_to_term_closed_wellformed)
        by auto
    next
      case False
      thus ?thesis
        apply auto
        apply (subst find_first_insert_nth_neq)
        subgoal by simp
        by (cases "find_first name Γ") auto
    qed
next
  case (Nabs y t)
  note insert_nth_take_drop[simp del]
  show ?case
    proof (cases "x = y")
      case True
      have "nterm_to_term (y # Γ) t = replace_bound (Suc n) (nterm_to_term (y # insert_nth n y Γ) t) (nterm_to_term Γ u')"
        proof (subst replace_bound_eq)
          show "Suc n |∉| bounds (nterm_to_term (y # insert_nth n y Γ) t)"
            apply (rule nterm_to_term_bounds_dupl[where i = 0])
            subgoal by simp
            subgoal using Nabs(3) by (simp add: insert_nth_take_drop)
            subgoal by simp
            apply simp
            apply (subst nth_insert_nth_index_eq)
            using Nabs by auto
          show "nterm_to_term (y # Γ) t = incr_bounds (- 1) (Suc n + 1) (nterm_to_term (y # insert_nth n y Γ) t)"
            apply (subst nterm_to_term_insert_dupl[where Γ = "y # Γ" and y = y and n = "Suc n"])
            using Nabs by auto
        qed
      with True show ?thesis
        by auto
    next
      case False
      have "nterm_to_term (y # Γ) (subst_single t x u') = replace_bound (Suc n) (nterm_to_term (y # insert_nth n x Γ) t) (nterm_to_term Γ u')"
        apply (subst Nabs(1)[of "Suc n"])
        subgoal by fact
        subgoal using Nabs by simp
        subgoal using False Nabs by simp
        apply (subst nterm_to_term_eq_closed[where t = u'])
        using Nabs by auto
      with False show ?thesis
        by auto
    qed
qed auto

corollary nterm_to_term_subst_β:
  assumes "closed u'"
  shows "nterm_to_term Γ (subst u (fmap_of_list [(x, u')])) = nterm_to_term (x # Γ) u [nterm_to_term Γ u']β"
using assms
by (rule nterm_to_term_subst_replace_bound[where n = 0, simplified, unfolded subst_single_eq])

end

Theory Unification_Compat

chapter ‹Instantiation for HOL-ex.Unification› from session HOL-ex›

theory Unification_Compat
imports
  "HOL-ex.Unification"
  Term_Class
begin

text ‹
  The Isabelle library provides a unification algorithm on lambda-free terms. To illustrate
  flexibility of the term algebra, I instantiate my class with that term type. The major issue is
  that those terms are parameterized over the constant and variable type, which cannot easily be
  supported by the classy approach, where those types are fixed to @{typ name}. As a workaround, I
  introduce a class that requires the constant and variable type to be isomorphic to @{typ name}.
›

hide_const (open) Unification.subst

class is_name =
  fixes of_name :: "name  'a"
  assumes bij: "bij of_name"
begin

definition to_name :: "'a  name" where
"to_name = inv of_name"

lemma to_of_name[simp]: "to_name (of_name a) = a"
unfolding to_name_def using bij by (metis bij_inv_eq_iff)

lemma of_to_name[simp]: "of_name (to_name a) = a"
unfolding to_name_def using bij by (meson bij_inv_eq_iff)

lemma of_name_inj: "of_name name1 = of_name name2  name1 = name2"
using bij by (metis to_of_name)

end

instantiation name :: is_name begin

definition of_name_name :: "name  name" where
[code_unfold]: "of_name_name x = x"

instance by standard (auto simp: of_name_name_def bij_betw_def inj_on_def)

end

lemma [simp, code_unfold]: "(to_name :: name  name) = id"
unfolding to_name_def of_name_name_def by auto

instantiation trm :: (is_name) "pre_term" begin

definition app_trm where
"app_trm = Comb"

definition unapp_trm where
"unapp_trm t = (case t of Comb t u  Some (t, u) | _  None)"

definition const_trm where
"const_trm n = trm.Const (of_name n)"

definition unconst_trm where
"unconst_trm t = (case t of trm.Const a  Some (to_name a) | _  None)"

definition free_trm where
"free_trm n = Var (of_name n)"

definition unfree_trm where
"unfree_trm t = (case t of Var a  Some (to_name a) | _  None)"

primrec consts_trm :: "'a trm  name fset" where
"consts_trm (Var _) = {||}" |
"consts_trm (trm.Const c) = {| to_name c |}" |
"consts_trm (M  N) = consts_trm M |∪| consts_trm N"

context
  includes fset.lifting
begin

lift_definition frees_trm :: "'a trm  name fset" is "λt. to_name ` vars_of t"
  by auto

end

lemma frees_trm[code, simp]:
  "frees (Var v) = {| to_name v |}"
  "frees (trm.Const c) = {||}"
  "frees (M  N) = frees M |∪| frees N"
including fset.lifting
by (transfer; auto)+

primrec subst_trm :: "'a trm  (name, 'a trm) fmap  'a trm" where
"subst_trm (Var v) env = (case fmlookup env (to_name v) of Some v'  v' | _  Var v)" |
"subst_trm (trm.Const c) _ = trm.Const c" |
"subst_trm (M  N) env = subst_trm M env  subst_trm N env"

instance
by standard
   (auto
      simp: app_trm_def unapp_trm_def const_trm_def unconst_trm_def free_trm_def unfree_trm_def of_name_inj
      split: trm.splits option.splits)

end

instantiation trm :: (is_name) "term" begin

definition abs_pred_trm :: "('a trm  bool)  'a trm  bool" where
"abs_pred_trm P t  True"

instance proof (standard, goal_cases)
  case (1 P t)
  then show ?case
    proof (induction t)
      case Var
      then show ?case
        unfolding free_trm_def
        by (metis of_to_name)
    next
      case Const
      then show ?case
        unfolding const_trm_def
        by (metis of_to_name)
    qed (auto simp: app_trm_def)
qed (auto simp: abs_pred_trm_def)

end

lemma assoc_alt_def[simp]:
  "assoc x y t = (case map_of t x of Some y'  y' | _  y)"
by (induction t) auto

lemma subst_eq: "Unification.subst t s = subst t (fmap_of_list s)"
by (induction t) (auto split: option.splits simp: fmlookup_of_list)

end

Theory Lambda_Free_Compat

chapter ‹Instantiation for λ›-free terms according to Blanchette›

theory Lambda_Free_Compat
imports Unification_Compat "Lambda_Free_RPOs.Lambda_Free_Term"
begin

text ‹
  Another instantiation of the algebra for Blanchette et al.'s term type
  @{cite blanchette2016lambda}.
›

hide_const (open) Lambda_Free_Term.subst

instantiation tm :: (is_name, is_name) "pre_term" begin

definition app_tm where
"app_tm = tm.App"

definition unapp_tm where
"unapp_tm t = (case t of App t u  Some (t, u) | _  None)"

definition const_tm where
"const_tm n = Hd (Sym (of_name n))"

definition unconst_tm where
"unconst_tm t = (case t of Hd (Sym a)  Some (to_name a) | _  None)"

definition free_tm where
"free_tm n = Hd (Var (of_name n))"

definition unfree_tm where
"unfree_tm t = (case t of Hd (Var a)  Some (to_name a) | _  None)"

context
  includes fset.lifting
begin

lift_definition frees_tm :: "('a, 'b) tm  name fset" is "λt. to_name ` vars t"
  by auto

lift_definition consts_tm :: "('a, 'b) tm  name fset" is "λt. to_name ` syms t"
  by auto

end

lemma frees_tm[code, simp]:
  "frees (App f x) = frees f |∪| frees x"
  "frees (Hd h) = (case h of Sym _  fempty | Var v  {| to_name v |})"
including fset.lifting
by (transfer; auto split: hd.splits)+

lemma consts_tm[code, simp]:
  "consts (App f x) = consts f |∪| consts x"
  "consts (Hd h) = (case h of Var _  fempty | Sym v  {| to_name v |})"
including fset.lifting
by (transfer; auto split: hd.splits)+

definition subst_tm :: "('a, 'b) tm  (name, ('a, 'b) tm) fmap  ('a, 'b) tm" where
"subst_tm t env =
  Lambda_Free_Term.subst (fmlookup_default env (Hd  Var  of_name)  to_name) t"

lemma subst_tm[code, simp]:
  "subst (App t u) env = App (subst t env) (subst u env)"
  "subst (Hd h) env = (case h of
    Sym s  Hd (Sym s) |
    Var x  (case fmlookup env (to_name x) of
      Some t'  t'
    | None  Hd (Var x)))"
unfolding subst_tm_def
by (auto simp: fmlookup_default_def split: hd.splits option.splits)

instance
by standard
   (auto
      simp: app_tm_def unapp_tm_def const_tm_def unconst_tm_def free_tm_def unfree_tm_def of_name_inj
      split: tm.splits hd.splits option.splits)

end

instantiation tm :: (is_name, is_name) "term" begin

definition abs_pred_tm :: "(('a, 'b) tm  bool)  ('a, 'b) tm  bool" where
"abs_pred_tm P t  True"

instance proof (standard, goal_cases)
  case (1 P t)
  then show ?case
    proof (induction t)
      case (Hd h)
      then show ?case
        apply (cases h)
        apply (auto simp: free_tm_def const_tm_def)
        apply (metis of_to_name)+
        done
    qed (auto simp: app_tm_def)
qed (auto simp: abs_pred_tm_def)

end

lemma apps_list_comb: "apps f xs = list_comb f xs"
by (induction xs arbitrary: f) (auto simp: app_tm_def)

end