# Theory Prelim

chapter ‹Preliminaries›

(*<*)
theory Prelim
imports Main "HOL-Eisbach.Eisbach"
begin
(*>*)

section ‹Trivia›

abbreviation (input) any where "any ≡ undefined"

lemma Un_Diff2: "B ∩ C = {} ⟹ A ∪ B - C = A - C ∪ B" by auto

lemma Diff_Diff_Un: "A - B - C = A - (B ∪ C)" by auto

fun first :: "nat ⇒ nat list" where
"first 0 = []"
| "first (Suc n) = n # first n"

lemma fst_set_zip_map_fst:
"length xs = length ys ⟹ fst  (set (zip (map fst xs) ys)) = fst  (set xs)"
by (induct xs ys rule: list_induct2) auto

lemma snd_set_zip_map_snd:
"length xs = length ys ⟹ snd  (set (zip xs (map snd ys))) = snd  (set ys)"
by (induct xs ys rule: list_induct2) auto

lemma snd_set_zip:
"length xs = length ys ⟹ snd  (set (zip xs ys)) = set ys"
by (induct xs ys rule: list_induct2) auto

lemma set_zip_D: "(x, y) ∈ set (zip xs ys) ⟹ x ∈ set xs ∧ y ∈ set ys"
using set_zip_leftD set_zip_rightD by auto

lemma inj_on_set_zip_map:
assumes i: "inj_on f X"
and a: "(f x1, y1) ∈ set (zip (map f xs) ys)" "set xs ⊆ X" "x1 ∈ X" "length xs = length ys"
shows "(x1, y1) ∈ set (zip xs ys)"
using a proof (induct xs arbitrary: ys x1 y1)
case (Cons x xs yys)
thus ?case using i unfolding inj_on_def by (cases yys) auto
qed (insert i, auto)

lemma set_zip_map_fst_snd:
assumes "(u,x) ∈ set (zip us (map snd txs))"
and "(t,u) ∈ set (zip (map fst txs) us)"
and "distinct (map snd txs)"
and "distinct us" and "length us = length txs"
shows "(t, x) ∈ set txs"
using assms(5,1-4)
by (induct us txs arbitrary: u x t rule: list_induct2)
(auto dest: set_zip_leftD set_zip_rightD)

lemma set_zip_map_fst_snd2:
assumes "(u, x) ∈ set (zip us (map snd txs))"
and "(t, x) ∈ set txs"
and "distinct (map snd txs)"
and "distinct us" and "length us = length txs"
shows "(t, u) ∈ set (zip (map fst txs) us)"
using assms(5,1-4)
by (induct us txs arbitrary: u x t rule: list_induct2)
(auto dest: set_zip_rightD simp: image_iff)

lemma set_zip_length_map:
assumes "(x1, y1) ∈ set (zip xs ys)" and "length xs = length ys"
shows "(f x1, y1) ∈ set (zip (map f xs) ys)"
using assms(2,1) by (induct xs ys arbitrary: x1 y1 rule: list_induct2) auto

definition asList :: "'a set ⇒ 'a list" where
"asList A ≡ SOME as. set as = A"

lemma asList[simp,intro!]: "finite A ⟹ set (asList A) = A"
unfolding asList_def by (meson finite_list tfl_some)

lemma triv_Un_imp_aux:
"(⋀a. φ ⟹ a ∉ A ⟹ a ∈ B ⟷ a ∈ C) ⟹ φ ⟶ A ∪ B = A ∪ C"
by auto

definition toN where "toN n ≡ [0..<(Suc n)]"

lemma set_toN[simp]: "set (toN n) = {0..n}"
unfolding toN_def by auto

declare list.map_cong[cong]

section ‹Some Proof Infrastructure›

ML ‹
exception TAC of term

