Theory Contracts

section ‹Contracts›
theory Contracts
  imports Environment
begin

subsection ‹Syntax of Contracts›

datatype l = Id Identifier
           | Ref Identifier "e list"
and      e = INT bits int
           | UINT bits int
           | ADDRESS String.literal
           | BALANCE e
           | THIS
           | SENDER
           | VALUE
           | TRUE
           | FALSE
           | LVAL l
           | PLUS e e
           | MINUS e e
           | EQUAL e e
           | LESS e e
           | AND e e
           | OR e e
           | NOT e
           | CALL Identifier "e list"
           | ECALL e Identifier "e list"
           | CONTRACTS

datatype s = SKIP
           | BLOCK "Identifier × type × (e option)" s
           | ASSIGN l e
           | TRANSFER e e
           | COMP s s
           | ITE e s s
           | WHILE e s
           | INVOKE Identifier "e list"
           | EXTERNAL e Identifier "e list" e
           | NEW Identifier "e list" e

subsection ‹state›

type_synonym gas = nat

record state =   
  Accounts :: accounts
  Stack :: stack
  Memory :: memoryT
  Storage :: "address ⇒ storageT"
  Gas :: gas

lemma all_gas_le:
  assumes "state.Gas x<(state.Gas y::nat)"
      and "∀z. state.Gas z < state.Gas y ⟶ P z ⟶ Q z"
    shows "∀z. state.Gas z ≤ state.Gas x ∧ P z ⟶ Q z" using assms by simp

lemma all_gas_less:
  assumes "∀z. state.Gas z < state.Gas y ⟶ P z"
      and "state.Gas x≤(state.Gas y::nat)"
    shows "∀z. state.Gas z < state.Gas x ⟶ P z" using assms by simp

definition incrementAccountContracts :: "address ⇒ state ⇒ state"
  where "incrementAccountContracts ad st = st ⦇Accounts := (Accounts st)(ad := (Accounts st ad)⦇Contracts := Suc (Contracts (Accounts st ad))⦈)⦈"

declare incrementAccountContracts_def [solidity_symbex]

lemma incrementAccountContracts_type[simp]:
  "Type (Accounts (incrementAccountContracts ad st) ad') = Type (Accounts st ad')"
  using incrementAccountContracts_def by simp

lemma incrementAccountContracts_bal[simp]:
  "Bal (Accounts (incrementAccountContracts ad st) ad') = Bal (Accounts st ad')"
  using incrementAccountContracts_def by simp

lemma incrementAccountContracts_stack[simp]:
  "Stack (incrementAccountContracts ad st) = Stack st"
  using incrementAccountContracts_def by simp

lemma incrementAccountContracts_memory[simp]:
  "Memory (incrementAccountContracts ad st) = Memory st"
  using incrementAccountContracts_def by simp

lemma incrementAccountContracts_storage[simp]:
  "Storage (incrementAccountContracts ad st) = Storage st"
  using incrementAccountContracts_def by simp

lemma incrementAccountContracts_gas[simp]:
  "Gas (incrementAccountContracts ad st) = Gas st"
  using incrementAccountContracts_def by simp

lemma gas_induct:
  assumes "⋀s. ∀s'. Gas s' < Gas s ⟶ P s' ⟹ P s"
  shows "P s" using assms by (rule Nat.measure_induct[of Gas])

definition emptyStorage :: "address ⇒ storageT"
where
  "emptyStorage _ = {$$}"

declare emptyStorage_def [solidity_symbex]

abbreviation mystate::state
  where "mystate ≡ ⦇
    Accounts = emptyAccount,
    Stack = emptyStore,
    Memory = emptyTypedStore,
    Storage = emptyStorage,
    Gas = 0
  ⦈"

datatype ex = Gas | Err

subsection ‹Contracts›

text ‹
  A contract consists of methods, functions, and storage variables.

  A method is a triple consisting of
  ▪ A list of formal parameters
  ▪ A flag to signal external methods
  ▪ A statement


  A function is a pair consisting of
  ▪ A list of formal parameters
  ▪ A flag to signal external functions
  ▪ An expression
