# Theory Coding_Predicates

```chapter ‹Predicates for Terms, Formulas and Substitution›

theory Coding_Predicates
imports Coding Sigma
begin

declare succ_iff [simp del]

text ‹This material comes from Section 3, greatly modified for de Bruijn syntax.›

section ‹Predicates for atomic terms›

subsection ‹Free Variables›

definition is_Var :: "hf ⇒ bool" where "is_Var x ≡ Ord x ∧ 0 ❙∈ x"

definition VarP :: "tm ⇒ fm" where "VarP x ≡ OrdP x AND Zero IN x"

lemma VarP_eqvt [eqvt]: "(p ∙ VarP x) = VarP (p ∙ x)"

lemma VarP_fresh_iff [simp]: "a ♯ VarP x ⟷ a ♯ x"

lemma eval_fm_VarP [simp]:  "eval_fm e (VarP x) ⟷ is_Var ⟦x⟧e"

lemma VarP_sf [iff]: "Sigma_fm (VarP x)"
by (auto simp: VarP_def)

lemma VarP_subst [simp]: "(VarP x)(i::=t) = VarP (subst i t x) "

lemma VarP_cong: "H ⊢ x EQ x' ⟹ H ⊢ VarP x IFF VarP x'"
by (rule P1_cong) auto

lemma VarP_HPairE [intro!]: "insert (VarP (HPair x y)) H ⊢ A"
by (auto simp: VarP_def)

lemma is_Var_succ_iff [simp]: "is_Var (succ x) = Ord x"
by (metis Ord_succ_iff is_Var_def succ_iff zero_in_Ord)

lemma is_Var_q_Var [iff]: "is_Var (q_Var i)"

definition decode_Var :: "hf ⇒ name"
where "decode_Var x ≡ name_of_nat (nat_of_ord (pred x))"

lemma decode_Var_q_Var [simp]: "decode_Var (q_Var i) = i"

lemma is_Var_imp_decode_Var: "is_Var x ⟹ x = ⟦«Var (decode_Var x)»⟧ e"
by (simp add: is_Var_def quot_Var decode_Var_def) (metis hempty_iff succ_pred)

lemma is_Var_iff: "is_Var v ⟷ v = succ (ord_of (nat_of_name (decode_Var v)))"
by (metis eval_tm_ORD_OF eval_tm_SUCC is_Var_imp_decode_Var quot_Var is_Var_succ_iff Ord_ord_of)

lemma decode_Var_inject [simp]: "is_Var v ⟹ is_Var v' ⟹ decode_Var v = decode_Var v' ⟷ v=v'"
by (metis is_Var_iff)

subsection ‹De Bruijn Indexes›

definition is_Ind :: "hf ⇒ bool"
where "is_Ind x ≡ (∃m. Ord m ∧ x = ⟨htuple 6, m⟩)"

abbreviation Q_Ind :: "tm ⇒ tm"
where "Q_Ind k ≡ HPair (HTuple 6) k"

nominal_function IndP :: "tm ⇒ fm"
where "atom m ♯ x ⟹
IndP x = Ex m (OrdP (Var m) AND x EQ HPair (HTuple 6) (Var m))"
by (auto simp: eqvt_def IndP_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)

nominal_termination (eqvt)
by lexicographic_order

lemma
shows IndP_fresh_iff [simp]: "a ♯ IndP x ⟷ a ♯ x"                (is ?thesis1)
and eval_fm_IndP [simp]:   "eval_fm e (IndP x) ⟷ is_Ind ⟦x⟧e"  (is ?thesis2)
and IndP_sf [iff]:         "Sigma_fm (IndP x)"                   (is ?thsf)
and OrdP_IndP_Q_Ind:       "{OrdP x} ⊢ IndP (Q_Ind x)"           (is ?thqind)
proof -
obtain m::name where "atom m ♯ x"
by (metis obtain_fresh)
thus ?thesis1 ?thesis2 ?thsf ?thqind
by (auto simp: is_Ind_def intro: Ex_I [where x=x])
qed

lemma IndP_Q_Ind: "H ⊢ OrdP x ⟹ H ⊢ IndP (Q_Ind x)"
by (rule cut1 [OF OrdP_IndP_Q_Ind])

lemma subst_fm_IndP [simp]: "(IndP t)(i::=x) = IndP (subst i x t)"
proof -
obtain m::name where "atom m ♯ (i,t,x)"
by (metis obtain_fresh)
thus ?thesis
by (auto simp: IndP.simps [of m])
qed

lemma IndP_cong: "H ⊢ x EQ x' ⟹ H ⊢ IndP x IFF IndP x'"
by (rule P1_cong) auto

definition decode_Ind :: "hf ⇒ nat"
where "decode_Ind x ≡ nat_of_ord (hsnd x)"

lemma is_Ind_pair_iff [simp]: "is_Ind ⟨x, y⟩ ⟷ x = htuple 6 ∧ Ord y"
by (auto simp: is_Ind_def)

subsection ‹Various syntactic lemmas›

lemma eval_Var_q: "⟦«Var i»⟧ e = q_Var i"

lemma is_Var_eval_Var [simp]: "is_Var ⟦«Var i»⟧e"
by (metis decode_Var_q_Var is_Var_imp_decode_Var is_Var_q_Var)

section ‹The predicate ‹SeqCTermP›, for Terms and Constants›

(*SeqCTerm(s,k,t) ≡ LstSeq(s,k,t) ∧ (∀l∈k)[s l=0 ∨ Var(s l)∨(∃m,n∈l)[s l = ⟨Eats, s m, s n⟩]]*)
definition SeqCTerm :: "bool ⇒ hf ⇒ hf ⇒ hf ⇒ bool"
where "SeqCTerm vf s k t ≡ BuildSeq (λu. u=0 ∨ vf ∧ is_Var u) (λu v w. u = q_Eats v w) s k t"

nominal_function SeqCTermP :: "bool ⇒ tm ⇒ tm ⇒ tm ⇒ fm"
where "⟦atom l ♯ (s,k,sl,m,n,sm,sn);  atom sl ♯ (s,m,n,sm,sn);
atom m ♯ (s,n,sm,sn);  atom n ♯ (s,sm,sn);
atom sm ♯ (s,sn);  atom sn ♯ (s)⟧ ⟹
SeqCTermP vf s k t =
LstSeqP s k t AND
All2 l (SUCC k) (Ex sl (HPair (Var l) (Var sl) IN s AND
(Var sl EQ Zero OR (if vf then VarP (Var sl) else Fls) OR
Ex m (Ex n (Ex sm (Ex sn (Var m IN Var l AND Var n IN Var l AND
HPair (Var m) (Var sm) IN s AND HPair (Var n) (Var sn) IN s AND
Var sl EQ Q_Eats (Var sm) (Var sn))))))))"
by (auto simp: eqvt_def SeqCTermP_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)

nominal_termination (eqvt)
by lexicographic_order

lemma
shows SeqCTermP_fresh_iff [simp]:
"a ♯ SeqCTermP vf s k t ⟷ a ♯ s ∧ a ♯ k ∧ a ♯ t"  (is ?thesis1)
and eval_fm_SeqCTermP [simp]:
"eval_fm e (SeqCTermP vf s k t) ⟷ SeqCTerm vf ⟦s⟧e ⟦k⟧e ⟦t⟧e"    (is ?thesis2)
and SeqCTermP_sf [iff]:
"Sigma_fm (SeqCTermP vf s k t)"   (is ?thsf)
and SeqCTermP_imp_LstSeqP:
"{ SeqCTermP vf s k t } ⊢ LstSeqP s k t"  (is ?thlstseq)
and SeqCTermP_imp_OrdP [simp]:
"{ SeqCTermP vf s k t } ⊢ OrdP k"  (is ?thord)
proof -
obtain l::name and sl::name and m::name and n::name and sm::name and sn::name
where atoms: "atom l ♯ (s,k,sl,m,n,sm,sn)"   "atom sl ♯ (s,m,n,sm,sn)"
"atom m ♯ (s,n,sm,sn)"   "atom n ♯ (s,sm,sn)"
"atom sm ♯ (s,sn)"   "atom sn ♯ (s)"
by (metis obtain_fresh)
thus ?thesis1 ?thsf ?thlstseq ?thord
by (auto simp: LstSeqP.simps)
show ?thesis2 using atoms
by (simp cong: conj_cong add: LstSeq_imp_Ord SeqCTerm_def BuildSeq_def Builds_def
HBall_def HBex_def q_Eats_def Fls_def
Seq_iff_app [of "⟦s⟧e", OF LstSeq_imp_Seq_succ]
Ord_trans [of _ _ "succ ⟦k⟧e"])
qed

lemma SeqCTermP_subst [simp]:
"(SeqCTermP vf s k t)(j::=w) = SeqCTermP vf (subst j w s) (subst j w k) (subst j w t)"
proof -
obtain l::name and sl::name and m::name and n::name and sm::name and sn::name
where "atom l ♯ (j,w,s,k,sl,m,n,sm,sn)"   "atom sl ♯ (j,w,s,m,n,sm,sn)"
"atom m ♯ (j,w,s,n,sm,sn)"   "atom n ♯ (j,w,s,sm,sn)"
"atom sm ♯ (j,w,s,sn)"   "atom sn ♯ (j,w,s)"
by (metis obtain_fresh)
thus ?thesis
by (force simp add: SeqCTermP.simps [of l _ _ sl m n sm sn])
qed

declare SeqCTermP.simps [simp del]

abbreviation SeqTerm :: "hf ⇒ hf ⇒ hf ⇒ bool"
where "SeqTerm ≡ SeqCTerm True"

abbreviation SeqTermP :: "tm ⇒ tm ⇒ tm ⇒ fm"
where "SeqTermP ≡ SeqCTermP True"

abbreviation SeqConst :: "hf ⇒ hf ⇒ hf ⇒ bool"
where "SeqConst ≡ SeqCTerm False"

abbreviation SeqConstP :: "tm ⇒ tm ⇒ tm ⇒ fm"
where "SeqConstP ≡ SeqCTermP False"

lemma SeqConst_imp_SeqTerm: "SeqConst s k x ⟹ SeqTerm s k x"
by (auto simp: SeqCTerm_def intro: BuildSeq_mono)

lemma SeqConstP_imp_SeqTermP: "{SeqConstP s k t} ⊢ SeqTermP s k t"
proof -
obtain l::name and sl::name and m::name and n::name and sm::name and sn::name
where "atom l ♯ (s,k,t,sl,m,n,sm,sn)"   "atom sl ♯ (s,k,t,m,n,sm,sn)"
"atom m ♯ (s,k,t,n,sm,sn)"   "atom n ♯ (s,k,t,sm,sn)"
"atom sm ♯ (s,k,t,sn)"   "atom sn ♯ (s,k,t)"
by (metis obtain_fresh)
thus ?thesis
apply (auto simp: SeqCTermP.simps [of l s k sl m n sm sn])
apply (rule Ex_I [where x="Var l"], auto)
apply (rule Ex_I [where x = "Var sl"], force intro: Disj_I1)
apply (rule Ex_I [where x = "Var sl"], simp)
apply (rule Conj_I, blast)
apply (rule Disj_I2)+
apply (rule Ex_I [where x = "Var m"], simp)
apply (rule Ex_I [where x = "Var n"], simp)
apply (rule Ex_I [where x = "Var sm"], simp)
apply (rule Ex_I [where x = "Var sn"], auto)
done
qed

section ‹The predicates ‹TermP› and ‹ConstP››

subsection ‹Definition›

definition CTerm :: "bool ⇒ hf ⇒ bool"
where "CTerm vf t ≡ (∃s k. SeqCTerm vf s k t)"

nominal_function CTermP :: "bool ⇒ tm ⇒ fm"
where "⟦atom k ♯ (s,t); atom s ♯ t⟧ ⟹
CTermP vf t = Ex s (Ex k (SeqCTermP vf (Var s) (Var k) t))"
by (auto simp: eqvt_def CTermP_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)

nominal_termination (eqvt)
by lexicographic_order

lemma
shows CTermP_fresh_iff [simp]: "a ♯ CTermP vf t ⟷ a ♯ t"            (is ?thesis1)
and eval_fm_CTermP [simp] :"eval_fm e (CTermP vf t) ⟷ CTerm vf ⟦t⟧e"  (is ?thesis2)
and CTermP_sf [iff]: "Sigma_fm (CTermP vf t)"                      (is ?thsf)
proof -
obtain k::name and s::name  where "atom k ♯ (s,t)" "atom s ♯ t"
by (metis obtain_fresh)
thus ?thesis1 ?thesis2 ?thsf
by (auto simp: CTerm_def)
qed

lemma CTermP_subst [simp]: "(CTermP vf i)(j::=w) = CTermP vf (subst j w i)"
proof -
obtain k::name and s::name  where "atom k ♯ (s,i,j,w)" "atom s ♯ (i,j,w)"
by (metis obtain_fresh)
thus ?thesis
by (simp add: CTermP.simps [of k s])
qed

abbreviation Term :: "hf ⇒ bool"
where "Term ≡ CTerm True"

abbreviation TermP :: "tm ⇒ fm"
where "TermP ≡ CTermP True"

abbreviation Const :: "hf ⇒ bool"
where "Const ≡ CTerm False"

abbreviation ConstP :: "tm ⇒ fm"
where "ConstP ≡ CTermP False"

subsection ‹Correctness: It Corresponds to Quotations of Real Terms›

lemma wf_Term_quot_dbtm [simp]: "wf_dbtm u ⟹ Term ⟦quot_dbtm u⟧e"
by (induct rule: wf_dbtm.induct)
(auto simp: CTerm_def SeqCTerm_def q_Eats_def intro: BuildSeq_combine BuildSeq_exI)

corollary Term_quot_tm [iff]: fixes t :: tm  shows "Term ⟦«t»⟧e"
by (metis quot_tm_def wf_Term_quot_dbtm wf_dbtm_trans_tm)

lemma SeqCTerm_imp_wf_dbtm:
assumes "SeqCTerm vf s k x"
shows "∃t::dbtm. wf_dbtm t ∧ x = ⟦quot_dbtm t⟧e"
using assms [unfolded SeqCTerm_def]
proof (induct x rule: BuildSeq_induct)
case (B x) thus ?case
by auto (metis ORD_OF.simps(2) Var quot_dbtm.simps(2) is_Var_imp_decode_Var quot_Var)
next
case (C x y z)
then obtain tm1::dbtm and tm2::dbtm
where "wf_dbtm tm1" "y = ⟦quot_dbtm tm1⟧e"
"wf_dbtm tm2" "z = ⟦quot_dbtm tm2⟧e"
by blast
thus ?case
by (auto simp: wf_dbtm.intros C q_Eats_def intro!: exI [of _ "DBEats tm1 tm2"])
qed

corollary Term_imp_wf_dbtm:
assumes "Term x" obtains t where "wf_dbtm t" "x = ⟦quot_dbtm t⟧e"
by (metis assms SeqCTerm_imp_wf_dbtm CTerm_def)

corollary Term_imp_is_tm: assumes "Term x" obtains t::tm where "x = ⟦«t»⟧ e"
by (metis assms Term_imp_wf_dbtm quot_tm_def wf_dbtm_imp_is_tm)

lemma Term_Var: "Term (q_Var i)"
using wf_Term_quot_dbtm [of "DBVar i"]
by (metis Term_quot_tm is_Var_imp_decode_Var is_Var_q_Var)

lemma Term_Eats: assumes x: "Term x" and y: "Term y" shows "Term (q_Eats x y)"
proof -
obtain t u  where "x = ⟦quot_dbtm t⟧e" "y = ⟦quot_dbtm u⟧e"
by (metis Term_imp_wf_dbtm x y)
thus ?thesis using wf_Term_quot_dbtm [of "DBEats t u"] x y
by (auto simp: q_defs) (metis Eats Term_imp_wf_dbtm quot_dbtm_inject_lemma)
qed

subsection ‹Correctness properties for constants›

lemma Const_imp_Term: "Const x ⟹ Term x"
by (metis SeqConst_imp_SeqTerm CTerm_def)

lemma Const_0: "Const 0"
by (force simp add: CTerm_def SeqCTerm_def intro: BuildSeq_exI)

lemma ConstP_imp_TermP: "{ConstP t} ⊢ TermP t"
proof -
obtain k::name and s::name  where "atom k ♯ (s,t)" "atom s ♯ t"
by (metis obtain_fresh)
thus ?thesis
apply auto
apply (rule Ex_I [where x = "Var s"], simp)
apply (rule Ex_I [where x = "Var k"], auto intro: SeqConstP_imp_SeqTermP [THEN cut1])
done
qed

section ‹Abstraction over terms›

definition SeqStTerm :: "hf ⇒ hf ⇒ hf ⇒ hf ⇒ hf ⇒ hf ⇒ bool"
where "SeqStTerm v u x x' s k ≡
is_Var v ∧ BuildSeq2 (λy y'. (is_Ind y ∨ Ord y) ∧ y' = (if y=v then u else y))
(λu u' v v' w w'. u = q_Eats v w ∧ u' = q_Eats v' w') s k x x'"

definition AbstTerm :: "hf ⇒ hf ⇒ hf ⇒ hf ⇒ bool"
where "AbstTerm v i x x' ≡ Ord i ∧ (∃s k. SeqStTerm v (q_Ind i) x x' s k)"

subsection ‹Defining the syntax: quantified body›

nominal_function SeqStTermP :: "tm ⇒ tm ⇒ tm ⇒ tm ⇒ tm ⇒ tm ⇒ fm"
where "⟦atom l ♯ (s,k,v,i,sl,sl',m,n,sm,sm',sn,sn');
atom sl ♯ (s,v,i,sl',m,n,sm,sm',sn,sn'); atom sl' ♯ (s,v,i,m,n,sm,sm',sn,sn');
atom m ♯ (s,n,sm,sm',sn,sn'); atom n ♯ (s,sm,sm',sn,sn');
atom sm ♯ (s,sm',sn,sn'); atom sm' ♯ (s,sn,sn');
atom sn ♯ (s,sn'); atom sn' ♯ s⟧ ⟹
SeqStTermP v i t u s k =
VarP v AND LstSeqP s k (HPair t u) AND
All2 l (SUCC k) (Ex sl (Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND
(((Var sl EQ v AND Var sl' EQ i) OR
((IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl)) OR
Ex m (Ex n (Ex sm (Ex sm' (Ex sn (Ex sn' (Var m IN Var l AND Var n IN Var l AND
HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND
HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND
Var sl EQ Q_Eats (Var sm) (Var sn) AND
Var sl' EQ Q_Eats (Var sm') (Var sn')))))))))))"
apply (simp_all add: eqvt_def SeqStTermP_graph_aux_def flip_fresh_fresh)
by auto (metis obtain_fresh)

nominal_termination (eqvt)
by lexicographic_order

lemma
shows SeqStTermP_fresh_iff [simp]:
"a ♯ SeqStTermP v i t u s k ⟷ a ♯ v ∧ a ♯ i ∧ a ♯ t ∧ a ♯ u ∧ a ♯ s ∧ a ♯ k"  (is ?thesis1)
and eval_fm_SeqStTermP [simp]:
"eval_fm e (SeqStTermP v i t u s k) ⟷ SeqStTerm ⟦v⟧e ⟦i⟧e ⟦t⟧e ⟦u⟧e ⟦s⟧e ⟦k⟧e"  (is ?thesis2)
and SeqStTermP_sf [iff]:
"Sigma_fm (SeqStTermP v i t u s k)"  (is ?thsf)
and SeqStTermP_imp_OrdP:
"{ SeqStTermP v i t u s k } ⊢ OrdP k"  (is ?thord)
and SeqStTermP_imp_VarP:
"{ SeqStTermP v i t u s k } ⊢ VarP v"  (is ?thvar)
and SeqStTermP_imp_LstSeqP:
"{ SeqStTermP v i t u s k } ⊢ LstSeqP s k (HPair t u)"  (is ?thlstseq)
proof -
obtain l::name and sl::name and sl'::name and m::name and n::name and
sm::name and sm'::name and sn::name and sn'::name
where atoms:
"atom l ♯ (s,k,v,i,sl,sl',m,n,sm,sm',sn,sn')"
"atom sl ♯ (s,v,i,sl',m,n,sm,sm',sn,sn')" "atom sl' ♯ (s,v,i,m,n,sm,sm',sn,sn')"
"atom m ♯ (s,n,sm,sm',sn,sn')" "atom n ♯ (s,sm,sm',sn,sn')"
"atom sm ♯ (s,sm',sn,sn')" "atom sm' ♯ (s,sn,sn')"
"atom sn ♯ (s,sn')" "atom sn' ♯ (s)"
by (metis obtain_fresh)
thus ?thesis1 ?thsf ?thord ?thvar ?thlstseq
by (auto intro: LstSeqP_OrdP)
show ?thesis2 using atoms
apply (simp add: LstSeq_imp_Ord SeqStTerm_def ex_disj_distrib
BuildSeq2_def BuildSeq_def Builds_def
HBall_def q_Eats_def q_Ind_def is_Var_def
Seq_iff_app [of "⟦s⟧e", OF LstSeq_imp_Seq_succ]
Ord_trans [of _ _ "succ ⟦k⟧e"]
cong: conj_cong)
apply (rule conj_cong refl all_cong)+
apply auto
apply (metis Not_Ord_hpair is_Ind_def)
done
qed

lemma SeqStTermP_subst [simp]:
"(SeqStTermP v i t u s k)(j::=w) =
SeqStTermP (subst j w v) (subst j w i) (subst j w t) (subst j w u) (subst j w s) (subst j w k)"
proof -
obtain l::name and sl::name and sl'::name and m::name and n::name and
sm::name and sm'::name and sn::name and sn'::name
where "atom l ♯ (s,k,v,i,w,j,sl,sl',m,n,sm,sm',sn,sn')"
"atom sl ♯ (s,v,i,w,j,sl',m,n,sm,sm',sn,sn')"
"atom sl' ♯ (s,v,i,w,j,m,n,sm,sm',sn,sn')"
"atom m ♯ (s,w,j,n,sm,sm',sn,sn')" "atom n ♯ (s,w,j,sm,sm',sn,sn')"
"atom sm ♯ (s,w,j,sm',sn,sn')" "atom sm' ♯ (s,w,j,sn,sn')"
"atom sn ♯ (s,w,j,sn')" "atom sn' ♯ (s,w,j)"
by (metis obtain_fresh)
thus ?thesis
by (force simp add: SeqStTermP.simps [of l _ _ _ _ sl sl' m n sm sm' sn sn'])
qed

lemma SeqStTermP_cong:
"⟦H ⊢ t EQ t'; H ⊢ u EQ u'; H ⊢ s EQ s'; H ⊢ k EQ k'⟧
⟹ H ⊢ SeqStTermP v i t u s k IFF SeqStTermP v i t' u' s' k'"
by (rule P4_cong [where tms="[v,i]"]) (auto simp: fresh_Cons)

declare SeqStTermP.simps [simp del]

subsection ‹Defining the syntax: main predicate›

nominal_function AbstTermP :: "tm ⇒ tm ⇒ tm ⇒ tm ⇒ fm"
where "⟦atom s ♯ (v,i,t,u,k); atom k ♯ (v,i,t,u)⟧ ⟹
AbstTermP v i t u =
OrdP i AND Ex s (Ex k (SeqStTermP v (Q_Ind i) t u (Var s) (Var k)))"
by (auto simp: eqvt_def AbstTermP_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)

nominal_termination (eqvt)
by lexicographic_order

lemma
shows AbstTermP_fresh_iff [simp]:
"a ♯ AbstTermP v i t u ⟷ a ♯ v ∧ a ♯ i ∧ a ♯ t ∧ a ♯ u"  (is ?thesis1)
and eval_fm_AbstTermP [simp]:
"eval_fm e (AbstTermP v i t u) ⟷ AbstTerm ⟦v⟧e ⟦i⟧e ⟦t⟧e ⟦u⟧e "  (is ?thesis2)
and AbstTermP_sf [iff]:
"Sigma_fm (AbstTermP v i t u)"  (is ?thsf)
proof -
obtain s::name and k::name where "atom s ♯ (v,i,t,u,k)"  "atom k ♯ (v,i,t,u)"
by (metis obtain_fresh)
thus ?thesis1 ?thesis2 ?thsf
by (auto simp: AbstTerm_def q_defs)
qed

lemma AbstTermP_subst [simp]:
"(AbstTermP v i t u)(j::=w) = AbstTermP (subst j w v) (subst j w i) (subst j w t) (subst j w u)"
proof -
obtain s::name and k::name  where "atom s ♯ (v,i,t,u,w,j,k)"  "atom k ♯ (v,i,t,u,w,j)"
by (metis obtain_fresh)
thus ?thesis
by (simp add: AbstTermP.simps [of s _ _ _ _ k])
qed

declare AbstTermP.simps [simp del]

subsection ‹Correctness: It Coincides with Abstraction over real terms›

lemma not_is_Var_is_Ind: "is_Var v ⟹ ¬ is_Ind v"
by (auto simp: is_Var_def is_Ind_def)

lemma AbstTerm_imp_abst_dbtm:
assumes "AbstTerm v i x x'"
shows "∃t. x = ⟦quot_dbtm t⟧e ∧
x' = ⟦quot_dbtm (abst_dbtm (decode_Var v) (nat_of_ord i) t)⟧e"
proof -
obtain s k where v: "is_Var v" and i: "Ord i" and sk: "SeqStTerm v (q_Ind i) x x' s k"
using assms
by (auto simp: AbstTerm_def SeqStTerm_def)
from sk [unfolded SeqStTerm_def, THEN conjunct2]
show ?thesis
proof (induct x x' rule: BuildSeq2_induct)
case (B x x') thus ?case using v i
apply (auto simp: not_is_Var_is_Ind)
apply (rule_tac [1] x="DBInd (nat_of_ord (hsnd x))" in exI)
apply (rule_tac [2] x="DBVar (decode_Var v)" in exI)
apply (case_tac [3] "is_Var x")
apply (rule_tac [3] x="DBVar (decode_Var x)" in exI)
apply (rule_tac [4] x=DBZero in exI)
apply (auto simp: is_Ind_def q_Ind_def is_Var_iff [symmetric])
apply (metis hmem_0_Ord is_Var_def)
done
next
case (C x x' y y' z z')
then obtain tm1 and tm2
where "y = ⟦quot_dbtm tm1⟧e"
"y' = ⟦quot_dbtm (abst_dbtm (decode_Var v) (nat_of_ord i) tm1)⟧e"
"z = ⟦quot_dbtm tm2⟧e"
"z' = ⟦quot_dbtm (abst_dbtm (decode_Var v) (nat_of_ord i) tm2)⟧e"
by blast
thus ?case
by (auto simp: wf_dbtm.intros C q_Eats_def intro!: exI [where x="DBEats tm1 tm2"])
qed
qed

lemma AbstTerm_abst_dbtm:
"AbstTerm (q_Var i) (ord_of n) ⟦quot_dbtm t⟧e
⟦quot_dbtm (abst_dbtm i n t)⟧e"
by (induct t rule: dbtm.induct)
(auto simp: AbstTerm_def SeqStTerm_def q_defs intro: BuildSeq2_exI BuildSeq2_combine)

section ‹Substitution over terms›

definition SubstTerm :: "hf ⇒ hf ⇒ hf ⇒ hf ⇒ bool"
where "SubstTerm v u x x' ≡ Term u ∧ (∃s k. SeqStTerm v u x x' s k)"

subsection ‹Defining the syntax›

nominal_function SubstTermP :: "tm ⇒ tm ⇒ tm ⇒ tm ⇒ fm"
where "⟦atom s ♯ (v,i,t,u,k); atom k ♯ (v,i,t,u)⟧ ⟹
SubstTermP v i t u = TermP i AND Ex s (Ex k (SeqStTermP v i t u (Var s) (Var k)))"
by (auto simp: eqvt_def SubstTermP_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)

nominal_termination (eqvt)
by lexicographic_order

lemma
shows SubstTermP_fresh_iff [simp]:
"a ♯ SubstTermP v i t u ⟷ a ♯ v ∧ a ♯ i ∧ a ♯ t ∧ a ♯ u"  (is ?thesis1)
and eval_fm_SubstTermP [simp]:
"eval_fm e (SubstTermP v i t u) ⟷ SubstTerm ⟦v⟧e ⟦i⟧e ⟦t⟧e ⟦u⟧e"  (is ?thesis2)
and SubstTermP_sf [iff]:
"Sigma_fm (SubstTermP v i t u)"     (is ?thsf)
and SubstTermP_imp_TermP:
"{ SubstTermP v i t u } ⊢ TermP i"  (is ?thterm)
and SubstTermP_imp_VarP:
"{ SubstTermP v i t u } ⊢ VarP v"   (is ?thvar)
proof -
obtain s::name and k::name  where "atom s ♯ (v,i,t,u,k)" "atom k ♯ (v,i,t,u)"
by (metis obtain_fresh)
thus ?thesis1 ?thesis2 ?thsf ?thterm ?thvar
by (auto simp: SubstTerm_def intro: SeqStTermP_imp_VarP thin2)
qed

lemma SubstTermP_subst [simp]:
"(SubstTermP v i t u)(j::=w) = SubstTermP (subst j w v) (subst j w i) (subst j w t) (subst j w u)"
proof -
obtain s::name and k::name
where "atom s ♯ (v,i,t,u,w,j,k)"  "atom k ♯ (v,i,t,u,w,j)"
by (metis obtain_fresh)
thus ?thesis
by (simp add: SubstTermP.simps [of s _ _ _ _ k])
qed

lemma SubstTermP_cong:
"⟦H ⊢ v EQ v'; H ⊢ i EQ i'; H ⊢ t EQ t'; H ⊢ u EQ u'⟧
⟹ H ⊢ SubstTermP v i t u IFF SubstTermP v' i' t' u'"
by (rule P4_cong) auto

declare SubstTermP.simps [simp del]

lemma SubstTerm_imp_subst_dbtm:
assumes "SubstTerm v ⟦quot_dbtm u⟧e x x'"
shows "∃t. x = ⟦quot_dbtm t⟧e ∧
x' = ⟦quot_dbtm (subst_dbtm u (decode_Var v) t)⟧e"
proof -
obtain s k where v: "is_Var v" and u: "Term ⟦quot_dbtm u⟧e"
and sk: "SeqStTerm v ⟦quot_dbtm u⟧e x x' s k"
using assms [unfolded SubstTerm_def]
by (auto simp: SeqStTerm_def)
from sk [unfolded SeqStTerm_def, THEN conjunct2]
show ?thesis
proof (induct x x' rule: BuildSeq2_induct)
case (B x x') thus ?case using v
apply (auto simp: not_is_Var_is_Ind)
apply (rule_tac [1] x="DBInd (nat_of_ord (hsnd x))" in exI)
apply (rule_tac [2] x="DBVar (decode_Var v)" in exI)
apply (case_tac [3] "is_Var x")
apply (rule_tac [3] x="DBVar (decode_Var x)" in exI)
apply (rule_tac [4] x=DBZero in exI)
apply (auto simp: is_Ind_def q_Ind_def is_Var_iff [symmetric])
apply (metis hmem_0_Ord is_Var_def)
done
next
case (C x x' y y' z z')
then obtain tm1 and tm2
where "y = ⟦quot_dbtm tm1⟧e"
"y' = ⟦quot_dbtm (subst_dbtm u (decode_Var v) tm1)⟧e"
"z = ⟦quot_dbtm tm2⟧e"
"z' = ⟦quot_dbtm (subst_dbtm u (decode_Var v) tm2)⟧e"
by blast
thus ?case
by (auto simp: wf_dbtm.intros C q_Eats_def intro!: exI [where x="DBEats tm1 tm2"])
qed
qed

corollary SubstTerm_imp_subst_dbtm':
assumes "SubstTerm v y x x'"
obtains t::dbtm and u::dbtm
where "y = ⟦quot_dbtm u⟧e"
"x = ⟦quot_dbtm t⟧e"
"x' = ⟦quot_dbtm (subst_dbtm u (decode_Var v) t)⟧e"
by (metis SubstTerm_def SubstTerm_imp_subst_dbtm Term_imp_is_tm assms quot_tm_def)

lemma SubstTerm_subst_dbtm:
assumes "Term ⟦quot_dbtm u⟧e"
shows "SubstTerm (q_Var v) ⟦quot_dbtm u⟧e ⟦quot_dbtm t⟧e ⟦quot_dbtm (subst_dbtm u v t)⟧e"
by (induct t rule: dbtm.induct)
(auto simp: assms SubstTerm_def SeqStTerm_def q_defs intro: BuildSeq2_exI BuildSeq2_combine)

section ‹Abstraction over formulas›

subsection ‹The predicate ‹AbstAtomicP››

definition AbstAtomic :: "hf ⇒ hf ⇒ hf ⇒ hf ⇒ bool"
where "AbstAtomic v i y y' ≡
(∃t u t' u'. AbstTerm v i t t' ∧ AbstTerm v i u u' ∧
((y = q_Eq t u ∧ y' = q_Eq t' u') ∨ (y = q_Mem t u ∧ y' = q_Mem t' u')))"

nominal_function AbstAtomicP :: "tm ⇒ tm ⇒ tm ⇒ tm ⇒ fm"
where "⟦atom t ♯ (v,i,y,y',t',u,u'); atom t' ♯ (v,i,y,y',u,u');
atom u ♯ (v,i,y,y',u'); atom u' ♯ (v,i,y,y')⟧ ⟹
AbstAtomicP v i y y' =
Ex t (Ex u (Ex t' (Ex u'
(AbstTermP v i (Var t) (Var t') AND AbstTermP v i (Var u) (Var u') AND
((y EQ Q_Eq (Var t) (Var u) AND y' EQ Q_Eq (Var t') (Var u')) OR
(y EQ Q_Mem (Var t) (Var u) AND y' EQ Q_Mem (Var t') (Var u')))))))"
by (auto simp: eqvt_def AbstAtomicP_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)

nominal_termination (eqvt)
by lexicographic_order

lemma
shows AbstAtomicP_fresh_iff [simp]:
"a ♯ AbstAtomicP v i y y' ⟷ a ♯ v ∧ a ♯ i ∧ a ♯ y ∧ a ♯ y'"         (is ?thesis1)
and eval_fm_AbstAtomicP [simp]:
"eval_fm e (AbstAtomicP v i y y') ⟷ AbstAtomic ⟦v⟧e ⟦i⟧e ⟦y⟧e ⟦y'⟧e"  (is ?thesis2)
and AbstAtomicP_sf [iff]: "Sigma_fm (AbstAtomicP v i y y')"              (is ?thsf)
proof -
obtain t::name and u::name and t'::name  and u'::name
where "atom t ♯ (v,i,y,y',t',u,u')" "atom t' ♯ (v,i,y,y',u,u')"
"atom u ♯ (v,i,y,y',u')" "atom u' ♯ (v,i,y,y')"
by (metis obtain_fresh)
thus ?thesis1 ?thesis2 ?thsf
by (auto simp: AbstAtomic_def q_defs)
qed

lemma AbstAtomicP_subst [simp]:
"(AbstAtomicP v tm y y')(i::=w) = AbstAtomicP (subst i w v) (subst i w tm) (subst i w y) (subst i w y')"
proof -
obtain t::name and u::name and t'::name  and u'::name
where "atom t ♯ (v,tm,y,y',w,i,t',u,u')"  "atom t' ♯ (v,tm,y,y',w,i,u,u')"
"atom u ♯ (v,tm,y,y',w,i,u')"       "atom u' ♯ (v,tm,y,y',w,i)"
by (metis obtain_fresh)
thus ?thesis
by (simp add: AbstAtomicP.simps [of t _ _ _ _ t' u u'])
qed

declare AbstAtomicP.simps [simp del]

subsection ‹The predicate ‹AbsMakeForm››

definition AbstMakeForm :: "hf ⇒ hf ⇒ hf ⇒ hf ⇒ hf ⇒ hf ⇒ hf ⇒ hf ⇒ hf ⇒ bool"
where "AbstMakeForm k y y' i u u' j w w' ≡
Ord k ∧
((k = i ∧ k = j ∧ y = q_Disj u w ∧ y' = q_Disj u' w') ∨
(k = i ∧ y = q_Neg u ∧ y' = q_Neg u') ∨
(succ k = i ∧ y = q_Ex u ∧ y' = q_Ex u'))"

definition SeqAbstForm :: "hf ⇒ hf ⇒ hf ⇒ hf ⇒ hf ⇒ hf ⇒ bool"
where "SeqAbstForm v i x x' s k ≡
BuildSeq3 (AbstAtomic v) AbstMakeForm s k i x x'"

nominal_function SeqAbstFormP :: "tm ⇒ tm ⇒ tm ⇒ tm ⇒ tm ⇒ tm ⇒ fm"
where "⟦atom l ♯ (s,k,v,sli,sl,sl',m,n,smi,sm,sm',sni,sn,sn');
atom sli ♯ (s,v,sl,sl',m,n,smi,sm,sm',sni,sn,sn');
atom sl ♯ (s,v,sl',m,n,smi,sm,sm',sni,sn,sn');
atom sl' ♯ (s,v,m,n,smi,sm,sm',sni,sn,sn');
atom m ♯ (s,n,smi,sm,sm',sni,sn,sn');
atom n ♯ (s,smi,sm,sm',sni,sn,sn'); atom smi ♯ (s,sm,sm',sni,sn,sn');
atom sm ♯ (s,sm',sni,sn,sn'); atom sm' ♯ (s,sni,sn,sn');
atom sni ♯ (s,sn,sn'); atom sn ♯ (s,sn'); atom sn' ♯ (s)⟧ ⟹
SeqAbstFormP v i x x' s k =
LstSeqP s k (HPair i (HPair x x')) AND
All2 l (SUCC k) (Ex sli (Ex sl (Ex sl' (HPair (Var l) (HPair (Var sli) (HPair (Var sl) (Var sl'))) IN s AND
(AbstAtomicP v (Var sli) (Var sl) (Var sl') OR
OrdP (Var sli) AND
Ex m (Ex n (Ex smi (Ex sm (Ex sm' (Ex sni (Ex sn (Ex sn'
(Var m IN Var l AND Var n IN Var l AND
HPair (Var m) (HPair (Var smi) (HPair (Var sm) (Var sm'))) IN s AND
HPair (Var n) (HPair (Var sni) (HPair (Var sn) (Var sn'))) IN s AND
((Var sli EQ Var smi AND Var sli EQ Var sni AND
Var sl EQ Q_Disj (Var sm) (Var sn) AND
Var sl' EQ Q_Disj (Var sm') (Var sn')) OR
(Var sli EQ Var smi AND
Var sl EQ Q_Neg (Var sm) AND Var sl' EQ Q_Neg (Var sm')) OR
(SUCC (Var sli) EQ Var smi AND
Var sl EQ Q_Ex (Var sm) AND Var sl' EQ Q_Ex (Var sm'))))))))))))))))"
by (auto simp: eqvt_def SeqAbstFormP_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)

nominal_termination (eqvt)
by lexicographic_order

lemma
shows SeqAbstFormP_fresh_iff [simp]:
"a ♯ SeqAbstFormP v i x x' s k ⟷ a ♯ v ∧ a ♯ i ∧ a ♯ x ∧ a ♯ x' ∧ a ♯ s ∧ a ♯ k"  (is ?thesis1)
and eval_fm_SeqAbstFormP [simp]:
"eval_fm e (SeqAbstFormP v i x x' s k) ⟷ SeqAbstForm ⟦v⟧e ⟦i⟧e ⟦x⟧e ⟦x'⟧e ⟦s⟧e ⟦k⟧e" (is ?thesis2)
and SeqAbstFormP_sf [iff]:
"Sigma_fm (SeqAbstFormP v i x x' s k)"  (is ?thsf)
proof -
obtain l::name and sli::name and sl::name and sl'::name and m::name and n::name and
smi::name and sm::name and sm'::name and sni::name and sn::name and sn'::name
where atoms:
"atom l ♯ (s,k,v,sli,sl,sl',m,n,smi,sm,sm',sni,sn,sn')"
"atom sli ♯ (s,v,sl,sl',m,n,smi,sm,sm',sni,sn,sn')"
"atom sl ♯ (s,v,sl',m,n,smi,sm,sm',sni,sn,sn')"
"atom sl' ♯ (s,v,m,n,smi,sm,sm',sni,sn,sn')"
"atom m ♯ (s,n,smi,sm,sm',sni,sn,sn')" "atom n ♯ (s,smi,sm,sm',sni,sn,sn')"
"atom smi ♯ (s,sm,sm',sni,sn,sn')"
"atom sm ♯ (s,sm',sni,sn,sn')"
"atom sm' ♯ (s,sni,sn,sn')"
"atom sni ♯ (s,sn,sn')" "atom sn ♯ (s,sn')" "atom sn' ♯ s"
by (metis obtain_fresh)
thus ?thesis1 ?thsf
by (auto intro: LstSeqP_OrdP)
show ?thesis2 using atoms
unfolding SeqAbstForm_def BuildSeq3_def BuildSeq_def Builds_def
HBall_def HBex_def q_defs AbstMakeForm_def
by (force simp add: LstSeq_imp_Ord   Ord_trans [of _ _ "succ ⟦k⟧e"]
Seq_iff_app [of "⟦s⟧e", OF LstSeq_imp_Seq_succ]
intro!: conj_cong [OF refl] all_cong)
qed

lemma SeqAbstFormP_subst [simp]:
"(SeqAbstFormP v u x x' s k)(i::=t) =
SeqAbstFormP (subst i t v) (subst i t u) (subst i t x) (subst i t x') (subst i t s) (subst i t k)"
proof -
obtain l::name and sli::name and sl::name and sl'::name and m::name and n::name and
smi::name and sm::name and sm'::name and sni::name and sn::name and sn'::name
where "atom l ♯ (i,t,s,k,v,sli,sl,sl',m,n,smi,sm,sm',sni,sn,sn')"
"atom sli ♯ (i,t,s,v,sl,sl',m,n,smi,sm,sm',sni,sn,sn')"
"atom sl ♯ (i,t,s,v,sl',m,n,smi,sm,sm',sni,sn,sn')"
"atom sl' ♯ (i,t,s,v,m,n,smi,sm,sm',sni,sn,sn')"
"atom m ♯ (i,t,s,n,smi,sm,sm',sni,sn,sn')"
"atom n ♯ (i,t,s,smi,sm,sm',sni,sn,sn')"
"atom smi ♯ (i,t,s,sm,sm',sni,sn,sn')"
"atom sm ♯ (i,t,s,sm',sni,sn,sn')" "atom sm' ♯ (i,t,s,sni,sn,sn')"
"atom sni ♯ (i,t,s,sn,sn')" "atom sn ♯ (i,t,s,sn')" "atom sn' ♯ (i,t,s)"
by (metis obtain_fresh)
thus ?thesis
by (force simp add: SeqAbstFormP.simps [of l _ _ _ sli sl sl' m n smi sm sm' sni sn sn'])
qed

declare SeqAbstFormP.simps [simp del]

subsection ‹Defining the syntax: the main AbstForm predicate›

definition AbstForm :: "hf ⇒ hf ⇒ hf ⇒ hf ⇒ bool"
where "AbstForm v i x x' ≡ is_Var v ∧ Ord i ∧ (∃s k. SeqAbstForm v i x x' s k)"

nominal_function AbstFormP :: "tm ⇒ tm ⇒ tm ⇒ tm ⇒ fm"
where "⟦atom s ♯ (v,i,x,x',k);
atom k ♯ (v,i,x,x')⟧ ⟹
AbstFormP v i x x' = VarP v AND OrdP i AND Ex s (Ex k (SeqAbstFormP v i x x' (Var s) (Var k)))"
by (auto simp: eqvt_def AbstFormP_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)

nominal_termination (eqvt)
by lexicographic_order

lemma
shows AbstFormP_fresh_iff [simp]:
"a ♯ AbstFormP v i x x' ⟷ a ♯ v ∧ a ♯ i ∧ a ♯ x ∧ a ♯ x'" (is ?thesis1)
and eval_fm_AbstFormP [simp]:
"eval_fm e (AbstFormP v i x x') ⟷ AbstForm ⟦v⟧e ⟦i⟧e ⟦x⟧e ⟦x'⟧e" (is ?thesis2)
and AbstFormP_sf [iff]:
"Sigma_fm (AbstFormP v i x x')"    (is ?thsf)
proof -
obtain s::name and k::name  where "atom s ♯ (v,i,x,x',k)" "atom k ♯ (v,i,x,x')"
by (metis obtain_fresh)
thus ?thesis1 ?thesis2 ?thsf
by (auto simp: AbstForm_def)
qed

lemma AbstFormP_subst [simp]:
"(AbstFormP v i x x')(j::=t) = AbstFormP (subst j t v) (subst j t i) (subst j t x) (subst j t x')"
proof -
obtain s::name and k::name  where "atom s ♯ (v,i,x,x',t,j,k)" "atom k ♯ (v,i,x,x',t,j)"
by (metis obtain_fresh)
thus ?thesis
by (auto simp: AbstFormP.simps [of s _ _ _ _ k])
qed

declare AbstFormP.simps [simp del]

subsection ‹Correctness: It Coincides with Abstraction over real Formulas›

lemma AbstForm_imp_Ord: "AbstForm v u x x' ⟹ Ord v"
by (metis AbstForm_def is_Var_def)

lemma AbstForm_imp_abst_dbfm:
assumes "AbstForm v i x x'"
shows "∃A. x = ⟦quot_dbfm A⟧e ∧
x' = ⟦quot_dbfm (abst_dbfm (decode_Var v) (nat_of_ord i) A)⟧e"
proof -
obtain s k where v: "is_Var v" and i: "Ord i" and sk: "SeqAbstForm v i x x' s k"
using assms [unfolded AbstForm_def]
by auto
from sk [unfolded SeqAbstForm_def]
show ?thesis
proof (induction i x x' rule: BuildSeq3_induct)
case (B i x x') thus ?case
apply (auto simp: AbstAtomic_def dest!: AbstTerm_imp_abst_dbtm [where e=e])
apply (rule_tac [1] x="DBEq ta tb" in exI)
apply (rule_tac [2] x="DBMem ta tb" in exI)
apply (auto simp: q_defs)
done
next
case (C i x x' j y y' k z z')
then obtain A1 and A2
where "y = ⟦quot_dbfm A1⟧e"
"y' = ⟦quot_dbfm (abst_dbfm (decode_Var v) (nat_of_ord j) A1)⟧e"
"z = ⟦quot_dbfm A2⟧e"
"z' = ⟦quot_dbfm (abst_dbfm (decode_Var v) (nat_of_ord k) A2)⟧e"
by blast
with C.hyps show ?case
apply (auto simp: AbstMakeForm_def)
apply (rule_tac [1] x="DBDisj A1 A2" in exI)
apply (rule_tac [2] x="DBNeg A1" in exI)
apply (rule_tac [3] x="DBEx A1" in exI)
apply (auto simp: C q_defs)
done
qed
qed

lemma AbstForm_abst_dbfm:
"AbstForm (q_Var i) (ord_of n) ⟦quot_dbfm fm⟧e ⟦quot_dbfm (abst_dbfm i n fm)⟧e"
apply (induction fm arbitrary: n rule: dbfm.induct)
apply (force simp add: AbstForm_def SeqAbstForm_def AbstMakeForm_def AbstAtomic_def
AbstTerm_abst_dbtm htuple_minus_1 q_defs simp del: q_Var_def
intro: BuildSeq3_exI BuildSeq3_combine)+
done

section ‹Substitution over formulas›

subsection ‹The predicate ‹SubstAtomicP››

definition SubstAtomic :: "hf ⇒ hf ⇒ hf ⇒ hf ⇒ bool"
where "SubstAtomic v tm y y' ≡
(∃t u t' u'. SubstTerm v tm t t' ∧ SubstTerm v tm u u' ∧
((y = q_Eq t u ∧ y' = q_Eq t' u') ∨ (y = q_Mem t u ∧ y' = q_Mem t' u')))"

nominal_function SubstAtomicP :: "tm ⇒ tm ⇒ tm ⇒ tm ⇒ fm"
where "⟦atom t ♯ (v,tm,y,y',t',u,u');
atom t' ♯ (v,tm,y,y',u,u');
atom u ♯ (v,tm,y,y',u');
atom u' ♯ (v,tm,y,y')⟧ ⟹
SubstAtomicP v tm y y' =
Ex t (Ex u (Ex t' (Ex u'
(SubstTermP v tm (Var t) (Var t') AND SubstTermP v tm (Var u) (Var u') AND
((y EQ Q_Eq (Var t) (Var u) AND y' EQ Q_Eq (Var t') (Var u')) OR
(y EQ Q_Mem (Var t) (Var u) AND y' EQ Q_Mem (Var t') (Var u')))))))"
by (auto simp: eqvt_def SubstAtomicP_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)

nominal_termination (eqvt)
by lexicographic_order

lemma
shows SubstAtomicP_fresh_iff [simp]:
"a ♯ SubstAtomicP v tm y y' ⟷ a ♯ v ∧ a ♯ tm ∧ a ♯ y ∧ a ♯ y'"           (is ?thesis1)
and eval_fm_SubstAtomicP [simp]:
"eval_fm e (SubstAtomicP v tm y y') ⟷ SubstAtomic ⟦v⟧e ⟦tm⟧e ⟦y⟧e ⟦y'⟧e"  (is ?thesis2)
and SubstAtomicP_sf [iff]: "Sigma_fm (SubstAtomicP v tm y y')"               (is ?thsf)
proof -
obtain t::name and u::name and t'::name  and u'::name
where "atom t ♯ (v,tm,y,y',t',u,u')" "atom t' ♯ (v,tm,y,y',u,u')"
"atom u ♯ (v,tm,y,y',u')" "atom u' ♯ (v,tm,y,y')"
by (metis obtain_fresh)
thus ?thesis1 ?thesis2 ?thsf
by (auto simp: SubstAtomic_def q_defs)
qed

lemma SubstAtomicP_subst [simp]:
"(SubstAtomicP v tm y y')(i::=w) = SubstAtomicP (subst i w v) (subst i w tm) (subst i w y) (subst i w y')"
proof -
obtain t::name and u::name and t'::name  and u'::name
where "atom t ♯ (v,tm,y,y',w,i,t',u,u')" "atom t' ♯ (v,tm,y,y',w,i,u,u')"
"atom u ♯ (v,tm,y,y',w,i,u')" "atom u' ♯ (v,tm,y,y',w,i)"
by (metis obtain_fresh)
thus ?thesis
by (simp add: SubstAtomicP.simps [of t _ _ _ _ t' u u'])
qed

lemma SubstAtomicP_cong:
"⟦H ⊢ v EQ v'; H ⊢ tm EQ tm'; H ⊢ x EQ x'; H ⊢ y EQ y'⟧
⟹ H ⊢ SubstAtomicP v tm x y IFF SubstAtomicP v' tm' x' y'"
by (rule P4_cong) auto

subsection ‹The predicate ‹SubstMakeForm››

definition SubstMakeForm :: "hf ⇒ hf ⇒ hf ⇒ hf ⇒ hf ⇒ hf ⇒ bool"
where "SubstMakeForm y y' u u' w w' ≡
((y = q_Disj u w ∧ y' = q_Disj u' w') ∨
(y = q_Neg u ∧ y' = q_Neg u') ∨
(y = q_Ex u ∧ y' = q_Ex u'))"

definition SeqSubstForm :: "hf ⇒ hf ⇒ hf ⇒ hf ⇒ hf ⇒ hf ⇒ bool"
where "SeqSubstForm v u x x' s k ≡ BuildSeq2 (SubstAtomic v u) SubstMakeForm s k x x'"

nominal_function SeqSubstFormP :: "tm ⇒ tm ⇒ tm ⇒ tm ⇒ tm ⇒ tm ⇒ fm"
where "⟦atom l ♯ (s,k,v,u,sl,sl',m,n,sm,sm',sn,sn');
atom sl ♯ (s,v,u,sl',m,n,sm,sm',sn,sn');
atom sl' ♯ (s,v,u,m,n,sm,sm',sn,sn');
atom m ♯ (s,n,sm,sm',sn,sn'); atom n ♯ (s,sm,sm',sn,sn');
atom sm ♯ (s,sm',sn,sn'); atom sm' ♯ (s,sn,sn');
atom sn ♯ (s,sn'); atom sn' ♯ s⟧ ⟹
SeqSubstFormP v u x x' s k =
LstSeqP s k (HPair x x') AND
All2 l (SUCC k) (Ex sl (Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND
(SubstAtomicP v u (Var sl) (Var sl') OR
Ex m (Ex n (Ex sm (Ex sm' (Ex sn (Ex sn' (Var m IN Var l AND Var n IN Var l AND
HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND
HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND
((Var sl EQ Q_Disj (Var sm) (Var sn) AND
Var sl' EQ Q_Disj (Var sm') (Var sn')) OR
(Var sl EQ Q_Neg (Var sm) AND Var sl' EQ Q_Neg (Var sm')) OR
(Var sl EQ Q_Ex (Var sm) AND Var sl' EQ Q_Ex (Var sm')))))))))))))"
apply (simp_all add: eqvt_def SeqSubstFormP_graph_aux_def flip_fresh_fresh)
by auto (metis obtain_fresh)

nominal_termination (eqvt)
by lexicographic_order

lemma
shows SeqSubstFormP_fresh_iff [simp]:
"a ♯ SeqSubstFormP v u x x' s k ⟷ a ♯ v ∧ a ♯ u ∧ a ♯ x ∧ a ♯ x' ∧ a ♯ s ∧ a ♯ k"  (is ?thesis1)
and eval_fm_SeqSubstFormP [simp]:
"eval_fm e (SeqSubstFormP v u x x' s k) ⟷
SeqSubstForm ⟦v⟧e ⟦u⟧e ⟦x⟧e ⟦x'⟧e ⟦s⟧e ⟦k⟧e" (is ?thesis2)
and SeqSubstFormP_sf [iff]:
"Sigma_fm (SeqSubstFormP v u x x' s k)"  (is ?thsf)
and SeqSubstFormP_imp_OrdP:
"{ SeqSubstFormP v u x x' s k } ⊢ OrdP k"  (is ?thOrd)
and SeqSubstFormP_imp_LstSeqP:
"{ SeqSubstFormP v u x x' s k } ⊢ LstSeqP s k (HPair x x')"  (is ?thLstSeq)
proof -
obtain l::name and sl::name and sl'::name and m::name and n::name and
sm::name and sm'::name and sn::name and sn'::name
where atoms:
"atom l ♯ (s,k,v,u,sl,sl',m,n,sm,sm',sn,sn')"
"atom sl ♯ (s,v,u,sl',m,n,sm,sm',sn,sn')"
"atom sl' ♯ (s,v,u,m,n,sm,sm',sn,sn')"
"atom m ♯ (s,n,sm,sm',sn,sn')" "atom n ♯ (s,sm,sm',sn,sn')"
"atom sm ♯ (s,sm',sn,sn')" "atom sm' ♯ (s,sn,sn')"
"atom sn ♯ (s,sn')" "atom sn' ♯ (s)"
by (metis obtain_fresh)
thus ?thesis1 ?thsf ?thOrd ?thLstSeq
by (auto intro: LstSeqP_OrdP)
show ?thesis2 using atoms
unfolding SeqSubstForm_def BuildSeq2_def BuildSeq_def Builds_def
HBall_def HBex_def q_defs SubstMakeForm_def
by (force simp add: LstSeq_imp_Ord   Ord_trans [of _ _ "succ ⟦k⟧e"]
Seq_iff_app [of "⟦s⟧e", OF LstSeq_imp_Seq_succ]
intro!: conj_cong [OF refl]  all_cong)
qed

lemma SeqSubstFormP_subst [simp]:
"(SeqSubstFormP v u x x' s k)(i::=t) =
SeqSubstFormP (subst i t v) (subst i t u) (subst i t x) (subst i t x') (subst i t s) (subst i t k)"
proof -
obtain l::name and sl::name and sl'::name and m::name and n::name and
sm::name and sm'::name and sn::name and sn'::name
where "atom l ♯ (s,k,v,u,t,i,sl,sl',m,n,sm,sm',sn,sn')"
"atom sl ♯ (s,v,u,t,i,sl',m,n,sm,sm',sn,sn')"
"atom sl' ♯ (s,v,u,t,i,m,n,sm,sm',sn,sn')"
"atom m ♯ (s,t,i,n,sm,sm',sn,sn')" "atom n ♯ (s,t,i,sm,sm',sn,sn')"
"atom sm ♯ (s,t,i,sm',sn,sn')" "atom sm' ♯ (s,t,i,sn,sn')"
"atom sn ♯ (s,t,i,sn')" "atom sn' ♯ (s,t,i)"
by (metis obtain_fresh)
thus ?thesis
by (force simp add: SeqSubstFormP.simps [of l _ _ _ _ sl sl' m n sm sm' sn sn'])
qed

lemma SeqSubstFormP_cong:
"⟦H ⊢ t EQ t'; H ⊢ u EQ u'; H ⊢ s EQ s'; H ⊢ k EQ k'⟧
⟹ H ⊢ SeqSubstFormP v i t u s k IFF SeqSubstFormP v i t' u' s' k'"
by (rule P4_cong [where tms="[v,i]"]) (auto simp: fresh_Cons)

declare SeqSubstFormP.simps [simp del]

subsection ‹Defining the syntax: the main SubstForm predicate›

definition SubstForm :: "hf ⇒ hf ⇒ hf ⇒ hf ⇒ bool"
where "SubstForm v u x x' ≡ is_Var v ∧ Term u ∧ (∃s k. SeqSubstForm v u x x' s k)"

nominal_function SubstFormP :: "tm ⇒ tm ⇒ tm ⇒ tm ⇒ fm"
where "⟦atom s ♯ (v,i,x,x',k); atom k ♯ (v,i,x,x')⟧ ⟹
SubstFormP v i x x' =
VarP v AND TermP i AND Ex s (Ex k (SeqSubstFormP v i x x' (Var s) (Var k)))"
by (auto simp: eqvt_def SubstFormP_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)

nominal_termination (eqvt)
by lexicographic_order

lemma
shows SubstFormP_fresh_iff [simp]:
"a ♯ SubstFormP v i x x' ⟷ a ♯ v ∧ a ♯ i ∧ a ♯ x ∧ a ♯ x'"  (is ?thesis1)
and eval_fm_SubstFormP [simp]:
"eval_fm e (SubstFormP v i x x') ⟷ SubstForm ⟦v⟧e ⟦i⟧e ⟦x⟧e ⟦x'⟧e"  (is ?thesis2)
and SubstFormP_sf [iff]:
"Sigma_fm (SubstFormP v i x x')"  (is ?thsf)
proof -
obtain s::name and k::name
where "atom s ♯ (v,i,x,x',k)"  "atom k ♯ (v,i,x,x')"
by (metis obtain_fresh)
thus ?thesis1 ?thesis2 ?thsf
by (auto simp: SubstForm_def)
qed

lemma SubstFormP_subst [simp]:
"(SubstFormP v i x x')(j::=t) = SubstFormP (subst j t v) (subst j t i) (subst j t x) (subst j t x')"
proof -
obtain s::name and k::name  where "atom s ♯ (v,i,x,x',t,j,k)" "atom k ♯ (v,i,x,x',t,j)"
by (metis obtain_fresh)
thus ?thesis
by (auto simp: SubstFormP.simps [of s _ _ _ _ k])
qed

lemma SubstFormP_cong:
"⟦H ⊢ v EQ v'; H ⊢ i EQ i'; H ⊢ t EQ t'; H ⊢ u EQ u'⟧
⟹ H ⊢ SubstFormP v i t u IFF SubstFormP v' i' t' u'"
by (rule P4_cong) auto

lemma ground_SubstFormP [simp]: "ground_fm (SubstFormP v y x x') ⟷ ground v ∧ ground y ∧ ground x ∧ ground x'"
by (auto simp: ground_aux_def ground_fm_aux_def supp_conv_fresh)

declare SubstFormP.simps [simp del]

subsection ‹Correctness of substitution over formulas›

lemma SubstForm_imp_subst_dbfm_lemma:
assumes "SubstForm v ⟦quot_dbtm u⟧e x x'"
shows "∃A. x = ⟦quot_dbfm A⟧e ∧
x' = ⟦quot_dbfm (subst_dbfm u (decode_Var v) A)⟧e"
proof -
obtain s k where v: "is_Var v" and u: "Term ⟦quot_dbtm u⟧e"
and sk: "SeqSubstForm v ⟦quot_dbtm u⟧e x x' s k"
using assms [unfolded SubstForm_def]
by blast
from sk [unfolded SeqSubstForm_def]
show ?thesis
proof (induct x x' rule: BuildSeq2_induct)
case (B x x') thus ?case
apply (auto simp: SubstAtomic_def elim!: SubstTerm_imp_subst_dbtm' [where e=e])
apply (rule_tac [1] x="DBEq ta tb" in exI)
apply (rule_tac [2] x="DBMem ta tb" in exI)
apply (auto simp: q_defs)
done
next
case (C x x' y y' z z')
then obtain A and B
where "y = ⟦quot_dbfm A⟧e" "y' = ⟦quot_dbfm (subst_dbfm u (decode_Var v) A)⟧e"
"z = ⟦quot_dbfm B⟧e" "z' = ⟦quot_dbfm (subst_dbfm u (decode_Var v) B)⟧e"
by blast
with C.hyps show ?case
apply (auto simp: SubstMakeForm_def)
apply (rule_tac [1] x="DBDisj A B" in exI)
apply (rule_tac [2] x="DBNeg A" in exI)
apply (rule_tac [3] x="DBEx A" in exI)
apply (auto simp: C q_defs)
done
qed
qed

lemma SubstForm_imp_subst_dbfm:
assumes "SubstForm v u x x'"
obtains t A where "u = ⟦quot_dbtm t⟧e"
"x = ⟦quot_dbfm A⟧e"
"x' = ⟦quot_dbfm (subst_dbfm t (decode_Var v) A)⟧e"
proof -
obtain t where "u = ⟦quot_dbtm t⟧e"
using assms [unfolded SubstForm_def]
by (metis Term_imp_wf_dbtm)
thus ?thesis
by (metis SubstForm_imp_subst_dbfm_lemma assms that)
qed

lemma SubstForm_subst_dbfm:
assumes u: "wf_dbtm u"
shows "SubstForm (q_Var i) ⟦quot_dbtm u⟧e ⟦quot_dbfm A⟧e
⟦quot_dbfm (subst_dbfm u i A)⟧e"
apply (induction A rule: dbfm.induct)
apply (force simp: u SubstForm_def SeqSubstForm_def SubstAtomic_def SubstMakeForm_def
SubstTerm_subst_dbtm q_defs simp del: q_Var_def
intro: BuildSeq2_exI BuildSeq2_combine)+
done

corollary SubstForm_subst_dbfm_eq:
"⟦v = q_Var i; Term ux; ux = ⟦quot_dbtm u⟧e; A' = subst_dbfm u i A⟧
⟹ SubstForm v ux ⟦quot_dbfm A⟧e ⟦quot_dbfm A'⟧e"
by (metis SubstForm_subst_dbfm Term_imp_is_tm quot_dbtm_inject_lemma quot_tm_def wf_dbtm_iff_is_tm)

section ‹The predicate ‹AtomicP››

definition Atomic :: "hf ⇒ bool"
where "Atomic y ≡∃t u. Term t ∧ Term u ∧ (y = q_Eq t u ∨ y = q_Mem t u)"

nominal_function AtomicP :: "tm ⇒ fm"
where "⟦atom t ♯ (u,y); atom u ♯ y⟧ ⟹
AtomicP y = Ex t (Ex u (TermP (Var t) AND TermP (Var u) AND
(y EQ Q_Eq (Var t) (Var u) OR
y EQ Q_Mem (Var t) (Var u))))"
by (auto simp: eqvt_def AtomicP_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)

nominal_termination (eqvt)
by lexicographic_order

lemma
shows AtomicP_fresh_iff [simp]: "a ♯ AtomicP y ⟷ a ♯ y"    (is ?thesis1)
and eval_fm_AtomicP [simp]: "eval_fm e (AtomicP y) ⟷ Atomic⟦y⟧e"    (is ?thesis2)
and AtomicP_sf [iff]: "Sigma_fm (AtomicP y)"  (is ?thsf)
proof -
obtain t::name and u::name  where "atom t ♯ (u,y)"  "atom u ♯ y"
by (metis obtain_fresh)
thus ?thesis1 ?thesis2 ?thsf
by (auto simp: Atomic_def q_defs)
qed

section ‹The predicate ‹MakeForm››

definition MakeForm :: "hf ⇒ hf ⇒ hf ⇒ bool"
where "MakeForm y u w ≡
y = q_Disj u w ∨ y = q_Neg u ∨
(∃v u'. AbstForm v 0 u u' ∧ y = q_Ex u')"

nominal_function MakeFormP :: "tm ⇒ tm ⇒ tm ⇒ fm"
where "⟦atom v ♯ (y,u,w,au); atom au ♯ (y,u,w)⟧ ⟹
MakeFormP y u w =
y EQ Q_Disj u w OR y EQ Q_Neg u OR
Ex v (Ex au (AbstFormP (Var v) Zero u (Var au) AND y EQ Q_Ex (Var au)))"
by (auto simp: eqvt_def MakeFormP_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)

nominal_termination (eqvt)
by lexicographic_order

lemma
shows MakeFormP_fresh_iff [simp]:
"a ♯ MakeFormP y u w ⟷ a ♯ y ∧ a ♯ u ∧ a ♯ w"  (is ?thesis1)
and eval_fm_MakeFormP [simp]:
"eval_fm e (MakeFormP y u w) ⟷ MakeForm ⟦y⟧e ⟦u⟧e ⟦w⟧e"  (is ?thesis2)
and MakeFormP_sf [iff]:
"Sigma_fm (MakeFormP y u w)"  (is ?thsf)
proof -
obtain v::name and au::name  where "atom v ♯ (y,u,w,au)"  "atom au ♯ (y,u,w)"
by (metis obtain_fresh)
thus ?thesis1 ?thesis2 ?thsf
by (auto simp: MakeForm_def q_defs)
qed

declare MakeFormP.simps [simp del]

section ‹The predicate ‹SeqFormP››

(*SeqForm(s,k,t) ≡ LstSeq(s,k,t) ∧ (∀n∈k)[Atomic (s n) ∨ (∃m,l∈n)[MakeForm (s m) (s l) (s n)]]*)
definition SeqForm :: "hf ⇒ hf ⇒ hf ⇒ bool"
where "SeqForm s k y ≡ BuildSeq Atomic MakeForm s k y"

nominal_function SeqFormP :: "tm ⇒ tm ⇒ tm ⇒ fm"
where "⟦atom l ♯ (s,k,t,sl,m,n,sm,sn); atom sl ♯ (s,k,t,m,n,sm,sn);
atom m ♯ (s,k,t,n,sm,sn); atom ```