src/HOL/Library/List_lexord.thy
changeset 27682 25aceefd4786
parent 27487 c8a6ce181805
child 28562 4e74209f113e
     1.1 --- a/src/HOL/Library/List_lexord.thy	Fri Jul 25 12:03:32 2008 +0200
     1.2 +++ b/src/HOL/Library/List_lexord.thy	Fri Jul 25 12:03:34 2008 +0200
     1.3 @@ -23,23 +23,41 @@
     1.4  end
     1.5  
     1.6  instance list :: (order) order
     1.7 -  apply (intro_classes, unfold list_less_def list_le_def)
     1.8 -  apply safe
     1.9 -  apply (rule_tac r1 = "{(a::'a,b). a < b}" in lexord_irreflexive [THEN notE])
    1.10 -  apply simp
    1.11 -  apply assumption
    1.12 -  apply (blast intro: lexord_trans transI order_less_trans)
    1.13 -  apply (rule_tac r1 = "{(a::'a,b). a < b}" in lexord_irreflexive [THEN notE])
    1.14 -  apply simp
    1.15 -  apply (blast intro: lexord_trans transI order_less_trans)
    1.16 -  done
    1.17 +proof
    1.18 +  fix xs :: "'a list"
    1.19 +  show "xs \<le> xs" by (simp add: list_le_def)
    1.20 +next
    1.21 +  fix xs ys zs :: "'a list"
    1.22 +  assume "xs \<le> ys" and "ys \<le> zs"
    1.23 +  then show "xs \<le> zs" by (auto simp add: list_le_def list_less_def)
    1.24 +    (rule lexord_trans, auto intro: transI)
    1.25 +next
    1.26 +  fix xs ys :: "'a list"
    1.27 +  assume "xs \<le> ys" and "ys \<le> xs"
    1.28 +  then show "xs = ys" apply (auto simp add: list_le_def list_less_def)
    1.29 +  apply (rule lexord_irreflexive [THEN notE])
    1.30 +  defer
    1.31 +  apply (rule lexord_trans) apply (auto intro: transI) done
    1.32 +next
    1.33 +  fix xs ys :: "'a list"
    1.34 +  show "xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs" 
    1.35 +  apply (auto simp add: list_less_def list_le_def)
    1.36 +  defer
    1.37 +  apply (rule lexord_irreflexive [THEN notE])
    1.38 +  apply auto
    1.39 +  apply (rule lexord_irreflexive [THEN notE])
    1.40 +  defer
    1.41 +  apply (rule lexord_trans) apply (auto intro: transI) done
    1.42 +qed
    1.43  
    1.44  instance list :: (linorder) linorder
    1.45 -  apply (intro_classes, unfold list_le_def list_less_def, safe)
    1.46 -  apply (cut_tac x = x and y = y and  r = "{(a,b). a < b}"  in lexord_linear)
    1.47 -   apply force
    1.48 -  apply simp
    1.49 -  done
    1.50 +proof
    1.51 +  fix xs ys :: "'a list"
    1.52 +  have "(xs, ys) \<in> lexord {(u, v). u < v} \<or> xs = ys \<or> (ys, xs) \<in> lexord {(u, v). u < v}"
    1.53 +    by (rule lexord_linear) auto
    1.54 +  then show "xs \<le> ys \<or> ys \<le> xs" 
    1.55 +    by (auto simp add: list_le_def list_less_def)
    1.56 +qed
    1.57  
    1.58  instantiation list :: (linorder) distrib_lattice
    1.59  begin