val simped = Thm.rule_attribute [] (fn context => fn thm =>
let
val ctxt = Context.proof_of context;
val (thm', ctxt') = yield_singleton (apfst snd oo Variable.import false) thm ctxt;
val full_goal = Thm.prop_of thm';
val goal = Goal.prove ctxt' [] [] full_goal (fn {context = ctxt, prems = _} =>
HEADGOAL (asm_full_simp_tac ctxt THEN' TRY o SUBGOAL (fn (goal, _) => raise (TAC goal))))
|> K (HOLogic.mk_Trueprop @{term True})
handle TAC goal => goal;
val thm = Goal.prove ctxt' [] [] goal (fn {context = ctxt, prems = _} =>
HEADGOAL (Method.insert_tac ctxt [thm'] THEN' asm_full_simp_tac ctxt))
|> singleton (Variable.export ctxt' ctxt);
in thm end)

val _ = Theory.setup
(Attrib.setup \<^binding>‹simped› (pair simped) "simped rule");
›

method RULE methods meth uses rule =
(rule rule; (solves meth)?)

text ‹TryUntilFail:›
(* This is non-hazardous, since it does not touch the goal on which it fails. *)
method TUF methods meth =
((meth;fail)+)?

text ‹Helping a method, usually simp or auto, with specific substitutions inserted.
For auto, this is a bit like a "simp!" analogue of "intro!" and "dest!": It forces
the application of an indicated simplification rule, if this is possible.›

method variousSubsts1 methods meth uses s1 =
(meth?,(subst s1)?, meth?)
method variousSubsts2 methods meth uses s1 s2 =
(meth?,(subst s1)?, meth?, subst s2, meth?)
method variousSubsts3 methods meth uses s1 s2 s3 =
(meth?,(subst s1)?, meth?, (subst s2)?, meth?, (subst s3)?, meth?)
method variousSubsts4 methods meth uses s1 s2 s3 s4 =
(meth?,(subst s1)?, meth?, (subst s2)?, meth?, (subst s3)?, meth?, (subst s4)?, meth?)
method variousSubsts5 methods meth uses s1 s2 s3 s4 s5 =
(meth?,(subst s1)?, meth?, (subst s2)?, meth?, (subst s3)?, meth?, (subst s4)?, meth?, (subst s5)?, meth?)
method variousSubsts6 methods meth uses s1 s2 s3 s4 s5 s6 =
(meth?,(subst s1)?, meth?, (subst s2)?, meth?, (subst s3)?, meth?,
(subst s4)?, meth?, (subst s5)?, meth?, (subst s6)?, meth?)

(*<*)
end
(*>*)



# Theory Syntax

chapter ‹Syntax›

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

section ‹Generic Syntax›

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

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

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

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

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

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

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

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

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

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

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

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

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

lemma exists_nat_var:
"∃ f::nat⇒'var. inj f ∧ range f ⊆ var"

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

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

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

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

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

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

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

subsection ‹Instance Operator›

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

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

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

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

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

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

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

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

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

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

subsection ‹Fresh Variables›

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

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

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

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

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

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

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

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

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

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

subsection ‹Parallel Term Substitution›

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

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

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

text ‹The psubstT versions of the subst axioms.›

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

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

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

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

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

subsection ‹Parallel Formula Substitution›

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

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

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

text ‹The psubst versions of the subst axioms.›

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

text ‹Some particular cases:›

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

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

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

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

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

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

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

lemma psubst_notIn[simp]:
assumes "x ∈ var" "snd  (set txs) ⊆ var" "fst  (set txs) ⊆ trm" "φ ∈ fmla"
and  "Fvars φ ∩ snd  (set txs) = {}"
shows "psubst φ txs = φ"
proof-
define us where us: "us = getFrN (map snd txs) (map fst txs) [φ] (length txs)"
have us_facts: "set us ⊆ var"
"set us ∩ Fvars φ = {}"
"set us ∩ ⋃ (FvarsT  (fst  (set txs))) = {}"
"set us ∩ snd  (set txs) = {}"
"length us = length txs"
using getFrN_Fvars[of "map snd txs" "map fst txs" "[φ]" _ "length txs"]
getFrN_FvarsT[of "map snd txs" "map fst txs" "[φ]" _ "length txs"]
getFrN_var[of "map snd txs" "map fst txs" "[φ]" _ "length txs"]
getFrN_length[of "map snd txs" "map fst txs" "[φ]" "length txs"]
using assms unfolding us apply -
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by (fastforce simp: image_iff)
subgoal by auto .
(* *)
have [simp]: "rawpsubst φ (zip (map Var us) (map snd txs)) = φ"
using assms us_facts apply(intro rawpsubst_notIn)
subgoal by (auto dest!: set_zip_rightD)
subgoal by (auto dest!: set_zip_leftD)
subgoal by auto
subgoal by (auto dest!: set_zip_rightD) .
have [simp]: "rawpsubst φ (zip (map fst txs) us) = φ"
using assms us_facts apply(intro rawpsubst_notIn)
subgoal by (auto dest!: set_zip_rightD)
subgoal by (auto dest!: set_zip_leftD)
subgoal by auto
subgoal by (auto dest!: set_zip_rightD) .
show ?thesis using assms us_facts unfolding psubst_def
by(auto simp: Let_def us[symmetric])
qed

end ― ‹context @{locale Generic_Syntax}›

section ‹Adding Numerals to the Generic Syntax›

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

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

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

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

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

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

end ― ‹context @{locale Syntax_with_Numerals}›

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

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

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

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

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

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

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

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

text ‹Parallel substitution versus connectives and quantifiers.›

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

have 0: "rawpsubst (all y φ) (zip (map Var ws) (map snd txs)) =
all y (rawpsubst φ (zip (map Var ws) (map snd txs)))"
using assms ws_facts  apply(intro rawpsubst_all)
subgoal by auto
subgoal by auto
subgoal by (auto dest!: set_zip_D)
subgoal by (auto dest!: set_zip_D)
subgoal by (auto dest!: set_zip_D)
subgoal by (fastforce dest: set_zip_D) .

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

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

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

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

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

have 0: "rawpsubst (exi y φ) (zip (map Var ws) (map snd txs)) =
exi y (rawpsubst φ (zip (map Var ws) (map snd txs)))"
using assms ws_facts apply(intro rawpsubst_exi)
subgoal by auto
subgoal by auto
subgoal by (auto dest!: set_zip_D)
subgoal by (auto dest!: set_zip_D)
subgoal by (auto dest!: set_zip_D)
subgoal by (fastforce dest: set_zip_D) .

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

end ― ‹context @{locale Syntax_with_Connectives}›

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

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

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

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

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

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

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

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

end ― ‹context @{locale Syntax_with_Connectives}›

text ‹The addition of False among logical connectives›

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

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

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

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

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

subsection ‹Iterated conjunction›

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

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

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

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

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

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

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

subsection ‹Parallel substitution versus the new connectives›

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

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

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

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

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

end ― ‹context @{locale Syntax_with_Connectives_False}›

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

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

subsection ‹Iterated disjunction›

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

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

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

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

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

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

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

subsection ‹Parallel substitution versus the new connectives›

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

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

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

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

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

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

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

end ― ‹context @{locale Syntax_with_Connectives_False_Disj}›

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

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

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

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

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

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

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

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

end ― ‹context @{locale Syntax_PseudoOrder}›

section ‹Allowing the Renaming of Quantified Variables›

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

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

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

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

section ‹The Exists-Unique Quantifier›

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

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

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

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

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

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

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

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

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

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

end ― ‹context @{locale Syntax_with_Connectives_Rename}›

(*<*)
end
(*>*)

# Theory Deduction

chapter ‹Deduction›

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

text ‹We formalize deduction in a logical system that (shallowly) embeds
intuitionistic logic connectives and quantifiers over a signature containing
the numerals.›

section ‹Positive Logic Deduction›

locale Deduct =
Syntax_with_Numerals_and_Connectives
var trm fmla Var FvarsT substT Fvars subst
num
eql cnj imp all exi
for
var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
and Var FvarsT substT Fvars subst
and num
and eql cnj imp all exi
+
fixes
― ‹Provability of numeric formulas:›
prv :: "'fmla ⇒ bool"
― ‹Hilbert-style system for intuitionistic logic over $\longrightarrow$,$\land$,$\forall$,$\exists$.
($\bot$, $\lnot$ and $\lor$ will be included later.)
Hilbert-style is preferred since it requires the least amount of infrastructure.
(Later, natural deduction rules will also be defined.)›
assumes
― ‹Propositional rules and axioms. There is a single propositional rule, modus ponens.›
― ‹The modus ponens rule:›
prv_imp_mp:
"⋀ φ χ. φ ∈ fmla ⟹ χ ∈ fmla ⟹
prv (imp φ χ) ⟹ prv φ ⟹ prv χ"
and
― ‹The propositional intuitionitic axioms:›
prv_imp_imp_triv:
"⋀φ χ. φ ∈ fmla ⟹ χ ∈ fmla ⟹
prv (imp φ (imp χ φ))"
and
prv_imp_trans:
"⋀ φ χ ψ. φ ∈ fmla ⟹ χ ∈ fmla ⟹ ψ ∈ fmla ⟹
prv (imp (imp φ (imp χ ψ))
(imp (imp φ χ) (imp φ ψ)))"
and
prv_imp_cnjL:
"⋀ φ χ. φ ∈ fmla ⟹ χ ∈ fmla ⟹
prv (imp (cnj φ χ) φ)"
and
prv_imp_cnjR:
"⋀ φ χ. φ ∈ fmla ⟹ χ ∈ fmla ⟹
prv (imp (cnj φ χ) χ)"
and
prv_imp_cnjI:
"⋀ φ χ. φ ∈ fmla ⟹ χ ∈ fmla ⟹
prv (imp φ (imp χ (cnj φ χ)))"
and
(*   *)
― ‹Predicate calculus (quantifier) rules and axioms›
― ‹The rules of universal and existential generalization:›
prv_all_imp_gen:
"⋀ x φ χ. x ∉ Fvars φ ⟹ prv (imp φ χ) ⟹ prv (imp φ (all x χ))"
and
prv_exi_imp_gen:
"⋀ x φ χ. x ∈ var ⟹ φ ∈ fmla ⟹ χ ∈ fmla ⟹
x ∉ Fvars χ ⟹ prv (imp φ χ) ⟹ prv (imp (exi x φ) χ)"
and
― ‹Two quantifier instantiation axioms:›
prv_all_inst:
"⋀ x φ t.
x ∈ var ⟹ φ ∈ fmla ⟹ t ∈ trm ⟹
prv (imp (all x φ) (subst φ t x))"
and
prv_exi_inst:
"⋀ x φ t.
x ∈ var ⟹ φ ∈ fmla ⟹ t ∈ trm ⟹
prv (imp (subst φ t x) (exi x φ))"
and
― ‹The equality axioms:›
prv_eql_refl:
"⋀ x. x ∈ var ⟹
prv (eql (Var x) (Var x))"
and
prv_eql_subst:
"⋀ φ x y.
x ∈ var ⟹ y ∈ var ⟹ φ ∈ fmla ⟹
prv ((imp (eql (Var x) (Var y))
(imp φ (subst φ (Var y) x))))"
begin

subsection ‹Properties of the propositional fragment›

lemma prv_imp_triv:
assumes phi: "φ ∈ fmla" and psi: "ψ ∈ fmla"
shows "prv ψ ⟹ prv (imp φ ψ)"
by (meson prv_imp_imp_triv prv_imp_mp imp phi psi)

lemma prv_imp_refl:
assumes phi: "φ ∈ fmla"
shows "prv (imp φ φ)"
by (metis prv_imp_imp_triv prv_imp_mp prv_imp_trans imp phi)

lemma prv_imp_refl2: "φ ∈ fmla ⟹ ψ ∈ fmla ⟹ φ = ψ ⟹ prv (imp φ ψ)"
using prv_imp_refl by auto

lemma prv_cnjI:
assumes phi: "φ ∈ fmla" and chi: "χ ∈ fmla"
shows "prv φ ⟹ prv χ ⟹ prv (cnj φ χ)"
by (meson cnj prv_imp_cnjI prv_imp_mp imp phi chi)

lemma prv_cnjEL:
assumes phi: "φ ∈ fmla" and chi: "χ ∈ fmla"
shows "prv (cnj φ χ) ⟹ prv φ"
using chi phi prv_imp_cnjL prv_imp_mp by blast

lemma prv_cnjER:
assumes phi: "φ ∈ fmla" and chi: "χ ∈ fmla"
shows "prv (cnj φ χ) ⟹ prv χ"
using chi phi prv_imp_cnjR prv_imp_mp by blast

lemma prv_prv_imp_trans:
assumes phi: "φ ∈ fmla" and chi: "χ ∈ fmla" and psi: "ψ ∈ fmla"
assumes 1: "prv (imp φ χ)" and 2: "prv (imp χ ψ)"
shows "prv (imp φ ψ)"
proof-
have "prv (imp φ (imp χ ψ))" by (simp add: 2 chi prv_imp_triv phi psi)
thus ?thesis by (metis 1 chi prv_imp_mp prv_imp_trans imp phi psi)
qed

lemma prv_imp_trans1:
assumes phi: "φ ∈ fmla" and chi: "χ ∈ fmla" and psi: "ψ ∈ fmla"
shows "prv (imp (imp χ ψ) (imp (imp φ χ) (imp φ ψ)))"
by (meson chi prv_prv_imp_trans prv_imp_imp_triv prv_imp_trans imp phi psi)

lemma prv_imp_com:
assumes phi: "φ ∈ fmla" and chi: "χ ∈ fmla" and psi: "ψ ∈ fmla"
assumes "prv (imp φ (imp χ ψ))"
shows "prv (imp χ (imp φ ψ))"
by (metis (no_types) assms prv_prv_imp_trans prv_imp_imp_triv prv_imp_mp prv_imp_trans imp)

lemma prv_imp_trans2:
assumes phi: "φ ∈ fmla" and chi: "χ ∈ fmla" and psi: "ψ ∈ fmla"
shows "prv (imp (imp φ χ) (imp (imp χ ψ) (imp φ ψ)))"
using prv_imp_mp prv_imp_trans prv_imp_trans1 prv_imp_imp_triv
by (meson chi prv_imp_com imp phi psi)

lemma prv_imp_cnj:
assumes "φ ∈ fmla" and "χ ∈ fmla" and "ψ ∈ fmla"
shows "prv (imp φ ψ) ⟹ prv (imp φ χ) ⟹ prv (imp φ (cnj ψ χ))"
proof -
assume "prv (imp φ ψ)"
moreover
assume "prv (imp φ χ)"
then have "prv (imp φ (imp ψ f))" if "prv (imp χ f)" "f ∈ fmla" for f
using that by (metis (no_types) assms imp prv_imp_imp_triv prv_prv_imp_trans)
moreover have "prv (imp φ (imp ψ ψ)) ⟹ prv (imp φ (imp φ ψ))"
using ‹prv (imp φ ψ)› by (metis (no_types) assms(1,3) imp prv_imp_com prv_prv_imp_trans)
ultimately show ?thesis
by (metis (no_types) assms cnj imp prv_imp_cnjI prv_imp_com prv_imp_mp prv_imp_trans)
qed

lemma prv_imp_imp_com:
assumes "φ ∈ fmla" and "χ ∈ fmla" and "ψ ∈ fmla"
shows
"prv (imp (imp φ (imp χ ψ))
(imp χ (imp φ ψ)))"
by (metis (no_types) assms
prv_prv_imp_trans prv_imp_com prv_imp_imp_triv prv_imp_trans imp)

lemma prv_cnj_imp_monoR2:
assumes "φ ∈ fmla" and "χ ∈ fmla" and "ψ ∈ fmla"
assumes "prv (imp φ (imp χ ψ))"
shows "prv (imp (cnj φ χ) ψ)"
proof -
have "prv (imp (cnj φ χ) (cnj φ χ))"
using prv_imp_refl by (blast intro: assms(1-3))
then have "prv (imp (imp (cnj φ χ) (imp (cnj φ χ) ψ)) (imp (cnj φ χ) ψ))"
by (metis (no_types) cnj imp assms(1-3) prv_imp_com prv_imp_mp prv_imp_trans)
then show ?thesis
by (metis (no_types) imp cnj assms prv_imp_cnjL prv_imp_cnjR prv_imp_com prv_imp_mp prv_prv_imp_trans)
qed

lemma prv_imp_imp_imp_cnj:
assumes "φ ∈ fmla" and "χ ∈ fmla" and "ψ ∈ fmla"
shows
"prv (imp (imp φ (imp χ ψ))
(imp (cnj φ χ) ψ))"
proof-
have "prv (imp φ (imp (imp φ (imp χ ψ)) (imp χ ψ)))"
by (simp add: assms prv_imp_com prv_imp_refl)
hence "prv (imp φ (imp χ (imp (imp φ (imp χ ψ)) ψ)))"
by (metis (no_types, lifting) assms prv_prv_imp_trans prv_imp_imp_com imp)
hence "prv (imp (cnj φ χ)
(imp (imp φ (imp χ ψ)) ψ))"
thus ?thesis using assms prv_imp_com prv_imp_mp by (meson cnj imp)
qed

