Tidy up Scenes and Scene_Spaces and improve automation

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)?

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 \<lbrakk>A\<rbrakk>\<^sub>F"
-  by (simp add: idem_scene_space of_frame)
+  by (simp add: of_frame)
 
 lemma compat_frames [simp]: "\<lbrakk>A\<rbrakk>\<^sub>F ##\<^sub>S \<lbrakk>B\<rbrakk>\<^sub>F"
   by (simp add: of_frame scene_space_compat)
@@ -342,7 +342,7 @@ lemma frame_equiv_sym [simp]: "s\<^sub>1 \<approx>\<^sub>F s\<^sub>2 on a \<Long
      (metis idem_scene_space scene_override_idem scene_override_overshadow_right)
 
 lemma frame_equiv_trans_gen [simp]: "\<lbrakk> s\<^sub>1 \<approx>\<^sub>F s\<^sub>2 on a; s\<^sub>2 \<approx>\<^sub>F s\<^sub>3 on b \<rbrakk> \<Longrightarrow> s\<^sub>1 \<approx>\<^sub>F s\<^sub>3 on (a \<inter>\<^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 \<in> scene_space" and b: "b \<in> scene_space" and
@@ -357,20 +357,19 @@ proof (transfer, simp add: scene_override_inter scene_space_compat scene_space_u
   have "s\<^sub>1 \<oplus>\<^sub>S (s\<^sub>1 \<oplus>\<^sub>S s\<^sub>3 on a) on b = s\<^sub>1 \<oplus>\<^sub>S (s\<^sub>1 \<oplus>\<^sub>S (s\<^sub>3 \<oplus>\<^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 \<oplus>\<^sub>S (s\<^sub>1 \<oplus>\<^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 \<oplus>\<^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 \<approx>\<^sub>S s\<^sub>3 on a \<sqinter>\<^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: "\<lbrakk> s\<^sub>1 \<approx>\<^sub>F s\<^sub>2 on a; s\<^sub>2 \<approx>\<^sub>F s\<^sub>3 on a \<rbrakk> \<Longrightarrow> s\<^sub>1 \<approx>\<^sub>F s\<^sub>3 on a"
   by (transfer)
      (metis scene_equiv_def scene_override_overshadow_right)
 
-
 lemma put_eq_ebasis_lens_notin:
   "\<lbrakk> ebasis_lens x; s\<^sub>1 \<approx>\<^sub>F s\<^sub>2 on A; x \<notin>\<^sub>F A \<rbrakk> \<Longrightarrow> put\<^bsub>x\<^esub> s\<^sub>1 v \<approx>\<^sub>F put\<^bsub>x\<^esub> s\<^sub>2 v on A"
   by (simp add: basis_lens_not_member_indep, transfer)

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: "\<lbrakk> vwb_lens x; vwb_lens y \<rbrakk> \<Longrightarrow> vwb_lens (x ;\<^sub>L y)"
+lemma comp_vwb_lens [intro]: "\<lbrakk> vwb_lens x; vwb_lens y \<rbrakk> \<Longrightarrow> 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"

Lens_Order.thy

@@ -30,23 +30,18 @@ text \<open>Sublens is a preorder as the following two theorems show.\<close>
 
 lemma sublens_refl [simp]:
   "X \<subseteq>\<^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]:
   "\<lbrakk> X \<subseteq>\<^sub>L Y; Y \<subseteq>\<^sub>L Z \<rbrakk> \<Longrightarrow> X \<subseteq>\<^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 \<open>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.\<close>
 
 lemma sublens_least: "wb_lens X \<Longrightarrow> 0\<^sub>L \<subseteq>\<^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 \<Longrightarrow> X \<subseteq>\<^sub>L 1\<^sub>L"
   by (simp add: sublens_def)
@@ -97,7 +92,7 @@ text \<open>Using our preorder, we can also derive an equivalence on lenses as f
 definition lens_equiv :: "('a \<Longrightarrow> 'c) \<Rightarrow> ('b \<Longrightarrow> 'c) \<Rightarrow> bool" (infix "\<approx>\<^sub>L" 51) where
 [lens_defs]: "lens_equiv X Y = (X \<subseteq>\<^sub>L Y \<and> Y \<subseteq>\<^sub>L X)"
 
-lemma lens_equivI [intro]:
+lemma lens_equivI [intro?]:
   "\<lbrakk> X \<subseteq>\<^sub>L Y; Y \<subseteq>\<^sub>L X \<rbrakk> \<Longrightarrow> X \<approx>\<^sub>L Y"
   by (simp add: lens_equiv_def)
 
@@ -283,7 +278,7 @@ lemma lens_plus_left_unit: "0\<^sub>L +\<^sub>L X \<approx>\<^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 \<approx>\<^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 \<open>We can also show that both sublens and equivalence are congruences with respect to lens plus
   and lens product.\<close>
@@ -453,25 +448,12 @@ text \<open>Consequently, if composition of two lenses $X$ and $Y$ yields @{text
 
 lemma bij_lens_via_comp_id_left:
   "\<lbrakk> wb_lens X; wb_lens Y; X ;\<^sub>L Y = 1\<^sub>L \<rbrakk> \<Longrightarrow> 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:
   "\<lbrakk> wb_lens X; wb_lens Y; X ;\<^sub>L Y = 1\<^sub>L \<rbrakk> \<Longrightarrow> 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 \<open>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 \<open>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 \<approx>\<^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 \<open>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 \<open>Indeed, we actually have a stronger result than this -- the equivale
 lemma lens_equiv_iff_bij:
   assumes "weak_lens Y"
   shows "X \<approx>\<^sub>L Y \<longleftrightarrow> (\<exists> Z. bij_lens Z \<and> 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:
   "\<lbrakk> a \<bowtie> b; mwb_lens a; mwb_lens b; pbij_lens (b +\<^sub>L a) \<rbrakk> \<Longrightarrow> 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
 

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 \<in> set xs" | (a_notin) "a \<notin> 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 *: "\<Squnion>\<^sub>S xs = \<Squnion>\<^sub>S (removeAll a ys)"
+      using Cons(2,3) by (auto intro!: Cons(1) simp: pairwise_insert)
+    then have "\<Squnion>\<^sub>S (a#xs) = (\<Squnion>\<^sub>S xs) \<squnion>\<^sub>S a"
+      by (simp add: scene_union_commute)
+    also have "... = \<Squnion>\<^sub>S (removeAll a ys) \<squnion>\<^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]: "\<bottom>\<^sub>S \<in> scene_space" |
 Vars_scene_space [intro]: "x \<in> set Vars \<Longrightarrow> x \<in> scene_space" |
 union_scene_space [intro]: "\<lbrakk> x \<in> scene_space; y \<in> scene_space \<rbrakk> \<Longrightarrow> x \<squnion>\<^sub>S y \<in> scene_space"
 
-lemma idem_scene_space: "a \<in> scene_space \<Longrightarrow> idem_scene a"
+lemma idem_scene_space [intro, simp]: "a \<in> scene_space \<Longrightarrow> idem_scene a"
   by (induct rule: scene_space.induct) auto
 
 lemma set_Vars_scene_space [simp]: "set Vars \<subseteq> scene_space"
@@ -263,7 +277,7 @@ next
     using scene_union_pres_compat by blast
 qed
 
-lemma scene_space_compat: "\<lbrakk> a \<in> scene_space; b \<in> scene_space \<rbrakk> \<Longrightarrow> a ##\<^sub>S b"
+lemma scene_space_compat [intro]: "\<lbrakk> a \<in> scene_space; b \<in> scene_space \<rbrakk> \<Longrightarrow> 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 (\<squnion>\<^sub>S) xs \<bott
        (metis \<open>idem_scene (- \<Squnion>\<^sub>S xs)\<close> local.span_Vars scene_span_def scene_union_compl uminus_scene_twice)
 qed
 
-lemma scene_space_uminus: "\<lbrakk> a \<in> scene_space \<rbrakk> \<Longrightarrow> - a \<in> scene_space"
+lemma scene_space_uminus [intro, simp]: "\<lbrakk> a \<in> scene_space \<rbrakk> \<Longrightarrow> - a \<in> scene_space"
   by (auto simp add: scene_space_vars_decomp_iff uminus_vars_other_vars)
      (metis filter_is_subset)
 
-lemma scene_space_inter: "\<lbrakk> a \<in> scene_space; b \<in> scene_space \<rbrakk> \<Longrightarrow> a \<sqinter>\<^sub>S b \<in> scene_space"
-  by (simp add: inf_scene_def scene_space.union_scene_space scene_space_uminus)
+lemma scene_space_inter [intro]: "\<lbrakk> a \<in> scene_space; b \<in> scene_space \<rbrakk> \<Longrightarrow> a \<sqinter>\<^sub>S b \<in> scene_space"
+  by (simp add: inf_scene_def scene_space.union_scene_space)
 
 lemma scene_union_foldr_remove_element:
   assumes "set xs \<subseteq> set Vars"
@@ -595,7 +609,7 @@ qed
 lemma scene_union_inter_minus:
   assumes "a \<in> scene_space" "b \<in> scene_space"
   shows "a \<squnion>\<^sub>S (b \<sqinter>\<^sub>S - a) = a \<squnion>\<^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 \<in> scene_space" "set xs \<subseteq> scene_space"
@@ -773,41 +787,50 @@ abbreviation (input) ebasis_lens :: "('a::two \<Longrightarrow> 's::scene_space)
 lemma basis_then_var [simp]: "basis_lens x \<Longrightarrow> 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: "\<lbrakk> vwb_lens x; \<lbrakk>x\<rbrakk>\<^sub>\<sim> \<in> set Vars \<rbrakk> \<Longrightarrow> basis_lens x"
+lemma basis_lensI: "\<lbrakk> vwb_lens x; \<lbrakk>x\<rbrakk>\<^sub>\<sim> \<in> set Vars \<rbrakk> \<Longrightarrow> basis_lens x"
   using basis_lens.intro basis_lens_axioms.intro by blast
 
-subsection \<open> Composite lenses \<close>
+lemma basis_lensE [elim]:
+  assumes "basis_lens x"
+  obtains "vwb_lens x" "\<lbrakk>x\<rbrakk>\<^sub>\<sim> \<in> set Vars"
+  by (simp add: assms)
 
+subsection \<open> Composite lenses \<close>
 locale composite_lens = vwb_lens +
-  assumes comp_in_Vars: "(\<lambda> a. a ;\<^sub>S x) ` set Vars \<subseteq> set Vars"
+  assumes comp_in_Vars: "\<And>a. a \<in> set Vars \<Longrightarrow> a ;\<^sub>S x \<in> set Vars"
 begin
 
-lemma Vars_closed_comp: "a \<in> set Vars \<Longrightarrow> a ;\<^sub>S x \<in> set Vars"
-  using comp_in_Vars by blast
-
-lemma scene_space_closed_comp:
+lemma scene_space_closed_comp [intro]:
   assumes "a \<in> scene_space"
   shows "a ;\<^sub>S x \<in> scene_space"
 proof -
-  obtain xs where xs: "a = \<Squnion>\<^sub>S xs" "set xs \<subseteq> set Vars"
-    using assms scene_space_vars_decomp by blast
-  have "(\<Squnion>\<^sub>S xs) ;\<^sub>S x = \<Squnion>\<^sub>S (map (\<lambda> a. a ;\<^sub>S x) xs)"
-    by (metis foldr_compat_dist pairwise_subset scene_space_compats xs(2))
-  also have "... \<in> 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 \<subseteq> set Vars" "a = \<Squnion>\<^sub>S xs"
+    using scene_space_vars_decomp_iff assms by blast
+  then have "b \<in> set xs \<Longrightarrow> b ;\<^sub>S x \<in> scene_space" for b
+    using comp_in_Vars by blast
+  then have "\<Squnion>\<^sub>S (map (\<lambda>y. y ;\<^sub>S x) xs) \<in> scene_space"
+    by (auto intro!: scene_space_foldr)
+  then show "a ;\<^sub>S x \<in> scene_space"
+    by (simp add: xs foldr_compat_dist pairwise_compat_Vars_subset)
 qed
 
 sublocale var_lens
 proof
   show "\<lbrakk>x\<rbrakk>\<^sub>\<sim> \<in> 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" "\<And>a. a \<in> set Vars \<Longrightarrow> a ;\<^sub>S x \<in> 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 "((\<And>a. a \<in> set Vars \<Longrightarrow> a ;\<^sub>S x \<in> set Vars) \<Longrightarrow> vwb_lens x \<Longrightarrow> P) \<Longrightarrow> P"
+  using assms composite_lens.axioms(1) composite_lens.comp_in_Vars by blast
+
 lemma composite_implies_var_lens [simp]:
   "composite_lens x \<Longrightarrow> 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 \<open> The extension of any lens in the scene space remains in the scene s
 
 lemma composite_lens_comp [simp]:
   "\<lbrakk> composite_lens a; var_lens x \<rbrakk> \<Longrightarrow> 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]:
   "\<lbrakk> composite_lens a; composite_lens x \<rbrakk> \<Longrightarrow> 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 \<open> A basis lens within a composite lens remains a basis lens (i.e. it remains atomic) \<close>
 
 lemma composite_lens_basis_comp [simp]:
   "\<lbrakk> composite_lens a; basis_lens x \<rbrakk> \<Longrightarrow> 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