# Theory ValuesFSetProps

```theory ValuesFSetProps
imports ValuesFSet
begin

inductive_cases
vfun_le_inv[elim!]: "VFun t1 ⊑ VFun t2" and
le_fun_nat_inv[elim!]: "VFun t2 ⊑ VNat x1" and
le_any_nat_inv[elim!]: "v ⊑ VNat n" and
le_nat_any_inv[elim!]: "VNat n ⊑ v" and
le_fun_any_inv[elim!]: "VFun t ⊑ v" and
le_any_fun_inv[elim!]: "v ⊑ VFun t"

proposition val_le_refl[simp]: fixes v::val shows "v ⊑ v" by (induction v) auto

proposition val_le_trans[trans]: fixes v2::val shows "⟦ v1 ⊑ v2; v2 ⊑ v3 ⟧ ⟹ v1 ⊑ v3"
by (induction v2 arbitrary: v1 v3) blast+

lemma fsubset[intro!]: "fset A ⊆ fset B ⟹ A |⊆| B"
proof (rule fsubsetI)
fix x assume ab: "fset A ⊆ fset B" and xa: "x |∈| A"
from xa have "x ∈ fset A" by simp
from this ab have "x ∈ fset B" by blast
from this show "x |∈| B" by simp
qed

proposition val_le_antisymm: fixes v1::val shows "⟦ v1 ⊑ v2; v2 ⊑ v1 ⟧ ⟹ v1 = v2"
by (induction v1 arbitrary: v2) auto

lemma le_nat_any[simp]: "VNat n ⊑ v ⟹ v = VNat n"
by (cases v) auto

lemma le_any_nat[simp]: "v ⊑ VNat n ⟹ v = VNat n"
by (cases v) auto

lemma le_nat_nat[simp]: "VNat n ⊑ VNat n' ⟹ n = n'"
by auto

end

```