src/HOL/Library/Sublist_Order.thy
changeset 49093 fdc301f592c4
parent 49088 5cd8b4426a57
child 50516 ed6b40d15d1c
     1.1 --- a/src/HOL/Library/Sublist_Order.thy	Thu Aug 30 13:44:15 2012 +0900
     1.2 +++ b/src/HOL/Library/Sublist_Order.thy	Thu Aug 30 15:44:03 2012 +0900
     1.3 @@ -47,6 +47,14 @@
     1.4    thus "xs <= zs" by (unfold less_eq_list_def) (rule sub_trans)
     1.5  qed
     1.6  
     1.7 +lemmas less_eq_list_induct [consumes 1, case_names empty drop take] =
     1.8 +  emb.induct [of "op =", folded less_eq_list_def]
     1.9 +lemmas less_eq_list_drop = emb.emb_Cons [of "op =", folded less_eq_list_def]
    1.10 +lemmas le_list_Cons2_iff [simp, code] = sub_Cons2_iff [folded less_eq_list_def]
    1.11 +lemmas le_list_map = sub_map [folded less_eq_list_def]
    1.12 +lemmas le_list_filter = sub_filter [folded less_eq_list_def]
    1.13 +lemmas le_list_length = emb_length [of "op =", folded less_eq_list_def]
    1.14 +
    1.15  lemma less_list_length: "xs < ys \<Longrightarrow> length xs < length ys"
    1.16    by (metis emb_length sub_same_length le_neq_implies_less less_list_def less_eq_list_def)
    1.17