lemma prv_imp_cnj_imp:
assumes "φ ∈ fmla" and "χ ∈ fmla" and "ψ ∈ fmla"
shows
"prv (imp (imp (cnj φ χ) ψ)
(imp φ (imp χ ψ)))"
by (metis (no_types) assms cnj prv_prv_imp_trans prv_imp_cnjI prv_imp_com prv_imp_trans2 imp)

lemma prv_cnj_imp:
assumes "φ ∈ fmla" and "χ ∈ fmla" and "ψ ∈ fmla"
assumes "prv (imp (cnj φ χ) ψ)"
shows "prv (imp φ (imp χ ψ))"
using assms prv_imp_cnj_imp prv_imp_mp by (meson cnj imp)

text ‹Monotonicy of conjunction w.r.t. implication:›

lemma prv_cnj_imp_monoR:
assumes "φ ∈ fmla" and "χ ∈ fmla" and "ψ ∈ fmla"
shows "prv (imp (imp φ χ) (imp (imp φ ψ) (imp φ (cnj χ ψ))))"
by (meson assms cnj imp prv_cnj_imp prv_cnj_imp_monoR2 prv_imp_cnj prv_imp_cnjL prv_imp_cnjR)

lemma prv_imp_cnj3L:
assumes "φ1 ∈ fmla" and "φ2 ∈ fmla" and "χ ∈ fmla"
shows "prv (imp (imp φ1 χ) (imp (cnj φ1 φ2) χ))"
using assms prv_imp_cnjL prv_imp_mp prv_imp_trans2
by (metis cnj imp)

