--- a/src/HOL/List.thy Sat Jan 20 16:15:05 2018 +0100
+++ b/src/HOL/List.thy Sun Jan 21 11:04:07 2018 +0100
@@ -360,26 +360,6 @@
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" |
--- a/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy Sat Jan 20 16:15:05 2018 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy Sun Jan 21 11:04:07 2018 +0100
@@ -48,9 +48,22 @@
values "{x. max_of_my_SucP x 6}"
-(* Sortedness is now expressed functionally.
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,7 +90,7 @@
qed
qed
thm sorted.equation
-*)
+
section \<open>Specialisation in POPLmark theory\<close>