# HG changeset patch
# User wenzelm
# Date 1472756391 -7200
# Node ID 6920b1885eff24a1d551b4589afa8b8bee6c7562
# Parent  2ca536d0163eb042ddb016e83050523f3538097c
clarified session;
misc tuning and modernization;

diff -r 2ca536d0163e -r 6920b1885eff src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy	Thu Sep 01 20:34:43 2016 +0200
+++ b/src/HOL/Library/Library.thy	Thu Sep 01 20:59:51 2016 +0200
@@ -83,6 +83,7 @@
   Sum_of_Squares
   Transitive_Closure_Table
   Tree_Multiset
+  Type_Length
   While_Combinator
 begin
 end
diff -r 2ca536d0163e -r 6920b1885eff src/HOL/Library/Saturated.thy
--- a/src/HOL/Library/Saturated.thy	Thu Sep 01 20:34:43 2016 +0200
+++ b/src/HOL/Library/Saturated.thy	Thu Sep 01 20:59:51 2016 +0200
@@ -7,7 +7,7 @@
 section \<open>Saturated arithmetic\<close>
 
 theory Saturated
-imports Numeral_Type "~~/src/HOL/Word/Type_Length"
+imports Numeral_Type Type_Length
 begin
 
 subsection \<open>The type of saturated naturals\<close>
diff -r 2ca536d0163e -r 6920b1885eff src/HOL/Library/Type_Length.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Type_Length.thy	Thu Sep 01 20:59:51 2016 +0200
@@ -0,0 +1,54 @@
+(*  Title:      HOL/Library/Type_Length.thy
+    Author:     John Matthews, Galois Connections, Inc., Copyright 2006
+*)
+
+section \<open>Assigning lengths to types by type classes\<close>
+
+theory Type_Length
+imports Numeral_Type
+begin
+
+text \<open>
+  The aim of this is to allow any type as index type, but to provide a
+  default instantiation for numeral types. This independence requires
+  some duplication with the definitions in \<^file>\<open>Numeral_Type.thy\<close>.
+\<close>
+
+class len0 =
+  fixes len_of :: "'a itself \<Rightarrow> nat"
+
+text \<open>Some theorems are only true on words with length greater 0.\<close>
+
+class len = len0 +
+  assumes len_gt_0 [iff]: "0 < len_of TYPE ('a)"
+
+instantiation num0 and num1 :: len0
+begin
+
+definition len_num0: "len_of (_ :: num0 itself) = 0"
+definition len_num1: "len_of (_ :: num1 itself) = 1"
+
+instance ..
+
+end
+
+instantiation bit0 and bit1 :: (len0) len0
+begin
+
+definition len_bit0: "len_of (_ :: 'a::len0 bit0 itself) = 2 * len_of TYPE('a)"
+definition len_bit1: "len_of (_ :: 'a::len0 bit1 itself) = 2 * len_of TYPE('a) + 1"
+
+instance ..
+
+end
+
+lemmas len_of_numeral_defs [simp] = len_num0 len_num1 len_bit0 len_bit1
+
+instance num1 :: len
+  by standard simp
+instance bit0 :: (len) len
+  by standard simp
+instance bit1 :: (len0) len
+  by standard simp
+
+end
diff -r 2ca536d0163e -r 6920b1885eff src/HOL/Word/Type_Length.thy
--- a/src/HOL/Word/Type_Length.thy	Thu Sep 01 20:34:43 2016 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,60 +0,0 @@
-(*  Title:      HOL/Word/Type_Length.thy
-    Author:     John Matthews, Galois Connections, Inc., copyright 2006
-*)
-
-section \<open>Assigning lengths to types by typeclasses\<close>
-
-theory Type_Length
-imports "~~/src/HOL/Library/Numeral_Type"
-begin
-
-text \<open>
-  The aim of this is to allow any type as index type, but to provide a
-  default instantiation for numeral types. This independence requires
-  some duplication with the definitions in \<open>Numeral_Type\<close>.
-\<close>
-
-class len0 =
-  fixes len_of :: "'a itself \<Rightarrow> nat"
-
-text \<open>
-  Some theorems are only true on words with length greater 0.
-\<close>
-
-class len = len0 +
-  assumes len_gt_0 [iff]: "0 < len_of TYPE ('a)"
-
-instantiation num0 and num1 :: len0
-begin
-
-definition
-  len_num0:  "len_of (x::num0 itself) = 0"
-
-definition
-  len_num1: "len_of (x::num1 itself) = 1"
-
-instance ..
-
-end
-
-instantiation bit0 and bit1 :: (len0) len0
-begin
-
-definition
-  len_bit0: "len_of (x::'a::len0 bit0 itself) = 2 * len_of TYPE ('a)"
-
-definition
-  len_bit1: "len_of (x::'a::len0 bit1 itself) = 2 * len_of TYPE ('a) + 1"
-
-instance ..
-
-end
-
-lemmas len_of_numeral_defs [simp] = len_num0 len_num1 len_bit0 len_bit1
-
-instance num1 :: len proof qed simp
-instance bit0 :: (len) len proof qed simp
-instance bit1 :: (len0) len proof qed simp
-
-end
-
diff -r 2ca536d0163e -r 6920b1885eff src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Thu Sep 01 20:34:43 2016 +0200
+++ b/src/HOL/Word/Word.thy	Thu Sep 01 20:59:51 2016 +0200
@@ -6,7 +6,7 @@
 
 theory Word
 imports
-  Type_Length
+  "~~/src/HOL/Library/Type_Length"
   "~~/src/HOL/Library/Boolean_Algebra"
   Bits_Bit
   Bool_List_Representation