lemma prv_imp_cnj3R:
assumes "φ1 ∈ fmla" and "φ2 ∈ fmla" and "χ ∈ fmla"
shows "prv (imp (imp φ2 χ) (imp (cnj φ1 φ2) χ))"
using prv_imp_cnjR prv_imp_mp prv_imp_trans2
by (metis assms cnj imp)

lemma prv_cnj_imp_mono:
assumes "φ1 ∈ fmla" and "φ2 ∈ fmla" and "χ1 ∈ fmla" and "χ2 ∈ fmla"
shows "prv (imp (imp φ1 χ1) (imp (imp φ2 χ2) (imp (cnj φ1 φ2) (cnj χ1 χ2))))"
proof-
have "prv (imp (imp (cnj φ1 φ2) χ1) (imp (imp (cnj φ1 φ2) χ2) (imp (cnj φ1 φ2) (cnj χ1 χ2))))"
using prv_cnj_imp_monoR[of "cnj φ1 φ2" χ1 χ2] assms by auto
hence "prv (imp (imp φ1 χ1) (imp (imp (cnj φ1 φ2) χ2) (imp (cnj φ1 φ2) (cnj χ1 χ2))))"
by (metis (no_types) imp cnj assms prv_imp_cnj3L prv_prv_imp_trans)
hence "prv (imp (imp (cnj φ1 φ2) χ2) (imp (imp φ1 χ1) (imp (cnj φ1 φ2) (cnj χ1 χ2))))"
using prv_imp_com assms by (meson cnj imp)
hence "prv (imp (imp φ2 χ2) (imp (imp φ1 χ1) (imp (cnj φ1 φ2) (cnj χ1 χ2))))"
using prv_imp_cnj3R prv_imp_mp prv_imp_trans1
by (metis (no_types) assms cnj prv_prv_imp_trans imp)
thus ?thesis using prv_imp_com assms
by (meson cnj imp)
qed

lemma prv_cnj_mono:
assumes "φ1 ∈ fmla" and "φ2 ∈ fmla" and "χ1 ∈ fmla" and "χ2 ∈ fmla"
assumes "prv (imp φ1 χ1)" and "prv (imp φ2 χ2)"
shows "prv (imp (cnj φ1 φ2) (cnj χ1 χ2))"
using assms prv_cnj_imp_mono prv_imp_mp
by (metis (mono_tags) cnj prv_prv_imp_trans prv_imp_cnj prv_imp_cnjL prv_imp_cnjR)

lemma prv_cnj_imp_monoR4:
assumes "φ ∈ fmla" and "χ ∈ fmla" and "ψ1 ∈ fmla" and "ψ2 ∈ fmla"
shows
"prv (imp (imp φ (imp χ ψ1))
(imp (imp φ (imp χ ψ2)) (imp φ (imp χ (cnj ψ1 ψ2)))))"
by (simp add: assms prv_cnj_imp prv_imp_cnj prv_imp_cnjL prv_imp_cnjR prv_cnj_imp_monoR2)

lemma prv_imp_cnj4:
assumes "φ ∈ fmla" and "χ ∈ fmla" and "ψ1 ∈ fmla" and "ψ2 ∈ fmla"
shows "prv (imp φ (imp χ ψ1)) ⟹ prv (imp φ (imp χ ψ2)) ⟹ prv (imp φ (imp χ (cnj ψ1 ψ2)))"
by (simp add: assms prv_cnj_imp prv_imp_cnj prv_cnj_imp_monoR2)

