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