chapter ‹Syntax› (*<*) theory Syntax imports Prelim begin (*>*) section ‹Generic Syntax› text ‹We develop some generic (meta-)axioms for syntax and substitution. We only assume that the syntax of our logic has notions of variable, term and formula, which \emph{include} subsets of "numeric" variables, terms and formulas, the latter being endowed with notions of free variables and substitution subject to some natural properties.› locale Generic_Syntax = fixes var :: "'var set" ― ‹numeric variables (i.e., variables ranging over numbers)› and trm :: "'trm set" ― ‹numeric trms, which include the numeric variables› and fmla :: "'fmla set" ― ‹numeric formulas› and Var :: "'var ⇒ 'trm" ― ‹trms include at least the variables› and FvarsT :: "'trm ⇒ 'var set" ― ‹free variables for trms› and substT :: "'trm ⇒ 'trm ⇒ 'var ⇒ 'trm" ― ‹substitution for trms› and Fvars :: "'fmla ⇒ 'var set" ― ‹free variables for formulas› and subst :: "'fmla ⇒ 'trm ⇒ 'var ⇒ 'fmla" ― ‹substitution for formulas› assumes infinite_var: "infinite var" ― ‹the variables are assumed infinite› and ― ‹Assumptions about the infrastructure (free vars, substitution and the embedding of variables into trms. NB: We need fewer assumptions for trm substitution than for formula substitution!› Var[simp,intro!]: "⋀x. x ∈ var ⟹ Var x ∈ trm" and inj_Var[simp]: "⋀ x y. x ∈ var ⟹ y ∈ var ⟹ (Var x = Var y ⟷ x = y)" and finite_FvarsT: "⋀ t. t ∈ trm ⟹ finite (FvarsT t)" and FvarsT: "⋀t. t ∈ trm ⟹ FvarsT t ⊆ var" and substT[simp,intro]: "⋀t1 t x. t1 ∈ trm ⟹ t ∈ trm ⟹ x ∈ var ⟹ substT t1 t x ∈ trm" and FvarsT_Var[simp]: "⋀ x. x ∈ var ⟹ FvarsT (Var x) = {x}" and substT_Var[simp]: "⋀ x t y. x ∈ var ⟹ y ∈ var ⟹ t ∈ trm ⟹ substT (Var x) t y = (if x = y then t else Var x)" and substT_notIn[simp]: "⋀t1 t2 x. x ∈ var ⟹ t1 ∈ trm ⟹ t2 ∈ trm ⟹ x ∉ FvarsT t1 ⟹ substT t1 t2 x = t1" and ― ‹Assumptions about the infrastructure (free vars and substitution) on formulas› finite_Fvars: "⋀ φ. φ ∈ fmla ⟹ finite (Fvars φ)" and Fvars: "⋀φ. φ ∈ fmla ⟹ Fvars φ ⊆ var" and subst[simp,intro]: "⋀φ t x. φ ∈ fmla ⟹ t ∈ trm ⟹ x ∈ var ⟹ subst φ t x ∈ fmla" and Fvars_subst_in: "⋀ φ t x. φ ∈ fmla ⟹ t ∈ trm ⟹ x ∈ var ⟹ x ∈ Fvars φ ⟹ Fvars (subst φ t x) = Fvars φ - {x} ∪ FvarsT t" and subst_compose_eq_or: "⋀ φ t1 t2 x1 x2. φ ∈ fmla ⟹ t1 ∈ trm ⟹ t2 ∈ trm ⟹ x1 ∈ var ⟹ x2 ∈ var ⟹ x1 = x2 ∨ x2 ∉ Fvars φ ⟹ subst (subst φ t1 x1) t2 x2 = subst φ (substT t1 t2 x2) x1" and subst_compose_diff: "⋀ φ t1 t2 x1 x2. φ ∈ fmla ⟹ t1 ∈ trm ⟹ t2 ∈ trm ⟹ x1 ∈ var ⟹ x2 ∈ var ⟹ x1 ≠ x2 ⟹ x1 ∉ FvarsT t2 ⟹ subst (subst φ t1 x1) t2 x2 = subst (subst φ t2 x2) (substT t1 t2 x2) x1" and subst_same_Var[simp]: "⋀ φ x. φ ∈ fmla ⟹ x ∈ var ⟹ subst φ (Var x) x = φ" and subst_notIn[simp]: "⋀ x φ t. φ ∈ fmla ⟹ t ∈ trm ⟹ x ∈ var ⟹ x ∉ Fvars φ ⟹ subst φ t x = φ" begin lemma var_NE: "var ≠ {}" using infinite_var by auto lemma Var_injD: "Var x = Var y ⟹ x ∈ var ⟹ y ∈ var ⟹ x = y" by auto lemma FvarsT_VarD: "x ∈ FvarsT (Var y) ⟹ y ∈ var ⟹ x = y" by auto lemma FvarsT': "t ∈ trm ⟹ x ∈ FvarsT t ⟹ x ∈ var" using FvarsT by auto lemma Fvars': "φ ∈ fmla ⟹ x ∈ Fvars φ ⟹ x ∈ var" using Fvars by auto lemma Fvars_subst[simp]: "φ ∈ fmla ⟹ t ∈ trm ⟹ x ∈ var ⟹ Fvars (subst φ t x) = (Fvars φ - {x}) ∪ (if x ∈ Fvars φ then FvarsT t else {})" by (simp add: Fvars_subst_in) lemma in_Fvars_substD: "y ∈ Fvars (subst φ t x) ⟹ φ ∈ fmla ⟹ t ∈ trm ⟹ x ∈ var ⟹ y ∈ (Fvars φ - {x}) ∪ (if x ∈ Fvars φ then FvarsT t else {})" using Fvars_subst by auto lemma inj_on_Var: "inj_on Var var" using inj_Var unfolding inj_on_def by auto lemma subst_compose_same: "⋀ φ t1 t2 x. φ ∈ fmla ⟹ t1 ∈ trm ⟹ t2 ∈ trm ⟹ x ∈ var ⟹ subst (subst φ t1 x) t2 x = subst φ (substT t1 t2 x) x" using subst_compose_eq_or by blast lemma subst_subst[simp]: assumes φ[simp]: "φ ∈ fmla" and t[simp]:"t ∈ trm" and x[simp]:"x ∈ var" and y[simp]:"y ∈ var" assumes yy: "x ≠ y" "y ∉ Fvars φ" shows "subst (subst φ (Var y) x) t y = subst φ t x" using subst_compose_eq_or[OF φ _ t x y, of "Var y"] using subst_notIn yy by simp lemma subst_comp: "⋀ x y φ t. φ ∈ fmla ⟹ t ∈ trm ⟹ x ∈ var ⟹ y ∈ var ⟹ x ≠ y ⟹ y ∉ FvarsT t ⟹ subst (subst φ (Var x) y) t x = subst (subst φ t x) t y" by (simp add: subst_compose_diff) lemma exists_nat_var: "∃ f::nat⇒'var. inj f ∧ range f ⊆ var" by (simp add: infinite_countable_subset infinite_var) definition Variable :: "nat ⇒ 'var" where "Variable = (SOME f. inj f ∧ range f ⊆ var)" lemma Variable_inj_var: "inj Variable ∧ range Variable ⊆ var" unfolding Variable_def using someI_ex[OF exists_nat_var] . lemma inj_Variable[simp]: "⋀ i j. Variable i = Variable j ⟷ i = j" and Variable[simp,intro!]: "⋀i. Variable i ∈ var" using Variable_inj_var image_def unfolding inj_def by auto text ‹Convenient notations for some variables We reserve the first 10 indexes for any special variables we may wish to consider later.› abbreviation xx where "xx ≡ Variable 10" abbreviation yy where "yy ≡ Variable 11" abbreviation zz where "zz ≡ Variable 12" abbreviation xx' where "xx' ≡ Variable 13" abbreviation yy' where "yy' ≡ Variable 14" abbreviation zz' where "zz' ≡ Variable 15" lemma xx: "xx ∈ var" and yy: "yy ∈ var" and zz: "zz ∈ var" and xx': "xx' ∈ var" and yy': "yy' ∈ var" and zz': "zz' ∈ var" by auto lemma vars_distinct[simp]: "xx ≠ yy" "yy ≠ xx" "xx ≠ zz" "zz ≠ xx" "xx ≠ xx'" "xx' ≠ xx" "xx ≠ yy'" "yy' ≠ xx" "xx ≠ zz'" "zz' ≠ xx" "yy ≠ zz" "zz ≠ yy" "yy ≠ xx'" "xx' ≠ yy" "yy ≠ yy'" "yy' ≠ yy" "yy ≠ zz'" "zz' ≠ yy" "zz ≠ xx'" "xx' ≠ zz" "zz ≠ yy'" "yy' ≠ zz" "zz ≠ zz'" "zz' ≠ zz" "xx' ≠ yy'" "yy' ≠ xx'" "xx' ≠ zz'" "zz' ≠ xx'" "yy' ≠ zz'" "zz' ≠ yy'" by auto subsection ‹Instance Operator› definition inst :: "'fmla ⇒ 'trm ⇒ 'fmla" where "inst φ t = subst φ t xx" lemma inst[simp]: "φ ∈ fmla ⟹ t ∈ trm ⟹ inst φ t ∈ fmla" unfolding inst_def by auto definition getFresh :: "'var set ⇒ 'var" where "getFresh V = (SOME x. x ∈ var ∧ x ∉ V)" lemma getFresh: "finite V ⟹ getFresh V ∈ var ∧ getFresh V ∉ V" by (metis (no_types, lifting) finite_subset getFresh_def infinite_var someI_ex subsetI) definition getFr :: "'var list ⇒ 'trm list ⇒ 'fmla list ⇒ 'var" where "getFr xs ts φs = getFresh (set xs ∪ (⋃(FvarsT ` set ts)) ∪ (⋃(Fvars ` set φs)))" lemma getFr_FvarsT_Fvars: assumes "set xs ⊆ var" "set ts ⊆ trm" and "set φs ⊆ fmla" shows "getFr xs ts φs ∈ var ∧ getFr xs ts φs ∉ set xs ∧ (t ∈ set ts ⟶ getFr xs ts φs ∉ FvarsT t) ∧ (φ ∈ set φs ⟶ getFr xs ts φs ∉ Fvars φ)" proof- have "finite (set xs ∪ (⋃(FvarsT ` set ts)) ∪ (⋃(Fvars ` set φs)))" using assms finite_FvarsT finite_Fvars by auto from getFresh[OF this] show ?thesis using assms unfolding getFr_def by auto qed lemma getFr[simp,intro]: assumes "set xs ⊆ var" "set ts ⊆ trm" and "set φs ⊆ fmla" shows "getFr xs ts φs ∈ var" using assms getFr_FvarsT_Fvars by auto lemma getFr_var: assumes "set xs ⊆ var" "set ts ⊆ trm" and "set φs ⊆ fmla" and "t ∈ set ts" shows "getFr xs ts φs ∉ set xs" using assms getFr_FvarsT_Fvars by auto lemma getFr_FvarsT: assumes "set xs ⊆ var" "set ts ⊆ trm" and "set φs ⊆ fmla" and "t ∈ set ts" shows "getFr xs ts φs ∉ FvarsT t" using assms getFr_FvarsT_Fvars by auto lemma getFr_Fvars: assumes "set xs ⊆ var" "set ts ⊆ trm" and "set φs ⊆ fmla" and "φ ∈ set φs" shows "getFr xs ts φs ∉ Fvars φ" using assms getFr_FvarsT_Fvars by auto subsection ‹Fresh Variables› fun getFreshN :: "'var set ⇒ nat ⇒ 'var list" where "getFreshN V 0 = []" | "getFreshN V (Suc n) = (let u = getFresh V in u # getFreshN (insert u V) n)" lemma getFreshN: "finite V ⟹ set (getFreshN V n) ⊆ var ∧ set (getFreshN V n) ∩ V = {} ∧ length (getFreshN V n) = n ∧ distinct (getFreshN V n)" by (induct n arbitrary: V) (auto simp: getFresh Let_def) definition getFrN :: "'var list ⇒ 'trm list ⇒ 'fmla list ⇒ nat ⇒ 'var list" where "getFrN xs ts φs n = getFreshN (set xs ∪ (⋃(FvarsT ` set ts)) ∪ (⋃(Fvars ` set φs))) n" lemma getFrN_FvarsT_Fvars: assumes "set xs ⊆ var" "set ts ⊆ trm" and "set φs ⊆ fmla" shows "set (getFrN xs ts φs n) ⊆ var ∧ set (getFrN xs ts φs n) ∩ set xs = {} ∧ (t ∈ set ts ⟶ set (getFrN xs ts φs n) ∩ FvarsT t = {}) ∧ (φ ∈ set φs ⟶ set (getFrN xs ts φs n) ∩ Fvars φ = {}) ∧ length (getFrN xs ts φs n) = n ∧ distinct (getFrN xs ts φs n)" proof- have "finite (set xs ∪ (⋃(FvarsT ` set ts)) ∪ (⋃(Fvars ` set φs)))" using assms finite_FvarsT finite_Fvars by auto from getFreshN[OF this] show ?thesis using assms unfolding getFrN_def by auto qed lemma getFrN[simp,intro]: assumes "set xs ⊆ var" "set ts ⊆ trm" and "set φs ⊆ fmla" shows "set (getFrN xs ts φs n) ⊆ var" using assms getFrN_FvarsT_Fvars by auto lemma getFrN_var: assumes "set xs ⊆ var" "set ts ⊆ trm" and "set φs ⊆ fmla" and "t ∈ set ts" shows "set (getFrN xs ts φs n) ∩ set xs = {}" using assms getFrN_FvarsT_Fvars by auto lemma getFrN_FvarsT: assumes "set xs ⊆ var" "set ts ⊆ trm" and "set φs ⊆ fmla" and "t ∈ set ts" shows "set (getFrN xs ts φs n) ∩ FvarsT t = {}" using assms getFrN_FvarsT_Fvars by auto lemma getFrN_Fvars: assumes "set xs ⊆ var" "set ts ⊆ trm" and "set φs ⊆ fmla" and "φ ∈ set φs" shows "set (getFrN xs ts φs n) ∩ Fvars φ = {}" using assms getFrN_FvarsT_Fvars by auto lemma getFrN_length: assumes "set xs ⊆ var" "set ts ⊆ trm" and "set φs ⊆ fmla" shows "length (getFrN xs ts φs n) = n" using assms getFrN_FvarsT_Fvars by auto lemma getFrN_distinct[simp,intro]: assumes "set xs ⊆ var" "set ts ⊆ trm" and "set φs ⊆ fmla" shows "distinct (getFrN xs ts φs n)" using assms getFrN_FvarsT_Fvars by auto subsection ‹Parallel Term Substitution› fun rawpsubstT :: "'trm ⇒ ('trm × 'var) list ⇒ 'trm" where "rawpsubstT t [] = t" | "rawpsubstT t ((t1,x1) # txs) = rawpsubstT (substT t t1 x1) txs" lemma rawpsubstT[simp]: assumes "t ∈ trm" and "snd ` (set txs) ⊆ var" and "fst ` (set txs) ⊆ trm" shows "rawpsubstT t txs ∈ trm" using assms by (induct txs arbitrary: t) fastforce+ definition psubstT :: "'trm ⇒ ('trm × 'var) list ⇒ 'trm" where "psubstT t txs = (let xs = map snd txs; ts = map fst txs; us = getFrN xs (t # ts) [] (length xs) in rawpsubstT (rawpsubstT t (zip (map Var us) xs)) (zip ts us))" text ‹The psubstT versions of the subst axioms.› lemma psubstT[simp,intro]: assumes "t ∈ trm" and "snd ` (set txs) ⊆ var" and "fst ` (set txs) ⊆ trm" shows "psubstT t txs ∈ trm" proof- define us where us: "us = getFrN (map snd txs) (t # map fst txs) [] (length txs)" have us_facts: "set us ⊆ var" "set us ∩ FvarsT t = {}" "set us ∩ ⋃ (FvarsT ` (fst ` (set txs))) = {}" "set us ∩ snd ` (set txs) = {}" "length us = length txs" "distinct us" using assms unfolding us using getFrN_FvarsT[of "map snd txs" "t # map fst txs" "[]" _ "length txs"] getFrN_var[of "map snd txs" "t # map fst txs" "[]" _ "length txs"] getFrN_length[of "map snd txs" "t # map fst txs" "[]" "length txs"] getFrN_distinct[of "map snd txs" "t # map fst txs" "[]" "length txs"] by auto (metis (no_types, opaque_lifting) IntI empty_iff image_iff old.prod.inject surjective_pairing) show ?thesis using assms us_facts unfolding psubstT_def by (force simp: Let_def us[symmetric] dest: set_zip_leftD set_zip_rightD intro!: rawpsubstT) qed lemma rawpsubstT_Var_not[simp]: assumes "x ∈ var" "snd ` (set txs) ⊆ var" "fst ` (set txs) ⊆ trm" and "x ∉ snd ` (set txs)" shows "rawpsubstT (Var x) txs = Var x" using assms by (induct txs) auto lemma psubstT_Var_not[simp]: assumes "x ∈ var" "snd ` (set txs) ⊆ var" "fst ` (set txs) ⊆ trm" and "x ∉ snd ` (set txs)" shows "psubstT (Var x) txs = Var x" proof- define us where us: "us = getFrN (map snd txs) (Var x # map fst txs) [] (length txs)" have us_facts: "set us ⊆ var" "x ∉ set us" "set us ∩ ⋃ (FvarsT ` (fst ` (set txs))) = {}" "set us ∩ snd ` (set txs) = {}" "length us = length txs" using assms unfolding us using getFrN_FvarsT[of "map snd txs" "Var x # map fst txs" "[]" "Var x" "length txs"] getFrN_FvarsT[of "map snd txs" "Var x # map fst txs" "[]" _ "length txs"] getFrN_var[of "map snd txs" "Var x # map fst txs" "[]" "Var x" "length txs"] getFrN_length[of "map snd txs" "Var x # map fst txs" "[]" "length txs"] by (auto simp: set_eq_iff) have [simp]: "rawpsubstT (Var x) (zip (map Var us) (map snd txs)) = Var x" using assms us_facts by(intro rawpsubstT_Var_not) (force dest: set_zip_rightD set_zip_leftD)+ have [simp]: "rawpsubstT (Var x) (zip (map fst txs) us) = Var x" using assms us_facts by(intro rawpsubstT_Var_not) (force dest: set_zip_rightD set_zip_leftD)+ show ?thesis using assms us_facts unfolding psubstT_def by (auto simp: Let_def us[symmetric]) qed lemma rawpsubstT_notIn[simp]: assumes "x ∈ var" "snd ` (set txs) ⊆ var" "fst ` (set txs) ⊆ trm" "t ∈ trm" and "FvarsT t ∩ snd ` (set txs) = {}" shows "rawpsubstT t txs = t" using assms by (induct txs) auto lemma psubstT_notIn[simp]: assumes "x ∈ var" "snd ` (set txs) ⊆ var" "fst ` (set txs) ⊆ trm" "t ∈ trm" and "FvarsT t ∩ snd ` (set txs) = {}" shows "psubstT t txs = t" proof- define us where us: "us = getFrN (map snd txs) (t # map fst txs) [] (length txs)" have us_facts: "set us ⊆ var" "set us ∩ FvarsT t = {}" "set us ∩ ⋃ (FvarsT ` (fst ` (set txs))) = {}" "set us ∩ snd ` (set txs) = {}" "length us = length txs" using assms unfolding us using getFrN_FvarsT[of "map snd txs" "t # map fst txs" "[]" _ "length txs"] getFrN_var[of "map snd txs" "t # map fst txs" "[]" t "length txs"] getFrN_length[of "map snd txs" "t # map fst txs" "[]" "length txs"] by (auto simp: set_eq_iff) have [simp]: "rawpsubstT t (zip (map Var us) (map snd txs)) = t" using assms us_facts by(intro rawpsubstT_notIn) (auto 0 3 dest: set_zip_rightD set_zip_leftD) have [simp]: "rawpsubstT t (zip (map fst txs) us) = t" using assms us_facts by(intro rawpsubstT_notIn) (auto 0 3 dest: set_zip_rightD set_zip_leftD) show ?thesis using assms us_facts unfolding psubstT_def by (auto simp: Let_def us[symmetric]) qed subsection ‹Parallel Formula Substitution› fun rawpsubst :: "'fmla ⇒ ('trm × 'var) list ⇒ 'fmla" where "rawpsubst φ [] = φ" | "rawpsubst φ ((t1,x1) # txs) = rawpsubst (subst φ t1 x1) txs" lemma rawpsubst[simp]: assumes "φ ∈ fmla" and "snd ` (set txs) ⊆ var" and "fst ` (set txs) ⊆ trm" shows "rawpsubst φ txs ∈ fmla" using assms by (induct txs arbitrary: φ) fastforce+ definition psubst :: "'fmla ⇒ ('trm × 'var) list ⇒ 'fmla" where "psubst φ txs = (let xs = map snd txs; ts = map fst txs; us = getFrN xs ts [φ] (length xs) in rawpsubst (rawpsubst φ (zip (map Var us) xs)) (zip ts us))" text ‹The psubst versions of the subst axioms.› lemma psubst[simp,intro]: assumes "φ ∈ fmla" and "snd ` (set txs) ⊆ var" and "fst ` (set txs) ⊆ trm" shows "psubst φ txs ∈ fmla" proof- define us where us: "us = getFrN (map snd txs) (map fst txs) [φ] (length txs)" have us_facts: "set us ⊆ var" "set us ∩ Fvars φ = {}" "set us ∩ ⋃ (FvarsT ` (fst ` (set txs))) = {}" "set us ∩ snd ` (set txs) = {}" "length us = length txs" "distinct us" using assms unfolding us using getFrN_FvarsT[of "map snd txs" "map fst txs" "[φ]" _ "length txs"] getFrN_Fvars[of "map snd txs" "map fst txs" "[φ]" φ "length txs"] getFrN_var[of "map snd txs" "map fst txs" "[φ]" _ "length txs"] getFrN_length[of "map snd txs" "map fst txs" "[φ]" "length txs"] getFrN_distinct[of "map snd txs" "map fst txs" "[φ]" "length txs"] by (auto 8 0 simp: set_eq_iff image_iff Bex_def Ball_def) show ?thesis using assms us_facts unfolding psubst_def by (auto 0 3 simp: Let_def us[symmetric] dest: set_zip_rightD set_zip_leftD intro!: rawpsubst) qed lemma Fvars_rawpsubst_su: assumes "φ ∈ fmla" and "snd ` (set txs) ⊆ var" and "fst ` (set txs) ⊆ trm" shows "Fvars (rawpsubst φ txs) ⊆ (Fvars φ - snd ` (set txs)) ∪ (⋃ {FvarsT t | t x . (t,x) ∈ set txs})" using assms proof(induction txs arbitrary: φ) case (Cons tx txs φ) then obtain t x where tx: "tx = (t,x)" by force have t: "t ∈ trm" and x: "x ∈ var" using Cons.prems unfolding tx by auto define χ where "χ = subst φ t x" have 0: "Fvars χ = Fvars φ - {x} ∪ (if x ∈ Fvars φ then FvarsT t else {})" using Cons.prems unfolding χ_def by (auto simp: tx t) have χ: "χ ∈ fmla" unfolding χ_def using Cons.prems t x by auto have "Fvars (rawpsubst χ txs) ⊆ (Fvars χ - snd ` (set txs)) ∪ (⋃ {FvarsT t | t x . (t,x) ∈ set txs})" using Cons.prems χ by (intro Cons.IH) auto also have "… ⊆ Fvars φ - insert x (snd ` set txs) ∪ ⋃{FvarsT ta |ta. ∃xa. ta = t ∧ xa = x ∨ (ta, xa) ∈ set txs}" (is "_ ⊆ ?R") by(auto simp: 0 tx Cons.prems) finally have 1: "Fvars (rawpsubst χ txs) ⊆ ?R" . have 2: "Fvars χ = Fvars φ - {x} ∪ (if x ∈ Fvars φ then FvarsT t else {})" using Cons.prems t x unfolding χ_def using Fvars_subst by auto show ?case using 1 by (simp add: tx χ_def[symmetric] 2) qed auto lemma in_Fvars_rawpsubst_imp: assumes "y ∈ Fvars (rawpsubst φ txs)" and "φ ∈ fmla" and "snd ` (set txs) ⊆ var" and "fst ` (set txs) ⊆ trm" shows "(y ∈ Fvars φ - snd ` (set txs)) ∨ (y ∈ ⋃ { FvarsT t | t x . (t,x) ∈ set txs})" using Fvars_rawpsubst_su[OF assms(2-4)] using assms(1) by blast lemma Fvars_rawpsubst: assumes "φ ∈ fmla" and "snd ` (set txs) ⊆ var" and "fst ` (set txs) ⊆ trm" and "distinct (map snd txs)" and "∀ x ∈ snd ` (set txs). ∀ t ∈ fst ` (set txs). x ∉ FvarsT t" shows "Fvars (rawpsubst φ txs) = (Fvars φ - snd ` (set txs)) ∪ (⋃ {if x ∈ Fvars φ then FvarsT t else {} | t x . (t,x) ∈ set txs})" using assms proof(induction txs arbitrary: φ) case (Cons a txs φ) then obtain t x where a: "a = (t,x)" by force have t: "t ∈ trm" and x: "x ∈ var" using Cons.prems unfolding a by auto have x_txs: "⋀ta xa. (ta, xa) ∈ set txs ⟹ x ≠ xa" using ‹distinct (map snd (a # txs))› unfolding a by (auto simp: rev_image_eqI) have xt: "x ∉ FvarsT t ∧ snd ` set txs ∩ FvarsT t = {}" using Cons.prems unfolding a by auto hence 0: "Fvars φ - {x} ∪ FvarsT t - snd ` set txs = Fvars φ - insert x (snd ` set txs) ∪ FvarsT t" by auto define χ where χ_def: "χ = subst φ t x" have χ: "χ ∈ fmla" unfolding χ_def using Cons.prems t x by auto have 1: "Fvars (rawpsubst χ txs) = (Fvars χ - snd ` (set txs)) ∪ (⋃ {if x ∈ Fvars χ then FvarsT t else {} | t x . (t,x) ∈ set txs})" using Cons.prems χ by (intro Cons.IH) auto have 2: "Fvars χ = Fvars φ - {x} ∪ (if x ∈ Fvars φ then FvarsT t else {})" using Cons.prems t x unfolding χ_def using Fvars_subst by auto define f where "f ≡ λta xa. if xa ∈ Fvars φ then FvarsT ta else {}" have 3: "⋃ {f ta xa |ta xa. (ta, xa) ∈ set ((t, x) # txs)} = f t x ∪ (⋃ {f ta xa |ta xa. (ta, xa) ∈ set txs})" by auto have 4: "snd ` set ((t, x) # txs) = {x} ∪ snd ` set txs" by auto have 5: "f t x ∩ snd ` set txs = {}" unfolding f_def using xt by auto have 6: "⋃ {if xa ∈ Fvars φ - {x} ∪ f t x then FvarsT ta else {} | ta xa. (ta, xa) ∈ set txs} = (⋃ {f ta xa | ta xa. (ta, xa) ∈ set txs})" unfolding f_def using xt x_txs by (fastforce split: if_splits) have "Fvars φ - {x} ∪ f t x - snd ` set txs ∪ ⋃ {if xa ∈ Fvars φ - {x} ∪ f t x then FvarsT ta else {} | ta xa. (ta, xa) ∈ set txs} = Fvars φ - snd ` set ((t, x) # txs) ∪ ⋃ {f ta xa |ta xa. (ta, xa) ∈ set ((t, x) # txs)}" unfolding 3 4 6 unfolding Un_Diff2[OF 5] Un_assoc unfolding Diff_Diff_Un .. thus ?case unfolding a rawpsubst.simps 1 2 χ_def[symmetric] f_def by simp qed auto lemma in_Fvars_rawpsubstD: assumes "y ∈ Fvars (rawpsubst φ txs)" and "φ ∈ fmla" and "snd ` (set txs) ⊆ var" and "fst ` (set txs) ⊆ trm" and "distinct (map snd txs)" and "∀ x ∈ snd ` (set txs). ∀ t ∈ fst ` (set txs). x ∉ FvarsT t" shows "(y ∈ Fvars φ - snd ` (set txs)) ∨ (y ∈ ⋃ {if x ∈ Fvars φ then FvarsT t else {} | t x . (t,x) ∈ set txs})" using Fvars_rawpsubst assms by auto lemma Fvars_psubst: assumes "φ ∈ fmla" and "snd ` (set txs) ⊆ var" and "fst ` (set txs) ⊆ trm" and "distinct (map snd txs)" shows "Fvars (psubst φ txs) = (Fvars φ - snd ` (set txs)) ∪ (⋃ {if x ∈ Fvars φ then FvarsT t else {} | t x . (t,x) ∈ set txs})" proof- define us where us: "us = getFrN (map snd txs) (map fst txs) [φ] (length txs)" have us_facts: "set us ⊆ var" "set us ∩ Fvars φ = {}" "set us ∩ ⋃ (FvarsT ` (fst ` (set txs))) = {}" "set us ∩ snd ` (set txs) = {}" "length us = length txs" "distinct us" using assms unfolding us using getFrN_FvarsT[of "map snd txs" "map fst txs" "[φ]" _ "length txs"] getFrN_Fvars[of "map snd txs" "map fst txs" "[φ]" _ "length txs"] getFrN_var[of "map snd txs" "map fst txs" "[φ]" _ "length txs"] getFrN_length[of "map snd txs" "map fst txs" "[φ]" "length txs"] getFrN_length[of "map snd txs" "map fst txs" "[φ]" "length txs"] by (auto 9 0 simp: set_eq_iff image_iff) define χ where χ_def: "χ = rawpsubst φ (zip (map Var us) (map snd txs))" have χ: "χ ∈ fmla" unfolding χ_def using assms us_facts by (intro rawpsubst) (auto dest!: set_zip_D) have set_us: "set us = snd ` (set (zip (map fst txs) us))" using us_facts by (intro snd_set_zip[symmetric]) auto have set_txs: "snd ` set txs = snd ` (set (zip (map Var us) (map snd txs)))" using us_facts by (intro snd_set_zip_map_snd[symmetric]) auto have "⋀ t x. (t, x) ∈ set (zip (map Var us) (map snd txs)) ⟹ ∃ u. t = Var u" using us_facts set_zip_leftD by fastforce hence 00: "⋀ t x. (t, x) ∈ set (zip (map Var us) (map snd txs)) ⟷ (∃ u ∈ var. t = Var u ∧ (Var u, x) ∈ set (zip (map Var us) (map snd txs)))" using us_facts set_zip_leftD by fastforce have "Fvars χ = Fvars φ - snd ` set txs ∪ ⋃{if x ∈ Fvars φ then FvarsT t else {} |t x. (t, x) ∈ set (zip (map Var us) (map snd txs))}" unfolding χ_def set_txs using assms us_facts apply(intro Fvars_rawpsubst) subgoal by auto subgoal by (auto dest!: set_zip_rightD) subgoal by (auto dest!: set_zip_leftD) subgoal by auto subgoal by (auto 0 6 simp: set_txs[symmetric] set_eq_iff subset_eq image_iff in_set_zip dest: spec[where P="λx. x ∈ set us ⟶ (∀y ∈ set txs. x ≠ snd y)", THEN mp[OF _ nth_mem]]) . also have "… = Fvars φ - snd ` set txs ∪ ⋃{if x ∈ Fvars φ then {u} else {} |u x. u ∈ var ∧ (Var u, x) ∈ set (zip (map Var us) (map snd txs))}" (is "… = ?R") using FvarsT_Var by (metis (no_types, opaque_lifting) 00) finally have 0: "Fvars χ = ?R" . have 1: "Fvars (rawpsubst χ (zip (map fst txs) us)) = (Fvars χ - set us) ∪ (⋃ {if u ∈ Fvars χ then FvarsT t else {} | t u . (t,u) ∈ set (zip (map fst txs) us)})" unfolding set_us using us_facts assms χ apply (intro Fvars_rawpsubst) subgoal by (auto dest: set_zip_rightD) subgoal by (auto dest: set_zip_rightD) subgoal by (auto dest!: set_zip_leftD) subgoal by (auto dest!: set_zip_leftD) subgoal by (metis IntI Union_iff empty_iff fst_set_zip_map_fst image_eqI set_us) . have 2: "Fvars χ - set us = Fvars φ - snd ` set txs" unfolding 0 using us_facts(1,2) by (fastforce dest!: set_zip_leftD split: if_splits) have 3: "(⋃ {if u ∈ Fvars χ then FvarsT t else {} | t u . (t,u) ∈ set (zip (map fst txs) us)}) = (⋃ {if x ∈ Fvars φ then FvarsT t else {} | t x . (t,x) ∈ set txs})" proof safe fix xx tt y assume xx: "xx ∈ (if y ∈ Fvars χ then FvarsT tt else {})" and ty: "(tt, y) ∈ set (zip (map fst txs) us)" have ttin: "tt ∈ fst ` set txs" using ty using set_zip_leftD by fastforce have yin: "y ∈ set us" using ty by (meson set_zip_D) have yvar: "y ∈ var" using us_facts yin by auto have ynotin: "y ∉ snd ` set txs" "y ∉ Fvars φ" using yin us_facts by auto show "xx ∈ ⋃{if x ∈ Fvars φ then FvarsT t else {} |t x. (t, x) ∈ set txs}" proof(cases "y ∈ Fvars χ") case True note y = True hence xx: "xx ∈ FvarsT tt" using xx by simp obtain x where xφ: "x ∈ Fvars φ" and yx: "(Var y, x) ∈ set (zip (map Var us) (map snd txs))" using y ynotin unfolding 0 by auto (metis empty_iff insert_iff) have yx: "(y, x) ∈ set (zip us (map snd txs))" using yvar us_facts by (intro inj_on_set_zip_map[OF inj_on_Var yx]) auto have "(tt, x) ∈ set txs" apply(rule set_zip_map_fst_snd[OF yx ty]) using ‹distinct (map snd txs)› us_facts by auto thus ?thesis using xx xφ by auto qed(insert xx, auto) next fix y tt xx assume y: "y ∈ (if xx ∈ Fvars φ then FvarsT tt else {})" and tx: "(tt, xx) ∈ set txs" hence xxsnd: "xx ∈ snd ` set txs" by force obtain u where uin: "u ∈ set us" and uxx: "(u, xx) ∈ set (zip us (map snd txs))" by (metis xxsnd in_set_impl_in_set_zip2 length_map set_map set_zip_leftD us_facts(5)) hence uvar: "u ∈ var" using us_facts by auto show "y ∈ ⋃{if u ∈ Fvars χ then FvarsT t else {} |t u. (t, u) ∈ set (zip (map fst txs) us)}" proof(cases "xx ∈ Fvars φ") case True note xx = True hence y: "y ∈ FvarsT tt" using y by auto have "(Var u, xx) ∈ set (zip (map Var us) (map snd txs))" using us_facts by (intro set_zip_length_map[OF uxx]) auto hence uχ: "u ∈ Fvars χ" using uin xx uvar unfolding 0 by auto have ttu: "(tt, u) ∈ set (zip (map fst txs) us)" using assms us_facts by (intro set_zip_map_fst_snd2[OF uxx tx]) auto show ?thesis using uχ ttu y by auto qed(insert y, auto) qed show ?thesis by (simp add: psubst_def Let_def us[symmetric] χ_def[symmetric] 1 2 3) qed lemma in_Fvars_psubstD: assumes "y ∈ Fvars (psubst φ txs)" and "φ ∈ fmla" and "snd ` (set txs) ⊆ var" and "fst ` (set txs) ⊆ trm" and "distinct (map snd txs)" shows "y ∈ (Fvars φ - snd ` (set txs)) ∪ (⋃ {if x ∈ Fvars φ then FvarsT t else {} | t x . (t,x) ∈ set txs})" using assms Fvars_psubst by auto lemma subst2_fresh_switch: assumes "φ ∈ fmla" "t ∈ trm" "s ∈ trm" "x ∈ var" "y ∈ var" and "x ≠ y" "x ∉ FvarsT s" "y ∉ FvarsT t" shows "subst (subst φ s y) t x = subst (subst φ t x) s y" (is "?L = ?R") using assms by (simp add: subst_compose_diff[of φ s t y x]) lemma rawpsubst2_fresh_switch: assumes "φ ∈ fmla" "t ∈ trm" "s ∈ trm" "x ∈ var" "y ∈ var" and "x ≠ y" "x ∉ FvarsT s" "y ∉ FvarsT t" shows "rawpsubst φ ([(s,y),(t,x)]) = rawpsubst φ ([(t,x),(s,y)])" using assms by (simp add: subst2_fresh_switch) lemma rawpsubst_compose: assumes "φ ∈ fmla" and "snd ` (set txs1) ⊆ var" and "fst ` (set txs1) ⊆ trm" and "snd ` (set txs2) ⊆ var" and "fst ` (set txs2) ⊆ trm" shows "rawpsubst (rawpsubst φ txs1) txs2 = rawpsubst φ (txs1 @ txs2)" using assms by (induct txs1 arbitrary: txs2 φ) auto lemma rawpsubst_subst_fresh_switch: assumes "φ ∈ fmla" "snd ` (set txs) ⊆ var" and "fst ` (set txs) ⊆ trm" and "∀ x ∈ snd ` (set txs). x ∉ FvarsT s" and "∀ t ∈ fst ` (set txs). y ∉ FvarsT t" and "distinct (map snd txs)" and "s ∈ trm" and "y ∈ var" "y ∉ snd ` (set txs)" shows "rawpsubst (subst φ s y) txs = rawpsubst φ (txs @ [(s,y)])" using assms proof(induction txs arbitrary: φ s y) case (Cons tx txs) obtain t x where tx[simp]: "tx = (t,x)" by force have x: "x ∈ var" and t: "t ∈ trm" using Cons unfolding tx by auto have "rawpsubst φ ((s, y) # (t, x) # txs) = rawpsubst φ ([(s, y),(t, x)] @ txs)" by simp also have "… = rawpsubst (rawpsubst φ [(s, y),(t, x)]) txs" using Cons by auto also have "rawpsubst φ [(s, y),(t, x)] = rawpsubst φ [(t, x),(s, y)]" using Cons by (intro rawpsubst2_fresh_switch) auto also have "rawpsubst (rawpsubst φ [(t, x),(s, y)]) txs = rawpsubst φ ([(t, x),(s, y)] @ txs)" using Cons by auto also have "… = rawpsubst (subst φ t x) (txs @ [(s,y)])" using Cons by auto also have "… = rawpsubst φ (((t, x) # txs) @ [(s, y)])" by simp finally show ?case unfolding tx by auto qed auto lemma subst_rawpsubst_fresh_switch: assumes "φ ∈ fmla" "snd ` (set txs) ⊆ var" and "fst ` (set txs) ⊆ trm" and "∀ x ∈ snd ` (set txs). x ∉ FvarsT s" and "∀ t ∈ fst ` (set txs). y ∉ FvarsT t" and "distinct (map snd txs)" and "s ∈ trm" and "y ∈ var" "y ∉ snd ` (set txs)" shows "subst (rawpsubst φ txs) s y = rawpsubst φ ((s,y) # txs)" using assms proof(induction txs arbitrary: φ s y) case (Cons tx txs) obtain t x where tx[simp]: "tx = (t,x)" by force have x: "x ∈ var" and t: "t ∈ trm" using Cons unfolding tx by auto have "subst (rawpsubst (subst φ t x) txs) s y = rawpsubst (subst φ t x) ((s,y) # txs)" using Cons.prems by (intro Cons.IH) auto also have "… = rawpsubst (rawpsubst φ [(t,x)]) ((s,y) # txs)" by simp also have "… = rawpsubst φ ([(t,x)] @ ((s,y) # txs))" using Cons.prems by auto also have "… = rawpsubst φ ([(t,x),(s,y)] @ txs)" by simp also have "… = rawpsubst (rawpsubst φ [(t,x),(s,y)]) txs" using Cons.prems by auto also have "rawpsubst φ [(t,x),(s,y)] = rawpsubst φ [(s,y),(t,x)]" using Cons.prems by (intro rawpsubst2_fresh_switch) auto also have "rawpsubst (rawpsubst φ [(s,y),(t,x)]) txs = rawpsubst φ ([(s,y),(t,x)] @ txs)" using Cons.prems by auto finally show ?case by simp qed auto lemma rawpsubst_compose_freshVar: assumes "φ ∈ fmla" "snd ` (set txs) ⊆ var" and "fst ` (set txs) ⊆ trm" and "distinct (map snd txs)" and "⋀ i j. i < j ⟹ j < length txs ⟹ snd (txs!j) ∉ FvarsT (fst (txs!i))" and us_facts: "set us ⊆ var" "set us ∩ Fvars φ = {}" "set us ∩ ⋃ (FvarsT ` (fst ` (set txs))) = {}" "set us ∩ snd ` (set txs) = {}" "length us = length txs" "distinct us" shows "rawpsubst (rawpsubst φ (zip (map Var us) (map snd txs))) (zip (map fst txs) us) = rawpsubst φ txs" using assms proof(induction txs arbitrary: us φ) case (Cons tx txs uus φ) obtain t x where tx[simp]: "tx = (t,x)" by force obtain u us where uus[simp]: "uus = u # us" using Cons by (cases uus) auto have us_facts: "set us ⊆ var" "set us ∩ Fvars φ = {}" "set us ∩ ⋃ (FvarsT ` (fst ` (set txs))) = {}" "set us ∩ snd ` (set txs) = {}" "length us = length txs" "distinct us" and u_facts: "u ∈ var" "u ∉ Fvars φ" "u ∉ ⋃ (FvarsT ` (fst ` (set txs)))" "u ∉ snd ` (set txs)" "u ∉ set us" using Cons by auto let ?uxs = "zip (map Var us) (map snd txs)" have 1: "rawpsubst (subst φ (Var u) x) ?uxs = rawpsubst φ (?uxs @ [(Var u,x)])" using u_facts Cons.prems by (intro rawpsubst_subst_fresh_switch) (auto simp: subsetD dest!: set_zip_D) let ?uuxs = "zip (map Var uus) (map snd (tx # txs))" let ?tus = "zip (map fst txs) us" let ?ttxs = "zip (map fst (tx # txs)) uus" have 2: "u ∈ Fvars (rawpsubst φ (zip (map Var us) (map snd txs))) ⟹ False" using Cons.prems apply- apply(drule in_Fvars_rawpsubstD) subgoal by auto subgoal by (auto dest!: set_zip_D) subgoal by (auto dest!: set_zip_D) subgoal by auto subgoal premises prems using us_facts(1,4,5) by (auto 0 3 simp: in_set_zip subset_eq set_eq_iff image_iff dest: spec[where P="λx. x ∈ set us ⟶ (∀y ∈ set txs. x ≠ snd y)", THEN mp[OF _ nth_mem], THEN bspec[OF _ nth_mem]]) subgoal by (auto simp: in_set_zip subset_eq split: if_splits) . have 3: "⋀ xx tt. xx ∈ FvarsT t ⟹ (tt, xx) ∉ set txs" using Cons.prems(4,5) tx unfolding set_conv_nth by simp (metis One_nat_def Suc_leI diff_Suc_1 fst_conv le_imp_less_Suc nth_Cons_0 snd_conv zero_less_Suc) have 00: "rawpsubst (rawpsubst φ ?uuxs) ?ttxs = rawpsubst (subst (rawpsubst φ (?uxs @ [(Var u, x)])) t u) ?tus" by (simp add: 1) have "rawpsubst φ (?uxs @ [(Var u, x)]) = rawpsubst (rawpsubst φ ?uxs) [(Var u, x)]" using Cons.prems by (intro rawpsubst_compose[symmetric]) (auto intro!: rawpsubst dest!: set_zip_D) also have "rawpsubst (rawpsubst φ ?uxs) [(Var u, x)] = subst (rawpsubst φ ?uxs) (Var u) x" by simp finally have "subst (rawpsubst φ (?uxs @ [(Var u, x)])) t u = subst (subst (rawpsubst φ ?uxs) (Var u) x) t u" by simp also have "… = subst (rawpsubst φ ?uxs) t x" using Cons 2 by (intro subst_subst) (auto intro!: rawpsubst dest!: set_zip_D) also have "… = rawpsubst φ ((t,x) # ?uxs)" using Cons.prems 3 apply(intro subst_rawpsubst_fresh_switch) subgoal by (auto dest!: set_zip_D) subgoal by (auto dest!: set_zip_D) subgoal by (auto dest!: set_zip_D) subgoal by (auto dest!: set_zip_D) subgoal by (fastforce dest!: set_zip_D) by (auto dest!: set_zip_D) also have "… = rawpsubst φ ([(t,x)] @ ?uxs)" by simp also have "… = rawpsubst (rawpsubst φ [(t,x)]) ?uxs" using Cons.prems by (intro rawpsubst_compose[symmetric]) (auto dest!: set_zip_D) finally have "rawpsubst (subst (rawpsubst φ (?uxs @ [(Var u, x)])) t u) ?tus = rawpsubst (rawpsubst (rawpsubst φ [(t,x)]) ?uxs) ?tus" by auto hence "rawpsubst (rawpsubst φ ?uuxs) ?ttxs = rawpsubst (rawpsubst (rawpsubst φ [(t,x)]) ?uxs) ?tus" using 00 by auto also have "… = rawpsubst (rawpsubst φ [(t,x)]) txs" using Cons.prems apply (intro Cons.IH rawpsubst) subgoal by (auto dest!: set_zip_D in_Fvars_substD) subgoal by (auto dest!: set_zip_D in_Fvars_substD) subgoal by (auto dest!: set_zip_D in_Fvars_substD) subgoal by (auto dest!: set_zip_D in_Fvars_substD) subgoal by (auto dest!: set_zip_D in_Fvars_substD) subgoal by (auto dest!: set_zip_D in_Fvars_substD) subgoal by (metis Suc_mono diff_Suc_1 length_Cons nat.simps(3) nth_Cons') by (auto dest!: set_zip_D in_Fvars_substD) also have "… = rawpsubst φ ([(t,x)] @ txs)" using Cons.prems by (intro rawpsubst_compose) (auto dest!: set_zip_D) finally show ?case by simp qed auto lemma rawpsubst_compose_freshVar2_aux: assumes φ[simp]: "φ ∈ fmla" and ts: "set ts ⊆ trm" and xs: "set xs ⊆ var" "distinct xs" and us_facts: "set us ⊆ var" "distinct us" "set us ∩ Fvars φ = {}" "set us ∩ ⋃ (FvarsT ` (set ts)) = {}" "set us ∩ set xs = {}" and vs_facts: "set vs ⊆ var" "distinct vs" "set vs ∩ Fvars φ = {}" "set vs ∩ ⋃ (FvarsT ` (set ts)) = {}" "set vs ∩ set xs = {}" and l: "length us = length xs" "length vs = length xs" "length ts = length xs" and (* Extra hypothesis, only to get induction through: *) d: "set us ∩ set vs = {}" shows "rawpsubst (rawpsubst φ (zip (map Var us) xs)) (zip ts us) = rawpsubst (rawpsubst φ (zip (map Var vs) xs)) (zip ts vs)" using assms proof(induction xs arbitrary: φ ts us vs) case (Cons x xs φ tts uus vvs) obtain t ts u us v vs where tts[simp]: "tts = t # ts" and lts[simp]: "length ts = length xs" and uus[simp]: "uus = u # us" and lus[simp]: "length us = length xs" and vvs[simp]: "vvs = v # vs" and lvs[simp]: "length vs = length xs" using ‹length uus = length (x # xs)› ‹length vvs = length (x # xs)› ‹length tts = length (x # xs)› apply(cases tts) subgoal by auto subgoal apply(cases uus) subgoal by auto subgoal by (cases vvs) auto . . let ?φux = "subst φ (Var u) x" let ?φvx = "subst φ (Var v) x" have 0: "rawpsubst (rawpsubst ?φux (zip (map Var us) xs)) (zip ts us) = rawpsubst (rawpsubst ?φux (zip (map Var vs) xs)) (zip ts vs)" apply(rule Cons.IH) using Cons.prems by (auto intro!: rawpsubst dest!: set_zip_D) have 1: "rawpsubst ?φux (zip (map Var vs) xs) = subst (rawpsubst φ (zip (map Var vs) xs)) (Var u) x" using Cons.prems by (intro subst_rawpsubst_fresh_switch[simplified,symmetric]) (force intro!: rawpsubst dest!: set_zip_D simp: subset_eq)+ have 11: "rawpsubst ?φvx (zip (map Var vs) xs) = subst (rawpsubst φ (zip (map Var vs) xs)) (Var v) x" using Cons.prems by (intro subst_rawpsubst_fresh_switch[simplified,symmetric]) (auto intro!: rawpsubst dest!: set_zip_D simp: subset_eq) have "subst (subst (rawpsubst φ (zip (map Var vs) xs)) (Var u) x) t u = subst (rawpsubst φ (zip (map Var vs) xs)) t x" using Cons.prems by (intro subst_subst) (force intro!: rawpsubst dest!: set_zip_D in_Fvars_rawpsubst_imp simp: Fvars_rawpsubst)+ also have "… = subst (subst (rawpsubst φ (zip (map Var vs) xs)) (Var v) x) t v" using Cons.prems by (intro subst_subst[symmetric]) (force intro!: rawpsubst dest!: set_zip_D in_Fvars_rawpsubst_imp simp: Fvars_rawpsubst)+ finally have 2: "subst (subst (rawpsubst φ (zip (map Var vs) xs)) (Var u) x) t u = subst (subst (rawpsubst φ (zip (map Var vs) xs)) (Var v) x) t v" . have "rawpsubst (subst (rawpsubst ?φux (zip (map Var us) xs)) t u) (zip ts us) = subst (rawpsubst (rawpsubst ?φux (zip (map Var us) xs)) (zip ts us)) t u" using Cons.prems by (intro subst_rawpsubst_fresh_switch[simplified,symmetric]) (auto intro!: rawpsubst dest!: set_zip_D) also have "… = subst (rawpsubst (rawpsubst ?φux (zip (map Var vs) xs)) (zip ts vs)) t u" unfolding 0 .. also have "… = rawpsubst (subst (rawpsubst ?φux (zip (map Var vs) xs)) t u) (zip ts vs)" using Cons.prems by (intro subst_rawpsubst_fresh_switch[simplified]) (auto intro!: rawpsubst dest!: set_zip_D) also have "… = rawpsubst (subst (subst (rawpsubst φ (zip (map Var vs) xs)) (Var u) x) t u) (zip ts vs)" unfolding 1 .. also have "… = rawpsubst (subst (subst (rawpsubst φ (zip (map Var vs) xs)) (Var v) x) t v) (zip ts vs)" unfolding 2 .. also have "… = rawpsubst (subst (rawpsubst ?φvx (zip (map Var vs) xs)) t v) (zip ts vs)" unfolding 11 .. finally have "rawpsubst (subst (rawpsubst ?φux (zip (map Var us) xs)) t u) (zip ts us) = rawpsubst (subst (rawpsubst ?φvx (zip (map Var vs) xs)) t v) (zip ts vs)" . thus ?case by simp qed auto text ‹... now getting rid of the disjointness hypothesis:› lemma rawpsubst_compose_freshVar2: assumes φ[simp]: "φ ∈ fmla" and ts: "set ts ⊆ trm" and xs: "set xs ⊆ var" "distinct xs" and us_facts: "set us ⊆ var" "distinct us" "set us ∩ Fvars φ = {}" "set us ∩ ⋃ (FvarsT ` (set ts)) = {}" "set us ∩ set xs = {}" and vs_facts: "set vs ⊆ var" "distinct vs" "set vs ∩ Fvars φ = {}" "set vs ∩ ⋃ (FvarsT ` (set ts)) = {}" "set vs ∩ set xs = {}" and l: "length us = length xs" "length vs = length xs" "length ts = length xs" shows "rawpsubst (rawpsubst φ (zip (map Var us) xs)) (zip ts us) = rawpsubst (rawpsubst φ (zip (map Var vs) xs)) (zip ts vs)" (is "?L = ?R") proof- define ws where "ws = getFrN (xs @ us @ vs) ts [φ] (length xs)" note fv = getFrN_Fvars[of "xs @ us @ vs" "ts" "[φ]" _ "length xs"] and fvt = getFrN_FvarsT[of "xs @ us @ vs" "ts" "[φ]" _ "length xs"] and var = getFrN_var[of "xs @ us @ vs" "ts" "[φ]" _ "length xs"] and l = getFrN_length[of "xs @ us @ vs" "ts" "[φ]" "length xs"] have ws_facts: "set ws ⊆ var" "distinct ws" "set ws ∩ Fvars φ = {}" "set ws ∩ ⋃ (FvarsT ` (set ts)) = {}" "set ws ∩ set xs = {}" "set ws ∩ set us = {}" "set ws ∩ set vs = {}" "length ws = length xs" using assms unfolding ws_def apply - subgoal by auto subgoal by auto subgoal using fv by auto subgoal using fvt IntI empty_iff by fastforce subgoal using var IntI empty_iff by fastforce subgoal using var IntI empty_iff by fastforce subgoal using var IntI empty_iff by fastforce subgoal using l by auto . have "?L = rawpsubst (rawpsubst φ (zip (map Var ws) xs)) (zip ts ws)" apply(rule rawpsubst_compose_freshVar2_aux) using assms ws_facts by auto also have "… = ?R" apply(rule rawpsubst_compose_freshVar2_aux) using assms ws_facts by auto finally show ?thesis . qed lemma psubst_subst_fresh_switch: assumes "φ ∈ fmla" "snd ` set txs ⊆ var" "fst ` set txs ⊆ trm" and "∀x∈snd ` set txs. x ∉ FvarsT s" "∀t∈fst ` set txs. y ∉ FvarsT t" and "distinct (map snd txs)" and "s ∈ trm" "y ∈ var" "y ∉ snd ` set txs" shows "psubst (subst φ s y) txs = subst (psubst φ txs) s y" proof- define us where us: "us = getFrN (map snd txs) (map fst txs) [φ] (length txs)" note fvt = getFrN_FvarsT[of "map snd txs" "map fst txs" "[φ]" _ "length txs"] and fv = getFrN_Fvars[of "map snd txs" "map fst txs" "[φ]" _ "length txs"] and var = getFrN_var[of "map snd txs" "map fst txs" "[φ]" _ "length txs"] and l = getFrN_length[of "map snd txs" "map fst txs" "[φ]" "length txs"] have us_facts: "set us ⊆ var" "set us ∩ Fvars φ = {}" "set us ∩ ⋃ (FvarsT ` (fst ` (set txs))) = {}" "set us ∩ snd ` (set txs) = {}" "length us = length txs" "distinct us" using assms unfolding us apply - subgoal by auto subgoal using fv by (cases txs, auto) subgoal using fvt by (cases txs, auto) subgoal using var by (cases txs, auto) subgoal using l by auto subgoal by auto . define vs where vs: "vs = getFrN (map snd txs) (map fst txs) [subst φ s y] (length txs)" note fvt = getFrN_FvarsT[of "map snd txs" "map fst txs" "[subst φ s y]" _ "length txs"] and fv = getFrN_Fvars[of "map snd txs" "map fst txs" "[subst φ s y]" _ "length txs"] and var = getFrN_var[of "map snd txs" "map fst txs" "[subst φ s y]" _ "length txs"] and l = getFrN_length[of "map snd txs" "map fst txs" "[subst φ s y]" "length txs"] have vs_facts: "set vs ⊆ var" "set vs ∩ Fvars (subst φ s y) = {}" "set vs ∩ ⋃ (FvarsT ` (fst ` (set txs))) = {}" "set vs ∩ snd ` (set txs) = {}" "length vs = length txs" "distinct vs" using assms unfolding vs apply - subgoal by auto subgoal using fv by (cases txs, auto) subgoal using fvt by (cases txs, auto) subgoal using var by (cases txs, auto) subgoal using l by auto subgoal by auto . define ws where ws: "ws = getFrN (y # map snd txs) (s # map fst txs) [φ] (length txs)" note fvt = getFrN_FvarsT[of "y # map snd txs" "s # map fst txs" "[φ]" _ "length txs"] and fv = getFrN_Fvars[of "y # map snd txs" "s # map fst txs" "[φ]" _ "length txs"] and var = getFrN_var[of "y # map snd txs" "s # map fst txs" "[φ]" _ "length txs"] and l = getFrN_length[of "y # map snd txs" "s # map fst txs" "[φ]" "length txs"] have ws_facts: "set ws ⊆ var" "set ws ∩ Fvars φ = {}" "y ∉ set ws" "set ws ∩ FvarsT s = {}" "set ws ∩ ⋃ (FvarsT ` (fst ` (set txs))) = {}" "set ws ∩ snd ` (set txs) = {}" "length ws = length txs" "distinct ws" using assms unfolding ws apply - subgoal by auto subgoal using fv by (cases txs, auto) subgoal using var by (cases txs, auto) subgoal using fvt by (cases txs, auto) subgoal using fvt by (cases txs, auto) subgoal using var by (cases txs, auto) subgoal using l by (cases txs, auto) by auto let ?vxs = "zip (map Var vs) (map snd txs)" let ?tvs = "(zip (map fst txs) vs)" let ?uxs = "zip (map Var us) (map snd txs)" let ?tus = "(zip (map fst txs) us)" let ?wxs = "zip (map Var ws) (map snd txs)" let ?tws = "(zip (map fst txs) ws)" have 0: "rawpsubst (subst φ s y) ?wxs = subst (rawpsubst φ ?wxs) s y" apply(subst rawpsubst_compose[of φ ?wxs "[(s,y)]",simplified]) using assms ws_facts apply - subgoal by auto subgoal by (auto dest!: set_zip_D) subgoal by (auto dest!: set_zip_D) subgoal by auto subgoal by auto subgoal apply(subst rawpsubst_subst_fresh_switch) by (auto dest!: set_zip_D simp: subset_eq rawpsubst_subst_fresh_switch) . have 1: "rawpsubst (rawpsubst φ ?wxs) ?tws = rawpsubst (rawpsubst φ ?uxs) ?tus" using assms ws_facts us_facts by (intro rawpsubst_compose_freshVar2) (auto simp: subset_eq) have "rawpsubst (rawpsubst (subst φ s y) ?vxs) ?tvs = rawpsubst (rawpsubst (subst φ s y) ?wxs) ?tws" using assms ws_facts vs_facts by (intro rawpsubst_compose_freshVar2) (auto simp: subset_eq) also have "… = rawpsubst (subst (rawpsubst φ ?wxs) s y) ?tws" unfolding 0 .. also have "… = subst (rawpsubst (rawpsubst φ ?wxs) ?tws) s y" apply(subst rawpsubst_compose[of "rawpsubst φ ?wxs" ?tws "[(s,y)]",simplified]) using assms ws_facts apply - subgoal by (auto dest!: set_zip_D simp: subset_eq intro!: rawpsubst) subgoal by (auto dest!: set_zip_D) subgoal by (auto dest!: set_zip_D) subgoal by auto subgoal by auto subgoal by (subst rawpsubst_subst_fresh_switch) (auto dest!: set_zip_D simp: subset_eq rawpsubst_subst_fresh_switch intro!: rawpsubst) . also have "… = subst (rawpsubst (rawpsubst φ ?uxs) ?tus) s y" unfolding 1 .. finally show ?thesis unfolding psubst_def by (simp add: Let_def vs[symmetric] us[symmetric]) qed text ‹For many cases, the simpler rawpsubst can replace psubst:› lemma psubst_eq_rawpsubst: assumes "φ ∈ fmla" "snd ` (set txs) ⊆ var" and "fst ` (set txs) ⊆ trm" and "distinct (map snd txs)" (* ... namely, when the substituted variables do not belong to trms substituted for previous variables: *) and "⋀ i j. i < j ⟹ j < length txs ⟹ snd (txs!j) ∉ FvarsT (fst (txs!i))" shows "psubst φ txs = rawpsubst φ txs" proof- define us where us: "us = getFrN (map snd txs) (map fst txs) [φ] (length txs)" note fvt = getFrN_FvarsT[of "map snd txs" "map fst txs" "[φ]" _ "length txs"] and fv = getFrN_Fvars[of "map snd txs" "map fst txs" "[φ]" _ "length txs"] and var = getFrN_var[of "map snd txs" "map fst txs" "[φ]" _ "length txs"] and l = getFrN_length[of "map snd txs" "map fst txs" "[φ]" "length txs"] have us_facts: "set us ⊆ var" "set us ∩ Fvars φ = {}" "set us ∩ ⋃ (FvarsT ` (fst ` (set txs))) = {}" "set us ∩ snd ` (set txs) = {}" "length us = length txs" "distinct us" using assms unfolding us apply - subgoal by auto subgoal using fv by auto subgoal using fvt by force subgoal using var by (force simp: image_iff) using l by auto show ?thesis using rawpsubst_compose_freshVar assms us_facts by (simp add: psubst_def Let_def us[symmetric]) qed text ‹Some particular cases:› lemma psubst_eq_subst: assumes "φ ∈ fmla" "x ∈ var" and "t ∈ trm" shows "psubst φ [(t,x)] = subst φ t x" proof- have "psubst φ [(t,x)] = rawpsubst φ [(t,x)]" apply(rule psubst_eq_rawpsubst) using assms by auto thus ?thesis by auto qed lemma psubst_eq_rawpsubst2: assumes "φ ∈ fmla" "x1 ∈ var" "x2 ∈ var" "t1 ∈ trm" "t2 ∈ trm" and "x1 ≠ x2" "x2 ∉ FvarsT t1" shows "psubst φ [(t1,x1),(t2,x2)] = rawpsubst φ [(t1,x1),(t2,x2)]" apply(rule psubst_eq_rawpsubst) using assms using less_SucE by force+ lemma psubst_eq_rawpsubst3: assumes "φ ∈ fmla" "x1 ∈ var" "x2 ∈ var" "x3 ∈ var" "t1 ∈ trm" "t2 ∈ trm" "t3 ∈ trm" and "x1 ≠ x2" "x1 ≠ x3" "x2 ≠ x3" "x2 ∉ FvarsT t1" "x3 ∉ FvarsT t1" "x3 ∉ FvarsT t2" shows "psubst φ [(t1,x1),(t2,x2),(t3,x3)] = rawpsubst φ [(t1,x1),(t2,x2),(t3,x3)]" using assms using less_SucE apply(intro psubst_eq_rawpsubst) subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal for i j apply(cases j) subgoal by auto subgoal by (simp add: nth_Cons') . . lemma psubst_eq_rawpsubst4: assumes "φ ∈ fmla" "x1 ∈ var" "x2 ∈ var" "x3 ∈ var" "x4 ∈ var" "t1 ∈ trm" "t2 ∈ trm" "t3 ∈ trm" "t4 ∈ trm" and "x1 ≠ x2" "x1 ≠ x3" "x2 ≠ x3" "x1 ≠ x4" "x2 ≠ x4" "x3 ≠ x4" "x2 ∉ FvarsT t1" "x3 ∉ FvarsT t1" "x3 ∉ FvarsT t2" "x4 ∉ FvarsT t1" "x4 ∉ FvarsT t2" "x4 ∉ FvarsT t3" shows "psubst φ [(t1,x1),(t2,x2),(t3,x3),(t4,x4)] = rawpsubst φ [(t1,x1),(t2,x2),(t3,x3),(t4,x4)]" using assms using less_SucE apply(intro psubst_eq_rawpsubst) subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal for i j apply(cases j) subgoal by auto subgoal by (simp add: nth_Cons') . . lemma rawpsubst_same_Var[simp]: assumes "φ ∈ fmla" "set xs ⊆ var" shows "rawpsubst φ (map (λx. (Var x,x)) xs) = φ" using assms by (induct xs) auto lemma psubst_same_Var[simp]: assumes "φ ∈ fmla" "set xs ⊆ var" and "distinct xs" shows "psubst φ (map (λx. (Var x,x)) xs) = φ" proof- have "psubst φ (map (λx. (Var x,x)) xs) = rawpsubst φ (map (λx. (Var x,x)) xs)" using assms by (intro psubst_eq_rawpsubst) (auto simp: nth_eq_iff_index_eq subsetD) thus ?thesis using assms by auto qed lemma rawpsubst_notIn[simp]: assumes "snd ` (set txs) ⊆ var" "fst ` (set txs) ⊆ trm" "φ ∈ fmla" and "Fvars φ ∩ snd ` (set txs) = {}" shows "rawpsubst φ txs = φ" using assms by (induct txs) auto lemma psubst_notIn[simp]: assumes "x ∈ var" "snd ` (set txs) ⊆ var" "fst ` (set txs) ⊆ trm" "φ ∈ fmla" and "Fvars φ ∩ snd ` (set txs) = {}" shows "psubst φ txs = φ" proof- define us where us: "us = getFrN (map snd txs) (map fst txs) [φ] (length txs)" have us_facts: "set us ⊆ var" "set us ∩ Fvars φ = {}" "set us ∩ ⋃ (FvarsT ` (fst ` (set txs))) = {}" "set us ∩ snd ` (set txs) = {}" "length us = length txs" using getFrN_Fvars[of "map snd txs" "map fst txs" "[φ]" _ "length txs"] getFrN_FvarsT[of "map snd txs" "map fst txs" "[φ]" _ "length<