Theory ValuesFSet

theory ValuesFSet
  imports Main Lambda "HOL-Library.FSet" 
begin

datatype val = VNat nat | VFun "(val × val) fset"

type_synonym func = "(val × val) fset"

inductive val_le :: "val ⇒ val ⇒ bool" (infix ‹⊑› 52) where
  vnat_le[intro!]: "(VNat n) ⊑ (VNat n)" |
  vfun_le[intro!]: "fset t1 ⊆ fset t2 ⟹ (VFun t1) ⊑ (VFun t2)"

type_synonym env = "((name × val) list)"

definition env_le :: "env ⇒ env ⇒ bool" (infix ‹⊑› 52) where 
  "ρ ⊑ ρ' ≡ ∀ x v. lookup ρ x = Some v ⟶ (∃ v'. lookup ρ' x = Some v' ∧ v ⊑ v')" 

definition env_eq :: "env ⇒ env ⇒ bool" (infix ‹≈› 50) where
  "ρ ≈ ρ' ≡ (∀ x. lookup ρ x = lookup ρ' x)"

fun vadd :: "(val × nat) × (val × nat) ⇒ nat ⇒ nat" where
  "vadd ((_,v),(_,u)) r = v + u + r"
  
primrec vsize :: "val ⇒ nat" where
"vsize (VNat n) = 1" |
"vsize (VFun t) = 1 + ffold vadd 0
                            (fimage (map_prod (λ v. (v,vsize v)) (λ v. (v,vsize v))) t)"

abbreviation vprod_size :: "val × val ⇒ (val × nat) × (val × nat)" where
  "vprod_size ≡ map_prod (λ v. (v,vsize v)) (λ v. (v,vsize v))"

abbreviation fsize :: "func ⇒ nat" where
  "fsize t ≡ 1 + ffold vadd 0 (fimage vprod_size t)"

interpretation vadd_vprod: comp_fun_commute "vadd ∘ vprod_size"
  unfolding comp_fun_commute_def by auto  

lemma vprod_size_inj: "inj_on vprod_size (fset A)"
  unfolding inj_on_def by auto
  
lemma fsize_def2: "fsize t = 1 + ffold (vadd ∘ vprod_size) 0 t"
  using vprod_size_inj[of t] ffold_fimage[of vprod_size t vadd 0] by simp

lemma fsize_finsert_in[simp]:
  assumes v12_t: "(v1,v2) |∈| t" shows "fsize (finsert (v1,v2) t) = fsize t"
proof -
  from v12_t have "finsert (v1,v2) t = t" by auto
  from this show ?thesis by simp
qed
 
lemma fsize_finsert_notin[simp]: 
  assumes v12_t: "(v1,v2) |∉| t"
  shows "fsize (finsert (v1,v2) t) = vsize v1 + vsize v2 + fsize t"
proof -
  let ?f = "vadd ∘ vprod_size"
  have "fsize (finsert (v1,v2) t) = 1 + ffold ?f 0 (finsert (v1,v2) t)"
    using fsize_def2[of "finsert (v1,v2) t"] by simp
  also from v12_t have "... = 1 + ?f (v1,v2) (ffold ?f 0 t)" by simp
  finally have "fsize (finsert (v1,v2) t) = 1 + ?f (v1,v2) (ffold ?f 0 t)" .
  from this show ?thesis using fsize_def2[of t] by simp
qed
    
end