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 txs"]
      getFrN_var[of "map snd txs" "map fst txs" "[φ]" _ "length txs"]
      getFrN_length[of "map snd txs" "map fst txs" "[φ]" "length txs"]
    using assms unfolding us apply -
    subgoal by auto
    subgoal by auto
    subgoal by auto
    subgoal by (fastforce simp: image_iff)
    subgoal by auto .
    (* *)
  have [simp]: "rawpsubst φ (zip (map Var us) (map snd txs)) = φ"
  using assms us_facts apply(intro rawpsubst_notIn)
  subgoal by (auto dest!: set_zip_rightD)
  subgoal by (auto dest!: set_zip_leftD)
  subgoal by auto
  subgoal by (auto dest!: set_zip_rightD) .
  have [simp]: "rawpsubst φ (zip (map fst txs) us) = φ"
    using assms us_facts apply(intro rawpsubst_notIn)
  subgoal by (auto dest!: set_zip_rightD)
  subgoal by (auto dest!: set_zip_leftD)
  subgoal by auto
  subgoal by (auto dest!: set_zip_rightD) .
  show ?thesis using assms us_facts unfolding psubst_def
    by(auto simp: Let_def us[symmetric])
qed

end ― ‹context @{locale Generic_Syntax}›


section ‹Adding Numerals to the Generic Syntax›

locale Syntax_with_Numerals =
  Generic_Syntax var trm fmla Var FvarsT substT Fvars subst
  for var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
    and Var FvarsT substT Fvars subst
    +
  fixes
    ― ‹Abstract notion of numerals, as a subset of the ground terms:›
    num :: "'trm set"
  assumes
    numNE: "num ≠ {}"
    and
    num: "num ⊆ trm"
    and
    FvarsT_num[simp, intro!]: "⋀n. n ∈ num ⟹ FvarsT n = {}"
begin

lemma substT_num1[simp]: "t ∈ trm ⟹ y ∈ var ⟹ n ∈ num ⟹ substT n t y = n"
  using num by auto

lemma in_num[simp]: "n ∈ num ⟹ n ∈ trm" using num by auto

lemma subst_comp_num:
  assumes "φ ∈ fmla" "x ∈ var" "y ∈ var" "n ∈ num"
  shows "x ≠ y ⟹ subst (subst φ (Var x) y) n x = subst (subst φ n x) n y"
  using assms by (simp add: subst_comp)

lemma rawpsubstT_num:
  assumes "snd ` (set txs) ⊆ var" "fst ` (set txs) ⊆ trm" "n ∈ num"
  shows "rawpsubstT n txs = n"
  using assms by (induct txs) auto

lemma psubstT_num[simp]:
  assumes "snd ` (set txs) ⊆ var" "fst ` (set txs) ⊆ trm" "n ∈ num"
  shows "psubstT n txs = n"
proof-
  define us where us: "us = getFrN (map snd txs) (n # map fst txs) [] (length txs)"
  have us_facts: "set us ⊆ var"
    "set us ∩ FvarsT n = {}"
    "set us ∩ ⋃ (FvarsT ` (fst ` (set txs))) = {}"
    "set us ∩ snd ` (set txs) = {}"
    "length us = length txs"
    using assms unfolding us
    using getFrN_Fvars[of "map snd txs" "n # map fst txs" "[]" _ "length txs"]
      getFrN_FvarsT[of "map snd txs" "n # map fst txs" "[]" _ "length txs"]
      getFrN_var[of "map snd txs" "n # map fst txs" "[]" _ "length txs"]
      getFrN_length[of "map snd txs" "n # map fst txs" "[]" "length txs"]
    by (auto 7 0 simp: set_eq_iff image_iff)
  let ?t = "rawpsubstT n (zip (map Var us) (map snd txs))"
  have t: "?t = n"
  using assms us_facts apply(intro rawpsubstT_num)
  subgoal by (auto dest!: set_zip_rightD)
  subgoal by (auto dest!: set_zip_leftD)
  subgoal by auto .
  have "rawpsubstT ?t (zip (map fst txs) us) = n"
  unfolding t using assms us_facts apply(intro rawpsubstT_num)
  subgoal by (auto dest!: set_zip_rightD)
  subgoal by (auto dest!: set_zip_leftD)
  subgoal by auto .
  thus ?thesis unfolding psubstT_def by(simp add: Let_def us[symmetric])
qed

end ― ‹context @{locale Syntax_with_Numerals}›


section ‹Adding Connectives and Quantifiers›

locale Syntax_with_Connectives =
  Generic_Syntax var trm fmla Var FvarsT substT Fvars subst
  for
    var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
    and Var FvarsT substT Fvars subst
    +
  fixes
    ― ‹Logical connectives›
    eql :: "'trm ⇒ 'trm ⇒ 'fmla"
    and
    cnj :: "'fmla ⇒ 'fmla ⇒ 'fmla"
    and
    imp :: "'fmla ⇒ 'fmla ⇒ 'fmla"
    and
    all :: "'var ⇒ 'fmla ⇒ 'fmla"
    and
    exi :: "'var ⇒ 'fmla ⇒ 'fmla"
  assumes
    eql[simp,intro]: "⋀ t1 t2. t1 ∈ trm ⟹ t2 ∈ trm ⟹ eql t1 t2 ∈ fmla"
    and
    cnj[simp,intro]: "⋀ φ1 φ2. φ1 ∈ fmla ⟹ φ2 ∈ fmla ⟹ cnj φ1 φ2 ∈ fmla"
    and
    imp[simp,intro]: "⋀ φ1 φ2. φ1 ∈ fmla ⟹ φ2 ∈ fmla ⟹ imp φ1 φ2 ∈ fmla"
    and
    all[simp,intro]: "⋀ x φ. x ∈ var ⟹ φ ∈ fmla ⟹ all x φ ∈ fmla"
    and
    exi[simp,intro]: "⋀ x φ. x ∈ var ⟹ φ ∈ fmla ⟹ exi x φ ∈ fmla"
    and
    Fvars_eql[simp]:
    "⋀ t1 t2. t1 ∈ trm ⟹ t2 ∈ trm ⟹ Fvars (eql t1 t2) = FvarsT t1 ∪ FvarsT t2"
    and
    Fvars_cnj[simp]:
    "⋀ φ χ. φ ∈ fmla ⟹ χ ∈ fmla ⟹ Fvars (cnj φ χ) = Fvars φ ∪ Fvars χ"
    and
    Fvars_imp[simp]:
    "⋀ φ χ. φ ∈ fmla ⟹ χ ∈ fmla ⟹ Fvars (imp φ χ) = Fvars φ ∪ Fvars χ"
    and
    Fvars_all[simp]:
    "⋀ x φ. x ∈ var ⟹ φ ∈ fmla ⟹ Fvars (all x φ) = Fvars φ - {x}"
    and
    Fvars_exi[simp]:
    "⋀ x φ. x ∈ var ⟹ φ ∈ fmla ⟹ Fvars (exi x φ) = Fvars φ - {x}"
    and
    ― ‹Assumed properties of substitution›
    subst_cnj[simp]:
    "⋀ x φ χ t. φ ∈ fmla ⟹ χ ∈ fmla ⟹ t ∈ trm ⟹ x ∈ var ⟹
      subst (cnj φ χ) t x = cnj (subst φ t x) (subst χ t x)"
    and
    subst_imp[simp]:
    "⋀ x φ χ t. φ ∈ fmla ⟹ χ ∈ fmla ⟹ t ∈ trm ⟹ x ∈ var ⟹
      subst (imp φ χ) t x = imp (subst φ t x) (subst χ t x)"
    and
    subst_all[simp]:
    "⋀ x y φ t. φ ∈ fmla ⟹ t ∈ trm ⟹ x ∈ var ⟹ y ∈ var ⟹
      x ≠ y ⟹ x ∉ FvarsT t ⟹ subst (all x φ) t y = all x (subst φ t y)"
    and
    subst_exi[simp]:
    "⋀ x y φ t. φ ∈ fmla ⟹ t ∈ trm ⟹ x ∈ var ⟹ y ∈ var ⟹
      x ≠ y ⟹ x ∉ FvarsT t ⟹ subst (exi x φ) t y = exi x (subst φ t y)"
    and
    subst_eql[simp]:
    "⋀ t1 t2 t x. t ∈ trm ⟹ t1 ∈ trm ⟹ t2 ∈ trm ⟹ x ∈ var ⟹
      subst (eql t1 t2) t x = eql (substT t1 t x) (substT t2 t x)"
