author  wenzelm 
Wed, 08 Mar 2017 10:50:59 +0100  
changeset 65151  a7394aa4d21c 
parent 63762  6920b1885eff 
child 70185  ac1706cdde25 
permissions  rwrr 
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 

60500  7 
section \<open>Saturated arithmetic\<close> 
44819
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 
63762  10 
imports Numeral_Type Type_Length 
44819
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 

60500  13 
subsection \<open>The type of saturated naturals\<close> 
44819
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

14 

61260  15 
typedef (overloaded) ('a::len) sat = "{.. len_of TYPE('a)}" 
44819
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" 
54863
82acc20ded73
prefer more canonical names for lemmas on min/max
haftmann
parents:
52729
diff
changeset

44 
by (rule min.absorb2 [OF nat_of_le_len_of]) 
44819
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" 
51540
eea5c4ca4a0e
explicit sublocale dependency for Min/Max yields more appropriate Min/Max prefix for a couple of facts
haftmann
parents:
51489
diff
changeset

48 
by (subst min.commute) simp 
44819
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 
60679  64 
by standard 
65 
(auto simp add: less_eq_sat_def less_sat_def not_le sat_eq_iff min.coboundedI1 mult.commute) 

44819
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

66 

fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

67 
end 
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

68 

44849
41fddafe20d5
Library/Saturated.thy: number_semiring class instance
huffman
parents:
44848
diff
changeset

69 
instantiation sat :: (len) "{minus, comm_semiring_1}" 
44819
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

70 
begin 
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

71 

fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

72 
definition 
44883
a7f9c97378b3
Library/Saturated.thy: 'Sat' abbreviates 'of_nat'
huffman
parents:
44849
diff
changeset

73 
"0 = Abs_sat' 0" 
44819
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

74 

fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

75 
definition 
44883
a7f9c97378b3
Library/Saturated.thy: 'Sat' abbreviates 'of_nat'
huffman
parents:
44849
diff
changeset

76 
"1 = Abs_sat' 1" 
44819
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

77 

fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

78 
lemma nat_of_zero_sat [simp, code abstract]: 
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

79 
"nat_of 0 = 0" 
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

80 
by (simp add: zero_sat_def) 
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

81 

fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

82 
lemma nat_of_one_sat [simp, code abstract]: 
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

83 
"nat_of 1 = min 1 (len_of TYPE('a))" 
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

84 
by (simp add: one_sat_def) 
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

85 

fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

86 
definition 
44883
a7f9c97378b3
Library/Saturated.thy: 'Sat' abbreviates 'of_nat'
huffman
parents:
44849
diff
changeset

87 
"x + y = Abs_sat' (nat_of x + nat_of y)" 
44819
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

88 

fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

89 
lemma nat_of_plus_sat [simp, code abstract]: 
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

90 
"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

91 
by (simp add: plus_sat_def) 
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

92 

fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

93 
definition 
44883
a7f9c97378b3
Library/Saturated.thy: 'Sat' abbreviates 'of_nat'
huffman
parents:
44849
diff
changeset

94 
"x  y = Abs_sat' (nat_of x  nat_of y)" 
44819
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

95 

fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

96 
lemma nat_of_minus_sat [simp, code abstract]: 
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

97 
"nat_of (x  y) = nat_of x  nat_of y" 
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

98 
proof  
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

99 
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

100 
then show ?thesis by (simp add: minus_sat_def) 
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

101 
qed 
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

102 

fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

103 
definition 
44883
a7f9c97378b3
Library/Saturated.thy: 'Sat' abbreviates 'of_nat'
huffman
parents:
44849
diff
changeset

104 
"x * y = Abs_sat' (nat_of x * nat_of y)" 
44819
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

105 

fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

106 
lemma nat_of_times_sat [simp, code abstract]: 
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

107 
"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

108 
by (simp add: times_sat_def) 
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

109 

60679  110 
instance 
111 
proof 

112 
fix a b c :: "'a::len sat" 

44819
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

113 
show "a * b * c = a * (b * c)" 
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

114 
proof(cases "a = 0") 
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

115 
case True thus ?thesis by (simp add: sat_eq_iff) 
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

116 
next 
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

117 
case False show ?thesis 
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

118 
proof(cases "c = 0") 
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

