clarified session;
authorwenzelm
Thu Sep 01 20:59:51 2016 +0200 (2016-09-01)
changeset 637626920b1885eff
parent 63761 2ca536d0163e
child 63763 0f61ea70d384
clarified session;
misc tuning and modernization;
src/HOL/Library/Library.thy
src/HOL/Library/Saturated.thy
src/HOL/Library/Type_Length.thy
src/HOL/Word/Type_Length.thy
src/HOL/Word/Word.thy
     1.1 --- a/src/HOL/Library/Library.thy	Thu Sep 01 20:34:43 2016 +0200
     1.2 +++ b/src/HOL/Library/Library.thy	Thu Sep 01 20:59:51 2016 +0200
     1.3 @@ -83,6 +83,7 @@
     1.4    Sum_of_Squares
     1.5    Transitive_Closure_Table
     1.6    Tree_Multiset
     1.7 +  Type_Length
     1.8    While_Combinator
     1.9  begin
    1.10  end
     2.1 --- a/src/HOL/Library/Saturated.thy	Thu Sep 01 20:34:43 2016 +0200
     2.2 +++ b/src/HOL/Library/Saturated.thy	Thu Sep 01 20:59:51 2016 +0200
     2.3 @@ -7,7 +7,7 @@
     2.4  section \<open>Saturated arithmetic\<close>
     2.5  
     2.6  theory Saturated
     2.7 -imports Numeral_Type "~~/src/HOL/Word/Type_Length"
     2.8 +imports Numeral_Type Type_Length
     2.9  begin
    2.10  
    2.11  subsection \<open>The type of saturated naturals\<close>
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Library/Type_Length.thy	Thu Sep 01 20:59:51 2016 +0200
     3.3 @@ -0,0 +1,54 @@
     3.4 +(*  Title:      HOL/Library/Type_Length.thy
     3.5 +    Author:     John Matthews, Galois Connections, Inc., Copyright 2006
     3.6 +*)
     3.7 +
     3.8 +section \<open>Assigning lengths to types by type classes\<close>
     3.9 +
    3.10 +theory Type_Length
    3.11 +imports Numeral_Type
    3.12 +begin
    3.13 +
    3.14 +text \<open>
    3.15 +  The aim of this is to allow any type as index type, but to provide a
    3.16 +  default instantiation for numeral types. This independence requires
    3.17 +  some duplication with the definitions in \<^file>\<open>Numeral_Type.thy\<close>.
    3.18 +\<close>
    3.19 +
    3.20 +class len0 =
    3.21 +  fixes len_of :: "'a itself \<Rightarrow> nat"
    3.22 +
    3.23 +text \<open>Some theorems are only true on words with length greater 0.\<close>
    3.24 +
    3.25 +class len = len0 +
    3.26 +  assumes len_gt_0 [iff]: "0 < len_of TYPE ('a)"
    3.27 +
    3.28 +instantiation num0 and num1 :: len0
    3.29 +begin
    3.30 +
    3.31 +definition len_num0: "len_of (_ :: num0 itself) = 0"
    3.32 +definition len_num1: "len_of (_ :: num1 itself) = 1"
    3.33 +
    3.34 +instance ..
    3.35 +
    3.36 +end
    3.37 +
    3.38 +instantiation bit0 and bit1 :: (len0) len0
    3.39 +begin
    3.40 +
    3.41 +definition len_bit0: "len_of (_ :: 'a::len0 bit0 itself) = 2 * len_of TYPE('a)"
    3.42 +definition len_bit1: "len_of (_ :: 'a::len0 bit1 itself) = 2 * len_of TYPE('a) + 1"
    3.43 +
    3.44 +instance ..
    3.45 +
    3.46 +end
    3.47 +
    3.48 +lemmas len_of_numeral_defs [simp] = len_num0 len_num1 len_bit0 len_bit1
    3.49 +
    3.50 +instance num1 :: len
    3.51 +  by standard simp
    3.52 +instance bit0 :: (len) len
    3.53 +  by standard simp
    3.54 +instance bit1 :: (len0) len
    3.55 +  by standard simp
    3.56 +
    3.57 +end
     4.1 --- a/src/HOL/Word/Type_Length.thy	Thu Sep 01 20:34:43 2016 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,60 +0,0 @@
     4.4 -(*  Title:      HOL/Word/Type_Length.thy
     4.5 -    Author:     John Matthews, Galois Connections, Inc., copyright 2006
     4.6 -*)
     4.7 -
     4.8 -section \<open>Assigning lengths to types by typeclasses\<close>
     4.9 -
    4.10 -theory Type_Length
    4.11 -imports "~~/src/HOL/Library/Numeral_Type"
    4.12 -begin
    4.13 -
    4.14 -text \<open>
    4.15 -  The aim of this is to allow any type as index type, but to provide a
    4.16 -  default instantiation for numeral types. This independence requires
    4.17 -  some duplication with the definitions in \<open>Numeral_Type\<close>.
    4.18 -\<close>
    4.19 -
    4.20 -class len0 =
    4.21 -  fixes len_of :: "'a itself \<Rightarrow> nat"
    4.22 -
    4.23 -text \<open>
    4.24 -  Some theorems are only true on words with length greater 0.
    4.25 -\<close>
    4.26 -
    4.27 -class len = len0 +
    4.28 -  assumes len_gt_0 [iff]: "0 < len_of TYPE ('a)"
    4.29 -
    4.30 -instantiation num0 and num1 :: len0
    4.31 -begin
    4.32 -
    4.33 -definition
    4.34 -  len_num0:  "len_of (x::num0 itself) = 0"
    4.35 -
    4.36 -definition
    4.37 -  len_num1: "len_of (x::num1 itself) = 1"
    4.38 -
    4.39 -instance ..
    4.40 -
    4.41 -end
    4.42 -
    4.43 -instantiation bit0 and bit1 :: (len0) len0
    4.44 -begin
    4.45 -
    4.46 -definition
    4.47 -  len_bit0: "len_of (x::'a::len0 bit0 itself) = 2 * len_of TYPE ('a)"
    4.48 -
    4.49 -definition
    4.50 -  len_bit1: "len_of (x::'a::len0 bit1 itself) = 2 * len_of TYPE ('a) + 1"
    4.51 -
    4.52 -instance ..
    4.53 -
    4.54 -end
    4.55 -
    4.56 -lemmas len_of_numeral_defs [simp] = len_num0 len_num1 len_bit0 len_bit1
    4.57 -
    4.58 -instance num1 :: len proof qed simp
    4.59 -instance bit0 :: (len) len proof qed simp
    4.60 -instance bit1 :: (len0) len proof qed simp
    4.61 -
    4.62 -end
    4.63 -
     5.1 --- a/src/HOL/Word/Word.thy	Thu Sep 01 20:34:43 2016 +0200
     5.2 +++ b/src/HOL/Word/Word.thy	Thu Sep 01 20:59:51 2016 +0200
     5.3 @@ -6,7 +6,7 @@
     5.4  
     5.5  theory Word
     5.6  imports
     5.7 -  Type_Length
     5.8 +  "~~/src/HOL/Library/Type_Length"
     5.9    "~~/src/HOL/Library/Boolean_Algebra"
    5.10    Bits_Bit
    5.11    Bool_List_Representation