begin

(*
(* "is the unique": isTU t x φ is the formula "t is the unique x such that phi(x)"
 *)
definition isTU :: "'trm ⇒ 'var ⇒ 'fmla  ⇒ 'fmla" where
"isTU t x φ ≡
 cnj (subst φ t x)
     (all x (imp φ (subst φ t x)))"

(* TODO: properties: works well when x is not free in t,
in particular, when t is num n *)
*)

text ‹Formula equivalence, $\longleftrightarrow$, a derived connective›

definition eqv :: "'fmla ⇒ 'fmla ⇒ 'fmla" where
  "eqv φ χ = cnj (imp φ χ) (imp χ φ)"

lemma
  eqv[simp]: "⋀φ χ. φ ∈ fmla ⟹ χ ∈ fmla ⟹ eqv φ χ ∈ fmla"
  and
  Fvars_eqv[simp]: "⋀φ χ. φ ∈ fmla ⟹ χ ∈ fmla ⟹
  Fvars (eqv φ χ)  = Fvars φ ∪ Fvars χ"
  and
  subst_eqv[simp]:
  "⋀φ χ t x. φ ∈ fmla ⟹ χ ∈ fmla ⟹ t ∈ trm ⟹ x ∈ var ⟹
  subst (eqv φ χ) t x = eqv (subst φ t x) (subst χ t x)"
  unfolding eqv_def by auto

lemma subst_all_idle[simp]:
assumes [simp]: "x ∈ var" "φ ∈ fmla" "t ∈ trm"
shows "subst (all x φ) t x = all x φ"
by (intro subst_notIn) auto

lemma subst_exi_idle[simp]:
assumes [simp]: "x ∈ var" "φ ∈ fmla" "t ∈ trm"
shows "subst (exi x φ) t x = exi x φ"
by (rule subst_notIn) auto


text ‹Parallel substitution versus connectives and quantifiers.›

lemma rawpsubst_cnj:
  assumes "φ1 ∈ fmla" "φ2 ∈ fmla"
    and "snd ` (set txs) ⊆ var" "fst ` (set txs) ⊆ trm"
  shows "rawpsubst (cnj φ1 φ2) txs = cnj (rawpsubst φ1 txs) (rawpsubst φ2 txs)"
  using assms by (induct txs arbitrary: φ1 φ2) auto

lemma psubst_cnj[simp]:
  assumes "φ1 ∈ fmla" "φ2 ∈ fmla"
    and "snd ` (set txs) ⊆ var" "fst ` (set txs) ⊆ trm"
    and "distinct (map snd txs)"
  shows "psubst (cnj φ1 φ2) txs = cnj (psubst φ1 txs) (psubst φ2 txs)"
proof-
  define us where us: "us = getFrN (map snd txs) (map fst txs) [cnj φ1 φ2] (length txs)"
  have us_facts: "set us ⊆ var"
    "set us ∩ Fvars φ1 = {}"
    "set us ∩ Fvars φ2 = {}"
    "set us ∩ ⋃ (FvarsT ` (fst ` (set txs))) = {}"
    "set us ∩ snd ` (set txs) = {}"
    "length us = length txs"
    "distinct us"
    using assms unfolding us
    using getFrN_Fvars[of "map snd txs" "map fst txs" "[cnj φ1 φ2]" _ "length txs"]
      getFrN_FvarsT[of "map snd txs" "map fst txs" "[cnj φ1 φ2]" _ "length txs"]
      getFrN_var[of "map snd txs" "map fst txs" "[cnj φ1 φ2]" _ "length txs"]
      getFrN_length[of "map snd txs" "map fst txs" "[cnj φ1 φ2]" "length txs"]
    apply -
    subgoal by auto
    subgoal by fastforce
    subgoal by fastforce
    subgoal by fastforce
    subgoal by (fastforce simp: image_iff)
    subgoal by auto
    subgoal by auto .
  define vs1 where vs1: "vs1 = getFrN (map snd txs) (map fst txs) [φ1] (length txs)"
  have vs1_facts: "set vs1  ⊆ var"
    "set vs1 ∩ Fvars φ1 = {}"
    "set vs1 ∩ ⋃ (FvarsT ` (fst ` (set txs))) = {}"
    "set vs1 ∩ snd ` (set txs) = {}"
    "length vs1 = length txs"
    "distinct vs1"
    using assms unfolding vs1
    using getFrN_Fvars[of "map snd txs" "map fst txs" "[φ1]" _ "length txs"]
      getFrN_FvarsT[of "map snd txs" "map fst txs" "[φ1]" _ "length txs"]
      getFrN_var[of "map snd txs" "map fst txs" "[φ1]" _ "length txs"]
      getFrN_length[of "map snd txs" "map fst txs" "[φ1]" "length txs"]
    apply -
    subgoal by auto
    subgoal by auto
    subgoal by fastforce
    subgoal by force
    subgoal by auto
    subgoal by auto .

  define vs2 where vs2: "vs2 = getFrN (map snd txs) (map fst txs) [φ2] (length txs)"
  have vs2_facts: "set vs2  ⊆ var"
    "set vs2 ∩ Fvars φ2 = {}"
    "set vs2 ∩ ⋃ (FvarsT ` (fst ` (set txs))) = {}"
    "set vs2 ∩ snd ` (set txs) = {}"
    "length vs2 = length txs"
    "distinct vs2"
    using assms unfolding vs2
    using getFrN_Fvars[of "map snd txs" "map fst txs" "[φ2]" _ "length txs"]
      getFrN_FvarsT[of "map snd txs" "map fst txs" "[φ2]" _ "length txs"]
      getFrN_var[of "map snd txs" "map fst txs" "[φ2]" _ "length txs"]
      getFrN_length[of "map snd txs" "map fst txs" "[φ2]" "length txs"]
    apply -
    subgoal by auto
    subgoal by auto
    subgoal by fastforce
    subgoal by force
    subgoal by auto
    subgoal by auto .

  let ?tus = "zip (map fst txs) us"
  let ?uxs = "zip (map Var us) (map snd txs)"
  let ?tvs1 = "zip (map fst txs) vs1"
  let ?vxs1 = "zip (map Var vs1) (map snd txs)"
  let ?tvs2 = "zip (map fst txs) vs2"
  let ?vxs2 = "zip (map Var vs2) (map snd txs)"

  let ?c = "rawpsubst (cnj φ1 φ2) ?uxs"
  have c: "?c = cnj (rawpsubst φ1 ?uxs) (rawpsubst φ2 ?uxs)"
    using assms us_facts
    by (intro rawpsubst_cnj) (auto intro!: rawpsubstT dest!: set_zip_D)
  have 0: "rawpsubst ?c ?tus =
    cnj (rawpsubst (rawpsubst φ1 ?uxs) ?tus) (rawpsubst (rawpsubst φ2 ?uxs) ?tus)"
    unfolding c using assms us_facts
    by (intro rawpsubst_cnj) (auto dest!: set_zip_D intro!: rawpsubst)

  have 1: "rawpsubst (rawpsubst φ1 ?uxs) ?tus = rawpsubst (rawpsubst φ1 ?vxs1) ?tvs1"
    using assms vs1_facts us_facts
    by (intro rawpsubst_compose_freshVar2) (auto intro!: rawpsubst)
  have 2: "rawpsubst (rawpsubst φ2 ?uxs) ?tus = rawpsubst (rawpsubst φ2 ?vxs2) ?tvs2"
    using assms vs2_facts us_facts
    by (intro rawpsubst_compose_freshVar2)(auto intro!: rawpsubst)
  show ?thesis unfolding psubst_def by (simp add: Let_def us[symmetric] vs1[symmetric] vs2[symmetric] 0 1 2)
qed

lemma rawpsubst_imp:
  assumes "φ1 ∈ fmla" "φ2 ∈ fmla"
    and "snd ` (set txs) ⊆ var" "fst ` (set txs) ⊆ trm"
  shows "rawpsubst (imp φ1 φ2) txs = imp (rawpsubst φ1 txs) (rawpsubst φ2 txs)"
  using assms apply (induct txs arbitrary: φ1 φ2)
  subgoal by auto
  subgoal for tx txs φ1 φ2 by (cases tx) auto .

