Theory Pseudo_Coding

```chapter‹Pseudo-Coding: Section 7 Material›

theory Pseudo_Coding
imports II_Prelims
begin

section‹General Lemmas›

lemma Collect_disj_Un: "{f i |i. P i ∨ Q i} = {f i |i. P i} ∪ {f i |i. Q i}"
by auto

abbreviation Q_Subset :: "tm ⇒ tm ⇒ tm"
where "Q_Subset t u ≡ (Q_All (Q_Imp (Q_Mem (Q_Ind Zero) t) (Q_Mem (Q_Ind Zero) u)))"

lemma NEQ_quot_tm: "i≠j ⟹ {} ⊢ «Var i» NEQ «Var j»"
by (auto intro: Sigma_fm_imp_thm [OF OrdNotEqP_sf]
simp: ground_fm_aux_def supp_conv_fresh quot_tm_def)

lemma EQ_quot_tm_Fls: "i≠j ⟹ insert («Var i» EQ «Var j») H ⊢ Fls"
by (metis (full_types) NEQ_quot_tm Assume OrdNotEqP_E cut2 thin0)

lemma perm_commute: "a ♯ p ⟹ a' ♯ p ⟹ (a ⇌ a') + p = p + (a ⇌ a')"
by (rule plus_perm_eq) (simp add: supp_swap fresh_def)

lemma perm_self_inverseI: "⟦-p = q; a ♯ p; a' ♯ p⟧ ⟹ - ((a ⇌ a') + p) = (a ⇌ a') + q"

lemma fresh_image:
fixes f :: "'a ⇒ 'b::fs"  shows "finite A ⟹ i ♯ f ` A ⟷ (∀x∈A. i ♯ f x)"
by (induct rule: finite_induct) (auto simp: fresh_finite_insert)

lemma atom_in_atom_image [simp]: "atom j ∈ atom ` V ⟷ j ∈ V"
by auto

lemma fresh_star_empty [simp]: "{} ♯* bs"

declare fresh_star_insert [simp]

lemma fresh_star_finite_insert:
fixes S :: "('a::fs) set"  shows "finite S ⟹ a ♯* insert x S ⟷ a ♯* x ∧ a ♯* S"
by (auto simp: fresh_star_def fresh_finite_insert)

lemma fresh_finite_Diff_single [simp]:
fixes V :: "name set"   shows "finite V ⟹ a ♯ (V - {j}) ⟷ (a ♯ j ⟶ a ♯ V)"
apply (auto simp: fresh_finite_insert)
apply (metis finite_Diff fresh_finite_insert insert_Diff_single)
apply (metis Diff_iff finite_Diff fresh_atom fresh_atom_at_base fresh_finite_set_at_base insertI1)
apply (metis Diff_idemp Diff_insert_absorb finite_Diff fresh_finite_insert insert_Diff_single insert_absorb)
done

lemma fresh_image_atom [simp]: "finite A ⟹ i ♯ atom ` A ⟷ i ♯ A"
by (induct rule: finite_induct) (auto simp: fresh_finite_insert)

lemma atom_fresh_star_atom_set_conv: "⟦atom i ♯ bs; finite bs⟧ ⟹ bs ♯* i"
by (metis fresh_finite_atom_set fresh_ineq_at_base fresh_star_def)

lemma notin_V:
assumes p: "atom i ♯ p" and V: "finite V" "atom ` (p ∙ V) ♯* V"
shows "i ∉ V" "i ∉ p ∙ V"
using V
apply (auto simp: fresh_def fresh_star_def supp_finite_set_at_base)
apply (metis p mem_permute_iff fresh_at_base_permI)+
done

section‹Simultaneous Substitution›

definition ssubst :: "tm ⇒ name set ⇒ (name ⇒ tm) ⇒ tm"
where "ssubst t V F = Finite_Set.fold (λi. subst i (F i)) t V"

definition make_F :: "name set ⇒ perm ⇒ name ⇒ tm"
where "make_F Vs p ≡ λi. if i ∈ Vs then Var (p ∙ i) else Var i"

