src/HOL/Library/Sublist_Order.thy
changeset 50516 ed6b40d15d1c
parent 49093 fdc301f592c4
child 57497 4106a2bc066a
     1.1 --- a/src/HOL/Library/Sublist_Order.thy	Thu Dec 13 09:21:45 2012 +0100
     1.2 +++ b/src/HOL/Library/Sublist_Order.thy	Thu Dec 13 13:11:38 2012 +0100
     1.3 @@ -21,7 +21,7 @@
     1.4  begin
     1.5  
     1.6  definition
     1.7 -  "(xs :: 'a list) \<le> ys \<longleftrightarrow> sub xs ys"
     1.8 +  "(xs :: 'a list) \<le> ys \<longleftrightarrow> sublisteq xs ys"
     1.9  
    1.10  definition
    1.11    "(xs :: 'a list) < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs"
    1.12 @@ -40,41 +40,41 @@
    1.13  next
    1.14    fix xs ys :: "'a list"
    1.15    assume "xs <= ys" and "ys <= xs"
    1.16 -  thus "xs = ys" by (unfold less_eq_list_def) (rule sub_antisym)
    1.17 +  thus "xs = ys" by (unfold less_eq_list_def) (rule sublisteq_antisym)
    1.18  next
    1.19    fix xs ys zs :: "'a list"
    1.20    assume "xs <= ys" and "ys <= zs"
    1.21 -  thus "xs <= zs" by (unfold less_eq_list_def) (rule sub_trans)
    1.22 +  thus "xs <= zs" by (unfold less_eq_list_def) (rule sublisteq_trans)
    1.23  qed
    1.24  
    1.25  lemmas less_eq_list_induct [consumes 1, case_names empty drop take] =
    1.26 -  emb.induct [of "op =", folded less_eq_list_def]
    1.27 -lemmas less_eq_list_drop = emb.emb_Cons [of "op =", folded less_eq_list_def]
    1.28 -lemmas le_list_Cons2_iff [simp, code] = sub_Cons2_iff [folded less_eq_list_def]
    1.29 -lemmas le_list_map = sub_map [folded less_eq_list_def]
    1.30 -lemmas le_list_filter = sub_filter [folded less_eq_list_def]
    1.31 -lemmas le_list_length = emb_length [of "op =", folded less_eq_list_def]
    1.32 +  list_hembeq.induct [of "op =", folded less_eq_list_def]
    1.33 +lemmas less_eq_list_drop = list_hembeq.list_hembeq_Cons [of "op =", folded less_eq_list_def]
    1.34 +lemmas le_list_Cons2_iff [simp, code] = sublisteq_Cons2_iff [folded less_eq_list_def]
    1.35 +lemmas le_list_map = sublisteq_map [folded less_eq_list_def]
    1.36 +lemmas le_list_filter = sublisteq_filter [folded less_eq_list_def]
    1.37 +lemmas le_list_length = list_hembeq_length [of "op =", folded less_eq_list_def]
    1.38  
    1.39  lemma less_list_length: "xs < ys \<Longrightarrow> length xs < length ys"
    1.40 -  by (metis emb_length sub_same_length le_neq_implies_less less_list_def less_eq_list_def)
    1.41 +  by (metis list_hembeq_length sublisteq_same_length le_neq_implies_less less_list_def less_eq_list_def)
    1.42  
    1.43  lemma less_list_empty [simp]: "[] < xs \<longleftrightarrow> xs \<noteq> []"
    1.44 -  by (metis less_eq_list_def emb_Nil order_less_le)
    1.45 +  by (metis less_eq_list_def list_hembeq_Nil order_less_le)
    1.46  
    1.47  lemma less_list_below_empty [simp]: "xs < [] \<longleftrightarrow> False"
    1.48 -  by (metis emb_Nil less_eq_list_def less_list_def)
    1.49 +  by (metis list_hembeq_Nil less_eq_list_def less_list_def)
    1.50  
    1.51  lemma less_list_drop: "xs < ys \<Longrightarrow> xs < x # ys"
    1.52    by (unfold less_le less_eq_list_def) (auto)
    1.53  
    1.54  lemma less_list_take_iff: "x # xs < x # ys \<longleftrightarrow> xs < ys"
    1.55 -  by (metis sub_Cons2_iff less_list_def less_eq_list_def)
    1.56 +  by (metis sublisteq_Cons2_iff less_list_def less_eq_list_def)
    1.57  
    1.58  lemma less_list_drop_many: "xs < ys \<Longrightarrow> xs < zs @ ys"
    1.59 -  by (metis sub_append_le_same_iff sub_drop_many order_less_le self_append_conv2 less_eq_list_def)
    1.60 +  by (metis sublisteq_append_le_same_iff sublisteq_drop_many order_less_le self_append_conv2 less_eq_list_def)
    1.61  
    1.62  lemma less_list_take_many_iff: "zs @ xs < zs @ ys \<longleftrightarrow> xs < ys"
    1.63 -  by (metis less_list_def less_eq_list_def sub_append')
    1.64 +  by (metis less_list_def less_eq_list_def sublisteq_append')
    1.65  
    1.66  lemma less_list_rev_take: "xs @ zs < ys @ zs \<longleftrightarrow> xs < ys"
    1.67    by (unfold less_le less_eq_list_def) auto