lemma psubst_imp[simp]:
  assumes "φ1 ∈ fmla" "φ2 ∈ fmla"
    and "snd ` (set txs) ⊆ var" "fst ` (set txs) ⊆ trm"
    and "distinct (map snd txs)"
  shows "psubst (imp φ1 φ2) txs = imp (psubst φ1 txs) (psubst φ2 txs)"
proof-
  define us where us: "us = getFrN (map snd txs) (map fst txs) [imp φ1 φ2] (length txs)"
  have us_facts: "set us ⊆ var"
    "set us ∩ Fvars φ1 = {}"
    "set us ∩ Fvars φ2 = {}"
    "set us ∩ ⋃ (FvarsT ` (fst ` (set txs))) = {}"
    "set us ∩ snd ` (set txs) = {}"
    "length us = length txs"
    "distinct us"
    using assms unfolding us
    using getFrN_Fvars[of "map snd txs" "map fst txs" "[imp φ1 φ2]" _ "length txs"]
      getFrN_FvarsT[of "map snd txs" "map fst txs" "[imp φ1 φ2]" _ "length txs"]
      getFrN_var[of "map snd txs" "map fst txs" "[imp φ1 φ2]" _ "length txs"]
      getFrN_length[of "map snd txs" "map fst txs" "[imp φ1 φ2]" "length txs"]
    apply -
    subgoal by auto
    subgoal by fastforce
    subgoal by fastforce
    subgoal by fastforce
    subgoal by (fastforce simp: image_iff)
    by auto

  define vs1 where vs1: "vs1 = getFrN (map snd txs) (map fst txs) [φ1] (length txs)"
  have vs1_facts: "set vs1  ⊆ var"
    "set vs1 ∩ Fvars φ1 = {}"
    "set vs1 ∩ ⋃ (FvarsT ` (fst ` (set txs))) = {}"
    "set vs1 ∩ snd ` (set txs) = {}"
    "length vs1 = length txs"
    "distinct vs1"
    using assms unfolding vs1
    using getFrN_Fvars[of "map snd txs" "map fst txs" "[φ1]" _ "length txs"]
      getFrN_FvarsT[of "map snd txs" "map fst txs" "[φ1]" _ "length txs"]
      getFrN_var[of "map snd txs" "map fst txs" "[φ1]" _ "length txs"]
      getFrN_length[of "map snd txs" "map fst txs" "[φ1]" "length txs"]
    apply -
    subgoal by auto
    subgoal by auto
    subgoal by fastforce
    subgoal by force
    by auto

  define vs2 where vs2: "vs2 = getFrN (map snd txs) (map fst txs) [φ2] (length txs)"
  have vs2_facts: "set vs2  ⊆ var"
    "set vs2 ∩ Fvars φ2 = {}"
    "set vs2 ∩ ⋃ (FvarsT ` (fst ` (set txs))) = {}"
    "set vs2 ∩ snd ` (set txs) = {}"
    "length vs2 = length txs"
    "distinct vs2"
    using assms unfolding vs2
    using getFrN_Fvars[of "map snd txs" "map fst txs" "[φ2]" _ "length txs"]
      getFrN_FvarsT[of "map snd txs" "map fst txs" "[φ2]" _ "length txs"]
      getFrN_var[of "map snd txs" "map fst txs" "[φ2]" _ "length txs"]
      getFrN_length[of "map snd txs" "map fst txs" "[φ2]" "length txs"]
    apply -
    subgoal by auto
    subgoal by auto
    subgoal by fastforce
    subgoal by force
    by auto

  let ?tus = "zip (map fst txs) us"
  let ?uxs = "zip (map Var us) (map snd txs)"
  let ?tvs1 = "zip (map fst txs) vs1"
  let ?vxs1 = "zip (map Var vs1) (map snd txs)"
  let ?tvs2 = "zip (map fst txs) vs2"
  let ?vxs2 = "zip (map Var vs2) (map snd txs)"

  let ?c = "rawpsubst (imp φ1 φ2) ?uxs"
  have c: "?c = imp (rawpsubst φ1 ?uxs) (rawpsubst φ2 ?uxs)"
    apply(rule rawpsubst_imp) using assms us_facts apply (auto intro!: rawpsubstT)
    apply(drule set_zip_rightD) apply simp apply blast
    apply(drule set_zip_leftD) apply simp apply blast .
  have 0: "rawpsubst ?c ?tus =
    imp (rawpsubst (rawpsubst φ1 ?uxs) ?tus) (rawpsubst (rawpsubst φ2 ?uxs) ?tus)"
    unfolding c
    using assms us_facts
    by (intro rawpsubst_imp) (auto intro!: rawpsubst dest!: set_zip_D)
  have 1: "rawpsubst (rawpsubst φ1 ?uxs) ?tus = rawpsubst (rawpsubst φ1 ?vxs1) ?tvs1"
    using assms vs1_facts us_facts
    by (intro rawpsubst_compose_freshVar2) (auto intro!: rawpsubst)
  have 2: "rawpsubst (rawpsubst φ2 ?uxs) ?tus = rawpsubst (rawpsubst φ2 ?vxs2) ?tvs2"
    using assms vs2_facts us_facts
    by (intro rawpsubst_compose_freshVar2) (auto intro!: rawpsubst)
  show ?thesis unfolding psubst_def by (simp add: Let_def us[symmetric] vs1[symmetric] vs2[symmetric] 0 1 2)
qed

lemma rawpsubst_eqv:
  assumes "φ1 ∈ fmla" "φ2 ∈ fmla"
    and "snd ` (set txs) ⊆ var" "fst ` (set txs) ⊆ trm"
  shows "rawpsubst (eqv φ1 φ2) txs = eqv (rawpsubst φ1 txs) (rawpsubst φ2 txs)"
  using assms apply (induct txs arbitrary: φ1 φ2)
  subgoal by auto
  subgoal for tx txs φ1 φ2 by (cases tx) auto .

lemma psubst_eqv[simp]:
  assumes "φ1 ∈ fmla" "φ2 ∈ fmla"
    and "snd ` (set txs) ⊆ var" "fst ` (set txs) ⊆ trm"
    and "distinct (map snd txs)"
  shows "psubst (eqv φ1 φ2) txs = eqv (psubst φ1 txs) (psubst φ2 txs)"
