# HG changeset patch
# User Christian Sternagel
# Date 1346299383 -32400
# Node ID 835fd053d17d6915b733125f963e67a3dfbb4075
# Parent  4eef5c2ff5add42894e1c4c88e631579d7600239
List is implicitly imported by Main

diff -r 4eef5c2ff5ad -r 835fd053d17d src/HOL/Codatatype/BNF_Library.thy
--- a/src/HOL/Codatatype/BNF_Library.thy	Wed Aug 29 16:25:35 2012 +0900
+++ b/src/HOL/Codatatype/BNF_Library.thy	Thu Aug 30 13:03:03 2012 +0900
@@ -654,16 +654,23 @@
 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
+begin
+  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
+end
+
 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_prefix_Cons[of k kl1 k kl2] by blast
+  thus "k # kl1 \<in> Kl" using Cons_prefixeq_Cons[of k kl1 k kl2, folded less_eq_list_def] by blast
 qed
 
 lemma not_in_Shift: "kl \<notin> Shift Kl x \<Longrightarrow> x # kl \<notin> Kl"
@@ -672,7 +679,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" by auto
+  moreover have "k # [] \<le> k # kl" unfolding less_eq_list_def by auto
   ultimately have "k # [] \<in> Kl" unfolding prefCl_def by blast
   thus "[] @ [k] \<in> Kl" by simp
 qed
diff -r 4eef5c2ff5ad -r 835fd053d17d src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML
--- a/src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML	Wed Aug 29 16:25:35 2012 +0900
+++ b/src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML	Thu Aug 30 13:03:03 2012 +0900
@@ -646,7 +646,7 @@
       REPEAT_DETERM o rtac allI,
       CONJ_WRAP' (fn Lev_0 =>
         EVERY' [rtac impI, etac conjE, dtac (Lev_0 RS equalityD1 RS @{thm set_mp}),
-          etac @{thm singletonE}, hyp_subst_tac, dtac @{thm prefix_Nil[THEN subst, of "%x. x"]},
+          etac @{thm singletonE}, hyp_subst_tac, dtac @{thm prefixeq_Nil[THEN subst, of "%x. x"]},
           hyp_subst_tac, rtac @{thm set_mp[OF equalityD2[OF trans[OF arg_cong[OF list.size(3)]]]]},
           rtac Lev_0, rtac @{thm singletonI}]) Lev_0s,
       REPEAT_DETERM o rtac allI,
@@ -654,7 +654,7 @@
         EVERY' [rtac impI, etac conjE, dtac (Lev_Suc RS equalityD1 RS @{thm set_mp}),
           CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
             (fn i => EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
-              dtac @{thm prefix_Cons[THEN subst, of "%x. x"]}, etac disjE, hyp_subst_tac,
+              dtac @{thm prefixeq_Cons[THEN subst, of "%x. x"]}, etac disjE, hyp_subst_tac,
               rtac @{thm set_mp[OF equalityD2[OF trans[OF arg_cong[OF list.size(3)]]]]},
               rtac Lev_0, rtac @{thm singletonI},
               REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac,
@@ -845,7 +845,7 @@
         rtac conjI,
           rtac @{thm prefCl_UN}, rtac ssubst, rtac @{thm PrefCl_def}, REPEAT_DETERM o rtac allI,
           rtac impI, etac conjE, rtac exI, rtac conjI, rtac @{thm ord_le_eq_trans},
-          etac @{thm prefix_length_le}, etac length_Lev, rtac prefCl_Lev, etac conjI, atac,
+          etac @{thm prefixeq_length_le}, etac length_Lev, rtac prefCl_Lev, etac conjI, atac,
         rtac conjI,
           rtac ballI, etac @{thm UN_E}, rtac conjI,
           if n = 1 then K all_tac else rtac (mk_sumEN n),
diff -r 4eef5c2ff5ad -r 835fd053d17d src/HOL/Library/Sublist.thy
--- a/src/HOL/Library/Sublist.thy	Wed Aug 29 16:25:35 2012 +0900
+++ b/src/HOL/Library/Sublist.thy	Thu Aug 30 13:03:03 2012 +0900
@@ -5,7 +5,7 @@
 header {* List prefixes, suffixes, and embedding*}
 
 theory Sublist
-imports List Main
+imports Main
 begin
 
 subsection {* Prefix order on lists *}
diff -r 4eef5c2ff5ad -r 835fd053d17d src/HOL/Unix/Unix.thy
--- a/src/HOL/Unix/Unix.thy	Wed Aug 29 16:25:35 2012 +0900
+++ b/src/HOL/Unix/Unix.thy	Thu Aug 30 13:03:03 2012 +0900
@@ -952,7 +952,7 @@
     with tr obtain opt where root': "root' = update (path_of x) opt root"
       by cases auto
     show ?thesis
-    proof (rule prefix_cases)
+    proof (rule prefixeq_cases)
       assume "path_of x \<parallel> path"
       with inv root'
       have "\<And>perms. access root' path user\<^isub>1 perms = access root path user\<^isub>1 perms"
@@ -960,7 +960,7 @@
       with inv show "invariant root' path"
         by (simp only: invariant_def)
     next
-      assume "path_of x \<le> path"
+      assume "prefixeq (path_of x) path"
       then obtain ys where path: "path = path_of x @ ys" ..
 
       show ?thesis
@@ -997,7 +997,7 @@
           by (simp only: invariant_def access_def)
       qed
     next
-      assume "path < path_of x"
+      assume "prefix path (path_of x)"
       then obtain y ys where path: "path_of x = path @ y # ys" ..
 
       obtain dir' where