lemma ssubst_empty [simp]: "ssubst t {} F = t"

text‹Renaming a finite set of variables. Based on the theorem ‹at_set_avoiding››
locale quote_perm =
fixes p :: perm and Vs :: "name set" and F :: "name ⇒ tm"
assumes p: "atom ` (p ∙ Vs) ♯* Vs"
and pinv: "-p = p"
and Vs:  "finite Vs"
defines "F ≡ make_F Vs p"
begin

lemma F_unfold: "F i = (if i ∈ Vs then Var (p ∙ i) else Var i)"

lemma finite_V [simp]: "V ⊆ Vs ⟹ finite V"
by (metis Vs finite_subset)

lemma perm_exits_Vs: "i ∈ Vs ⟹ (p ∙ i) ∉ Vs"
by (metis Vs fresh_finite_set_at_base imageI fresh_star_def mem_permute_iff p)

lemma atom_fresh_perm: "⟦x ∈ Vs; y ∈ Vs⟧ ⟹ atom x ♯ p ∙ y"
by (metis imageI Vs p fresh_finite_set_at_base fresh_star_def mem_permute_iff fresh_at_base(2))

lemma fresh_pj: "⟦a ♯ p; j ∈ Vs⟧ ⟹ a ♯ p ∙ j"
by (metis atom_fresh_perm fresh_at_base(2) fresh_perm fresh_permute_left pinv)

lemma fresh_Vs: "a ♯ p ⟹ a ♯ Vs"
by (metis Vs fresh_def fresh_perm fresh_permute_iff fresh_star_def p permute_finite supp_finite_set_at_base)

lemma fresh_pVs: "a ♯ p ⟹ a ♯ p ∙ Vs"
by (metis fresh_Vs fresh_perm fresh_permute_left pinv)

lemma assumes "V ⊆ Vs" "a ♯ p"
shows fresh_pV [simp]: "a ♯ p ∙ V" and fresh_V [simp]: "a ♯ V"
using fresh_pVs fresh_Vs assms
apply (auto simp: fresh_def)
apply (metis (full_types) Vs finite_V permute_finite subsetD subset_Un_eq supp_of_finite_union union_eqvt)
by (metis Vs finite_V subsetD subset_Un_eq supp_of_finite_union)

lemma qp_insert:
fixes i::name and i'::name
assumes "atom i ♯ p" "atom i' ♯ (i,p)"
shows  "quote_perm ((atom i ⇌ atom i') + p) (insert i Vs)"
using p pinv Vs assms
by (auto simp: quote_perm_def fresh_at_base_permI atom_fresh_star_atom_set_conv swap_fresh_fresh
fresh_star_finite_insert fresh_finite_insert perm_self_inverseI)

lemma subst_F_left_commute: "subst x (F x) (subst y (F y) t) = subst y (F y) (subst x (F x) t)"
by (metis subst_tm_commute2 F_unfold subst_tm_id F_unfold atom_fresh_perm tm.fresh(2))

lemma
assumes "finite V" "i ∉ V"
shows ssubst_insert:  "ssubst t (insert i V) F = subst i (F i) (ssubst t V F)"  (is ?thesis1)
and ssubst_insert2: "ssubst t (insert i V) F = ssubst (subst i (F i) t) V F"  (is ?thesis2)
proof -
interpret comp_fun_commute "(λi. subst i (F i))"
proof qed (simp add: subst_F_left_commute fun_eq_iff)
show ?thesis1 using assms Vs
show ?thesis2 using assms Vs
by (simp add: ssubst_def fold_insert2 del: fold_insert)
qed

lemma ssubst_insert_if:
"finite V ⟹
ssubst t (insert i V) F = (if i ∈ V then ssubst t V F
else subst i (F i) (ssubst t V F))"

lemma ssubst_single [simp]: "ssubst t {i} F = subst i (F i) t"

lemma ssubst_Var_if [simp]:
assumes "finite V"
shows "ssubst (Var i) V F = (if i ∈ V then F i else Var i)"
using assms
apply (induction V, auto)
apply (metis ssubst_insert subst.simps(2))
apply (metis ssubst_insert2 subst.simps(2))+
done