proof-
  define us where us: "us = getFrN (map snd txs) (map fst txs) [eqv φ1 φ2] (length txs)"
  have us_facts: "set us ⊆ var"
    "set us ∩ Fvars φ1 = {}"
    "set us ∩ Fvars φ2 = {}"
    "set us ∩ ⋃ (FvarsT ` (fst ` (set txs))) = {}"
    "set us ∩ snd ` (set txs) = {}"
    "length us = length txs"
    "distinct us"
    using assms unfolding us
    using getFrN_Fvars[of "map snd txs" "map fst txs" "[eqv φ1 φ2]" _ "length txs"]
      getFrN_FvarsT[of "map snd txs" "map fst txs" "[eqv φ1 φ2]" _ "length txs"]
      getFrN_var[of "map snd txs" "map fst txs" "[eqv φ1 φ2]" _ "length txs"]
      getFrN_length[of "map snd txs" "map fst txs" "[eqv φ1 φ2]" "length txs"]
    apply -
    subgoal by auto
    subgoal by fastforce
    subgoal by fastforce
    subgoal by fastforce
    subgoal by (fastforce simp: image_iff)
    by auto

  define vs1 where vs1: "vs1 = getFrN (map snd txs) (map fst txs) [φ1] (length txs)"
  have vs1_facts: "set vs1  ⊆ var"
    "set vs1 ∩ Fvars φ1 = {}"
    "set vs1 ∩ ⋃ (FvarsT ` (fst ` (set txs))) = {}"
    "set vs1 ∩ snd ` (set txs) = {}"
    "length vs1 = length txs"
    "distinct vs1"
    using assms unfolding vs1
    using getFrN_Fvars[of "map snd txs" "map fst txs" "[φ1]" _ "length txs"]
      getFrN_FvarsT[of "map snd txs" "map fst txs" "[φ1]" _ "length txs"]
      getFrN_var[of "map snd txs" "map fst txs" "[φ1]" _ "length txs"]
      getFrN_length[of "map snd txs" "map fst txs" "[φ1]" "length txs"]
    apply -
    subgoal by auto
    subgoal by auto
    subgoal by fastforce
    subgoal by force
    by auto

  define vs2 where vs2: "vs2 = getFrN (map snd txs) (map fst txs) [φ2] (length txs)"
  have vs2_facts: "set vs2  ⊆ var"
    "set vs2 ∩ Fvars φ2 = {}"
    "set vs2 ∩ ⋃ (FvarsT ` (fst ` (set txs))) = {}"
    "set vs2 ∩ snd ` (set txs) = {}"
    "length vs2 = length txs"
    "distinct vs2"
    using assms unfolding vs2
    using getFrN_Fvars[of "map snd txs" "map fst txs" "[φ2]" _ "length txs"]
      getFrN_FvarsT[of "map snd txs" "map fst txs" "[φ2]" _ "length txs"]
      getFrN_var[of "map snd txs" "map fst txs" "[φ2]" _ "length txs"]
      getFrN_length[of "map snd txs" "map fst txs" "[φ2]" "length txs"]
    apply -
    subgoal by auto
    subgoal by auto
    subgoal by fastforce
    subgoal by force
    by auto

  let ?tus = "zip (map fst txs) us"
  let ?uxs = "zip (map Var us) (map snd txs)"
  let ?tvs1 = "zip (map fst txs) vs1"
  let ?vxs1 = "zip (map Var vs1) (map snd txs)"
  let ?tvs2 = "zip (map fst txs) vs2"
  let ?vxs2 = "zip (map Var vs2) (map snd txs)"

  let ?c = "rawpsubst (eqv φ1 φ2) ?uxs"
  have c: "?c = eqv (rawpsubst φ1 ?uxs) (rawpsubst φ2 ?uxs)"
    using assms us_facts
    by (intro rawpsubst_eqv) (auto intro!: rawpsubstT dest!: set_zip_D)
  have 0: "rawpsubst ?c ?tus =
    eqv (rawpsubst (rawpsubst φ1 ?uxs) ?tus) (rawpsubst (rawpsubst φ2 ?uxs) ?tus)"
    unfolding c using assms us_facts
    by (intro rawpsubst_eqv) (auto intro!: rawpsubst dest!: set_zip_D)
  have 1: "rawpsubst (rawpsubst φ1 ?uxs) ?tus = rawpsubst (rawpsubst φ1 ?vxs1) ?tvs1"
    using assms vs1_facts us_facts
    by (intro rawpsubst_compose_freshVar2) (auto intro!: rawpsubst)
  have 2: "rawpsubst (rawpsubst φ2 ?uxs) ?tus = rawpsubst (rawpsubst φ2 ?vxs2) ?tvs2"
    using assms vs2_facts us_facts
    by (intro rawpsubst_compose_freshVar2) (auto intro!: rawpsubst)
  show ?thesis unfolding psubst_def by (simp add: Let_def us[symmetric] vs1[symmetric] vs2[symmetric] 0 1 2)
qed

lemma rawpsubst_all:
  assumes "φ ∈ fmla" "y ∈ var"
    and "snd ` (set txs) ⊆ var" "fst ` (set txs) ⊆ trm"
    and "y ∉ snd ` (set txs)" "y ∉ ⋃ (FvarsT ` fst ` (set txs))"
  shows "rawpsubst (all y φ) txs = all y (rawpsubst φ txs)"
  using assms apply (induct txs arbitrary: φ)
  subgoal by auto
  subgoal for tx txs φ by (cases tx) auto .

lemma psubst_all[simp]:
  assumes "φ ∈ fmla" "y ∈ var"
    and "snd ` (set txs) ⊆ var" "fst ` (set txs) ⊆ trm"
    and "y ∉ snd ` (set txs)" "y ∉ ⋃ (FvarsT ` fst ` (set txs))"
    and "distinct (map snd txs)"
  shows "psubst (all y φ) txs = all y (psubst φ txs)"
proof-
  define us where us: "us = getFrN (map snd txs) (map fst txs) [all y φ] (length txs)"
  have us_facts: "set us ⊆ var"
    "set us ∩ (Fvars φ - {y}) = {}"
    "set us ∩ ⋃ (FvarsT ` (fst ` (set txs))) = {}"
    "set us ∩ snd ` (set txs) = {}"
    "length us = length txs"
    "distinct us"
    using assms unfolding us
    using getFrN_Fvars[of "map snd txs" "map fst txs" "[all y φ]" _ "length txs"]
      getFrN_FvarsT[of "map snd txs" "map fst txs" "[all y φ]" _ "length txs"]
      getFrN_var[of "map snd txs" "map fst txs" "[all y φ]" _ "length txs"]
      getFrN_length[of "map snd txs" "map fst txs" "[all y φ]" "length txs"]
    apply -
    subgoal by auto
    subgoal by fastforce
    subgoal by fastforce
    subgoal by (fastforce simp: image_iff)
    by auto

  define vs where vs: "vs = getFrN (map snd txs) (map fst txs) [φ] (length txs)"
  have vs_facts: "set vs  ⊆ var"
    "set vs ∩ Fvars φ = {}"
    "set vs ∩ ⋃ (FvarsT ` (fst ` (set txs))) = {}"
    "set vs ∩ snd ` (set txs) = {}"
    "length vs = length txs"
    "distinct vs"
    using assms unfolding vs
    using getFrN_Fvars[of "map snd txs" "map fst txs" "[φ]" _ "length txs"]
      getFrN_FvarsT[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"]
    apply -
    subgoal by auto
    subgoal by fastforce
    subgoal by fastforce
    subgoal by (fastforce simp: image_iff)
    by auto

  define ws where ws: "ws = getFrN (y # map snd txs) (map fst txs) [φ] (length txs)"
  have ws_facts: "set ws  ⊆ var"
    "set ws ∩ Fvars φ = {}"  "y ∉ set ws"
    "set ws ∩ ⋃ (FvarsT ` (fst ` (set txs))) = {}"
    "set ws ∩ snd ` (set txs) = {}"
    "length ws = length txs"
    "distinct ws"
    using assms unfolding ws
    using getFrN_Fvars[of "y # map snd txs" "map fst txs" "[φ]" _ "length txs"]
      getFrN_FvarsT[of "y # map snd txs" "map fst txs" "[φ]" _ "length txs"]
      getFrN_var[of "y # map snd txs" "map fst txs" "[φ]" _ "length txs"]
      getFrN_length[of "y # map snd txs" "map fst txs" "[φ]" "length txs"]
    apply -
    subgoal by auto
    subgoal by fastforce
    subgoal by fastforce
    subgoal by (fastforce simp: image_iff)
    subgoal by (fastforce simp: image_iff)
    by auto

  have 0: "rawpsubst (all y φ) (zip (map Var ws) (map snd txs)) =
           all y (rawpsubst φ (zip (map Var ws) (map snd txs)))"
    using assms ws_facts  apply(intro rawpsubst_all)
    subgoal by auto
    subgoal by auto
    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) .

  have 1: "rawpsubst ((rawpsubst φ (zip (map Var ws) (map snd txs)))) (zip (map fst txs) ws) =
           rawpsubst ((rawpsubst φ (zip (map Var vs) (map snd txs)))) (zip (map fst txs) vs)"
    apply(rule rawpsubst_compose_freshVar2)
    using assms ws_facts vs_facts by (auto intro!: rawpsubst)
  have "rawpsubst (rawpsubst (all y φ) (zip (map Var us) (map snd txs))) (zip (map fst txs) us) =
        rawpsubst (rawpsubst (all y φ) (zip (map Var ws) (map snd txs))) (zip (map fst txs) ws)"
    using assms ws_facts us_facts
    by (intro rawpsubst_compose_freshVar2) (auto intro!: rawpsubst)
  also have
    "… = all y (rawpsubst ((rawpsubst φ (zip (map Var ws) (map snd txs)))) (zip (map fst txs) ws))"
    unfolding 0 using assms ws_facts
    by (intro rawpsubst_all) (auto dest!: set_zip_D intro!: rawpsubst)
  also have
    "… = all y (rawpsubst (rawpsubst φ (zip (map Var vs) (map snd txs))) (zip (map fst txs) vs))"
    unfolding 1 ..
  finally show ?thesis unfolding psubst_def by (simp add: Let_def us[symmetric] vs[symmetric])
