reverted (accidentally commited) changes from changeset fd4aef9bc7a9
authorChristian Sternagel
Thu, 30 Aug 2012 13:39:30 +0900
changeset 49090 6be57c7d84f8
parent 49089 cd73b439cbe5
child 49091 0da7116b1b23
reverted (accidentally commited) changes from changeset fd4aef9bc7a9
--- a/src/HOL/Codatatype/BNF_Library.thy	Thu Aug 30 13:38:27 2012 +0900
+++ b/src/HOL/Codatatype/BNF_Library.thy	Thu Aug 30 13:39:30 2012 +0900
@@ -8,7 +8,9 @@
 header {* Library for Bounded Natural Functors *}
 theory BNF_Library
-imports "../Ordinals_and_Cardinals/Cardinal_Arithmetic" "~~/src/HOL/Library/Sublist"
+  "../Ordinals_and_Cardinals/Cardinal_Arithmetic"
+  "~~/src/HOL/Library/Prefix_Order"
@@ -654,23 +656,16 @@
 lemma empty_Shift: "\<lbrakk>[] \<in> Kl; k \<in> Succ Kl []\<rbrakk> \<Longrightarrow> [] \<in> Shift Kl k"
 unfolding Shift_def Succ_def by simp
-instantiation list :: (type) order
-  definition "(xs::'a list) \<le> ys \<equiv> prefixeq xs ys"
-  definition "(xs::'a list) < ys \<equiv> xs \<le> ys \<and> \<not> (ys \<le> xs)"
-instance by (default, unfold less_eq_list_def less_list_def) auto
 lemma Shift_clists: "Kl \<subseteq> Field (clists r) \<Longrightarrow> Shift Kl k \<subseteq> Field (clists r)"
 unfolding Shift_def clists_def Field_card_of by auto
 lemma Shift_prefCl: "prefCl Kl \<Longrightarrow> prefCl (Shift Kl k)"
 unfolding prefCl_def Shift_def
 proof safe
   fix kl1 kl2
   assume "\<forall>kl1 kl2. kl1 \<le> kl2 \<and> kl2 \<in> Kl \<longrightarrow> kl1 \<in> Kl"
     "kl1 \<le> kl2" "k # kl2 \<in> Kl"
-  thus "k # kl1 \<in> Kl" using Cons_prefixeq_Cons[of k kl1 k kl2, folded less_eq_list_def] by blast
+  thus "k # kl1 \<in> Kl" using Cons_prefix_Cons[of k kl1 k kl2] by blast
 lemma not_in_Shift: "kl \<notin> Shift Kl x \<Longrightarrow> x # kl \<notin> Kl"
@@ -679,7 +674,7 @@
 lemma prefCl_Succ: "\<lbrakk>prefCl Kl; k # kl \<in> Kl\<rbrakk> \<Longrightarrow> k \<in> Succ Kl []"
 unfolding Succ_def proof
   assume "prefCl Kl" "k # kl \<in> Kl"
-  moreover have "k # [] \<le> k # kl" unfolding less_eq_list_def by auto
+  moreover have "k # [] \<le> k # kl" by auto
   ultimately have "k # [] \<in> Kl" unfolding prefCl_def by blast
   thus "[] @ [k] \<in> Kl" by simp