author  haftmann 
Mon, 14 Aug 2006 13:46:17 +0200  
changeset 20383  58f65fc90cf4 
parent 20187  af47971ea304 
child 20427  0b102b4182de 
permissions  rwrr 
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

1 
(* ID: $Id$ 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

2 
Author: Florian Haftmann, TU Muenchen 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

3 
*) 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

4 

b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

5 
header {* Test and Examples for Pure/Tools/class_package.ML *} 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

6 

b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

7 
theory Classpackage 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

8 
imports Main 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

9 
begin 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

10 

b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

11 
class semigroup = 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

12 
fixes mult :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<^loc>\<otimes>" 70) 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

13 
assumes assoc: "x \<^loc>\<otimes> y \<^loc>\<otimes> z = x \<^loc>\<otimes> (y \<^loc>\<otimes> z)" 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

14 

b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

15 
instance nat :: semigroup 
20178  16 
"m \<otimes> n \<equiv> m + n" 
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

17 
proof 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

18 
fix m n q :: nat 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

19 
from semigroup_nat_def show "m \<otimes> n \<otimes> q = m \<otimes> (n \<otimes> q)" by simp 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

20 
qed 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

21 

b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

22 
instance int :: semigroup 
20178  23 
"k \<otimes> l \<equiv> k + l" 
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

24 
proof 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

25 
fix k l j :: int 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

26 
from semigroup_int_def show "k \<otimes> l \<otimes> j = k \<otimes> (l \<otimes> j)" by simp 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

27 
qed 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

28 

b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

29 
instance (type) list :: semigroup 
20178  30 
"xs \<otimes> ys \<equiv> xs @ ys" 
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

31 
proof 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

32 
fix xs ys zs :: "'a list" 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

33 
show "xs \<otimes> ys \<otimes> zs = xs \<otimes> (ys \<otimes> zs)" 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

34 
proof  
20178  35 
from semigroup_list_def have "\<And>xs ys\<Colon>'a list. xs \<otimes> ys \<equiv> xs @ ys" . 
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

36 
thus ?thesis by simp 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

37 
qed 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

38 
qed 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

39 

b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

40 
class monoidl = semigroup + 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

41 
fixes one :: 'a ("\<^loc>\<one>") 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

42 
assumes neutl: "\<^loc>\<one> \<^loc>\<otimes> x = x" 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

43 

20178  44 
instance monoidl_num_def: nat :: monoidl and int :: monoidl 
45 
"\<one> \<equiv> 0" 

46 
"\<one> \<equiv> 0" 

19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

47 
proof 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

48 
fix n :: nat 
20178  49 
from monoidl_num_def show "\<one> \<otimes> n = n" by simp 
50 
next 

19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

51 
fix k :: int 
20178  52 
from monoidl_num_def show "\<one> \<otimes> k = k" by simp 
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

53 
qed 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

54 

b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

55 
instance (type) list :: monoidl 
20178  56 
"\<one> \<equiv> []" 
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

57 
proof 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

58 
fix xs :: "'a list" 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

59 
show "\<one> \<otimes> xs = xs" 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

60 
proof  
20178  61 
from mult_list_def have "\<And>xs ys\<Colon>'a list. xs \<otimes> ys \<equiv> xs @ ys" . 
62 
moreover from monoidl_list_def have "\<one> \<equiv> []\<Colon>'a list" by simp 

19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

63 
ultimately show ?thesis by simp 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

64 
qed 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

65 
qed 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

66 

b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

67 
class monoid = monoidl + 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

68 
assumes neutr: "x \<^loc>\<otimes> \<^loc>\<one> = x" 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

69 

20178  70 
instance monoid_list_def: (type) list :: monoid 
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

71 
proof 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

72 
fix xs :: "'a list" 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

73 
show "xs \<otimes> \<one> = xs" 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

74 
proof  
20178  75 
from mult_list_def have "\<And>xs ys\<Colon>'a list. xs \<otimes> ys \<equiv> xs @ ys" . 
76 
moreover from monoid_list_def have "\<one> \<equiv> []\<Colon>'a list" by simp 

19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

77 
ultimately show ?thesis by simp 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

78 
qed 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

79 
qed 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

80 

b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