qed

lemma rawpsubst_exi:
  assumes "φ ∈ fmla" "y ∈ var"
    and "snd ` (set txs) ⊆ var" "fst ` (set txs) ⊆ trm"
    and "y ∉ snd ` (set txs)" "y ∉ ⋃ (FvarsT ` fst ` (set txs))"
  shows "rawpsubst (exi y φ) txs = exi y (rawpsubst φ txs)"
  using assms apply (induct txs arbitrary: φ)
  subgoal by auto
  subgoal for tx txs φ by (cases tx) auto .

lemma psubst_exi[simp]:
  assumes "φ ∈ fmla" "y ∈ var"
    and "snd ` (set txs) ⊆ var" "fst ` (set txs) ⊆ trm"
    and "y ∉ snd ` (set txs)" "y ∉ ⋃ (FvarsT ` fst ` (set txs))"
    and "distinct (map snd txs)"
  shows "psubst (exi y φ) txs = exi y (psubst φ txs)"
proof-
  define us where us: "us = getFrN (map snd txs) (map fst txs) [exi y φ] (length txs)"
  have us_facts: "set us ⊆ var"
    "set us ∩ (Fvars φ - {y}) = {}"
    "set us ∩ ⋃ (FvarsT ` (fst ` (set txs))) = {}"
    "set us ∩ snd ` (set txs) = {}"
    "length us = length txs"
    "distinct us"
    using assms unfolding us
    using getFrN_Fvars[of "map snd txs" "map fst txs" "[exi y φ]" _ "length txs"]
      getFrN_FvarsT[of "map snd txs" "map fst txs" "[exi y φ]" _ "length txs"]
      getFrN_var[of "map snd txs" "map fst txs" "[exi y φ]" _ "length txs"]
      getFrN_length[of "map snd txs" "map fst txs" "[exi y φ]" "length txs"]
    apply -
    subgoal by auto
    subgoal by fastforce
    subgoal by fastforce
    subgoal by (fastforce simp: image_iff)
    subgoal by (fastforce simp: image_iff)
    by auto

  define vs where vs: "vs = getFrN (map snd txs) (map fst txs) [φ] (length txs)"
  have vs_facts: "set vs  ⊆ var"
    "set vs ∩ Fvars φ = {}"
    "set vs ∩ ⋃ (FvarsT ` (fst ` (set txs))) = {}"
    "set vs ∩ snd ` (set txs) = {}"
    "length vs = length txs"
    "distinct vs"
    using assms unfolding vs
    using getFrN_Fvars[of "map snd txs" "map fst txs" "[φ]" _ "length txs"]
      getFrN_FvarsT[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"]
    apply -
    subgoal by auto
    subgoal by fastforce
    subgoal by fastforce
    subgoal by (fastforce simp: image_iff)
    subgoal by (fastforce simp: image_iff)
    by auto

  define ws where ws: "ws = getFrN (y # map snd txs) (map fst txs) [φ] (length txs)"
  have ws_facts: "set ws  ⊆ var"
    "set ws ∩ Fvars φ = {}"  "y ∉ set ws"
    "set ws ∩ ⋃ (FvarsT ` (fst ` (set txs))) = {}"
    "set ws ∩ snd ` (set txs) = {}"
    "length ws = length txs"
    "distinct ws"
    using assms unfolding ws
    using getFrN_Fvars[of "y # map snd txs" "map fst txs" "[φ]" _ "length txs"]
      getFrN_FvarsT[of "y # map snd txs" "map fst txs" "[φ]" _ "length txs"]
      getFrN_var[of "y # map snd txs" "map fst txs" "[φ]" _ "length txs"]
      getFrN_length[of "y # map snd txs" "map fst txs" "[φ]" "length txs"]
    apply -
    subgoal by auto
    subgoal by fastforce
    subgoal by fastforce
    subgoal by (fastforce simp: image_iff)
    subgoal by (fastforce simp: image_iff)
    by auto

  have 0: "rawpsubst (exi y φ) (zip (map Var ws) (map snd txs)) =
           exi y (rawpsubst φ (zip (map Var ws) (map snd txs)))"
    using assms ws_facts apply(intro rawpsubst_exi)
    subgoal by auto
    subgoal by auto
    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) .

  have 1: "rawpsubst ((rawpsubst φ (zip (map Var ws) (map snd txs)))) (zip (map fst txs) ws) =
           rawpsubst ((rawpsubst φ (zip (map Var vs) (map snd txs)))) (zip (map fst txs) vs)"
    using assms ws_facts vs_facts
    by (intro rawpsubst_compose_freshVar2) (auto intro!: rawpsubst)
  have "rawpsubst (rawpsubst (exi y φ) (zip (map Var us) (map snd txs))) (zip (map fst txs) us) =
        rawpsubst (rawpsubst (exi y φ) (zip (map Var ws) (map snd txs))) (zip (map fst txs) ws)"
    using assms ws_facts us_facts
    by (intro rawpsubst_compose_freshVar2) (auto intro!: rawpsubst)
  also have
    "… = exi y (rawpsubst ((rawpsubst φ (zip (map Var ws) (map snd txs)))) (zip (map fst txs) ws))"
    using assms ws_facts unfolding 0
    by (intro rawpsubst_exi) (auto dest!: set_zip_D intro!: rawpsubst)
  also have
    "… = exi y (rawpsubst (rawpsubst φ (zip (map Var vs) (map snd txs))) (zip (map fst txs) vs))"
    unfolding 1 ..
  finally show ?thesis unfolding psubst_def by (simp add: Let_def us[symmetric] vs[symmetric])
qed

end ― ‹context @{locale Syntax_with_Connectives}›


locale Syntax_with_Numerals_and_Connectives =
  Syntax_with_Numerals
  var trm fmla Var FvarsT substT Fvars subst
  num
  +
  Syntax_with_Connectives
  var trm fmla Var FvarsT substT Fvars subst
  eql cnj imp all exi
  for
    var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
    and Var FvarsT substT Fvars subst
    and num
    and eql cnj imp all exi
begin

lemma subst_all_num[simp]:
  assumes "φ ∈ fmla" "x ∈ var" "y ∈ var" "n ∈ num"
  shows "x ≠ y ⟹ subst (all x φ) n y = all x (subst φ n y)"
  using assms by simp

lemma subst_exi_num[simp]:
  assumes "φ ∈ fmla" "x ∈ var" "y ∈ var" "n ∈ num"
  shows "x ≠ y ⟹ subst (exi x φ) n y = exi x (subst φ n y)"
  using assms by simp


text ‹The "soft substitution" function:›
definition softSubst :: "'fmla ⇒ 'trm ⇒ 'var ⇒ 'fmla" where
  "softSubst φ t x = exi x (cnj (eql (Var x) t) φ)"

lemma softSubst[simp,intro]: "φ ∈ fmla ⟹ t ∈ trm ⟹ x ∈ var ⟹ softSubst φ t x ∈ fmla"
  unfolding softSubst_def by auto

lemma Fvars_softSubst[simp]:
  "φ ∈ fmla ⟹ t ∈ trm ⟹ x ∈ var ⟹
 Fvars (softSubst φ t x) = (Fvars φ ∪ FvarsT t - {x})"
  unfolding softSubst_def by auto

lemma Fvars_softSubst_subst_in:
  "φ ∈ fmla ⟹ t ∈ trm ⟹ x ∈ var ⟹ x ∉ FvarsT t ⟹ x ∈ Fvars φ ⟹
 Fvars (softSubst φ t x) = Fvars (subst φ t x)"
  by auto

lemma Fvars_softSubst_subst_notIn:
  "φ ∈ fmla ⟹ t ∈ trm ⟹ x ∈ var ⟹ x ∉ FvarsT t ⟹ x ∉ Fvars φ ⟹
 Fvars (softSubst φ t x) = Fvars (subst φ t x) ∪ FvarsT t"
  by auto

end ― ‹context @{locale Syntax_with_Connectives}›

text ‹The addition of False among logical connectives›