›
datatype(discs_sels) member = Method "(Identifier × type) list × bool × s"
                | Function "(Identifier × type) list × bool × e"
                | Var stypes

text ‹
  A procedure environment assigns a contract to an address.
  A contract consists of
  ▪ An assignment of contract to identifiers
  ▪ A constructor
  ▪ A fallback statement which is executed after money is beeing transferred to the contract.

  \url{https://docs.soliditylang.org/en/v0.8.6/Contracts.html#fallback-function}
›

type_synonym contract = "(Identifier, member) fmap × ((Identifier × type) list × s) × s"

type_synonym environmentp = "(Identifier, contract) fmap"

definition init::"(Identifier, member) fmap ⇒ Identifier ⇒ environment ⇒ environment"
  where "init ct i e = (case ct $$ i of
                                Some (Var tp) ⇒ updateEnvDup i (type.Storage tp) (Storeloc i) e
                               | _ ⇒ e)"

declare init_def [solidity_symbex]

lemma init_s11[simp]:
  assumes "fmlookup ct i = Some (Var tp)"
  shows "init ct i e = updateEnvDup i (type.Storage tp) (Storeloc i) e"
  using assms init_def by simp

lemma init_s12[simp]:
  assumes "i |∈| fmdom (Denvalue e)"
  shows "init ct i e = e"
proof (cases "fmlookup ct i")
  case None
  then show ?thesis using init_def by simp
next
  case (Some a)
  then show ?thesis
  proof (cases a)
    case (Method _)
    with Some show ?thesis using init_def by simp
  next
    case (Function _)
    with Some show ?thesis using init_def by simp
  next
    case (Var tp)
    with Some have "init ct i e = updateEnvDup i (type.Storage tp) (Storeloc i) e" using init_def by simp
    moreover from assms have "updateEnvDup i (type.Storage tp) (Storeloc i) e = e" by auto
    ultimately show ?thesis by simp
  qed
qed

lemma init_s13[simp]:
  assumes "fmlookup ct i = Some (Var tp)"
      and "¬ i |∈| fmdom (Denvalue e)"
  shows "init ct i e = updateEnv i (type.Storage tp) (Storeloc i) e"
  using assms init_def by auto

lemma init_s21[simp]:
  assumes "fmlookup ct i = None"
  shows "init ct i e = e"
  using assms init_def by auto

lemma init_s22[simp]:
  assumes "fmlookup ct i = Some (Method m)"
  shows "init ct i e = e"
  using assms init_def by auto

lemma init_s23[simp]:
  assumes "fmlookup ct i = Some (Function f)"
  shows "init ct i e = e"
  using assms init_def by auto