81 
class monoid_comm = monoid + 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

82 
assumes comm: "x \<^loc>\<otimes> y = y \<^loc>\<otimes> x" 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

83 

20178  84 
instance monoid_comm_num_def: nat :: monoid_comm and int :: monoid_comm 
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

85 
proof 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

86 
fix n :: nat 
20178  87 
from monoid_comm_num_def show "n \<otimes> \<one> = n" by simp 
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

88 
next 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

89 
fix n m :: nat 
20178  90 
from monoid_comm_num_def show "n \<otimes> m = m \<otimes> n" by simp 
91 
next 

19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

92 
fix k :: int 
20178  93 
from monoid_comm_num_def show "k \<otimes> \<one> = k" by simp 
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

94 
next 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

95 
fix k l :: int 
20178  96 
from monoid_comm_num_def show "k \<otimes> l = l \<otimes> k" by simp 
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

97 
qed 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

98 

b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

99 
definition (in monoid) 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

100 
units :: "'a set" 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

101 
units_def: "units = { y. \<exists>x. x \<^loc>\<otimes> y = \<^loc>\<one> \<and> y \<^loc>\<otimes> x = \<^loc>\<one> }" 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

102 

b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

103 
lemma (in monoid) inv_obtain: 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

104 
assumes ass: "x \<in> units" 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

105 
obtains y where "y \<^loc>\<otimes> x = \<^loc>\<one>" and "x \<^loc>\<otimes> y = \<^loc>\<one>" 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

106 
proof  
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

107 
from ass units_def obtain y 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

108 
where "y \<^loc>\<otimes> x = \<^loc>\<one>" and "x \<^loc>\<otimes> y = \<^loc>\<one>" by auto 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

109 
thus ?thesis .. 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

110 
qed 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

111 

b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

112 
lemma (in monoid) inv_unique: 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

113 
assumes eq: "y \<^loc>\<otimes> x = \<^loc>\<one>" "x \<^loc>\<otimes> y' = \<^loc>\<one>" 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

114 
shows "y = y'" 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

115 
proof  
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

116 
from eq neutr have "y = y \<^loc>\<otimes> (x \<^loc>\<otimes> y')" by simp 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

117 
also with assoc have "... = (y \<^loc>\<otimes> x) \<^loc>\<otimes> y'" by simp 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

118 
also with eq neutl have "... = y'" by simp 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

119 
finally show ?thesis . 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

120 
qed 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

121 

b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

122 
lemma (in monoid) units_inv_comm: 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

123 
assumes inv: "x \<^loc>\<otimes> y = \<^loc>\<one>" 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

124 
and G: "x \<in> units" 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

125 
shows "y \<^loc>\<otimes> x = \<^loc>\<one>" 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

126 
proof  
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

127 
from G inv_obtain obtain z 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

128 
where z_choice: "z \<^loc>\<otimes> x = \<^loc>\<one>" by blast 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

129 
from inv neutl neutr have "x \<^loc>\<otimes> y \<^loc>\<otimes> x = x \<^loc>\<otimes> \<^loc>\<one>" by simp 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

130 
with assoc have "z \<^loc>\<otimes> x \<^loc>\<otimes> y \<^loc>\<otimes> x = z \<^loc>\<otimes> x \<^loc>\<otimes> \<^loc>\<one>" by simp 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

131 
with neutl z_choice show ?thesis by simp 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

132 
qed 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

133 

b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

134 
consts 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

135 
reduce :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

136 

b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

137 
primrec 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

138 
"reduce f g 0 x = g" 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

139 
"reduce f g (Suc n) x = f x (reduce f g n x)" 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

140 

b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

141 
definition (in monoid) 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

142 
npow :: "nat \<Rightarrow> 'a \<Rightarrow> 'a" 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

143 
npow_def_prim: "npow n x = reduce (op \<^loc>\<otimes>) \<^loc>\<one> n x" 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

144 

b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

145 
abbreviation (in monoid) 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

146 
abbrev_npow :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infix "\<^loc>\<up>" 75) 
20178  147 
"x \<^loc>\<up> n \<equiv> npow n x" 
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

148 

b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

149 
lemma (in monoid) npow_def: 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