locale Syntax_with_Connectives_False =
  Syntax_with_Connectives
  var trm fmla Var FvarsT substT Fvars subst
  eql cnj imp all exi
  for
    var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
    and Var FvarsT substT Fvars subst
    and eql cnj imp all exi
    +
  fixes fls::'fmla
  assumes
    fls[simp,intro!]: "fls ∈ fmla"
    and
    Fvars_fls[simp,intro!]: "Fvars fls = {}"
    and
    subst_fls[simp]:
    "⋀t x. t ∈ trm ⟹ x ∈ var ⟹ subst fls t x = fls"
begin

text ‹Negation as a derrived connective:›
definition neg :: "'fmla ⇒ 'fmla" where
  "neg φ = imp φ fls"

lemma
  neg[simp]: "⋀φ. φ ∈ fmla ⟹ neg φ ∈ fmla"
  and
  Fvars_neg[simp]: "⋀φ. φ ∈ fmla ⟹ Fvars (neg φ) = Fvars φ"
  and
  subst_neg[simp]:
  "⋀φ t x. φ ∈ fmla ⟹ t ∈ trm ⟹ x ∈ var ⟹
  subst (neg φ) t x = neg (subst φ t x)"
  unfolding neg_def by auto

text ‹True as a derived connective:›
definition tru where "tru = neg fls"

lemma
  tru[simp,intro!]: "tru ∈ fmla"
  and
  Fvars_tru[simp]: "Fvars tru = {}"
  and
  subst_tru[simp]: "⋀ t x. t ∈ trm ⟹ x ∈ var ⟹ subst tru t x = tru"
  unfolding tru_def by auto


subsection ‹Iterated conjunction›

text ‹First we define list-based conjunction:›
fun lcnj :: "'fmla list ⇒ 'fmla" where
  "lcnj [] = tru"
| "lcnj (φ # φs) = cnj φ (lcnj φs)"

lemma lcnj[simp,intro!]: "set φs ⊆ fmla ⟹ lcnj φs ∈ fmla"
  by (induct φs) auto

lemma Fvars_lcnj[simp]:
  "set φs ⊆ fmla ⟹ finite F ⟹ Fvars (lcnj φs) = ⋃ (set (map Fvars φs))"
  by(induct φs) auto

lemma subst_lcnj[simp]:
  "set φs ⊆ fmla ⟹ t ∈ trm ⟹ x ∈ var ⟹
 subst (lcnj φs) t x = lcnj (map (λφ. subst φ t x) φs)"
  by(induct φs) auto

text ‹Then we define (finite-)set-based conjunction:›
definition scnj :: "'fmla set ⇒ 'fmla" where
  "scnj F = lcnj (asList F)"

lemma scnj[simp,intro!]: "F ⊆ fmla ⟹ finite F ⟹ scnj F ∈ fmla"
  unfolding scnj_def by auto

lemma Fvars_scnj[simp]:
  "F ⊆ fmla ⟹ finite F ⟹Fvars (scnj F) = ⋃ (Fvars ` F)"
  unfolding scnj_def by auto

subsection ‹Parallel substitution versus the new connectives›

lemma rawpsubst_fls:
  "snd ` (set txs) ⊆ var ⟹ fst ` (set txs) ⊆ trm ⟹ rawpsubst fls txs = fls"
  by (induct txs) auto

lemma psubst_fls[simp]:
  assumes "snd ` (set txs) ⊆ var" and "fst ` (set txs) ⊆ trm"
  shows "psubst fls txs = fls"
proof-
  define us where us: "us = getFrN (map snd txs) (map fst txs) [fls] (length txs)"
  have us_facts: "set us ⊆ var"
    "set us ∩ ⋃ (FvarsT ` (fst ` (set txs))) = {}"
    "set us ∩ snd ` (set txs) = {}"
    "length us = length txs"
    "distinct us"
    using assms unfolding us
    using getFrN_Fvars[of "map snd txs" "map fst txs" "[fls]" _ "length txs"]
      getFrN_FvarsT[of "map snd txs" "map fst txs" "[fls]" _ "length txs"]
      getFrN_var[of "map snd txs" "map fst txs" "[fls]" _ "length txs"]
      getFrN_length[of "map snd txs" "map fst txs" "[fls]" "length txs"]
    apply -
    subgoal by auto
    subgoal by fastforce
    subgoal by (fastforce simp: image_iff)
    subgoal by (fastforce simp: image_iff)
    by auto
  have [simp]: "rawpsubst fls (zip (map Var us) (map snd txs)) = fls"
    using us_facts assms by (intro rawpsubst_fls) (auto dest!: set_zip_D)
  show ?thesis using assms us_facts
    unfolding psubst_def by (auto simp add: Let_def us[symmetric] intro!: rawpsubst_fls dest!: set_zip_D)
qed

lemma psubst_neg[simp]:
  assumes "φ ∈ fmla"
    and "snd ` (set txs) ⊆ var" "fst ` (set txs) ⊆ trm"
    and "distinct (map snd txs)"
  shows "psubst (neg φ) txs = neg (psubst φ txs)"
  unfolding neg_def using assms psubst_imp psubst_fls by auto

lemma psubst_tru[simp]:
  assumes "snd ` (set txs) ⊆ var" and "fst ` (set txs) ⊆ trm"
    and "distinct (map snd txs)"
  shows "psubst tru txs = tru"
  unfolding tru_def using assms psubst_neg[of fls txs] psubst_fls by auto

lemma psubst_lcnj[simp]:
  "set φs ⊆ fmla ⟹ snd ` (set txs) ⊆ var ⟹ fst ` (set txs) ⊆ trm ⟹
 distinct (map snd txs) ⟹
 psubst (lcnj φs) txs = lcnj (map (λφ. psubst φ txs) φs)"
  by (induct  φs) auto

end ― ‹context @{locale Syntax_with_Connectives_False}›


section ‹Adding Disjunction›

text ‹NB: In intuitionistic logic, disjunction is not definable from the other connectives.›

locale Syntax_with_Connectives_False_Disj =
  Syntax_with_Connectives_False
  var trm fmla Var FvarsT substT Fvars subst
  eql cnj imp all exi
  fls
  for
    var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
    and Var FvarsT substT Fvars subst
    and eql cnj imp all exi
    and fls
    +
  fixes dsj :: "'fmla ⇒ 'fmla ⇒ 'fmla"
  assumes
    dsj[simp]: "⋀φ χ. φ ∈ fmla ⟹ χ ∈ fmla ⟹ dsj φ χ ∈ fmla"
    and
    Fvars_dsj[simp]: "⋀φ χ. φ ∈ fmla ⟹ χ ∈ fmla ⟹
  Fvars (dsj φ χ) = Fvars φ ∪ Fvars χ"
    and
    subst_dsj[simp]:
    "⋀ x φ χ t. φ ∈ fmla ⟹ χ ∈ fmla ⟹ t ∈ trm ⟹ x ∈ var ⟹
   subst (dsj φ χ) t x = dsj (subst φ t x) (subst χ t x)"
begin

subsection ‹Iterated disjunction›

text ‹First we define list-based disjunction:›
fun ldsj :: "'fmla list ⇒ 'fmla" where
  "ldsj [] = fls"
| "ldsj (φ # φs) = dsj φ (ldsj φs)"

lemma ldsj[simp,intro!]: "set φs ⊆ fmla ⟹ ldsj φs ∈ fmla"
  by (induct φs) auto

lemma Fvars_ldsj[simp]:
  "set φs ⊆ fmla ⟹ Fvars (ldsj φs) = ⋃ (set (map Fvars φs))"
  by(induct φs) auto

lemma subst_ldsj[simp]:
  "set φs ⊆ fmla ⟹ t ∈ trm ⟹ x ∈ var ⟹
 subst (ldsj φs) t x = ldsj (map (λφ. subst φ t x) φs)"
  by(induct φs) auto

text ‹Then we define (finite-)set-based disjunction:›
definition sdsj :: "'fmla set ⇒ 'fmla" where
  "sdsj F = ldsj (asList F)"

lemma sdsj[simp,intro!]: "F ⊆ fmla ⟹ finite F ⟹ sdsj F ∈ fmla"
  unfolding sdsj_def by auto

