src/HOL/Library/List_lexord.thy
changeset 25502 9200b36280c0
parent 22845 5f9138bcb3d7
child 25595 6c48275f9c76
     1.1 --- a/src/HOL/Library/List_lexord.thy	Thu Nov 29 07:55:46 2007 +0100
     1.2 +++ b/src/HOL/Library/List_lexord.thy	Thu Nov 29 17:08:26 2007 +0100
     1.3 @@ -10,13 +10,11 @@
     1.4  begin
     1.5  
     1.6  instance list :: (ord) ord
     1.7 -  list_le_def:  "(xs::('a::ord) list) \<le> ys \<equiv> (xs < ys \<or> xs = ys)"
     1.8 -  list_less_def: "(xs::('a::ord) list) < ys \<equiv> (xs, ys) \<in> lexord {(u,v). u < v}" ..
     1.9 -
    1.10 -lemmas list_ord_defs [code func del] = list_less_def list_le_def
    1.11 +  list_less_def [code func del]: "(xs::('a::ord) list) < ys \<longleftrightarrow> (xs, ys) \<in> lexord {(u,v). u < v}"
    1.12 +  list_le_def [code func del]: "(xs::('a::ord) list) \<le> ys \<longleftrightarrow> (xs < ys \<or> xs = ys)" ..
    1.13  
    1.14  instance list :: (order) order
    1.15 -  apply (intro_classes, unfold list_ord_defs)
    1.16 +  apply (intro_classes, unfold list_less_def list_le_def)
    1.17    apply safe
    1.18    apply (rule_tac r1 = "{(a::'a,b). a < b}" in lexord_irreflexive [THEN notE])
    1.19    apply simp
    1.20 @@ -35,13 +33,11 @@
    1.21    done
    1.22  
    1.23  instance list :: (linorder) distrib_lattice
    1.24 -  "inf \<equiv> min"
    1.25 -  "sup \<equiv> max"
    1.26 +  [code func del]: "(inf \<Colon> 'a list \<Rightarrow> _) = min"
    1.27 +  [code func del]: "(sup \<Colon> 'a list \<Rightarrow> _) = max"
    1.28    by intro_classes
    1.29      (auto simp add: inf_list_def sup_list_def min_max.sup_inf_distrib1)
    1.30  
    1.31 -lemmas [code func del] = inf_list_def sup_list_def
    1.32 -
    1.33  lemma not_less_Nil [simp]: "\<not> (x < [])"
    1.34    by (unfold list_less_def) simp
    1.35  
    1.36 @@ -52,13 +48,13 @@
    1.37    by (unfold list_less_def) simp
    1.38  
    1.39  lemma le_Nil [simp]: "x \<le> [] \<longleftrightarrow> x = []"
    1.40 -  by (unfold list_ord_defs, cases x) auto
    1.41 +  by (unfold list_le_def, cases x) auto
    1.42  
    1.43  lemma Nil_le_Cons [simp]: "[] \<le> x"
    1.44 -  by (unfold list_ord_defs, cases x) auto
    1.45 +  by (unfold list_le_def, cases x) auto
    1.46  
    1.47  lemma Cons_le_Cons [simp]: "a # x \<le> b # y \<longleftrightarrow> a < b \<or> a = b \<and> x \<le> y"
    1.48 -  by (unfold list_ord_defs) auto
    1.49 +  by (unfold list_le_def) auto
    1.50  
    1.51  lemma less_code [code func]:
    1.52    "xs < ([]\<Colon>'a\<Colon>{eq, order} list) \<longleftrightarrow> False"