diff --git a/Featherweight_OCL/UML_PropertyProfiles.thy b/Featherweight_OCL/UML_PropertyProfiles.thy index 8ca00d3..f5dedce 100644 --- a/Featherweight_OCL/UML_PropertyProfiles.thy +++ b/Featherweight_OCL/UML_PropertyProfiles.thy @@ -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 diff --git a/Featherweight_OCL/UML_State.thy b/Featherweight_OCL/UML_State.thy index cee9795..bfdfaf6 100644 --- a/Featherweight_OCL/UML_State.thy +++ b/Featherweight_OCL/UML_State.thy @@ -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 = "\x. x \ 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 (\, \'))" 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 (\x. (\ \ \ (f p x))) s_set" apply(rule rev_induct[where P = "\s_set. \ \ \ foldl UML_Sequence.OclIncluding Sequence{} (List.map (f p) s_set) \ list_all (\x. \ \ \ 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 (\x. (\ \ \ (f p x))) s_set" apply(rule rev_induct[where P = "\s_set. \ \ \ foldl UML_Set.OclIncluding Set{} (List.map (f p) s_set) \ list_all (\x. \ \ \ 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 "(\x. f x \) ` set s_set = {z'} \ s_set = a # list \ \e. List.member s_set e \ z' = f e \" 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+ diff --git a/Featherweight_OCL/collection_types/UML_Bag.thy b/Featherweight_OCL/collection_types/UML_Bag.thy index 50edd48..f618271 100644 --- a/Featherweight_OCL/collection_types/UML_Bag.thy +++ b/Featherweight_OCL/collection_types/UML_Bag.thy @@ -640,7 +640,7 @@ text\OclIncluding\ lemma OclIncluding_valid_args_valid: "(\ \ \(X->including\<^sub>B\<^sub>a\<^sub>g(x))) = ((\ \(\ X)) \ (\ \(\ 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]: "\(X->including\<^sub>B\<^sub>a\<^sub>g(x)) = ((\ X) and (\ x))" @@ -721,7 +721,7 @@ lemma OclIsEmpty_defined_args_valid:"\ \ \ (X->isEmpty\<^ 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) -by (metis (hide_lams, no_types) +by (metis (opaque_lifting, no_types) bot_fun_def OclValid_def defined_def foundation2 invalid_def) lemma "\ \ \ (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\OclNotEmpty\ lemma OclNotEmpty_defined_args_valid:"\ \ \ (X->notEmpty\<^sub>B\<^sub>a\<^sub>g()) \ \ \ \ 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 "\ \ \ (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: "\ \ \ X \ \ finite (Rep_Bag_base X \) \ \ \ \ \ (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 "(\ X) \ = true \") 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, diff --git a/Featherweight_OCL/collection_types/UML_Set.thy b/Featherweight_OCL/collection_types/UML_Set.thy index 9fd6616..803b422 100644 --- a/Featherweight_OCL/collection_types/UML_Set.thy +++ b/Featherweight_OCL/collection_types/UML_Set.thy @@ -682,7 +682,7 @@ text\OclIncluding\ lemma OclIncluding_valid_args_valid: "(\ \ \(X->including\<^sub>S\<^sub>e\<^sub>t(x))) = ((\ \(\ X)) \ (\ \(\ 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]: "\(X->including\<^sub>S\<^sub>e\<^sub>t(x)) = ((\ X) and (\ x))" @@ -764,7 +764,7 @@ lemma OclIsEmpty_defined_args_valid:"\ \ \ (X->isEmpty\<^ 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) -by (metis (hide_lams, no_types) +by (metis (opaque_lifting, no_types) bot_fun_def OclValid_def defined_def foundation2 invalid_def) lemma "\ \ \ (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\OclNotEmpty\ lemma OclNotEmpty_defined_args_valid:"\ \ \ (X->notEmpty\<^sub>S\<^sub>e\<^sub>t()) \ \ \ \ 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 "\ \ \ (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: "\ \ \ X \ \ finite \\Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e (X \)\\ \ \ \ \ \ (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 "(\ X) \ = true \") 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 = "\S. \\S\\ \ {X. X = \ \ X = null \ (\x\\\X\\. x \ \)}" have diff_in_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e : "?OclSet (\\Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e (X \)\\ - {x \})" 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: "\ \ \ X \ \ \ \ x \ \\insert (x \) \\Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e (X \)\\\\ \ {X. X = \ \ X = null \ (\x\\\X\\. x \ \)}" 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 : "\\. (\_. \) = (\_. invalid \)" 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 \], 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 (\a \. 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 "\ ((\ S) \ = true \ \ (\ a) \ = true \)", simp add: invalid_def) @@ -2303,7 +2305,7 @@ proof - apply(case_tac "\ ((\ A) \ = true \)", (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 (\\'. a \) (Finite_Set.fold F A ((\a \. a) ` \\Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e (S \)\\ - {\\'. a \})) \") 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\Execution Rules on Select\ @@ -2338,14 +2340,14 @@ proof - (f (P (\_. y \)) \ \ (\x\\\Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e (X \)\\. f (P (\_. x)) \))" 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 : "\f X y \. \ \ \ X \ \ \ \ y \ (\x\\\Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e (X->including\<^sub>S\<^sub>e\<^sub>t(y) \)\\. f (P (\_. x)) \) = (f (P (\_. y \)) \ \ (\x\\\Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e (X \)\\. f (P (\_. x)) \))" 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 : "\f X y \. \ \ \ X \ \ \ \ y \ \ (f (P (\_. y \)) \) \ (\x\\\Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e (X \)\\. f (P (\_. x)) \) = @@ -2367,7 +2369,7 @@ proof - if f (P (\_. y \) \) then insert (y \) 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 = "\S. \\S\\ \ {X. X = \ \ X = null \ (\x\\\X\\. x \ \)}" @@ -2379,29 +2381,29 @@ proof - have ins_in_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e : "\\. (\ X) \ = true \ \ (\ y) \ = true \ \ ?OclSet (insert (y \) {x \ \\Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e (X \)\\. P (\_. x) \ \ false \})" 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' : "\\. (\ X) \ = true \ \ (\ y) \ = true \ \ ?OclSet (insert (y \) {x \ \\Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e (X \)\\. x \ y \ \ P (\_. x) \ \ false \})" 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'' : "\\. (\ X) \ = true \ \ ?OclSet {x \ \\Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e (X \)\\. P (\_. x) \ \ false \}" 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''' : "\\. (\ X) \ = true \ \ ?OclSet {x \ \\Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e (X \)\\. x \ y \ \ P (\_. x) \ \ false \}" 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 : "\a b c d \. \ \ \ a \ b \ = d \ \ c \ = d \ \ (if a then b else c endif) \ = d \" by(simp add: OclIf_def OclValid_def) have invert_including : "\P y \. P \ = \ \ P->including\<^sub>S\<^sub>e\<^sub>t(y) \ = \" - 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 : "\\. \ \ \ X \ @@ -2491,7 +2493,7 @@ proof - apply(case_tac "\ (\ \ (\ P y))") apply(subgoal_tac "P y \ \ false \") 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': "\\ X. \ \ \ X \ finite \\Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e (X \)\\ \ not (X->isEmpty\<^sub>S\<^sub>e\<^sub>t()) \ \ true \ \ X \ = Set{} \" apply(case_tac "X \", 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() \ = \") 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 \\Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e (S \)\\" shows "S->forAll\<^sub>S\<^sub>e\<^sub>t(x | P x) \ = (S->iterate\<^sub>S\<^sub>e\<^sub>t(x; acc = true | acc and P x)) \" proof - - have and_comm : "comp_fun_commute (\x acc. acc and P x)" + interpret and_comm: comp_fun_commute "(\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 : "\x F P. (\x\insert x F. P x) = (P x \ (\x\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) (* *) diff --git a/Featherweight_OCL/document/root.tex b/Featherweight_OCL/document/root.tex index 9ea4bc3..05d69cb 100644 --- a/Featherweight_OCL/document/root.tex +++ b/Featherweight_OCL/document/root.tex @@ -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}