Theory Syntax_Arith

```chapter ‹Arithmetic Constructs›

text ‹Less genereric syntax, more committed towards embedding arithmetics›

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

text ‹(An embedding of) the syntax of arithmetic, obtained by adding plus and times›

locale Syntax_Arith_aux =
Syntax_with_Connectives_Rename
var trm fmla Var FvarsT substT Fvars subst
eql cnj imp all exi
+
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
zer :: "'trm"
and
suc :: "'trm ⇒ 'trm"
and
pls :: "'trm ⇒ 'trm ⇒ 'trm"
and
tms :: "'trm ⇒ 'trm ⇒ 'trm"
assumes
Fvars_zero[simp,intro!]: "FvarsT zer = {}"
and
substT_zer[simp]: "⋀ t x. t ∈ trm ⟹ x ∈ var ⟹
substT zer t x = zer"
and
suc[simp]: "⋀t. t ∈ trm ⟹ suc t ∈ trm"
and
FvarsT_suc[simp]: "⋀ t. t ∈ trm ⟹
FvarsT (suc t) = FvarsT t"
and
substT_suc[simp]: "⋀ t1 t x. t1 ∈ trm ⟹ t ∈ trm ⟹ x ∈ var ⟹
substT (suc t1) t x = suc (substT t1 t x)"
and
pls[simp]: "⋀ t1 t2. t1 ∈ trm ⟹ t2 ∈ trm ⟹ pls t1 t2 ∈ trm"
and
Fvars_pls[simp]: "⋀ t1 t2. t1 ∈ trm ⟹ t2 ∈ trm ⟹
FvarsT (pls t1 t2) = FvarsT t1 ∪ FvarsT t2"
and
substT_pls[simp]: "⋀ t1 t2 t x. t1 ∈ trm ⟹ t2 ∈ trm ⟹ t ∈ trm ⟹ x ∈ var ⟹
substT (pls t1 t2) t x = pls (substT t1 t x) (substT t2 t x)"
and
tms[simp]: "⋀ t1 t2. t1 ∈ trm ⟹ t2 ∈ trm ⟹ tms t1 t2 ∈ trm"
and
Fvars_tms[simp]: "⋀ t1 t2. t1 ∈ trm ⟹ t2 ∈ trm ⟹
FvarsT (tms t1 t2) = FvarsT t1 ∪ FvarsT t2"
and
substT_tms[simp]: "⋀ t1 t2 t x. t1 ∈ trm ⟹ t2 ∈ trm ⟹ t ∈ trm ⟹ x ∈ var ⟹
substT (tms t1 t2) t x = tms (substT t1 t x) (substT t2 t x)"
begin

text ‹The embedding of numbers into our abstract notion of numerals
(not required to be surjective)›
fun Num :: "nat ⇒ 'trm" where
"Num 0 = zer"
|"Num (Suc n) = suc (Num n)"

end ― ‹context @{locale Syntax_Arith_aux}›

locale Syntax_Arith =
Syntax_Arith_aux
var trm fmla Var FvarsT substT Fvars subst
eql cnj imp all exi
fls
dsj
num
zer suc pls tms
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
zer suc pls tms
+
assumes
― ‹We assume that numbers are the only numerals:›
num_Num: "num = range Num"
begin

lemma Num[simp,intro!]: "Num n ∈ num"
using num_Num by auto

lemma FvarsT_Num[simp]: "FvarsT (Num n) = {}"
by auto

lemma substT_Num[simp]: "x ∈ var ⟹ t ∈ trm ⟹ substT (Num n) t x = Num n"
by auto

lemma zer[simp,intro!]: "zer ∈ num"
and suc_num[simp]: "⋀n. n ∈ num ⟹ suc n ∈ num"
by (metis Num Num.simps(1), metis Num Num.simps(2) imageE num_Num)

section ‹Arithmetic Terms›

text ‹Arithmetic terms are inductively defined to contain the numerals and the variables
and be closed under the arithmetic operators:›

inductive_set atrm :: "'trm set" where
atrm_num[simp]: "n ∈ num ⟹ n ∈ atrm"
|atrm_Var[simp,intro]: "x ∈ var ⟹ Var x ∈ atrm"
|atrm_suc[simp,intro]: "t ∈ atrm ⟹ suc t ∈ atrm"
|atrm_pls[simp,intro]: "t ∈ atrm ⟹ t' ∈ atrm ⟹ pls t t' ∈ atrm"
|atrm_tms[simp,intro]: "t ∈ atrm ⟹ t' ∈ atrm ⟹ tms t t' ∈ atrm"

lemma atrm_imp_trm[simp]: assumes "t ∈ atrm" shows "t ∈ trm"
using assms by induct auto

lemma atrm_trm: "atrm ⊆ trm"
using atrm_imp_trm by auto

lemma zer_atrm[simp]: "zer ∈ atrm" by auto

lemma Num_atrm[simp]: "Num n ∈ atrm"
by auto

lemma substT_atrm[simp]:
assumes "r ∈ atrm" and "x ∈ var" and "t ∈ atrm"
shows "substT r t x ∈ atrm"
using assms by (induct) auto

text ‹Whereas we did not assume the rich set of formula-substitution properties to hold
for all terms, we can prove that these properties hold for arithmetic terms.›

text ‹Properties for arithmetic terms corresponding to the axioms for formulas:›

lemma FvarsT_substT:
assumes "s ∈ atrm" "t ∈ trm" "x ∈ var"
shows "FvarsT (substT s t x) = (FvarsT s - {x}) ∪ (if x ∈ FvarsT s then FvarsT t else {})"
using assms by induct auto

lemma substT_compose_eq_or:
assumes "s ∈ atrm" "t1 ∈ trm" "t2 ∈ trm" "x1 ∈ var" "x2 ∈ var"
and "x1 = x2 ∨ x2 ∉ FvarsT s"
shows "substT (substT s t1 x1) t2 x2 = substT s (substT t1 t2 x2) x1"
using assms apply induct
subgoal by auto
subgoal by auto
subgoal by (metis FvarsT_suc atrm_imp_trm substT substT_suc)
subgoal by (metis Fvars_pls UnCI atrm_imp_trm substT substT_pls)
subgoal by (metis Fvars_tms UnCI atrm_imp_trm substT substT_tms) .

lemma substT_compose_diff:
assumes "s ∈ atrm" "t1 ∈ trm" "t2 ∈ trm" "x1 ∈ var" "x2 ∈ var"
and "x1 ≠ x2" "x1 ∉ FvarsT t2"
shows "substT (substT s t1 x1) t2 x2 = substT (substT s t2 x2) (substT t1 t2 x2) x1"
using assms apply induct
subgoal by auto
subgoal by auto
subgoal by (metis atrm_imp_trm substT substT_suc)
subgoal by (metis atrm_imp_trm substT substT_pls)
subgoal by (metis atrm_imp_trm substT substT_tms) .

lemma substT_same_Var[simp]:
assumes "s ∈ atrm" "x ∈ var"
shows "substT s (Var x) x = s"
using assms by induct auto

text ‹... and corresponding to some corollaries we proved for formulas
(with essentially the same proofs):›

lemma in_FvarsT_substTD:
"y ∈ FvarsT (substT r t x) ⟹ r ∈ atrm ⟹ t ∈ trm ⟹ x ∈ var
⟹ y ∈ (FvarsT r - {x}) ∪ (if x ∈ FvarsT r then FvarsT t else {})"
using FvarsT_substT by auto

lemma substT_compose_same:
"⋀ s t1 t2 x. s ∈ atrm ⟹ t1 ∈ trm ⟹ t2 ∈ trm ⟹ x ∈ var ⟹
substT (substT s t1 x) t2 x = substT s (substT t1 t2 x) x"
using substT_compose_eq_or by blast

lemma substT_substT[simp]:
assumes s[simp]: "s ∈ atrm" and t[simp]:"t ∈ trm" and x[simp]:"x ∈ var" and y[simp]:"y ∈ var"
assumes yy: "x ≠ y" "y ∉ FvarsT s"
shows "substT (substT s (Var y) x) t y = substT s t x"
using substT_compose_eq_or[OF s _ t x y, of "Var y"] using subst_notIn yy by simp

lemma substT_comp:
"⋀ x y s t. s ∈ atrm ⟹ t ∈ trm ⟹ x ∈ var ⟹ y ∈ var ⟹
x ≠ y ⟹ y ∉ FvarsT t ⟹
substT (substT s (Var x) y) t x = substT (substT s t x) t y"

text ‹Now the corresponding development of parallel substitution for arithmetic terms:›

lemma rawpsubstT_atrm[simp,intro]:
assumes "r ∈ atrm" and "snd ` (set txs) ⊆ var" and "fst ` (set txs) ⊆ atrm"
shows "rawpsubstT r txs ∈ atrm"
using assms by (induct txs arbitrary: r) auto

lemma psubstT_atrm[simp,intro]:
assumes "r ∈ atrm" and "snd ` (set txs) ⊆ var" and "fst ` (set txs) ⊆ atrm"
shows "psubstT r txs ∈ atrm"
proof-
have txs_trm: "fst ` (set txs) ⊆ trm" using assms atrm_trm by auto
define us where us: "us ≡ getFrN (map snd txs) (r # map fst txs) [] (length txs)"
have us_facts: "set us ⊆ var"
"set us ∩ FvarsT r = {}"
"set us ∩ ⋃ (FvarsT ` (fst ` (set txs))) = {}"
"set us ∩ snd ` (set txs) = {}"
"length us = length txs"
"distinct us"
using assms(1,2) txs_trm unfolding us
using getFrN_FvarsT[of "map snd txs" "r # map fst txs" "[]" _ "length txs"]
getFrN_Fvars[of "map snd txs" "r # map fst txs" "[]" _ "length txs"]
getFrN_var[of "map snd txs" "r # map fst txs" "[]" _ "length txs"]
getFrN_length[of "map snd txs" "r # map fst txs" "[]" "length txs"]
getFrN_distinct[of "map snd txs" "r # map fst txs" "[]" "length txs"]
apply -
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by force
by auto
(* *)
show ?thesis using assms us_facts unfolding psubstT_def
by (force simp: Let_def us[symmetric]
intro!: rawpsubstT_atrm[of _ "zip (map fst txs) us"] dest!: set_zip_D)
qed

