Theory MSOinHOL_deep_subst_lemma

theory MSOinHOL_deep_subst_lemma
  imports MSOinHOL_deep
begin

subsection ‹First-order machinery (Part A)›

text ‹Free and bound first-order variable occurrences.›

primrec is_free (infix "free'_in" 900)
  where
    "x free_in (r⇧d(u,v)) = (x = u ∨ x = v)"
  | "x free_in (X⇧d(z)) = (x = z)"
  | "x free_in (¬⇧dφ) = (x free_in φ)"
  | "x free_in (φ ∧⇧d ψ) = (x free_in φ ∨ x free_in ψ)"
  | "x free_in (∃⇧dy. φ) = (x free_in φ ∧ x ≠ y)"
  | "x free_in (∃⇧d⇩2Y. φ) = (x free_in φ)"

abbreviation is_not_free (infix "not'_free'_in" 900)
  where "x not_free_in φ ≡ ¬ (x free_in φ)"

fun is_bound (infix "bound'_in" 900)
  where
    "x bound_in (r⇧d(u,v)) = False"
  | "x bound_in (X⇧d(z)) = False"
  | "x bound_in (¬⇧dφ) = (x bound_in φ)"
  | "x bound_in (φ ∧⇧d ψ) = (x bound_in φ ∨ x bound_in ψ)"
  | "x bound_in (∃⇧dy. φ) = (x = y ∨ x bound_in φ)"
  | "x bound_in (∃⇧d⇩2Y. φ) = (x bound_in φ)"

abbreviation is_not_bound (infix "not'_bound'_in" 900)
  where "x not_bound_in φ ≡ ¬ (x bound_in φ)"

abbreviation occurs (infix "occurs'_in" 900)
  where "x occurs_in φ ≡ x free_in φ ∨ x bound_in φ"

abbreviation not_in (infix "not'_in" 900)
  where "x not_in φ ≡ x not_free_in φ ∧ x not_bound_in φ"

text ‹A fresh first-order variable: strictly larger than every first-order
  variable occurring in ‹φ›.›

primrec fresh ("fresh'(_')")
  where
    "fresh (r⇧d(u,v)) = max (u+1) (v+1)"
  | "fresh (X⇧d(z)) = z+1"
  | "fresh (¬⇧dφ) = fresh φ"
  | "fresh (φ ∧⇧d ψ) = max (fresh φ) (fresh ψ)"
  | "fresh (∃⇧dx. φ) = max (x+1) (fresh φ)"
  | "fresh (∃⇧d⇩2Y. φ) = fresh φ"

lemma L5: "x bound_in φ ⟹ x < (fresh φ)"
  by (induct φ) auto

lemma L6: "x free_in φ ⟹ x < (fresh φ)"
  by (induct φ) auto

lemma L7: "(fresh φ) not_in φ"
  using L5 L6 by blast

lemma L8: "max (fresh φ) (fresh ψ) not_free_in φ"
  by (metis L6 L7 max.absorb3 max_def)

lemma L9: "max (fresh φ) (fresh ψ) not_bound_in φ"
  by (metis L5 L7 max.absorb3 max_def)

lemma L10: "max (fresh φ) (fresh ψ) not_free_in ψ"
  by (metis L8 max.commute)

lemma L11: "max (fresh φ) (fresh ψ) not_bound_in ψ"
  by (metis L9 max.commute)

text ‹Irrelevance lemma: updating a non-free first-order variable does not
  affect truth.›

lemma L12:
  "y not_free_in φ ⟹ (⟨I,D,E⟩,g[y←d],G ⊨⇧d φ) = (⟨I,D,E⟩,g,G ⊨⇧d φ)"
  by (induct φ arbitrary: g G; simp; metis L4 L2)

text ‹First-order variable-for-variable substitution.  The second-order
  binder descends transparently.›

primrec Subst ("[_←_]'(_')")
  where
    "[x←z](r⇧d(u,v)) = r⇧d((if x = u then z else u), (if x = v then z else v))"
  | "[x←z](X⇧d(w)) = X⇧d(if x = w then z else w)"
  | "[x←z](¬⇧dφ) = ¬⇧d([x←z](φ))"
  | "[x←z](φ ∧⇧d ψ) = ([x←z](φ) ∧⇧d [x←z](ψ))"
  | "[x←z](∃⇧dy. φ) = (if x = y then (∃⇧dy. φ) else (∃⇧dy. [x←z](φ)))"
  | "[x←z](∃⇧d⇩2Y. φ) = (∃⇧d⇩2Y. [x←z](φ))"

