afp-mirror
/
Featherweight_OCL
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Import of Featherweight OCL release afp-Featherweight_OCL-2014-08-28 (Isabelle 2014).

This commit is contained in:
Achim D. Brucker 2016-08-10 11:09:12 +01:00
parent 70a24eef96
commit 8449924cbd
4 changed files with 26 additions and 26 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
OCL_core.thy
View File

@ -557,7 +557,7 @@ text{*
the strict extension of the logical
equality:
*}
defs StrictRefEq\<^sub>B\<^sub>o\<^sub>o\<^sub>l\<^sub>e\<^sub>a\<^sub>n[code_unfold] :
defs (overloaded) StrictRefEq\<^sub>B\<^sub>o\<^sub>o\<^sub>l\<^sub>e\<^sub>a\<^sub>n[code_unfold] :
"(x::('\<AA>)Boolean) \<doteq> y \<equiv> \<lambda> \<tau>. if (\<upsilon> x) \<tau> = true \<tau> \<and> (\<upsilon> y) \<tau> = true \<tau>
then (x \<triangleq> y)\<tau>
else invalid \<tau>"
@ -949,7 +949,7 @@ lemma OclOr_null1[simp]: "\<And>\<tau>. X \<tau> \<noteq> true \<tau> \<Longrigh
apply(auto simp:true_def false_def bot_fun_def bot_option_def null_fun_def null_option_def
split: option.split option.split_asm)
apply (metis (full_types) bool.simps(3) bot_option_def null_is_valid null_option_def)
by (metis (full_types) bool.simps(3) option.distinct(1) the.simps)
by (metis (full_types) bool.simps(3) option.distinct(1) option.sel)
lemma OclOr_null2[simp]: "\<And>\<tau>. X \<tau> \<noteq> true \<tau> \<Longrightarrow> X \<tau> \<noteq> bot \<tau> \<Longrightarrow> (X or null) \<tau> = null \<tau>"
by(simp add: OclOr_commute)
@ -1127,9 +1127,9 @@ apply(simp add:invalid_def null_def null_fun_def)
by(auto simp: OclValid_def defined_def false_def true_def bot_fun_def null_fun_def
split:split_if_asm)
lemmas foundation17 = foundation16[THEN iffD1,standard]
lemmas foundation17 = foundation16[THEN iffD1]
(* correcter rule; the previous is deprecated *)
lemmas foundation17' = foundation16'[THEN iffD1,standard]
lemmas foundation17' = foundation16'[THEN iffD1]
lemma foundation18: "\<tau> \<Turnstile> (\<upsilon> X) = (X \<tau> \<noteq> invalid \<tau>)"
by(auto simp: OclValid_def valid_def false_def true_def bot_fun_def invalid_def
@ -1141,7 +1141,7 @@ by(auto simp: OclValid_def valid_def false_def true_def bot_fun_def
split:split_if_asm)
lemmas foundation19 = foundation18[THEN iffD1,standard]
lemmas foundation19 = foundation18[THEN iffD1]
lemma foundation20 : "\<tau> \<Turnstile> (\<delta> X) \<Longrightarrow> \<tau> \<Turnstile> \<upsilon> X"
by(simp add: foundation18 foundation16 invalid_def)

6
OCL_lib.thy
View File

@ -235,7 +235,7 @@ subsection{* Definition *}
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 "('\<AA>)Boolean"}-case as strict extension of the strong equality:*}
defs StrictRefEq\<^sub>I\<^sub>n\<^sub>t\<^sub>e\<^sub>g\<^sub>e\<^sub>r[code_unfold] :
defs (overloaded) StrictRefEq\<^sub>I\<^sub>n\<^sub>t\<^sub>e\<^sub>g\<^sub>e\<^sub>r[code_unfold] :
"(x::('\<AA>)Integer) \<doteq> y \<equiv> \<lambda> \<tau>. if (\<upsilon> x) \<tau> = true \<tau> \<and> (\<upsilon> y) \<tau> = true \<tau>
then (x \<triangleq> y) \<tau>
else invalid \<tau>"
@ -558,7 +558,7 @@ lemma S_lift' :
assumes S_all_def : "(\<tau> :: '\<AA> st) \<Turnstile> \<delta> S"
shows "\<exists>S'. (\<lambda>a (_::'\<AA> st). a) ` \<lceil>\<lceil>Rep_Set_0 (S \<tau>)\<rceil>\<rceil> = (\<lambda>a (_::'\<AA> st). \<lfloor>a\<rfloor>) ` S'"
apply(rule_tac x = "(\<lambda>a. \<lceil>a\<rceil>) ` \<lceil>\<lceil>Rep_Set_0 (S \<tau>)\<rceil>\<rceil>" in exI)
apply(simp only: image_comp[symmetric])
apply(simp only: image_comp)
apply(simp add: comp_def)
apply(rule image_cong, fast)
(* *)
@ -1363,7 +1363,7 @@ 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:*}
defs StrictRefEq\<^sub>S\<^sub>e\<^sub>t :
defs (overloaded) StrictRefEq\<^sub>S\<^sub>e\<^sub>t :
"(x::('\<AA>,'\<alpha>::null)Set) \<doteq> y \<equiv> \<lambda> \<tau>. if (\<upsilon> x) \<tau> = true \<tau> \<and> (\<upsilon> y) \<tau> = true \<tau>
then (x \<triangleq> y)\<tau>
else invalid \<tau>"