lemma Fvars_rawpsubst_su:
assumes "r ∈ atrm" and "snd ` (set txs) ⊆ var" and "fst ` (set txs) ⊆ atrm"
shows "FvarsT (rawpsubstT r txs) ⊆
(FvarsT r - snd ` (set txs)) ∪ (⋃ {FvarsT t | t x . (t,x) ∈ set txs})"
using assms proof(induction txs arbitrary: r)
case (Cons tx txs r)
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 "χ ≡ substT r t x"
have 0: "FvarsT χ =  FvarsT r - {x} ∪ (if x ∈ FvarsT r then FvarsT t else {})"
using Cons.prems unfolding χ_def by (auto simp: tx t FvarsT_substT)
have χ: "χ ∈ trm" "χ ∈ atrm" unfolding χ_def using Cons.prems t x  by (auto simp add: tx)
have "FvarsT (rawpsubstT χ txs) ⊆
(FvarsT χ - snd ` (set txs)) ∪
(⋃ {FvarsT t | t x . (t,x) ∈ set txs})"
using Cons.prems χ by (intro Cons.IH) auto
also have "… ⊆ FvarsT r - 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: "FvarsT (rawpsubstT χ txs) ⊆ ?R" .
have 2: "FvarsT χ = FvarsT r - {x} ∪ (if x ∈ FvarsT r then FvarsT t else {})"
using Cons.prems t x unfolding χ_def using FvarsT_substT by auto
show ?case using 1 by (simp add: tx χ_def[symmetric] 2)
qed auto

lemma in_FvarsT_rawpsubstT_imp:
assumes "y ∈ FvarsT (rawpsubstT r txs)"
and "r ∈ atrm" and "snd ` (set txs) ⊆ var" and "fst ` (set txs) ⊆ atrm"
shows "(y ∈ FvarsT r - 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 FvarsT_rawpsubstT:
assumes "r ∈ atrm" and "snd ` (set txs) ⊆ var" and "fst ` (set txs) ⊆ atrm"
and "distinct (map snd txs)" and "∀ x ∈ snd ` (set txs). ∀ t ∈ fst ` (set txs). x ∉ FvarsT t"
shows "FvarsT (rawpsubstT r txs) =
(FvarsT r - snd ` (set txs)) ∪
(⋃ {if x ∈ FvarsT r then FvarsT t else {} | t x . (t,x) ∈ set txs})"
using assms proof(induction txs arbitrary: r)
case (Cons a txs r)
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 xt: "x ∉ FvarsT t ∧ snd ` set txs ∩ FvarsT t = {}" using Cons.prems unfolding a by auto
hence 0: "FvarsT r - {x} ∪ FvarsT t - snd ` set txs = FvarsT r - insert x (snd ` set txs) ∪ FvarsT t"
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)