lemma prv_cnj_imp_monoR5:
assumes "φ1 ∈ fmla" and "φ2 ∈ fmla" and "χ1 ∈ fmla" and "χ2 ∈ fmla"
shows "prv (imp (imp φ1 χ1) (imp (imp φ2 χ2) (imp φ1 (imp φ2 (cnj χ1 χ2)))))"
proof-
have "prv (imp (imp φ1 χ1) (imp (imp φ2 χ2) (imp (cnj φ1 φ2) (cnj χ1 χ2))))"
using prv_cnj_imp_mono[of φ1 φ2  χ1 χ2] assms by auto
hence "prv (imp (imp φ1 χ1) (imp (cnj φ1 φ2) (imp (imp φ2 χ2) (cnj χ1 χ2))))"
by (metis (no_types, lifting) assms cnj imp prv_imp_imp_com prv_prv_imp_trans)
hence "prv (imp (imp φ1 χ1) (imp φ1 (imp φ2 (imp (imp φ2 χ2) (cnj χ1 χ2)))))"
using prv_imp_cnj_imp prv_imp_mp prv_imp_trans2
by (metis (mono_tags) assms cnj prv_prv_imp_trans imp)
hence 1: "prv (imp (imp φ1 χ1) (imp φ1 (imp (imp φ2 χ2) (imp φ2  (cnj χ1 χ2)))))"
using prv_cnj_imp prv_imp_cnjR prv_imp_mp prv_imp_trans1
by (metis (no_types) assms cnj prv_cnj_imp_monoR prv_prv_imp_trans prv_imp_imp_triv imp)
thus ?thesis
by (metis (no_types, lifting) assms cnj imp prv_prv_imp_trans prv_imp_imp_com)
qed

lemma prv_imp_cnj5:
assumes "φ1 ∈ fmla" and "φ2 ∈ fmla" and "χ1 ∈ fmla" and "χ2 ∈ fmla"
assumes "prv (imp φ1 χ1)" and "prv (imp φ2 χ2)"
shows "prv (imp φ1 (imp φ2 (cnj χ1 χ2)))"
by (simp add: assms prv_cnj_imp prv_cnj_mono)

text ‹Properties of formula equivalence:›

lemma prv_eqv_imp:
assumes "φ ∈ fmla" and "χ ∈ fmla"
shows "prv (imp (eqv φ χ) (eqv χ φ))"
by (simp add: assms prv_imp_cnj prv_imp_cnjL prv_imp_cnjR eqv_def)

lemma prv_eqv_eqv:
assumes "φ ∈ fmla" and "χ ∈ fmla"
shows "prv (eqv (eqv φ χ) (eqv χ φ))"
using assms prv_cnjI prv_eqv_imp eqv_def by auto

lemma prv_imp_eqvEL:
"φ1 ∈ fmla ⟹ φ2 ∈ fmla ⟹ prv (eqv φ1 φ2) ⟹ prv (imp φ1 φ2)"
unfolding eqv_def by (meson cnj imp prv_imp_cnjL prv_imp_mp)

lemma prv_imp_eqvER:
"φ1 ∈ fmla ⟹ φ2 ∈ fmla ⟹ prv (eqv φ1 φ2) ⟹ prv (imp φ2 φ1)"
unfolding eqv_def by (meson cnj imp prv_imp_cnjR prv_imp_mp)

lemma prv_eqv_imp_trans:
assumes "φ ∈ fmla" and "χ ∈ fmla" and "ψ ∈ fmla"
shows "prv (imp (eqv φ χ) (imp (eqv χ ψ) (eqv φ ψ)))"
proof-
have "prv (imp (eqv φ χ) (imp (imp χ ψ) (imp φ ψ)))"
using assms prv_imp_cnjL prv_imp_mp prv_imp_trans2 eqv_def
by (metis prv_imp_cnj3L eqv imp)
hence "prv (imp (eqv φ χ) (imp (eqv χ ψ) (imp φ ψ)))"
using prv_imp_cnjL prv_imp_mp prv_imp_trans2 eqv_def
by (metis (no_types) assms prv_imp_cnj3L prv_imp_com eqv imp)
hence 1: "prv (imp (cnj (eqv φ χ) (eqv χ ψ)) (imp φ ψ))"
using prv_cnj_imp_monoR2
by (simp add: assms(1) assms(2) assms(3))
have "prv (imp (eqv φ χ) (imp (imp ψ χ) (imp ψ φ)))"
using prv_imp_cnjR prv_imp_mp prv_imp_trans1 eqv_def
by (metis assms prv_cnj_imp_monoR2 prv_imp_triv imp)
hence "prv (imp (eqv φ χ) (imp (eqv χ ψ) (imp ψ φ)))"
by (metis assms cnj eqv_def imp prv_imp_cnj3R prv_prv_imp_trans)
hence 2: "prv (imp (cnj (eqv φ χ) (eqv χ ψ)) (imp ψ φ))"
using prv_cnj_imp_monoR2
by (metis (no_types, lifting) assms eqv imp)
have "prv (imp (cnj (eqv φ χ) (eqv χ ψ)) (eqv φ ψ))"
using 1 2  using assms prv_imp_cnj by (auto simp: eqv_def[of φ ψ])
thus ?thesis
qed

lemma prv_eqv_cnj_trans:
assumes "φ ∈ fmla" and "χ ∈ fmla" and "ψ ∈ fmla"
shows "prv (imp (cnj (eqv φ χ) (eqv χ ψ)) (eqv φ ψ))"
by (simp add: assms prv_eqv_imp_trans prv_cnj_imp_monoR2)

lemma prv_eqvI:
assumes "φ ∈ fmla" and "χ ∈ fmla"
assumes "prv (imp φ χ)" and "prv (imp χ φ)"
shows "prv (eqv φ χ)"
by (simp add: assms eqv_def prv_cnjI)

text ‹Formula equivalence is a congruence (i.e., an equivalence that
is compatible with the other connectives):›

lemma prv_eqv_refl: "φ ∈ fmla ⟹ prv (eqv φ φ)"
by (simp add: prv_cnjI prv_imp_refl eqv_def)

lemma prv_eqv_sym:
assumes "φ ∈ fmla" and "χ ∈ fmla"
shows "prv (eqv φ χ) ⟹ prv (eqv χ φ)"
using assms prv_cnjI prv_imp_cnjL prv_imp_cnjR prv_imp_mp eqv_def
by (meson prv_eqv_imp eqv)