lemma ssubst_Zero [simp]: "finite V ⟹ ssubst Zero V F = Zero"
by (induct V rule: finite_induct) (auto simp: ssubst_insert)

lemma ssubst_Eats [simp]: "finite V ⟹ ssubst (Eats t u) V F = Eats (ssubst t V F) (ssubst u V F)"
by (induct V rule: finite_induct) (auto simp: ssubst_insert)

lemma ssubst_SUCC [simp]: "finite V ⟹ ssubst (SUCC t) V F = SUCC (ssubst t V F)"
by (metis SUCC_def ssubst_Eats)

lemma ssubst_ORD_OF [simp]: "finite V ⟹ ssubst (ORD_OF n) V F = ORD_OF n"
by (induction n) auto

lemma ssubst_HPair [simp]:
"finite V ⟹ ssubst (HPair t u) V F = HPair (ssubst t V F) (ssubst u V F)"

lemma ssubst_HTuple [simp]: "finite V ⟹ ssubst (HTuple n) V F = (HTuple n)"
by (induction n) (auto simp: HTuple.simps)

lemma ssubst_Subset:
assumes "finite V" shows "ssubst ⌊t SUBS u⌋V V F = Q_Subset (ssubst ⌊t⌋V V F) (ssubst ⌊u⌋V V F)"
proof -
obtain i::name where "atom i ♯ (t,u)"
by (rule obtain_fresh)
thus ?thesis using assms
by (auto simp: Subset.simps [of i] vquot_fm_def vquot_tm_def trans_tm_forget)
qed

lemma fresh_ssubst:
assumes "finite V" "a ♯ p ∙ V" "a ♯ t"
shows "a ♯ ssubst t V F"
using assms
by (induct V)
(auto simp: ssubst_insert_if fresh_finite_insert F_unfold intro: fresh_ineq_at_base)

lemma fresh_ssubst':
assumes "finite V" "atom i ♯ t" "atom (p ∙ i) ♯ t"
shows "atom i ♯ ssubst t V F"
using assms
by (induct t rule: tm.induct) (auto simp: F_unfold fresh_permute_left pinv)

lemma ssubst_vquot_Ex:
"⟦finite V; atom i ♯ p ∙ V⟧
⟹ ssubst ⌊Ex i A⌋(insert i V) (insert i V) F = ssubst ⌊Ex i A⌋V V F"
by (simp add: ssubst_insert_if insert_absorb vquot_fm_insert fresh_ssubst)

lemma ground_ssubst_eq: "⟦finite V; supp t = {}⟧ ⟹ ssubst t V F = t"
by (induct V rule: finite_induct) (auto simp: ssubst_insert fresh_def)

lemma ssubst_quot_tm [simp]:
fixes t::tm shows "finite V ⟹ ssubst «t» V F = «t»"

lemma ssubst_quot_fm [simp]:
fixes A::fm shows "finite V ⟹ ssubst «A» V F = «A»"

lemma atom_in_p_Vs: "⟦i ∈ p ∙ V; V ⊆ Vs⟧ ⟹ i ∈ p ∙ Vs"
by (metis (full_types) True_eqvt subsetD subset_eqvt)

section‹The Main Theorems of Section 7›