lemma Fvars_sdsj[simp]:
  "F ⊆ fmla ⟹ finite F ⟹ Fvars (sdsj F) = ⋃ (Fvars ` F)"
  unfolding sdsj_def by auto


subsection ‹Parallel substitution versus the new connectives›

lemma rawpsubst_dsj:
  assumes "φ1 ∈ fmla" "φ2 ∈ fmla"
    and "snd ` (set txs) ⊆ var" "fst ` (set txs) ⊆ trm"
  shows "rawpsubst (dsj φ1 φ2) txs = dsj (rawpsubst φ1 txs) (rawpsubst φ2 txs)"
  using assms apply (induct txs arbitrary: φ1 φ2)
  subgoal by auto
  subgoal for tx txs φ1 φ2 apply (cases tx) by auto .

lemma psubst_dsj[simp]:
  assumes "φ1 ∈ fmla" "φ2 ∈ fmla"
    and "snd ` (set txs) ⊆ var" "fst ` (set txs) ⊆ trm"
    and "distinct (map snd txs)"
  shows "psubst (dsj φ1 φ2) txs = dsj (psubst φ1 txs) (psubst φ2 txs)"
proof-
  define us where us: "us = getFrN (map snd txs) (map fst txs) [dsj φ1 φ2] (length txs)"
  have us_facts: "set us ⊆ var"
    "set us ∩ Fvars φ1 = {}"
    "set us ∩ Fvars φ2 = {}"
    "set us ∩ ⋃ (FvarsT ` (fst ` (set txs))) = {}"
    "set us ∩ snd ` (set txs) = {}"
    "length us = length txs"
    "distinct us"
    using assms unfolding us
    using getFrN_Fvars[of "map snd txs" "map fst txs" "[dsj φ1 φ2]" _ "length txs"]
      getFrN_FvarsT[of "map snd txs" "map fst txs" "[dsj φ1 φ2]" _ "length txs"]
      getFrN_var[of "map snd txs" "map fst txs" "[dsj φ1 φ2]" _ "length txs"]
      getFrN_length[of "map snd txs" "map fst txs" "[dsj φ1 φ2]" "length txs"]
    apply -
    subgoal by auto
    subgoal by fastforce
    subgoal by (fastforce simp: image_iff)
    subgoal by (fastforce simp: image_iff)
    subgoal by (fastforce simp: image_iff)
    by auto

  define vs1 where vs1: "vs1 = getFrN (map snd txs) (map fst txs) [φ1] (length txs)"
  have vs1_facts: "set vs1  ⊆ var"
    "set vs1 ∩ Fvars φ1 = {}"
    "set vs1 ∩ ⋃ (FvarsT ` (fst ` (set txs))) = {}"
    "set vs1 ∩ snd ` (set txs) = {}"
    "length vs1 = length txs"
    "distinct vs1"
    using assms unfolding vs1
    using getFrN_Fvars[of "map snd txs" "map fst txs" "[φ1]" _ "length txs"]
      getFrN_FvarsT[of "map snd txs" "map fst txs" "[φ1]" _ "length txs"]
      getFrN_var[of "map snd txs" "map fst txs" "[φ1]" _ "length txs"]
      getFrN_length[of "map snd txs" "map fst txs" "[φ1]" "length txs"]
    apply -
    subgoal by auto
    subgoal by fastforce
    subgoal by fastforce
    subgoal by (fastforce simp: image_iff)
    by auto

  define vs2 where vs2: "vs2 = getFrN (map snd txs) (map fst txs) [φ2] (length txs)"
  have vs2_facts: "set vs2  ⊆ var"
    "set vs2 ∩ Fvars φ2 = {}"
    "set vs2 ∩ ⋃ (FvarsT ` (fst ` (set txs))) = {}"
    "set vs2 ∩ snd ` (set txs) = {}"
    "length vs2 = length txs"
    "distinct vs2"
    using assms unfolding vs2
    using getFrN_Fvars[of "map snd txs" "map fst txs" "[φ2]" _ "length txs"]
      getFrN_FvarsT[of "map snd txs" "map fst txs" "[φ2]" _ "length txs"]
      getFrN_var[of "map snd txs" "map fst txs" "[φ2]" _ "length txs"]
      getFrN_length[of "map snd txs" "map fst txs" "[φ2]" "length txs"]
    apply -
    apply -
    subgoal by auto
    subgoal by fastforce
    subgoal by fastforce
    subgoal by (fastforce simp: image_iff)
    by auto

  let ?tus = "zip (map fst txs) us"
  let ?uxs = "zip (map Var us) (map snd txs)"
  let ?tvs1 = "zip (map fst txs) vs1"
  let ?vxs1 = "zip (map Var vs1) (map snd txs)"
  let ?tvs2 = "zip (map fst txs) vs2"
  let ?vxs2 = "zip (map Var vs2) (map snd txs)"

  let ?c = "rawpsubst (dsj φ1 φ2) ?uxs"
  have c: "?c = dsj (rawpsubst φ1 ?uxs) (rawpsubst φ2 ?uxs)"
    apply(rule rawpsubst_dsj) using assms us_facts apply (auto intro!: rawpsubstT)
    apply(drule set_zip_rightD) apply simp apply blast
    apply(drule set_zip_leftD) apply simp apply blast .
  have 0: "rawpsubst ?c ?tus =
    dsj (rawpsubst (rawpsubst φ1 ?uxs) ?tus) (rawpsubst (rawpsubst φ2 ?uxs) ?tus)"
    unfolding c using assms us_facts
    by (intro rawpsubst_dsj) (auto intro!: rawpsubst dest!: set_zip_D)
  have 1: "rawpsubst (rawpsubst φ1 ?uxs) ?tus = rawpsubst (rawpsubst φ1 ?vxs1) ?tvs1"
    using assms vs1_facts us_facts
    by (intro rawpsubst_compose_freshVar2) (auto intro!: rawpsubst)
  have 2: "rawpsubst (rawpsubst φ2 ?uxs) ?tus = rawpsubst (rawpsubst φ2 ?vxs2) ?tvs2"
    using assms vs2_facts us_facts
    by (intro rawpsubst_compose_freshVar2) (auto intro!: rawpsubst)
  show ?thesis unfolding psubst_def by (simp add: Let_def us[symmetric] vs1[symmetric] vs2[symmetric] 0 1 2)
qed

lemma psubst_ldsj[simp]:
  "set φs ⊆ fmla ⟹ snd ` (set txs) ⊆ var ⟹ fst ` (set txs) ⊆ trm ⟹
 distinct (map snd txs) ⟹
 psubst (ldsj φs) txs = ldsj (map (λφ. psubst φ txs) φs)"
  by (induct  φs) auto

end ― ‹context @{locale Syntax_with_Connectives_False_Disj}›


section ‹Adding an Ordering-Like Formula›

locale Syntax_with_Numerals_and_Connectives_False_Disj =
  Syntax_with_Connectives_False_Disj
  var trm fmla Var FvarsT substT Fvars subst
  eql cnj imp all exi
  fls
  dsj
  +
  Syntax_with_Numerals_and_Connectives
  var trm fmla Var FvarsT substT Fvars subst
  num
  eql cnj imp all exi
  for
    var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
    and Var FvarsT substT Fvars subst
    and eql cnj imp all exi
    and fls
    and dsj
    and num

text ‹... and in addition a formula expressing order (think: less than or equal to)›
locale Syntax_PseudoOrder =
  Syntax_with_Numerals_and_Connectives_False_Disj
  var trm fmla Var FvarsT substT Fvars subst
  eql cnj imp all exi
  fls
  dsj
  num
  for
    var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
    and Var FvarsT substT Fvars subst
    and eql cnj imp all exi
    and fls
    and dsj
    and num
    +
  fixes
    ― ‹Lq is a formula with free variables xx yy:›
    Lq :: 'fmla
  assumes
    Lq[simp,intro!]: "Lq ∈ fmla"
    and
    Fvars_Lq[simp]: "Fvars Lq = {zz,yy}"
begin

definition LLq where "LLq t1 t2 = psubst Lq [(t1,zz), (t2,yy)]"

lemma LLq_def2: "t1 ∈ trm ⟹ t2 ∈ trm ⟹ yy ∉ FvarsT t1 ⟹
 LLq t1 t2 = subst (subst Lq t1 zz) t2 yy"
  unfolding LLq_def by (rule psubst_eq_rawpsubst2[simplified]) auto