define χ where χ_def: "χ ≡ substT r t x"
have χ: "χ ∈ trm" "χ ∈ atrm" unfolding χ_def using Cons.prems t x  by (auto simp: a)
have 1: "FvarsT (rawpsubstT χ txs) =
(FvarsT χ - snd ` (set txs)) ∪
(⋃ {if x ∈ FvarsT χ then FvarsT t else {} | t x . (t,x) ∈ set txs})"
using Cons.prems χ by (intro Cons.IH) auto
have 2: "FvarsT χ = FvarsT r - {x} ∪ (if x ∈ FvarsT r then FvarsT t else {})"
using Cons.prems t x unfolding χ_def using FvarsT_substT by auto

define f where "f ≡ λta xa. if xa ∈ FvarsT r 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 ∈ FvarsT r - {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 "FvarsT r - {x} ∪ f t x  - snd ` set txs ∪
⋃ {if xa ∈ FvarsT r - {x} ∪ f t x then FvarsT ta else {}
| ta xa. (ta, xa) ∈ set txs} =
FvarsT r - 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 rawpsubstT.simps 1 2 χ_def[symmetric] f_def by simp
qed auto

lemma in_FvarsT_rawpsubstTD:
assumes "y ∈ FvarsT (rawpsubstT r txs)"
and "r ∈ atrm" and "snd ` (set txs) ⊆ var" and "fst ` (set txs) ⊆ atrm"
and "distinct (map snd txs)" and "∀ x ∈ snd ` (set txs). ∀ t ∈ fst ` (set txs). x ∉ FvarsT t"
shows "(y ∈ FvarsT r - snd ` (set txs)) ∨
(y ∈ ⋃ {if x ∈ FvarsT r then FvarsT t else {} | t x . (t,x) ∈ set txs})"
using FvarsT_rawpsubstT assms by auto

lemma FvarsT_psubstT:
assumes "r ∈ atrm" and "snd ` (set txs) ⊆ var" and "fst ` (set txs) ⊆ atrm"
and "distinct (map snd txs)"
shows "FvarsT (psubstT r txs) =
(FvarsT r - snd ` (set txs)) ∪
(⋃ {if x ∈ FvarsT r then FvarsT t else {} | t x . (t,x) ∈ set txs})"
proof-
have txs_trm: "fst ` (set txs) ⊆ trm" using assms by auto
define us where us: "us ≡ getFrN (map snd txs) (r # map fst txs) [] (length txs)"
have us_facts: "set us ⊆ var"
"set us ∩ FvarsT r = {}"
"set us ∩ ⋃ (FvarsT ` (fst ` (set txs))) = {}"
"set us ∩ snd ` (set txs) = {}"
"length us = length txs"
"distinct us"
using assms(1,2) txs_trm unfolding us
using getFrN_FvarsT[of "map snd txs" "r # map fst txs" "[]" _ "length txs"]
getFrN_Fvars[of "map snd txs" "r # map fst txs" "[]" _ "length txs"]
getFrN_var[of "map snd txs" "r # map fst txs" "[]" _ "length txs"]
getFrN_length[of "map snd txs" "r # map fst txs" "[]" "length txs"]
getFrN_length[of "map snd txs" "r # map fst txs" "[]" "length txs"]
apply -
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by force
by auto
have [simp]: "⋀ aa b. b ∈ set (map snd txs) ⟹
aa ∈ set (map Var us) ⟹ b ∉ FvarsT aa"
using us_facts by (fastforce simp: image_def Int_def)
have [simp]:
"⋀b ac bc. b ∈ set us ⟹ b ∈ FvarsT ac ⟹ (ac, bc) ∉ set txs"
using us_facts(3) by (fastforce simp: image_def Int_def)

define χ where χ_def: "χ ≡ rawpsubstT r (zip (map Var us) (map snd txs))"
have χ: "χ ∈ atrm" unfolding χ_def
using assms using us_facts by (intro rawpsubstT_atrm) (force dest!: set_zip_D)+

hence "χ ∈ trm" by auto
note χ = χ this
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 "FvarsT χ =
FvarsT r - snd ` set txs ∪
⋃{if x ∈ FvarsT r then FvarsT t else {} |t x.
(t, x) ∈ set (zip (map Var us) (map snd txs))}"
unfolding χ_def set_txs using assms us_facts set_txs
by (intro FvarsT_rawpsubstT) (force dest!: set_zip_D)+
also have "… =
FvarsT r - snd ` set txs ∪
⋃{if x ∈ FvarsT r then {u} else {} |u x. u ∈ var ∧ (Var u, x) ∈ set (zip (map Var us) (map snd txs))}"
(is "… = ?R")
apply(subst 00)
by (metis (no_types, opaque_lifting) FvarsT_Var)
finally have 0: "FvarsT χ = ?R" .
have 1: "FvarsT (rawpsubstT χ (zip (map fst txs) us)) =
(FvarsT χ - set us) ∪
(⋃ {if u ∈ FvarsT χ then FvarsT t else {} | t u . (t,u) ∈ set (zip (map fst txs) us)})"
unfolding us_facts set_us using assms χ apply (intro FvarsT_rawpsubstT)
subgoal by auto
subgoal using us_facts by (auto dest!: set_zip_D)
subgoal using us_facts by (auto dest!: set_zip_D)
subgoal using us_facts by (auto dest!: set_zip_D)
subgoal by (auto dest!: set_zip_D) .

have 2: "FvarsT χ - set us = FvarsT r - snd ` set txs"
unfolding 0 apply auto
using set_zip_leftD us_facts(1) apply fastforce
using set_zip_leftD us_facts(1) apply fastforce
using us_facts(2) by auto
have 3:
"(⋃ {if u ∈ FvarsT χ then FvarsT t else {} | t u . (t,u) ∈ set (zip (map fst txs) us)}) =
(⋃ {if x ∈ FvarsT r then FvarsT t else {} | t x . (t,x) ∈ set txs})"
proof safe
fix xx tt y
assume xx: "xx ∈ (if y ∈ FvarsT χ 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 ∉ FvarsT r" using yin us_facts by auto
show "xx ∈ ⋃{if x ∈ FvarsT r then FvarsT t else {} |t x. (t, x) ∈ set txs}"
proof(cases "y ∈ FvarsT χ")
case True note y = True
hence xx: "xx ∈ FvarsT tt" using xx by simp
obtain x where xr: "x ∈ FvarsT r"
and yx: "(Var y, x) ∈ set (zip (map Var us) (map snd txs))"
using y ynotin unfolding 0 by (auto split: if_splits)
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 xr by auto
qed(insert xx, auto)
next
fix y tt xx
assume y: "y ∈ (if xx ∈ FvarsT r 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 ∈ FvarsT χ then FvarsT t else {} |t u. (t, u) ∈ set (zip (map fst txs) us)}"
proof(cases "xx ∈ FvarsT r")
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))"
apply(rule set_zip_length_map[OF uxx]) using us_facts by auto
hence uχ: "u ∈ FvarsT χ" using uin xx uvar unfolding 0 by auto
have ttu: "(tt, u) ∈ set (zip (map fst txs) us)"
apply(rule set_zip_map_fst_snd2[OF uxx tx]) using assms us_facts by auto
show ?thesis using uχ ttu y by auto
qed(insert y, auto)
qed
show ?thesis
by (simp add: psubstT_def Let_def us[symmetric] χ_def[symmetric] 1 2 3)
qed

lemma in_FvarsT_psubstTD:
assumes "y ∈ FvarsT (psubstT r txs)"
and "r ∈ atrm" and "snd ` (set txs) ⊆ var" and "fst ` (set txs) ⊆ atrm"
and "distinct (map snd txs)"
shows "y ∈ (FvarsT r - snd ` (set txs)) ∪
(⋃ {if x ∈ FvarsT r then FvarsT t else {} | t x . (t,x) ∈ set txs})"
using assms FvarsT_psubstT by auto

lemma substT2_fresh_switch:
assumes "r ∈ atrm" "t ∈ trm" "s ∈ trm" "x ∈ var" "y ∈ var"
and "x ≠ y" "x ∉ FvarsT s" "y ∉ FvarsT t"
shows "substT (substT r s y) t x = substT (substT r t x) s y"   (is "?L = ?R")
using assms by (simp add: substT_compose_diff[of r s t y x])

lemma rawpsubst2_fresh_switch:
assumes "r ∈ atrm" "t ∈ trm" "s ∈ trm" "x ∈ var" "y ∈ var"
and "x ≠ y" "x ∉ FvarsT s" "y ∉ FvarsT t"
shows "rawpsubstT r ([(s,y),(t,x)]) = rawpsubstT r ([(t,x),(s,y)])"
using assms by (simp add: substT2_fresh_switch)

(* this actually works for any trms, does not need atrms: *)
lemma rawpsubstT_compose:
assumes "t ∈ trm" and "snd ` (set txs1) ⊆ var" and "fst ` (set txs1) ⊆ atrm"
and "snd ` (set txs2) ⊆ var" and "fst ` (set txs2) ⊆ atrm"
shows "rawpsubstT (rawpsubstT t txs1) txs2 = rawpsubstT t (txs1 @ txs2)"
using assms apply (induct txs1 arbitrary: txs2 t)
subgoal by simp
subgoal for tx1 txs1 txs2 t apply (cases tx1) by auto .

