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