# HG changeset patch
# User nipkow
# Date 1516529058 -3600
# Node ID df252c3d48f2d16aaa75de799db4a12993dc133f
# Parent  14d3163588aeb39903ae39309ea37130f3b9613d# Parent  f261aefbe702c7741db850c74feb9a9c912bd80a
merged

diff -r 14d3163588ae -r df252c3d48f2 src/HOL/List.thy
--- 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>
diff -r 14d3163588ae -r df252c3d48f2 src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy
--- 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
diff -r 14d3163588ae -r df252c3d48f2 src/HOL/ex/Bubblesort.thy
--- 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