src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy
changeset 37802 f2e9c104cebd
parent 37798 0b0570445a2a
child 37805 0f797d586ce5
     1.1 --- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Tue Jul 13 11:23:21 2010 +0100
     1.2 +++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Tue Jul 13 15:34:02 2010 +0200
     1.3 @@ -22,7 +22,7 @@
     1.4       }"
     1.5  
     1.6  lemma crel_swapI [crel_intros]:
     1.7 -  assumes "i < Array.length a h" "j < Array.length a h"
     1.8 +  assumes "i < Array.length h a" "j < Array.length h a"
     1.9      "x = get_array a h ! i" "y = get_array a h ! j"
    1.10      "h' = Array.update a j x (Array.update a i y h)"
    1.11    shows "crel (swap a i j) h h' r"
    1.12 @@ -108,7 +108,7 @@
    1.13  
    1.14  lemma part_length_remains:
    1.15    assumes "crel (part1 a l r p) h h' rs"
    1.16 -  shows "Array.length a h = Array.length a h'"
    1.17 +  shows "Array.length h a = Array.length h' a"
    1.18  using assms
    1.19  proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
    1.20    case (1 a l r p h h' rs)
    1.21 @@ -250,7 +250,7 @@
    1.22  
    1.23  lemma partition_length_remains:
    1.24    assumes "crel (partition a l r) h h' rs"
    1.25 -  shows "Array.length a h = Array.length a h'"
    1.26 +  shows "Array.length h a = Array.length h' a"
    1.27  proof -
    1.28    from assms part_length_remains show ?thesis
    1.29      unfolding partition.simps swap_def
    1.30 @@ -298,10 +298,10 @@
    1.31      (Array.update a rs (get_array a h1 ! r) h1)"
    1.32      unfolding swap_def
    1.33      by (elim crel_bindE crel_returnE crel_nthE crel_updE) simp
    1.34 -  from swap have in_bounds: "r < Array.length a h1 \<and> rs < Array.length a h1"
    1.35 +  from swap have in_bounds: "r < Array.length h1 a \<and> rs < Array.length h1 a"
    1.36      unfolding swap_def
    1.37      by (elim crel_bindE crel_returnE crel_nthE crel_updE) simp
    1.38 -  from swap have swap_length_remains: "Array.length a h1 = Array.length a h'"
    1.39 +  from swap have swap_length_remains: "Array.length h1 a = Array.length h' a"
    1.40      unfolding swap_def by (elim crel_bindE crel_returnE crel_nthE crel_updE) auto
    1.41    from `l < r` have "l \<le> r - 1" by simp
    1.42    note middle_in_bounds = part_returns_index_in_bounds[OF part this]
    1.43 @@ -321,7 +321,7 @@
    1.44        fix i
    1.45        assume i_is_left: "l \<le> i \<and> i < rs"
    1.46        with swap_length_remains in_bounds middle_in_bounds rs_equals `l < r`
    1.47 -      have i_props: "i < Array.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
    1.48 +      have i_props: "i < Array.length h' a" "i \<noteq> r" "i \<noteq> rs" by auto
    1.49        from i_is_left rs_equals have "l \<le> i \<and> i < middle \<or> i = middle" by arith
    1.50        with part_partitions[OF part] right_remains True
    1.51        have "get_array a h1 ! i \<le> get_array a h' ! rs" by fastsimp
    1.52 @@ -338,7 +338,7 @@
    1.53        proof
    1.54          assume i_is: "rs < i \<and> i \<le> r - 1"
    1.55          with swap_length_remains in_bounds middle_in_bounds rs_equals
    1.56 -        have i_props: "i < Array.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
    1.57 +        have i_props: "i < Array.length h' a" "i \<noteq> r" "i \<noteq> rs" by auto
    1.58          from part_partitions[OF part] rs_equals right_remains i_is
    1.59          have "get_array a h' ! rs \<le> get_array a h1 ! i"
    1.60            by fastsimp
    1.61 @@ -364,7 +364,7 @@
    1.62        fix i
    1.63        assume i_is_left: "l \<le> i \<and> i < rs"
    1.64        with swap_length_remains in_bounds middle_in_bounds rs_equals
    1.65 -      have i_props: "i < Array.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
    1.66 +      have i_props: "i < Array.length h' a" "i \<noteq> r" "i \<noteq> rs" by auto
    1.67        from part_partitions[OF part] rs_equals right_remains i_is_left
    1.68        have "get_array a h1 ! i \<le> get_array a h' ! rs" by fastsimp
    1.69        with i_props h'_def have "get_array a h' ! i \<le> get_array a h' ! rs"
    1.70 @@ -379,7 +379,7 @@
    1.71        proof
    1.72          assume i_is: "rs < i \<and> i \<le> r - 1"
    1.73          with swap_length_remains in_bounds middle_in_bounds rs_equals
    1.74 -        have i_props: "i < Array.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
    1.75 +        have i_props: "i < Array.length h' a" "i \<noteq> r" "i \<noteq> rs" by auto
    1.76          from part_partitions[OF part] rs_equals right_remains i_is
    1.77          have "get_array a h' ! rs \<le> get_array a h1 ! i"
    1.78            by fastsimp
    1.79 @@ -432,7 +432,7 @@
    1.80  
    1.81  lemma length_remains:
    1.82    assumes "crel (quicksort a l r) h h' rs"
    1.83 -  shows "Array.length a h = Array.length a h'"
    1.84 +  shows "Array.length h a = Array.length h' a"
    1.85  using assms
    1.86  proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
    1.87    case (1 a l r h h' rs)
    1.88 @@ -489,7 +489,7 @@
    1.89   
    1.90  lemma quicksort_sorts:
    1.91    assumes "crel (quicksort a l r) h h' rs"
    1.92 -  assumes l_r_length: "l < Array.length a h" "r < Array.length a h" 
    1.93 +  assumes l_r_length: "l < Array.length h a" "r < Array.length h a" 
    1.94    shows "sorted (subarray l (r + 1) a h')"
    1.95    using assms
    1.96  proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
    1.97 @@ -563,7 +563,7 @@
    1.98  
    1.99  
   1.100  lemma quicksort_is_sort:
   1.101 -  assumes crel: "crel (quicksort a 0 (Array.length a h - 1)) h h' rs"
   1.102 +  assumes crel: "crel (quicksort a 0 (Array.length h a - 1)) h h' rs"
   1.103    shows "get_array a h' = sort (get_array a h)"
   1.104  proof (cases "get_array a h = []")
   1.105    case True
   1.106 @@ -583,7 +583,7 @@
   1.107  We will now show that exceptions do not occur. *}
   1.108  
   1.109  lemma success_part1I: 
   1.110 -  assumes "l < Array.length a h" "r < Array.length a h"
   1.111 +  assumes "l < Array.length h a" "r < Array.length h a"
   1.112    shows "success (part1 a l r p) h"
   1.113    using assms
   1.114  proof (induct a l r p arbitrary: h rule: part1.induct)
   1.115 @@ -606,7 +606,7 @@
   1.116  qed
   1.117  
   1.118  lemma success_partitionI:
   1.119 -  assumes "l < r" "l < Array.length a h" "r < Array.length a h"
   1.120 +  assumes "l < r" "l < Array.length h a" "r < Array.length h a"
   1.121    shows "success (partition a l r) h"
   1.122  using assms unfolding partition.simps swap_def
   1.123  apply (auto intro!: success_bindI' success_ifI success_returnI success_nthI success_updI success_part1I elim!: crel_bindE crel_updE crel_nthE crel_returnE simp add:)
   1.124 @@ -621,7 +621,7 @@
   1.125  done
   1.126  
   1.127  lemma success_quicksortI:
   1.128 -  assumes "l < Array.length a h" "r < Array.length a h"
   1.129 +  assumes "l < Array.length h a" "r < Array.length h a"
   1.130    shows "success (quicksort a l r) h"
   1.131  using assms
   1.132  proof (induct a l r arbitrary: h rule: quicksort.induct)