Added definedness properties for partial function collections

isabelle-utp · Sep 11, 2023 · 4f34621 · 4f34621
1 parent 24e1592
commit 4f34621
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 0 deletions.
diff --git a/Collections.thy b/Collections.thy
@@ -77,4 +77,9 @@ lemma defined_list_collection_lens [simp]:
   by (simp add: lens_defined_def src_dyn_lens unrest source_ns_alpha source_list_collection_lens)
      (simp add: lens_defs wb_lens.source_UNIV)
 
+lemma lens_defined_list_code [code_unfold]: 
+  "vwb_lens x \<Longrightarrow> lens_defined (ns_alpha x (list_collection_lens i)) = (\<guillemotleft>i\<guillemotright> < length($x))\<^sub>e"
+  by (simp add: lens_defined_def src_dyn_lens unrest source_ns_alpha source_list_collection_lens)
+     (simp add: lens_defs wb_lens.source_UNIV)
+
 end
diff --git a/Z/Collections_Z.thy b/Z/Collections_Z.thy
@@ -22,6 +22,11 @@ lemma defined_pfun_collection_lens [simp, code_unfold]:
   by (simp add: lens_defined_def src_dyn_lens unrest source_ns_alpha source_pfun_collection_lens)
      (simp add: lens_defs wb_lens.source_UNIV)
 
+lemma lens_defined_pfun_code [code_unfold]: 
+  "vwb_lens x \<Longrightarrow> lens_defined (ns_alpha x (pfun_collection_lens i)) = (\<guillemotleft>i\<guillemotright> \<in> pdom($x))\<^sub>e"
+  by (simp add: lens_defined_def src_dyn_lens unrest source_ns_alpha source_pfun_collection_lens)
+     (simp add: lens_defs wb_lens.source_UNIV)
+
 subsection \<open> Finite Function Collection Lens \<close>
 
 definition ffun_collection_lens :: "'a \<Rightarrow> 'b \<Longrightarrow> 'a \<Zffun> 'b" where