lemma LLq[simp,intro]:
  assumes "t1 ∈ trm" "t2 ∈ trm"
  shows "LLq t1 t2 ∈ fmla"
  using assms unfolding LLq_def by auto

lemma LLq2[simp,intro!]:
  "n ∈ num ⟹ LLq n (Var yy') ∈ fmla"
  by auto

lemma Fvars_LLq[simp]: "t1 ∈ trm ⟹ t2 ∈ trm ⟹ yy ∉ FvarsT t1 ⟹
Fvars (LLq t1 t2) = FvarsT t1 ∪ FvarsT t2"
  by (auto simp add: LLq_def2 subst2_fresh_switch)

lemma LLq_simps[simp]:
  "m ∈ num ⟹ n ∈ num ⟹ subst (LLq m (Var yy)) n yy = LLq m n"
  "m ∈ num ⟹ n ∈ num ⟹ subst (LLq m (Var yy')) n yy = LLq m (Var yy')"
  "m ∈ num ⟹ subst (LLq m (Var yy')) (Var yy) yy' = LLq m (Var yy)"
  "n ∈ num ⟹ subst (LLq (Var xx) (Var yy)) n xx = LLq n (Var yy)"
  "n ∈ num ⟹ subst (LLq (Var zz) (Var yy)) n yy = LLq (Var zz) n"
  "m ∈ num ⟹ subst (LLq (Var zz) (Var yy)) m zz = LLq m (Var yy)"
  "m ∈ num ⟹ n ∈ num ⟹ subst (LLq (Var zz) n) m xx = LLq (Var zz) n"
  by (auto simp: LLq_def2 subst2_fresh_switch)

end ― ‹context @{locale Syntax_PseudoOrder}›


section ‹Allowing the Renaming of Quantified Variables›

text ‹So far, we did not need any renaming axiom for the quantifiers. However,
our axioms for substitution implicitly assume the irrelevance of the bound names;
in other words, their usual instances would have this property; and since this assumption
greatly simplifies the formal development, we make it at this point.›

locale Syntax_with_Connectives_Rename =
Syntax_with_Connectives
  var trm fmla Var FvarsT substT Fvars subst
  eql cnj imp all exi
for
var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
and Var FvarsT substT Fvars subst
and eql cnj imp all exi
+
assumes all_rename:
"⋀φ x y. φ ∈ fmla ⟹ x ∈ var ⟹ y ∈ var ⟹ y ∉ Fvars φ ⟹
  all x φ = all y (subst φ (Var y) x)"
and exi_rename:
"⋀φ x y. φ ∈ fmla ⟹ x ∈ var ⟹ y ∈ var ⟹ y ∉ Fvars φ ⟹
  exi x φ = exi y (subst φ (Var y) x)"
begin

lemma all_rename2:
"φ ∈ fmla ⟹ x ∈ var ⟹ y ∈ var ⟹ (y = x ∨ y ∉ Fvars φ) ⟹
  all x φ = all y (subst φ (Var y) x)"
using all_rename by (cases "y = x") (auto simp del: Fvars_subst)

lemma exi_rename2:
"φ ∈ fmla ⟹ x ∈ var ⟹ y ∈ var ⟹ (y = x ∨ y ∉ Fvars φ) ⟹
  exi x φ = exi y (subst φ (Var y) x)"
using exi_rename by (cases "y = x") (auto simp del: Fvars_subst)


section ‹The Exists-Unique Quantifier›

text ‹It is phrased in such a way as to avoid substitution:›

definition exu :: "'var ⇒ 'fmla ⇒ 'fmla" where
"exu x φ ≡ let y = getFr [x] [] [φ] in
 cnj (exi x φ) (exi y (all x (imp φ (eql (Var x) (Var y)))))"

lemma exu[simp,intro]:
"x ∈ var ⟹ φ ∈ fmla ⟹ exu x φ ∈ fmla"
unfolding exu_def by (simp add: Let_def)

lemma Fvars_exu[simp]:
"x ∈ var ⟹ φ ∈ fmla ⟹ Fvars (exu x φ) = Fvars φ - {x}"
unfolding exu_def by (auto simp: Let_def getFr_Fvars)

lemma exu_def_var:
assumes [simp]: "x ∈ var" "y ∈ var" "y ≠ x" "y ∉ Fvars φ" "φ ∈ fmla"
shows
"exu x φ = cnj (exi x φ) (exi y (all x (imp φ (eql (Var x) (Var y)))))"
proof-
  have [simp]: "x ≠ y" using assms by blast
  define z where z: "z ≡ getFr [x] [] [φ]"
  have z_facts[simp]:  "z ∈ var" "z ≠ x" "x ≠ z" "z ∉ Fvars φ"
  unfolding z using getFr_FvarsT_Fvars[of "[x]" "[]" "[φ]"] by auto
  define u where u: "u ≡ getFr [x,y,z] [] [φ]"
  have u_facts[simp]:  "u ∈ var" "u ≠ x" "u ≠ z" "y ≠ u" "u ≠ y" "x ≠ u" "z ≠ u" "u ∉ Fvars φ"
  unfolding u using getFr_FvarsT_Fvars[of "[x,y,z]" "[]" "[φ]"] by auto

  have "exu x φ =  cnj (exi x φ) (exi u (all x (imp φ (eql (Var x) (Var u)))))"
  by (auto simp: exu_def Let_def z[symmetric] exi_rename[of "all x (imp φ (eql (Var x) (Var z)))" z u])
  also have "… = cnj (exi x φ) (exi y (all x (imp φ (eql (Var x) (Var y)))))"
  by (auto simp: exi_rename[of "all x (imp φ (eql (Var x) (Var u)))" u y]
     split: if_splits)
  finally show ?thesis .
qed

lemma subst_exu[simp]:
assumes [simp]: "φ ∈ fmla" "t ∈ trm" "x ∈ var" "y ∈ var" "x ≠ y" "x ∉ FvarsT t"
shows "subst (exu x φ) t y = exu x (subst φ t y)"
proof-
  define u where u: "u ≡ getFr [x,y] [t] [φ]"
  have u_facts[simp]:  "u ∈ var" "u ≠ x" "u ≠ y" "y ≠ u" "x ≠ u"
    "u ∉ FvarsT t" "u ∉ Fvars φ"
  unfolding u using getFr_FvarsT_Fvars[of "[x,y]" "[t]" "[φ]"] by auto
  show ?thesis
  by (auto simp: Let_def exu_def_var[of _ u] subst_compose_diff)
qed

lemma subst_exu_idle[simp]:
assumes [simp]: "x ∈ var" "φ ∈ fmla" "t ∈ trm"
shows "subst (exu x φ) t x = exu x φ"
by (intro subst_notIn) auto

lemma exu_rename:
assumes [simp]: "φ ∈ fmla" "x ∈ var" "y ∈ var" "y ∉ Fvars φ"
shows "exu x φ = exu y (subst φ (Var y) x)"
proof(cases "y = x")
  case [simp]: False
  define z where z: "z = getFr [x] [] [φ]"
  have z_facts[simp]:  "z ∈ var" "z ≠ x" "x ≠ z" "z ∉ Fvars φ"
  unfolding z using getFr_FvarsT_Fvars[of "[x]" "[]" "[φ]"] by auto
  define u where u: "u ≡ getFr [x,y,z] [] [φ]"
  have u_facts[simp]: "u ∈ var" "u ≠ x" "x ≠ u" "u ≠ y" "y ≠ u" "u ≠ z" "z ≠ u"
     "u ∉ Fvars φ"
  unfolding u using getFr_FvarsT_Fvars[of "[x,y,z]" "[]" "[φ]"] by auto
  show ?thesis
  by (auto simp: exu_def_var[of _ u] exi_rename[of _ _ y] all_rename[of _ _ y])
qed auto

lemma exu_rename2:
"φ ∈ fmla ⟹ x ∈ var ⟹ y ∈ var ⟹ (y = x ∨ y ∉ Fvars φ) ⟹
  exu x φ = exu y (subst φ (Var y) x)"
using exu_rename by (cases "y = x") (auto simp del: Fvars_subst)

end ― ‹context @{locale Syntax_with_Connectives_Rename}›

(*<*)
end
(*>*)