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