Theory UML_Contracts

(*****************************************************************************
 * Featherweight-OCL --- A Formal Semantics for UML-OCL Version OCL 2.5
 *                       for the OMG Standard.
 *                       http://www.brucker.ch/projects/hol-testgen/
 *
 * UML_Contracts.thy ---
 * This file is part of HOL-TestGen.
 *
 * Copyright (c) 2013-2015 Université Paris-Saclay, Univ. Paris-Sud, France
 *               2013-2015 IRT SystemX, France
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are
 * met:
 *
 *     * Redistributions of source code must retain the above copyright
 *       notice, this list of conditions and the following disclaimer.
 *
 *     * Redistributions in binary form must reproduce the above
 *       copyright notice, this list of conditions and the following
 *       disclaimer in the documentation and/or other materials provided
 *       with the distribution.
 *
 *     * Neither the name of the copyright holders nor the names of its
 *       contributors may be used to endorse or promote products derived
 *       from this software without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
 * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
 * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
 * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
 * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
 * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
 * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
 * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
 * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 ******************************************************************************)

theory UML_Contracts
imports UML_State
begin

text‹Modeling of an operation contract for an operation  with 2 arguments,
       (so depending on three parameters if one takes "self" into account).›

locale contract_scheme =
   fixes f_υ
   fixes f_lam
   fixes f   :: "('𝔄,'α0::null)val ⇒ 
                 'b ⇒
                  ('𝔄,'res::null)val"
   fixes PRE
   fixes POST
   assumes def_scheme': "f self x ≡  (λ τ. SOME res. let res = λ _. res in
                                           if (τ ⊨ (δ self)) ∧ f_υ x τ
                                           then (τ ⊨ PRE self x) ∧
                                                (τ ⊨ POST self x res)
                                           else τ ⊨ res ≜ invalid)"
   assumes all_post': "∀ σ σ' σ''. ((σ,σ') ⊨ PRE self x) = ((σ,σ'') ⊨ PRE self x)"
           (* PRE is really a pre-condition semantically,
              i.e. it does not depend on the post-state. ... *)
   assumes cp⇩P⇩R⇩E': "PRE (self) x τ = PRE (λ _. self τ) (f_lam x τ) τ "
           (* this interface is preferable than :
              assumes "cp self' ⟹ cp a1' ⟹ cp a2' ⟹ cp (λX. PRE (self' X) (a1' X) (a2' X) )"
              which is too polymorphic. *)
   assumes cp⇩P⇩O⇩S⇩T':"POST (self) x (res) τ = POST (λ _. self τ) (f_lam x τ) (λ _. res τ) τ"
   assumes f_υ_val: "⋀a1. f_υ (f_lam a1 τ) τ = f_υ a1 τ"
begin  
   lemma strict0 [simp]: "f invalid X = invalid"
   by(rule ext, rename_tac "τ", simp add: def_scheme' StrongEq_def OclValid_def false_def true_def)

   lemma nullstrict0[simp]: "f null X = invalid"
   by(rule ext, rename_tac "τ", simp add: def_scheme' StrongEq_def OclValid_def false_def true_def)
    
   lemma cp0 : "f self a1 τ = f (λ _. self τ) (f_lam a1 τ) τ"
   proof -
      have A: "(τ ⊨ δ (λ_. self τ)) = (τ ⊨ δ self)" by(simp add: OclValid_def cp_defined[symmetric])
      have B: "f_υ (f_lam a1 τ) τ = f_υ a1 τ" by (rule f_υ_val)
      have D: "(τ ⊨ PRE (λ_. self τ) (f_lam a1 τ)) = ( τ ⊨ PRE self a1 )"
                                                 by(simp add: OclValid_def cp⇩P⇩R⇩E'[symmetric])
      show ?thesis
        apply(auto simp: def_scheme' A B D)
        apply(simp add: OclValid_def)
        by(subst cp⇩P⇩O⇩S⇩T', simp)
      qed

   theorem unfold' : 
      assumes context_ok:    "cp E"
      and args_def_or_valid: "(τ ⊨ δ self) ∧ f_υ a1 τ"
      and pre_satisfied:     "τ ⊨ PRE self a1"
      and post_satisfiable:  " ∃res. (τ ⊨ POST self a1 (λ _. res))"
      and sat_for_sols_post: "(⋀res. τ ⊨ POST self a1 (λ _. res)  ⟹ τ ⊨ E (λ _. res))"
      shows                  "τ ⊨ E(f self a1)"
   proof -  
      have cp0: "⋀ X τ. E X τ = E (λ_. X τ) τ" by(insert context_ok[simplified cp_def], auto)
      show ?thesis
         apply(simp add: OclValid_def, subst cp0, fold OclValid_def)
         apply(simp add:def_scheme' args_def_or_valid pre_satisfied)
         apply(insert post_satisfiable, elim exE)
         apply(rule Hilbert_Choice.someI2, assumption)
         by(rule sat_for_sols_post, simp)
   qed
   
   lemma unfold2' :
      assumes context_ok:      "cp E"
      and args_def_or_valid:   "(τ ⊨ δ self) ∧ (f_υ a1 τ)"
      and pre_satisfied:       "τ ⊨ PRE self a1"
      and postsplit_satisfied: "τ ⊨ POST' self a1" (* split constraint holds on post-state *)
      and post_decomposable  : "⋀ res. (POST self a1 res) = 
                                       ((POST' self a1)  and (res ≜ (BODY self a1)))"
      shows "(τ ⊨ E(f self a1)) = (τ ⊨ E(BODY self a1))"
   proof -
      have cp0: "⋀ X τ. E X τ = E (λ_. X τ) τ" by(insert context_ok[simplified cp_def], auto)
      show ?thesis
         apply(simp add: OclValid_def, subst cp0, fold OclValid_def)      
         apply(simp add:def_scheme' args_def_or_valid pre_satisfied 
                        post_decomposable postsplit_satisfied foundation10')
         apply(subst some_equality)
         apply(simp add: OclValid_def StrongEq_def true_def)+
         by(subst (2) cp0, rule refl)
   qed
end


locale contract0 =
   fixes f   :: "('𝔄,'α0::null)val ⇒            
                  ('𝔄,'res::null)val"
   fixes PRE
   fixes POST
   assumes def_scheme: "f self ≡  (λ τ. SOME res. let res = λ _. res in
                                        if (τ ⊨ (δ self))
                                        then (τ ⊨ PRE self) ∧
                                             (τ ⊨ POST self res)
                                        else τ ⊨ res ≜ invalid)"
   assumes all_post: "∀ σ σ' σ''. ((σ,σ') ⊨ PRE self) = ((σ,σ'') ⊨ PRE self)"
           (* PRE is really a pre-condition semantically,
              i.e. it does not depend on the post-state. ... *)
   assumes cp⇩P⇩R⇩E: "PRE (self)  τ = PRE (λ _. self τ) τ "
           (* this interface is preferable than :
              assumes "cp self' ⟹ cp a1' ⟹ cp a2' ⟹ cp (λX. PRE (self' X) (a1' X) (a2' X) )"
              which is too polymorphic. *)
   assumes cp⇩P⇩O⇩S⇩T:"POST (self) (res) τ = POST (λ _. self τ) (λ _. res τ) τ"

sublocale contract0 < contract_scheme "λ_ _. True" "λx _. x" "λx _. f x" "λx _. PRE x" "λx _. POST x"
 apply(unfold_locales)
     apply(simp add: def_scheme, rule all_post, rule cp⇩P⇩R⇩E, rule cp⇩P⇩O⇩S⇩T)
by simp

context contract0
begin
   lemma cp_pre: "cp self' ⟹  cp (λX. PRE (self' X)  )"
   by(rule_tac f=PRE in cpI1, auto intro: cp⇩P⇩R⇩E)
  
   lemma cp_post: "cp self' ⟹ cp res'  ⟹ cp (λX. POST (self' X) (res' X))"
   by(rule_tac f=POST in cpI2, auto intro: cp⇩P⇩O⇩S⇩T)  

   lemma cp [simp]:  "cp self' ⟹  cp res' ⟹ cp (λX. f (self' X) )"
      by(rule_tac f=f in cpI1, auto intro:cp0)  

   lemmas unfold = unfold'[simplified]

   lemma unfold2 :
      assumes                  "cp E"
      and                      "(τ ⊨ δ self)"
      and                      "τ ⊨ PRE self"
      and                      "τ ⊨ POST' self" (* split constraint holds on post-state *)
      and                      "⋀ res. (POST self res) = 
                                       ((POST' self)  and (res ≜ (BODY self)))"
      shows "(τ ⊨ E(f self)) = (τ ⊨ E(BODY self))"
        apply(rule unfold2'[simplified])
      by((rule assms)+)

end

locale contract1 =
   fixes f   :: "('𝔄,'α0::null)val ⇒            
                  ('𝔄,'α1::null)val ⇒ 
                  ('𝔄,'res::null)val"
   fixes PRE
   fixes POST 
   assumes def_scheme: "f self a1 ≡ 
                               (λ τ. SOME res. let res = λ _. res in
                                     if (τ ⊨ (δ self)) ∧  (τ ⊨ υ a1)
                                     then (τ ⊨ PRE self a1) ∧
                                          (τ ⊨ POST self a1 res)
                                     else τ ⊨ res ≜ invalid) "
   assumes all_post: "∀ σ σ' σ''.  ((σ,σ') ⊨ PRE self a1) = ((σ,σ'') ⊨ PRE self a1)"
           (* PRE is really a pre-condition semantically,
              i.e. it does not depend on the post-state. ... *)
   assumes cp⇩P⇩R⇩E: "PRE (self) (a1)  τ = PRE (λ _. self τ) (λ _. a1 τ) τ "
           (* this interface is preferable than :
              assumes "cp self' ⟹ cp a1' ⟹ cp a2' ⟹ cp (λX. PRE (self' X) (a1' X) (a2' X) )"
              which is too polymorphic. *)
   assumes cp⇩P⇩O⇩S⇩T:"POST (self) (a1) (res) τ = POST (λ _. self τ)(λ _. a1 τ) (λ _. res τ) τ"

sublocale contract1 < contract_scheme "λa1 τ. (τ ⊨ υ a1)" "λa1 τ. (λ _. a1 τ)"
 apply(unfold_locales)
     apply(rule def_scheme, rule all_post, rule cp⇩P⇩R⇩E, rule cp⇩P⇩O⇩S⇩T)
by(simp add: OclValid_def cp_valid[symmetric])

context contract1
begin
   lemma strict1[simp]: "f self invalid = invalid"
   by(rule ext, rename_tac "τ", simp add: def_scheme StrongEq_def OclValid_def false_def true_def)

   lemma defined_mono : "τ ⊨υ(f Y Z) ⟹ (τ ⊨δ Y) ∧ (τ ⊨υ Z)"
   by(auto simp: valid_def bot_fun_def invalid_def 
                 def_scheme StrongEq_def OclValid_def false_def true_def
           split: if_split_asm)
   
   lemma cp_pre: "cp self' ⟹ cp a1' ⟹  cp (λX. PRE (self' X) (a1' X)  )"
   by(rule_tac f=PRE in cpI2, auto intro: cp⇩P⇩R⇩E)
     
   lemma cp_post: "cp self' ⟹ cp a1' ⟹ cp res'
                   ⟹ cp (λX. POST (self' X) (a1' X) (res' X))"
   by(rule_tac f=POST in cpI3, auto intro: cp⇩P⇩O⇩S⇩T)  
      
   lemma cp [simp]:  "cp self' ⟹ cp a1' ⟹  cp res' ⟹ cp (λX. f (self' X) (a1' X))"
      by(rule_tac f=f in cpI2, auto intro:cp0)  

   lemmas unfold = unfold'
   lemmas unfold2 = unfold2'
end

locale contract2 =
   fixes f   :: "('𝔄,'α0::null)val ⇒            
                  ('𝔄,'α1::null)val ⇒ ('𝔄,'α2::null)val ⇒
                  ('𝔄,'res::null)val"
   fixes PRE 
   fixes POST 
   assumes def_scheme: "f self a1 a2 ≡ 
                               (λ τ. SOME res. let res = λ _. res in
                                     if (τ ⊨ (δ self)) ∧  (τ ⊨ υ a1) ∧  (τ ⊨ υ a2)
                                     then (τ ⊨ PRE self a1 a2) ∧
                                          (τ ⊨ POST self a1 a2 res)
                                     else τ ⊨ res ≜ invalid) "
   assumes all_post: "∀ σ σ' σ''.  ((σ,σ') ⊨ PRE self a1 a2) = ((σ,σ'') ⊨ PRE self a1 a2)"
           (* PRE is really a pre-condition semantically,
              i.e. it does not depend on the post-state. ... *)
   assumes cp⇩P⇩R⇩E: "PRE (self) (a1) (a2) τ = PRE (λ _. self τ) (λ _. a1 τ) (λ _. a2 τ) τ "
           (* this interface is preferable than :
              assumes "cp self' ⟹ cp a1' ⟹ cp a2' ⟹ cp (λX. PRE (self' X) (a1' X) (a2' X) )"
              which is too polymorphic. *)
   assumes cp⇩P⇩O⇩S⇩T:"⋀res. POST (self) (a1) (a2) (res) τ = 
                         POST (λ _. self τ)(λ _. a1 τ)(λ _. a2 τ) (λ _. res τ) τ"


sublocale contract2 < contract_scheme "λ(a1,a2) τ. (τ ⊨ υ a1) ∧ (τ ⊨ υ a2)" 
                                      "λ(a1,a2) τ. (λ _.a1 τ, λ _.a2 τ)"
                                      "(λx (a,b). f x a b)"
                                      "(λx (a,b). PRE x a b)"
                                      "(λx (a,b). POST x a b)"
 apply(unfold_locales)
     apply(auto simp add: def_scheme)
        apply (metis all_post, metis all_post)
      apply(subst cp⇩P⇩R⇩E, simp)
     apply(subst cp⇩P⇩O⇩S⇩T, simp)
by(simp_all add: OclValid_def cp_valid[symmetric])

context contract2
begin
   lemma strict0'[simp] : "f invalid X Y = invalid"
   by(insert strict0[of "(X,Y)"], simp)

   lemma nullstrict0'[simp]: "f null X Y = invalid"
   by(insert nullstrict0[of "(X,Y)"], simp)

   lemma strict1[simp]: "f self invalid Y = invalid"
   by(rule ext, rename_tac "τ", simp add: def_scheme StrongEq_def OclValid_def false_def true_def)

   lemma strict2[simp]: "f self X invalid = invalid"
   by(rule ext, rename_tac "τ", simp add: def_scheme StrongEq_def OclValid_def false_def true_def)
   
   lemma defined_mono : "τ ⊨υ(f X Y Z) ⟹ (τ ⊨δ X) ∧ (τ ⊨υ Y) ∧ (τ ⊨υ Z)"
   by(auto simp: valid_def bot_fun_def invalid_def 
                 def_scheme StrongEq_def OclValid_def false_def true_def
           split: if_split_asm)
   
   lemma cp_pre: "cp self' ⟹ cp a1' ⟹ cp a2' ⟹ cp (λX. PRE (self' X) (a1' X) (a2' X) )"
   by(rule_tac f=PRE in cpI3, auto intro: cp⇩P⇩R⇩E)
  
   lemma cp_post: "cp self' ⟹ cp a1' ⟹ cp a2' ⟹ cp res'
                   ⟹ cp (λX. POST (self' X) (a1' X) (a2' X) (res' X))"
   by(rule_tac f=POST in cpI4, auto intro: cp⇩P⇩O⇩S⇩T)  
   
   lemma cp0' : "f self a1 a2 τ = f (λ _. self τ) (λ _. a1 τ) (λ _. a2 τ) τ"
   by (rule cp0[of _ "(a1,a2)", simplified])
      
   lemma cp [simp]:  "cp self' ⟹ cp a1' ⟹ cp a2' ⟹ cp res'
                       ⟹ cp (λX. f (self' X) (a1' X) (a2' X))"
      by(rule_tac f=f in cpI3, auto intro:cp0')  

   theorem unfold : 
      assumes                "cp E"
      and                    "(τ ⊨ δ self) ∧ (τ ⊨ υ a1) ∧  (τ ⊨ υ a2)"
      and                    "τ ⊨ PRE self a1 a2"
      and                    " ∃res. (τ ⊨ POST self a1 a2 (λ _. res))"
      and                    "(⋀res. τ ⊨ POST self a1 a2 (λ _. res)  ⟹ τ ⊨ E (λ _. res))"
      shows                  "τ ⊨ E(f self a1 a2)"
      apply(rule unfold'[of _ _ _ "(a1, a2)", simplified])
      by((rule assms)+)

   lemma unfold2 :
      assumes                  "cp E"
      and                      "(τ ⊨ δ self) ∧ (τ ⊨ υ a1) ∧  (τ ⊨ υ a2)"
      and                      "τ ⊨ PRE self a1 a2"
      and                      "τ ⊨ POST' self a1 a2" (* split constraint holds on post-state *)
      and                      "⋀ res. (POST self a1 a2 res) = 
                                       ((POST' self a1 a2)  and (res ≜ (BODY self a1 a2)))"
      shows "(τ ⊨ E(f self a1 a2)) = (τ ⊨ E(BODY self a1 a2))"
      apply(rule unfold2'[of _ _ _ "(a1, a2)", simplified])
      by((rule assms)+)
end

locale contract3 =
   fixes f   :: "('𝔄,'α0::null)val ⇒            
                  ('𝔄,'α1::null)val ⇒ 
                  ('𝔄,'α2::null)val ⇒
                  ('𝔄,'α3::null)val ⇒
                  ('𝔄,'res::null)val"
   fixes PRE 
   fixes POST 
   assumes def_scheme: "f self a1 a2 a3 ≡ 
                               (λ τ. SOME res. let res = λ _. res in
                                     if (τ ⊨ (δ self)) ∧  (τ ⊨ υ a1) ∧  (τ ⊨ υ a2) ∧  (τ ⊨ υ a3)
                                     then (τ ⊨ PRE self a1 a2 a3) ∧
                                          (τ ⊨ POST self a1 a2 a3 res)
                                     else τ ⊨ res ≜ invalid) "
   assumes all_post: "∀ σ σ' σ''.  ((σ,σ') ⊨ PRE self a1 a2 a3) = ((σ,σ'') ⊨ PRE self a1 a2 a3)"
           (* PRE is really a pre-condition semantically,
              i.e. it does not depend on the post-state. ... *)
   assumes cp⇩P⇩R⇩E: "PRE (self) (a1) (a2) (a3) τ = PRE (λ _. self τ) (λ _. a1 τ) (λ _. a2 τ) (λ _. a3 τ) τ "
           (* this interface is preferable than :
              assumes "cp self' ⟹ cp a1' ⟹ cp a2' ⟹ cp a3' ⟹ cp (λX. PRE (self' X) (a1' X) (a2' X) (a3' X) )"
              which is too polymorphic. *)
   assumes cp⇩P⇩O⇩S⇩T:"⋀res. POST (self) (a1) (a2) (a3) (res) τ = 
                         POST (λ _. self τ)(λ _. a1 τ)(λ _. a2 τ)(λ _. a3 τ) (λ _. res τ) τ"


sublocale contract3 < contract_scheme "λ(a1,a2,a3) τ. (τ ⊨ υ a1) ∧ (τ ⊨ υ a2)∧ (τ ⊨ υ a3)" 
                                      "λ(a1,a2,a3) τ. (λ _.a1 τ, λ _.a2 τ, λ _.a3 τ)"
                                      "(λx (a,b,c). f x a b c)"
                                      "(λx (a,b,c). PRE x a b c)"
                                      "(λx (a,b,c). POST x a b c)"
 apply(unfold_locales)
     apply(auto simp add: def_scheme)
        apply (metis all_post, metis all_post)
      apply(subst cp⇩P⇩R⇩E, simp)
     apply(subst cp⇩P⇩O⇩S⇩T, simp)
by(simp_all add: OclValid_def cp_valid[symmetric])

context contract3
begin
   lemma strict0'[simp] : "f invalid X Y Z = invalid"
   by(rule ext, rename_tac "τ", simp add: def_scheme StrongEq_def OclValid_def false_def true_def)

   lemma nullstrict0'[simp]: "f null X Y Z = invalid"
   by(rule ext, rename_tac "τ", simp add: def_scheme StrongEq_def OclValid_def false_def true_def)

   lemma strict1[simp]: "f self invalid Y Z = invalid"
   by(rule ext, rename_tac "τ", simp add: def_scheme StrongEq_def OclValid_def false_def true_def)

   lemma strict2[simp]: "f self X invalid Z = invalid"
   by(rule ext, rename_tac "τ", simp add: def_scheme StrongEq_def OclValid_def false_def true_def)

   lemma defined_mono : "τ ⊨υ(f W X Y Z) ⟹ (τ ⊨δ W) ∧ (τ ⊨υ X) ∧ (τ ⊨υ Y) ∧ (τ ⊨υ Z)"
   by(auto simp: valid_def bot_fun_def invalid_def 
                 def_scheme StrongEq_def OclValid_def false_def true_def
           split: if_split_asm)
   
   lemma cp_pre: "cp self' ⟹ cp a1' ⟹ cp a2'⟹ cp a3' 
                  ⟹ cp (λX. PRE (self' X) (a1' X) (a2' X) (a3' X) )"
   by(rule_tac f=PRE in cpI4, auto intro: cp⇩P⇩R⇩E)
  
   lemma cp_post: "cp self' ⟹ cp a1' ⟹ cp a2' ⟹ cp a3' ⟹ cp res'
                   ⟹ cp (λX. POST (self' X) (a1' X) (a2' X) (a3' X)  (res' X))"
   by(rule_tac f=POST in cpI5, auto intro: cp⇩P⇩O⇩S⇩T)  
   
   lemma cp0' : "f self a1 a2 a3 τ = f (λ _. self τ) (λ _. a1 τ) (λ _. a2 τ) (λ _. a3 τ) τ"
   by (rule cp0[of _ "(a1,a2,a3)", simplified])
      
   lemma cp [simp]:  "cp self' ⟹ cp a1' ⟹ cp a2' ⟹ cp a3' ⟹ cp res'
                       ⟹ cp (λX. f (self' X) (a1' X) (a2' X) (a3' X))"
      by(rule_tac f=f in cpI4, auto intro:cp0')  

   theorem unfold : 
      assumes                "cp E"
      and                    "(τ ⊨ δ self) ∧ (τ ⊨ υ a1) ∧  (τ ⊨ υ a2) ∧  (τ ⊨ υ a3)"
      and                    "τ ⊨ PRE self a1 a2 a3"
      and                    " ∃res. (τ ⊨ POST self a1 a2 a3 (λ _. res))"
      and                    "(⋀res. τ ⊨ POST self a1 a2 a3 (λ _. res)  ⟹ τ ⊨ E (λ _. res))"
      shows                  "τ ⊨ E(f self a1 a2 a3)"
      apply(rule unfold'[of _ _ _ "(a1, a2, a3)", simplified])
      by((rule assms)+)

   lemma unfold2 :
      assumes                  "cp E"
      and                      "(τ ⊨ δ self) ∧ (τ ⊨ υ a1) ∧  (τ ⊨ υ a2) ∧  (τ ⊨ υ a3)"
      and                      "τ ⊨ PRE self a1 a2 a3"
      and                      "τ ⊨ POST' self a1 a2 a3" (* split constraint holds on post-state *)
      and                      "⋀ res. (POST self a1 a2 a3 res) = 
                                       ((POST' self a1 a2 a3)  and (res ≜ (BODY self a1 a2 a3)))"
      shows "(τ ⊨ E(f self a1 a2 a3)) = (τ ⊨ E(BODY self a1 a2 a3))"
      apply(rule unfold2'[of _ _ _ "(a1, a2, a3)", simplified])
      by((rule assms)+)
end


end