lemma L13 [simp]: "size [x←z](φ) = size φ"
  by (induct φ; auto)

lemma L14 [simp]: "[x←x](φ) = φ"
  by (induct φ; auto)

lemma L15:
  assumes "x ≠ a"
  shows "[a←z]([a←x](φ)) = [a←x](φ)"
  using assms by (induct φ) auto

lemma L16 [simp]:
  assumes "a ≠ x"
  shows "a not_free_in ([a←x](φ))"
  using assms by (induct φ) auto

text ‹Size-based induction principle (size-based on both existential
  binders).›

lemma SInduct:
  assumes "⋀r u v. P (r⇧d(u,v))"
    and "⋀X z. P (X⇧d(z))"
    and "⋀φ. (⋀ψ. size ψ ≤ size φ ⟹ P ψ) ⟹ P (¬⇧dφ)"
    and "⋀φ ψ. (⋀χ. size χ ≤ size φ + size ψ ⟹ P χ) ⟹ P (φ ∧⇧d ψ)"
    and "⋀y φ. (⋀ψ. size ψ ≤ size φ ⟹ P ψ) ⟹ P (∃⇧dy. φ)"
    and "⋀Y φ. (⋀ψ. size ψ ≤ size φ ⟹ P ψ) ⟹ P (∃⇧d⇩2Y. φ)"
  shows "P φ"
  using assms
proof (induct "size φ" arbitrary: φ rule: less_induct)
  case less thus ?case by (induct φ) auto
qed

text ‹Stronger induction: structural for the propositional cases,
  size-based for the two binders.›

lemma QInduct:
  assumes "⋀r u v. P (r⇧d(u,v))"
    and "⋀X z. P (X⇧d(z))"
    and "⋀φ. P φ ⟹ P (¬⇧dφ)"
    and "⋀φ ψ. P φ ⟹ P ψ ⟹ P (φ ∧⇧d ψ)"
    and "⋀y φ. (⋀ψ. size ψ ≤ size φ ⟹ P ψ) ⟹ P (∃⇧dy. φ)"
    and "⋀Y φ. (⋀ψ. size ψ ≤ size φ ⟹ P ψ) ⟹ P (∃⇧d⇩2Y. φ)"
  shows "P φ"
  using assms by (induct φ rule: SInduct) auto

text ‹Substitutability predicate: ‹z› may safely replace ‹x› in ‹φ›
  without capture.›

primrec SubstitutableForIn ("_ is'_subst'_for _ in _" [999,1,999] 999)
  where
    "z is_subst_for x in (r⇧d(u,v)) = True"
  | "z is_subst_for x in (X⇧d(w)) = True"
  | "z is_subst_for x in (¬⇧dφ) = (z is_subst_for x in φ)"
  | "z is_subst_for x in (φ ∧⇧d ψ) = (z is_subst_for x in φ ∧ z is_subst_for x in ψ)"
  | "z is_subst_for x in (∃⇧dy. φ) = (y = x ∨ (x not_free_in φ ∨ y ≠ z) ∧ z is_subst_for x in φ)"
  | "z is_subst_for x in (∃⇧d⇩2Y. φ) = (z is_subst_for x in φ)"

text ‹Substitution lemma: a syntactic ‹z›-for-‹x› substitution
  corresponds to updating the assignment.›

lemma SubstitutionLemma [simp]:
  assumes "z is_subst_for x in φ"
  shows "(⟨I,D,E⟩,g,G ⊨⇧d ([x←z](φ))) = (⟨I,D,E⟩,g[x←(g z)],G ⊨⇧d φ)"
  using assms by (induction φ arbitrary: g G; auto simp: L12 L2)

text ‹Alphabetic renaming preparing capture-avoiding substitution.›

