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
```