128 |
128 |
129 lemma array_ran_upd_array_Some: |
129 lemma array_ran_upd_array_Some: |
130 assumes "cl \<in> array_ran a (Array.update a i (Some b) h)" |
130 assumes "cl \<in> array_ran a (Array.update a i (Some b) h)" |
131 shows "cl \<in> array_ran a h \<or> cl = b" |
131 shows "cl \<in> array_ran a h \<or> cl = b" |
132 proof - |
132 proof - |
133 have "set (Array.get h a[i := Some b]) \<subseteq> insert (Some b) (set (Array.get h a))" by (rule set_update_subset_insert) |
133 have "set ((Array.get h a)[i := Some b]) \<subseteq> insert (Some b) (set (Array.get h a))" by (rule set_update_subset_insert) |
134 with assms show ?thesis |
134 with assms show ?thesis |
135 unfolding array_ran_def Array.update_def by fastforce |
135 unfolding array_ran_def Array.update_def by fastforce |
136 qed |
136 qed |
137 |
137 |
138 lemma array_ran_upd_array_None: |
138 lemma array_ran_upd_array_None: |
139 assumes "cl \<in> array_ran a (Array.update a i None h)" |
139 assumes "cl \<in> array_ran a (Array.update a i None h)" |
140 shows "cl \<in> array_ran a h" |
140 shows "cl \<in> array_ran a h" |
141 proof - |
141 proof - |
142 have "set (Array.get h a[i := None]) \<subseteq> insert None (set (Array.get h a))" by (rule set_update_subset_insert) |
142 have "set ((Array.get h a)[i := None]) \<subseteq> insert None (set (Array.get h a))" by (rule set_update_subset_insert) |
143 with assms show ?thesis |
143 with assms show ?thesis |
144 unfolding array_ran_def Array.update_def by auto |
144 unfolding array_ran_def Array.update_def by auto |
145 qed |
145 qed |
146 |
146 |
147 definition correctArray :: "Clause list \<Rightarrow> Clause option array \<Rightarrow> heap \<Rightarrow> bool" |
147 definition correctArray :: "Clause list \<Rightarrow> Clause option array \<Rightarrow> heap \<Rightarrow> bool" |