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"