(*
 * Copyright 2016, NICTA
 *
 * This software may be distributed and modified according to the terms of
 * the GNU General Public License version 2. Note that NO WARRANTY is provided.
 * See "LICENSE_GPLv2.txt" for details.
 *
 * @TAG(NICTA_GPL)
 *)

(*
 * Primitive ops
 *   
 *)

theory Prim
imports
  "../Deep_Embedding_Auto"
  "../SpecialisedLemmaTactic"
  "../Cogent_Corres"
  "../Corres_Tac"
  "../TypeProofGen"
  "../Tidy"
  "../Heap_Relation_Generation" "../Type_Relation_Generation"
begin


(* Cogent semantics generated by
  cogent --fml-typing-tree --type-proof=Foo.thy pass_prim-ops.cogent
*)

lemmas abbreviated_type_defs =
  TrueI

definition
  "ops8_type \<equiv> ([], (TPrim (Num U8), TPrim (Num U8)))"

definition
  "ops8 \<equiv> Let (Var 0) (Let (Lit (LU8 1)) (Let (Prim (Plus U8) [Var 1, Var 0]) (Let (Prim (Times U8) [Var 0, Var 2]) (Let (Prim (Minus U8) [Var 0, Var 1]) (Let (Prim (BitOr U8) [Var 0, Var 1]) (Let (Prim (BitAnd U8) [Var 0, Var 1]) (Let (Prim (BitXor U8) [Var 1, Var 2]) (Let (Prim (Complement U8) [Var 0]) (Let (Prim (LShift U8) [Var 1, Var 0]) (Let (Prim (RShift U8) [Var 1, Var 0]) (Let (Prim (Divide U8) [Var 0, Var 1]) (Let (Prim (Mod U8) [Var 1, Var 0]) (Let (Prim (Lt U8) [Var 2, Var 1]) (Let (Prim (Le U8) [Var 2, Var 1]) (Let (Prim (Eq (Num U8)) [Var 4, Var 2]) (Let (Prim Cogent.And [Var 1, Var 0]) (Let (Prim Cogent.And [Var 3, Var 0]) (If (Var 0) (Lit (LU8 0)) (Lit (LU8 1))))))))))))))))))))"

definition
  "ops64_type \<equiv> ([], (TPrim (Num U64), TPrim (Num U64)))"

definition
  "ops64 \<equiv> Let (Var 0) (Let (Lit (LU8 1)) (Let (Cast U64 (Var 0)) (Let (Prim (Plus U64) [Var 2, Var 0]) (Let (Prim (Times U64) [Var 0, Var 3]) (Let (Prim (Minus U64) [Var 0, Var 1]) (Let (Prim (BitOr U64) [Var 0, Var 1]) (Let (Prim (BitAnd U64) [Var 0, Var 1]) (Let (Prim (BitXor U64) [Var 1, Var 0]) (Let (Prim (Complement U64) [Var 0]) (Let (Prim (LShift U64) [Var 1, Var 0]) (Let (Prim (RShift U64) [Var 1, Var 0]) (Let (Prim (Divide U64) [Var 0, Var 1]) (Let (Prim (Mod U64) [Var 1, Var 0]) (Let (Prim (Lt U64) [Var 2, Var 1]) (Let (Prim (Le U64) [Var 2, Var 1]) (Let (Prim (Eq (Num U64)) [Var 4, Var 2]) (Let (Prim Cogent.And [Var 1, Var 0]) (Let (Prim Cogent.And [Var 3, Var 0]) (If (Var 0) (Let (Lit (LU8 0)) (Cast U64 (Var 0))) (Let (Lit (LU8 1)) (Cast U64 (Var 0))))))))))))))))))))))"

definition
  "ops32_type \<equiv> ([], (TPrim (Num U32), TPrim (Num U32)))"

definition
  "ops32 \<equiv> Let (Var 0) (Let (Lit (LU8 1)) (Let (Cast U32 (Var 0)) (Let (Prim (Plus U32) [Var 2, Var 0]) (Let (Prim (Times U32) [Var 0, Var 3]) (Let (Prim (Minus U32) [Var 0, Var 1]) (Let (Prim (BitOr U32) [Var 0, Var 1]) (Let (Prim (BitAnd U32) [Var 0, Var 1]) (Let (Prim (BitXor U32) [Var 1, Var 2]) (Let (Prim (Complement U32) [Var 0]) (Let (Prim (LShift U32) [Var 1, Var 0]) (Let (Prim (RShift U32) [Var 1, Var 0]) (Let (Prim (Divide U32) [Var 0, Var 1]) (Let (Prim (Mod U32) [Var 1, Var 0]) (Let (Prim (Lt U32) [Var 2, Var 1]) (Let (Prim (Le U32) [Var 2, Var 1]) (Let (Prim (Eq (Num U32)) [Var 4, Var 2]) (Let (Prim Cogent.And [Var 1, Var 0]) (Let (Prim Cogent.And [Var 3, Var 0]) (If (Var 0) (Let (Lit (LU8 0)) (Cast U32 (Var 0))) (Let (Lit (LU8 1)) (Cast U32 (Var 0))))))))))))))))))))))"

definition
  "ops16_type \<equiv> ([], (TPrim (Num U16), TPrim (Num U16)))"