150 
"x \<^loc>\<up> 0 = \<^loc>\<one>" 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

151 
"x \<^loc>\<up> Suc n = x \<^loc>\<otimes> x \<^loc>\<up> n" 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

152 
using npow_def_prim by simp_all 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

153 

b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

154 
lemma (in monoid) nat_pow_one: 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

155 
"\<^loc>\<one> \<^loc>\<up> n = \<^loc>\<one>" 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

156 
using npow_def neutl by (induct n) simp_all 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

157 

b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

158 
lemma (in monoid) nat_pow_mult: 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

159 
"npow n x \<^loc>\<otimes> npow m x = npow (n + m) x" 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

160 
proof (induct n) 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

161 
case 0 with neutl npow_def show ?case by simp 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

162 
next 
19933  163 
case (Suc n) with Suc.hyps assoc npow_def show ?case by simp 
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

164 
qed 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

165 

b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

166 
lemma (in monoid) nat_pow_pow: 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

167 
"npow n (npow m x) = npow (n * m) x" 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

168 
using npow_def nat_pow_mult by (induct n) simp_all 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

169 

b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

170 
class group = monoidl + 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

171 
fixes inv :: "'a \<Rightarrow> 'a" ("\<^loc>\<div> _" [81] 80) 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

172 
assumes invl: "\<^loc>\<div> x \<^loc>\<otimes> x = \<^loc>\<one>" 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

173 

b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

174 
class group_comm = group + monoid_comm 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

175 

20178  176 
instance group_comm_int_def: int :: group_comm 
177 
"\<div> k \<equiv>  (k\<Colon>int)" 

19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

178 
proof 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

179 
fix k :: int 
20178  180 
from group_comm_int_def show "\<div> k \<otimes> k = \<one>" by simp 
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

181 
qed 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

182 

b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

183 
lemma (in group) cancel: 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

184 
"(x \<^loc>\<otimes> y = x \<^loc>\<otimes> z) = (y = z)" 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

185 
proof 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

186 
fix x y z :: 'a 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

187 
assume eq: "x \<^loc>\<otimes> y = x \<^loc>\<otimes> z" 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

188 
hence "\<^loc>\<div> x \<^loc>\<otimes> (x \<^loc>\<otimes> y) = \<^loc>\<div> x \<^loc>\<otimes> (x \<^loc>\<otimes> z)" by simp 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

189 
with assoc have "\<^loc>\<div> x \<^loc>\<otimes> x \<^loc>\<otimes> y = \<^loc>\<div> x \<^loc>\<otimes> x \<^loc>\<otimes> z" by simp 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

190 
with neutl invl show "y = z" by simp 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

191 
next 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

192 
fix x y z :: 'a 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

193 
assume eq: "y = z" 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

194 
thus "x \<^loc>\<otimes> y = x \<^loc>\<otimes> z" by simp 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

195 
qed 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

196 

b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

197 
lemma (in group) neutr: 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

198 
"x \<^loc>\<otimes> \<^loc>\<one> = x" 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

199 
proof  
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

200 
from invl have "\<^loc>\<div> x \<^loc>\<otimes> x = \<^loc>\<one>" by simp 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

201 
with assoc [symmetric] neutl invl have "\<^loc>\<div> x \<^loc>\<otimes> (x \<^loc>\<otimes> \<^loc>\<one>) = \<^loc>\<div> x \<^loc>\<otimes> x" by simp 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

202 
with cancel show ?thesis by simp 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

203 
qed 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

204 

b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

205 
lemma (in group) invr: 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

206 
"x \<^loc>\<otimes> \<^loc>\<div> x = \<^loc>\<one>" 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

207 
proof  
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

208 
from neutl invl have "\<^loc>\<div> x \<^loc>\<otimes> x \<^loc>\<otimes> \<^loc>\<div> x = \<^loc>\<div> x" by simp 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

209 
with neutr have "\<^loc>\<div> x \<^loc>\<otimes> x \<^loc>\<otimes> \<^loc>\<div> x = \<^loc>\<div> x \<^loc>\<otimes> \<^loc>\<one> " by simp 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

210 
with assoc have "\<^loc>\<div> x \<^loc>\<otimes> (x \<^loc>\<otimes> \<^loc>\<div> x) = \<^loc>\<div> x \<^loc>\<otimes> \<^loc>\<one> " by simp 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