lemma prv_eqv_trans:
assumes "φ ∈ fmla" and "χ ∈ fmla" and "ψ ∈ fmla"
shows "prv (eqv φ χ) ⟹ prv (eqv χ ψ) ⟹ prv (eqv φ ψ)"
using assms prv_cnjI prv_cnj_imp_monoR2 prv_imp_mp prv_imp_trans1 prv_imp_imp_triv eqv_def
by (metis prv_prv_imp_trans prv_imp_cnjL prv_imp_cnjR eqv imp)

lemma imp_imp_compat_eqvL:
assumes "φ1 ∈ fmla" and "φ2 ∈ fmla" and "χ ∈ fmla"
shows "prv (imp (eqv φ1 φ2) (eqv (imp φ1 χ) (imp φ2 χ)))"
proof -
have f: "prv (imp (eqv φ1 φ2) (eqv (imp φ1 χ) (imp φ2 χ)))"
if "prv (imp (eqv φ1 φ2) (imp (imp φ2 χ) (imp φ1 χ)))" "prv (imp (eqv φ1 φ2) (imp (imp φ1 χ) (imp φ2 χ)))"
using assms that prv_imp_cnj by (auto simp: eqv_def)
moreover have "(prv (imp (eqv φ1 φ2) (imp φ1 φ2)) ∧ prv (imp (eqv φ1 φ2) (imp φ2 φ1)))"
by (simp add: assms eqv_def prv_imp_cnjL prv_imp_cnjR)
ultimately show ?thesis
by (metis (no_types) assms eqv imp prv_imp_trans2 prv_prv_imp_trans)
qed

lemma imp_imp_compat_eqvR:
assumes "φ ∈ fmla" and "χ1 ∈ fmla" and "χ2 ∈ fmla"
shows "prv (imp (eqv χ1 χ2) (eqv (imp φ χ1) (imp φ χ2)))"
by (simp add: assms prv_cnj_mono prv_imp_trans1 eqv_def)

lemma imp_imp_compat_eqv:
assumes "φ1 ∈ fmla" and "φ2 ∈ fmla" and "χ1 ∈ fmla" and "χ2 ∈ fmla"
shows "prv (imp (eqv φ1 φ2) (imp (eqv χ1 χ2) (eqv (imp φ1 χ1) (imp φ2 χ2))))"
proof-
have "prv (imp (eqv φ1 φ2) (imp (eqv χ1 χ2) (cnj (eqv (imp φ1 χ1) (imp φ2 χ1))
(eqv (imp φ2 χ1) (imp φ2 χ2)))))"
using prv_imp_cnj5
[OF _ _ _ _ imp_imp_compat_eqvL[of φ1 φ2 χ1] imp_imp_compat_eqvR[of φ2 χ1 χ2]] assms by auto
hence "prv (imp (cnj (eqv φ1 φ2) (eqv χ1 χ2)) (cnj (eqv (imp φ1 χ1) (imp φ2 χ1))
(eqv (imp φ2 χ1) (imp φ2 χ2))))"
hence "prv (imp (cnj (eqv φ1 φ2) (eqv χ1 χ2)) (eqv (imp φ1 χ1) (imp φ2 χ2)))"
using assms prv_eqv_cnj_trans[of "imp φ1 χ1" "imp φ2 χ1" "imp φ2 χ2"]
using prv_imp_mp prv_imp_trans2
by (metis (no_types) cnj prv_prv_imp_trans eqv imp)
thus ?thesis using assms prv_cnj_imp by auto
qed

lemma imp_compat_eqvL:
assumes "φ1 ∈ fmla" and "φ2 ∈ fmla" and "χ ∈ fmla"
assumes "prv (eqv φ1 φ2)"
shows "prv (eqv (imp φ1 χ) (imp φ2 χ))"
using assms prv_imp_mp imp_imp_compat_eqvL by (meson eqv imp)

lemma imp_compat_eqvR:
assumes "φ ∈ fmla" and "χ1 ∈ fmla" and "χ2 ∈ fmla"
assumes "prv (eqv χ1 χ2)"
shows "prv (eqv (imp φ χ1) (imp φ χ2))"
using assms prv_imp_mp imp_imp_compat_eqvR by (meson eqv imp)

lemma imp_compat_eqv:
assumes "φ1 ∈ fmla" and "φ2 ∈ fmla" and "χ1 ∈ fmla" and "χ2 ∈ fmla"
assumes "prv (eqv φ1 φ2)" and "prv (eqv χ1 χ2)"
shows "prv (eqv (imp φ1 χ1) (imp φ2 χ2))"
using assms prv_imp_mp imp_imp_compat_eqv by (metis eqv imp)

(*  *)

lemma imp_cnj_compat_eqvL:
assumes "φ1 ∈ fmla" and "φ2 ∈ fmla" and "χ ∈ fmla"
shows "prv (imp (eqv φ1 φ2) (eqv (cnj φ1 χ) (cnj φ2 χ)))"
proof -
have "prv (imp (imp (imp φ2 φ1) (imp (cnj φ2 χ) (cnj φ1 χ)))
(imp (cnj (imp φ1 φ2) (imp φ2 φ1)) (cnj (imp (cnj φ1 χ) (cnj φ2 χ))
(imp (cnj φ2 χ) (cnj φ1 χ)))))"
by (metis (no_types) imp cnj assms prv_imp_mp assms prv_cnj_imp_mono prv_imp_com prv_imp_refl)
then show ?thesis
by (metis (no_types) imp cnj assms prv_imp_mp assms eqv_def prv_cnj_imp_mono prv_imp_com prv_imp_refl)
qed

lemma imp_cnj_compat_eqvR:
assumes "φ ∈ fmla" and "χ1 ∈ fmla" and "χ2 ∈ fmla"
shows "prv (imp (eqv χ1 χ2) (eqv (cnj φ χ1) (cnj φ χ2)))"
by (simp add: assms prv_cnj_mono prv_imp_cnj3R prv_imp_cnj4 prv_imp_cnjL prv_imp_triv eqv_def)

