src/HOL/Imperative_HOL/ex/SatChecker.thy
 changeset 37805 0f797d586ce5 parent 37802 f2e9c104cebd child 37806 a7679be14442
```     1.1 --- a/src/HOL/Imperative_HOL/ex/SatChecker.thy	Tue Jul 13 16:00:56 2010 +0200
1.2 +++ b/src/HOL/Imperative_HOL/ex/SatChecker.thy	Tue Jul 13 16:12:40 2010 +0200
1.3 @@ -120,17 +120,17 @@
1.4
1.5  definition
1.6    array_ran :: "('a\<Colon>heap) option array \<Rightarrow> heap \<Rightarrow> 'a set" where
1.7 -  "array_ran a h = {e. Some e \<in> set (get_array a h)}"
1.8 +  "array_ran a h = {e. Some e \<in> set (get_array h a)}"
1.9      -- {*FIXME*}
1.10
1.11 -lemma array_ranI: "\<lbrakk> Some b = get_array a h ! i; i < Array.length h a \<rbrakk> \<Longrightarrow> b \<in> array_ran a h"
1.12 +lemma array_ranI: "\<lbrakk> Some b = get_array h a ! i; i < Array.length h a \<rbrakk> \<Longrightarrow> b \<in> array_ran a h"
1.13  unfolding array_ran_def Array.length_def by simp
1.14
1.15  lemma array_ran_upd_array_Some:
1.16    assumes "cl \<in> array_ran a (Array.update 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 +  have "set (get_array h a[i := Some b]) \<subseteq> insert (Some b) (set (get_array h a))" by (rule set_update_subset_insert)
1.21    with assms show ?thesis
1.22      unfolding array_ran_def Array.update_def by fastsimp
1.23  qed
1.24 @@ -139,7 +139,7 @@
1.25    assumes "cl \<in> array_ran a (Array.update 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 +  have "set (get_array h a[i := None]) \<subseteq> insert None (set (get_array h a))" by (rule set_update_subset_insert)
1.30    with assms show ?thesis
1.31      unfolding array_ran_def Array.update_def by auto
1.32  qed
1.33 @@ -477,7 +477,7 @@
1.34      fix clj
1.35      let ?rs = "merge (remove l cli) (remove (compl l) clj)"
1.36      let ?rs' = "merge (remove (compl l) cli) (remove l clj)"
1.37 -    assume "h = h'" "Some clj = get_array a h' ! j" "j < Array.length h' a"
1.38 +    assume "h = h'" "Some clj = get_array h' a ! j" "j < Array.length h' a"
1.39      with correct_a have clj: "correctClause r clj" "sorted clj" "distinct clj"
1.40        unfolding correctArray_def by (auto intro: array_ranI)
1.41      with clj l_not_zero correct_cli
1.42 @@ -491,7 +491,7 @@
1.43    }
1.44    {
1.45      fix v clj
1.46 -    assume "Some clj = get_array a h ! j" "j < Array.length h a"
1.47 +    assume "Some clj = get_array h a ! j" "j < Array.length h a"
1.48      with correct_a have clj: "correctClause r clj \<and> sorted clj \<and> distinct clj"
1.49        unfolding correctArray_def by (auto intro: array_ranI)
1.50      assume "crel (res_thm' l cli clj) h h' rs"
```