--- a/src/HOL/List.thy Sat Jan 20 15:50:15 2018 +0100
+++ b/src/HOL/List.thy Sun Jan 21 11:04:18 2018 +0100
@@ -361,24 +361,16 @@
context linorder
begin
-inductive sorted :: "'a list \<Rightarrow> bool" where
- Nil [iff]: "sorted []"
-| Cons: "\<forall>y\<in>set xs. x \<le> y \<Longrightarrow> sorted xs \<Longrightarrow> sorted (x # xs)"
-
-lemma sorted_single [iff]: "sorted [x]"
-by (rule sorted.Cons) auto
-
-lemma sorted_many: "x \<le> y \<Longrightarrow> sorted (y # zs) \<Longrightarrow> sorted (x # y # zs)"
-by (rule sorted.Cons) (cases "y # zs" rule: sorted.cases, auto)
-
-lemma sorted_many_eq [simp, code]:
- "sorted (x # y # zs) \<longleftrightarrow> x \<le> y \<and> sorted (y # zs)"
-by (auto intro: sorted_many elim: sorted.cases)
-
-lemma [code]:
- "sorted [] \<longleftrightarrow> True"
- "sorted [x] \<longleftrightarrow> True"
-by simp_all
+fun sorted :: "'a list \<Rightarrow> bool" where
+"sorted [] = True" |
+"sorted [x] = True" |
+"sorted (x # y # zs) = (x \<le> y \<and> sorted (y # zs))"
+
+lemma sorted_sorted_wrt: "sorted = sorted_wrt (\<le>)"
+proof (rule ext)
+ fix xs show "sorted xs = sorted_wrt (\<le>) xs"
+ by(induction xs rule: sorted.induct) auto
+qed
primrec insort_key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b \<Rightarrow> 'b list \<Rightarrow> 'b list" where
"insort_key f x [] = [x]" |
@@ -4981,7 +4973,7 @@
apply(induction xs arbitrary: x)
apply simp
by simp (blast intro: order_trans)
-
+(*
lemma sorted_iff_wrt: "sorted xs = sorted_wrt (\<le>) xs"
proof
assume "sorted xs" thus "sorted_wrt (\<le>) xs"
@@ -4989,7 +4981,7 @@
case (Cons xs x) thus ?case by (cases xs) simp_all
qed simp
qed (induct xs rule: induct_list012, simp_all)
-
+*)
lemma sorted_tl:
"sorted xs \<Longrightarrow> sorted (tl xs)"
by (cases xs) (simp_all add: sorted_Cons)
@@ -5365,18 +5357,17 @@
done
lemma sorted_find_Min:
- assumes "sorted xs"
- assumes "\<exists>x \<in> set xs. P x"
- shows "List.find P xs = Some (Min {x\<in>set xs. P x})"
-using assms proof (induct xs rule: sorted.induct)
+ "sorted xs \<Longrightarrow> \<exists>x \<in> set xs. P x \<Longrightarrow> List.find P xs = Some (Min {x\<in>set xs. P x})"
+proof (induct xs)
case Nil then show ?case by simp
next
- case (Cons xs x) show ?case proof (cases "P x")
- case True with Cons show ?thesis by (auto intro: Min_eqI [symmetric])
+ case (Cons x xs) show ?case proof (cases "P x")
+ case True
+ with Cons show ?thesis by (auto simp: sorted_Cons intro: Min_eqI [symmetric])
next
case False then have "{y. (y = x \<or> y \<in> set xs) \<and> P y} = {y \<in> set xs. P y}"
by auto
- with Cons False show ?thesis by simp_all
+ with Cons False show ?thesis by (simp_all add: sorted_Cons)
qed
qed
@@ -6271,7 +6262,7 @@
end
lemma sorted_insort_is_snoc: "sorted xs \<Longrightarrow> \<forall>x \<in> set xs. a \<ge> x \<Longrightarrow> insort a xs = xs @ [a]"
- by (induct rule: sorted.induct) (auto dest!: insort_is_Cons)
+ by (induct xs) (auto dest!: insort_is_Cons simp: sorted_Cons)
subsubsection \<open>Lexicographic combination of measure functions\<close>
--- a/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy Sat Jan 20 15:50:15 2018 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy Sun Jan 21 11:04:18 2018 +0100
@@ -50,6 +50,20 @@
subsection \<open>Sorts\<close>
+inductive sorted :: "'a::linorder list \<Rightarrow> bool" where
+ Nil [simp]: "sorted []"
+| Cons: "\<forall>y\<in>set xs. x \<le> y \<Longrightarrow> sorted xs \<Longrightarrow> sorted (x # xs)"
+
+lemma sorted_single [simp]: "sorted [x]"
+by (rule sorted.Cons) auto
+
+lemma sorted_many: "x \<le> y \<Longrightarrow> sorted (y # zs) \<Longrightarrow> sorted (x # y # zs)"
+by (rule sorted.Cons) (cases "y # zs" rule: sorted.cases, auto)
+
+lemma sorted_many_eq [simp]:
+ "sorted (x # y # zs) \<longleftrightarrow> x \<le> y \<and> sorted (y # zs)"
+by (auto intro: sorted_many elim: sorted.cases)
+
declare sorted.Nil [code_pred_intro]
sorted_single [code_pred_intro]
sorted_many [code_pred_intro]
@@ -77,6 +91,7 @@
qed
thm sorted.equation
+
section \<open>Specialisation in POPLmark theory\<close>
notation
--- a/src/HOL/ex/Bubblesort.thy Sat Jan 20 15:50:15 2018 +0100
+++ b/src/HOL/ex/Bubblesort.thy Sun Jan 21 11:04:18 2018 +0100
@@ -73,8 +73,7 @@
apply(induction xs rule: bubblesort.induct)
apply simp
apply simp
-apply (fastforce simp: set_bubblesort split: list.split if_splits
- intro!: sorted.Cons dest: bubble_min_min)
+apply (fastforce simp: set_bubblesort sorted_Cons split: list.split if_splits dest: bubble_min_min)
done
end