Theory Substitutions

(*******************************************************************************

  Project: Sumcheck Protocol

  Authors: Azucena Garvia Bosshard <zucegb@gmail.com>
           Christoph Sprenger, ETH Zurich <sprenger@inf.ethz.ch>
           Jonathan Bootle, IBM Research Europe <jbt@zurich.ibm.com>

*******************************************************************************)

section ‹Substitutions›

theory Substitutions
  imports
    Main
    "HOL-Library.FuncSet"
begin

type_synonym ('v, 'a) subst = "'v ⇀ 'a"

definition substs :: "'v set ⇒ 'a set ⇒ ('v, 'a) subst set" where
  "substs V H = {σ. dom σ = V ∧ ran σ ⊆ H}"

text ‹Small lemmas about the set of substitutions›

lemma substE [elim]: "⟦ σ ∈ substs V H; ⟦ dom σ = V; ran σ ⊆ H ⟧ ⟹ P ⟧ ⟹ P"
  by (simp add: substs_def)

lemma substs_empty_dom [simp]: "substs {} H = {Map.empty}"
  by (auto simp add: substs_def)

lemma substs_finite: "⟦ finite V; finite H ⟧ ⟹ finite (substs V H)"
  by (simp add: finite_set_of_finite_maps substs_def)

lemma substs_nonempty:
  assumes "H ≠ {}"
  shows "substs V H ≠ {}" 
proof -
  obtain h where A1: "h ∈ H" using assms by(auto)
  obtain ρ where A2: "ρ = (λv. if v ∈ V then Some h else None)" by(simp)
  have "ρ ∈ substs V H" using A1 A2 by(auto simp add: substs_def ran_def dom_def)
  then show ?thesis by(auto)
qed

lemma subst_dom: ‹⟦ ρ ∈ substs V H; x ∉ V ⟧ ⟹ x ∉ dom ρ›
  by(auto simp add: substs_def)

lemma subst_add:
  assumes  "x ∈ V" and "ρ ∈ substs (V - {x}) H" and "a ∈ H"
  shows "ρ(x ↦ a) ∈ substs V H"
  using assms
  by(simp add: substs_def)
    (auto simp add: dom_def ran_def)

lemma subst_im:
  assumes "x ∈ V" and "ρ ∈ substs V H"
  shows "the (ρ x) ∈ H"
  using assms
  by(auto simp add: substs_def dom_def ran_def)

lemma subst_restr:
  assumes "x ∈ V" and "ρ ∈ substs V H"
  shows "ρ |` (dom ρ - {x}) ∈ substs (V - {x}) H"
  using assms
  by(auto simp add: substs_def ran_def dom_def restrict_map_def)


text ‹Bijection between sets of substitutions›

lemma restrict_map_dom: "σ |` dom σ = σ"
  by (metis (no_types, lifting) domIff map_le_antisym map_le_def restrict_in restrict_out)
   

lemma bij_betw_set_substs:
  assumes "x ∈ V" 
  defines "f ≡ λ(a, σ::'v ⇀ 'a). σ(x ↦ a)" 
      and "g ≡ λθ::'v ⇀ 'a. (the (θ x), θ|`(dom θ - {x}))"
    shows "bij_betw f
                    (H × substs (V - {x}) H) 
                    (substs V H)"
proof (intro bij_betwI) 
  show "f ∈ H × substs (V - {x}) H → substs V H"
    using assms
    by(auto simp add: f_def subst_add)
next 
  show "g ∈ substs V H → H × substs (V - {x}) H" 
    using assms
    by(auto simp add: g_def subst_im subst_restr)
next 
  fix xa
  assume "xa ∈ H × substs (V - {x}) H"
  then show "g (f xa) = xa" using assms
    by (smt (verit, ccfv_threshold) Diff_insert_absorb SigmaE case_prod_conv domI
        fun_upd_None_restrict fun_upd_same fun_upd_upd mk_disjoint_insert option.sel restrict_map_dom
        subst_dom)
next
  fix y
  assume "y ∈ substs V H"
  then show "f (g y) = y" using assms 
    by(auto simp add: g_def f_def)
      (metis domIff fun_upd_restrict map_upd_triv option.exhaust_sel restrict_map_dom substE)
qed

end