Session Syntax_Independent_Logic

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"


text ‹Facts about zipping lists:›

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 {})"
  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, 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  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  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 "xsnd ` set txs. x  FvarsT s" "tfst ` 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}


section ‹Adding Connectives and Quantifiers›

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}


section ‹Adding Disjunction›

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}


section ‹Adding an Ordering-Like Formula›

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 χ ψ)) ψ))"
    by (simp add: assms prv_cnj_imp_monoR2)
  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
    by (simp add: assms prv_cnj_imp)
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))))"
    by(simp add: assms prv_cnj_imp_monoR2)
  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))))"
    by(simp add: assms prv_cnj_imp_monoR2)
  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 χ φ))"
  by (simp add: prv_cnj_com_imp prv_eqvI)

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

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