Theory Syntax

chapter ‹Syntax›

(*<*)
theory Syntax
  imports Prelim
begin
(*>*)


section ‹Generic Syntax›

text ‹We develop some generic (meta-)axioms for syntax and substitution.
We only assume that the syntax of our logic has notions of variable, term and formula,
which \emph{include} subsets of "numeric" variables, terms and formulas,
the latter being endowed with notions of free variables and substitution subject to
some natural properties.›

locale Generic_Syntax =
  fixes
    var :: "'var set" ― ‹numeric variables (i.e., variables ranging over numbers)›
    and trm :: "'trm set" ― ‹numeric trms, which include the numeric variables›
    and fmla :: "'fmla set" ― ‹numeric formulas›
    and Var :: "'var ⇒ 'trm" ― ‹trms include at least the variables›
    and FvarsT :: "'trm ⇒ 'var set" ― ‹free variables for trms›
    and substT :: "'trm ⇒ 'trm ⇒ 'var ⇒ 'trm" ― ‹substitution for trms›
    and Fvars :: "'fmla ⇒ 'var set" ― ‹free variables for formulas›
    and subst :: "'fmla ⇒ 'trm ⇒ 'var ⇒ 'fmla" ― ‹substitution for formulas›
  assumes
    infinite_var: "infinite var" ― ‹the variables are assumed infinite›
    and ― ‹Assumptions about the infrastructure (free vars, substitution and the embedding of variables into trms.
      NB: We need fewer assumptions for trm substitution than for formula substitution!›
    Var[simp,intro!]: "⋀x. x ∈ var ⟹ Var x ∈ trm"
    and
    inj_Var[simp]: "⋀ x y. x ∈ var ⟹ y ∈ var ⟹ (Var x = Var y ⟷ x = y)"
    and
    finite_FvarsT: "⋀ t. t ∈ trm ⟹ finite (FvarsT t)"
    and
    FvarsT: "⋀t. t ∈ trm ⟹ FvarsT t ⊆ var"
    and
    substT[simp,intro]: "⋀t1 t x. t1 ∈ trm ⟹ t ∈ trm ⟹ x ∈ var ⟹ substT t1 t x ∈ trm"
    and
    FvarsT_Var[simp]: "⋀ x. x ∈ var ⟹ FvarsT (Var x) = {x}"
    and
    substT_Var[simp]: "⋀ x t y. x ∈ var ⟹ y ∈ var ⟹ t ∈ trm ⟹
      substT (Var x) t y = (if x  = y then t else Var x)"
    and
    substT_notIn[simp]:
    "⋀t1 t2 x. x ∈ var ⟹ t1 ∈ trm ⟹ t2 ∈ trm ⟹ x ∉ FvarsT t1 ⟹ substT t1 t2 x = t1"
    and
    ― ‹Assumptions about the infrastructure (free vars and substitution) on formulas›
    finite_Fvars: "⋀ φ. φ ∈ fmla ⟹ finite (Fvars φ)"
    and
    Fvars: "⋀φ. φ ∈ fmla ⟹ Fvars φ ⊆ var"
    and
    subst[simp,intro]: "⋀φ t x. φ ∈ fmla ⟹ t ∈ trm ⟹ x ∈ var ⟹ subst φ t x ∈ fmla"
    and
    Fvars_subst_in:
    "⋀ φ t x. φ ∈ fmla ⟹ t ∈ trm ⟹ x ∈ var ⟹ x ∈ Fvars φ ⟹
      Fvars (subst φ t x) = Fvars φ - {x} ∪ FvarsT t"
    and
    subst_compose_eq_or:
    "⋀ φ t1 t2 x1 x2. φ ∈ fmla ⟹ t1 ∈ trm ⟹ t2 ∈ trm ⟹ x1 ∈ var ⟹ x2 ∈ var ⟹
      x1 = x2 ∨ x2 ∉ Fvars φ ⟹ subst (subst φ t1 x1) t2 x2 = subst φ (substT t1 t2 x2) x1"
    and
    subst_compose_diff:
    "⋀ φ t1 t2 x1 x2. φ ∈ fmla ⟹ t1 ∈ trm ⟹ t2 ∈ trm ⟹ x1 ∈ var ⟹ x2 ∈ var ⟹
      x1 ≠ x2 ⟹ x1 ∉ FvarsT t2 ⟹
      subst (subst φ t1 x1) t2 x2 = subst (subst φ t2 x2) (substT t1 t2 x2) x1"
    and
    subst_same_Var[simp]:
    "⋀ φ x. φ ∈ fmla ⟹ x ∈ var ⟹ subst φ (Var x) x = φ"
    and
    subst_notIn[simp]:
    "⋀ x φ t. φ ∈ fmla ⟹ t ∈ trm ⟹ x ∈ var ⟹ x ∉ Fvars φ ⟹ subst φ t x = φ"
begin

lemma var_NE: "var ≠ {}"
using infinite_var by auto

lemma Var_injD: "Var x = Var y ⟹ x ∈ var ⟹ y ∈ var ⟹ x = y"
by auto

lemma FvarsT_VarD: "x ∈ FvarsT (Var y) ⟹ y ∈ var ⟹ x = y"
by auto

lemma FvarsT': "t ∈ trm ⟹ x ∈ FvarsT t ⟹ x ∈ var"
using FvarsT by auto

lemma Fvars': "φ ∈ fmla ⟹ x ∈ Fvars φ ⟹ x ∈ var"
using Fvars by auto

lemma Fvars_subst[simp]:
  "φ ∈ fmla ⟹ t ∈ trm ⟹ x ∈ var ⟹
  Fvars (subst φ t x) = (Fvars φ - {x}) ∪ (if x ∈ Fvars φ then FvarsT t else {})"
  by (simp add: Fvars_subst_in)

lemma in_Fvars_substD:
  "y ∈ Fvars (subst φ t x) ⟹ φ ∈ fmla ⟹ t ∈ trm ⟹ x ∈ var
   ⟹ y ∈ (Fvars φ - {x}) ∪ (if x ∈ Fvars φ then FvarsT t else {})"
  using Fvars_subst by auto

lemma inj_on_Var: "inj_on Var var"
  using inj_Var unfolding inj_on_def by auto

lemma subst_compose_same:
  "⋀ φ t1 t2 x. φ ∈ fmla ⟹ t1 ∈ trm ⟹ t2 ∈ trm ⟹ x ∈ var ⟹
  subst (subst φ t1 x) t2 x = subst φ (substT t1 t2 x) x"
  using subst_compose_eq_or by blast

lemma subst_subst[simp]:
  assumes φ[simp]: "φ ∈ fmla" and t[simp]:"t ∈ trm" and x[simp]:"x ∈ var" and y[simp]:"y ∈ var"
  assumes yy: "x ≠ y" "y ∉ Fvars φ"
  shows "subst (subst φ (Var y) x) t y = subst φ t x"
  using subst_compose_eq_or[OF φ _ t x y, of "Var y"] using subst_notIn yy by simp

lemma subst_comp:
  "⋀ x y φ t. φ ∈ fmla ⟹ t ∈ trm ⟹ x ∈ var ⟹ y ∈ var ⟹
  x ≠ y ⟹ y ∉ FvarsT t ⟹
  subst (subst φ (Var x) y) t x = subst (subst φ t x) t y"
  by (simp add: subst_compose_diff)

lemma exists_nat_var:
  "∃ f::nat⇒'var. inj f ∧ range f ⊆ var"
  by (simp add: infinite_countable_subset infinite_var)

definition Variable :: "nat ⇒ 'var" where
  "Variable = (SOME f. inj f ∧ range f ⊆ var)"

lemma Variable_inj_var:
  "inj Variable ∧ range Variable ⊆ var"
  unfolding Variable_def using someI_ex[OF exists_nat_var] .

lemma inj_Variable[simp]: "⋀ i j. Variable i = Variable j ⟷ i = j"
  and Variable[simp,intro!]: "⋀i. Variable i ∈ var"
  using Variable_inj_var image_def unfolding inj_def by auto

text ‹Convenient notations for some variables
We reserve the first 10 indexes for any special variables we
may wish to consider later.›
abbreviation xx where "xx ≡ Variable 10"
abbreviation yy where "yy ≡ Variable 11"
abbreviation zz where "zz ≡ Variable 12"

abbreviation xx' where "xx' ≡ Variable 13"
abbreviation yy' where "yy' ≡ Variable 14"
abbreviation zz' where "zz' ≡ Variable 15"

lemma xx: "xx ∈ var"
  and yy: "yy ∈ var"
  and zz: "zz ∈ var"
  and xx': "xx' ∈ var"
  and yy': "yy' ∈ var"
  and zz': "zz' ∈ var"
  by auto

lemma vars_distinct[simp]:
  "xx ≠ yy" "yy ≠ xx" "xx ≠ zz" "zz ≠ xx" "xx ≠ xx'" "xx' ≠ xx" "xx ≠ yy'" "yy' ≠ xx" "xx ≠ zz'" "zz' ≠ xx"
  "yy ≠ zz" "zz ≠ yy" "yy ≠ xx'" "xx' ≠ yy" "yy ≠ yy'" "yy' ≠ yy" "yy ≠ zz'" "zz' ≠ yy"
  "zz ≠ xx'" "xx' ≠ zz" "zz ≠ yy'" "yy' ≠ zz" "zz ≠ zz'" "zz' ≠ zz"
  "xx' ≠ yy'" "yy' ≠ xx'" "xx' ≠ zz'" "zz' ≠ xx'"
  "yy' ≠ zz'" "zz' ≠ yy'"
  by auto


subsection ‹Instance Operator›

definition inst :: "'fmla ⇒ 'trm ⇒ 'fmla" where
  "inst φ t = subst φ t xx"

lemma inst[simp]: "φ ∈ fmla ⟹ t ∈ trm ⟹ inst φ t ∈ fmla"
  unfolding inst_def by auto

definition getFresh :: "'var set ⇒ 'var" where
  "getFresh V = (SOME x. x ∈ var ∧ x ∉ V)"

lemma getFresh: "finite V ⟹  getFresh V ∈ var ∧ getFresh V ∉ V"
  by (metis (no_types, lifting) finite_subset getFresh_def infinite_var someI_ex subsetI)

definition getFr :: "'var list ⇒ 'trm list ⇒ 'fmla list ⇒ 'var" where
  "getFr xs ts φs =
 getFresh (set xs ∪ (⋃(FvarsT ` set ts)) ∪ (⋃(Fvars ` set φs)))"

lemma getFr_FvarsT_Fvars:
  assumes "set xs ⊆ var" "set ts ⊆ trm" and "set φs ⊆ fmla"
  shows "getFr xs ts φs ∈ var ∧
       getFr xs ts φs ∉ set xs ∧
       (t ∈ set ts ⟶ getFr xs ts φs ∉ FvarsT t) ∧
       (φ ∈ set φs ⟶ getFr xs ts φs ∉ Fvars φ)"
proof-
  have "finite (set xs ∪ (⋃(FvarsT ` set ts)) ∪ (⋃(Fvars ` set φs)))"
    using assms finite_FvarsT finite_Fvars by auto
  from getFresh[OF this] show ?thesis using assms unfolding getFr_def by auto
qed

lemma getFr[simp,intro]:
  assumes "set xs ⊆ var" "set ts ⊆ trm" and "set φs ⊆ fmla"
  shows "getFr xs ts φs ∈ var"
  using assms getFr_FvarsT_Fvars by auto

lemma getFr_var:
  assumes "set xs ⊆ var" "set ts ⊆ trm" and "set φs ⊆ fmla" and "t ∈ set ts"
  shows "getFr xs ts φs ∉ set xs"
  using assms getFr_FvarsT_Fvars by auto

lemma getFr_FvarsT:
  assumes "set xs ⊆ var" "set ts ⊆ trm" and "set φs ⊆ fmla" and "t ∈ set ts"
  shows "getFr xs ts φs ∉ FvarsT t"
  using assms getFr_FvarsT_Fvars by auto

lemma getFr_Fvars:
  assumes "set xs ⊆ var" "set ts ⊆ trm" and "set φs ⊆ fmla" and "φ ∈ set φs"
  shows "getFr xs ts φs ∉ Fvars φ"
  using assms getFr_FvarsT_Fvars by auto


subsection ‹Fresh Variables›

fun getFreshN :: "'var set ⇒ nat ⇒ 'var list" where
  "getFreshN V 0 = []"
| "getFreshN V (Suc n) = (let u = getFresh V in u # getFreshN (insert u V) n)"

lemma getFreshN: "finite V ⟹
  set (getFreshN V n) ⊆ var ∧ set (getFreshN V n) ∩ V = {} ∧ length (getFreshN V n) = n ∧ distinct (getFreshN V n)"
  by (induct n arbitrary: V) (auto simp: getFresh Let_def)

definition getFrN :: "'var list ⇒ 'trm list ⇒ 'fmla list ⇒ nat ⇒ 'var list" where
  "getFrN xs ts φs n =
 getFreshN (set xs ∪ (⋃(FvarsT ` set ts)) ∪ (⋃(Fvars ` set φs))) n"

lemma getFrN_FvarsT_Fvars:
  assumes "set xs ⊆ var" "set ts ⊆ trm" and "set φs ⊆ fmla"
  shows "set (getFrN xs ts φs n) ⊆ var ∧
       set (getFrN xs ts φs n) ∩ set xs = {} ∧
       (t ∈ set ts ⟶ set (getFrN xs ts φs n) ∩ FvarsT t = {}) ∧
       (φ ∈ set φs ⟶ set (getFrN xs ts φs n) ∩ Fvars φ = {}) ∧
       length (getFrN xs ts φs n) = n ∧
       distinct (getFrN xs ts φs n)"
proof-
  have "finite (set xs ∪ (⋃(FvarsT ` set ts)) ∪ (⋃(Fvars ` set φs)))"
    using assms finite_FvarsT finite_Fvars by auto
  from getFreshN[OF this] show ?thesis using assms unfolding getFrN_def by auto
qed

lemma getFrN[simp,intro]:
  assumes "set xs ⊆ var" "set ts ⊆ trm" and "set φs ⊆ fmla"
  shows "set (getFrN xs ts φs n) ⊆ var"
  using assms getFrN_FvarsT_Fvars by auto

lemma getFrN_var:
  assumes "set xs ⊆ var" "set ts ⊆ trm" and "set φs ⊆ fmla" and "t ∈ set ts"
  shows "set (getFrN xs ts φs n) ∩ set xs = {}"
  using assms getFrN_FvarsT_Fvars by auto

lemma getFrN_FvarsT:
  assumes "set xs ⊆ var" "set ts ⊆ trm" and "set φs ⊆ fmla" and "t ∈ set ts"
  shows "set (getFrN xs ts φs n) ∩ FvarsT t = {}"
  using assms getFrN_FvarsT_Fvars by auto

lemma getFrN_Fvars:
  assumes "set xs ⊆ var" "set ts ⊆ trm" and "set φs ⊆ fmla" and "φ ∈ set φs"
  shows "set (getFrN xs ts φs n) ∩ Fvars φ = {}"
  using assms getFrN_FvarsT_Fvars by auto

lemma getFrN_length:
  assumes "set xs ⊆ var" "set ts ⊆ trm" and "set φs ⊆ fmla"
  shows "length (getFrN xs ts φs n) = n"
  using assms getFrN_FvarsT_Fvars by auto

lemma getFrN_distinct[simp,intro]:
  assumes "set xs ⊆ var" "set ts ⊆ trm" and "set φs ⊆ fmla"
  shows "distinct (getFrN xs ts φs n)"
  using assms getFrN_FvarsT_Fvars by auto


subsection ‹Parallel Term Substitution›

fun rawpsubstT :: "'trm ⇒ ('trm × 'var) list ⇒ 'trm" where
  "rawpsubstT t [] = t"
| "rawpsubstT t ((t1,x1) # txs) = rawpsubstT (substT t t1 x1) txs"

lemma rawpsubstT[simp]:
  assumes "t ∈ trm" and "snd ` (set txs) ⊆ var" and "fst ` (set txs) ⊆ trm"
  shows "rawpsubstT t txs ∈ trm"
  using assms by (induct txs arbitrary: t) fastforce+

definition psubstT :: "'trm ⇒ ('trm × 'var) list ⇒ 'trm" where
  "psubstT t txs =
    (let xs = map snd txs; ts = map fst txs; us = getFrN xs (t # ts) [] (length xs) in
      rawpsubstT (rawpsubstT t (zip (map Var us) xs)) (zip ts us))"

text ‹The psubstT versions of the subst axioms.›

lemma psubstT[simp,intro]:
  assumes "t ∈ trm" and "snd ` (set txs) ⊆ var" and "fst ` (set txs) ⊆ trm"
  shows "psubstT t txs ∈ trm"
proof-
  define us where us: "us = getFrN (map snd txs) (t # map fst txs) [] (length txs)"
  have us_facts: "set us ⊆ var"
    "set us ∩ FvarsT t = {}"
    "set us ∩ ⋃ (FvarsT ` (fst ` (set txs))) = {}"
    "set us ∩ snd ` (set txs) = {}"
    "length us = length txs"
    "distinct us"
    using assms unfolding us
    using getFrN_FvarsT[of "map snd txs" "t # map fst txs" "[]" _ "length txs"]
      getFrN_var[of "map snd txs" "t # map fst txs" "[]" _ "length txs"]
      getFrN_length[of "map snd txs" "t # map fst txs" "[]" "length txs"]
      getFrN_distinct[of "map snd txs" "t # map fst txs" "[]" "length txs"]
    by auto (metis (no_types, opaque_lifting) IntI empty_iff image_iff old.prod.inject surjective_pairing)
  show ?thesis using assms us_facts unfolding psubstT_def
    by (force simp: Let_def us[symmetric] dest: set_zip_leftD set_zip_rightD intro!: rawpsubstT)
qed

lemma rawpsubstT_Var_not[simp]:
  assumes "x ∈ var" "snd ` (set txs) ⊆ var" "fst ` (set txs) ⊆ trm"
    and "x ∉ snd ` (set txs)"
  shows "rawpsubstT (Var x) txs = Var x"
  using assms by (induct txs) auto

lemma psubstT_Var_not[simp]:
  assumes "x ∈ var" "snd ` (set txs) ⊆ var" "fst ` (set txs) ⊆ trm"
    and "x ∉ snd ` (set txs)"
  shows "psubstT (Var x) txs = Var x"
proof-
  define us where us: "us = getFrN (map snd txs) (Var x # map fst txs) [] (length txs)"
  have us_facts: "set us ⊆ var"
    "x ∉ set us"
    "set us ∩ ⋃ (FvarsT ` (fst ` (set txs))) = {}"
    "set us ∩ snd ` (set txs) = {}"
    "length us = length txs"
    using assms unfolding us
    using getFrN_FvarsT[of "map snd txs" "Var x # map fst txs" "[]" "Var x" "length txs"]
      getFrN_FvarsT[of "map snd txs" "Var x # map fst txs" "[]" _ "length txs"]
      getFrN_var[of "map snd txs" "Var x # map fst txs" "[]" "Var x" "length txs"]
      getFrN_length[of "map snd txs" "Var x # map fst txs" "[]" "length txs"]
    by (auto simp: set_eq_iff)
  have [simp]: "rawpsubstT (Var x) (zip (map Var us) (map snd txs)) = Var x"
    using assms us_facts
    by(intro rawpsubstT_Var_not) (force dest: set_zip_rightD set_zip_leftD)+
  have [simp]: "rawpsubstT (Var x) (zip (map fst txs) us) = Var x"
    using assms us_facts
    by(intro rawpsubstT_Var_not) (force dest: set_zip_rightD set_zip_leftD)+
  show ?thesis using assms us_facts unfolding psubstT_def
    by (auto simp: Let_def us[symmetric])
qed

lemma rawpsubstT_notIn[simp]:
  assumes "x ∈ var" "snd ` (set txs) ⊆ var" "fst ` (set txs) ⊆ trm" "t ∈ trm"
    and "FvarsT t ∩ snd ` (set txs) = {}"
  shows "rawpsubstT t txs = t"
  using assms by (induct txs) auto

lemma psubstT_notIn[simp]:
  assumes "x ∈ var" "snd ` (set txs) ⊆ var" "fst ` (set txs) ⊆ trm" "t ∈ trm"
    and "FvarsT t ∩ snd ` (set txs) = {}"
  shows "psubstT t txs = t"
proof-
  define us where us: "us = getFrN (map snd txs) (t # map fst txs) [] (length txs)"
  have us_facts: "set us ⊆ var"
    "set us ∩ FvarsT t = {}"
    "set us ∩ ⋃ (FvarsT ` (fst ` (set txs))) = {}"
    "set us ∩ snd ` (set txs) = {}"
    "length us = length txs"
    using assms unfolding us
    using getFrN_FvarsT[of "map snd txs" "t # map fst txs" "[]" _ "length txs"]
      getFrN_var[of "map snd txs" "t # map fst txs" "[]" t "length txs"]
      getFrN_length[of "map snd txs" "t # map fst txs" "[]" "length txs"]
    by (auto simp: set_eq_iff)
  have [simp]: "rawpsubstT t (zip (map Var us) (map snd txs)) = t"
    using assms us_facts
    by(intro rawpsubstT_notIn) (auto 0 3 dest: set_zip_rightD set_zip_leftD)
  have [simp]: "rawpsubstT t (zip (map fst txs) us) = t"
    using assms us_facts
    by(intro rawpsubstT_notIn) (auto 0 3 dest: set_zip_rightD set_zip_leftD)
  show ?thesis using assms us_facts unfolding psubstT_def
    by (auto simp: Let_def us[symmetric])
qed


subsection ‹Parallel Formula Substitution›

fun rawpsubst :: "'fmla ⇒ ('trm × 'var) list ⇒ 'fmla" where
  "rawpsubst φ [] = φ"
| "rawpsubst φ ((t1,x1) # txs) = rawpsubst (subst φ t1 x1) txs"

lemma rawpsubst[simp]:
  assumes "φ ∈ fmla" and "snd ` (set txs) ⊆ var" and "fst ` (set txs) ⊆ trm"
  shows "rawpsubst φ txs ∈ fmla"
  using assms by (induct txs arbitrary: φ) fastforce+

definition psubst :: "'fmla ⇒ ('trm × 'var) list ⇒ 'fmla" where
  "psubst φ txs =
    (let xs = map snd txs; ts = map fst txs; us = getFrN xs ts [φ] (length xs) in
      rawpsubst (rawpsubst φ (zip (map Var us) xs)) (zip ts us))"

text ‹The psubst versions of the subst axioms.›

lemma psubst[simp,intro]:
  assumes "φ ∈ fmla" and "snd ` (set txs) ⊆ var" and "fst ` (set txs) ⊆ trm"
  shows "psubst φ txs ∈ fmla"
proof-
  define us where us: "us = getFrN (map snd txs) (map fst txs) [φ] (length txs)"
  have us_facts: "set us ⊆ var"
    "set us ∩ Fvars φ = {}"
    "set us ∩ ⋃ (FvarsT ` (fst ` (set txs))) = {}"
    "set us ∩ snd ` (set txs) = {}"
    "length us = length txs"
    "distinct us"
    using assms unfolding us
    using getFrN_FvarsT[of "map snd txs" "map fst txs" "[φ]" _ "length txs"]
      getFrN_Fvars[of "map snd txs" "map fst txs" "[φ]" φ "length txs"]
      getFrN_var[of "map snd txs" "map fst txs" "[φ]" _ "length txs"]
      getFrN_length[of "map snd txs" "map fst txs" "[φ]" "length txs"]
      getFrN_distinct[of "map snd txs" "map fst txs" "[φ]" "length txs"]
    by (auto 8 0 simp: set_eq_iff image_iff Bex_def Ball_def)
  show ?thesis using assms us_facts unfolding psubst_def
    by (auto 0 3 simp: Let_def us[symmetric] dest: set_zip_rightD set_zip_leftD intro!: rawpsubst)
qed

lemma Fvars_rawpsubst_su:
  assumes "φ ∈ fmla" and "snd ` (set txs) ⊆ var" and "fst ` (set txs) ⊆ trm"
  shows "Fvars (rawpsubst φ txs) ⊆
       (Fvars φ - snd ` (set txs)) ∪ (⋃ {FvarsT t | t x . (t,x) ∈ set txs})"
  using assms proof(induction txs arbitrary: φ)
  case (Cons tx txs φ)
  then obtain t x where tx: "tx = (t,x)" by force
  have t: "t ∈ trm" and x: "x ∈ var" using Cons.prems unfolding tx by auto
  define χ where "χ = subst φ t x"
  have 0: "Fvars χ =  Fvars φ - {x} ∪ (if x ∈ Fvars φ then FvarsT t else {})"
    using Cons.prems unfolding χ_def by (auto simp: tx t)
  have χ: "χ ∈ fmla" unfolding χ_def using Cons.prems t x by auto
  have "Fvars (rawpsubst χ txs) ⊆
       (Fvars χ - snd ` (set txs)) ∪
       (⋃ {FvarsT t | t x . (t,x) ∈ set txs})"
     using Cons.prems χ by (intro Cons.IH) auto
  also have "… ⊆ Fvars φ - insert x (snd ` set txs) ∪ ⋃{FvarsT ta |ta. ∃xa. ta = t ∧ xa = x ∨ (ta, xa) ∈ set txs}"
    (is "_ ⊆ ?R") by(auto simp: 0 tx Cons.prems)
  finally have 1: "Fvars (rawpsubst χ txs) ⊆ ?R" .
  have 2: "Fvars χ = Fvars φ - {x} ∪ (if x ∈ Fvars φ then FvarsT t else {})"
    using Cons.prems t x unfolding χ_def using Fvars_subst by auto
  show ?case using 1 by (simp add: tx χ_def[symmetric] 2)
qed auto

lemma in_Fvars_rawpsubst_imp:
  assumes "y ∈ Fvars (rawpsubst φ txs)"
    and "φ ∈ fmla" and "snd ` (set txs) ⊆ var" and "fst ` (set txs) ⊆ trm"
  shows "(y ∈ Fvars φ - snd ` (set txs)) ∨
     (y ∈ ⋃ { FvarsT t | t x . (t,x) ∈ set txs})"
  using Fvars_rawpsubst_su[OF assms(2-4)]
  using assms(1) by blast

lemma Fvars_rawpsubst:
  assumes "φ ∈ fmla" and "snd ` (set txs) ⊆ var" and "fst ` (set txs) ⊆ trm"
    and "distinct (map snd txs)" and "∀ x ∈ snd ` (set txs). ∀ t ∈ fst ` (set txs). x ∉ FvarsT t"
  shows "Fvars (rawpsubst φ txs) =
       (Fvars φ - snd ` (set txs)) ∪
       (⋃ {if x ∈ Fvars φ then FvarsT t else {} | t x . (t,x) ∈ set txs})"
  using assms proof(induction txs arbitrary: φ)
  case (Cons a txs φ)
  then obtain t x where a: "a = (t,x)" by force
  have t: "t ∈ trm" and x: "x ∈ var" using Cons.prems unfolding a by auto
  have x_txs: "⋀ta xa. (ta, xa) ∈ set txs ⟹ x ≠ xa" using ‹distinct (map snd (a # txs))›
   unfolding a by (auto simp: rev_image_eqI)
  have xt: "x ∉ FvarsT t ∧ snd ` set txs ∩ FvarsT t = {}" using Cons.prems unfolding a by auto
  hence 0: "Fvars φ - {x} ∪ FvarsT t - snd ` set txs =
            Fvars φ - insert x (snd ` set txs) ∪ FvarsT t"
    by auto
  define χ where χ_def: "χ = subst φ t x"
  have χ: "χ ∈ fmla" unfolding χ_def using Cons.prems t x by auto
  have 1: "Fvars (rawpsubst χ txs) =
       (Fvars χ - snd ` (set txs)) ∪
       (⋃ {if x ∈ Fvars χ then FvarsT t else {} | t x . (t,x) ∈ set txs})"
     using Cons.prems χ by (intro Cons.IH) auto
  have 2: "Fvars χ = Fvars φ - {x} ∪ (if x ∈ Fvars φ then FvarsT t else {})"
    using Cons.prems t x unfolding χ_def using Fvars_subst by auto

  define f where "f ≡ λta xa. if xa ∈ Fvars φ then FvarsT ta else {}"

  have 3: "⋃ {f ta xa  |ta xa. (ta, xa) ∈ set ((t, x) # txs)} =
        f t x ∪ (⋃ {f ta xa  |ta xa. (ta, xa) ∈ set txs})" by auto
  have 4: "snd ` set ((t, x) # txs) = {x} ∪ snd ` set txs" by auto
  have 5: "f t x ∩ snd ` set txs = {}" unfolding f_def using xt by auto
  have 6: "⋃ {if xa ∈ Fvars φ - {x} ∪ f t x then FvarsT ta else {} | ta xa. (ta, xa) ∈ set txs}
     = (⋃ {f ta xa | ta xa. (ta, xa) ∈ set txs})"
  unfolding f_def using xt x_txs by (fastforce split: if_splits)

  have "Fvars φ - {x} ∪ f t x  - snd ` set txs ∪
    ⋃ {if xa ∈ Fvars φ - {x} ∪ f t x then FvarsT ta else {}
         | ta xa. (ta, xa) ∈ set txs} =
        Fvars φ - snd ` set ((t, x) # txs) ∪
    ⋃ {f ta xa  |ta xa. (ta, xa) ∈ set ((t, x) # txs)}"
  unfolding 3 4 6 unfolding Un_Diff2[OF 5] Un_assoc unfolding Diff_Diff_Un ..

  thus ?case unfolding a rawpsubst.simps 1 2 χ_def[symmetric] f_def by simp
qed auto

lemma in_Fvars_rawpsubstD:
  assumes "y ∈ Fvars (rawpsubst φ txs)"
    and "φ ∈ fmla" and "snd ` (set txs) ⊆ var" and "fst ` (set txs) ⊆ trm"
    and "distinct (map snd txs)" and "∀ x ∈ snd ` (set txs). ∀ t ∈ fst ` (set txs). x ∉ FvarsT t"
  shows "(y ∈ Fvars φ - snd ` (set txs)) ∨
     (y ∈ ⋃ {if x ∈ Fvars φ then FvarsT t else {} | t x . (t,x) ∈ set txs})"
  using Fvars_rawpsubst assms by auto

lemma Fvars_psubst:
  assumes "φ ∈ fmla" and "snd ` (set txs) ⊆ var" and "fst ` (set txs) ⊆ trm"
    and "distinct (map snd txs)"
  shows "Fvars (psubst φ txs) =
       (Fvars φ - snd ` (set txs)) ∪
       (⋃ {if x ∈ Fvars φ then FvarsT t else {} | t x . (t,x) ∈ set txs})"
proof-
  define us where us: "us = getFrN (map snd txs) (map fst txs) [φ] (length txs)"
  have us_facts: "set us ⊆ var"
    "set us ∩ Fvars φ = {}"
    "set us ∩ ⋃ (FvarsT ` (fst ` (set txs))) = {}"
    "set us ∩ snd ` (set txs) = {}"
    "length us = length txs"
    "distinct us"
    using assms unfolding us
    using getFrN_FvarsT[of "map snd txs" "map fst txs" "[φ]" _ "length txs"]
      getFrN_Fvars[of "map snd txs" "map fst txs" "[φ]" _ "length txs"]
      getFrN_var[of "map snd txs" "map fst txs" "[φ]" _ "length txs"]
      getFrN_length[of "map snd txs" "map fst txs" "[φ]" "length txs"]
      getFrN_length[of "map snd txs" "map fst txs" "[φ]" "length txs"]
    by (auto 9 0 simp: set_eq_iff image_iff)
  define χ where χ_def: "χ = rawpsubst φ (zip (map Var us) (map snd txs))"
  have χ: "χ ∈ fmla" unfolding χ_def using assms us_facts
    by (intro rawpsubst) (auto dest!: set_zip_D)
  have set_us: "set us = snd ` (set (zip (map fst txs) us))"
     using us_facts by (intro snd_set_zip[symmetric]) auto
  have set_txs: "snd ` set txs = snd ` (set (zip (map Var us) (map snd txs)))"
     using us_facts by (intro snd_set_zip_map_snd[symmetric]) auto
  have "⋀ t x. (t, x) ∈ set (zip (map Var us) (map snd txs)) ⟹ ∃ u. t = Var u"
    using us_facts set_zip_leftD by fastforce
  hence 00: "⋀ t x. (t, x) ∈ set (zip (map Var us) (map snd txs))
     ⟷  (∃ u ∈ var. t = Var u ∧ (Var u, x) ∈ set (zip (map Var us) (map snd txs)))"
    using us_facts set_zip_leftD by fastforce
  have "Fvars χ =
        Fvars φ - snd ` set txs ∪
        ⋃{if x ∈ Fvars φ then FvarsT t else {} |t x.
             (t, x) ∈ set (zip (map Var us) (map snd txs))}"
    unfolding χ_def set_txs using assms us_facts
    apply(intro Fvars_rawpsubst)
    subgoal by auto
    subgoal by (auto dest!: set_zip_rightD)
    subgoal by (auto dest!: set_zip_leftD)
    subgoal by auto
    subgoal  by (auto 0 6 simp: set_txs[symmetric] set_eq_iff subset_eq image_iff in_set_zip
      dest: spec[where P="λx. x ∈ set us ⟶ (∀y ∈ set txs. x ≠ snd y)", THEN mp[OF _ nth_mem]]) .
  also have "… =
    Fvars φ - snd ` set txs ∪
    ⋃{if x ∈ Fvars φ then {u} else {} |u x. u ∈ var ∧ (Var u, x) ∈ set (zip (map Var us) (map snd txs))}"
    (is "… = ?R")
    using FvarsT_Var by (metis (no_types, opaque_lifting) 00)
  finally have 0: "Fvars χ = ?R" .
  have 1: "Fvars (rawpsubst χ (zip (map fst txs) us)) =
        (Fvars χ - set us) ∪
        (⋃ {if u ∈ Fvars χ then FvarsT t else {} | t u . (t,u) ∈ set (zip (map fst txs) us)})"
    unfolding set_us using us_facts assms χ
    apply (intro Fvars_rawpsubst)
    subgoal by (auto dest: set_zip_rightD)
    subgoal by (auto dest: set_zip_rightD)
    subgoal by (auto dest!: set_zip_leftD)
    subgoal by (auto dest!: set_zip_leftD)
    subgoal by (metis IntI Union_iff empty_iff fst_set_zip_map_fst image_eqI set_us) .
  have 2: "Fvars χ - set us = Fvars φ - snd ` set txs"
    unfolding 0 using us_facts(1,2)
    by (fastforce dest!: set_zip_leftD split: if_splits)
  have 3:
    "(⋃ {if u ∈ Fvars χ then FvarsT t else {} | t u . (t,u) ∈ set (zip (map fst txs) us)}) =
   (⋃ {if x ∈ Fvars φ then FvarsT t else {} | t x . (t,x) ∈ set txs})"
  proof safe
    fix xx tt y
    assume xx: "xx ∈ (if y ∈ Fvars χ then FvarsT tt else {})"
      and ty: "(tt, y) ∈ set (zip (map fst txs) us)"
    have ttin: "tt ∈ fst ` set txs" using ty using set_zip_leftD by fastforce
    have yin: "y ∈ set us" using ty by (meson set_zip_D)
    have yvar: "y ∈ var" using us_facts yin by auto
    have ynotin: "y ∉ snd ` set txs" "y ∉ Fvars φ" using yin us_facts by auto
    show "xx ∈ ⋃{if x ∈ Fvars φ then FvarsT t else {} |t x. (t, x) ∈ set txs}"
    proof(cases "y ∈ Fvars χ")
      case True note y = True
      hence xx: "xx ∈ FvarsT tt" using xx by simp
      obtain x where xφ: "x ∈ Fvars φ"
        and yx: "(Var y, x) ∈ set (zip (map Var us) (map snd txs))"
        using y ynotin unfolding 0 by auto (metis empty_iff insert_iff)
      have yx: "(y, x) ∈ set (zip us (map snd txs))"
      using yvar us_facts by (intro inj_on_set_zip_map[OF inj_on_Var yx]) auto
      have "(tt, x) ∈ set txs" apply(rule set_zip_map_fst_snd[OF yx ty])
        using  ‹distinct (map snd txs)› us_facts by auto
      thus ?thesis using xx xφ by auto
    qed(insert xx, auto)
  next
    fix y tt xx
    assume y: "y ∈ (if xx ∈ Fvars φ then FvarsT tt else {})"
      and tx: "(tt, xx) ∈ set txs"
    hence xxsnd: "xx ∈ snd ` set txs" by force
    obtain u where uin: "u ∈ set us" and uxx: "(u, xx) ∈ set (zip us (map snd txs))"
      by (metis xxsnd in_set_impl_in_set_zip2 length_map set_map set_zip_leftD us_facts(5))
    hence uvar: "u ∈ var" using us_facts by auto
    show "y ∈ ⋃{if u ∈ Fvars χ then FvarsT t else {} |t u. (t, u) ∈ set (zip (map fst txs) us)}"
    proof(cases "xx ∈ Fvars φ")
      case True note xx = True
      hence y: "y ∈ FvarsT tt" using y by auto
      have "(Var u, xx) ∈ set (zip (map Var us) (map snd txs))"
      using us_facts by (intro set_zip_length_map[OF uxx]) auto
      hence uχ: "u ∈ Fvars χ" using uin xx uvar unfolding 0 by auto
      have ttu: "(tt, u) ∈ set (zip (map fst txs) us)"
      using assms us_facts by (intro set_zip_map_fst_snd2[OF uxx tx]) auto
      show ?thesis using uχ ttu y by auto
    qed(insert y, auto)
  qed
  show ?thesis
  by (simp add: psubst_def Let_def us[symmetric] χ_def[symmetric] 1 2 3)
qed

lemma in_Fvars_psubstD:
  assumes "y ∈ Fvars (psubst φ txs)"
    and "φ ∈ fmla" and "snd ` (set txs) ⊆ var" and "fst ` (set txs) ⊆ trm"
    and "distinct (map snd txs)"
  shows "y ∈ (Fvars φ - snd ` (set txs)) ∪
           (⋃ {if x ∈ Fvars φ then FvarsT t else {} | t x . (t,x) ∈ set txs})"
  using assms Fvars_psubst by auto

lemma subst2_fresh_switch:
  assumes "φ ∈ fmla" "t ∈ trm" "s ∈ trm" "x ∈ var" "y ∈ var"
    and "x ≠ y" "x ∉ FvarsT s" "y ∉ FvarsT t"
  shows "subst (subst φ s y) t x = subst (subst φ t x) s y"   (is "?L = ?R")
  using assms by (simp add: subst_compose_diff[of φ s t y x])

lemma rawpsubst2_fresh_switch:
  assumes "φ ∈ fmla" "t ∈ trm" "s ∈ trm" "x ∈ var" "y ∈ var"
    and "x ≠ y" "x ∉ FvarsT s" "y ∉ FvarsT t"
  shows "rawpsubst φ ([(s,y),(t,x)]) = rawpsubst φ ([(t,x),(s,y)])"
  using assms by (simp add: subst2_fresh_switch)

lemma rawpsubst_compose:
  assumes "φ ∈ fmla" and "snd ` (set txs1) ⊆ var" and "fst ` (set txs1) ⊆ trm"
    and "snd ` (set txs2) ⊆ var" and "fst ` (set txs2) ⊆ trm"
  shows "rawpsubst (rawpsubst φ txs1) txs2 = rawpsubst φ (txs1 @ txs2)"
  using assms by (induct txs1 arbitrary: txs2 φ) auto

lemma rawpsubst_subst_fresh_switch:
  assumes "φ ∈ fmla" "snd ` (set txs) ⊆ var" and "fst ` (set txs) ⊆ trm"
    and "∀ x ∈ snd ` (set txs). x ∉ FvarsT s"
    and "∀ t ∈ fst ` (set txs). y ∉ FvarsT t"
    and "distinct (map snd txs)"
    and "s ∈ trm" and "y ∈ var" "y ∉ snd ` (set txs)"
  shows "rawpsubst (subst φ s y) txs = rawpsubst φ (txs @ [(s,y)])"
  using assms proof(induction txs arbitrary: φ s y)
  case (Cons tx txs)
  obtain t x where tx[simp]: "tx = (t,x)" by force
  have x: "x ∈ var" and t: "t ∈ trm" using Cons unfolding tx by auto
  have "rawpsubst φ ((s, y) # (t, x) # txs) = rawpsubst φ ([(s, y),(t, x)] @ txs)" by simp
  also have "… = rawpsubst (rawpsubst φ [(s, y),(t, x)]) txs"
    using Cons by auto
  also have "rawpsubst φ [(s, y),(t, x)] = rawpsubst φ [(t, x),(s, y)]"
    using Cons by (intro rawpsubst2_fresh_switch) auto
  also have "rawpsubst (rawpsubst φ [(t, x),(s, y)]) txs = rawpsubst φ ([(t, x),(s, y)] @ txs)"
    using Cons by auto
  also have "… = rawpsubst (subst φ t x) (txs @ [(s,y)])" using Cons by auto
  also have "… = rawpsubst φ (((t, x) # txs) @ [(s, y)])" by simp
  finally show ?case unfolding tx by auto
qed auto

lemma subst_rawpsubst_fresh_switch:
  assumes "φ ∈ fmla" "snd ` (set txs) ⊆ var" and "fst ` (set txs) ⊆ trm"
    and "∀ x ∈ snd ` (set txs). x ∉ FvarsT s"
    and "∀ t ∈ fst ` (set txs). y ∉ FvarsT t"
    and "distinct (map snd txs)"
    and "s ∈ trm" and "y ∈ var" "y ∉ snd ` (set txs)"
  shows "subst (rawpsubst φ txs) s y = rawpsubst φ ((s,y) # txs)"
  using assms proof(induction txs arbitrary: φ s y)
  case (Cons tx txs)
  obtain t x where tx[simp]: "tx = (t,x)" by force
  have x: "x ∈ var" and t: "t ∈ trm" using Cons unfolding tx by auto
  have "subst (rawpsubst (subst φ t x) txs) s y = rawpsubst (subst φ t x) ((s,y) # txs)"
   using Cons.prems by (intro Cons.IH) auto
  also have "… = rawpsubst (rawpsubst φ [(t,x)]) ((s,y) # txs)" by simp
  also have "… = rawpsubst φ ([(t,x)] @ ((s,y) # txs))"
    using Cons.prems by auto
  also have "… = rawpsubst φ ([(t,x),(s,y)] @ txs)" by simp
  also have "… = rawpsubst (rawpsubst φ [(t,x),(s,y)]) txs"
    using Cons.prems by auto
  also have "rawpsubst φ [(t,x),(s,y)] = rawpsubst φ [(s,y),(t,x)]"
    using Cons.prems by (intro rawpsubst2_fresh_switch) auto
  also have "rawpsubst (rawpsubst φ [(s,y),(t,x)]) txs = rawpsubst φ ([(s,y),(t,x)] @ txs)"
    using Cons.prems by auto
  finally show ?case by simp
qed auto

lemma rawpsubst_compose_freshVar:
  assumes "φ ∈ fmla" "snd ` (set txs) ⊆ var" and "fst ` (set txs) ⊆ trm"
    and "distinct (map snd txs)"
    and "⋀ i j. i < j ⟹ j < length txs ⟹ snd (txs!j) ∉ FvarsT (fst (txs!i))"
    and us_facts: "set us ⊆ var"
    "set us ∩ Fvars φ = {}"
    "set us ∩ ⋃ (FvarsT ` (fst ` (set txs))) = {}"
    "set us ∩ snd ` (set txs) = {}"
    "length us = length txs"
    "distinct us"
  shows "rawpsubst (rawpsubst φ (zip (map Var us) (map snd txs))) (zip (map fst txs) us) = rawpsubst φ txs"
  using assms proof(induction txs arbitrary: us φ)
  case (Cons tx txs uus φ)
  obtain t x where tx[simp]: "tx = (t,x)" by force
  obtain u us where uus[simp]: "uus = u # us" using Cons by (cases uus) auto
  have us_facts: "set us ⊆ var"
    "set us ∩ Fvars φ = {}"
    "set us ∩ ⋃ (FvarsT ` (fst ` (set txs))) = {}"
    "set us ∩ snd ` (set txs) = {}"
    "length us = length txs"
    "distinct us" and u_facts: "u ∈ var" "u ∉ Fvars φ"
    "u ∉ ⋃ (FvarsT ` (fst ` (set txs)))"
    "u ∉ snd ` (set txs)" "u ∉ set us"
    using Cons by auto
  let ?uxs = "zip (map Var us) (map snd txs)"
  have 1: "rawpsubst (subst φ (Var u) x) ?uxs = rawpsubst φ (?uxs @ [(Var u,x)])"
    using u_facts Cons.prems
    by (intro rawpsubst_subst_fresh_switch) (auto simp: subsetD dest!: set_zip_D)
  let ?uuxs = "zip (map Var uus) (map snd (tx # txs))"
  let ?tus = "zip (map fst txs) us"  let ?ttxs = "zip (map fst (tx # txs)) uus"
  have 2: "u ∈ Fvars (rawpsubst φ (zip (map Var us) (map snd txs))) ⟹ False"
  using Cons.prems apply- apply(drule in_Fvars_rawpsubstD)
  subgoal by auto
  subgoal by (auto dest!: set_zip_D)
  subgoal by (auto dest!: set_zip_D)
  subgoal by auto
  subgoal premises prems using us_facts(1,4,5)
    by (auto 0 3 simp: in_set_zip subset_eq set_eq_iff image_iff
      dest: spec[where P="λx. x ∈ set us ⟶ (∀y ∈ set txs. x ≠ snd y)",
        THEN mp[OF _ nth_mem], THEN bspec[OF _ nth_mem]])
  subgoal
    by (auto simp: in_set_zip subset_eq split: if_splits) .

  have 3: "⋀ xx tt. xx ∈ FvarsT t ⟹ (tt, xx) ∉ set txs"
  using Cons.prems(4,5) tx unfolding set_conv_nth
  by simp (metis One_nat_def Suc_leI diff_Suc_1 fst_conv le_imp_less_Suc
            nth_Cons_0 snd_conv zero_less_Suc)

  have 00: "rawpsubst (rawpsubst φ ?uuxs) ?ttxs = rawpsubst (subst (rawpsubst φ (?uxs @ [(Var u, x)])) t u) ?tus"
    by (simp add: 1)

  have "rawpsubst φ (?uxs @ [(Var u, x)]) = rawpsubst (rawpsubst φ ?uxs) [(Var u, x)]"
  using Cons.prems by (intro rawpsubst_compose[symmetric]) (auto intro!: rawpsubst dest!: set_zip_D)
  also have "rawpsubst (rawpsubst φ ?uxs) [(Var u, x)] = subst (rawpsubst φ ?uxs) (Var u) x" by simp
  finally have "subst (rawpsubst φ (?uxs @ [(Var u, x)])) t u =
                subst (subst (rawpsubst φ ?uxs) (Var u) x) t u" by simp
  also have "… = subst (rawpsubst φ ?uxs) t x"
    using Cons 2 by (intro subst_subst) (auto intro!: rawpsubst dest!: set_zip_D)
  also have "… = rawpsubst φ ((t,x) # ?uxs)"
  using Cons.prems 3 apply(intro subst_rawpsubst_fresh_switch)
    subgoal by (auto dest!: set_zip_D)
    subgoal by (auto dest!: set_zip_D)
    subgoal by (auto dest!: set_zip_D)
    subgoal by (auto dest!: set_zip_D)
    subgoal by (fastforce dest!: set_zip_D)
    by (auto dest!: set_zip_D)
  also have "… =  rawpsubst φ ([(t,x)] @ ?uxs)" by simp
  also have "… = rawpsubst (rawpsubst φ [(t,x)]) ?uxs"
    using Cons.prems by (intro rawpsubst_compose[symmetric]) (auto dest!: set_zip_D)
  finally have "rawpsubst (subst (rawpsubst φ (?uxs @ [(Var u, x)])) t u) ?tus =
                rawpsubst (rawpsubst (rawpsubst φ [(t,x)]) ?uxs) ?tus" by auto
  hence "rawpsubst (rawpsubst φ ?uuxs) ?ttxs = rawpsubst (rawpsubst (rawpsubst φ [(t,x)]) ?uxs) ?tus"
    using 00 by auto
  also have "… = rawpsubst (rawpsubst φ [(t,x)]) txs"
    using Cons.prems apply (intro Cons.IH rawpsubst)
    subgoal by (auto dest!: set_zip_D in_Fvars_substD)
    subgoal by (auto dest!: set_zip_D in_Fvars_substD)
    subgoal by (auto dest!: set_zip_D in_Fvars_substD)
    subgoal by (auto dest!: set_zip_D in_Fvars_substD)
    subgoal by (auto dest!: set_zip_D in_Fvars_substD)
    subgoal by (auto dest!: set_zip_D in_Fvars_substD)
    subgoal by (metis Suc_mono diff_Suc_1 length_Cons nat.simps(3) nth_Cons')
    by (auto dest!: set_zip_D in_Fvars_substD)
  also have "… = rawpsubst φ ([(t,x)] @ txs)"
    using Cons.prems by (intro rawpsubst_compose) (auto dest!: set_zip_D)
  finally show ?case by simp
qed auto

lemma rawpsubst_compose_freshVar2_aux:
  assumes φ[simp]: "φ ∈ fmla"
    and ts: "set ts ⊆ trm"
    and xs: "set xs ⊆ var"  "distinct xs"
    and us_facts: "set us ⊆ var"  "distinct us"
    "set us ∩ Fvars φ = {}"
    "set us ∩ ⋃ (FvarsT ` (set ts)) = {}"
    "set us ∩ set xs = {}"
    and vs_facts: "set vs ⊆ var"  "distinct vs"
    "set vs ∩ Fvars φ = {}"
    "set vs ∩ ⋃ (FvarsT ` (set ts)) = {}"
    "set vs ∩ set xs = {}"
    and l: "length us = length xs" "length vs = length xs" "length ts = length xs"
    and (* Extra hypothesis, only to get induction through: *) d: "set us ∩ set vs = {}"
  shows "rawpsubst (rawpsubst φ (zip (map Var us) xs)) (zip ts us) =
       rawpsubst (rawpsubst φ (zip (map Var vs) xs)) (zip ts vs)"
  using assms proof(induction xs arbitrary: φ ts us vs)
  case (Cons x xs φ tts uus vvs)
  obtain t ts u us v vs where tts[simp]: "tts = t # ts" and lts[simp]: "length ts = length xs"
    and uus[simp]: "uus = u # us" and lus[simp]: "length us = length xs"
    and vvs[simp]: "vvs = v # vs" and lvs[simp]: "length vs = length xs"
    using ‹length uus = length (x # xs)› ‹length vvs = length (x # xs)› ‹length tts = length (x # xs)›
    apply(cases tts)
    subgoal by auto
    subgoal apply(cases uus)
      subgoal by auto
      subgoal by (cases vvs) auto . .

  let ?φux = "subst φ (Var u) x"   let ?φvx = "subst φ (Var v) x"

  have 0: "rawpsubst (rawpsubst ?φux (zip (map Var us) xs)) (zip ts us) =
           rawpsubst (rawpsubst ?φux (zip (map Var vs) xs)) (zip ts vs)"
    apply(rule Cons.IH) using Cons.prems by (auto intro!: rawpsubst dest!: set_zip_D)

  have 1: "rawpsubst ?φux (zip (map Var vs) xs) =
           subst (rawpsubst φ (zip (map Var vs) xs)) (Var u) x"
    using Cons.prems
    by (intro subst_rawpsubst_fresh_switch[simplified,symmetric])
       (force intro!: rawpsubst dest!: set_zip_D simp: subset_eq)+

  have 11: "rawpsubst ?φvx (zip (map Var vs) xs) =
           subst (rawpsubst φ (zip (map Var vs) xs)) (Var v) x"
    using Cons.prems
    by (intro subst_rawpsubst_fresh_switch[simplified,symmetric])
       (auto intro!: rawpsubst dest!: set_zip_D simp: subset_eq)

  have "subst (subst (rawpsubst φ (zip (map Var vs) xs)) (Var u) x) t u =
        subst (rawpsubst φ (zip (map Var vs) xs)) t x"
  using Cons.prems
  by (intro subst_subst) (force intro!: rawpsubst dest!: set_zip_D in_Fvars_rawpsubst_imp simp: Fvars_rawpsubst)+
  also have "… = subst (subst (rawpsubst φ (zip (map Var vs) xs)) (Var v) x) t v"
  using Cons.prems
  by (intro subst_subst[symmetric])
     (force intro!: rawpsubst dest!: set_zip_D in_Fvars_rawpsubst_imp simp: Fvars_rawpsubst)+

  finally have
    2: "subst (subst (rawpsubst φ (zip (map Var vs) xs)) (Var u) x) t u =
      subst (subst (rawpsubst φ (zip (map Var vs) xs)) (Var v) x) t v"  .

  have "rawpsubst (subst (rawpsubst ?φux (zip (map Var us) xs)) t u) (zip ts us) =
        subst (rawpsubst (rawpsubst ?φux (zip (map Var us) xs)) (zip ts us)) t u"
    using Cons.prems
    by (intro subst_rawpsubst_fresh_switch[simplified,symmetric]) (auto intro!: rawpsubst dest!: set_zip_D)
  also have "… = subst (rawpsubst (rawpsubst ?φux (zip (map Var vs) xs)) (zip ts vs)) t u"
    unfolding 0 ..
  also have "… = rawpsubst (subst (rawpsubst ?φux (zip (map Var vs) xs)) t u) (zip ts vs)"
    using Cons.prems
    by (intro subst_rawpsubst_fresh_switch[simplified]) (auto intro!: rawpsubst dest!: set_zip_D)
  also have "… = rawpsubst (subst (subst (rawpsubst φ (zip (map Var vs) xs)) (Var u) x) t u) (zip ts vs)"
    unfolding 1 ..
  also have "… = rawpsubst (subst (subst (rawpsubst φ (zip (map Var vs) xs)) (Var v) x) t v) (zip ts vs)"
    unfolding 2 ..
  also have "… = rawpsubst (subst (rawpsubst ?φvx (zip (map Var vs) xs)) t v) (zip ts vs)"
    unfolding 11 ..
  finally have "rawpsubst (subst (rawpsubst ?φux (zip (map Var us) xs)) t u) (zip ts us) =
        rawpsubst (subst (rawpsubst ?φvx (zip (map Var vs) xs)) t v) (zip ts vs)" .
  thus ?case by simp
qed auto

text ‹... now getting rid of the disjointness hypothesis:›

lemma rawpsubst_compose_freshVar2:
  assumes φ[simp]: "φ ∈ fmla"
    and ts: "set ts ⊆ trm"
    and xs: "set xs ⊆ var"  "distinct xs"
    and us_facts: "set us ⊆ var"  "distinct us"
    "set us ∩ Fvars φ = {}"
    "set us ∩ ⋃ (FvarsT ` (set ts)) = {}"
    "set us ∩ set xs = {}"
    and vs_facts: "set vs ⊆ var"  "distinct vs"
    "set vs ∩ Fvars φ = {}"
    "set vs ∩ ⋃ (FvarsT ` (set ts)) = {}"
    "set vs ∩ set xs = {}"
    and l: "length us = length xs" "length vs = length xs" "length ts = length xs"
  shows "rawpsubst (rawpsubst φ (zip (map Var us) xs)) (zip ts us) =
       rawpsubst (rawpsubst φ (zip (map Var vs) xs)) (zip ts vs)"  (is "?L = ?R")
proof-
  define ws where "ws = getFrN (xs @ us @ vs) ts [φ] (length xs)"
  note fv = getFrN_Fvars[of "xs @ us @ vs" "ts" "[φ]" _ "length xs"]
  and fvt = getFrN_FvarsT[of "xs @ us @ vs" "ts" "[φ]" _ "length xs"]
  and var = getFrN_var[of "xs @ us @ vs" "ts" "[φ]" _ "length xs"]
  and l = getFrN_length[of "xs @ us @ vs" "ts" "[φ]" "length xs"]
  have ws_facts: "set ws ⊆ var"  "distinct ws"
    "set ws ∩ Fvars φ = {}"
    "set ws ∩ ⋃ (FvarsT ` (set ts)) = {}"
    "set ws ∩ set xs = {}" "set ws ∩ set us = {}" "set ws ∩ set vs = {}"
    "length ws = length xs" using assms unfolding ws_def
    apply -
    subgoal by auto
    subgoal by auto
    subgoal using fv by auto
    subgoal using fvt IntI empty_iff by fastforce
    subgoal using var IntI empty_iff by fastforce
    subgoal using var IntI empty_iff by fastforce
    subgoal using var IntI empty_iff by fastforce
    subgoal using l by auto  .
  have "?L = rawpsubst (rawpsubst φ (zip (map Var ws) xs)) (zip ts ws)"
    apply(rule rawpsubst_compose_freshVar2_aux) using assms ws_facts by auto
  also have "… = ?R"
    apply(rule rawpsubst_compose_freshVar2_aux) using assms ws_facts by auto
  finally show ?thesis .
qed

lemma psubst_subst_fresh_switch:
  assumes "φ ∈ fmla" "snd ` set txs ⊆ var" "fst ` set txs ⊆ trm"
    and "∀x∈snd ` set txs. x ∉ FvarsT s" "∀t∈fst ` set txs. y ∉ FvarsT t"
    and "distinct (map snd txs)"
    and "s ∈ trm" "y ∈ var" "y ∉ snd ` set txs"
  shows "psubst (subst φ s y) txs = subst (psubst φ txs) s y"
proof-
  define us where us: "us = getFrN (map snd txs) (map fst txs) [φ] (length txs)"
  note fvt = getFrN_FvarsT[of "map snd txs" "map fst txs" "[φ]" _ "length txs"]
  and fv = getFrN_Fvars[of "map snd txs" "map fst txs" "[φ]" _ "length txs"]
  and var = getFrN_var[of "map snd txs" "map fst txs" "[φ]" _ "length txs"]
  and l = getFrN_length[of "map snd txs" "map fst txs" "[φ]" "length txs"]

  have us_facts: "set us ⊆ var"
    "set us ∩ Fvars φ = {}"
    "set us ∩ ⋃ (FvarsT ` (fst ` (set txs))) = {}"
    "set us ∩ snd ` (set txs) = {}"
    "length us = length txs"
    "distinct us"
  using assms unfolding us apply -
  subgoal by auto
  subgoal using fv by (cases txs, auto)
  subgoal using fvt by (cases txs, auto)
  subgoal using var by (cases txs, auto)
  subgoal using l by auto
  subgoal by auto .

  define vs where vs: "vs = getFrN (map snd txs) (map fst txs) [subst φ s y] (length txs)"
  note fvt = getFrN_FvarsT[of "map snd txs" "map fst txs" "[subst φ s y]" _ "length txs"]
  and fv = getFrN_Fvars[of "map snd txs" "map fst txs" "[subst φ s y]" _ "length txs"]
  and var = getFrN_var[of "map snd txs" "map fst txs" "[subst φ s y]" _ "length txs"]
  and l = getFrN_length[of "map snd txs" "map fst txs" "[subst φ s y]" "length txs"]

  have vs_facts: "set vs ⊆ var"
    "set vs ∩ Fvars (subst φ s y) = {}"
    "set vs ∩ ⋃ (FvarsT ` (fst ` (set txs))) = {}"
    "set vs ∩ snd ` (set txs) = {}"
    "length vs = length txs"
    "distinct vs"
  using assms unfolding vs apply -
  subgoal by auto
  subgoal using fv by (cases txs, auto)
  subgoal using fvt by (cases txs, auto)
  subgoal using var by (cases txs, auto)
  subgoal using l by auto
  subgoal by auto .

  define ws where ws: "ws = getFrN (y # map snd txs) (s # map fst txs) [φ] (length txs)"
  note fvt = getFrN_FvarsT[of "y # map snd txs" "s # map fst txs" "[φ]" _ "length txs"]
  and fv = getFrN_Fvars[of "y # map snd txs" "s # map fst txs" "[φ]" _ "length txs"]
  and var = getFrN_var[of "y # map snd txs" "s # map fst txs" "[φ]" _ "length txs"]
  and l = getFrN_length[of "y # map snd txs" "s # map fst txs" "[φ]" "length txs"]

  have ws_facts: "set ws ⊆ var"
    "set ws ∩ Fvars φ = {}" "y ∉ set ws" "set ws ∩ FvarsT s = {}"
    "set ws ∩ ⋃ (FvarsT ` (fst ` (set txs))) = {}"
    "set ws ∩ snd ` (set txs) = {}"
    "length ws = length txs"
    "distinct ws"
  using assms unfolding ws apply -
  subgoal by auto
  subgoal using fv by (cases txs, auto)
  subgoal using var by (cases txs, auto)
  subgoal using fvt  by (cases txs, auto)
  subgoal using fvt by (cases txs, auto)
  subgoal using var by (cases txs, auto)
  subgoal using l by (cases txs, auto)
  by auto

  let ?vxs = "zip (map Var vs) (map snd txs)"
  let ?tvs = "(zip (map fst txs) vs)"
  let ?uxs = "zip (map Var us) (map snd txs)"
  let ?tus = "(zip (map fst txs) us)"
  let ?wxs = "zip (map Var ws) (map snd txs)"
  let ?tws = "(zip (map fst txs) ws)"

  have 0: "rawpsubst (subst φ s y) ?wxs = subst (rawpsubst φ ?wxs) s y"
  apply(subst rawpsubst_compose[of φ ?wxs  "[(s,y)]",simplified])
  using assms ws_facts apply -
  subgoal by auto
  subgoal by (auto dest!: set_zip_D)
  subgoal by (auto dest!: set_zip_D)
  subgoal by auto
  subgoal by auto
  subgoal apply(subst rawpsubst_subst_fresh_switch)
    by (auto dest!: set_zip_D simp: subset_eq rawpsubst_subst_fresh_switch) .

  have 1: "rawpsubst (rawpsubst φ ?wxs) ?tws = rawpsubst (rawpsubst φ ?uxs) ?tus"
    using assms ws_facts us_facts by (intro rawpsubst_compose_freshVar2) (auto simp: subset_eq)

  have "rawpsubst (rawpsubst (subst φ s y) ?vxs) ?tvs =
        rawpsubst (rawpsubst (subst φ s y) ?wxs) ?tws"
    using assms ws_facts vs_facts
    by (intro rawpsubst_compose_freshVar2)  (auto simp: subset_eq)
  also have "… = rawpsubst (subst (rawpsubst φ ?wxs) s y) ?tws" unfolding 0 ..
  also have "… = subst (rawpsubst (rawpsubst φ ?wxs) ?tws) s y"
  apply(subst rawpsubst_compose[of "rawpsubst φ ?wxs" ?tws  "[(s,y)]",simplified])
  using assms ws_facts apply -
  subgoal by (auto dest!: set_zip_D simp: subset_eq intro!: rawpsubst)
  subgoal by (auto dest!: set_zip_D)
  subgoal by (auto dest!: set_zip_D)
  subgoal by auto
  subgoal by auto
  subgoal by (subst rawpsubst_subst_fresh_switch)
    (auto dest!: set_zip_D simp: subset_eq rawpsubst_subst_fresh_switch
          intro!: rawpsubst) .
  also have "… = subst (rawpsubst (rawpsubst φ ?uxs) ?tus) s y" unfolding 1 ..
  finally show  ?thesis unfolding psubst_def by (simp add: Let_def vs[symmetric] us[symmetric])
qed

text ‹For many cases, the simpler rawpsubst can replace psubst:›

lemma psubst_eq_rawpsubst:
  assumes "φ ∈ fmla" "snd ` (set txs) ⊆ var" and "fst ` (set txs) ⊆ trm"
    and "distinct (map snd txs)"
    (* ... namely, when the substituted variables do not belong to trms substituted for previous variables: *)
    and "⋀ i j. i < j ⟹ j < length txs ⟹ snd (txs!j) ∉ FvarsT (fst (txs!i))"
  shows "psubst φ txs = rawpsubst φ txs"
proof-
  define us where us: "us = getFrN (map snd txs) (map fst txs) [φ] (length txs)"
  note fvt = getFrN_FvarsT[of "map snd txs" "map fst txs" "[φ]" _ "length txs"]
  and fv = getFrN_Fvars[of "map snd txs" "map fst txs" "[φ]" _ "length txs"]
  and var = getFrN_var[of "map snd txs" "map fst txs" "[φ]" _ "length txs"]
  and l = getFrN_length[of "map snd txs" "map fst txs" "[φ]" "length txs"]
  have us_facts: "set us ⊆ var"
    "set us ∩ Fvars φ = {}"
    "set us ∩ ⋃ (FvarsT ` (fst ` (set txs))) = {}"
    "set us ∩ snd ` (set txs) = {}"
    "length us = length txs"
    "distinct us"
    using assms unfolding us
    apply -
    subgoal by auto
    subgoal using fv by auto
    subgoal using fvt by force
    subgoal using var by (force simp: image_iff)
    using l by auto
  show ?thesis
    using rawpsubst_compose_freshVar assms us_facts
    by (simp add: psubst_def Let_def us[symmetric])
qed

text ‹Some particular cases:›

lemma psubst_eq_subst:
  assumes "φ ∈ fmla" "x ∈ var" and "t ∈ trm"
  shows "psubst φ [(t,x)] = subst φ t x"
proof-
  have "psubst φ [(t,x)] = rawpsubst φ [(t,x)]" apply(rule psubst_eq_rawpsubst)
    using assms by auto
  thus ?thesis by auto
qed

lemma psubst_eq_rawpsubst2:
  assumes "φ ∈ fmla" "x1 ∈ var" "x2 ∈ var" "t1 ∈ trm" "t2 ∈ trm"
    and "x1 ≠ x2" "x2 ∉ FvarsT t1"
  shows "psubst φ [(t1,x1),(t2,x2)] = rawpsubst φ [(t1,x1),(t2,x2)]"
  apply(rule psubst_eq_rawpsubst)
  using assms using less_SucE by force+

lemma psubst_eq_rawpsubst3:
  assumes "φ ∈ fmla" "x1 ∈ var" "x2 ∈ var" "x3 ∈ var" "t1 ∈ trm" "t2 ∈ trm" "t3 ∈ trm"
    and "x1 ≠ x2" "x1 ≠ x3" "x2 ≠ x3"
    "x2 ∉ FvarsT t1" "x3 ∉ FvarsT t1" "x3 ∉ FvarsT t2"
  shows "psubst φ [(t1,x1),(t2,x2),(t3,x3)] = rawpsubst φ [(t1,x1),(t2,x2),(t3,x3)]"
  using assms using less_SucE apply(intro psubst_eq_rawpsubst)
  subgoal by auto
  subgoal by auto
  subgoal by auto
  subgoal by auto
  subgoal for i j
    apply(cases j)
    subgoal by auto
    subgoal by (simp add: nth_Cons') . .

lemma psubst_eq_rawpsubst4:
  assumes "φ ∈ fmla" "x1 ∈ var" "x2 ∈ var" "x3 ∈ var" "x4 ∈ var"
    "t1 ∈ trm" "t2 ∈ trm" "t3 ∈ trm" "t4 ∈ trm"
    and "x1 ≠ x2" "x1 ≠ x3" "x2 ≠ x3" "x1 ≠ x4" "x2 ≠ x4" "x3 ≠ x4"
    "x2 ∉ FvarsT t1" "x3 ∉ FvarsT t1" "x3 ∉ FvarsT t2" "x4 ∉ FvarsT t1" "x4 ∉ FvarsT t2" "x4 ∉ FvarsT t3"
  shows "psubst φ [(t1,x1),(t2,x2),(t3,x3),(t4,x4)] = rawpsubst φ [(t1,x1),(t2,x2),(t3,x3),(t4,x4)]"
  using assms using less_SucE apply(intro psubst_eq_rawpsubst)
  subgoal by auto
  subgoal by auto
  subgoal by auto
  subgoal by auto
  subgoal for i j
    apply(cases j)
    subgoal by auto
    subgoal by (simp add: nth_Cons') . .

lemma rawpsubst_same_Var[simp]:
  assumes "φ ∈ fmla" "set xs ⊆ var"
  shows "rawpsubst φ (map (λx. (Var x,x)) xs) = φ"
  using assms by (induct xs) auto

lemma psubst_same_Var[simp]:
  assumes "φ ∈ fmla" "set xs ⊆ var" and "distinct xs"
  shows "psubst φ (map (λx. (Var x,x)) xs) = φ"
proof-
  have "psubst φ (map (λx. (Var x,x)) xs) = rawpsubst φ (map (λx. (Var x,x)) xs)"
  using assms by (intro psubst_eq_rawpsubst) (auto simp: nth_eq_iff_index_eq subsetD)
  thus ?thesis using assms by auto
qed

lemma rawpsubst_notIn[simp]:
  assumes "snd ` (set txs) ⊆ var" "fst ` (set txs) ⊆ trm" "φ ∈ fmla"
    and "Fvars φ ∩ snd ` (set txs) = {}"
  shows "rawpsubst φ txs = φ"
  using assms by (induct txs) auto

lemma psubst_notIn[simp]:
  assumes "x ∈ var" "snd ` (set txs) ⊆ var" "fst ` (set txs) ⊆ trm" "φ ∈ fmla"
    and  "Fvars φ ∩ snd ` (set txs) = {}"
  shows "psubst φ txs = φ"
proof-
  define us where us: "us = getFrN (map snd txs) (map fst txs) [φ] (length txs)"
  have us_facts: "set us ⊆ var"
    "set us ∩ Fvars φ = {}"
    "set us ∩ ⋃ (FvarsT ` (fst ` (set txs))) = {}"
    "set us ∩ snd ` (set txs) = {}"
    "length us = length txs"
    using getFrN_Fvars[of "map snd txs" "map fst txs" "[φ]" _ "length txs"]
      getFrN_FvarsT[of "map snd txs" "map fst txs" "[φ]" _ "length<