Import of current (Isabelle 2017) release of Featherweight OCL.
This commit is contained in:
parent
98db296499
commit
8bf5757ecd
|
@ -5,7 +5,7 @@ session Featherweight_OCL (AFP) = HOL +
|
||||||
options [document_variants = "annex-a=annexa,-theory,-afp,-proof,-ML:document=afp,-annexa:outline=-annexa,afp,/proof,/ML",
|
options [document_variants = "annex-a=annexa,-theory,-afp,-proof,-ML:document=afp,-annexa:outline=-annexa,afp,/proof,/ML",
|
||||||
show_question_marks = false, timeout = 600]
|
show_question_marks = false, timeout = 600]
|
||||||
theories
|
theories
|
||||||
"UML_Main"
|
UML_Main
|
||||||
"examples/Employee_Model/Analysis/Analysis_OCL"
|
"examples/Employee_Model/Analysis/Analysis_OCL"
|
||||||
"examples/Employee_Model/Design/Design_OCL"
|
"examples/Employee_Model/Design/Design_OCL"
|
||||||
document_files
|
document_files
|
||||||
|
|
|
@ -43,7 +43,7 @@
|
||||||
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
|
theory UML_Types
|
||||||
imports Transcendental
|
imports HOL.Transcendental
|
||||||
keywords "Assert" :: thy_decl
|
keywords "Assert" :: thy_decl
|
||||||
and "Assert_local" :: thy_decl
|
and "Assert_local" :: thy_decl
|
||||||
begin
|
begin
|
||||||
|
@ -616,9 +616,9 @@ fun outer_syntax_command command_spec theory in_local =
|
||||||
Outer_Syntax.command command_spec "assert that the given specification is true"
|
Outer_Syntax.command command_spec "assert that the given specification is true"
|
||||||
(Parse.term >> (fn elems_concl => theory (fn thy =>
|
(Parse.term >> (fn elems_concl => theory (fn thy =>
|
||||||
case
|
case
|
||||||
lemma "code_unfold" (Specification.theorem true)
|
lemma "nbe" (Specification.theorem true)
|
||||||
(fn lthy =>
|
(fn lthy =>
|
||||||
let val expr = Value_Command.value lthy (Syntax.read_term lthy elems_concl)
|
let val expr = Nbe.dynamic_value lthy (Syntax.read_term lthy elems_concl)
|
||||||
val thy = Proof_Context.theory_of lthy
|
val thy = Proof_Context.theory_of lthy
|
||||||
open HOLogic in
|
open HOLogic in
|
||||||
if Sign.typ_equiv thy (fastype_of expr, @{typ "prop"}) then
|
if Sign.typ_equiv thy (fastype_of expr, @{typ "prop"}) then
|
||||||
|
|
|
@ -67,7 +67,7 @@ text{* Our notion of typed bag goes beyond the usual notion of a finite executab
|
||||||
is powerful enough to capture \emph{the extension of a type} in UML and OCL. This means
|
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
|
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,
|
those (finite) ones representable in a state. This holds for base types as well as class types,
|
||||||
although the notion for class-types --- involving object id's not occuring in a state ---
|
although the notion for class-types --- involving object id's not occurring in a state ---
|
||||||
requires some care.
|
requires some care.
|
||||||
|
|
||||||
In a world with @{term invalid} and @{term null}, there are two notions extensions possible:
|
In a world with @{term invalid} and @{term null}, there are two notions extensions possible:
|
||||||
|
|
|
@ -59,7 +59,7 @@ text{* Our notion of typed set goes beyond the usual notion of a finite executab
|
||||||
is powerful enough to capture \emph{the extension of a type} in UML and OCL. This means
|
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
|
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,
|
those (finite) ones representable in a state. This holds for base types as well as class types,
|
||||||
although the notion for class-types --- involving object id's not occuring in a state ---
|
although the notion for class-types --- involving object id's not occurring in a state ---
|
||||||
requires some care.
|
requires some care.
|
||||||
|
|
||||||
In a world with @{term invalid} and @{term null}, there are two notions extensions possible:
|
In a world with @{term invalid} and @{term null}, there are two notions extensions possible:
|
||||||
|
|
|
@ -401,7 +401,7 @@
|
||||||
morekeywords={text,txt,finally,next,also,with,moreover,ultimately,thus,prefer,defer,declare,apply,of,OF,THEN,intros,in,fix,assume,from,this,show,have,and,note,let,hence,where,using},% then, and
|
morekeywords={text,txt,finally,next,also,with,moreover,ultimately,thus,prefer,defer,declare,apply,of,OF,THEN,intros,in,fix,assume,from,this,show,have,and,note,let,hence,where,using},% then, and
|
||||||
classoffset=2,%
|
classoffset=2,%
|
||||||
keywordstyle=\color{Blue}\textbf,%
|
keywordstyle=\color{Blue}\textbf,%
|
||||||
morekeywords={axclass,class,instance,recdef,primrec,constdefs,consts_code,types_code,consts,axioms,syntax,typedecl,arities,types,translations,inductive,typedef,datatype,record,instance,defs,specification,proof,test_spec,lemmas,lemma,assumes,shows,definition,fun,function,theorem,case},%
|
morekeywords={axclass,class,instance,primrec,constdefs,consts_code,types_code,consts,axioms,syntax,typedecl,arities,types,translations,inductive,typedef,datatype,record,instance,defs,specification,proof,test_spec,lemmas,lemma,assumes,shows,definition,fun,function,theorem,case},%
|
||||||
classoffset=3,%
|
classoffset=3,%
|
||||||
keywordstyle=\color{BrickRed}\textbf,%
|
keywordstyle=\color{BrickRed}\textbf,%
|
||||||
morekeywords={oops,sorry},%
|
morekeywords={oops,sorry},%
|
||||||
|
|
|
@ -627,7 +627,7 @@ by(simp add: OclIsKindOf\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n_OclAny
|
||||||
|
|
||||||
section{* OclAllInstances *}
|
section{* OclAllInstances *}
|
||||||
|
|
||||||
text{* To denote OCL-types occuring 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
|
``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.'' *}
|
||||||
|
|
||||||
|
|
|
@ -616,7 +616,7 @@ by(simp add: OclIsKindOf\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n_OclAny
|
||||||
|
|
||||||
section{* OclAllInstances *}
|
section{* OclAllInstances *}
|
||||||
|
|
||||||
text{* To denote OCL-types occuring 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
|
``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.'' *}
|
||||||
|
|
||||||
|
|
|
@ -54,7 +54,7 @@ Isabelle (version 3.6) mentions:
|
||||||
of their own. No starting spaces, nothing after it."
|
of their own. No starting spaces, nothing after it."
|
||||||
In particular, it is not advised to put these tags in a single line:
|
In particular, it is not advised to put these tags in a single line:
|
||||||
\isatagafp ... \endisatagafp % wrong
|
\isatagafp ... \endisatagafp % wrong
|
||||||
otherwise as side effects some parts occuring after these tags may be
|
otherwise as side effects some parts occurring after these tags may be
|
||||||
skipped. The recommanded solution is to always write each tag in a
|
skipped. The recommanded solution is to always write each tag in a
|
||||||
separate line:
|
separate line:
|
||||||
\isatagafp
|
\isatagafp
|
||||||
|
|
Loading…
Reference in New Issue