definition
  "ops16 \<equiv> Let (Var 0) (Let (Lit (LU8 1)) (Let (Cast U16 (Var 0)) (Let (Prim (Plus U16) [Var 2, Var 0]) (Let (Prim (Times U16) [Var 0, Var 3]) (Let (Prim (Minus U16) [Var 0, Var 1]) (Let (Prim (BitOr U16) [Var 0, Var 1]) (Let (Prim (BitAnd U16) [Var 0, Var 1]) (Let (Prim (BitXor U16) [Var 1, Var 2]) (Let (Prim (Complement U16) [Var 0]) (Let (Prim (LShift U16) [Var 1, Var 0]) (Let (Prim (RShift U16) [Var 1, Var 0]) (Let (Prim (Divide U16) [Var 0, Var 1]) (Let (Prim (Mod U16) [Var 1, Var 0]) (Let (Prim (Lt U16) [Var 2, Var 1]) (Let (Prim (Le U16) [Var 2, Var 1]) (Let (Prim (Eq (Num U16)) [Var 4, Var 2]) (Let (Prim Cogent.And [Var 1, Var 0]) (Let (Prim Cogent.And [Var 3, Var 0]) (If (Var 0) (Let (Lit (LU8 0)) (Cast U16 (Var 0))) (Let (Lit (LU8 1)) (Cast U16 (Var 0))))))))))))))))))))))"

definition
  "bool_ops_type \<equiv> ([], (TPrim (Num U32), TPrim Bool))"

definition
  "bool_ops \<equiv> Let (Var 0) (Let (Lit (LU8 1)) (Let (Cast U32 (Var 0)) (Let (Prim (Plus U32) [Var 2, Var 0]) (Let (Prim (Times U32) [Var 0, Var 3]) (Let (Prim (Lt U32) [Var 4, Var 1]) (Let (Prim (Le U32) [Var 2, Var 1]) (Let (Prim (Eq (Num U32)) [Var 2, Var 6]) (Let (Prim Cogent.And [Var 1, Var 0]) (Let (Prim Cogent.Or [Var 0, Var 1]) (Let (Prim Not [Var 0]) (Let (Lit (LBool True)) (Let (Prim Cogent.Or [Var 1, Var 0]) (Let (Prim Not [Var 0]) (Let (Lit (LBool False)) (Let (Prim Cogent.And [Var 1, Var 0]) (Var 0))))))))))))))))"

ML {*
val Cogent_functions = ["ops8","ops64","ops32","ops16","bool_ops"]
val Cogent_abstract_functions = []
*}

definition
  "\<Xi> func_name' \<equiv> case func_name' of ''ops8'' \<Rightarrow> ops8_type | ''ops64'' \<Rightarrow> ops64_type | ''ops32'' \<Rightarrow> ops32_type | ''ops16'' \<Rightarrow> ops16_type | ''bool_ops'' \<Rightarrow> bool_ops_type"

definition
  "ops8_typetree \<equiv> TyTrSplit (Cons (Some TSK_L) []) [] TyTrLeaf [Some (TPrim (Num U8))] (TyTrSplit (append (replicate 2 None) []) [] TyTrLeaf [Some (TPrim (Num U8))] (TyTrSplit (Cons (Some TSK_L) (Cons (Some TSK_S) (Cons None []))) [] TyTrLeaf [Some (TPrim (Num U8))] (TyTrSplit (Cons (Some TSK_S) (Cons None (Cons (Some TSK_L) (Cons None [])))) [] TyTrLeaf [Some (TPrim (Num U8))] (TyTrSplit (Cons (Some TSK_S) (Cons (Some TSK_L) (append (replicate 3 None) []))) [] TyTrLeaf [Some (TPrim (Num U8))] (TyTrSplit (Cons (Some TSK_S) (Cons (Some TSK_L) (append (replicate 4 None) []))) [] TyTrLeaf [Some (TPrim (Num U8))] (TyTrSplit (Cons (Some TSK_S) (Cons (Some TSK_S) (append (replicate 5 None) []))) [] TyTrLeaf [Some (TPrim (Num U8))] (TyTrSplit (Cons (Some TSK_L) (Cons (Some TSK_L) (Cons (Some TSK_L) (append (replicate 5 None) [])))) [] TyTrLeaf [Some (TPrim (Num U8))] (TyTrSplit (Cons (Some TSK_S) (append (replicate 8 None) [])) [] TyTrLeaf [Some (TPrim (Num U8))] (TyTrSplit (Cons (Some TSK_S) (Cons (Some TSK_L) (append (replicate 8 None) []))) [] TyTrLeaf [Some (TPrim (Num U8))] (TyTrSplit (Cons (Some TSK_S) (Cons (Some TSK_L) (append (replicate 9 None) []))) [] TyTrLeaf [Some (TPrim (Num U8))] (TyTrSplit (Cons (Some TSK_S) (Cons (Some TSK_L) (append (replicate 10 None) []))) [] TyTrLeaf [Some (TPrim (Num U8))] (TyTrSplit (Cons (Some TSK_S) (Cons (Some TSK_S) (append (replicate 11 None) []))) [] TyTrLeaf [Some (TPrim (Num U8))] (TyTrSplit (Cons None (Cons (Some TSK_S) (Cons (Some TSK_S) (append (replicate 11 None) [])))) [] TyTrLeaf [Some (TPrim Bool)] (TyTrSplit (Cons None (Cons (Some TSK_S) (Cons (Some TSK_L) (append (replicate 12 None) [])))) [] TyTrLeaf [Some (TPrim Bool)] (TyTrSplit (append (replicate 2 None) (Cons (Some TSK_L) (Cons None (Cons (Some TSK_L) (append (replicate 11 None) []))))) [] TyTrLeaf [Some (TPrim Bool)] (TyTrSplit (Cons (Some TSK_L) (Cons (Some TSK_L) (append (replicate 15 None) []))) [] TyTrLeaf [Some (TPrim Bool)] (TyTrSplit (Cons (Some TSK_L) (append (replicate 2 None) (Cons (Some TSK_L) (append (replicate 14 None) [])))) [] TyTrLeaf [Some (TPrim Bool)] (TyTrSplit (Cons (Some TSK_L) (append (replicate 18 None) [])) [] TyTrLeaf [] (TyTrSplit (append (replicate 19 None) []) [] TyTrLeaf [] TyTrLeaf)))))))))))))))))))"

