39 show "xs \<le> zs" if "xs \<le> ys" and "ys \<le> zs" |
39 show "xs \<le> zs" if "xs \<le> ys" and "ys \<le> zs" |
40 using that unfolding less_eq_list_def by (rule subseq_order.order_trans) |
40 using that unfolding less_eq_list_def by (rule subseq_order.order_trans) |
41 qed |
41 qed |
42 |
42 |
43 lemmas less_eq_list_induct [consumes 1, case_names empty drop take] = |
43 lemmas less_eq_list_induct [consumes 1, case_names empty drop take] = |
44 list_emb.induct [of "op =", folded less_eq_list_def] |
44 list_emb.induct [of "(=)", folded less_eq_list_def] |
45 lemmas less_eq_list_drop = list_emb.list_emb_Cons [of "op =", folded less_eq_list_def] |
45 lemmas less_eq_list_drop = list_emb.list_emb_Cons [of "(=)", folded less_eq_list_def] |
46 lemmas le_list_Cons2_iff [simp, code] = subseq_Cons2_iff [folded less_eq_list_def] |
46 lemmas le_list_Cons2_iff [simp, code] = subseq_Cons2_iff [folded less_eq_list_def] |
47 lemmas le_list_map = subseq_map [folded less_eq_list_def] |
47 lemmas le_list_map = subseq_map [folded less_eq_list_def] |
48 lemmas le_list_filter = subseq_filter [folded less_eq_list_def] |
48 lemmas le_list_filter = subseq_filter [folded less_eq_list_def] |
49 lemmas le_list_length = list_emb_length [of "op =", folded less_eq_list_def] |
49 lemmas le_list_length = list_emb_length [of "(=)", folded less_eq_list_def] |
50 |
50 |
51 lemma less_list_length: "xs < ys \<Longrightarrow> length xs < length ys" |
51 lemma less_list_length: "xs < ys \<Longrightarrow> length xs < length ys" |
52 by (metis list_emb_length subseq_same_length le_neq_implies_less less_list_def less_eq_list_def) |
52 by (metis list_emb_length subseq_same_length le_neq_implies_less less_list_def less_eq_list_def) |
53 |
53 |
54 lemma less_list_empty [simp]: "[] < xs \<longleftrightarrow> xs \<noteq> []" |
54 lemma less_list_empty [simp]: "[] < xs \<longleftrightarrow> xs \<noteq> []" |