Theory Transition_QuasiTerms_Terms

section ‹Transition from Quasi-Terms to Terms›

theory Transition_QuasiTerms_Terms
imports QuasiTerms_Environments_Substitution Equiv_Relation2
begin

text‹This section transits from quasi-terms to terms: defines terms as alpha-equivalence
classes of quasi-terms
(and also abstractions as alpha-equivalence classes of  quasi-abstractions),
then defines operators on terms corresponding to those on quasi-terms:
variable injection, binding operation, freshness, swapping, parallel substitution, etc.
Properties previously shown invariant
under alpha-equivalence, including induction principles, are lifted from quasi-terms.
Moreover, a new powerful induction principle, allowing freshness assumptions,
is proved for terms.

As a matter of notation:
Starting from this section, we change the notations for quasi-item meta-variables, prefixing
their names with a "q" -- e.g., qX, qA, qinp, qenv, etc. The old names are now assigned
to the ``real" items: terms, abstractions, inputs, environments.›

subsection ‹Preparation: Integrating quasi-inputs as first-class citizens›

context FixVars
begin

text‹From now on it will be convenient to
   also define fresh, swap, good and alpha-equivalence for quasi-inpus.›

definition qSwapInp where
"qSwapInp xs x y qinp == lift (qSwap xs x y) qinp"

definition qSwapBinp where
"qSwapBinp xs x y qbinp == lift (qSwapAbs xs x y) qbinp"

abbreviation qSwapInp_abbrev ("_ %[[_  _]]'__" 200) where
"(qinp %[[z1  z2]]_zs) == qSwapInp zs z1 z2 qinp"

abbreviation qSwapBinp_abbrev ("_ %%[[_  _]]'__" 200) where
"(qbinp %%[[z1  z2]]_zs) == qSwapBinp zs z1 z2 qbinp"

lemma qSwap_qSwapInp:
"((qOp delta qinp qbinp) #[[x  y]]_xs) =
 qOp delta (qinp %[[x  y]]_xs) (qbinp %%[[x  y]]_xs)"
unfolding qSwapInp_def qSwapBinp_def by simp

(* For the qOp case, qSwap shall henceforth simplify to qSwapInp:  *)

declare qSwap.simps(2) [simp del]
declare qSwap_qSwapInp[simp]

(* and qSwap_simps and qSwapAll_simps, rather than qSwap.simps and qSwapAll.simps,
   shall refer to the simplification rules for qSwap *)

lemmas qSwapAll_simps = qSwap.simps(1) qSwap_qSwapInp

definition qPsubstInp where
"qPsubstInp qrho qinp == lift (qPsubst qrho) qinp"

definition qPsubstBinp where
"qPsubstBinp qrho qbinp == lift (qPsubstAbs qrho) qbinp"

abbreviation qPsubstInp_abbrev ("_ %[[_]]" 200)
where "(qinp %[[qrho]]) == qPsubstInp qrho qinp"

abbreviation qPsubstBinp_abbrev ("_ %%[[_]]" 200)
where "(qbinp %%[[qrho]]) == qPsubstBinp qrho qbinp"

lemma qPsubst_qPsubstInp:
"((qOp delta qinp qbinp) #[[rho]]) = qOp delta (qinp %[[rho]]) (qbinp %%[[rho]])"
unfolding qPsubstInp_def qPsubstBinp_def by simp

(* For the qOp case, qPsubst shall henceforth simplify to qPsubstInp:  *)

declare qPsubst.simps(2) [simp del]
declare qPsubst_qPsubstInp[simp]

(* and qPsubst_simps and qPsubstAll_simps, rather than qPsubst.simps and qPsubstAll.simps,
   shall refer to the simplification rules for qPsubst *)

lemmas qPsubstAll_simps = qPsubst.simps(1) qPsubst_qPsubstInp

definition qSkelInp
where "qSkelInp qinp = lift qSkel qinp"

definition qSkelBinp
where "qSkelBinp qbinp = lift qSkelAbs qbinp"

lemma qSkel_qSkelInp:
"qSkel (qOp delta qinp qbinp) =
 Branch (qSkelInp qinp) (qSkelBinp qbinp)"
unfolding qSkelInp_def qSkelBinp_def by simp

(* For the qOp case, qSkel shall henceforth simplify to qSkelInp:  *)

declare qSkel.simps(2) [simp del]
declare qSkel_qSkelInp[simp]

(* and qSkel_simps and qSkelAll_simps, rather than qSkel.simps and qSkelAll.simps,
   shall refer to the simplification rules for qSkel *)

lemmas qSkelAll_simps = qSkel.simps(1) qSkel_qSkelInp

definition qFreshInp ::
"'varSort  'var  ('index,('index,'bindex,'varSort,'var,'opSym)qTerm)input  bool"
where
"qFreshInp xs x qinp == liftAll (qFresh xs x) qinp"

definition qFreshBinp ::
"'varSort  'var  ('bindex,('index,'bindex,'varSort,'var,'opSym)qAbs)input  bool"
where
"qFreshBinp xs x qbinp == liftAll (qFreshAbs xs x) qbinp"

lemma qFresh_qFreshInp:
"qFresh xs x (qOp delta qinp qbinp) =
 (qFreshInp xs x qinp  qFreshBinp xs x qbinp)"
unfolding qFreshInp_def qFreshBinp_def by simp

(* For the qOp case, qFresh shall henceforth simplify to qFreshInp:  *)

declare qFresh.simps(2) [simp del]
declare qFresh_qFreshInp[simp]

(* and qFresh_simps and qFreshAll_simps, rather than qFresh.simps and qFreshAll.simps,
   shall refer to the simplification rules for qFresh *)

lemmas qFreshAll_simps = qFresh.simps(1) qFresh_qFreshInp

definition qGoodInp where
"qGoodInp qinp ==
 liftAll qGood qinp 
 |{i. qinp i  None}| <o |UNIV :: 'var set|"

definition qGoodBinp where
"qGoodBinp qbinp ==
 liftAll qGoodAbs qbinp 
 |{i. qbinp i  None}| <o |UNIV :: 'var set|"

lemma qGood_qGoodInp:
"qGood (qOp delta qinp qbinp) = (qGoodInp qinp  qGoodBinp qbinp)"
unfolding qGoodInp_def qGoodBinp_def by auto

(* For the qOp case, qGood shall henceforth simplify to qGoodInp:  *)

declare qGood.simps(2) [simp del]
declare qGood_qGoodInp [simp]

(* and qGood_simps (and qGoodAll_simps), rather than qGood.simps,
   shall refer to the simplification rules for qGood *)

lemmas qGoodAll_simps = qGood.simps(1) qGood_qGoodInp

