src/HOL/Library/Char_ord.thy
changeset 23394 474ff28210c0
parent 22845 5f9138bcb3d7
child 25502 9200b36280c0
     1.1 --- a/src/HOL/Library/Char_ord.thy	Thu Jun 14 23:04:36 2007 +0200
     1.2 +++ b/src/HOL/Library/Char_ord.thy	Thu Jun 14 23:04:39 2007 +0200
     1.3 @@ -13,32 +13,36 @@
     1.4    nibble_less_eq_def: "n \<le> m \<equiv> nat_of_nibble n \<le> nat_of_nibble m"
     1.5    nibble_less_def: "n < m \<equiv> nat_of_nibble n < nat_of_nibble m"
     1.6  proof
     1.7 -  fix n :: nibble show "n \<le> n" unfolding nibble_less_eq_def nibble_less_def by auto
     1.8 +  fix n :: nibble
     1.9 +  show "n \<le> n" unfolding nibble_less_eq_def nibble_less_def by auto
    1.10  next
    1.11    fix n m q :: nibble
    1.12    assume "n \<le> m"
    1.13 -  and "m \<le> q"
    1.14 +    and "m \<le> q"
    1.15    then show "n \<le> q" unfolding nibble_less_eq_def nibble_less_def by auto
    1.16  next
    1.17    fix n m :: nibble
    1.18    assume "n \<le> m"
    1.19 -  and "m \<le> n"
    1.20 -  then show "n = m" unfolding nibble_less_eq_def nibble_less_def by (auto simp add: nat_of_nibble_eq)
    1.21 +    and "m \<le> n"
    1.22 +  then show "n = m"
    1.23 +    unfolding nibble_less_eq_def nibble_less_def
    1.24 +    by (auto simp add: nat_of_nibble_eq)
    1.25  next
    1.26    fix n m :: nibble
    1.27    show "n < m \<longleftrightarrow> n \<le> m \<and> n \<noteq> m"
    1.28 -  unfolding nibble_less_eq_def nibble_less_def less_le by (auto simp add: nat_of_nibble_eq)
    1.29 +    unfolding nibble_less_eq_def nibble_less_def less_le
    1.30 +    by (auto simp add: nat_of_nibble_eq)
    1.31  next
    1.32    fix n m :: nibble
    1.33    show "n \<le> m \<or> m \<le> n"
    1.34 -  unfolding nibble_less_eq_def by auto
    1.35 +    unfolding nibble_less_eq_def by auto
    1.36  qed
    1.37  
    1.38  instance nibble :: distrib_lattice
    1.39 -  "inf \<equiv> min"
    1.40 -  "sup \<equiv> max"
    1.41 -  by default
    1.42 -    (auto simp add: inf_nibble_def sup_nibble_def min_max.sup_inf_distrib1)
    1.43 +    "inf \<equiv> min"
    1.44 +    "sup \<equiv> max"
    1.45 +  by default (auto simp add:
    1.46 +    inf_nibble_def sup_nibble_def min_max.sup_inf_distrib1)
    1.47  
    1.48  instance char :: linorder
    1.49    char_less_eq_def: "c1 \<le> c2 \<equiv> case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow>
    1.50 @@ -50,10 +54,10 @@
    1.51  lemmas [code func del] = char_less_eq_def char_less_def
    1.52  
    1.53  instance char :: distrib_lattice
    1.54 -  "inf \<equiv> min"
    1.55 -  "sup \<equiv> max"
    1.56 -  by default
    1.57 -    (auto simp add: inf_char_def sup_char_def min_max.sup_inf_distrib1)
    1.58 +    "inf \<equiv> min"
    1.59 +    "sup \<equiv> max"
    1.60 +  by default (auto simp add:
    1.61 +    inf_char_def sup_char_def min_max.sup_inf_distrib1)
    1.62  
    1.63  lemma [simp, code func]:
    1.64    shows char_less_eq_simp: "Char n1 m1 \<le> Char n2 m2 \<longleftrightarrow> n1 < n2 \<or> n1 = n2 \<and> m1 \<le> m2"