From 49ed81521f12cf21fb4e3767b23aac329d65051c Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Mon, 26 Dec 2016 11:28:09 +0000 Subject: [PATCH] Import of current (Isabelle 2016-1) release of Featherweight OCL. --- ROOT | 1 - .../Employee_Model/Analysis/Analysis_UML.thy | 2 +- src/UML_Contracts.thy | 6 +-- src/UML_Logic.thy | 22 ++++----- src/UML_PropertyProfiles.thy | 12 ++--- src/UML_State.thy | 46 +++++++++---------- src/UML_Types.thy | 18 +++----- src/collection_types/UML_Bag.thy | 22 ++++----- src/collection_types/UML_Sequence.thy | 2 +- src/collection_types/UML_Set.thy | 46 +++++++++---------- src/document/introduction.tex | 2 +- 11 files changed, 86 insertions(+), 93 deletions(-) diff --git a/ROOT b/ROOT index 3030b52..fc500c4 100644 --- a/ROOT +++ b/ROOT @@ -65,4 +65,3 @@ session Featherweight_OCL (AFP) in "src" = HOL + "root.bib" "root.tex" "FOCL_Syntax.tex" - diff --git a/examples/Employee_Model/Analysis/Analysis_UML.thy b/examples/Employee_Model/Analysis/Analysis_UML.thy index 2768998..36c0ef9 100644 --- a/examples/Employee_Model/Analysis/Analysis_UML.thy +++ b/examples/Employee_Model/Analysis/Analysis_UML.thy @@ -82,7 +82,7 @@ done in our ``design model'' (see \autoref{ex:employee-design:uml}). \endisatagafp \isatagannexa -(see \url{http://afp.sourceforge.net/entries/Featherweight_OCL.shtml}). +(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}):*} diff --git a/src/UML_Contracts.thy b/src/UML_Contracts.thy index 0a154c4..65344bc 100644 --- a/src/UML_Contracts.thy +++ b/src/UML_Contracts.thy @@ -210,7 +210,7 @@ begin lemma defined_mono : "\ \\(f Y Z) \ (\ \\ Y) \ (\ \\ Z)" by(auto simp: valid_def bot_fun_def invalid_def def_scheme StrongEq_def OclValid_def false_def true_def - split: split_if_asm) + split: if_split_asm) lemma cp_pre: "cp self' \ cp a1' \ cp (\X. PRE (self' X) (a1' X) )" by(rule_tac f=PRE in cpI2, auto intro: cp\<^sub>P\<^sub>R\<^sub>E) @@ -278,7 +278,7 @@ begin lemma defined_mono : "\ \\(f X Y Z) \ (\ \\ X) \ (\ \\ Y) \ (\ \\ Z)" by(auto simp: valid_def bot_fun_def invalid_def def_scheme StrongEq_def OclValid_def false_def true_def - split: split_if_asm) + split: if_split_asm) lemma cp_pre: "cp self' \ cp a1' \ cp a2' \ cp (\X. PRE (self' X) (a1' X) (a2' X) )" by(rule_tac f=PRE in cpI3, auto intro: cp\<^sub>P\<^sub>R\<^sub>E) @@ -370,7 +370,7 @@ begin lemma defined_mono : "\ \\(f W X Y Z) \ (\ \\ W) \ (\ \\ X) \ (\ \\ Y) \ (\ \\ Z)" by(auto simp: valid_def bot_fun_def invalid_def def_scheme StrongEq_def OclValid_def false_def true_def - split: split_if_asm) + split: if_split_asm) lemma cp_pre: "cp self' \ cp a1' \ cp a2'\ cp a3' \ cp (\X. PRE (self' X) (a1' X) (a2' X) (a3' X) )" diff --git a/src/UML_Logic.thy b/src/UML_Logic.thy index 1f4cfe3..dd2b22e 100644 --- a/src/UML_Logic.thy +++ b/src/UML_Logic.thy @@ -710,7 +710,7 @@ apply(rule ext,auto simp: OclValid_def true_def defined_def) apply(erule_tac x=a in allE) apply(erule_tac x=b in allE) apply(auto simp: false_def true_def defined_def bot_Boolean_def null_Boolean_def - split: option.split_asm HOL.split_if_asm) + split: option.split_asm HOL.if_split_asm) done text{* However, certain properties (like transitivity) can not @@ -859,7 +859,7 @@ by(auto simp: OclNot_def OclValid_def valid_def invalid_def false_def true_def n (* ... and the usual rules on strictness, definedness propoagation, and cp ... *) lemma foundation16: "\ \ (\ X) = (X \ \ bot \ X \ \ null)" by(auto simp: OclValid_def defined_def false_def true_def bot_fun_def null_fun_def - split:split_if_asm) + split:if_split_asm) lemma foundation16'': "\(\ \ (\ X)) = ((\ \ (X \ invalid)) \ (\ \ (X \ null)))" apply(simp add: foundation16) @@ -869,18 +869,18 @@ by(auto simp:defined_def false_def true_def bot_fun_def null_fun_def OclValid_d lemma foundation16': "(\ \ (\ X)) = (X \ \ invalid \ \ X \ \ null \)" 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) + split:if_split_asm) lemma foundation18: "(\ \ (\ X)) = (X \ \ invalid \)" by(auto simp: OclValid_def valid_def false_def true_def bot_fun_def invalid_def - split:split_if_asm) + split:if_split_asm) (*legacy*) lemma foundation18': "(\ \ (\ X)) = (X \ \ bot)" by(auto simp: OclValid_def valid_def false_def true_def bot_fun_def - split:split_if_asm) + split:if_split_asm) lemma foundation18'': "(\ \ (\ X) )= (\(\ \ (X \ invalid)))" by(auto simp:foundation15) @@ -891,7 +891,7 @@ by(simp add: foundation18 foundation16 invalid_def) lemma foundation21: "(not A \ not B) = (A \ B)" by(rule ext, auto simp: OclNot_def StrongEq_def - split: bool.split_asm HOL.split_if_asm option.split) + split: bool.split_asm HOL.if_split_asm option.split) lemma foundation22: "(\ \ (X \ Y)) = (X \ = Y \)" by(auto simp: StrongEq_def OclValid_def true_def) @@ -926,24 +926,24 @@ by (simp add: foundation12 foundation6) lemma defined_not_I : "\ \ \ (x) \ \ \ \ (not x)" by(auto simp: OclNot_def null_def invalid_def defined_def valid_def OclValid_def true_def false_def bot_option_def null_option_def null_fun_def bot_fun_def - split: option.split_asm HOL.split_if_asm) + split: option.split_asm HOL.if_split_asm) lemma valid_not_I : "\ \ \ (x) \ \ \ \ (not x)" by(auto simp: OclNot_def null_def invalid_def defined_def valid_def OclValid_def true_def false_def bot_option_def null_option_def null_fun_def bot_fun_def - split: option.split_asm option.split HOL.split_if_asm) + split: option.split_asm option.split HOL.if_split_asm) lemma defined_and_I : "\ \ \ (x) \ \ \ \ (y) \ \ \ \ (x and y)" apply(simp add: OclAnd_def null_def invalid_def defined_def valid_def OclValid_def true_def false_def bot_option_def null_option_def null_fun_def bot_fun_def - split: option.split_asm HOL.split_if_asm) + split: option.split_asm HOL.if_split_asm) apply(auto simp: null_option_def split: bool.split) by(case_tac "ya",simp_all) lemma valid_and_I : "\ \ \ (x) \ \ \ \ (y) \ \ \ \ (x and y)" apply(simp add: OclAnd_def null_def invalid_def defined_def valid_def OclValid_def true_def false_def bot_option_def null_option_def null_fun_def bot_fun_def - split: option.split_asm HOL.split_if_asm) + split: option.split_asm HOL.if_split_asm) by(auto simp: null_option_def split: option.split bool.split) lemma defined_or_I : "\ \ \ (x) \ \ \ \ (y) \ \ \ \ (x or y)" @@ -1165,7 +1165,7 @@ lemma OclNot_defargs: "\ \ (not P) \ \ \ \ P" by(auto simp: OclNot_def OclValid_def true_def invalid_def defined_def false_def bot_fun_def bot_option_def null_fun_def null_option_def - split: bool.split_asm HOL.split_if_asm option.split option.split_asm) + split: bool.split_asm HOL.if_split_asm option.split option.split_asm) lemma OclNot_contrapos_nn: diff --git a/src/UML_PropertyProfiles.thy b/src/UML_PropertyProfiles.thy index c6e0aef..db2983e 100644 --- a/src/UML_PropertyProfiles.thy +++ b/src/UML_PropertyProfiles.thy @@ -125,7 +125,7 @@ begin apply(simp_all add:def_scheme) apply(simp add: OclValid_def) by(auto simp:foundation13 StrongEq_def false_def true_def defined_def bot_fun_def null_fun_def def_body - split: split_if_asm) + split: if_split_asm) lemma def_valid_then_def: "\(f x) = (\(f x))" apply(rule ext, rename_tac "\",subst foundation22[symmetric]) @@ -137,7 +137,7 @@ begin apply(simp add: OclValid_def valid_def, subst cp_StrongEq) apply(subst (2) cp_defined, simp, simp add: cp_defined[symmetric]) by(auto simp:foundation13 StrongEq_def false_def true_def defined_def bot_fun_def null_fun_def def_body - split: split_if_asm) + split: if_split_asm) end subsection{* Property Profiles for Single *} @@ -262,7 +262,7 @@ proof - apply(simp) apply(simp add: def_scheme') apply(simp add: defined_def OclValid_def false_def true_def - bot_fun_def null_fun_def def_scheme' split: split_if_asm, rule def_body') + bot_fun_def null_fun_def def_scheme' split: if_split_asm, rule def_body') by(simp add: true_def)+ qed @@ -286,7 +286,7 @@ sublocale profile_bin\<^sub>d_\<^sub>d < profile_bin_scheme_defined defined apply(erule StrongEq_L_subst2_rev, simp, simp)+ apply(simp add: def_scheme) apply(simp add: defined_def OclValid_def false_def true_def bot_fun_def null_fun_def def_scheme) - apply(rule def_body, simp_all add: true_def false_def split:split_if_asm) + apply(rule def_body, simp_all add: true_def false_def split:if_split_asm) done locale profile_bin\<^sub>d_\<^sub>v = @@ -326,7 +326,7 @@ context profile_bin\<^sub>S\<^sub>t\<^sub>r\<^sub>o\<^sub>n\<^sub>g\<^sub>E\<^su (* definedness *) lemma defargs: "\ \ f x y \ (\ \ \ x) \ (\ \ \ y)" by(simp add: def_scheme OclValid_def true_def invalid_def valid_def bot_option_def - split: bool.split_asm HOL.split_if_asm) + split: bool.split_asm HOL.if_split_asm) lemma defined_args_valid' : "\ (f x y) = (\ x and \ y)" by(auto intro!: transform2_rev defined_and_I simp:foundation10 defined_args_valid) @@ -370,7 +370,7 @@ sublocale profile_bin\<^sub>v_\<^sub>v < profile_bin_scheme valid valid foundation1 foundation10' foundation16' foundation18 foundation21 foundation22 foundation9) apply(simp add: def_scheme) apply(simp add: defined_def OclValid_def false_def true_def - bot_fun_def null_fun_def def_scheme split: split_if_asm, rule def_body) + bot_fun_def null_fun_def def_scheme split: if_split_asm, rule def_body) by (metis OclValid_def foundation18' true_def)+ end diff --git a/src/UML_State.thy b/src/UML_State.thy index 426036e..0755d31 100644 --- a/src/UML_State.thy +++ b/src/UML_State.thy @@ -106,7 +106,7 @@ 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 - split: bool.split_asm HOL.split_if_asm) + split: bool.split_asm HOL.if_split_asm) lemma defined_StrictRefEq\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_I: assumes val_x : "\ \ \ x" @@ -726,7 +726,7 @@ proof - simp add: OclAllInstances_at_pre_def OclAllInstances_at_post_def OclValid_def OclIncludes_def true_def F F' valid_x[simplified OclValid_def] valid_y[simplified OclValid_def] bot_option_def - split: split_if_asm, + split: if_split_asm, simp add: comp_def image_def, fastforce)+ qed @@ -807,7 +807,7 @@ lemma apply(insert X_null, simp add : OclIncludes_def OclIsModifiedOnly_def StrongEq_def OclValid_def true_def) apply(case_tac \, simp) - apply(simp split: split_if_asm) + apply(simp split: if_split_asm) by(simp add: null_fun_def, blast) subsubsection{* Context Passing *} @@ -869,7 +869,7 @@ proof - apply(erule bexE, rename_tac x') apply(simp add: P_def) apply(simp only: OclNot3[symmetric], simp only: not_inj) - apply(simp add: StrictRefEq\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def split: split_if_asm) + apply(simp add: StrictRefEq\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def split: if_split_asm) apply(subgoal_tac "x \ \ null \ x' \ null", simp) apply (metis (mono_tags) drop.simps def_x foundation16[THEN iffD1] true_def) by(simp add: invalid_def bot_option_def true_def)+ @@ -881,7 +881,7 @@ proof - apply(rule ballI, drule_tac x = "x'" in ballE) prefer 3 apply assumption apply(simp add: P_def) apply(simp only: OclNot4[symmetric], simp only: not_inj) - apply(simp add: StrictRefEq\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def false_def split: split_if_asm) + apply(simp add: StrictRefEq\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def false_def split: if_split_asm) apply(subgoal_tac "x \ \ null \ x' \ null", simp) apply (metis def_X' def_x foundation16[THEN iffD1]) by(simp add: invalid_def bot_option_def false_def)+ @@ -912,13 +912,13 @@ theorem framing: proof - show "\ \ \ x \ ?thesis" proof - assume def_x : "\ \ \ x" show ?thesis proof - have def_X : "\ \ \ X" - apply(insert oid_is_typerepr, simp add: UML_Set.OclForall_def OclValid_def split: split_if_asm) + apply(insert oid_is_typerepr, simp add: UML_Set.OclForall_def OclValid_def split: if_split_asm) by(simp add: bot_option_def true_def) have def_X' : "\x. x \ \\Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e (X \)\\ \ x \ null" - apply(insert modifiesclause, simp add: OclIsModifiedOnly_def OclValid_def split: split_if_asm) - apply(case_tac \, simp split: split_if_asm) - apply(simp add: UML_Set.OclExcluding_def split: split_if_asm) + apply(insert modifiesclause, simp add: OclIsModifiedOnly_def OclValid_def split: if_split_asm) + apply(case_tac \, simp split: if_split_asm) + apply(simp add: UML_Set.OclExcluding_def split: if_split_asm) apply(subst (asm) (2) Abs_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e_inverse) apply(simp, (rule disjI2)+) apply (metis (hide_lams, mono_tags) Diff_iff Set_inv_lemma def_X) @@ -939,7 +939,7 @@ theorem framing: apply(rule conjI, rule impI) apply(rule_tac f = "\x. P \x\" in arg_cong) apply(insert modifiesclause[simplified OclIsModifiedOnly_def OclValid_def]) - apply(case_tac \, rename_tac \ \', simp split: split_if_asm) + apply(case_tac \, rename_tac \ \', simp split: if_split_asm) apply(subst (asm) (2) UML_Set.OclExcluding_def) apply(drule foundation5[simplified OclValid_def true_def], simp) apply(subst (asm) Abs_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e_inverse, simp) @@ -971,7 +971,7 @@ theorem framing': shows "\ \ (x @pre P \ (x @post P))" proof - have def_X : "\ \ \ X" - apply(insert oid_is_typerepr, simp add: UML_Set.OclForall_def OclValid_def split: split_if_asm) + apply(insert oid_is_typerepr, simp add: UML_Set.OclForall_def OclValid_def split: if_split_asm) by(simp add: bot_option_def true_def) show ?thesis apply(case_tac "\ \ \ x", drule foundation20) @@ -991,32 +991,32 @@ lemma pre_post_new: "\ \ (x .oclIsNew()) \ \ \ (x .oclIsDeleted()) \ \ (\ \ \(x @pre H1)) \ \ (\ \ \(x @post H2))" by(simp add: OclIsDeleted_def OclSelf_at_pre_def OclSelf_at_post_def OclValid_def StrongEq_def true_def false_def bot_option_def invalid_def bot_fun_def valid_def - split: split_if_asm) + split: if_split_asm) lemma pre_post_absent: "\ \ (x .oclIsAbsent()) \ \ (\ \ \(x @pre H1)) \ \ (\ \ \(x @post H2))" by(simp add: OclIsAbsent_def OclSelf_at_pre_def OclSelf_at_post_def OclValid_def StrongEq_def true_def false_def bot_option_def invalid_def bot_fun_def valid_def - split: split_if_asm) + split: if_split_asm) lemma pre_post_maintained: "(\ \ \(x @pre H1) \ \ \ \(x @post H2)) \ \ \ (x .oclIsMaintained())" by(simp add: OclIsMaintained_def OclSelf_at_pre_def OclSelf_at_post_def OclValid_def StrongEq_def true_def false_def bot_option_def invalid_def bot_fun_def valid_def - split: split_if_asm) + split: if_split_asm) lemma pre_post_maintained': "\ \ (x .oclIsMaintained()) \ (\ \ \(x @pre (Some o H1)) \ \ \ \(x @post (Some o H2)))" by(simp add: OclIsMaintained_def OclSelf_at_pre_def OclSelf_at_post_def OclValid_def StrongEq_def true_def false_def bot_option_def invalid_def bot_fun_def valid_def - split: split_if_asm) + split: if_split_asm) 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) @@ -1110,7 +1110,7 @@ lemma select_object_any_defined\<^sub>S\<^sub>e\<^sub>q: apply(simp add: select_object_any\<^sub>S\<^sub>e\<^sub>q_def UML_Sequence.OclANY_def select_object\<^sub>S\<^sub>e\<^sub>q_def select_object_def defined_def OclValid_def false_def true_def bot_fun_def bot_option_def - split: split_if_asm) + split: if_split_asm) apply(simp add: mtSequence_def, subst (asm) Abs_Sequence\<^sub>b\<^sub>a\<^sub>s\<^sub>e_inverse, simp, simp) by(simp) @@ -1121,7 +1121,7 @@ lemma (*select_object_any_defined\<^sub>S\<^sub>e\<^sub>t:*) apply(simp add: select_object_any0\<^sub>S\<^sub>e\<^sub>t_def UML_Sequence.OclANY_def select_object\<^sub>S\<^sub>e\<^sub>t_def select_object_def defined_def OclValid_def false_def true_def bot_fun_def bot_option_def - split: split_if_asm) + split: if_split_asm) by(simp) lemma select_object_any_defined\<^sub>S\<^sub>e\<^sub>t: @@ -1132,14 +1132,14 @@ lemma select_object_any_defined\<^sub>S\<^sub>e\<^sub>t: defined_def OclValid_def false_def true_def bot_fun_def bot_option_def OclInt0_def OclInt1_def StrongEq_def OclIf_def null_fun_def null_option_def - split: split_if_asm) + split: if_split_asm) by(simp) lemma select_object_any_exec0\<^sub>S\<^sub>e\<^sub>q: assumes def_sel: "\ \ \ (select_object_any\<^sub>S\<^sub>e\<^sub>q f s_set)" shows "\ \ (select_object_any\<^sub>S\<^sub>e\<^sub>q f s_set \ f (hd s_set))" apply(insert def_sel[simplified foundation16], - simp add: select_object_any\<^sub>S\<^sub>e\<^sub>q_def foundation22 UML_Sequence.OclANY_def split: split_if_asm) + simp add: select_object_any\<^sub>S\<^sub>e\<^sub>q_def foundation22 UML_Sequence.OclANY_def split: if_split_asm) apply(case_tac "\\Rep_Sequence\<^sub>b\<^sub>a\<^sub>s\<^sub>e (select_object\<^sub>S\<^sub>e\<^sub>q f s_set \)\\", simp add: bot_option_def, simp) apply(simp add: select_object\<^sub>S\<^sub>e\<^sub>q_def select_object_def) apply(subst (asm) select_fold_exec\<^sub>S\<^sub>e\<^sub>q) @@ -1166,7 +1166,7 @@ proof - show ?thesis when "\\Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e (select_object\<^sub>S\<^sub>e\<^sub>t f s_set \)\\ = z" apply(insert that def_sel[simplified foundation16], - simp add: select_object_any0\<^sub>S\<^sub>e\<^sub>t_def foundation22 UML_Set.OclANY_def null_fun_def split: split_if_asm) + simp add: select_object_any0\<^sub>S\<^sub>e\<^sub>t_def foundation22 UML_Set.OclANY_def null_fun_def split: if_split_asm) apply(simp add: select_object\<^sub>S\<^sub>e\<^sub>t_def select_object_def) apply(subst (asm) select_fold_exec\<^sub>S\<^sub>e\<^sub>t) @@ -1239,10 +1239,10 @@ proof - apply(insert that def_sel[simplified foundation16], simp add: select_object_any\<^sub>S\<^sub>e\<^sub>t_def foundation22 Let_def null_fun_def bot_fun_def OclIf_def - split: split_if_asm) + split: if_split_asm) apply(simp add: StrongEq_def OclInt1_def true_def UML_Set.OclSize_def bot_option_def UML_Set.OclANY_def null_fun_def - split: split_if_asm) + split: if_split_asm) apply(subgoal_tac "\z'. z = {z'}") prefer 2 apply(rule finite.cases[where a = z], simp, simp, simp) diff --git a/src/UML_Types.thy b/src/UML_Types.thy index fd5dfbc..df5e6b3 100644 --- a/src/UML_Types.thy +++ b/src/UML_Types.thy @@ -600,8 +600,8 @@ fun disp_msg title msg status = title ^ ": '" ^ msg ^ "' " ^ status fun lemma msg specification_theorem concl in_local thy = SOME (in_local (fn lthy => - specification_theorem Thm.theoremK NONE (K I) (@{binding ""}, []) [] [] - (Element.Shows [((@{binding ""}, []),[(concl lthy, [])])]) + specification_theorem Thm.theoremK NONE (K I) Binding.empty_atts [] [] + (Element.Shows [(Binding.empty_atts, [(concl lthy, [])])]) false lthy |> Proof.global_terminal_proof ((Method.Combinator ( Method.no_combinator_info @@ -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" (Parse.term >> (fn elems_concl => theory (fn thy => case - lemma "code_unfold" Specification.theorem + lemma "code_unfold" (Specification.theorem true) (fn lthy => - let val expr = Value.value lthy (Syntax.read_term lthy elems_concl) + let val expr = Value_Command.value lthy (Syntax.read_term lthy elems_concl) val thy = Proof_Context.theory_of lthy open HOLogic in if Sign.typ_equiv thy (fastype_of expr, @{typ "prop"}) then @@ -629,7 +629,7 @@ fun outer_syntax_command command_spec theory in_local = thy of NONE => let val attr_simp = "simp" in - case lemma attr_simp Specification.theorem_cmd (K elems_concl) in_local thy of + case lemma attr_simp (Specification.theorem_cmd true) (K elems_concl) in_local thy of NONE => raise (ERROR "Assertion failed") | SOME thy => (writeln (disp_msg "OK" "simp" "finished the normalization"); @@ -637,13 +637,7 @@ fun outer_syntax_command command_spec theory in_local = end | SOME thy => thy))) -fun in_local decl thy = - thy - |> Named_Target.init "" - |> decl - |> Local_Theory.exit_global - -val () = outer_syntax_command @{command_keyword Assert} Toplevel.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/src/collection_types/UML_Bag.thy b/src/collection_types/UML_Bag.thy index f9dd7cb..a138a45 100644 --- a/src/collection_types/UML_Bag.thy +++ b/src/collection_types/UML_Bag.thy @@ -228,7 +228,7 @@ lemma Bag_inv_lemma: "\ \ (\ X) \ \b\<^sub>a\<^sub>s\<^sub>e [of "X \"], simp) apply(auto simp: OclValid_def defined_def false_def true_def cp_def bot_fun_def bot_Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e_def null_Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e_def null_fun_def - split:split_if_asm) + split:if_split_asm) apply(erule contrapos_pp [of "Rep_Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e (X \) = bot"]) apply(subst Abs_Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e_inject[symmetric], rule Rep_Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e, simp) apply(simp add: Rep_Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e_inverse bot_Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e_def bot_option_def) @@ -684,7 +684,7 @@ 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 defined_def invalid_def bot_fun_def null_fun_def - split: bool.split_asm HOL.split_if_asm option.split) + split: bool.split_asm HOL.if_split_asm option.split) lemma OclSize_infinite: assumes non_finite:"\ \ not(\(S->size\<^sub>B\<^sub>a\<^sub>g()))" @@ -692,7 +692,7 @@ shows "(\ \ not(\(S))) \ \ finite (Rep_Bag_bas apply(insert non_finite, simp) apply(rule impI) apply(simp add: OclSize_def OclValid_def defined_def bot_fun_def null_fun_def bot_option_def null_option_def - split: split_if_asm) + split: if_split_asm) done lemma "\ \ \ X \ \ finite (Rep_Bag_base X \) \ \ \ \ \ (X->size\<^sub>B\<^sub>a\<^sub>g())" @@ -717,7 +717,7 @@ 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 bot_fun_def null_fun_def OclAnd_def OclOr_def OclNot_def - split: split_if_asm) + split: if_split_asm) apply(case_tac "(X->size\<^sub>B\<^sub>a\<^sub>g() \ \) \", simp add: bot_option_def, simp, rename_tac x) apply(case_tac x, simp add: null_option_def bot_option_def, simp) apply(simp add: OclSize_def StrictRefEq\<^sub>I\<^sub>n\<^sub>t\<^sub>e\<^sub>g\<^sub>e\<^sub>r valid_def) @@ -727,12 +727,12 @@ by (metis (hide_lams, no_types) lemma "\ \ \ (null->isEmpty\<^sub>B\<^sub>a\<^sub>g())" by(auto simp: OclIsEmpty_def OclValid_def defined_def valid_def false_def true_def bot_fun_def null_fun_def OclAnd_def OclOr_def OclNot_def null_is_valid - split: split_if_asm) + split: if_split_asm) lemma OclIsEmpty_infinite: "\ \ \ X \ \ finite (Rep_Bag_base X \) \ \ \ \ \ (X->isEmpty\<^sub>B\<^sub>a\<^sub>g())" apply(auto simp: OclIsEmpty_def OclValid_def defined_def valid_def false_def true_def bot_fun_def null_fun_def OclAnd_def OclOr_def OclNot_def - split: split_if_asm) + split: if_split_asm) apply(case_tac "(X->size\<^sub>B\<^sub>a\<^sub>g() \ \) \", simp add: bot_option_def, simp, rename_tac x) apply(case_tac x, simp add: null_option_def bot_option_def, simp) by(simp add: OclSize_def StrictRefEq\<^sub>I\<^sub>n\<^sub>t\<^sub>e\<^sub>g\<^sub>e\<^sub>r valid_def bot_fun_def false_def true_def invalid_def) @@ -764,10 +764,10 @@ show "\ \ \ X \ apply(simp add: OclNotEmpty_def OclIsEmpty_def deMorgan1 deMorgan2, drule foundation5) apply(subst (asm) (2) OclNot_def, simp add: OclValid_def StrictRefEq\<^sub>I\<^sub>n\<^sub>t\<^sub>e\<^sub>g\<^sub>e\<^sub>r StrongEq_def - split: split_if_asm) + split: if_split_asm) prefer 2 apply(simp add: invalid_def bot_option_def true_def) - apply(simp add: OclSize_def valid_def split: split_if_asm, + apply(simp add: OclSize_def valid_def split: if_split_asm, simp_all add: false_def true_def bot_option_def bot_fun_def OclInt0_def) apply(drule s_non_empty[of "Rep_Bag_base X \"], erule exE, case_tac x) by blast @@ -784,7 +784,7 @@ 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 defined_def invalid_def bot_fun_def null_fun_def OclAnd_def - split: bool.split_asm HOL.split_if_asm option.split) + split: bool.split_asm HOL.if_split_asm option.split) lemma "\ \ \ X \ \ \ X->isEmpty\<^sub>B\<^sub>a\<^sub>g() \ \ \ \ \ (X->any\<^sub>B\<^sub>a\<^sub>g())" apply(simp add: OclANY_def OclValid_def) @@ -799,13 +799,13 @@ proof - have A: "(\ \ \(X->any\<^sub>B\<^sub>a\<^sub>g())) \ ((\ \(\ X)))" by(auto simp: OclANY_def OclValid_def true_def valid_def false_def StrongEq_def defined_def invalid_def bot_fun_def null_fun_def - split: bool.split_asm HOL.split_if_asm option.split) + split: bool.split_asm HOL.if_split_asm option.split) have B: "(\ \(\ X)) \ (\ \ \(X->any\<^sub>B\<^sub>a\<^sub>g()))" apply(auto simp: OclANY_def OclValid_def true_def false_def StrongEq_def defined_def invalid_def valid_def bot_fun_def null_fun_def bot_option_def null_option_def null_is_valid OclAnd_def - split: bool.split_asm HOL.split_if_asm option.split) + split: bool.split_asm HOL.if_split_asm option.split) apply(frule Bag_inv_lemma[OF foundation16[THEN iffD2], OF conjI], simp) apply(subgoal_tac "(\ X) \ = true \") prefer 2 diff --git a/src/collection_types/UML_Sequence.thy b/src/collection_types/UML_Sequence.thy index 3f37539..53b388d 100644 --- a/src/collection_types/UML_Sequence.thy +++ b/src/collection_types/UML_Sequence.thy @@ -57,7 +57,7 @@ lemma Sequence_inv_lemma: "\ \ (\ X) \ \< apply(insert Rep_Sequence\<^sub>b\<^sub>a\<^sub>s\<^sub>e [of "X \"], simp) apply(auto simp: OclValid_def defined_def false_def true_def cp_def bot_fun_def bot_Sequence\<^sub>b\<^sub>a\<^sub>s\<^sub>e_def null_Sequence\<^sub>b\<^sub>a\<^sub>s\<^sub>e_def null_fun_def - split:split_if_asm) + split:if_split_asm) apply(erule contrapos_pp [of "Rep_Sequence\<^sub>b\<^sub>a\<^sub>s\<^sub>e (X \) = bot"]) apply(subst Abs_Sequence\<^sub>b\<^sub>a\<^sub>s\<^sub>e_inject[symmetric], rule Rep_Sequence\<^sub>b\<^sub>a\<^sub>s\<^sub>e, simp) apply(simp add: Rep_Sequence\<^sub>b\<^sub>a\<^sub>s\<^sub>e_inverse bot_Sequence\<^sub>b\<^sub>a\<^sub>s\<^sub>e_def bot_option_def) diff --git a/src/collection_types/UML_Set.thy b/src/collection_types/UML_Set.thy index aa074b5..fb7baaf 100644 --- a/src/collection_types/UML_Set.thy +++ b/src/collection_types/UML_Set.thy @@ -160,7 +160,7 @@ show "?thesis" apply_end(erule ballE[where x = y], simp_all) apply_end(case_tac y, - simp add: bot_option_def null_option_def OclValid_def defined_def split: split_if_asm, + simp add: bot_option_def null_option_def OclValid_def defined_def split: if_split_asm, simp add: false_def true_def) qed (erule disjE, simp add: bot_Void_def, simp) qed qed qed qed qed @@ -221,7 +221,7 @@ lemma Set_inv_lemma: "\ \ (\ X) \ \b\<^sub>a\<^sub>s\<^sub>e [of "X \"], simp) apply(auto simp: OclValid_def defined_def false_def true_def cp_def bot_fun_def bot_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e_def null_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e_def null_fun_def - split:split_if_asm) + split:if_split_asm) apply(erule contrapos_pp [of "Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e (X \) = bot"]) apply(subst Abs_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e_inject[symmetric], rule Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e, simp) apply(simp add: Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e_inverse bot_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e_def bot_option_def) @@ -726,7 +726,7 @@ 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 defined_def invalid_def bot_fun_def null_fun_def - split: bool.split_asm HOL.split_if_asm option.split) + split: bool.split_asm HOL.if_split_asm option.split) lemma OclSize_infinite: assumes non_finite:"\ \ not(\(S->size\<^sub>S\<^sub>e\<^sub>t()))" @@ -760,7 +760,7 @@ 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 bot_fun_def null_fun_def OclAnd_def OclOr_def OclNot_def - split: split_if_asm) + split: if_split_asm) apply(case_tac "(X->size\<^sub>S\<^sub>e\<^sub>t() \ \) \", simp add: bot_option_def, simp, rename_tac x) apply(case_tac x, simp add: null_option_def bot_option_def, simp) apply(simp add: OclSize_def StrictRefEq\<^sub>I\<^sub>n\<^sub>t\<^sub>e\<^sub>g\<^sub>e\<^sub>r valid_def) @@ -770,12 +770,12 @@ by (metis (hide_lams, no_types) lemma "\ \ \ (null->isEmpty\<^sub>S\<^sub>e\<^sub>t())" by(auto simp: OclIsEmpty_def OclValid_def defined_def valid_def false_def true_def bot_fun_def null_fun_def OclAnd_def OclOr_def OclNot_def null_is_valid - split: split_if_asm) + split: if_split_asm) lemma OclIsEmpty_infinite: "\ \ \ X \ \ finite \\Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e (X \)\\ \ \ \ \ \ (X->isEmpty\<^sub>S\<^sub>e\<^sub>t())" apply(auto simp: OclIsEmpty_def OclValid_def defined_def valid_def false_def true_def bot_fun_def null_fun_def OclAnd_def OclOr_def OclNot_def - split: split_if_asm) + split: if_split_asm) apply(case_tac "(X->size\<^sub>S\<^sub>e\<^sub>t() \ \) \", simp add: bot_option_def, simp, rename_tac x) apply(case_tac x, simp add: null_option_def bot_option_def, simp) by(simp add: OclSize_def StrictRefEq\<^sub>I\<^sub>n\<^sub>t\<^sub>e\<^sub>g\<^sub>e\<^sub>r valid_def bot_fun_def false_def true_def invalid_def) @@ -801,10 +801,10 @@ lemma OclNotEmpty_has_elt : "\ \ \ X \ apply(simp add: OclNotEmpty_def OclIsEmpty_def deMorgan1 deMorgan2, drule foundation5) apply(subst (asm) (2) OclNot_def, simp add: OclValid_def StrictRefEq\<^sub>I\<^sub>n\<^sub>t\<^sub>e\<^sub>g\<^sub>e\<^sub>r StrongEq_def - split: split_if_asm) + split: if_split_asm) prefer 2 apply(simp add: invalid_def bot_option_def true_def) - apply(simp add: OclSize_def valid_def split: split_if_asm, + apply(simp add: OclSize_def valid_def split: if_split_asm, simp_all add: false_def true_def bot_option_def bot_fun_def OclInt0_def) by (metis equals0I) @@ -813,7 +813,7 @@ 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 defined_def invalid_def bot_fun_def null_fun_def OclAnd_def - split: bool.split_asm HOL.split_if_asm option.split) + split: bool.split_asm HOL.if_split_asm option.split) lemma "\ \ \ X \ \ \ X->isEmpty\<^sub>S\<^sub>e\<^sub>t() \ \ \ \ \ (X->any\<^sub>S\<^sub>e\<^sub>t())" apply(simp add: OclANY_def OclValid_def) @@ -828,13 +828,13 @@ proof - have A: "(\ \ \(X->any\<^sub>S\<^sub>e\<^sub>t())) \ ((\ \(\ X)))" by(auto simp: OclANY_def OclValid_def true_def valid_def false_def StrongEq_def defined_def invalid_def bot_fun_def null_fun_def - split: bool.split_asm HOL.split_if_asm option.split) + split: bool.split_asm HOL.if_split_asm option.split) have B: "(\ \(\ X)) \ (\ \ \(X->any\<^sub>S\<^sub>e\<^sub>t()))" apply(auto simp: OclANY_def OclValid_def true_def false_def StrongEq_def defined_def invalid_def valid_def bot_fun_def null_fun_def bot_option_def null_option_def null_is_valid OclAnd_def - split: bool.split_asm HOL.split_if_asm option.split) + split: bool.split_asm HOL.if_split_asm option.split) apply(frule Set_inv_lemma[OF foundation16[THEN iffD2], OF conjI], simp) apply(subgoal_tac "(\ X) \ = true \") prefer 2 @@ -1466,7 +1466,7 @@ proof - apply(simp add: Abs_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e_inverse[OF C]) apply(simp_all add: false_def true_def defined_def valid_def null_fun_def bot_fun_def null_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e_def bot_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e_def - split: bool.split_asm HOL.split_if_asm option.split) + split: bool.split_asm HOL.if_split_asm option.split) apply(auto simp: G1 G2) done qed @@ -1911,7 +1911,7 @@ proof - apply(rule impI) apply(drule Finite_Set.card.insert[where x = "x \"]) apply(rule includes_notin, simp, simp) - apply (metis Suc_eq_plus1 int_1 of_nat_add) + apply (metis Suc_eq_plus1 of_nat_1 of_nat_add) apply(subst (1 2) m[of \], simp only: OclAdd\<^sub>I\<^sub>n\<^sub>t\<^sub>e\<^sub>g\<^sub>e\<^sub>r.cp0[symmetric],simp, simp add:invalid_def) apply(subst OclIncluding_finite_rep_set, fast+, simp add: OclValid_def) @@ -1999,7 +1999,7 @@ lemma OclANY_singleton_exec[simp,code_unfold]: (* *) apply(subgoal_tac "a \ = \") prefer 2 - apply(simp add: OclValid_def valid_def bot_fun_def split: split_if_asm) + apply(simp add: OclValid_def valid_def bot_fun_def split: if_split_asm) apply(simp) apply(subst (1 2 3 4) cp_OclAnd, simp add: mtSet_defined[simplified mtSet_def] valid_def bot_fun_def) @@ -2692,7 +2692,7 @@ proof - subst (asm) cp_OclAnd, subst (asm) cp_OclNot) apply(simp only: OclValid_def foundation20[simplified OclValid_def] cp_OclNot[symmetric] cp_OclAnd[symmetric] cp_OclOr[symmetric]) - apply(simp add: Abs_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e_inverse split: split_if_asm) + apply(simp add: Abs_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e_inverse split: if_split_asm) by(simp add: true_def OclInt0_def OclNot_def StrictRefEq\<^sub>I\<^sub>n\<^sub>t\<^sub>e\<^sub>g\<^sub>e\<^sub>r StrongEq_def) have B: "\X \. \ finite \\Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e (X \)\\ \ (\ (X->size\<^sub>S\<^sub>e\<^sub>t())) \ = false \" @@ -2802,7 +2802,7 @@ proof - simp only: cp_OclAnd[THEN sym], simp add: defined_def bot_fun_def) - apply(split split_if_asm) + apply(split if_split_asm) apply(simp add: OclIncluding_finite_rep_set[simplified OclValid_def] card_including_exec)+ apply(simp only: cp_OclAnd[THEN sym], simp, rule impI, erule conjE) apply(case_tac "(\ x) \ = true \", simp add: cp_OclAnd[of "\ X" "\ x"]) @@ -2856,7 +2856,7 @@ proof - simp only: cp_OclAnd[THEN sym], simp add: defined_def bot_fun_def) - apply(split split_if_asm) + apply(split if_split_asm) apply(simp add: OclExcluding_finite_rep_set[simplified OclValid_def] card_excluding_exec)+ apply(simp only: cp_OclAnd[THEN sym], simp, rule impI, erule conjE) apply(case_tac "(\ x) \ = true \", simp add: cp_OclAnd[of "\ X" "\ x"]) @@ -2892,7 +2892,7 @@ proof - by metis show ?thesis apply(simp add: OclForall_def OclValid_def true_def false_def invalid_def - bot_fun_def bot_option_def null_fun_def null_option_def split: split_if_asm) + bot_fun_def bot_option_def null_fun_def null_option_def split: if_split_asm) apply(rule conjI, rule impI) apply (metis drop.simps option.distinct(1) invalid_def) apply(rule impI, rule conjI, rule impI) apply (metis option.distinct(1)) apply(rule impI, rule conjI, rule impI) apply (metis drop.simps) @@ -2991,7 +2991,7 @@ lemma OclForall_cong: shows "\ \ OclForall X Q" proof - have def_X: "\ \ \ X" - by(insert P, simp add: OclForall_def OclValid_def bot_option_def true_def split: split_if_asm) + by(insert P, simp add: OclForall_def OclValid_def bot_option_def true_def split: if_split_asm) show ?thesis apply(insert P) apply(subst (asm) OclForall_rep_set_true[OF def_X], subst OclForall_rep_set_true[OF def_X]) @@ -3005,7 +3005,7 @@ lemma OclForall_cong': shows "\ \ OclForall X R" proof - have def_X: "\ \ \ X" - by(insert P, simp add: OclForall_def OclValid_def bot_option_def true_def split: split_if_asm) + by(insert P, simp add: OclForall_def OclValid_def bot_option_def true_def split: if_split_asm) show ?thesis apply(insert P Q) apply(subst (asm) (1 2) OclForall_rep_set_true[OF def_X], subst OclForall_rep_set_true[OF def_X]) @@ -3025,7 +3025,7 @@ proof - x \ \ y \ \ \\Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e (y \)\\ \ \\Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e (x \)\\" apply(simp add: defined_def) - apply(split split_if_asm, simp add: false_def true_def)+ + apply(split if_split_asm, simp add: false_def true_def)+ apply(simp add: null_fun_def null_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e_def bot_fun_def bot_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e_def) apply(case_tac "x \", rename_tac x') @@ -3103,7 +3103,7 @@ qed lemma StrictRefEq\<^sub>S\<^sub>e\<^sub>t_L_subst1 : "cp P \ \ \ \ x \ \ \ \ y \ \ \ \ P x \ \ \ \ P y \ \ \ (x::('\,'\::null)Set) \ y \ \ \ (P x ::('\,'\::null)Set) \ P y" apply(simp only: StrictRefEq\<^sub>S\<^sub>e\<^sub>t OclValid_def) - apply(split split_if_asm) + apply(split if_split_asm) apply(simp add: StrongEq_L_subst1[simplified OclValid_def]) by (simp add: invalid_def bot_option_def true_def) @@ -3127,7 +3127,7 @@ lemma OclIncluding_cong : "\(s::('\,'a::null)Set) t x y \. \ \ \ s \ t \ x = y \ \ \ s->including\<^sub>S\<^sub>e\<^sub>t(x) \ (t->including\<^sub>S\<^sub>e\<^sub>t(y))" apply(simp only:) apply(rule OclIncluding_cong', simp_all only:) -by(auto simp: OclValid_def OclIf_def invalid_def bot_option_def OclNot_def split : split_if_asm) +by(auto simp: OclValid_def OclIf_def invalid_def bot_option_def OclNot_def split : if_split_asm) (* < *) lemma const_StrictRefEq\<^sub>S\<^sub>e\<^sub>t_empty : "const X \ const (X \ Set{})" diff --git a/src/document/introduction.tex b/src/document/introduction.tex index 9f4ea1e..69804e6 100644 --- a/src/document/introduction.tex +++ b/src/document/introduction.tex @@ -93,7 +93,7 @@ formal semantics of the core of OCL, called \FOCL\footnote{An updated, machine-checked version and formally complete version of the complete formalization is maintained by the Isabelle Archive of Formal Proofs (AFP), see - \url{http://afp.sourceforge.net/entries/Featherweight_OCL.shtml}}. \FOCL + \url{http://isa-afp.org/entries/Featherweight_OCL.shtml}}. \FOCL has a formal semantics in Isabelle/\HOL~\cite{nipkow.ea:isabelle:2002}. \endisatagannexa