definition alphaInp where
"alphaInp ==
 {(qinp,qinp'). sameDom qinp qinp'  liftAll2 (λqX qX'. qX #= qX') qinp qinp'}"

definition alphaBinp where
"alphaBinp ==
 {(qbinp,qbinp'). sameDom qbinp qbinp'  liftAll2 (λqA qA'. qA $= qA') qbinp qbinp'}"

abbreviation alphaInp_abbrev (infix "%=" 50) where
"qinp %= qinp' == (qinp,qinp')  alphaInp"

abbreviation alphaBinp_abbrev (infix "%%=" 50) where
"qbinp %%= qbinp' == (qbinp,qbinp')  alphaBinp"

lemma alpha_alphaInp:
"(qOp delta qinp qbinp #= qOp delta' qinp' qbinp') =
 (delta = delta'  qinp %= qinp'  qbinp %%= qbinp')"
unfolding alphaInp_def alphaBinp_def by auto

(* For the qOp case, alpha shall henceforth simplify to alphaInp:  *)
declare alpha.simps(2) [simp del]
declare alpha_alphaInp[simp]

(* and alpha_Simps and alphaAll_Simps, rather than alpha_simps and alphaAll_simps,
   shall refer to the simplification rules for alpha *)

lemmas alphaAll_Simps =
alpha.simps(1) alpha_alphaInp
alphaAbs.simps

lemma alphaInp_refl:
"qGoodInp qinp  qinp %= qinp"
using alpha_refl
unfolding alphaInp_def qGoodInp_def liftAll_def liftAll2_def sameDom_def
by fastforce

lemma alphaBinp_refl:
"qGoodBinp qbinp  qbinp %%= qbinp"
using alphaAbs_refl
unfolding alphaBinp_def qGoodBinp_def liftAll_def liftAll2_def sameDom_def
by fastforce

lemma alphaInp_sym:
fixes qinp qinp' :: "('index,('index,'bindex,'varSort,'var,'opSym)qTerm)input"
shows "qinp %= qinp'  qinp' %= qinp"
using alpha_sym unfolding alphaInp_def sameDom_def liftAll2_def by blast

lemma alphaBinp_sym:
fixes qbinp qbinp' :: "('bindex,('index,'bindex,'varSort,'var,'opSym)qAbs)input"
shows "qbinp %%= qbinp'  qbinp' %%= qbinp"
using alphaAbs_sym unfolding alphaBinp_def sameDom_def liftAll2_def by blast

lemma alphaInp_trans:
assumes good: "qGoodInp qinp" and
        alpha1: "qinp %= qinp'" and alpha2: "qinp' %= qinp''"
shows "qinp %= qinp''"
proof-
  {fix i qX qX''  assume qinp: "qinp i = Some qX" and qinp'': "qinp'' i = Some qX''"
  then obtain qX' where qinp': "qinp' i = Some qX'"
  using alpha1 unfolding alphaInp_def sameDom_def liftAll2_def by(cases "qinp' i", force)
  hence "qX #= qX'"
  using alpha1 qinp unfolding alphaInp_def sameDom_def liftAll2_def by auto
  moreover have "qX' #= qX''" using alpha2 qinp' qinp''
  unfolding alphaInp_def sameDom_def liftAll2_def by auto
  moreover have "qGood qX" using good qinp unfolding qGoodInp_def liftAll_def by auto
  ultimately have "qX #= qX''" using alpha_trans by blast
  }
  thus ?thesis using assms unfolding alphaInp_def sameDom_def liftAll2_def by auto
qed

lemma alphaBinp_trans:
assumes good: "qGoodBinp qbinp" and
        alpha1: "qbinp %%= qbinp'" and alpha2: "qbinp' %%= qbinp''"
shows "qbinp %%= qbinp''"
proof-
  {fix i qA qA''  assume qbinp: "qbinp i = Some qA" and qbinp'': "qbinp'' i = Some qA''"
  then obtain qA' where qbinp': "qbinp' i = Some qA'"
  using alpha1 unfolding alphaBinp_def sameDom_def liftAll2_def by(cases "qbinp' i", force)
  hence "qA $= qA'"
  using alpha1 qbinp unfolding alphaBinp_def sameDom_def liftAll2_def by auto
  moreover have "qA' $= qA''" using alpha2 qbinp' qbinp''
  unfolding alphaBinp_def sameDom_def liftAll2_def by auto
  moreover have "qGoodAbs qA" using good qbinp unfolding qGoodBinp_def liftAll_def by auto
  ultimately have "qA $= qA''" using alphaAbs_trans by blast
  }
  thus ?thesis using assms unfolding alphaBinp_def sameDom_def liftAll2_def by auto
qed

lemma qSwapInp_preserves_qGoodInp:
assumes "qGoodInp qinp"
shows "qGoodInp (qinp %[[x1  x2]]_xs)"
proof-
  {let ?qinp' = "lift (qSwap xs x1 x2) qinp"
  fix xsa  let ?Left = "{i. ?qinp' i  None}"
  have "?Left = {i. qinp i  None}" by(auto simp add: lift_None)
  hence "|?Left| <o |UNIV :: 'var set|" using assms unfolding qGoodInp_def by auto
  }
  thus ?thesis using assms 
  unfolding qGoodInp_def qSwapInp_def liftAll_lift_comp qGoodInp_def
  unfolding comp_def liftAll_def
  by (auto simp add: qSwap_preserves_qGood simp del: not_None_eq)
qed

lemma qSwapBinp_preserves_qGoodBinp:
assumes "qGoodBinp qbinp"
shows "qGoodBinp (qbinp %%[[x1  x2]]_xs)"
proof-
  {let ?qbinp' = "lift (qSwapAbs xs x1 x2) qbinp"
  fix xsa  let ?Left = "{i. ?qbinp' i  None}"
  have "?Left = {i. qbinp i  None}" by(auto simp add: lift_None)
  hence "|?Left| <o |UNIV :: 'var set|" using assms unfolding qGoodBinp_def by auto
  }
  thus ?thesis using assms 
  unfolding qGoodBinp_def qSwapBinp_def liftAll_lift_comp 
  unfolding qGoodBinp_def unfolding comp_def liftAll_def
  by (auto simp add: qSwapAbs_preserves_qGoodAbs simp del: not_None_eq)
qed

lemma qSwapInp_preserves_alphaInp:
assumes "qGoodInp qinp  qGoodInp qinp'" and "qinp %= qinp'"
shows "(qinp %[[x1  x2]]_xs) %= (qinp' %[[x1  x2]]_xs)"
using assms unfolding alphaInp_def qSwapInp_def sameDom_def liftAll2_def
by (simp add: lift_None)  
   (smt (verit) liftAll_def lift_def option.case_eq_if option.exhaust_sel 
      option.sel qGoodInp_def qSwap_preserves_alpha)

lemma qSwapBinp_preserves_alphaBinp:
assumes "qGoodBinp qbinp  qGoodBinp qbinp'" and "qbinp %%= qbinp'"
shows "(qbinp %%[[x1  x2]]_xs) %%= (qbinp' %%[[x1  x2]]_xs)"
using assms unfolding alphaBinp_def qSwapBinp_def sameDom_def liftAll2_def
by (simp add: lift_None)
   (smt (verit) liftAll_def lift_def option.case_eq_if option.exhaust_sel option.sel 
     qGoodBinp_def qSwapAbs_preserves_alphaAbs) 

lemma qPsubstInp_preserves_qGoodInp:
assumes "qGoodInp qinp" and "qGoodEnv qrho"
shows "qGoodInp (qinp %[[qrho]])"
using assms unfolding qGoodInp_def qPsubstInp_def liftAll_def
by simp (smt (verit) Collect_cong lift_def option.case_eq_if 
   option.exhaust_sel option.sel qPsubst_preserves_qGood) 

lemma qPsubstBinp_preserves_qGoodBinp:
assumes "qGoodBinp qbinp" and "qGoodEnv qrho"
shows "qGoodBinp (qbinp %%[[qrho]])"
using assms unfolding qGoodBinp_def qPsubstBinp_def liftAll_def
by simp (smt (verit) Collect_cong lift_def option.case_eq_if 
   option.exhaust_sel option.sel qPsubstAbs_preserves_qGoodAbs)  

lemma qPsubstInp_preserves_alphaInp:
assumes "qGoodInp qinp  qGoodInp qinp'" and "qGoodEnv qrho" and "qinp %= qinp'"
shows "(qinp %[[qrho]]) %= (qinp' %[[qrho]])"
using assms unfolding alphaInp_def qPsubstInp_def sameDom_def liftAll2_def
by (simp add: lift_None)
   (smt (verit) liftAll_def lift_def option.case_eq_if option.exhaust_sel 
       option.sel qGoodInp_def qPsubst_preserves_alpha1)

lemma qPsubstBinp_preserves_alphaBinp:
assumes "qGoodBinp qbinp  qGoodBinp qbinp'" and "qGoodEnv qrho" and "qbinp %%= qbinp'"
shows "(qbinp %%[[qrho]]) %%= (qbinp' %%[[qrho]])"
using assms unfolding alphaBinp_def qPsubstBinp_def sameDom_def liftAll2_def
by (simp add: lift_None)
   (smt (verit) liftAll_def lift_def option.case_eq_if option.exhaust_sel 
       option.sel qGoodBinp_def qPsubstAbs_preserves_alphaAbs1) 

lemma qFreshInp_preserves_alphaInp_aux:
assumes good: "qGoodInp qinp  qGoodInp qinp'" and alpha: "qinp %= qinp'"
and fresh: "qFreshInp xs x qinp"
shows "qFreshInp xs x qinp'"
using assms unfolding qFreshInp_def liftAll_def proof clarify
  fix i qX' assume qinp': "qinp' i = Some qX'"
  then obtain qX where qinp: "qinp i = Some qX"
  using alpha unfolding alphaInp_def sameDom_def liftAll2_def by (cases "qinp i", auto)
  hence "qGood qX  qGood qX'"
  using qinp' good unfolding qGoodInp_def liftAll_def by auto
  moreover have "qX #= qX'"
  using qinp qinp' alpha unfolding alphaInp_def sameDom_def liftAll2_def by auto
  moreover have "qFresh xs x qX"
  using fresh qinp unfolding qFreshInp_def liftAll_def by simp
  ultimately show "qFresh xs x qX'"
  using qFresh_preserves_alpha by auto
qed

lemma qFreshBinp_preserves_alphaBinp_aux:
assumes good: "qGoodBinp qbinp  qGoodBinp qbinp'" and alpha: "qbinp %%= qbinp'"
and fresh: "qFreshBinp xs x qbinp"
shows "qFreshBinp xs x qbinp'"
using assms unfolding qFreshBinp_def liftAll_def proof clarify
  fix i qA' assume qbinp': "qbinp' i = Some qA'"
  then obtain qA where qbinp: "qbinp i = Some qA"
  using alpha unfolding alphaBinp_def sameDom_def liftAll2_def by (cases "qbinp i", auto)
  hence "qGoodAbs qA  qGoodAbs qA'"
  using qbinp' good unfolding qGoodBinp_def liftAll_def by auto
  moreover have "qA $= qA'"
  using qbinp qbinp' alpha unfolding alphaBinp_def sameDom_def liftAll2_def by auto
  moreover have "qFreshAbs xs x qA"
  using fresh qbinp unfolding qFreshBinp_def liftAll_def by simp
  ultimately show "qFreshAbs xs x qA'"
  using qFreshAbs_preserves_alphaAbs by auto
qed

lemma qFreshInp_preserves_alphaInp:
assumes "qGoodInp qinp  qGoodInp qinp'" and "qinp %= qinp'"
shows "qFreshInp xs x qinp  qFreshInp xs x qinp'"
using alphaInp_sym assms qFreshInp_preserves_alphaInp_aux by blast
 
lemma qFreshBinp_preserves_alphaBinp:
assumes "qGoodBinp qbinp  qGoodBinp qbinp'" and "qbinp %%= qbinp'"
shows "qFreshBinp xs x qbinp  qFreshBinp xs x qbinp'"
using alphaBinp_sym assms qFreshBinp_preserves_alphaBinp_aux by blast
 

(****************************************************)
lemmas qItem_simps =
qSkelAll_simps qFreshAll_simps qSwapAll_simps qPsubstAll_simps qGoodAll_simps alphaAll_Simps
qSwap_qAFresh_otherSimps qAFresh.simps qGoodItem.simps
(****************************************************)

end (* context FixVars *)

subsection ‹Definitions of terms and their operators›

type_synonym ('index,'bindex,'varSort,'var,'opSym)"term" =
      "('index,'bindex,'varSort,'var,'opSym)qTerm set"

type_synonym ('index,'bindex,'varSort,'var,'opSym)abs =
      "('index,'bindex,'varSort,'var,'opSym)qAbs set"

type_synonym ('index,'bindex,'varSort,'var,'opSym)env =
      "'varSort  'var  ('index,'bindex,'varSort,'var,'opSym)term option"

text‹A ``parameter" will be something for which
freshness makes sense.  Here is the most typical case of a parameter in proofs, putting
together (as lists) finite collections of variables, terms, abstractions and environments:›

datatype ('index,'bindex,'varSort,'var,'opSym)param =
  Par "'var list"
      "('index,'bindex,'varSort,'var,'opSym)term list"
      "('index,'bindex,'varSort,'var,'opSym)abs list"
      "('index,'bindex,'varSort,'var,'opSym)env list"

fun varsOf where
"varsOf (Par xL _ _ _) = set xL"

fun termsOf where
"termsOf (Par _ XL _ _) = set XL"

fun absOf where
"absOf (Par _ _ AL _) = set AL"

fun envsOf where
"envsOf (Par _ _ _ rhoL) = set rhoL"

context FixVars  (* scope all throughout the file *)
begin

(* Recall the abbreviation "Restr r qA" for "r Int (qA <*> qA)"  *)
definition "alphaGood  λ qX qY. qGood qX  qGood qY  qX #= qY"
definition "alphaAbsGood  λ qA qB. qGoodAbs qA  qGoodAbs qB  qA $= qB"

definition "good  qGood /// alphaGood"
definition "goodAbs  qGoodAbs /// alphaAbsGood"

definition goodInp where
"goodInp inp ==
 liftAll good inp 
 |{i. inp i  None}| <o |UNIV :: 'var set|"

definition goodBinp where
"goodBinp binp ==
 liftAll goodAbs binp 
 |{i. binp i  None}| <o |UNIV :: 'var set|"

definition goodEnv where
"goodEnv rho ==
 ( ys. liftAll good (rho ys)) 
 ( ys. |{y. rho ys y  None}| <o |UNIV :: 'var set| )"

definition asTerm where
"asTerm qX  proj alphaGood qX"

definition asAbs where
"asAbs qA  proj alphaAbsGood qA"

definition pickInp where
"pickInp inp  lift pick inp"

definition pickBinp where
"pickBinp binp  lift pick binp"

(* Note: pickInp and pickBinp are the same (polymorphically), but
  I keep distinct notations for uniformity with the rest of the notations. *)

definition asInp where
"asInp qinp  lift asTerm qinp"

definition asBinp where
"asBinp qbinp  lift asAbs qbinp"

definition pickE where
"pickE rho  λ xs. lift pick (rho xs)" 

definition asEnv where
"asEnv qrho  λ xs. lift asTerm (qrho xs)"

definition Var where
"Var xs x  asTerm(qVar xs x)"

definition Op where
"Op delta inp binp  asTerm (qOp delta (pickInp inp) (pickBinp binp))"

definition Abs where
"Abs xs x X  asAbs (qAbs xs x (pick X))"

definition skel where
"skel X  qSkel (pick X)"

definition skelAbs where
"skelAbs A  qSkelAbs (pick A)"

definition skelInp where
"skelInp inp = qSkelInp (pickInp inp)"

definition skelBinp where
"skelBinp binp = qSkelBinp (pickBinp binp)"

lemma skelInp_def2:
assumes "goodInp inp"
shows "skelInp inp = lift skel inp"
unfolding skelInp_def
unfolding qSkelInp_def pickInp_def skel_def[abs_def]
unfolding lift_comp comp_def by simp

lemma skelBinp_def2:
assumes "goodBinp binp"
shows "skelBinp binp = lift skelAbs binp"
unfolding skelBinp_def
unfolding qSkelBinp_def pickBinp_def skelAbs_def[abs_def]
unfolding lift_comp comp_def by simp

definition swap where
"swap xs x y X = asTerm (qSwap xs x y (pick X))"

abbreviation swap_abbrev ("_ #[_  _]'__" 200) where
"(X #[z1  z2]_zs)  swap zs z1 z2 X"

definition swapAbs where
"swapAbs xs x y A = asAbs (qSwapAbs xs x y (pick A))"

abbreviation swapAbs_abbrev ("_ $[_  _]'__" 200) where
"(A $[z1  z2]_zs)  swapAbs zs z1 z2 A"

definition swapInp where
"swapInp xs x y inp  lift (swap xs x y) inp"

definition swapBinp where
"swapBinp xs x y binp  lift (swapAbs xs x y) binp"

abbreviation swapInp_abbrev ("_ %[_  _]'__" 200) where
"(inp %[z1  z2]_zs)  swapInp zs z1 z2 inp"

abbreviation swapBinp_abbrev ("_ %%[_  _]'__" 200) where
"(binp %%[z1  z2]_zs)  swapBinp zs z1 z2 binp"

definition swapEnvDom where
"swapEnvDom xs x y rho  λzs z. rho zs (z @zs[x  y]_xs)"

definition swapEnvIm where
"swapEnvIm xs x y rho  λzs. lift (swap xs x y) (rho zs)"

definition swapEnv where
"swapEnv xs x y  swapEnvIm xs x y o swapEnvDom xs x y"

abbreviation swapEnv_abbrev ("_ &[_  _]'__" 200) where
"(rho &[z1  z2]_zs)  swapEnv zs z1 z2 rho"

lemmas swapEnv_defs = swapEnv_def comp_def swapEnvDom_def swapEnvIm_def

inductive_set swapped where
Refl: "(X,X)  swapped"
|
Trans: "(X,Y)  swapped; (Y,Z)  swapped  (X,Z)  swapped"
|
Swap: "(X,Y)  swapped  (X, Y #[x  y]_zs)  swapped"

lemmas swapped_Clauses = swapped.Refl swapped.Trans swapped.Swap

definition fresh where
"fresh xs x X  qFresh xs x (pick X)"

definition freshAbs where
"freshAbs xs x A  qFreshAbs xs x (pick A)"

definition freshInp where
"freshInp xs x inp  liftAll (fresh xs x) inp"

definition freshBinp where
"freshBinp xs x binp  liftAll (freshAbs xs x) binp"

definition freshEnv where
"freshEnv xs x rho ==
rho xs x = None  ( ys. liftAll (fresh xs x) (rho ys))"

definition psubst where
"psubst rho X  asTerm(qPsubst (pickE rho) (pick X))"

abbreviation psubst_abbrev ("_ #[_]") where
"(X #[rho])  psubst rho X"

definition psubstAbs where
"psubstAbs rho A  asAbs(qPsubstAbs (pickE rho) (pick A))"

abbreviation psubstAbs_abbrev  ("_ $[_]") where
"A $[rho]  psubstAbs rho A"

definition psubstInp where
"psubstInp rho inp  lift (psubst rho) inp"

definition psubstBinp where
"psubstBinp rho binp  lift (psubstAbs rho) binp"

abbreviation psubstInp_abbrev  ("_ %[_]") where
"inp %[rho]  psubstInp rho inp"

abbreviation psubstBinp_abbrev  ("_ %%[_]") where
"binp %%[rho]  psubstBinp rho binp"

definition psubstEnv where
"psubstEnv rho rho' 
 λ xs x. case rho' xs x of None  rho xs x
                          |Some X  Some (X #[rho])"

abbreviation psubstEnv_abbrev ("_ &[_]") where
"rho &[rho']  psubstEnv rho' rho"

definition idEnv where
"idEnv  λxs. Map.empty"

definition updEnv ::
"('index,'bindex,'varSort,'var,'opSym)env 
 'var  ('index,'bindex,'varSort,'var,'opSym)term  'varSort 
 ('index,'bindex,'varSort,'var,'opSym)env"
("_ [_  _]'__" 200) where
"(rho [x  X]_xs)  λ ys y. (if ys = xs  y = x then Some X else rho ys y)"

text‹(Unary) substitution:›

definition subst where
"subst xs X x  psubst (idEnv [x  X]_xs)"

abbreviation subst_abbrev ("_ #[_ '/ _]'__" 200) where
"(Y #[X / x]_xs)  subst xs X x Y"

definition substAbs where
"substAbs xs X x  psubstAbs (idEnv [x  X]_xs)"

abbreviation substAbs_abbrev ("_ $[_ '/ _]'__" 200) where
"(A $[X / x]_xs)  substAbs xs X x A"

definition substInp where
"substInp xs X x  psubstInp (idEnv [x  X]_xs)"

definition substBinp where
"substBinp xs X x  psubstBinp (idEnv [x  X]_xs)"

abbreviation substInp_abbrev ("_ %[_ '/ _]'__" 200) where
"(inp %[X / x]_xs)  substInp xs X x inp"

abbreviation substBinp_abbrev ("_ %%[_ '/ _]'__" 200) where
"(binp %%[X / x]_xs)  substBinp xs X x binp"

theorem substInp_def2:
"substInp ys Y y = lift (subst ys Y y)"
unfolding substInp_def[abs_def] subst_def psubstInp_def[abs_def] by simp

theorem substBinp_def2:
"substBinp ys Y y = lift (substAbs ys Y y)"
unfolding substBinp_def[abs_def] substAbs_def psubstBinp_def[abs_def] by simp

definition substEnv where
"substEnv xs X x  psubstEnv (idEnv [x  X]_xs)"

abbreviation substEnv_abbrev ("_ &[_ '/ _]'__" 200) where
"(Y &[X / x]_xs)  substEnv xs X x Y"

theorem substEnv_def2:
"(rho &[Y / y]_ys) =
 (λxs x. case rho xs x of
           None  if (xs = ys  x = y) then Some Y else None
          |Some X  Some (X #[Y / y]_ys))"
unfolding substEnv_def psubstEnv_def subst_def idEnv_def updEnv_def
apply(rule ext)+ by(case_tac "rho xs x", simp_all)

text‹Variable-for-variable substitution:›

definition vsubst where
"vsubst ys y1 y2  subst ys (Var ys y1) y2"

abbreviation vsubst_abbrev ("_ #[_ '/'/ _]'__" 200) where
"(X #[y1 // y2]_ys)  vsubst ys y1 y2 X"

definition vsubstAbs where
"vsubstAbs ys y1 y2  substAbs ys (Var ys y1) y2"

abbreviation vsubstAbs_abbrev ("_ $[_ '/'/ _]'__" 200) where
"(A $[y1 // y2]_ys)  vsubstAbs ys y1 y2 A"

definition vsubstInp where
"vsubstInp ys y1 y2  substInp ys (Var ys y1) y2"

definition vsubstBinp where
"vsubstBinp ys y1 y2  substBinp ys (Var ys y1) y2"

abbreviation vsubstInp_abbrev ("_ %[_ '/'/ _]'__" 200) where
"(inp %[y1 // y2]_ys)  vsubstInp ys y1 y2 inp"

abbreviation vsubstBinp_abbrev ("_ %%[_ '/'/ _]'__" 200) where
"(binp %%[y1 // y2]_ys)  vsubstBinp ys y1 y2 binp"

lemma vsubstInp_def2:
"(inp %[y1 // y2]_ys) = lift (vsubst ys y1 y2) inp"
unfolding vsubstInp_def vsubst_def
by(auto simp add: substInp_def2)

lemma vsubstBinp_def2:
"(binp %%[y1 // y2]_ys) = lift (vsubstAbs ys y1 y2) binp"
unfolding vsubstBinp_def vsubstAbs_def
by(auto simp add: substBinp_def2)

definition vsubstEnv where
"vsubstEnv ys y1 y2  substEnv ys (Var ys y1) y2"

abbreviation vsubstEnv_abbrev ("_ &[_ '/'/ _]'__" 200) where
"(rho &[y1 // y2]_ys)  vsubstEnv ys y1 y2 rho"

theorem vsubstEnv_def2:
"(rho &[y1 // y]_ys) =
 (λxs x. case rho xs x of
           None  if (xs = ys  x = y) then Some (Var ys y1) else None
          |Some X  Some (X #[y1 // y]_ys))"
unfolding vsubstEnv_def vsubst_def by(auto simp add: substEnv_def2)

definition goodPar where
"goodPar P  ( X  termsOf P. good X) 
              ( A  absOf P. goodAbs A) 
              ( rho  envsOf P. goodEnv rho)"

lemma Par_preserves_good[simp]:
assumes "!! X. X  set XL  good X"
and "!! A. A  set AL   goodAbs A"
and "!! rho. rho  set rhoL  goodEnv rho"
shows "goodPar (Par xL XL AL rhoL)"
using assms unfolding goodPar_def by auto

lemma termsOf_preserves_good[simp]:
assumes "goodPar P" and "X : termsOf P"
shows "good X"
using assms unfolding goodPar_def by auto

lemma absOf_preserves_good[simp]:
assumes "goodPar P" and "A : absOf P"
shows "goodAbs A"
using assms unfolding goodPar_def by auto

lemma envsOf_preserves_good[simp]:
assumes "goodPar P" and "rho : envsOf P"
shows "goodEnv rho"
using assms unfolding goodPar_def by blast

lemmas param_simps =
termsOf.simps absOf.simps envsOf.simps
Par_preserves_good
termsOf_preserves_good absOf_preserves_good envsOf_preserves_good

subsection ‹Items versus quasi-items modulo alpha›

text‹Here we ``close the accounts" (for a while) with quasi-items  --
 beyond this subsection, there will not be any theorem that mentions
 quasi-items, except much later when we deal with iteration principles
 (and need to briefly switch back to quasi-terms in order to define the needed
 iterative map by the universality of the alpha-quotient).›

subsubsection ‹For terms›

lemma alphaGood_equivP: "equivP qGood alphaGood"
unfolding equivP_def reflP_def symP_def transP_def alphaGood_def
using alpha_refl alpha_sym alpha_trans by blast

lemma univ_asTerm_alphaGood[simp]:
assumes *: "congruentP alphaGood f" and **: "qGood X"
shows "univ f (asTerm X) = f X"
by (metis assms alphaGood_equivP asTerm_def univ_commute)

corollary univ_asTerm_alpha[simp]:
assumes *: "congruentP alpha f" and **: "qGood X"
shows "univ f (asTerm X) = f X"
apply(rule univ_asTerm_alphaGood)
using assms unfolding alphaGood_def congruentP_def by auto

lemma pick_inj_on_good: "inj_on pick (Collect good)"
unfolding good_def using alphaGood_equivP equivP_pick_inj_on by auto

lemma pick_injective_good[simp]:
"good X; good Y  (pick X = pick Y) = (X = Y)"
using pick_inj_on_good unfolding inj_on_def by auto

lemma good_imp_qGood_pick:
"good X  qGood (pick X)"
unfolding good_def
by (metis alphaGood_equivP equivP_pick_preserves)

lemma qGood_iff_good_asTerm:
"good (asTerm qX) = qGood qX"
unfolding good_def asTerm_def
using alphaGood_equivP proj_in_iff by fastforce

lemma pick_asTerm:
assumes "qGood qX"
shows "pick (asTerm qX) #= qX"
by (metis (full_types) alphaGood_def alphaGood_equivP asTerm_def assms pick_proj)

lemma asTerm_pick:
assumes "good X"
shows "asTerm (pick X) = X"
by (metis alphaGood_equivP asTerm_def assms good_def proj_pick)

lemma pick_alpha: "good X  pick X #= pick X"
using good_imp_qGood_pick alpha_refl by auto

lemma alpha_imp_asTerm_equal:
assumes "qGood qX" and "qX #= qY"
shows "asTerm qX = asTerm qY"
proof-
  have "alphaGood qX qY" unfolding alphaGood_def using assms
  by (metis alpha_preserves_qGood)
  thus ?thesis unfolding asTerm_def using alphaGood_equivP proj_iff
  by (metis alpha_preserves_qGood1 assms)
qed

lemma asTerm_equal_imp_alpha:
assumes "qGood qX" and "asTerm qX = asTerm qY"
shows "qX #= qY"
by (metis alphaAll_sym alphaAll_trans assms pick_asTerm qGood_iff_good_asTerm)

lemma asTerm_equal_iff_alpha:
assumes "qGood qX  qGood qY"
shows "(asTerm qX = asTerm qY) = (qX #= qY)"
by (metis alpha_imp_asTerm_equal alpha_sym asTerm_equal_imp_alpha assms)

lemma pick_alpha_iff_equal:
assumes "good X" and "good Y"
shows "pick X #= pick Y  X = Y"
by (metis asTerm_equal_iff_alpha asTerm_pick assms good_imp_qGood_pick)

lemma pick_swap_qSwap:
assumes "good X"
shows "pick (X #[x1  x2]_xs) #= ((pick X) #[[x1  x2]]_xs)"
by (metis assms good_imp_qGood_pick pick_asTerm qSwap_preserves_qGood1 swap_def)

lemma asTerm_qSwap_swap:
assumes "qGood qX"
shows "asTerm (qX #[[x1  x2]]_xs) = ((asTerm qX) #[x1  x2]_xs)"
 by (simp add: alpha_imp_asTerm_equal alpha_sym assms local.swap_def 
pick_asTerm qSwap_preserves_alpha qSwap_preserves_qGood1) 

lemma fresh_asTerm_qFresh:
assumes "qGood qX"
shows "fresh xs x (asTerm qX) = qFresh xs x qX"
by (simp add: assms fresh_def pick_asTerm qFresh_preserves_alpha)
 
(* Note that fresh and skel commute with pick by definition, so we only need
  to prove they commute with asTerm.  *)

lemma skel_asTerm_qSkel:
assumes "qGood qX"
shows "skel (asTerm qX) = qSkel qX"
by (simp add: alpha_qSkel assms pick_asTerm skel_def)
 
lemma double_swap_qSwap:
assumes "good X"
shows "qGood (((pick X) #[[x  y]]_zs) #[[x'  y']]_zs') 
       ((X #[x  y]_zs) #[x'  y']_zs') = asTerm (((pick X) #[[x  y]]_zs) #[[x'  y']]_zs')"
by (simp add: asTerm_qSwap_swap assms 
    good_imp_qGood_pick local.swap_def qSwap_preserves_qGood1)

lemma fresh_swap_qFresh_qSwap:
assumes "good X"
shows "fresh xs x (X #[y1  y2]_ys) = qFresh xs x ((pick X) #[[y1  y2]]_ys)"
by (simp add: assms 
    fresh_asTerm_qFresh good_imp_qGood_pick local.swap_def qSwap_preserves_qGood)

subsubsection ‹For abstractions›

lemma alphaAbsGood_equivP: "equivP qGoodAbs alphaAbsGood"
unfolding equivP_def reflP_def symP_def transP_def alphaAbsGood_def
using alphaAbs_refl alphaAbs_sym alphaAbs_trans by blast

lemma univ_asAbs_alphaAbsGood[simp]:
assumes "fAbs respectsP alphaAbsGood" and "qGoodAbs A"
shows "univ fAbs (asAbs A) = fAbs A"
by (metis assms alphaAbsGood_equivP asAbs_def univ_commute)

corollary univ_asAbs_alphaAbs[simp]:
assumes *: "fAbs respectsP alphaAbs" and **: "qGoodAbs A"
shows "univ fAbs (asAbs A) = fAbs A"
apply(rule univ_asAbs_alphaAbsGood)
using assms unfolding alphaAbsGood_def congruentP_def by auto

lemma pick_inj_on_goodAbs: "inj_on pick (Collect goodAbs)"
unfolding goodAbs_def using alphaAbsGood_equivP equivP_pick_inj_on by auto

lemma pick_injective_goodAbs[simp]:
"goodAbs A; goodAbs B  pick A = pick B  A = B"
using pick_inj_on_goodAbs unfolding inj_on_def by auto

lemma goodAbs_imp_qGoodAbs_pick:
"goodAbs A  qGoodAbs (pick A)"
unfolding goodAbs_def
using alphaAbsGood_equivP equivP_pick_preserves by fastforce

lemma qGoodAbs_iff_goodAbs_asAbs:
"goodAbs(asAbs qA) = qGoodAbs qA"
unfolding goodAbs_def asAbs_def
using alphaAbsGood_equivP proj_in_iff by fastforce

lemma pick_asAbs:
assumes "qGoodAbs qA"
shows "pick (asAbs qA) $= qA"
by (metis (full_types) alphaAbsGood_def alphaAbsGood_equivP asAbs_def assms pick_proj)

lemma asAbs_pick:
assumes "goodAbs A"
shows "asAbs (pick A) = A"
by (metis alphaAbsGood_equivP asAbs_def assms goodAbs_def proj_pick)

lemma pick_alphaAbs: "goodAbs A  pick A $= pick A"
using goodAbs_imp_qGoodAbs_pick alphaAbs_refl by auto

lemma alphaAbs_imp_asAbs_equal:
assumes "qGoodAbs qA" and "qA $= qB"
shows "asAbs qA = asAbs qB"
by (metis (no_types, opaque_lifting) proj_iff alphaAbsGood_def alphaAbsGood_equivP 
 alphaAbs_preserves_qGoodAbs asAbs_def assms)

lemma asAbs_equal_imp_alphaAbs:
assumes "qGoodAbs qA" and "asAbs qA = asAbs qB"
shows "qA $= qB"
by (metis alphaAbs_refl 
  alphaAbs_sym alphaAbs_trans_twice assms pick_asAbs qGoodAbs_iff_goodAbs_asAbs)
 
lemma asAbs_equal_iff_alphaAbs:
assumes "qGoodAbs qA  qGoodAbs qB"
shows "(asAbs qA = asAbs qB) = (qA $= qB)"
by (metis alphaAbs_imp_asAbs_equal alphaAbs_preserves_qGoodAbs 
 asAbs_equal_imp_alphaAbs assms) 

lemma pick_alphaAbs_iff_equal:
assumes "goodAbs A" and "goodAbs B"
shows "(pick A $= pick B) = (A = B)"
using asAbs_equal_iff_alphaAbs asAbs_pick assms goodAbs_imp_qGoodAbs_pick by blast

lemma pick_swapAbs_qSwapAbs:
assumes "goodAbs A"
shows "pick (A $[x1  x2]_xs) $= ((pick A) $[[x1  x2]]_xs)"
by (simp add: assms goodAbs_imp_qGoodAbs_pick 
 pick_asAbs qSwapAbs_preserves_qGoodAbs swapAbs_def)
 
lemma asAbs_qSwapAbs_swapAbs:
assumes "qGoodAbs qA"
shows "asAbs (qA $[[x1  x2]]_xs) = ((asAbs qA) $[x1  x2]_xs)"
 by (simp add: alphaAbs_imp_asAbs_equal alphaAbs_sym assms pick_asAbs 
   qSwapAbs_preserves_alphaAbs 
  qSwapAbs_preserves_qGoodAbs1 swapAbs_def)

lemma freshAbs_asAbs_qFreshAbs:
assumes "qGoodAbs qA"
shows "freshAbs xs x (asAbs qA) = qFreshAbs xs x qA"
by (simp add: assms freshAbs_def pick_asAbs qFreshAbs_preserves_alphaAbs)

lemma skelAbs_asAbs_qSkelAbs:
assumes "qGoodAbs qA"
shows "skelAbs (asAbs qA) = qSkelAbs qA"
by (simp add: alphaAll_qSkelAll assms pick_asAbs skelAbs_def)

subsubsection ‹For inputs›

text ‹For unbound inputs:›

lemma pickInp_inj_on_goodInp: "inj_on pickInp (Collect goodInp)"
unfolding pickInp_def[abs_def] inj_on_def  
proof(safe, rule ext)
  fix inp inp' i
  assume good: "goodInp inp" "goodInp inp'" and *: "lift pick inp = lift pick inp'"
  show "inp i = inp' i"
  proof(cases "inp i")
    assume inp: "inp i = None"
    hence "lift pick inp i = None" by (auto simp add: lift_None)
    hence "lift pick inp' i = None" using * by simp
    hence "inp' i = None" by (auto simp add: lift_None)
    thus ?thesis using inp by simp
  next
    fix X assume inp: "inp i = Some X"
    hence "lift pick inp i = Some (pick X)" unfolding lift_def by simp
    hence "lift pick inp' i = Some (pick X)" using * by simp
    then obtain X' where inp': "inp' i = Some X'" and XX': "pick X = pick X'"
    unfolding lift_def by(cases "inp' i", auto)
    hence "good X  good X'"
    using inp good goodInp_def liftAll_def by (metis (opaque_lifting, full_types))
    hence "X = X'" using XX' by auto
    thus ?thesis unfolding inp inp' by simp
  qed
qed

lemma goodInp_imp_qGoodInp_pickInp:
assumes "goodInp inp"
shows "qGoodInp (pickInp inp)"
unfolding pickInp_def qGoodInp_def liftAll_def  
proof safe
  fix i qX assume "lift pick inp i = Some qX"
  then obtain X where inp: "inp i = Some X" and qX: "qX = pick X"
  unfolding lift_def by(cases "inp i", auto)
  hence "good X" using assms
  unfolding goodInp_def liftAll_def by simp
  thus "qGood qX" unfolding qX using good_imp_qGood_pick by auto
next
  fix xs   let ?Left = "{i. lift pick inp i  None}"
  have "?Left = {i. inp i  None}" by(force simp add: lift_None)
  thus "|?Left| <o |UNIV :: 'var set|" using assms unfolding goodInp_def by auto
qed

lemma qGoodInp_iff_goodInp_asInp:
"goodInp (asInp qinp) = qGoodInp qinp"
proof(unfold asInp_def)
  let ?inp = "lift asTerm qinp"
  {assume qgood_qinp: "qGoodInp qinp"
   have "goodInp ?inp"
   unfolding goodInp_def liftAll_def proof safe
     fix i X assume inp: "?inp i = Some X"
     then obtain qX where qinp: "qinp i = Some qX" and X: "X = asTerm qX"
     unfolding lift_def by(cases "qinp i", auto)
     hence "qGood qX"
     using qgood_qinp unfolding qGoodInp_def liftAll_def by auto
     thus "good X" using X qGood_iff_good_asTerm by auto
   next
     fix xs let ?Left = "{i. lift asTerm qinp i  None}"
     have "?Left = {i. qinp i  None}" by(auto simp add: lift_None)
     thus "|?Left| <o |UNIV :: 'var set|" using qgood_qinp unfolding qGoodInp_def by auto
   qed
  }
  moreover
  {assume good_inp: "goodInp ?inp"
   have "qGoodInp qinp"
   unfolding qGoodInp_def liftAll_def proof safe
     fix i qX assume qinp: "qinp i = Some qX"  let ?X = "asTerm qX"
     have inp: "?inp i = Some ?X" unfolding lift_def using qinp by simp
     hence "good ?X"
     using good_inp unfolding goodInp_def liftAll_def by auto
     thus "qGood qX" using qGood_iff_good_asTerm by auto
   next
     fix xs let ?Left = "{i. qinp i  None}"
     have "?Left = {i. lift asTerm qinp i  None}" by(auto simp add: lift_None)
     thus "|?Left| <o |UNIV :: 'var set|" using good_inp unfolding goodInp_def by auto
   qed
  }
  ultimately show "goodInp ?inp = qGoodInp qinp" by blast
qed

lemma pickInp_asInp:
assumes "qGoodInp qinp"
shows "pickInp (asInp qinp) %= qinp"
using assms unfolding pickInp_def asInp_def lift_comp  
by (smt (verit) CollectI alphaInp_def asTerm_equal_iff_alpha asTerm_pick case_prodI comp_apply liftAll2_def liftAll_def lift_def option.case(2) option.sel qGoodInp_def qGood_iff_good_asTerm 
sameDom_lift2)

lemma asInp_pickInp:
assumes "goodInp inp"
shows "asInp (pickInp inp) = inp"
unfolding asInp_def pickInp_def lift_comp
proof(rule ext)
  fix i  show "lift (asTerm  pick) inp i = inp i"
  unfolding lift_def proof(cases "inp i", simp+)
    fix X assume "inp i = Some X"
    hence "good X" using assms unfolding goodInp_def liftAll_def by simp
    thus "asTerm (pick X) = X" using asTerm_pick by auto
  qed   
qed

lemma pickInp_alphaInp:
assumes goodInp: "goodInp inp"
shows "pickInp inp %= pickInp inp"
using assms goodInp_imp_qGoodInp_pickInp alphaInp_refl by auto

lemma alphaInp_imp_asInp_equal:
assumes "qGoodInp qinp" and "qinp %= qinp'"
shows "asInp qinp = asInp qinp'"
unfolding asInp_def proof(rule ext)
  fix i show "lift asTerm qinp i = lift asTerm qinp' i"
  proof(cases "qinp i")
    assume Case1: "qinp i = None"
    hence "qinp' i = None"
    using assms unfolding alphaInp_def sameDom_def liftAll2_def by auto
    thus ?thesis using Case1 unfolding lift_def by simp
  next
    fix qX assume Case2: "qinp i = Some qX"
    then obtain qX' where qinp': "qinp' i = Some qX'"
    using assms unfolding alphaInp_def sameDom_def liftAll2_def by (cases "qinp' i", force)
    hence "qX #= qX'"
    using assms Case2 unfolding alphaInp_def sameDom_def liftAll2_def by auto
    moreover have "qGood qX" using assms Case2 unfolding qGoodInp_def liftAll_def by auto
    ultimately show ?thesis
    using Case2 qinp' alpha_imp_asTerm_equal unfolding lift_def by auto
  qed
qed

lemma asInp_equal_imp_alphaInp:
assumes "qGoodInp qinp" and "asInp qinp = asInp qinp'"
shows "qinp %= qinp'"
using assms unfolding alphaInp_def liftAll2_def sameDom_def
by simp (smt (verit) asInp_def asTerm_equal_iff_alpha liftAll_def lift_def option.case(2) 
  option.sel qGoodInp_def sameDom_def sameDom_lift2)  

lemma asInp_equal_iff_alphaInp:
"qGoodInp qinp  (asInp qinp = asInp qinp') = (qinp %= qinp')"
using asInp_equal_imp_alphaInp alphaInp_imp_asInp_equal by blast

lemma pickInp_alphaInp_iff_equal:
assumes "goodInp inp" and "goodInp inp'"
shows "(pickInp inp %= pickInp inp') = (inp = inp')"
by (metis alphaInp_imp_asInp_equal asInp_equal_imp_alphaInp 
 asInp_pickInp assms goodInp_imp_qGoodInp_pickInp)

lemma pickInp_swapInp_qSwapInp:
assumes "goodInp inp"
shows "pickInp (inp %[x1  x2]_xs) %= ((pickInp inp) %[[x1  x2]]_xs)"
using assms unfolding alphaInp_def sameDom_def liftAll2_def 
pickInp_def swapInp_def qSwapInp_def lift_comp
by (simp add: lift_None)  
(smt (verit) assms comp_apply goodInp_imp_qGoodInp_pickInp liftAll_def lift_def local.swap_def option.case_eq_if option.sel option.simps(3) pickInp_def 
pick_asTerm qGoodInp_def qSwap_preserves_qGood1) 

lemma asInp_qSwapInp_swapInp:
assumes "qGoodInp qinp"
shows "asInp (qinp %[[x1  x2]]_xs) = ((asInp qinp) %[x1  x2]_xs)"
proof- 
  {fix i qX assume "qinp i = Some qX"
  hence "qGood qX" using assms unfolding qGoodInp_def liftAll_def by auto
  hence "asTerm (qX #[[x1  x2]]_xs) = swap xs x1 x2 (asTerm qX)"
  by(auto simp add: asTerm_qSwap_swap)
  }
  thus ?thesis
  using assms 
  by (smt (verit) asInp_def comp_apply lift_comp lift_cong qSwapInp_def swapInp_def)
qed

lemma swapInp_def2:
"(inp %[x1  x2]_xs) = asInp ((pickInp inp) %[[x1  x2]]_xs)"
unfolding swapInp_def asInp_def pickInp_def qSwapInp_def lift_def swap_def
apply(rule ext) subgoal for i by (cases "inp i") auto .

lemma freshInp_def2:
"freshInp xs x inp = qFreshInp xs x (pickInp inp)"
unfolding freshInp_def qFreshInp_def pickInp_def lift_def fresh_def liftAll_def
apply(rule iff_allI) subgoal for i by (cases "inp i") auto . 

text ‹For bound inputs:›

lemma pickBinp_inj_on_goodBinp: "inj_on pickBinp (Collect goodBinp)"
unfolding pickBinp_def[abs_def] inj_on_def 
proof(safe, rule ext)
  fix binp binp' i
  assume good: "goodBinp binp" "goodBinp binp'" and *: "lift pick binp = lift pick binp'"
  show "binp i = binp' i"
  proof(cases "binp i")
    assume binp: "binp i = None"
    hence "lift pick binp i = None" by (auto simp add: lift_None)
    hence "lift pick binp' i = None" using * by simp
    hence "binp' i = None" by (auto simp add: lift_None)
    thus ?thesis using binp by simp
  next
    fix A assume binp: "binp i = Some A"
    hence "lift pick binp i = Some (pick A)" unfolding lift_def by simp
    hence "lift pick binp' i = Some (pick A)" using * by simp
    then obtain A' where binp': "binp' i = Some A'" and AA': "pick A = pick A'"
    unfolding lift_def by(cases "binp' i", auto)
    hence "goodAbs A  goodAbs A'"
    using binp good goodBinp_def liftAll_def by (metis (opaque_lifting, full_types))
    hence "A = A'" using AA' by auto
    thus ?thesis unfolding binp binp' by simp
  qed
qed

lemma goodBinp_imp_qGoodBinp_pickBinp:
assumes "goodBinp binp"
shows "qGoodBinp (pickBinp binp)"
unfolding pickBinp_def qGoodBinp_def liftAll_def proof safe
  fix i qA assume "lift pick binp i = Some qA"
  then obtain A where binp: "binp i = Some A" and qA: "qA = pick A"
  unfolding lift_def by(cases "binp i", auto)
  hence "goodAbs A" using assms
  unfolding goodBinp_def liftAll_def by simp
  thus "qGoodAbs qA" unfolding qA using goodAbs_imp_qGoodAbs_pick by auto
next
  fix xs   let ?Left = "{i. lift pick binp i  None}"
  have "?Left = {i. binp i  None}" by(force simp add: lift_None)
  thus "|?Left| <o |UNIV :: 'var set|" using assms unfolding goodBinp_def by auto
qed

lemma qGoodBinp_iff_goodBinp_asBinp:
"goodBinp (asBinp qbinp) = qGoodBinp qbinp"
proof(unfold asBinp_def)
  let ?binp = "lift asAbs qbinp"
  {assume qgood_qbinp: "qGoodBinp qbinp"
   have "goodBinp ?binp"
   unfolding goodBinp_def liftAll_def proof safe
     fix i A assume binp: "?binp i = Some A"
     then obtain qA where qbinp: "qbinp i = Some qA" and A: "A = asAbs qA"
     unfolding lift_def by(cases "qbinp i", auto)
     hence "qGoodAbs qA"
     using qgood_qbinp unfolding qGoodBinp_def liftAll_def by auto
     thus "goodAbs A" using A qGoodAbs_iff_goodAbs_asAbs by auto
   next
     fix xs let ?Left = "{i. lift asAbs qbinp i  None}"
     have "?Left = {i. qbinp i  None}" by(auto simp add: lift_None)
     thus "|?Left| <o |UNIV :: 'var set|" using qgood_qbinp unfolding qGoodBinp_def by auto
   qed
  }
  moreover
  {assume good_binp: "goodBinp ?binp"
   have "qGoodBinp qbinp"
   unfolding qGoodBinp_def liftAll_def proof safe
     fix i qA assume qbinp: "qbinp i = Some qA"  let ?A = "asAbs qA"
     have binp: "?binp i = Some ?A" unfolding lift_def using qbinp by simp
     hence "goodAbs ?A"
     using good_binp unfolding goodBinp_def liftAll_def by auto
     thus "qGoodAbs qA" using qGoodAbs_iff_goodAbs_asAbs by auto
   next
     fix xs let ?Left = "{i. qbinp i  None}"
     have "?Left = {i. lift asAbs qbinp i  None}" by(auto simp add: lift_None)
     thus "|?Left| <o |UNIV :: 'var set|" using good_binp unfolding goodBinp_def by auto
   qed
  }
  ultimately show "goodBinp ?binp = qGoodBinp qbinp" by blast
qed

lemma pickBinp_asBinp:
assumes "qGoodBinp qbinp"
shows "pickBinp (asBinp qbinp) %%= qbinp"
unfolding pickBinp_def asBinp_def lift_comp alphaBinp_def using sameDom_lift2  
by auto (smt (verit) assms comp_apply liftAll2_def liftAll_def 
lift_def option.sel option.simps(5) pick_asAbs qGoodBinp_def)

lemma asBinp_pickBinp:
assumes "goodBinp binp"
shows "asBinp (pickBinp binp) = binp"
unfolding asBinp_def pickBinp_def lift_comp 
apply(rule ext)
subgoal for i apply(cases "binp i") 
using assms asAbs_pick unfolding goodBinp_def liftAll_def lift_def by auto .

lemma pickBinp_alphaBinp:
assumes goodBinp: "goodBinp binp"
shows "pickBinp binp %%= pickBinp binp"
using assms goodBinp_imp_qGoodBinp_pickBinp alphaBinp_refl by auto

lemma alphaBinp_imp_asBinp_equal:
assumes "qGoodBinp qbinp" and "qbinp %%= qbinp'"
shows "asBinp qbinp = asBinp qbinp'"
unfolding asBinp_def proof(rule ext)
  fix i show "lift asAbs qbinp i = lift asAbs qbinp' i"
  proof(cases "qbinp i") 
    case None
    hence "qbinp' i = None"
    using assms unfolding alphaBinp_def sameDom_def liftAll2_def by auto
    thus ?thesis using None unfolding lift_def by simp
  next
    case (Some qA)
    then obtain qA' where qbinp': "qbinp' i = Some qA'"
    using assms unfolding alphaBinp_def sameDom_def liftAll2_def by (cases "qbinp' i", force)
    hence "qA $= qA'"
    using assms Some unfolding alphaBinp_def sameDom_def liftAll2_def by auto
    moreover have "qGoodAbs qA" using assms Some unfolding qGoodBinp_def liftAll_def by auto
    ultimately show ?thesis
    using Some qbinp' alphaAbs_imp_asAbs_equal unfolding lift_def by auto
  qed
qed

lemma asBinp_equal_imp_alphaBinp:
assumes "qGoodBinp qbinp" and "asBinp qbinp = asBinp qbinp'"
shows "qbinp %%= qbinp'"
using assms unfolding alphaBinp_def liftAll2_def sameDom_def
by simp (smt (verit) asAbs_equal_imp_alphaAbs asBinp_def liftAll_def 
lift_None lift_def option.inject option.simps(5) qGoodBinp_def)  

lemma asBinp_equal_iff_alphaBinp:
"qGoodBinp qbinp  (asBinp qbinp = asBinp qbinp') = (qbinp %%= qbinp')"
using asBinp_equal_imp_alphaBinp alphaBinp_imp_asBinp_equal by blast

lemma pickBinp_alphaBinp_iff_equal:
assumes "goodBinp binp" and "goodBinp binp'"
shows "(pickBinp binp %%= pickBinp binp') = (binp = binp')"
using assms goodBinp_imp_qGoodBinp_pickBinp asBinp_pickBinp pickBinp_alphaBinp 
by (metis asBinp_equal_iff_alphaBinp)

lemma pickBinp_swapBinp_qSwapBinp:
assumes "goodBinp binp"
shows "pickBinp (binp %%[x1  x2]_xs) %%= ((pickBinp binp) %%[[x1  x2]]_xs)"
using assms unfolding pickBinp_def swapBinp_def qSwapBinp_def lift_comp
alphaBinp_def sameDom_def liftAll2_def  
by (simp add: goodBinp_def liftAll_def lift_def option.case_eq_if pick_swapAbs_qSwapAbs)

lemma asBinp_qSwapBinp_swapBinp:
assumes "qGoodBinp qbinp"
shows "asBinp (qbinp %%[[x1  x2]]_xs) = ((asBinp qbinp) %%[x1  x2]_xs)"
unfolding asBinp_def swapBinp_def qSwapBinp_def lift_comp alphaBinp_def lift_def
apply(rule ext) subgoal for i  apply(cases "qbinp i")
using assms asAbs_qSwapAbs_swapAbs by (fastforce simp add: liftAll_def qGoodBinp_def)+ .

lemma swapBinp_def2:
"(binp %%[x1  x2]_xs) = asBinp ((pickBinp binp) %%[[x1  x2]]_xs)"
unfolding swapBinp_def asBinp_def pickBinp_def qSwapBinp_def lift_def swapAbs_def
apply (rule ext) subgoal for i by (cases "binp i") simp_all . 

lemma freshBinp_def2:
"freshBinp xs x binp = qFreshBinp xs x (pickBinp binp)"
unfolding freshBinp_def qFreshBinp_def pickBinp_def lift_def freshAbs_def liftAll_def
apply (rule iff_allI) subgoal for i by (cases "binp i") simp_all .  

(* Note that psubstInp and psubstBinp are discussed in the next subsubsection,
about environments.  *)

subsubsection ‹For environments›

(* Remember we do not have any "quasi-swap" for environments --
   we plan to prove most of the things concerning parallel substitution
   and environments for equivPalence classes directly. *)

lemma goodEnv_imp_qGoodEnv_pickE:
assumes "goodEnv rho"
shows "qGoodEnv (pickE rho)"
unfolding qGoodEnv_def pickE_def
apply(auto simp del: "not_None_eq")
using assms good_imp_qGood_pick unfolding liftAll_lift_comp comp_def   
by (auto simp: goodEnv_def liftAll_def lift_None)   

lemma qGoodEnv_iff_goodEnv_asEnv:
"goodEnv (asEnv qrho) = qGoodEnv qrho"
unfolding asEnv_def unfolding goodEnv_def liftAll_lift_comp comp_def
by (auto simp: qGoodEnv_def lift_None liftAll_def qGood_iff_good_asTerm)

lemma pickE_asEnv:
assumes "qGoodEnv qrho"
shows "pickE (asEnv qrho) &= qrho"
using assms 
by (auto simp: lift_None liftAll_def lift_def alphaEnv_def sameDom_def liftAll2_def
pick_asTerm qGoodEnv_def pickE_def asEnv_def split: option.splits) 

lemma asEnv_pickE:
assumes "goodEnv rho"  shows "asEnv (pickE rho) xs x = rho xs x"
using assms asTerm_pick 
by (cases "rho xs x") (auto simp: goodEnv_def liftAll_def asEnv_def pickE_def lift_comp lift_def)
 
lemma pickE_alphaEnv:
assumes goodEnv: "goodEnv rho"  shows "pickE rho &= pickE rho"
using assms goodEnv_imp_qGoodEnv_pickE alphaEnv_refl by auto

lemma alphaEnv_imp_asEnv_equal:
assumes "qGoodEnv qrho" and "qrho &= qrho'"
shows "asEnv qrho = asEnv qrho'"
apply (rule ext)+ subgoal for xs x  apply(cases "qrho xs x") 
using assms asTerm_equal_iff_alpha alpha_imp_asTerm_equal 
by (auto simp add: alphaEnv_def sameDom_def asEnv_def lift_def 
    qGoodEnv_def liftAll_def liftAll2_def option.case_eq_if split: option.splits)
   blast+ .

lemma asEnv_equal_imp_alphaEnv:
assumes "qGoodEnv qrho" and "asEnv qrho = asEnv qrho'"
shows "qrho &= qrho'"
using assms unfolding alphaEnv_def sameDom_def liftAll2_def
apply (simp add: asEnv_def lift_None lift_def qGoodEnv_def liftAll_def) 
by (smt (verit) asTerm_equal_imp_alpha option.sel option.simps(5) option.case_eq_if option.distinct(1)) 

lemma asEnv_equal_iff_alphaEnv:
"qGoodEnv qrho  (asEnv qrho = asEnv qrho') = (qrho &= qrho')"
using asEnv_equal_imp_alphaEnv alphaEnv_imp_asEnv_equal by blast

lemma pickE_alphaEnv_iff_equal:
assumes "goodEnv rho" and "goodEnv rho'"
shows "(pickE rho &= pickE rho') = (rho = rho')"
proof(rule iffI, safe, (rule ext)+)
  fix xs x
  assume alpha: "pickE rho &= pickE rho'"
  have qgood_rho: "qGoodEnv (pickE rho)" using assms goodEnv_imp_qGoodEnv_pickE by auto
  have "rho xs x = asEnv (pickE rho) xs x" using assms asEnv_pickE by fastforce
  also have " = asEnv (pickE rho') xs x"
  using qgood_rho alpha alphaEnv_imp_asEnv_equal by fastforce
  also have " = rho' xs x" using assms asEnv_pickE by fastforce
  finally show "rho xs x = rho' xs x" .
next
  have "qGoodEnv(pickE rho')" using assms goodEnv_imp_qGoodEnv_pickE by auto
  thus "pickE rho' &= pickE rho'" using alphaEnv_refl by auto
qed

lemma freshEnv_def2:
"freshEnv xs x rho = qFreshEnv xs x (pickE rho)"
unfolding freshEnv_def qFreshEnv_def pickE_def lift_def fresh_def liftAll_def
apply(cases "rho xs x") 
by (auto intro!: iff_allI) (metis map_option_case map_option_eq_Some)

lemma pick_psubst_qPsubst:
assumes "good X" and "goodEnv rho"
shows "pick (X #[rho]) #= ((pick X) #[[pickE rho]])"
by (simp add: assms goodEnv_imp_qGoodEnv_pickE good_imp_qGood_pick 
              pick_asTerm psubst_def qPsubst_preserves_qGood)
 
lemma pick_psubstAbs_qPsubstAbs:
assumes "goodAbs A" and "goodEnv rho"
shows "pick (A $[rho]) $= ((pick A) $[[pickE rho]])"
by (simp add: assms goodAbs_imp_qGoodAbs_pick goodEnv_imp_qGoodEnv_pickE pick_asAbs 
   psubstAbs_def qPsubstAbs_preserves_qGoodAbs)
 
lemma pickInp_psubstInp_qPsubstInp:
assumes good: "goodInp inp" and good_rho: "goodEnv rho"
shows "pickInp (inp %[rho]) %= ((pickInp inp) %[[pickE rho]])"
using assms unfolding pickInp_def psubstInp_def qPsubstInp_def lift_comp
unfolding alphaInp_def sameDom_def liftAll2_def
by (simp add: lift_None)  
   (smt (verit) comp_apply goodEnv_imp_qGoodEnv_pickE goodInp_imp_qGoodInp_pickInp liftAll_def lift_def map_option_case map_option_eq_Some option.sel pickInp_def 
   pick_asTerm psubst_def qGoodInp_def qPsubst_preserves_qGood)

lemma pickBinp_psubstBinp_qPsubstBinp:
assumes good: "goodBinp binp" and good_rho: "goodEnv rho"
shows "pickBinp (binp %%[rho]) %%= ((pickBinp binp) %%[[pickE rho]])"
using assms unfolding pickBinp_def psubstBinp_def qPsubstBinp_def lift_comp
unfolding alphaBinp_def sameDom_def liftAll2_def
by (simp add: lift_None)  
   (smt (verit) comp_apply goodBinp_def liftAll_def lift_def map_option_case map_option_eq_Some 
        option.sel pick_psubstAbs_qPsubstAbs)

subsubsection‹The structural alpha-equivPalence maps commute with the syntactic constructs›

lemma pick_Var_qVar:
"pick (Var xs x) #= qVar xs x"
unfolding Var_def using pick_asTerm by force  

lemma Op_asInp_asTerm_qOp:
assumes "qGoodInp qinp" and "qGoodBinp qbinp"
shows "Op delta (asInp qinp) (asBinp qbinp) = asTerm (qOp delta qinp qbinp)"
using assms pickInp_asInp pickBinp_asBinp unfolding Op_def 
by(auto simp add: asTerm_equal_iff_alpha) 

lemma qOp_pickInp_pick_Op:
assumes "goodInp inp" and "goodBinp binp"
shows "qOp delta (pickInp inp) (pickBinp binp) #= pick (Op delta inp binp)"
using assms goodInp_imp_qGoodInp_pickInp goodBinp_imp_qGoodBinp_pickBinp  
unfolding Op_def using pick_asTerm alpha_sym by force

lemma Abs_asTerm_asAbs_qAbs:
assumes "qGood qX"
shows "Abs xs x (asTerm qX) = asAbs (qAbs xs x qX)"
using assms pick_asTerm qAbs_preserves_alpha unfolding Abs_def  
by(force simp add: asAbs_equal_iff_alphaAbs) 

lemma qAbs_pick_Abs:
assumes "good X"
shows "qAbs xs x (pick X) $= pick (Abs xs x X)"
using assms good_imp_qGood_pick  pick_asAbs alphaAbs_sym unfolding Abs_def by force

lemmas qItem_versus_item_simps =
univ_asTerm_alphaGood univ_asAbs_alphaAbsGood
univ_asTerm_alpha univ_asAbs_alphaAbs
pick_injective_good pick_injective_goodAbs

subsection ‹All operators preserve the ``good'' predicate›

(* Note: some facts here simply do not hold as ``iff"s.  *)

lemma Var_preserves_good[simp]:
"good(Var xs x::('index,'bindex,'varSort,'var,'opSym)term)"
by (metis Var_def qGood.simps(1) qGood_iff_good_asTerm)

lemma Op_preserves_good[simp]:
assumes "goodInp inp" and "goodBinp binp"
shows "good(Op delta inp binp)"
using assms goodInp_imp_qGoodInp_pickInp goodBinp_imp_qGoodBinp_pickBinp
qGood_iff_good_asTerm unfolding Op_def by fastforce
 
lemma Abs_preserves_good[simp]:
assumes good: "good X"
shows "goodAbs(Abs xs x X)"
using assms good_imp_qGood_pick qGoodAbs_iff_goodAbs_asAbs
unfolding Abs_def by fastforce

lemmas Cons_preserve_good =
Var_preserves_good Op_preserves_good Abs_preserves_good

lemma swap_preserves_good[simp]:
assumes "good X"
shows "good (X #[x  y]_xs)"
using assms good_imp_qGood_pick qSwap_preserves_qGood qGood_iff_good_asTerm 
unfolding swap_def by fastforce

lemma swapAbs_preserves_good[simp]:
assumes "goodAbs A"
shows "goodAbs (A $[x  y]_xs)"
using assms goodAbs_imp_qGoodAbs_pick qSwapAbs_preserves_qGoodAbs qGoodAbs_iff_goodAbs_asAbs 
unfolding swapAbs_def by fastforce

lemma swapInp_preserves_good[simp]:
assumes "goodInp inp"
shows "goodInp (inp %[x  y]_xs)"
using assms    
by (auto simp: goodInp_def lift_def swapInp_def liftAll_def split: option.splits)  

lemma swapBinp_preserves_good[simp]:
assumes "goodBinp binp"
shows "goodBinp (binp %%[x  y]_xs)"
using assms    
by (auto simp: goodBinp_def lift_def swapBinp_def liftAll_def split: option.splits) 

lemma swapEnvDom_preserves_good:
assumes "goodEnv rho"
shows "goodEnv (swapEnvDom xs x y rho)" (is "goodEnv ?rho'")
unfolding goodEnv_def liftAll_def  proof safe
  fix zs z X'  assume rho': "?rho' zs z = Some X'"
  hence "rho zs (z @zs[x  y]_xs) = Some X'" unfolding swapEnvDom_def by simp
  thus "good X'" using assms unfolding goodEnv_def liftAll_def by simp
next
  fix xsa ys  let ?Left = "{ya. ?rho' ys ya  None}"
  have "|{y}  {ya. rho ys ya  None}| <o |UNIV :: 'var set|"
  using assms var_infinite_INNER card_of_Un_singl_ordLess_infinite
  unfolding goodEnv_def by fastforce
  hence "|{x,y}  {ya. rho ys ya  None}| <o |UNIV :: 'var set|"
  using var_infinite_INNER card_of_Un_singl_ordLess_infinite by fastforce
  moreover
  {have "?Left  {x,y}  {ya. rho ys ya  None}"
   unfolding swapEnvDom_def sw_def[abs_def] by auto
   hence "|?Left| ≤o |{x,y}  {ya. rho ys ya  None}|"
   using card_of_mono1 by auto
  }
  ultimately show "|?Left| <o |UNIV :: 'var set|" using ordLeq_ordLess_trans by blast
qed 

lemma swapEnvIm_preserves_good:
assumes "goodEnv rho"
shows "goodEnv (swapEnvIm xs x y rho)"
using assms unfolding goodEnv_def swapEnvIm_def liftAll_def
by (auto simp: lift_def split: option.splits)

lemma swapEnv_preserves_good[simp]:
assumes "goodEnv rho"
shows "goodEnv (rho &[x  y]_xs)"
unfolding swapEnv_def comp_def
using assms by(auto simp add: swapEnvDom_preserves_good swapEnvIm_preserves_good)

lemmas swapAll_preserve_good =
swap_preserves_good swapAbs_preserves_good
swapInp_preserves_good swapBinp_preserves_good
swapEnv_preserves_good

lemma psubst_preserves_good[simp]:
assumes  "goodEnv rho" and "good X"
shows "good (X #[rho])"
using assms good_imp_qGood_pick goodEnv_imp_qGoodEnv_pickE  
qPsubst_preserves_qGood qGood_iff_good_asTerm unfolding psubst_def by fastforce

lemma psubstAbs_preserves_good[simp]:
assumes good_rho: "goodEnv rho" and goodAbs_A: "goodAbs A"
shows "goodAbs (A $[rho])"
using assms goodAbs_A goodAbs_imp_qGoodAbs_pick  goodEnv_imp_qGoodEnv_pickE 
qPsubstAbs_preserves_qGoodAbs qGoodAbs_iff_goodAbs_asAbs unfolding psubstAbs_def by fastforce

lemma psubstInp_preserves_good[simp]:
assumes good_rho: "goodEnv rho" and good: "goodInp inp"
shows "goodInp (inp %[rho])"
using assms unfolding goodInp_def psubstInp_def liftAll_def 
by (auto simp add: lift_def split: option.splits)

lemma psubstBinp_preserves_good[simp]:
assumes good_rho: "goodEnv rho" and good: "goodBinp binp"
shows "goodBinp (binp %%[rho])"
using assms unfolding goodBinp_def psubstBinp_def liftAll_def 
by (auto simp add: lift_def split: option.splits) 

lemma psubstEnv_preserves_good[simp]:
assumes good: "goodEnv rho" and good': "goodEnv rho'"
shows "goodEnv (rho &[rho'])"
unfolding goodEnv_def liftAll_def
proof safe
  fix zs z X'
  assume *: "(rho &[rho']) zs z = Some X'"
  show "good X'"
  proof(cases "rho zs z")
    case None
    hence "rho' zs z = Some X'" using * unfolding psubstEnv_def by auto
    thus ?thesis using good' unfolding goodEnv_def liftAll_def by auto
  next
    case (Some X)
    hence "X' = (X #[rho'])" using * unfolding psubstEnv_def by auto
    moreover have "good X" using Some good unfolding goodEnv_def liftAll_def by auto
    ultimately show ?thesis using good' psubst_preserves_good by auto
  qed
next
  fix xs ys  let ?Left = "{y. (rho &[rho']) ys y  None}"
  let ?Left1 = "{y. rho ys y  None}"  let ?Left2 = "{y. rho' ys y  None}"
  have "|?Left1| <o |UNIV :: 'var set|  |?Left2| <o |UNIV :: 'var set|"
  using good good' unfolding goodEnv_def by simp
  hence "|?Left1  ?Left2| <o |UNIV :: 'var set|"
  using var_infinite_INNER card_of_Un_ordLess_infinite by auto
  moreover
  {have "?Left  ?Left1  ?Left2" unfolding psubstEnv_def by auto
   hence "|?Left| ≤o |?Left1  ?Left2|" using card_of_mono1 by auto
  }
  ultimately show "|?Left| <o |UNIV :: 'var set|" using ordLeq_ordLess_trans by blast
qed

lemmas psubstAll_preserve_good =
psubst_preserves_good psubstAbs_preserves_good
psubstInp_preserves_good psubstBinp_preserves_good
psubstEnv_preserves_good

lemma idEnv_preserves_good[simp]: "goodEnv idEnv"
unfolding goodEnv_def idEnv_def liftAll_def
using var_infinite_INNER finite_ordLess_infinite2 by auto

lemma updEnv_preserves_good[simp]:
assumes good_X: "good X" and good_rho: "goodEnv rho"
shows "goodEnv (rho [x  X]_xs)"
using assms unfolding updEnv_def goodEnv_def liftAll_def
proof safe
  fix ys y Y
  assume "good X" and "ys y Y. rho ys y = Some Y  good Y"
  and "(if ys = xs  y = x then Some X else rho ys y) = Some Y"
  thus "good Y"
  by(cases "ys = xs  y = x") auto
next
  fix ys
  let ?V' = "{y.  (if ys = xs  y = x then Some X else rho ys y)  None}"
  let ?V = "λ ys. {y. rho ys y  None}"
  assume " ys. |?V ys| <o |UNIV :: 'var set|"
  hence "|{x}  ?V ys| <o |UNIV :: 'var set|"
  using var_infinite_INNER card_of_Un_singl_ordLess_infinite by fastforce
  moreover
  {have "?V'  {x}  ?V ys" by auto
   hence "|?V'| ≤o |{x}  ?V ys|" using card_of_mono1 by auto
  }
  ultimately show "|?V'| <o |UNIV :: 'var set|" using ordLeq_ordLess_trans by blast
qed

lemma getEnv_preserves_good[simp]:
assumes "goodEnv rho" and "rho xs x = Some X"
shows "good X"
using assms unfolding goodEnv_def liftAll_def by simp

lemmas envOps_preserve_good =
idEnv_preserves_good updEnv_preserves_good
getEnv_preserves_good

lemma subst_preserves_good[simp]:
assumes "good X" and "good Y"
shows "good (Y #[X / x]_xs)"
unfolding subst_def
using assms by simp

lemma substAbs_preserves_good[simp]:
assumes "good X" and "goodAbs A"
shows "goodAbs (A $[X / x]_xs)"
unfolding substAbs_def
using assms by simp

lemma substInp_preserves_good[simp]:
assumes "good X" and "goodInp inp"
shows "goodInp (inp %[X / x]_xs)"
unfolding substInp_def using assms by simp

lemma substBinp_preserves_good[simp]:
assumes "good X" and "goodBinp binp"
shows "goodBinp (binp %%[X / x]_xs)"
unfolding substBinp_def using assms by simp

lemma substEnv_preserves_good[simp]:
assumes "good X" and "goodEnv rho"
shows "goodEnv (rho &[X / x]_xs)"
unfolding substEnv_def using assms by simp

lemmas substAll_preserve_good =
subst_preserves_good substAbs_preserves_good
substInp_preserves_good substBinp_preserves_good
substEnv_preserves_good

lemma vsubst_preserves_good[simp]:
assumes "good Y"
shows "good (Y #[x1 // x]_xs)"
unfolding vsubst_def using assms by simp

lemma vsubstAbs_preserves_good[simp]:
assumes "goodAbs A"
shows "goodAbs (A $[x1 // x]_xs)"
unfolding vsubstAbs_def using assms by simp

lemma vsubstInp_preserves_good[simp]:
assumes "goodInp inp"
shows "goodInp (inp %[x1 // x]_xs)"
unfolding vsubstInp_def using assms by simp

lemma vsubstBinp_preserves_good[simp]:
assumes "goodBinp binp"
shows "goodBinp (binp %%[x1 // x]_xs)"
unfolding vsubstBinp_def using assms by simp

lemma vsubstEnv_preserves_good[simp]:
assumes "goodEnv rho"
shows "goodEnv (rho &[x1 // x]_xs)"
unfolding vsubstEnv_def using assms by simp

lemmas vsubstAll_preserve_good =
vsubst_preserves_good vsubstAbs_preserves_good
vsubstInp_preserves_good vsubstBinp_preserves_good
vsubstEnv_preserves_good

lemmas all_preserve_good =
Cons_preserve_good
swapAll_preserve_good
psubstAll_preserve_good
envOps_preserve_good
substAll_preserve_good
vsubstAll_preserve_good

subsubsection ‹The syntactic operators are almost constructors›

text‹The only one that does not act precisely like a constructor is ``Abs".›

theorem Var_inj[simp]:
"(((Var xs x)::('index,'bindex,'varSort,'var,'opSym)term) = Var ys y) =
 (xs = ys  x = y)"
by (metis alpha_qVar_iff pick_Var_qVar qTerm.inject)

lemma Op_inj[simp]:
assumes "goodInp inp" and "goodBinp binp"
and "goodInp inp'" and "goodBinp binp'"
shows
"(Op delta inp binp = Op delta' inp' binp') =
 (delta = delta'  inp = inp'  binp = binp')"
using assms pickInp_alphaInp_iff_equal pickBinp_alphaBinp_iff_equal 
goodInp_imp_qGoodInp_pickInp goodBinp_imp_qGoodBinp_pickBinp 
unfolding Op_def by (fastforce simp: asTerm_equal_iff_alpha) 

text‹``Abs" is almost injective (``ainj"), with almost injectivity expressed
   in two ways:
   \\- maximally, using "forall" -- this is suitable for elimination of ``Abs" equalities;
   \\- minimally, using "exists" -- this is suitable for introduction of ``Abs" equalities.
›

lemma Abs_ainj_all:
assumes good: "good X" and good': "good X'"
shows
"(Abs xs x X = Abs xs' x' X') =
 (xs = xs' 
  ( y. (y = x  fresh xs y X)  (y = x'  fresh xs y X') 
        (X #[y  x]_xs) = (X' #[y  x']_xs)))"
proof-
  let ?qX = "pick X"  let ?qX' = "pick X'"
  have qgood: "qGood ?qX  qGood ?qX'" using good good' good_imp_qGood_pick by auto
  hence qgood_qXyx: " y. qGood (?qX #[[y  x]]_xs)"
  using qSwap_preserves_qGood by auto
  have "qGoodAbs(qAbs xs x ?qX)" using qgood by simp
  hence "(Abs xs x X = Abs xs' x' X') = (qAbs xs x ?qX $= qAbs xs' x' ?qX')"
  unfolding Abs_def by (auto simp add: asAbs_equal_iff_alphaAbs)
  also
  have " = (xs = xs' 
             ( y. (y = x  qFresh xs y ?qX)  (y = x'  qFresh xs y ?qX') 
                   (?qX #[[y  x]]_xs) #= (?qX' #[[y  x']]_xs)))"
  using qgood alphaAbs_qAbs_iff_all_equal_or_qFresh[of ?qX ?qX'] by blast
  also
  have " = (xs = xs' 
             ( y. (y = x  fresh xs y X)  (y = x'  fresh xs y X') 
                   (X #[y  x]_xs) = (X' #[y  x']_xs)))"
  unfolding fresh_def swap_def using qgood_qXyx by (auto simp add: asTerm_equal_iff_alpha)
  finally show ?thesis .
qed

lemma Abs_ainj_ex:
assumes good: "good X" and good': "good X'"
shows
"(Abs xs x X = Abs xs' x' X') =
 (xs = xs' 
  ( y. y  {x,x'}  fresh xs y X  fresh xs y X' 
        (X #[y  x]_xs) = (X' #[y  x']_xs)))"
proof-
  let ?qX = "pick X"  let ?qX' = "pick X'"
  have qgood: "qGood ?qX  qGood ?qX'" using good good' good_imp_qGood_pick by auto
  hence qgood_qXyx: " y. qGood (?qX #[[y  x]]_xs)"
  using qSwap_preserves_qGood by auto
  have "qGoodAbs(qAbs xs x ?qX)" using qgood by simp
  hence "(Abs xs x X = Abs xs' x' X') = (qAbs xs x ?qX $= qAbs xs' x' ?qX')"
  unfolding Abs_def by (auto simp add: asAbs_equal_iff_alphaAbs)
  also
  have " =  (xs = xs' 
              ( y. y  {x,x'}  qFresh xs y ?qX  qFresh xs y ?qX' 
                    (?qX #[[y  x]]_xs) #= (?qX' #[[y  x']]_xs)))"
  using qgood alphaAbs_qAbs_iff_ex_distinct_qFresh[of ?qX xs x xs' x' ?qX'] by blast
  also
  have " =  (xs = xs' 
               ( y. y  {x,x'}  fresh xs y X  fresh xs y X' 
                     (X #[y  x]_xs) = (X' #[y  x']_xs)))"
  unfolding fresh_def swap_def using qgood_qXyx asTerm_equal_iff_alpha by auto
  finally show ?thesis .
qed

lemma Abs_cong[fundef_cong]:
assumes good: "good X" and good': "good X'"
and y: "fresh xs y X" and y': "fresh xs y X'"
and eq: "(X #[y  x]_xs) = (X' #[y  x']_xs)"
shows "Abs xs x X = Abs xs x' X'"
proof-
  let ?qX = "pick X"  let ?qX' = "pick X'"
  have qgood: "qGood ?qX  qGood ?qX'" using good good' good_imp_qGood_pick by auto
  hence qgood_qXyx: " y. qGood (?qX #[[y  x]]_xs)"
  using qSwap_preserves_qGood by auto
  have qEq: "(?qX #[[y  x]]_xs) #= (?qX' #[[y  x']]_xs)"
  using eq unfolding fresh_def swap_def
  using qgood_qXyx asTerm_equal_iff_alpha by auto
  have "(qAbs xs x ?qX $= qAbs xs x' ?qX')"
  apply(rule alphaAbs_ex_equal_or_qFresh_imp_alphaAbs_qAbs)
  using qgood apply simp
  unfolding alphaAbs_ex_equal_or_qFresh_def using y y' qEq
  unfolding fresh_def by auto
  moreover have "qGoodAbs(qAbs xs x ?qX)" using qgood by simp
  ultimately show "Abs xs x X = Abs xs x' X'"
  unfolding Abs_def by (auto simp add: asAbs_equal_iff_alphaAbs)
qed

lemma Abs_swap_fresh:
assumes good_X: "good X" and fresh: "fresh xs x' X"
shows "Abs xs x X = Abs xs x' (X #[x'  x]_xs)"
proof-
  let ?x'x = "swap xs x' x"   let ?qx'x = "qSwap xs x' x"
  have good_pickX: "qGood (pick X)" using good_X good_imp_qGood_pick by auto
  hence good_qAbs_pickX: "qGoodAbs (qAbs xs x (pick X))" by simp
  have good_x'x_pickX: "qGood (?qx'x (pick X))"
  using good_pickX qSwap_preserves_qGood by auto
  (*  *)
  have "Abs xs x X = asAbs (qAbs xs x (pick X))" unfolding Abs_def by simp
  also
  {have "qAbs xs x (pick X) $= qAbs xs x' (?qx'x (pick X))"
   using good_pickX fresh unfolding fresh_def using qAbs_alphaAbs_qSwap_qFresh by fastforce
   moreover
   {have "?qx'x (pick X) #= pick (?x'x X)"
    using good_X by (auto simp add: pick_swap_qSwap alpha_sym)
    hence "qAbs xs x' (?qx'x (pick X)) $= qAbs xs x' (pick (?x'x X))"
    using good_x'x_pickX qAbs_preserves_alpha by fastforce
   }
   ultimately have "qAbs xs x (pick X) $= qAbs xs x' (pick (?x'x X))"
   using good_qAbs_pickX alphaAbs_trans by blast
   hence "asAbs (qAbs xs x (pick X)) = asAbs (qAbs xs x' (pick (?x'x X)))"
   using good_qAbs_pickX by (auto simp add: asAbs_equal_iff_alphaAbs)
  }
  also have "asAbs (qAbs xs x' (pick (?x'x X))) = Abs xs x' (?x'x X)"
  unfolding Abs_def by auto
  finally show ?thesis .
qed

lemma Var_diff_Op[simp]:
"Var xs x  Op delta inp binp"
by (simp add: Op_def Var_def asTerm_equal_iff_alpha)

lemma Op_diff_Var[simp]:
"Op delta inp binp  Var xs x"
using Var_diff_Op[of _ _ _ inp] by blast

theorem term_nchotomy:
assumes "good X"
shows
"( xs x. X = Var xs x) 
 ( delta inp binp. goodInp inp  goodBinp binp  X = Op delta inp binp)"
proof-
  let ?qX = "pick X"
  have good_qX: "qGood ?qX" using assms good_imp_qGood_pick by auto
  have X: "X = asTerm ?qX" using assms asTerm_pick by auto
  show ?thesis
  proof(cases "?qX")
    fix xs x  assume Case1: "?qX = qVar xs x"
    have "X = Var xs x" unfolding Var_def using X Case1 by simp
    thus ?thesis by blast
  next
    fix delta qinp qbinp assume Case2: "?qX = qOp delta qinp qbinp"
    hence good_qinp: "qGoodInp qinp  qGoodBinp qbinp" using good_qX by simp
    let ?inp = "asInp qinp"  let ?binp = "asBinp qbinp"
    have "qinp %= pickInp ?inp  qbinp %%= pickBinp ?binp"
    using good_qinp pickInp_asInp alphaInp_sym pickBinp_asBinp alphaBinp_sym by blast
    hence "qOp delta qinp qbinp #= qOp delta (pickInp ?inp) (pickBinp ?binp)" by simp
    hence "asTerm (qOp delta qinp qbinp) = Op delta ?inp ?binp"
    unfolding Op_def using Case2 good_qX by (auto simp add: asTerm_equal_iff_alpha)
    hence "X = Op delta ?inp ?binp" using X Case2 by auto
    moreover have "goodInp ?inp  goodBinp ?binp"
    using good_qinp qGoodInp_iff_goodInp_asInp qGoodBinp_iff_goodBinp_asBinp by auto
    ultimately show ?thesis by blast
  qed
qed

theorem abs_nchotomy:
assumes "goodAbs A"
shows " xs x X. good X  A = Abs xs x X"
by (metis Abs_asTerm_asAbs_qAbs asAbs_pick assms 
     goodAbs_imp_qGoodAbs_pick qGoodAbs.elims(2) qGood_iff_good_asTerm)
 
lemmas good_freeCons =
Op_inj Var_diff_Op Op_diff_Var

subsection ‹Properties lifted from quasi-terms to terms›

subsubsection ‹Simplification rules›

theorem swap_Var_simp[simp]:
"((Var xs x) #[y1  y2]_ys) = Var xs (x @xs[y1  y2]_ys)"
by (metis QuasiTerms_Swap_Fresh.qSwapAll_simps(1) Var_def asTerm_qSwap_swap qItem_simps(9))

lemma swap_Op_simp[simp]:
assumes "goodInp inp"  "goodBinp binp"
shows "((Op delta inp binp) #[x1  x2]_xs) =
       Op delta (inp %[x1  x2]_xs) (binp %%[x1  x2]_xs)"
by (metis Op_asInp_asTerm_qOp Op_def asTerm_qSwap_swap assms(1) assms(2) goodBinp_imp_qGoodBinp_pickBinp goodInp_imp_qGoodInp_pickInp qGood_qGoodInp qSwapBinp_preserves_qGoodBinp 
     qSwapInp_preserves_qGoodInp qSwap_qSwapInp swapBinp_def2 swapInp_def2)

lemma swapAbs_simp[simp]:
assumes "good X"
shows "((Abs xs x X) $[y1  y2]_ys) = Abs xs (x @xs[y1  y2]_ys) (X #[y1  y2]_ys)"
by (metis Abs_asTerm_asAbs_qAbs Abs_preserves_good alphaAbs_preserves_qGoodAbs2 asAbs_qSwapAbs_swapAbs assms goodAbs_imp_qGoodAbs_pick good_imp_qGood_pick local.Abs_def 
     local.swap_def qAbs_pick_Abs qSwapAbs.simps qSwap_preserves_qGood1)

lemmas good_swapAll_simps =
swap_Op_simp swapAbs_simp

theorem fresh_Var_simp[simp]:
"fresh ys y (Var xs x :: ('index,'bindex,'varSort,'var,'opSym)term) 
 (ys  xs  y  x)"
by (simp add: Var_def fresh_asTerm_qFresh)
 
lemma fresh_Op_simp[simp]:
assumes "goodInp inp" "goodBinp binp"
shows
"fresh xs x (Op delta inp binp) 
 (freshInp xs x inp  freshBinp xs x binp)"
by (metis Op_def Op_preserves_good assms(1) assms(2) freshBinp_def2 
freshInp_def2 fresh_asTerm_qFresh qFresh_qFreshInp qGood_iff_good_asTerm)
 
lemma freshAbs_simp[simp]:
assumes "good X"
shows "freshAbs ys y (Abs xs x X)  (ys = xs  y = x  fresh ys y X)"
proof-
  let ?fr = "fresh ys y"  let ?qfr = "qFresh ys y"
  let ?frA = "freshAbs ys y"  let ?qfrA = "qFreshAbs ys y"
  have "qGood (pick X)" using assms by(auto simp add: good_imp_qGood_pick)
  hence good_qAbs_pick_X: "qGoodAbs (qAbs xs x (pick X))"
  using assms good_imp_qGood_pick by auto
  (*  *)
  have "?frA (Abs xs x X) = ?qfrA ((pick o asAbs) (qAbs xs x (pick X)))"
  unfolding freshAbs_def Abs_def by simp
  also
  {have "(pick o asAbs) (qAbs xs x (pick X)) $= qAbs xs x (pick X)"
   using good_qAbs_pick_X pick_asAbs by fastforce
   hence "?qfrA ((pick o asAbs) (qAbs xs x (pick X))) = ?qfrA (qAbs xs x (pick X))"
   using good_qAbs_pick_X qFreshAbs_preserves_alphaAbs by blast
  }
  also have "?qfrA(qAbs xs x (pick X)) = (ys = xs  y = x  ?qfr (pick X))" by simp
  also have " = (ys = xs  y = x  ?fr X)" unfolding fresh_def by simp
  finally show ?thesis .
qed

lemmas good_freshAll_simps =
fresh_Op_simp freshAbs_simp

theorem skel_Var_simp[simp]:
"skel (Var xs x) = Branch Map.empty Map.empty"
by (metis alpha_qSkel pick_Var_qVar qSkel.simps(1) skel_def) 

lemma skel_Op_simp[simp]:
assumes "goodInp inp" and "goodBinp binp"
shows "skel (Op delta inp binp) = Branch (skelInp inp) (skelBinp binp)"
by (metis (no_types, lifting) alpha_qSkel assms 
      qOp_pickInp_pick_Op qSkel_qSkelInp skelBinp_def skelInp_def skel_def)

lemma skelAbs_simp[simp]:
assumes "good X"
shows "skelAbs (Abs xs x X) = Branch (λi. Some (skel X)) Map.empty"
by (metis alphaAll_qSkelAll assms qAbs_pick_Abs qSkelAbs.simps skelAbs_def skel_def)

lemmas good_skelAll_simps =
skel_Op_simp skelAbs_simp

lemma psubst_Var:
assumes "goodEnv rho"
shows "((Var xs x) #[rho]) =
        (case rho xs x of None  Var xs x
                         |Some X  X)"
proof-
  let ?X = "Var xs x"  let ?qX = "qVar xs x"
  let ?qrho = "pickE rho"
  have good_qX: "qGood ?qX" using assms by simp
  moreover have good_qrho: "qGoodEnv ?qrho" using assms goodEnv_imp_qGoodEnv_pickE by auto
  ultimately have good_qXrho: "qGood (?qX #[[?qrho]])"
  using assms qPsubst_preserves_qGood by(auto simp del: qGoodAll_simps qPsubst.simps)
  (*  *)
  have "(?X #[rho]) = asTerm ((pick (asTerm ?qX)) #[[?qrho]])"
  unfolding Var_def psubst_def by simp
  also
  {have "?qX  #= pick (asTerm ?qX)" using good_qX pick_asTerm alpha_sym by fastforce
   hence "(?qX #[[?qrho]]) #= ((pick (asTerm ?qX)) #[[?qrho]])"
   using good_qrho good_qX qPsubst_preserves_alpha1[of _ ?qX] by fastforce
   hence "asTerm ((pick (asTerm ?qX))  #[[?qrho]]) = asTerm (?qX #[[?qrho]])"
   using good_qXrho asTerm_equal_iff_alpha[of "?qX #[[?qrho]]"] by blast
  }
  also have "asTerm (?qX #[[?qrho]]) =
             asTerm (case ?qrho xs x of None  qVar xs x
                                       |Some qY  qY)" unfolding Var_def by simp
  finally have 1: "(?X #[rho]) =  asTerm (case ?qrho xs x of None  qVar xs x
                                                            |Some qY  qY)" .
  show ?thesis
  proof(cases "rho xs x")
    assume Case1: "rho xs x = None"
    hence "?qrho xs x = None" unfolding pickE_def lift_def by simp
    thus ?thesis using 1 Case1 unfolding Var_def by simp
  next
    fix X assume Case2: "rho xs x = Some X"
    hence "good X" using assms unfolding goodEnv_def liftAll_def by auto
    hence "asTerm (pick X) = X" using asTerm_pick by auto
    moreover have qrho: "?qrho xs x = Some (pick X)"
    using Case2 unfolding pickE_def lift_def by simp
    ultimately show ?thesis using 1 Case2 unfolding Var_def by simp
  qed
qed

corollary psubst_Var_simp1[simp]:
assumes "goodEnv rho" and "rho xs x = None"
shows "((Var xs x) #[rho]) = Var xs x"
using assms by(simp add: psubst_Var)

corollary psubst_Var_simp2[simp]:
assumes "goodEnv rho" and "rho xs x = Some X"
shows "((Var xs x) #[rho]) = X"
using assms by(simp add: psubst_Var)

lemma psubst_Op_simp[simp]:
assumes good_inp: "goodInp inp"  "goodBinp binp"
and good_rho: "goodEnv rho"
shows
"((Op delta inp binp) #[rho]) = Op delta (inp %[rho]) (binp %%[rho])"
proof-
  let ?qrho = "pickE rho"
  let ?sbs = "psubst rho"   let ?qsbs = "qPsubst ?qrho"
  let ?sbsI = "psubstInp rho"  let ?qsbsI = "qPsubstInp ?qrho"
  let ?sbsB = "psubstBinp rho"  let ?qsbsB = "qPsubstBinp ?qrho"
  let ?op = "Op delta"   let ?qop = "qOp delta"
  have good_qop_pickInp_inp: "qGood (?qop (pickInp inp) (pickBinp binp))"
  using good_inp goodInp_imp_qGoodInp_pickInp
                 goodBinp_imp_qGoodBinp_pickBinp by auto
  hence "qGood ((pick o asTerm) (?qop (pickInp inp) (pickBinp binp)))"
  using good_imp_qGood_pick qGood_iff_good_asTerm by fastforce
  moreover have good_qrho: "qGoodEnv ?qrho"
  using good_rho goodEnv_imp_qGoodEnv_pickE by auto
  ultimately have good: "qGood (?qsbs((pick o asTerm) (?qop (pickInp inp) (pickBinp binp))))"
  using qPsubst_preserves_qGood by auto
  (*  *)
  have "?sbs (?op inp binp) =
        asTerm (?qsbs ((pick o asTerm) (?qop (pickInp inp) (pickBinp binp))))"
  unfolding psubst_def Op_def by simp
  also
  {have "(pick o asTerm) (?qop (pickInp inp) (pickBinp binp)) #=
         ?qop (pickInp inp) (pickBinp binp)"
   using good_qop_pickInp_inp pick_asTerm by fastforce
   hence "?qsbs((pick o asTerm) (?qop (pickInp inp) (pickBinp binp))) #=
          ?qsbs(?qop (pickInp inp) (pickBinp binp))"
   using good_qop_pickInp_inp good_qrho qPsubst_preserves_alpha1 by fastforce
   moreover have "?qsbs (?qop (pickInp inp) (pickBinp binp)) =
                  ?qop (?qsbsI (pickInp inp)) (?qsbsB (pickBinp binp))" by simp
   moreover
   {have "?qsbsI (pickInp inp) %= pickInp (?sbsI inp) 
          ?qsbsB (pickBinp binp) %%= pickBinp (?sbsB binp)"
    using good_rho good_inp pickInp_psubstInp_qPsubstInp[of inp rho]
          pickBinp_psubstBinp_qPsubstBinp[of binp rho] alphaInp_sym alphaBinp_sym by auto
    hence "?qop (?qsbsI (pickInp inp)) (?qsbsB (pickBinp binp)) #=
           ?qop (pickInp (?sbsI inp)) (pickBinp (?sbsB binp))" by simp
   }
   ultimately have "?qsbs((pick o asTerm) (?qop (pickInp inp) (pickBinp binp))) #=
                    ?qop (pickInp (?sbsI inp)) (pickBinp (?sbsB binp))"
   using good alpha_trans by force
   hence "asTerm (?qsbs((pick o asTerm) (?qop (pickInp inp) (pickBinp binp)))) =
          asTerm (?qop (pickInp (?sbsI inp)) (pickBinp (?sbsB binp)))"
   using good by (auto simp add: asTerm_equal_iff_alpha)
  }
  also have "asTerm (?qop (pickInp (?sbsI inp)) (pickBinp (?sbsB binp))) =
             ?op (?sbsI inp) (?sbsB binp)" unfolding Op_def by simp
  finally show ?thesis .
qed

lemma psubstAbs_simp[simp]:
assumes good_X: "good X" and good_rho: "goodEnv rho" and
        x_fresh_rho: "freshEnv xs x rho"
shows "((Abs xs x X) $[rho]) = Abs xs x (X #[rho])"
proof-
  let ?qrho = "pickE rho"
  let ?sbs = "psubst rho"  let ?qsbs = "qPsubst ?qrho"
  let ?sbsA = "psubstAbs rho"  let ?qsbsA = "qPsubstAbs ?qrho"
  have good_qrho: "qGoodEnv ?qrho"
  using good_rho goodEnv_imp_qGoodEnv_pickE by auto
  have good_pick_X: "qGood (pick X)" using good_X good_imp_qGood_pick by auto
  hence good_qsbs_pick_X: "qGood(?qsbs (pick X))"
  using good_qrho qPsubst_preserves_qGood by auto
  have good_qAbs_pick_X: "qGoodAbs (qAbs xs x (pick X))"
  using good_X good_imp_qGood_pick by auto
  hence "qGoodAbs ((pick o asAbs) (qAbs xs x (pick X)))"
  using goodAbs_imp_qGoodAbs_pick qGoodAbs_iff_goodAbs_asAbs by fastforce
  hence good: "qGoodAbs (?qsbsA ((pick o asAbs) (qAbs xs x (pick X))))"
  using good_qrho qPsubstAbs_preserves_qGoodAbs by auto
  have x_fresh_qrho: "qFreshEnv xs x ?qrho"
  using x_fresh_rho unfolding freshEnv_def2 by auto
  (*  *)
  have "?sbsA (Abs xs x X) = asAbs (?qsbsA ((pick o asAbs) (qAbs xs x (pick X))))"
  unfolding psubstAbs_def Abs_def by simp
  also
  {have "(pick o asAbs) (qAbs xs x (pick X)) $= qAbs xs x (pick X)"
   using good_qAbs_pick_X pick_asAbs by fastforce
   hence "?qsbsA((pick o asAbs) (qAbs xs x (pick X))) $= ?qsbsA(qAbs xs x (pick X))"
   using good_qAbs_pick_X good_qrho qPsubstAbs_preserves_alphaAbs1 by force
   moreover have "?qsbsA(qAbs xs x (pick X)) $= qAbs xs x (?qsbs (pick X))"
   using qFresh_qPsubst_commute_qAbs good_pick_X good_qrho x_fresh_qrho by auto
   moreover
   {have "?qsbs (pick X) #= pick (?sbs X)"
    using good_rho good_X pick_psubst_qPsubst alpha_sym by fastforce
    hence "qAbs xs x (?qsbs (pick X)) $= qAbs xs x (pick (?sbs X))"
    using good_qsbs_pick_X qAbs_preserves_alpha by fastforce
   }
   ultimately
   have "?qsbsA((pick o asAbs) (qAbs xs x (pick X))) $= qAbs xs x (pick (?sbs X))"
   using good alphaAbs_trans by blast
   hence "asAbs (?qsbsA((pick o asAbs) (qAbs xs x (pick X)))) =
          asAbs (qAbs xs x (pick (?sbs X)))"
   using good asAbs_equal_iff_alphaAbs by auto
  }
  also have "asAbs (qAbs xs x (pick (?sbs X))) = Abs xs x (?sbs X)"
  unfolding Abs_def by simp
  finally show ?thesis .
qed

lemmas good_psubstAll_simps =
psubst_Var_simp1 psubst_Var_simp2
psubst_Op_simp psubstAbs_simp

theorem getEnv_idEnv[simp]: "idEnv xs x = None"
unfolding idEnv_def by simp

lemma getEnv_updEnv[simp]:
"(rho [x  X]_xs) ys y = (if ys = xs  y = x then Some X else rho ys y)"
unfolding updEnv_def by auto

theorem getEnv_updEnv1:
"ys  xs  y  x  (rho [x  X]_xs) ys y = rho ys y"
by auto

theorem getEnv_updEnv2:
"(rho [x  X]_xs) xs x = Some X"
by auto

lemma subst_Var_simp1[simp]:
assumes "good Y"
and "ys  xs  y  x"
shows "((Var xs x) #[Y / y]_ys) = Var xs x"
using assms unfolding subst_def by auto

lemma subst_Var_simp2[simp]:
assumes "good Y"
shows "((Var xs x) #[Y / x]_xs) = Y"
using assms unfolding subst_def by auto

lemma subst_Op_simp[simp]:
assumes "good Y"
and "goodInp inp" and "goodBinp binp"
shows
"((Op delta inp binp) #[Y / y]_ys) =
 Op delta (inp %[Y / y]_ys) (binp %%[Y / y]_ys)"
using assms unfolding subst_def substInp_def substBinp_def by auto

lemma substAbs_simp[simp]:
assumes good: "good Y" and good_X: "good X" and
        x_dif_y: "xs  ys  x  y" and x_fresh: "fresh xs x Y"
shows "((Abs xs x X) $[Y / y]_ys) = Abs xs x (X #[Y / y]_ys)"
proof-
  have "freshEnv xs x (idEnv [y  Y]_ys)" unfolding freshEnv_def liftAll_def
  using x_dif_y x_fresh by auto
  thus ?thesis using assms unfolding subst_def substAbs_def by auto
qed

lemmas good_substAll_simps =
subst_Var_simp1 subst_Var_simp2
subst_Op_simp substAbs_simp

theorem vsubst_Var_simp[simp]:
"((Var xs x) #[y1 // y]_ys) = Var xs (x @xs[y1 / y]_ys)"
unfolding vsubst_def
apply(case_tac "ys = xs  y = x") by simp_all

lemma vsubst_Op_simp[simp]:
assumes "goodInp inp" and "goodBinp binp"
shows
"((Op delta inp binp) #[y1 // y]_ys) =
 Op delta (inp %[y1 // y]_ys) (binp %%[y1 // y]_ys)"
using assms unfolding vsubst_def vsubstInp_def vsubstBinp_def by auto

lemma vsubstAbs_simp[simp]:
assumes "good X" and
        "xs  ys  x  {y,y1}"
shows "((Abs xs x X) $[y1 // y]_ys) = Abs xs x (X #[y1 // y]_ys)"
using assms unfolding vsubst_def vsubstAbs_def by auto

lemmas good_vsubstAll_simps =
vsubst_Op_simp vsubstAbs_simp

lemmas good_allOpers_simps =
good_swapAll_simps
good_freshAll_simps
good_skelAll_simps
good_psubstAll_simps
good_substAll_simps
good_vsubstAll_simps

subsubsection ‹The ability to pick fresh variables›

lemma single_non_fresh_ordLess_var:
"good X  |{x. ¬ fresh xs x X}| <o |UNIV :: 'var set|"
unfolding fresh_def
by(auto simp add: good_imp_qGood_pick single_non_qFresh_ordLess_var)

lemma single_non_freshAbs_ordLess_var:
"goodAbs A  |{x. ¬ freshAbs xs x A}| <o |UNIV :: 'var set|"
unfolding freshAbs_def
by(auto simp add: goodAbs_imp_qGoodAbs_pick single_non_qFreshAbs_ordLess_var)

lemma obtain_fresh1:
fixes XS::"('index,'bindex,'varSort,'var,'opSym)term set" and
      Rho::"('index,'bindex,'varSort,'var,'opSym)env set" and rho
assumes Vvar: "|V| <o |UNIV :: 'var set|  finite V" and XSvar: "|XS| <o |UNIV :: 'var set|  finite XS" and
        good: " X  XS. good X" and
        Rhovar: "|Rho| <o |UNIV :: 'var set|  finite Rho" and RhoGood: " rho  Rho. goodEnv rho"
shows
" z. z  V 
 ( X  XS. fresh xs z X) 
 ( rho  Rho. freshEnv xs z rho)"
proof-
  let ?qXS = "pick ` XS"    let ?qRho = "pickE ` Rho"
  have "|?qXS| ≤o |XS|" using card_of_image by auto
  hence 1: "|?qXS| <o |UNIV :: 'var set|  finite ?qXS"
  using ordLeq_ordLess_trans card_of_ordLeq_finite XSvar by blast
  have "|?qRho| ≤o |Rho|" using card_of_image by auto
  hence 2: "|?qRho| <o |UNIV :: 'var set|  finite ?qRho"
  using ordLeq_ordLess_trans card_of_ordLeq_finite Rhovar by blast
  have 3: " qX  ?qXS. qGood qX" using good good_imp_qGood_pick by auto
  have " qrho  ?qRho. qGoodEnv qrho" using RhoGood goodEnv_imp_qGoodEnv_pickE by auto
  then obtain z where
  "z  V  ( qX  ?qXS. qFresh xs z qX) 
   ( qrho  ?qRho. qFreshEnv xs z qrho)"
  using Vvar 1 2 3 obtain_qFreshEnv[of V ?qXS ?qRho] by fastforce
  thus ?thesis unfolding fresh_def freshEnv_def2 by auto
qed

lemma obtain_fresh:
fixes V::"'var set" and
      XS::"('index,'bindex,'varSort,'var,'opSym)term set" and
      AS::"('index,'bindex,'varSort,'var,'opSym)abs set" and
      Rho::"('index,'bindex,'varSort,'var,'opSym)env set"
assumes Vvar: "|V| <o |UNIV :: 'var set|  finite V" and
        XSvar: "|XS| <o |UNIV :: 'var set|  finite XS" and
        ASvar: "|AS| <o |UNIV :: 'var set|  finite AS" and
        Rhovar: "|Rho| <o |UNIV :: 'var set|  finite Rho" and
        good: " X  XS. good X" and
        ASGood: " A  AS. goodAbs A" and
        RhoGood: " rho  Rho. goodEnv rho"
shows
" z. z  V 
     ( X  XS. fresh xs z X) 
     ( A  AS. freshAbs xs z A) 
     ( rho  Rho. freshEnv xs z rho)"
proof-
  have XS: "|XS| <o |UNIV :: 'var set|" and AS: "|AS| <o |UNIV :: 'var set|"
  using XSvar ASvar finite_ordLess_var by auto
  let ?phi = "% A Y. (good Y  (EX ys y. A = Abs ys y Y))"
  {fix A assume "A  AS"
   hence "goodAbs A" using ASGood by simp
   hence "EX Y. ?phi A Y" using abs_nchotomy[of A] by auto
  }
  then obtain f where 1: "ALL A : AS. ?phi A (f A)"
  using bchoice[of AS ?phi] by auto
  let ?YS = "f ` AS"
  have 2: "ALL Y : ?YS. good Y" using 1 by simp
  have "|?YS| <=o |AS|" using card_of_image by auto
  hence "|?YS| <o |UNIV :: 'var set|"
  using AS ordLeq_ordLess_trans by blast
  hence "|XS Un ?YS| <o |UNIV :: 'var set|"
  using XS by (auto simp add: var_infinite_INNER card_of_Un_ordLess_infinite)
  then obtain z where z: "z  V"
  and XSYS: " X  XS Un ?YS. fresh xs z X"
  and Rho: " rho  Rho. freshEnv xs z rho"
  using Vvar Rhovar good 2 RhoGood
        obtain_fresh1[of V "XS Un ?YS" Rho xs] by blast
  moreover
  {fix A
   obtain Y where Y_def: "Y = f A" by blast
   assume "A : AS"
   hence "fresh xs z Y" unfolding Y_def using XSYS by simp
   moreover obtain ys y where Y: "good Y" and A: "A = Abs ys y Y"
   unfolding Y_def using A : AS 1 by auto
   ultimately have "freshAbs xs z A" unfolding A using z by auto
  }
  ultimately show ?thesis by auto
qed

subsubsection ‹Compositionality›

lemma swap_ident[simp]:
assumes "good X"
shows "(X #[x  x]_xs) = X"
using assms asTerm_pick qSwap_ident unfolding swap_def by auto

lemma swap_compose:
assumes good_X: "good X"
shows "((X #[x  y]_zs) #[x'  y']_zs') =
       ((X #[x'  y']_zs') #[(x @zs[x'  y']_zs')  (y @zs[x'  y']_zs')]_zs)"
using assms qSwap_compose[of _ _ _ _ _ _ "pick X"] by(auto simp add: double_swap_qSwap)

lemma swap_commute:
"good X; zs  zs'  {x,y}  {x',y'} = {} 
 ((X #[x  y]_zs) #[x'  y']_zs') = ((X #[x'  y']_zs') #[x  y]_zs)"
using swap_compose[of X  zs' x' y' zs x y] by(auto simp add: sw_def)

lemma swap_involutive[simp]:
assumes good_X: "good X"
shows "((X #[x  y]_zs) #[x  y]_zs) = X"
using assms asTerm_pick[of X] by (auto simp add: double_swap_qSwap)

theorem swap_sym: "(X #[x  y]_zs) = (X #[y  x]_zs)"
unfolding swap_def by(auto simp add: qSwap_sym)

lemma swap_involutive2[simp]:
assumes "good X"
shows "((X #[x  y]_zs) #[y  x]_zs) = X"
using assms by(simp add: swap_sym)

lemma swap_preserves_fresh[simp]:
assumes "good X"
shows "fresh xs (x @xs[y1  y2]_ys) (X #[y1  y2]_ys) = fresh xs x X"
unfolding fresh_def[of _ _ X] using assms qSwap_preserves_qFresh[of _ _ _ _ _ "pick X"]
by(auto simp add: fresh_swap_qFresh_qSwap)

lemma swap_preserves_fresh_distinct:
assumes "good X" and
       "xs  ys  x  {y1,y2}"
shows "fresh xs x (X #[y1  y2]_ys) = fresh xs x X"
unfolding fresh_def[of _ _ X] using assms  
by(auto simp: fresh_swap_qFresh_qSwap qSwap_preserves_qFresh_distinct)

lemma fresh_swap_exchange1:
assumes "good X"
shows "fresh xs x2 (X #[x1  x2]_xs) = fresh xs x1 X"
unfolding fresh_def[of _ _ X]
using assms by(auto simp: fresh_swap_qFresh_qSwap qFresh_qSwap_exchange1)

lemma fresh_swap_exchange2:
assumes "good X" and "{x1,x2}  var xs"
shows "fresh xs x2 (X #[x2  x1]_xs) = fresh xs x1 X"
using assms by(simp add: fresh_swap_exchange1 swap_sym)

(* Note: the lemmas swap_preserves_fresh_distinct, fresh_swap_exchange1 and
   fresh_swap_exchange2 do cover all possibilities of simplifying an
   expression of the form "fresh ys y (X #[x2 ∧ x1]_xs)".   *)

lemma fresh_swap_id[simp]:
assumes "good X" and "fresh xs x1 X" "fresh xs x2 X"
shows "(X #[x1  x2]_xs) = X"
by (metis (no_types, lifting)  assms alpha_imp_asTerm_equal alpha_qFresh_qSwap_id asTerm_pick   
      fresh_def good_imp_qGood_pick local.swap_def qSwap_preserves_qGood1)

lemma freshAbs_swapAbs_id[simp]:
assumes "goodAbs A" "freshAbs xs x1 A"  "freshAbs xs x2 A"
shows "(A $[x1  x2]_xs) = A"
using assms 
by (meson alphaAbs_qFreshAbs_qSwapAbs_id alphaAll_trans freshAbs_def goodAbs_imp_qGoodAbs_pick 
    pick_alphaAbs_iff_equal pick_swapAbs_qSwapAbs swapAbs_preserves_good)
 
lemma fresh_swap_compose:
assumes "good X" "fresh xs y X" "fresh xs z X"
shows "((X #[y  x]_xs) #[z  y]_xs) = (X #[z  x]_xs)"
using assms by (simp add: sw_def swap_compose)

lemma skel_swap:
assumes "good X"
shows "skel (X #[x1  x2]_xs) = skel X"
using assms by (metis alpha_qSkel pick_swap_qSwap qSkel_qSwap skel_def)

subsubsection ‹Compositionality for environments›

lemma swapEnv_ident[simp]:
assumes "goodEnv rho"
shows "(rho &[x  x]_xs) = rho"
using assms unfolding swapEnv_defs lift_def  
by (intro ext) (auto simp: option.case_eq_if) 

lemma swapEnv_compose:
assumes good: "goodEnv rho"
shows "((rho &[x  y]_zs) &[x'  y']_zs') =
       ((rho &[x'  y']_zs') &[(x @zs[x'  y']_zs')  (y @zs[x'  y']_zs')]_zs)"
proof(rule ext)+
  let ?xsw = "x @zs[x'  y']_zs'"  let ?ysw = "y @zs[x'  y']_zs'"
  let ?xswsw = "?xsw @zs[x'  y']_zs'"  let ?yswsw = "?ysw @zs[x'  y']_zs'"
  let ?rhosw1 = "rho &[x  y]_zs"   let ?rhosw11 = "?rhosw1 &[x'  y']_zs'"
  let ?rhosw2 = "rho &[x'  y']_zs'" let ?rhosw22 = "?rhosw2 &[?xsw  ?ysw]_zs"
  let ?Sw1 = "λX. (X #[x  y]_zs)"  let ?Sw11 = "λX. ((?Sw1 X) #[x'  y']_zs')"
  let ?Sw2 = "λX. (X #[x'  y']_zs')"  let ?Sw22 = "λX. ((?Sw2 X) #[?xsw  ?ysw]_zs)"
  fix us u
  let ?usw1 = "u @us [x'  y']_zs'" let ?usw11 = "?usw1 @us [x  y]_zs"
  let ?usw2 = "u @us [?xsw  ?ysw]_zs" let ?usw22 = "?usw2 @us [x'  y']_zs'"
  have "(?xsw @zs[x'  y']_zs') = x" and "(?ysw @zs[x'  y']_zs') = y" by auto
  have "?usw22 = (?usw1 @us[?xswsw  ?yswsw]_zs)" using sw_compose .
  hence *: "?usw22 = ?usw11" by simp
  show "?rhosw11 us u = ?rhosw22 us u"
  proof(cases "rho us ?usw11")
    case None
    hence "?rhosw11 us u = None" unfolding swapEnv_defs lift_def by simp
    also have " = ?rhosw22 us u"
    using None unfolding * swapEnv_defs lift_def by simp
    finally show ?thesis .
  next
    case (Some X)
    hence "good X" using good unfolding goodEnv_def liftAll_def by simp
    have "?rhosw11 us u = Some(?Sw11 X)" using Some unfolding swapEnv_defs lift_def by simp
    also have "?Sw11 X = ?Sw22 X"
    using good X by(rule swap_compose)
    also have "Some(?Sw22 X) = ?rhosw22 us u"
    using Some unfolding * swapEnv_defs lift_def by simp
    finally show ?thesis .
  qed
qed

lemma swapEnv_commute:
"goodEnv rho; {x,y}  var zs; zs  zs'  {x,y}  {x',y'} = {} 
 ((rho &[x  y]_zs) &[x'  y']_zs') = ((rho &[x'  y']_zs') &[x  y]_zs)"
using swapEnv_compose[of rho zs' x' y' zs x y] by(auto simp add: sw_def)

lemma swapEnv_involutive[simp]:
assumes "goodEnv rho"
shows "((rho &[x  y]_zs) &[x  y]_zs) = rho"
using assms unfolding swapEnv_defs lift_def  
by (fastforce simp: option.case_eq_if) 

theorem swapEnv_sym: "(rho &[x  y]_zs) = (rho &[y  x]_zs)"
proof(intro ext)
  fix us u
  have *: "(u @us[x  y]_zs) = (u @us[y  x]_zs)" using sw_sym by fastforce
  show "(rho &[x  y]_zs) us u = (rho &[y  x]_zs) us u"
  unfolding swapEnv_defs lift_def *
  by(cases "rho us (u @us[y  x]_zs)") (auto simp: swap_sym)
qed

lemma swapEnv_involutive2[simp]:
assumes good: "goodEnv rho"
shows "((rho &[x  y]_zs) &[y  x]_zs) = rho"
using assms by(simp add: swapEnv_sym)

lemma swapEnv_preserves_freshEnv[simp]:
assumes good: "goodEnv rho"
shows "freshEnv xs (x @xs[y1  y2]_ys) (rho &[y1  y2]_ys) = freshEnv xs x rho"
proof-
 let ?xsw = "x @xs[y1  y2]_ys"  let ?xswsw = "?xsw @xs[y1  y2]_ys"
 let ?rhosw = "rho &[y1  y2]_ys"
 let ?Left = "freshEnv xs ?xsw ?rhosw"
 let ?Right = "freshEnv xs x rho"
 have "(?rhosw xs ?xsw = None) = (rho xs x = None)"
 unfolding freshEnv_def swapEnv_defs
 by(simp add: lift_None sw_involutive)
 moreover
 have "( zs z' Z'. ?rhosw zs z' = Some Z'  fresh xs ?xsw Z') =
       ( zs z Z. rho zs z = Some Z  fresh xs x Z)"
 proof(rule iff_allI, auto)
   fix zs z Z assume *: " z' Z'. ?rhosw zs z' = Some Z'  fresh xs ?xsw Z'"
   and **: "rho zs z = Some Z"  let ?z' = "z @zs[y1  y2]_ys"  let ?Z' = "Z #[y1  y2]_ys"
   have "?rhosw zs ?z' = Some ?Z'" using ** unfolding swapEnv_defs lift_def
   by(simp add: sw_involutive)
   hence "fresh xs ?xsw ?Z'" using * by simp
   moreover have "good Z" using ** good unfolding goodEnv_def liftAll_def by simp
   ultimately show "fresh xs x Z" using swap_preserves_fresh by auto
 next
   fix zs z' Z'
   assume *: "z Z. rho zs z = Some Z  fresh xs x Z" and **: "?rhosw zs z' = Some Z'"
   let ?z = "z' @zs[y1  y2]_ys"
   obtain Z where rho: "rho zs ?z = Some Z" and Z': "Z' = Z #[y1  y2]_ys"
   using ** unfolding swapEnv_defs lift_def by(cases "rho zs ?z", auto)
   hence "fresh xs x Z" using * by simp
   moreover have "good Z" using rho good unfolding goodEnv_def liftAll_def by simp
   ultimately show "fresh xs ?xsw Z'" unfolding Z' using swap_preserves_fresh by auto
 qed
 ultimately show ?thesis unfolding freshEnv_def swapEnv_defs
 unfolding liftAll_def by simp
qed

lemma swapEnv_preserves_freshEnv_distinct:
assumes "goodEnv rho" and
       "xs  ys  x  {y1,y2}"
shows "freshEnv xs x (rho &[y1  y2]_ys) = freshEnv xs x rho"
by (metis assms sw_simps3 swapEnv_preserves_freshEnv)

lemma freshEnv_swapEnv_exchange1:
assumes "goodEnv rho"
shows "freshEnv xs x2 (rho &[x1  x2]_xs) = freshEnv xs x1 rho"
by (metis assms sw_simps1 swapEnv_preserves_freshEnv)

lemma freshEnv_swapEnv_exchange2:
assumes "goodEnv rho"
shows "freshEnv xs x2 (rho &[x2  x1]_xs) = freshEnv xs x1 rho"
using assms by(simp add: freshEnv_swapEnv_exchange1 swapEnv_sym)

lemma freshEnv_swapEnv_id[simp]:
assumes good: "goodEnv rho" and
        fresh: "freshEnv xs x1 rho"  "freshEnv xs x2 rho"
shows "(rho &[x1  x2]_xs) = rho"
proof(intro ext)
  fix us u
  let ?usw = "u @us[x1  x2]_xs" let ?rhosw = "rho &[x1  x2]_xs"
  let ?Sw = "λ X. (X #[x1  x2]_xs)"
  show "?rhosw us u = rho us u"
  proof(cases "rho us u")
    case None
    hence "rho us ?usw = None" using fresh unfolding freshEnv_def sw_def by auto
    hence "?rhosw us u = None" unfolding swapEnv_defs lift_def by auto
    with None show ?thesis by simp
  next
   case (Some X)
   moreover have "?usw = u"  using fresh Some unfolding freshEnv_def sw_def by auto
   ultimately have "?rhosw us u = Some (?Sw X)" unfolding swapEnv_defs lift_def by auto
   moreover
   {have "good X" using Some good unfolding goodEnv_def liftAll_def by auto
    moreover have "fresh xs x1 X" and "fresh xs x2 X"
    using Some fresh unfolding freshEnv_def liftAll_def by auto
    ultimately have "?Sw X = X" by simp
   }
   ultimately show ?thesis using Some by simp
  qed
qed

lemma freshEnv_swapEnv_compose:
assumes good: "goodEnv rho" and
        fresh: "freshEnv xs y rho"  "freshEnv xs z rho"
shows "((rho &[y  x]_xs) &[z  y]_xs) = (rho &[z  x]_xs)"
by (simp add: fresh good sw_def swapEnv_compose)

lemmas good_swapAll_freshAll_otherSimps =
swap_ident swap_involutive swap_involutive2 swap_preserves_fresh fresh_swap_id
freshAbs_swapAbs_id
swapEnv_ident swapEnv_involutive swapEnv_involutive2 swapEnv_preserves_freshEnv freshEnv_swapEnv_id

subsubsection ‹Properties of the relation of being swapped›

theorem swap_swapped: "(X, X #[x  y]_zs)  swapped"
by(auto simp add: swapped.Refl swapped.Swap)

lemma swapped_preserves_good:
assumes "good X" and "(X,Y)  swapped"
shows "good Y"
using assms(2,1) by (induct rule: swapped.induct) auto

lemma swapped_skel:
assumes "good X" and "(X,Y)  swapped"
shows "skel Y = skel X"
using assms(2,1) 
by (induct rule: swapped.induct) (auto simp: swapped_preserves_good skel_swap)

lemma obtain_rep:
assumes GOOD: "good X" and FRESH: "fresh xs x' X"
shows " X'. (X,X')  swapped  good X'  Abs xs x X = Abs xs x' X'"
using Abs_swap_fresh FRESH GOOD swap_preserves_good swap_swapped by blast

subsection ‹Induction›

subsubsection ‹Induction lifted from quasi-terms›

lemma term_templateInduct[case_names rel Var Op Abs]:
fixes X::"('index,'bindex,'varSort,'var,'opSym)term" and
      A::"('index,'bindex,'varSort,'var,'opSym)abs" and phi phiAbs rel
assumes
rel: " X Y. good X; (X,Y)  rel  good Y  skel Y = skel X" and
var: " xs x. phi (Var xs x)" and
op: " delta inp binp. goodInp inp; goodBinp binp; liftAll phi inp; liftAll phiAbs binp
                        phi (Op delta inp binp)" and
abs: " xs x X. good X;  Y. (X,Y)  rel  phi Y
                 phiAbs (Abs xs x X)"
shows "(good X  phi X)  (goodAbs A  phiAbs A)"
proof-
  let ?qX = "pick X"   let ?qA = "pick A"
  let ?qphi = "phi o asTerm"   let ?qphiAbs = "phiAbs o asAbs"
  let ?qrel = "{(qY, qY')| qY qY'. (asTerm qY, asTerm qY')  rel}"
  (*   *)
  have "(good X  qGood ?qX)  (goodAbs A  qGoodAbs ?qA)"
  using good_imp_qGood_pick goodAbs_imp_qGoodAbs_pick by auto
  moreover
  have "(good X  (?qphi ?qX = phi X))  (goodAbs A  (?qphiAbs ?qA = phiAbs A))"
  using asTerm_pick asAbs_pick by fastforce
  moreover
  have "(qGood ?qX  ?qphi ?qX)  (qGoodAbs ?qA  ?qphiAbs ?qA)"
  proof(induction rule: qGood_qTerm_templateInduct[of ?qrel])
    case (Rel qX qY)
    thus ?case using qGood_iff_good_asTerm pick_asTerm unfolding skel_def 
    using rel skel_asTerm_qSkel   
    by simp (smt (verit) qGood_iff_good_asTerm skel_asTerm_qSkel)  
  next
    case (Var xs x)
    then show ?case using var unfolding Var_def by simp
  next
    case (Op delta qinp qbinp) 
    hence good_qinp: "qGoodInp qinp  qGoodBinp qbinp"
    unfolding qGoodInp_def qGoodBinp_def liftAll_def by simp
    let ?inp = "asInp qinp"   let ?binp = "asBinp qbinp"
    have good_inp: "goodInp ?inp  goodBinp ?binp"
    using good_qinp qGoodInp_iff_goodInp_asInp qGoodBinp_iff_goodBinp_asBinp by auto
    have 1: "Op delta ?inp ?binp = asTerm (qOp delta qinp qbinp)"
    using good_qinp Op_asInp_asTerm_qOp by fastforce
    {fix i X
     assume inp: "?inp i = Some X"
     then obtain qX where qinp: "qinp i = Some qX" and X: "X = asTerm qX"
     unfolding asInp_def lift_def by(cases "qinp i", auto)
     have "qGood qX  phi (asTerm qX)" using qinp Op.IH by (simp add: liftAll_def)
     hence "good X  phi X" unfolding X using qGood_iff_good_asTerm by auto
    }
    moreover
    {fix i A
     assume binp: "?binp i = Some A"
     then obtain qA where qbinp: "qbinp i = Some qA" and A: "A = asAbs qA"
     unfolding asBinp_def lift_def by(cases "qbinp i", auto)
     have "qGoodAbs qA  phiAbs (asAbs qA)" using qbinp Op.IH by (simp add: liftAll_def)
     hence "goodAbs A  phiAbs A" unfolding A using qGoodAbs_iff_goodAbs_asAbs by auto
    }
    ultimately show ?case
    using op[of ?inp ?binp delta] good_inp unfolding 1 liftAll_def by simp
  next
    case (Abs xs x qX) 
    have "good (asTerm qX)" using qGood qX qGood_iff_good_asTerm by auto
    moreover
    {fix Y   assume *: "(asTerm qX, Y)  rel"
     obtain qY where qY: "qY = pick Y" by blast
     have "good (asTerm qX)" using qGood qX qGood_iff_good_asTerm by auto
     hence "good Y" using * rel by auto 
     hence Y: "Y = asTerm qY" unfolding qY using asTerm_pick by auto
     have "phi Y" using * Abs.IH unfolding Y by simp
    }
    ultimately have "phiAbs (Abs xs x (asTerm qX))" using abs by simp
    thus ?case using qGood qX Abs_asTerm_asAbs_qAbs by fastforce
  qed
  (*  *)
  ultimately show ?thesis by blast
qed

lemma term_rawInduct[case_names Var Op Abs]:
fixes X::"('index,'bindex,'varSort,'var,'opSym)term" and
      A::"('index,'bindex,'varSort,'var,'opSym)abs" and phi phiAbs
assumes
Var: " xs x. phi (Var xs x)" and
Op: " delta inp binp. goodInp inp; goodBinp binp; liftAll phi inp; liftAll phiAbs binp
                        phi (Op delta inp binp)" and
Abs: " xs x X. good X; phi X  phiAbs (Abs xs x X)"
shows "(good X  phi X)  (goodAbs A  phiAbs A)"
by(rule term_templateInduct[of Id], auto simp add: assms)

lemma term_induct[case_names Var Op Abs]:
fixes X::"('index,'bindex,'varSort,'var,'opSym)term" and
      A::"('index,'bindex,'varSort,'var,'opSym)abs" and phi phiAbs
assumes
Var: " xs x. phi (Var xs x)" and
Op: " delta inp binp. goodInp inp; goodBinp binp; liftAll phi inp; liftAll phiAbs binp
                        phi (Op delta inp binp)" and
Abs: " xs x X. good X;
                  Y. (X,Y)  swapped  phi Y;
                  Y. good Y; skel Y = skel X  phi Y
                 phiAbs (Abs xs x X)"
shows "(good X  phi X)  (goodAbs A  phiAbs A)"
apply(induct rule: term_templateInduct[of "swapped  {(X,Y). good Y  skel Y = skel X}"])
by(auto simp: assms swapped_skel swapped_preserves_good) 

subsubsection ‹Fresh induction›

text‹First a general situation, where parameters are of an unspecified type (that should be given by the user):›
 
lemma term_fresh_forall_induct[case_names PAR Var Op Abs]:
fixes X::"('index,'bindex,'varSort,'var,'opSym)term" and A::"('index,'bindex,'varSort,'var,'opSym)abs" 
and phi and phiAbs and varsOf :: "'param  'varSort  'var set" 
assumes
PAR: " p xs. ( |varsOf xs p| <o |UNIV::'var set| )" and
var: " xs x p. phi (Var xs x) p" and
op: " delta inp binp p.  
   |{i. inp i  None}| <o |UNIV::'var set|; |{i. binp i  None}| <o |UNIV::'var set|;
    liftAll (λ X. good X  ( q. phi X p)) inp; liftAll (λ A. goodAbs A  ( q. phiAbs A p)) binp
    phi (Op delta inp binp) p" and
abs: " xs x X p. good X; x  varsOf p xs; phi X p  phiAbs (Abs xs x X) p"
shows "(good X  ( p. phi X p))  (goodAbs A  ( p. phiAbs A p))"
proof(induction rule: term_templateInduct[of swapped])
  case (Abs xs x X)
  show ?case proof safe 
    fix p 
    obtain x' where x'_freshP: "x'  varsOf p xs" and x'_fresh_X: "fresh xs x' X"
    using good X PAR obtain_fresh[of "varsOf p xs" "{X}" "{}" "{}" xs] by auto
    then obtain X' where XX': "(X, X')  swapped" and good_X': "good X'" and
    Abs_eq: "Abs xs x X = Abs xs x' X'"
    using good X x'_freshP x'_fresh_X using obtain_rep[of X xs x' x] by auto
    thus "phiAbs (Abs xs x X) p"
    unfolding Abs_eq using x'_freshP good_X' abs Abs.IH by simp
  qed
qed(insert assms swapped_preserves_good swapped_skel, 
   unfold liftAll_def goodInp_def goodBinp_def, auto)

  
lemma term_templateInduct_fresh[case_names PAR Var Op Abs]:
fixes X::"('index,'bindex,'varSort,'var,'opSym)term" and
      A::"('index,'bindex,'varSort,'var,'opSym)abs" and
      rel and phi and phiAbs and
      vars :: "'varSort  'var set" and
      terms :: "('index,'bindex,'varSort,'var,'opSym)term set" and
      abs :: "('index,'bindex,'varSort,'var,'opSym)abs set" and
      envs :: "('index,'bindex,'varSort,'var,'opSym)env set"
assumes
PAR:
" xs.
   ( |vars xs| <o |UNIV :: 'var set|  finite (vars xs)) 
   ( |terms| <o |UNIV :: 'var set|  finite terms)  ( X  terms. good X) 
   ( |abs| <o |UNIV :: 'var set|  finite abs)  ( A  abs. goodAbs A) 
   ( |envs| <o |UNIV :: 'var set|  finite envs)  ( rho  envs. goodEnv rho)" and
rel: " X Y. good X; (X,Y)  rel  good Y  skel Y = skel X" and
Var: " xs x. phi (Var xs x)" and
Op:
" delta inp binp.
   goodInp inp; goodBinp binp;
    liftAll phi inp; liftAll phiAbs binp
    phi (Op delta inp binp)" and
abs:
" xs x X.
  good X;
   x  vars xs;
    Y. Y  terms  fresh xs x Y;
    A. A  abs  freshAbs xs x A;
    rho. rho  envs  freshEnv xs x rho;
    Y. (X,Y)  rel  phi Y
   phiAbs (Abs xs x X)"
shows
"(good X  phi X) 
 (goodAbs A  phiAbs A)"
proof(induction rule: term_templateInduct[of "swapped O rel"])
  case (Abs xs x X) note good_X = good X  
  have "|{X}  terms| <o |UNIV :: 'var set|  finite ({X}  terms)"
  apply(cases "finite terms", auto simp add: PAR)
  using PAR var_infinite_INNER card_of_Un_singl_ordLess_infinite by force
  then obtain x' where x'_not: "x'  vars xs" and
  x'_fresh_X: "fresh xs x' X" and
  x'_freshP: "( Y  terms. fresh xs x' Y) 
              ( A  abs. freshAbs xs x' A) 
              ( rho  envs. freshEnv xs x' rho)"
  using good_X PAR
  using obtain_fresh[of "vars xs" "{X}  terms" abs envs xs] by auto
  then obtain X' where XX': "(X, X')  swapped" and good_X': "good X'" and
  Abs_eq: "Abs xs x X = Abs xs x' X'"
  using good_X x'_not x'_fresh_X using obtain_rep[of X xs x' x] by auto
  have "Y. (X', Y)  rel  phi Y" using XX' Abs.IH by auto 
  thus ?case
  unfolding Abs_eq using x'_not x'_freshP good_X' abs by auto
qed(insert Op rel, unfold relcomp_unfold liftAll_def, simp_all add: Var, 
     metis rel swapped_preserves_good swapped_skel) 

text‹A version of the above not employing any relation for the bound-argument case:›

lemma term_rawInduct_fresh[case_names Par Var Op Obs]:
fixes X::"('index,'bindex,'varSort,'var,'opSym)term" and
      A::"('index,'bindex,'varSort,'var,'opSym)abs" and
      vars :: "'varSort  'var set" and
      terms :: "('index,'bindex,'varSort,'var,'opSym)term set" and
      abs :: "('index,'bindex,'varSort,'var,'opSym)abs set" and
      envs :: "('index,'bindex,'varSort,'var,'opSym)env set"
assumes
PAR:
" xs.
   ( |vars xs| <o |UNIV :: 'var set|  finite (vars xs)) 
   ( |terms| <o |UNIV :: 'var set|  finite terms)  ( X  terms. good X) 
   ( |abs| <o |UNIV :: 'var set|  finite abs)  ( A  abs. goodAbs A) 
   ( |envs| <o |UNIV :: 'var set|  finite envs)  ( rho  envs. goodEnv rho)" and
Var: " xs x. phi (Var xs x)" and
Op:
" delta inp binp.
   goodInp inp; goodBinp binp;
    liftAll phi inp; liftAll phiAbs binp
    phi (Op delta inp binp)" and
Abs:
" xs x X.
  good X;
   x  vars xs;
    Y. Y  terms  fresh xs x Y;
    A. A  abs  freshAbs xs x A;
    rho. rho  envs  freshEnv xs x rho;
   phi X
   phiAbs (Abs xs x X)"
shows
"(good X  phi X) 
 (goodAbs A  phiAbs A)"
apply(induct rule: term_templateInduct_fresh[of vars terms abs envs Id])
using assms by auto

(* Note that here, since we avoid variable-capture and hence will
 not typically need to swap, term-inductRaw_fresh will suffice in proofs.
 Therefore we do not prove a swapped-and-skel version of fresh induction, although such a version
 could be easily inferred from ``term-templateInduct". *)

text‹The typical raw induction with freshness is one dealing with
   finitely many variables, terms, abstractions and environments as parameters --
   we have all these condensed in the notion of a parameter (type
   constructor ``param"):›

lemma term_induct_fresh[case_names Par Var Op Abs]:
fixes X :: "('index,'bindex,'varSort,'var,'opSym)term" and
      A :: "('index,'bindex,'varSort,'var,'opSym)abs" and
      P :: "('index,'bindex,'varSort,'var,'opSym)param"
assumes
goodP: "goodPar P" and
Var: " xs x. phi (Var xs x)" and
Op:
" delta inp binp.
   goodInp inp; goodBinp binp;
    liftAll phi inp; liftAll phiAbs binp
    phi (Op delta inp binp)" and
Abs:
" xs x X.
   good X;
    x  varsOf P;
     Y. Y  termsOf P  fresh xs x Y;
     A. A  absOf P  freshAbs xs x A;
     rho. rho  envsOf P  freshEnv xs x rho;
    phi X
    phiAbs (Abs xs x X)"
shows
"(good X  phi X) 
 (goodAbs A  phiAbs A)"
proof(induct rule: term_rawInduct_fresh
      [of "λ xs. varsOf P" "termsOf P" "absOf P" "envsOf P"])
  case (Par xs)
  then show ?case unfolding goodPar_def  
  using goodP by(cases P) simp
qed(insert assms, auto) 

end  (* context FixVars  *)

end