# 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)"

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

```