38 fix xs :: "'a list" |
38 fix xs :: "'a list" |
39 show "xs \<le> xs" by (simp add: less_eq_list_def) |
39 show "xs \<le> xs" by (simp add: less_eq_list_def) |
40 next |
40 next |
41 fix xs ys :: "'a list" |
41 fix xs ys :: "'a list" |
42 assume "xs <= ys" and "ys <= xs" |
42 assume "xs <= ys" and "ys <= xs" |
43 thus "xs = ys" by (unfold less_eq_list_def) (rule sub_antisym) |
43 thus "xs = ys" by (unfold less_eq_list_def) (rule sublisteq_antisym) |
44 next |
44 next |
45 fix xs ys zs :: "'a list" |
45 fix xs ys zs :: "'a list" |
46 assume "xs <= ys" and "ys <= zs" |
46 assume "xs <= ys" and "ys <= zs" |
47 thus "xs <= zs" by (unfold less_eq_list_def) (rule sub_trans) |
47 thus "xs <= zs" by (unfold less_eq_list_def) (rule sublisteq_trans) |
48 qed |
48 qed |
49 |
49 |
50 lemmas less_eq_list_induct [consumes 1, case_names empty drop take] = |
50 lemmas less_eq_list_induct [consumes 1, case_names empty drop take] = |
51 emb.induct [of "op =", folded less_eq_list_def] |
51 list_hembeq.induct [of "op =", folded less_eq_list_def] |
52 lemmas less_eq_list_drop = emb.emb_Cons [of "op =", folded less_eq_list_def] |
52 lemmas less_eq_list_drop = list_hembeq.list_hembeq_Cons [of "op =", folded less_eq_list_def] |
53 lemmas le_list_Cons2_iff [simp, code] = sub_Cons2_iff [folded less_eq_list_def] |
53 lemmas le_list_Cons2_iff [simp, code] = sublisteq_Cons2_iff [folded less_eq_list_def] |
54 lemmas le_list_map = sub_map [folded less_eq_list_def] |
54 lemmas le_list_map = sublisteq_map [folded less_eq_list_def] |
55 lemmas le_list_filter = sub_filter [folded less_eq_list_def] |
55 lemmas le_list_filter = sublisteq_filter [folded less_eq_list_def] |
56 lemmas le_list_length = emb_length [of "op =", folded less_eq_list_def] |
56 lemmas le_list_length = list_hembeq_length [of "op =", folded less_eq_list_def] |
57 |
57 |
58 lemma less_list_length: "xs < ys \<Longrightarrow> length xs < length ys" |
58 lemma less_list_length: "xs < ys \<Longrightarrow> length xs < length ys" |
59 by (metis emb_length sub_same_length le_neq_implies_less less_list_def less_eq_list_def) |
59 by (metis list_hembeq_length sublisteq_same_length le_neq_implies_less less_list_def less_eq_list_def) |
60 |
60 |
61 lemma less_list_empty [simp]: "[] < xs \<longleftrightarrow> xs \<noteq> []" |
61 lemma less_list_empty [simp]: "[] < xs \<longleftrightarrow> xs \<noteq> []" |
62 by (metis less_eq_list_def emb_Nil order_less_le) |
62 by (metis less_eq_list_def list_hembeq_Nil order_less_le) |
63 |
63 |
64 lemma less_list_below_empty [simp]: "xs < [] \<longleftrightarrow> False" |
64 lemma less_list_below_empty [simp]: "xs < [] \<longleftrightarrow> False" |
65 by (metis emb_Nil less_eq_list_def less_list_def) |
65 by (metis list_hembeq_Nil less_eq_list_def less_list_def) |
66 |
66 |
67 lemma less_list_drop: "xs < ys \<Longrightarrow> xs < x # ys" |
67 lemma less_list_drop: "xs < ys \<Longrightarrow> xs < x # ys" |
68 by (unfold less_le less_eq_list_def) (auto) |
68 by (unfold less_le less_eq_list_def) (auto) |
69 |
69 |
70 lemma less_list_take_iff: "x # xs < x # ys \<longleftrightarrow> xs < ys" |
70 lemma less_list_take_iff: "x # xs < x # ys \<longleftrightarrow> xs < ys" |
71 by (metis sub_Cons2_iff less_list_def less_eq_list_def) |
71 by (metis sublisteq_Cons2_iff less_list_def less_eq_list_def) |
72 |
72 |
73 lemma less_list_drop_many: "xs < ys \<Longrightarrow> xs < zs @ ys" |
73 lemma less_list_drop_many: "xs < ys \<Longrightarrow> xs < zs @ ys" |
74 by (metis sub_append_le_same_iff sub_drop_many order_less_le self_append_conv2 less_eq_list_def) |
74 by (metis sublisteq_append_le_same_iff sublisteq_drop_many order_less_le self_append_conv2 less_eq_list_def) |
75 |
75 |
76 lemma less_list_take_many_iff: "zs @ xs < zs @ ys \<longleftrightarrow> xs < ys" |
76 lemma less_list_take_many_iff: "zs @ xs < zs @ ys \<longleftrightarrow> xs < ys" |
77 by (metis less_list_def less_eq_list_def sub_append') |
77 by (metis less_list_def less_eq_list_def sublisteq_append') |
78 |
78 |
79 lemma less_list_rev_take: "xs @ zs < ys @ zs \<longleftrightarrow> xs < ys" |
79 lemma less_list_rev_take: "xs @ zs < ys @ zs \<longleftrightarrow> xs < ys" |
80 by (unfold less_le less_eq_list_def) auto |
80 by (unfold less_le less_eq_list_def) auto |
81 |
81 |
82 end |
82 end |