# HG changeset patch
# User haftmann
# Date 1278336342 -7200
# Node ID ede4b8397e0128baaed094e42550966443ba5498
# Parent  24bb91462892e276e2885c7e1167e23e8654f504
moved special operation array_ran here

diff -r 24bb91462892 -r ede4b8397e01 src/HOL/Imperative_HOL/ex/SatChecker.thy
--- a/src/HOL/Imperative_HOL/ex/SatChecker.thy	Mon Jul 05 15:25:42 2010 +0200
+++ b/src/HOL/Imperative_HOL/ex/SatChecker.thy	Mon Jul 05 15:25:42 2010 +0200
@@ -118,6 +118,32 @@
 
 text {* Specific definition for derived clauses in the Array *}
 
+definition
+  array_ran :: "('a\<Colon>heap) option array \<Rightarrow> heap \<Rightarrow> 'a set" where
+  "array_ran a h = {e. Some e \<in> set (get_array a h)}"
+    -- {*FIXME*}
+
+lemma array_ranI: "\<lbrakk> Some b = get_array a h ! i; i < Heap.length a h \<rbrakk> \<Longrightarrow> b \<in> array_ran a h"
+unfolding array_ran_def Heap.length_def by simp
+
+lemma array_ran_upd_array_Some:
+  assumes "cl \<in> array_ran a (Heap.upd a i (Some b) h)"
+  shows "cl \<in> array_ran a h \<or> cl = b"
+proof -
+  have "set (get_array a h[i := Some b]) \<subseteq> insert (Some b) (set (get_array a h))" by (rule set_update_subset_insert)
+  with assms show ?thesis 
+    unfolding array_ran_def Heap.upd_def by fastsimp
+qed
+
+lemma array_ran_upd_array_None:
+  assumes "cl \<in> array_ran a (Heap.upd a i None h)"
+  shows "cl \<in> array_ran a h"
+proof -
+  have "set (get_array a h[i := None]) \<subseteq> insert None (set (get_array a h))" by (rule set_update_subset_insert)
+  with assms show ?thesis
+    unfolding array_ran_def Heap.upd_def by auto
+qed
+
 definition correctArray :: "Clause list \<Rightarrow> Clause option array \<Rightarrow> heap \<Rightarrow> bool"
 where
   "correctArray rootcls a h =