fun ren_for_subst
  where
    "ren_for_subst x z (r⇧d(u,v)) = r⇧d(u,v)"
  | "ren_for_subst x z (X⇧d(w)) = X⇧d(w)"
  | "ren_for_subst x z (¬⇧dφ) = ¬⇧d(ren_for_subst x z φ)"
  | "ren_for_subst x z (φ ∧⇧d ψ) = (ren_for_subst x z φ ∧⇧d ren_for_subst x z ψ)"
  | "ren_for_subst x z (∃⇧dy. φ) =
       (if y = z ∧ x free_in φ
        then let f = max (fresh φ) (z+1); φ' = [y←f](φ)
             in (∃⇧df. ren_for_subst x z φ')
        else ∃⇧dy. ren_for_subst x z φ)"
  | "ren_for_subst x z (∃⇧d⇩2Y. φ) = ∃⇧d⇩2Y. ren_for_subst x z φ"

lemma L17 [simp]: "size (ren_for_subst x z φ) = size φ"
  by (induct φ arbitrary: z x rule: QInduct; simp add: Let_def)

lemma L18: "α not_in φ ⟹ α is_subst_for β in φ"
  by (induct φ) auto

lemma L19: "x free_in ψ ⟹ y ≠ x ⟹ x free_in [y←z](ψ)"
  by (induct ψ) auto

lemma L20 [simp]:
  "x free_in ren_for_subst x z φ = (x free_in φ)"
  by (induct φ rule: QInduct; simp add: Let_def)
     (metis L16 L6 L7 L19 max.absorb3 max_def_raw)

lemma L21:
  "(⟨I,D,E⟩,g,G ⊨⇧d φ) = (⟨I,D,E⟩,g,G ⊨⇧d (ren_for_subst x z φ))"
  by (induct φ arbitrary: z g G rule: QInduct;
      simp add: Let_def;
      smt (verit) L12 L18 L2 L3 L5 L6 SubstitutionLemma
        max.strict_order_iff max_def)

lemma L22: "z is_subst_for x in (ren_for_subst x z φ)"
  by (induct φ rule: QInduct; simp;
      metis L13 SubstitutableForIn.simps(5)
        Suc_n_not_le_n dual_order.refl max.cobounded2)

lemma L23: "x is_subst_for x in φ"
  by (induct φ) auto

lemma L24: "x not_free_in φ ⟹ [x←z](φ) = φ"
  by (induct φ) auto

lemma L26 [simp]: "z bound_in [x←y](φ) = z bound_in φ"
  by (induct φ) auto

text ‹Safe (capture-avoiding) first-order substitution: rename first, then
  substitute.›

definition ren_subst ("[_ ←⇩r _]'(_')")
  where "[x ←⇩r z](φ) = [x←z](ren_for_subst x z φ)"

lemma L27 [simp]:
  "(⟨I,D,E⟩,g,G ⊨⇧d [x ←⇩r z](φ)) = (⟨I,D,E⟩,g[x←g z],G ⊨⇧d φ)"
  using L21 L22 ren_subst_def by auto

lemma L28 [simp]: "size ([x ←⇩r z](φ)) = size φ"
  by (induct φ rule: QInduct) (auto simp: ren_subst_def Let_def)

lemma L29:
  "g onto D ⟹ (⟨I,D,E⟩,g,G ⊨⇧d (∃⇧dx. φ)) = (∃z. ⟨I,D,E⟩,g,G ⊨⇧d ([x ←⇩r z](φ)))"
  by (induct φ arbitrary: I g G x rule: QInduct; simp; blast)

subsection ‹Second-order machinery (Part B)›

primrec is_free2 (infix "free2'_in" 900)
  where
    "X free2_in (r⇧d(u,v)) = False"
  | "X free2_in (Y⇧d(z)) = (X = Y)"
  | "X free2_in (¬⇧dφ) = (X free2_in φ)"
  | "X free2_in (φ ∧⇧d ψ) = (X free2_in φ ∨ X free2_in ψ)"
  | "X free2_in (∃⇧dy. φ) = (X free2_in φ)"
  | "X free2_in (∃⇧d⇩2Y. φ) = (X free2_in φ ∧ X ≠ Y)"

abbreviation is_not_free2 (infix "not'_free2'_in" 900)
  where "X not_free2_in φ ≡ ¬ (X free2_in φ)"

fun is_bound2 (infix "bound2'_in" 900)
  where
    "X bound2_in (r⇧d(u,v)) = False"
  | "X bound2_in (Y⇧d(z)) = False"
  | "X bound2_in (¬⇧dφ) = (X bound2_in φ)"
  | "X bound2_in (φ ∧⇧d ψ) = (X bound2_in φ ∨ X bound2_in ψ)"
  | "X bound2_in (∃⇧dy. φ) = (X bound2_in φ)"
  | "X bound2_in (∃⇧d⇩2Y. φ) = (X = Y ∨ X bound2_in φ)"

abbreviation is_not_bound2 (infix "not'_bound2'_in" 900)
  where "X not_bound2_in φ ≡ ¬ (X bound2_in φ)"

abbreviation not_in2 (infix "not2'_in" 900)
  where "X not2_in φ ≡ X not_free2_in φ ∧ X not_bound2_in φ"

primrec fresh2
  where
    "fresh2 (r⇧d(u,v)) = 0"
  | "fresh2 (Y⇧d(z)) = Y+1"
  | "fresh2 (¬⇧dφ) = fresh2 φ"
  | "fresh2 (φ ∧⇧d ψ) = max (fresh2 φ) (fresh2 ψ)"
  | "fresh2 (∃⇧dy. φ) = fresh2 φ"
  | "fresh2 (∃⇧d⇩2Y. φ) = max (Y+1) (fresh2 φ)"

lemma N5: "X bound2_in φ ⟹ X < (fresh2 φ)"
  by (induct φ) auto

lemma N6: "X free2_in φ ⟹ X < (fresh2 φ)"
  by (induct φ) auto

lemma N7: "(fresh2 φ) not2_in φ"
  using N5 N6 by blast

lemma N8: "max (fresh2 φ) (fresh2 ψ) not_free2_in φ"
  by (metis N6 N7 max.absorb3 max_def)

lemma N9: "max (fresh2 φ) (fresh2 ψ) not_bound2_in φ"
  by (metis N5 N7 max.absorb3 max_def)

lemma N10: "max (fresh2 φ) (fresh2 ψ) not_free2_in ψ"
  by (metis N8 max.commute)

lemma N11: "max (fresh2 φ) (fresh2 ψ) not_bound2_in ψ"
  by (metis N9 max.commute)

text ‹Irrelevance lemma for second-order assignments.›

lemma N12:
  "Y not_free2_in φ ⟹ (⟨I,D,E⟩,g,G⟨Y←S⟩ ⊨⇧d φ) = (⟨I,D,E⟩,g,G ⊨⇧d φ)"
  by (induct φ arbitrary: g G; simp; metis M4 M2)

text ‹Second-order variable-for-variable substitution.  The first-order
  binder descends transparently.›

primrec Subst2 ("[_←⇩2_]'(_')")
  where
    "[X←⇩2Z](r⇧d(u,v)) = r⇧d(u,v)"
  | "[X←⇩2Z](Y⇧d(w)) = (if X = Y then Z else Y)⇧d(w)"
  | "[X←⇩2Z](¬⇧dφ) = ¬⇧d([X←⇩2Z](φ))"
  | "[X←⇩2Z](φ ∧⇧d ψ) = ([X←⇩2Z](φ) ∧⇧d [X←⇩2Z](ψ))"
  | "[X←⇩2Z](∃⇧dy. φ) = (∃⇧dy. [X←⇩2Z](φ))"
  | "[X←⇩2Z](∃⇧d⇩2Y. φ) = (if X = Y then (∃⇧d⇩2Y. φ) else (∃⇧d⇩2Y. [X←⇩2Z](φ)))"

lemma N13 [simp]: "size [X←⇩2Z](φ) = size φ"
  by (induct φ; auto)

lemma N14 [simp]: "[X←⇩2X](φ) = φ"
  by (induct φ; auto)

lemma N16 [simp]:
  assumes "A ≠ X"
  shows "A not_free2_in ([A←⇩2X](φ))"
  using assms by (induct φ) auto

primrec SubstitutableForIn2 ("_ is'_subst2'_for _ in _" [999,1,999] 999)
  where
    "Z is_subst2_for X in (r⇧d(u,v)) = True"
  | "Z is_subst2_for X in (Y⇧d(w)) = True"
  | "Z is_subst2_for X in (¬⇧dφ) = (Z is_subst2_for X in φ)"
  | "Z is_subst2_for X in (φ ∧⇧d ψ) = (Z is_subst2_for X in φ ∧ Z is_subst2_for X in ψ)"
  | "Z is_subst2_for X in (∃⇧dy. φ) = (Z is_subst2_for X in φ)"
  | "Z is_subst2_for X in (∃⇧d⇩2Y. φ) = (Y = X ∨ (X not_free2_in φ ∨ Y ≠ Z) ∧ Z is_subst2_for X in φ)"

lemma SubstitutionLemma2 [simp]:
  assumes "Z is_subst2_for X in φ"
  shows "(⟨I,D,E⟩,g,G ⊨⇧d ([X←⇩2Z](φ))) = (⟨I,D,E⟩,g,G⟨X←(G Z)⟩ ⊨⇧d φ)"
  using assms by (induction φ arbitrary: g G; auto simp: N12 M2)

fun ren_for_subst2
  where
    "ren_for_subst2 X Z (r⇧d(u,v)) = r⇧d(u,v)"
  | "ren_for_subst2 X Z (Y⇧d(w)) = Y⇧d(w)"
  | "ren_for_subst2 X Z (¬⇧dφ) = ¬⇧d(ren_for_subst2 X Z φ)"
  | "ren_for_subst2 X Z (φ ∧⇧d ψ) = (ren_for_subst2 X Z φ ∧⇧d ren_for_subst2 X Z ψ)"
  | "ren_for_subst2 X Z (∃⇧dy. φ) = ∃⇧dy. ren_for_subst2 X Z φ"
  | "ren_for_subst2 X Z (∃⇧d⇩2Y. φ) =
       (if Y = Z ∧ X free2_in φ
        then let f = max (fresh2 φ) (Z+1); φ' = [Y←⇩2f](φ)
             in (∃⇧d⇩2f. ren_for_subst2 X Z φ')
        else ∃⇧d⇩2Y. ren_for_subst2 X Z φ)"

lemma N17 [simp]: "size (ren_for_subst2 X Z φ) = size φ"
  by (induct φ arbitrary: Z X rule: QInduct; simp add: Let_def)

lemma N18: "α not2_in φ ⟹ α is_subst2_for β in φ"
  by (induct φ) auto

lemma N19: "X free2_in ψ ⟹ Y ≠ X ⟹ X free2_in [Y←⇩2Z](ψ)"
  by (induct ψ) auto

lemma N20 [simp]:
  "X free2_in ren_for_subst2 X Z φ = (X free2_in φ)"
  by (induct φ rule: QInduct; simp add: Let_def)
     (metis N16 N6 N7 N19 max.absorb3 max_def_raw)

lemma N21:
  "(⟨I,D,E⟩,g,G ⊨⇧d φ) = (⟨I,D,E⟩,g,G ⊨⇧d (ren_for_subst2 X Z φ))"
  by (induct φ arbitrary: Z g G rule: QInduct;
      simp add: Let_def;
      smt (verit) N12 N18 M2 M3 N5 N6 SubstitutionLemma2
        max.strict_order_iff max_def)

lemma N22: "Z is_subst2_for X in (ren_for_subst2 X Z φ)"
  by (induct φ rule: QInduct; simp;
      metis N13 SubstitutableForIn2.simps(6)
        Suc_n_not_le_n dual_order.refl max.cobounded2)

definition ren_subst2 ("[_ ←⇩r⇩2 _]'(_')")
  where "[X ←⇩r⇩2 Z](φ) = [X←⇩2Z](ren_for_subst2 X Z φ)"

lemma N27 [simp]:
  "(⟨I,D,E⟩,g,G ⊨⇧d [X ←⇩r⇩2 Z](φ)) = (⟨I,D,E⟩,g,G⟨X←G Z⟩ ⊨⇧d φ)"
  using N21 N22 ren_subst2_def by auto

lemma N28 [simp]: "size ([X ←⇩r⇩2 Z](φ)) = size φ"
  by (induct φ rule: QInduct) (auto simp: ren_subst2_def Let_def)

lemma N29:
  "G onto E ⟹ (⟨I,D,E⟩,g,G ⊨⇧d (∃⇧d⇩2X. φ)) = (∃Z. ⟨I,D,E⟩,g,G ⊨⇧d ([X ←⇩r⇩2 Z](φ)))"
  by (induct φ arbitrary: I g G X rule: QInduct; simp; blast)

end