Theory MutableRefProps

theory MutableRefProps
  imports MutableRef
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" and
  le_pair_any_inv[elim!]: "VPair v1 v2 ⊑ v" and
  le_any_pair_inv[elim!]: "v ⊑ VPair v1 v2" and
  le_addr_any_inv[elim!]: "VAddr a ⊑ v" and
  le_any_addr_inv[elim!]: "v ⊑ VAddr a" and
  le_wrong_any_inv[elim!]: "Wrong ⊑ v" and
  le_any_wrong_inv[elim!]: "v ⊑ Wrong"

proposition val_le_refl: "v ⊑ v" by (induction v) auto

proposition val_le_trans: "⟦ v1 ⊑ v2; v2 ⊑ v3 ⟧ ⟹ v1 ⊑ v3"
  by (induction v2 arbitrary: v1 v3) blast+

proposition val_le_antisymm: "⟦ v1 ⊑ v2; v2 ⊑ v1 ⟧ ⟹ v1 = v2"
  by (induction v1 arbitrary: v2) blast+
    
end