src/HOL/Library/Char_ord.thy
changeset 63462 c1fe30f2bc32
parent 62597 b3f2b8c906a6
child 67399 eab6ce8368fa
     1.1 --- a/src/HOL/Library/Char_ord.thy	Tue Jul 12 14:53:47 2016 +0200
     1.2 +++ b/src/HOL/Library/Char_ord.thy	Tue Jul 12 15:45:32 2016 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  section \<open>Order on characters\<close>
     1.5  
     1.6  theory Char_ord
     1.7 -imports Main
     1.8 +  imports Main
     1.9  begin
    1.10  
    1.11  instantiation char :: linorder
    1.12 @@ -20,17 +20,19 @@
    1.13  end
    1.14  
    1.15  lemma less_eq_char_simps:
    1.16 -  "(0 :: char) \<le> c"
    1.17 +  "0 \<le> c"
    1.18    "Char k \<le> 0 \<longleftrightarrow> numeral k mod 256 = (0 :: nat)"
    1.19    "Char k \<le> Char l \<longleftrightarrow> numeral k mod 256 \<le> (numeral l mod 256 :: nat)"
    1.20 +  for c :: char
    1.21    by (simp_all add: Char_def less_eq_char_def)
    1.22  
    1.23  lemma less_char_simps:
    1.24 -  "\<not> c < (0 :: char)"
    1.25 +  "\<not> c < 0"
    1.26    "0 < Char k \<longleftrightarrow> (0 :: nat) < numeral k mod 256"
    1.27    "Char k < Char l \<longleftrightarrow> numeral k mod 256 < (numeral l mod 256 :: nat)"
    1.28 +  for c :: char
    1.29    by (simp_all add: Char_def less_char_def)
    1.30 -  
    1.31 +
    1.32  instantiation char :: distrib_lattice
    1.33  begin
    1.34  
    1.35 @@ -45,28 +47,34 @@
    1.36  instantiation String.literal :: linorder
    1.37  begin
    1.38  
    1.39 -context includes literal.lifting begin
    1.40 -lift_definition less_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> bool" is "ord.lexordp op <" .
    1.41 -lift_definition less_eq_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> bool" is "ord.lexordp_eq op <" .
    1.42 +context includes literal.lifting
    1.43 +begin
    1.44 +
    1.45 +lift_definition less_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> bool"
    1.46 +  is "ord.lexordp op <" .
    1.47 +
    1.48 +lift_definition less_eq_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> bool"
    1.49 +  is "ord.lexordp_eq op <" .
    1.50  
    1.51  instance
    1.52  proof -
    1.53    interpret linorder "ord.lexordp_eq op <" "ord.lexordp op < :: string \<Rightarrow> string \<Rightarrow> bool"
    1.54 -    by(rule linorder.lexordp_linorder[where less_eq="op \<le>"])(unfold_locales)
    1.55 +    by (rule linorder.lexordp_linorder[where less_eq="op \<le>"]) unfold_locales
    1.56    show "PROP ?thesis"
    1.57 -    by(intro_classes)(transfer, simp add: less_le_not_le linear)+
    1.58 +    by intro_classes (transfer, simp add: less_le_not_le linear)+
    1.59  qed
    1.60  
    1.61  end
    1.62 +
    1.63  end
    1.64  
    1.65 -lemma less_literal_code [code]: 
    1.66 +lemma less_literal_code [code]:
    1.67    "op < = (\<lambda>xs ys. ord.lexordp op < (String.explode xs) (String.explode ys))"
    1.68 -by(simp add: less_literal.rep_eq fun_eq_iff)
    1.69 +  by (simp add: less_literal.rep_eq fun_eq_iff)
    1.70  
    1.71  lemma less_eq_literal_code [code]:
    1.72    "op \<le> = (\<lambda>xs ys. ord.lexordp_eq op < (String.explode xs) (String.explode ys))"
    1.73 -by(simp add: less_eq_literal.rep_eq fun_eq_iff)
    1.74 +  by (simp add: less_eq_literal.rep_eq fun_eq_iff)
    1.75  
    1.76  lifting_update literal.lifting
    1.77  lifting_forget literal.lifting