author nipkow Mon, 24 Sep 2007 22:00:18 +0200 changeset 24697 b37d3980da3c parent 24696 b5e68fe31eba child 24698 9800a7602629
fixed haftmann bug
 src/HOL/List.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/List.thy	Mon Sep 24 21:07:41 2007 +0200
+++ b/src/HOL/List.thy	Mon Sep 24 22:00:18 2007 +0200
@@ -215,23 +215,18 @@
text{* The following simple sort functions are intended for proofs,
not for efficient implementations. *}

-context linorder
-begin
-
-fun  sorted :: "'a list \<Rightarrow> bool" where
-  "sorted [] \<longleftrightarrow> True" |
-  "sorted [x] \<longleftrightarrow> True" |
-  "sorted (x#y#zs) \<longleftrightarrow> x \<^loc><= y \<and> sorted (y#zs)"
-
-fun insort :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
-  "insort x [] = [x]" |
-  "insort x (y#ys) = (if x \<^loc><= y then (x#y#ys) else y#(insort x ys))"
-
-fun sort :: "'a list \<Rightarrow> 'a list" where
-  "sort [] = []" |
-  "sort (x#xs) = insort x (sort xs)"
-
-end
+fun (in linorder) sorted :: "'a list \<Rightarrow> bool" where
+"sorted [] \<longleftrightarrow> True" |
+"sorted [x] \<longleftrightarrow> True" |
+"sorted (x#y#zs) \<longleftrightarrow> x \<^loc><= y \<and> sorted (y#zs)"
+
+fun (in linorder) insort :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+"insort x [] = [x]" |
+"insort x (y#ys) = (if x \<^loc><= y then (x#y#ys) else y#(insort x ys))"
+
+fun (in linorder) sort :: "'a list \<Rightarrow> 'a list" where
+"sort [] = []" |
+"sort (x#xs) = insort x (sort xs)"

subsubsection {* List comprehension *}
@@ -2545,28 +2540,62 @@

subsubsection {* @{text upto}: the generic interval-list *}

-(* FIXME why does (in linorder) fail? *)
-definition upto :: "'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a list" ("(1[_../_])") where
-"upto i j == THE is. set is = {i..j} & sorted is & distinct is"
-
-(*The following lemmas could/should be generalized to discrete linear orders*)
-
-lemma set_upto[simp]: "set[a::int..b] = {a..b}"
+class finite_intvl_succ = linorder +
+fixes successor :: "'a \<Rightarrow> 'a"
+assumes finite_intvl: "finite(ord.atLeastAtMost (op \<sqsubseteq>) a b)" (* FIXME should be finite({a..b}) *)
+and successor_incr: "a \<sqsubset> successor a"
+and ord_discrete: "\<not>(\<exists>x. a \<sqsubset> x & x \<sqsubset> successor a)"
+
+context finite_intvl_succ
+begin
+
+definition
+ upto :: "'a \<Rightarrow> 'a \<Rightarrow> 'a list" ("(1\<^loc>[_../_])") where
+"upto i j == THE is. set is = \<^loc>{i..j} & sorted is & distinct is"
+
+lemma set_upto[simp]: "set\<^loc>[a..b] = \<^loc>{a..b}"
apply(rule the1I2)
+done
+
+lemma insert_intvl: "i \<^loc>\<le> j \<Longrightarrow> insert i \<^loc>{successor i..j} = \<^loc>{i..j}"
+apply(insert successor_incr[of i])
+apply(auto simp: atLeastAtMost_def atLeast_def atMost_def)
+apply (metis ord_discrete less_le not_le)
done

-lemma upto_rec: "[i::int..j] = (if i <= j then i # [i+1..j] else [])"
-apply clarify
-apply (rule the1_equality[OF finite_sorted_distinct_unique])
- apply simp
-apply(rule the1I2[OF finite_sorted_distinct_unique])
- apply simp
-apply (fastsimp simp: sorted_Cons)
+lemma upto_rec[code]: "\<^loc>[i..j] = (if i \<sqsubseteq> j then i # \<^loc>[successor i..j] else [])"
+proof cases
+  assume "i \<sqsubseteq> j" thus ?thesis
+    apply (rule the1_equality[OF finite_sorted_distinct_unique])
+    apply(rule the1I2[OF finite_sorted_distinct_unique])
+    apply (simp add: sorted_Cons insert_intvl Ball_def)
+    apply (metis successor_incr leD less_imp_le order_trans)
+    done
+next
+  assume "~ i \<sqsubseteq> j" thus ?thesis
+    apply(subst atLeastAtMost_empty) apply simp
+    apply(simp cong:conj_cong)
+    done (* FIXME should reduce to the first simp alone *)
+qed
+
+end
+
+text{* The integers are an instance of the above class: *}
+
+instance int:: finite_intvl_succ
+  successor_int_def: "successor == (%i. i+1)"
+apply(intro_classes)