tuned imports;
authorwenzelm
Mon Aug 26 23:39:53 2013 +0200 (2013-08-26)
changeset 53214bae01293f4dd
parent 53213 a11e55f667db
child 53215 5e47c31c6f7c
child 53217 1a8673a6d669
child 53226 9cf8e2263ca7
tuned imports;
tuned proofs;
src/HOL/Library/List_lexord.thy
     1.1 --- a/src/HOL/Library/List_lexord.thy	Mon Aug 26 22:01:39 2013 +0200
     1.2 +++ b/src/HOL/Library/List_lexord.thy	Mon Aug 26 23:39:53 2013 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* Lexicographic order on lists *}
     1.5  
     1.6  theory List_lexord
     1.7 -imports List Main
     1.8 +imports Main
     1.9  begin
    1.10  
    1.11  instantiation list :: (ord) ord
    1.12 @@ -28,25 +28,33 @@
    1.13  next
    1.14    fix xs ys zs :: "'a list"
    1.15    assume "xs \<le> ys" and "ys \<le> zs"
    1.16 -  then show "xs \<le> zs" by (auto simp add: list_le_def list_less_def)
    1.17 -    (rule lexord_trans, auto intro: transI)
    1.18 +  then show "xs \<le> zs"
    1.19 +    apply (auto simp add: list_le_def list_less_def)
    1.20 +    apply (rule lexord_trans)
    1.21 +    apply (auto intro: transI)
    1.22 +    done
    1.23  next
    1.24    fix xs ys :: "'a list"
    1.25    assume "xs \<le> ys" and "ys \<le> xs"
    1.26 -  then show "xs = ys" apply (auto simp add: list_le_def list_less_def)
    1.27 -  apply (rule lexord_irreflexive [THEN notE])
    1.28 -  defer
    1.29 -  apply (rule lexord_trans) apply (auto intro: transI) done
    1.30 +  then show "xs = ys"
    1.31 +    apply (auto simp add: list_le_def list_less_def)
    1.32 +    apply (rule lexord_irreflexive [THEN notE])
    1.33 +    defer
    1.34 +    apply (rule lexord_trans)
    1.35 +    apply (auto intro: transI)
    1.36 +    done
    1.37  next
    1.38    fix xs ys :: "'a list"
    1.39 -  show "xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs" 
    1.40 -  apply (auto simp add: list_less_def list_le_def)
    1.41 -  defer
    1.42 -  apply (rule lexord_irreflexive [THEN notE])
    1.43 -  apply auto
    1.44 -  apply (rule lexord_irreflexive [THEN notE])
    1.45 -  defer
    1.46 -  apply (rule lexord_trans) apply (auto intro: transI) done
    1.47 +  show "xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs"
    1.48 +    apply (auto simp add: list_less_def list_le_def)
    1.49 +    defer
    1.50 +    apply (rule lexord_irreflexive [THEN notE])
    1.51 +    apply auto
    1.52 +    apply (rule lexord_irreflexive [THEN notE])
    1.53 +    defer
    1.54 +    apply (rule lexord_trans)
    1.55 +    apply (auto intro: transI)
    1.56 +    done
    1.57  qed
    1.58  
    1.59  instance list :: (linorder) linorder
    1.60 @@ -54,51 +62,47 @@
    1.61    fix xs ys :: "'a list"
    1.62    have "(xs, ys) \<in> lexord {(u, v). u < v} \<or> xs = ys \<or> (ys, xs) \<in> lexord {(u, v). u < v}"
    1.63      by (rule lexord_linear) auto
    1.64 -  then show "xs \<le> ys \<or> ys \<le> xs" 
    1.65 +  then show "xs \<le> ys \<or> ys \<le> xs"
    1.66      by (auto simp add: list_le_def list_less_def)
    1.67  qed
    1.68  
    1.69  instantiation list :: (linorder) distrib_lattice
    1.70  begin
    1.71  
    1.72 -definition
    1.73 -  "(inf \<Colon> 'a list \<Rightarrow> _) = min"
    1.74 +definition "(inf \<Colon> 'a list \<Rightarrow> _) = min"
    1.75  
    1.76 -definition
    1.77 -  "(sup \<Colon> 'a list \<Rightarrow> _) = max"
    1.78 +definition "(sup \<Colon> 'a list \<Rightarrow> _) = max"
    1.79  
    1.80  instance
    1.81 -  by intro_classes
    1.82 -    (auto simp add: inf_list_def sup_list_def min_max.sup_inf_distrib1)
    1.83 +  by default (auto simp add: inf_list_def sup_list_def min_max.sup_inf_distrib1)
    1.84  
    1.85  end
    1.86  
    1.87 -lemma not_less_Nil [simp]: "\<not> (x < [])"
    1.88 -  by (unfold list_less_def) simp
    1.89 +lemma not_less_Nil [simp]: "\<not> x < []"
    1.90 +  by (simp add: list_less_def)
    1.91  
    1.92  lemma Nil_less_Cons [simp]: "[] < a # x"
    1.93 -  by (unfold list_less_def) simp
    1.94 +  by (simp add: list_less_def)
    1.95  
    1.96  lemma Cons_less_Cons [simp]: "a # x < b # y \<longleftrightarrow> a < b \<or> a = b \<and> x < y"
    1.97 -  by (unfold list_less_def) simp
    1.98 +  by (simp add: list_less_def)
    1.99  
   1.100  lemma le_Nil [simp]: "x \<le> [] \<longleftrightarrow> x = []"
   1.101 -  by (unfold list_le_def, cases x) auto
   1.102 +  unfolding list_le_def by (cases x) auto
   1.103  
   1.104  lemma Nil_le_Cons [simp]: "[] \<le> x"
   1.105 -  by (unfold list_le_def, cases x) auto
   1.106 +  unfolding list_le_def by (cases x) auto
   1.107  
   1.108  lemma Cons_le_Cons [simp]: "a # x \<le> b # y \<longleftrightarrow> a < b \<or> a = b \<and> x \<le> y"
   1.109 -  by (unfold list_le_def) auto
   1.110 +  unfolding list_le_def by auto
   1.111  
   1.112  instantiation list :: (order) order_bot
   1.113  begin
   1.114  
   1.115 -definition
   1.116 -  "bot = []"
   1.117 +definition "bot = []"
   1.118  
   1.119 -instance proof
   1.120 -qed (simp add: bot_list_def)
   1.121 +instance
   1.122 +  by default (simp add: bot_list_def)
   1.123  
   1.124  end
   1.125