diff --git a/Alphabet_Scene_Spaces.thy b/Alphabet_Scene_Spaces.thy index a351cb1..3e78335 100644 --- a/Alphabet_Scene_Spaces.thy +++ b/Alphabet_Scene_Spaces.thy @@ -125,11 +125,10 @@ lemmas scene_space_lemmas = lens_indep_left_ext lens_indep_right_ext method basis_lens uses defs = - (rule basis_lens_intro, simp_all add: scene_space_defs alpha_scene_space_def alpha_scene_space'_def scene_space_lemmas) + (auto intro!: basis_lensI simp: scene_space_defs alpha_scene_space_def alpha_scene_space'_def scene_space_lemmas) method composite_lens = - (rule composite_lens.intro, simp, rule composite_lens_axioms.intro - ,simp add: scene_space_defs alpha_scene_space_def alpha_scene_space'_def scene_space_lemmas image_comp) + (auto intro!: composite_lensI simp add: scene_space_defs alpha_scene_space_def alpha_scene_space'_def scene_space_lemmas image_comp) method more_frame = ((simp add: frame_scene_top frame_scene_foldr)? diff --git a/Frames.thy b/Frames.thy index ab08f0d..fd5f1be 100644 --- a/Frames.thy +++ b/Frames.thy @@ -18,7 +18,7 @@ lemma UNIV_frame_scene_space: "UNIV = mk_frame ` scene_space" by (metis of_frame of_frame_inverse UNIV_eq_I imageI) lemma idem_scene_frame [simp]: "idem_scene \A\\<^sub>F" - by (simp add: idem_scene_space of_frame) + by (simp add: of_frame) lemma compat_frames [simp]: "\A\\<^sub>F ##\<^sub>S \B\\<^sub>F" by (simp add: of_frame scene_space_compat) @@ -342,7 +342,7 @@ lemma frame_equiv_sym [simp]: "s\<^sub>1 \\<^sub>F s\<^sub>2 on a \ s\<^sub>1 \\<^sub>F s\<^sub>2 on a; s\<^sub>2 \\<^sub>F s\<^sub>3 on b \ \ s\<^sub>1 \\<^sub>F s\<^sub>3 on (a \\<^sub>F b)" -proof (transfer, simp add: scene_override_inter scene_space_compat scene_space_uminus) +proof (transfer) fix a b :: "'a scene" and s\<^sub>1 s\<^sub>2 s\<^sub>3 :: "'a" assume a:"a \ scene_space" and b: "b \ scene_space" and @@ -357,20 +357,19 @@ proof (transfer, simp add: scene_override_inter scene_space_compat scene_space_u have "s\<^sub>1 \\<^sub>S (s\<^sub>1 \\<^sub>S s\<^sub>3 on a) on b = s\<^sub>1 \\<^sub>S (s\<^sub>1 \\<^sub>S (s\<^sub>3 \\<^sub>S s\<^sub>2 on b) on a) on b" using "1" by auto also from 1 2 3 a b have "... = s\<^sub>1 \\<^sub>S (s\<^sub>1 \\<^sub>S s\<^sub>2 on a) on b" - by (metis scene_inter_commute scene_override_inter scene_override_overshadow_right scene_space_compat scene_space_uminus) + by (smt (verit) scene_inter_commute scene_override_inter scene_override_overshadow_right scene_space_compat scene_space_uminus) also have "... = s\<^sub>1 \\<^sub>S s\<^sub>1 on b" using 2 by auto also have "... = s\<^sub>1" - by (simp add: b idem_scene_space) + by (simp add: b) finally show "s\<^sub>1 \\<^sub>S s\<^sub>3 on a \\<^sub>S b" - by (simp add: a b scene_equiv_def scene_override_inter scene_space_compat scene_space_uminus) + by (simp add: a b scene_equiv_def scene_override_inter scene_space_compat) qed lemma frame_equiv_trans: "\ s\<^sub>1 \\<^sub>F s\<^sub>2 on a; s\<^sub>2 \\<^sub>F s\<^sub>3 on a \ \ s\<^sub>1 \\<^sub>F s\<^sub>3 on a" by (transfer) (metis scene_equiv_def scene_override_overshadow_right) - lemma put_eq_ebasis_lens_notin: "\ ebasis_lens x; s\<^sub>1 \\<^sub>F s\<^sub>2 on A; x \\<^sub>F A \ \ put\<^bsub>x\<^esub> s\<^sub>1 v \\<^sub>F put\<^bsub>x\<^esub> s\<^sub>2 v on A" by (simp add: basis_lens_not_member_indep, transfer) diff --git a/Lens_Algebra.thy b/Lens_Algebra.thy index 9062987..71d180b 100644 --- a/Lens_Algebra.thy +++ b/Lens_Algebra.thy @@ -123,7 +123,7 @@ lemma id_vwb_lens [simp]: "vwb_lens 1\<^sub>L" lemma unit_vwb_lens [simp]: "vwb_lens 0\<^sub>L" by (unfold_locales, simp_all add: zero_lens_def) -lemma comp_vwb_lens: "\ vwb_lens x; vwb_lens y \ \ vwb_lens (x ;\<^sub>L y)" +lemma comp_vwb_lens [intro]: "\ vwb_lens x; vwb_lens y \ \ vwb_lens (x ;\<^sub>L y)" by (unfold_locales, simp_all add: lens_comp_def weak_lens.put_closure) lemma unit_ief_lens: "ief_lens 0\<^sub>L" diff --git a/Lens_Order.thy b/Lens_Order.thy index be9bdc5..576f8a3 100644 --- a/Lens_Order.thy +++ b/Lens_Order.thy @@ -30,23 +30,18 @@ text \Sublens is a preorder as the following two theorems show.\ lemma sublens_refl [simp]: "X \\<^sub>L X" - using id_vwb_lens sublens_def by fastforce + unfolding sublens_def by (auto intro: exI[where x="1\<^sub>L"]) lemma sublens_trans [trans]: "\ X \\<^sub>L Y; Y \\<^sub>L Z \ \ X \\<^sub>L Z" - apply (auto simp add: sublens_def lens_comp_assoc) - apply (rename_tac Z\<^sub>1 Z\<^sub>2) - apply (rule_tac x="Z\<^sub>1 ;\<^sub>L Z\<^sub>2" in exI) - apply (simp add: lens_comp_assoc) - using comp_vwb_lens apply blast -done + by (auto simp add: sublens_def lens_comp_assoc) text \Sublens has a least element -- @{text "0\<^sub>L"} -- and a greatest element -- @{text "1\<^sub>L"}. Intuitively, this shows that sublens orders how large a portion of the source type a particular lens views, with @{text "0\<^sub>L"} observing the least, and @{text "1\<^sub>L"} observing the most.\ lemma sublens_least: "wb_lens X \ 0\<^sub>L \\<^sub>L X" - using sublens_def unit_vwb_lens by fastforce + unfolding sublens_def by (auto intro: exI[where x="0\<^sub>L"]) lemma sublens_greatest: "vwb_lens X \ X \\<^sub>L 1\<^sub>L" by (simp add: sublens_def) @@ -97,7 +92,7 @@ text \Using our preorder, we can also derive an equivalence on lenses as f definition lens_equiv :: "('a \ 'c) \ ('b \ 'c) \ bool" (infix "\\<^sub>L" 51) where [lens_defs]: "lens_equiv X Y = (X \\<^sub>L Y \ Y \\<^sub>L X)" -lemma lens_equivI [intro]: +lemma lens_equivI [intro?]: "\ X \\<^sub>L Y; Y \\<^sub>L X \ \ X \\<^sub>L Y" by (simp add: lens_equiv_def) @@ -283,7 +278,7 @@ lemma lens_plus_left_unit: "0\<^sub>L +\<^sub>L X \\<^sub>L X" by (simp add: lens_equivI lens_unit_plus_sublens_1 lens_unit_prod_sublens_2) lemma lens_plus_right_unit: "X +\<^sub>L 0\<^sub>L \\<^sub>L X" - using lens_equiv_trans lens_indep_sym lens_plus_comm lens_plus_left_unit zero_lens_indep by blast + using lens_equiv_trans lens_plus_comm lens_plus_left_unit zero_lens_indep' by blast text \We can also show that both sublens and equivalence are congruences with respect to lens plus and lens product.\ @@ -453,25 +448,12 @@ text \Consequently, if composition of two lenses $X$ and $Y$ yields @{text lemma bij_lens_via_comp_id_left: "\ wb_lens X; wb_lens Y; X ;\<^sub>L Y = 1\<^sub>L \ \ bij_lens X" - apply (cases Y) - apply (cases X) - apply (auto simp add: lens_comp_def comp_def id_lens_def fun_eq_iff) - apply (unfold_locales) - apply (simp_all) - using vwb_lens_wb wb_lens_weak weak_lens.put_get apply fastforce - apply (metis select_convs(1) select_convs(2) wb_lens_weak weak_lens.put_get) -done + by (smt (z3) bij_lens.intro bij_lens_axioms.intro id_lens_def lens_comp_def lens_comp_right_id + select_convs(1,2) wb_lens_weak weak_lens.put_get) lemma bij_lens_via_comp_id_right: "\ wb_lens X; wb_lens Y; X ;\<^sub>L Y = 1\<^sub>L \ \ bij_lens Y" - apply (cases Y) - apply (cases X) - apply (auto simp add: lens_comp_def comp_def id_lens_def fun_eq_iff) - apply (unfold_locales) - apply (simp_all) - using vwb_lens_wb wb_lens_weak weak_lens.put_get apply fastforce - apply (metis select_convs(1) select_convs(2) wb_lens_weak weak_lens.put_get) -done + by (metis bij_lens_via_comp_id_left lens_comp_assoc lens_comp_right_id lens_id_unique wb_lens_weak) text \Importantly, an equivalence between two lenses can be demonstrated by showing that one lens can be converted to the other by application of a suitable bijective lens $Z$. This $Z$ lens @@ -480,13 +462,7 @@ text \Importantly, an equivalence between two lenses can be demonstrated b lemma lens_equiv_via_bij: assumes "bij_lens Z" "X = Z ;\<^sub>L Y" shows "X \\<^sub>L Y" - using assms - apply (auto simp add: lens_equiv_def sublens_def) - using bij_lens_vwb apply blast - apply (rule_tac x="lens_inv Z" in exI) - apply (auto simp add: lens_comp_assoc bij_lens_inv_left) - using bij_lens_vwb lens_inv_bij apply blast -done + by (metis assms(1,2) bij_lens_equiv_id lens_comp_cong_1 lens_comp_left_id) text \Indeed, we actually have a stronger result than this -- the equivalent lenses are precisely those than can be converted to one another through a suitable bijective lens. Bijective lenses @@ -495,20 +471,12 @@ text \Indeed, we actually have a stronger result than this -- the equivale lemma lens_equiv_iff_bij: assumes "weak_lens Y" shows "X \\<^sub>L Y \ (\ Z. bij_lens Z \ X = Z ;\<^sub>L Y)" - apply (rule iffI) - apply (auto simp add: lens_equiv_def sublens_def lens_id_unique)[1] - apply (rename_tac Z\<^sub>1 Z\<^sub>2) - apply (rule_tac x="Z\<^sub>1" in exI) - apply (simp) - apply (subgoal_tac "Z\<^sub>2 ;\<^sub>L Z\<^sub>1 = 1\<^sub>L") - apply (meson bij_lens_via_comp_id_right vwb_lens_wb) - apply (metis assms lens_comp_assoc lens_id_unique) - using lens_equiv_via_bij apply blast -done + by (smt (verit, best) assms bij_lens_equiv_id lens_comp_assoc lens_equiv_def lens_equiv_via_bij + lens_id_unique sublens_def) lemma pbij_plus_commute: "\ a \ b; mwb_lens a; mwb_lens b; pbij_lens (b +\<^sub>L a) \ \ pbij_lens (a +\<^sub>L b)" - apply (unfold_locales, simp_all add:lens_defs lens_indep_sym prod.case_eq_if) + apply (unfold_locales, simp_all add: lens_defs lens_indep_sym prod.case_eq_if) using lens_indep.lens_put_comm pbij_lens.put_det apply fastforce done diff --git a/Scene_Spaces.thy b/Scene_Spaces.thy index 160d8bf..0f842cb 100644 --- a/Scene_Spaces.thy +++ b/Scene_Spaces.thy @@ -101,10 +101,24 @@ using assms proof (induct xs arbitrary: ys) by simp next case (Cons a xs) - hence ys: "set ys = insert a (set (removeAll a ys))" - by (auto) + consider (a_in) "a \ set xs" | (a_notin) "a \ set xs" + by blast then show ?case - by (metis (no_types, lifting) Cons.hyps Cons.prems(1) Cons.prems(2) Diff_insert_absorb foldr_scene_union_removeAll insertCI insert_absorb list.simps(15) pairwise_insert set_removeAll) + proof cases + case a_in + then show ?thesis + by (metis Cons remdups.simps(2) set_remdups) + next + case a_notin + then have *: "\\<^sub>S xs = \\<^sub>S (removeAll a ys)" + using Cons(2,3) by (auto intro!: Cons(1) simp: pairwise_insert) + then have "\\<^sub>S (a#xs) = (\\<^sub>S xs) \\<^sub>S a" + by (simp add: scene_union_commute) + also have "... = \\<^sub>S (removeAll a ys) \\<^sub>S a" + using * by simp + finally show ?thesis + using foldr_scene_union_removeAll Cons(2,3) by auto + qed qed lemma foldr_scene_removeAll: @@ -224,7 +238,7 @@ bot_scene_space [intro]: "\\<^sub>S \ scene_space" | Vars_scene_space [intro]: "x \ set Vars \ x \ scene_space" | union_scene_space [intro]: "\ x \ scene_space; y \ scene_space \ \ x \\<^sub>S y \ scene_space" -lemma idem_scene_space: "a \ scene_space \ idem_scene a" +lemma idem_scene_space [intro, simp]: "a \ scene_space \ idem_scene a" by (induct rule: scene_space.induct) auto lemma set_Vars_scene_space [simp]: "set Vars \ scene_space" @@ -263,7 +277,7 @@ next using scene_union_pres_compat by blast qed -lemma scene_space_compat: "\ a \ scene_space; b \ scene_space \ \ a ##\<^sub>S b" +lemma scene_space_compat [intro]: "\ a \ scene_space; b \ scene_space \ \ a ##\<^sub>S b" proof (induct rule: scene_space.induct) case bot_scene_space then show ?case @@ -372,12 +386,12 @@ proof (rule scene_union_indep_uniq[where Z="foldr (\\<^sub>S) xs \idem_scene (- \\<^sub>S xs)\ local.span_Vars scene_span_def scene_union_compl uminus_scene_twice) qed -lemma scene_space_uminus: "\ a \ scene_space \ \ - a \ scene_space" +lemma scene_space_uminus [intro, simp]: "\ a \ scene_space \ \ - a \ scene_space" by (auto simp add: scene_space_vars_decomp_iff uminus_vars_other_vars) (metis filter_is_subset) -lemma scene_space_inter: "\ a \ scene_space; b \ scene_space \ \ a \\<^sub>S b \ scene_space" - by (simp add: inf_scene_def scene_space.union_scene_space scene_space_uminus) +lemma scene_space_inter [intro]: "\ a \ scene_space; b \ scene_space \ \ a \\<^sub>S b \ scene_space" + by (simp add: inf_scene_def scene_space.union_scene_space) lemma scene_union_foldr_remove_element: assumes "set xs \ set Vars" @@ -595,7 +609,7 @@ qed lemma scene_union_inter_minus: assumes "a \ scene_space" "b \ scene_space" shows "a \\<^sub>S (b \\<^sub>S - a) = a \\<^sub>S b" - by (metis assms(1) assms(2) bot_idem_scene idem_scene_space idem_scene_uminus local.scene_union_inter_distrib scene_demorgan1 scene_space_uminus scene_union_compl scene_union_unit(1) uminus_scene_twice) + by (simp add: assms scene_union_inter_distrib scene_union_compl) lemma scene_union_foldr_minus_element: assumes "a \ scene_space" "set xs \ scene_space" @@ -773,31 +787,31 @@ abbreviation (input) ebasis_lens :: "('a::two \ 's::scene_space) lemma basis_then_var [simp]: "basis_lens x \ var_lens x" using basis_lens.lens_in_basis basis_lens_def var_lens_axioms_def var_lens_def by blast -lemma basis_lens_intro: "\ vwb_lens x; \x\\<^sub>\ \ set Vars \ \ basis_lens x" +lemma basis_lensI: "\ vwb_lens x; \x\\<^sub>\ \ set Vars \ \ basis_lens x" using basis_lens.intro basis_lens_axioms.intro by blast -subsection \ Composite lenses \ +lemma basis_lensE [elim]: + assumes "basis_lens x" + obtains "vwb_lens x" "\x\\<^sub>\ \ set Vars" + by (simp add: assms) +subsection \ Composite lenses \ locale composite_lens = vwb_lens + - assumes comp_in_Vars: "(\ a. a ;\<^sub>S x) ` set Vars \ set Vars" + assumes comp_in_Vars: "\a. a \ set Vars \ a ;\<^sub>S x \ set Vars" begin -lemma Vars_closed_comp: "a \ set Vars \ a ;\<^sub>S x \ set Vars" - using comp_in_Vars by blast - -lemma scene_space_closed_comp: +lemma scene_space_closed_comp [intro]: assumes "a \ scene_space" shows "a ;\<^sub>S x \ scene_space" proof - - obtain xs where xs: "a = \\<^sub>S xs" "set xs \ set Vars" - using assms scene_space_vars_decomp by blast - have "(\\<^sub>S xs) ;\<^sub>S x = \\<^sub>S (map (\ a. a ;\<^sub>S x) xs)" - by (metis foldr_compat_dist pairwise_subset scene_space_compats xs(2)) - also have "... \ scene_space" - by (auto simp add: scene_space_vars_decomp_iff) - (metis comp_in_Vars image_Un le_iff_sup le_supE list.set_map xs(2)) - finally show ?thesis - by (simp add: xs) + obtain xs where xs: "set xs \ set Vars" "a = \\<^sub>S xs" + using scene_space_vars_decomp_iff assms by blast + then have "b \ set xs \ b ;\<^sub>S x \ scene_space" for b + using comp_in_Vars by blast + then have "\\<^sub>S (map (\y. y ;\<^sub>S x) xs) \ scene_space" + by (auto intro!: scene_space_foldr) + then show "a ;\<^sub>S x \ scene_space" + by (simp add: xs foldr_compat_dist pairwise_compat_Vars_subset) qed sublocale var_lens @@ -805,9 +819,18 @@ proof show "\x\\<^sub>\ \ scene_space" by (metis scene_comp_top_scene scene_space_closed_comp top_scene_space vwb_lens_axioms) qed - end +lemma composite_lensI: + assumes "vwb_lens x" "\a. a \ set Vars \ a ;\<^sub>S x \ set Vars" + shows "composite_lens x" + by (intro composite_lens.intro composite_lens_axioms.intro; simp add: assms) + +lemma composite_lensE [elim]: + assumes "composite_lens x" + shows "((\a. a \ set Vars \ a ;\<^sub>S x \ set Vars) \ vwb_lens x \ P) \ P" + using assms composite_lens.axioms(1) composite_lens.comp_in_Vars by blast + lemma composite_implies_var_lens [simp]: "composite_lens x \ var_lens x" by (metis composite_lens.axioms(1) composite_lens.scene_space_closed_comp scene_comp_top_scene top_scene_space var_lens_axioms.intro var_lens_def) @@ -816,18 +839,18 @@ text \ The extension of any lens in the scene space remains in the scene s lemma composite_lens_comp [simp]: "\ composite_lens a; var_lens x \ \ var_lens (x ;\<^sub>L a)" - by (metis comp_vwb_lens composite_lens.scene_space_closed_comp composite_lens_def lens_scene_comp var_lens_axioms_def var_lens_def) + by (metis comp_vwb_lens composite_lens.scene_space_closed_comp composite_lens_def lens_scene_comp + var_lens_axioms_def var_lens_def) lemma comp_composite_lens [simp]: "\ composite_lens a; composite_lens x \ \ composite_lens (x ;\<^sub>L a)" - by (auto intro!: composite_lens.intro simp add: composite_lens_axioms_def) - (metis composite_lens.Vars_closed_comp composite_lens.axioms(1) scene_comp_assoc) + by (metis comp_vwb_lens composite_lens_axioms_def composite_lens_def scene_comp_assoc) text \ A basis lens within a composite lens remains a basis lens (i.e. it remains atomic) \ lemma composite_lens_basis_comp [simp]: "\ composite_lens a; basis_lens x \ \ basis_lens (x ;\<^sub>L a)" - by (metis basis_lens.lens_in_basis basis_lens_def basis_lens_intro comp_vwb_lens composite_lens.Vars_closed_comp composite_lens_def lens_scene_comp) + using lens_scene_comp by (force intro: basis_lensI) lemma id_composite_lens: "composite_lens 1\<^sub>L" by (force intro: composite_lens.intro composite_lens_axioms.intro) @@ -836,6 +859,7 @@ lemma fst_composite_lens: "composite_lens fst\<^sub>L" by (rule composite_lens.intro, simp add: fst_vwb_lens, rule composite_lens_axioms.intro, simp add: Vars_prod_def) lemma snd_composite_lens: "composite_lens snd\<^sub>L" - by (rule composite_lens.intro, simp add: snd_vwb_lens, rule composite_lens_axioms.intro, simp add: Vars_prod_def) + by (intro composite_lens.intro composite_lens_axioms.intro; + simp add: snd_vwb_lens Vars_prod_def) end \ No newline at end of file diff --git a/Scenes.thy b/Scenes.thy index f960375..ce9c339 100644 --- a/Scenes.thy +++ b/Scenes.thy @@ -60,22 +60,14 @@ lemma equiv_region: "equiv UNIV (region X)" done lemma equiv_coregion: "equiv UNIV (coregion X)" - apply (transfer) - apply (rule equivI) - apply (rule refl_onI) - apply (auto) - apply (rule symI) - apply (auto) - apply (rule transI) - apply (auto) - done + by (transfer) (auto intro!: equivI refl_onI symI transI) lemma region_coregion_Id: "idem_scene X \ region X \ coregion X = Id" by (transfer, auto, metis idem_overrider.ovr_idem) lemma state_eq_iff: "idem_scene S \ x = y \ (x, y) \ region S \ (x, y) \ coregion S" - by (metis IntE IntI pair_in_Id_conv region_coregion_Id) + using region_coregion_Id by auto lift_definition scene_override :: "'a \ 'a \ ('a scene) \ 'a" ("_ \\<^sub>S _ on _" [95,0,96] 95) is "\ s\<^sub>1 s\<^sub>2 F. F s\<^sub>1 s\<^sub>2" . @@ -221,6 +213,9 @@ lemma scene_equiv_sym [simp]: "idem_scene a \ s\<^sub>1 \\<^sub>S \\<^sub>S = X" "\\<^sub>S \\<^sub>S X = X" by (transfer, simp)+ +lemma scene_inter_unit [simp]: "X \\<^sub>S \\<^sub>S = X" "\\<^sub>S \\<^sub>S X = X" + by (simp_all add: inf_scene_def uminus_scene_twice) + lemma scene_indep_bot [simp]: "X \\<^sub>S \\<^sub>S" by (transfer, simp) @@ -283,7 +278,7 @@ lemma scene_union_indep_uniq: lemma scene_union_idem: "X \\<^sub>S X = X" by (transfer, simp) -lemma scene_union_compl: "idem_scene X \ X \\<^sub>S - X = \\<^sub>S" +lemma scene_union_compl [intro]: "idem_scene X \ X \\<^sub>S - X = \\<^sub>S" by (transfer, auto) lemma scene_inter_idem: "X \\<^sub>S X = X"