# HG changeset patch # User haftmann # Date 1237831294 -3600 # Node ID 55ef8e0459315463e19f9bc3c436b661d2dd2761 # Parent df8a3c2fd5a214c25b5943f57910a326c059d134# Parent b14b2cc4e25e5fc0531a056118ed20053325458a merged diff -r df8a3c2fd5a2 -r 55ef8e045931 doc-src/HOL/HOL.tex --- a/doc-src/HOL/HOL.tex Mon Mar 23 15:33:35 2009 +0100 +++ b/doc-src/HOL/HOL.tex Mon Mar 23 19:01:34 2009 +0100 @@ -1427,7 +1427,7 @@ provides a decision procedure for \emph{linear arithmetic}: formulae involving addition and subtraction. The simplifier invokes a weak version of this decision procedure automatically. If this is not sufficent, you can invoke the -full procedure \ttindex{arith_tac} explicitly. It copes with arbitrary +full procedure \ttindex{linear_arith_tac} explicitly. It copes with arbitrary formulae involving {\tt=}, {\tt<}, {\tt<=}, {\tt+}, {\tt-}, {\tt Suc}, {\tt min}, {\tt max} and numerical constants. Other subterms are treated as atomic, while subformulae not involving numerical types are ignored. Quantified @@ -1438,10 +1438,10 @@ If {\tt k} is a numeral, then {\tt div k}, {\tt mod k} and {\tt k dvd} are also supported. The former two are eliminated by case distinctions, again blowing up the running time. -If the formula involves explicit quantifiers, \texttt{arith_tac} may take +If the formula involves explicit quantifiers, \texttt{linear_arith_tac} may take super-exponential time and space. -If \texttt{arith_tac} fails, try to find relevant arithmetic results in +If \texttt{linear_arith_tac} fails, try to find relevant arithmetic results in the library. The theories \texttt{Nat} and \texttt{NatArith} contain theorems about {\tt<}, {\tt<=}, \texttt{+}, \texttt{-} and \texttt{*}. Theory \texttt{Divides} contains theorems about \texttt{div} and diff -r df8a3c2fd5a2 -r 55ef8e045931 src/HOL/Decision_Procs/Ferrack.thy --- a/src/HOL/Decision_Procs/Ferrack.thy Mon Mar 23 15:33:35 2009 +0100 +++ b/src/HOL/Decision_Procs/Ferrack.thy Mon Mar 23 19:01:34 2009 +0100 @@ -1995,6 +1995,8 @@ "ferrack_test u = linrqe (A (A (Imp (Lt (Sub (Bound 1) (Bound 0))) (E (Eq (Sub (Add (Bound 0) (Bound 2)) (Bound 1)))))))" +code_reserved SML oo + ML {* @{code ferrack_test} () *} oracle linr_oracle = {* diff -r df8a3c2fd5a2 -r 55ef8e045931 src/HOL/HoareParallel/OG_Examples.thy --- a/src/HOL/HoareParallel/OG_Examples.thy Mon Mar 23 15:33:35 2009 +0100 +++ b/src/HOL/HoareParallel/OG_Examples.thy Mon Mar 23 19:01:34 2009 +0100 @@ -443,7 +443,7 @@ --{* 32 subgoals left *} apply(tactic {* ALLGOALS (clarify_tac @{claset}) *}) -apply(tactic {* TRYALL (simple_arith_tac @{context}) *}) +apply(tactic {* TRYALL (linear_arith_tac @{context}) *}) --{* 9 subgoals left *} apply (force simp add:less_Suc_eq) apply(drule sym) diff -r df8a3c2fd5a2 -r 55ef8e045931 src/HOL/Imperative_HOL/ROOT.ML --- a/src/HOL/Imperative_HOL/ROOT.ML Mon Mar 23 15:33:35 2009 +0100 +++ b/src/HOL/Imperative_HOL/ROOT.ML Mon Mar 23 19:01:34 2009 +0100 @@ -1,2 +1,2 @@ -use_thy "Imperative_HOL"; +use_thy "Imperative_HOL_ex"; diff -r df8a3c2fd5a2 -r 55ef8e045931 src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy Mon Mar 23 19:01:34 2009 +0100 @@ -0,0 +1,639 @@ +(* Author: Lukas Bulwahn, TU Muenchen *) + +theory Imperative_Quicksort +imports "~~/src/HOL/Imperative_HOL/Imperative_HOL" Subarray Multiset Efficient_Nat +begin + +text {* We prove QuickSort correct in the Relational Calculus. *} + +definition swap :: "nat array \ nat \ nat \ unit Heap" +where + "swap arr i j = ( + do + x \ nth arr i; + y \ nth arr j; + upd i y arr; + upd j x arr; + return () + done)" + +lemma swap_permutes: + assumes "crel (swap a i j) h h' rs" + shows "multiset_of (get_array a h') + = multiset_of (get_array a h)" + using assms + unfolding swap_def + by (auto simp add: Heap.length_def multiset_of_swap dest: sym [of _ "h'"] elim!: crelE crel_nth crel_return crel_upd) + +function part1 :: "nat array \ nat \ nat \ nat \ nat Heap" +where + "part1 a left right p = ( + if (right \ left) then return right + else (do + v \ nth a left; + (if (v \ p) then (part1 a (left + 1) right p) + else (do swap a left right; + part1 a left (right - 1) p done)) + done))" +by pat_completeness auto + +termination +by (relation "measure (\(_,l,r,_). r - l )") auto + +declare part1.simps[simp del] + +lemma part_permutes: + assumes "crel (part1 a l r p) h h' rs" + shows "multiset_of (get_array a h') + = multiset_of (get_array a h)" + using assms +proof (induct a l r p arbitrary: h h' rs rule:part1.induct) + case (1 a l r p h h' rs) + thus ?case + unfolding part1.simps [of a l r p] + by (elim crelE crel_if crel_return crel_nth) (auto simp add: swap_permutes) +qed + +lemma part_returns_index_in_bounds: + assumes "crel (part1 a l r p) h h' rs" + assumes "l \ r" + shows "l \ rs \ rs \ r" +using assms +proof (induct a l r p arbitrary: h h' rs rule:part1.induct) + case (1 a l r p h h' rs) + note cr = `crel (part1 a l r p) h h' rs` + show ?case + proof (cases "r \ l") + case True (* Terminating case *) + with cr `l \ r` show ?thesis + unfolding part1.simps[of a l r p] + by (elim crelE crel_if crel_return crel_nth) auto + next + case False (* recursive case *) + note rec_condition = this + let ?v = "get_array a h ! l" + show ?thesis + proof (cases "?v \ p") + case True + with cr False + have rec1: "crel (part1 a (l + 1) r p) h h' rs" + unfolding part1.simps[of a l r p] + by (elim crelE crel_nth crel_if crel_return) auto + from rec_condition have "l + 1 \ r" by arith + from 1(1)[OF rec_condition True rec1 `l + 1 \ r`] + show ?thesis by simp + next + case False + with rec_condition cr + obtain h1 where swp: "crel (swap a l r) h h1 ()" + and rec2: "crel (part1 a l (r - 1) p) h1 h' rs" + unfolding part1.simps[of a l r p] + by (elim crelE crel_nth crel_if crel_return) auto + from rec_condition have "l \ r - 1" by arith + from 1(2) [OF rec_condition False rec2 `l \ r - 1`] show ?thesis by fastsimp + qed + qed +qed + +lemma part_length_remains: + assumes "crel (part1 a l r p) h h' rs" + shows "Heap.length a h = Heap.length a h'" +using assms +proof (induct a l r p arbitrary: h h' rs rule:part1.induct) + case (1 a l r p h h' rs) + note cr = `crel (part1 a l r p) h h' rs` + + show ?case + proof (cases "r \ l") + case True (* Terminating case *) + with cr show ?thesis + unfolding part1.simps[of a l r p] + by (elim crelE crel_if crel_return crel_nth) auto + next + case False (* recursive case *) + with cr 1 show ?thesis + unfolding part1.simps [of a l r p] swap_def + by (auto elim!: crelE crel_if crel_nth crel_return crel_upd) fastsimp + qed +qed + +lemma part_outer_remains: + assumes "crel (part1 a l r p) h h' rs" + shows "\i. i < l \ r < i \ get_array (a::nat array) h ! i = get_array a h' ! i" + using assms +proof (induct a l r p arbitrary: h h' rs rule:part1.induct) + case (1 a l r p h h' rs) + note cr = `crel (part1 a l r p) h h' rs` + + show ?case + proof (cases "r \ l") + case True (* Terminating case *) + with cr show ?thesis + unfolding part1.simps[of a l r p] + by (elim crelE crel_if crel_return crel_nth) auto + next + case False (* recursive case *) + note rec_condition = this + let ?v = "get_array a h ! l" + show ?thesis + proof (cases "?v \ p") + case True + with cr False + have rec1: "crel (part1 a (l + 1) r p) h h' rs" + unfolding part1.simps[of a l r p] + by (elim crelE crel_nth crel_if crel_return) auto + from 1(1)[OF rec_condition True rec1] + show ?thesis by fastsimp + next + case False + with rec_condition cr + obtain h1 where swp: "crel (swap a l r) h h1 ()" + and rec2: "crel (part1 a l (r - 1) p) h1 h' rs" + unfolding part1.simps[of a l r p] + by (elim crelE crel_nth crel_if crel_return) auto + from swp rec_condition have + "\i. i < l \ r < i \ get_array a h ! i = get_array a h1 ! i" + unfolding swap_def + by (elim crelE crel_nth crel_upd crel_return) auto + with 1(2) [OF rec_condition False rec2] show ?thesis by fastsimp + qed + qed +qed + + +lemma part_partitions: + assumes "crel (part1 a l r p) h h' rs" + shows "(\i. l \ i \ i < rs \ get_array (a::nat array) h' ! i \ p) + \ (\i. rs < i \ i \ r \ get_array a h' ! i \ p)" + using assms +proof (induct a l r p arbitrary: h h' rs rule:part1.induct) + case (1 a l r p h h' rs) + note cr = `crel (part1 a l r p) h h' rs` + + show ?case + proof (cases "r \ l") + case True (* Terminating case *) + with cr have "rs = r" + unfolding part1.simps[of a l r p] + by (elim crelE crel_if crel_return crel_nth) auto + with True + show ?thesis by auto + next + case False (* recursive case *) + note lr = this + let ?v = "get_array a h ! l" + show ?thesis + proof (cases "?v \ p") + case True + with lr cr + have rec1: "crel (part1 a (l + 1) r p) h h' rs" + unfolding part1.simps[of a l r p] + by (elim crelE crel_nth crel_if crel_return) auto + from True part_outer_remains[OF rec1] have a_l: "get_array a h' ! l \ p" + by fastsimp + have "\i. (l \ i = (l = i \ Suc l \ i))" by arith + with 1(1)[OF False True rec1] a_l show ?thesis + by auto + next + case False + with lr cr + obtain h1 where swp: "crel (swap a l r) h h1 ()" + and rec2: "crel (part1 a l (r - 1) p) h1 h' rs" + unfolding part1.simps[of a l r p] + by (elim crelE crel_nth crel_if crel_return) auto + from swp False have "get_array a h1 ! r \ p" + unfolding swap_def + by (auto simp add: Heap.length_def elim!: crelE crel_nth crel_upd crel_return) + with part_outer_remains [OF rec2] lr have a_r: "get_array a h' ! r \ p" + by fastsimp + have "\i. (i \ r = (i = r \ i \ r - 1))" by arith + with 1(2)[OF lr False rec2] a_r show ?thesis + by auto + qed + qed +qed + + +fun partition :: "nat array \ nat \ nat \ nat Heap" +where + "partition a left right = (do + pivot \ nth a right; + middle \ part1 a left (right - 1) pivot; + v \ nth a middle; + m \ return (if (v \ pivot) then (middle + 1) else middle); + swap a m right; + return m + done)" + +declare partition.simps[simp del] + +lemma partition_permutes: + assumes "crel (partition a l r) h h' rs" + shows "multiset_of (get_array a h') + = multiset_of (get_array a h)" +proof - + from assms part_permutes swap_permutes show ?thesis + unfolding partition.simps + by (elim crelE crel_return crel_nth crel_if crel_upd) auto +qed + +lemma partition_length_remains: + assumes "crel (partition a l r) h h' rs" + shows "Heap.length a h = Heap.length a h'" +proof - + from assms part_length_remains show ?thesis + unfolding partition.simps swap_def + by (elim crelE crel_return crel_nth crel_if crel_upd) auto +qed + +lemma partition_outer_remains: + assumes "crel (partition a l r) h h' rs" + assumes "l < r" + shows "\i. i < l \ r < i \ get_array (a::nat array) h ! i = get_array a h' ! i" +proof - + from assms part_outer_remains part_returns_index_in_bounds show ?thesis + unfolding partition.simps swap_def + by (elim crelE crel_return crel_nth crel_if crel_upd) fastsimp +qed + +lemma partition_returns_index_in_bounds: + assumes crel: "crel (partition a l r) h h' rs" + assumes "l < r" + shows "l \ rs \ rs \ r" +proof - + from crel obtain middle h'' p where part: "crel (part1 a l (r - 1) p) h h'' middle" + and rs_equals: "rs = (if get_array a h'' ! middle \ get_array a h ! r then middle + 1 + else middle)" + unfolding partition.simps + by (elim crelE crel_return crel_nth crel_if crel_upd) simp + from `l < r` have "l \ r - 1" by arith + from part_returns_index_in_bounds[OF part this] rs_equals `l < r` show ?thesis by auto +qed + +lemma partition_partitions: + assumes crel: "crel (partition a l r) h h' rs" + assumes "l < r" + shows "(\i. l \ i \ i < rs \ get_array (a::nat array) h' ! i \ get_array a h' ! rs) \ + (\i. rs < i \ i \ r \ get_array a h' ! rs \ get_array a h' ! i)" +proof - + let ?pivot = "get_array a h ! r" + from crel obtain middle h1 where part: "crel (part1 a l (r - 1) ?pivot) h h1 middle" + and swap: "crel (swap a rs r) h1 h' ()" + and rs_equals: "rs = (if get_array a h1 ! middle \ ?pivot then middle + 1 + else middle)" + unfolding partition.simps + by (elim crelE crel_return crel_nth crel_if crel_upd) simp + from swap have h'_def: "h' = Heap.upd a r (get_array a h1 ! rs) + (Heap.upd a rs (get_array a h1 ! r) h1)" + unfolding swap_def + by (elim crelE crel_return crel_nth crel_upd) simp + from swap have in_bounds: "r < Heap.length a h1 \ rs < Heap.length a h1" + unfolding swap_def + by (elim crelE crel_return crel_nth crel_upd) simp + from swap have swap_length_remains: "Heap.length a h1 = Heap.length a h'" + unfolding swap_def by (elim crelE crel_return crel_nth crel_upd) auto + from `l < r` have "l \ r - 1" by simp + note middle_in_bounds = part_returns_index_in_bounds[OF part this] + from part_outer_remains[OF part] `l < r` + have "get_array a h ! r = get_array a h1 ! r" + by fastsimp + with swap + have right_remains: "get_array a h ! r = get_array a h' ! rs" + unfolding swap_def + by (auto simp add: Heap.length_def elim!: crelE crel_return crel_nth crel_upd) (cases "r = rs", auto) + from part_partitions [OF part] + show ?thesis + proof (cases "get_array a h1 ! middle \ ?pivot") + case True + with rs_equals have rs_equals: "rs = middle + 1" by simp + { + fix i + assume i_is_left: "l \ i \ i < rs" + with swap_length_remains in_bounds middle_in_bounds rs_equals `l < r` + have i_props: "i < Heap.length a h'" "i \ r" "i \ rs" by auto + from i_is_left rs_equals have "l \ i \ i < middle \ i = middle" by arith + with part_partitions[OF part] right_remains True + have "get_array a h1 ! i \ get_array a h' ! rs" by fastsimp + with i_props h'_def in_bounds have "get_array a h' ! i \ get_array a h' ! rs" + unfolding Heap.upd_def Heap.length_def by simp + } + moreover + { + fix i + assume "rs < i \ i \ r" + + hence "(rs < i \ i \ r - 1) \ (rs < i \ i = r)" by arith + hence "get_array a h' ! rs \ get_array a h' ! i" + proof + assume i_is: "rs < i \ i \ r - 1" + with swap_length_remains in_bounds middle_in_bounds rs_equals + have i_props: "i < Heap.length a h'" "i \ r" "i \ rs" by auto + from part_partitions[OF part] rs_equals right_remains i_is + have "get_array a h' ! rs \ get_array a h1 ! i" + by fastsimp + with i_props h'_def show ?thesis by fastsimp + next + assume i_is: "rs < i \ i = r" + with rs_equals have "Suc middle \ r" by arith + with middle_in_bounds `l < r` have "Suc middle \ r - 1" by arith + with part_partitions[OF part] right_remains + have "get_array a h' ! rs \ get_array a h1 ! (Suc middle)" + by fastsimp + with i_is True rs_equals right_remains h'_def + show ?thesis using in_bounds + unfolding Heap.upd_def Heap.length_def + by auto + qed + } + ultimately show ?thesis by auto + next + case False + with rs_equals have rs_equals: "middle = rs" by simp + { + fix i + assume i_is_left: "l \ i \ i < rs" + with swap_length_remains in_bounds middle_in_bounds rs_equals + have i_props: "i < Heap.length a h'" "i \ r" "i \ rs" by auto + from part_partitions[OF part] rs_equals right_remains i_is_left + have "get_array a h1 ! i \ get_array a h' ! rs" by fastsimp + with i_props h'_def have "get_array a h' ! i \ get_array a h' ! rs" + unfolding Heap.upd_def by simp + } + moreover + { + fix i + assume "rs < i \ i \ r" + hence "(rs < i \ i \ r - 1) \ i = r" by arith + hence "get_array a h' ! rs \ get_array a h' ! i" + proof + assume i_is: "rs < i \ i \ r - 1" + with swap_length_remains in_bounds middle_in_bounds rs_equals + have i_props: "i < Heap.length a h'" "i \ r" "i \ rs" by auto + from part_partitions[OF part] rs_equals right_remains i_is + have "get_array a h' ! rs \ get_array a h1 ! i" + by fastsimp + with i_props h'_def show ?thesis by fastsimp + next + assume i_is: "i = r" + from i_is False rs_equals right_remains h'_def + show ?thesis using in_bounds + unfolding Heap.upd_def Heap.length_def + by auto + qed + } + ultimately + show ?thesis by auto + qed +qed + + +function quicksort :: "nat array \ nat \ nat \ unit Heap" +where + "quicksort arr left right = + (if (right > left) then + do + pivotNewIndex \ partition arr left right; + pivotNewIndex \ assert (\x. left \ x \ x \ right) pivotNewIndex; + quicksort arr left (pivotNewIndex - 1); + quicksort arr (pivotNewIndex + 1) right + done + else return ())" +by pat_completeness auto + +(* For termination, we must show that the pivotNewIndex is between left and right *) +termination +by (relation "measure (\(a, l, r). (r - l))") auto + +declare quicksort.simps[simp del] + + +lemma quicksort_permutes: + assumes "crel (quicksort a l r) h h' rs" + shows "multiset_of (get_array a h') + = multiset_of (get_array a h)" + using assms +proof (induct a l r arbitrary: h h' rs rule: quicksort.induct) + case (1 a l r h h' rs) + with partition_permutes show ?case + unfolding quicksort.simps [of a l r] + by (elim crel_if crelE crel_assert crel_return) auto +qed + +lemma length_remains: + assumes "crel (quicksort a l r) h h' rs" + shows "Heap.length a h = Heap.length a h'" +using assms +proof (induct a l r arbitrary: h h' rs rule: quicksort.induct) + case (1 a l r h h' rs) + with partition_length_remains show ?case + unfolding quicksort.simps [of a l r] + by (elim crel_if crelE crel_assert crel_return) auto +qed + +lemma quicksort_outer_remains: + assumes "crel (quicksort a l r) h h' rs" + shows "\i. i < l \ r < i \ get_array (a::nat array) h ! i = get_array a h' ! i" + using assms +proof (induct a l r arbitrary: h h' rs rule: quicksort.induct) + case (1 a l r h h' rs) + note cr = `crel (quicksort a l r) h h' rs` + thus ?case + proof (cases "r > l") + case False + with cr have "h' = h" + unfolding quicksort.simps [of a l r] + by (elim crel_if crel_return) auto + thus ?thesis by simp + next + case True + { + fix h1 h2 p ret1 ret2 i + assume part: "crel (partition a l r) h h1 p" + assume qs1: "crel (quicksort a l (p - 1)) h1 h2 ret1" + assume qs2: "crel (quicksort a (p + 1) r) h2 h' ret2" + assume pivot: "l \ p \ p \ r" + assume i_outer: "i < l \ r < i" + from partition_outer_remains [OF part True] i_outer + have "get_array a h !i = get_array a h1 ! i" by fastsimp + moreover + with 1(1) [OF True pivot qs1] pivot i_outer + have "get_array a h1 ! i = get_array a h2 ! i" by auto + moreover + with qs2 1(2) [of p h2 h' ret2] True pivot i_outer + have "get_array a h2 ! i = get_array a h' ! i" by auto + ultimately have "get_array a h ! i= get_array a h' ! i" by simp + } + with cr show ?thesis + unfolding quicksort.simps [of a l r] + by (elim crel_if crelE crel_assert crel_return) auto + qed +qed + +lemma quicksort_is_skip: + assumes "crel (quicksort a l r) h h' rs" + shows "r \ l \ h = h'" + using assms + unfolding quicksort.simps [of a l r] + by (elim crel_if crel_return) auto + +lemma quicksort_sorts: + assumes "crel (quicksort a l r) h h' rs" + assumes l_r_length: "l < Heap.length a h" "r < Heap.length a h" + shows "sorted (subarray l (r + 1) a h')" + using assms +proof (induct a l r arbitrary: h h' rs rule: quicksort.induct) + case (1 a l r h h' rs) + note cr = `crel (quicksort a l r) h h' rs` + thus ?case + proof (cases "r > l") + case False + hence "l \ r + 1 \ l = r" by arith + with length_remains[OF cr] 1(5) show ?thesis + by (auto simp add: subarray_Nil subarray_single) + next + case True + { + fix h1 h2 p + assume part: "crel (partition a l r) h h1 p" + assume qs1: "crel (quicksort a l (p - 1)) h1 h2 ()" + assume qs2: "crel (quicksort a (p + 1) r) h2 h' ()" + from partition_returns_index_in_bounds [OF part True] + have pivot: "l\ p \ p \ r" . + note length_remains = length_remains[OF qs2] length_remains[OF qs1] partition_length_remains[OF part] + from quicksort_outer_remains [OF qs2] quicksort_outer_remains [OF qs1] pivot quicksort_is_skip[OF qs1] + have pivot_unchanged: "get_array a h1 ! p = get_array a h' ! p" by (cases p, auto) + (*-- First of all, by induction hypothesis both sublists are sorted. *) + from 1(1)[OF True pivot qs1] length_remains pivot 1(5) + have IH1: "sorted (subarray l p a h2)" by (cases p, auto simp add: subarray_Nil) + from quicksort_outer_remains [OF qs2] length_remains + have left_subarray_remains: "subarray l p a h2 = subarray l p a h'" + by (simp add: subarray_eq_samelength_iff) + with IH1 have IH1': "sorted (subarray l p a h')" by simp + from 1(2)[OF True pivot qs2] pivot 1(5) length_remains + have IH2: "sorted (subarray (p + 1) (r + 1) a h')" + by (cases "Suc p \ r", auto simp add: subarray_Nil) + (* -- Secondly, both sublists remain partitioned. *) + from partition_partitions[OF part True] + have part_conds1: "\j. j \ set (subarray l p a h1) \ j \ get_array a h1 ! p " + and part_conds2: "\j. j \ set (subarray (p + 1) (r + 1) a h1) \ get_array a h1 ! p \ j" + by (auto simp add: all_in_set_subarray_conv) + from quicksort_outer_remains [OF qs1] quicksort_permutes [OF qs1] True + length_remains 1(5) pivot multiset_of_sublist [of l p "get_array a h1" "get_array a h2"] + have multiset_partconds1: "multiset_of (subarray l p a h2) = multiset_of (subarray l p a h1)" + unfolding Heap.length_def subarray_def by (cases p, auto) + with left_subarray_remains part_conds1 pivot_unchanged + have part_conds2': "\j. j \ set (subarray l p a h') \ j \ get_array a h' ! p" + by (simp, subst set_of_multiset_of[symmetric], simp) + (* -- These steps are the analogous for the right sublist \ *) + from quicksort_outer_remains [OF qs1] length_remains + have right_subarray_remains: "subarray (p + 1) (r + 1) a h1 = subarray (p + 1) (r + 1) a h2" + by (auto simp add: subarray_eq_samelength_iff) + from quicksort_outer_remains [OF qs2] quicksort_permutes [OF qs2] True + length_remains 1(5) pivot multiset_of_sublist [of "p + 1" "r + 1" "get_array a h2" "get_array a h'"] + have multiset_partconds2: "multiset_of (subarray (p + 1) (r + 1) a h') = multiset_of (subarray (p + 1) (r + 1) a h2)" + unfolding Heap.length_def subarray_def by auto + with right_subarray_remains part_conds2 pivot_unchanged + have part_conds1': "\j. j \ set (subarray (p + 1) (r + 1) a h') \ get_array a h' ! p \ j" + by (simp, subst set_of_multiset_of[symmetric], simp) + (* -- Thirdly and finally, we show that the array is sorted + following from the facts above. *) + from True pivot 1(5) length_remains have "subarray l (r + 1) a h' = subarray l p a h' @ [get_array a h' ! p] @ subarray (p + 1) (r + 1) a h'" + by (simp add: subarray_nth_array_Cons, cases "l < p") (auto simp add: subarray_append subarray_Nil) + with IH1' IH2 part_conds1' part_conds2' pivot have ?thesis + unfolding subarray_def + apply (auto simp add: sorted_append sorted_Cons all_in_set_sublist'_conv) + by (auto simp add: set_sublist' dest: le_trans [of _ "get_array a h' ! p"]) + } + with True cr show ?thesis + unfolding quicksort.simps [of a l r] + by (elim crel_if crel_return crelE crel_assert) auto + qed +qed + + +lemma quicksort_is_sort: + assumes crel: "crel (quicksort a 0 (Heap.length a h - 1)) h h' rs" + shows "get_array a h' = sort (get_array a h)" +proof (cases "get_array a h = []") + case True + with quicksort_is_skip[OF crel] show ?thesis + unfolding Heap.length_def by simp +next + case False + from quicksort_sorts [OF crel] False have "sorted (sublist' 0 (List.length (get_array a h)) (get_array a h'))" + unfolding Heap.length_def subarray_def by auto + with length_remains[OF crel] have "sorted (get_array a h')" + unfolding Heap.length_def by simp + with quicksort_permutes [OF crel] properties_for_sort show ?thesis by fastsimp +qed + +subsection {* No Errors in quicksort *} +text {* We have proved that quicksort sorts (if no exceptions occur). +We will now show that exceptions do not occur. *} + +lemma noError_part1: + assumes "l < Heap.length a h" "r < Heap.length a h" + shows "noError (part1 a l r p) h" + using assms +proof (induct a l r p arbitrary: h rule: part1.induct) + case (1 a l r p) + thus ?case + unfolding part1.simps [of a l r] swap_def + by (auto intro!: noError_if noErrorI noError_return noError_nth noError_upd elim!: crelE crel_upd crel_nth crel_return) +qed + +lemma noError_partition: + assumes "l < r" "l < Heap.length a h" "r < Heap.length a h" + shows "noError (partition a l r) h" +using assms +unfolding partition.simps swap_def +apply (auto intro!: noError_if noErrorI noError_return noError_nth noError_upd noError_part1 elim!: crelE crel_upd crel_nth crel_return) +apply (frule part_length_remains) +apply (frule part_returns_index_in_bounds) +apply auto +apply (frule part_length_remains) +apply (frule part_returns_index_in_bounds) +apply auto +apply (frule part_length_remains) +apply auto +done + +lemma noError_quicksort: + assumes "l < Heap.length a h" "r < Heap.length a h" + shows "noError (quicksort a l r) h" +using assms +proof (induct a l r arbitrary: h rule: quicksort.induct) + case (1 a l ri h) + thus ?case + unfolding quicksort.simps [of a l ri] + apply (auto intro!: noError_if noErrorI noError_return noError_nth noError_upd noError_assert noError_partition) + apply (frule partition_returns_index_in_bounds) + apply auto + apply (frule partition_returns_index_in_bounds) + apply auto + apply (auto elim!: crel_assert dest!: partition_length_remains length_remains) + apply (subgoal_tac "Suc r \ ri \ r = ri") + apply (erule disjE) + apply auto + unfolding quicksort.simps [of a "Suc ri" ri] + apply (auto intro!: noError_if noError_return) + done +qed + + +subsection {* Example *} + +definition "qsort a = do + k \ length a; + quicksort a 0 (k - 1); + return a + done" + +ML {* @{code qsort} (Array.fromList [42, 2, 3, 5, 0, 1705, 8, 3, 15]) () *} + +export_code qsort in SML_imp module_name QSort +export_code qsort in OCaml module_name QSort file - +export_code qsort in OCaml_imp module_name QSort file - +export_code qsort in Haskell module_name QSort file - + +end \ No newline at end of file diff -r df8a3c2fd5a2 -r 55ef8e045931 src/HOL/Imperative_HOL/ex/Subarray.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Imperative_HOL/ex/Subarray.thy Mon Mar 23 19:01:34 2009 +0100 @@ -0,0 +1,66 @@ +theory Subarray +imports Array Sublist +begin + +definition subarray :: "nat \ nat \ ('a::heap) array \ heap \ 'a list" +where + "subarray n m a h \ sublist' n m (get_array a h)" + +lemma subarray_upd: "i \ m \ subarray n m a (Heap.upd a i v h) = subarray n m a h" +apply (simp add: subarray_def Heap.upd_def) +apply (simp add: sublist'_update1) +done + +lemma subarray_upd2: " i < n \ subarray n m a (Heap.upd a i v h) = subarray n m a h" +apply (simp add: subarray_def Heap.upd_def) +apply (subst sublist'_update2) +apply fastsimp +apply simp +done + +lemma subarray_upd3: "\ n \ i; i < m\ \ subarray n m a (Heap.upd a i v h) = subarray n m a h[i - n := v]" +unfolding subarray_def Heap.upd_def +by (simp add: sublist'_update3) + +lemma subarray_Nil: "n \ m \ subarray n m a h = []" +by (simp add: subarray_def sublist'_Nil') + +lemma subarray_single: "\ n < Heap.length a h \ \ subarray n (Suc n) a h = [get_array a h ! n]" +by (simp add: subarray_def Heap.length_def sublist'_single) + +lemma length_subarray: "m \ Heap.length a h \ List.length (subarray n m a h) = m - n" +by (simp add: subarray_def Heap.length_def length_sublist') + +lemma length_subarray_0: "m \ Heap.length a h \ List.length (subarray 0 m a h) = m" +by (simp add: length_subarray) + +lemma subarray_nth_array_Cons: "\ i < Heap.length a h; i < j \ \ (get_array a h ! i) # subarray (Suc i) j a h = subarray i j a h" +unfolding Heap.length_def subarray_def +by (simp add: sublist'_front) + +lemma subarray_nth_array_back: "\ i < j; j \ Heap.length a h\ \ subarray i j a h = subarray i (j - 1) a h @ [get_array a h ! (j - 1)]" +unfolding Heap.length_def subarray_def +by (simp add: sublist'_back) + +lemma subarray_append: "\ i < j; j < k \ \ subarray i j a h @ subarray j k a h = subarray i k a h" +unfolding subarray_def +by (simp add: sublist'_append) + +lemma subarray_all: "subarray 0 (Heap.length a h) a h = get_array a h" +unfolding Heap.length_def subarray_def +by (simp add: sublist'_all) + +lemma nth_subarray: "\ k < j - i; j \ Heap.length a h \ \ subarray i j a h ! k = get_array a h ! (i + k)" +unfolding Heap.length_def subarray_def +by (simp add: nth_sublist') + +lemma subarray_eq_samelength_iff: "Heap.length a h = Heap.length a h' \ (subarray i j a h = subarray i j a h') = (\i'. i \ i' \ i' < j \ get_array a h ! i' = get_array a h' ! i')" +unfolding Heap.length_def subarray_def by (rule sublist'_eq_samelength_iff) + +lemma all_in_set_subarray_conv: "(\j. j \ set (subarray l r a h) \ P j) = (\k. l \ k \ k < r \ k < Heap.length a h \ P (get_array a h ! k))" +unfolding subarray_def Heap.length_def by (rule all_in_set_sublist'_conv) + +lemma ball_in_set_subarray_conv: "(\j \ set (subarray l r a h). P j) = (\k. l \ k \ k < r \ k < Heap.length a h \ P (get_array a h ! k))" +unfolding subarray_def Heap.length_def by (rule ball_in_set_sublist'_conv) + +end \ No newline at end of file diff -r df8a3c2fd5a2 -r 55ef8e045931 src/HOL/Imperative_HOL/ex/Sublist.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Imperative_HOL/ex/Sublist.thy Mon Mar 23 19:01:34 2009 +0100 @@ -0,0 +1,505 @@ +(* $Id$ *) + +header {* Slices of lists *} + +theory Sublist +imports Multiset +begin + + +lemma sublist_split: "i \ j \ j \ k \ sublist xs {i.. j - 1 \ j - 1 \ k - 1") +apply simp +apply (subgoal_tac "{ja. Suc ja < j} = {0.. Suc ja \ Suc ja < k} = {j - Suc 0.. Suc ja \ Suc ja < j} = {i - 1 .. Suc ja \ Suc ja < k} = {j - 1.. Suc j \ Suc j < k} = {i - 1.. j - 1 \ j - 1 \ k - 1") +apply simp +apply fastsimp +apply fastsimp +apply fastsimp +apply fastsimp +done + +lemma sublist_update1: "i \ inds \ sublist (xs[i := v]) inds = sublist xs inds" +apply (induct xs arbitrary: i inds) +apply simp +apply (case_tac i) +apply (simp add: sublist_Cons) +apply (simp add: sublist_Cons) +done + +lemma sublist_update2: "i \ inds \ sublist (xs[i := v]) inds = (sublist xs inds)[(card {k \ inds. k < i}):= v]" +proof (induct xs arbitrary: i inds) + case Nil thus ?case by simp +next + case (Cons x xs) + thus ?case + proof (cases i) + case 0 with Cons show ?thesis by (simp add: sublist_Cons) + next + case (Suc i') + with Cons show ?thesis + apply simp + apply (simp add: sublist_Cons) + apply auto + apply (auto simp add: nat.split) + apply (simp add: card_less_Suc[symmetric]) + apply (simp add: card_less_Suc2) + done + qed +qed + +lemma sublist_update: "sublist (xs[i := v]) inds = (if i \ inds then (sublist xs inds)[(card {k \ inds. k < i}) := v] else sublist xs inds)" +by (simp add: sublist_update1 sublist_update2) + +lemma sublist_take: "sublist xs {j. j < m} = take m xs" +apply (induct xs arbitrary: m) +apply simp +apply (case_tac m) +apply simp +apply (simp add: sublist_Cons) +done + +lemma sublist_take': "sublist xs {0.. sublist xs {a} = [xs ! a]" +apply (induct xs arbitrary: a) +apply simp +apply(case_tac aa) +apply simp +apply (simp add: sublist_Cons) +apply simp +apply (simp add: sublist_Cons) +done + +lemma sublist_is_Nil: "\i \ inds. i \ length xs \ sublist xs inds = []" +apply (induct xs arbitrary: inds) +apply simp +apply (simp add: sublist_Cons) +apply auto +apply (erule_tac x="{j. Suc j \ inds}" in meta_allE) +apply auto +done + +lemma sublist_Nil': "sublist xs inds = [] \ \i \ inds. i \ length xs" +apply (induct xs arbitrary: inds) +apply simp +apply (simp add: sublist_Cons) +apply (auto split: if_splits) +apply (erule_tac x="{j. Suc j \ inds}" in meta_allE) +apply (case_tac x, auto) +done + +lemma sublist_Nil[simp]: "(sublist xs inds = []) = (\i \ inds. i \ length xs)" +apply (induct xs arbitrary: inds) +apply simp +apply (simp add: sublist_Cons) +apply auto +apply (erule_tac x="{j. Suc j \ inds}" in meta_allE) +apply (case_tac x, auto) +done + +lemma sublist_eq_subseteq: " \ inds' \ inds; sublist xs inds = sublist ys inds \ \ sublist xs inds' = sublist ys inds'" +apply (induct xs arbitrary: ys inds inds') +apply simp +apply (drule sym, rule sym) +apply (simp add: sublist_Nil, fastsimp) +apply (case_tac ys) +apply (simp add: sublist_Nil, fastsimp) +apply (auto simp add: sublist_Cons) +apply (erule_tac x="list" in meta_allE) +apply (erule_tac x="{j. Suc j \ inds}" in meta_allE) +apply (erule_tac x="{j. Suc j \ inds'}" in meta_allE) +apply fastsimp +apply (erule_tac x="list" in meta_allE) +apply (erule_tac x="{j. Suc j \ inds}" in meta_allE) +apply (erule_tac x="{j. Suc j \ inds'}" in meta_allE) +apply fastsimp +done + +lemma sublist_eq: "\ \i \ inds. ((i < length xs) \ (i < length ys)) \ ((i \ length xs ) \ (i \ length ys)); \i \ inds. xs ! i = ys ! i \ \ sublist xs inds = sublist ys inds" +apply (induct xs arbitrary: ys inds) +apply simp +apply (rule sym, simp add: sublist_Nil) +apply (case_tac ys) +apply (simp add: sublist_Nil) +apply (auto simp add: sublist_Cons) +apply (erule_tac x="list" in meta_allE) +apply (erule_tac x="{j. Suc j \ inds}" in meta_allE) +apply fastsimp +apply (erule_tac x="list" in meta_allE) +apply (erule_tac x="{j. Suc j \ inds}" in meta_allE) +apply fastsimp +done + +lemma sublist_eq_samelength: "\ length xs = length ys; \i \ inds. xs ! i = ys ! i \ \ sublist xs inds = sublist ys inds" +by (rule sublist_eq, auto) + +lemma sublist_eq_samelength_iff: "length xs = length ys \ (sublist xs inds = sublist ys inds) = (\i \ inds. xs ! i = ys ! i)" +apply (induct xs arbitrary: ys inds) +apply simp +apply (rule sym, simp add: sublist_Nil) +apply (case_tac ys) +apply (simp add: sublist_Nil) +apply (auto simp add: sublist_Cons) +apply (case_tac i) +apply auto +apply (case_tac i) +apply auto +done + +section {* Another sublist function *} + +function sublist' :: "nat \ nat \ 'a list \ 'a list" +where + "sublist' n m [] = []" +| "sublist' n 0 xs = []" +| "sublist' 0 (Suc m) (x#xs) = (x#sublist' 0 m xs)" +| "sublist' (Suc n) (Suc m) (x#xs) = sublist' n m xs" +by pat_completeness auto +termination by lexicographic_order + +subsection {* Proving equivalence to the other sublist command *} + +lemma sublist'_sublist: "sublist' n m xs = sublist xs {j. n \ j \ j < m}" +apply (induct xs arbitrary: n m) +apply simp +apply (case_tac n) +apply (case_tac m) +apply simp +apply (simp add: sublist_Cons) +apply (case_tac m) +apply simp +apply (simp add: sublist_Cons) +done + + +lemma "sublist' n m xs = sublist xs {n.. (x # sublist' 0 j xs) | Suc i' \ sublist' i' j xs)" +by (cases i) auto + +lemma sublist'_Cons2[simp]: "sublist' i j (x#xs) = (if (j = 0) then [] else ((if (i = 0) then [x] else []) @ sublist' (i - 1) (j - 1) xs))" +apply (cases j) +apply auto +apply (cases i) +apply auto +done + +lemma sublist_n_0: "sublist' n 0 xs = []" +by (induct xs, auto) + +lemma sublist'_Nil': "n \ m \ sublist' n m xs = []" +apply (induct xs arbitrary: n m) +apply simp +apply (case_tac m) +apply simp +apply (case_tac n) +apply simp +apply simp +done + +lemma sublist'_Nil2: "n \ length xs \ sublist' n m xs = []" +apply (induct xs arbitrary: n m) +apply simp +apply (case_tac m) +apply simp +apply (case_tac n) +apply simp +apply simp +done + +lemma sublist'_Nil3: "(sublist' n m xs = []) = ((n \ m) \ (n \ length xs))" +apply (induct xs arbitrary: n m) +apply simp +apply (case_tac m) +apply simp +apply (case_tac n) +apply simp +apply simp +done + +lemma sublist'_notNil: "\ n < length xs; n < m \ \ sublist' n m xs \ []" +apply (induct xs arbitrary: n m) +apply simp +apply (case_tac m) +apply simp +apply (case_tac n) +apply simp +apply simp +done + +lemma sublist'_single: "n < length xs \ sublist' n (Suc n) xs = [xs ! n]" +apply (induct xs arbitrary: n) +apply simp +apply simp +apply (case_tac n) +apply (simp add: sublist_n_0) +apply simp +done + +lemma sublist'_update1: "i \ m \ sublist' n m (xs[i:=v]) = sublist' n m xs" +apply (induct xs arbitrary: n m i) +apply simp +apply simp +apply (case_tac i) +apply simp +apply simp +done + +lemma sublist'_update2: "i < n \ sublist' n m (xs[i:=v]) = sublist' n m xs" +apply (induct xs arbitrary: n m i) +apply simp +apply simp +apply (case_tac i) +apply simp +apply simp +done + +lemma sublist'_update3: "\n \ i; i < m\ \ sublist' n m (xs[i := v]) = (sublist' n m xs)[i - n := v]" +proof (induct xs arbitrary: n m i) + case Nil thus ?case by auto +next + case (Cons x xs) + thus ?case + apply - + apply auto + apply (cases i) + apply auto + apply (cases i) + apply auto + done +qed + +lemma "\ sublist' i j xs = sublist' i j ys; n \ i; m \ j \ \ sublist' n m xs = sublist' n m ys" +proof (induct xs arbitrary: i j ys n m) + case Nil + thus ?case + apply - + apply (rule sym, drule sym) + apply (simp add: sublist'_Nil) + apply (simp add: sublist'_Nil3) + apply arith + done +next + case (Cons x xs i j ys n m) + note c = this + thus ?case + proof (cases m) + case 0 thus ?thesis by (simp add: sublist_n_0) + next + case (Suc m') + note a = this + thus ?thesis + proof (cases n) + case 0 note b = this + show ?thesis + proof (cases ys) + case Nil with a b Cons.prems show ?thesis by (simp add: sublist'_Nil3) + next + case (Cons y ys) + show ?thesis + proof (cases j) + case 0 with a b Cons.prems show ?thesis by simp + next + case (Suc j') with a b Cons.prems Cons show ?thesis + apply - + apply (simp, rule Cons.hyps [of "0" "j'" "ys" "0" "m'"], auto) + done + qed + qed + next + case (Suc n') + show ?thesis + proof (cases ys) + case Nil with Suc a Cons.prems show ?thesis by (auto simp add: sublist'_Nil3) + next + case (Cons y ys) with Suc a Cons.prems show ?thesis + apply - + apply simp + apply (cases j) + apply simp + apply (cases i) + apply simp + apply (rule_tac j="nat" in Cons.hyps [of "0" _ "ys" "n'" "m'"]) + apply simp + apply simp + apply simp + apply simp + apply (rule_tac i="nata" and j="nat" in Cons.hyps [of _ _ "ys" "n'" "m'"]) + apply simp + apply simp + apply simp + done + qed + qed + qed +qed + +lemma length_sublist': "j \ length xs \ length (sublist' i j xs) = j - i" +by (induct xs arbitrary: i j, auto) + +lemma sublist'_front: "\ i < j; i < length xs \ \ sublist' i j xs = xs ! i # sublist' (Suc i) j xs" +apply (induct xs arbitrary: a i j) +apply simp +apply (case_tac j) +apply simp +apply (case_tac i) +apply simp +apply simp +done + +lemma sublist'_back: "\ i < j; j \ length xs \ \ sublist' i j xs = sublist' i (j - 1) xs @ [xs ! (j - 1)]" +apply (induct xs arbitrary: a i j) +apply simp +apply simp +apply (case_tac j) +apply simp +apply auto +apply (case_tac nat) +apply auto +done + +(* suffices that j \ length xs and length ys *) +lemma sublist'_eq_samelength_iff: "length xs = length ys \ (sublist' i j xs = sublist' i j ys) = (\i'. i \ i' \ i' < j \ xs ! i' = ys ! i')" +proof (induct xs arbitrary: ys i j) + case Nil thus ?case by simp +next + case (Cons x xs) + thus ?case + apply - + apply (cases ys) + apply simp + apply simp + apply auto + apply (case_tac i', auto) + apply (erule_tac x="Suc i'" in allE, auto) + apply (erule_tac x="i' - 1" in allE, auto) + apply (case_tac i', auto) + apply (erule_tac x="Suc i'" in allE, auto) + done +qed + +lemma sublist'_all[simp]: "sublist' 0 (length xs) xs = xs" +by (induct xs, auto) + +lemma sublist'_sublist': "sublist' n m (sublist' i j xs) = sublist' (i + n) (min (i + m) j) xs" +by (induct xs arbitrary: i j n m) (auto simp add: min_diff) + +lemma sublist'_append: "\ i \ j; j \ k \ \(sublist' i j xs) @ (sublist' j k xs) = sublist' i k xs" +by (induct xs arbitrary: i j k) auto + +lemma nth_sublist': "\ k < j - i; j \ length xs \ \ (sublist' i j xs) ! k = xs ! (i + k)" +apply (induct xs arbitrary: i j k) +apply auto +apply (case_tac k) +apply auto +apply (case_tac i) +apply auto +done + +lemma set_sublist': "set (sublist' i j xs) = {x. \k. i \ k \ k < j \ k < List.length xs \ x = xs ! k}" +apply (simp add: sublist'_sublist) +apply (simp add: set_sublist) +apply auto +done + +lemma all_in_set_sublist'_conv: "(\j. j \ set (sublist' l r xs) \ P j) = (\k. l \ k \ k < r \ k < List.length xs \ P (xs ! k))" +unfolding set_sublist' by blast + +lemma ball_in_set_sublist'_conv: "(\j \ set (sublist' l r xs). P j) = (\k. l \ k \ k < r \ k < List.length xs \ P (xs ! k))" +unfolding set_sublist' by blast + + +lemma multiset_of_sublist: +assumes l_r: "l \ r \ r \ List.length xs" +assumes left: "\ i. i < l \ (xs::'a list) ! i = ys ! i" +assumes right: "\ i. i \ r \ (xs::'a list) ! i = ys ! i" +assumes multiset: "multiset_of xs = multiset_of ys" + shows "multiset_of (sublist' l r xs) = multiset_of (sublist' l r ys)" +proof - + from l_r have xs_def: "xs = (sublist' 0 l xs) @ (sublist' l r xs) @ (sublist' r (List.length xs) xs)" (is "_ = ?xs_long") + by (simp add: sublist'_append) + from multiset have length_eq: "List.length xs = List.length ys" by (rule multiset_of_eq_length) + with l_r have ys_def: "ys = (sublist' 0 l ys) @ (sublist' l r ys) @ (sublist' r (List.length ys) ys)" (is "_ = ?ys_long") + by (simp add: sublist'_append) + from xs_def ys_def multiset have "multiset_of ?xs_long = multiset_of ?ys_long" by simp + moreover + from left l_r length_eq have "sublist' 0 l xs = sublist' 0 l ys" + by (auto simp add: length_sublist' nth_sublist' intro!: nth_equalityI) + moreover + from right l_r length_eq have "sublist' r (List.length xs) xs = sublist' r (List.length ys) ys" + by (auto simp add: length_sublist' nth_sublist' intro!: nth_equalityI) + moreover + ultimately show ?thesis by (simp add: multiset_of_append) +qed + + +end diff -r df8a3c2fd5a2 -r 55ef8e045931 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Mon Mar 23 15:33:35 2009 +0100 +++ b/src/HOL/IsaMakefile Mon Mar 23 19:01:34 2009 +0100 @@ -649,7 +649,11 @@ $(LOG)/HOL-Imperative_HOL.gz: $(OUT)/HOL Imperative_HOL/Heap.thy \ Imperative_HOL/Heap_Monad.thy Imperative_HOL/Array.thy \ Imperative_HOL/Relational.thy \ - Imperative_HOL/Ref.thy Imperative_HOL/Imperative_HOL.thy + Imperative_HOL/Ref.thy Imperative_HOL/Imperative_HOL.thy \ + Imperative_HOL/Imperative_HOL_ex.thy \ + Imperative_HOL/ex/Imperative_Quicksort.thy \ + Imperative_HOL/ex/Subarray.thy \ + Imperative_HOL/ex/Sublist.thy @$(ISABELLE_TOOL) usedir $(OUT)/HOL Imperative_HOL @@ -836,7 +840,7 @@ ex/Formal_Power_Series_Examples.thy ex/Fundefs.thy \ ex/Groebner_Examples.thy ex/Guess.thy ex/HarmonicSeries.thy \ ex/Hebrew.thy ex/Hex_Bin_Examples.thy ex/Higher_Order_Logic.thy \ - ex/Hilbert_Classical.thy ex/ImperativeQuicksort.thy \ + ex/Hilbert_Classical.thy \ ex/Induction_Scheme.thy ex/InductiveInvariant.thy \ ex/InductiveInvariant_examples.thy ex/Intuitionistic.thy \ ex/Lagrange.thy ex/LocaleTest2.thy ex/MT.thy ex/MergeSort.thy \ @@ -845,8 +849,8 @@ ex/Quickcheck_Examples.thy ex/Quickcheck_Generators.thy ex/ROOT.ML \ ex/Recdefs.thy ex/Records.thy ex/ReflectionEx.thy \ ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy \ - ex/Serbian.thy ex/Sqrt.thy ex/Sqrt_Script.thy ex/Subarray.thy \ - ex/Sublist.thy ex/Sudoku.thy ex/Tarski.thy ex/Term_Of_Syntax.thy \ + ex/Serbian.thy ex/Sqrt.thy ex/Sqrt_Script.thy \ + ex/Sudoku.thy ex/Tarski.thy ex/Term_Of_Syntax.thy \ ex/Termination.thy ex/Unification.thy ex/document/root.bib \ ex/document/root.tex ex/set.thy ex/svc_funcs.ML ex/svc_test.thy \ ex/Predicate_Compile.thy ex/predicate_compile.ML diff -r df8a3c2fd5a2 -r 55ef8e045931 src/HOL/NSA/hypreal_arith.ML --- a/src/HOL/NSA/hypreal_arith.ML Mon Mar 23 15:33:35 2009 +0100 +++ b/src/HOL/NSA/hypreal_arith.ML Mon Mar 23 19:01:34 2009 +0100 @@ -30,10 +30,10 @@ Simplifier.simproc (the_context ()) "fast_hypreal_arith" ["(m::hypreal) < n", "(m::hypreal) <= n", "(m::hypreal) = n"] - (K LinArith.lin_arith_simproc); + (K Lin_Arith.lin_arith_simproc); val hypreal_arith_setup = - LinArith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} => + Lin_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} => {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = real_inj_thms @ inj_thms, diff -r df8a3c2fd5a2 -r 55ef8e045931 src/HOL/Nat.thy --- a/src/HOL/Nat.thy Mon Mar 23 15:33:35 2009 +0100 +++ b/src/HOL/Nat.thy Mon Mar 23 19:01:34 2009 +0100 @@ -63,9 +63,8 @@ end lemma Suc_not_Zero: "Suc m \ 0" - apply (simp add: Zero_nat_def Suc_def Abs_Nat_inject [unfolded mem_def] + by (simp add: Zero_nat_def Suc_def Abs_Nat_inject [unfolded mem_def] Rep_Nat [unfolded mem_def] Suc_RepI Zero_RepI Suc_Rep_not_Zero_Rep [unfolded mem_def]) - done lemma Zero_not_Suc: "0 \ Suc m" by (rule not_sym, rule Suc_not_Zero not_sym) @@ -82,7 +81,7 @@ done lemma nat_induct [case_names 0 Suc, induct type: nat]: - -- {* for backward compatibility -- naming of variables differs *} + -- {* for backward compatibility -- names of variables differ *} fixes n assumes "P 0" and "\n. P n \ P (Suc n)" @@ -1345,19 +1344,13 @@ shows "u = s" using 2 1 by (rule trans) +setup Arith_Data.setup + use "Tools/nat_arith.ML" declaration {* K Nat_Arith.setup *} -ML{* -structure ArithFacts = - NamedThmsFun(val name = "arith" - val description = "arith facts - only ground formulas"); -*} - -setup ArithFacts.setup - use "Tools/lin_arith.ML" -declaration {* K LinArith.setup *} +declaration {* K Lin_Arith.setup *} lemmas [arith_split] = nat_diff_split split_min split_max diff -r df8a3c2fd5a2 -r 55ef8e045931 src/HOL/NatBin.thy --- a/src/HOL/NatBin.thy Mon Mar 23 15:33:35 2009 +0100 +++ b/src/HOL/NatBin.thy Mon Mar 23 19:01:34 2009 +0100 @@ -651,7 +651,7 @@ val numeral_ss = @{simpset} addsimps @{thms numerals}; val nat_bin_arith_setup = - LinArith.map_data + Lin_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} => {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = inj_thms, diff -r df8a3c2fd5a2 -r 55ef8e045931 src/HOL/Presburger.thy --- a/src/HOL/Presburger.thy Mon Mar 23 15:33:35 2009 +0100 +++ b/src/HOL/Presburger.thy Mon Mar 23 19:01:34 2009 +0100 @@ -439,12 +439,7 @@ use "Tools/Qelim/presburger.ML" -declaration {* fn _ => - arith_tactic_add - (mk_arith_tactic "presburger" (fn ctxt => fn i => fn st => - (warning "Trying Presburger arithmetic ..."; - Presburger.cooper_tac true [] [] ctxt i st))) -*} +setup {* Arith_Data.add_tactic "Presburger arithmetic" (K (Presburger.cooper_tac true [] [])) *} method_setup presburger = {* let diff -r df8a3c2fd5a2 -r 55ef8e045931 src/HOL/Tools/Qelim/cooper.ML --- a/src/HOL/Tools/Qelim/cooper.ML Mon Mar 23 15:33:35 2009 +0100 +++ b/src/HOL/Tools/Qelim/cooper.ML Mon Mar 23 19:01:34 2009 +0100 @@ -172,7 +172,7 @@ (* Canonical linear form for terms, formulae etc.. *) fun provelin ctxt t = Goal.prove ctxt [] [] t - (fn _ => EVERY [simp_tac lin_ss 1, TRY (simple_arith_tac ctxt 1)]); + (fn _ => EVERY [simp_tac lin_ss 1, TRY (linear_arith_tac ctxt 1)]); fun linear_cmul 0 tm = zero | linear_cmul n tm = case tm of Const (@{const_name HOL.plus}, _) $ a $ b => addC $ linear_cmul n a $ linear_cmul n b diff -r df8a3c2fd5a2 -r 55ef8e045931 src/HOL/Tools/TFL/post.ML --- a/src/HOL/Tools/TFL/post.ML Mon Mar 23 15:33:35 2009 +0100 +++ b/src/HOL/Tools/TFL/post.ML Mon Mar 23 19:01:34 2009 +0100 @@ -55,7 +55,7 @@ Prim.postprocess strict {wf_tac = REPEAT (ares_tac wfs 1), terminator = asm_simp_tac ss 1 - THEN TRY (silent_arith_tac (Simplifier.the_context ss) 1 ORELSE + THEN TRY (Arith_Data.arith_tac (Simplifier.the_context ss) 1 ORELSE fast_tac (cs addSDs [@{thm not0_implies_Suc}] addss ss) 1), simplifier = Rules.simpl_conv ss []}; diff -r df8a3c2fd5a2 -r 55ef8e045931 src/HOL/Tools/arith_data.ML --- a/src/HOL/Tools/arith_data.ML Mon Mar 23 15:33:35 2009 +0100 +++ b/src/HOL/Tools/arith_data.ML Mon Mar 23 19:01:34 2009 +0100 @@ -6,6 +6,11 @@ signature ARITH_DATA = sig + val arith_tac: Proof.context -> int -> tactic + val verbose_arith_tac: Proof.context -> int -> tactic + val add_tactic: string -> (bool -> Proof.context -> int -> tactic) -> theory -> theory + val get_arith_facts: Proof.context -> thm list + val prove_conv_nohyps: tactic list -> Proof.context -> term * term -> thm option val prove_conv: tactic list -> Proof.context -> thm list -> term * term -> thm option val prove_conv2: tactic -> (simpset -> tactic) -> simpset -> term * term -> thm @@ -14,11 +19,54 @@ val trans_tac: thm option -> tactic val prep_simproc: string * string list * (theory -> simpset -> term -> thm option) -> simproc + + val setup: theory -> theory end; structure Arith_Data: ARITH_DATA = struct +(* slots for pluging in arithmetic facts and tactics *) + +structure Arith_Facts = NamedThmsFun( + val name = "arith" + val description = "arith facts - only ground formulas" +); + +val get_arith_facts = Arith_Facts.get; + +structure Arith_Tactics = TheoryDataFun +( + type T = (serial * (string * (bool -> Proof.context -> int -> tactic))) list; + val empty = []; + val copy = I; + val extend = I; + fun merge _ = AList.merge (op =) (K true); +); + +fun add_tactic name tac = Arith_Tactics.map (cons (serial (), (name, tac))); + +fun gen_arith_tac verbose ctxt = + let + val tactics = (Arith_Tactics.get o ProofContext.theory_of) ctxt + fun invoke (_, (name, tac)) k st = (if verbose + then warning ("Trying " ^ name ^ "...") else (); + tac verbose ctxt k st); + in FIRST' (map invoke (rev tactics)) end; + +val arith_tac = gen_arith_tac false; +val verbose_arith_tac = gen_arith_tac true; + +val arith_method = Args.bang_facts >> (fn prems => fn ctxt => + METHOD (fn facts => HEADGOAL (Method.insert_tac (prems @ get_arith_facts ctxt @ facts) + THEN' verbose_arith_tac ctxt))); + +val setup = Arith_Facts.setup + #> Method.setup @{binding arith} arith_method "various arithmetic decision procedures"; + + +(* various auxiliary and legacy *) + fun prove_conv_nohyps tacs ctxt (t, u) = if t aconv u then NONE else let val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u)) diff -r df8a3c2fd5a2 -r 55ef8e045931 src/HOL/Tools/function_package/scnp_reconstruct.ML --- a/src/HOL/Tools/function_package/scnp_reconstruct.ML Mon Mar 23 15:33:35 2009 +0100 +++ b/src/HOL/Tools/function_package/scnp_reconstruct.ML Mon Mar 23 19:01:34 2009 +0100 @@ -197,7 +197,7 @@ else if b <= a then @{thm pair_leqI2} else @{thm pair_leqI1} in rtac rule 1 THEN PRIMITIVE (Thm.elim_implies stored_thm) - THEN (if tag_flag then arith_tac ctxt 1 else all_tac) + THEN (if tag_flag then Arith_Data.verbose_arith_tac ctxt 1 else all_tac) end fun steps_tac MAX strict lq lp = diff -r df8a3c2fd5a2 -r 55ef8e045931 src/HOL/Tools/int_arith.ML --- a/src/HOL/Tools/int_arith.ML Mon Mar 23 15:33:35 2009 +0100 +++ b/src/HOL/Tools/int_arith.ML Mon Mar 23 19:01:34 2009 +0100 @@ -530,7 +530,7 @@ :: Int_Numeral_Simprocs.cancel_numerals; val setup = - LinArith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} => + Lin_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} => {add_mono_thms = add_mono_thms, mult_mono_thms = @{thm mult_strict_left_mono} :: @{thm mult_left_mono} :: mult_mono_thms, inj_thms = nat_inj_thms @ inj_thms, @@ -547,7 +547,7 @@ "fast_int_arith" ["(m::'a::{ordered_idom,number_ring}) < n", "(m::'a::{ordered_idom,number_ring}) <= n", - "(m::'a::{ordered_idom,number_ring}) = n"] (K LinArith.lin_arith_simproc); + "(m::'a::{ordered_idom,number_ring}) = n"] (K Lin_Arith.lin_arith_simproc); end; diff -r df8a3c2fd5a2 -r 55ef8e045931 src/HOL/Tools/int_factor_simprocs.ML --- a/src/HOL/Tools/int_factor_simprocs.ML Mon Mar 23 15:33:35 2009 +0100 +++ b/src/HOL/Tools/int_factor_simprocs.ML Mon Mar 23 19:01:34 2009 +0100 @@ -232,7 +232,7 @@ val less = Const(@{const_name HOL.less}, [T,T] ---> HOLogic.boolT); val pos = less $ zero $ t and neg = less $ t $ zero fun prove p = - Option.map Eq_True_elim (LinArith.lin_arith_simproc ss p) + Option.map Eq_True_elim (Lin_Arith.lin_arith_simproc ss p) handle THM _ => NONE in case prove pos of SOME th => SOME(th RS pos_th) diff -r df8a3c2fd5a2 -r 55ef8e045931 src/HOL/Tools/lin_arith.ML --- a/src/HOL/Tools/lin_arith.ML Mon Mar 23 15:33:35 2009 +0100 +++ b/src/HOL/Tools/lin_arith.ML Mon Mar 23 19:01:34 2009 +0100 @@ -6,13 +6,9 @@ signature BASIC_LIN_ARITH = sig - type arith_tactic - val mk_arith_tactic: string -> (Proof.context -> int -> tactic) -> arith_tactic - val eq_arith_tactic: arith_tactic * arith_tactic -> bool val arith_split_add: attribute val arith_discrete: string -> Context.generic -> Context.generic val arith_inj_const: string * typ -> Context.generic -> Context.generic - val arith_tactic_add: arith_tactic -> Context.generic -> Context.generic val fast_arith_split_limit: int Config.T val fast_arith_neq_limit: int Config.T val lin_arith_pre_tac: Proof.context -> int -> tactic @@ -21,9 +17,7 @@ val trace_arith: bool ref val lin_arith_simproc: simpset -> term -> thm option val fast_nat_arith_simproc: simproc - val simple_arith_tac: Proof.context -> int -> tactic - val arith_tac: Proof.context -> int -> tactic - val silent_arith_tac: Proof.context -> int -> tactic + val linear_arith_tac: Proof.context -> int -> tactic end; signature LIN_ARITH = @@ -39,7 +33,7 @@ val setup: Context.generic -> Context.generic end; -structure LinArith: LIN_ARITH = +structure Lin_Arith: LIN_ARITH = struct (* Parameters data for general linear arithmetic functor *) @@ -72,7 +66,7 @@ let val _ $ t = Thm.prop_of thm in t = Const("False",HOLogic.boolT) end; -fun is_nat(t) = fastype_of1 t = HOLogic.natT; +fun is_nat t = (fastype_of1 t = HOLogic.natT); fun mk_nat_thm sg t = let val ct = cterm_of sg t and cn = cterm_of sg (Var(("n",0),HOLogic.natT)) @@ -83,49 +77,35 @@ (* arith context data *) -datatype arith_tactic = - ArithTactic of {name: string, tactic: Proof.context -> int -> tactic, id: stamp}; - -fun mk_arith_tactic name tactic = ArithTactic {name = name, tactic = tactic, id = stamp ()}; - -fun eq_arith_tactic (ArithTactic {id = id1, ...}, ArithTactic {id = id2, ...}) = (id1 = id2); - structure ArithContextData = GenericDataFun ( type T = {splits: thm list, inj_consts: (string * typ) list, - discrete: string list, - tactics: arith_tactic list}; - val empty = {splits = [], inj_consts = [], discrete = [], tactics = []}; + discrete: string list}; + val empty = {splits = [], inj_consts = [], discrete = []}; val extend = I; fun merge _ - ({splits= splits1, inj_consts= inj_consts1, discrete= discrete1, tactics= tactics1}, - {splits= splits2, inj_consts= inj_consts2, discrete= discrete2, tactics= tactics2}) : T = + ({splits= splits1, inj_consts= inj_consts1, discrete= discrete1}, + {splits= splits2, inj_consts= inj_consts2, discrete= discrete2}) : T = {splits = Library.merge Thm.eq_thm_prop (splits1, splits2), inj_consts = Library.merge (op =) (inj_consts1, inj_consts2), - discrete = Library.merge (op =) (discrete1, discrete2), - tactics = Library.merge eq_arith_tactic (tactics1, tactics2)}; + discrete = Library.merge (op =) (discrete1, discrete2)}; ); val get_arith_data = ArithContextData.get o Context.Proof; val arith_split_add = Thm.declaration_attribute (fn thm => - ArithContextData.map (fn {splits, inj_consts, discrete, tactics} => + ArithContextData.map (fn {splits, inj_consts, discrete} => {splits = update Thm.eq_thm_prop thm splits, - inj_consts = inj_consts, discrete = discrete, tactics = tactics})); - -fun arith_discrete d = ArithContextData.map (fn {splits, inj_consts, discrete, tactics} => - {splits = splits, inj_consts = inj_consts, - discrete = update (op =) d discrete, tactics = tactics}); + inj_consts = inj_consts, discrete = discrete})); -fun arith_inj_const c = ArithContextData.map (fn {splits, inj_consts, discrete, tactics} => - {splits = splits, inj_consts = update (op =) c inj_consts, - discrete = discrete, tactics= tactics}); +fun arith_discrete d = ArithContextData.map (fn {splits, inj_consts, discrete} => + {splits = splits, inj_consts = inj_consts, + discrete = update (op =) d discrete}); -fun arith_tactic_add tac = ArithContextData.map (fn {splits, inj_consts, discrete, tactics} => - {splits = splits, inj_consts = inj_consts, discrete = discrete, - tactics = update eq_arith_tactic tac tactics}); - +fun arith_inj_const c = ArithContextData.map (fn {splits, inj_consts, discrete} => + {splits = splits, inj_consts = update (op =) c inj_consts, + discrete = discrete}); val (fast_arith_split_limit, setup1) = Attrib.config_int "fast_arith_split_limit" 9; val (fast_arith_neq_limit, setup2) = Attrib.config_int "fast_arith_neq_limit" 9; @@ -794,7 +774,7 @@ Most of the work is done by the cancel tactics. *) val init_arith_data = - Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, ...} => + map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, ...} => {add_mono_thms = add_mono_thms @ @{thms add_mono_thms_ordered_semiring} @ @{thms add_mono_thms_ordered_field}, mult_mono_thms = mult_mono_thms, @@ -815,7 +795,7 @@ arith_discrete "nat"; fun add_arith_facts ss = - add_prems (ArithFacts.get (MetaSimplifier.the_context ss)) ss; + add_prems (Arith_Data.get_arith_facts (MetaSimplifier.the_context ss)) ss; val lin_arith_simproc = add_arith_facts #> Fast_Arith.lin_arith_simproc; @@ -895,27 +875,16 @@ (REPEAT_DETERM o split_tac (#splits (get_arith_data ctxt))) (fast_ex_arith_tac ctxt ex); -fun more_arith_tacs ctxt = - let val tactics = #tactics (get_arith_data ctxt) - in FIRST' (map (fn ArithTactic {tactic, ...} => tactic ctxt) tactics) end; - in -fun simple_arith_tac ctxt = FIRST' [fast_arith_tac ctxt, - ObjectLogic.full_atomize_tac THEN' (REPEAT_DETERM o rtac impI) THEN' raw_arith_tac ctxt true]; - -fun arith_tac ctxt = FIRST' [fast_arith_tac ctxt, - ObjectLogic.full_atomize_tac THEN' (REPEAT_DETERM o rtac impI) THEN' raw_arith_tac ctxt true, - more_arith_tacs ctxt]; +fun gen_linear_arith_tac ex ctxt = FIRST' [fast_arith_tac ctxt, + ObjectLogic.full_atomize_tac THEN' (REPEAT_DETERM o rtac impI) THEN' raw_arith_tac ctxt ex]; -fun silent_arith_tac ctxt = FIRST' [fast_arith_tac ctxt, - ObjectLogic.full_atomize_tac THEN' (REPEAT_DETERM o rtac impI) THEN' raw_arith_tac ctxt false, - more_arith_tacs ctxt]; +val linear_arith_tac = gen_linear_arith_tac true; -val arith_method = Args.bang_facts >> - (fn prems => fn ctxt => METHOD (fn facts => - HEADGOAL (Method.insert_tac (prems @ ArithFacts.get ctxt @ facts) - THEN' arith_tac ctxt))); +val linarith_method = Args.bang_facts >> (fn prems => fn ctxt => + METHOD (fn facts => HEADGOAL (Method.insert_tac (prems @ Arith_Data.get_arith_facts ctxt @ facts) + THEN' linear_arith_tac ctxt))); end; @@ -929,11 +898,12 @@ (add_arith_facts #> Fast_Arith.cut_lin_arith_tac))) #> Context.mapping (setup_options #> - Method.setup @{binding arith} arith_method "decide linear arithmetic" #> + Arith_Data.add_tactic "linear arithmetic" gen_linear_arith_tac #> + Method.setup @{binding linarith} linarith_method "linear arithmetic" #> Attrib.setup @{binding arith_split} (Scan.succeed arith_split_add) "declaration of split rules for arithmetic procedure") I; end; -structure BasicLinArith: BASIC_LIN_ARITH = LinArith; -open BasicLinArith; +structure Basic_Lin_Arith: BASIC_LIN_ARITH = Lin_Arith; +open Basic_Lin_Arith; diff -r df8a3c2fd5a2 -r 55ef8e045931 src/HOL/Tools/nat_simprocs.ML --- a/src/HOL/Tools/nat_simprocs.ML Mon Mar 23 15:33:35 2009 +0100 +++ b/src/HOL/Tools/nat_simprocs.ML Mon Mar 23 19:01:34 2009 +0100 @@ -565,7 +565,7 @@ in val nat_simprocs_setup = - LinArith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} => + Lin_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} => {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = inj_thms, lessD = lessD, neqE = neqE, simpset = simpset addsimps add_rules diff -r df8a3c2fd5a2 -r 55ef8e045931 src/HOL/Tools/rat_arith.ML --- a/src/HOL/Tools/rat_arith.ML Mon Mar 23 15:33:35 2009 +0100 +++ b/src/HOL/Tools/rat_arith.ML Mon Mar 23 19:01:34 2009 +0100 @@ -35,7 +35,7 @@ in val rat_arith_setup = - LinArith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} => + Lin_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} => {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = int_inj_thms @ nat_inj_thms @ inj_thms, diff -r df8a3c2fd5a2 -r 55ef8e045931 src/HOL/Tools/real_arith.ML --- a/src/HOL/Tools/real_arith.ML Mon Mar 23 15:33:35 2009 +0100 +++ b/src/HOL/Tools/real_arith.ML Mon Mar 23 19:01:34 2009 +0100 @@ -29,7 +29,7 @@ in val real_arith_setup = - LinArith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} => + Lin_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} => {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = int_inj_thms @ nat_inj_thms @ inj_thms, diff -r df8a3c2fd5a2 -r 55ef8e045931 src/HOL/Word/WordArith.thy --- a/src/HOL/Word/WordArith.thy Mon Mar 23 15:33:35 2009 +0100 +++ b/src/HOL/Word/WordArith.thy Mon Mar 23 19:01:34 2009 +0100 @@ -512,7 +512,7 @@ fun uint_arith_tacs ctxt = let - fun arith_tac' n t = arith_tac ctxt n t handle COOPER => Seq.empty; + fun arith_tac' n t = Arith_Data.verbose_arith_tac ctxt n t handle COOPER => Seq.empty; val cs = local_claset_of ctxt; val ss = local_simpset_of ctxt; in @@ -1075,7 +1075,7 @@ fun unat_arith_tacs ctxt = let - fun arith_tac' n t = arith_tac ctxt n t handle COOPER => Seq.empty; + fun arith_tac' n t = Arith_Data.verbose_arith_tac ctxt n t handle COOPER => Seq.empty; val cs = local_claset_of ctxt; val ss = local_simpset_of ctxt; in diff -r df8a3c2fd5a2 -r 55ef8e045931 src/HOL/ex/Arith_Examples.thy --- a/src/HOL/ex/Arith_Examples.thy Mon Mar 23 15:33:35 2009 +0100 +++ b/src/HOL/ex/Arith_Examples.thy Mon Mar 23 19:01:34 2009 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/ex/Arith_Examples.thy - ID: $Id$ Author: Tjark Weber *) @@ -14,13 +13,13 @@ @{ML fast_arith_tac} is a very basic version of the tactic. It performs no meta-to-object-logic conversion, and only some splitting of operators. - @{ML simple_arith_tac} performs meta-to-object-logic conversion, full + @{ML linear_arith_tac} performs meta-to-object-logic conversion, full splitting of operators, and NNF normalization of the goal. The @{text arith} method combines them both, and tries other methods (e.g.~@{text presburger}) as well. This is the one that you should use in your proofs! An @{text arith}-based simproc is available as well (see @{ML - LinArith.lin_arith_simproc}), which---for performance + Lin_Arith.lin_arith_simproc}), which---for performance reasons---however does even less splitting than @{ML fast_arith_tac} at the moment (namely inequalities only). (On the other hand, it does take apart conjunctions, which @{ML fast_arith_tac} currently @@ -83,7 +82,7 @@ by (tactic {* fast_arith_tac @{context} 1 *}) lemma "!!x. ((x::nat) <= y) = (x - y = 0)" - by (tactic {* simple_arith_tac @{context} 1 *}) + by (tactic {* linear_arith_tac @{context} 1 *}) lemma "[| (x::nat) < y; d < 1 |] ==> x - y = d" by (tactic {* fast_arith_tac @{context} 1 *}) @@ -140,34 +139,34 @@ subsection {* Meta-Logic *} lemma "x < Suc y == x <= y" - by (tactic {* simple_arith_tac @{context} 1 *}) + by (tactic {* linear_arith_tac @{context} 1 *}) lemma "((x::nat) == z ==> x ~= y) ==> x ~= y | z ~= y" - by (tactic {* simple_arith_tac @{context} 1 *}) + by (tactic {* linear_arith_tac @{context} 1 *}) subsection {* Various Other Examples *} lemma "(x < Suc y) = (x <= y)" - by (tactic {* simple_arith_tac @{context} 1 *}) + by (tactic {* linear_arith_tac @{context} 1 *}) lemma "[| (x::nat) < y; y < z |] ==> x < z" by (tactic {* fast_arith_tac @{context} 1 *}) lemma "(x::nat) < y & y < z ==> x < z" - by (tactic {* simple_arith_tac @{context} 1 *}) + by (tactic {* linear_arith_tac @{context} 1 *}) text {* This example involves no arithmetic at all, but is solved by preprocessing (i.e. NNF normalization) alone. *} lemma "(P::bool) = Q ==> Q = P" - by (tactic {* simple_arith_tac @{context} 1 *}) + by (tactic {* linear_arith_tac @{context} 1 *}) lemma "[| P = (x = 0); (~P) = (y = 0) |] ==> min (x::nat) y = 0" - by (tactic {* simple_arith_tac @{context} 1 *}) + by (tactic {* linear_arith_tac @{context} 1 *}) lemma "[| P = (x = 0); (~P) = (y = 0) |] ==> max (x::nat) y = x + y" - by (tactic {* simple_arith_tac @{context} 1 *}) + by (tactic {* linear_arith_tac @{context} 1 *}) lemma "[| (x::nat) ~= y; a + 2 = b; a < y; y < b; a < x; x < b |] ==> False" by (tactic {* fast_arith_tac @{context} 1 *}) @@ -185,7 +184,7 @@ by (tactic {* fast_arith_tac @{context} 1 *}) lemma "[| (x::nat) < y; P (x - y) |] ==> P 0" - by (tactic {* simple_arith_tac @{context} 1 *}) + by (tactic {* linear_arith_tac @{context} 1 *}) lemma "(x - y) - (x::nat) = (x - x) - y" by (tactic {* fast_arith_tac @{context} 1 *}) @@ -207,7 +206,7 @@ (* preprocessing negates the goal and tries to compute its negation *) (* normal form, which creates lots of separate cases for this *) (* disjunction of conjunctions *) -(* by (tactic {* simple_arith_tac 1 *}) *) +(* by (tactic {* linear_arith_tac 1 *}) *) oops lemma "2 * (x::nat) ~= 1" diff -r df8a3c2fd5a2 -r 55ef8e045931 src/HOL/ex/ImperativeQuicksort.thy --- a/src/HOL/ex/ImperativeQuicksort.thy Mon Mar 23 15:33:35 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,637 +0,0 @@ -theory ImperativeQuicksort -imports "~~/src/HOL/Imperative_HOL/Imperative_HOL" Subarray Multiset Efficient_Nat -begin - -text {* We prove QuickSort correct in the Relational Calculus. *} - -definition swap :: "nat array \ nat \ nat \ unit Heap" -where - "swap arr i j = ( - do - x \ nth arr i; - y \ nth arr j; - upd i y arr; - upd j x arr; - return () - done)" - -lemma swap_permutes: - assumes "crel (swap a i j) h h' rs" - shows "multiset_of (get_array a h') - = multiset_of (get_array a h)" - using assms - unfolding swap_def - by (auto simp add: Heap.length_def multiset_of_swap dest: sym [of _ "h'"] elim!: crelE crel_nth crel_return crel_upd) - -function part1 :: "nat array \ nat \ nat \ nat \ nat Heap" -where - "part1 a left right p = ( - if (right \ left) then return right - else (do - v \ nth a left; - (if (v \ p) then (part1 a (left + 1) right p) - else (do swap a left right; - part1 a left (right - 1) p done)) - done))" -by pat_completeness auto - -termination -by (relation "measure (\(_,l,r,_). r - l )") auto - -declare part1.simps[simp del] - -lemma part_permutes: - assumes "crel (part1 a l r p) h h' rs" - shows "multiset_of (get_array a h') - = multiset_of (get_array a h)" - using assms -proof (induct a l r p arbitrary: h h' rs rule:part1.induct) - case (1 a l r p h h' rs) - thus ?case - unfolding part1.simps [of a l r p] - by (elim crelE crel_if crel_return crel_nth) (auto simp add: swap_permutes) -qed - -lemma part_returns_index_in_bounds: - assumes "crel (part1 a l r p) h h' rs" - assumes "l \