src/HOL/Library/Sublist_Order.thy
changeset 27682 25aceefd4786
parent 27487 c8a6ce181805
child 28562 4e74209f113e
     1.1 --- a/src/HOL/Library/Sublist_Order.thy	Fri Jul 25 12:03:32 2008 +0200
     1.2 +++ b/src/HOL/Library/Sublist_Order.thy	Fri Jul 25 12:03:34 2008 +0200
     1.3 @@ -47,7 +47,7 @@
     1.4    using assms by (induct rule: less_eq_list.induct) blast+
     1.5  
     1.6  definition
     1.7 -  [code func del]: "(xs \<Colon> 'a list) < ys \<longleftrightarrow> xs \<le> ys \<and> xs \<noteq> ys"
     1.8 +  [code func del]: "(xs \<Colon> 'a list) < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs"
     1.9  
    1.10  lemma ileq_length: "xs \<le> ys \<Longrightarrow> length xs \<le> length ys"
    1.11    by (induct rule: ileq_induct) auto
    1.12 @@ -56,7 +56,7 @@
    1.13  
    1.14  instance proof
    1.15    fix xs ys :: "'a list"
    1.16 -  show "xs < ys \<longleftrightarrow> xs \<le> ys \<and> xs \<noteq> ys" unfolding less_list_def ..
    1.17 +  show "xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs" unfolding less_list_def .. 
    1.18  next
    1.19    fix xs :: "'a list"
    1.20    show "xs \<le> xs" by (induct xs) (auto intro!: ileq_empty ileq_drop ileq_take)
    1.21 @@ -140,7 +140,7 @@
    1.22    assumes "xs < ys"
    1.23    shows "length xs < length ys"
    1.24  proof -
    1.25 -  from assms have "xs \<le> ys" and "xs \<noteq> ys" by (simp_all add: less_list_def)
    1.26 +  from assms have "xs \<le> ys" and "xs \<noteq> ys" by (simp_all add: less_le)
    1.27    moreover with ileq_length have "length xs \<le> length ys" by auto
    1.28    ultimately show ?thesis by (auto intro: ileq_same_length)
    1.29  qed
    1.30 @@ -154,9 +154,9 @@
    1.31  lemma ilt_below_empty[simp]: "xs < [] \<Longrightarrow> False"
    1.32    by (auto dest: ilt_length)
    1.33  lemma ilt_drop: "xs < ys \<Longrightarrow> xs < x # ys"
    1.34 -  by (unfold less_list_def) (auto intro: ileq_intros)
    1.35 +  by (unfold less_le) (auto intro: ileq_intros)
    1.36  lemma ilt_take: "xs < ys \<Longrightarrow> x # xs < x # ys"
    1.37 -  by (unfold less_list_def) (auto intro: ileq_intros)
    1.38 +  by (unfold less_le) (auto intro: ileq_intros)
    1.39  lemma ilt_drop_many: "xs < ys \<Longrightarrow> xs < zs @ ys"
    1.40    by (induct zs) (auto intro: ilt_drop)
    1.41  lemma ilt_take_many: "xs < ys \<Longrightarrow> zs @ xs < zs @ ys"
    1.42 @@ -168,7 +168,7 @@
    1.43  lemma ileq_rev_take: "xs \<le> ys \<Longrightarrow> xs @ [x] \<le> ys @ [x]"
    1.44    by (induct rule: ileq_induct) (auto intro: ileq_intros ileq_drop_many)
    1.45  lemma ilt_rev_take: "xs < ys \<Longrightarrow> xs @ [x] < ys @ [x]"
    1.46 -  by (unfold less_list_def) (auto dest: ileq_rev_take)
    1.47 +  by (unfold less_le) (auto dest: ileq_rev_take)
    1.48  lemma ileq_rev_drop: "xs \<le> ys \<Longrightarrow> xs \<le> ys @ [x]"
    1.49    by (induct rule: ileq_induct) (auto intro: ileq_intros)
    1.50  lemma ileq_rev_drop_many: "xs \<le> ys \<Longrightarrow> xs \<le> ys @ zs"