proper merge of operation changes and generic do-syntax
authorhaftmann
Tue Jul 13 12:16:24 2010 +0200 (2010-07-13 ago)
changeset 377980b0570445a2a
parent 37797 96551d6b1414
child 37799 b2f84bb86c73
proper merge of operation changes and generic do-syntax
src/HOL/Imperative_HOL/Array.thy
src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy
src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy
src/HOL/Imperative_HOL/ex/SatChecker.thy
     1.1 --- a/src/HOL/Imperative_HOL/Array.thy	Tue Jul 13 12:05:20 2010 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/Array.thy	Tue Jul 13 12:16:24 2010 +0200
     1.3 @@ -35,9 +35,8 @@
     1.4    length :: "'a\<Colon>heap array \<Rightarrow> heap \<Rightarrow> nat" where
     1.5    "length a h = List.length (get_array a h)"
     1.6    
     1.7 -definition (*FIXME update*)
     1.8 -  change :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> heap \<Rightarrow> heap" where
     1.9 -  "change a i x h = set_array a ((get_array a h)[i:=x]) h"
    1.10 +definition update :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> heap \<Rightarrow> heap" where
    1.11 +  "update a i x h = set_array a ((get_array a h)[i:=x]) h"
    1.12  
    1.13  definition (*FIXME noteq*)
    1.14    noteq_arrs :: "'a\<Colon>heap array \<Rightarrow> 'b\<Colon>heap array \<Rightarrow> bool" (infix "=!!=" 70) where
    1.15 @@ -64,15 +63,15 @@
    1.16  
    1.17  definition upd :: "nat \<Rightarrow> 'a \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> 'a\<Colon>heap array Heap" where
    1.18    [code del]: "upd i x a = Heap_Monad.guard (\<lambda>h. i < length a h)
    1.19 -    (\<lambda>h. (a, change a i x h))"
    1.20 +    (\<lambda>h. (a, update a i x h))"
    1.21  
    1.22  definition map_entry :: "nat \<Rightarrow> ('a\<Colon>heap \<Rightarrow> 'a) \<Rightarrow> 'a array \<Rightarrow> 'a array Heap" where
    1.23    [code del]: "map_entry i f a = Heap_Monad.guard (\<lambda>h. i < length a h)
    1.24 -    (\<lambda>h. (a, change a i (f (get_array a h ! i)) h))"
    1.25 +    (\<lambda>h. (a, update a i (f (get_array a h ! i)) h))"
    1.26  
    1.27  definition swap :: "nat \<Rightarrow> 'a \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> 'a Heap" where
    1.28    [code del]: "swap i x a = Heap_Monad.guard (\<lambda>h. i < length a h)
    1.29 -    (\<lambda>h. (get_array a h ! i, change a i x h))"
    1.30 +    (\<lambda>h. (get_array a h ! i, update a i x h))"
    1.31  
    1.32  definition freeze :: "'a\<Colon>heap array \<Rightarrow> 'a list Heap" where
    1.33    [code del]: "freeze a = Heap_Monad.tap (\<lambda>h. get_array a h)"
    1.34 @@ -109,27 +108,27 @@
    1.35    "r =!!= r' \<Longrightarrow> set_array r x (set_array r' x' h) = set_array r' x' (set_array r x h)"
    1.36    by (simp add: Let_def expand_fun_eq noteq_arrs_def set_array_def)
    1.37  
    1.38 -lemma get_array_change_eq [simp]:
    1.39 -  "get_array a (change a i v h) = (get_array a h) [i := v]"
    1.40 -  by (simp add: change_def)
    1.41 +lemma get_array_update_eq [simp]:
    1.42 +  "get_array a (update a i v h) = (get_array a h) [i := v]"
    1.43 +  by (simp add: update_def)
    1.44  
    1.45 -lemma nth_change_array_neq_array [simp]:
    1.46 -  "a =!!= b \<Longrightarrow> get_array a (change b j v h) ! i = get_array a h ! i"
    1.47 -  by (simp add: change_def noteq_arrs_def)
    1.48 +lemma nth_update_array_neq_array [simp]:
    1.49 +  "a =!!= b \<Longrightarrow> get_array a (update b j v h) ! i = get_array a h ! i"
    1.50 +  by (simp add: update_def noteq_arrs_def)
    1.51  
    1.52 -lemma get_arry_array_change_elem_neqIndex [simp]:
    1.53 -  "i \<noteq> j \<Longrightarrow> get_array a (change a j v h) ! i = get_array a h ! i"
    1.54 +lemma get_arry_array_update_elem_neqIndex [simp]:
    1.55 +  "i \<noteq> j \<Longrightarrow> get_array a (update a j v h) ! i = get_array a h ! i"
    1.56    by simp
    1.57  
    1.58 -lemma length_change [simp]: 
    1.59 -  "length a (change b i v h) = length a h"
    1.60 -  by (simp add: change_def length_def set_array_def get_array_def)
    1.61 +lemma length_update [simp]: 
    1.62 +  "length a (update b i v h) = length a h"
    1.63 +  by (simp add: update_def length_def set_array_def get_array_def)
    1.64  
    1.65 -lemma change_swap_neqArray:
    1.66 +lemma update_swap_neqArray:
    1.67    "a =!!= a' \<Longrightarrow> 
    1.68 -  change a i v (change a' i' v' h) 
    1.69 -  = change a' i' v' (change a i v h)"
    1.70 -apply (unfold change_def)
    1.71 +  update a i v (update a' i' v' h) 
    1.72 +  = update a' i' v' (update a i v h)"
    1.73 +apply (unfold update_def)
    1.74  apply simp
    1.75  apply (subst array_set_set_swap, assumption)
    1.76  apply (subst array_get_set_neq)
    1.77 @@ -137,9 +136,9 @@
    1.78  apply (simp)
    1.79  done
    1.80  
    1.81 -lemma change_swap_neqIndex:
    1.82 -  "\<lbrakk> i \<noteq> i' \<rbrakk> \<Longrightarrow> change a i v (change a i' v' h) = change a i' v' (change a i v h)"
    1.83 -  by (auto simp add: change_def array_set_set_swap list_update_swap)
    1.84 +lemma update_swap_neqIndex:
    1.85 +  "\<lbrakk> i \<noteq> i' \<rbrakk> \<Longrightarrow> update a i v (update a i' v' h) = update a i' v' (update a i v h)"
    1.86 +  by (auto simp add: update_def array_set_set_swap list_update_swap)
    1.87  
    1.88  lemma get_array_init_array_list:
    1.89    "get_array (fst (array ls h)) (snd (array ls' h)) = ls'"
    1.90 @@ -151,9 +150,9 @@
    1.91         = snd (array new_ls h)"
    1.92    by (simp add: Let_def split_def array_def)
    1.93  
    1.94 -lemma array_present_change [simp]: 
    1.95 -  "array_present a (change b i v h) = array_present a h"
    1.96 -  by (simp add: change_def array_present_def set_array_def get_array_def)
    1.97 +lemma array_present_update [simp]: 
    1.98 +  "array_present a (update b i v h) = array_present a h"
    1.99 +  by (simp add: update_def array_present_def set_array_def get_array_def)
   1.100  
   1.101  lemma array_present_array [simp]:
   1.102    "array_present (fst (array xs h)) (snd (array xs h))"
   1.103 @@ -264,7 +263,7 @@
   1.104  
   1.105  lemma execute_upd [execute_simps]:
   1.106    "i < length a h \<Longrightarrow>
   1.107 -    execute (upd i x a) h = Some (a, change a i x h)"
   1.108 +    execute (upd i x a) h = Some (a, update a i x h)"
   1.109    "i \<ge> length a h \<Longrightarrow> execute (upd i x a) h = None"
   1.110    by (simp_all add: upd_def execute_simps)
   1.111  
   1.112 @@ -273,20 +272,20 @@
   1.113    by (auto intro: success_intros simp add: upd_def)
   1.114  
   1.115  lemma crel_updI [crel_intros]:
   1.116 -  assumes "i < length a h" "h' = change a i v h"
   1.117 +  assumes "i < length a h" "h' = update a i v h"
   1.118    shows "crel (upd i v a) h h' a"
   1.119    by (rule crelI) (insert assms, simp add: execute_simps)
   1.120  
   1.121  lemma crel_updE [crel_elims]:
   1.122    assumes "crel (upd i v a) h h' r"
   1.123 -  obtains "r = a" "h' = change a i v h" "i < length a h"
   1.124 +  obtains "r = a" "h' = update a i v h" "i < length a h"
   1.125    using assms by (rule crelE)
   1.126      (erule successE, cases "i < length a h", simp_all add: execute_simps)
   1.127  
   1.128  lemma execute_map_entry [execute_simps]:
   1.129    "i < length a h \<Longrightarrow>
   1.130     execute (map_entry i f a) h =
   1.131 -      Some (a, change a i (f (get_array a h ! i)) h)"
   1.132 +      Some (a, update a i (f (get_array a h ! i)) h)"
   1.133    "i \<ge> length a h \<Longrightarrow> execute (map_entry i f a) h = None"
   1.134    by (simp_all add: map_entry_def execute_simps)
   1.135  
   1.136 @@ -295,20 +294,20 @@
   1.137    by (auto intro: success_intros simp add: map_entry_def)
   1.138  
   1.139  lemma crel_map_entryI [crel_intros]:
   1.140 -  assumes "i < length a h" "h' = change a i (f (get_array a h ! i)) h" "r = a"
   1.141 +  assumes "i < length a h" "h' = update a i (f (get_array a h ! i)) h" "r = a"
   1.142    shows "crel (map_entry i f a) h h' r"
   1.143    by (rule crelI) (insert assms, simp add: execute_simps)
   1.144  
   1.145  lemma crel_map_entryE [crel_elims]:
   1.146    assumes "crel (map_entry i f a) h h' r"
   1.147 -  obtains "r = a" "h' = change a i (f (get_array a h ! i)) h" "i < length a h"
   1.148 +  obtains "r = a" "h' = update a i (f (get_array a h ! i)) h" "i < length a h"
   1.149    using assms by (rule crelE)
   1.150      (erule successE, cases "i < length a h", simp_all add: execute_simps)
   1.151  
   1.152  lemma execute_swap [execute_simps]:
   1.153    "i < length a h \<Longrightarrow>
   1.154     execute (swap i x a) h =
   1.155 -      Some (get_array a h ! i, change a i x h)"
   1.156 +      Some (get_array a h ! i, update a i x h)"
   1.157    "i \<ge> length a h \<Longrightarrow> execute (swap i x a) h = None"
   1.158    by (simp_all add: swap_def execute_simps)
   1.159  
   1.160 @@ -317,13 +316,13 @@
   1.161    by (auto intro: success_intros simp add: swap_def)
   1.162  
   1.163  lemma crel_swapI [crel_intros]:
   1.164 -  assumes "i < length a h" "h' = change a i x h" "r = get_array a h ! i"
   1.165 +  assumes "i < length a h" "h' = update a i x h" "r = get_array a h ! i"
   1.166    shows "crel (swap i x a) h h' r"
   1.167    by (rule crelI) (insert assms, simp add: execute_simps)
   1.168  
   1.169  lemma crel_swapE [crel_elims]:
   1.170    assumes "crel (swap i x a) h h' r"
   1.171 -  obtains "r = get_array a h ! i" "h' = change a i x h" "i < length a h"
   1.172 +  obtains "r = get_array a h ! i" "h' = update a i x h" "i < length a h"
   1.173    using assms by (rule crelE)
   1.174      (erule successE, cases "i < length a h", simp_all add: execute_simps)
   1.175  
   1.176 @@ -357,7 +356,7 @@
   1.177    "of_list xs = make (List.length xs) (\<lambda>n. xs ! n)"
   1.178    by (rule Heap_eqI) (simp add: map_nth execute_simps)
   1.179  
   1.180 -hide_const (open) new
   1.181 +hide_const (open) update new of_list make len nth upd map_entry swap freeze
   1.182  
   1.183  
   1.184  subsection {* Code generator setup *}
   1.185 @@ -407,24 +406,24 @@
   1.186    by (simp add: upd'_def upd_return)
   1.187  
   1.188  lemma [code]:
   1.189 -  "map_entry i f a = do {
   1.190 -     x \<leftarrow> nth a i;
   1.191 -     upd i (f x) a
   1.192 +  "Array.map_entry i f a = do {
   1.193 +     x \<leftarrow> Array.nth a i;
   1.194 +     Array.upd i (f x) a
   1.195     }"
   1.196    by (rule Heap_eqI) (simp add: bind_def guard_def map_entry_def execute_simps)
   1.197  
   1.198  lemma [code]:
   1.199 -  "swap i x a = do {
   1.200 -     y \<leftarrow> nth a i;
   1.201 -     upd i x a;
   1.202 +  "Array.swap i x a = do {
   1.203 +     y \<leftarrow> Array.nth a i;
   1.204 +     Array.upd i x a;
   1.205       return y
   1.206     }"
   1.207    by (rule Heap_eqI) (simp add: bind_def guard_def swap_def execute_simps)
   1.208  
   1.209  lemma [code]:
   1.210 -  "freeze a = do {
   1.211 -     n \<leftarrow> len a;
   1.212 -     Heap_Monad.fold_map (\<lambda>i. nth a i) [0..<n]
   1.213 +  "Array.freeze a = do {
   1.214 +     n \<leftarrow> Array.len a;
   1.215 +     Heap_Monad.fold_map (\<lambda>i. Array.nth a i) [0..<n]
   1.216     }"
   1.217  proof (rule Heap_eqI)
   1.218    fix h
   1.219 @@ -441,12 +440,12 @@
   1.220      apply (simp add: length_def map_nth)
   1.221      done
   1.222    then have "execute (do {
   1.223 -      n \<leftarrow> len a;
   1.224 +      n \<leftarrow> Array.len a;
   1.225        Heap_Monad.fold_map (Array.nth a) [0..<n]
   1.226      }) h = Some (get_array a h, h)"
   1.227      by (auto intro: execute_bind_eq_SomeI simp add: execute_simps)
   1.228 -  then show "execute (freeze a) h = execute (do {
   1.229 -      n \<leftarrow> len a;
   1.230 +  then show "execute (Array.freeze a) h = execute (do {
   1.231 +      n \<leftarrow> Array.len a;
   1.232        Heap_Monad.fold_map (Array.nth a) [0..<n]
   1.233      }) h" by (simp add: execute_simps)
   1.234  qed
     2.1 --- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Tue Jul 13 12:05:20 2010 +0200
     2.2 +++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Tue Jul 13 12:16:24 2010 +0200
     2.3 @@ -14,17 +14,17 @@
     2.4  where
     2.5    "swap arr i j =
     2.6       do {
     2.7 -       x \<leftarrow> nth arr i;
     2.8 -       y \<leftarrow> nth arr j;
     2.9 -       upd i y arr;
    2.10 -       upd j x arr;
    2.11 +       x \<leftarrow> Array.nth arr i;
    2.12 +       y \<leftarrow> Array.nth arr j;
    2.13 +       Array.upd i y arr;
    2.14 +       Array.upd j x arr;
    2.15         return ()
    2.16       }"
    2.17  
    2.18  lemma crel_swapI [crel_intros]:
    2.19    assumes "i < Array.length a h" "j < Array.length a h"
    2.20      "x = get_array a h ! i" "y = get_array a h ! j"
    2.21 -    "h' = Array.change a j x (Array.change a i y h)"
    2.22 +    "h' = Array.update a j x (Array.update a i y h)"
    2.23    shows "crel (swap a i j) h h' r"
    2.24    unfolding swap_def using assms by (auto intro!: crel_intros)
    2.25  
    2.26 @@ -41,7 +41,7 @@
    2.27    "part1 a left right p = (
    2.28       if (right \<le> left) then return right
    2.29       else do {
    2.30 -       v \<leftarrow> nth a left;
    2.31 +       v \<leftarrow> Array.nth a left;
    2.32         (if (v \<le> p) then (part1 a (left + 1) right p)
    2.33                      else (do { swap a left right;
    2.34    part1 a left (right - 1) p }))
    2.35 @@ -228,9 +228,9 @@
    2.36  fun partition :: "nat array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat Heap"
    2.37  where
    2.38    "partition a left right = do {
    2.39 -     pivot \<leftarrow> nth a right;
    2.40 +     pivot \<leftarrow> Array.nth a right;
    2.41       middle \<leftarrow> part1 a left (right - 1) pivot;
    2.42 -     v \<leftarrow> nth a middle;
    2.43 +     v \<leftarrow> Array.nth a middle;
    2.44       m \<leftarrow> return (if (v \<le> pivot) then (middle + 1) else middle);
    2.45       swap a m right;
    2.46       return m
    2.47 @@ -294,8 +294,8 @@
    2.48           else middle)"
    2.49      unfolding partition.simps
    2.50      by (elim crel_bindE crel_returnE crel_nthE crel_ifE crel_updE) simp
    2.51 -  from swap have h'_def: "h' = Array.change a r (get_array a h1 ! rs)
    2.52 -    (Array.change a rs (get_array a h1 ! r) h1)"
    2.53 +  from swap have h'_def: "h' = Array.update a r (get_array a h1 ! rs)
    2.54 +    (Array.update a rs (get_array a h1 ! r) h1)"
    2.55      unfolding swap_def
    2.56      by (elim crel_bindE crel_returnE crel_nthE crel_updE) simp
    2.57    from swap have in_bounds: "r < Array.length a h1 \<and> rs < Array.length a h1"
    2.58 @@ -326,7 +326,7 @@
    2.59        with part_partitions[OF part] right_remains True
    2.60        have "get_array a h1 ! i \<le> get_array a h' ! rs" by fastsimp
    2.61        with i_props h'_def in_bounds have "get_array a h' ! i \<le> get_array a h' ! rs"
    2.62 -        unfolding Array.change_def Array.length_def by simp
    2.63 +        unfolding Array.update_def Array.length_def by simp
    2.64      }
    2.65      moreover
    2.66      {
    2.67 @@ -352,7 +352,7 @@
    2.68            by fastsimp
    2.69          with i_is True rs_equals right_remains h'_def
    2.70          show ?thesis using in_bounds
    2.71 -          unfolding Array.change_def Array.length_def
    2.72 +          unfolding Array.update_def Array.length_def
    2.73            by auto
    2.74        qed
    2.75      }
    2.76 @@ -368,7 +368,7 @@
    2.77        from part_partitions[OF part] rs_equals right_remains i_is_left
    2.78        have "get_array a h1 ! i \<le> get_array a h' ! rs" by fastsimp
    2.79        with i_props h'_def have "get_array a h' ! i \<le> get_array a h' ! rs"
    2.80 -        unfolding Array.change_def by simp
    2.81 +        unfolding Array.update_def by simp
    2.82      }
    2.83      moreover
    2.84      {
    2.85 @@ -388,7 +388,7 @@
    2.86          assume i_is: "i = r"
    2.87          from i_is False rs_equals right_remains h'_def
    2.88          show ?thesis using in_bounds
    2.89 -          unfolding Array.change_def Array.length_def
    2.90 +          unfolding Array.update_def Array.length_def
    2.91            by auto
    2.92        qed
    2.93      }
    2.94 @@ -646,7 +646,7 @@
    2.95  subsection {* Example *}
    2.96  
    2.97  definition "qsort a = do {
    2.98 -    k \<leftarrow> len a;
    2.99 +    k \<leftarrow> Array.len a;
   2.100      quicksort a 0 (k - 1);
   2.101      return a
   2.102    }"
     3.1 --- a/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy	Tue Jul 13 12:05:20 2010 +0200
     3.2 +++ b/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy	Tue Jul 13 12:16:24 2010 +0200
     3.3 @@ -8,14 +8,12 @@
     3.4  imports Imperative_HOL Subarray
     3.5  begin
     3.6  
     3.7 -hide_const (open) swap rev
     3.8 -
     3.9  fun swap :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap" where
    3.10    "swap a i j = do {
    3.11 -     x \<leftarrow> nth a i;
    3.12 -     y \<leftarrow> nth a j;
    3.13 -     upd i y a;
    3.14 -     upd j x a;
    3.15 +     x \<leftarrow> Array.nth a i;
    3.16 +     y \<leftarrow> Array.nth a j;
    3.17 +     Array.upd i y a;
    3.18 +     Array.upd j x a;
    3.19       return ()
    3.20     }"
    3.21  
    3.22 @@ -26,9 +24,6 @@
    3.23     }
    3.24     else return ())"
    3.25  
    3.26 -notation (output) swap ("swap")
    3.27 -notation (output) rev ("rev")
    3.28 -
    3.29  declare swap.simps [simp del] rev.simps [simp del]
    3.30  
    3.31  lemma swap_pointwise: assumes "crel (swap a i j) h h' r"
     4.1 --- a/src/HOL/Imperative_HOL/ex/SatChecker.thy	Tue Jul 13 12:05:20 2010 +0200
     4.2 +++ b/src/HOL/Imperative_HOL/ex/SatChecker.thy	Tue Jul 13 12:16:24 2010 +0200
     4.3 @@ -127,21 +127,21 @@
     4.4  unfolding array_ran_def Array.length_def by simp
     4.5  
     4.6  lemma array_ran_upd_array_Some:
     4.7 -  assumes "cl \<in> array_ran a (Array.change a i (Some b) h)"
     4.8 +  assumes "cl \<in> array_ran a (Array.update a i (Some b) h)"
     4.9    shows "cl \<in> array_ran a h \<or> cl = b"
    4.10  proof -
    4.11    have "set (get_array a h[i := Some b]) \<subseteq> insert (Some b) (set (get_array a h))" by (rule set_update_subset_insert)
    4.12    with assms show ?thesis 
    4.13 -    unfolding array_ran_def Array.change_def by fastsimp
    4.14 +    unfolding array_ran_def Array.update_def by fastsimp
    4.15  qed
    4.16  
    4.17  lemma array_ran_upd_array_None:
    4.18 -  assumes "cl \<in> array_ran a (Array.change a i None h)"
    4.19 +  assumes "cl \<in> array_ran a (Array.update a i None h)"
    4.20    shows "cl \<in> array_ran a h"
    4.21  proof -
    4.22    have "set (get_array a h[i := None]) \<subseteq> insert None (set (get_array a h))" by (rule set_update_subset_insert)
    4.23    with assms show ?thesis
    4.24 -    unfolding array_ran_def Array.change_def by auto
    4.25 +    unfolding array_ran_def Array.update_def by auto
    4.26  qed
    4.27  
    4.28  definition correctArray :: "Clause list \<Rightarrow> Clause option array \<Rightarrow> heap \<Rightarrow> bool"
    4.29 @@ -152,7 +152,7 @@
    4.30  lemma correctArray_update:
    4.31    assumes "correctArray rcs a h"
    4.32    assumes "correctClause rcs c" "sorted c" "distinct c"
    4.33 -  shows "correctArray rcs a (Array.change a i (Some c) h)"
    4.34 +  shows "correctArray rcs a (Array.update a i (Some c) h)"
    4.35    using assms
    4.36    unfolding correctArray_def
    4.37    by (auto dest:array_ran_upd_array_Some)
    4.38 @@ -413,7 +413,7 @@
    4.39  definition get_clause :: "Clause option array \<Rightarrow> ClauseId \<Rightarrow> Clause Heap"
    4.40  where
    4.41    "get_clause a i = 
    4.42 -       do { c \<leftarrow> nth a i;
    4.43 +       do { c \<leftarrow> Array.nth a i;
    4.44             (case c of None \<Rightarrow> raise (''Clause not found'')
    4.45                      | Some x \<Rightarrow> return x)
    4.46         }"
    4.47 @@ -440,11 +440,11 @@
    4.48    do {
    4.49       cli \<leftarrow> get_clause a i;
    4.50       result \<leftarrow> foldM (res_thm2 a) rs cli;
    4.51 -     upd saveTo (Some result) a; 
    4.52 +     Array.upd saveTo (Some result) a; 
    4.53       return rcs
    4.54    }"
    4.55 -| "doProofStep2 a (Delete cid) rcs = do { upd cid None a; return rcs }"
    4.56 -| "doProofStep2 a (Root cid clause) rcs = do { upd cid (Some (remdups (sort clause))) a; return (clause # rcs) }"
    4.57 +| "doProofStep2 a (Delete cid) rcs = do { Array.upd cid None a; return rcs }"
    4.58 +| "doProofStep2 a (Root cid clause) rcs = do { Array.upd cid (Some (remdups (sort clause))) a; return (clause # rcs) }"
    4.59  | "doProofStep2 a (Xstep cid1 cid2) rcs = raise ''MiniSatChecked.doProofStep: Xstep constructor found.''"
    4.60  | "doProofStep2 a (ProofDone b) rcs = raise ''MiniSatChecked.doProofStep: ProofDone constructor found.''"
    4.61