30
ROOT
View File

@ -2,23 +2,23 @@ chapter AFP
session Featherweight_OCL (AFP) = HOL +
description {* Featherweight-OCL *}
options [document = pdf, document_variants="document:outline=/proof,/ML"]
options [document_variants = "document:outline=/proof,/ML"]
theories
"OCL_main"
"examples/Employee_AnalysisModel_OCLPart"
"examples/Employee_DesignModel_OCLPart"
files
"document/conclusion.tex"
"document/formalization.tex"
"document/hol-ocl-isar.sty"
"document/introduction.tex"
"document/lstisar.sty"
"document/prooftree.sty"
"document/root.bib"
"document/root.tex"
"document/figures/AbstractSimpleChair.pdf"
"document/figures/jedit.png"
"document/figures/pdf.png"
"document/figures/person.png"
"document/figures/pre-post.pdf"
document_files
"conclusion.tex"
"formalization.tex"
"hol-ocl-isar.sty"
"introduction.tex"
"lstisar.sty"
"prooftree.sty"
"root.bib"
"root.tex"
"figures/AbstractSimpleChair.pdf"
"figures/jedit.png"
"figures/pdf.png"
"figures/person.png"
"figures/pre-post.pdf"

6
document/root.tex
View File

@ -1,4 +1,4 @@
\documentclass[11pt,a4paper,openright,twoside,abstracton]{scrreprt}
\documentclass[fontsize=11pt,paper=a4,open=right,twoside,abstract=true]{scrreprt}
\usepackage{fixltx2e}
\usepackage{isabelle,isabellesym}
\usepackage[nocolortable, noaclist]{hol-ocl-isar}
@ -11,7 +11,7 @@
\usepackage{tabu}
\usepackage[]{mathtools}
\usepackage{prooftree}
\usepackage{aeguill}
\usepackage[english]{babel}
\usepackage[pdfpagelabels, pageanchor=false, plainpages=false]{hyperref}
% \usepackage[draft]{fixme}
@ -55,7 +55,7 @@
{\operatorname{state}}%
{\operatorname{\mathit{state}}(#1)}%
}
\newcommand{\mocl}[1]{\text{\inlineocl{#1}}}
\newcommand{\mocl}[1]{\text{\inlineocl|#1|}}
\DeclareMathOperator{\TCnull}{null}
\DeclareMathOperator{\HolNull}{null}
\DeclareMathOperator{\HolBot}{bot}