author  haftmann 
Tue, 27 Jun 2006 10:09:44 +0200  
changeset 19951  d58e2c564100 
parent 19933  16a5037f2d25 
child 19958  fc4ac94f03e0 
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 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

16 
"m \<otimes> n == (m::nat) + n" 
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 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

23 
"k \<otimes> l == (k::int) + l" 
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 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

30 
"xs \<otimes> ys == xs @ ys" 
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  
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

35 
from semigroup_list_def have "\<And>xs ys::'a list. xs \<otimes> ys == xs @ ys". 
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 

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

44 
instance nat :: monoidl 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

45 
"\<one> == (0::nat)" 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

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

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

48 
from semigroup_nat_def monoidl_nat_def show "\<one> \<otimes> n = n" by simp 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

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

50 

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

51 
instance int :: monoidl 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

52 
"\<one> == (0::int)" 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

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

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

55 
from semigroup_int_def monoidl_int_def show "\<one> \<otimes> k = k" by simp 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

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

57 

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

58 
instance (type) list :: monoidl 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

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

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

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

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

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

64 
from semigroup_list_def have "\<And>xs ys::'a list. xs \<otimes> ys == xs @ ys". 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

65 
moreover from monoidl_list_def have "\<one> == []::'a list". 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

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

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

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

69 

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

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

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

72 

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

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

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

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

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

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

78 
from semigroup_list_def have "\<And>xs ys::'a list. xs \<otimes> ys == xs @ ys". 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

79 
moreover from monoidl_list_def have "\<one> == []::'a list". 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

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

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

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

83 

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

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

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

86 

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

87 
instance nat :: monoid_comm 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

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

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

90 
from semigroup_nat_def monoidl_nat_def show "n \<otimes> \<one> = n" by simp 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

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

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

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

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

95 

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

96 
instance int :: monoid_comm 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

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

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

99 
from semigroup_int_def monoidl_int_def show "k \<otimes> \<one> = k" by simp 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

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

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

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

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

104 

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

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

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

107 
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

108 

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

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

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

111 
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

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

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

114 
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

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

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

117 

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

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

119 
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

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

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

122 
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

123 
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

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

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

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

127 

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

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

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

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

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

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

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

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

135 
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

136 
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

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

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

139 

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

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

141 
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

142 

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

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

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

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

146 

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

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

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

149 
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

150 

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

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

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

154 

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

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

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

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

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

159 

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

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

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

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

163 

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

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

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

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

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

168 
next 
19933  169 
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

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

171 

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

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

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

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

175 

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

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

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

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

179 

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

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

181 

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

182 
instance int :: group_comm 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

183 
"\<div> k ==  (k::int)" 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

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

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

186 
from semigroup_int_def monoidl_int_def group_comm_int_def show "\<div> k \<otimes> k = \<one>" by simp 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

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

188 

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

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

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

191 
proof 
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: "x \<^loc>\<otimes> y = x \<^loc>\<otimes> z" 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

194 
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

195 
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

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

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

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

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

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

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

202 

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

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

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

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

206 
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

207 
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

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

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

210 

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

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

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

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

214 
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

215 
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

216 
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

217 
with cancel show ?thesis .. 
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 
interpretation group < monoid 
19928  221 
proof  
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

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

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

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

225 

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

226 
instance group < monoid 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

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

228 
fix x :: "'a::group" 
19928  229 
from group.neutr show "x \<otimes> \<one> = x" . 
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

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

231 

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

232 
lemma (in group) all_inv [intro]: 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

233 
"(x::'a) \<in> monoid.units (op \<^loc>\<otimes>) \<^loc>\<one>" 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

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

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

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

237 
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

238 
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

239 
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

240 
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

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

242 

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

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

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

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

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

247 
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

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

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

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

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

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

253 

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

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

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

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

257 
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

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

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

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

261 

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

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

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

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

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

266 
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

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

268 
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

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

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

271 

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

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

273 
"\<^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

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

275 
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

276 
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

277 
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

278 
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

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

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

281 

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

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

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

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

285 

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

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

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

288 
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

289 
else (monoid.npow (op \<^loc>\<otimes>) \<^loc>\<one> (nat k) x))" 
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 
abbreviation (in group) 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

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

294 

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

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

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

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

298 

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

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

300 
"\<^loc>\<one> \<^loc>\<up> (k::int) = \<^loc>\<one>" 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

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

302 

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

303 
instance group_prod_def: (group, group) * :: group 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

304 
mult_prod_def: "x \<otimes> y == let (x1, x2) = x in (let (y1, y2) = y in 
19345  305 
((x1::'a::group) \<otimes> y1, (x2::'b::group) \<otimes> y2))" 
306 
mult_one_def: "\<one> == (\<one>::'a::group, \<one>::'b::group)" 

19951  307 
mult_inv_def: "\<div> x == let (x1::'a::group, x2::'b::group) = x in (\<div> x1, \<div> x2)" 
19928  308 
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

309 

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

310 
instance group_comm_prod_def: (group_comm, group_comm) * :: group_comm 
19928  311 
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

312 

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

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

314 
"x = ((2::nat) \<otimes> \<one> \<otimes> 3, (2::int) \<otimes> \<one> \<otimes> \<div> 3, [1::nat, 2] \<otimes> \<one> \<otimes> [1, 2, 3])" 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

315 
"y = (2 :: int, \<div> 2 :: int) \<otimes> \<one> \<otimes> (3, \<div> 3)" 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

316 

19928  317 
code_generate "op \<otimes>" "\<one>" "inv" 
19888  318 
code_generate (ml, haskell) x 
319 
code_generate (ml, haskell) y 

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

320 

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

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

322 

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

323 
end 