definition
  "ops64_typetree \<equiv> TyTrSplit (Cons (Some TSK_L) []) [] TyTrLeaf [Some (TPrim (Num U64))] (TyTrSplit (append (replicate 2 None) []) [] TyTrLeaf [Some (TPrim (Num U8))] (TyTrSplit (Cons (Some TSK_L) (append (replicate 2 None) [])) [] TyTrLeaf [Some (TPrim (Num U64))] (TyTrSplit (Cons (Some TSK_L) (Cons None (Cons (Some TSK_S) (Cons None [])))) [] TyTrLeaf [Some (TPrim (Num U64))] (TyTrSplit (Cons (Some TSK_S) (append (replicate 2 None) (Cons (Some TSK_L) (Cons None [])))) [] TyTrLeaf [Some (TPrim (Num U64))] (TyTrSplit (Cons (Some TSK_S) (Cons (Some TSK_L) (append (replicate 4 None) []))) [] TyTrLeaf [Some (TPrim (Num U64))] (TyTrSplit (Cons (Some TSK_S) (Cons (Some TSK_L) (append (replicate 5 None) []))) [] TyTrLeaf [Some (TPrim (Num U64))] (TyTrSplit (Cons (Some TSK_S) (Cons (Some TSK_L) (append (replicate 6 None) []))) [] TyTrLeaf [Some (TPrim (Num U64))] (TyTrSplit (Cons (Some TSK_L) (Cons (Some TSK_L) (append (replicate 7 None) []))) [] TyTrLeaf [Some (TPrim (Num U64))] (TyTrSplit (Cons (Some TSK_S) (append (replicate 9 None) [])) [] TyTrLeaf [Some (TPrim (Num U64))] (TyTrSplit (Cons (Some TSK_S) (Cons (Some TSK_L) (append (replicate 9 None) []))) [] TyTrLeaf [Some (TPrim (Num U64))] (TyTrSplit (Cons (Some TSK_S) (Cons (Some TSK_L) (append (replicate 10 None) []))) [] TyTrLeaf [Some (TPrim (Num U64))] (TyTrSplit (Cons (Some TSK_S) (Cons (Some TSK_L) (append (replicate 11 None) []))) [] TyTrLeaf [Some (TPrim (Num U64))] (TyTrSplit (Cons (Some TSK_S) (Cons (Some TSK_S) (append (replicate 12 None) []))) [] TyTrLeaf [Some (TPrim (Num U64))] (TyTrSplit (Cons None (Cons (Some TSK_S) (Cons (Some TSK_S) (append (replicate 12 None) [])))) [] TyTrLeaf [Some (TPrim Bool)] (TyTrSplit (Cons None (Cons (Some TSK_S) (Cons (Some TSK_L) (append (replicate 13 None) [])))) [] TyTrLeaf [Some (TPrim Bool)] (TyTrSplit (append (replicate 2 None) (Cons (Some TSK_L) (Cons None (Cons (Some TSK_L) (append (replicate 12 None) []))))) [] TyTrLeaf [Some (TPrim Bool)] (TyTrSplit (Cons (Some TSK_L) (Cons (Some TSK_L) (append (replicate 16 None) []))) [] TyTrLeaf [Some (TPrim Bool)] (TyTrSplit (Cons (Some TSK_L) (append (replicate 2 None) (Cons (Some TSK_L) (append (replicate 15 None) [])))) [] TyTrLeaf [Some (TPrim Bool)] (TyTrSplit (Cons (Some TSK_L) (append (replicate 19 None) [])) [] TyTrLeaf [] (TyTrSplit (append (replicate 20 None) []) [] (TyTrSplit (append (replicate 20 None) []) [] TyTrLeaf [Some (TPrim (Num U8))] TyTrLeaf) [] (TyTrSplit (append (replicate 20 None) []) [] TyTrLeaf [Some (TPrim (Num U8))] TyTrLeaf)))))))))))))))))))))"

