author | haftmann |
Sat, 24 Dec 2011 15:53:10 +0100 | |
changeset 45970 | b6d0cff57d96 |
parent 45692 | d2567e55af83 |
child 45994 | 38a46e029784 |
permissions | -rw-r--r-- |
45692 | 1 |
(* Title: HOL/Library/Saturated.thy |
2 |
Author: Brian Huffman |
|
3 |
Author: Peter Gammie |
|
4 |
Author: Florian Haftmann |
|
5 |
*) |
|
44819
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
6 |
|
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
7 |
header {* Saturated arithmetic *} |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
8 |
|
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
9 |
theory Saturated |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
10 |
imports Main "~~/src/HOL/Library/Numeral_Type" "~~/src/HOL/Word/Type_Length" |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
11 |
begin |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
12 |
|
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
13 |
subsection {* The type of saturated naturals *} |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
14 |
|
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
15 |
typedef (open) ('a::len) sat = "{.. len_of TYPE('a)}" |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
16 |
morphisms nat_of Abs_sat |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
17 |
by auto |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
18 |
|
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
19 |
lemma sat_eqI: |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
20 |
"nat_of m = nat_of n \<Longrightarrow> m = n" |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
21 |
by (simp add: nat_of_inject) |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
22 |
|
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
23 |
lemma sat_eq_iff: |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
24 |
"m = n \<longleftrightarrow> nat_of m = nat_of n" |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
25 |
by (simp add: nat_of_inject) |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
26 |
|
44883
a7f9c97378b3
Library/Saturated.thy: 'Sat' abbreviates 'of_nat'
huffman
parents:
44849
diff
changeset
|
27 |
lemma Abs_sat_nat_of [code abstype]: |
44819
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
28 |
"Abs_sat (nat_of n) = n" |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
29 |
by (fact nat_of_inverse) |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
30 |
|
44883
a7f9c97378b3
Library/Saturated.thy: 'Sat' abbreviates 'of_nat'
huffman
parents:
44849
diff
changeset
|
31 |
definition Abs_sat' :: "nat \<Rightarrow> 'a::len sat" where |
a7f9c97378b3
Library/Saturated.thy: 'Sat' abbreviates 'of_nat'
huffman
parents:
44849
diff
changeset
|
32 |
"Abs_sat' n = Abs_sat (min (len_of TYPE('a)) n)" |
44819
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
33 |
|
44883
a7f9c97378b3
Library/Saturated.thy: 'Sat' abbreviates 'of_nat'
huffman
parents:
44849
diff
changeset
|
34 |
lemma nat_of_Abs_sat' [simp]: |
a7f9c97378b3
Library/Saturated.thy: 'Sat' abbreviates 'of_nat'
huffman
parents:
44849
diff
changeset
|
35 |
"nat_of (Abs_sat' n :: ('a::len) sat) = min (len_of TYPE('a)) n" |
a7f9c97378b3
Library/Saturated.thy: 'Sat' abbreviates 'of_nat'
huffman
parents:
44849
diff
changeset
|
36 |
unfolding Abs_sat'_def by (rule Abs_sat_inverse) simp |
44819
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
37 |
|
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
38 |
lemma nat_of_le_len_of [simp]: |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
39 |
"nat_of (n :: ('a::len) sat) \<le> len_of TYPE('a)" |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
40 |
using nat_of [where x = n] by simp |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
41 |
|
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
42 |
lemma min_len_of_nat_of [simp]: |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
43 |
"min (len_of TYPE('a)) (nat_of (n::('a::len) sat)) = nat_of n" |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
44 |
by (rule min_max.inf_absorb2 [OF nat_of_le_len_of]) |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
45 |
|
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
46 |
lemma min_nat_of_len_of [simp]: |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
47 |
"min (nat_of (n::('a::len) sat)) (len_of TYPE('a)) = nat_of n" |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
48 |
by (subst min_max.inf.commute) simp |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
49 |
|
44883
a7f9c97378b3
Library/Saturated.thy: 'Sat' abbreviates 'of_nat'
huffman
parents:
44849
diff
changeset
|
50 |
lemma Abs_sat'_nat_of [simp]: |
a7f9c97378b3
Library/Saturated.thy: 'Sat' abbreviates 'of_nat'
huffman
parents:
44849
diff
changeset
|
51 |
"Abs_sat' (nat_of n) = n" |
a7f9c97378b3
Library/Saturated.thy: 'Sat' abbreviates 'of_nat'
huffman
parents:
44849
diff
changeset
|
52 |
by (simp add: Abs_sat'_def nat_of_inverse) |
44819
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
53 |
|
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
54 |
instantiation sat :: (len) linorder |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
55 |
begin |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
56 |
|
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
57 |
definition |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
58 |
less_eq_sat_def: "x \<le> y \<longleftrightarrow> nat_of x \<le> nat_of y" |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
59 |
|
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
60 |
definition |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
61 |
less_sat_def: "x < y \<longleftrightarrow> nat_of x < nat_of y" |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
62 |
|
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
63 |
instance |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
64 |
by default (auto simp add: less_eq_sat_def less_sat_def not_le sat_eq_iff min_max.le_infI1 nat_mult_commute) |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
65 |
|
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
66 |
end |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
67 |
|
44849
41fddafe20d5
Library/Saturated.thy: number_semiring class instance
huffman
parents:
44848
diff
changeset
|
68 |
instantiation sat :: (len) "{minus, comm_semiring_1}" |
44819
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
69 |
begin |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
70 |
|
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
71 |
definition |
44883
a7f9c97378b3
Library/Saturated.thy: 'Sat' abbreviates 'of_nat'
huffman
parents:
44849
diff
changeset
|
72 |
"0 = Abs_sat' 0" |
44819
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
73 |
|
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
74 |
definition |
44883
a7f9c97378b3
Library/Saturated.thy: 'Sat' abbreviates 'of_nat'
huffman
parents:
44849
diff
changeset
|
75 |
"1 = Abs_sat' 1" |
44819
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
76 |
|
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
77 |
lemma nat_of_zero_sat [simp, code abstract]: |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
78 |
"nat_of 0 = 0" |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
79 |
by (simp add: zero_sat_def) |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
80 |
|
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
81 |
lemma nat_of_one_sat [simp, code abstract]: |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
82 |
"nat_of 1 = min 1 (len_of TYPE('a))" |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
83 |
by (simp add: one_sat_def) |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
84 |
|
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
85 |
definition |
44883
a7f9c97378b3
Library/Saturated.thy: 'Sat' abbreviates 'of_nat'
huffman
parents:
44849
diff
changeset
|
86 |
"x + y = Abs_sat' (nat_of x + nat_of y)" |
44819
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
87 |
|
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
88 |
lemma nat_of_plus_sat [simp, code abstract]: |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
89 |
"nat_of (x + y) = min (nat_of x + nat_of y) (len_of TYPE('a))" |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
90 |
by (simp add: plus_sat_def) |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
91 |
|
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
92 |
definition |
44883
a7f9c97378b3
Library/Saturated.thy: 'Sat' abbreviates 'of_nat'
huffman
parents:
44849
diff
changeset
|
93 |
"x - y = Abs_sat' (nat_of x - nat_of y)" |
44819
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
94 |
|
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
95 |
lemma nat_of_minus_sat [simp, code abstract]: |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
96 |
"nat_of (x - y) = nat_of x - nat_of y" |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
97 |
proof - |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
98 |
from nat_of_le_len_of [of x] have "nat_of x - nat_of y \<le> len_of TYPE('a)" by arith |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
99 |
then show ?thesis by (simp add: minus_sat_def) |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
100 |
qed |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
101 |
|
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
102 |
definition |
44883
a7f9c97378b3
Library/Saturated.thy: 'Sat' abbreviates 'of_nat'
huffman
parents:
44849
diff
changeset
|
103 |
"x * y = Abs_sat' (nat_of x * nat_of y)" |
44819
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
104 |
|
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
105 |
lemma nat_of_times_sat [simp, code abstract]: |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
106 |
"nat_of (x * y) = min (nat_of x * nat_of y) (len_of TYPE('a))" |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
107 |
by (simp add: times_sat_def) |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
108 |
|
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
109 |
instance proof |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
110 |
fix a b c :: "('a::len) sat" |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
111 |
show "a * b * c = a * (b * c)" |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
112 |
proof(cases "a = 0") |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
113 |
case True thus ?thesis by (simp add: sat_eq_iff) |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
114 |
next |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
115 |
case False show ?thesis |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
116 |
proof(cases "c = 0") |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
117 |
case True thus ?thesis by (simp add: sat_eq_iff) |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
118 |
next |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
119 |
case False with `a \<noteq> 0` show ?thesis |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
120 |
by (simp add: sat_eq_iff nat_mult_min_left nat_mult_min_right mult_assoc min_max.inf_assoc min_max.inf_absorb2) |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
121 |
qed |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
122 |
qed |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
123 |
next |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
124 |
fix a :: "('a::len) sat" |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
125 |
show "1 * a = a" |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
126 |
apply (simp add: sat_eq_iff) |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
127 |
apply (metis One_nat_def len_gt_0 less_Suc0 less_zeroE linorder_not_less min_max.le_iff_inf min_nat_of_len_of nat_mult_1_right nat_mult_commute) |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
128 |
done |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
129 |
next |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
130 |
fix a b c :: "('a::len) sat" |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
131 |
show "(a + b) * c = a * c + b * c" |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
132 |
proof(cases "c = 0") |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
133 |
case True thus ?thesis by (simp add: sat_eq_iff) |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
134 |
next |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
135 |
case False thus ?thesis |
44848
f4d0b060c7ca
remove lemmas nat_add_min_{left,right} in favor of generic lemmas min_add_distrib_{left,right}
huffman
parents:
44819
diff
changeset
|
136 |
by (simp add: sat_eq_iff nat_mult_min_left add_mult_distrib min_add_distrib_left min_add_distrib_right min_max.inf_assoc min_max.inf_absorb2) |
44819
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
137 |
qed |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
138 |
qed (simp_all add: sat_eq_iff mult.commute) |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
139 |
|
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
140 |
end |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
141 |
|
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
142 |
instantiation sat :: (len) ordered_comm_semiring |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
143 |
begin |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
144 |
|
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
145 |
instance |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
146 |
by default (auto simp add: less_eq_sat_def less_sat_def not_le sat_eq_iff min_max.le_infI1 nat_mult_commute) |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
147 |
|
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
148 |
end |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
149 |
|
44883
a7f9c97378b3
Library/Saturated.thy: 'Sat' abbreviates 'of_nat'
huffman
parents:
44849
diff
changeset
|
150 |
lemma Abs_sat'_eq_of_nat: "Abs_sat' n = of_nat n" |
44849
41fddafe20d5
Library/Saturated.thy: number_semiring class instance
huffman
parents:
44848
diff
changeset
|
151 |
by (rule sat_eqI, induct n, simp_all) |
41fddafe20d5
Library/Saturated.thy: number_semiring class instance
huffman
parents:
44848
diff
changeset
|
152 |
|
44883
a7f9c97378b3
Library/Saturated.thy: 'Sat' abbreviates 'of_nat'
huffman
parents:
44849
diff
changeset
|
153 |
abbreviation Sat :: "nat \<Rightarrow> 'a::len sat" where |
a7f9c97378b3
Library/Saturated.thy: 'Sat' abbreviates 'of_nat'
huffman
parents:
44849
diff
changeset
|
154 |
"Sat \<equiv> of_nat" |
a7f9c97378b3
Library/Saturated.thy: 'Sat' abbreviates 'of_nat'
huffman
parents:
44849
diff
changeset
|
155 |
|
a7f9c97378b3
Library/Saturated.thy: 'Sat' abbreviates 'of_nat'
huffman
parents:
44849
diff
changeset
|
156 |
lemma nat_of_Sat [simp]: |
a7f9c97378b3
Library/Saturated.thy: 'Sat' abbreviates 'of_nat'
huffman
parents:
44849
diff
changeset
|
157 |
"nat_of (Sat n :: ('a::len) sat) = min (len_of TYPE('a)) n" |
a7f9c97378b3
Library/Saturated.thy: 'Sat' abbreviates 'of_nat'
huffman
parents:
44849
diff
changeset
|
158 |
by (rule nat_of_Abs_sat' [unfolded Abs_sat'_eq_of_nat]) |
a7f9c97378b3
Library/Saturated.thy: 'Sat' abbreviates 'of_nat'
huffman
parents:
44849
diff
changeset
|
159 |
|
44849
41fddafe20d5
Library/Saturated.thy: number_semiring class instance
huffman
parents:
44848
diff
changeset
|
160 |
instantiation sat :: (len) number_semiring |
44819
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
161 |
begin |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
162 |
|
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
163 |
definition |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
164 |
number_of_sat_def [code del]: "number_of = Sat \<circ> nat" |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
165 |
|
44849
41fddafe20d5
Library/Saturated.thy: number_semiring class instance
huffman
parents:
44848
diff
changeset
|
166 |
instance |
44883
a7f9c97378b3
Library/Saturated.thy: 'Sat' abbreviates 'of_nat'
huffman
parents:
44849
diff
changeset
|
167 |
by default (simp add: number_of_sat_def) |
44819
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
168 |
|
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
169 |
end |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
170 |
|
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
171 |
lemma [code abstract]: |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
172 |
"nat_of (number_of n :: ('a::len) sat) = min (nat n) (len_of TYPE('a))" |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
173 |
unfolding number_of_sat_def by simp |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
174 |
|
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
175 |
instance sat :: (len) finite |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
176 |
proof |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
177 |
show "finite (UNIV::'a sat set)" |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
178 |
unfolding type_definition.univ [OF type_definition_sat] |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
179 |
using finite by simp |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
180 |
qed |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
181 |
|
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
182 |
instantiation sat :: (len) equal |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
183 |
begin |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
184 |
|
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
185 |
definition |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
186 |
"HOL.equal A B \<longleftrightarrow> nat_of A = nat_of B" |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
187 |
|
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
188 |
instance proof |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
189 |
qed (simp add: equal_sat_def nat_of_inject) |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
190 |
|
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
191 |
end |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
192 |
|
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
193 |
instantiation sat :: (len) "{bounded_lattice, distrib_lattice}" |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
194 |
begin |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
195 |
|
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
196 |
definition |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
197 |
"(inf :: 'a sat \<Rightarrow> 'a sat \<Rightarrow> 'a sat) = min" |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
198 |
|
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
199 |
definition |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
200 |
"(sup :: 'a sat \<Rightarrow> 'a sat \<Rightarrow> 'a sat) = max" |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
201 |
|
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
202 |
definition |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
203 |
"bot = (0 :: 'a sat)" |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
204 |
|
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
205 |
definition |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
206 |
"top = Sat (len_of TYPE('a))" |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
207 |
|
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
208 |
instance proof |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
209 |
qed (simp_all add: inf_sat_def sup_sat_def bot_sat_def top_sat_def min_max.sup_inf_distrib1, |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
210 |
simp_all add: less_eq_sat_def) |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
211 |
|
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
212 |
end |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
213 |
|
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
214 |
instantiation sat :: (len) complete_lattice |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
215 |
begin |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
216 |
|
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
217 |
definition |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
218 |
"Inf (A :: 'a sat set) = fold min top A" |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
219 |
|
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
220 |
definition |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
221 |
"Sup (A :: 'a sat set) = fold max bot A" |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
222 |
|
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
223 |
instance proof |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
224 |
fix x :: "'a sat" |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
225 |
fix A :: "'a sat set" |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
226 |
note finite |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
227 |
moreover assume "x \<in> A" |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
228 |
ultimately have "fold min top A \<le> min x top" by (rule min_max.fold_inf_le_inf) |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
229 |
then show "Inf A \<le> x" by (simp add: Inf_sat_def) |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
230 |
next |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
231 |
fix z :: "'a sat" |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
232 |
fix A :: "'a sat set" |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
233 |
note finite |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
234 |
moreover assume z: "\<And>x. x \<in> A \<Longrightarrow> z \<le> x" |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
235 |
ultimately have "min z top \<le> fold min top A" by (blast intro: min_max.inf_le_fold_inf) |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
236 |
then show "z \<le> Inf A" by (simp add: Inf_sat_def min_def) |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
237 |
next |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
238 |
fix x :: "'a sat" |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
239 |
fix A :: "'a sat set" |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
240 |
note finite |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
241 |
moreover assume "x \<in> A" |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
242 |
ultimately have "max x bot \<le> fold max bot A" by (rule min_max.sup_le_fold_sup) |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
243 |
then show "x \<le> Sup A" by (simp add: Sup_sat_def) |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
244 |
next |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
245 |
fix z :: "'a sat" |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
246 |
fix A :: "'a sat set" |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
247 |
note finite |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
248 |
moreover assume z: "\<And>x. x \<in> A \<Longrightarrow> x \<le> z" |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
249 |
ultimately have "fold max bot A \<le> max z bot" by (blast intro: min_max.fold_sup_le_sup) |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
250 |
then show "Sup A \<le> z" by (simp add: Sup_sat_def max_def bot_unique) |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
251 |
qed |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
252 |
|
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
253 |
end |
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
254 |
|
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset
|
255 |
end |