119 
case True thus ?thesis by (simp add: sat_eq_iff) 
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

120 
next 
60500  121 
case False with \<open>a \<noteq> 0\<close> show ?thesis 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
54863
diff
changeset

122 
by (simp add: sat_eq_iff nat_mult_min_left nat_mult_min_right mult.assoc min.assoc min.absorb2) 
44819
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

123 
qed 
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

124 
qed 
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) 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
54863
diff
changeset

127 
apply (metis One_nat_def len_gt_0 less_Suc0 less_zeroE linorder_not_less min.absorb_iff1 min_nat_of_len_of nat_mult_1_right mult.commute) 
44819
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 
show "(a + b) * c = a * c + b * c" 
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

130 
proof(cases "c = 0") 
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

131 
case True thus ?thesis by (simp add: sat_eq_iff) 
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

132 
next 
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

133 
case False thus ?thesis 
54863
82acc20ded73
prefer more canonical names for lemmas on min/max
haftmann
parents:
52729
diff
changeset

134 
by (simp add: sat_eq_iff nat_mult_min_left add_mult_distrib min_add_distrib_left min_add_distrib_right min.assoc min.absorb2) 
44819
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

135 
qed 
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

136 
qed (simp_all add: sat_eq_iff mult.commute) 
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

137 

fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

138 
end 
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 
instantiation sat :: (len) ordered_comm_semiring 
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

141 
begin 
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

142 

fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

143 
instance 
60679  144 
by standard 
145 
(auto simp add: less_eq_sat_def less_sat_def not_le sat_eq_iff min.coboundedI1 mult.commute) 

44819
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

146 

fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

147 
end 
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

148 

44883
a7f9c97378b3
Library/Saturated.thy: 'Sat' abbreviates 'of_nat'
huffman
parents:
44849
diff
changeset

149 
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

150 
by (rule sat_eqI, induct n, simp_all) 
41fddafe20d5
Library/Saturated.thy: number_semiring class instance
huffman
parents:
44848
diff
changeset

151 

44883
a7f9c97378b3
Library/Saturated.thy: 'Sat' abbreviates 'of_nat'
huffman
parents:
44849
diff
changeset

152 
abbreviation Sat :: "nat \<Rightarrow> 'a::len sat" where 
a7f9c97378b3
Library/Saturated.thy: 'Sat' abbreviates 'of_nat'
huffman
parents:
44849
diff
changeset

153 
"Sat \<equiv> of_nat" 
a7f9c97378b3
Library/Saturated.thy: 'Sat' abbreviates 'of_nat'
huffman
parents:
44849
diff
changeset

154 

a7f9c97378b3
Library/Saturated.thy: 'Sat' abbreviates 'of_nat'
huffman
parents:
44849
diff
changeset

155 
lemma nat_of_Sat [simp]: 
a7f9c97378b3
Library/Saturated.thy: 'Sat' abbreviates 'of_nat'
huffman
parents:
44849
diff
changeset

156 
"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

157 
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

158 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45994
diff
changeset

159 
lemma [code_abbrev]: 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45994
diff
changeset

160 
"of_nat (numeral k) = (numeral k :: 'a::len sat)" 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45994
diff
changeset

161 
by simp 
44819
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

162 

60011  163 
context 
164 
begin 

165 

166 
qualified definition sat_of_nat :: "nat \<Rightarrow> ('a::len) sat" 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45994
diff
changeset

167 
where [code_abbrev]: "sat_of_nat = of_nat" 
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 
lemma [code abstract]: 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45994
diff
changeset

170 
"nat_of (sat_of_nat n :: ('a::len) sat) = min (len_of TYPE('a)) n" 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45994
diff
changeset

171 
by (simp add: sat_of_nat_def) 
44819
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

172 

60011  173 
end 
174 

44819
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 

60679  185 
definition "HOL.equal A B \<longleftrightarrow> nat_of A = nat_of B" 
44819
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

186 

60679  187 
instance 
188 
by standard (simp add: equal_sat_def nat_of_inject) 

44819
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

189 

fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

190 
end 
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

191 

fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

192 
instantiation sat :: (len) "{bounded_lattice, distrib_lattice}" 
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

193 
begin 
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

194 