definition
  "ops32_typetree \<equiv> TyTrSplit (Cons (Some TSK_L) []) [] TyTrLeaf [Some (TPrim (Num U32))] (TyTrSplit (append (replicate 2 None) []) [] TyTrLeaf [Some (TPrim (Num U8))] (TyTrSplit (Cons (Some TSK_L) (append (replicate 2 None) [])) [] TyTrLeaf [Some (TPrim (Num U32))] (TyTrSplit (Cons (Some TSK_L) (Cons None (Cons (Some TSK_S) (Cons None [])))) [] TyTrLeaf [Some (TPrim (Num U32))] (TyTrSplit (Cons (Some TSK_S) (append (replicate 2 None) (Cons (Some TSK_L) (Cons None [])))) [] TyTrLeaf [Some (TPrim (Num U32))] (TyTrSplit (Cons (Some TSK_S) (Cons (Some TSK_L) (append (replicate 4 None) []))) [] TyTrLeaf [Some (TPrim (Num U32))] (TyTrSplit (Cons (Some TSK_S) (Cons (Some TSK_L) (append (replicate 5 None) []))) [] TyTrLeaf [Some (TPrim (Num U32))] (TyTrSplit (Cons (Some TSK_S) (Cons (Some TSK_S) (append (replicate 6 None) []))) [] TyTrLeaf [Some (TPrim (Num U32))] (TyTrSplit (Cons (Some TSK_L) (Cons (Some TSK_L) (Cons (Some TSK_L) (append (replicate 6 None) [])))) [] TyTrLeaf [Some (TPrim (Num U32))] (TyTrSplit (Cons (Some TSK_S) (append (replicate 9 None) [])) [] TyTrLeaf [Some (TPrim (Num U32))] (TyTrSplit (Cons (Some TSK_S) (Cons (Some TSK_L) (append (replicate 9 None) []))) [] TyTrLeaf [Some (TPrim (Num U32))] (TyTrSplit (Cons (Some TSK_S) (Cons (Some TSK_L) (append (replicate 10 None) []))) [] TyTrLeaf [Some (TPrim (Num U32))] (TyTrSplit (Cons (Some TSK_S) (Cons (Some TSK_L) (append (replicate 11 None) []))) [] TyTrLeaf [Some (TPrim (Num U32))] (TyTrSplit (Cons (Some TSK_S) (Cons (Some TSK_S) (append (replicate 12 None) []))) [] TyTrLeaf [Some (TPrim (Num U32))] (TyTrSplit (Cons None (Cons (Some TSK_S) (Cons (Some TSK_S) (append (replicate 12 None) [])))) [] TyTrLeaf [Some (TPrim Bool)] (TyTrSplit (Cons None (Cons (Some TSK_S) (Cons (Some TSK_L) (append (replicate 13 None) [])))) [] TyTrLeaf [Some (TPrim Bool)] (TyTrSplit (append (replicate 2 None) (Cons (Some TSK_L) (Cons None (Cons (Some TSK_L) (append (replicate 12 None) []))))) [] TyTrLeaf [Some (TPrim Bool)] (TyTrSplit (Cons (Some TSK_L) (Cons (Some TSK_L) (append (replicate 16 None) []))) [] TyTrLeaf [Some (TPrim Bool)] (TyTrSplit (Cons (Some TSK_L) (append (replicate 2 None) (Cons (Some TSK_L) (append (replicate 15 None) [])))) [] TyTrLeaf [Some (TPrim Bool)] (TyTrSplit (Cons (Some TSK_L) (append (replicate 19 None) [])) [] TyTrLeaf [] (TyTrSplit (append (replicate 20 None) []) [] (TyTrSplit (append (replicate 20 None) []) [] TyTrLeaf [Some (TPrim (Num U8))] TyTrLeaf) [] (TyTrSplit (append (replicate 20 None) []) [] TyTrLeaf [Some (TPrim (Num U8))] TyTrLeaf)))))))))))))))))))))"

definition
  "ops16_typetree \<equiv> TyTrSplit (Cons (Some TSK_L) []) [] TyTrLeaf [Some (TPrim (Num U16))] (TyTrSplit (append (replicate 2 None) []) [] TyTrLeaf [Some (TPrim (Num U8))] (TyTrSplit (Cons (Some TSK_L) (append (replicate 2 None) [])) [] TyTrLeaf [Some (TPrim (Num U16))] (TyTrSplit (Cons (Some TSK_L) (Cons None (Cons (Some TSK_S) (Cons None [])))) [] TyTrLeaf [Some (TPrim (Num U16))] (TyTrSplit (Cons (Some TSK_S) (append (replicate 2 None) (Cons (Some TSK_L) (Cons None [])))) [] TyTrLeaf [Some (TPrim (Num U16))] (TyTrSplit (Cons (Some TSK_S) (Cons (Some TSK_L) (append (replicate 4 None) []))) [] TyTrLeaf [Some (TPrim (Num U16))] (TyTrSplit (Cons (Some TSK_S) (Cons (Some TSK_L) (append (replicate 5 None) []))) [] TyTrLeaf [Some (TPrim (Num U16))] (TyTrSplit (Cons (Some TSK_S) (Cons (Some TSK_S) (append (replicate 6 None) []))) [] TyTrLeaf [Some (TPrim (Num U16))] (TyTrSplit (Cons (Some TSK_L) (Cons (Some TSK_L) (Cons (Some TSK_L) (append (replicate 6 None) [])))) [] TyTrLeaf [Some (TPrim (Num U16))] (TyTrSplit (Cons (Some TSK_S) (append (replicate 9 None) [])) [] TyTrLeaf [Some (TPrim (Num U16))] (TyTrSplit (Cons (Some TSK_S) (Cons (Some TSK_L) (append (replicate 9 None) []))) [] TyTrLeaf [Some (TPrim (Num U16))] (TyTrSplit (Cons (Some TSK_S) (Cons (Some TSK_L) (append (replicate 10 None) []))) [] TyTrLeaf [Some (TPrim (Num U16))] (TyTrSplit (Cons (Some TSK_S) (Cons (Some TSK_L) (append (replicate 11 None) []))) [] TyTrLeaf [Some (TPrim (Num U16))] (TyTrSplit (Cons (Some TSK_S) (Cons (Some TSK_S) (append (replicate 12 None) []))) [] TyTrLeaf [Some (TPrim (Num U16))] (TyTrSplit (Cons None (Cons (Some TSK_S) (Cons (Some TSK_S) (append (replicate 12 None) [])))) [] TyTrLeaf [Some (TPrim Bool)] (TyTrSplit (Cons None (Cons (Some TSK_S) (Cons (Some TSK_L) (append (replicate 13 None) [])))) [] TyTrLeaf [Some (TPrim Bool)] (TyTrSplit (append (replicate 2 None) (Cons (Some TSK_L) (Cons None (Cons (Some TSK_L) (append (replicate 12 None) []))))) [] TyTrLeaf [Some (TPrim Bool)] (TyTrSplit (Cons (Some TSK_L) (Cons (Some TSK_L) (append (replicate 16 None) []))) [] TyTrLeaf [Some (TPrim Bool)] (TyTrSplit (Cons (Some TSK_L) (append (replicate 2 None) (Cons (Some TSK_L) (append (replicate 15 None) [])))) [] TyTrLeaf [Some (TPrim Bool)] (TyTrSplit (Cons (Some TSK_L) (append (replicate 19 None) [])) [] TyTrLeaf [] (TyTrSplit (append (replicate 20 None) []) [] (TyTrSplit (append (replicate 20 None) []) [] TyTrLeaf [Some (TPrim (Num U8))] TyTrLeaf) [] (TyTrSplit (append (replicate 20 None) []) [] TyTrLeaf [Some (TPrim (Num U8))] TyTrLeaf)))))))))))))))))))))"

