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"
  by (simp add: substT_compose_diff)

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"
    by (simp add: 1)

  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: *)

(* We already have: *)
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)) =