From ed232e8aa36bd9257d5f03a5c979d037c1db1a75 Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Wed, 10 Aug 2016 11:10:49 +0100 Subject: [PATCH] Import of Featherweight OCL release afp-Featherweight_OCL-2015-05-27 (Isabelle 2015). --- OCL_core.thy | 2 +- OCL_lib.thy | 17 +++---- OCL_state.thy | 2 +- document/formalization.tex | 9 ---- document/root.tex | 7 --- examples/Employee_AnalysisModel_OCLPart.thy | 10 ++-- examples/Employee_AnalysisModel_UMLPart.thy | 54 ++++++++++----------- examples/Employee_DesignModel_OCLPart.thy | 10 ++-- examples/Employee_DesignModel_UMLPart.thy | 54 ++++++++++----------- 9 files changed, 74 insertions(+), 91 deletions(-) diff --git a/OCL_core.thy b/OCL_core.thy index 916e0f1..a108385 100644 --- a/OCL_core.thy +++ b/OCL_core.thy @@ -40,7 +40,7 @@ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. ******************************************************************************) -header{* Formalization I: Core Definitions *} +chapter{* Formalization I: Core Definitions *} theory OCL_core diff --git a/OCL_lib.thy b/OCL_lib.thy index 7089f2c..d41664c 100644 --- a/OCL_lib.thy +++ b/OCL_lib.thy @@ -40,7 +40,7 @@ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. ******************************************************************************) -header{* Formalization II: Library Definitions *} +chapter{* Formalization II: Library Definitions *} theory OCL_lib imports OCL_core @@ -1783,7 +1783,6 @@ proof - done qed -(*declare [[names_long,show_types,show_sorts]]*) lemma OclIncludes_charn1: assumes def_X:"\ \ (\ X)" assumes val_x:"\ \ (\ x)" @@ -2185,7 +2184,7 @@ proof - (* false *) (* false YES *) apply(case_tac "\x\\\Rep_Set_0 (S->including(x) \)\\. P (\_. x) \ = false \", simp_all) - apply(subst contradict_Rep_Set_0[where f = "\ x \. P x \ = false \"], simp)+ + apply(subst contradict_Rep_Set_0[where f1 = "\ x \. P x \ = false \"], simp)+ apply(simp add: exists_including_invert[where f = "\ x \. P x \ = false \", OF cp_eq]) apply(simp add: cp_OclAnd[of "P x"]) @@ -2203,7 +2202,7 @@ proof - (* bot *) (* bot YES *) apply(case_tac "\x\\\Rep_Set_0 (S->including(x) \)\\. P (\_. x) \ = bot \", simp_all) - apply(subst contradict_Rep_Set_0[where f = "\ x \. P x \ = bot \"], simp)+ + apply(subst contradict_Rep_Set_0[where f1 = "\ x \. P x \ = bot \"], simp)+ apply(simp add: exists_including_invert[where f = "\ x \. P x \ = bot \", OF cp_eq]) apply(simp add: cp_OclAnd[of "P x"]) @@ -2226,7 +2225,7 @@ proof - (* null *) (* null YES *) apply(case_tac "\x\\\Rep_Set_0 (S->including(x) \)\\. P (\_. x) \ = null \", simp_all) - apply(subst contradict_Rep_Set_0[where f = "\ x \. P x \ = null \"], simp)+ + apply(subst contradict_Rep_Set_0[where f1 = "\ x \. P x \ = null \"], simp)+ apply(simp add: exists_including_invert[where f = "\ x \. P x \ = null \", OF cp_eq]) apply(simp add: cp_OclAnd[of "P x"]) @@ -2455,7 +2454,7 @@ proof - have OclSelect_body_bot: "\\. \ \ \ X \ \ \ \ y \ P y \ \ \ \ (\x\\\Rep_Set_0 (X \)\\. P (\_. x) \ = \) \ \ = ?select \" - apply(drule ex_excluding1[where X = X and y = y and f = "\x \. x \ = \"], + apply(drule ex_excluding1[where X2 = X and y2 = y and f2 = "\x \. x \ = \"], (simp add: P_cp[symmetric])+) apply(subgoal_tac "\ \ (\ \ ?select)", simp add: OclValid_def StrongEq_def true_def bot_fun_def) apply(simp add: OclSelect_body_def) @@ -2464,7 +2463,7 @@ proof - apply(subgoal_tac "\x\\\Rep_Set_0 (X->excluding(y) \)\\. P (\_. x) \ = \ \") prefer 2 apply (metis OCL_core.bot_fun_def foundation18') - apply(subst if_same[where d = "\"]) + apply(subst if_same[where d5 = "\"]) apply (metis defined7 transform1) apply(simp add: OclSelect_def bot_option_def bot_fun_def) apply(subst invert_including) @@ -2522,7 +2521,7 @@ proof - apply(simp) (* *) apply(subst conj_comm, rule conjI) - apply(drule_tac y = false in bool_invalid) + apply(drule_tac y11 = false in bool_invalid) apply(simp only: OclSelect_body_def, metis OclIf_def OclValid_def defined_def foundation2 foundation22 bot_fun_def invalid_def) @@ -2917,7 +2916,7 @@ proof - proof - fix x F show "(\ S) \ = true \ \ \x. x \ F \ ?forall (\b \. ?P_eq x b \ \ ?P F b \) = ((\_. ?forall (?P F)) and (\_. P (\\. x) \)) \" - apply(rule disjE4[OF destruct_ocl[where x = "P (\\. x) \"]]) + apply(rule disjE4[OF destruct_ocl[where x1 = "P (\\. x) \"]]) apply(simp_all add: true_def false_def OclAnd_def null_fun_def null_option_def bot_fun_def bot_option_def) by (metis (lifting) option.distinct(1))+ diff --git a/OCL_state.thy b/OCL_state.thy index e69d8ec..e5f184c 100644 --- a/OCL_state.thy +++ b/OCL_state.thy @@ -40,7 +40,7 @@ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. ******************************************************************************) -header{* Formalization III: State Operations and Objects *} +chapter{* Formalization III: State Operations and Objects *} theory OCL_state imports OCL_lib diff --git a/document/formalization.tex b/document/formalization.tex index 2dde8b8..1f9f024 100644 --- a/document/formalization.tex +++ b/document/formalization.tex @@ -1,8 +1,6 @@ \part{A Proposal for Formal Semantics of OCL 2.5} - -% \input{session} \input{OCL_core.tex} \input{OCL_lib.tex} \input{OCL_state.tex} @@ -10,13 +8,6 @@ \input{OCL_main.tex} -\renewcommand{\isamarkupheader}[1]{\section{#1}} -\renewcommand{\isamarkupsection}[1]{\subsection{#1}} -\renewcommand{\isamarkupsubsection}[1]{\subsubsection{#1}} -\renewcommand{\isamarkupsubsubsection}[1]{\paragraph{#1}} -\renewcommand{\isamarkupsect}[1]{\subsection{#1}} -\renewcommand{\isamarkupsubsect}[1]{\paragraph{#1}} -\renewcommand{\isamarkupsubsubsect}[1]{\paragraph{#1}} \part{Examples} \chapter{The Employee Analysis Model} \label{ex:employee-analysis} diff --git a/document/root.tex b/document/root.tex index 29b35a8..40336cc 100644 --- a/document/root.tex +++ b/document/root.tex @@ -66,13 +66,6 @@ \isabellestyle{it} \newcommand{\ie}{i.\,e.\xspace} \newcommand{\eg}{e.\,g.\xspace} -\renewcommand{\isamarkupheader}[1]{\chapter{#1}} -\renewcommand{\isamarkupsection}[1]{\section{#1}} -\renewcommand{\isamarkupsubsection}[1]{\subsection{#1}} -\renewcommand{\isamarkupsubsubsection}[1]{\subsubsection{#1}} -\renewcommand{\isamarkupsect}[1]{\section{#1}} -\renewcommand{\isamarkupsubsect}[1]{\susubsection{#1}} -\renewcommand{\isamarkupsubsubsect}[1]{\subsubsection{#1}} \begin{document} \renewcommand{\subsubsectionautorefname}{Section} diff --git a/examples/Employee_AnalysisModel_OCLPart.thy b/examples/Employee_AnalysisModel_OCLPart.thy index 9cd602d..09b143d 100644 --- a/examples/Employee_AnalysisModel_OCLPart.thy +++ b/examples/Employee_AnalysisModel_OCLPart.thy @@ -40,7 +40,7 @@ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. ******************************************************************************) -header{* The Employee Analysis Model (OCL) *} +section{* The Employee Analysis Model (OCL) *} theory Employee_AnalysisModel_OCLPart @@ -48,10 +48,10 @@ imports Employee_AnalysisModel_UMLPart begin text {* \label{ex:employee-analysis:ocl} *} -section{* Standard State Infrastructure *} +subsection{* Standard State Infrastructure *} text{* Ideally, these definitions are automatically generated from the class model. *} -section{* Invariant *} +subsection{* 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} @@ -81,7 +81,7 @@ coinductive inv :: "Person \ (\)st \ bool" where ( (inv(self .boss))\ ))) \ ( inv self \)" -section{* The Contract of a Recursive Query *} +subsection{* The Contract of a Recursive Query *} text{* The original specification of a recursive query : \begin{ocl} context Person::contents():Set(Integer) @@ -121,7 +121,7 @@ text{* These \inlineocl{@pre} variants on methods are only available on queries, operations without side-effect. *} -section{* The Contract of a Method *} +subsection{* The Contract of a Method *} text{* The specification in high-level OCL input syntax reads as follows: \begin{ocl} diff --git a/examples/Employee_AnalysisModel_UMLPart.thy b/examples/Employee_AnalysisModel_UMLPart.thy index 0f8136b..0484178 100644 --- a/examples/Employee_AnalysisModel_UMLPart.thy +++ b/examples/Employee_AnalysisModel_UMLPart.thy @@ -40,7 +40,7 @@ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. ******************************************************************************) -header{* The Employee Analysis Model (UML) *} +section{* The Employee Analysis Model (UML) *} theory Employee_AnalysisModel_UMLPart @@ -50,7 +50,7 @@ begin text {* \label{ex:employee-analysis:uml} *} -section{* Introduction *} +subsection{* Introduction *} text{* For certain concepts like classes and class-types, only a generic definition for its resulting semantics can be given. Generic means, @@ -69,7 +69,7 @@ text{* Such generic function or ``compiler'' can be implemented in concepts of the compilation informally, and present a concrete example which is verified in Isabelle/HOL. *} -subsection{* Outlining the Example *} +subsubsection{* Outlining the Example *} text{* We are presenting here an ``analysis-model'' of the (slightly modified) example Figure 7.3, page 20 of @@ -95,7 +95,7 @@ by the attribute \inlineocl+boss+ and the operation \inlineocl+employees+ (to b captured by the subsequent theory). *} -section{* Example Data-Universe and its Infrastructure *} +subsection{* Example Data-Universe and its Infrastructure *} text{* Ideally, the following is generated automatically from a UML class model. *} (* @{text "'\"} -- \mathfrak{A} *) @@ -160,7 +160,7 @@ end -section{* Instantiation of the Generic Strict Equality *} +subsection{* Instantiation of the Generic Strict Equality *} text{* We instantiate the referential equality on @{text "Person"} and @{text "OclAny"} *} @@ -194,8 +194,8 @@ two operations to declare and to provide two overloading definitions for the two *} -section{* OclAsType *} -subsection{* Definition *} +subsection{* OclAsType *} +subsubsection{* 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')") @@ -236,7 +236,7 @@ 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 *} +subsubsection{* 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) @@ -267,7 +267,7 @@ 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 -subsection{* Execution with Invalid or Null as Argument *} +subsubsection{* 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) @@ -296,8 +296,8 @@ 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 *} -subsection{* Definition *} +subsection{* OclIsTypeOf *} +subsubsection{* 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')") @@ -332,7 +332,7 @@ defs (overloaded) OclIsTypeOf\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n_Pe \ \ invalid \ | _ \ true \)" -subsection{* Context Passing *} +subsubsection{* 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) @@ -364,7 +364,7 @@ lemmas [simp] = 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 -subsection{* Execution with Invalid or Null as Argument *} +subsubsection{* 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" @@ -399,7 +399,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 *} +subsubsection{* Up Down Casting *} lemma actualType_larger_staticType: assumes isdef: "\ \ (\ X)" @@ -456,8 +456,8 @@ shows "\ \ (X .oclIsTypeOf(Person) implies (X .oclAsType(OclAny) by (simp add: OclImplies_true) -section{* OclIsKindOf *} -subsection{* Definition *} +subsection{* OclIsKindOf *} +subsubsection{* 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')") @@ -488,7 +488,7 @@ defs (overloaded) OclIsKindOf\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n_Pe \ \ invalid \ | _ \ true \)" -subsection{* Context Passing *} +subsubsection{* 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) @@ -519,7 +519,7 @@ lemmas [simp] = 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 -subsection{* Execution with Invalid or Null as Argument *} +subsubsection{* 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 @@ -553,7 +553,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 *} +subsubsection{* Up Down Casting *} lemma actualKind_larger_staticKind: assumes isdef: "\ \ (\ X)" @@ -572,7 +572,7 @@ 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 *} +subsection{* OclAllInstances *} text{* To denote OCL-types occuring in OCL expressions syntactically---as, for example, as ``argument'' of \inlineisar{oclAllInstances()}---we use the inverses of the injection @@ -603,7 +603,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 *} +subsubsection{* 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" @@ -667,7 +667,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 *} +subsubsection{* OclIsKindOf *} lemma OclAny_allInstances_generic_oclIsKindOf\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y: "\ \ ((OclAllInstances_generic pre_post OclAny)->forAll(X|X .oclIsKindOf(OclAny)))" apply(simp add: OclValid_def del: OclAllInstances_generic_def) @@ -725,12 +725,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) *} +subsection{* 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) *} +subsubsection{* Definition (of the association Employee-Boss) *} 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, @@ -891,7 +891,7 @@ lemmas [simp] = 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 *} +subsubsection{* Context Passing *} lemmas [simp] = eval_extract_def @@ -924,7 +924,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 *} +subsubsection{* 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: null_fun_def null_option_def bot_option_def null_def invalid_def) @@ -956,7 +956,7 @@ lemma dot\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n\\\\\\ (\)st \ bool" where ( (inv(self .boss))\ ))) \ ( inv self \)" -section{* The Contract of a Recursive Query *} +subsection{* The Contract of a Recursive Query *} text{* The original specification of a recursive query : \begin{ocl} context Person::contents():Set(Integer) @@ -121,7 +121,7 @@ text{* These \inlineocl{@pre} variants on methods are only available on queries, operations without side-effect. *} -section{* The Contract of a Method *} +subsection{* The Contract of a Method *} text{* The specification in high-level OCL input syntax reads as follows: \begin{ocl} diff --git a/examples/Employee_DesignModel_UMLPart.thy b/examples/Employee_DesignModel_UMLPart.thy index 110b3d7..c446788 100644 --- a/examples/Employee_DesignModel_UMLPart.thy +++ b/examples/Employee_DesignModel_UMLPart.thy @@ -40,7 +40,7 @@ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. ******************************************************************************) -header{* The Employee Design Model (UML) *} +section{* The Employee Design Model (UML) *} theory Employee_DesignModel_UMLPart @@ -50,7 +50,7 @@ begin text {* \label{ex:employee-design:uml} *} -section{* Introduction *} +subsection{* Introduction *} text{* For certain concepts like classes and class-types, only a generic definition for its resulting semantics can be given. Generic means, @@ -69,7 +69,7 @@ text{* Such generic function or ``compiler'' can be implemented in concepts of the compilation informally, and present a concrete example which is verified in Isabelle/HOL. *} -subsection{* Outlining the Example *} +subsubsection{* Outlining the Example *} text{* We are presenting here a ``design-model'' of the (slightly modified) example Figure 7.3, page 20 of @@ -90,7 +90,7 @@ by the attribute \inlineocl+boss+ and the operation \inlineocl+employees+ (to b captured by the subsequent theory). *} -section{* Example Data-Universe and its Infrastructure *} +subsection{* Example Data-Universe and its Infrastructure *} text{* Ideally, the following is generated automatically from a UML class model. *} (* @{text "'\"} -- \mathfrak{A} *) @@ -156,7 +156,7 @@ end -section{* Instantiation of the Generic Strict Equality *} +subsection{* Instantiation of the Generic Strict Equality *} text{* We instantiate the referential equality on @{text "Person"} and @{text "OclAny"} *} @@ -190,8 +190,8 @@ two operations to declare and to provide two overloading definitions for the two *} -section{* OclAsType *} -subsection{* Definition *} +subsection{* OclAsType *} +subsubsection{* 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')") @@ -232,7 +232,7 @@ 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 *} +subsubsection{* 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) @@ -263,7 +263,7 @@ 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 -subsection{* Execution with Invalid or Null as Argument *} +subsubsection{* 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) @@ -292,8 +292,8 @@ 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 *} -subsection{* Definition *} +subsection{* OclIsTypeOf *} +subsubsection{* 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')") @@ -328,7 +328,7 @@ defs (overloaded) OclIsTypeOf\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n_Pe \ \ invalid \ | _ \ true \)" -subsection{* Context Passing *} +subsubsection{* 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) @@ -360,7 +360,7 @@ lemmas [simp] = 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 -subsection{* Execution with Invalid or Null as Argument *} +subsubsection{* 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" @@ -395,7 +395,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 *} +subsubsection{* Up Down Casting *} lemma actualType_larger_staticType: assumes isdef: "\ \ (\ X)" @@ -452,8 +452,8 @@ shows "\ \ (X .oclIsTypeOf(Person) implies (X .oclAsType(OclAny) by (simp add: OclImplies_true) -section{* OclIsKindOf *} -subsection{* Definition *} +subsection{* OclIsKindOf *} +subsubsection{* 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')") @@ -484,7 +484,7 @@ defs (overloaded) OclIsKindOf\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n_Pe \ \ invalid \ | _ \ true \)" -subsection{* Context Passing *} +subsubsection{* 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) @@ -515,7 +515,7 @@ lemmas [simp] = 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 -subsection{* Execution with Invalid or Null as Argument *} +subsubsection{* 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 @@ -549,7 +549,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 *} +subsubsection{* Up Down Casting *} lemma actualKind_larger_staticKind: assumes isdef: "\ \ (\ X)" @@ -568,7 +568,7 @@ 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 *} +subsection{* OclAllInstances *} text{* To denote OCL-types occuring in OCL expressions syntactically---as, for example, as ``argument'' of \inlineisar{oclAllInstances()}---we use the inverses of the injection @@ -599,7 +599,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 *} +subsubsection{* 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" @@ -663,7 +663,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 *} +subsubsection{* OclIsKindOf *} lemma OclAny_allInstances_generic_oclIsKindOf\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y: "\ \ ((OclAllInstances_generic pre_post OclAny)->forAll(X|X .oclIsKindOf(OclAny)))" apply(simp add: OclValid_def del: OclAllInstances_generic_def) @@ -721,12 +721,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) *} +subsection{* The Accessors (any, boss, salary) *} text{*\label{sec:edm-accessors}*} text{* Should be generated entirely from a class-diagram. *} -subsection{* Definition *} +subsubsection{* Definition *} definition eval_extract :: "('\,('a::object) option option) val \ (oid \ ('\,'c::null) val) @@ -823,7 +823,7 @@ lemmas [simp] = 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 *} +subsubsection{* Context Passing *} lemmas [simp] = eval_extract_def @@ -856,7 +856,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 *} +subsubsection{* 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: null_fun_def null_option_def bot_option_def null_def invalid_def) @@ -888,7 +888,7 @@ lemma dot\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n\\\\\\