lemma init_commte: "comp_fun_commute (init ct)"
proof
  fix x y
  show "init ct y ∘ init ct x = init ct x ∘ init ct y"
  proof
    fix e
    show "(init ct y ∘ init ct x) e = (init ct x ∘ init ct y) e"
    proof (cases "fmlookup ct x")
      case None
      then show ?thesis by simp
    next
      case s1: (Some a)
      then show ?thesis
      proof (cases a)
        case (Method _)
        with s1 show ?thesis by simp
      next
        case (Function _)
        with s1 show ?thesis by simp
      next
        case v1: (Var tp)
        then show ?thesis
        proof (cases "x |∈| fmdom (Denvalue e)")
          case True
          with s1 v1 have *: "init ct x e = e" by auto
          then show ?thesis
          proof (cases "fmlookup ct y")
            case None
            then show ?thesis by simp
          next
            case s2: (Some a)
            then show ?thesis
            proof (cases a)
              case (Method _)
              with s2 show ?thesis by simp
            next
              case (Function _)
              with s2 show ?thesis by simp
            next
              case v2: (Var tp')
              then show ?thesis
              proof (cases "y |∈| fmdom (Denvalue e)")
                case t1: True
                with s1 v1 True s2 v2 show ?thesis by fastforce
              next
                define e' where "e' = updateEnv y (type.Storage tp') (Storeloc y) e"
                case False
                with s2 v2 have "init ct y e = e'" using e'_def by auto
                with s1 v1 True e'_def * show ?thesis by auto
              qed
            qed
          qed
        next
          define e' where "e' = updateEnv x (type.Storage tp) (Storeloc x) e"
          case f1: False
          with s1 v1 have *: "init ct x e = e'" using e'_def by auto
          then show ?thesis
          proof (cases "fmlookup ct y")
            case None
            then show ?thesis by simp
          next
            case s3: (Some a)
            then show ?thesis
            proof (cases a)
              case (Method _)
              with s3 show ?thesis by simp
            next
              case (Function _)
              with s3 show ?thesis by simp
            next
              case v2: (Var tp')
              then show ?thesis
              proof (cases "y |∈| fmdom (Denvalue e)")
                case t1: True
                with e'_def have "y |∈| fmdom (Denvalue e')" by simp
                with s1 s3 v1 f1 v2 show ?thesis using e'_def by fastforce
              next
                define f' where "f' = updateEnv y (type.Storage tp') (Storeloc y) e"
                define e'' where "e'' = updateEnv y (type.Storage tp') (Storeloc y) e'"
                case f2: False
                with s3 v2 have **: "init ct y e = f'" using f'_def by auto
                show ?thesis
                proof (cases "y = x")
                  case True
                  with s3 v2 e'_def have "init ct y e' = e'" by simp
                  moreover from s3 v2 True f'_def have "init ct x f' = f'" by simp
                  ultimately show ?thesis using True by simp
                next
                  define f'' where "f'' = updateEnv x (type.Storage tp) (Storeloc x) f'"
                  case f3: False
                  with f2 have "¬ y |∈| fmdom (Denvalue e')" using e'_def by simp
                  with s3 v2 e''_def have "init ct y e' = e''" by auto
                  with * have "(init ct y ∘ init ct x) e = e''" by simp
                  moreover have "init ct x f' = f''"
                  proof -
                    from s1 v1 have "init ct x f' = updateEnvDup x (type.Storage tp) (Storeloc x) f'" by simp
                    moreover from f1 f3 have "x |∉| fmdom (Denvalue f')" using f'_def by simp
                    ultimately show ?thesis using f''_def by auto
                  qed
                  moreover from f''_def e''_def f'_def e'_def f3 have "Some f'' = Some e''" using env_reorder_neq by simp
                  ultimately show ?thesis using ** by simp
                qed
              qed
            qed
          qed
        qed
      qed
    qed
  qed
qed

lemma init_address[simp]:
  "Address (init ct i e) = Address e"
proof (cases "fmlookup ct i")
  case None
  then show ?thesis by simp
next
  case (Some a)
  show ?thesis
  proof (cases a)
    case (Method _)
    with Some show ?thesis by simp
  next
    case (Function _)
    with Some show ?thesis by simp
  next
    case (Var _)
    with Some show ?thesis using updateEnvDup_address updateEnvDup_sender by simp
  qed 
qed

lemma init_sender[simp]:
"Sender (init ct i e) = Sender e"
proof (cases "fmlookup ct i")
  case None
  then show ?thesis by simp
next
  case (Some a)
  show ?thesis
  proof (cases a)
    case (Method _)
    with Some show ?thesis by simp
  next
    case (Function _)
    with Some show ?thesis by simp
  next
    case (Var _)
    with Some show ?thesis using updateEnvDup_sender by simp
  qed 
qed

lemma init_svalue[simp]:
"Svalue (init ct i e) = Svalue e"
proof (cases "fmlookup ct i")
  case None
  then show ?thesis by simp
next
  case (Some a)
  show ?thesis
  proof (cases a)
    case (Method _)
    with Some show ?thesis by simp
  next
    case (Function _)
    with Some show ?thesis by simp
  next
    case (Var _)
    with Some show ?thesis using updateEnvDup_svalue by simp
  qed
qed

lemma init_contract[simp]:
"Contract (init ct i e) = Contract e"
proof (cases "fmlookup ct i")
  case None
  then show ?thesis by simp
next
  case (Some a)
  show ?thesis
  proof (cases a)
    case (Method _)
    with Some show ?thesis by simp
  next
    case (Function _)
    with Some show ?thesis by simp
  next
    case (Var _)
    with Some show ?thesis using updateEnvDup_contract by simp
  qed
qed

lemma ffold_init_ad_same[rule_format]: "∀e'. ffold (init ct) e xs = e' ⟶ Address e' = Address e ∧ Sender e' = Sender e ∧ Svalue e' = Svalue e ∧ Contract e' = Contract e"
proof (induct xs)
  case empty
  then show ?case by (simp add: ffold_def)
next
  case (insert x xs)
  then have *: "ffold (init ct) e (finsert x xs) =
    init ct x (ffold (init ct) e xs)" using FSet.comp_fun_commute.ffold_finsert[OF init_commte] by simp
  show ?case
  proof (rule allI[OF impI])
    fix e' assume **: "ffold (init ct) e (finsert x xs) = e'"
    with * obtain e'' where ***: "ffold (init ct) e xs = e''" by simp
    with insert have "Address e'' = Address e ∧ Sender e'' = Sender e ∧ Svalue e'' = Svalue e ∧ Contract e'' = Contract e" by blast
    with * ** *** show "Address e' = Address e ∧ Sender e' = Sender e ∧ Svalue e' = Svalue e ∧ environment.Contract e' = environment.Contract e" 
      using init_address init_sender init_svalue init_contract by metis
  qed
qed

lemma ffold_init_ad[simp]: "Address (ffold (init ct) e xs) = Address e"
  using ffold_init_ad_same by simp

lemma ffold_init_sender[simp]: "Sender (ffold (init ct) e xs) = Sender e"
  using ffold_init_ad_same by simp

lemma ffold_init_contract[simp]: "Contract (ffold (init ct) e xs) = Contract e"
  using ffold_init_ad_same by simp


lemma ffold_init_dom:
  "fmdom (Denvalue (ffold (init ct) e xs)) |⊆| fmdom (Denvalue e) |∪| xs"
proof (induct "xs")
  case empty
  then show ?case
  proof
    fix x
    assume "x |∈| fmdom (Denvalue (ffold (init ct) e {||}))"
    moreover have "ffold (init ct) e {||} = e" using FSet.comp_fun_commute.ffold_empty[OF init_commte, of ct e] by simp
    ultimately show "x |∈| fmdom (Denvalue e) |∪| {||}" by simp
  qed
next
  case (insert x xs)
  then have *: "ffold (init ct) e (finsert x xs) =
    init ct x (ffold (init ct) e xs)" using FSet.comp_fun_commute.ffold_finsert[OF init_commte] by simp

  show ?case
  proof
    fix x' assume "x' |∈| fmdom (Denvalue (ffold (init ct) e (finsert x xs)))"
    with * have **: "x' |∈| fmdom (Denvalue (init ct x (ffold (init ct) e xs)))" by simp
    then consider "x' |∈| fmdom (Denvalue (ffold (init ct) e xs))" | "x'=x"
    proof (cases "fmlookup ct x")
      case None
      then show ?thesis using that ** by simp
    next
      case (Some a)
      then show ?thesis
      proof (cases a)
        case (Method _)
        then show ?thesis using Some ** that by simp
      next
        case (Function _)
        then show ?thesis using Some ** that by simp
      next
        case (Var x2)
        show ?thesis
        proof (cases "x=x'")
          case True
          then show ?thesis using that by simp
        next
          case False
          then have "fmlookup (Denvalue (updateEnvDup x (type.Storage x2) (Storeloc x) (ffold (init ct) e xs))) x' = fmlookup (Denvalue (ffold (init ct) e xs)) x'" using updateEnvDup_dup by simp
          moreover from ** Some Var have ***:"x' |∈| fmdom (Denvalue (updateEnvDup x (type.Storage x2) (Storeloc x) (ffold (init ct) e xs)))" by simp
          ultimately have "x' |∈| fmdom (Denvalue (ffold (init ct) e xs))" by (simp add: fmlookup_dom_iff)
          then show ?thesis using that by simp
        qed
      qed 
    qed
    then show "x' |∈| fmdom (Denvalue e) |∪| finsert x xs"
    proof cases
      case 1
      then show ?thesis using insert.hyps by auto
    next
      case 2
      then show ?thesis by simp
    qed
  qed
qed

lemma ffold_init_fmap: 
  assumes "ct $$ i = Some (Var tp)"
      and "i |∉| fmdom (Denvalue e)"
  shows "i|∈|xs ⟹ Denvalue (ffold (init ct) e xs) $$ i = Some (type.Storage tp, Storeloc i)"
proof (induct "xs")
  case empty
  then show ?case by simp
next
  case (insert x xs)
  then have *: "ffold (init ct) e (finsert x xs) =
    init ct x (ffold (init ct) e xs)" using FSet.comp_fun_commute.ffold_finsert[OF init_commte] by simp

  from insert.prems consider (a) "i |∈| xs" | (b) "¬ i |∈| xs ∧ i = x" by auto
  then show "fmlookup (Denvalue (ffold (init ct) e (finsert x xs))) i = Some (type.Storage tp, Storeloc i)"
  proof cases
    case a
    with insert.hyps(2) have "fmlookup (Denvalue (ffold (init ct) e xs)) i = Some (type.Storage tp, Storeloc i)" by simp
    moreover have "fmlookup (Denvalue (init ct x (ffold (init ct) e xs))) i = fmlookup (Denvalue (ffold (init ct) e xs)) i"
    proof (cases "ct $$ x")
      case None
      then show ?thesis by simp
    next
      case (Some a)
      then show ?thesis
      proof (cases a)
        case (Method _)
        with Some show ?thesis by simp
      next
        case (Function _)
        with Some show ?thesis by simp
      next
        case (Var x2)
        with Some have "init ct x (ffold (init ct) e xs) = updateEnvDup x (type.Storage x2) (Storeloc x) (ffold (init ct) e xs)" using init_def[of ct x "(ffold (init ct) e xs)"] by simp
        moreover from insert a have "i≠x" by auto
        then have "Denvalue (updateEnvDup x (type.Storage x2) (Storeloc x) (ffold (init ct) e xs)) $$ i = Denvalue (ffold (init ct) e xs) $$ i" using updateEnvDup_dup[of x i] by simp
        ultimately show ?thesis by simp
      qed
    qed
    ultimately show ?thesis using * by simp
  next
    case b
    with assms(1) have "fmlookup ct x = Some (Var tp)" by simp
    moreover from b assms(2) have "¬ x |∈| fmdom (Denvalue (ffold (init ct) e xs))" using ffold_init_dom by auto
    ultimately have "init ct x (ffold (init ct) e xs) = updateEnv x (type.Storage tp) (Storeloc x) (ffold (init ct) e xs)" by auto
    with b * show ?thesis by simp
  qed
qed

lemma ffold_init_fmdom: 
  assumes "fmlookup ct i = Some (Var tp)"
      and "i |∉| fmdom (Denvalue e)"
    shows "fmlookup (Denvalue (ffold (init ct) e (fmdom ct))) i = Some (type.Storage tp, Storeloc i)"
proof -
  from assms(1) have "i |∈| fmdom ct" by (rule Finite_Map.fmdomI)
  then show ?thesis using ffold_init_fmap[OF assms] by simp
qed

lemma ffold_init_emptyDen:
  shows " fmlookup (Denvalue (ffold (init ct) (emptyEnv a b c d) xs)) i = Some x ⟶ i |∈| xs"
proof(induct xs)
  case empty
  then show ?case 
    by (simp add: comp_fun_commute.ffold_empty init_commte)
next
  case (insert x xs)
 then have *: "ffold (init ct) (emptyEnv a b c d) (finsert x xs) =
    init ct x (ffold (init ct) (emptyEnv a b c d) xs)" 
   using FSet.comp_fun_commute.ffold_finsert[OF init_commte] by simp
  then show ?case 
    by (metis Environment.select_convs(5) emptyEnv_def femptyE ffold_init_dom finsert_absorb finsert_fsubset fmdomI
        fmdom_empty funionE)
qed

lemma ffold_init_emptyDen_ran:
  shows "fmlookup (Denvalue (ffold (init ct) (emptyEnv a b c d) xs)) i = Some (type.Storage tp, Storeloc i)
          ⟶ ct $$ i = Some(Var tp) "
proof(induct xs)
  case empty
  then show ?case 
    by (simp add: comp_fun_commute.ffold_empty init_commte)
next
  case (insert x xs)
 then have *: "ffold (init ct) (emptyEnv a b c d) (finsert x xs) =
    init ct x (ffold (init ct) (emptyEnv a b c d) xs)" 
   using FSet.comp_fun_commute.ffold_finsert[OF init_commte] by simp

  then show ?case 
  proof(cases "x = i")
    case True
    then show ?thesis using * 
      by (smt (z3) member.exhaust Option.option.simps(4) type.inject(4) domIff emptyEnv_denvalue femptyE
          ffold_init_emptyDen ffold_init_fmap fmdom.rep_eq fmdom_empty fmlookup_dom_iff init_commte init_def init_s22
          init_s23 insert.hyps(1) option.inject prod.inject)
  next
    case False
    show ?thesis
    proof intros
      assume **:"Denvalue (ffold (init ct) (emptyEnv a b c d) (finsert x xs)) $$ i = Some (type.Storage tp, Storeloc i)"
      then have "Denvalue (init ct x (ffold (init ct) (emptyEnv a b c d) xs)) $$ i = Some (type.Storage tp, Storeloc i)" using * by simp
      then show " ct $$ i = Some (Var tp) " using False 
        by (metis (lifting) member.exhaust_sel domIff fmdom.rep_eq fmdomE init_s11 init_s21 init_s22 init_s23
            insert.hyps(2) updateEnvDup_dup)
    qed
  qed
qed

text‹The following definition allows for a more fine-grained configuration of the 
     code generator.
›
definition ffold_init::"(String.literal, member) fmap ⇒ environment ⇒ String.literal fset ⇒ environment" where
          ‹ffold_init ct a c = ffold (init ct) a c›
declare ffold_init_def [simp,solidity_symbex]

lemma ffold_init_code [code]:
     ‹ffold_init ct a c = fold (init ct) (remdups (sorted_list_of_set (fset c))) a›
  using  comp_fun_commute_on.fold_set_fold_remdups ffold.rep_eq 
            ffold_init_def init_commte sorted_list_of_fset.rep_eq 
            sorted_list_of_fset_simps(1)
  by (metis comp_fun_commute.comp_fun_commute comp_fun_commute_on.intro order_refl)

lemma bind_case_stackvalue_cong [fundef_cong]:
  assumes "x = x'"
      and "⋀v. x = KValue v ⟹ f v s = f' v s"
      and "⋀p. x = KCDptr p ⟹ g p s = g' p s"
      and "⋀p. x = KMemptr p ⟹ h p s = h' p s"
      and "⋀p. x = KStoptr p ⟹ i p s = i' p s"
    shows "(case x of KValue v ⇒ f v | KCDptr p ⇒ g p | KMemptr p ⇒ h p | KStoptr p ⇒ i p) s
         = (case x' of KValue v ⇒ f' v | KCDptr p ⇒ g' p | KMemptr p ⇒ h' p | KStoptr p ⇒ i' p) s"
  using assms by (cases x, auto)

lemma bind_case_type_cong [fundef_cong]:
  assumes "x = x'"
      and "⋀t. x = Value t ⟹ f t s = f' t s"
      and "⋀t. x = Calldata t ⟹ g t s = g' t s"
      and "⋀t. x = type.Memory t ⟹ h t s = h' t s"
      and "⋀t. x = type.Storage t ⟹ i t s = i' t s"
    shows "(case x of Value t ⇒ f t | Calldata t ⇒ g t | type.Memory t ⇒ h t | type.Storage t ⇒ i t ) s
         = (case x' of Value t ⇒ f' t | Calldata t ⇒ g' t | type.Memory t ⇒ h' t | type.Storage t ⇒ i' t) s"
  using assms by (cases x, auto)

lemma bind_case_denvalue_cong [fundef_cong]:
  assumes "x = x'"
      and "⋀a. x = (Stackloc a) ⟹ f a s = f' a s"
      and "⋀a. x = (Storeloc a) ⟹ g a s = g' a s"
    shows "(case x of (Stackloc a) ⇒ f a | (Storeloc a) ⇒ g a) s
         = (case x' of (Stackloc a) ⇒ f' a | (Storeloc a) ⇒ g' a) s"
  using assms by (cases x, auto)

lemma bind_case_mtypes_cong [fundef_cong]:
  assumes "x = x'"
      and "⋀a t. x = (MTArray a t) ⟹ f a t s = f' a t s"
      and "⋀p. x = (MTValue p) ⟹ g p s = g' p s"
    shows "(case x of (MTArray a t) ⇒ f a t | (MTValue p) ⇒ g p) s
         = (case x' of (MTArray a t) ⇒ f' a t | (MTValue p) ⇒ g' p) s"
  using assms by (cases x, auto)

lemma bind_case_stypes_cong [fundef_cong]:
  assumes "x = x'"
      and "⋀a t. x = (STArray a t) ⟹ f a t s = f' a t s"
      and "⋀a t. x = (STMap a t) ⟹ g a t s = g' a t s"
      and "⋀p. x = (STValue p) ⟹ h p s = h' p s"
    shows "(case x of (STArray a t) ⇒ f a t | (STMap a t) ⇒ g a t | (STValue p) ⇒ h p) s
         = (case x' of (STArray a t) ⇒ f' a t | (STMap a t) ⇒ g' a t | (STValue p) ⇒ h' p) s"
  using assms by (cases x, auto)

lemma bind_case_types_cong [fundef_cong]:
  assumes "x = x'"
      and "⋀a. x = (TSInt a) ⟹ f a s = f' a s"
      and "⋀a. x = (TUInt a) ⟹ g a s = g' a s"
      and "x = TBool ⟹ h s = h' s"
      and "x = TAddr ⟹ i s = i' s"
    shows "(case x of (TSInt a) ⇒ f a | (TUInt a) ⇒ g a | TBool ⇒ h | TAddr ⇒ i) s
         = (case x' of (TSInt a) ⇒ f' a | (TUInt a) ⇒ g' a | TBool ⇒ h' | TAddr ⇒ i') s"
  using assms by (cases x, auto)

lemma bind_case_contract_cong [fundef_cong]:
  assumes "x = x'"
      and "⋀a. x = Method a ⟹ f a s = f' a s"
      and "⋀a. x = Function a ⟹ g a s = g' a s"
      and "⋀a. x = Var a ⟹ h a s = h' a s"
    shows "(case x of Method a ⇒ f a | Function a ⇒ g a | Var a ⇒ h a) s
         = (case x' of Method a ⇒ f' a | Function a ⇒ g' a | Var a ⇒ h' a) s"
  using assms by (cases x, auto)

lemma bind_case_memoryvalue_cong [fundef_cong]:
  assumes "x = x'"
      and "⋀a. x = MValue a ⟹ f a s = f' a s"
      and "⋀a. x = MPointer a ⟹ g a s = g' a s"
    shows "(case x of (MValue a) ⇒ f a | (MPointer a) ⇒ g a) s
         = (case x' of (MValue a) ⇒ f' a | (MPointer a) ⇒ g' a) s"
  using assms by (cases x, auto)

end