From 98df20394520ff0421cd335ebda20ee950413b17 Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Sat, 22 Jun 2019 23:44:04 +0100 Subject: [PATCH] Import of official AFP entry for Isabelle 2019. --- .ci/Jenkinsfile | 2 +- Featherweight_OCL/ROOT | 2 +- Featherweight_OCL/UML_Contracts.thy | 4 +- Featherweight_OCL/UML_Library.thy | 30 +-- Featherweight_OCL/UML_Logic.thy | 152 +++++------ Featherweight_OCL/UML_PropertyProfiles.thy | 18 +- Featherweight_OCL/UML_State.thy | 132 ++++----- Featherweight_OCL/UML_Tools.thy | 4 +- Featherweight_OCL/UML_Types.thy | 252 +++++++++--------- Featherweight_OCL/basic_types/UML_Boolean.thy | 26 +- Featherweight_OCL/basic_types/UML_Integer.thy | 56 ++-- Featherweight_OCL/basic_types/UML_Real.thy | 56 ++-- Featherweight_OCL/basic_types/UML_String.thy | 50 ++-- Featherweight_OCL/basic_types/UML_Void.thy | 22 +- .../collection_types/UML_Bag.thy | 174 ++++++------ .../collection_types/UML_Pair.thy | 32 +-- .../collection_types/UML_Sequence.thy | 92 +++---- .../collection_types/UML_Set.thy | 228 ++++++++-------- Featherweight_OCL/document/root.bib | 4 +- Featherweight_OCL/document/root.tex | 2 +- .../Employee_Model/Analysis/Analysis_OCL.thy | 50 ++-- .../Employee_Model/Analysis/Analysis_UML.thy | 158 +++++------ .../Employee_Model/Design/Design_OCL.thy | 18 +- .../Employee_Model/Design/Design_UML.thy | 142 +++++----- 24 files changed, 853 insertions(+), 853 deletions(-) diff --git a/.ci/Jenkinsfile b/.ci/Jenkinsfile index 793446c..a6eea6e 100644 --- a/.ci/Jenkinsfile +++ b/.ci/Jenkinsfile @@ -3,7 +3,7 @@ pipeline { stages { stage('Build') { steps { - sh 'docker run -v $PWD/Featherweight_OCL:/Featherweight_OCL logicalhacking:isabelle2018 isabelle build -D /Featherweight_OCL' + sh 'docker run -v $PWD/Featherweight_OCL:/Featherweight_OCL logicalhacking:isabelle2019 isabelle build -D /Featherweight_OCL' } } } diff --git a/Featherweight_OCL/ROOT b/Featherweight_OCL/ROOT index 3ef4b7d..11a7306 100644 --- a/Featherweight_OCL/ROOT +++ b/Featherweight_OCL/ROOT @@ -1,7 +1,7 @@ chapter AFP session "Featherweight_OCL-devel" (AFP) = HOL + - description {* Featherweight-OCL *} + description "Featherweight-OCL" options [document_variants = "annex-a=annexa,-theory,-afp,-proof,-ML:document=afp,-annexa:outline=-annexa,afp,/proof,/ML", show_question_marks = false, timeout = 600] theories diff --git a/Featherweight_OCL/UML_Contracts.thy b/Featherweight_OCL/UML_Contracts.thy index 65344bc..34d52cd 100644 --- a/Featherweight_OCL/UML_Contracts.thy +++ b/Featherweight_OCL/UML_Contracts.thy @@ -44,8 +44,8 @@ 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). *} +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_\ diff --git a/Featherweight_OCL/UML_Library.thy b/Featherweight_OCL/UML_Library.thy index 6912a09..e5309b5 100644 --- a/Featherweight_OCL/UML_Library.thy +++ b/Featherweight_OCL/UML_Library.thy @@ -56,9 +56,9 @@ imports (* Basic Type Operations *) "collection_types/UML_Sequence" begin -section{* Miscellaneous Stuff*} +section\Miscellaneous Stuff\ -subsection{* Definition: asBoolean *} +subsection\Definition: asBoolean\ definition OclAsBoolean\<^sub>I\<^sub>n\<^sub>t :: "('\) Integer \ ('\) Boolean" ("(_)->oclAsType\<^sub>I\<^sub>n\<^sub>t'(Boolean')") where "OclAsBoolean\<^sub>I\<^sub>n\<^sub>t X = (\\. if (\ X) \ = true \ @@ -76,7 +76,7 @@ where "OclAsBoolean\<^sub>R\<^sub>e\<^sub>a\<^sub>l X = (\\. if interpretation OclAsBoolean\<^sub>R\<^sub>e\<^sub>a\<^sub>l : profile_mono\<^sub>d OclAsBoolean\<^sub>R\<^sub>e\<^sub>a\<^sub>l "\x. \\\\x\\ \ 0\\" by unfold_locales (auto simp: OclAsBoolean\<^sub>R\<^sub>e\<^sub>a\<^sub>l_def bot_option_def) -subsection{* Definition: asInteger *} +subsection\Definition: asInteger\ definition OclAsInteger\<^sub>R\<^sub>e\<^sub>a\<^sub>l :: "('\) Real \ ('\) Integer" ("(_)->oclAsType\<^sub>R\<^sub>e\<^sub>a\<^sub>l'(Integer')") where "OclAsInteger\<^sub>R\<^sub>e\<^sub>a\<^sub>l X = (\\. if (\ X) \ = true \ @@ -86,7 +86,7 @@ where "OclAsInteger\<^sub>R\<^sub>e\<^sub>a\<^sub>l X = (\\. if interpretation OclAsInteger\<^sub>R\<^sub>e\<^sub>a\<^sub>l : profile_mono\<^sub>d OclAsInteger\<^sub>R\<^sub>e\<^sub>a\<^sub>l "\x. \\floor \\x\\\\" by unfold_locales (auto simp: OclAsInteger\<^sub>R\<^sub>e\<^sub>a\<^sub>l_def bot_option_def) -subsection{* Definition: asReal *} +subsection\Definition: asReal\ definition OclAsReal\<^sub>I\<^sub>n\<^sub>t :: "('\) Integer \ ('\) Real" ("(_)->oclAsType\<^sub>I\<^sub>n\<^sub>t'(Real')") where "OclAsReal\<^sub>I\<^sub>n\<^sub>t X = (\\. if (\ X) \ = true \ @@ -103,7 +103,7 @@ lemma Integer_subtype_of_Real: apply(subst (2 4) cp_defined, simp add: true_def) by (metis assms bot_option_def drop.elims foundation16 null_option_def) -subsection{* Definition: asPair *} +subsection\Definition: asPair\ definition OclAsPair\<^sub>S\<^sub>e\<^sub>q :: "[('\,'\::null)Sequence]\('\,'\::null,'\::null) Pair" ("(_)->asPair\<^sub>S\<^sub>e\<^sub>q'(')") where "OclAsPair\<^sub>S\<^sub>e\<^sub>q S = (if S->size\<^sub>S\<^sub>e\<^sub>q() \ \ @@ -125,7 +125,7 @@ where "OclAsPair\<^sub>B\<^sub>a\<^sub>g S = (if S->size\<^sub>B\<^sub>a\<^s else invalid endif)" -subsection{* Definition: asSet *} +subsection\Definition: asSet\ definition OclAsSet\<^sub>S\<^sub>e\<^sub>q :: "[('\,'\::null)Sequence]\('\,'\)Set" ("(_)->asSet\<^sub>S\<^sub>e\<^sub>q'(')") where "OclAsSet\<^sub>S\<^sub>e\<^sub>q S = (S->iterate\<^sub>S\<^sub>e\<^sub>q(b; x = Set{} | x ->including\<^sub>S\<^sub>e\<^sub>t(b)))" @@ -139,7 +139,7 @@ where "OclAsSet\<^sub>B\<^sub>a\<^sub>g S = (\ \. if (\ else if (\ S) \ = true \ then null \ else invalid \)" -subsection{* Definition: asSequence *} +subsection\Definition: asSequence\ definition OclAsSeq\<^sub>S\<^sub>e\<^sub>t :: "[('\,'\::null)Set]\('\,'\)Sequence" ("(_)->asSequence\<^sub>S\<^sub>e\<^sub>t'(')") where "OclAsSeq\<^sub>S\<^sub>e\<^sub>t S = (S->iterate\<^sub>S\<^sub>e\<^sub>t(b; x = Sequence{} | x ->including\<^sub>S\<^sub>e\<^sub>q(b)))" @@ -150,7 +150,7 @@ where "OclAsSeq\<^sub>B\<^sub>a\<^sub>g S = (S->iterate\<^sub>B\<^sub>a\<^su definition OclAsSeq\<^sub>P\<^sub>a\<^sub>i\<^sub>r :: "[('\,'\::null,'\::null) Pair]\('\,'\)Sequence" ("(_)->asSequence\<^sub>P\<^sub>a\<^sub>i\<^sub>r'(')") where "OclAsSeq\<^sub>P\<^sub>a\<^sub>i\<^sub>r S = Sequence{S .First(), S .Second()}" -subsection{* Definition: asBag *} +subsection\Definition: asBag\ definition OclAsBag\<^sub>S\<^sub>e\<^sub>q :: "[('\,'\::null)Sequence]\('\,'\)Bag" ("(_)->asBag\<^sub>S\<^sub>e\<^sub>q'(')") where "OclAsBag\<^sub>S\<^sub>e\<^sub>q S = (\\. Abs_Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e \\\s. if list_ex ((=) s) \\Rep_Sequence\<^sub>b\<^sub>a\<^sub>s\<^sub>e (S \)\\ then 1 else 0\\)" @@ -165,21 +165,21 @@ oops definition OclAsBag\<^sub>P\<^sub>a\<^sub>i\<^sub>r :: "[('\,'\::null,'\::null) Pair]\('\,'\)Bag" ("(_)->asBag\<^sub>P\<^sub>a\<^sub>i\<^sub>r'(')") where "OclAsBag\<^sub>P\<^sub>a\<^sub>i\<^sub>r S = Bag{S .First(), S .Second()}" -text_raw{* \isatagafp *} -subsection{* Collection Types *} +text_raw\\isatagafp\ +subsection\Collection Types\ lemmas cp_intro'' [intro!,simp,code_unfold] = cp_intro' (* cp_intro''\<^sub>P\<^sub>a\<^sub>i\<^sub>r *) cp_intro''\<^sub>S\<^sub>e\<^sub>t cp_intro''\<^sub>S\<^sub>e\<^sub>q -text_raw{* \endisatagafp *} +text_raw\\endisatagafp\ -subsection{* Test Statements *} +subsection\Test Statements\ lemma syntax_test: "Set{\,\} = (Set{}->including\<^sub>S\<^sub>e\<^sub>t(\)->including\<^sub>S\<^sub>e\<^sub>t(\))" by (rule refl) -text{* Here is an example of a nested collection. *} +text\Here is an example of a nested collection.\ lemma semantic_test2: assumes H:"(Set{\} \ null) = (false::('\)Boolean)" shows "(\::('\)st) \ (Set{Set{\},null}->includes\<^sub>S\<^sub>e\<^sub>t(null))" @@ -207,7 +207,7 @@ done Assert "\ \ (\ <\<^sub>i\<^sub>n\<^sub>t \) and (\ <\<^sub>i\<^sub>n\<^sub>t \) " -text{* Elementary computations on Sets.*} +text\Elementary computations on Sets.\ declare OclSelect_body_def [simp] @@ -248,7 +248,7 @@ Assert "\ \ (Set{null}->reject\<^sub>S\<^sub>e\<^sub>t(x | no lemma "const (Set{Set{\,null}, invalid})" by(simp add: const_ss) -text{* Elementary computations on Sequences.*} +text\Elementary computations on Sequences.\ Assert "\ (\ \ \(invalid::('\,'\::null) Sequence))" Assert "\ \ \(null::('\,'\::null) Sequence)" diff --git a/Featherweight_OCL/UML_Logic.thy b/Featherweight_OCL/UML_Logic.thy index 2d7ef7f..84892a5 100644 --- a/Featherweight_OCL/UML_Logic.thy +++ b/Featherweight_OCL/UML_Logic.thy @@ -40,15 +40,15 @@ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. ******************************************************************************) -chapter{* Formalization II: OCL Terms and Library Operations *} +chapter\Formalization II: OCL Terms and Library Operations\ theory UML_Logic imports UML_Types begin -section{* The Operations of the Boolean Type and the OCL Logic*} +section\The Operations of the Boolean Type and the OCL Logic\ -subsection{* Basic Constants *} +subsection\Basic Constants\ lemma bot_Boolean_def : "(bot::('\)Boolean) = (\ \. \)" by(simp add: bot_fun_def bot_option_def) @@ -86,7 +86,7 @@ by(simp add: Sem_def true_def) lemma textbook_false: "I\false\ \ = \\False\\" by(simp add: Sem_def false_def) -text {* +text \ \begin{table}[htbp] \centering \begin{tabu}{lX[,c,]} @@ -102,12 +102,12 @@ text {* \caption{Basic semantic constant definitions of the logic} \label{tab:sem_basic_constants} \end{table} -*} +\ -subsection{* Validity and Definedness *} +subsection\Validity and Definedness\ -text{* However, this has also the consequence that core concepts like definedness, -validity and even cp have to be redefined on this type class:*} +text\However, this has also the consequence that core concepts like definedness, +validity and even cp have to be redefined on this type class:\ definition valid :: "('\,'a::null)val \ ('\)Boolean" ("\ _" [100]100) where "\ X \ \ \ . if X \ = bot \ then false \ else true \" @@ -124,16 +124,16 @@ lemma valid3[simp]: "\ true = true" lemma valid4[simp]: "\ false = true" by(rule ext,simp add: valid_def bot_fun_def bot_option_def null_is_valid null_fun_def invalid_def true_def false_def) -text_raw{* \isatagafp *} +text_raw\\isatagafp\ lemma cp_valid: "(\ X) \ = (\ (\ _. X \)) \" by(simp add: valid_def) -text_raw{* \endisatagafp *} +text_raw\\endisatagafp\ definition defined :: "('\,'a::null)val \ ('\)Boolean" ("\ _" [100]100) where "\ X \ \ \ . if X \ = bot \ \ X \ = null \ then false \ else true \" -text{* The generalized definitions of invalid and definedness have the same -properties as the old ones : *} +text\The generalized definitions of invalid and definedness have the same +properties as the old ones :\ lemma defined1[simp]: "\ invalid = false" by(rule ext,simp add: defined_def bot_fun_def bot_option_def null_def invalid_def true_def false_def) @@ -162,13 +162,13 @@ lemma valid6[simp]: "\ \ X = true" by(rule ext, auto simp: valid_def defined_def true_def false_def bot_fun_def bot_option_def null_option_def null_fun_def) -text_raw{* \isatagafp *} +text_raw\\isatagafp\ lemma cp_defined:"(\ X)\ = (\ (\ _. X \)) \" by(simp add: defined_def) -text_raw{* \endisatagafp *} +text_raw\\endisatagafp\ -text{* The definitions above for the constants @{const defined} and @{const valid} -can be rewritten into the conventional semantic "textbook" format as follows: *} +text\The definitions above for the constants @{const defined} and @{const valid} +can be rewritten into the conventional semantic "textbook" format as follows:\ lemma textbook_defined: "I\\(X)\ \ = (if I\X\ \ = I\bot\ \ \ I\X\ \ = I\null\ \ then I\false\ \ @@ -181,7 +181,7 @@ lemma textbook_valid: "I\\(X)\ \ = (if I\X by(simp add: Sem_def valid_def) -text {* +text \ \autoref{tab:sem_definedness} and \autoref{tab:alglaws_definedness} summarize the results of this section. \begin{table}[htbp] @@ -214,10 +214,10 @@ summarize the results of this section. \caption{Laws of the basic predicates of the logic.} \label{tab:alglaws_definedness} \end{table} -*} +\ -subsection{* The Equalities of OCL \label{sec:equality}*} -text{* +subsection\The Equalities of OCL \label{sec:equality}\ +text\ The OCL contains a particular version of equality, written in Standard documents \inlineocl+_ = _+ and \inlineocl+_ <> _+ for its negation, which is referred as \emph{weak referential equality} @@ -236,7 +236,7 @@ text{* Standard. The purpose of strong equality is to define and reason over OCL. It is therefore a natural task in Featherweight OCL to formally investigate the somewhat quite complex relationship between - these two. *} text{* Strong equality has two motivations: a + these two.\ text\Strong equality has two motivations: a pragmatic one and a fundamental one. \begin{enumerate} \item The pragmatic reason is fairly simple: users of object-oriented languages want @@ -279,8 +279,8 @@ text{* sub-expression $s$ in a term $P$ by $t$ and we have that the replacement is equal to the original.'' \end{enumerate} -*} -text{* +\ +text\ While weak referential equality is defined to be strict in the OCL standard, we will define strong equality as non-strict. It is quite nasty (but not impossible) to define the logical equality in a @@ -288,31 +288,31 @@ text{* however, whenever references were used, strong equality is needed since references refer to particular states (pre or post), and that they mean the same thing can therefore not be taken for granted. -*} +\ -subsubsection{* Definition *} -text{* +subsubsection\Definition\ +text\ The strict equality on basic types (actually on all types) must be exceptionally defined on @{term "null"}---otherwise the entire concept of null in the language does not make much sense. This is an important exception from the general rule that null arguments---especially if passed as ``self''-argument---lead to invalid results. -*} +\ -text{* +text\ We define strong equality extremely generic, even for types that - contain a @{text "null"} or @{text "\"} element. Strong + contain a \null\ or \\\ element. Strong equality is simply polymorphic in Featherweight OCL, \ie, is defined identical for all types in OCL and HOL. -*} +\ definition StrongEq::"['\ st \ '\,'\ st \ '\] \ ('\)Boolean" (infixl "\" 30) where "X \ Y \ \ \. \\X \ = Y \ \\" -text{* +text\ From this follow already elementary properties like: -*} +\ lemma [simp,code_unfold]: "(true \ false) = false" by(rule ext, auto simp: StrongEq_def) @@ -320,10 +320,10 @@ lemma [simp,code_unfold]: "(false \ true) = false" by(rule ext, auto simp: StrongEq_def) -subsubsection{* Fundamental Predicates on Strong Equality *} +subsubsection\Fundamental Predicates on Strong Equality\ -text{* Equality reasoning in OCL is not humpty dumpty. While strong equality -is clearly an equivalence: *} +text\Equality reasoning in OCL is not humpty dumpty. While strong equality +is clearly an equivalence:\ lemma StrongEq_refl [simp]: "(X \ X) = true" by(rule ext, simp add: null_def invalid_def true_def false_def StrongEq_def) @@ -339,7 +339,7 @@ lemma StrongEq_trans_strong [simp]: apply(drule_tac x=x in fun_cong)+ by auto -text{* +text\ it is only in a limited sense a congruence, at least from the point of view of this semantic theory. The point is that it is only a congruence on OCL expressions, not arbitrary HOL @@ -351,7 +351,7 @@ text{* the sub-expressions, \ie, all sub-expressions inside an OCL expression refer to the same context. Expressed formally, this boils down to: -*} +\ lemma StrongEq_subst : assumes cp: "\X. P(X)\ = P(\ _. X \)\" and eq: "(X \ Y)\ = true \" @@ -375,8 +375,8 @@ lemma valid7[simp]: "\ (X \ Y) = true" lemma cp_StrongEq: "(X \ Y) \ = ((\ _. X \) \ (\ _. Y \)) \" by(simp add: StrongEq_def) -subsection{* Logical Connectives and their Universal Properties *} -text{* +subsection\Logical Connectives and their Universal Properties\ +text\ It is a design goal to give OCL a semantics that is as closely as possible to a ``logical system'' in a known sense; a specification logic where the logical connectives can not be understood other that @@ -397,7 +397,7 @@ text{* Kleene-Logics with @{term "invalid"} as least, @{term "null"} as middle and @{term "true"} resp. @{term "false"} as unrelated top-elements. -*} +\ definition OclNot :: "('\)Boolean \ ('\)Boolean" ("not") @@ -447,16 +447,16 @@ where "X and Y \ (\ \ . case X \ of | \\True\\ \ Y \)" -text{* +text\ Note that @{term "not"} is \emph{not} defined as a strict function; proximity to lattice laws implies that we \emph{need} a definition - of @{term "not"} that satisfies @{text "not(not(x))=x"}. -*} + of @{term "not"} that satisfies \not(not(x))=x\. +\ -text{* +text\ In textbook notation, the logical core constructs @{const "OclNot"} and @{const "OclAnd"} were represented as follows: -*} +\ lemma textbook_OclNot: "I\not(X)\ \ = (case I\X\ \ of \ \ \ | \ \ \ \ \ \ \ @@ -685,7 +685,7 @@ lemma OclImplies_true2[simp]: "(X implies true) = true" lemma OclImplies_false1[simp]:"(false implies X) = true" by(simp add: OclImplies_def) -subsection{* A Standard Logical Calculus for OCL *} +subsection\A Standard Logical Calculus for OCL\ definition OclValid :: "[('\)st, ('\)Boolean] \ bool" ("(1(_)/ \ (_))" 50) where "\ \ P \ ((P \) = true \)" @@ -694,7 +694,7 @@ syntax OclNonValid :: "[('\)st, ('\)Boolean] \ bool" ("(1(_ translations "\ |\ P" == "\(\ \ P)" -subsubsection{* Global vs. Local Judgements*} +subsubsection\Global vs. Local Judgements\ lemma transform1: "P = true \ \ \ P" by(simp add: OclValid_def) @@ -713,9 +713,9 @@ apply(auto simp: false_def true_def defined_def bot_Boolean_def null_Boolean_def split: option.split_asm HOL.if_split_asm) done -text{* However, certain properties (like transitivity) can not +text\However, certain properties (like transitivity) can not be \emph{transformed} from the global level to the local one, - they have to be re-proven on the local level. *} + they have to be re-proven on the local level.\ lemma (*transform3:*) assumes H : "P = true \ Q = true" @@ -725,8 +725,8 @@ apply(rule H[THEN fun_cong]) apply(rule ext) oops -subsubsection{* Local Validity and Meta-logic*} -text{* \label{sec:localVal} *} +subsubsection\Local Validity and Meta-logic\ +text\\label{sec:localVal}\ lemma foundation1[simp]: "\ \ true" by(auto simp: OclValid_def) @@ -784,12 +784,12 @@ by(simp add: OclNot_def OclValid_def true_def false_def valid_def split: option.split option.split_asm) -text{* +text\ Key theorem for the $\delta$-closure: either an expression is - defined, or it can be replaced (substituted via @{text "StrongEq_L_subst2"}; - see below) by @{text invalid} or @{text null}. Strictness-reduction rules will + defined, or it can be replaced (substituted via \StrongEq_L_subst2\; + see below) by \invalid\ or \null\. Strictness-reduction rules will usually reduce these substituted terms drastically. -*} +\ lemma foundation8: @@ -952,7 +952,7 @@ by(simp add: OclOr_def defined_and_I defined_not_I) lemma valid_or_I : "\ \ \ (x) \ \ \ \ (y) \ \ \ \ (x or y)" by(simp add: OclOr_def valid_and_I valid_not_I) -subsubsection{* Local Judgements and Strong Equality *} +subsubsection\Local Judgements and Strong Equality\ lemma StrongEq_L_refl: "\ \ (x \ x)" by(simp add: OclValid_def StrongEq_def) @@ -966,18 +966,18 @@ by(simp add: OclValid_def StrongEq_def true_def) -text{* In order to establish substitutivity (which does not +text\In order to establish substitutivity (which does not hold in general HOL formulas) we introduce the following -predicate that allows for a calculus of the necessary side-conditions.*} +predicate that allows for a calculus of the necessary side-conditions.\ definition cp :: "(('\,'\) val \ ('\,'\) val) \ bool" where "cp P \ (\ f. \ X \. P X \ = f (X \) \)" -text{* The rule of substitutivity in Featherweight OCL holds only +text\The rule of substitutivity in Featherweight OCL holds only for context-passing expressions, \ie those that pass -the context @{text "\"} without changing it. Fortunately, all +the context \\\ without changing it. Fortunately, all operators of the OCL language satisfy this property -(but not all HOL operators).*} +(but not all HOL operators).\ lemma StrongEq_L_subst1: "\ \. cp P \ \ \ (x \ y) \ \ \ (P x \ P y)" by(auto simp: OclValid_def StrongEq_def true_def cp_def) @@ -1055,7 +1055,7 @@ lemma cp_const : "cp(\_. c)" lemma cp_id : "cp(\X. X)" by (simp add: cp_def, fast) -text_raw{* \isatagafp *} +text_raw\\isatagafp\ lemmas cp_intro[intro!,simp,code_unfold] = cp_const @@ -1069,10 +1069,10 @@ lemmas cp_intro[intro!,simp,code_unfold] = cp_StrongEq[THEN allI[THEN allI[THEN allI[THEN cpI2]], of "StrongEq"]] -text_raw{* \endisatagafp *} +text_raw\\endisatagafp\ -subsection{* OCL's if then else endif *} +subsection\OCL's if then else endif\ definition OclIf :: "[('\)Boolean , ('\,'\::null) val, ('\,'\) val] \ ('\,'\) val" ("if (_) then (_) else (_) endif" [10,10,10]50) @@ -1086,12 +1086,12 @@ where "(if C then B\<^sub>1 else B\<^sub>2 endif) = (\ \. if (\1 else B\<^sub>2 endif) \ = (if (\ _. C \) then (\ _. B\<^sub>1 \) else (\ _. B\<^sub>2 \) endif) \)" by(simp only: OclIf_def, subst cp_defined, rule refl) -text_raw{* \isatagafp *} +text_raw\\isatagafp\ lemmas cp_intro'[intro!,simp,code_unfold] = cp_intro cp_OclIf[THEN allI[THEN allI[THEN allI[THEN allI[THEN cpI3]]], of "OclIf"]] -text_raw{* \endisatagafp *} +text_raw\\endisatagafp\ lemma OclIf_invalid [simp]: "(if invalid then B\<^sub>1 else B\<^sub>2 endif) = invalid" by(rule ext, auto simp: OclIf_def) @@ -1135,9 +1135,9 @@ by simp -subsection{* Fundamental Predicates on Basic Types: Strict (Referential) Equality *} +subsection\Fundamental Predicates on Basic Types: Strict (Referential) Equality\ -text{* +text\ In contrast to logical equality, the OCL standard defines an equality operation which we call ``strict referential equality''. It behaves differently for all types---on value types, it is basically a strict version of strong equality, @@ -1145,22 +1145,22 @@ text{* their references within the store. We introduce strict referential equality as an \emph{overloaded} concept and will handle it for each type instance individually. -*} +\ consts StrictRefEq :: "[('\,'a)val,('\,'a)val] \ ('\)Boolean" (infixl "\" 30) -text{* with {term "not"} we can express the notation:*} +text\with {term "not"} we can express the notation:\ syntax "notequal" :: "('\)Boolean \ ('\)Boolean \ ('\)Boolean" (infix "<>" 40) translations "a <> b" == "CONST OclNot(a \ b)" -text{* We will define instances of this equality in a case-by-case basis.*} +text\We will define instances of this equality in a case-by-case basis.\ -subsection{* Laws to Establish Definedness (\texorpdfstring{$\delta$}{d}-closure) *} +subsection\Laws to Establish Definedness (\texorpdfstring{$\delta$}{d}-closure)\ -text{* For the logical connectives, we have --- beyond -@{thm foundation6} --- the following facts: *} +text\For the logical connectives, we have --- beyond +@{thm foundation6} --- the following facts:\ lemma OclNot_defargs: "\ \ (not P) \ \ \ \ P" by(auto simp: OclNot_def OclValid_def true_def invalid_def defined_def false_def @@ -1181,7 +1181,7 @@ proof - qed -subsection{* A Side-calculus for Constant Terms *} +subsection\A Side-calculus for Constant Terms\ definition "const X \ \ \ \'. X \ = X \'" @@ -1354,7 +1354,7 @@ lemmas const_ss = const_bot const_null const_invalid const_false const_true const_HOL_if const_HOL_and const_HOL_eq -text{* Miscellaneous: Overloading the syntax of ``bottom'' *} +text\Miscellaneous: Overloading the syntax of ``bottom''\ notation bot ("\") diff --git a/Featherweight_OCL/UML_PropertyProfiles.thy b/Featherweight_OCL/UML_PropertyProfiles.thy index db2983e..8ca00d3 100644 --- a/Featherweight_OCL/UML_PropertyProfiles.thy +++ b/Featherweight_OCL/UML_PropertyProfiles.thy @@ -47,17 +47,17 @@ theory UML_PropertyProfiles imports UML_Logic begin -section{* Property Profiles for OCL Operators via Isabelle Locales *} +section\Property Profiles for OCL Operators via Isabelle Locales\ -text{* We use the Isabelle mechanism of a \emph{Locale} to generate the +text\We use the Isabelle mechanism of a \emph{Locale} to generate the common lemmas for each type and operator; Locales can be seen as a functor that takes a local theory and generates a number of theorems. In our case, we will instantiate later these locales by the local theory of an operator definition and obtain the common rules for strictness, definedness propagation, context-passingness and constance in a systematic way. -*} +\ -subsection{* Property Profiles for Monadic Operators *} +subsection\Property Profiles for Monadic Operators\ locale profile_mono_scheme_defined = fixes f :: "('\,'\::null)val \ ('\,'\::null)val" @@ -140,7 +140,7 @@ begin split: if_split_asm) end -subsection{* Property Profiles for Single *} +subsection\Property Profiles for Single\ locale profile_single = fixes d:: "('\,'a::null)val \ '\ Boolean" @@ -148,7 +148,7 @@ locale profile_single = assumes d_cp0: "d X \ = d (\ _. X \) \" assumes d_const[simp,code_unfold]: "const X \ const (d X)" -subsection{* Property Profiles for Binary Operators *} +subsection\Property Profiles for Binary Operators\ definition "bin' f g d\<^sub>x d\<^sub>y X Y = (f X Y = (\ \. if (d\<^sub>x X) \ = true \ \ (d\<^sub>y Y) \ = true \ @@ -223,14 +223,14 @@ begin end -text{* +text\ In our context, we will use Locales as ``Property Profiles'' for OCL operators; if an operator @{term "f"} is of profile @{term "profile_bin_scheme defined f g"} we know -that it satisfies a number of properties like @{text "strict1"} or @{text "strict2"} +that it satisfies a number of properties like \strict1\ or \strict2\ \ie{} @{term "f invalid y = invalid"} and @{term "f null y = invalid"}. Since some of the more advanced Locales come with 10 - 15 theorems, property profiles represent a major structuring mechanism for the OCL library. -*} +\ locale profile_bin_scheme_defined = diff --git a/Featherweight_OCL/UML_State.thy b/Featherweight_OCL/UML_State.thy index 901c2a7..cee9795 100644 --- a/Featherweight_OCL/UML_State.thy +++ b/Featherweight_OCL/UML_State.thy @@ -40,31 +40,31 @@ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. ******************************************************************************) -chapter{* Formalization III: UML/OCL constructs: State Operations and Objects *} +chapter\Formalization III: UML/OCL constructs: State Operations and Objects\ theory UML_State imports UML_Library begin no_notation None ("\") -section{* Introduction: States over Typed Object Universes *} +section\Introduction: States over Typed Object Universes\ -text{* \label{sec:universe} +text\\label{sec:universe} In the following, we will refine the concepts of a user-defined data-model (implied by a class-diagram) as well as the notion of $\state{}$ used in the previous section to much more detail. Surprisingly, even without a concrete notion of an objects and a universe of object representation, the generic infrastructure of state-related operations is fairly rich. -*} +\ -subsection{* Fundamental Properties on Objects: Core Referential Equality *} -subsubsection{* Definition *} +subsection\Fundamental Properties on Objects: Core Referential Equality\ +subsubsection\Definition\ -text{* Generic referential equality - to be used for instantiations - with concrete object types ... *} +text\Generic referential equality - to be used for instantiations + with concrete object types ...\ definition StrictRefEq\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t :: "('\,'a::{object,null})val \ ('\,'a)val \ ('\)Boolean" where "StrictRefEq\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t x y \ \ \. if (\ x) \ = true \ \ (\ y) \ = true \ @@ -73,7 +73,7 @@ where "StrictRefEq\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t x y else \\(oid_of (x \)) = (oid_of (y \)) \\ else invalid \" -subsubsection{* Strictness and context passing *} +subsubsection\Strictness and context passing\ lemma StrictRefEq\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_strict1[simp,code_unfold] : "(StrictRefEq\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t x invalid) = invalid" @@ -88,7 +88,7 @@ lemma cp_StrictRefEq\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t: "(StrictRefEq\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t x y \) = (StrictRefEq\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t (\_. x \) (\_. y \)) \" by(auto simp: StrictRefEq\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def cp_valid[symmetric]) -text_raw{* \isatagafp *} +text_raw\\isatagafp\ lemmas cp0_StrictRefEq\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t= cp_StrictRefEq\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t[THEN allI[THEN allI[THEN allI[THEN cpI2]], of "StrictRefEq\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t"]] @@ -97,12 +97,12 @@ lemmas cp_intro''[intro!,simp,code_unfold] = cp_StrictRefEq\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t[THEN allI[THEN allI[THEN allI[THEN cpI2]], of "StrictRefEq\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t"]] -text_raw{* \endisatagafp *} +text_raw\\endisatagafp\ -subsection{* Logic and Algebraic Layer on Object *} -subsubsection{* Validity and Definedness Properties *} +subsection\Logic and Algebraic Layer on Object\ +subsubsection\Validity and Definedness Properties\ -text{* We derive the usual laws on definedness for (generic) object equality:*} +text\We derive the usual laws on definedness for (generic) object equality:\ lemma StrictRefEq\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_defargs: "\ \ (StrictRefEq\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t x (y::('\,'a::{null,object})val))\ (\ \(\ x)) \ (\ \(\ y))" by(simp add: StrictRefEq\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def OclValid_def true_def invalid_def bot_option_def @@ -119,7 +119,7 @@ lemma StrictRefEq\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def_homo : "\(StrictRefEq\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t x (y::('\,'a::{null,object})val)) = ((\ x) and (\ y))" oops (* sorry *) -subsubsection{* Symmetry *} +subsubsection\Symmetry\ lemma StrictRefEq\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_sym : assumes x_val : "\ \ \ x" @@ -128,9 +128,9 @@ by(simp add: StrictRefEq\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def tru x_val[simplified OclValid_def]) -subsubsection{* Behavior vs StrongEq *} +subsubsection\Behavior vs StrongEq\ -text{* It remains to clarify the role of the state invariant +text\It remains to clarify the role of the state invariant $\inv_\sigma(\sigma)$ mentioned above that states the condition that there is a ``one-to-one'' correspondence between object representations and $\oid$'s: $\forall \mathit{oid} \in \dom\ap @@ -140,33 +140,33 @@ back to \citet{richters:precise:2002}; however, we state this condition as an invariant on states rather than a global axiom. It can, therefore, not be taken for granted that an $\oid$ makes sense both in pre- and post-states of OCL expressions. -*} +\ -text{* We capture this invariant in the predicate WFF :*} +text\We capture this invariant in the predicate WFF :\ definition WFF :: "('\::object)st \ bool" where "WFF \ = ((\ x \ ran(heap(fst \)). \heap(fst \) (oid_of x)\ = x) \ (\ x \ ran(heap(snd \)). \heap(snd \) (oid_of x)\ = x))" -text{* It turns out that WFF is a key-concept for linking strict referential equality to +text\It turns out that WFF is a key-concept for linking strict referential equality to logical equality: in well-formed states (i.e. those states where the self (oid-of) field contains the pointer to which the object is associated to in the state), referential equality coincides -with logical equality. *} +with logical equality.\ -text{* We turn now to the generic definition of referential equality on objects: +text\We turn now to the generic definition of referential equality on objects: Equality on objects in a state is reduced to equality on the references to these objects. As in HOL-OCL~\cite{brucker.ea:hol-ocl:2008,brucker.ea:hol-ocl-book:2006}, we will store the reference of an object inside the object in a (ghost) field. By establishing certain invariants (``consistent state''), it can be assured that there is a ``one-to-one-correspondence'' of objects to their references---and therefore the definition below -behaves as we expect. *} -text{* Generic Referential Equality enjoys the usual properties: +behaves as we expect.\ +text\Generic Referential Equality enjoys the usual properties: (quasi) reflexivity, symmetry, transitivity, substitutivity for defined values. For type-technical reasons, for each concrete -object type, the equality @{text "\"} is defined by generic referential -equality. *} +object type, the equality \\\ is defined by generic referential +equality.\ theorem StrictRefEq\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_vs_StrongEq: assumes WFF: "WFF \" @@ -198,21 +198,21 @@ shows "(\ \ (StrictRefEq\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c apply(auto simp: StrictRefEq\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def OclValid_def WFF_def StrongEq_def true_def Ball_def) by (metis foundation18' oid_preserve valid_x valid_y)+ -text{* So, if two object descriptions live in the same state (both pre or post), the referential -equality on objects implies in a WFF state the logical equality. *} +text\So, if two object descriptions live in the same state (both pre or post), the referential +equality on objects implies in a WFF state the logical equality.\ -section{* Operations on Object *} -subsection{* Initial States (for testing and code generation) *} +section\Operations on Object\ +subsection\Initial States (for testing and code generation)\ definition \\<^sub>0 :: "('\)st" where "\\<^sub>0 \ (\heap=Map.empty, assocs = Map.empty\, \heap=Map.empty, assocs = Map.empty\)" -subsection{* OclAllInstances *} +subsection\OclAllInstances\ -text{* To denote OCL types occurring in OCL expressions syntactically---as, for example, +text\To denote OCL types occurring in OCL expressions syntactically---as, for example, as ``argument'' of \inlineocl{oclAllInstances()}---we use the inverses of the injection functions into the object -universes; we show that this is a sufficient ``characterization.'' *} +universes; we show that this is a sufficient ``characterization.''\ definition OclAllInstances_generic :: "(('\::object) st \ '\ state) \ ('\::object \ '\) \ ('\, '\ option option) Set" @@ -264,7 +264,7 @@ by (metis OclAllInstances_generic_defined A foundation16' foundation18 foundation24 foundation6) -text{* One way to establish the actual presence of an object representation in a state is:*} +text\One way to establish the actual presence of an object representation in a state is:\ definition "is_represented_in_state fst_snd x H \ = (x \ \ (Some o H) ` ran (heap (fst_snd \)))" @@ -305,12 +305,12 @@ proof - by(subst Abs_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e_inject, (simp add: bot_option_def true_def)+) qed -text{* Here comes a couple of operational rules that allow to infer the value +text\Here comes a couple of operational rules that allow to infer the value of \inlineisar+oclAllInstances+ from the context $\tau$. These rules are a special-case in the sense that they are the only rules that relate statements with \emph{different} $\tau$'s. For that reason, new concepts like ``constant contexts P'' are necessary (for which we do not elaborate an own theory for reasons of space limitations; - in examples, we will prove resulting constraints straight forward by hand). *} + in examples, we will prove resulting constraints straight forward by hand).\ lemma state_update_vs_allInstances_generic_including': @@ -475,7 +475,7 @@ qed declare OclAllInstances_generic_def [simp] -subsubsection{* OclAllInstances (@post) *} +subsubsection\OclAllInstances (@post)\ definition OclAllInstances_at_post :: "('\ :: object \ '\) \ ('\, '\ option option) Set" ("_ .allInstances'(')") @@ -503,7 +503,7 @@ unfolding OclAllInstances_at_post_def by(rule represented_generic_objects_defined[OF A[simplified OclAllInstances_at_post_def]]) -text{* One way to establish the actual presence of an object representation in a state is:*} +text\One way to establish the actual presence of an object representation in a state is:\ lemma assumes A: "\ \ H .allInstances()->includes\<^sub>S\<^sub>e\<^sub>t(x)" @@ -515,12 +515,12 @@ shows "(\, \heap=Map.empty, assocs=A\) \ Type unfolding OclAllInstances_at_post_def by(rule state_update_vs_allInstances_generic_empty[OF snd_conv]) -text{* Here comes a couple of operational rules that allow to infer the value +text\Here comes a couple of operational rules that allow to infer the value of \inlineisar+oclAllInstances+ from the context $\tau$. These rules are a special-case in the sense that they are the only rules that relate statements with \emph{different} $\tau$'s. For that reason, new concepts like ``constant contexts P'' are necessary (for which we do not elaborate an own theory for reasons of space limitations; - in examples, we will prove resulting constraints straight forward by hand). *} + in examples, we will prove resulting constraints straight forward by hand).\ lemma state_update_vs_allInstances_at_post_including': @@ -581,7 +581,7 @@ shows "((\, \heap=\'(oid\Object),assocs=A\ unfolding OclAllInstances_at_post_def by(rule state_update_vs_allInstances_generic_tc[OF snd_conv], insert assms) -subsubsection{* OclAllInstances (@pre) *} +subsubsection\OclAllInstances (@pre)\ definition OclAllInstances_at_pre :: "('\ :: object \ '\) \ ('\, '\ option option) Set" ("_ .allInstances@pre'(')") @@ -608,7 +608,7 @@ unfolding OclAllInstances_at_pre_def by(rule represented_generic_objects_defined[OF A[simplified OclAllInstances_at_pre_def]]) -text{* One way to establish the actual presence of an object representation in a state is:*} +text\One way to establish the actual presence of an object representation in a state is:\ lemma assumes A: "\ \ H .allInstances@pre()->includes\<^sub>S\<^sub>e\<^sub>t(x)" @@ -621,12 +621,12 @@ shows "(\heap=Map.empty, assocs=A\, \) \ Type unfolding OclAllInstances_at_pre_def by(rule state_update_vs_allInstances_generic_empty[OF fst_conv]) -text{* Here comes a couple of operational rules that allow to infer the value +text\Here comes a couple of operational rules that allow to infer the value of \inlineisar+oclAllInstances@pre+ from the context $\tau$. These rules are a special-case in the sense that they are the only rules that relate statements with \emph{different} $\tau$'s. For that reason, new concepts like ``constant contexts P'' are necessary (for which we do not elaborate an own theory for reasons of space limitations; - in examples, we will prove resulting constraints straight forward by hand). *} + in examples, we will prove resulting constraints straight forward by hand).\ lemma state_update_vs_allInstances_at_pre_including': @@ -687,7 +687,7 @@ shows "((\heap=\'(oid\Object),assocs=A\, \ unfolding OclAllInstances_at_pre_def by(rule state_update_vs_allInstances_generic_tc[OF fst_conv], insert assms) -subsubsection{* @post or @pre *} +subsubsection\@post or @pre\ theorem StrictRefEq\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_vs_StrongEq'': assumes WFF: "WFF \" @@ -730,7 +730,7 @@ proof - simp add: comp_def image_def, fastforce)+ qed -subsection{* OclIsNew, OclIsDeleted, OclIsMaintained, OclIsAbsent *} +subsection\OclIsNew, OclIsDeleted, OclIsMaintained, OclIsAbsent\ definition OclIsNew:: "('\, '\::{null,object})val \ ('\)Boolean" ("(_).oclIsNew'(')") where "X .oclIsNew() \ (\\ . if (\ X) \ = true \ @@ -738,9 +738,9 @@ where "X .oclIsNew() \ (\\ . if (\ X) \ = true \ oid_of (X \) \ dom(heap(snd \))\\ else invalid \)" -text{* The following predicates --- which are not part of the OCL standard descriptions --- +text\The following predicates --- which are not part of the OCL standard descriptions --- complete the goal of \inlineisar+oclIsNew+ by describing where an object belongs. -*} +\ definition OclIsDeleted:: "('\, '\::{null,object})val \ ('\)Boolean" ("(_).oclIsDeleted'(')") where "X .oclIsDeleted() \ (\\ . if (\ X) \ = true \ @@ -772,17 +772,17 @@ lemma notNew_vs_others : "\ \ \ X \ by(simp add: OclIsDeleted_def OclIsNew_def OclIsMaintained_def OclIsAbsent_def OclNot_def OclValid_def true_def, blast) -subsection{* OclIsModifiedOnly *} -subsubsection{* Definition *} +subsection\OclIsModifiedOnly\ +subsubsection\Definition\ -text{* The following predicate---which is not part of the OCL +text\The following predicate---which is not part of the OCL standard---provides a simple, but powerful means to describe framing conditions. For any formal approach, be it animation of OCL contracts, test-case generation or die-hard theorem proving, the specification of the part of a system transition that \emph{does not change} is of primordial importance. The following operator establishes the equality between old and new objects in the state (provided that they exist in -both states), with the exception of those objects. *} +both states), with the exception of those objects.\ definition OclIsModifiedOnly ::"('\::object,'\::{null,object})Set \ '\ Boolean" ("_->oclIsModifiedOnly'(')") @@ -793,7 +793,7 @@ where "X->oclIsModifiedOnly() \ (\(\,\'). then \\\ x \ S. (heap \) x = (heap \') x\\ else invalid (\,\'))" -subsubsection{* Execution with Invalid or Null or Null Element as Argument *} +subsubsection\Execution with Invalid or Null or Null Element as Argument\ lemma "invalid->oclIsModifiedOnly() = invalid" by(simp add: OclIsModifiedOnly_def) @@ -810,16 +810,16 @@ lemma apply(simp split: if_split_asm) by(simp add: null_fun_def, blast) -subsubsection{* Context Passing *} +subsubsection\Context Passing\ lemma cp_OclIsModifiedOnly : "X->oclIsModifiedOnly() \ = (\_. X \)->oclIsModifiedOnly() \" by(simp only: OclIsModifiedOnly_def, case_tac \, simp only:, subst cp_defined, simp) -subsection{* OclSelf *} +subsection\OclSelf\ -text{* The following predicate---which is not part of the OCL +text\The following predicate---which is not part of the OCL standard---explicitly retrieves in the pre or post state the original OCL expression -given as argument. *} +given as argument.\ definition [simp]: "OclSelf x H fst_snd = (\\ . if (\ x) \ = true \ then if oid_of (x \) \ dom(heap(fst \)) \ oid_of (x \) \ dom(heap (snd \)) @@ -837,7 +837,7 @@ definition OclSelf_at_post :: "('\::object,'\::{null,object})val \::object,'\::{null,object})val" ("(_)@post(_)") where "x @post H = OclSelf x H snd" -subsection{* Framing Theorem *} +subsection\Framing Theorem\ lemma all_oid_diff: assumes def_x : "\ \ \ x" @@ -956,8 +956,8 @@ theorem framing: qed(simp add: OclSelf_at_post_def OclSelf_at_pre_def OclValid_def StrongEq_def true_def)+ -text{* As corollary, the framing property can be expressed with only the strong equality -as comparison operator. *} +text\As corollary, the framing property can be expressed with only the strong equality +as comparison operator.\ theorem framing': assumes wff : "WFF \" @@ -985,7 +985,7 @@ proof - by(simp add: OclSelf_at_post_def OclSelf_at_pre_def OclValid_def StrongEq_def true_def)+ qed -subsection{* Miscellaneous *} +subsection\Miscellaneous\ lemma pre_post_new: "\ \ (x .oclIsNew()) \ \ (\ \ \(x @pre H1)) \ \ (\ \ \(x @post H2))" by(simp add: OclIsNew_def OclSelf_at_pre_def OclSelf_at_post_def @@ -1021,17 +1021,17 @@ by(simp add: OclIsMaintained_def OclSelf_at_pre_def OclSelf_at_post_def lemma framing_same_state: "(\, \) \ (x @pre H \ (x @post H))" by(simp add: OclSelf_at_pre_def OclSelf_at_post_def OclValid_def StrongEq_def) -section{* Accessors on Object *} -subsection{* Definition *} +section\Accessors on Object\ +subsection\Definition\ definition "select_object mt incl smash deref l = smash (foldl incl mt (map deref l)) \ \smash returns null with \mt\ in input (in this case, object contains null pointer)\" -text{* The continuation @{text f} is usually instantiated with a smashing +text\The continuation \f\ is usually instantiated with a smashing function which is either the identity @{term id} or, for \inlineocl{0..1} cardinalities of associations, the @{term OclANY}-selector which also handles the @{term null}-cases appropriately. A standard use-case for this combinator -is for example: *} +is for example:\ term "(select_object mtSet UML_Set.OclIncluding UML_Set.OclANY f l oid )::('\, 'a::null)val" definition "select_object\<^sub>S\<^sub>e\<^sub>t = select_object mtSet UML_Set.OclIncluding id" @@ -1047,7 +1047,7 @@ definition "select_object\<^sub>S\<^sub>e\<^sub>q = select_object mtSequence UML definition "select_object_any\<^sub>S\<^sub>e\<^sub>q f s_set = UML_Sequence.OclANY (select_object\<^sub>S\<^sub>e\<^sub>q f s_set)" definition "select_object\<^sub>P\<^sub>a\<^sub>i\<^sub>r f1 f2 = (\(a,b). OclPair (f1 a) (f2 b))" -subsection{* Validity and Definedness Properties *} +subsection\Validity and Definedness Properties\ lemma select_fold_exec\<^sub>S\<^sub>e\<^sub>q: assumes "list_all (\f. (\ \ \ f)) l" diff --git a/Featherweight_OCL/UML_Tools.thy b/Featherweight_OCL/UML_Tools.thy index 5b6f728..bf088e6 100644 --- a/Featherweight_OCL/UML_Tools.thy +++ b/Featherweight_OCL/UML_Tools.thy @@ -70,7 +70,7 @@ lemmas substs4 = StrongEq_L_subst4_rev lemmas substs = substs1 substs2 substs4 [THEN iffD2] substs4 thm substs -ML{* +ML\ fun ocl_subst_asm_tac ctxt = FIRST'(map (fn C => (eresolve0_tac [C]) THEN' (simp_tac ctxt)) @{thms "substs"}) @@ -81,7 +81,7 @@ val _ = Theory.setup (Scan.succeed (ocl_subst_asm)) "ocl substition step") -*} +\ lemma test1 : "\ \ A \ \ \ (A and B \ B)" apply(tactic "ocl_subst_asm_tac @{context} 1") diff --git a/Featherweight_OCL/UML_Types.thy b/Featherweight_OCL/UML_Types.thy index 96b57e9..25f82fa 100644 --- a/Featherweight_OCL/UML_Types.thy +++ b/Featherweight_OCL/UML_Types.thy @@ -40,7 +40,7 @@ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. ******************************************************************************) -chapter{* Formalization I: OCL Types and Core Definitions \label{sec:focl-types}*} +chapter\Formalization I: OCL Types and Core Definitions \label{sec:focl-types}\ theory UML_Types imports HOL.Transcendental @@ -48,14 +48,14 @@ keywords "Assert" :: thy_decl and "Assert_local" :: thy_decl begin -section{* Preliminaries *} -subsection{* Notations for the Option Type *} +section\Preliminaries\ +subsection\Notations for the Option Type\ -text{* +text\ First of all, we will use a more compact notation for the library option type which occur all over in our definitions and which will make the presentation more like a textbook: -*} +\ no_notation ceiling ("\_\") (* For Real Numbers only ... Otherwise has unfortunate side-effects on syntax. *) no_notation floor ("\_\") (* For Real Numbers only ... Otherwise has unfortunate side-effects on syntax. *) @@ -64,65 +64,65 @@ type_notation option ("\_\\<^sub>\") (* NOTE: "_\<^sub>\ notation Some ("\(_)\") notation None ("\") -text{* These commands introduce an alternative, more compact notation for the type constructor +text\These commands introduce an alternative, more compact notation for the type constructor @{typ "'\ option"}, namely @{typ "\'\\\<^sub>\"}. Furthermore, the constructors @{term "Some X"} and - @{term "None"} of the type @{typ "'\ option"}, namely @{term "\X\"} and @{term "\"}. *} + @{term "None"} of the type @{typ "'\ option"}, namely @{term "\X\"} and @{term "\"}.\ -text{* +text\ The following function (corresponding to @{term the} in the Isabelle/HOL library) is defined as the inverse of the injection @{term Some}. -*} +\ fun drop :: "'\ option \ '\" ("\(_)\") where drop_lift[simp]: "\\v\\ = v" -text{* The definitions for the constants and operations based on functions +text\The definitions for the constants and operations based on functions will be geared towards a format that Isabelle can check to be a ``conservative'' (\ie, logically safe) axiomatic definition. By introducing an explicit interpretation function (which happens to be defined just as the identity since we are using a shallow embedding of OCL into HOL), all these definitions can be rewritten into the conventional semantic textbook format. -To say it in other words: The interpretation function @{text Sem} as defined +To say it in other words: The interpretation function \Sem\ as defined below is just a textual marker for presentation purposes, i.e. intended for readers used to conventional textbook notations on semantics. Since we use a ``shallow embedding'', i.e. since we represent the syntax of OCL directly by HOL constants, the interpretation function is semantically not only superfluous, but from an Isabelle perspective strictly in the way for certain consistency checks performed by the definitional packages. -*} +\ definition Sem :: "'a \ 'a" ("I\_\") where "I\x\ \ x" -subsection{* Common Infrastructure for all OCL Types \label{sec:focl-common-types}*} +subsection\Common Infrastructure for all OCL Types \label{sec:focl-common-types}\ -text {* In order to have the possibility to nest collection types, - such that we can give semantics to expressions like @{text "Set{Set{\},null}"}, +text \In order to have the possibility to nest collection types, + such that we can give semantics to expressions like \Set{Set{\},null}\, it is necessary to introduce a uniform interface for types having - the @{text "invalid"} (= bottom) element. The reason is that we impose + the \invalid\ (= bottom) element. The reason is that we impose a data-invariant on raw-collection \inlineisar|types_code| which assures - that the @{text "invalid"} element is not allowed inside the collection; - all raw-collections of this form were identified with the @{text "invalid"} element + that the \invalid\ element is not allowed inside the collection; + all raw-collections of this form were identified with the \invalid\ element itself. The construction requires that the new collection type is not comparable with the raw-types (consisting of nested option type constructions), such that the data-invariant must be expressed in terms of the interface. In a second step, our base-types will be shown to be instances of this interface. - *} +\ -text{* +text\ This uniform interface consists in a type class requiring the existence of a bot and a null element. The construction proceeds by - abstracting the null (defined by @{text "\ \ \"} on - @{text "'a option option"}) to a @{text null} element, which may - have an arbitrary semantic structure, and an undefinedness element @{text "\"} - to an abstract undefinedness element @{text "bot"} (also written - @{text "\"} whenever no confusion arises). As a consequence, it is necessary + abstracting the null (defined by \\ \ \\ on + \'a option option\) to a \null\ element, which may + have an arbitrary semantic structure, and an undefinedness element \\\ + to an abstract undefinedness element \bot\ (also written + \\\ whenever no confusion arises). As a consequence, it is necessary to redefine the notions of invalid, defined, valuation etc. - on top of this interface. *} + on top of this interface.\ -text{* - This interface consists in two abstract type classes @{text bot} - and @{text null} for the class of all types comprising a bot and a - distinct null element. *} +text\ + This interface consists in two abstract type classes \bot\ + and \null\ for the class of all types comprising a bot and a + distinct null element.\ class bot = fixes bot :: "'a" @@ -134,15 +134,15 @@ class null = bot + assumes null_is_valid : "null \ bot" -subsection{* Accommodation of Basic Types to the Abstract Interface *} +subsection\Accommodation of Basic Types to the Abstract Interface\ -text{* +text\ In the following it is shown that the ``option-option'' type is - in fact in the @{text null} class and that function spaces over these + in fact in the \null\ class and that function spaces over these classes again ``live'' in these classes. This motivates the default construction of the semantic domain for the basic types (\inlineocl{Boolean}, \inlineocl{Integer}, \inlineocl{Real}, \ldots). -*} +\ instantiation option :: (type)bot begin @@ -188,32 +188,32 @@ begin qed end -text{* A trivial consequence of this adaption of the interface is that +text\A trivial consequence of this adaption of the interface is that abstract and concrete versions of null are the same on base types -(as could be expected). *} +(as could be expected).\ -subsection{* The Common Infrastructure of Object Types (Class Types) and States. *} +subsection\The Common Infrastructure of Object Types (Class Types) and States.\ -text{* Recall that OCL is a textual extension of the UML; in particular, we use OCL as means to +text\Recall that OCL is a textual extension of the UML; in particular, we use OCL as means to annotate UML class models. Thus, OCL inherits a notion of \emph{data} in the UML: UML class models provide classes, inheritance, types of objects, and subtypes connecting them along the inheritance hierarchie. -*} +\ -text{* For the moment, we formalize the most common notions of objects, in particular +text\For the moment, we formalize the most common notions of objects, in particular the existance of object-identifiers (oid) for each object under which it can -be referenced in a \emph{state}. *} +be referenced in a \emph{state}.\ type_synonym oid = nat -text{* We refrained from the alternative: +text\We refrained from the alternative: \begin{isar}[mathescape] $\text{\textbf{type-synonym}}$ $\mathit{oid = ind}$ \end{isar} which is slightly more abstract but non-executable. -*} +\ -text{* \emph{States} in UML/OCL are a pair of +text\\emph{States} in UML/OCL are a pair of \begin{itemize} \item a partial map from oid's to elements of an \emph{object universe}, \ie{} the set of all possible object representations. @@ -221,32 +221,32 @@ text{* \emph{States} in UML/OCL are a pair of objects living in a state. These relations can be n-ary which we model by nested lists. \end{itemize} For the moment we do not have to describe the concrete structure of the object universe and denote -it by the polymorphic variable @{text "'\"}.*} +it by the polymorphic variable \'\\.\ record ('\)state = heap :: "oid \ '\ " assocs :: "oid \ ((oid list) list) list" -text{* In general, OCL operations are functions implicitly depending on a pair +text\In general, OCL operations are functions implicitly depending on a pair of pre- and post-state, \ie{} \emph{state transitions}. Since this will be reflected in our representation of OCL Types within HOL, we need to introduce the foundational concept of an -object id (oid), which is just some infinite set, and some abstract notion of state. *} +object id (oid), which is just some infinite set, and some abstract notion of state.\ type_synonym ('\)st = "'\ state \ '\ state" -text{* We will require for all objects that there is a function that +text\We will require for all objects that there is a function that projects the oid of an object in the state (we will settle the question how to define this function later). We will use the Isabelle type class mechanism~\cite{haftmann.ea:constructive:2006} -to capture this: *} +to capture this:\ class object = fixes oid_of :: "'a \ oid" -text{* Thus, if needed, we can constrain the object universe to objects by adding -the following type class constraint:*} +text\Thus, if needed, we can constrain the object universe to objects by adding +the following type class constraint:\ typ "'\ :: object" -text{* The major instance needed are instances constructed over options: once an object, -options of objects are also objects. *} +text\The major instance needed are instances constructed over options: once an object, +options of objects are also objects.\ instantiation option :: (object)object begin definition oid_of_option_def: "oid_of x = oid_of (the x)" @@ -254,43 +254,43 @@ begin end -subsection{* Common Infrastructure for all OCL Types (II): Valuations as OCL Types *} -text{* Since OCL operations in general depend on pre- and post-states, we will +subsection\Common Infrastructure for all OCL Types (II): Valuations as OCL Types\ +text\Since OCL operations in general depend on pre- and post-states, we will represent OCL types as \emph{functions} from pre- and post-state to some HOL raw-type that contains exactly the data in the OCL type --- see below. This gives rise to the idea that we represent OCL types by \emph{Valuations}. -*} -text{* Valuations are functions from a state pair (built upon +\ +text\Valuations are functions from a state pair (built upon data universe @{typ "'\"}) to an arbitrary null-type (\ie, containing -at least a destinguished @{text "null"} and @{text "invalid"} element). *} +at least a destinguished \null\ and \invalid\ element).\ type_synonym ('\,'\) val = "'\ st \ '\::null" -text{* The definitions for the constants and operations based on valuations +text\The definitions for the constants and operations based on valuations will be geared towards a format that Isabelle can check to be a ``conservative'' (\ie, logically safe) axiomatic definition. By introducing an explicit interpretation function (which happens to be defined just as the identity since we are using a shallow embedding of OCL into HOL), all these definitions -can be rewritten into the conventional semantic textbook format as follows: *} +can be rewritten into the conventional semantic textbook format as follows:\ -subsection{* The fundamental constants 'invalid' and 'null' in all OCL Types *} +subsection\The fundamental constants 'invalid' and 'null' in all OCL Types\ -text{* As a consequence of semantic domain definition, any OCL type will -have the two semantic constants @{text "invalid"} (for exceptional, aborted -computation) and @{text "null"}: - *} +text\As a consequence of semantic domain definition, any OCL type will +have the two semantic constants \invalid\ (for exceptional, aborted +computation) and \null\: +\ definition invalid :: "('\,'\::bot) val" where "invalid \ \ \. bot" -text{* This conservative Isabelle definition of the polymorphic constant -@{const invalid} is equivalent with the textbook definition: *} +text\This conservative Isabelle definition of the polymorphic constant +@{const invalid} is equivalent with the textbook definition:\ lemma textbook_invalid: "I\invalid\\ = bot" by(simp add: invalid_def Sem_def) -text {* Note that the definition : +text \Note that the definition : {\small \begin{isar}[mathescape] definition null :: "('$\mathfrak{A}$,'\::null) val" @@ -302,27 +302,27 @@ Thus, the polymorphic constant @{const null} is simply the result of a general type class construction. Nevertheless, we can derive the semantic textbook definition for the OCL null constant based on the abstract null: -*} +\ lemma textbook_null_fun: "I\null::('\,'\::null) val\ \ = (null::('\::null))" by(simp add: null_fun_def Sem_def) -section{* Basic OCL Value Types *} +section\Basic OCL Value Types\ -text {* The structure of this section roughly follows the structure of Chapter +text \The structure of this section roughly follows the structure of Chapter 11 of the OCL standard~\cite{omg:ocl:2012}, which introduces the OCL -Library. *} +Library.\ -text{* The semantic domain of the (basic) boolean type is now defined as the Standard: -the space of valuation to @{typ "bool option option"}, \ie{} the Boolean base type:*} +text\The semantic domain of the (basic) boolean type is now defined as the Standard: +the space of valuation to @{typ "bool option option"}, \ie{} the Boolean base type:\ type_synonym Boolean\<^sub>b\<^sub>a\<^sub>s\<^sub>e = "bool option option" type_synonym ('\)Boolean = "('\,Boolean\<^sub>b\<^sub>a\<^sub>s\<^sub>e) val" -text{* Because of the previous class definitions, Isabelle type-inference establishes that +text\Because of the previous class definitions, Isabelle type-inference establishes that @{typ "('\)Boolean"} lives actually both in the type class @{term bot} and @{term null}; this type is sufficiently rich to contain at least these two elements. -Analogously we build: *} +Analogously we build:\ type_synonym Integer\<^sub>b\<^sub>a\<^sub>s\<^sub>e = "int option option" type_synonym ('\)Integer = "('\,Integer\<^sub>b\<^sub>a\<^sub>s\<^sub>e) val" @@ -332,19 +332,19 @@ type_synonym ('\)String = "('\,String\<^sub>b\<^sub>a\<^sub>s\<^sub>e) v type_synonym Real\<^sub>b\<^sub>a\<^sub>s\<^sub>e = "real option option" type_synonym ('\)Real = "('\,Real\<^sub>b\<^sub>a\<^sub>s\<^sub>e) val" -text{* Since @{term "Real"} is again a basic type, we define its semantic domain -as the valuations over @{text "real option option"} --- i.e. the mathematical type of real numbers. -The HOL-theory for @{text real} ``Real'' transcendental numbers such as $\pi$ and $e$ as well as +text\Since @{term "Real"} is again a basic type, we define its semantic domain +as the valuations over \real option option\ --- i.e. the mathematical type of real numbers. +The HOL-theory for \real\ ``Real'' transcendental numbers such as $\pi$ and $e$ as well as infrastructure to reason over infinite convergent Cauchy-sequences (it is thus possible, in principle, to reason in Featherweight OCL that the sum of inverted two-s exponentials is actually 2. -If needed, a code-generator to compile @{text "Real"} to floating-point +If needed, a code-generator to compile \Real\ to floating-point numbers can be added; this allows for mapping reals to an efficient machine representation; -of course, this feature would be logically unsafe.*} +of course, this feature would be logically unsafe.\ -text{* For technical reasons related to the Isabelle type inference for type-classes +text\For technical reasons related to the Isabelle type inference for type-classes (we don't get the properties in the right order that class instantiation provides them, -if we would follow the previous scheme), we give a slightly atypic definition:*} +if we would follow the previous scheme), we give a slightly atypic definition:\ typedef Void\<^sub>b\<^sub>a\<^sub>s\<^sub>e = "{X::unit option option. X = bot \ X = null }" by(rule_tac x="bot" in exI, simp) @@ -353,41 +353,41 @@ type_synonym ('\)Void = "('\,Void\<^sub>b\<^sub>a\<^sub>s\<^sub>e) val" -section{* Some OCL Collection Types *} +section\Some OCL Collection Types\ -text{* For the semantic construction of the collection types, we have two goals: +text\For the semantic construction of the collection types, we have two goals: \begin{enumerate} \item we want the types to be \emph{fully abstract}, \ie, the type should not contain junk-elements that are not representable by OCL expressions, and \item we want a possibility to nest collection types (so, we want the - potential of talking about @{text "Set(Set(Sequences(Pairs(X,Y))))"}). + potential of talking about \Set(Set(Sequences(Pairs(X,Y))))\). \end{enumerate} -The former principle rules out the option to define @{text "'\ Set"} just by - @{text "('\, ('\ option option) set) val"}. This would allow sets to contain -junk elements such as @{text "{\}"} which we need to identify with undefinedness +The former principle rules out the option to define \'\ Set\ just by + \('\, ('\ option option) set) val\. This would allow sets to contain +junk elements such as \{\}\ which we need to identify with undefinedness itself. Abandoning fully abstractness of rules would later on produce all sorts of problems when quantifying over the elements of a type. However, if we build an own type, then it must conform to our abstract interface in order to have nested types: arguments of type-constructors must conform to our abstract interface, and the result type too. -*} +\ -subsection{* The Construction of the Pair Type (Tuples) *} +subsection\The Construction of the Pair Type (Tuples)\ -text{* The core of an own type construction is done via a type - definition which provides the base-type @{text "('\, '\) Pair\<^sub>b\<^sub>a\<^sub>s\<^sub>e"}. It +text\The core of an own type construction is done via a type + definition which provides the base-type \('\, '\) Pair\<^sub>b\<^sub>a\<^sub>s\<^sub>e\. It is shown that this type ``fits'' indeed into the abstract type - interface discussed in the previous section. *} + interface discussed in the previous section.\ typedef (overloaded) ('\, '\) Pair\<^sub>b\<^sub>a\<^sub>s\<^sub>e = "{X::('\::null \ '\::null) option option. X = bot \ X = null \ (fst\\X\\ \ bot \ snd\\X\\ \ bot)}" by (rule_tac x="bot" in exI, simp) -text{* We ``carve'' out from the concrete type @{typ "('\::null \ '\::null) option option"} +text\We ``carve'' out from the concrete type @{typ "('\::null \ '\::null) option option"} the new fully abstract type, which will not contain representations like @{term "\\(\,a)\\"} -or @{term "\\(b,\)\\"}. The type constuctor @{text "Pair{x,y}"} to be defined later will +or @{term "\\(b,\)\\"}. The type constuctor \Pair{x,y}\ to be defined later will identify these with @{term "invalid"}. -*} +\ instantiation Pair\<^sub>b\<^sub>a\<^sub>s\<^sub>e :: (null,null)bot begin @@ -410,20 +410,20 @@ begin end -text{* ... and lifting this type to the format of a valuation gives us:*} +text\... and lifting this type to the format of a valuation gives us:\ type_synonym ('\,'\,'\) Pair = "('\, ('\,'\) Pair\<^sub>b\<^sub>a\<^sub>s\<^sub>e) val" type_notation Pair\<^sub>b\<^sub>a\<^sub>s\<^sub>e ("Pair'(_,_')") -subsection{* The Construction of the Set Type *} +subsection\The Construction of the Set Type\ -text{* The core of an own type construction is done via a type - definition which provides the raw-type @{text "'\ Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e"}. It +text\The core of an own type construction is done via a type + definition which provides the raw-type \'\ Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e\. It is shown that this type ``fits'' indeed into the abstract type interface discussed in the previous section. Note that we make no restriction whatsoever to \emph{finite} sets; while with the standards type-constructors only finite sets can be denoted, there is the possibility to define in fact infinite - type constructors in \FOCL (c.f. \autoref{sec:type-extensions}). *} + type constructors in \FOCL (c.f. \autoref{sec:type-extensions}).\ typedef (overloaded) '\ Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e ="{X::('\::null) set option option. X = bot \ X = null \ (\x\\\X\\. x \ bot)}" by (rule_tac x="bot" in exI, simp) @@ -450,13 +450,13 @@ begin qed end -text{* ... and lifting this type to the format of a valuation gives us:*} +text\... and lifting this type to the format of a valuation gives us:\ type_synonym ('\,'\) Set = "('\, '\ Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e) val" type_notation Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e ("Set'(_')") -subsection{* The Construction of the Bag Type *} -text{* The core of an own type construction is done via a type - definition which provides the raw-type @{text "'\ Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e"} +subsection\The Construction of the Bag Type\ +text\The core of an own type construction is done via a type + definition which provides the raw-type \'\ Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e\ based on multi-sets from the \HOL library. As in Sets, it is shown that this type ``fits'' indeed into the abstract type interface discussed in the previous section, and as in sets, we make @@ -464,9 +464,9 @@ text{* The core of an own type construction is done via a type the standards type-constructors only finite sets can be denoted, there is the possibility to define in fact infinite type constructors in \FOCL (c.f. \autoref{sec:type-extensions}). - However, while several @{text null} elements are possible in a Bag, there + However, while several \null\ elements are possible in a Bag, there can't be no bottom (invalid) element in them. -*} +\ typedef (overloaded) '\ Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e ="{X::('\::null \ nat) option option. X = bot \ X = null \ \\X\\ bot = 0 }" by (rule_tac x="bot" in exI, simp) @@ -494,16 +494,16 @@ begin qed end -text{* ... and lifting this type to the format of a valuation gives us:*} +text\... and lifting this type to the format of a valuation gives us:\ type_synonym ('\,'\) Bag = "('\, '\ Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e) val" type_notation Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e ("Bag'(_')") -subsection{* The Construction of the Sequence Type *} +subsection\The Construction of the Sequence Type\ -text{* The core of an own type construction is done via a type - definition which provides the base-type @{text "'\ Sequence\<^sub>b\<^sub>a\<^sub>s\<^sub>e"}. It +text\The core of an own type construction is done via a type + definition which provides the base-type \'\ Sequence\<^sub>b\<^sub>a\<^sub>s\<^sub>e\. It is shown that this type ``fits'' indeed into the abstract type - interface discussed in the previous section. *} + interface discussed in the previous section.\ typedef (overloaded) '\ Sequence\<^sub>b\<^sub>a\<^sub>s\<^sub>e ="{X::('\::null) list option option. X = bot \ X = null \ (\x\set \\X\\. x \ bot)}" @@ -534,12 +534,12 @@ begin end -text{* ... and lifting this type to the format of a valuation gives us:*} +text\... and lifting this type to the format of a valuation gives us:\ type_synonym ('\,'\) Sequence = "('\, '\ Sequence\<^sub>b\<^sub>a\<^sub>s\<^sub>e) val" type_notation Sequence\<^sub>b\<^sub>a\<^sub>s\<^sub>e ("Sequence'(_')") -subsection{* Discussion: The Representation of UML/OCL Types in Featherweight OCL *} -text{* In the introduction, we mentioned that there is an ``injective representation +subsection\Discussion: The Representation of UML/OCL Types in Featherweight OCL\ +text\In the introduction, we mentioned that there is an ``injective representation mapping'' between the types of OCL and the types of Featherweight OCL (and its meta-language: HOL). This injectivity is at the heart of our representation technique --- a so-called \emph{shallow embedding} --- and means: OCL types were mapped one-to-one @@ -547,9 +547,9 @@ to types in HOL, ruling out a resentation where everything is mapped on some common HOL-type, say ``OCL-expression'', in which we would have to sort out the typing of OCL and its impact on the semantic representation function in an own, quite heavy side-calculus. -*} +\ -text{* After the previous sections, we are now able to exemplify this representation as follows: +text\After the previous sections, we are now able to exemplify this representation as follows: \begin{table}[htbp] \centering @@ -579,22 +579,22 @@ We do not formalize the representation map here; however, its principles are qui \item the arguments of type constructors \inlineocl{Set(T)} remain corresponding HOL base-types. \end{enumerate} -*} +\ -text{* Note, furthermore, that our construction of ``fully abstract types'' (no junk, no confusion) +text\Note, furthermore, that our construction of ``fully abstract types'' (no junk, no confusion) assures that the logical equality to be defined in the next section works correctly and comes -as element of the ``lingua franca'', \ie{} HOL. *} +as element of the ``lingua franca'', \ie{} HOL.\ (*<*) -section{* Miscelleaneous: ML assertions *} +section\Miscelleaneous: ML assertions\ -text{* We introduce here a new command \emph{Assert} similar as \emph{value} for proving +text\We introduce here a new command \emph{Assert} similar as \emph{value} for proving that the given term in argument is a true proposition. The difference with \emph{value} is that \emph{Assert} fails if the normal form of the term evaluated is not equal to @{term True}. Moreover, in case \emph{value} could not normalize the given term, as another strategy of reduction - we try to prove it with a single ``simp'' tactic. *} + we try to prove it with a single ``simp'' tactic.\ -ML{* +ML\ fun disp_msg title msg status = title ^ ": '" ^ msg ^ "' " ^ status fun lemma msg specification_theorem concl in_local thy = @@ -639,7 +639,7 @@ fun outer_syntax_command command_spec theory in_local = val () = outer_syntax_command @{command_keyword Assert} Toplevel.theory Named_Target.theory_map val () = outer_syntax_command @{command_keyword Assert_local} (Toplevel.local_theory NONE NONE) I -*} +\ (*>*) diff --git a/Featherweight_OCL/basic_types/UML_Boolean.thy b/Featherweight_OCL/basic_types/UML_Boolean.thy index a7b244e..d1c64f1 100644 --- a/Featherweight_OCL/basic_types/UML_Boolean.thy +++ b/Featherweight_OCL/basic_types/UML_Boolean.thy @@ -45,13 +45,13 @@ imports "../UML_PropertyProfiles" begin -subsection{* Fundamental Predicates on Basic Types: Strict (Referential) Equality *} -text{* +subsection\Fundamental Predicates on Basic Types: Strict (Referential) Equality\ +text\ Here is a first instance of a definition of strict value equality---for the special case of the type @{typ "('\)Boolean"}, it is just the strict extension of the logical equality: -*} +\ overloading StrictRefEq \ "StrictRefEq :: [('\)Boolean,('\)Boolean] \ ('\)Boolean" begin definition StrictRefEq\<^sub>B\<^sub>o\<^sub>o\<^sub>l\<^sub>e\<^sub>a\<^sub>n[code_unfold] : @@ -60,7 +60,7 @@ begin else invalid \" end -text{* which implies elementary properties like: *} +text\which implies elementary properties like:\ lemma [simp,code_unfold] : "(true \ false) = false" by(simp add:StrictRefEq\<^sub>B\<^sub>o\<^sub>o\<^sub>l\<^sub>e\<^sub>a\<^sub>n) lemma [simp,code_unfold] : "(false \ true) = false" @@ -84,28 +84,28 @@ lemma true_non_null [simp,code_unfold]:"(true \ null) = false" apply(rule ext, simp add: StrictRefEq\<^sub>B\<^sub>o\<^sub>o\<^sub>l\<^sub>e\<^sub>a\<^sub>n StrongEq_def false_def) by(simp add: true_def bot_option_def null_fun_def null_option_def) -text{* With respect to strictness properties and miscelleaneous side-calculi, +text\With respect to strictness properties and miscelleaneous side-calculi, strict referential equality behaves on booleans as described in the -@{term "profile_bin\<^sub>S\<^sub>t\<^sub>r\<^sub>o\<^sub>n\<^sub>g\<^sub>E\<^sub>q_\<^sub>v_\<^sub>v"}:*} +@{term "profile_bin\<^sub>S\<^sub>t\<^sub>r\<^sub>o\<^sub>n\<^sub>g\<^sub>E\<^sub>q_\<^sub>v_\<^sub>v"}:\ interpretation StrictRefEq\<^sub>B\<^sub>o\<^sub>o\<^sub>l\<^sub>e\<^sub>a\<^sub>n : profile_bin\<^sub>S\<^sub>t\<^sub>r\<^sub>o\<^sub>n\<^sub>g\<^sub>E\<^sub>q_\<^sub>v_\<^sub>v "\ x y. (x::('\)Boolean) \ y" by unfold_locales (auto simp:StrictRefEq\<^sub>B\<^sub>o\<^sub>o\<^sub>l\<^sub>e\<^sub>a\<^sub>n) -text{* In particular, it is strict, cp-preserving and const-preserving. In particular, -it generates the simplifier rules for terms like:*} +text\In particular, it is strict, cp-preserving and const-preserving. In particular, +it generates the simplifier rules for terms like:\ lemma "(invalid \ false) = invalid" by(simp) lemma "(invalid \ true) = invalid" by(simp) lemma "(false \ invalid) = invalid" by(simp) lemma "(true \ invalid) = invalid" by(simp) lemma "((invalid::('\)Boolean) \ invalid) = invalid" by(simp) -text{* Thus, the weak equality is \emph{not} reflexive. *} +text\Thus, the weak equality is \emph{not} reflexive.\ -subsection{* Test Statements on Boolean Operations. *} -text{* Here follows a list of code-examples, that explain the meanings -of the above definitions by compilation to code and execution to @{term "True"}.*} +subsection\Test Statements on Boolean Operations.\ +text\Here follows a list of code-examples, that explain the meanings +of the above definitions by compilation to code and execution to @{term "True"}.\ -text{* Elementary computations on Boolean *} +text\Elementary computations on Boolean\ Assert "\ \ \(true)" Assert "\ \ \(false)" Assert "\ |\ \(null)" diff --git a/Featherweight_OCL/basic_types/UML_Integer.thy b/Featherweight_OCL/basic_types/UML_Integer.thy index 66661dc..c4a36e1 100644 --- a/Featherweight_OCL/basic_types/UML_Integer.thy +++ b/Featherweight_OCL/basic_types/UML_Integer.thy @@ -44,13 +44,13 @@ theory UML_Integer imports "../UML_PropertyProfiles" begin -section{* Basic Type Integer: Operations *} +section\Basic Type Integer: Operations\ -subsection{* Fundamental Predicates on Integers: Strict Equality \label{sec:integer-strict-eq}*} +subsection\Fundamental Predicates on Integers: Strict Equality \label{sec:integer-strict-eq}\ -text{* The last basic operation belonging to the fundamental infrastructure +text\The last basic operation belonging to the fundamental infrastructure of a value-type in OCL is the weak equality, which is defined similar -to the @{typ "('\)Boolean"}-case as strict extension of the strong equality:*} +to the @{typ "('\)Boolean"}-case as strict extension of the strong equality:\ overloading StrictRefEq \ "StrictRefEq :: [('\)Integer,('\)Integer] \ ('\)Boolean" begin definition StrictRefEq\<^sub>I\<^sub>n\<^sub>t\<^sub>e\<^sub>g\<^sub>e\<^sub>r[code_unfold] : @@ -59,20 +59,20 @@ begin else invalid \" end -text{* Property proof in terms of @{term "profile_bin\<^sub>S\<^sub>t\<^sub>r\<^sub>o\<^sub>n\<^sub>g\<^sub>E\<^sub>q_\<^sub>v_\<^sub>v"}*} +text\Property proof in terms of @{term "profile_bin\<^sub>S\<^sub>t\<^sub>r\<^sub>o\<^sub>n\<^sub>g\<^sub>E\<^sub>q_\<^sub>v_\<^sub>v"}\ interpretation StrictRefEq\<^sub>I\<^sub>n\<^sub>t\<^sub>e\<^sub>g\<^sub>e\<^sub>r : profile_bin\<^sub>S\<^sub>t\<^sub>r\<^sub>o\<^sub>n\<^sub>g\<^sub>E\<^sub>q_\<^sub>v_\<^sub>v "\ x y. (x::('\)Integer) \ y" by unfold_locales (auto simp: StrictRefEq\<^sub>I\<^sub>n\<^sub>t\<^sub>e\<^sub>g\<^sub>e\<^sub>r) -subsection{* Basic Integer Constants *} +subsection\Basic Integer Constants\ -text{* Although the remaining part of this library reasons about -integers abstractly, we provide here as example some convenient shortcuts. *} +text\Although the remaining part of this library reasons about +integers abstractly, we provide here as example some convenient shortcuts.\ definition OclInt0 ::"('\)Integer" ("\") where "\ = (\ _ . \\0::int\\)" definition OclInt1 ::"('\)Integer" ("\") where "\ = (\ _ . \\1::int\\)" definition OclInt2 ::"('\)Integer" ("\") where "\ = (\ _ . \\2::int\\)" -text{* Etc. *} -text_raw{* \isatagafp *} +text\Etc.\ +text_raw\\isatagafp\ definition OclInt3 ::"('\)Integer" ("\") where "\ = (\ _ . \\3::int\\)" definition OclInt4 ::"('\)Integer" ("\") where "\ = (\ _ . \\4::int\\)" definition OclInt5 ::"('\)Integer" ("\") where "\ = (\ _ . \\5::int\\)" @@ -82,7 +82,7 @@ definition OclInt8 ::"('\)Integer" ("\") where "\ = (\)Integer" ("\") where "\ = (\ _ . \\9::int\\)" definition OclInt10 ::"('\)Integer" ("\\")where "\\ = (\ _ . \\10::int\\)" -subsection{* Validity and Definedness Properties *} +subsection\Validity and Definedness Properties\ lemma "\(null::('\)Integer) = false" by simp lemma "\(null::('\)Integer) = true" by simp @@ -109,18 +109,18 @@ lemma [simp,code_unfold]: "\ \ = true" by(simp add:OclInt8_def) lemma [simp,code_unfold]: "\ \ = true" by(simp add:OclInt9_def) lemma [simp,code_unfold]: "\ \ = true" by(simp add:OclInt9_def) -text_raw{* \endisatagafp *} +text_raw\\endisatagafp\ -subsection{* Arithmetical Operations *} +subsection\Arithmetical Operations\ -subsubsection{* Definition *} -text{* Here is a common case of a built-in operation on built-in types. -Note that the arguments must be both defined (non-null, non-bot). *} -text{* Note that we can not follow the lexis of the OCL Standard for Isabelle +subsubsection\Definition\ +text\Here is a common case of a built-in operation on built-in types. +Note that the arguments must be both defined (non-null, non-bot).\ +text\Note that we can not follow the lexis of the OCL Standard for Isabelle technical reasons; these operators are heavily overloaded in the HOL library that a further overloading would lead to heavy technical buzz in this document. -*} +\ definition OclAdd\<^sub>I\<^sub>n\<^sub>t\<^sub>e\<^sub>g\<^sub>e\<^sub>r ::"('\)Integer \ ('\)Integer \ ('\)Integer" (infix "+\<^sub>i\<^sub>n\<^sub>t" 40) where "x +\<^sub>i\<^sub>n\<^sub>t y \ \ \. if (\ x) \ = true \ \ (\ y) \ = true \ then \\\\x \\\ + \\y \\\\\ @@ -144,8 +144,8 @@ where "x *\<^sub>i\<^sub>n\<^sub>t y \ \ \. if (\ x) interpretation OclMult\<^sub>I\<^sub>n\<^sub>t\<^sub>e\<^sub>g\<^sub>e\<^sub>r : profile_bin\<^sub>d_\<^sub>d "OclMult\<^sub>I\<^sub>n\<^sub>t\<^sub>e\<^sub>g\<^sub>e\<^sub>r" "\ x y. \\\\x\\ * \\y\\\\" by unfold_locales (auto simp:OclMult\<^sub>I\<^sub>n\<^sub>t\<^sub>e\<^sub>g\<^sub>e\<^sub>r_def bot_option_def null_option_def) -text{* Here is the special case of division, which is defined as invalid for division -by zero. *} +text\Here is the special case of division, which is defined as invalid for division +by zero.\ definition OclDivision\<^sub>I\<^sub>n\<^sub>t\<^sub>e\<^sub>g\<^sub>e\<^sub>r ::"('\)Integer \ ('\)Integer \ ('\)Integer" (infix "div\<^sub>i\<^sub>n\<^sub>t" 45) where "x div\<^sub>i\<^sub>n\<^sub>t y \ \ \. if (\ x) \ = true \ \ (\ y) \ = true \ then if y \ \ OclInt0 \ then \\\\x \\\ div \\y \\\\\ else invalid \ @@ -173,14 +173,14 @@ where "x \\<^sub>i\<^sub>n\<^sub>t y \ \ \. if (\ interpretation OclLe\<^sub>I\<^sub>n\<^sub>t\<^sub>e\<^sub>g\<^sub>e\<^sub>r : profile_bin\<^sub>d_\<^sub>d "(\\<^sub>i\<^sub>n\<^sub>t)" "\ x y. \\\\x\\ \ \\y\\\\" by unfold_locales (auto simp:OclLe\<^sub>I\<^sub>n\<^sub>t\<^sub>e\<^sub>g\<^sub>e\<^sub>r_def bot_option_def null_option_def) -subsubsection{* Basic Properties *} +subsubsection\Basic Properties\ lemma OclAdd\<^sub>I\<^sub>n\<^sub>t\<^sub>e\<^sub>g\<^sub>e\<^sub>r_commute: "(X +\<^sub>i\<^sub>n\<^sub>t Y) = (Y +\<^sub>i\<^sub>n\<^sub>t X)" by(rule ext,auto simp:true_def false_def OclAdd\<^sub>I\<^sub>n\<^sub>t\<^sub>e\<^sub>g\<^sub>e\<^sub>r_def invalid_def split: option.split option.split_asm bool.split bool.split_asm) -subsubsection{* Execution with Invalid or Null or Zero as Argument *} +subsubsection\Execution with Invalid or Null or Zero as Argument\ lemma OclAdd\<^sub>I\<^sub>n\<^sub>t\<^sub>e\<^sub>g\<^sub>e\<^sub>r_zero1[simp,code_unfold] : "(x +\<^sub>i\<^sub>n\<^sub>t \) = (if \ x and not (\ x) then invalid else x endif)" @@ -214,9 +214,9 @@ by(subst OclAdd\<^sub>I\<^sub>n\<^sub>t\<^sub>e\<^sub>g\<^sub>e\<^sub>r_commute, -subsection{* Test Statements *} -text{* Here follows a list of code-examples, that explain the meanings -of the above definitions by compilation to code and execution to @{term "True"}.*} +subsection\Test Statements\ +text\Here follows a list of code-examples, that explain the meanings +of the above definitions by compilation to code and execution to @{term "True"}.\ Assert "\ \ ( \ \\<^sub>i\<^sub>n\<^sub>t \\ )" Assert "\ \ (( \ +\<^sub>i\<^sub>n\<^sub>t \ ) \\<^sub>i\<^sub>n\<^sub>t \\ )" @@ -250,11 +250,11 @@ lemma OclInt9_non_null [simp,code_unfold]: "(\ \ null) = false" by( lemma null_non_OclInt9 [simp,code_unfold]: "(null \ \) = false" by(simp add: OclInt9_def) -text{* Here follows a list of code-examples, that explain the meanings -of the above definitions by compilation to code and execution to @{term "True"}.*} +text\Here follows a list of code-examples, that explain the meanings +of the above definitions by compilation to code and execution to @{term "True"}.\ -text{* Elementary computations on Integer *} +text\Elementary computations on Integer\ Assert "\ \ ((\ <\<^sub>i\<^sub>n\<^sub>t \) and (\ <\<^sub>i\<^sub>n\<^sub>t \))" diff --git a/Featherweight_OCL/basic_types/UML_Real.thy b/Featherweight_OCL/basic_types/UML_Real.thy index 2c380c4..4f38c6f 100644 --- a/Featherweight_OCL/basic_types/UML_Real.thy +++ b/Featherweight_OCL/basic_types/UML_Real.thy @@ -44,13 +44,13 @@ theory UML_Real imports "../UML_PropertyProfiles" begin -section{* Basic Type Real: Operations *} +section\Basic Type Real: Operations\ -subsection{* Fundamental Predicates on Reals: Strict Equality \label{sec:real-strict-eq}*} +subsection\Fundamental Predicates on Reals: Strict Equality \label{sec:real-strict-eq}\ -text{* The last basic operation belonging to the fundamental infrastructure +text\The last basic operation belonging to the fundamental infrastructure of a value-type in OCL is the weak equality, which is defined similar -to the @{typ "('\)Boolean"}-case as strict extension of the strong equality:*} +to the @{typ "('\)Boolean"}-case as strict extension of the strong equality:\ overloading StrictRefEq \ "StrictRefEq :: [('\)Real,('\)Real] \ ('\)Boolean" begin definition StrictRefEq\<^sub>R\<^sub>e\<^sub>a\<^sub>l [code_unfold] : @@ -59,20 +59,20 @@ begin else invalid \" end -text{* Property proof in terms of @{term "profile_bin\<^sub>S\<^sub>t\<^sub>r\<^sub>o\<^sub>n\<^sub>g\<^sub>E\<^sub>q_\<^sub>v_\<^sub>v"}*} +text\Property proof in terms of @{term "profile_bin\<^sub>S\<^sub>t\<^sub>r\<^sub>o\<^sub>n\<^sub>g\<^sub>E\<^sub>q_\<^sub>v_\<^sub>v"}\ interpretation StrictRefEq\<^sub>R\<^sub>e\<^sub>a\<^sub>l : profile_bin\<^sub>S\<^sub>t\<^sub>r\<^sub>o\<^sub>n\<^sub>g\<^sub>E\<^sub>q_\<^sub>v_\<^sub>v "\ x y. (x::('\)Real) \ y" by unfold_locales (auto simp: StrictRefEq\<^sub>R\<^sub>e\<^sub>a\<^sub>l) -subsection{* Basic Real Constants *} +subsection\Basic Real Constants\ -text{* Although the remaining part of this library reasons about -reals abstractly, we provide here as example some convenient shortcuts. *} +text\Although the remaining part of this library reasons about +reals abstractly, we provide here as example some convenient shortcuts.\ definition OclReal0 ::"('\)Real" ("\.\") where "\.\ = (\ _ . \\0::real\\)" definition OclReal1 ::"('\)Real" ("\.\") where "\.\ = (\ _ . \\1::real\\)" definition OclReal2 ::"('\)Real" ("\.\") where "\.\ = (\ _ . \\2::real\\)" -text{* Etc. *} -text_raw{* \isatagafp *} +text\Etc.\ +text_raw\\isatagafp\ definition OclReal3 ::"('\)Real" ("\.\") where "\.\ = (\ _ . \\3::real\\)" definition OclReal4 ::"('\)Real" ("\.\") where "\.\ = (\ _ . \\4::real\\)" definition OclReal5 ::"('\)Real" ("\.\") where "\.\ = (\ _ . \\5::real\\)" @@ -83,7 +83,7 @@ definition OclReal9 ::"('\)Real" ("\.\") where "\.\ definition OclReal10 ::"('\)Real" ("\\.\") where "\\.\ = (\ _ . \\10::real\\)" definition OclRealpi ::"('\)Real" ("\") where "\ = (\ _ . \\pi\\)" -subsection{* Validity and Definedness Properties *} +subsection\Validity and Definedness Properties\ lemma "\(null::('\)Real) = false" by simp lemma "\(null::('\)Real) = true" by simp @@ -109,18 +109,18 @@ lemma [simp,code_unfold]: "\ \.\ = true" by(simp add:OclReal lemma [simp,code_unfold]: "\ \.\ = true" by(simp add:OclReal8_def) lemma [simp,code_unfold]: "\ \.\ = true" by(simp add:OclReal9_def) lemma [simp,code_unfold]: "\ \.\ = true" by(simp add:OclReal9_def) -text_raw{* \endisatagafp *} +text_raw\\endisatagafp\ -subsection{* Arithmetical Operations *} +subsection\Arithmetical Operations\ -subsubsection{* Definition *} -text{* Here is a common case of a built-in operation on built-in types. -Note that the arguments must be both defined (non-null, non-bot). *} -text{* Note that we can not follow the lexis of the OCL Standard for Isabelle +subsubsection\Definition\ +text\Here is a common case of a built-in operation on built-in types. +Note that the arguments must be both defined (non-null, non-bot).\ +text\Note that we can not follow the lexis of the OCL Standard for Isabelle technical reasons; these operators are heavily overloaded in the HOL library that a further overloading would lead to heavy technical buzz in this document. -*} +\ definition OclAdd\<^sub>R\<^sub>e\<^sub>a\<^sub>l ::"('\)Real \ ('\)Real \ ('\)Real" (infix "+\<^sub>r\<^sub>e\<^sub>a\<^sub>l" 40) where "x +\<^sub>r\<^sub>e\<^sub>a\<^sub>l y \ \ \. if (\ x) \ = true \ \ (\ y) \ = true \ then \\\\x \\\ + \\y \\\\\ @@ -144,8 +144,8 @@ where "x *\<^sub>r\<^sub>e\<^sub>a\<^sub>l y \ \ \. if (\R\<^sub>e\<^sub>a\<^sub>l : profile_bin\<^sub>d_\<^sub>d "OclMult\<^sub>R\<^sub>e\<^sub>a\<^sub>l" "\ x y. \\\\x\\ * \\y\\\\" by unfold_locales (auto simp:OclMult\<^sub>R\<^sub>e\<^sub>a\<^sub>l_def bot_option_def null_option_def) -text{* Here is the special case of division, which is defined as invalid for division -by zero. *} +text\Here is the special case of division, which is defined as invalid for division +by zero.\ definition OclDivision\<^sub>R\<^sub>e\<^sub>a\<^sub>l ::"('\)Real \ ('\)Real \ ('\)Real" (infix "div\<^sub>r\<^sub>e\<^sub>a\<^sub>l" 45) where "x div\<^sub>r\<^sub>e\<^sub>a\<^sub>l y \ \ \. if (\ x) \ = true \ \ (\ y) \ = true \ then if y \ \ OclReal0 \ then \\\\x \\\ / \\y \\\\\ else invalid \ @@ -174,14 +174,14 @@ where "x \\<^sub>r\<^sub>e\<^sub>a\<^sub>l y \ \ \. if ( interpretation OclLe\<^sub>R\<^sub>e\<^sub>a\<^sub>l : profile_bin\<^sub>d_\<^sub>d "(\\<^sub>r\<^sub>e\<^sub>a\<^sub>l)" "\ x y. \\\\x\\ \ \\y\\\\" by unfold_locales (auto simp:OclLe\<^sub>R\<^sub>e\<^sub>a\<^sub>l_def bot_option_def null_option_def) -subsubsection{* Basic Properties *} +subsubsection\Basic Properties\ lemma OclAdd\<^sub>R\<^sub>e\<^sub>a\<^sub>l_commute: "(X +\<^sub>r\<^sub>e\<^sub>a\<^sub>l Y) = (Y +\<^sub>r\<^sub>e\<^sub>a\<^sub>l X)" by(rule ext,auto simp:true_def false_def OclAdd\<^sub>R\<^sub>e\<^sub>a\<^sub>l_def invalid_def split: option.split option.split_asm bool.split bool.split_asm) -subsubsection{* Execution with Invalid or Null or Zero as Argument *} +subsubsection\Execution with Invalid or Null or Zero as Argument\ lemma OclAdd\<^sub>R\<^sub>e\<^sub>a\<^sub>l_zero1[simp,code_unfold] : "(x +\<^sub>r\<^sub>e\<^sub>a\<^sub>l \.\) = (if \ x and not (\ x) then invalid else x endif)" @@ -215,9 +215,9 @@ by(subst OclAdd\<^sub>R\<^sub>e\<^sub>a\<^sub>l_commute, simp) -subsection{* Test Statements *} -text{* Here follows a list of code-examples, that explain the meanings -of the above definitions by compilation to code and execution to @{term "True"}.*} +subsection\Test Statements\ +text\Here follows a list of code-examples, that explain the meanings +of the above definitions by compilation to code and execution to @{term "True"}.\ Assert "\ \ ( \.\ \\<^sub>r\<^sub>e\<^sub>a\<^sub>l \\.\ )" Assert "\ \ (( \.\ +\<^sub>r\<^sub>e\<^sub>a\<^sub>l \.\ ) \\<^sub>r\<^sub>e\<^sub>a\<^sub>l \\.\ )" @@ -251,11 +251,11 @@ lemma OclReal9_non_null [simp,code_unfold]: "(\.\ \ null) = f lemma null_non_OclReal9 [simp,code_unfold]: "(null \ \.\) = false" by(simp add: OclReal9_def) -text{* Here follows a list of code-examples, that explain the meanings -of the above definitions by compilation to code and execution to @{term "True"}.*} +text\Here follows a list of code-examples, that explain the meanings +of the above definitions by compilation to code and execution to @{term "True"}.\ -text{* Elementary computations on Real *} +text\Elementary computations on Real\ Assert "\ \ \.\ <> \.\" Assert "\ \ \.\ <> \.\" diff --git a/Featherweight_OCL/basic_types/UML_String.thy b/Featherweight_OCL/basic_types/UML_String.thy index 4354d4f..7ac03a0 100644 --- a/Featherweight_OCL/basic_types/UML_String.thy +++ b/Featherweight_OCL/basic_types/UML_String.thy @@ -44,13 +44,13 @@ theory UML_String imports "../UML_PropertyProfiles" begin -section{* Basic Type String: Operations *} +section\Basic Type String: Operations\ -subsection{* Fundamental Properties on Strings: Strict Equality \label{sec:string-strict-eq}*} +subsection\Fundamental Properties on Strings: Strict Equality \label{sec:string-strict-eq}\ -text{* The last basic operation belonging to the fundamental infrastructure +text\The last basic operation belonging to the fundamental infrastructure of a value-type in OCL is the weak equality, which is defined similar -to the @{typ "('\)Boolean"}-case as strict extension of the strong equality:*} +to the @{typ "('\)Boolean"}-case as strict extension of the strong equality:\ overloading StrictRefEq \ "StrictRefEq :: [('\)String,('\)String] \ ('\)Boolean" begin definition StrictRefEq\<^sub>S\<^sub>t\<^sub>r\<^sub>i\<^sub>n\<^sub>g[code_unfold] : @@ -59,22 +59,22 @@ begin else invalid \" end -text{* Property proof in terms of @{term "profile_bin\<^sub>S\<^sub>t\<^sub>r\<^sub>o\<^sub>n\<^sub>g\<^sub>E\<^sub>q_\<^sub>v_\<^sub>v"}*} +text\Property proof in terms of @{term "profile_bin\<^sub>S\<^sub>t\<^sub>r\<^sub>o\<^sub>n\<^sub>g\<^sub>E\<^sub>q_\<^sub>v_\<^sub>v"}\ interpretation StrictRefEq\<^sub>S\<^sub>t\<^sub>r\<^sub>i\<^sub>n\<^sub>g : profile_bin\<^sub>S\<^sub>t\<^sub>r\<^sub>o\<^sub>n\<^sub>g\<^sub>E\<^sub>q_\<^sub>v_\<^sub>v "\ x y. (x::('\)String) \ y" by unfold_locales (auto simp: StrictRefEq\<^sub>S\<^sub>t\<^sub>r\<^sub>i\<^sub>n\<^sub>g) -subsection{* Basic String Constants *} +subsection\Basic String Constants\ -text{* Although the remaining part of this library reasons about -integers abstractly, we provide here as example some convenient shortcuts. *} +text\Although the remaining part of this library reasons about +integers abstractly, we provide here as example some convenient shortcuts.\ definition OclStringa ::"('\)String" ("\") where "\ = (\ _ . \\''a''\\)" definition OclStringb ::"('\)String" ("\") where "\ = (\ _ . \\''b''\\)" definition OclStringc ::"('\)String" ("\") where "\ = (\ _ . \\''c''\\)" -text{* Etc.*} -text_raw{* \isatagafp *} +text\Etc.\ +text_raw\\isatagafp\ -subsection{* Validity and Definedness Properties *} +subsection\Validity and Definedness Properties\ lemma "\(null::('\)String) = false" by simp lemma "\(null::('\)String) = true" by simp @@ -90,18 +90,18 @@ by(simp add:valid_def true_def (* ecclectic proofs to make examples executable *) lemma [simp,code_unfold]: "\ \ = true" by(simp add:OclStringa_def) lemma [simp,code_unfold]: "\ \ = true" by(simp add:OclStringa_def) -text_raw{* \endisatagafp *} +text_raw\\endisatagafp\ -subsection{* String Operations *} +subsection\String Operations\ -subsubsection{* Definition *} -text{* Here is a common case of a built-in operation on built-in types. -Note that the arguments must be both defined (non-null, non-bot). *} -text{* Note that we can not follow the lexis of the OCL Standard for Isabelle +subsubsection\Definition\ +text\Here is a common case of a built-in operation on built-in types. +Note that the arguments must be both defined (non-null, non-bot).\ +text\Note that we can not follow the lexis of the OCL Standard for Isabelle technical reasons; these operators are heavily overloaded in the HOL library that a further overloading would lead to heavy technical buzz in this document. -*} +\ definition OclAdd\<^sub>S\<^sub>t\<^sub>r\<^sub>i\<^sub>n\<^sub>g ::"('\)String \ ('\)String \ ('\)String" (infix "+\<^sub>s\<^sub>t\<^sub>r\<^sub>i\<^sub>n\<^sub>g" 40) where "x +\<^sub>s\<^sub>t\<^sub>r\<^sub>i\<^sub>n\<^sub>g y \ \ \. if (\ x) \ = true \ \ (\ y) \ = true \ then \\concat [\\x \\\, \\y \\\]\\ @@ -112,7 +112,7 @@ interpretation OclAdd\<^sub>S\<^sub>t\<^sub>r\<^sub>i\<^sub>n\<^sub>g : profile_ (* TODO : size(), concat, substring(s:string) toInteger, toReal, at(i:Integer), characters() etc. *) -subsubsection{* Basic Properties *} +subsubsection\Basic Properties\ lemma OclAdd\<^sub>S\<^sub>t\<^sub>r\<^sub>i\<^sub>n\<^sub>g_not_commute: "\X Y. (X +\<^sub>s\<^sub>t\<^sub>r\<^sub>i\<^sub>n\<^sub>g Y) \ (Y +\<^sub>s\<^sub>t\<^sub>r\<^sub>i\<^sub>n\<^sub>g X)" apply(rule_tac x = "\_. \\''b''\\" in exI) @@ -121,9 +121,9 @@ lemma OclAdd\<^sub>S\<^sub>t\<^sub>r\<^sub>i\<^sub>n\<^sub>g_not_commute: "\Test Statements\ +text\Here follows a list of code-examples, that explain the meanings +of the above definitions by compilation to code and execution to @{term "True"}.\ (* Assert "\ \ ( \ \\<^sub>s\<^sub>t\<^sub>r\<^sub>i\<^sub>n\<^sub>g \\ )" Assert "\ \ (( \ +\<^sub>s\<^sub>t\<^sub>r\<^sub>i\<^sub>n\<^sub>g \ ) \\<^sub>s\<^sub>t\<^sub>r\<^sub>i\<^sub>n\<^sub>g \\ )" @@ -131,11 +131,11 @@ Assert "\ |\ (( \ +\<^sub>s\<^sub>t\<^sub>r\<^sub>i\<^sub>n\<^ Assert "\ \ not (\ (null +\<^sub>s\<^sub>t\<^sub>r\<^sub>i\<^sub>n\<^sub>g \)) " *) -text{* Here follows a list of code-examples, that explain the meanings -of the above definitions by compilation to code and execution to @{term "True"}.*} +text\Here follows a list of code-examples, that explain the meanings +of the above definitions by compilation to code and execution to @{term "True"}.\ -text{* Elementary computations on String *} +text\Elementary computations on String\ Assert "\ \ \ <> \" Assert "\ \ \ <> \" diff --git a/Featherweight_OCL/basic_types/UML_Void.thy b/Featherweight_OCL/basic_types/UML_Void.thy index 35e5678..0a5c21c 100644 --- a/Featherweight_OCL/basic_types/UML_Void.thy +++ b/Featherweight_OCL/basic_types/UML_Void.thy @@ -44,18 +44,18 @@ theory UML_Void imports "../UML_PropertyProfiles" begin -section{* Basic Type Void: Operations *} +section\Basic Type Void: Operations\ (* For technical reasons, the type does not contain to the null-class yet. *) -text {* This \emph{minimal} OCL type contains only two elements: +text \This \emph{minimal} OCL type contains only two elements: @{term "invalid"} and @{term "null"}. @{term "Void"} could initially be defined as @{typ "unit option option"}, however the cardinal of this type is more than two, so it would have the cost to consider - @{text "Some None"} and @{text "Some (Some ())"} seemingly everywhere.*} + \Some None\ and \Some (Some ())\ seemingly everywhere.\ -subsection{* Fundamental Properties on Voids: Strict Equality *} +subsection\Fundamental Properties on Voids: Strict Equality\ -subsubsection{* Definition *} +subsubsection\Definition\ instantiation Void\<^sub>b\<^sub>a\<^sub>s\<^sub>e :: bot begin @@ -81,9 +81,9 @@ begin end -text{* The last basic operation belonging to the fundamental infrastructure +text\The last basic operation belonging to the fundamental infrastructure of a value-type in OCL is the weak equality, which is defined similar -to the @{typ "('\)Void"}-case as strict extension of the strong equality:*} +to the @{typ "('\)Void"}-case as strict extension of the strong equality:\ overloading StrictRefEq \ "StrictRefEq :: [('\)Void,('\)Void] \ ('\)Boolean" begin definition StrictRefEq\<^sub>V\<^sub>o\<^sub>i\<^sub>d[code_unfold] : @@ -92,15 +92,15 @@ begin else invalid \" end -text{* Property proof in terms of @{term "profile_bin\<^sub>S\<^sub>t\<^sub>r\<^sub>o\<^sub>n\<^sub>g\<^sub>E\<^sub>q_\<^sub>v_\<^sub>v"}*} +text\Property proof in terms of @{term "profile_bin\<^sub>S\<^sub>t\<^sub>r\<^sub>o\<^sub>n\<^sub>g\<^sub>E\<^sub>q_\<^sub>v_\<^sub>v"}\ interpretation StrictRefEq\<^sub>V\<^sub>o\<^sub>i\<^sub>d : profile_bin\<^sub>S\<^sub>t\<^sub>r\<^sub>o\<^sub>n\<^sub>g\<^sub>E\<^sub>q_\<^sub>v_\<^sub>v "\ x y. (x::('\)Void) \ y" by unfold_locales (auto simp: StrictRefEq\<^sub>V\<^sub>o\<^sub>i\<^sub>d) -subsection{* Basic Void Constants *} +subsection\Basic Void Constants\ -subsection{* Validity and Definedness Properties *} +subsection\Validity and Definedness Properties\ lemma "\(null::('\)Void) = false" by simp lemma "\(null::('\)Void) = true" by simp @@ -130,7 +130,7 @@ apply(rule ext, simp split:, intro conjI impI) by(metis null_Void_def null_is_valid, simp add: true_def) -subsection{* Test Statements *} +subsection\Test Statements\ Assert "\ \ ((null::('\)Void) \ null)" diff --git a/Featherweight_OCL/collection_types/UML_Bag.thy b/Featherweight_OCL/collection_types/UML_Bag.thy index 545967a..50edd48 100644 --- a/Featherweight_OCL/collection_types/UML_Bag.thy +++ b/Featherweight_OCL/collection_types/UML_Bag.thy @@ -50,7 +50,7 @@ imports "../basic_types/UML_Void" begin no_notation None ("\") -section{* Collection Type Bag: Operations *} +section\Collection Type Bag: Operations\ definition "Rep_Bag_base' x = {(x0, y). y < \\Rep_Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e x\\ x0 }" definition "Rep_Bag_base x \ = {(x0, y). y < \\Rep_Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e (x \)\\ x0 }" @@ -60,10 +60,10 @@ definition ApproxEq (infixl "\" 30) where "X \ Y \ \ \. \\Rep_Set_base X \ = Rep_Set_base Y \ \\" -subsection{* As a Motivation for the (infinite) Type Construction: Type-Extensions as Bags - \label{sec:type-extensions}*} +subsection\As a Motivation for the (infinite) Type Construction: Type-Extensions as Bags + \label{sec:type-extensions}\ -text{* Our notion of typed bag goes beyond the usual notion of a finite executable bag and +text\Our notion of typed bag goes beyond the usual notion of a finite executable bag and is powerful enough to capture \emph{the extension of a type} in UML and OCL. This means we can have in Featherweight OCL Bags containing all possible elements of a type, not only those (finite) ones representable in a state. This holds for base types as well as class types, @@ -77,9 +77,9 @@ In a world with @{term invalid} and @{term null}, there are two notions extensio \item the bag of all \emph{valid} values of a type @{term T}, so including @{term null} (for which we will introduce the constant @{term T\<^sub>n\<^sub>u\<^sub>l\<^sub>l}). \end{enumerate} -*} +\ -text{* We define the bag extensions for the base type @{term Integer} as follows: *} +text\We define the bag extensions for the base type @{term Integer} as follows:\ definition Integer :: "('\,Integer\<^sub>b\<^sub>a\<^sub>s\<^sub>e) Bag" where "Integer \ (\ \. (Abs_Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e o Some o Some) (\ None \ 0 | Some None \ 0 | _ \ 1))" @@ -96,20 +96,20 @@ apply(rule ext, auto simp: Integer\<^sub>n\<^sub>u\<^sub>l\<^sub>l_def defined_d bot_fun_def null_fun_def null_option_def) by(simp_all add: Abs_Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e_inject bot_option_def bot_Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e_def null_Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e_def null_option_def) -text{* This allows the theorems: +text\This allows the theorems: - @{text "\ \ \ x \ \ \ (Integer->includes\<^sub>B\<^sub>a\<^sub>g(x))"} - @{text "\ \ \ x \ \ \ Integer \ (Integer->including\<^sub>B\<^sub>a\<^sub>g(x))"} + \\ \ \ x \ \ \ (Integer->includes\<^sub>B\<^sub>a\<^sub>g(x))\ + \\ \ \ x \ \ \ Integer \ (Integer->including\<^sub>B\<^sub>a\<^sub>g(x))\ and - @{text "\ \ \ x \ \ \ (Integer\<^sub>n\<^sub>u\<^sub>l\<^sub>l->includes\<^sub>B\<^sub>a\<^sub>g(x))"} - @{text "\ \ \ x \ \ \ Integer\<^sub>n\<^sub>u\<^sub>l\<^sub>l \ (Integer\<^sub>n\<^sub>u\<^sub>l\<^sub>l->including\<^sub>B\<^sub>a\<^sub>g(x))"} + \\ \ \ x \ \ \ (Integer\<^sub>n\<^sub>u\<^sub>l\<^sub>l->includes\<^sub>B\<^sub>a\<^sub>g(x))\ + \\ \ \ x \ \ \ Integer\<^sub>n\<^sub>u\<^sub>l\<^sub>l \ (Integer\<^sub>n\<^sub>u\<^sub>l\<^sub>l->including\<^sub>B\<^sub>a\<^sub>g(x))\ which characterize the infiniteness of these bags by a recursive property on these bags. -*} +\ -text{* In the same spirit, we proceed similarly for the remaining base types: *} +text\In the same spirit, we proceed similarly for the remaining base types:\ definition Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l :: "('\,Void\<^sub>b\<^sub>a\<^sub>s\<^sub>e) Bag" where "Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l \ (\ \. (Abs_Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e o Some o Some) (\ x. if x = Abs_Void\<^sub>b\<^sub>a\<^sub>s\<^sub>e (Some None) then 1 else 0))" @@ -220,9 +220,9 @@ apply(rule ext, auto simp: Real\<^sub>n\<^sub>u\<^sub>l\<^sub>l_def defined_def bot_fun_def null_fun_def null_option_def) by(simp_all add: Abs_Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e_inject bot_option_def bot_Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e_def null_Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e_def null_option_def) -subsection{* Basic Properties of the Bag Type*} +subsection\Basic Properties of the Bag Type\ -text{* Every element in a defined bag is valid. *} +text\Every element in a defined bag is valid.\ lemma Bag_inv_lemma: "\ \ (\ X) \ \\Rep_Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e (X \)\\ bot = 0" apply(insert Rep_Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e [of "X \"], simp) @@ -271,18 +271,18 @@ apply(simp add: valid_def null_fun_def bot_fun_def bot_Bag\<^sub>b\<^sub>a\<^sub apply(subst Abs_Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e_inject,simp_all add: null_option_def bot_option_def) done -text{* ... which means that we can have a type @{text "('\,('\,('\) Integer) Bag) Bag"} +text\... which means that we can have a type \('\,('\,('\) Integer) Bag) Bag\ corresponding exactly to Bag(Bag(Integer)) in OCL notation. Note that the parameter -@{text "'\"} still refers to the object universe; making the OCL semantics entirely parametric +\'\\ still refers to the object universe; making the OCL semantics entirely parametric in the object universe makes it possible to study (and prove) its properties -independently from a concrete class diagram. *} +independently from a concrete class diagram.\ -subsection{* Definition: Strict Equality \label{sec:bag-strict-equality}*} +subsection\Definition: Strict Equality \label{sec:bag-strict-equality}\ -text{* After the part of foundational operations on bags, we detail here equality on bags. +text\After the part of foundational operations on bags, we detail here equality on bags. Strong equality is inherited from the OCL core, but we have to consider the case of the strict equality. We decide to overload strict equality in the -same way we do for other value's in OCL:*} +same way we do for other value's in OCL:\ overloading StrictRefEq \ "StrictRefEq :: [('\,'\::null)Bag,('\,'\::null)Bag] \ ('\)Boolean" begin @@ -292,20 +292,20 @@ begin else invalid \" end -text{* One might object here that for the case of objects, this is an empty definition. +text\One might object here that for the case of objects, this is an empty definition. The answer is no, we will restrain later on states and objects such that any object has its oid stored inside the object (so the ref, under which an object can be referenced in the store will represented in the object itself). For such well-formed stores that satisfy this invariant (the WFF-invariant), the referential equality and the -strong equality---and therefore the strict equality on bags in the sense above---coincides.*} +strong equality---and therefore the strict equality on bags in the sense above---coincides.\ -text{* Property proof in terms of @{term "profile_bin\<^sub>S\<^sub>t\<^sub>r\<^sub>o\<^sub>n\<^sub>g\<^sub>E\<^sub>q_\<^sub>v_\<^sub>v"}*} +text\Property proof in terms of @{term "profile_bin\<^sub>S\<^sub>t\<^sub>r\<^sub>o\<^sub>n\<^sub>g\<^sub>E\<^sub>q_\<^sub>v_\<^sub>v"}\ interpretation StrictRefEq\<^sub>B\<^sub>a\<^sub>g : profile_bin\<^sub>S\<^sub>t\<^sub>r\<^sub>o\<^sub>n\<^sub>g\<^sub>E\<^sub>q_\<^sub>v_\<^sub>v "\ x y. (x::('\,'\::null)Bag) \ y" by unfold_locales (auto simp: StrictRefEq\<^sub>B\<^sub>a\<^sub>g) -subsection{* Constants: mtBag *} +subsection\Constants: mtBag\ definition mtBag::"('\,'\::null) Bag" ("Bag{}") where "Bag{} \ (\ \. Abs_Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e \\\_. 0::nat\\ )" @@ -324,18 +324,18 @@ lemma mtBag_rep_bag: "\\Rep_Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e (B apply(simp add: mtBag_def, subst Abs_Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e_inverse) by(simp add: bot_option_def)+ -text_raw{* \isatagafp *} +text_raw\\isatagafp\ lemma [simp,code_unfold]: "const Bag{}" by(simp add: const_def mtBag_def) -text{* Note that the collection types in OCL allow for null to be included; - however, there is the null-collection into which inclusion yields invalid. *} +text\Note that the collection types in OCL allow for null to be included; + however, there is the null-collection into which inclusion yields invalid.\ -text_raw{* \endisatagafp *} +text_raw\\endisatagafp\ -subsection{* Definition: Including *} +subsection\Definition: Including\ definition OclIncluding :: "[('\,'\::null) Bag,('\,'\) val] \ ('\,'\) Bag" where "OclIncluding x y = (\ \. if (\ x) \ = true \ \ (\ y) \ = true \ @@ -365,7 +365,7 @@ translations "Bag{x}" == "CONST OclIncluding (Bag{}) x " -subsection{* Definition: Excluding *} +subsection\Definition: Excluding\ definition OclExcluding :: "[('\,'\::null) Bag,('\,'\) val] \ ('\,'\) Bag" where "OclExcluding x y = (\ \. if (\ x) \ = true \ \ (\ y) \ = true \ @@ -386,7 +386,7 @@ proof - mem_Collect_eq null_option_def)+ qed -subsection{* Definition: Includes *} +subsection\Definition: Includes\ definition OclIncludes :: "[('\,'\::null) Bag,('\,'\) val] \ '\ Boolean" where "OclIncludes x y = (\ \. if (\ x) \ = true \ \ (\ y) \ = true \ @@ -397,21 +397,21 @@ notation OclIncludes ("_->includes\<^sub>B\<^sub>a\<^sub>g'(_')" (*[66,65]6 interpretation OclIncludes : profile_bin\<^sub>d_\<^sub>v OclIncludes "\x y. \\ \\Rep_Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e x\\ y > 0 \\" by(unfold_locales, auto simp:OclIncludes_def bot_option_def null_option_def invalid_def) -subsection{* Definition: Excludes *} +subsection\Definition: Excludes\ definition OclExcludes :: "[('\,'\::null) Bag,('\,'\) val] \ '\ Boolean" where "OclExcludes x y = (not(OclIncludes x y))" notation OclExcludes ("_->excludes\<^sub>B\<^sub>a\<^sub>g'(_')" (*[66,65]65*)) -text{* The case of the size definition is somewhat special, we admit +text\The case of the size definition is somewhat special, we admit explicitly in Featherweight OCL the possibility of infinite bags. For the size definition, this requires an extra condition that assures -that the cardinality of the bag is actually a defined integer. *} +that the cardinality of the bag is actually a defined integer.\ interpretation OclExcludes : profile_bin\<^sub>d_\<^sub>v OclExcludes "\x y. \\ \\Rep_Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e x\\ y \ 0 \\" by(unfold_locales, auto simp:OclExcludes_def OclIncludes_def OclNot_def bot_option_def null_option_def invalid_def) -subsection{* Definition: Size *} +subsection\Definition: Size\ definition OclSize :: "('\,'\::null)Bag \ '\ Integer" where "OclSize x = (\ \. if (\ x) \ = true \ \ finite (Rep_Bag_base x \) @@ -420,16 +420,16 @@ where "OclSize x = (\ \. if (\ x) \ = true \ \ notation (* standard ascii syntax *) OclSize ("_->size\<^sub>B\<^sub>a\<^sub>g'(')" (*[66]*)) -text{* The following definition follows the requirement of the +text\The following definition follows the requirement of the standard to treat null as neutral element of bags. It is a well-documented exception from the general strictness rule and the rule that the distinguished argument self should -be non-null. *} +be non-null.\ (*TODO Locale - Equivalent*) -subsection{* Definition: IsEmpty *} +subsection\Definition: IsEmpty\ definition OclIsEmpty :: "('\,'\::null) Bag \ '\ Boolean" where "OclIsEmpty x = ((\ x and not (\ x)) or ((OclSize x) \ \))" @@ -437,7 +437,7 @@ notation OclIsEmpty ("_->isEmpty\<^sub>B\<^sub>a\<^sub>g'(')" (*[66]*)) (*TODO Locale - Equivalent*) -subsection{* Definition: NotEmpty *} +subsection\Definition: NotEmpty\ definition OclNotEmpty :: "('\,'\::null) Bag \ '\ Boolean" where "OclNotEmpty x = not(OclIsEmpty x)" @@ -445,7 +445,7 @@ notation OclNotEmpty ("_->notEmpty\<^sub>B\<^sub>a\<^sub>g'(')" (*[66]*)) (*TODO Locale - Equivalent*) -subsection{* Definition: Any *} +subsection\Definition: Any\ (* Slight breach of naming convention in order to avoid naming conflict on constant.*) definition OclANY :: "[('\,'\::null) Bag] \ ('\,'\) val" @@ -464,10 +464,10 @@ source->any\<^sub>B\<^sub>a\<^sub>g(iterator | body) = source->select(iterator | body)->asSequence()->first(). Since we don't have sequences, we have to go for a direct---restricted---definition. *) -subsection{* Definition: Forall *} +subsection\Definition: Forall\ -text{* The definition of OclForall mimics the one of @{term "OclAnd"}: -OclForall is not a strict operation. *} +text\The definition of OclForall mimics the one of @{term "OclAnd"}: +OclForall is not a strict operation.\ definition OclForall :: "[('\,'\::null)Bag,('\,'\)val\('\)Boolean] \ '\ Boolean" where "OclForall S P = (\ \. if (\ S) \ = true \ then if (\x\Rep_Set_base S \. P (\_. x) \ = false \) @@ -485,9 +485,9 @@ translations (*TODO Locale - Equivalent*) -subsection{* Definition: Exists *} +subsection\Definition: Exists\ -text{* Like OclForall, OclExists is also not strict. *} +text\Like OclForall, OclExists is also not strict.\ definition OclExists :: "[('\,'\::null) Bag,('\,'\)val\('\)Boolean] \ '\ Boolean" where "OclExists S P = not(UML_Bag.OclForall S (\ X. not (P X)))" @@ -498,7 +498,7 @@ translations (*TODO Locale - Equivalent*) -subsection{* Definition: Iterate *} +subsection\Definition: Iterate\ definition OclIterate :: "[('\,'\::null) Bag,('\,'\::null)val, ('\,'\)val\('\,'\)val\('\,'\)val] \ ('\,'\)val" @@ -513,7 +513,7 @@ translations (*TODO Locale - Equivalent*) -subsection{* Definition: Select *} +subsection\Definition: Select\ definition OclSelect :: "[('\,'\::null)Bag,('\,'\)val\('\)Boolean] \ ('\,'\)Bag" @@ -534,7 +534,7 @@ translations (*TODO Locale - Equivalent*) -subsection{* Definition: Reject *} +subsection\Definition: Reject\ definition OclReject :: "[('\,'\::null)Bag,('\,'\)val\('\)Boolean] \ ('\,'\::null)Bag" where "OclReject S P = OclSelect S (not o P)" @@ -545,7 +545,7 @@ translations (*TODO Locale - Equivalent*) -subsection{* Definition: IncludesAll *} +subsection\Definition: IncludesAll\ definition OclIncludesAll :: "[('\,'\::null) Bag,('\,'\) Bag] \ '\ Boolean" where "OclIncludesAll x y = (\ \. if (\ x) \ = true \ \ (\ y) \ = true \ @@ -557,7 +557,7 @@ interpretation OclIncludesAll : profile_bin\<^sub>d_\<^sub>d OclIncludesAll "\Definition: ExcludesAll\ definition OclExcludesAll :: "[('\,'\::null) Bag,('\,'\) Bag] \ '\ Boolean" where "OclExcludesAll x y = (\ \. if (\ x) \ = true \ \ (\ y) \ = true \ @@ -569,7 +569,7 @@ interpretation OclExcludesAll : profile_bin\<^sub>d_\<^sub>d OclExcludesAll "\Definition: Union\ definition OclUnion :: "[('\,'\::null) Bag,('\,'\) Bag] \ ('\,'\) Bag" where "OclUnion x y = (\ \. if (\ x) \ = true \ \ (\ y) \ = true \ @@ -592,7 +592,7 @@ proof - null_option_def)+ qed -subsection{* Definition: Intersection *} +subsection\Definition: Intersection\ definition OclIntersection :: "[('\,'\::null) Bag,('\,'\) Bag] \ ('\,'\) Bag" where "OclIntersection x y = (\ \. if (\ x) \ = true \ \ (\ y) \ = true \ @@ -616,7 +616,7 @@ proof - null_option_def)+ qed -subsection{* Definition: Count *} +subsection\Definition: Count\ definition OclCount :: "[('\,'\::null) Bag,('\,'\) val] \ ('\) Integer" where "OclCount x y = (\ \. if (\ x) \ = true \ \ (\ y) \ = true \ @@ -627,16 +627,16 @@ notation OclCount ("_->count\<^sub>B\<^sub>a\<^sub>g'(_')" (*[66,65]65*)) interpretation OclCount : profile_bin\<^sub>d_\<^sub>d OclCount "\x y. \\int(\\Rep_Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e x\\ y)\\" by(unfold_locales, auto simp:OclCount_def bot_option_def null_option_def) -subsection{* Definition (future operators) *} +subsection\Definition (future operators)\ consts (* abstract bag collection operations *) OclSum :: " ('\,'\::null) Bag \ '\ Integer" notation OclSum ("_->sum\<^sub>B\<^sub>a\<^sub>g'(')" (*[66]*)) -subsection{* Logical Properties *} +subsection\Logical Properties\ -text{* OclIncluding *} +text\OclIncluding\ lemma OclIncluding_valid_args_valid: "(\ \ \(X->including\<^sub>B\<^sub>a\<^sub>g(x))) = ((\ \(\ X)) \ (\ \(\ x)))" @@ -646,10 +646,10 @@ lemma OclIncluding_valid_args_valid''[simp,code_unfold]: "\(X->including\<^sub>B\<^sub>a\<^sub>g(x)) = ((\ X) and (\ x))" by (simp add: OclIncluding.def_valid_then_def) -text{* etc. etc. *} -text_raw{* \isatagafp *} +text\etc. etc.\ +text_raw\\isatagafp\ -text{* OclExcluding *} +text\OclExcluding\ lemma OclExcluding_valid_args_valid: "(\ \ \(X->excluding\<^sub>B\<^sub>a\<^sub>g(x))) = ((\ \(\ X)) \ (\ \(\ x)))" @@ -659,7 +659,7 @@ lemma OclExcluding_valid_args_valid''[simp,code_unfold]: "\(X->excluding\<^sub>B\<^sub>a\<^sub>g(x)) = ((\ X) and (\ x))" by (simp add: OclExcluding.def_valid_then_def) -text{* OclIncludes *} +text\OclIncludes\ lemma OclIncludes_valid_args_valid: "(\ \ \(X->includes\<^sub>B\<^sub>a\<^sub>g(x))) = ((\ \(\ X)) \ (\ \(\ x)))" @@ -669,7 +669,7 @@ lemma OclIncludes_valid_args_valid''[simp,code_unfold]: "\(X->includes\<^sub>B\<^sub>a\<^sub>g(x)) = ((\ X) and (\ x))" by (simp add: OclIncludes.def_valid_then_def) -text{* OclExcludes *} +text\OclExcludes\ lemma OclExcludes_valid_args_valid: "(\ \ \(X->excludes\<^sub>B\<^sub>a\<^sub>g(x))) = ((\ \(\ X)) \ (\ \(\ x)))" @@ -679,7 +679,7 @@ lemma OclExcludes_valid_args_valid''[simp,code_unfold]: "\(X->excludes\<^sub>B\<^sub>a\<^sub>g(x)) = ((\ X) and (\ x))" by (simp add: OclExcludes.def_valid_then_def) -text{* OclSize *} +text\OclSize\ lemma OclSize_defined_args_valid: "\ \ \ (X->size\<^sub>B\<^sub>a\<^sub>g()) \ \ \ \ X" by(auto simp: OclSize_def OclValid_def true_def valid_def false_def StrongEq_def @@ -712,7 +712,7 @@ lemma size_defined': apply(simp add: defined_def bot_option_def bot_fun_def null_option_def null_fun_def X_finite) done -text{* OclIsEmpty *} +text\OclIsEmpty\ lemma OclIsEmpty_defined_args_valid:"\ \ \ (X->isEmpty\<^sub>B\<^sub>a\<^sub>g()) \ \ \ \ X" apply(auto simp: OclIsEmpty_def OclValid_def defined_def valid_def false_def true_def @@ -737,7 +737,7 @@ lemma OclIsEmpty_infinite: "\ \ \ X \ \I\<^sub>n\<^sub>t\<^sub>e\<^sub>g\<^sub>e\<^sub>r valid_def bot_fun_def false_def true_def invalid_def) -text{* OclNotEmpty *} +text\OclNotEmpty\ lemma OclNotEmpty_defined_args_valid:"\ \ \ (X->notEmpty\<^sub>B\<^sub>a\<^sub>g()) \ \ \ \ X" by (metis (hide_lams, no_types) OclNotEmpty_def OclNot_defargs OclNot_not foundation6 foundation9 @@ -779,7 +779,7 @@ lemma OclNotEmpty_has_elt' : "\ \ \ X \ apply(drule OclNotEmpty_has_elt, simp) by(simp add: Rep_Bag_base_def Rep_Set_base_def image_def) -text{* OclANY *} +text\OclANY\ lemma OclANY_defined_args_valid: "\ \ \ (X->any\<^sub>B\<^sub>a\<^sub>g()) \ \ \ \ X" by(auto simp: OclANY_def OclValid_def true_def valid_def false_def StrongEq_def @@ -824,19 +824,19 @@ lemma OclANY_valid_args_valid''[simp,code_unfold]: by(auto intro!: OclANY_valid_args_valid transform2_rev) (* and higher order ones : forall, exists, iterate, select, reject... *) -text_raw{* \endisatagafp *} +text_raw\\endisatagafp\ -subsection{* Execution Laws with Invalid or Null or Infinite Set as Argument *} +subsection\Execution Laws with Invalid or Null or Infinite Set as Argument\ -text{* OclIncluding *} (* properties already generated by the corresponding locale *) +text\OclIncluding\ (* properties already generated by the corresponding locale *) -text{* OclExcluding *} (* properties already generated by the corresponding locale *) +text\OclExcluding\ (* properties already generated by the corresponding locale *) -text{* OclIncludes *} (* properties already generated by the corresponding locale *) +text\OclIncludes\ (* properties already generated by the corresponding locale *) -text{* OclExcludes *} (* properties already generated by the corresponding locale *) +text\OclExcludes\ (* properties already generated by the corresponding locale *) -text{* OclSize *} +text\OclSize\ lemma OclSize_invalid[simp,code_unfold]:"(invalid->size\<^sub>B\<^sub>a\<^sub>g()) = invalid" by(simp add: bot_fun_def OclSize_def invalid_def defined_def valid_def false_def true_def) @@ -846,7 +846,7 @@ by(rule ext, simp add: bot_fun_def null_fun_def null_is_valid OclSize_def invalid_def defined_def valid_def false_def true_def) -text{* OclIsEmpty *} +text\OclIsEmpty\ lemma OclIsEmpty_invalid[simp,code_unfold]:"(invalid->isEmpty\<^sub>B\<^sub>a\<^sub>g()) = invalid" by(simp add: OclIsEmpty_def) @@ -854,7 +854,7 @@ by(simp add: OclIsEmpty_def) lemma OclIsEmpty_null[simp,code_unfold]:"(null->isEmpty\<^sub>B\<^sub>a\<^sub>g()) = true" by(simp add: OclIsEmpty_def) -text{* OclNotEmpty *} +text\OclNotEmpty\ lemma OclNotEmpty_invalid[simp,code_unfold]:"(invalid->notEmpty\<^sub>B\<^sub>a\<^sub>g()) = invalid" by(simp add: OclNotEmpty_def) @@ -862,7 +862,7 @@ by(simp add: OclNotEmpty_def) lemma OclNotEmpty_null[simp,code_unfold]:"(null->notEmpty\<^sub>B\<^sub>a\<^sub>g()) = false" by(simp add: OclNotEmpty_def) -text{* OclANY *} +text\OclANY\ lemma OclANY_invalid[simp,code_unfold]:"(invalid->any\<^sub>B\<^sub>a\<^sub>g()) = invalid" by(simp add: bot_fun_def OclANY_def invalid_def defined_def valid_def false_def true_def) @@ -870,7 +870,7 @@ by(simp add: bot_fun_def OclANY_def invalid_def defined_def valid_def false_def lemma OclANY_null[simp,code_unfold]:"(null->any\<^sub>B\<^sub>a\<^sub>g()) = null" by(simp add: OclANY_def false_def true_def) -text{* OclForall *} +text\OclForall\ lemma OclForall_invalid[simp,code_unfold]:"invalid->forAll\<^sub>B\<^sub>a\<^sub>g(a| P a) = invalid" by(simp add: bot_fun_def invalid_def OclForall_def defined_def valid_def false_def true_def) @@ -878,7 +878,7 @@ by(simp add: bot_fun_def invalid_def OclForall_def defined_def valid_def false_d lemma OclForall_null[simp,code_unfold]:"null->forAll\<^sub>B\<^sub>a\<^sub>g(a | P a) = invalid" by(simp add: bot_fun_def invalid_def OclForall_def defined_def valid_def false_def true_def) -text{* OclExists *} +text\OclExists\ lemma OclExists_invalid[simp,code_unfold]:"invalid->exists\<^sub>B\<^sub>a\<^sub>g(a| P a) = invalid" by(simp add: OclExists_def) @@ -886,7 +886,7 @@ by(simp add: OclExists_def) lemma OclExists_null[simp,code_unfold]:"null->exists\<^sub>B\<^sub>a\<^sub>g(a | P a) = invalid" by(simp add: OclExists_def) -text{* OclIterate *} +text\OclIterate\ lemma OclIterate_invalid[simp,code_unfold]:"invalid->iterate\<^sub>B\<^sub>a\<^sub>g(a; x = A | P a x) = invalid" by(simp add: bot_fun_def invalid_def OclIterate_def defined_def valid_def false_def true_def) @@ -898,7 +898,7 @@ by(simp add: bot_fun_def invalid_def OclIterate_def defined_def valid_def false_ lemma OclIterate_invalid_args[simp,code_unfold]:"S->iterate\<^sub>B\<^sub>a\<^sub>g(a; x = invalid | P a x) = invalid" by(simp add: bot_fun_def invalid_def OclIterate_def defined_def valid_def false_def true_def) -text{* An open question is this ... *} +text\An open question is this ...\ lemma (*OclIterate_null_args[simp,code_unfold]:*) "S->iterate\<^sub>B\<^sub>a\<^sub>g(a; x = null | P a x) = invalid" oops (* In the definition above, this does not hold in general. @@ -911,7 +911,7 @@ apply(insert non_finite [THEN OclSize_infinite]) apply(subst (asm) foundation9, simp) by(metis OclIterate_def OclValid_def invalid_def) -text{* OclSelect *} +text\OclSelect\ lemma OclSelect_invalid[simp,code_unfold]:"invalid->select\<^sub>B\<^sub>a\<^sub>g(a | P a) = invalid" by(simp add: bot_fun_def invalid_def OclSelect_def defined_def valid_def false_def true_def) @@ -919,7 +919,7 @@ by(simp add: bot_fun_def invalid_def OclSelect_def defined_def valid_def false_d lemma OclSelect_null[simp,code_unfold]:"null->select\<^sub>B\<^sub>a\<^sub>g(a | P a) = invalid" by(simp add: bot_fun_def invalid_def OclSelect_def defined_def valid_def false_def true_def) -text{* OclReject *} +text\OclReject\ lemma OclReject_invalid[simp,code_unfold]:"invalid->reject\<^sub>B\<^sub>a\<^sub>g(a | P a) = invalid" by(simp add: OclReject_def) @@ -927,9 +927,9 @@ by(simp add: OclReject_def) lemma OclReject_null[simp,code_unfold]:"null->reject\<^sub>B\<^sub>a\<^sub>g(a | P a) = invalid" by(simp add: OclReject_def) -text_raw{* \isatagafp *} +text_raw\\isatagafp\ -subsubsection{* Context Passing *} +subsubsection\Context Passing\ lemma cp_OclIncludes1: "(X->includes\<^sub>B\<^sub>a\<^sub>g(x)) \ = (X->includes\<^sub>B\<^sub>a\<^sub>g(\ _. x \)) \" @@ -1012,7 +1012,7 @@ lemmas cp_intro''\<^sub>B\<^sub>a\<^sub>g[intro!,simp,code_unfold] = cp_OclNotEmpty [THEN allI[THEN allI[THEN cpI1], of "OclNotEmpty"]] cp_OclANY [THEN allI[THEN allI[THEN cpI1], of "OclANY"]] -subsubsection{* Const *} +subsubsection\Const\ lemma const_OclIncluding[simp,code_unfold] : assumes const_x : "const x" @@ -1040,9 +1040,9 @@ lemma const_OclIncluding[simp,code_unfold] : apply(subst (1 2) const_charn[OF const_S]) by simp qed -text_raw{* \endisatagafp *} +text_raw\\endisatagafp\ -subsection{* Test Statements *} +subsection\Test Statements\ (*Assert "(\ \ (Bag{\_. \\x\\} \ Bag{\_. \\x\\}))" Assert "(\ \ (Bag{\_. \x\} \ Bag{\_. \x\}))"*) diff --git a/Featherweight_OCL/collection_types/UML_Pair.thy b/Featherweight_OCL/collection_types/UML_Pair.thy index 0280808..7fec757 100644 --- a/Featherweight_OCL/collection_types/UML_Pair.thy +++ b/Featherweight_OCL/collection_types/UML_Pair.thy @@ -44,15 +44,15 @@ theory UML_Pair imports "../UML_PropertyProfiles" begin -section{* Collection Type Pairs: Operations \label{sec:collection_pairs} *} +section\Collection Type Pairs: Operations \label{sec:collection_pairs}\ -text{* The OCL standard provides the concept of \emph{Tuples}, \ie{} a family of record-types +text\The OCL standard provides the concept of \emph{Tuples}, \ie{} a family of record-types with projection functions. In FeatherWeight OCL, only the theory of a special case is developped, namely the type of Pairs, which is, however, sufficient for all applications since it can be used to mimick all tuples. In particular, it can be used to express operations -with multiple arguments, roles of n-ary associations, ... *} +with multiple arguments, roles of n-ary associations, ...\ -subsection{* Semantic Properties of the Type Constructor *} +subsection\Semantic Properties of the Type Constructor\ lemma A[simp]:"Rep_Pair\<^sub>b\<^sub>a\<^sub>s\<^sub>e x \ None \ Rep_Pair\<^sub>b\<^sub>a\<^sub>s\<^sub>e x \ null \ (fst \\Rep_Pair\<^sub>b\<^sub>a\<^sub>s\<^sub>e x\\) \ bot" by(insert Rep_Pair\<^sub>b\<^sub>a\<^sub>s\<^sub>e[of x],auto simp:null_option_def bot_option_def) @@ -82,12 +82,12 @@ apply(subst Rep_Pair\<^sub>b\<^sub>a\<^sub>s\<^sub>e_inject[symmetric], simp) apply(subst Pair\<^sub>b\<^sub>a\<^sub>s\<^sub>e.Abs_Pair\<^sub>b\<^sub>a\<^sub>s\<^sub>e_inverse, simp_all,simp add: null_option_def bot_option_def) done -subsection{* Fundamental Properties of Strict Equality \label{sec:pair-strict-eq}*} +subsection\Fundamental Properties of Strict Equality \label{sec:pair-strict-eq}\ -text{* After the part of foundational operations on sets, we detail here equality on sets. +text\After the part of foundational operations on sets, we detail here equality on sets. Strong equality is inherited from the OCL core, but we have to consider the case of the strict equality. We decide to overload strict equality in the -same way we do for other value's in OCL:*} +same way we do for other value's in OCL:\ overloading StrictRefEq \ "StrictRefEq :: [('\,'\::null,'\::null)Pair,('\,'\::null,'\::null)Pair] \ ('\)Boolean" @@ -98,15 +98,15 @@ begin else invalid \)" end -text{* Property proof in terms of @{term "profile_bin\<^sub>S\<^sub>t\<^sub>r\<^sub>o\<^sub>n\<^sub>g\<^sub>E\<^sub>q_\<^sub>v_\<^sub>v"}*} +text\Property proof in terms of @{term "profile_bin\<^sub>S\<^sub>t\<^sub>r\<^sub>o\<^sub>n\<^sub>g\<^sub>E\<^sub>q_\<^sub>v_\<^sub>v"}\ interpretation StrictRefEq\<^sub>P\<^sub>a\<^sub>i\<^sub>r : profile_bin\<^sub>S\<^sub>t\<^sub>r\<^sub>o\<^sub>n\<^sub>g\<^sub>E\<^sub>q_\<^sub>v_\<^sub>v "\ x y. (x::('\,'\::null,'\::null)Pair) \ y" by unfold_locales (auto simp: StrictRefEq\<^sub>P\<^sub>a\<^sub>i\<^sub>r) -subsection{* Standard Operations Definitions *} +subsection\Standard Operations Definitions\ -text{* This part provides a collection of operators for the Pair type. *} +text\This part provides a collection of operators for the Pair type.\ -subsubsection{* Definition: Pair Constructor *} +subsubsection\Definition: Pair Constructor\ definition OclPair::"('\, '\) val \ ('\, '\) val \ @@ -121,7 +121,7 @@ interpretation OclPair : profile_bin\<^sub>v_\<^sub>v by(auto simp: Abs_Pair\<^sub>b\<^sub>a\<^sub>s\<^sub>e_inject null_option_def bot_option_def) -subsubsection{* Definition: First *} +subsubsection\Definition: First\ definition OclFirst::" ('\,'\::null,'\::null) Pair \ ('\, '\) val" (" _ .First'(')") where "X .First() \ (\ \. if (\ X) \ = true \ @@ -132,7 +132,7 @@ where "X .First() \ (\ \. if (\ X) \ = true interpretation OclFirst : profile_mono\<^sub>d OclFirst "\x. fst \\Rep_Pair\<^sub>b\<^sub>a\<^sub>s\<^sub>e (x)\\" by unfold_locales (auto simp: OclFirst_def) -subsubsection{* Definition: Second *} +subsubsection\Definition: Second\ definition OclSecond::" ('\,'\::null,'\::null) Pair \ ('\, '\) val" ("_ .Second'(')") where "X .Second() \ (\ \. if (\ X) \ = true \ @@ -142,7 +142,7 @@ where "X .Second() \ (\ \. if (\ X) \ = true interpretation OclSecond : profile_mono\<^sub>d OclSecond "\x. snd \\Rep_Pair\<^sub>b\<^sub>a\<^sub>s\<^sub>e (x)\\" by unfold_locales (auto simp: OclSecond_def) -subsection{* Logical Properties *} +subsection\Logical Properties\ lemma 1 : "\ \ \ Y \ \ \ Pair{X,Y} .First() \ X" apply(case_tac "\(\ \ \ X)") @@ -162,7 +162,7 @@ apply(auto simp: OclValid_def valid_def defined_def StrongEq_def OclSecond_def O apply(auto simp: Abs_Pair\<^sub>b\<^sub>a\<^sub>s\<^sub>e_inject null_option_def bot_option_def bot_Pair\<^sub>b\<^sub>a\<^sub>s\<^sub>e_def null_Pair\<^sub>b\<^sub>a\<^sub>s\<^sub>e_def) by(simp add: Abs_Pair\<^sub>b\<^sub>a\<^sub>s\<^sub>e_inverse) -subsection{* Algebraic Execution Properties *} +subsection\Algebraic Execution Properties\ lemma proj1_exec [simp, code_unfold] : "Pair{X,Y} .First() = (if (\ Y) then X else invalid endif)" apply(rule ext, rename_tac "\", simp add: foundation22[symmetric]) @@ -185,7 +185,7 @@ by(erule 2) (* < *) -subsection{* Test Statements*} +subsection\Test Statements\ (* Assert "(\ \ (Pair{\_. \\x\\,\_. \\x\\} \ Pair{\_. \\x\\,\_. \\x\\}))" Assert "(\ \ (Pair{\_. \x\,\_. \x\} \ Pair{\_. \x\,\_. \x\}))" diff --git a/Featherweight_OCL/collection_types/UML_Sequence.thy b/Featherweight_OCL/collection_types/UML_Sequence.thy index 53b388d..26090b9 100644 --- a/Featherweight_OCL/collection_types/UML_Sequence.thy +++ b/Featherweight_OCL/collection_types/UML_Sequence.thy @@ -47,11 +47,11 @@ imports "../basic_types/UML_Boolean" begin no_notation None ("\") -section{* Collection Type Sequence: Operations *} +section\Collection Type Sequence: Operations\ -subsection{* Basic Properties of the Sequence Type *} +subsection\Basic Properties of the Sequence Type\ -text{* Every element in a defined sequence is valid. *} +text\Every element in a defined sequence is valid.\ lemma Sequence_inv_lemma: "\ \ (\ X) \ \x\set \\Rep_Sequence\<^sub>b\<^sub>a\<^sub>s\<^sub>e (X \)\\. x \ bot" apply(insert Rep_Sequence\<^sub>b\<^sub>a\<^sub>s\<^sub>e [of "X \"], simp) @@ -66,12 +66,12 @@ apply(subst Abs_Sequence\<^sub>b\<^sub>a\<^sub>s\<^sub>e_inject[symmetric], rule apply(simp add: Rep_Sequence\<^sub>b\<^sub>a\<^sub>s\<^sub>e_inverse null_option_def) by (simp add: bot_option_def) -subsection{* Definition: Strict Equality \label{sec:seq-strict-equality}*} +subsection\Definition: Strict Equality \label{sec:seq-strict-equality}\ -text{* After the part of foundational operations on sets, we detail here equality on sets. +text\After the part of foundational operations on sets, we detail here equality on sets. Strong equality is inherited from the OCL core, but we have to consider the case of the strict equality. We decide to overload strict equality in the -same way we do for other value's in OCL:*} +same way we do for other value's in OCL:\ overloading StrictRefEq \ "StrictRefEq :: [('\,'\::null)Sequence,('\,'\::null)Sequence] \ ('\)Boolean" @@ -82,22 +82,22 @@ begin else invalid \)" end -text_raw{* \isatagafp *} -text{* One might object here that for the case of objects, this is an empty definition. +text_raw\\isatagafp\ +text\One might object here that for the case of objects, this is an empty definition. The answer is no, we will restrain later on states and objects such that any object has its oid stored inside the object (so the ref, under which an object can be referenced in the store will represented in the object itself). For such well-formed stores that satisfy this invariant (the WFF-invariant), the referential equality and the -strong equality---and therefore the strict equality on sequences in the sense above---coincides.*} -text_raw{* \endisatagafp *} +strong equality---and therefore the strict equality on sequences in the sense above---coincides.\ +text_raw\\endisatagafp\ -text{* Property proof in terms of @{term "profile_bin\<^sub>S\<^sub>t\<^sub>r\<^sub>o\<^sub>n\<^sub>g\<^sub>E\<^sub>q_\<^sub>v_\<^sub>v"}*} +text\Property proof in terms of @{term "profile_bin\<^sub>S\<^sub>t\<^sub>r\<^sub>o\<^sub>n\<^sub>g\<^sub>E\<^sub>q_\<^sub>v_\<^sub>v"}\ interpretation StrictRefEq\<^sub>S\<^sub>e\<^sub>q : profile_bin\<^sub>S\<^sub>t\<^sub>r\<^sub>o\<^sub>n\<^sub>g\<^sub>E\<^sub>q_\<^sub>v_\<^sub>v "\ x y. (x::('\,'\::null)Sequence) \ y" by unfold_locales (auto simp: StrictRefEq\<^sub>S\<^sub>e\<^sub>q) -subsection{* Constants: mtSequence *} +subsection\Constants: mtSequence\ definition mtSequence ::"('\,'\::null) Sequence" ("Sequence{}") where "Sequence{} \ (\ \. Abs_Sequence\<^sub>b\<^sub>a\<^sub>s\<^sub>e \\[]::'\ list\\ )" @@ -116,18 +116,18 @@ lemma mtSequence_rep_set: "\\Rep_Sequence\<^sub>b\<^sub>a\<^sub>s\ apply(simp add: mtSequence_def, subst Abs_Sequence\<^sub>b\<^sub>a\<^sub>s\<^sub>e_inverse) by(simp add: bot_option_def)+ -text_raw{* \isatagafp *} +text_raw\\isatagafp\ lemma [simp,code_unfold]: "const Sequence{}" by(simp add: const_def mtSequence_def) -text{* Note that the collection types in OCL allow for null to be included; - however, there is the null-collection into which inclusion yields invalid. *} +text\Note that the collection types in OCL allow for null to be included; + however, there is the null-collection into which inclusion yields invalid.\ -text_raw{* \endisatagafp *} +text_raw\\endisatagafp\ -subsection{* Definition: Prepend *} +subsection\Definition: Prepend\ definition OclPrepend :: "[('\,'\::null) Sequence,('\,'\) val] \ ('\,'\) Sequence" where "OclPrepend x y = (\ \. if (\ x) \ = true \ \ (\ y) \ = true \ then Abs_Sequence\<^sub>b\<^sub>a\<^sub>s\<^sub>e \\ (y \)#\\Rep_Sequence\<^sub>b\<^sub>a\<^sub>s\<^sub>e (x \)\\ \\ @@ -163,7 +163,7 @@ translations "Sequence{x, xs}" == "CONST OclPrepend (Sequence{xs}) x" "Sequence{x}" == "CONST OclPrepend (Sequence{}) x " -subsection{* Definition: Including *} +subsection\Definition: Including\ definition OclIncluding :: "[('\,'\::null) Sequence,('\,'\) val] \ ('\,'\) Sequence" where "OclIncluding x y = (\ \. if (\ x) \ = true \ \ (\ y) \ = true \ @@ -223,7 +223,7 @@ lemma [simp,code_unfold] : "((S->prepend\<^sub>S\<^sub>e\<^sub>q(a))->including\ by (metis OclValid_def foundation16 invalid_def)+ qed -subsection{* Definition: Excluding *} +subsection\Definition: Excluding\ definition OclExcluding :: "[('\,'\::null) Sequence,('\,'\) val] \ ('\,'\) Sequence" where "OclExcluding x y = (\ \. if (\ x) \ = true \ \ (\ y) \ = true \ then Abs_Sequence\<^sub>b\<^sub>a\<^sub>s\<^sub>e \\ filter (\x. x = y \) @@ -243,8 +243,8 @@ proof - done qed -subsection{* Definition: Append *} -text{* Identical to OclIncluding. *} +subsection\Definition: Append\ +text\Identical to OclIncluding.\ definition OclAppend :: "[('\,'\::null) Sequence,('\,'\) val] \ ('\,'\) Sequence" where "OclAppend = OclIncluding" notation OclAppend ("_->append\<^sub>S\<^sub>e\<^sub>q'(_')") @@ -255,7 +255,7 @@ interpretation OclAppend : by(auto simp: OclAppend_def bin_def bin'_def OclIncluding.def_scheme OclIncluding.def_body) -subsection{* Definition: Union *} +subsection\Definition: Union\ definition OclUnion :: "[('\,'\::null) Sequence,('\,'\) Sequence] \ ('\,'\) Sequence" where "OclUnion x y = (\ \. if (\ x) \ = true \ \ (\ y) \ = true \ then Abs_Sequence\<^sub>b\<^sub>a\<^sub>s\<^sub>e \\ \\Rep_Sequence\<^sub>b\<^sub>a\<^sub>s\<^sub>e (x \)\\ @ @@ -277,7 +277,7 @@ proof - simp_all add: bot_option_def null_option_def Set.ball_Un A null_Sequence\<^sub>b\<^sub>a\<^sub>s\<^sub>e_def bot_Sequence\<^sub>b\<^sub>a\<^sub>s\<^sub>e_def)+ qed -subsection{* Definition: At *} +subsection\Definition: At\ definition OclAt :: "[('\,'\::null) Sequence,('\) Integer] \ ('\,'\) val" where "OclAt x y = (\ \. if (\ x) \ = true \ \ (\ y) \ = true \ then if 1 \ \\y \\\ \ \\y \\\ \ length\\Rep_Sequence\<^sub>b\<^sub>a\<^sub>s\<^sub>e (x \)\\ @@ -288,7 +288,7 @@ notation OclAt ("_->at\<^sub>S\<^sub>e\<^sub>q'(_')") (*TODO Locale - Equivalent*) -subsection{* Definition: First *} +subsection\Definition: First\ definition OclFirst :: "[('\,'\::null) Sequence] \ ('\,'\) val" where "OclFirst x = (\ \. if (\ x) \ = true \ then case \\Rep_Sequence\<^sub>b\<^sub>a\<^sub>s\<^sub>e (x \)\\ of [] \ invalid \ @@ -298,7 +298,7 @@ notation OclFirst ("_->first\<^sub>S\<^sub>e\<^sub>q'(_')") (*TODO Locale - Equivalent*) -subsection{* Definition: Last *} +subsection\Definition: Last\ definition OclLast :: "[('\,'\::null) Sequence] \ ('\,'\) val" where "OclLast x = (\ \. if (\ x) \ = true \ then if \\Rep_Sequence\<^sub>b\<^sub>a\<^sub>s\<^sub>e (x \)\\ = [] then @@ -309,7 +309,7 @@ where "OclLast x = (\ \. if (\ x) \ = true \ t notation OclLast ("_->last\<^sub>S\<^sub>e\<^sub>q'(_')") (*TODO Locale - Equivalent*) -subsection{* Definition: Iterate *} +subsection\Definition: Iterate\ definition OclIterate :: "[('\,'\::null) Sequence,('\,'\::null)val, ('\,'\)val\('\,'\)val\('\,'\)val] \ ('\,'\)val" @@ -326,7 +326,7 @@ translations -subsection{* Definition: Forall *} +subsection\Definition: Forall\ definition OclForall :: "[('\,'\::null) Sequence,('\,'\)val\('\)Boolean] \ '\ Boolean" where "OclForall S P = (S->iterate\<^sub>S\<^sub>e\<^sub>q(b; x = true | x and (P b)))" @@ -337,7 +337,7 @@ translations (*TODO Locale - Equivalent*) -subsection{* Definition: Exists *} +subsection\Definition: Exists\ definition OclExists :: "[('\,'\::null) Sequence,('\,'\)val\('\)Boolean] \ '\ Boolean" where "OclExists S P = (S->iterate\<^sub>S\<^sub>e\<^sub>q(b; x = false | x or (P b)))" @@ -348,7 +348,7 @@ translations (*TODO Locale - Equivalent*) -subsection{* Definition: Collect *} +subsection\Definition: Collect\ definition OclCollect :: "[('\,'\::null)Sequence,('\,'\)val\('\,'\)val]\('\,'\::null)Sequence" where "OclCollect S P = (S->iterate\<^sub>S\<^sub>e\<^sub>q(b; x = Sequence{} | x->prepend\<^sub>S\<^sub>e\<^sub>q(P b)))" @@ -359,7 +359,7 @@ translations (*TODO Locale - Equivalent*) -subsection{* Definition: Select *} +subsection\Definition: Select\ definition OclSelect :: "[('\,'\::null)Sequence,('\,'\)val\('\)Boolean]\('\,'\::null)Sequence" where "OclSelect S P = (S->iterate\<^sub>S\<^sub>e\<^sub>q(b; x = Sequence{} | if P b then x->prepend\<^sub>S\<^sub>e\<^sub>q(b) else x endif))" @@ -371,20 +371,20 @@ translations (*TODO Locale - Equivalent*) -subsection{* Definition: Size *} +subsection\Definition: Size\ definition OclSize :: "[('\,'\::null)Sequence]\('\)Integer" ("(_)->size\<^sub>S\<^sub>e\<^sub>q'(')") where "OclSize S = (S->iterate\<^sub>S\<^sub>e\<^sub>q(b; x = \ | x +\<^sub>i\<^sub>n\<^sub>t \ ))" (*TODO Locale - Equivalent*) -subsection{* Definition: IsEmpty *} +subsection\Definition: IsEmpty\ definition OclIsEmpty :: "('\,'\::null) Sequence \ '\ Boolean" where "OclIsEmpty x = ((\ x and not (\ x)) or ((OclSize x) \ \))" notation OclIsEmpty ("_->isEmpty\<^sub>S\<^sub>e\<^sub>q'(')" (*[66]*)) (*TODO Locale - Equivalent*) -subsection{* Definition: NotEmpty *} +subsection\Definition: NotEmpty\ definition OclNotEmpty :: "('\,'\::null) Sequence \ '\ Boolean" where "OclNotEmpty x = not(OclIsEmpty x)" @@ -392,7 +392,7 @@ notation OclNotEmpty ("_->notEmpty\<^sub>S\<^sub>e\<^sub>q'(')" (*[66]*)) (*TODO Locale - Equivalent*) -subsection{* Definition: Any *} +subsection\Definition: Any\ definition "OclANY x = (\ \. if x \ = invalid \ then @@ -404,7 +404,7 @@ notation OclANY ("_->any\<^sub>S\<^sub>e\<^sub>q'(')") (*TODO Locale - Equivalent*) -subsection{* Definition (future operators) *} +subsection\Definition (future operators)\ consts (* abstract set collection operations *) OclCount :: "[('\,'\::null) Sequence,('\,'\) Sequence] \ '\ Integer" @@ -418,11 +418,11 @@ consts (* abstract set collection operations *) notation OclCount ("_->count\<^sub>S\<^sub>e\<^sub>q'(_')" (*[66,65]65*)) notation OclSum ("_->sum\<^sub>S\<^sub>e\<^sub>q'(')" (*[66]*)) -subsection{* Logical Properties *} +subsection\Logical Properties\ -subsection{* Execution Laws with Invalid or Null as Argument *} +subsection\Execution Laws with Invalid or Null as Argument\ -text{* OclIterate *} +text\OclIterate\ lemma OclIterate_invalid[simp,code_unfold]:"invalid->iterate\<^sub>S\<^sub>e\<^sub>q(a; x = A | P a x) = invalid" by(simp add: OclIterate_def false_def true_def, simp add: invalid_def) @@ -433,9 +433,9 @@ by(simp add: OclIterate_def false_def true_def, simp add: invalid_def) lemma OclIterate_invalid_args[simp,code_unfold]:"S->iterate\<^sub>S\<^sub>e\<^sub>q(a; x = invalid | P a x) = invalid" by(simp add: bot_fun_def invalid_def OclIterate_def defined_def valid_def false_def true_def) -text_raw{* \isatagafp *} +text_raw\\isatagafp\ -subsubsection{* Context Passing *} +subsubsection\Context Passing\ lemma cp_OclIncluding: "(X->including\<^sub>S\<^sub>e\<^sub>q(x)) \ = ((\ _. X \)->including\<^sub>S\<^sub>e\<^sub>q(\ _. x \)) \" @@ -450,12 +450,12 @@ by(simp add: OclIterate_def cp_defined[symmetric]) lemmas cp_intro''\<^sub>S\<^sub>e\<^sub>q[intro!,simp,code_unfold] = cp_OclIncluding [THEN allI[THEN allI[THEN allI[THEN cpI2]], of "OclIncluding"]] -subsubsection{* Const *} +subsubsection\Const\ -text_raw{* \endisatagafp *} +text_raw\\endisatagafp\ -subsection{* General Algebraic Execution Rules *} -subsubsection{* Execution Rules on Iterate *} +subsection\General Algebraic Execution Rules\ +subsubsection\Execution Rules on Iterate\ lemma OclIterate_empty[simp,code_unfold]:"Sequence{}->iterate\<^sub>S\<^sub>e\<^sub>q(a; x = A | P a x) = A" apply(simp add: OclIterate_def foundation22[symmetric] foundation13, @@ -464,7 +464,7 @@ apply(case_tac "\ \ \ A", simp_all add: foundation18') apply(simp add: mtSequence_def) apply(subst Abs_Sequence\<^sub>b\<^sub>a\<^sub>s\<^sub>e_inverse) by auto -text{* In particular, this does hold for A = null. *} +text\In particular, this does hold for A = null.\ lemma OclIterate_including[simp,code_unfold]: assumes strict1 : "\X. P invalid X = invalid" @@ -540,7 +540,7 @@ qed (* < *) -subsection{* Test Statements *} +subsection\Test Statements\ (* Assert "(\ \ (Sequence{\_. \\x\\} \ Sequence{\_. \\x\\}))" Assert "(\ \ (Sequence{\_. \x\} \ Sequence{\_. \x\}))" diff --git a/Featherweight_OCL/collection_types/UML_Set.thy b/Featherweight_OCL/collection_types/UML_Set.thy index 4c00745..9fd6616 100644 --- a/Featherweight_OCL/collection_types/UML_Set.thy +++ b/Featherweight_OCL/collection_types/UML_Set.thy @@ -50,12 +50,12 @@ imports "../basic_types/UML_Void" begin no_notation None ("\") -section{* Collection Type Set: Operations \label{formal-set}*} +section\Collection Type Set: Operations \label{formal-set}\ -subsection{* As a Motivation for the (infinite) Type Construction: Type-Extensions as Sets - \label{sec:type-extensions}*} +subsection\As a Motivation for the (infinite) Type Construction: Type-Extensions as Sets + \label{sec:type-extensions}\ -text{* Our notion of typed set goes beyond the usual notion of a finite executable set and +text\Our notion of typed set goes beyond the usual notion of a finite executable set and is powerful enough to capture \emph{the extension of a type} in UML and OCL. This means we can have in Featherweight OCL Sets containing all possible elements of a type, not only those (finite) ones representable in a state. This holds for base types as well as class types, @@ -69,9 +69,9 @@ In a world with @{term invalid} and @{term null}, there are two notions extensio \item the set of all \emph{valid} values of a type @{term T}, so including @{term null} (for which we will introduce the constant @{term T\<^sub>n\<^sub>u\<^sub>l\<^sub>l}). \end{enumerate} -*} +\ -text{* We define the set extensions for the base type @{term Integer} as follows: *} +text\We define the set extensions for the base type @{term Integer} as follows:\ definition Integer :: "('\,Integer\<^sub>b\<^sub>a\<^sub>s\<^sub>e) Set" where "Integer \ (\ \. (Abs_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e o Some o Some) ((Some o Some) ` (UNIV::int set)))" @@ -88,20 +88,20 @@ apply(rule ext, auto simp: Integer\<^sub>n\<^sub>u\<^sub>l\<^sub>l_def defined_d bot_fun_def null_fun_def null_option_def) by(simp_all add: Abs_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e_inject bot_option_def bot_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e_def null_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e_def null_option_def) -text{* This allows the theorems: +text\This allows the theorems: - @{text "\ \ \ x \ \ \ (Integer->includes\<^sub>S\<^sub>e\<^sub>t(x))"} - @{text "\ \ \ x \ \ \ Integer \ (Integer->including\<^sub>S\<^sub>e\<^sub>t(x))"} + \\ \ \ x \ \ \ (Integer->includes\<^sub>S\<^sub>e\<^sub>t(x))\ + \\ \ \ x \ \ \ Integer \ (Integer->including\<^sub>S\<^sub>e\<^sub>t(x))\ and - @{text "\ \ \ x \ \ \ (Integer\<^sub>n\<^sub>u\<^sub>l\<^sub>l->includes\<^sub>S\<^sub>e\<^sub>t(x))"} - @{text "\ \ \ x \ \ \ Integer\<^sub>n\<^sub>u\<^sub>l\<^sub>l \ (Integer\<^sub>n\<^sub>u\<^sub>l\<^sub>l->including\<^sub>S\<^sub>e\<^sub>t(x))"} + \\ \ \ x \ \ \ (Integer\<^sub>n\<^sub>u\<^sub>l\<^sub>l->includes\<^sub>S\<^sub>e\<^sub>t(x))\ + \\ \ \ x \ \ \ Integer\<^sub>n\<^sub>u\<^sub>l\<^sub>l \ (Integer\<^sub>n\<^sub>u\<^sub>l\<^sub>l->including\<^sub>S\<^sub>e\<^sub>t(x))\ which characterize the infiniteness of these sets by a recursive property on these sets. -*} +\ -text{* In the same spirit, we proceed similarly for the remaining base types: *} +text\In the same spirit, we proceed similarly for the remaining base types:\ definition Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l :: "('\,Void\<^sub>b\<^sub>a\<^sub>s\<^sub>e) Set" where "Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l \ (\ \. (Abs_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e o Some o Some) {Abs_Void\<^sub>b\<^sub>a\<^sub>s\<^sub>e (Some None)})" @@ -213,9 +213,9 @@ apply(rule ext, auto simp: Real\<^sub>n\<^sub>u\<^sub>l\<^sub>l_def defined_def bot_fun_def null_fun_def null_option_def) by(simp_all add: Abs_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e_inject bot_option_def bot_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e_def null_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e_def null_option_def) -subsection{* Basic Properties of the Set Type*} +subsection\Basic Properties of the Set Type\ -text{* Every element in a defined set is valid. *} +text\Every element in a defined set is valid.\ lemma Set_inv_lemma: "\ \ (\ X) \ \x\\\Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e (X \)\\. x \ bot" apply(insert Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e [of "X \"], simp) @@ -276,18 +276,18 @@ apply(simp add: valid_def null_fun_def bot_fun_def bot_Set\<^sub>b\<^sub>a\<^sub apply(subst Abs_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e_inject,simp_all add: null_option_def bot_option_def) done -text{* ... which means that we can have a type @{text "('\,('\,('\) Integer) Set) Set"} +text\... which means that we can have a type \('\,('\,('\) Integer) Set) Set\ corresponding exactly to Set(Set(Integer)) in OCL notation. Note that the parameter -@{text "'\"} still refers to the object universe; making the OCL semantics entirely parametric +\'\\ still refers to the object universe; making the OCL semantics entirely parametric in the object universe makes it possible to study (and prove) its properties -independently from a concrete class diagram. *} +independently from a concrete class diagram.\ -subsection{* Definition: Strict Equality \label{sec:set-strict-equality}*} +subsection\Definition: Strict Equality \label{sec:set-strict-equality}\ -text{* After the part of foundational operations on sets, we detail here equality on sets. +text\After the part of foundational operations on sets, we detail here equality on sets. Strong equality is inherited from the OCL core, but we have to consider the case of the strict equality. We decide to overload strict equality in the -same way we do for other value's in OCL:*} +same way we do for other value's in OCL:\ overloading StrictRefEq \ "StrictRefEq :: [('\,'\::null)Set,('\,'\::null)Set] \ ('\)Boolean" @@ -298,20 +298,20 @@ begin else invalid \" end -text{* One might object here that for the case of objects, this is an empty definition. +text\One might object here that for the case of objects, this is an empty definition. The answer is no, we will restrain later on states and objects such that any object has its oid stored inside the object (so the ref, under which an object can be referenced in the store will represented in the object itself). For such well-formed stores that satisfy this invariant (the WFF-invariant), the referential equality and the -strong equality---and therefore the strict equality on sets in the sense above---coincides.*} +strong equality---and therefore the strict equality on sets in the sense above---coincides.\ -text{* Property proof in terms of @{term "profile_bin\<^sub>S\<^sub>t\<^sub>r\<^sub>o\<^sub>n\<^sub>g\<^sub>E\<^sub>q_\<^sub>v_\<^sub>v"}*} +text\Property proof in terms of @{term "profile_bin\<^sub>S\<^sub>t\<^sub>r\<^sub>o\<^sub>n\<^sub>g\<^sub>E\<^sub>q_\<^sub>v_\<^sub>v"}\ interpretation StrictRefEq\<^sub>S\<^sub>e\<^sub>t : profile_bin\<^sub>S\<^sub>t\<^sub>r\<^sub>o\<^sub>n\<^sub>g\<^sub>E\<^sub>q_\<^sub>v_\<^sub>v "\ x y. (x::('\,'\::null)Set) \ y" by unfold_locales (auto simp: StrictRefEq\<^sub>S\<^sub>e\<^sub>t) -subsection{* Constants: mtSet *} +subsection\Constants: mtSet\ definition mtSet::"('\,'\::null) Set" ("Set{}") where "Set{} \ (\ \. Abs_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e \\{}::'\ set\\ )" @@ -334,10 +334,10 @@ lemma [simp,code_unfold]: "const Set{}" by(simp add: const_def mtSet_def) -text{* Note that the collection types in OCL allow for null to be included; - however, there is the null-collection into which inclusion yields invalid. *} +text\Note that the collection types in OCL allow for null to be included; + however, there is the null-collection into which inclusion yields invalid.\ -subsection{* Definition: Including *} +subsection\Definition: Including\ definition OclIncluding :: "[('\,'\::null) Set,('\,'\) val] \ ('\,'\) Set" where "OclIncluding x y = (\ \. if (\ x) \ = true \ \ (\ y) \ = true \ @@ -373,7 +373,7 @@ translations "Set{x}" == "CONST OclIncluding (Set{}) x " -subsection{* Definition: Excluding *} +subsection\Definition: Excluding\ definition OclExcluding :: "[('\,'\::null) Set,('\,'\) val] \ ('\,'\) Set" where "OclExcluding x y = (\ \. if (\ x) \ = true \ \ (\ y) \ = true \ @@ -409,7 +409,7 @@ proof - qed -subsection{* Definition: Includes *} +subsection\Definition: Includes\ definition OclIncludes :: "[('\,'\::null) Set,('\,'\) val] \ '\ Boolean" where "OclIncludes x y = (\ \. if (\ x) \ = true \ \ (\ y) \ = true \ @@ -421,21 +421,21 @@ interpretation OclIncludes : profile_bin\<^sub>d_\<^sub>v OclIncludes "\ by(unfold_locales, auto simp:OclIncludes_def bot_option_def null_option_def invalid_def) -subsection{* Definition: Excludes *} +subsection\Definition: Excludes\ definition OclExcludes :: "[('\,'\::null) Set,('\,'\) val] \ '\ Boolean" where "OclExcludes x y = (not(OclIncludes x y))" notation OclExcludes ("_->excludes\<^sub>S\<^sub>e\<^sub>t'(_')" (*[66,65]65*)) -text{* The case of the size definition is somewhat special, we admit +text\The case of the size definition is somewhat special, we admit explicitly in Featherweight OCL the possibility of infinite sets. For the size definition, this requires an extra condition that assures -that the cardinality of the set is actually a defined integer. *} +that the cardinality of the set is actually a defined integer.\ interpretation OclExcludes : profile_bin\<^sub>d_\<^sub>v OclExcludes "\x y. \\y \ \\Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e x\\\\" by(unfold_locales, auto simp:OclExcludes_def OclIncludes_def OclNot_def bot_option_def null_option_def invalid_def) -subsection{* Definition: Size *} +subsection\Definition: Size\ definition OclSize :: "('\,'\::null)Set \ '\ Integer" where "OclSize x = (\ \. if (\ x) \ = true \ \ finite(\\Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e (x \)\\) @@ -444,16 +444,16 @@ where "OclSize x = (\ \. if (\ x) \ = true \ \ notation (* standard ascii syntax *) OclSize ("_->size\<^sub>S\<^sub>e\<^sub>t'(')" (*[66]*)) -text{* The following definition follows the requirement of the +text\The following definition follows the requirement of the standard to treat null as neutral element of sets. It is a well-documented exception from the general strictness rule and the rule that the distinguished argument self should -be non-null. *} +be non-null.\ (*TODO Locale - Equivalent*) -subsection{* Definition: IsEmpty *} +subsection\Definition: IsEmpty\ definition OclIsEmpty :: "('\,'\::null) Set \ '\ Boolean" where "OclIsEmpty x = ((\ x and not (\ x)) or ((OclSize x) \ \))" @@ -462,7 +462,7 @@ notation OclIsEmpty ("_->isEmpty\<^sub>S\<^sub>e\<^sub>t'(')" (*[66]*)) (*TODO Locale - Equivalent*) -subsection{* Definition: NotEmpty *} +subsection\Definition: NotEmpty\ definition OclNotEmpty :: "('\,'\::null) Set \ '\ Boolean" where "OclNotEmpty x = not(OclIsEmpty x)" @@ -470,7 +470,7 @@ notation OclNotEmpty ("_->notEmpty\<^sub>S\<^sub>e\<^sub>t'(')" (*[66]*)) (*TODO Locale - Equivalent*) -subsection{* Definition: Any *} +subsection\Definition: Any\ (* Slight breach of naming convention in order to avoid naming conflict on constant.*) definition OclANY :: "[('\,'\::null) Set] \ ('\,'\) val" @@ -491,10 +491,10 @@ we have to go for a direct---restricted---definition. *) -subsection{* Definition: Forall *} +subsection\Definition: Forall\ -text{* The definition of OclForall mimics the one of @{term "OclAnd"}: -OclForall is not a strict operation. *} +text\The definition of OclForall mimics the one of @{term "OclAnd"}: +OclForall is not a strict operation.\ definition OclForall :: "[('\,'\::null)Set,('\,'\)val\('\)Boolean] \ '\ Boolean" where "OclForall S P = (\ \. if (\ S) \ = true \ then if (\x\\\Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e (S \)\\. P(\ _. x) \ = false \) @@ -512,9 +512,9 @@ translations (*TODO Locale - Equivalent*) -subsection{* Definition: Exists *} +subsection\Definition: Exists\ -text{* Like OclForall, OclExists is also not strict. *} +text\Like OclForall, OclExists is also not strict.\ definition OclExists :: "[('\,'\::null) Set,('\,'\)val\('\)Boolean] \ '\ Boolean" where "OclExists S P = not(UML_Set.OclForall S (\ X. not (P X)))" @@ -525,7 +525,7 @@ translations (*TODO Locale - Equivalent*) -subsection{* Definition: Iterate *} +subsection\Definition: Iterate\ definition OclIterate :: "[('\,'\::null) Set,('\,'\::null)val, ('\,'\)val\('\,'\)val\('\,'\)val] \ ('\,'\)val" @@ -540,7 +540,7 @@ translations (*TODO Locale - Equivalent*) -subsection{* Definition: Select *} +subsection\Definition: Select\ definition OclSelect :: "[('\,'\::null)Set,('\,'\)val\('\)Boolean] \ ('\,'\)Set" where "OclSelect S P = (\\. if (\ S) \ = true \ @@ -555,7 +555,7 @@ translations (*TODO Locale - Equivalent*) -subsection{* Definition: Reject *} +subsection\Definition: Reject\ definition OclReject :: "[('\,'\::null)Set,('\,'\)val\('\)Boolean] \ ('\,'\::null)Set" where "OclReject S P = OclSelect S (not o P)" @@ -566,7 +566,7 @@ translations (*TODO Locale - Equivalent*) -subsection{* Definition: IncludesAll *} +subsection\Definition: IncludesAll\ definition OclIncludesAll :: "[('\,'\::null) Set,('\,'\) Set] \ '\ Boolean" where "OclIncludesAll x y = (\ \. if (\ x) \ = true \ \ (\ y) \ = true \ @@ -577,7 +577,7 @@ notation OclIncludesAll ("_->includesAll\<^sub>S\<^sub>e\<^sub>t'(_')" (*[66,6 interpretation OclIncludesAll : profile_bin\<^sub>d_\<^sub>d OclIncludesAll "\x y. \\\\Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e y\\ \ \\Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e x\\\\" by(unfold_locales, auto simp:OclIncludesAll_def bot_option_def null_option_def invalid_def) -subsection{* Definition: ExcludesAll *} +subsection\Definition: ExcludesAll\ definition OclExcludesAll :: "[('\,'\::null) Set,('\,'\) Set] \ '\ Boolean" where "OclExcludesAll x y = (\ \. if (\ x) \ = true \ \ (\ y) \ = true \ @@ -588,7 +588,7 @@ notation OclExcludesAll ("_->excludesAll\<^sub>S\<^sub>e\<^sub>t'(_')" (*[66,65 interpretation OclExcludesAll : profile_bin\<^sub>d_\<^sub>d OclExcludesAll "\x y. \\\\Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e y\\ \ \\Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e x\\ = {}\\" by(unfold_locales, auto simp:OclExcludesAll_def bot_option_def null_option_def invalid_def) -subsection{* Definition: Union *} +subsection\Definition: Union\ definition OclUnion :: "[('\,'\::null) Set,('\,'\) Set] \ ('\,'\) Set" where "OclUnion x y = (\ \. if (\ x) \ = true \ \ (\ y) \ = true \ @@ -627,7 +627,7 @@ proof - done qed -subsection{* Definition: Intersection *} +subsection\Definition: Intersection\ definition OclIntersection :: "[('\,'\::null) Set,('\,'\) Set] \ ('\,'\) Set" where "OclIntersection x y = (\ \. if (\ x) \ = true \ \ (\ y) \ = true \ @@ -667,7 +667,7 @@ proof - done qed -subsection{* Definition (future operators) *} +subsection\Definition (future operators)\ consts (* abstract set collection operations *) OclCount :: "[('\,'\::null) Set,('\,'\) Set] \ '\ Integer" @@ -676,9 +676,9 @@ consts (* abstract set collection operations *) notation OclCount ("_->count\<^sub>S\<^sub>e\<^sub>t'(_')" (*[66,65]65*)) notation OclSum ("_->sum\<^sub>S\<^sub>e\<^sub>t'(')" (*[66]*)) -subsection{* Logical Properties *} +subsection\Logical Properties\ -text{* OclIncluding *} +text\OclIncluding\ lemma OclIncluding_valid_args_valid: "(\ \ \(X->including\<^sub>S\<^sub>e\<^sub>t(x))) = ((\ \(\ X)) \ (\ \(\ x)))" @@ -688,10 +688,10 @@ lemma OclIncluding_valid_args_valid''[simp,code_unfold]: "\(X->including\<^sub>S\<^sub>e\<^sub>t(x)) = ((\ X) and (\ x))" by (simp add: OclIncluding.def_valid_then_def) -text{* etc. etc. *} -text_raw{* \isatagafp *} +text\etc. etc.\ +text_raw\\isatagafp\ -text{* OclExcluding *} +text\OclExcluding\ lemma OclExcluding_valid_args_valid: "(\ \ \(X->excluding\<^sub>S\<^sub>e\<^sub>t(x))) = ((\ \(\ X)) \ (\ \(\ x)))" @@ -701,7 +701,7 @@ lemma OclExcluding_valid_args_valid''[simp,code_unfold]: "\(X->excluding\<^sub>S\<^sub>e\<^sub>t(x)) = ((\ X) and (\ x))" by (simp add: OclExcluding.def_valid_then_def) -text{* OclIncludes *} +text\OclIncludes\ lemma OclIncludes_valid_args_valid: "(\ \ \(X->includes\<^sub>S\<^sub>e\<^sub>t(x))) = ((\ \(\ X)) \ (\ \(\ x)))" @@ -711,7 +711,7 @@ lemma OclIncludes_valid_args_valid''[simp,code_unfold]: "\(X->includes\<^sub>S\<^sub>e\<^sub>t(x)) = ((\ X) and (\ x))" by (simp add: OclIncludes.def_valid_then_def) -text{* OclExcludes *} +text\OclExcludes\ lemma OclExcludes_valid_args_valid: "(\ \ \(X->excludes\<^sub>S\<^sub>e\<^sub>t(x))) = ((\ \(\ X)) \ (\ \(\ x)))" @@ -721,7 +721,7 @@ lemma OclExcludes_valid_args_valid''[simp,code_unfold]: "\(X->excludes\<^sub>S\<^sub>e\<^sub>t(x)) = ((\ X) and (\ x))" by (simp add: OclExcludes.def_valid_then_def) -text{* OclSize *} +text\OclSize\ lemma OclSize_defined_args_valid: "\ \ \ (X->size\<^sub>S\<^sub>e\<^sub>t()) \ \ \ \ X" by(auto simp: OclSize_def OclValid_def true_def valid_def false_def StrongEq_def @@ -755,7 +755,7 @@ lemma size_defined': apply(simp add: defined_def bot_option_def bot_fun_def null_option_def null_fun_def X_finite) done -text{* OclIsEmpty *} +text\OclIsEmpty\ lemma OclIsEmpty_defined_args_valid:"\ \ \ (X->isEmpty\<^sub>S\<^sub>e\<^sub>t()) \ \ \ \ X" apply(auto simp: OclIsEmpty_def OclValid_def defined_def valid_def false_def true_def @@ -780,7 +780,7 @@ lemma OclIsEmpty_infinite: "\ \ \ X \ \I\<^sub>n\<^sub>t\<^sub>e\<^sub>g\<^sub>e\<^sub>r valid_def bot_fun_def false_def true_def invalid_def) -text{* OclNotEmpty *} +text\OclNotEmpty\ lemma OclNotEmpty_defined_args_valid:"\ \ \ (X->notEmpty\<^sub>S\<^sub>e\<^sub>t()) \ \ \ \ X" by (metis (hide_lams, no_types) OclNotEmpty_def OclNot_defargs OclNot_not foundation6 foundation9 @@ -808,7 +808,7 @@ lemma OclNotEmpty_has_elt : "\ \ \ X \ simp_all add: false_def true_def bot_option_def bot_fun_def OclInt0_def) by (metis equals0I) -text{* OclANY *} +text\OclANY\ lemma OclANY_defined_args_valid: "\ \ \ (X->any\<^sub>S\<^sub>e\<^sub>t()) \ \ \ \ X" by(auto simp: OclANY_def OclValid_def true_def valid_def false_def StrongEq_def @@ -852,19 +852,19 @@ lemma OclANY_valid_args_valid''[simp,code_unfold]: by(auto intro!: OclANY_valid_args_valid transform2_rev) (* and higher order ones : forall, exists, iterate, select, reject... *) -text_raw{* \endisatagafp *} +text_raw\\endisatagafp\ -subsection{* Execution Laws with Invalid or Null or Infinite Set as Argument *} +subsection\Execution Laws with Invalid or Null or Infinite Set as Argument\ -text{* OclIncluding *} (* properties already generated by the corresponding locale *) +text\OclIncluding\ (* properties already generated by the corresponding locale *) -text{* OclExcluding *} (* properties already generated by the corresponding locale *) +text\OclExcluding\ (* properties already generated by the corresponding locale *) -text{* OclIncludes *} (* properties already generated by the corresponding locale *) +text\OclIncludes\ (* properties already generated by the corresponding locale *) -text{* OclExcludes *} (* properties already generated by the corresponding locale *) +text\OclExcludes\ (* properties already generated by the corresponding locale *) -text{* OclSize *} +text\OclSize\ lemma OclSize_invalid[simp,code_unfold]:"(invalid->size\<^sub>S\<^sub>e\<^sub>t()) = invalid" by(simp add: bot_fun_def OclSize_def invalid_def defined_def valid_def false_def true_def) @@ -874,7 +874,7 @@ by(rule ext, simp add: bot_fun_def null_fun_def null_is_valid OclSize_def invalid_def defined_def valid_def false_def true_def) -text{* OclIsEmpty *} +text\OclIsEmpty\ lemma OclIsEmpty_invalid[simp,code_unfold]:"(invalid->isEmpty\<^sub>S\<^sub>e\<^sub>t()) = invalid" by(simp add: OclIsEmpty_def) @@ -882,7 +882,7 @@ by(simp add: OclIsEmpty_def) lemma OclIsEmpty_null[simp,code_unfold]:"(null->isEmpty\<^sub>S\<^sub>e\<^sub>t()) = true" by(simp add: OclIsEmpty_def) -text{* OclNotEmpty *} +text\OclNotEmpty\ lemma OclNotEmpty_invalid[simp,code_unfold]:"(invalid->notEmpty\<^sub>S\<^sub>e\<^sub>t()) = invalid" by(simp add: OclNotEmpty_def) @@ -890,7 +890,7 @@ by(simp add: OclNotEmpty_def) lemma OclNotEmpty_null[simp,code_unfold]:"(null->notEmpty\<^sub>S\<^sub>e\<^sub>t()) = false" by(simp add: OclNotEmpty_def) -text{* OclANY *} +text\OclANY\ lemma OclANY_invalid[simp,code_unfold]:"(invalid->any\<^sub>S\<^sub>e\<^sub>t()) = invalid" by(simp add: bot_fun_def OclANY_def invalid_def defined_def valid_def false_def true_def) @@ -898,7 +898,7 @@ by(simp add: bot_fun_def OclANY_def invalid_def defined_def valid_def false_def lemma OclANY_null[simp,code_unfold]:"(null->any\<^sub>S\<^sub>e\<^sub>t()) = null" by(simp add: OclANY_def false_def true_def) -text{* OclForall *} +text\OclForall\ lemma OclForall_invalid[simp,code_unfold]:"invalid->forAll\<^sub>S\<^sub>e\<^sub>t(a| P a) = invalid" by(simp add: bot_fun_def invalid_def OclForall_def defined_def valid_def false_def true_def) @@ -906,7 +906,7 @@ by(simp add: bot_fun_def invalid_def OclForall_def defined_def valid_def false_d lemma OclForall_null[simp,code_unfold]:"null->forAll\<^sub>S\<^sub>e\<^sub>t(a | P a) = invalid" by(simp add: bot_fun_def invalid_def OclForall_def defined_def valid_def false_def true_def) -text{* OclExists *} +text\OclExists\ lemma OclExists_invalid[simp,code_unfold]:"invalid->exists\<^sub>S\<^sub>e\<^sub>t(a| P a) = invalid" by(simp add: OclExists_def) @@ -914,7 +914,7 @@ by(simp add: OclExists_def) lemma OclExists_null[simp,code_unfold]:"null->exists\<^sub>S\<^sub>e\<^sub>t(a | P a) = invalid" by(simp add: OclExists_def) -text{* OclIterate *} +text\OclIterate\ lemma OclIterate_invalid[simp,code_unfold]:"invalid->iterate\<^sub>S\<^sub>e\<^sub>t(a; x = A | P a x) = invalid" by(simp add: bot_fun_def invalid_def OclIterate_def defined_def valid_def false_def true_def) @@ -926,7 +926,7 @@ by(simp add: bot_fun_def invalid_def OclIterate_def defined_def valid_def false_ lemma OclIterate_invalid_args[simp,code_unfold]:"S->iterate\<^sub>S\<^sub>e\<^sub>t(a; x = invalid | P a x) = invalid" by(simp add: bot_fun_def invalid_def OclIterate_def defined_def valid_def false_def true_def) -text{* An open question is this ... *} +text\An open question is this ...\ lemma (*OclIterate_null_args[simp,code_unfold]:*) "S->iterate\<^sub>S\<^sub>e\<^sub>t(a; x = null | P a x) = invalid" oops (* In the definition above, this does not hold in general. @@ -939,7 +939,7 @@ apply(insert non_finite [THEN OclSize_infinite]) apply(subst (asm) foundation9, simp) by(metis OclIterate_def OclValid_def invalid_def) -text{* OclSelect *} +text\OclSelect\ lemma OclSelect_invalid[simp,code_unfold]:"invalid->select\<^sub>S\<^sub>e\<^sub>t(a | P a) = invalid" by(simp add: bot_fun_def invalid_def OclSelect_def defined_def valid_def false_def true_def) @@ -947,7 +947,7 @@ by(simp add: bot_fun_def invalid_def OclSelect_def defined_def valid_def false_d lemma OclSelect_null[simp,code_unfold]:"null->select\<^sub>S\<^sub>e\<^sub>t(a | P a) = invalid" by(simp add: bot_fun_def invalid_def OclSelect_def defined_def valid_def false_def true_def) -text{* OclReject *} +text\OclReject\ lemma OclReject_invalid[simp,code_unfold]:"invalid->reject\<^sub>S\<^sub>e\<^sub>t(a | P a) = invalid" by(simp add: OclReject_def) @@ -955,9 +955,9 @@ by(simp add: OclReject_def) lemma OclReject_null[simp,code_unfold]:"null->reject\<^sub>S\<^sub>e\<^sub>t(a | P a) = invalid" by(simp add: OclReject_def) -text_raw{* \isatagafp *} +text_raw\\isatagafp\ -subsubsection{* Context Passing *} +subsubsection\Context Passing\ lemma cp_OclIncludes1: "(X->includes\<^sub>S\<^sub>e\<^sub>t(x)) \ = (X->includes\<^sub>S\<^sub>e\<^sub>t(\ _. x \)) \" @@ -1040,7 +1040,7 @@ lemmas cp_intro''\<^sub>S\<^sub>e\<^sub>t[intro!,simp,code_unfold] = cp_OclNotEmpty [THEN allI[THEN allI[THEN cpI1], of "OclNotEmpty"]] cp_OclANY [THEN allI[THEN allI[THEN cpI1], of "OclANY"]] -subsubsection{* Const *} +subsubsection\Const\ lemma const_OclIncluding[simp,code_unfold] : assumes const_x : "const x" @@ -1068,10 +1068,10 @@ lemma const_OclIncluding[simp,code_unfold] : apply(subst const_charn[OF const_S]) by simp qed -text_raw{* \endisatagafp *} +text_raw\\endisatagafp\ -subsection{* General Algebraic Execution Rules *} -subsubsection{* Execution Rules on Including *} +subsection\General Algebraic Execution Rules\ +subsubsection\Execution Rules on Including\ lemma OclIncluding_finite_rep_set : assumes X_def : "\ \ \ X" @@ -1221,7 +1221,7 @@ proof - qed -subsubsection{* Execution Rules on Excluding *} +subsubsection\Execution Rules on Excluding\ lemma OclExcluding_finite_rep_set : assumes X_def : "\ \ \ X" @@ -1508,7 +1508,7 @@ proof - qed -text{* One would like a generic theorem of the form: +text\One would like a generic theorem of the form: \begin{isar}[mathescape] lemma OclExcluding_charn_exec: "(X->including$_{Set}$(x::('$\mathfrak{A}$,'a::null)val)->excluding$_{Set}$(y)) = @@ -1522,14 +1522,14 @@ Unfortunately, this does not hold in general, since referential equality is an overloaded concept and has to be defined for each type individually. Consequently, it is only valid for concrete type instances for Boolean, Integer, and Sets thereof... -*} +\ -text{* The computational law \emph{OclExcluding-charn-exec} becomes generic since it +text\The computational law \emph{OclExcluding-charn-exec} becomes generic since it uses strict equality which in itself is generic. It is possible to prove the following generic theorem and instantiate it later (using properties that link the polymorphic logical strong equality with the concrete instance -of strict quality).*} +of strict quality).\ lemma OclExcluding_charn_exec: assumes strict1: "(invalid \ y) = invalid" and strict2: "(x \ invalid) = invalid" @@ -1632,7 +1632,7 @@ by(rule OclExcluding_charn_exec[OF StrictRefEq\<^sub>S\<^sub>e\<^sub>t.strict1 S StrictRefEq\<^sub>S\<^sub>e\<^sub>t.cp0 StrictRefEq\<^sub>S\<^sub>e\<^sub>t.StrictRefEq_vs_StrongEq], simp_all) -subsubsection{* Execution Rules on Includes *} +subsubsection\Execution Rules on Includes\ lemma OclIncludes_charn0[simp]: assumes val_x:"\ \ (\ x)" @@ -1698,7 +1698,7 @@ proof - by(metis foundation22 foundation6 foundation9 neq) qed -text{* Here is again a generic theorem similar as above. *} +text\Here is again a generic theorem similar as above.\ lemma OclIncludes_execute_generic: assumes strict1: "(invalid \ y) = invalid" @@ -1813,7 +1813,7 @@ qed lemmas OclIncludes_including\<^sub>I\<^sub>n\<^sub>t\<^sub>e\<^sub>g\<^sub>e\<^sub>r = OclIncludes_including_generic[OF OclIncludes_execute\<^sub>I\<^sub>n\<^sub>t\<^sub>e\<^sub>g\<^sub>e\<^sub>r StrictRefEq\<^sub>I\<^sub>n\<^sub>t\<^sub>e\<^sub>g\<^sub>e\<^sub>r.def_homo] -subsubsection{* Execution Rules on Excludes *} +subsubsection\Execution Rules on Excludes\ lemma OclExcludes_charn1: assumes def_X:"\ \ (\ X)" @@ -1834,7 +1834,7 @@ proof - by(simp add: OclAnd_def def_X[simplified OclValid_def] val_x[simplified OclValid_def] true_def) qed -subsubsection{* Execution Rules on Size *} +subsubsection\Execution Rules on Size\ lemma [simp,code_unfold]: "Set{} ->size\<^sub>S\<^sub>e\<^sub>t() = \" apply(rule ext) @@ -1922,7 +1922,7 @@ proof - qed qed -subsubsection{* Execution Rules on IsEmpty *} +subsubsection\Execution Rules on IsEmpty\ lemma [simp,code_unfold]: "Set{}->isEmpty\<^sub>S\<^sub>e\<^sub>t() = true" by(simp add: OclIsEmpty_def) @@ -1960,7 +1960,7 @@ proof - OclIncluding_notempty_rep_set[OF X_def a_val]) qed -subsubsection{* Execution Rules on NotEmpty *} +subsubsection\Execution Rules on NotEmpty\ lemma [simp,code_unfold]: "Set{}->notEmpty\<^sub>S\<^sub>e\<^sub>t() = false" by(simp add: OclNotEmpty_def) @@ -1974,7 +1974,7 @@ shows "X->including\<^sub>S\<^sub>e\<^sub>t(a)->notEmpty\<^sub>S\<^sub>e\<^sub>t apply(subst cp_OclNot, subst OclIsEmpty_including, simp_all add: assms) by (metis OclNot4 cp_OclNot) -subsubsection{* Execution Rules on Any *} +subsubsection\Execution Rules on Any\ lemma [simp,code_unfold]: "Set{}->any\<^sub>S\<^sub>e\<^sub>t() = null" by(rule ext, simp add: OclANY_def, simp add: false_def true_def) @@ -2005,7 +2005,7 @@ lemma OclANY_singleton_exec[simp,code_unfold]: simp add: mtSet_defined[simplified mtSet_def] valid_def bot_fun_def) by(simp add: cp_OclAnd[symmetric], rule impI, simp add: false_def true_def) -subsubsection{* Execution Rules on Forall *} +subsubsection\Execution Rules on Forall\ lemma OclForall_mtSet_exec[simp,code_unfold] :"((Set{})->forAll\<^sub>S\<^sub>e\<^sub>t(z| P(z))) = true" apply(simp add: OclForall_def) @@ -2014,7 +2014,7 @@ apply(subst Abs_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e_inverse, simp_all add: true_ done -text{* The following rule is a main theorem of our approach: From a denotational definition +text\The following rule is a main theorem of our approach: From a denotational definition that assures consistency, but may be --- as in the case of the @{term "X->forAll\<^sub>S\<^sub>e\<^sub>t(x | P x)"} --- dauntingly complex, we derive operational rules that can serve as a gold-standard for operational execution, since they may be evaluated in whatever situation and according to whatever strategy. @@ -2029,7 +2029,7 @@ or even: @{term "Integer ->forAll\<^sub>S\<^sub>e\<^sub>t(x | (Integer ->forAll\<^sub>S\<^sub>e\<^sub>t(y | x +\<^sub>i\<^sub>n\<^sub>t y \ y +\<^sub>i\<^sub>n\<^sub>t x)))"} are valid OCL statements in any context $\tau$. -*} +\ theorem OclForall_including_exec[simp,code_unfold] : assumes cp0 : "cp P" @@ -2215,7 +2215,7 @@ qed -subsubsection{* Execution Rules on Exists *} +subsubsection\Execution Rules on Exists\ lemma OclExists_mtSet_exec[simp,code_unfold] : "((Set{})->exists\<^sub>S\<^sub>e\<^sub>t(z | P(z))) = false" @@ -2230,7 +2230,7 @@ lemma OclExists_including_exec[simp,code_unfold] : by(simp add: OclExists_def OclOr_def cp OclNot_inject) -subsubsection{* Execution Rules on Iterate *} +subsubsection\Execution Rules on Iterate\ lemma OclIterate_empty[simp,code_unfold]: "((Set{})->iterate\<^sub>S\<^sub>e\<^sub>t(a; x = A | P a x)) = A" proof - @@ -2244,7 +2244,7 @@ proof - done qed -text{* In particular, this does hold for A = null. *} +text\In particular, this does hold for A = null.\ lemma OclIterate_including: assumes S_finite: "\ \ \(S->size\<^sub>S\<^sub>e\<^sub>t())" @@ -2314,7 +2314,7 @@ proof - by(subst Finite_Set.comp_fun_commute.fold_insert_remove[OF F_commute], simp+) qed -subsubsection{* Execution Rules on Select *} +subsubsection\Execution Rules on Select\ lemma OclSelect_mtSet_exec[simp,code_unfold]: "OclSelect mtSet P = mtSet" apply(rule ext, rename_tac \) @@ -2560,7 +2560,7 @@ proof - done qed -subsubsection{* Execution Rules on Reject *} +subsubsection\Execution Rules on Reject\ lemma OclReject_mtSet_exec[simp,code_unfold]: "OclReject mtSet P = mtSet" by(simp add: OclReject_def) @@ -2571,9 +2571,9 @@ lemma OclReject_including_exec[simp,code_unfold]: apply(simp add: OclReject_def comp_def, rule OclSelect_including_exec) by (metis assms cp_intro'(5)) -subsubsection{* Execution Rules Combining Previous Operators *} +subsubsection\Execution Rules Combining Previous Operators\ -text{* OclIncluding *} +text\OclIncluding\ (* logical level : *) lemma OclIncluding_idem0 : @@ -2615,7 +2615,7 @@ proof - done qed -text{* OclExcluding *} +text\OclExcluding\ (* logical level : *) lemma OclExcluding_idem0 : @@ -2657,7 +2657,7 @@ proof - done qed -text{* OclIncludes *} +text\OclIncludes\ lemma OclIncludes_any[simp,code_unfold]: @@ -2748,7 +2748,7 @@ proof - simp add: false_def true_def OclIf_false[simplified false_def] invalid_def) qed -text{* OclSize *} +text\OclSize\ lemma [simp,code_unfold]: "\ (Set{} ->size\<^sub>S\<^sub>e\<^sub>t()) = true" by simp @@ -2869,7 +2869,7 @@ lemma [simp]: by(simp add: size_defined[OF X_finite] del: OclSize_including_exec) -text{* OclForall *} +text\OclForall\ lemma OclForall_rep_set_false: assumes "\ \ \ X" @@ -2923,7 +2923,7 @@ lemma OclForall_not_includes : apply(simp add: OclForall_rep_set_false[OF x_def], simp add: OclIncludes_def OclValid_def y_def[simplified OclValid_def]) apply(insert Set_inv_lemma[OF x_def], simp add: valid_def false_def true_def bot_fun_def) -by(rule iffI, metis set_rev_mp, metis subsetI) +by(rule iffI, metis rev_subsetD, metis subsetI) lemma OclForall_iterate: assumes S_finite: "finite \\Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e (S \)\\" @@ -3012,7 +3012,7 @@ proof - by (simp add: assms) qed -text{* Strict Equality *} +text\Strict Equality\ lemma StrictRefEq\<^sub>S\<^sub>e\<^sub>t_defined : assumes x_def: "\ \ \ x" @@ -3139,7 +3139,7 @@ lemma const_StrictRefEq\<^sub>S\<^sub>e\<^sub>t_including : apply(rule StrictRefEq\<^sub>S\<^sub>e\<^sub>t.const, assumption) by(rule const_OclIncluding) -subsection{* Test Statements *} +subsection\Test Statements\ Assert "(\ \ (Set{\_. \\x\\} \ Set{\_. \\x\\}))" Assert "(\ \ (Set{\_. \x\} \ Set{\_. \x\}))" diff --git a/Featherweight_OCL/document/root.bib b/Featherweight_OCL/document/root.bib index 1d6fde6..def7d20 100644 --- a/Featherweight_OCL/document/root.bib +++ b/Featherweight_OCL/document/root.bib @@ -9,7 +9,7 @@ # {\providecommand{\isbn}{\textsc{isbn}} } # {\providecommand{\Cpp}{C++} } # {\providecommand{\Specsharp}{Spec\#} } - # {\providecommand{\doi}[1]{\href{http://dx.doi.org/#1}{doi: + # {\providecommand{\doi}[1]{\href{https://doi.org/#1}{doi: {\urlstyle{rm}\nolinkurl{#1}}}}} } @STRING{conf-tphols="{TPHOLs}" } @STRING{iso = {International Organization for Standardization} } @@ -1425,7 +1425,7 @@ year = 2006, pages = {160--174}, crossref = {altenkirch.ea:types:2007}, - url = {http://dx.doi.org/10.1007/978-3-540-74464-1_11}, + url = {https://doi.org/10.1007/978-3-540-74464-1_11}, doi = {10.1007/978-3-540-74464-1_11}, timestamp = {Thu, 04 Sep 2014 22:14:34 +0200}, biburl = {http://dblp.uni-trier.de/rec/bib/conf/types/HaftmannW06} diff --git a/Featherweight_OCL/document/root.tex b/Featherweight_OCL/document/root.tex index d9ac898..9ea4bc3 100644 --- a/Featherweight_OCL/document/root.tex +++ b/Featherweight_OCL/document/root.tex @@ -120,7 +120,7 @@ \newcommand{\ie}{i.\,e.\xspace} \newcommand{\eg}{e.\,g.\xspace} -\newenvironment{isamarkuplazy_text}{\par \isacommand{lazy{\isacharunderscore}text}\isamarkupfalse\isacharverbatimopen\isastyletext\begin{isapar}}{\end{isapar}\isacharverbatimclose} +\newenvironment{isamarkuplazy_text}{\par \isacommand{lazy{\isacharunderscore}text}\isamarkupfalse\isacartoucheopen\isastyletext\begin{isapar}}{\end{isapar}\isacartoucheclose} \renewcommand{\isasymguillemotleft}{\isatext{\textquotedblleft}} \renewcommand{\isasymguillemotright}{\isatext{\textquotedblright}} \begin{document} diff --git a/Featherweight_OCL/examples/Employee_Model/Analysis/Analysis_OCL.thy b/Featherweight_OCL/examples/Employee_Model/Analysis/Analysis_OCL.thy index 5ec6b3d..e9cd790 100644 --- a/Featherweight_OCL/examples/Employee_Model/Analysis/Analysis_OCL.thy +++ b/Featherweight_OCL/examples/Employee_Model/Analysis/Analysis_OCL.thy @@ -45,10 +45,10 @@ theory imports Analysis_UML begin -text {* \label{ex:employee-analysis:ocl} *} +text \\label{ex:employee-analysis:ocl}\ -section{* OCL Part: Invariant *} -text{* These recursive predicates can be defined conservatively +section\OCL Part: Invariant\ +text\These recursive predicates can be defined conservatively by greatest fix-point constructions---automatically. See~\cite{brucker.ea:hol-ocl-book:2006,brucker:interactive:2007} for details. For the purpose of this example, we state them as axioms @@ -58,7 +58,7 @@ here. context Person inv label : self .boss <> null implies (self .salary \ ((self .boss) .salary)) \end{ocl} -*} +\ definition Person_label\<^sub>i\<^sub>n\<^sub>v :: "Person \ Boolean" where "Person_label\<^sub>i\<^sub>n\<^sub>v (self) \ @@ -87,7 +87,7 @@ lemma REC_pre : "\ \ Person_label\<^sub>g\<^sub>l\<^sub>o\<^sub> oops (* Attempt to allegiate the burden of he following axiomatizations: could be a witness for a constant specification ...*) -text{* This allows to state a predicate: *} +text\This allows to state a predicate:\ axiomatization inv\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n\<^sub>_\<^sub>l\<^sub>a\<^sub>b\<^sub>e\<^sub>l :: "Person \ Boolean" where inv\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n\<^sub>_\<^sub>l\<^sub>a\<^sub>b\<^sub>e\<^sub>l_def: @@ -121,8 +121,8 @@ lemma inv_2 : (\ \ (inv\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n\<^sub>_\<^sub>l\<^sub>a\<^sub>b\<^sub>e\<^sub>l\<^sub>A\<^sub>T\<^sub>p\<^sub>r\<^sub>e(self .boss@pre)))))" oops (* Let's hope that this holds ... *) -text{* A very first attempt to characterize the axiomatization by an inductive -definition - this can not be the last word since too weak (should be equality!) *} +text\A very first attempt to characterize the axiomatization by an inductive +definition - this can not be the last word since too weak (should be equality!)\ coinductive inv :: "Person \ (\)st \ bool" where "(\ \ (\ self)) \ ((\ \ (self .boss \ null)) \ (\ \ (self .boss <> null) \ (\ \ (self .boss .salary \\<^sub>i\<^sub>n\<^sub>t self .salary)) \ @@ -130,8 +130,8 @@ coinductive inv :: "Person \ (\)st \ bool" where \ ( inv self \)" -section{* OCL Part: The Contract of a Recursive Query *} -text{* The original specification of a recursive query : +section\OCL Part: The Contract of a Recursive Query\ +text\The original specification of a recursive query : \begin{ocl} context Person::contents():Set(Integer) pre: true @@ -139,11 +139,11 @@ post: result = if self.boss = null then Set{i} else self.boss.contents()->including(i) endif -\end{ocl} *} +\end{ocl}\ -text{* For the case of recursive queries, we use at present just axiomatizations: *} +text\For the case of recursive queries, we use at present just axiomatizations:\ axiomatization contents :: "Person \ Set_Integer" ("(1(_).contents'('))" 50) where contents_def: @@ -206,8 +206,8 @@ interpretation contents : contract0 "contents" "\ self. true" qed -text{* Specializing @{thm contents.unfold2}, one gets the following more practical rewrite -rule that is amenable to symbolic evaluation: *} +text\Specializing @{thm contents.unfold2}, one gets the following more practical rewrite +rule that is amenable to symbolic evaluation:\ theorem unfold_contents : assumes "cp E" and "\ \ \ self" @@ -218,8 +218,8 @@ theorem unfold_contents : by(rule contents.unfold2[of _ _ _ "\ X. true"], simp_all add: assms) -text{* Since we have only one interpretation function, we need the corresponding -operation on the pre-state: *} +text\Since we have only one interpretation function, we need the corresponding +operation on the pre-state:\ consts contentsATpre :: "Person \ Set_Integer" ("(1(_).contents@pre'('))" 50) @@ -281,8 +281,8 @@ interpretation contentsATpre : contract0 "contentsATpre" "\ self. true" by(simp add: A B C) qed -text{* Again, we derive via @{thm [source] contents.unfold2} a Knaster-Tarski like Fixpoint rule -that is amenable to symbolic evaluation: *} +text\Again, we derive via @{thm [source] contents.unfold2} a Knaster-Tarski like Fixpoint rule +that is amenable to symbolic evaluation:\ theorem unfold_contentsATpre : assumes "cp E" and "\ \ \ self" @@ -293,11 +293,11 @@ theorem unfold_contentsATpre : by(rule contentsATpre.unfold2[of _ _ _ "\ X. true"], simp_all add: assms) -text{* Note that these \inlineocl{@pre} variants on methods are only available on queries, \ie, -operations without side-effect. *} +text\Note that these \inlineocl{@pre} variants on methods are only available on queries, \ie, +operations without side-effect.\ -section{* OCL Part: The Contract of a User-defined Method *} -text{* +section\OCL Part: The Contract of a User-defined Method\ +text\ The example specification in high-level OCL input syntax reads as follows: \begin{ocl} context Person::insert(x:Integer) @@ -307,7 +307,7 @@ contents() = contents@pre()->including(x) \end{ocl} This boils down to: -*} +\ definition insert :: "Person \Integer \ Void" ("(1(_).insert'(_'))" 50) where "self .insert(x) \ @@ -317,7 +317,7 @@ where "self .insert(x) \ (\ \ ((self).contents() \ (self).contents@pre()->including\<^sub>S\<^sub>e\<^sub>t(x)))) else \ \ res \ invalid)" -text{* The semantic consequences of this definition were computed inside this locale interpretation:*} +text\The semantic consequences of this definition were computed inside this locale interpretation:\ interpretation insert : contract1 "insert" "\ self x. true" "\ self x res. ((self .contents()) \ (self .contents@pre()->including\<^sub>S\<^sub>e\<^sub>t(x)))" @@ -330,7 +330,7 @@ interpretation insert : contract1 "insert" "\ self x. true" by(simp) (* an extremely hacky proof that cries for reformulation and automation - bu *) -text{* The result of this locale interpretation for our @{term insert} contract is the following +text\The result of this locale interpretation for our @{term insert} contract is the following set of properties, which serves as basis for automated deduction on them: \begin{table}[htbp] @@ -357,6 +357,6 @@ set of properties, which serves as basis for automated deduction on them: \label{tab:sem_operation_contract} \end{table} -*} +\ end diff --git a/Featherweight_OCL/examples/Employee_Model/Analysis/Analysis_UML.thy b/Featherweight_OCL/examples/Employee_Model/Analysis/Analysis_UML.thy index a953fbe..6f79303 100644 --- a/Featherweight_OCL/examples/Employee_Model/Analysis/Analysis_UML.thy +++ b/Featherweight_OCL/examples/Employee_Model/Analysis/Analysis_UML.thy @@ -40,7 +40,7 @@ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. ******************************************************************************) -chapter{* Example: The Employee Analysis Model *} (* UML part *) +chapter\Example: The Employee Analysis Model\ (* UML part *) theory Analysis_UML @@ -48,10 +48,10 @@ imports "../../../UML_Main" begin -text {* \label{ex:employee-analysis:uml} *} +text \\label{ex:employee-analysis:uml}\ -section{* Introduction *} -text{* +section\Introduction\ +text\ For certain concepts like classes and class-types, only a generic definition for its resulting semantics can be given. Generic means, there is a function outside HOL that ``compiles'' a concrete, @@ -59,19 +59,19 @@ text{* consisting of a bunch of definitions for classes, accessors, method, casts, and tests for actual types, as well as proofs for the fundamental properties of these operations in this concrete data - model. *} + model.\ -text{* Such generic function or ``compiler'' can be implemented in +text\Such generic function or ``compiler'' can be implemented in Isabelle on the ML level. This has been done, for a semantics following the open-world assumption, for UML 2.0 in~\cite{brucker.ea:extensible:2008-b, brucker:interactive:2007}. In this paper, we follow another approach for UML 2.4: we define the concepts of the compilation informally, and present a concrete - example which is verified in Isabelle/HOL. *} + example which is verified in Isabelle/HOL.\ -subsection{* Outlining the Example *} +subsection\Outlining the Example\ -text{* We are presenting here an ``analysis-model'' of the (slightly +text\We are presenting here an ``analysis-model'' of the (slightly modified) example Figure 7.3, page 20 of the OCL standard~\cite{omg:ocl:2012}. Here, analysis model means that associations @@ -85,28 +85,28 @@ done in our ``design model'' (see \url{http://isa-afp.org/entries/Featherweight_OCL.shtml}). \endisatagannexa To be precise, this theory contains the formalization of the data-part -covered by the UML class model (see \autoref{fig:person-ana}):*} +covered by the UML class model (see \autoref{fig:person-ana}):\ -text{* +text\ \begin{figure} \centering\scalebox{.3}{\includegraphics{figures/person.png}}% \caption{A simple UML class model drawn from Figure 7.3, page 20 of~\cite{omg:ocl:2012}. \label{fig:person-ana}} \end{figure} -*} +\ -text{* This means that the association (attached to the association class +text\This means that the association (attached to the association class \inlineocl{EmployeeRanking}) with the association ends \inlineocl+boss+ and \inlineocl+employees+ is implemented by the attribute \inlineocl+boss+ and the operation \inlineocl+employees+ (to be discussed in the OCL part captured by the subsequent theory). -*} +\ -section{* Example Data-Universe and its Infrastructure *} -text{* Ideally, the following is generated automatically from a UML class model. *} +section\Example Data-Universe and its Infrastructure\ +text\Ideally, the following is generated automatically from a UML class model.\ -text{* Our data universe consists in the concrete class diagram just of node's, +text\Our data universe consists in the concrete class diagram just of node's, and implicitly of the class object. Each class implies the existence of a class -type defined for the corresponding object representations as follows: *} +type defined for the corresponding object representations as follows:\ datatype type\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n = mk\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n oid (* the oid to the person itself *) "int option" (* the attribute "salary" or null *) @@ -119,15 +119,15 @@ datatype type\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y = mk\<^sub>O\<^sub in case of existence of several subclasses of oclany, sums of extensions have to be provided. *) -text{* Now, we construct a concrete ``universe of OclAny types'' by injection into a +text\Now, we construct a concrete ``universe of OclAny types'' by injection into a sum type containing the class types. This type of OclAny will be used as instance -for all respective type-variables. *} +for all respective type-variables.\ datatype \ = in\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n type\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n | in\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y type\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y -text{* Having fixed the object universe, we can introduce type synonyms that exactly correspond +text\Having fixed the object universe, we can introduce type synonyms that exactly correspond to OCL types. Again, we exploit that our representation of OCL is a ``shallow embedding'' with a -one-to-one correspondance of OCL-types to types of the meta-language HOL. *} +one-to-one correspondance of OCL-types to types of the meta-language HOL.\ type_synonym Boolean = " \ Boolean" type_synonym Integer = " \ Integer" type_synonym Void = " \ Void" @@ -136,12 +136,12 @@ type_synonym Person = "(\, type\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o type_synonym Set_Integer = "(\, int option option) Set" type_synonym Set_Person = "(\, type\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n option option) Set" -text{* Just a little check: *} +text\Just a little check:\ typ "Boolean" -text{* To reuse key-elements of the library like referential equality, we have +text\To reuse key-elements of the library like referential equality, we have to show that the object universe belongs to the type class ``oclany,'' \ie, - each class type has to provide a function @{term oid_of} yielding the object id (oid) of the object. *} + each class type has to provide a function @{term oid_of} yielding the object id (oid) of the object.\ instantiation type\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n :: object begin definition oid_of_type\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n_def: "oid_of x = (case x of mk\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n oid _ \ oid)" @@ -165,9 +165,9 @@ end -section{* Instantiation of the Generic Strict Equality *} -text{* We instantiate the referential equality -on @{text "Person"} and @{text "OclAny"} *} +section\Instantiation of the Generic Strict Equality\ +text\We instantiate the referential equality +on \Person\ and \OclAny\\ overloading StrictRefEq \ "StrictRefEq :: [Person,Person] \ Boolean" begin @@ -195,17 +195,17 @@ lemmas cps23 = [of "x::Person", simplified StrictRefEq\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n[symmetric]] for x y \ P Q -text{* For each Class \emph{C}, we will have a casting operation \inlineocl{.oclAsType($C$)}, +text\For each Class \emph{C}, we will have a casting operation \inlineocl{.oclAsType($C$)}, a test on the actual type \inlineocl{.oclIsTypeOf($C$)} as well as its relaxed form \inlineocl{.oclIsKindOf($C$)} (corresponding exactly to Java's \verb+instanceof+-operator. -*} -text{* Thus, since we have two class-types in our concrete class hierarchy, we have +\ +text\Thus, since we have two class-types in our concrete class hierarchy, we have two operations to declare and to provide two overloading definitions for the two static types. -*} +\ -section{* OclAsType *} -subsection{* Definition *} +section\OclAsType\ +subsection\Definition\ consts OclAsType\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y :: "'\ \ OclAny" ("(_) .oclAsType'(OclAny')") consts OclAsType\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n :: "'\ \ Person" ("(_) .oclAsType'(Person')") @@ -254,12 +254,12 @@ begin "(X::Person) .oclAsType(Person) \ X " (* to avoid identity for null ? *) end -text_raw{* \isatagafp *} +text_raw\\isatagafp\ lemmas [simp] = OclAsType\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y_OclAny OclAsType\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n_Person -subsection{* Context Passing *} +subsection\Context Passing\ lemma cp_OclAsType\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y_Person_Person: "cp P \ cp(\X. (P (X::Person)::Person) .oclAsType(OclAny))" by(rule cpI1, simp_all add: OclAsType\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y_Person) @@ -290,9 +290,9 @@ lemmas [simp] = cp_OclAsType\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n_Person_OclAny cp_OclAsType\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n_OclAny_Person -text_raw{* \endisatagafp*} +text_raw\\endisatagafp\ -subsection{* Execution with Invalid or Null as Argument *} +subsection\Execution with Invalid or Null as Argument\ lemma OclAsType\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y_OclAny_strict : "(invalid::OclAny) .oclAsType(OclAny) = invalid" by(simp) lemma OclAsType\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y_OclAny_nullstrict : "(null::OclAny) .oclAsType(OclAny) = null" by(simp) @@ -307,9 +307,9 @@ lemma OclAsType\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n_OclAny_nullstric lemma OclAsType\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n_Person_strict : "(invalid::Person) .oclAsType(Person) = invalid" by(simp) lemma OclAsType\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n_Person_nullstrict : "(null::Person) .oclAsType(Person) = null" by(simp) -section{* OclIsTypeOf *} +section\OclIsTypeOf\ -subsection{* Definition *} +subsection\Definition\ consts OclIsTypeOf\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y :: "'\ \ Boolean" ("(_).oclIsTypeOf'(OclAny')") consts OclIsTypeOf\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n :: "'\ \ Boolean" ("(_).oclIsTypeOf'(Person')") @@ -375,8 +375,8 @@ begin \ \ invalid \ | _ \ true \)" (* for (* \\ _ \\ \ true \ *) : must have actual type Node otherwise *) end -text_raw{* \isatagafp *} -subsection{* Context Passing *} +text_raw\\isatagafp\ +subsection\Context Passing\ lemma cp_OclIsTypeOf\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y_Person_Person: "cp P \ cp(\X.(P(X::Person)::Person).oclIsTypeOf(OclAny))" by(rule cpI1, simp_all add: OclIsTypeOf\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y_Person) @@ -407,9 +407,9 @@ lemmas [simp] = cp_OclIsTypeOf\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y_OclAny_Person cp_OclIsTypeOf\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n_Person_OclAny cp_OclIsTypeOf\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n_OclAny_Person -text_raw{* \endisatagafp *} +text_raw\\endisatagafp\ -subsection{* Execution with Invalid or Null as Argument *} +subsection\Execution with Invalid or Null as Argument\ lemma OclIsTypeOf\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y_OclAny_strict1[simp]: "(invalid::OclAny) .oclIsTypeOf(OclAny) = invalid" @@ -444,7 +444,7 @@ lemma OclIsTypeOf\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n_Person_strict2 by(rule ext, simp add: null_fun_def null_option_def bot_option_def null_def invalid_def OclIsTypeOf\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n_Person) -subsection{* Up Down Casting *} +subsection\Up Down Casting\ lemma actualType_larger_staticType: assumes isdef: "\ \ (\ X)" @@ -503,8 +503,8 @@ shows "\ \ (X .oclIsTypeOf(Person) implies (X .oclAsType(OclAn by simp -section{* OclIsKindOf *} -subsection{* Definition *} +section\OclIsKindOf\ +subsection\Definition\ consts OclIsKindOf\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y :: "'\ \ Boolean" ("(_).oclIsKindOf'(OclAny')") consts OclIsKindOf\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n :: "'\ \ Boolean" ("(_).oclIsKindOf'(Person')") @@ -547,8 +547,8 @@ begin \ \ invalid \ | _ \ true \)" end -text_raw{* \isatagafp *} -subsection{* Context Passing *} +text_raw\\isatagafp\ +subsection\Context Passing\ lemma cp_OclIsKindOf\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y_Person_Person: "cp P \ cp(\X.(P(X::Person)::Person).oclIsKindOf(OclAny))" by(rule cpI1, simp_all add: OclIsKindOf\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y_Person) @@ -578,8 +578,8 @@ lemmas [simp] = cp_OclIsKindOf\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y_OclAny_Person cp_OclIsKindOf\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n_Person_OclAny cp_OclIsKindOf\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n_OclAny_Person -text_raw{* \endisatagafp *} -subsection{* Execution with Invalid or Null as Argument *} +text_raw\\endisatagafp\ +subsection\Execution with Invalid or Null as Argument\ lemma OclIsKindOf\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y_OclAny_strict1[simp] : "(invalid::OclAny) .oclIsKindOf(OclAny) = invalid" by(rule ext, simp add: invalid_def bot_option_def @@ -606,7 +606,7 @@ lemma OclIsKindOf\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n_Person_strict2 by(rule ext, simp add: null_fun_def null_option_def bot_option_def null_def invalid_def OclIsKindOf\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n_Person) -subsection{* Up Down Casting *} +subsection\Up Down Casting\ lemma actualKind_larger_staticKind: assumes isdef: "\ \ (\ X)" @@ -625,11 +625,11 @@ apply(auto simp : bot_fun_def null_fun_def null_option_def bot_option_def null_d split: option.split type\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y.split type\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n.split) by(simp add: OclIsKindOf\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n_OclAny OclValid_def false_def true_def) -section{* OclAllInstances *} +section\OclAllInstances\ -text{* To denote OCL-types occurring in OCL expressions syntactically---as, for example, as +text\To denote OCL-types occurring in OCL expressions syntactically---as, for example, as ``argument'' of \inlineisar{oclAllInstances()}---we use the inverses of the injection -functions into the object universes; we show that this is sufficient ``characterization.'' *} +functions into the object universes; we show that this is sufficient ``characterization.''\ definition "Person \ OclAsType\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n_\" definition "OclAny \ OclAsType\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y_\" @@ -656,7 +656,7 @@ lemma OclAllInstances_at_pre\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y_exe unfolding OclAllInstances_at_pre_def by(rule OclAllInstances_generic\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y_exec) -subsection{* OclIsTypeOf *} +subsection\OclIsTypeOf\ lemma OclAny_allInstances_generic_oclIsTypeOf\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y1: assumes [simp]: "\x. pre_post (x, x) = x" @@ -720,7 +720,7 @@ lemma Person_allInstances_at_pre_oclIsTypeOf\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^s unfolding OclAllInstances_at_pre_def by(rule Person_allInstances_generic_oclIsTypeOf\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n) -subsection{* OclIsKindOf *} +subsection\OclIsKindOf\ lemma OclAny_allInstances_generic_oclIsKindOf\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y: "\ \ ((OclAllInstances_generic pre_post OclAny)->forAll\<^sub>S\<^sub>e\<^sub>t(X|X .oclIsKindOf(OclAny)))" apply(simp add: OclValid_def del: OclAllInstances_generic_def) @@ -778,23 +778,23 @@ lemma Person_allInstances_at_pre_oclIsKindOf\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^s unfolding OclAllInstances_at_pre_def by(rule Person_allInstances_generic_oclIsKindOf\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n) -section{* The Accessors (any, boss, salary) *} -text{*\label{sec:eam-accessors}*} -text{* Should be generated entirely from a class-diagram. *} +section\The Accessors (any, boss, salary)\ +text\\label{sec:eam-accessors}\ +text\Should be generated entirely from a class-diagram.\ -subsection{* Definition (of the association Employee-Boss) *} +subsection\Definition (of the association Employee-Boss)\ -text{* We start with a oid for the association; this oid can be used +text\We start with a oid for the association; this oid can be used in presence of association classes to represent the association inside an object, pretty much similar to the \inlineisar+Design_UML+, where we stored -an \verb+oid+ inside the class as ``pointer.'' *} +an \verb+oid+ inside the class as ``pointer.''\ definition oid\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n\\\\ ::"oid" where "oid\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n\\\\ = 10" -text{* From there on, we can already define an empty state which must contain +text\From there on, we can already define an empty state which must contain for $\mathit{oid}_{Person}\mathcal{BOSS}$ the empty relation (encoded as association list, since there are -associations with a Sequence-like structure).*} +associations with a Sequence-like structure).\ definition eval_extract :: "('\,('a::object) option option) val @@ -823,9 +823,9 @@ where "deref_assocs\<^sub>2 pre_post to_from assoc_oid f oid = | _ \ invalid \)" -text{* The @{text pre_post}-parameter is configured with @{text fst} or -@{text snd}, the @{text to_from}-parameter either with the identity @{term id} or -the following combinator @{text switch}: *} +text\The \pre_post\-parameter is configured with \fst\ or +\snd\, the \to_from\-parameter either with the identity @{term id} or +the following combinator \switch\:\ definition "switch\<^sub>2_1 = (\[x,y]\ (x,y))" definition "switch\<^sub>2_2 = (\[x,y]\ (y,x))" definition "switch\<^sub>3_1 = (\[x,y,z]\ (x,y))" @@ -853,7 +853,7 @@ where "deref_oid\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y fst_snd f oid = \ in\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y obj \ \ f obj \ | _ \ invalid \)" -text{* pointer undefined in state or not referencing a type conform object representation *} +text\pointer undefined in state or not referencing a type conform object representation\ definition "select\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y\\\ f = (\ X. case X of @@ -923,7 +923,7 @@ lemmas dot_accessor = dot\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n\\\\_at_pre_def dot\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n\\\\\\_at_pre_def -subsection{* Context Passing *} +subsection\Context Passing\ lemmas [simp] = eval_extract_def @@ -956,7 +956,7 @@ lemmas cp_dot\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n\\\\\P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n\\\\\\_at_pre[THEN allI[THEN allI], of "\ X _. X" "\ _ \. \", THEN cpI1] -subsection{* Execution with Invalid or Null as Argument *} +subsection\Execution with Invalid or Null as Argument\ lemma dot\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y\\\_nullstrict [simp]: "(null).any = invalid" by(rule ext, simp add: dot_accessor null_fun_def null_option_def bot_option_def null_def invalid_def) @@ -987,7 +987,7 @@ by(rule ext, simp add: dot_accessor null_fun_def null_option_def bot_option_def lemma dot\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n\\\\\\_at_pre_strict [simp] : "(invalid).salary@pre = invalid" by(rule ext, simp add: dot_accessor null_fun_def null_option_def bot_option_def null_def invalid_def) -subsection{* Representation in States *} +subsection\Representation in States\ lemma dot\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n\\\\_def_mono:"\ \ \(X .boss) \ \ \ \(X)" apply(case_tac "\ \ (X \ invalid)", insert StrongEq_L_subst2[where P = "(\x. (\ (x .boss)))" and \ = "\" and x = "X" and y = "invalid"], simp add: foundation16') @@ -1008,9 +1008,9 @@ assumes A: "\ \ \(x .boss)" shows "\ \ ((Person .allInstances()) ->includes\<^sub>S\<^sub>e\<^sub>t(x .boss))" oops -section{* A Little Infra-structure on Example States *} +section\A Little Infra-structure on Example States\ -text{* +text\ The example we are defining in this section comes from the figure~\ref{fig:eam1_system-states}. \begin{figure} \includegraphics[width=\textwidth]{figures/pre-post.pdf} @@ -1018,9 +1018,9 @@ The example we are defining in this section comes from the figure~\ref{fig:eam1_ (b) post-state $\sigma_1'$.} \label{fig:eam1_system-states} \end{figure} -*} +\ -text_raw{* \isatagafp*} +text_raw\\isatagafp\ definition OclInt1000 ("\\\\") where "OclInt1000 = (\ _ . \\1000\\)" definition OclInt1200 ("\\\\") where "OclInt1200 = (\ _ . \\1200\\)" @@ -1051,7 +1051,7 @@ definition "person7 \ mk\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y definition "person8 \ mk\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y oid7 None" definition "person9 \ mk\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n oid8 \0\" -text_raw{* \endisatagafp*} +text_raw\\endisatagafp\ definition "\\<^sub>1 \ \ heap = Map.empty(oid0 \ in\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n (mk\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n oid0 \1000\)) @@ -1093,7 +1093,7 @@ by(auto simp: \\<^sub>1_def) lemma [simp,code_unfold]: "dom (heap \\<^sub>1') = {oid0,oid1,oid2,oid3\<^cancel>\,oid4\,oid5,oid6,oid7,oid8}" by(auto simp: \\<^sub>1'_def) -text_raw{* \isatagafp *} +text_raw\\isatagafp\ definition "X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n1 :: Person \ \ _ .\\ person1 \\" definition "X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n2 :: Person \ \ _ .\\ person2 \\" @@ -1123,7 +1123,7 @@ lemmas [simp,code_unfold] = OclIsKindOf\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y_Person OclIsKindOf\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n_OclAny OclIsKindOf\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n_Person -text_raw{* \endisatagafp *} +text_raw\\endisatagafp\ Assert "\s\<^sub>p\<^sub>r\<^sub>e . (s\<^sub>p\<^sub>r\<^sub>e,\\<^sub>1') \ (X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n1 .salary <> \\\\)" Assert "\s\<^sub>p\<^sub>r\<^sub>e . (s\<^sub>p\<^sub>r\<^sub>e,\\<^sub>1') \ (X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n1 .salary \ \\\\)" diff --git a/Featherweight_OCL/examples/Employee_Model/Design/Design_OCL.thy b/Featherweight_OCL/examples/Employee_Model/Design/Design_OCL.thy index e80d0c2..565e7b7 100644 --- a/Featherweight_OCL/examples/Employee_Model/Design/Design_OCL.thy +++ b/Featherweight_OCL/examples/Employee_Model/Design/Design_OCL.thy @@ -45,10 +45,10 @@ theory imports Design_UML begin -text {* \label{ex:employee-design:ocl} *} +text \\label{ex:employee-design:ocl}\ -section{* OCL Part: Invariant *} -text{* These recursive predicates can be defined conservatively +section\OCL Part: Invariant\ +text\These recursive predicates can be defined conservatively by greatest fix-point constructions---automatically. See~\cite{brucker.ea:hol-ocl-book:2006,brucker:interactive:2007} for details. For the purpose of this example, we state them as axioms @@ -58,7 +58,7 @@ here. context Person inv label : self .boss <> null implies (self .salary \ ((self .boss) .salary)) \end{ocl} -*} +\ definition Person_label\<^sub>i\<^sub>n\<^sub>v :: "Person \ Boolean" where "Person_label\<^sub>i\<^sub>n\<^sub>v (self) \ @@ -87,7 +87,7 @@ lemma REC_pre : "\ \ Person_label\<^sub>g\<^sub>l\<^sub>o\<^sub> oops (* Attempt to allegiate the burden of he following axiomatizations: could be a witness for a constant specification ...*) -text{* This allows to state a predicate: *} +text\This allows to state a predicate:\ axiomatization inv\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n\<^sub>_\<^sub>l\<^sub>a\<^sub>b\<^sub>e\<^sub>l :: "Person \ Boolean" where inv\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n\<^sub>_\<^sub>l\<^sub>a\<^sub>b\<^sub>e\<^sub>l_def: @@ -121,8 +121,8 @@ lemma inv_2 : (\ \ (inv\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n\<^sub>_\<^sub>l\<^sub>a\<^sub>b\<^sub>e\<^sub>l\<^sub>A\<^sub>T\<^sub>p\<^sub>r\<^sub>e(self .boss@pre)))))" oops (* Let's hope that this holds ... *) -text{* A very first attempt to characterize the axiomatization by an inductive -definition - this can not be the last word since too weak (should be equality!) *} +text\A very first attempt to characterize the axiomatization by an inductive +definition - this can not be the last word since too weak (should be equality!)\ coinductive inv :: "Person \ (\)st \ bool" where "(\ \ (\ self)) \ ((\ \ (self .boss \ null)) \ (\ \ (self .boss <> null) \ (\ \ (self .boss .salary \\<^sub>i\<^sub>n\<^sub>t self .salary)) \ @@ -130,8 +130,8 @@ coinductive inv :: "Person \ (\)st \ bool" where \ ( inv self \)" -section{* OCL Part: The Contract of a Recursive Query *} -text{* This part is analogous to the Analysis Model and skipped here. *} +section\OCL Part: The Contract of a Recursive Query\ +text\This part is analogous to the Analysis Model and skipped here.\ end diff --git a/Featherweight_OCL/examples/Employee_Model/Design/Design_UML.thy b/Featherweight_OCL/examples/Employee_Model/Design/Design_UML.thy index 139418b..425e4da 100644 --- a/Featherweight_OCL/examples/Employee_Model/Design/Design_UML.thy +++ b/Featherweight_OCL/examples/Employee_Model/Design/Design_UML.thy @@ -40,7 +40,7 @@ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. ******************************************************************************) -chapter{* Example: The Employee Design Model *} (* UML part *) +chapter\Example: The Employee Design Model\ (* UML part *) theory Design_UML @@ -48,10 +48,10 @@ imports "../../../UML_Main" begin -text {* \label{ex:employee-design:uml} *} +text \\label{ex:employee-design:uml}\ -section{* Introduction *} -text{* +section\Introduction\ +text\ For certain concepts like classes and class-types, only a generic definition for its resulting semantics can be given. Generic means, there is a function outside HOL that ``compiles'' a concrete, @@ -59,43 +59,43 @@ text{* consisting of a bunch of definitions for classes, accessors, method, casts, and tests for actual types, as well as proofs for the fundamental properties of these operations in this concrete data - model. *} + model.\ -text{* Such generic function or ``compiler'' can be implemented in +text\Such generic function or ``compiler'' can be implemented in Isabelle on the ML level. This has been done, for a semantics following the open-world assumption, for UML 2.0 in~\cite{brucker.ea:extensible:2008-b, brucker:interactive:2007}. In this paper, we follow another approach for UML 2.4: we define the concepts of the compilation informally, and present a concrete - example which is verified in Isabelle/HOL. *} + example which is verified in Isabelle/HOL.\ -subsection{* Outlining the Example *} +subsection\Outlining the Example\ -text{* We are presenting here a ``design-model'' of the (slightly +text\We are presenting here a ``design-model'' of the (slightly modified) example Figure 7.3, page 20 of the OCL standard~\cite{omg:ocl:2012}. To be precise, this theory contains the formalization of -the data-part covered by the UML class model (see \autoref{fig:person}):*} +the data-part covered by the UML class model (see \autoref{fig:person}):\ -text{* +text\ \begin{figure} \centering\scalebox{.3}{\includegraphics{figures/person.png}}% \caption{A simple UML class model drawn from Figure 7.3, page 20 of~\cite{omg:ocl:2012}. \label{fig:person}} \end{figure} -*} +\ -text{* This means that the association (attached to the association class +text\This means that the association (attached to the association class \inlineocl{EmployeeRanking}) with the association ends \inlineocl+boss+ and \inlineocl+employees+ is implemented by the attribute \inlineocl+boss+ and the operation \inlineocl+employees+ (to be discussed in the OCL part captured by the subsequent theory). -*} +\ -section{* Example Data-Universe and its Infrastructure *} -text{* Ideally, the following is generated automatically from a UML class model. *} +section\Example Data-Universe and its Infrastructure\ +text\Ideally, the following is generated automatically from a UML class model.\ -text{* Our data universe consists in the concrete class diagram just of node's, +text\Our data universe consists in the concrete class diagram just of node's, and implicitly of the class object. Each class implies the existence of a class -type defined for the corresponding object representations as follows: *} +type defined for the corresponding object representations as follows:\ datatype type\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n = mk\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n oid (* the oid to the person itself *) "int option" (* the attribute "salary" or null *) @@ -109,15 +109,15 @@ datatype type\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y = mk\<^sub>O\<^sub in case of existence of several subclasses of oclany, sums of extensions have to be provided. *) -text{* Now, we construct a concrete ``universe of OclAny types'' by injection into a +text\Now, we construct a concrete ``universe of OclAny types'' by injection into a sum type containing the class types. This type of OclAny will be used as instance -for all respective type-variables. *} +for all respective type-variables.\ datatype \ = in\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n type\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n | in\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y type\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y -text{* Having fixed the object universe, we can introduce type synonyms that exactly correspond +text\Having fixed the object universe, we can introduce type synonyms that exactly correspond to OCL types. Again, we exploit that our representation of OCL is a ``shallow embedding'' with a -one-to-one correspondance of OCL-types to types of the meta-language HOL. *} +one-to-one correspondance of OCL-types to types of the meta-language HOL.\ type_synonym Boolean = " \ Boolean" type_synonym Integer = " \ Integer" type_synonym Void = " \ Void" @@ -126,12 +126,12 @@ type_synonym Person = "(\, type\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o type_synonym Set_Integer = "(\, int option option) Set" type_synonym Set_Person = "(\, type\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n option option) Set" -text{* Just a little check: *} +text\Just a little check:\ typ "Boolean" -text{* To reuse key-elements of the library like referential equality, we have +text\To reuse key-elements of the library like referential equality, we have to show that the object universe belongs to the type class ``oclany,'' \ie, - each class type has to provide a function @{term oid_of} yielding the object id (oid) of the object. *} + each class type has to provide a function @{term oid_of} yielding the object id (oid) of the object.\ instantiation type\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n :: object begin definition oid_of_type\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n_def: "oid_of x = (case x of mk\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n oid _ _ \ oid)" @@ -155,9 +155,9 @@ end -section{* Instantiation of the Generic Strict Equality *} -text{* We instantiate the referential equality -on @{text "Person"} and @{text "OclAny"} *} +section\Instantiation of the Generic Strict Equality\ +text\We instantiate the referential equality +on \Person\ and \OclAny\\ overloading StrictRefEq \ "StrictRefEq :: [Person,Person] \ Boolean" begin @@ -185,17 +185,17 @@ lemmas cps23 = [of "x::Person", simplified StrictRefEq\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n[symmetric]] for x y \ P Q -text{* For each Class \emph{C}, we will have a casting operation \inlineocl{.oclAsType($C$)}, +text\For each Class \emph{C}, we will have a casting operation \inlineocl{.oclAsType($C$)}, a test on the actual type \inlineocl{.oclIsTypeOf($C$)} as well as its relaxed form \inlineocl{.oclIsKindOf($C$)} (corresponding exactly to Java's \verb+instanceof+-operator. -*} -text{* Thus, since we have two class-types in our concrete class hierarchy, we have +\ +text\Thus, since we have two class-types in our concrete class hierarchy, we have two operations to declare and to provide two overloading definitions for the two static types. -*} +\ -section{* OclAsType *} -subsection{* Definition *} +section\OclAsType\ +subsection\Definition\ consts OclAsType\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y :: "'\ \ OclAny" ("(_) .oclAsType'(OclAny')") consts OclAsType\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n :: "'\ \ Person" ("(_) .oclAsType'(Person')") @@ -243,12 +243,12 @@ begin definition OclAsType\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n_Person: "(X::Person) .oclAsType(Person) \ X " (* to avoid identity for null ? *) end -text_raw{* \isatagafp *} +text_raw\\isatagafp\ lemmas [simp] = OclAsType\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y_OclAny OclAsType\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n_Person -subsection{* Context Passing *} +subsection\Context Passing\ lemma cp_OclAsType\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y_Person_Person: "cp P \ cp(\X. (P (X::Person)::Person) .oclAsType(OclAny))" by(rule cpI1, simp_all add: OclAsType\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y_Person) @@ -279,9 +279,9 @@ lemmas [simp] = cp_OclAsType\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n_Person_OclAny cp_OclAsType\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n_OclAny_Person -text_raw{* \endisatagafp*} +text_raw\\endisatagafp\ -subsection{* Execution with Invalid or Null as Argument *} +subsection\Execution with Invalid or Null as Argument\ lemma OclAsType\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y_OclAny_strict : "(invalid::OclAny) .oclAsType(OclAny) = invalid" by(simp) lemma OclAsType\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y_OclAny_nullstrict : "(null::OclAny) .oclAsType(OclAny) = null" by(simp) @@ -296,9 +296,9 @@ lemma OclAsType\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n_OclAny_nullstric lemma OclAsType\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n_Person_strict : "(invalid::Person) .oclAsType(Person) = invalid" by(simp) lemma OclAsType\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n_Person_nullstrict : "(null::Person) .oclAsType(Person) = null" by(simp) -section{* OclIsTypeOf *} +section\OclIsTypeOf\ -subsection{* Definition *} +subsection\Definition\ consts OclIsTypeOf\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y :: "'\ \ Boolean" ("(_).oclIsTypeOf'(OclAny')") consts OclIsTypeOf\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n :: "'\ \ Boolean" ("(_).oclIsTypeOf'(Person')") @@ -364,8 +364,8 @@ begin \ \ invalid \ | _ \ true \)" (* for (* \\ _ \\ \ true \ *) : must have actual type Node otherwise *) end -text_raw{* \isatagafp *} -subsection{* Context Passing *} +text_raw\\isatagafp\ +subsection\Context Passing\ lemma cp_OclIsTypeOf\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y_Person_Person: "cp P \ cp(\X.(P(X::Person)::Person).oclIsTypeOf(OclAny))" by(rule cpI1, simp_all add: OclIsTypeOf\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y_Person) @@ -396,9 +396,9 @@ lemmas [simp] = cp_OclIsTypeOf\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y_OclAny_Person cp_OclIsTypeOf\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n_Person_OclAny cp_OclIsTypeOf\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n_OclAny_Person -text_raw{* \endisatagafp *} +text_raw\\endisatagafp\ -subsection{* Execution with Invalid or Null as Argument *} +subsection\Execution with Invalid or Null as Argument\ lemma OclIsTypeOf\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y_OclAny_strict1[simp]: "(invalid::OclAny) .oclIsTypeOf(OclAny) = invalid" @@ -433,7 +433,7 @@ lemma OclIsTypeOf\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n_Person_strict2 by(rule ext, simp add: null_fun_def null_option_def bot_option_def null_def invalid_def OclIsTypeOf\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n_Person) -subsection{* Up Down Casting *} +subsection\Up Down Casting\ lemma actualType_larger_staticType: assumes isdef: "\ \ (\ X)" @@ -492,8 +492,8 @@ shows "\ \ (X .oclIsTypeOf(Person) implies (X .oclAsType(OclAn by simp -section{* OclIsKindOf *} -subsection{* Definition *} +section\OclIsKindOf\ +subsection\Definition\ consts OclIsKindOf\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y :: "'\ \ Boolean" ("(_).oclIsKindOf'(OclAny')") consts OclIsKindOf\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n :: "'\ \ Boolean" ("(_).oclIsKindOf'(Person')") @@ -536,8 +536,8 @@ begin \ \ invalid \ | _ \ true \)" end -text_raw{* \isatagafp *} -subsection{* Context Passing *} +text_raw\\isatagafp\ +subsection\Context Passing\ lemma cp_OclIsKindOf\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y_Person_Person: "cp P \ cp(\X.(P(X::Person)::Person).oclIsKindOf(OclAny))" by(rule cpI1, simp_all add: OclIsKindOf\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y_Person) @@ -567,8 +567,8 @@ lemmas [simp] = cp_OclIsKindOf\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y_OclAny_Person cp_OclIsKindOf\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n_Person_OclAny cp_OclIsKindOf\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n_OclAny_Person -text_raw{* \endisatagafp *} -subsection{* Execution with Invalid or Null as Argument *} +text_raw\\endisatagafp\ +subsection\Execution with Invalid or Null as Argument\ lemma OclIsKindOf\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y_OclAny_strict1[simp] : "(invalid::OclAny) .oclIsKindOf(OclAny) = invalid" by(rule ext, simp add: invalid_def bot_option_def @@ -595,7 +595,7 @@ lemma OclIsKindOf\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n_Person_strict2 by(rule ext, simp add: null_fun_def null_option_def bot_option_def null_def invalid_def OclIsKindOf\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n_Person) -subsection{* Up Down Casting *} +subsection\Up Down Casting\ lemma actualKind_larger_staticKind: assumes isdef: "\ \ (\ X)" @@ -614,11 +614,11 @@ apply(auto simp : bot_fun_def null_fun_def null_option_def bot_option_def null_d split: option.split type\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y.split type\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n.split) by(simp add: OclIsKindOf\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n_OclAny OclValid_def false_def true_def) -section{* OclAllInstances *} +section\OclAllInstances\ -text{* To denote OCL-types occurring in OCL expressions syntactically---as, for example, as +text\To denote OCL-types occurring in OCL expressions syntactically---as, for example, as ``argument'' of \inlineisar{oclAllInstances()}---we use the inverses of the injection -functions into the object universes; we show that this is sufficient ``characterization.'' *} +functions into the object universes; we show that this is sufficient ``characterization.''\ definition "Person \ OclAsType\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n_\" definition "OclAny \ OclAsType\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y_\" @@ -645,7 +645,7 @@ lemma OclAllInstances_at_pre\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y_exe unfolding OclAllInstances_at_pre_def by(rule OclAllInstances_generic\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y_exec) -subsection{* OclIsTypeOf *} +subsection\OclIsTypeOf\ lemma OclAny_allInstances_generic_oclIsTypeOf\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y1: assumes [simp]: "\x. pre_post (x, x) = x" @@ -709,7 +709,7 @@ lemma Person_allInstances_at_pre_oclIsTypeOf\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^s unfolding OclAllInstances_at_pre_def by(rule Person_allInstances_generic_oclIsTypeOf\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n) -subsection{* OclIsKindOf *} +subsection\OclIsKindOf\ lemma OclAny_allInstances_generic_oclIsKindOf\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y: "\ \ ((OclAllInstances_generic pre_post OclAny)->forAll\<^sub>S\<^sub>e\<^sub>t(X|X .oclIsKindOf(OclAny)))" apply(simp add: OclValid_def del: OclAllInstances_generic_def) @@ -767,12 +767,12 @@ lemma Person_allInstances_at_pre_oclIsKindOf\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^s unfolding OclAllInstances_at_pre_def by(rule Person_allInstances_generic_oclIsKindOf\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n) -section{* The Accessors (any, boss, salary) *} -text{*\label{sec:edm-accessors}*} -text{* Should be generated entirely from a class-diagram. *} +section\The Accessors (any, boss, salary)\ +text\\label{sec:edm-accessors}\ +text\Should be generated entirely from a class-diagram.\ -subsection{* Definition *} +subsection\Definition\ definition eval_extract :: "('\,('a::object) option option) val \ (oid \ ('\,'c::null) val) @@ -801,7 +801,7 @@ where "deref_oid\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y fst_snd f oid = \ in\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y obj \ \ f obj \ | _ \ invalid \)" -text{* pointer undefined in state or not referencing a type conform object representation *} +text\pointer undefined in state or not referencing a type conform object representation\ definition "select\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y\\\ f = (\ X. case X of @@ -868,7 +868,7 @@ lemmas dot_accessor = dot\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n\\\\_at_pre_def dot\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n\\\\\\_at_pre_def -subsection{* Context Passing *} +subsection\Context Passing\ lemmas [simp] = eval_extract_def @@ -901,7 +901,7 @@ lemmas cp_dot\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n\\\\\P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n\\\\\\_at_pre[THEN allI[THEN allI], of "\ X _. X" "\ _ \. \", THEN cpI1] -subsection{* Execution with Invalid or Null as Argument *} +subsection\Execution with Invalid or Null as Argument\ lemma dot\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y\\\_nullstrict [simp]: "(null).any = invalid" by(rule ext, simp add: dot_accessor null_fun_def null_option_def bot_option_def null_def invalid_def) @@ -932,7 +932,7 @@ by(rule ext, simp add: dot_accessor null_fun_def null_option_def bot_option_def lemma dot\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n\\\\\\_at_pre_strict [simp] : "(invalid).salary@pre = invalid" by(rule ext, simp add: dot_accessor null_fun_def null_option_def bot_option_def null_def invalid_def) -subsection{* Representation in States *} +subsection\Representation in States\ lemma dot\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n\\\\_def_mono:"\ \ \(X .boss) \ \ \ \(X)" apply(case_tac "\ \ (X \ invalid)", insert StrongEq_L_subst2[where P = "(\x. (\ (x .boss)))" and \ = "\" and x = "X" and y = "invalid"], simp add: foundation16') @@ -968,9 +968,9 @@ proof - by(simp add: image_comp B true_def) qed -section{* A Little Infra-structure on Example States *} +section\A Little Infra-structure on Example States\ -text{* +text\ The example we are defining in this section comes from the figure~\ref{fig:edm1_system-states}. \begin{figure} \includegraphics[width=\textwidth]{figures/pre-post.pdf} @@ -978,9 +978,9 @@ The example we are defining in this section comes from the figure~\ref{fig:edm1_ (b) post-state $\sigma_1'$.} \label{fig:edm1_system-states} \end{figure} -*} +\ -text_raw{* \isatagafp*} +text_raw\\isatagafp\ definition OclInt1000 ("\\\\") where "OclInt1000 = (\ _ . \\1000\\)" definition OclInt1200 ("\\\\") where "OclInt1200 = (\ _ . \\1200\\)" @@ -1051,7 +1051,7 @@ by(auto simp: \\<^sub>1_def) lemma [simp,code_unfold]: "dom (heap \\<^sub>1') = {oid0,oid1,oid2,oid3\<^cancel>\,oid4\,oid5,oid6,oid7,oid8}" by(auto simp: \\<^sub>1'_def) -text_raw{* \isatagafp *} +text_raw\\isatagafp\ definition "X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n1 :: Person \ \ _ .\\ person1 \\" definition "X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n2 :: Person \ \ _ .\\ person2 \\" @@ -1081,7 +1081,7 @@ lemmas [simp,code_unfold] = OclIsKindOf\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y_Person OclIsKindOf\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n_OclAny OclIsKindOf\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n_Person -text_raw{* \endisatagafp *} +text_raw\\endisatagafp\ Assert "\s\<^sub>p\<^sub>r\<^sub>e . (s\<^sub>p\<^sub>r\<^sub>e,\\<^sub>1') \ (X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n1 .salary <> \\\\)" Assert "\s\<^sub>p\<^sub>r\<^sub>e . (s\<^sub>p\<^sub>r\<^sub>e,\\<^sub>1') \ (X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n1 .salary \ \\\\)"