lemma rawpsubstT_subst_fresh_switch:
assumes "r ∈ atrm" "snd ` (set txs) ⊆ var" and "fst ` (set txs) ⊆ atrm"
and "∀ x ∈ snd ` (set txs). x ∉ FvarsT s"
and "∀ t ∈ fst ` (set txs). y ∉ FvarsT t"
and "distinct (map snd txs)"
and "s ∈ atrm" and "y ∈ var" "y ∉ snd ` (set txs)"
shows "rawpsubstT (substT r s y) txs = rawpsubstT r (txs @ [(s,y)])"
using assms proof(induction txs arbitrary: r 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 "rawpsubstT r ((s, y) # (t, x) # txs) = rawpsubstT r ([(s, y),(t, x)] @ txs)" by simp
also have "… = rawpsubstT (rawpsubstT r [(s, y),(t, x)]) txs"
using Cons by auto
also have "rawpsubstT r [(s, y),(t, x)] = rawpsubstT r [(t, x),(s, y)]"
using Cons by (intro rawpsubst2_fresh_switch) auto
also have "rawpsubstT (rawpsubstT r [(t, x),(s, y)]) txs = rawpsubstT r ([(t, x),(s, y)] @ txs)"
using Cons by (intro rawpsubstT_compose) auto
also have "… = rawpsubstT (substT r t x) (txs @ [(s,y)])" using Cons by auto
also have "… = rawpsubstT r (((t, x) # txs) @ [(s, y)])" by simp
finally show ?case unfolding tx by auto
qed auto

lemma substT_rawpsubstT_fresh_switch:
assumes "r ∈ atrm" "snd ` (set txs) ⊆ var" and "fst ` (set txs) ⊆ atrm"
and "∀ x ∈ snd ` (set txs). x ∉ FvarsT s"
and "∀ t ∈ fst ` (set txs). y ∉ FvarsT t"
and "distinct (map snd txs)"
and "s ∈ atrm" and "y ∈ var" "y ∉ snd ` (set txs)"
shows "substT (rawpsubstT r txs) s y = rawpsubstT r ((s,y) # txs)"
using assms proof(induction txs arbitrary: r 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 "substT (rawpsubstT (substT r t x) txs) s y = rawpsubstT (substT r t x) ((s,y) # txs)"
using Cons.prems by (intro Cons.IH) auto
also have "… = rawpsubstT (rawpsubstT r [(t,x)]) ((s,y) # txs)" by simp
also have "… = rawpsubstT r ([(t,x)] @ ((s,y) # txs))"
using Cons.prems by (intro rawpsubstT_compose) auto
also have "… = rawpsubstT r ([(t,x),(s,y)] @ txs)" by simp
also have "… = rawpsubstT (rawpsubstT r [(t,x),(s,y)]) txs"
using Cons.prems by (intro rawpsubstT_compose[symmetric]) auto
also have "rawpsubstT r [(t,x),(s,y)] = rawpsubstT r [(s,y),(t,x)]"
using Cons.prems by (intro rawpsubst2_fresh_switch) auto
also have "rawpsubstT (rawpsubstT r [(s,y),(t,x)]) txs = rawpsubstT r ([(s,y),(t,x)] @ txs)"
using Cons.prems by (intro rawpsubstT_compose) auto
finally show ?case by simp
qed auto

lemma rawpsubstT_compose_freshVar:
assumes "r ∈ atrm" "snd ` (set txs) ⊆ var" and "fst ` (set txs) ⊆ atrm"
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 ∩ FvarsT r = {}"
"set us ∩ ⋃ (FvarsT ` (fst ` (set txs))) = {}"
"set us ∩ snd ` (set txs) = {}"
"length us = length txs"
"distinct us"
shows "rawpsubstT (rawpsubstT r (zip (map Var us) (map snd txs))) (zip (map fst txs) us) = rawpsubstT r txs"
using assms proof(induction txs arbitrary: us r)
case (Cons tx txs uus r)
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 ∩ FvarsT r = {}"
"set us ∩ ⋃ (FvarsT ` (fst ` (set txs))) = {}"
"set us ∩ snd ` (set txs) = {}"
"length us = length txs"
"distinct us" and u_facts: "u ∈ var" "u ∉ FvarsT r"
"u ∉ ⋃ (FvarsT ` (fst ` (set txs)))"
"u ∉ snd ` (set txs)" "u ∉ set us"
using Cons by auto
have [simp]: "⋀ bb xaa ab. bb ∈ FvarsT (Var xaa) ⟹
(ab, bb) ∈ set txs ⟹ xaa ∉ set us"
using us_facts(1,4) by force

let ?uxs = "zip (map Var us) (map snd txs)"
have 1: "rawpsubstT (substT r (Var u) x) ?uxs = rawpsubstT r (?uxs @ [(Var u,x)])"
using Cons.prems u_facts apply(intro rawpsubstT_subst_fresh_switch)
subgoal by auto
subgoal by (auto dest!: set_zip_D)
subgoal by (fastforce dest!: set_zip_D)
subgoal by (auto dest!: set_zip_D)
subgoal by (fastforce dest!: set_zip_D)
by (auto 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 ∈ FvarsT (rawpsubstT r (zip (map Var us) (map snd txs))) ⟹ False"
apply(drule in_FvarsT_rawpsubstTD) apply-
subgoal using Cons.prems by auto
subgoal using Cons.prems by (auto dest!: set_zip_D)
subgoal using Cons.prems  by (force dest!: set_zip_D)
subgoal using Cons.prems by (auto dest!: set_zip_D)
subgoal by (auto dest!: set_zip_D)
subgoal using us_facts(1,4,5) Cons.prems(7)
by(fastforce dest!: set_zip_D split: if_splits simp: u_facts(5)) .

have 3: "(tt, xx) ∉ set txs" if "xx ∈ FvarsT t" for tt xx
unfolding set_conv_nth mem_Collect_eq
proof safe
fix i
assume "(tt, xx) = txs ! i" "i < length txs"
then show False
using that Cons.prems(4) Cons.prems(5)[of 0 "Suc i"] tx
by (auto simp: nth_Cons' split: if_splits dest: sym)
qed

have 00: "rawpsubstT (rawpsubstT r ?uuxs) ?ttxs = rawpsubstT (substT (rawpsubstT r (?uxs @ [(Var u, x)])) t u) ?tus"

have "rawpsubstT r (?uxs @ [(Var u, x)]) = rawpsubstT (rawpsubstT r ?uxs) [(Var u, x)]"
using Cons.prems
by (intro rawpsubstT_compose[symmetric]) (auto 0 3 dest!: set_zip_D)
also have "rawpsubstT (rawpsubstT r ?uxs) [(Var u, x)] = substT (rawpsubstT r ?uxs) (Var u) x" by simp
finally have "substT (rawpsubstT r (?uxs @ [(Var u, x)])) t u =
substT (substT (rawpsubstT r ?uxs) (Var u) x) t u" by simp
also have "… = substT (rawpsubstT r ?uxs) t x"
using Cons 2 by (intro substT_substT) (auto 0 3 intro!: rawpsubstT_atrm[of r] dest!: set_zip_D)
also have "… = rawpsubstT r ((t,x) # ?uxs)"
using Cons.prems 3
by (intro substT_rawpsubstT_fresh_switch) (auto 0 3 dest!: set_zip_D FvarsT_VarD)
also have "… =  rawpsubstT r ([(t,x)] @ ?uxs)" by simp
also have "… = rawpsubstT (rawpsubstT r [(t,x)]) ?uxs"
using Cons.prems by (intro rawpsubstT_compose[symmetric]) (auto 0 3 dest!: set_zip_D)
finally have "rawpsubstT (substT (rawpsubstT r (?uxs @ [(Var u, x)])) t u) ?tus =
rawpsubstT (rawpsubstT (rawpsubstT r [(t,x)]) ?uxs) ?tus" by auto
hence "rawpsubstT (rawpsubstT r ?uuxs) ?ttxs = rawpsubstT (rawpsubstT (rawpsubstT r [(t,x)]) ?uxs) ?tus"
using 00 by auto
also have "… = rawpsubstT (rawpsubstT r [(t,x)]) txs"
using Cons.prems apply(intro Cons.IH)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by (metis Suc_leI le_imp_less_Suc length_Cons nth_Cons_Suc)
subgoal by auto
subgoal by (auto intro!: rawpsubstT dest!: set_zip_D in_FvarsT_substTD
split: if_splits)
by auto
finally show ?case by simp
qed auto

lemma rawpsubstT_compose_freshVar2_aux:
assumes r[simp]: "r ∈ atrm"
and ts: "set ts ⊆ atrm"
and xs: "set xs ⊆ var"  "distinct xs"
and us_facts: "set us ⊆ var"  "distinct us"
"set us ∩ FvarsT r = {}"
"set us ∩ ⋃ (FvarsT ` (set ts)) = {}"
"set us ∩ set xs = {}"
and vs_facts: "set vs ⊆ var"  "distinct vs"
"set vs ∩ FvarsT r = {}"
"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 "rawpsubstT (rawpsubstT r (zip (map Var us) xs)) (zip ts us) =
rawpsubstT (rawpsubstT r (zip (map Var vs) xs)) (zip ts vs)"
using assms proof(induction xs arbitrary: r ts us vs)
case (Cons x xs r 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 ?rux = "substT r (Var u) x"   let ?rvx = "substT r (Var v) x"

have 0: "rawpsubstT (rawpsubstT ?rux (zip (map Var us) xs)) (zip ts us) =
rawpsubstT (rawpsubstT ?rux (zip (map Var vs) xs)) (zip ts vs)"
using Cons.prems by (intro Cons.IH) (auto intro!: rawpsubstT dest!: set_zip_D simp: FvarsT_substT)

have 1: "rawpsubstT ?rux (zip (map Var vs) xs) =
substT (rawpsubstT r (zip (map Var vs) xs)) (Var u) x"
using Cons.prems
by (intro substT_rawpsubstT_fresh_switch[simplified,symmetric])
(auto intro!: rawpsubstT dest!: set_zip_D simp: subset_eq)

have 11: "rawpsubstT ?rvx (zip (map Var vs) xs) =
substT (rawpsubstT r (zip (map Var vs) xs)) (Var v) x"
using Cons.prems
by (intro substT_rawpsubstT_fresh_switch[simplified,symmetric])
(auto intro!: rawpsubstT dest!: set_zip_D simp: subset_eq)

have "substT (substT (rawpsubstT r (zip (map Var vs) xs)) (Var u) x) t u =
substT (rawpsubstT r (zip (map Var vs) xs)) t x"
using Cons.prems
by (intro substT_substT)
(auto 0 3 intro!: rawpsubstT_atrm[of r]
dest!: set_zip_D in_FvarsT_rawpsubstT_imp FvarsT_VarD simp: FvarsT_rawpsubstT)
also have "… = substT (substT (rawpsubstT r (zip (map Var vs) xs)) (Var v) x) t v"
using Cons.prems
by (intro substT_substT[symmetric])
(auto 0 3 intro!: rawpsubstT_atrm[of r] dest!: set_zip_D in_FvarsT_rawpsubstT_imp FvarsT_VarD
simp: FvarsT_rawpsubstT)
finally have
2: "substT (substT (rawpsubstT r (zip (map Var vs) xs)) (Var u) x) t u =
substT (substT (rawpsubstT r (zip (map Var vs) xs)) (Var v) x) t v"  .

have "rawpsubstT (substT (rawpsubstT ?rux (zip (map Var us) xs)) t u) (zip ts us) =
substT (rawpsubstT (rawpsubstT ?rux (zip (map Var us) xs)) (zip ts us)) t u"
using Cons.prems
by (intro substT_rawpsubstT_fresh_switch[simplified,symmetric])
(auto 0 3 intro!: rawpsubstT_atrm[of ?rux] substT_atrm dest!: set_zip_D)
also have "… = substT (rawpsubstT (rawpsubstT ?rux (zip (map Var vs) xs)) (zip ts vs)) t u"
unfolding 0 ..
also have "… = rawpsubstT (substT (rawpsubstT ?rux (zip (map Var vs) xs)) t u) (zip ts vs)"
using Cons.prems
by (intro substT_rawpsubstT_fresh_switch[simplified])
(auto 0 3 intro!: rawpsubstT_atrm[of ?rux] dest!: set_zip_D)
also have "… = rawpsubstT (substT (substT (rawpsubstT r (zip (map Var vs) xs)) (Var u) x) t u) (zip ts vs)"
unfolding 1 ..
also have "… = rawpsubstT (substT (substT (rawpsubstT r (zip (map Var vs) xs)) (Var v) x) t v) (zip ts vs)"
unfolding 2 ..
also have "… = rawpsubstT (substT (rawpsubstT ?rvx (zip (map Var vs) xs)) t v) (zip ts vs)"
unfolding 11 ..
finally have "rawpsubstT (substT (rawpsubstT ?rux (zip (map Var us) xs)) t u) (zip ts us) =
rawpsubstT (substT (rawpsubstT ?rvx (zip (map Var vs) xs)) t v) (zip ts vs)" .
thus ?case by simp
qed auto

(* ... now getting rid of the disjointness hypothesis: *)
lemma rawpsubstT_compose_freshVar2:
assumes r[simp]: "r ∈ atrm"
and ts: "set ts ⊆ atrm"
and xs: "set xs ⊆ var"  "distinct xs"
and us_facts: "set us ⊆ var"  "distinct us"
"set us ∩ FvarsT r = {}"
"set us ∩ ⋃ (FvarsT ` (set ts)) = {}"
"set us ∩ set xs = {}"
and vs_facts: "set vs ⊆ var"  "distinct vs"
"set vs ∩ FvarsT r = {}"
"set vs ∩ ⋃ (FvarsT ` (set ts)) = {}"
"set vs ∩ set xs = {}"
and l: "length us = length xs" "length vs = length xs" "length ts = length xs"
shows "rawpsubstT (rawpsubstT r (zip (map Var us) xs)) (zip ts us) =
rawpsubstT (rawpsubstT r (zip (map Var vs) xs)) (zip ts vs)"  (is "?L = ?R")
proof-
have ts_trm: "set ts ⊆ trm" using ts by auto
define ws where "ws = getFrN (xs @ us @ vs) (r # ts) [] (length xs)"
have ws_facts: "set ws ⊆ var"  "distinct ws"
"set ws ∩ FvarsT r = {}"
"set ws ∩ ⋃ (FvarsT ` (set ts)) = {}"
"set ws ∩ set xs = {}" "set ws ∩ set us = {}" "set ws ∩ set vs = {}"
"length ws = length xs" using assms(1) ts_trm assms(3-17) unfolding ws_def
using getFrN_Fvars[of "xs @ us @ vs" "r # ts" "[]" _ "length xs"]
getFrN_FvarsT[of "xs @ us @ vs" "r # ts" "[]" _ "length xs"]
getFrN_var[of "xs @ us @ vs" "r # ts" "[]" _ "length xs"]
getFrN_length[of "xs @ us @ vs" "r # ts" "[]" "length xs"]
apply -
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by force
subgoal by force
subgoal by force
subgoal by force
by auto
have "?L = rawpsubstT (rawpsubstT r (zip (map Var ws) xs)) (zip ts ws)"
using assms ws_facts by (intro rawpsubstT_compose_freshVar2_aux) auto
also have "… = ?R"
using assms ws_facts by (intro rawpsubstT_compose_freshVar2_aux) auto
finally show ?thesis .
qed

lemma in_fst_image: "a ∈ fst ` AB ⟷ (∃b. (a,b) ∈ AB)" by force

(* For many cases, the simpler rawpsubstT can replace psubst: *)
lemma psubstT_eq_rawpsubstT:
assumes "r ∈ atrm" "snd ` (set txs) ⊆ var" and "fst ` (set txs) ⊆ atrm"
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 "psubstT r txs = rawpsubstT r txs"
proof-
have txs_trm: "r ∈ trm" "fst ` (set txs) ⊆ trm" using assms by auto

note frt = getFrN_FvarsT[of "map snd txs" "r # map fst txs" "[]" _ "length txs"]
and fr = getFrN_Fvars[of "map snd txs" "r # map fst txs" "[]" _ "length txs"]
and var =  getFrN_var[of "map snd txs" "r # map fst txs" "[]" _ "length txs"]
and l = getFrN_length[of "map snd txs" "r # map fst txs" "[]" "length txs"]
define us where us: "us ≡ getFrN (map snd txs) (r # map fst txs) [] (length txs)"
have us_facts: "set us ⊆ var"
"set us ∩ FvarsT r = {}"
"set us ∩ ⋃ (FvarsT ` (fst ` (set txs))) = {}"
"set us ∩ snd ` (set txs) = {}"
"length us = length txs"
"distinct us"
using assms(2,4,5) txs_trm unfolding us

apply -
subgoal by auto
subgoal using frt by auto
subgoal using frt by (simp add: in_fst_image Int_def) (metis prod.collapse)
subgoal using var by (simp add: in_fst_image Int_def) (metis)
subgoal using l by auto
subgoal by auto .

show ?thesis
using rawpsubstT_compose_freshVar assms us_facts
by (simp add: psubstT_def Let_def us[symmetric])
qed

(* Some particular cases: *)
lemma psubstT_eq_substT:
assumes "r ∈ atrm" "x ∈ var" and "t ∈ atrm"
shows "psubstT r [(t,x)] = substT r t x"
proof-
have "psubstT r [(t,x)] = rawpsubstT r [(t,x)]"
using assms by (intro psubstT_eq_rawpsubstT) auto
thus ?thesis by auto
qed

lemma psubstT_eq_rawpsubst2:
assumes "r ∈ atrm" "x1 ∈ var" "x2 ∈ var" "t1 ∈ atrm" "t2 ∈ atrm"
and "x1 ≠ x2" "x2 ∉ FvarsT t1"
shows "psubstT r [(t1,x1),(t2,x2)] = rawpsubstT r [(t1,x1),(t2,x2)]"
using assms using less_SucE by (intro psubstT_eq_rawpsubstT) force+

lemma psubstT_eq_rawpsubst3:
assumes "r ∈ atrm" "x1 ∈ var" "x2 ∈ var" "x3 ∈ var" "t1 ∈ atrm" "t2 ∈ atrm" "t3 ∈ atrm"
and "x1 ≠ x2" "x1 ≠ x3" "x2 ≠ x3"
"x2 ∉ FvarsT t1" "x3 ∉ FvarsT t1" "x3 ∉ FvarsT t2"
shows "psubstT r [(t1,x1),(t2,x2),(t3,x3)] = rawpsubstT r [(t1,x1),(t2,x2),(t3,x3)]"
using assms less_SucE less_Suc_eq_0_disj
by (intro psubstT_eq_rawpsubstT) auto

lemma psubstT_eq_rawpsubst4:
assumes "r ∈ atrm" "x1 ∈ var" "x2 ∈ var" "x3 ∈ var" "x4 ∈ var"
"t1 ∈ atrm" "t2 ∈ atrm" "t3 ∈ atrm" "t4 ∈ atrm"
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 "psubstT r [(t1,x1),(t2,x2),(t3,x3),(t4,x4)] = rawpsubstT r [(t1,x1),(t2,x2),(t3,x3),(t4,x4)]"
using assms less_SucE less_Suc_eq_0_disj
by (intro psubstT_eq_rawpsubstT) auto

lemma rawpsubstT_same_Var[simp]:
assumes "r ∈ atrm" "set xs ⊆ var"
shows "rawpsubstT r (map (λx. (Var x,x)) xs) = r"
using assms by (induct xs) auto

lemma psubstT_same_Var[simp]:
assumes "r ∈ atrm" "set xs ⊆ var" and "distinct xs"
shows "psubstT r (map (λx. (Var x,x)) xs) = r"
proof-
have "psubstT r (map (λx. (Var x,x)) xs) = rawpsubstT r (map (λx. (Var x,x)) xs)"
using assms FvarsT_Var[of "xs ! _"] nth_mem[of _ xs]
by (intro psubstT_eq_rawpsubstT)
(auto simp: o_def distinct_conv_nth dest!: FvarsT_VarD)
thus ?thesis using assms by auto
qed

(* The following holds for all trms, so no need to prove it for a trms: *)
thm psubstT_notIn

(***)

(* Behavior of psubst w.r.t. equality formulas: *)

lemma rawpsubst_eql:
assumes "t1 ∈ trm" "t2 ∈ trm"
and "snd ` (set txs) ⊆ var" "fst ` (set txs) ⊆ trm"
shows "rawpsubst (eql t1 t2) txs = eql (rawpsubstT t1 txs) (rawpsubstT t2 txs)"
using assms apply (induct txs arbitrary: t1 t2)
subgoal by auto
subgoal for tx txs t1 t2 by (cases tx) auto .

lemma psubst_eql[simp]:
assumes "t1 ∈ atrm" "t2 ∈ atrm"
and "snd ` (set txs) ⊆ var" "fst ` (set txs) ⊆ atrm"
and "distinct (map snd txs)"
shows "psubst (eql t1 t2) txs = eql (psubstT t1 txs) (psubstT t2 txs)"
proof-
have t12: "fst ` (set txs) ⊆ trm"  using assms by auto
define us where us: "us ≡ getFrN (map snd txs) (map fst txs) [eql t1 t2] (length txs)"
have us_facts: "set us ⊆ var"
"set us ∩ FvarsT t1 = {}"
"set us ∩ FvarsT t2 = {}"
"set us ∩ ⋃ (FvarsT ` (fst ` (set txs))) = {}"
"set us ∩ snd ` (set txs) = {}"
"length us = length txs"
"distinct us"
using assms(1-3) t12 unfolding us
using getFrN_Fvars[of "map snd txs" "map fst txs" "[eql t1 t2]" _ "length txs"]
getFrN_FvarsT[of "map snd txs" "map fst txs" "[eql t1 t2]" _ "length txs"]
getFrN_var[of "map snd txs" "map fst txs" "[eql t1 t2]" _ "length txs"]
getFrN_length[of "map snd txs" "map fst txs" "[eql t1 t2]" "length txs"]
apply -
subgoal by auto
subgoal by force
subgoal by force
subgoal by fastforce
subgoal by (fastforce simp: image_iff)
by auto

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

define vs2 where vs2: "vs2 ≡ getFrN (map snd txs) (t2 # map fst txs) [] (length txs)"
have vs2_facts: "set vs2  ⊆ var"
"set vs2 ∩ FvarsT t2 = {}"
"set vs2 ∩ ⋃ (FvarsT ` (fst ` (set txs))) = {}"
"set vs2 ∩ snd ` (set txs) = {}"
"length vs2 = length txs"
"distinct vs2"
using assms(1-3) t12 unfolding vs2
using getFrN_Fvars[of "map snd txs" "t2 # map fst txs" "[]" _ "length txs"]
getFrN_FvarsT[of "map snd txs" "t2 # map fst txs" "[]" _ "length txs"]
getFrN_var[of "map snd txs" "t2 # map fst txs" "[]" _ "length txs"]
getFrN_length[of "map snd txs" "t2 # map fst txs" "[]" "length txs"]
apply -
subgoal by auto
subgoal by force
subgoal by auto
subgoal by force
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 ?e = "rawpsubst (eql t1 t2) ?uxs"
have e: "?e = eql (rawpsubstT t1 ?uxs) (rawpsubstT t2 ?uxs)"
apply(rule rawpsubst_eql) using assms us_facts apply auto
apply(drule set_zip_rightD) apply simp apply blast
apply(drule set_zip_leftD) apply simp apply blast .
have 0: "rawpsubst ?e ?tus =
eql (rawpsubstT (rawpsubstT t1 ?uxs) ?tus) (rawpsubstT (rawpsubstT t2 ?uxs) ?tus)"
unfolding e using assms us_facts apply(intro rawpsubst_eql)
subgoal by (auto intro!: rawpsubstT dest!: set_zip_D)
subgoal by (auto intro!: rawpsubstT dest!: set_zip_D)
subgoal by (auto intro!: rawpsubstT dest!: set_zip_D)
subgoal by (fastforce intro!: rawpsubstT dest!: set_zip_D) .
have 1: "rawpsubstT (rawpsubstT t1 ?uxs) ?tus =
rawpsubstT (rawpsubstT t1 (zip (map Var vs1) (map snd txs))) (zip (map fst txs) vs1)"
using assms us_facts vs1_facts
by (intro rawpsubstT_compose_freshVar2) auto
have 2: "rawpsubstT (rawpsubstT t2 ?uxs) ?tus =
rawpsubstT (rawpsubstT t2 (zip (map Var vs2) (map snd txs))) (zip (map fst txs) vs2)"
using assms us_facts vs2_facts
by (intro rawpsubstT_compose_freshVar2) auto
show ?thesis unfolding psubstT_def psubst_def
by (simp add: Let_def us[symmetric] vs1[symmetric] vs2[symmetric] 0 1 2)
qed

(* psubst versus the exists-unique quantifier: *)

lemma psubst_exu[simp]:
assumes "φ ∈ fmla" "x ∈ var" "snd ` set txs ⊆ var" "fst ` set txs ⊆ atrm"
"x ∉ snd ` set txs" "x ∉ (⋃t ∈ fst ` set txs. FvarsT t)" "distinct (map snd txs)"
shows "psubst (exu x φ) txs = exu x (psubst φ txs)"
proof-
have f: "fst ` set txs ⊆ trm" using assms by (meson atrm_trm subset_trans)
note assms1 = assms(1-3) assms(5-7) f
define u where u: "u ≡ getFr (x # map snd txs) (map fst txs) [φ]"
have u_facts:  "u ∈ var" "u ≠ x"
"u ∉ snd ` set txs" "u ∉ (⋃t ∈ fst ` set txs. FvarsT t)" "u ∉ Fvars φ"
unfolding u using f getFr_FvarsT_Fvars[of "x # map snd txs" "map fst txs" "[φ]"] by (auto simp: assms)
hence [simp]: "psubst (subst φ (Var u) x) txs = subst (psubst φ txs) (Var u) x"
using assms apply(intro psubst_subst_fresh_switch f) by auto
show ?thesis using f assms u_facts
by (subst exu_def_var[of _ u "psubst φ txs"])
(auto dest!: in_Fvars_psubstD split: if_splits simp: exu_def_var[of _ u] )
qed

(* psubst versus the arithmetic trm constructors: *)

thm psubstT_Var_not[no_vars]

lemma rawpsubstT_Var_in:
assumes "snd ` (set txs) ⊆ var" "fst ` (set txs) ⊆ trm"
and "distinct (map snd txs)" and "(s,y) ∈ set txs"
and "⋀ i j. i < j ⟹ j < length txs ⟹ snd (txs!j) ∉ FvarsT (fst (txs!i))"
shows "rawpsubstT (Var y) txs = s"
using assms proof(induction txs)
case (Cons tx txs)
obtain t x where tx[simp]: "tx = (t,x)" by (cases tx) auto

have 00: "FvarsT t ∩ snd ` set txs = {}"
using Cons.prems(5)[of 0 "Suc _"] by (auto simp: set_conv_nth)

have "rawpsubstT (substT (Var y) t x) txs = s"
proof(cases "y = x")
case [simp]:True hence [simp]: "s = t" using ‹distinct (map snd (tx # txs))›
‹(s, y) ∈ set (tx # txs)› using image_iff by fastforce
show ?thesis using Cons.prems 00 by auto
next
case False
hence [simp]: "substT (Var y) t x = Var y"
using Cons.prems by (intro substT_notIn) auto
have "rawpsubstT (Var y) txs = s"
using Cons.prems apply(intro Cons.IH)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal using False by auto
subgoal by (metis length_Cons less_Suc_eq_0_disj nth_Cons_Suc) .
thus ?thesis by simp
qed
thus ?case by simp
qed auto

lemma psubstT_Var_in:
assumes "y ∈ var" "snd ` (set txs) ⊆ var" "fst ` (set txs) ⊆ trm"
and "distinct (map snd txs)" and "(s,y) ∈ set txs"
shows "psubstT (Var y) txs = s"
proof-
define us where us: "us ≡ getFrN (map snd txs) (Var y # map fst txs) [] (length txs)"
have us_facts: "set us ⊆ var"
"set us ∩ ⋃ (FvarsT ` (fst ` (set txs))) = {}"
"y ∉ set us"
"set us ∩ snd ` (set txs) = {}"
"length us = length txs"
"distinct us"
using assms unfolding us
using getFrN_FvarsT[of "map snd txs" "Var y # map fst txs" "[]" _ "length txs"]
getFrN_var[of "map snd txs" "Var y # map fst txs" "[]" _ "length txs"]
getFrN_length[of "map snd txs" "Var y # map fst txs" "[]" "length txs"]
apply -
subgoal by auto
subgoal by auto
subgoal by force
subgoal by force
by auto
obtain i where i[simp]: "i < length txs" "txs!i = (s,y)" using ‹(s,y) ∈ set txs›
by (metis in_set_conv_nth)
hence 00[simp]: "⋀ j. j < length txs ⟹ txs ! j = txs ! i ⟹ j = i"
using ‹distinct (map snd txs)› distinct_Ex1 nth_mem by fastforce
have 000[simp]: "⋀ j ia. j < length txs ⟹ ia < length txs ⟹ snd (txs ! j) ≠ us ! ia"
using assms us_facts
by (metis IntI empty_iff length_map list.set_map nth_map nth_mem)
have [simp]: "⋀ii jj. ii < jj ⟹ jj < length txs ⟹ us ! ii ∈ var"
using nth_mem us_facts(1) us_facts(5) by auto
have [simp]: "⋀i j. i < j ⟹ j < length txs ⟹ us ! j ∉ FvarsT (fst (txs ! i))"
using us_facts(2,5) by (auto simp: Int_def)

have 0: "rawpsubstT (Var y) (zip (map Var us) (map snd txs)) = Var (us!i)"
using assms us_facts
by (intro rawpsubstT_Var_in)
(auto dest!: set_zip_D simp: in_set_conv_nth intro!: exI[of _ i])

have "rawpsubstT (rawpsubstT (Var y) (zip (map Var us) (map snd txs))) (zip (map fst txs) us) = s"
unfolding 0 using assms us_facts
by (intro rawpsubstT_Var_in)
(auto dest!: set_zip_D simp: in_set_conv_nth intro!: exI[of _ i])
thus ?thesis unfolding psubstT_def by (simp add: Let_def us[symmetric])
qed

lemma psubstT_Var_Cons_aux:
assumes "y ∈ var" "x ∈ var" "t ∈ atrm"
"snd ` set txs ⊆ var" "fst ` set txs ⊆ atrm" "x ∉ snd ` set txs"
"distinct (map snd txs)"  "y ≠ x"
shows "psubstT (Var y) ((t, x) # txs) = psubstT (Var y) txs"
proof-
have txs_trm: "t ∈ trm" "fst ` set txs ⊆ trm" using assms by auto
note assms1 = assms(1,2) assms(4) assms(6-8) txs_trm

note fvt = getFrN_FvarsT[of "x # map snd txs" "Var y # t # map fst txs" "[]" _ "Suc (length txs)"]
and var = getFrN_var[of "x # map snd txs" "Var y # t # map fst txs" "[]" _ "Suc (length txs)"]
and l = getFrN_length[of "x # map snd txs" "Var y # t # map fst txs" "[]" "Suc (length txs)"]
define uus where uus:
"uus ≡ getFrN (x # map snd txs) (Var y # t # map fst txs) [] (Suc (length txs))"
have uus_facts: "set uus ⊆ var"
"set uus ∩ ⋃ (FvarsT ` (fst ` (set txs))) = {}"
"set uus ∩ snd ` (set txs) = {}"
"set uus ∩ FvarsT t = {}"
"x ∉ set uus"
"y ∉ set uus"
"length uus = Suc (length txs)"
"distinct uus"
using assms1 unfolding uus
apply -
subgoal by auto
subgoal using fvt by (simp add: in_fst_image Int_def) (metis prod.collapse)
subgoal using var by (force simp add: in_fst_image Int_def)
subgoal using fvt by auto
subgoal using var by (fastforce simp: in_fst_image Int_def)
subgoal using fvt by (force simp: in_fst_image Int_def)
subgoal using l by auto
subgoal by auto .

obtain u us where uus_us[simp]: "uus = u # us" using uus_facts by (cases uus) auto

have us_facts: "set us ⊆ var"
"set us ∩ ⋃ (FvarsT ` (fst ` (set txs))) = {}"
"set us ∩ snd ` (set txs) = {}"
"set us ∩ FvarsT t = {}"
"x ∉ set us"
"y ∉ set us"
"length us = length txs"
"distinct us"
and u_facts: "u ∈ var"
"u ∉ ⋃ (FvarsT ` (fst ` (set txs)))"
"u ∉ snd ` (set txs)"
"u ∉FvarsT t"
"u ≠ x"
"u ≠ y"
"u ∉ set us"
using uus_facts by auto

note fvt = getFrN_FvarsT[of "map snd txs" "Var y # map fst txs" "[]" _ "length txs"]
and var = getFrN_var[of "map snd txs" "Var y # map fst txs" "[]" _ "length txs"]
and l = getFrN_length[of "map snd txs" "Var y # map fst txs" "[]" "length txs"]
define vs where vs: "vs ≡ getFrN (map snd txs) (Var y #  map fst txs) [] (length txs)"
have vs_facts: "set vs ⊆ var"
"set vs ∩ ⋃ (FvarsT ` (fst ` (set txs))) = {}"
"y ∉ set vs"
"set vs ∩ snd ` (set txs) = {}"
"length vs = length txs"
"distinct vs"
using assms1 unfolding vs
apply -
subgoal by auto
subgoal using fvt by (simp add: in_fst_image Int_def) (metis prod.collapse)
subgoal using fvt l by fastforce
subgoal using var by (force simp: Int_def in_fst_image)
subgoal using l by auto
subgoal by auto .

have 0: "substT (Var y) (Var u) x = Var y"
using assms u_facts by auto
have 1: "substT (rawpsubstT (Var y) (zip (map Var us) (map snd txs))) t u =
rawpsubstT (Var y) (zip (map Var us) (map snd txs))"
using assms u_facts us_facts
by (intro substT_notIn)
(auto 0 3 intro!: rawpsubstT dest!: set_zip_D in_FvarsT_rawpsubstT_imp FvarsT_VarD)

have "rawpsubstT (rawpsubstT (Var y) (zip (map Var us) (map snd txs))) (zip (map fst txs) us) =
rawpsubstT (rawpsubstT (Var y) (zip (map Var vs) (map snd txs))) (zip (map fst txs) vs)"
using assms vs_facts us_facts by (intro rawpsubstT_compose_freshVar2) auto
thus ?thesis unfolding psubstT_def
by (simp add: Let_def uus[symmetric] vs[symmetric] 0 1)
qed

text ‹Simplification rules for parallel substitution:›

lemma psubstT_Var_Cons[simp]:
"y ∈ var ⟹ x ∈ var ⟹ t ∈ atrm ⟹
snd ` set txs ⊆ var ⟹ fst ` set txs ⊆ atrm ⟹ distinct (map snd txs) ⟹ x ∉ snd ` set txs ⟹
psubstT (Var y) ((t,x) # txs) = (if y = x then t else psubstT (Var y) txs)"
apply(cases "y = x")
subgoal by (rule psubstT_Var_in) auto
subgoal by (auto intro!: psubstT_Var_Cons_aux) .

lemma psubstT_zer[simp]:
assumes "snd ` (set txs) ⊆ var" and "fst ` (set txs) ⊆ trm"
shows "psubstT zer txs = zer"
using assms by (intro psubstT_num) auto

lemma rawpsubstT_suc:
assumes "r ∈ trm" and "snd ` (set txs) ⊆ var" and "fst ` (set txs) ⊆ trm"
shows "rawpsubstT (suc r) txs = suc (rawpsubstT r txs)"
using assms apply(induct txs arbitrary: r)
subgoal by simp
subgoal for tx txs r by (cases tx) auto .

lemma psubstT_suc[simp]:
assumes "r ∈ atrm" and "snd ` (set txs) ⊆ var" and "fst ` (set txs) ⊆ atrm"
and "distinct (map snd txs)"
shows "psubstT (suc r) txs = suc (psubstT r txs)"
proof-
have 000: "r ∈ trm" "fst ` (set txs) ⊆ trm" using assms by auto
define us where us: "us ≡ getFrN (map snd txs) (suc r # map fst txs) [] (length txs)"
have us_facts: "set us ⊆ var"
"set us ∩ FvarsT r = {}"
"set us ∩ ⋃ (FvarsT ` (fst ` (set txs))) = {}"
"set us ∩ snd ` (set txs) = {}"
"length us = length txs"
"distinct us"
using assms(2) 000 unfolding us
using getFrN_FvarsT[of "map snd txs" "suc r # map fst txs" "[]" _ "length txs"]
getFrN_Fvars[of "map snd txs" "suc r # map fst txs" "[]" _ "length txs"]
getFrN_var[of "map snd txs" "suc r # map fst txs" "[]" _ "length txs"]
getFrN_length[of "map snd txs" "suc r # map fst txs" "[]" "length txs"]
getFrN_length[of "map snd txs" "suc r # map fst txs" "[]" "length txs"]
apply -
subgoal by auto
subgoal by force
subgoal by auto
subgoal by force
by auto
define vs where vs: "vs ≡ getFrN (map snd txs) (r # map fst txs) [] (length txs)"
have vs_facts: "set vs ⊆ var"
"set vs ∩ FvarsT r = {}"
"set vs ∩ ⋃ (FvarsT ` (fst ` (set txs))) = {}"
"set vs ∩ snd ` (set txs) = {}"
"length vs = length txs"
"distinct vs"
using assms(2) 000 unfolding vs
using getFrN_FvarsT[of "map snd txs" "r # map fst txs" "[]" _ "length txs"]
getFrN_Fvars[of "map snd txs" "r # map fst txs" "[]" _ "length txs"]
getFrN_var[of "map snd txs" "r # map fst txs" "[]" _ "length txs"]
getFrN_length[of "map snd txs" "r # map fst txs" "[]" "length txs"]
getFrN_length[of "map snd txs" "r # map fst txs" "[]" "length txs"]
apply -
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by force
by auto
have 0: "rawpsubstT (suc r) (zip (map Var vs) (map snd txs)) =
```