211 
with cancel show ?thesis .. 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

212 
qed 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

213 

20383  214 
instance group < monoid 
19928  215 
proof  
20383  216 
fix x 
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

217 
from neutr show "x \<^loc>\<otimes> \<^loc>\<one> = x" . 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

218 
qed 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

219 

b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

220 
lemma (in group) all_inv [intro]: 
20178  221 
"(x\<Colon>'a) \<in> monoid.units (op \<^loc>\<otimes>) \<^loc>\<one>" 
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

222 
unfolding units_def 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

223 
proof  
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

224 
fix x :: "'a" 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

225 
from invl invr have "\<^loc>\<div> x \<^loc>\<otimes> x = \<^loc>\<one>" and "x \<^loc>\<otimes> \<^loc>\<div> x = \<^loc>\<one>" . 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

226 
then obtain y where "y \<^loc>\<otimes> x = \<^loc>\<one>" and "x \<^loc>\<otimes> y = \<^loc>\<one>" .. 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

227 
hence "\<exists>y\<Colon>'a. y \<^loc>\<otimes> x = \<^loc>\<one> \<and> x \<^loc>\<otimes> y = \<^loc>\<one>" by blast 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

228 
thus "x \<in> {y\<Colon>'a. \<exists>x\<Colon>'a. x \<^loc>\<otimes> y = \<^loc>\<one> \<and> y \<^loc>\<otimes> x = \<^loc>\<one>}" by simp 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

229 
qed 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

230 

b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

231 
lemma (in group) cancer: 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

232 
"(y \<^loc>\<otimes> x = z \<^loc>\<otimes> x) = (y = z)" 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

233 
proof 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

234 
assume eq: "y \<^loc>\<otimes> x = z \<^loc>\<otimes> x" 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

235 
with assoc [symmetric] have "y \<^loc>\<otimes> (x \<^loc>\<otimes> \<^loc>\<div> x) = z \<^loc>\<otimes> (x \<^loc>\<otimes> \<^loc>\<div> x)" by (simp del: invr) 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

236 
with invr neutr show "y = z" by simp 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

237 
next 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

238 
assume eq: "y = z" 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

239 
thus "y \<^loc>\<otimes> x = z \<^loc>\<otimes> x" by simp 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

240 
qed 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

241 

b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

242 
lemma (in group) inv_one: 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

243 
"\<^loc>\<div> \<^loc>\<one> = \<^loc>\<one>" 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

244 
proof  
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

245 
from neutl have "\<^loc>\<div> \<^loc>\<one> = \<^loc>\<one> \<^loc>\<otimes> (\<^loc>\<div> \<^loc>\<one>)" .. 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

246 
moreover from invr have "... = \<^loc>\<one>" by simp 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

247 
finally show ?thesis . 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

248 
qed 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

249 

b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

250 
lemma (in group) inv_inv: 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

251 
"\<^loc>\<div> (\<^loc>\<div> x) = x" 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

252 
proof  
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

253 
from invl invr neutr 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

254 
have "\<^loc>\<div> (\<^loc>\<div> x) \<^loc>\<otimes> \<^loc>\<div> x \<^loc>\<otimes> x = x \<^loc>\<otimes> \<^loc>\<div> x \<^loc>\<otimes> x" by simp 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

255 
with assoc [symmetric] 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

256 
have "\<^loc>\<div> (\<^loc>\<div> x) \<^loc>\<otimes> (\<^loc>\<div> x \<^loc>\<otimes> x) = x \<^loc>\<otimes> (\<^loc>\<div> x \<^loc>\<otimes> x)" by simp 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

257 
with invl neutr show ?thesis by simp 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

258 
qed 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

259 

b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

260 
lemma (in group) inv_mult_group: 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

261 
"\<^loc>\<div> (x \<^loc>\<otimes> y) = \<^loc>\<div> y \<^loc>\<otimes> \<^loc>\<div> x" 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

262 
proof  
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

263 
from invl have "\<^loc>\<div> (x \<^loc>\<otimes> y) \<^loc>\<otimes> (x \<^loc>\<otimes> y) = \<^loc>\<one>" by simp 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

