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)) =
           suc (rawpsubstT r (zip (map Var vs) (map snd txs)))"
  using assms vs_facts by (intro rawpsubstT_suc) (auto dest!: set_zip_D)

  have "rawpsubstT (rawpsubstT (suc r) (zip (map Var us) (map snd txs))) (zip (map fst txs) us) =
        rawpsubstT (rawpsubstT (suc r) (zip (map Var vs) (map snd txs))) (zip (map fst txs) vs)"
  using assms us_facts vs_facts by (intro rawpsubstT_compose_freshVar2) auto
  also have "… = suc (rawpsubstT (rawpsubstT r (zip (map Var vs) (map snd txs))) (zip (map fst txs) vs))"
  unfolding 0 using assms vs_facts apply(intro rawpsubstT_suc)
  subgoal by (auto dest!: set_zip_D intro!: rawpsubstT)
  subgoal by (auto dest!: set_zip_D)
  subgoal by (fastforce dest!: set_zip_D simp: Int_def) .
  finally show ?thesis
  by (simp add: Let_def us[symmetric] vs[symmetric] psubstT_def)
qed

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

lemma psubstT_pls[simp]:
assumes "r1 ∈ atrm" "r2 ∈ atrm" and "snd ` (set txs) ⊆ var" and "fst ` (set txs) ⊆ atrm"
and "distinct (map snd txs)"
shows "psubstT (pls r1 r2) txs = pls (psubstT r1 txs) (psubstT r2 txs)"
proof-
  have 000: "fst ` (set txs) ⊆ trm" using assms by auto
  define us where us: "us ≡ getFrN (map snd txs) (pls r1 r2 # map fst txs) [] (length txs)"
  have us_facts: "set us ⊆ var"
  "set us ∩ FvarsT r1 = {}"
  "set us ∩ FvarsT r2 = {}"
  "set us ∩ ⋃ (FvarsT ` (fst ` (set txs))) = {}"
  "set us ∩ snd ` (set txs) = {}"
  "length us = length txs"
  "distinct us"
  using assms(1-3) 000 unfolding us
  using getFrN_FvarsT[of "map snd txs" "pls r1 r2 # map fst txs" "[]" _ "length txs"]
        getFrN_Fvars[of "map snd txs" "pls r1 r2 # map fst txs" "[]" _ "length txs"]
        getFrN_var[of "map snd txs" "pls r1 r2 # map fst txs" "[]" _ "length txs"]
        getFrN_length[of "map snd txs" "pls r1 r2 # map fst txs" "[]" "length txs"]
        getFrN_length[of "map snd txs" "pls r1 r2 # map fst txs" "[]" "length txs"]
  apply -
  subgoal by auto
  subgoal by force
  subgoal by force
  subgoal by auto
  subgoal by force
  by auto
  define vs1 where vs1: "vs1 ≡ getFrN (map snd txs) (r1 # map fst txs) [] (length txs)"
  have vs1_facts: "set vs1 ⊆ var"
  "set vs1 ∩ FvarsT r1 = {}"
  "set vs1 ∩ ⋃ (FvarsT ` (fst ` (set txs))) = {}"
  "set vs1 ∩ snd ` (set txs) = {}"
  "length vs1 = length txs"
  "distinct vs1"
  using assms(1-3) 000 unfolding vs1
  using getFrN_FvarsT[of "map snd txs" "r1 # map fst txs" "[]" _ "length txs"]
        getFrN_Fvars[of "map snd txs" "r1 # map fst txs" "[]" _ "length txs"]
        getFrN_var[of "map snd txs" "r1 # map fst txs" "[]" _ "length txs"]
        getFrN_length[of "map snd txs" "r1 # map fst txs" "[]" "length txs"]
        getFrN_length[of "map snd txs" "r1 # map fst txs" "[]" "length txs"]
  apply -
  subgoal by auto
  subgoal by auto
  subgoal by auto
  subgoal by force
  by auto
  define vs2 where vs2: "vs2 ≡ getFrN (map snd txs) (r2 # map fst txs) [] (length txs)"
  have vs2_facts: "set vs2 ⊆ var"
  "set vs2 ∩ FvarsT r2 = {}"
  "set vs2 ∩ ⋃ (FvarsT ` (fst ` (set txs))) = {}"
  "set vs2 ∩ snd ` (set txs) = {}"
  "length vs2 = length txs"
  "distinct vs2"
  using assms(1-3) 000 unfolding vs2
  using getFrN_FvarsT[of "map snd txs" "r2 # map fst txs" "[]" _ "length txs"]
        getFrN_Fvars[of "map snd txs" "r2 # map fst txs" "[]" _ "length txs"]
        getFrN_var[of "map snd txs" "r2 # map fst txs" "[]" _ "length txs"]
        getFrN_length[of "map snd txs" "r2 # map fst txs" "[]" "length txs"]
        getFrN_length[of "map snd txs" "r2 # map fst txs" "[]" "length txs"]
  apply -
  subgoal by auto
  subgoal by auto
  subgoal by auto
  subgoal by force
  by auto
  have 0: "rawpsubstT (pls r1 r2) (zip (map Var us) (map snd txs)) =
           pls (rawpsubstT r1 (zip (map Var us) (map snd txs)))
               (rawpsubstT r2 (zip (map Var us) (map snd txs)))"
  using assms us_facts by (intro rawpsubstT_pls) (auto dest!: set_zip_D)

  have 1: "rawpsubstT (rawpsubstT r1 (zip (map Var us) (map snd txs))) (zip (map fst txs) us) =
           rawpsubstT (rawpsubstT r1 (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 r2 (zip (map Var us) (map snd txs))) (zip (map fst txs) us) =
           rawpsubstT (rawpsubstT r2 (zip (map Var vs2) (map snd txs))) (zip (map fst txs) vs2)"
  using assms us_facts vs2_facts by (intro rawpsubstT_compose_freshVar2) auto

  have 3: "rawpsubstT (rawpsubstT (pls r1 r2) (zip (map Var us) (map snd txs))) (zip (map fst txs) us) =
    pls (rawpsubstT (rawpsubstT r1 (zip (map Var us) (map snd txs))) (zip (map fst txs) us))
     (rawpsubstT (rawpsubstT r2 (zip (map Var us) (map snd txs))) (zip (map fst txs) us))"
  unfolding 0 using assms us_facts apply(intro rawpsubstT_pls)
  subgoal by (auto dest!: set_zip_D intro!: rawpsubstT)
  subgoal by (force dest!: set_zip_D intro!: rawpsubstT simp: Int_def)
  subgoal by (auto dest!: set_zip_D intro!: rawpsubstT)
  subgoal by (fastforce dest!: set_zip_D intro!: rawpsubstT simp: Int_def) .
  show ?thesis unfolding psubstT_def
  by (simp add: Let_def us[symmetric] vs1[symmetric] vs2[symmetric] 1 2 3)
qed

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

lemma psubstT_tms[simp]:
assumes "r1 ∈ atrm" "r2 ∈ atrm" and "snd ` (set txs) ⊆ var" and "fst ` (set txs) ⊆ atrm"
and "distinct (map snd txs)"
shows "psubstT (tms r1 r2) txs = tms (psubstT r1 txs) (psubstT r2 txs)"
proof-
  have 000: "fst ` (set txs) ⊆ trm" using assms by auto
  define us where us: "us ≡ getFrN (map snd txs) (tms r1 r2 # map fst txs) [] (length txs)"
  have us_facts: "set us ⊆ var"
  "set us ∩ FvarsT r1 = {}"
  "set us ∩ FvarsT r2 = {}"
  "set us ∩ ⋃ (FvarsT ` (fst ` (set txs))) = {}"
  "set us ∩ snd ` (set txs) = {}"
  "length us = length txs"
  "distinct us"
  using assms(1-3) 000 unfolding us
  using getFrN_FvarsT[of "map snd txs" "tms r1 r2 # map fst txs" "[]" _ "length txs"]
        getFrN_Fvars[of "map snd txs" "tms r1 r2 # map fst txs" "[]" _ "length txs"]
        getFrN_var[of "map snd txs" "tms r1 r2 # map fst txs" "[]" _ "length txs"]
        getFrN_length[of "map snd txs" "tms r1 r2 # map fst txs" "[]" "length txs"]
        getFrN_length[of "map snd txs" "tms r1 r2 # map fst txs" "[]" "length txs"]
  apply -
  subgoal by auto
  subgoal by force
  subgoal by force
  subgoal by auto
  subgoal by force
  by auto
  define vs1 where vs1: "vs1 ≡ getFrN (map snd txs) (r1 # map fst txs) [] (length txs)"
  have vs1_facts: "set vs1 ⊆ var"
  "set vs1 ∩ FvarsT r1 = {}"
  "set vs1 ∩ ⋃ (FvarsT ` (fst ` (set txs))) = {}"
  "set vs1 ∩ snd ` (set txs) = {}"
  "length vs1 = length txs"
  "distinct vs1"
  using assms(1-3) 000 unfolding vs1
  using getFrN_FvarsT[of "map snd txs" "r1 # map fst txs" "[]" _ "length txs"]
        getFrN_Fvars[of "map snd txs" "r1 # map fst txs" "[]" _ "length txs"]
        getFrN_var[of "map snd txs" "r1 # map fst txs" "[]" _ "length txs"]
        getFrN_length[of "map snd txs" "r1 # map fst txs" "[]" "length txs"]
        getFrN_length[of "map snd txs" "r1 # map fst txs" "[]" "length txs"]
  apply -
  subgoal by auto
  subgoal by force
  subgoal by auto
  subgoal by force
  subgoal by force
  by auto
  define vs2 where vs2: "vs2 ≡ getFrN (map snd txs) (r2 # map fst txs) [] (length txs)"
  have vs2_facts: "set vs2 ⊆ var"
  "set vs2 ∩ FvarsT r2 = {}"
  "set vs2 ∩ ⋃ (FvarsT ` (fst ` (set txs))) = {}"
  "set vs2 ∩ snd ` (set txs) = {}"
  "length vs2 = length txs"
  "distinct vs2"
  using assms(1-3) 000 unfolding vs2
  using getFrN_FvarsT[of "map snd txs" "r2 # map fst txs" "[]" _ "length txs"]
        getFrN_Fvars[of "map snd txs" "r2 # map fst txs" "[]" _ "length txs"]
        getFrN_var[of "map snd txs" "r2 # map fst txs" "[]" _ "length txs"]
        getFrN_length[of "map snd txs" "r2 # map fst txs" "[]" "length txs"]
        getFrN_length[of "map snd txs" "r2 # map fst txs" "[]" "length txs"]
  apply -
  subgoal by auto
  subgoal by force
  subgoal by auto
  subgoal by force
  subgoal by force
  by auto
  have 0: "rawpsubstT (tms r1 r2) (zip (map Var us) (map snd txs)) =
           tms (rawpsubstT r1 (zip (map Var us) (map snd txs)))
               (rawpsubstT r2 (zip (map Var us) (map snd txs)))"
  using assms us_facts by (intro rawpsubstT_tms) (auto dest!: set_zip_D)

  have 1: "rawpsubstT (rawpsubstT r1 (zip (map Var us) (map snd txs))) (zip (map fst txs) us) =
           rawpsubstT (rawpsubstT r1 (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 r2 (zip (map Var us) (map snd txs))) (zip (map fst txs) us) =
           rawpsubstT (rawpsubstT r2 (zip (map Var vs2) (map snd txs))) (zip (map fst txs) vs2)"
  using assms us_facts vs2_facts by (intro rawpsubstT_compose_freshVar2) auto

  have 3: "rawpsubstT (rawpsubstT (tms r1 r2) (zip (map Var us) (map snd txs))) (zip (map fst txs) us) =
    tms (rawpsubstT (rawpsubstT r1 (zip (map Var us) (map snd txs))) (zip (map fst txs) us))
     (rawpsubstT (rawpsubstT r2 (zip (map Var us) (map snd txs))) (zip (map fst txs) us))"
  unfolding 0 using assms us_facts apply(intro rawpsubstT_tms)
  subgoal by (auto dest!: set_zip_D intro!: rawpsubstT)
  subgoal by (force dest!: set_zip_D intro!: rawpsubstT simp: Int_def)
  subgoal by (auto dest!: set_zip_D intro!: rawpsubstT)
  subgoal by (fastforce dest!: set_zip_D intro!: rawpsubstT simp: Int_def) .

  show ?thesis unfolding psubstT_def
  by (simp add: Let_def us[symmetric] vs1[symmetric] vs2[symmetric] 1 2 3)
qed


section ‹The (Nonstrict and Strict) Order Relations›

text ‹Lq (less than or equal to) is a formula with free vars xx and yy.
NB: Out of the two possible ways, adding zz to the left or to the right,
we choose the former, since this seems to enable Q (Robinson arithmetic)
to prove as many useful properties as possible.›

definition Lq :: "'fmla" where
"Lq ≡ exi zz (eql (Var yy) (pls (Var zz) (Var xx)))"

text ‹Alternative, more flexible definition , for any non-capturing bound variable:›
lemma Lq_def2: "z ∈ var ⟹ z ≠ yy ⟹ z ≠ xx ⟹ Lq = exi z (eql (Var yy) (pls  (Var z) (Var xx)))"
unfolding Lq_def using exi_rename[of "eql (Var yy) (pls (Var zz) (Var xx))" zz z] by auto

lemma Lq[simp,intro!]: "Lq ∈ fmla"
unfolding Lq_def by auto

lemma Fvars_Lq[simp]: "Fvars Lq = {xx,yy}"
unfolding Lq_def by auto

text ‹As usual, we also define a predicate version:›
definition LLq where "LLq ≡ λ t1 t2. psubst Lq [(t1,xx), (t2,yy)]"

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

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

lemma Fvars_LLq[simp]: "t1 ∈ trm ⟹ t2 ∈ trm ⟹
Fvars (LLq t1 t2) = FvarsT t1 ∪ FvarsT t2"
unfolding LLq_def apply(subst Fvars_psubst)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal apply safe
  subgoal by auto
  subgoal by auto
  subgoal by force
  subgoal by force
  subgoal by force
  subgoal by force . .

text ‹This lemma will be the working definition of LLq:›
lemma LLq_pls:
assumes [simp]: "t1 ∈ atrm" "t2 ∈ atrm" "z ∈ var" "z ∉ FvarsT t1" "z ∉ FvarsT t2"
shows "LLq t1 t2 = exi z (eql t2 (pls (Var z) t1))"
proof-
  define z' where "z' ≡ getFr [xx,yy,z] [t1,t2] []"
  have z_facts[simp]: "z' ∈ var" "z' ≠ yy" "z' ≠ xx" "z' ≠ z" "z ≠ z'" "z' ∉ FvarsT t1" "z' ∉ FvarsT t2"
  using getFr_FvarsT_Fvars[of "[xx,yy,z]" "[t1,t2]" "[]"] unfolding z'_def by auto
  have "LLq t1 t2 = exi z' (eql t2 (pls (Var z') t1))"
  by (simp add: LLq_def Lq_def2[of z'])
  also have "… = exi z (eql t2 (pls (Var z) t1))"
  using exi_rename[of "eql t2 (pls (Var z') t1)" z' z, simplified] .
  finally show ?thesis .
qed

lemma LLq_pls_zz:
assumes "t1 ∈ atrm" "t2 ∈ atrm" "zz ∉ FvarsT t1" "zz ∉ FvarsT t2"
shows "LLq t1 t2 = exi zz (eql t2 (pls (Var zz) t1))"
using assms by (intro LLq_pls) auto

text ‹If we restrict attention to arithmetic terms, we can prove a uniform
substitution property for LLq:›
lemma subst_LLq[simp]:
assumes [simp]: "t1 ∈ atrm" "t2 ∈ atrm" "s ∈ atrm" "x ∈ var"
shows "subst (LLq t1 t2) s x = LLq (substT t1 s x) (substT t2 s x)"
proof-
  define z where "z ≡ getFr [xx,yy,x] [t1,t2,s] []"
  have z_facts[simp]: "z ∈ var" "z ≠ xx" "z ≠ yy" "z ≠ x" "z ∉ FvarsT t1" "z ∉ FvarsT t2" "z ∉ FvarsT s"
  using getFr_FvarsT_Fvars[of "[xx,yy,x]" "[t1,t2,s]" "[]"] unfolding z_def by auto
  show ?thesis
  by(simp add: FvarsT_substT LLq_pls[of _ _ z] subst2_fresh_switch Lq_def)
qed

lemma psubst_LLq[simp]:
assumes 1: "t1 ∈ atrm" "t2 ∈ atrm" "fst ` set txs ⊆ atrm"
and 2: "snd ` set txs ⊆ var"
and 3: "distinct (map snd txs)"
shows "psubst (LLq t1 t2) txs = LLq (psubstT t1 txs) (psubstT t2 txs)"
proof-
  have 0: "t1 ∈ trm" "t2 ∈ trm" "fst ` set txs ⊆ trm" using 1 by auto
  define z where z: "z ≡ getFr ([xx,yy] @ map snd txs) ([t1,t2] @ map fst txs) []"
  have us_facts: "z ∈ var"  "z ≠ xx" "z ≠ yy"
  "z ∉ FvarsT t1" "z ∉ FvarsT t2"
  "z ∉ ⋃ (FvarsT ` (fst ` (set txs)))"
  "z ∉ snd ` (set txs)"
  using 0 2 unfolding z
  using getFr_FvarsT[of "[xx,yy] @  map snd txs" "[t1,t2] @ map fst txs" "[]" ]
        getFr_Fvars[of "[xx,yy] @  map snd txs" "[t1,t2] @ map fst txs" "[]" ]
        getFr_var[of "[xx,yy] @  map snd txs" "[t1,t2] @ map fst txs" "[]"]
  apply -
  subgoal by auto
  subgoal by force
  subgoal by force
  subgoal by force
  subgoal by force
  subgoal by auto
  subgoal by (force simp: image_iff) .

  note in_FvarsT_psubstTD[dest!]
  note if_splits[split]
  show ?thesis
  using assms 0 us_facts apply(subst LLq_pls[of _ _ z])
  subgoal by auto
  subgoal by auto
  subgoal by auto
  subgoal by auto
  subgoal by auto
  subgoal apply(subst LLq_pls[of _ _ z]) by auto .
qed


text ‹Lq less than) is the strict version of the order relation.
We prove similar facts as for Lq›

definition Ls :: "'fmla" where
"Ls ≡ cnj Lq (neg (eql (Var xx) (Var yy)))"

lemma Ls[simp,intro!]: "Ls ∈ fmla"
unfolding Ls_def by auto

lemma Fvars_Ls[simp]: "Fvars Ls = {xx,yy}"
unfolding Ls_def by auto

definition LLs where "LLs ≡ λ t1 t2. psubst Ls [(t1,xx), (t2,yy)]"

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

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

lemma Fvars_LLs[simp]: "t1 ∈ trm ⟹ t2 ∈ trm ⟹
Fvars (LLs t1 t2) = FvarsT t1 ∪ FvarsT t2"
unfolding LLs_def apply(subst Fvars_psubst)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal apply safe
  subgoal by auto
  subgoal by auto
  subgoal by force
  subgoal by force
  subgoal by force
  subgoal by force . .

text ‹The working definition of LLs:›
lemma LLs_LLq:
"t1 ∈ atrm ⟹ t2 ∈ atrm ⟹
 LLs t1 t2 = cnj (LLq t1 t2) (neg (eql t1 t2))"
by (simp add: LLs_def Ls_def LLq_def)

lemma subst_LLs[simp]:
assumes [simp]: "t1 ∈ atrm" "t2 ∈ atrm" "s ∈ atrm" "x ∈ var"
shows "subst (LLs t1 t2) s x = LLs (substT t1 s x) (substT t2 s x)"
by(simp add: LLs_LLq subst2_fresh_switch Ls_def)

lemma psubst_LLs[simp]:
assumes 1: "t1 ∈ atrm" "t2 ∈ atrm" "fst ` set txs ⊆ atrm"
and 2: "snd ` set txs ⊆ var"
and 3: "distinct (map snd txs)"
shows "psubst (LLs t1 t2) txs = LLs (psubstT t1 txs) (psubstT t2 txs)"
proof-
  have 0: "t1 ∈ trm" "t2 ∈ trm" "fst ` set txs ⊆ trm" using 1 by auto
  define z where z: "z ≡ getFr ([xx,yy] @ map snd txs) ([t1,t2] @ map fst txs) []"
  have us_facts: "z ∈ var"  "z ≠ xx" "z ≠ yy"
  "z ∉ FvarsT t1" "z ∉ FvarsT t2"
  "z ∉ ⋃ (FvarsT ` (fst ` (set txs)))"
  "z ∉ snd ` (set txs)"
  using 0 2 unfolding z
  using getFr_FvarsT[of "[xx,yy] @  map snd txs" "[t1,t2] @ map fst txs" "[]" ]
        getFr_Fvars[of "[xx,yy] @  map snd txs" "[t1,t2] @ map fst txs" "[]" ]
        getFr_var[of "[xx,yy] @  map snd txs" "[t1,t2] @ map fst txs" "[]"]
   apply -
  subgoal by auto
  subgoal by force
  subgoal by force
  subgoal by force
  subgoal by force
  subgoal by auto
  subgoal by (force simp: image_iff) .
  show ?thesis
  using assms 0 us_facts by (simp add: LLs_LLq)
qed


section ‹Bounded Quantification›

text ‹Bounded forall›

definition ball :: "'var ⇒ 'trm ⇒ 'fmla ⇒ 'fmla" where
"ball x t φ ≡ all x (imp (LLq (Var x) t) φ)"

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

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

lemma subst_ball:
"φ ∈ fmla ⟹ t ∈ atrm ⟹ t1 ∈ atrm ⟹ x ∈ var ⟹ y ∈ var ⟹ x ≠ y ⟹ x ∉ FvarsT t1 ⟹
 subst (ball x t φ) t1 y = ball x (substT t t1 y) (subst φ t1 y)"
  unfolding ball_def by simp

lemma psubst_ball:
"φ ∈ fmla ⟹ y ∈ var ⟹ snd ` set txs ⊆ var ⟹ t ∈ atrm ⟹
 fst ` set txs ⊆ trm ⟹ fst ` set txs ⊆ atrm ⟹ y ∉ snd ` set txs ⟹ y ∉ (⋃t ∈ fst ` set txs. FvarsT t) ⟹
 distinct (map snd txs) ⟹
 psubst (ball y t φ) txs = ball y (psubstT t txs) (psubst φ txs)"
unfolding ball_def by simp

text ‹Bounded exists›

definition bexi :: "'var ⇒ 'trm ⇒ 'fmla ⇒ 'fmla" where
"bexi x t φ ≡ exi x (cnj (LLq (Var x) t) φ)"

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

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

lemma subst_bexi:
"φ ∈ fmla ⟹ t ∈ atrm ⟹ t1 ∈ atrm ⟹ x ∈ var ⟹ y ∈ var ⟹ x ≠ y ⟹ x ∉ FvarsT t1 ⟹
 subst (bexi x t φ) t1 y = bexi x (substT t t1 y) (subst φ t1 y)"
unfolding bexi_def by simp

lemma psubst_bexi:
"φ ∈ fmla ⟹ y ∈ var ⟹ snd ` set txs ⊆ var ⟹ t ∈ atrm ⟹
 fst ` set txs ⊆ trm ⟹ fst ` set txs ⊆ atrm ⟹ y ∉ snd ` set txs ⟹ y ∉ (⋃t ∈ fst ` set txs. FvarsT t) ⟹
 distinct (map snd txs) ⟹
 psubst (bexi y t φ) txs = bexi y (psubstT t txs) (psubst φ txs)"
unfolding bexi_def by simp

end ― ‹context @{locale Syntax_Arith}›

(*<*)
end
(*>*)