Theory Messages

(*  Title:      Messages.thy
    Author:     Andreas Viktor Hess, DTU
    SPDX-License-Identifier: BSD-3-Clause
*)

section ‹Protocol Messages as (First-Order) Terms›

theory Messages
  imports Miscellaneous "First_Order_Terms.Term"
begin

subsection ‹Term-related definitions: subterms and free variables›
abbreviation "the_Fun ≡ un_Fun1"
lemmas the_Fun_def = un_Fun1_def

fun subterms::"('a,'b) term ⇒ ('a,'b) terms" where
  "subterms (Var x) = {Var x}"
| "subterms (Fun f T) = {Fun f T} ∪ (⋃t ∈ set T. subterms t)"

abbreviation subtermeq (infix "⊑" 50) where "t' ⊑ t ≡ (t' ∈ subterms t)"
abbreviation subterm (infix "⊏" 50) where "t' ⊏ t ≡ (t' ⊑ t ∧ t' ≠ t)"

abbreviation "subterms⇩s⇩e⇩t M ≡ ⋃(subterms ` M)"
abbreviation subtermeqset (infix "⊑⇩s⇩e⇩t" 50) where "t ⊑⇩s⇩e⇩t M ≡ (t ∈ subterms⇩s⇩e⇩t M)"

abbreviation fv where "fv ≡ vars_term"
lemmas fv_simps = term.simps(17,18)

fun fv⇩s⇩e⇩t where "fv⇩s⇩e⇩t M = ⋃(fv ` M)"

abbreviation fv⇩p⇩a⇩i⇩r where "fv⇩p⇩a⇩i⇩r p ≡ case p of (t,t') ⇒ fv t ∪ fv t'"

fun fv⇩p⇩a⇩i⇩r⇩s where "fv⇩p⇩a⇩i⇩r⇩s F = ⋃(fv⇩p⇩a⇩i⇩r ` set F)"

abbreviation ground where "ground M ≡ fv⇩s⇩e⇩t M = {}"


subsection ‹Variants that return lists insteads of sets›
fun fv_list where
  "fv_list (Var x) = [x]"
| "fv_list (Fun f T) = concat (map fv_list T)"

definition fv_list⇩p⇩a⇩i⇩r⇩s where
  "fv_list⇩p⇩a⇩i⇩r⇩s F ≡ concat (map (λ(t,t'). fv_list t@fv_list t') F)"

fun subterms_list::"('a,'b) term ⇒ ('a,'b) term list" where
  "subterms_list (Var x) = [Var x]"
| "subterms_list (Fun f T) = remdups (Fun f T#concat (map subterms_list T))"

lemma fv_list_is_fv: "fv t = set (fv_list t)"
by (induct t) auto

lemma fv_list⇩p⇩a⇩i⇩r⇩s_is_fv⇩p⇩a⇩i⇩r⇩s: "fv⇩p⇩a⇩i⇩r⇩s F = set (fv_list⇩p⇩a⇩i⇩r⇩s F)"
by (induct F) (auto simp add: fv_list_is_fv fv_list⇩p⇩a⇩i⇩r⇩s_def)

lemma subterms_list_is_subterms: "subterms t = set (subterms_list t)"
by (induct t) auto


subsection ‹The subterm relation defined as a function›
fun subterm_of where
  "subterm_of t (Var y) = (t = Var y)"
| "subterm_of t (Fun f T) = (t = Fun f T ∨ list_ex (subterm_of t) T)"

