author | haftmann |
Wed, 24 Feb 2021 13:31:33 +0000 | |
changeset 73301 | bfe92e4f6ea4 |
parent 72792 | 26492b600d78 |
permissions | -rw-r--r-- |
63762 | 1 |
(* Title: HOL/Library/Type_Length.thy |
2 |
Author: John Matthews, Galois Connections, Inc., Copyright 2006 |
|
24465 | 3 |
*) |
25262
d0928156e326
Added reference to Jeremy Dawson's paper on the word library.
kleing
parents:
24465
diff
changeset
|
4 |
|
63762 | 5 |
section \<open>Assigning lengths to types by type classes\<close> |
25262
d0928156e326
Added reference to Jeremy Dawson's paper on the word library.
kleing
parents:
24465
diff
changeset
|
6 |
|
37655 | 7 |
theory Type_Length |
63762 | 8 |
imports Numeral_Type |
24465 | 9 |
begin |
10 |
||
61799 | 11 |
text \<open> |
24465 | 12 |
The aim of this is to allow any type as index type, but to provide a |
13 |
default instantiation for numeral types. This independence requires |
|
63762 | 14 |
some duplication with the definitions in \<^file>\<open>Numeral_Type.thy\<close>. |
61799 | 15 |
\<close> |
24465 | 16 |
|
29608 | 17 |
class len0 = |
26514 | 18 |
fixes len_of :: "'a itself \<Rightarrow> nat" |
24465 | 19 |
|
69597 | 20 |
syntax "_type_length" :: "type \<Rightarrow> nat" (\<open>(1LENGTH/(1'(_')))\<close>) |
64113 | 21 |
|
22 |
translations "LENGTH('a)" \<rightharpoonup> |
|
23 |
"CONST len_of (CONST Pure.type :: 'a itself)" |
|
24 |
||
25 |
print_translation \<open> |
|
26 |
let |
|
69593 | 27 |
fun len_of_itself_tr' ctxt [Const (\<^const_syntax>\<open>Pure.type\<close>, Type (_, [T]))] = |
28 |
Syntax.const \<^syntax_const>\<open>_type_length\<close> $ Syntax_Phases.term_of_typ ctxt T |
|
29 |
in [(\<^const_syntax>\<open>len_of\<close>, len_of_itself_tr')] end |
|
64113 | 30 |
\<close> |
31 |
||
63762 | 32 |
text \<open>Some theorems are only true on words with length greater 0.\<close> |
26514 | 33 |
|
34 |
class len = len0 + |
|
64113 | 35 |
assumes len_gt_0 [iff]: "0 < LENGTH('a)" |
70348
bde161c740ca
more theorems for proof of concept for word type
haftmann
parents:
69597
diff
changeset
|
36 |
begin |
bde161c740ca
more theorems for proof of concept for word type
haftmann
parents:
69597
diff
changeset
|
37 |
|
bde161c740ca
more theorems for proof of concept for word type
haftmann
parents:
69597
diff
changeset
|
38 |
lemma len_not_eq_0 [simp]: |
bde161c740ca
more theorems for proof of concept for word type
haftmann
parents:
69597
diff
changeset
|
39 |
"LENGTH('a) \<noteq> 0" |
bde161c740ca
more theorems for proof of concept for word type
haftmann
parents:
69597
diff
changeset
|
40 |
by simp |
bde161c740ca
more theorems for proof of concept for word type
haftmann
parents:
69597
diff
changeset
|
41 |
|
bde161c740ca
more theorems for proof of concept for word type
haftmann
parents:
69597
diff
changeset
|
42 |
end |
26514 | 43 |
|
44 |
instantiation num0 and num1 :: len0 |
|
45 |
begin |
|
46 |
||
63762 | 47 |
definition len_num0: "len_of (_ :: num0 itself) = 0" |
48 |
definition len_num1: "len_of (_ :: num1 itself) = 1" |
|
26514 | 49 |
|
50 |
instance .. |
|
24465 | 51 |
|
26514 | 52 |
end |
53 |
||
54 |
instantiation bit0 and bit1 :: (len0) len0 |
|
55 |
begin |
|
24465 | 56 |
|
64113 | 57 |
definition len_bit0: "len_of (_ :: 'a::len0 bit0 itself) = 2 * LENGTH('a)" |
58 |
definition len_bit1: "len_of (_ :: 'a::len0 bit1 itself) = 2 * LENGTH('a) + 1" |
|
26514 | 59 |
|
60 |
instance .. |
|
61 |
||
62 |
end |
|
24465 | 63 |
|
64 |
lemmas len_of_numeral_defs [simp] = len_num0 len_num1 len_bit0 len_bit1 |
|
65 |
||
63762 | 66 |
instance num1 :: len |
67 |
by standard simp |
|
68 |
instance bit0 :: (len) len |
|
69 |
by standard simp |
|
70 |
instance bit1 :: (len0) len |
|
71 |
by standard simp |
|
24465 | 72 |
|
70901 | 73 |
instantiation Enum.finite_1 :: len |
74 |
begin |
|
75 |
||
76 |
definition |
|
77 |
"len_of_finite_1 (x :: Enum.finite_1 itself) \<equiv> (1 :: nat)" |
|
78 |
||
79 |
instance |
|
80 |
by standard (auto simp: len_of_finite_1_def) |
|
81 |
||
24465 | 82 |
end |
70901 | 83 |
|
84 |
instantiation Enum.finite_2 :: len |
|
85 |
begin |
|
86 |
||
87 |
definition |
|
88 |
"len_of_finite_2 (x :: Enum.finite_2 itself) \<equiv> (2 :: nat)" |
|
89 |
||
90 |
instance |
|
91 |
by standard (auto simp: len_of_finite_2_def) |
|
92 |
||
93 |
end |
|
94 |
||
95 |
instantiation Enum.finite_3 :: len |
|
96 |
begin |
|
97 |
||
98 |
definition |
|
99 |
"len_of_finite_3 (x :: Enum.finite_3 itself) \<equiv> (4 :: nat)" |
|
100 |
||
101 |
instance |
|
102 |
by standard (auto simp: len_of_finite_3_def) |
|
103 |
||
104 |
end |
|
105 |
||
71195 | 106 |
lemma length_not_greater_eq_2_iff [simp]: |
107 |
\<open>\<not> 2 \<le> LENGTH('a::len) \<longleftrightarrow> LENGTH('a) = 1\<close> |
|
108 |
by (auto simp add: not_le dest: less_2_cases) |
|
109 |
||
71759 | 110 |
context linordered_idom |
111 |
begin |
|
112 |
||
113 |
lemma two_less_eq_exp_length [simp]: |
|
114 |
\<open>2 \<le> 2 ^ LENGTH('b::len)\<close> |
|
115 |
using mult_left_mono [of 1 \<open>2 ^ (LENGTH('b::len) - 1)\<close> 2] |
|
72792 | 116 |
by (cases \<open>LENGTH('b::len)\<close>) simp_all |
71759 | 117 |
|
70901 | 118 |
end |
71759 | 119 |
|
72281
beeadb35e357
more thorough treatment of division, particularly signed division on int and word
haftmann
parents:
71759
diff
changeset
|
120 |
lemma less_eq_decr_length_iff [simp]: |
beeadb35e357
more thorough treatment of division, particularly signed division on int and word
haftmann
parents:
71759
diff
changeset
|
121 |
\<open>n \<le> LENGTH('a::len) - Suc 0 \<longleftrightarrow> n < LENGTH('a)\<close> |
beeadb35e357
more thorough treatment of division, particularly signed division on int and word
haftmann
parents:
71759
diff
changeset
|
122 |
by (cases \<open>LENGTH('a)\<close>) (simp_all add: less_Suc_eq le_less) |
beeadb35e357
more thorough treatment of division, particularly signed division on int and word
haftmann
parents:
71759
diff
changeset
|
123 |
|
beeadb35e357
more thorough treatment of division, particularly signed division on int and word
haftmann
parents:
71759
diff
changeset
|
124 |
lemma decr_length_less_iff [simp]: |
beeadb35e357
more thorough treatment of division, particularly signed division on int and word
haftmann
parents:
71759
diff
changeset
|
125 |
\<open>LENGTH('a::len) - Suc 0 < n \<longleftrightarrow> LENGTH('a) \<le> n\<close> |
beeadb35e357
more thorough treatment of division, particularly signed division on int and word
haftmann
parents:
71759
diff
changeset
|
126 |
by (cases \<open>LENGTH('a)\<close>) auto |
beeadb35e357
more thorough treatment of division, particularly signed division on int and word
haftmann
parents:
71759
diff
changeset
|
127 |
|
71759 | 128 |
end |