definition
  "bool_ops_typetree \<equiv> TyTrSplit (Cons (Some TSK_L) []) [] TyTrLeaf [Some (TPrim (Num U32))] (TyTrSplit (append (replicate 2 None) []) [] TyTrLeaf [Some (TPrim (Num U8))] (TyTrSplit (Cons (Some TSK_L) (append (replicate 2 None) [])) [] TyTrLeaf [Some (TPrim (Num U32))] (TyTrSplit (Cons (Some TSK_L) (Cons None (Cons (Some TSK_S) (Cons None [])))) [] TyTrLeaf [Some (TPrim (Num U32))] (TyTrSplit (Cons (Some TSK_S) (append (replicate 2 None) (Cons (Some TSK_S) (Cons None [])))) [] TyTrLeaf [Some (TPrim (Num U32))] (TyTrSplit (Cons None (Cons (Some TSK_S) (append (replicate 2 None) (Cons (Some TSK_S) (Cons None []))))) [] TyTrLeaf [Some (TPrim Bool)] (TyTrSplit (Cons (Some TSK_L) (Cons (Some TSK_S) (Cons (Some TSK_L) (append (replicate 4 None) [])))) [] TyTrLeaf [Some (TPrim Bool)] (TyTrSplit (append (replicate 2 None) (Cons (Some TSK_L) (append (replicate 3 None) (Cons (Some TSK_L) (Cons None []))))) [] TyTrLeaf [Some (TPrim Bool)] (TyTrSplit (Cons (Some TSK_S) (Cons (Some TSK_L) (append (replicate 7 None) []))) [] TyTrLeaf [Some (TPrim Bool)] (TyTrSplit (Cons (Some TSK_L) (Cons (Some TSK_L) (append (replicate 8 None) []))) [] TyTrLeaf [Some (TPrim Bool)] (TyTrSplit (Cons (Some TSK_L) (append (replicate 10 None) [])) [] TyTrLeaf [Some (TPrim Bool)] (TyTrSplit (append (replicate 12 None) []) [] TyTrLeaf [Some (TPrim Bool)] (TyTrSplit (Cons (Some TSK_L) (Cons (Some TSK_L) (append (replicate 11 None) []))) [] TyTrLeaf [Some (TPrim Bool)] (TyTrSplit (Cons (Some TSK_L) (append (replicate 13 None) [])) [] TyTrLeaf [Some (TPrim Bool)] (TyTrSplit (append (replicate 15 None) []) [] TyTrLeaf [Some (TPrim Bool)] (TyTrSplit (Cons (Some TSK_L) (Cons (Some TSK_L) (append (replicate 14 None) []))) [] TyTrLeaf [Some (TPrim Bool)] TyTrLeaf)))))))))))))))"

ML {* open TTyping_Tactics *}

ML_quiet {*
val typing_helper_1_script : tac list = [
(RTac @{thm kind_tprim[where k = "{E,S,D}"]})
] *}


lemma typing_helper_1[unfolded abbreviated_type_defs] :
  "kinding [] (TPrim (Num U8)) {E, S, D}"
  apply (unfold abbreviated_type_defs)?
  apply (tactic {* map (fn t => DETERM (interpret_tac t @{context} 1)) typing_helper_1_script |> EVERY *})
  done

ML_quiet {*
val typing_helper_2_script : tac list = [
(RTac @{thm kind_tprim[where k = "{E,S,D}"]})
] *}


lemma typing_helper_2[unfolded abbreviated_type_defs] :
  "kinding [] (TPrim Bool) {E, S, D}"
  apply (unfold abbreviated_type_defs)?
  apply (tactic {* map (fn t => DETERM (interpret_tac t @{context} 1)) typing_helper_2_script |> EVERY *})
  done

ML_quiet {*
val typing_helper_3_script : tac list = [
(RTac @{thm kind_tprim[where k = "{E,S,D}"]})
] *}


lemma typing_helper_3[unfolded abbreviated_type_defs] :
  "kinding [] (TPrim (Num U64)) {E, S, D}"
  apply (unfold abbreviated_type_defs)?
  apply (tactic {* map (fn t => DETERM (interpret_tac t @{context} 1)) typing_helper_3_script |> EVERY *})
  done

ML_quiet {*
val typing_helper_4_script : tac list = [
(RTac @{thm kind_tprim[where k = "{E,S,D}"]})
] *}


lemma typing_helper_4[unfolded abbreviated_type_defs] :
  "kinding [] (TPrim (Num U32)) {E, S, D}"
  apply (unfold abbreviated_type_defs)?
  apply (tactic {* map (fn t => DETERM (interpret_tac t @{context} 1)) typing_helper_4_script |> EVERY *})
  done

ML_quiet {*
val typing_helper_5_script : tac list = [
(RTac @{thm kind_tprim[where k = "{E,S,D}"]})
] *}


lemma typing_helper_5[unfolded abbreviated_type_defs] :
  "kinding [] (TPrim (Num U16)) {E, S, D}"
  apply (unfold abbreviated_type_defs)?
  apply (tactic {* map (fn t => DETERM (interpret_tac t @{context} 1)) typing_helper_5_script |> EVERY *})
  done