lemma subterm_of_iff_subtermeq[code_unfold]: "t ⊑ t' = subterm_of t t'"
proof (induction t')
  case (Fun f T) thus ?case
  proof (cases "t = Fun f T")
    case False thus ?thesis
      using Fun.IH subterm_of.simps(2)[of t f T]
      unfolding list_ex_iff by fastforce
  qed simp
qed simp

lemma subterm_of_ex_set_iff_subtermeqset[code_unfold]: "t ⊑⇩s⇩e⇩t M = (∃t' ∈ M. subterm_of t t')"
using subterm_of_iff_subtermeq by blast


subsection ‹The subterm relation is a partial order on terms›
interpretation "term": order "(⊑)" "(⊏)"
proof
  show "s ⊑ s" for s :: "('a,'b) term"
    by (induct s rule: subterms.induct) auto

  show trans: "s ⊑ t ⟹ t ⊑ u ⟹ s ⊑ u" for s t u :: "('a,'b) term"
    by (induct u rule: subterms.induct) auto

  show "s ⊑ t ⟹ t ⊑ s ⟹ s = t" for s t :: "('a,'b) term"
  proof (induction s arbitrary: t rule: subterms.induct[case_names Var Fun])
    case (Fun f T)
    { assume 0: "t ≠ Fun f T"
      then obtain u::"('a,'b) term" where u: "u ∈ set T" "t ⊑ u" using Fun.prems(2) by auto
      hence 1: "Fun f T ⊑ u" using trans[OF Fun.prems(1)] by simp
   
      have 2: "u ⊑ Fun f T"
        by (cases u) (use u(1) in force, use u(1) subterms.simps(2)[of f T] in fastforce)
      hence 3: "u = Fun f T" using Fun.IH[OF u(1) _ 1] by simp

      have "u ⊑ t" using trans[OF 2 Fun.prems(1)] by simp
      hence 4: "u = t" using Fun.IH[OF u(1) _ u(2)] by simp
  
      have "t = Fun f T" using 3 4 by simp
      hence False using 0 by simp
    }
    thus ?case by auto
  qed simp
  thus "(s ⊏ t) = (s ⊑ t ∧ ¬(t ⊑ s))" for s t :: "('a,'b) term"
    by blast
qed


subsection ‹Lemmata concerning subterms and free variables›
lemma fv_list⇩p⇩a⇩i⇩r⇩s_append: "fv_list⇩p⇩a⇩i⇩r⇩s (F@G) = fv_list⇩p⇩a⇩i⇩r⇩s F@fv_list⇩p⇩a⇩i⇩r⇩s G"
by (simp add: fv_list⇩p⇩a⇩i⇩r⇩s_def)

lemma distinct_fv_list_idx_fv_disjoint:
  assumes t: "distinct (fv_list t)" "Fun f T ⊑ t"
    and ij: "i < length T" "j < length T" "i < j"
  shows "fv (T ! i) ∩ fv (T ! j) = {}"
using t
proof (induction t rule: fv_list.induct)
  case (2 g S)
  have "distinct (fv_list s)" when s: "s ∈ set S" for s
    by (metis (no_types, lifting) s "2.prems"(1) concat_append distinct_append 
          map_append split_list fv_list.simps(2) concat.simps(2) list.simps(9))
  hence IH: "fv (T ! i) ∩ fv (T ! j) = {}"
    when s: "s ∈ set S" "Fun f T ⊑ s" for s
    using "2.IH" s by blast

  show ?case
  proof (cases "Fun f T = Fun g S")
    case True
    define U where "U ≡ map fv_list T"

    have a: "distinct (concat U)"
      using "2.prems"(1) True unfolding U_def by auto
    
    have b: "i < length U" "j < length U"
      using ij(1,2) unfolding U_def by simp_all

    show ?thesis
      using b distinct_concat_idx_disjoint[OF a b ij(3)]
            fv_list_is_fv[of "T ! i"] fv_list_is_fv[of "T ! j"]
      unfolding U_def by force
  qed (use IH "2.prems"(2) in auto)
qed force

lemma distinct_fv_list_Fun_param:
  assumes f: "distinct (fv_list (Fun f ts))"
    and t: "t ∈ set ts"
  shows "distinct (fv_list t)"
proof -
  obtain pre suf where "ts = pre@t#suf" using t by (meson split_list)
  thus ?thesis using distinct_append f by simp
qed

lemmas subtermeqI'[intro] = term.eq_refl

lemma subtermeqI''[intro]: "t ∈ set T ⟹ t ⊑ Fun f T"
by force

lemma finite_fv_set[intro]: "finite M ⟹ finite (fv⇩s⇩e⇩t M)"
by auto

lemma finite_fun_symbols[simp]: "finite (funs_term t)"
by (induct t) simp_all

lemma fv_set_mono: "M ⊆ N ⟹ fv⇩s⇩e⇩t M ⊆ fv⇩s⇩e⇩t N"
by auto

lemma subterms⇩s⇩e⇩t_mono: "M ⊆ N ⟹ subterms⇩s⇩e⇩t M ⊆ subterms⇩s⇩e⇩t N"
by auto

lemma ground_empty[simp]: "ground {}"
by simp

lemma ground_subset: "M ⊆ N ⟹ ground N ⟹ ground M"
by auto

lemma fv_map_fv_set: "⋃(set (map fv L)) = fv⇩s⇩e⇩t (set L)"
by (induct L) auto

lemma fv⇩s⇩e⇩t_union: "fv⇩s⇩e⇩t (M ∪ N) = fv⇩s⇩e⇩t M ∪ fv⇩s⇩e⇩t N"
by auto

lemma finite_subset_Union:
  fixes A::"'a set" and f::"'a ⇒ 'b set"
  assumes "finite (⋃a ∈ A. f a)"
  shows "∃B. finite B ∧ B ⊆ A ∧ (⋃b ∈ B. f b) = (⋃a ∈ A. f a)"
by (metis assms eq_iff finite_subset_image finite_UnionD)

lemma inv_set_fv: "finite M ⟹ ⋃(set (map fv (inv set M))) = fv⇩s⇩e⇩t M"
using fv_map_fv_set[of "inv set M"] inv_set_fset by auto

lemma ground_subterm: "fv t = {} ⟹ t' ⊑ t ⟹ fv t' = {}" by (induct t) auto

lemma empty_fv_not_var: "fv t = {} ⟹ t ≠ Var x" by auto

lemma empty_fv_exists_fun: "fv t = {} ⟹ ∃f X. t = Fun f X" by (cases t) auto

lemma vars_iff_subtermeq: "x ∈ fv t ⟷ Var x ⊑ t" by (induct t) auto

lemma vars_iff_subtermeq_set: "x ∈ fv⇩s⇩e⇩t M ⟷ Var x ∈ subterms⇩s⇩e⇩t M"
using vars_iff_subtermeq[of x] by auto

lemma vars_if_subtermeq_set: "Var x ∈ subterms⇩s⇩e⇩t M ⟹ x ∈ fv⇩s⇩e⇩t M"
by (metis vars_iff_subtermeq_set)

lemma subtermeq_set_if_vars: "x ∈ fv⇩s⇩e⇩t M ⟹ Var x ∈ subterms⇩s⇩e⇩t M"
by (metis vars_iff_subtermeq_set)

lemma vars_iff_subterm_or_eq: "x ∈ fv t ⟷ Var x ⊏ t ∨ Var x = t"
by (induct t) (auto simp add: vars_iff_subtermeq)

lemma var_is_subterm: "x ∈ fv t ⟹ Var x ∈ subterms t"
by (simp add: vars_iff_subtermeq)

lemma subterm_is_var: "Var x ∈ subterms t ⟹ x ∈ fv t"
by (simp add: vars_iff_subtermeq)

lemma no_var_subterm: "¬t ⊏ Var v" by auto

lemma fun_if_subterm: "t ⊏ u ⟹ ∃f X. u = Fun f X" by (induct u) simp_all

lemma subtermeq_vars_subset: "M ⊑ N ⟹ fv M ⊆ fv N" by (induct N) auto

lemma fv_subterms[simp]: "fv⇩s⇩e⇩t (subterms t) = fv t"
by (induct t) auto

lemma fv_subterms_set[simp]: "fv⇩s⇩e⇩t (subterms⇩s⇩e⇩t M) = fv⇩s⇩e⇩t M"
using subtermeq_vars_subset by auto

lemma fv_subset: "t ∈ M ⟹ fv t ⊆ fv⇩s⇩e⇩t M"
by auto

lemma fv_subset_subterms: "t ∈ subterms⇩s⇩e⇩t M ⟹ fv t ⊆ fv⇩s⇩e⇩t M"
using fv_subset fv_subterms_set by metis

lemma subterms_finite[simp]: "finite (subterms t)" by (induction rule: subterms.induct) auto

lemma subterms_union_finite: "finite M ⟹ finite (⋃t ∈ M. subterms t)"
by (induction rule: subterms.induct) auto

lemma subterms_subset: "t' ⊑ t ⟹ subterms t' ⊆ subterms t"
by (induction rule: subterms.induct) auto

lemma subterms_subset_set: "M ⊆ subterms t ⟹ subterms⇩s⇩e⇩t M ⊆ subterms t"
by (metis SUP_least contra_subsetD subterms_subset)

lemma subset_subterms_Union[simp]: "M ⊆ subterms⇩s⇩e⇩t M" by auto

lemma in_subterms_Union: "t ∈ M ⟹ t ∈ subterms⇩s⇩e⇩t M" using subset_subterms_Union by blast

lemma in_subterms_subset_Union: "t ∈ subterms⇩s⇩e⇩t M ⟹ subterms t ⊆ subterms⇩s⇩e⇩t M"
using subterms_subset by auto

lemma subterm_param_split: 
  assumes "t ⊏ Fun f X"
  shows "∃pre x suf. t ⊑ x ∧ X = pre@x#suf"
proof -
  obtain x where "t ⊑ x" "x ∈ set X" using assms by auto
  then obtain pre suf where "X = pre@x#suf" "x ∉ set pre ∨ x ∉ set suf"
    by (meson split_list_first split_list_last)
  thus ?thesis using ‹t ⊑ x› by auto
qed

lemma ground_iff_no_vars: "ground (M::('a,'b) terms) ⟷ (∀v. Var v ∉ (⋃m ∈ M. subterms m))"
proof
  assume "ground M"
  hence "∀v. ∀m ∈ M. v ∉ fv m" by auto
  hence "∀v. ∀m ∈ M. Var v ∉ subterms m" by (simp add: vars_iff_subtermeq)
  thus "(∀v. Var v ∉ (⋃m ∈ M. subterms m))" by simp
next
  assume no_vars: "∀v. Var v ∉ (⋃m ∈ M. subterms m)"
  moreover
  { assume "¬ground M"
    then obtain v and m::"('a,'b) term" where "m ∈ M" "fv m ≠ {}" "v ∈ fv m" by auto
    hence "Var v ∈ (subterms m)" by (simp add: vars_iff_subtermeq)
    hence "∃v. Var v ∈ (⋃t ∈ M. subterms t)" using ‹m ∈ M› by auto
    hence False using no_vars by simp
  }
  ultimately show "ground M" by blast
qed

lemma index_Fun_subterms_subset[simp]: "i < length T ⟹ subterms (T ! i) ⊆ subterms (Fun f T)"
by auto

lemma index_Fun_fv_subset[simp]: "i < length T ⟹ fv (T ! i) ⊆ fv (Fun f T)"
using subtermeq_vars_subset by fastforce

lemma subterms_union_ground:
  assumes "ground M"
  shows "ground (subterms⇩s⇩e⇩t M)"
proof -
  { fix t assume "t ∈ M"
    hence "fv t = {}"
      using ground_iff_no_vars[of M] assms
      by auto
    hence "∀t' ∈ subterms t. fv t' = {}" using subtermeq_vars_subset[of _ t] by simp
    hence "ground (subterms t)" by auto
  }
  thus ?thesis by auto
qed

lemma Var_subtermeq: "t ⊑ Var v ⟹ t = Var v" by simp

lemma subtermeq_imp_funs_term_subset: "s ⊑ t ⟹ funs_term s ⊆ funs_term t"
by (induct t arbitrary: s) auto

lemma subterms_const: "subterms (Fun f []) = {Fun f []}" by simp

lemma subterm_subtermeq_neq: "⟦t ⊏ u; u ⊑ v⟧ ⟹ t ≠ v"
  using term.dual_order.strict_trans1 by blast 

lemma subtermeq_subterm_neq: "⟦t ⊑ u; u ⊏ v⟧ ⟹ t ≠ v"
by (metis term.order.eq_iff)

lemma subterm_size_lt: "x ⊏ y ⟹ size x < size y"
using not_less_eq size_list_estimation by (induct y, simp, fastforce)

lemma in_subterms_eq: "⟦x ∈ subterms y; y ∈ subterms x⟧ ⟹ subterms x = subterms y"
  using term.order.antisym by auto

lemma Fun_param_size_lt:
  "t ∈ set ts ⟹ size t < size (Fun f ts)"
by (induct ts) auto

lemma Fun_zip_size_lt:
  assumes "(t,s) ∈ set (zip ts ss)"
  shows "size t < size (Fun f ts)"
    and "size s < size (Fun g ss)"
by (metis assms Fun_param_size_lt in_set_zipE)+

lemma Fun_gt_params: "Fun f X ∉ (⋃x ∈ set X. subterms x)"
proof -
  have "size_list size X < size (Fun f X)" by simp
  hence "Fun f X ∉ set X" by (meson less_not_refl size_list_estimation) 
  hence "∀x ∈ set X. Fun f X ∉ subterms x ∨ x ∉ subterms (Fun f X)"
    using subtermeq_subterm_neq by blast 
  moreover have "∀x ∈ set X. x ∈ subterms (Fun f X)" by fastforce
  ultimately show ?thesis by auto
qed

lemma params_subterms[simp]: "set X ⊆ subterms (Fun f X)" by auto

lemma params_subterms_Union[simp]: "subterms⇩s⇩e⇩t (set X) ⊆ subterms (Fun f X)" by auto

lemma Fun_subterm_inside_params: "t ⊏ Fun f X ⟷ t ∈ (⋃x ∈ (set X). subterms x)"
using Fun_gt_params by fastforce

lemma Fun_param_is_subterm: "x ∈ set X ⟹ x ⊏ Fun f X"
using Fun_subterm_inside_params by fastforce

lemma Fun_param_in_subterms: "x ∈ set X ⟹ x ∈ subterms (Fun f X)"
using Fun_subterm_inside_params by fastforce

lemma Fun_not_in_param: "x ∈ set X ⟹ ¬Fun f X ⊏ x"
  by (meson Fun_param_in_subterms term.less_le_not_le) 

lemma Fun_ex_if_subterm: "t ⊏ s ⟹ ∃f T. Fun f T ⊑ s ∧ t ∈ set T"
proof (induction s)
  case (Fun f T)
  then obtain s' where s': "s' ∈ set T" "t ⊑ s'" by auto
  show ?case
  proof (cases "t = s'")
    case True thus ?thesis using s' by blast
  next
    case False
    thus ?thesis
      using Fun.IH[OF s'(1)] s'(2) term.order_trans[OF _ Fun_param_in_subterms[OF s'(1), of f]]
      by metis
  qed
qed simp

lemma const_subterm_obtain:
  assumes "fv t = {}"
  obtains c where "Fun c [] ⊑ t"
using assms
proof (induction t)
  case (Fun f T) thus ?case by (cases "T = []") force+
qed simp

lemma const_subterm_obtain': "fv t = {} ⟹ ∃c. Fun c [] ⊑ t"
by (metis const_subterm_obtain)

lemma subterms_singleton:
  assumes "(∃v. t = Var v) ∨ (∃f. t = Fun f [])"
  shows "subterms t = {t}"
using assms by (cases t) auto

lemma subtermeq_Var_const:
  assumes "s ⊑ t"
  shows "t = Var v ⟹ s = Var v" "t = Fun f [] ⟹ s = Fun f []"
using assms by fastforce+

lemma subterms_singleton':
  assumes "subterms t = {t}"
  shows "(∃v. t = Var v) ∨ (∃f. t = Fun f [])"
proof (cases t)
  case (Fun f T)
  { fix s S assume "T = s#S"
    hence "s ∈ subterms t" using Fun by auto
    hence "s = t" using assms by auto
    hence False
      using Fun_param_is_subterm[of s "s#S" f] ‹T = s#S› Fun
      by auto
  }
  hence "T = []" by (cases T) auto
  thus ?thesis using Fun by simp
qed (simp add: assms)

lemma funs_term_subterms_eq[simp]:
  "(⋃s ∈ subterms t. funs_term s) = funs_term t" 
  "(⋃s ∈ subterms⇩s⇩e⇩t M. funs_term s) = ⋃(funs_term ` M)"
proof -
  show "⋀t. ⋃(funs_term ` subterms t) = funs_term t"
    using term.order_refl subtermeq_imp_funs_term_subset by blast
  thus "⋃(funs_term ` (subterms⇩s⇩e⇩t M)) = ⋃(funs_term ` M)" by force
qed

lemmas subtermI'[intro] = Fun_param_is_subterm

lemma funs_term_Fun_subterm: "f ∈ funs_term t ⟹ ∃T. Fun f T ∈ subterms t"
proof (induction t)
  case (Fun g T)
  hence "f = g ∨ (∃s ∈ set T. f ∈ funs_term s)" by simp
  thus ?case
  proof
    assume "∃s ∈ set T. f ∈ funs_term s"
    then obtain s where "s ∈ set T" "∃T. Fun f T ∈ subterms s" using Fun.IH by auto
    thus ?thesis by auto
  qed (auto simp add: Fun)
qed simp

lemma funs_term_Fun_subterm': "Fun f T ∈ subterms t ⟹ f ∈ funs_term t"
by (induct t) auto

lemma zip_arg_subterm:
  assumes "(s,t) ∈ set (zip X Y)"
  shows "s ⊏ Fun f X" "t ⊏ Fun g Y"
proof -
  from assms have *: "s ∈ set X" "t ∈ set Y" by (meson in_set_zipE)+
  show "s ⊏ Fun f X" by (metis Fun_param_is_subterm[OF *(1)])
  show "t ⊏ Fun g Y" by (metis Fun_param_is_subterm[OF *(2)])
qed

lemma fv_disj_Fun_subterm_param_cases:
  assumes "fv t ∩ X = {}" "Fun f T ∈ subterms t"
  shows "T = [] ∨ (∃s∈set T. s ∉ Var ` X)"
proof (cases T)
  case (Cons s S)
  hence "s ∈ subterms t"
    using assms(2) term.order_trans[of _ "Fun f T" t]
    by auto
  hence "fv s ∩ X = {}" using assms(1) fv_subterms by force
  thus ?thesis using Cons by auto
qed simp

lemma fv_eq_FunI:
  assumes "length T = length S" "⋀i. i < length T ⟹ fv (T ! i) = fv (S ! i)"
  shows "fv (Fun f T) = fv (Fun g S)"
using assms
proof (induction T arbitrary: S)
  case (Cons t T S')
  then obtain s S where S': "S' = s#S" by (cases S') simp_all
  have "fv (T ! i) = fv (S ! i)" when "i < length T" for i
    using that Cons.prems(2)[of "Suc i"] unfolding S' by simp
  hence "fv (Fun f T) = fv (Fun g S)"
    using Cons.prems(1) Cons.IH[of S] unfolding S' by simp
  thus ?case using Cons.prems(2)[of 0] unfolding S' by auto
qed simp

lemma fv_eq_FunI':
  assumes "length T = length S" "⋀i. i < length T ⟹ x ∈ fv (T ! i) ⟷ x ∈ fv (S ! i)"
  shows "x ∈ fv (Fun f T) ⟷ x ∈ fv (Fun g S)"
using assms
proof (induction T arbitrary: S)
  case (Cons t T S')
  then obtain s S where S': "S' = s#S" by (cases S') simp_all
  show ?case using Cons.prems Cons.IH[of S] unfolding S' by fastforce
qed simp

lemma funs_term_eq_FunI:
  assumes "length T = length S" "⋀i. i < length T ⟹ funs_term (T ! i) = funs_term (S ! i)"
  shows "funs_term (Fun f T) = funs_term (Fun f S)"
using assms
proof (induction T arbitrary: S)
  case (Cons t T S')
  then obtain s S where S': "S' = s#S" by (cases S') simp_all
  have "funs_term (T ! i) = funs_term (S ! i)" when "i < length T" for i
    using that Cons.prems(2)[of "Suc i"] unfolding S' by simp
  hence "funs_term (Fun f T) = funs_term (Fun f S)"
    using Cons.prems(1) Cons.IH[of S] unfolding S' by simp
  thus ?case using Cons.prems(2)[of 0] unfolding S' by auto
qed simp

lemma finite_fv⇩p⇩a⇩i⇩r⇩s[simp]: "finite (fv⇩p⇩a⇩i⇩r⇩s x)" by auto

lemma fv⇩p⇩a⇩i⇩r⇩s_Nil[simp]: "fv⇩p⇩a⇩i⇩r⇩s [] = {}" by simp

lemma fv⇩p⇩a⇩i⇩r⇩s_singleton[simp]: "fv⇩p⇩a⇩i⇩r⇩s [(t,s)] = fv t ∪ fv s" by simp

lemma fv⇩p⇩a⇩i⇩r⇩s_Cons: "fv⇩p⇩a⇩i⇩r⇩s ((s,t)#F) = fv s ∪ fv t ∪ fv⇩p⇩a⇩i⇩r⇩s F" by simp

lemma fv⇩p⇩a⇩i⇩r⇩s_append: "fv⇩p⇩a⇩i⇩r⇩s (F@G) = fv⇩p⇩a⇩i⇩r⇩s F ∪ fv⇩p⇩a⇩i⇩r⇩s G" by simp

lemma fv⇩p⇩a⇩i⇩r⇩s_mono: "set M ⊆ set N ⟹ fv⇩p⇩a⇩i⇩r⇩s M ⊆ fv⇩p⇩a⇩i⇩r⇩s N" by auto

lemma fv⇩p⇩a⇩i⇩r⇩s_inI[intro]:
  "f ∈ set F ⟹ x ∈ fv⇩p⇩a⇩i⇩r f ⟹ x ∈ fv⇩p⇩a⇩i⇩r⇩s F"
  "f ∈ set F ⟹ x ∈ fv (fst f) ⟹ x ∈ fv⇩p⇩a⇩i⇩r⇩s F"
  "f ∈ set F ⟹ x ∈ fv (snd f) ⟹ x ∈ fv⇩p⇩a⇩i⇩r⇩s F"
  "(t,s) ∈ set F ⟹ x ∈ fv t ⟹ x ∈ fv⇩p⇩a⇩i⇩r⇩s F"
  "(t,s) ∈ set F ⟹ x ∈ fv s ⟹ x ∈ fv⇩p⇩a⇩i⇩r⇩s F"
using UN_I by fastforce+

lemma fv⇩p⇩a⇩i⇩r⇩s_cons_subset: "fv⇩p⇩a⇩i⇩r⇩s F ⊆ fv⇩p⇩a⇩i⇩r⇩s (f#F)"
by auto

lemma in_Fun_fv_iff_in_args_nth_fv:
  "x ∈ fv (Fun f ts) ⟷ (∃i < length ts. x ∈ fv (ts ! i))"
  (is "?A ⟷ ?B")
proof
  assume ?A
  hence "x ∈ ⋃(fv ` set ts)" by auto
  thus ?B by (metis UN_E in_set_conv_nth)
qed auto


subsection ‹Other lemmata›
lemma nonvar_term_has_composed_shallow_term:
  fixes t::"('f,'v) term"
  assumes "¬(∃x. t = Var x)"
  shows "∃f T. Fun f T ⊑ t ∧ (∀s ∈ set T. (∃c. s = Fun c []) ∨ (∃x. s = Var x))"
proof -
  let ?Q = "λS. ∀s ∈ set S. (∃c. s = Fun c []) ∨ (∃x. s = Var x)"
  let ?P = "λt. ∃g S. Fun g S ⊑ t ∧ ?Q S"
  { fix t::"('f,'v) term"
    have "(∃x. t = Var x) ∨ ?P t"
    proof (induction t)
      case (Fun h R) show ?case
      proof (cases "R = [] ∨ (∀r ∈ set R. ∃x. r = Var x)")
        case False
        then obtain r g S where "r ∈ set R" "?P r" "Fun g S ⊑ r" "?Q S" using Fun.IH by fast
        thus ?thesis by auto
      qed force
    qed simp
  } thus ?thesis using assms by blast
qed

end