264 
with assoc have "\<^loc>\<div> (x \<^loc>\<otimes> y) \<^loc>\<otimes> x \<^loc>\<otimes> y = \<^loc>\<one>" by simp 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

265 
with neutl have "\<^loc>\<div> (x \<^loc>\<otimes> y) \<^loc>\<otimes> x \<^loc>\<otimes> y \<^loc>\<otimes> \<^loc>\<div> y \<^loc>\<otimes> \<^loc>\<div> x = \<^loc>\<div> y \<^loc>\<otimes> \<^loc>\<div> x" by simp 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

266 
with assoc have "\<^loc>\<div> (x \<^loc>\<otimes> y) \<^loc>\<otimes> (x \<^loc>\<otimes> (y \<^loc>\<otimes> \<^loc>\<div> y) \<^loc>\<otimes> \<^loc>\<div> x) = \<^loc>\<div> y \<^loc>\<otimes> \<^loc>\<div> x" by simp 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

267 
with invr neutr show ?thesis by simp 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

268 
qed 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

269 

b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

270 
lemma (in group) inv_comm: 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

271 
"x \<^loc>\<otimes> \<^loc>\<div> x = \<^loc>\<div> x \<^loc>\<otimes> x" 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

272 
using invr invl by simp 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

273 

b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

274 
definition (in group) 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

275 
pow :: "int \<Rightarrow> 'a \<Rightarrow> 'a" 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

276 
pow_def: "pow k x = (if k < 0 then \<^loc>\<div> (monoid.npow (op \<^loc>\<otimes>) \<^loc>\<one> (nat (k)) x) 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

277 
else (monoid.npow (op \<^loc>\<otimes>) \<^loc>\<one> (nat k) x))" 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

278 

b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

279 
abbreviation (in group) 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

280 
abbrev_pow :: "'a \<Rightarrow> int \<Rightarrow> 'a" (infix "\<^loc>\<up>" 75) 
19928  281 
"x \<^loc>\<up> k \<equiv> pow k x" 
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

282 

b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

283 
lemma (in group) int_pow_zero: 
20178  284 
"x \<^loc>\<up> (0\<Colon>int) = \<^loc>\<one>" 
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

285 
using npow_def pow_def by simp 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

286 

b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

287 
lemma (in group) int_pow_one: 
20178  288 
"\<^loc>\<one> \<^loc>\<up> (k\<Colon>int) = \<^loc>\<one>" 
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

289 
using pow_def nat_pow_one inv_one by simp 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

290 

b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

291 
instance group_prod_def: (group, group) * :: group 
20178  292 
mult_prod_def: "x \<otimes> y \<equiv> let (x1, x2) = x; (y1, y2) = y in 
19958  293 
(x1 \<otimes> y1, x2 \<otimes> y2)" 
20178  294 
mult_one_def: "\<one> \<equiv> (\<one>, \<one>)" 
295 
mult_inv_def: "\<div> x \<equiv> let (x1, x2) = x in (\<div> x1, \<div> x2)" 

19928  296 
by default (simp_all add: split_paired_all group_prod_def assoc neutl invl) 
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

297 

b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

298 
instance group_comm_prod_def: (group_comm, group_comm) * :: group_comm 
19928  299 
by default (simp_all add: split_paired_all group_prod_def assoc neutl invl comm) 
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

300 

b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

301 
definition 
20383  302 
"X a b c = (a \<otimes> \<one> \<otimes> b, a \<otimes> \<one> \<otimes> b, [a, b] \<otimes> \<one> \<otimes> [a, b, c])" 
303 
"Y a b c = (a, \<div> a) \<otimes> \<one> \<otimes> \<div> (b, \<div> c)" 

304 

305 
definition 

306 
"x1 = X (1::nat) 2 3" 

307 
"x2 = X (1::int) 2 3" 

308 
"y2 = Y (1::int) 2 3" 

19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

309 

20178  310 
code_generate "op \<otimes>" \<one> inv 
20383  311 
code_generate (ml, haskell) X Y 
312 
code_generate (ml, haskell) x1 x2 y2 

19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

313 

b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

314 
code_serialize ml () 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

315 

b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

316 
end 