ML_quiet {*
val ops8_typecorrect_script : hints list = [
KindingTacs [(RTac @{thm typing_helper_1})],
KindingTacs [(RTac @{thm typing_helper_1})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_1})],
TypingTacs [(RTac @{thm typing_lit'}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac []),(SimpTac ([],[]))],
KindingTacs [(RTac @{thm typing_helper_1})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_1})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_1})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_1})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_1})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_1})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_1})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_1})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_1})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_1})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_1})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_2})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_2})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_2})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_2})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_2})],
TypingTacs [],
TypingTacs [],
TypingTacs [(RTac @{thm typing_lit'}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac []),(SimpTac ([],[]))],
TypingTacs [(RTac @{thm typing_lit'}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac []),(SimpTac ([],[]))]
] *}


ML_quiet {*
val ops8_ttyping_details_future = get_all_typing_details_future @{context} "ops8"
   ops8_typecorrect_script*}


lemma ops8_typecorrect :
  "\<Xi>, fst ops8_type, (ops8_typetree, [Some (fst (snd ops8_type))]) T\<turnstile> ops8 : snd (snd ops8_type)"
  apply (tactic {* resolve_future_typecorrect @{context} ops8_ttyping_details_future *})
  done

ML_quiet {*
val ops64_typecorrect_script : hints list = [
KindingTacs [(RTac @{thm typing_helper_3})],
KindingTacs [(RTac @{thm typing_helper_3})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_1})],
TypingTacs [(RTac @{thm typing_lit'}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac []),(SimpTac ([],[]))],
KindingTacs [(RTac @{thm typing_helper_3})],
TypingTacs [(RTac @{thm typing_cast}),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_1}]),(SimpTac ([],[])),(SimpTac ([],[]))],
KindingTacs [(RTac @{thm typing_helper_3})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_3})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_3})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_3})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_3})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_3})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_3})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_3})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_3})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_3})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_3})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_2})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_2})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_2})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_2})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_2})],
TypingTacs [],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_1})],
TypingTacs [(RTac @{thm typing_lit'}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac []),(SimpTac ([],[]))],
TypingTacs [(RTac @{thm typing_cast}),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_1}]),(SimpTac ([],[])),(SimpTac ([],[]))],
KindingTacs [(RTac @{thm typing_helper_1})],
TypingTacs [(RTac @{thm typing_lit'}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac []),(SimpTac ([],[]))],
TypingTacs [(RTac @{thm typing_cast}),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_1}]),(SimpTac ([],[])),(SimpTac ([],[]))]
] *}


ML_quiet {*
val ops64_ttyping_details_future = get_all_typing_details_future @{context} "ops64"
   ops64_typecorrect_script*}


lemma ops64_typecorrect :
  "\<Xi>, fst ops64_type, (ops64_typetree, [Some (fst (snd ops64_type))]) T\<turnstile> ops64 : snd (snd ops64_type)"
  apply (tactic {* resolve_future_typecorrect @{context} ops64_ttyping_details_future *})
  done

ML_quiet {*
val ops32_typecorrect_script : hints list = [
KindingTacs [(RTac @{thm typing_helper_4})],
KindingTacs [(RTac @{thm typing_helper_4})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_1})],
TypingTacs [(RTac @{thm typing_lit'}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac []),(SimpTac ([],[]))],
KindingTacs [(RTac @{thm typing_helper_4})],
TypingTacs [(RTac @{thm typing_cast}),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_1}]),(SimpTac ([],[])),(SimpTac ([],[]))],
KindingTacs [(RTac @{thm typing_helper_4})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_4})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_4})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_4})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_4})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_4})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_4})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_4})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_4})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_4})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_4})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_2})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_2})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_2})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_2})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_2})],
TypingTacs [],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_1})],
TypingTacs [(RTac @{thm typing_lit'}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac []),(SimpTac ([],[]))],
TypingTacs [(RTac @{thm typing_cast}),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_1}]),(SimpTac ([],[])),(SimpTac ([],[]))],
KindingTacs [(RTac @{thm typing_helper_1})],
TypingTacs [(RTac @{thm typing_lit'}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac []),(SimpTac ([],[]))],
TypingTacs [(RTac @{thm typing_cast}),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_1}]),(SimpTac ([],[])),(SimpTac ([],[]))]
] *}


ML_quiet {*
val ops32_ttyping_details_future = get_all_typing_details_future @{context} "ops32"
   ops32_typecorrect_script*}


lemma ops32_typecorrect :
  "\<Xi>, fst ops32_type, (ops32_typetree, [Some (fst (snd ops32_type))]) T\<turnstile> ops32 : snd (snd ops32_type)"
  apply (tactic {* resolve_future_typecorrect @{context} ops32_ttyping_details_future *})
  done

ML_quiet {*
val ops16_typecorrect_script : hints list = [
KindingTacs [(RTac @{thm typing_helper_5})],
KindingTacs [(RTac @{thm typing_helper_5})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_1})],
TypingTacs [(RTac @{thm typing_lit'}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac []),(SimpTac ([],[]))],
KindingTacs [(RTac @{thm typing_helper_5})],
TypingTacs [(RTac @{thm typing_cast}),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_1}]),(SimpTac ([],[])),(SimpTac ([],[]))],
KindingTacs [(RTac @{thm typing_helper_5})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_5})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_5})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_5})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_5})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_5})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_5})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_5})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_5})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_5})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_5})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_2})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_2})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_2})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_2})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_2})],
TypingTacs [],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_1})],
TypingTacs [(RTac @{thm typing_lit'}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac []),(SimpTac ([],[]))],
TypingTacs [(RTac @{thm typing_cast}),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_1}]),(SimpTac ([],[])),(SimpTac ([],[]))],
KindingTacs [(RTac @{thm typing_helper_1})],
TypingTacs [(RTac @{thm typing_lit'}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac []),(SimpTac ([],[]))],
TypingTacs [(RTac @{thm typing_cast}),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_1}]),(SimpTac ([],[])),(SimpTac ([],[]))]
] *}


ML_quiet {*
val ops16_ttyping_details_future = get_all_typing_details_future @{context} "ops16"
   ops16_typecorrect_script*}


