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

Migration to Isabelle 2021-1 (based on afp-2021-12-28).

This commit is contained in:
Achim D. Brucker 2021-12-30 19:13:15 +00:00
parent fd305c8136
commit f30ae05ab6
5 changed files with 50 additions and 50 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
Featherweight_OCL/UML_PropertyProfiles.thy
View File

@ -314,7 +314,7 @@ sublocale profile_bin\<^sub>S\<^sub>t\<^sub>r\<^sub>o\<^sub>n\<^sub>g\<^sub>E\<^
apply(simp)
apply(subst cp_valid, simp)
apply (simp add: const_valid)
apply (metis (hide_lams, mono_tags) OclValid_def def_scheme defined5 defined6 defined_and_I foundation1 foundation10' foundation16' foundation18 foundation21 foundation22 foundation9)
apply (metis (opaque_lifting, mono_tags) OclValid_def def_scheme defined5 defined6 defined_and_I foundation1 foundation10' foundation16' foundation18 foundation21 foundation22 foundation9)
apply(simp add: def_scheme, subst StrongEq_def, simp)
by (metis OclValid_def def_scheme defined7 foundation16)
@ -366,7 +366,7 @@ locale profile_bin\<^sub>v_\<^sub>v =
sublocale profile_bin\<^sub>v_\<^sub>v < profile_bin_scheme valid valid
apply(unfold_locales)
apply(simp, subst cp_valid, simp, rule const_valid, simp)+
apply (metis (hide_lams, mono_tags) OclValid_def def_scheme defined5 defined6 defined_and_I
apply (metis (opaque_lifting, mono_tags) OclValid_def def_scheme defined5 defined6 defined_and_I
foundation1 foundation10' foundation16' foundation18 foundation21 foundation22 foundation9)
apply(simp add: def_scheme)
apply(simp add: defined_def OclValid_def false_def true_def

16
Featherweight_OCL/UML_State.thy
View File

@ -921,12 +921,12 @@ theorem framing:
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)
apply (metis (opaque_lifting, mono_tags) Diff_iff Set_inv_lemma def_X)
apply(simp)
apply(erule ballE[where P = "\<lambda>x. x \<noteq> null"]) apply(assumption)
apply(simp)
apply (metis (hide_lams, no_types) def_x foundation16[THEN iffD1])
apply (metis (hide_lams, no_types) OclValid_def def_X def_x foundation20
apply (metis (opaque_lifting, no_types) def_x foundation16[THEN iffD1])
apply (metis (opaque_lifting, no_types) OclValid_def def_X def_x foundation20
OclExcluding_valid_args_valid OclExcluding_valid_args_valid'')
by(simp add: invalid_def bot_option_def)
@ -944,11 +944,11 @@ theorem framing:
apply(drule foundation5[simplified OclValid_def true_def], simp)
apply(subst (asm) Abs_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e_inverse, simp)
apply(rule disjI2)+
apply (metis (hide_lams, no_types) DiffD1 OclValid_def Set_inv_lemma def_x
apply (metis (opaque_lifting, no_types) DiffD1 OclValid_def Set_inv_lemma def_x
foundation16 foundation18')
apply(simp)
apply(erule_tac x = "oid_of (x (\<sigma>, \<sigma>'))" in ballE) apply simp+
apply (metis (hide_lams, no_types)
apply (metis (opaque_lifting, no_types)
DiffD1 image_iff image_insert insert_Diff_single insert_absorb oid_is_typerepr)
apply(simp add: invalid_def bot_option_def)+
by blast
@ -1092,7 +1092,7 @@ lemma fold_val_elem\<^sub>S\<^sub>e\<^sub>q:
shows "list_all (\<lambda>x. (\<tau> \<Turnstile> \<upsilon> (f p x))) s_set"
apply(rule rev_induct[where P = "\<lambda>s_set. \<tau> \<Turnstile> \<upsilon> foldl UML_Sequence.OclIncluding Sequence{} (List.map (f p) s_set) \<longrightarrow> list_all (\<lambda>x. \<tau> \<Turnstile> \<upsilon> f p x) s_set", THEN mp])
apply(simp, auto)
apply (metis (hide_lams, mono_tags) UML_Sequence.OclIncluding.def_valid_then_def UML_Sequence.OclIncluding.defined_args_valid foundation20)+
apply (metis (opaque_lifting, mono_tags) UML_Sequence.OclIncluding.def_valid_then_def UML_Sequence.OclIncluding.defined_args_valid foundation20)+
by(simp add: assms)
lemma fold_val_elem\<^sub>S\<^sub>e\<^sub>t:
@ -1100,7 +1100,7 @@ lemma fold_val_elem\<^sub>S\<^sub>e\<^sub>t:
shows "list_all (\<lambda>x. (\<tau> \<Turnstile> \<upsilon> (f p x))) s_set"
apply(rule rev_induct[where P = "\<lambda>s_set. \<tau> \<Turnstile> \<upsilon> foldl UML_Set.OclIncluding Set{} (List.map (f p) s_set) \<longrightarrow> list_all (\<lambda>x. \<tau> \<Turnstile> \<upsilon> f p x) s_set", THEN mp])
apply(simp, auto)
apply (metis (hide_lams, mono_tags) foundation10' foundation20)+
apply (metis (opaque_lifting, mono_tags) foundation10' foundation20)+
by(simp add: assms)
lemma select_object_any_defined\<^sub>S\<^sub>e\<^sub>q:
@ -1258,7 +1258,7 @@ proof -
proof - fix z' a list show "(\<lambda>x. f x \<tau>) ` set s_set = {z'} \<Longrightarrow> s_set = a # list \<Longrightarrow> \<exists>e. List.member s_set e \<and> z' = f e \<tau>"
apply(drule list_same[where x1 = a])
apply (metis member_rec(1))
by (metis (hide_lams, mono_tags) ListMem_iff elem in_set_member)
by (metis (opaque_lifting, mono_tags) ListMem_iff elem in_set_member)
qed
qed blast+

10
Featherweight_OCL/collection_types/UML_Bag.thy
View File

@ -640,7 +640,7 @@ text\<open>OclIncluding\<close>
lemma OclIncluding_valid_args_valid:
"(\<tau> \<Turnstile> \<upsilon>(X->including\<^sub>B\<^sub>a\<^sub>g(x))) = ((\<tau> \<Turnstile>(\<delta> X)) \<and> (\<tau> \<Turnstile>(\<upsilon> x)))"
by (metis (hide_lams, no_types) OclIncluding.def_valid_then_def OclIncluding.defined_args_valid)
by (metis (opaque_lifting, no_types) OclIncluding.def_valid_then_def OclIncluding.defined_args_valid)
lemma OclIncluding_valid_args_valid''[simp,code_unfold]:
"\<upsilon>(X->including\<^sub>B\<^sub>a\<^sub>g(x)) = ((\<delta> X) and (\<upsilon> x))"
@ -721,7 +721,7 @@ lemma OclIsEmpty_defined_args_valid:"\<tau> \<Turnstile> \<delta> (X->isEmpty\<^
apply(case_tac "(X->size\<^sub>B\<^sub>a\<^sub>g() \<doteq> \<zero>) \<tau>", 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)
by (metis (hide_lams, no_types)
by (metis (opaque_lifting, no_types)
bot_fun_def OclValid_def defined_def foundation2 invalid_def)
lemma "\<tau> \<Turnstile> \<delta> (null->isEmpty\<^sub>B\<^sub>a\<^sub>g())"
@ -740,11 +740,11 @@ by(simp add: OclSize_def StrictRefEq\<^sub>I\<^sub>n\<^sub>t\<^sub>e\<^sub>g\<^s
text\<open>OclNotEmpty\<close>
lemma OclNotEmpty_defined_args_valid:"\<tau> \<Turnstile> \<delta> (X->notEmpty\<^sub>B\<^sub>a\<^sub>g()) \<Longrightarrow> \<tau> \<Turnstile> \<upsilon> X"
by (metis (hide_lams, no_types) OclNotEmpty_def OclNot_defargs OclNot_not foundation6 foundation9
by (metis (opaque_lifting, no_types) OclNotEmpty_def OclNot_defargs OclNot_not foundation6 foundation9
OclIsEmpty_defined_args_valid)
lemma "\<tau> \<Turnstile> \<delta> (null->notEmpty\<^sub>B\<^sub>a\<^sub>g())"
by (metis (hide_lams, no_types) OclNotEmpty_def OclAnd_false1 OclAnd_idem OclIsEmpty_def
by (metis (opaque_lifting, no_types) OclNotEmpty_def OclAnd_false1 OclAnd_idem OclIsEmpty_def
OclNot3 OclNot4 OclOr_def defined2 defined4 transform1 valid2)
lemma OclNotEmpty_infinite: "\<tau> \<Turnstile> \<delta> X \<Longrightarrow> \<not> finite (Rep_Bag_base X \<tau>) \<Longrightarrow> \<not> \<tau> \<Turnstile> \<delta> (X->notEmpty\<^sub>B\<^sub>a\<^sub>g())"
@ -809,7 +809,7 @@ proof -
apply(frule Bag_inv_lemma[OF foundation16[THEN iffD2], OF conjI], simp)
apply(subgoal_tac "(\<delta> X) \<tau> = true \<tau>")
prefer 2
apply (metis (hide_lams, no_types) OclValid_def foundation16)
apply (metis (opaque_lifting, no_types) OclValid_def foundation16)
apply(simp add: true_def,
drule OclNotEmpty_has_elt'[simplified OclValid_def true_def], simp)
apply(erule exE,

68
Featherweight_OCL/collection_types/UML_Set.thy
View File

@ -682,7 +682,7 @@ text\<open>OclIncluding\<close>
lemma OclIncluding_valid_args_valid:
"(\<tau> \<Turnstile> \<upsilon>(X->including\<^sub>S\<^sub>e\<^sub>t(x))) = ((\<tau> \<Turnstile>(\<delta> X)) \<and> (\<tau> \<Turnstile>(\<upsilon> x)))"
by (metis (hide_lams, no_types) OclIncluding.def_valid_then_def OclIncluding.defined_args_valid)
by (metis (opaque_lifting, no_types) OclIncluding.def_valid_then_def OclIncluding.defined_args_valid)
lemma OclIncluding_valid_args_valid''[simp,code_unfold]:
"\<upsilon>(X->including\<^sub>S\<^sub>e\<^sub>t(x)) = ((\<delta> X) and (\<upsilon> x))"
@ -764,7 +764,7 @@ lemma OclIsEmpty_defined_args_valid:"\<tau> \<Turnstile> \<delta> (X->isEmpty\<^
apply(case_tac "(X->size\<^sub>S\<^sub>e\<^sub>t() \<doteq> \<zero>) \<tau>", 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)
by (metis (hide_lams, no_types)
by (metis (opaque_lifting, no_types)
bot_fun_def OclValid_def defined_def foundation2 invalid_def)
lemma "\<tau> \<Turnstile> \<delta> (null->isEmpty\<^sub>S\<^sub>e\<^sub>t())"
@ -783,11 +783,11 @@ by(simp add: OclSize_def StrictRefEq\<^sub>I\<^sub>n\<^sub>t\<^sub>e\<^sub>g\<^s
text\<open>OclNotEmpty\<close>
lemma OclNotEmpty_defined_args_valid:"\<tau> \<Turnstile> \<delta> (X->notEmpty\<^sub>S\<^sub>e\<^sub>t()) \<Longrightarrow> \<tau> \<Turnstile> \<upsilon> X"
by (metis (hide_lams, no_types) OclNotEmpty_def OclNot_defargs OclNot_not foundation6 foundation9
by (metis (opaque_lifting, no_types) OclNotEmpty_def OclNot_defargs OclNot_not foundation6 foundation9
OclIsEmpty_defined_args_valid)
lemma "\<tau> \<Turnstile> \<delta> (null->notEmpty\<^sub>S\<^sub>e\<^sub>t())"
by (metis (hide_lams, no_types) OclNotEmpty_def OclAnd_false1 OclAnd_idem OclIsEmpty_def
by (metis (opaque_lifting, no_types) OclNotEmpty_def OclAnd_false1 OclAnd_idem OclIsEmpty_def
OclNot3 OclNot4 OclOr_def defined2 defined4 transform1 valid2)
lemma OclNotEmpty_infinite: "\<tau> \<Turnstile> \<delta> X \<Longrightarrow> \<not> finite \<lceil>\<lceil>Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e (X \<tau>)\<rceil>\<rceil> \<Longrightarrow> \<not> \<tau> \<Turnstile> \<delta> (X->notEmpty\<^sub>S\<^sub>e\<^sub>t())"
@ -838,7 +838,7 @@ proof -
apply(frule Set_inv_lemma[OF foundation16[THEN iffD2], OF conjI], simp)
apply(subgoal_tac "(\<delta> X) \<tau> = true \<tau>")
prefer 2
apply (metis (hide_lams, no_types) OclValid_def foundation16)
apply (metis (opaque_lifting, no_types) OclValid_def foundation16)
apply(simp add: true_def,
drule OclNotEmpty_has_elt[simplified OclValid_def true_def], simp)
by(erule exE,
@ -1259,7 +1259,7 @@ proof -
show ?thesis
apply(insert excludes_def[OF assms] excludes_val[OF assms] assms,
simp add: OclExcluding_def OclExcludes_def OclIncludes_def OclNot_def OclValid_def true_def)
by (metis (hide_lams, no_types) abs_rep_simp' assms excludes_def)
by (metis (opaque_lifting, no_types) abs_rep_simp' assms excludes_def)
qed
lemma OclExcluding_excludes:
@ -1823,7 +1823,7 @@ proof -
let ?OclSet = "\<lambda>S. \<lfloor>\<lfloor>S\<rfloor>\<rfloor> \<in> {X. X = \<bottom> \<or> X = null \<or> (\<forall>x\<in>\<lceil>\<lceil>X\<rceil>\<rceil>. x \<noteq> \<bottom>)}"
have diff_in_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e : "?OclSet (\<lceil>\<lceil>Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e (X \<tau>)\<rceil>\<rceil> - {x \<tau>})"
apply(simp, (rule disjI2)+)
by (metis (hide_lams, no_types) Diff_iff Set_inv_lemma def_X)
by (metis (opaque_lifting, no_types) Diff_iff Set_inv_lemma def_X)
show ?thesis
apply(subst OclExcludes_def, simp add: foundation10[simplified OclValid_def] OclValid_def
@ -1878,7 +1878,7 @@ proof -
have ins_in_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e: "\<tau> \<Turnstile> \<delta> X \<Longrightarrow> \<tau> \<Turnstile> \<upsilon> x \<Longrightarrow>
\<lfloor>\<lfloor>insert (x \<tau>) \<lceil>\<lceil>Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e (X \<tau>)\<rceil>\<rceil>\<rfloor>\<rfloor> \<in> {X. X = \<bottom> \<or> X = null \<or> (\<forall>x\<in>\<lceil>\<lceil>X\<rceil>\<rceil>. x \<noteq> \<bottom>)}"
apply(simp add: bot_option_def null_option_def)
by (metis (hide_lams, no_types) Set_inv_lemma foundation18' foundation5)
by (metis (opaque_lifting, no_types) Set_inv_lemma foundation18' foundation5)
have m : "\<And>\<tau>. (\<lambda>_. \<bottom>) = (\<lambda>_. invalid \<tau>)" by(rule ext, simp add:invalid_def)
@ -1893,10 +1893,10 @@ proof -
apply(drule OclSize_infinite)
apply(frule includes_def, drule includes_val, simp)
apply(subst OclSize_def, subst OclIncluding_finite_rep_set, assumption+)
apply (metis (hide_lams, no_types) invalid_def)
apply (metis (opaque_lifting, no_types) invalid_def)
apply(subst OclIf_false',
metis (hide_lams, no_types) defined5 defined6 defined_and_I defined_not_I
metis (opaque_lifting, no_types) defined5 defined6 defined_and_I defined_not_I
foundation1 foundation9)
apply(subst cp_OclSize, simp add: OclIncluding_includes0 cp_OclSize[symmetric])
(* *)
@ -1916,7 +1916,7 @@ proof -
apply(subst (1 2) m[of \<tau>], 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)
(* *)
apply(subst OclIf_false', metis (hide_lams, no_types) defined6 foundation1 foundation9
apply(subst OclIf_false', metis (opaque_lifting, no_types) defined6 foundation1 foundation9
OclExcluding_valid_args_valid'')
by (metis cp_OclSize foundation18' OclIncluding_valid_args_valid'' invalid_def OclSize_invalid)
qed
@ -1988,7 +1988,7 @@ lemma OclANY_singleton_exec[simp,code_unfold]:
apply(subst (1 2) cp_OclAnd,
subst (1 2) OclNotEmpty_including[where X = "Set{}", simplified mtSet_def])
apply(simp add: mtSet_defined[simplified mtSet_def])
apply(metis (hide_lams, no_types) finite.emptyI mtSet_def mtSet_rep_set)
apply(metis (opaque_lifting, no_types) finite.emptyI mtSet_def mtSet_rep_set)
apply(simp add: OclValid_def)
apply(simp add: OclIncluding_def)
apply(rule conjI)
@ -2287,6 +2287,8 @@ proof -
have inject : "inj (\<lambda>a \<tau>. a)"
by(rule inj_fun, simp)
interpret F_commute: comp_fun_commute "F"
by (fact F_commute)
show ?thesis
apply(subst (1 2) cp_OclIterate, subst OclIncluding_def, subst OclExcluding_def)
apply(case_tac "\<not> ((\<delta> S) \<tau> = true \<tau> \<and> (\<upsilon> a) \<tau> = true \<tau>)", simp add: invalid_def)
@ -2303,7 +2305,7 @@ proof -
apply(case_tac "\<not> ((\<upsilon> A) \<tau> = true \<tau>)", (simp add: F_valid_arg)+)
apply(rule impI,
subst Finite_Set.comp_fun_commute.fold_fun_left_comm[symmetric, OF F_commute],
subst F_commute.fold_fun_left_comm[symmetric],
rule remove_finite, simp)
apply(subst image_set_diff[OF inject], simp)
@ -2311,7 +2313,7 @@ proof -
F (\<lambda>\<tau>'. a \<tau>) (Finite_Set.fold F A ((\<lambda>a \<tau>. a) ` \<lceil>\<lceil>Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e (S \<tau>)\<rceil>\<rceil> - {\<lambda>\<tau>'. a \<tau>})) \<tau>")
apply(subst F_cp, simp)
by(subst Finite_Set.comp_fun_commute.fold_insert_remove[OF F_commute], simp+)
by(subst F_commute.fold_insert_remove, simp+)
qed
subsubsection\<open>Execution Rules on Select\<close>
@ -2338,14 +2340,14 @@ proof -
(f (P (\<lambda>_. y \<tau>)) \<tau> \<or> (\<exists>x\<in>\<lceil>\<lceil>Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e (X \<tau>)\<rceil>\<rceil>. f (P (\<lambda>_. x)) \<tau>))"
apply(simp add: OclIncluding_def OclValid_def)
apply(subst Abs_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e_inverse, simp, (rule disjI2)+)
by (metis (hide_lams, no_types) OclValid_def Set_inv_lemma foundation18',simp)
by (metis (opaque_lifting, no_types) OclValid_def Set_inv_lemma foundation18',simp)
have al_including : "\<And>f X y \<tau>. \<tau> \<Turnstile> \<delta> X \<Longrightarrow> \<tau> \<Turnstile> \<upsilon> y \<Longrightarrow>
(\<forall>x\<in>\<lceil>\<lceil>Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e (X->including\<^sub>S\<^sub>e\<^sub>t(y) \<tau>)\<rceil>\<rceil>. f (P (\<lambda>_. x)) \<tau>) =
(f (P (\<lambda>_. y \<tau>)) \<tau> \<and> (\<forall>x\<in>\<lceil>\<lceil>Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e (X \<tau>)\<rceil>\<rceil>. f (P (\<lambda>_. x)) \<tau>))"
apply(simp add: OclIncluding_def OclValid_def)
apply(subst Abs_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e_inverse, simp, (rule disjI2)+)
by (metis (hide_lams, no_types) OclValid_def Set_inv_lemma foundation18', simp)
by (metis (opaque_lifting, no_types) OclValid_def Set_inv_lemma foundation18', simp)
have ex_excluding1 : "\<And>f X y \<tau>. \<tau> \<Turnstile> \<delta> X \<Longrightarrow> \<tau> \<Turnstile> \<upsilon> y \<Longrightarrow> \<not> (f (P (\<lambda>_. y \<tau>)) \<tau>) \<Longrightarrow>
(\<exists>x\<in>\<lceil>\<lceil>Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e (X \<tau>)\<rceil>\<rceil>. f (P (\<lambda>_. x)) \<tau>) =
@ -2367,7 +2369,7 @@ proof -
if f (P (\<lambda>_. y \<tau>) \<tau>) then insert (y \<tau>) s else s)"
apply(simp add: OclIncluding_def OclValid_def)
apply(subst Abs_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e_inverse, simp, (rule disjI2)+)
apply (metis (hide_lams, no_types) OclValid_def Set_inv_lemma foundation18')
apply (metis (opaque_lifting, no_types) OclValid_def Set_inv_lemma foundation18')
by(simp add: Let_def, auto)
let ?OclSet = "\<lambda>S. \<lfloor>\<lfloor>S\<rfloor>\<rfloor> \<in> {X. X = \<bottom> \<or> X = null \<or> (\<forall>x\<in>\<lceil>\<lceil>X\<rceil>\<rceil>. x \<noteq> \<bottom>)}"
@ -2379,29 +2381,29 @@ proof -
have ins_in_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e : "\<And>\<tau>. (\<delta> X) \<tau> = true \<tau> \<Longrightarrow> (\<upsilon> y) \<tau> = true \<tau> \<Longrightarrow>
?OclSet (insert (y \<tau>) {x \<in> \<lceil>\<lceil>Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e (X \<tau>)\<rceil>\<rceil>. P (\<lambda>_. x) \<tau> \<noteq> false \<tau>})"
apply(simp, (rule disjI2)+)
by (metis (hide_lams, no_types) OclValid_def Set_inv_lemma foundation18')
by (metis (opaque_lifting, no_types) OclValid_def Set_inv_lemma foundation18')
have ins_in_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e' : "\<And>\<tau>. (\<delta> X) \<tau> = true \<tau> \<Longrightarrow> (\<upsilon> y) \<tau> = true \<tau> \<Longrightarrow>
?OclSet (insert (y \<tau>) {x \<in> \<lceil>\<lceil>Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e (X \<tau>)\<rceil>\<rceil>. x \<noteq> y \<tau> \<and> P (\<lambda>_. x) \<tau> \<noteq> false \<tau>})"
apply(simp, (rule disjI2)+)
by (metis (hide_lams, no_types) OclValid_def Set_inv_lemma foundation18')
by (metis (opaque_lifting, no_types) OclValid_def Set_inv_lemma foundation18')
have ins_in_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e'' : "\<And>\<tau>. (\<delta> X) \<tau> = true \<tau> \<Longrightarrow>
?OclSet {x \<in> \<lceil>\<lceil>Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e (X \<tau>)\<rceil>\<rceil>. P (\<lambda>_. x) \<tau> \<noteq> false \<tau>}"
apply(simp, (rule disjI2)+)
by (metis (hide_lams, no_types) OclValid_def Set_inv_lemma)
by (metis (opaque_lifting, no_types) OclValid_def Set_inv_lemma)
have ins_in_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e''' : "\<And>\<tau>. (\<delta> X) \<tau> = true \<tau> \<Longrightarrow>
?OclSet {x \<in> \<lceil>\<lceil>Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e (X \<tau>)\<rceil>\<rceil>. x \<noteq> y \<tau> \<and> P (\<lambda>_. x) \<tau> \<noteq> false \<tau>}"
apply(simp, (rule disjI2)+)
by(metis (hide_lams, no_types) OclValid_def Set_inv_lemma)
by(metis (opaque_lifting, no_types) OclValid_def Set_inv_lemma)
have if_same : "\<And>a b c d \<tau>. \<tau> \<Turnstile> \<delta> a \<Longrightarrow> b \<tau> = d \<tau> \<Longrightarrow> c \<tau> = d \<tau> \<Longrightarrow>
(if a then b else c endif) \<tau> = d \<tau>"
by(simp add: OclIf_def OclValid_def)
have invert_including : "\<And>P y \<tau>. P \<tau> = \<bottom> \<Longrightarrow> P->including\<^sub>S\<^sub>e\<^sub>t(y) \<tau> = \<bottom>"
by (metis (hide_lams, no_types) foundation16[THEN iffD1]
by (metis (opaque_lifting, no_types) foundation16[THEN iffD1]
foundation18' OclIncluding_valid_args_valid)
have exclude_defined : "\<And>\<tau>. \<tau> \<Turnstile> \<delta> X \<Longrightarrow>
@ -2491,7 +2493,7 @@ proof -
apply(case_tac "\<not> (\<tau> \<Turnstile> (\<upsilon> P y))")
apply(subgoal_tac "P y \<tau> \<noteq> false \<tau>")
prefer 2
apply (metis (hide_lams, no_types) foundation1 foundation18' valid4)
apply (metis (opaque_lifting, no_types) foundation1 foundation18' valid4)
apply(simp)
(* *)
apply(subst conj_comm, rule conjI)
@ -2681,12 +2683,12 @@ proof -
have notempty': "\<And>\<tau> X. \<tau> \<Turnstile> \<delta> X \<Longrightarrow> finite \<lceil>\<lceil>Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e (X \<tau>)\<rceil>\<rceil> \<Longrightarrow> not (X->isEmpty\<^sub>S\<^sub>e\<^sub>t()) \<tau> \<noteq> true \<tau> \<Longrightarrow>
X \<tau> = Set{} \<tau>"
apply(case_tac "X \<tau>", rename_tac X', simp add: mtSet_def Abs_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e_inject)
apply(erule disjE, metis (hide_lams, mono_tags) bot_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e_def bot_option_def foundation16)
apply(erule disjE, metis (hide_lams, no_types) bot_option_def
apply(erule disjE, metis (opaque_lifting, mono_tags) bot_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e_def bot_option_def foundation16)
apply(erule disjE, metis (opaque_lifting, no_types) bot_option_def
null_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e_def null_option_def foundation16[THEN iffD1])
apply(case_tac X', simp, metis (hide_lams, no_types) bot_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e_def foundation16[THEN iffD1])
apply(case_tac X', simp, metis (opaque_lifting, no_types) bot_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e_def foundation16[THEN iffD1])
apply(rename_tac X'', case_tac X'', simp)
apply (metis (hide_lams, no_types) foundation16[THEN iffD1] null_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e_def)
apply (metis (opaque_lifting, no_types) foundation16[THEN iffD1] null_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e_def)
apply(simp add: OclIsEmpty_def OclSize_def)
apply(subst (asm) cp_OclNot, subst (asm) cp_OclOr, subst (asm) StrictRefEq\<^sub>I\<^sub>n\<^sub>t\<^sub>e\<^sub>g\<^sub>e\<^sub>r.cp0,
subst (asm) cp_OclAnd, subst (asm) cp_OclNot)
@ -2725,7 +2727,7 @@ proof -
apply(frule notempty'[simplified OclValid_def],
(simp add: mtSet_def Abs_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e_inverse OclInt0_def false_def)+)
apply(drule notempty'[simplified OclValid_def], simp, simp)
apply (metis (hide_lams, no_types) empty_iff mtSet_rep_set)
apply (metis (opaque_lifting, no_types) empty_iff mtSet_rep_set)
(* *)
apply(frule B)
apply(subst (1 2 3 4) cp_OclIf, simp)
@ -2735,7 +2737,7 @@ proof -
apply(simp add: OclNotEmpty_def OclIsEmpty_def)
apply(subgoal_tac "X->size\<^sub>S\<^sub>e\<^sub>t() \<tau> = \<bottom>")
prefer 2
apply (metis (hide_lams, no_types) OclSize_def)
apply (metis (opaque_lifting, no_types) OclSize_def)
apply(subst (asm) cp_OclNot, subst (asm) cp_OclOr, subst (asm) StrictRefEq\<^sub>I\<^sub>n\<^sub>t\<^sub>e\<^sub>g\<^sub>e\<^sub>r.cp0,
subst (asm) cp_OclAnd, subst (asm) cp_OclNot)
apply(simp add: OclValid_def foundation20[simplified OclValid_def]
@ -2929,9 +2931,9 @@ lemma OclForall_iterate:
assumes S_finite: "finite \<lceil>\<lceil>Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e (S \<tau>)\<rceil>\<rceil>"
shows "S->forAll\<^sub>S\<^sub>e\<^sub>t(x | P x) \<tau> = (S->iterate\<^sub>S\<^sub>e\<^sub>t(x; acc = true | acc and P x)) \<tau>"
proof -
have and_comm : "comp_fun_commute (\<lambda>x acc. acc and P x)"
interpret and_comm: comp_fun_commute "(\<lambda>x acc. acc and P x)"
apply(simp add: comp_fun_commute_def comp_def)
by (metis OclAnd_assoc OclAnd_commute)
by (metis OclAnd_assoc OclAnd_commute)
have ex_insert : "\<And>x F P. (\<exists>x\<in>insert x F. P x) = (P x \<or> (\<exists>x\<in>F. P x))"
by (metis insert_iff)
@ -2961,13 +2963,13 @@ proof -
apply(rule finite_ne_induct[OF S_finite], simp)
(* *)
apply(simp only: image_insert)
apply(subst comp_fun_commute.fold_insert[OF and_comm], simp)
apply(subst and_comm.fold_insert, simp)
apply (metis empty_iff image_empty)
apply(simp add: invalid_def)
apply (metis bot_fun_def destruct_ocl null_fun_def)
(* *)
apply(simp only: image_insert)
apply(subst comp_fun_commute.fold_insert[OF and_comm], simp)
apply(subst and_comm.fold_insert, simp)
apply (metis (mono_tags) imageE)
(* *)

2
Featherweight_OCL/document/root.tex
View File

@ -1,8 +1,6 @@
\documentclass[fontsize=10pt,DIV12,paper=a4,open=right,twoside,abstract=true]{scrreprt}
\usepackage{fixltx2e}
\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage{lmodern}
\usepackage{textcomp}
\usepackage[english]{babel}
\usepackage{isabelle}