lemma imp_cnj_compat_eqv:
assumes "φ1 ∈ fmla" and "φ2 ∈ fmla" and "χ1 ∈ fmla" and "χ2 ∈ fmla"
shows "prv (imp (eqv φ1 φ2) (imp (eqv χ1 χ2) (eqv (cnj φ1 χ1) (cnj φ2 χ2))))"
proof-
have "prv (imp (eqv φ1 φ2) (imp (eqv χ1 χ2) (cnj (eqv (cnj φ1 χ1) (cnj φ2 χ1))
(eqv (cnj φ2 χ1) (cnj φ2 χ2)))))"
using prv_imp_cnj5
[OF _ _ _ _ imp_cnj_compat_eqvL[of φ1 φ2 χ1] imp_cnj_compat_eqvR[of φ2 χ1 χ2]] assms by auto
hence "prv (imp (cnj (eqv φ1 φ2) (eqv χ1 χ2)) (cnj (eqv (cnj φ1 χ1) (cnj φ2 χ1))
(eqv (cnj φ2 χ1) (cnj φ2 χ2))))"
hence "prv (imp (cnj (eqv φ1 φ2) (eqv χ1 χ2)) (eqv (cnj φ1 χ1) (cnj φ2 χ2)))"
using assms prv_eqv_cnj_trans[of "cnj φ1 χ1" "cnj φ2 χ1" "cnj φ2 χ2"]
using prv_imp_mp prv_imp_trans2
by (metis (no_types) cnj prv_prv_imp_trans eqv)
thus ?thesis using assms prv_cnj_imp by auto
qed

lemma cnj_compat_eqvL:
assumes "φ1 ∈ fmla" and "φ2 ∈ fmla" and "χ ∈ fmla"
assumes "prv (eqv φ1 φ2)"
shows "prv (eqv (cnj φ1 χ) (cnj φ2 χ))"
using assms prv_imp_mp imp_cnj_compat_eqvL by (meson eqv cnj)

lemma cnj_compat_eqvR:
assumes "φ ∈ fmla" and "χ1 ∈ fmla" and "χ2 ∈ fmla"
assumes "prv (eqv χ1 χ2)"
shows "prv (eqv (cnj φ χ1) (cnj φ χ2))"
using assms prv_imp_mp imp_cnj_compat_eqvR by (meson eqv cnj)

lemma cnj_compat_eqv:
assumes "φ1 ∈ fmla" and "φ2 ∈ fmla" and "χ1 ∈ fmla" and "χ2 ∈ fmla"
assumes "prv (eqv φ1 φ2)" and "prv (eqv χ1 χ2)"
shows "prv (eqv (cnj φ1 χ1) (cnj φ2 χ2))"
using assms prv_imp_mp imp_cnj_compat_eqv by (metis eqv imp cnj)

lemma prv_eqv_prv:
assumes "φ ∈ fmla" and "χ ∈ fmla"
assumes "prv φ" and "prv (eqv φ χ)"
shows "prv χ"
by (metis assms prv_imp_cnjL prv_imp_mp eqv eqv_def imp)

lemma prv_eqv_prv_rev:
assumes "φ ∈ fmla" and "χ ∈ fmla"
assumes "prv φ" and "prv (eqv χ φ)"
shows "prv χ"
using assms prv_eqv_prv prv_eqv_sym by blast

lemma prv_imp_eqv_transi:
assumes "φ ∈ fmla" and "χ1 ∈ fmla" and "χ2 ∈ fmla"
assumes "prv (imp φ χ1)" and "prv (eqv χ1 χ2)"
shows "prv (imp φ χ2)"
by (meson assms imp imp_compat_eqvR prv_eqv_prv)

lemma prv_imp_eqv_transi_rev:
assumes "φ ∈ fmla" and "χ1 ∈ fmla" and "χ2 ∈ fmla"
assumes "prv (imp φ χ2)" and "prv (eqv χ1 χ2)"
shows "prv (imp φ χ1)"
by (meson assms prv_eqv_sym prv_imp_eqv_transi)

lemma prv_eqv_imp_transi:
assumes "φ1 ∈ fmla" and "φ2 ∈ fmla" and "χ ∈ fmla"
assumes "prv (eqv φ1 φ2)" and "prv (imp φ2 χ)"
shows "prv (imp φ1 χ)"
by (meson assms prv_imp_eqv_transi prv_imp_refl prv_prv_imp_trans)

lemma prv_eqv_imp_transi_rev:
assumes "φ1 ∈ fmla" and "φ2 ∈ fmla" and "χ ∈ fmla"
assumes "prv (eqv φ1 φ2)" and "prv (imp φ1 χ)"
shows "prv (imp φ2 χ)"
by (meson assms prv_eqv_imp_transi prv_eqv_sym)

lemma prv_imp_monoL: "φ ∈ fmla ⟹ χ ∈ fmla ⟹ ψ ∈ fmla ⟹
prv (imp χ ψ) ⟹ prv (imp (imp φ χ) (imp φ ψ))"
by (meson imp prv_imp_mp prv_imp_trans1)

lemma prv_imp_monoR: "φ ∈ fmla ⟹ χ ∈ fmla ⟹ ψ ∈ fmla ⟹
prv (imp ψ χ) ⟹ prv (imp (imp χ φ) (imp ψ φ))"
by (meson imp prv_imp_mp prv_imp_trans2)

text ‹More properties involving conjunction:›

lemma prv_cnj_com_imp:
assumes φ[simp]: "φ ∈ fmla" and χ[simp]: "χ ∈ fmla"
shows "prv (imp (cnj φ χ) (cnj χ φ))"
by (simp add: prv_imp_cnj prv_imp_cnjL prv_imp_cnjR)

lemma prv_cnj_com:
assumes φ[simp]: "φ ∈ fmla" and χ[simp]: "χ ∈ fmla"
shows "prv (eqv (cnj φ χ) (cnj χ φ))"

lemma prv_cnj_assoc_imp1:
assumes φ[simp]: "φ ∈ fmla" and χ[simp]: "χ ∈ fmla" and ψ[simp]: "ψ ∈ fmla"
shows "prv (imp (cnj φ (cnj χ ψ)) (cnj (cnj φ χ) ψ))"
by (simp add: prv_cnj_imp_monoR2 prv_imp_cnj prv_imp_cnjL prv_imp_cnjR prv_imp_triv)

lemma prv_cnj_assoc_imp2:
assumes φ[simp]: "φ ∈ fmla" and χ[simp]: "χ ∈ fmla" and ψ[simp]: "ψ ∈ fmla"
shows "prv (imp (cnj (cnj φ χ) ψ) (cnj φ (cnj χ ψ)))"
proof -
have "prv (imp (cnj φ χ) (imp ψ φ)) ∧ cnj χ ψ ∈ fmla ∧ cnj φ χ ∈ fmla"
by (meson χ φ ψ cnj imp prv_cnj_imp_monoR2 prv_imp_imp_triv prv_prv_imp_trans)
then show ?thesis
using χ φ ψ cnj imp prv_cnj_imp_monoR2 prv_imp_cnj4 prv_imp_cnjI prv_imp_triv by presburger
qed