lemma ops16_typecorrect :
  "\<Xi>, fst ops16_type, (ops16_typetree, [Some (fst (snd ops16_type))]) T\<turnstile> ops16 : snd (snd ops16_type)"
  apply (tactic {* resolve_future_typecorrect @{context} ops16_ttyping_details_future *})
  done

ML_quiet {*
val bool_ops_typecorrect_script : hints list = [
KindingTacs [(RTac @{thm typing_helper_4})],
KindingTacs [(RTac @{thm typing_helper_4})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_1})],
TypingTacs [(RTac @{thm typing_lit'}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac []),(SimpTac ([],[]))],
KindingTacs [(RTac @{thm typing_helper_4})],
TypingTacs [(RTac @{thm typing_cast}),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_1}]),(SimpTac ([],[])),(SimpTac ([],[]))],
KindingTacs [(RTac @{thm typing_helper_4})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_4})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_2})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_2})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_2})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_2})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_2})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_2})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_2})],
TypingTacs [(RTac @{thm typing_lit'}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac []),(SimpTac ([],[]))],
KindingTacs [(RTac @{thm typing_helper_2})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_2})],
TypingTacs [],
KindingTacs [(RTac @{thm typing_helper_2})],
TypingTacs [(RTac @{thm typing_lit'}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac []),(SimpTac ([],[]))],
KindingTacs [(RTac @{thm typing_helper_2})],
TypingTacs [],
TypingTacs []
] *}


ML_quiet {*
val bool_ops_ttyping_details_future = get_all_typing_details_future @{context} "bool_ops"
   bool_ops_typecorrect_script*}


lemma bool_ops_typecorrect :
  "\<Xi>, fst bool_ops_type, (bool_ops_typetree, [Some (fst (snd bool_ops_type))]) T\<turnstile> bool_ops : snd (snd bool_ops_type)"
  apply (tactic {* resolve_future_typecorrect @{context} bool_ops_ttyping_details_future *})
  done

ML_quiet {*
val (_, ops8_typing_tree, ops8_typing_bucket)
= Future.join ops8_ttyping_details_future
*}


ML_quiet {*
val (_, ops64_typing_tree, ops64_typing_bucket)
= Future.join ops64_ttyping_details_future
*}


ML_quiet {*
val (_, ops32_typing_tree, ops32_typing_bucket)
= Future.join ops32_ttyping_details_future
*}


ML_quiet {*
val (_, ops16_typing_tree, ops16_typing_bucket)
= Future.join ops16_ttyping_details_future
*}


ML_quiet {*
val (_, bool_ops_typing_tree, bool_ops_typing_bucket)
= Future.join bool_ops_ttyping_details_future
*}


(* end Cogent semantics *)

(* C semantics, generated by C parser *)
new_C_include_dir "../../cogent/tests"
install_C_file "pass_prim-ops.c"

autocorres [ts_rules=nondet, no_opt, gen_word_heaps, skip_word_abs] "pass_prim-ops.c"

instantiation bool_t_C :: cogent_C_val
begin
definition type_rel_bool_t_C_def:
  "type_rel typ (_ :: bool_t_C itself) \<equiv> (typ = RPrim Bool)"

definition val_rel_bool_t_C_def:
  "val_rel uv (x :: bool_t_C) \<equiv> uv = UPrim (LBool (bool_t_C.boolean_C x \<noteq> 0))"
instance ..
end

(* Relation between Cogent and C data *)
local_setup{* local_setup_val_rel_type_rel_put_them_in_buckets "pass_prim-ops.c" *}

(* Lemma bucket.*)
ML{* TypeRelSimp.get @{context} *}
ML{* ValRelSimp.get @{context} *}

lemmas val_rel_simps[ValRelSimp] = val_rel_word val_rel_ptr_def val_rel_bool_t_C_def
lemmas type_rel_simps[TypeRelSimp] = type_rel_word type_rel_ptr_def type_rel_bool_t_C_def

class cogent_C_heap = cogent_C_val +
  fixes is_valid    :: "lifted_globals \<Rightarrow> 'a ptr \<Rightarrow> bool"
  fixes heap        :: "lifted_globals \<Rightarrow> 'a ptr \<Rightarrow> 'a"
  fixes heap_update :: "(('a ptr \<Rightarrow> 'a) \<Rightarrow> 'a ptr \<Rightarrow> 'a) \<Rightarrow> lifted_globals \<Rightarrow> lifted_globals"

local_setup{* local_setup_instantiate_cogent_C_heaps_store_them_in_buckets "pass_prim-ops.c"*}
ML{* HeapSimp.get @{context}; IsValidSimp.get @{context} *}

locale take_cogent = "pass_prim-ops" + update_sem_init
begin

(* Relation between program heaps *)
definition
  heap_rel_ptr ::
  "(funtyp, abstyp, ptrtyp) store \<Rightarrow> lifted_globals \<Rightarrow>
   ('a :: cogent_C_heap) ptr \<Rightarrow> bool"
where
  "heap_rel_ptr \<sigma> h p \<equiv>
   (\<forall>uv.
     \<sigma> (ptr_val p) = Some uv \<longrightarrow>
     type_rel (uval_repr uv) TYPE('a) \<longrightarrow>
     is_valid h p \<and> val_rel uv (heap h p))"

lemma heap_rel_ptr_meta:
  "heap_rel_ptr = heap_rel_meta is_valid heap"
  by (simp add: heap_rel_ptr_def[abs_def] heap_rel_meta_def[abs_def])

lemmas heap_rel_def = TrueI

definition state_rel :: "((funtyp, abstyp, ptrtyp) store \<times> lifted_globals) set"
where
  "state_rel = {(\<sigma>, h). True}"


(* Preprocess AutoCorres output *)
local_setup {* fold tidy_C_fun_def' Cogent_functions *}

(* Defined here because it relies on bool_t_C *)

lemma corres_if_base:
  assumes split\<Gamma>: "[] \<turnstile> \<Gamma>' \<leadsto> \<Gamma>1 | \<Gamma>2"
  assumes typing_cond: "\<Xi>', [], \<Gamma>1 \<turnstile> Var c : TPrim Bool"
  assumes val_rel_cond: "\<gamma>!c = UPrim (LBool (bool_val' c' \<noteq> (0::word8)))"
  assumes corres_true: "corres srel a a' \<xi> \<gamma> \<Xi>' \<Gamma>2 \<sigma> s"
  assumes corres_false: "corres srel b b' \<xi> \<gamma> \<Xi>' \<Gamma>2 \<sigma> s"
  shows "corres srel (If (Var c) a b)
           (do x \<leftarrow> condition (\<lambda>s. bool_val' c' \<noteq> 0) a' b'; gets (\<lambda>_. x) od)
           \<xi> \<gamma> \<Xi>' \<Gamma>' \<sigma> s"
  apply (clarsimp simp: corres_def snd_condition in_condition)
  apply (rename_tac r w)
  apply (insert typing_cond)
  apply (erule typing_varE)
  apply (frule matches_ptrs_split'[OF split\<Gamma>])
  apply clarsimp
  apply (rename_tac r' w' r'' w'')
  apply (frule_tac \<Gamma>=\<Gamma>1 in matches_ptrs_proj', simp+)
  apply clarsimp
  apply (rename_tac rr')
  apply (insert val_rel_cond[unfolded val_rel_bool_t_C_def])
  apply clarsimp
  apply (cases "bool_val' c'=0")
   apply (insert corres_false[unfolded corres_def])[1]
   apply simp
   apply (erule impE, fast)
   apply clarsimp
   apply (rename_tac v' s')
   apply (erule_tac x=v' in allE)
   apply (erule_tac x=s' in allE )
   apply clarsimp
   apply (rename_tac \<sigma>' v)
   apply (rule_tac x=\<sigma>' in exI)
   apply (rule_tac x=v in exI)
   apply (fastforce intro!: u_sem_if u_sem_var elim: subst split: uval.splits lit.splits) 
  apply (insert corres_true[unfolded corres_def])[1]
  apply simp
  apply (erule impE, fast)
  apply clarsimp
  apply (rename_tac v' s')
  apply (erule_tac x=v' in allE)
  apply (erule_tac x=s' in allE )
  apply clarsimp
  apply (rename_tac \<sigma>' v)
  apply (rule_tac x=\<sigma>' in exI)
  apply (rule_tac x=v in exI)
  apply (fastforce intro!: u_sem_if u_sem_var elim: subst split: uval.splits lit.splits)
  done

lemmas corres_if = corres_if_base[where bool_val' = boolean_C,
                     OF _ _ val_rel_bool_t_C_def[THEN meta_eq_to_obj_eq, THEN iffD1]]

(* dummy *)
lemmas corres_nested_let = TrueI

lemma ops32_corres:
  "val_rel a a' \<Longrightarrow> corres state_rel ops32 (ops32' a') \<xi> [a] \<Xi> [Some (fst (snd ops32_type))] \<sigma> s"
  apply (tactic {* corres_tac @{context}
    (peel_two ops32_typing_tree)
    @{thms ops32_def ops32'_def' ops32_type_def abbreviated_type_defs} [] []
    @{thm corres_if} [] @{thms } @{thms } []
    @{thm LETBANG_TRUE_def} @{thms } true *})
  done

lemma ops64_corres:
  "val_rel a a' \<Longrightarrow> corres state_rel ops64 (ops64' a') \<xi> [a] \<Xi> [Some (fst (snd ops64_type))] \<sigma> s"
  apply (tactic {* corres_tac @{context}
    (peel_two ops64_typing_tree)
    @{thms ops64_def ops64'_def' ops64_type_def abbreviated_type_defs} [] []
    @{thm corres_if} [] @{thms } @{thms } []
    @{thm LETBANG_TRUE_def} @{thms } true *})
  done

lemma ops8_corres:
  "val_rel a a' \<Longrightarrow> corres state_rel ops8 (ops8' a') \<xi> [a] \<Xi> [Some (fst (snd ops8_type))] \<sigma> s"
  apply (tactic {* corres_tac @{context}
    (peel_two ops8_typing_tree)
    @{thms ops8_def ops8'_def' ops8_type_def abbreviated_type_defs} [] []
    @{thm corres_if} [] @{thms } @{thms } []
    @{thm LETBANG_TRUE_def} @{thms } true *})
  done

lemma ops16_corres:
  "val_rel a a' \<Longrightarrow> corres state_rel ops16 (ops16' a') \<xi> [a] \<Xi> [Some (fst (snd ops16_type))] \<sigma> s"
  apply (tactic {* corres_tac @{context}
    (peel_two ops16_typing_tree)
    @{thms ops16_def ops16'_def' ops16_type_def abbreviated_type_defs} [] []
    @{thm corres_if} [] @{thms } @{thms } []
    @{thm LETBANG_TRUE_def} @{thms } true *})
  done

lemma bool_ops_corres:
  "val_rel a a' \<Longrightarrow> corres state_rel bool_ops (bool_ops' a') \<xi> [a] \<Xi> [Some (fst (snd bool_ops_type))] \<sigma> s"
  apply (tactic {* corres_tac @{context}
    (peel_two bool_ops_typing_tree)
    @{thms bool_ops_def bool_ops'_def' bool_ops_type_def abbreviated_type_defs} [] []
    @{thm corres_if} [] @{thms } @{thms } []
    @{thm LETBANG_TRUE_def} @{thms } true *})
  done

end
end