60679  195 
definition "(inf :: 'a sat \<Rightarrow> 'a sat \<Rightarrow> 'a sat) = min" 
196 
definition "(sup :: 'a sat \<Rightarrow> 'a sat \<Rightarrow> 'a sat) = max" 

197 
definition "bot = (0 :: 'a sat)" 

198 
definition "top = Sat (len_of TYPE('a))" 

44819
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

199 

60679  200 
instance 
201 
by standard 

202 
(simp_all add: inf_sat_def sup_sat_def bot_sat_def top_sat_def max_min_distrib2, 

203 
simp_all add: less_eq_sat_def) 

44819
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 
end 
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

206 

51489  207 
instantiation sat :: (len) "{Inf, Sup}" 
44819
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

208 
begin 
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

209 

60679  210 
definition "Inf = (semilattice_neutr_set.F min top :: 'a sat set \<Rightarrow> 'a sat)" 
211 
definition "Sup = (semilattice_neutr_set.F max bot :: 'a sat set \<Rightarrow> 'a sat)" 

51489  212 

213 
instance .. 

214 

215 
end 

44819
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

216 

61605  217 
interpretation Inf_sat: semilattice_neutr_set min "top :: 'a::len sat" 
63433  218 
rewrites "semilattice_neutr_set.F min (top :: 'a sat) = Inf" 
51489  219 
proof  
60679  220 
show "semilattice_neutr_set min (top :: 'a sat)" 
221 
by standard (simp add: min_def) 

222 
show "semilattice_neutr_set.F min (top :: 'a sat) = Inf" 

223 
by (simp add: Inf_sat_def) 

51489  224 
qed 
225 

61605  226 
interpretation Sup_sat: semilattice_neutr_set max "bot :: 'a::len sat" 
63433  227 
rewrites "semilattice_neutr_set.F max (bot :: 'a sat) = Sup" 
51489  228 
proof  
60679  229 
show "semilattice_neutr_set max (bot :: 'a sat)" 
230 
by standard (simp add: max_def bot.extremum_unique) 

231 
show "semilattice_neutr_set.F max (bot :: 'a sat) = Sup" 

232 
by (simp add: Sup_sat_def) 

51489  233 
qed 
234 

235 
instance sat :: (len) complete_lattice 

236 
proof 

44819
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

237 
fix x :: "'a sat" 
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

238 
fix A :: "'a sat set" 
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

239 
note finite 
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

240 
moreover assume "x \<in> A" 
51489  241 
ultimately show "Inf A \<le> x" 
54863
82acc20ded73
prefer more canonical names for lemmas on min/max
haftmann
parents:
52729
diff
changeset

242 
by (induct A) (auto intro: min.coboundedI2) 
44819
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

243 
next 
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

244 
fix z :: "'a sat" 
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

245 
fix A :: "'a sat set" 
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

246 
note finite 
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

247 
moreover assume z: "\<And>x. x \<in> A \<Longrightarrow> z \<le> x" 
51489  248 
ultimately show "z \<le> Inf A" by (induct A) simp_all 
44819
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

249 
next 
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

250 
fix x :: "'a sat" 
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

251 
fix A :: "'a sat set" 
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

252 
note finite 
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

253 
moreover assume "x \<in> A" 
51489  254 
ultimately show "x \<le> Sup A" 
54863
82acc20ded73
prefer more canonical names for lemmas on min/max
haftmann
parents:
52729
diff
changeset

255 
by (induct A) (auto intro: max.coboundedI2) 
44819
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

256 
next 
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

257 
fix z :: "'a sat" 
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

258 
fix A :: "'a sat set" 
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

259 
note finite 
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

260 
moreover assume z: "\<And>x. x \<in> A \<Longrightarrow> x \<le> z" 
51489  261 
ultimately show "Sup A \<le> z" by (induct A) auto 
52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51545
diff
changeset

262 
next 
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51545
diff
changeset

263 
show "Inf {} = (top::'a sat)" 
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51545
diff
changeset

264 
by (auto simp: top_sat_def) 
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51545
diff
changeset

265 
show "Sup {} = (bot::'a sat)" 
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51545
diff
changeset

266 
by (auto simp: bot_sat_def) 
44819
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

267 
qed 
fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

268 

fe33d6655186
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
diff
changeset

269 
end 