lemma SubstTermP_vquot_dbtm:
assumes w: "w ∈ Vs - V" and V: "V ⊆ Vs" "V' = p ∙ V"
and s: "supp dbtm ⊆ atom ` Vs"
shows
"insert (ConstP (F w)) {ConstP (F i) | i. i ∈ V}
⊢ SubstTermP «Var w» (F w)
(ssubst (vquot_dbtm V dbtm) V F)
(subst w (F w) (ssubst (vquot_dbtm (insert w V) dbtm) V F))"
using s
proof (induct dbtm rule: dbtm.induct)
case DBZero thus ?case using V w
by (auto intro: SubstTermP_Zero [THEN cut1] ConstP_imp_TermP [THEN cut1])
next
case (DBInd n) thus ?case using V
apply auto
apply (rule thin [of "{ConstP (F w)}"])
apply (rule SubstTermP_Ind [THEN cut3])
apply (auto simp: IndP_Q_Ind OrdP_ORD_OF ConstP_imp_TermP)
done
next
case (DBVar i) show ?case
proof (cases "i ∈ V'")
case True hence "i ∉ Vs" using assms
by (metis p Vs atom_in_atom_image atom_in_p_Vs fresh_finite_set_at_base fresh_star_def)
thus ?thesis using DBVar True V
by auto
next
case False thus ?thesis using DBVar V w
apply (auto simp: quot_Var [symmetric])
apply (blast intro: thin [of "{ConstP (F w)}"] ConstP_imp_TermP
SubstTermP_Var_same [THEN cut2])
apply (subst forget_subst_tm, metis F_unfold atom_fresh_perm tm.fresh(2))
apply (blast intro: Hyp thin [of "{ConstP (F w)}"] ConstP_imp_TermP
SubstTermP_Const [THEN cut2])
apply (blast intro: Hyp thin [of "{ConstP (F w)}"] ConstP_imp_TermP EQ_quot_tm_Fls
SubstTermP_Var_diff [THEN cut4])
done
qed
next
case (DBEats tm1 tm2) thus ?case using V
by (auto simp: SubstTermP_Eats [THEN cut2])
qed

lemma SubstFormP_vquot_dbfm:
assumes w: "w ∈ Vs - V" and V: "V ⊆ Vs" "V' = p ∙ V"
and s: "supp dbfm ⊆ atom ` Vs"
shows
"insert (ConstP (F w)) {ConstP (F i) | i. i ∈ V}
⊢ SubstFormP «Var w» (F w)
(ssubst (vquot_dbfm V dbfm) V F)
(subst w (F w) (ssubst (vquot_dbfm (insert w V) dbfm) V F))"
using w s
proof (induct dbfm rule: dbfm.induct)
case (DBMem t u) thus ?case using V
by (auto intro: SubstTermP_vquot_dbtm SubstFormP_Mem [THEN cut2])
next
case (DBEq t u) thus ?case using V
by (auto intro: SubstTermP_vquot_dbtm SubstFormP_Eq [THEN cut2])
next
case (DBDisj A B) thus ?case using V
by (auto intro: SubstFormP_Disj [THEN cut2])
next
case (DBNeg A) thus ?case using V
by (auto intro: SubstFormP_Neg [THEN cut1])
next
case (DBEx A) thus ?case using V
by (auto intro: SubstFormP_Ex [THEN cut1])
qed

text‹Lemmas 7.5 and 7.6›
lemma ssubst_SubstFormP:
fixes A::fm
assumes w: "w ∈ Vs - V" and V: "V ⊆ Vs" "V' = p ∙ V"
and s: "supp A ⊆ atom ` Vs"
shows
"insert (ConstP (F w)) {ConstP (F i) | i. i ∈ V}
⊢ SubstFormP «Var w» (F w)
(ssubst ⌊A⌋V V F)
(ssubst ⌊A⌋(insert w V) (insert w V) F)"
proof -
have "w ∉ V" using assms
by auto
thus ?thesis using assms
by (simp add: vquot_fm_def supp_conv_fresh ssubst_insert_if SubstFormP_vquot_dbfm)
qed

text‹Theorem 7.3›
theorem PfP_implies_PfP_ssubst:
fixes β::fm
assumes β: "{} ⊢ PfP «β»"
and V: "V ⊆ Vs"
and s: "supp β ⊆ atom ` Vs"
shows    "{ConstP (F i) | i. i ∈ V} ⊢ PfP (ssubst ⌊β⌋V V F)"
proof -
show ?thesis using finite_V [OF V] V
proof induction
case empty thus ?case
by (auto simp: β)
next
case (insert i V)
thus ?case using assms
by (auto simp: Collect_disj_Un fresh_finite_set_at_base
intro: PfP_implies_SubstForm_PfP thin1 ssubst_SubstFormP)
qed
qed

end

end

```