1.1 --- a/src/HOL/Imperative_HOL/ex/SatChecker.thy	Mon Jul 05 15:25:42 2010 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/ex/SatChecker.thy	Mon Jul 05 15:25:42 2010 +0200
     1.3 @@ -118,6 +118,32 @@
     1.4  
     1.5  text {* Specific definition for derived clauses in the Array *}
     1.6  
     1.7 +definition
     1.8 +  array_ran :: "('a\<Colon>heap) option array \<Rightarrow> heap \<Rightarrow> 'a set" where
     1.9 +  "array_ran a h = {e. Some e \<in> set (get_array a h)}"
    1.10 +    -- {*FIXME*}
    1.11 +
    1.12 +lemma array_ranI: "\<lbrakk> Some b = get_array a h ! i; i < Heap.length a h \<rbrakk> \<Longrightarrow> b \<in> array_ran a h"
    1.13 +unfolding array_ran_def Heap.length_def by simp
    1.14 +
    1.15 +lemma array_ran_upd_array_Some:
    1.16 +  assumes "cl \<in> array_ran a (Heap.upd a i (Some b) h)"
    1.17 +  shows "cl \<in> array_ran a h \<or> cl = b"
    1.18 +proof -
    1.19 +  have "set (get_array a h[i := Some b]) \<subseteq> insert (Some b) (set (get_array a h))" by (rule set_update_subset_insert)
    1.20 +  with assms show ?thesis 
    1.21 +    unfolding array_ran_def Heap.upd_def by fastsimp
    1.22 +qed
    1.23 +
    1.24 +lemma array_ran_upd_array_None:
    1.25 +  assumes "cl \<in> array_ran a (Heap.upd a i None h)"
    1.26 +  shows "cl \<in> array_ran a h"
    1.27 +proof -
    1.28 +  have "set (get_array a h[i := None]) \<subseteq> insert None (set (get_array a h))" by (rule set_update_subset_insert)
    1.29 +  with assms show ?thesis
    1.30 +    unfolding array_ran_def Heap.upd_def by auto
    1.31 +qed
    1.32 +
    1.33  definition correctArray :: "Clause list \<Rightarrow> Clause option array \<Rightarrow> heap \<Rightarrow> bool"
    1.34  where
    1.35    "correctArray rootcls a h =