Improve automation for scene_spaces and fix proofs that broke

Author: cplaursen

Alphabet_Scene_Space_Examples.thy

@@ -9,6 +9,7 @@ alphabet test =
   y :: nat 
   z :: "int list"
 
+(* TODO: figure out why it's re-declaring the intro rule *)
 alphabet_scene_space test
 
 lemma "UNIV\<^sub>F(test) = \<lbrace>x, y, z\<rbrace>\<^sub>F"

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)
@@ -357,7 +357,7 @@ proof (transfer)
   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"
@@ -370,7 +370,6 @@ lemma frame_equiv_trans: "\<lbrakk> s\<^sub>1 \<approx>\<^sub>F s\<^sub>2 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)

Scene_Spaces.thy

@@ -773,7 +773,7 @@ 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 [intro]: "\<lbrakk> vwb_lens x; \<lbrakk>x\<rbrakk>\<^sub>\<sim> \<in> set Vars \<rbrakk> \<Longrightarrow> basis_lens x"
+lemma basis_lensI [intro]: "\<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
 
 lemma basis_lensE [elim]:
@@ -782,46 +782,40 @@ lemma basis_lensE [elim]:
   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 [intro]: "a \<in> set Vars \<Longrightarrow> a ;\<^sub>S x \<in> set Vars"
-  using comp_in_Vars by blast
-
 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 [intro]:
-  assumes "vwb_lens x" "(\<lambda> a. a ;\<^sub>S x) ` set Vars \<subseteq> set Vars"
+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"
-  obtains "vwb_lens x" "(\<lambda> a. a ;\<^sub>S x) ` set Vars \<subseteq> set Vars"
-  using assms composite_lens.Vars_closed_comp composite_lens_def by blast
+  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"
@@ -831,19 +825,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)"
-  apply (auto intro!: composite_lensI elim!: composite_lensE simp: image_subset_iff)
-  apply (metis scene_comp_assoc)
-  done
+  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)"
-  using lens_scene_comp by blast
+  using lens_scene_comp by force
 
 lemma id_composite_lens: "composite_lens 1\<^sub>L"
   by (force intro: composite_lens.intro composite_lens_axioms.intro)