Theory Incompleteness.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"
  by (simp_all add: perm_commute fresh_plus_perm minus_add)

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

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

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)"
  by (simp add: F_def make_F_def)

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
    by (simp add: ssubst_def)
  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))"
  by (simp add: ssubst_insert insert_absorb)

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

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

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»"
  by (simp add: ground_ssubst_eq supp_conv_fresh)

lemma ssubst_quot_fm [simp]:
  fixes A::fm shows "finite V ⟹ ssubst «A» V F = «A»"
  by (simp add: ground_ssubst_eq supp_conv_fresh)

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