lemma prv_cnj_assoc:
assumes φ[simp]: "φ ∈ fmla" and χ[simp]: "χ ∈ fmla" and ψ[simp]: "ψ ∈ fmla"
shows "prv (eqv (cnj φ (cnj χ ψ)) (cnj (cnj φ χ) ψ))"
by (simp add: prv_cnj_assoc_imp1 prv_cnj_assoc_imp2 prv_eqvI)

lemma prv_cnj_com_imp3:
assumes "φ1 ∈ fmla" "φ2 ∈ fmla" "φ3 ∈ fmla"
shows "prv (imp (cnj φ1 (cnj φ2 φ3))
(cnj φ2 (cnj φ1 φ3)))"
by (simp add: assms prv_cnj_imp_monoR2 prv_imp_cnj prv_imp_cnjL prv_imp_refl prv_imp_triv)

subsection ‹Properties involving quantifiers›

text ‹Fundamental properties:›

lemma prv_allE:
assumes "x ∈ var" and "φ ∈ fmla" and "t ∈ trm"
shows "prv (all x φ) ⟹ prv (subst φ t x)"
using assms prv_all_inst prv_imp_mp by (meson subst all)

lemma prv_exiI:
assumes "x ∈ var" and "φ ∈ fmla" and "t ∈ trm"
shows "prv (subst φ t x) ⟹ prv (exi x φ)"
using assms prv_exi_inst prv_imp_mp by (meson subst exi)

lemma prv_imp_imp_exi:
assumes "x ∈ var" and "φ ∈ fmla" and "χ ∈ fmla"
assumes "x ∉ Fvars φ"
shows "prv (imp (exi x (imp φ χ)) (imp φ (exi x χ)))"
using assms imp exi Fvars_exi Fvars_imp Un_iff assms prv_exi_imp_gen prv_exi_inst prv_imp_mp
prv_imp_trans1 member_remove remove_def subst_same_Var by (metis (full_types) Var)

lemma prv_imp_exi:
assumes "x ∈ var" and "φ ∈ fmla" and "χ ∈ fmla"
shows "x ∉ Fvars φ ⟹ prv (exi x (imp φ χ)) ⟹ prv (imp φ (exi x χ))"
using assms prv_imp_imp_exi prv_imp_mp by (meson exi imp)

lemma prv_exi_imp:
assumes x: "x ∈ var" and "φ ∈ fmla" and "χ ∈ fmla"
assumes "x ∉ Fvars χ" and d: "prv (all x (imp φ χ))"
shows "prv (imp (exi x φ) χ)"
proof-
have "prv (imp φ χ)" using prv_allE[of x _ "Var x", of "imp φ χ"] assms by simp
thus ?thesis using assms prv_exi_imp_gen by blast
qed

lemma prv_all_imp:
assumes x: "x ∈ var" and "φ ∈ fmla" and "χ ∈ fmla"
assumes "x ∉ Fvars φ" and "prv (all x (imp φ χ))"
shows "prv (imp φ (all x χ))"
proof-
have "prv (imp φ χ)" using prv_allE[of x _ "Var x", of "imp φ χ"] assms by simp
thus ?thesis using assms prv_all_imp_gen by blast
qed

lemma prv_exi_inst_same:
assumes "φ ∈ fmla" "χ ∈ fmla" "x ∈ var"
shows "prv (imp φ (exi x φ))"
proof-
have 0: "φ = subst φ (Var x) x" using assms by simp
show ?thesis
apply(subst 0)
using assms by (intro prv_exi_inst) auto
qed

lemma prv_exi_cong:
assumes "φ ∈ fmla" "χ ∈ fmla" "x ∈ var"
and "prv (imp φ χ)"
shows "prv (imp (exi x φ) (exi x χ))"
proof-
have 0: "prv (imp χ (exi x χ))" using assms prv_exi_inst_same by auto
show ?thesis
using assms apply(intro prv_exi_imp_gen)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal using "0" exi prv_prv_imp_trans by blast .
qed

lemma prv_exi_congW:
assumes "φ ∈ fmla" "χ ∈ fmla" "x ∈ var"
and "prv (imp φ χ)" "prv (exi x φ)"
shows "prv (exi x χ)"
by (meson exi assms prv_exi_cong prv_imp_mp)

lemma prv_all_cong:
assumes "φ ∈ fmla" "χ ∈ fmla" "x ∈ var"
and "prv (imp φ χ)"
shows "prv (imp (all x φ) (all x χ))"
proof-
have 0: "prv (imp (all x φ) χ)" using assms
by (metis Var all prv_all_inst prv_prv_imp_trans subst_same_Var)
show ?thesis by (simp add: "0" assms prv_all_imp_gen)
qed

lemma prv_all_congW:
assumes "φ ∈ fmla" "χ ∈ fmla" "x ∈ var"
and "prv (imp φ χ)" "prv (all x φ)"
shows "prv (all x χ)"
by (meson all assms prv_all_cong prv_imp_mp)

text ‹Quantifiers versus free variables and substitution:›

lemma exists_no_Fvars: "∃ φ. φ ∈ fmla ∧ prv φ ∧ Fvars φ = {}"
proof-
obtain n where [simp]: "n ∈ num" using numNE by blast
show ?thesis
by (intro exI[of _ "imp (eql n n) (eql n n)"]) (simp add: prv_imp_refl)
qed

lemma prv_all_gen:
assumes "x ∈ var" and "φ ∈ fmla"
assumes "prv φ" shows "prv (all x φ)"
using assms prv_all_imp_gen prv_imp_mp prv_imp_triv exists_no_Fvars by blast

lemma all_subst_rename_prv:
"φ ∈ fmla ⟹ x ∈ var ⟹ y ∈ var ⟹
y ∉ Fvars φ ⟹ prv (all x φ) ⟹ prv (all y (subst φ (Var y) x))"

lemma allE_id:
assumes "y ∈ var" and "φ ∈ fmla"
assumes "prv (all y φ)"
shows "prv φ"
using assms prv_allE by (metis Var subst_same_Var)

lemma prv_subst:
assumes "x ∈ var" and "φ ∈ fmla" and "t ∈ trm"
shows "prv φ ⟹ prv (subst φ t x)"
by (simp add: assms prv_allE prv_all_gen)

lemma prv_rawpsubst:
assumes "φ ∈ fmla" and "snd  (set txs) ⊆ var" and "fst  (set txs) ⊆ trm"
and "prv φ"
shows "prv (rawpsubst φ txs)"
using assms apply (induct txs arbitrary: φ)
subgoal by auto
subgoal for tx txs φ by (cases tx) (auto