author | haftmann |
Mon, 08 Oct 2007 22:03:21 +0200 | |
changeset 24914 | 95cda5dd58d5 |
parent 24843 | 0fc73c4003ac |
child 25062 | af5ef0d4d655 |
permissions | -rw-r--r-- |
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 |
|
22424 | 5 |
header {* Test and examples for Isar class package *} |
19281
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 |
24914
95cda5dd58d5
added proper subclass concept; improved class target
haftmann
parents:
24843
diff
changeset
|
8 |
imports List |
19281
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 |
|
22473 | 11 |
class semigroup = type + |
19281
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 |
21924 | 19 |
from mult_nat_def show "m \<otimes> n \<otimes> q = m \<otimes> (n \<otimes> q)" by simp |
19281
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 |
21924 | 26 |
from mult_int_def show "k \<otimes> l \<otimes> j = k \<otimes> (l \<otimes> j)" by simp |
19281
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 |
|
23952 | 29 |
instance * :: (semigroup, semigroup) semigroup |
30 |
mult_prod_def: "x \<otimes> y \<equiv> let (x1, x2) = x; (y1, y2) = y in |
|
31 |
(x1 \<otimes> y1, x2 \<otimes> y2)" |
|
32 |
by default (simp_all add: split_paired_all mult_prod_def assoc) |
|
33 |
||
20597 | 34 |
instance list :: (type) semigroup |
20178 | 35 |
"xs \<otimes> ys \<equiv> xs @ ys" |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
36 |
proof |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
37 |
fix xs ys zs :: "'a list" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
38 |
show "xs \<otimes> ys \<otimes> zs = xs \<otimes> (ys \<otimes> zs)" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
39 |
proof - |
21924 | 40 |
from mult_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
|
41 |
thus ?thesis by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
42 |
qed |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
43 |
qed |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
44 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
45 |
class monoidl = semigroup + |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
46 |
fixes one :: 'a ("\<^loc>\<one>") |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
47 |
assumes neutl: "\<^loc>\<one> \<^loc>\<otimes> x = x" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
48 |
|
21924 | 49 |
instance nat :: monoidl and int :: monoidl |
20178 | 50 |
"\<one> \<equiv> 0" |
51 |
"\<one> \<equiv> 0" |
|
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
52 |
proof |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
53 |
fix n :: nat |
21924 | 54 |
from mult_nat_def one_nat_def show "\<one> \<otimes> n = n" by simp |
20178 | 55 |
next |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
56 |
fix k :: int |
21924 | 57 |
from mult_int_def one_int_def show "\<one> \<otimes> k = k" by simp |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
58 |
qed |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
59 |
|
23952 | 60 |
instance * :: (monoidl, monoidl) monoidl |
61 |
one_prod_def: "\<one> \<equiv> (\<one>, \<one>)" |
|
62 |
by default (simp_all add: split_paired_all mult_prod_def one_prod_def neutl) |
|
63 |
||
20597 | 64 |
instance list :: (type) monoidl |
20178 | 65 |
"\<one> \<equiv> []" |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
66 |
proof |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
67 |
fix xs :: "'a list" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
68 |
show "\<one> \<otimes> xs = xs" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
69 |
proof - |
20178 | 70 |
from mult_list_def have "\<And>xs ys\<Colon>'a list. xs \<otimes> ys \<equiv> xs @ ys" . |
21924 | 71 |
moreover from one_list_def have "\<one> \<equiv> []\<Colon>'a list" by simp |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
72 |
ultimately show ?thesis by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
73 |
qed |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
74 |
qed |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
75 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
76 |
class monoid = monoidl + |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
77 |
assumes neutr: "x \<^loc>\<otimes> \<^loc>\<one> = x" |
21707 | 78 |
begin |
79 |
||
80 |
definition |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21125
diff
changeset
|
81 |
units :: "'a set" where |
21707 | 82 |
"units = {y. \<exists>x. x \<^loc>\<otimes> y = \<^loc>\<one> \<and> y \<^loc>\<otimes> x = \<^loc>\<one>}" |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
83 |
|
21707 | 84 |
lemma inv_obtain: |
85 |
assumes "x \<in> units" |
|
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
86 |
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
|
87 |
proof - |
21707 | 88 |
from assms units_def obtain y |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
89 |
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
|
90 |
thus ?thesis .. |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
91 |
qed |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
92 |
|
21707 | 93 |
lemma inv_unique: |
94 |
assumes "y \<^loc>\<otimes> x = \<^loc>\<one>" "x \<^loc>\<otimes> y' = \<^loc>\<one>" |
|
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
95 |
shows "y = y'" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
96 |
proof - |
21707 | 97 |
from assms neutr have "y = y \<^loc>\<otimes> (x \<^loc>\<otimes> y')" by simp |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
98 |
also with assoc have "... = (y \<^loc>\<otimes> x) \<^loc>\<otimes> y'" by simp |
21707 | 99 |
also with assms neutl have "... = y'" by simp |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
100 |
finally show ?thesis . |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
101 |
qed |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
102 |
|
21707 | 103 |
lemma units_inv_comm: |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
104 |
assumes inv: "x \<^loc>\<otimes> y = \<^loc>\<one>" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
105 |
and G: "x \<in> units" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
106 |
shows "y \<^loc>\<otimes> x = \<^loc>\<one>" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
107 |
proof - |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
108 |
from G inv_obtain obtain z |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
109 |
where z_choice: "z \<^loc>\<otimes> x = \<^loc>\<one>" by blast |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
110 |
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
|
111 |
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
|
112 |
with neutl z_choice show ?thesis by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
113 |
qed |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
114 |
|
23952 | 115 |
fun |
116 |
npow :: "nat \<Rightarrow> 'a \<Rightarrow> 'a" |
|
117 |
where |
|
118 |
"npow 0 x = \<^loc>\<one>" |
|
119 |
| "npow (Suc n) x = x \<^loc>\<otimes> npow n x" |
|
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
120 |
|
21707 | 121 |
abbreviation |
122 |
npow_syn :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infix "\<^loc>\<up>" 75) where |
|
20178 | 123 |
"x \<^loc>\<up> n \<equiv> npow n x" |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
124 |
|
21707 | 125 |
lemma nat_pow_one: |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
126 |
"\<^loc>\<one> \<^loc>\<up> n = \<^loc>\<one>" |
23952 | 127 |
using neutl by (induct n) simp_all |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
128 |
|
21707 | 129 |
lemma nat_pow_mult: "x \<^loc>\<up> n \<^loc>\<otimes> x \<^loc>\<up> m = x \<^loc>\<up> (n + m)" |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
130 |
proof (induct n) |
23952 | 131 |
case 0 with neutl show ?case by simp |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
132 |
next |
23952 | 133 |
case (Suc n) with Suc.hyps assoc show ?case by simp |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
134 |
qed |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
135 |
|
21707 | 136 |
lemma nat_pow_pow: "(x \<^loc>\<up> m) \<^loc>\<up> n = x \<^loc>\<up> (n * m)" |
23952 | 137 |
using nat_pow_mult by (induct n) simp_all |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
138 |
|
21707 | 139 |
end |
140 |
||
23952 | 141 |
instance * :: (monoid, monoid) monoid |
24282 | 142 |
by default (simp_all add: split_paired_all mult_prod_def one_prod_def neutr) |
23952 | 143 |
|
144 |
instance list :: (type) monoid |
|
145 |
proof |
|
146 |
fix xs :: "'a list" |
|
147 |
show "xs \<otimes> \<one> = xs" |
|
148 |
proof - |
|
149 |
from mult_list_def have "\<And>xs ys\<Colon>'a list. xs \<otimes> ys \<equiv> xs @ ys" . |
|
150 |
moreover from one_list_def have "\<one> \<equiv> []\<Colon>'a list" by simp |
|
151 |
ultimately show ?thesis by simp |
|
152 |
qed |
|
153 |
qed |
|
154 |
||
155 |
class monoid_comm = monoid + |
|
156 |
assumes comm: "x \<^loc>\<otimes> y = y \<^loc>\<otimes> x" |
|
157 |
||
158 |
instance nat :: monoid_comm and int :: monoid_comm |
|
159 |
proof |
|
160 |
fix n :: nat |
|
161 |
from mult_nat_def one_nat_def show "n \<otimes> \<one> = n" by simp |
|
162 |
next |
|
163 |
fix n m :: nat |
|
164 |
from mult_nat_def show "n \<otimes> m = m \<otimes> n" by simp |
|
165 |
next |
|
166 |
fix k :: int |
|
167 |
from mult_int_def one_int_def show "k \<otimes> \<one> = k" by simp |
|
168 |
next |
|
169 |
fix k l :: int |
|
170 |
from mult_int_def show "k \<otimes> l = l \<otimes> k" by simp |
|
171 |
qed |
|
172 |
||
173 |
instance * :: (monoid_comm, monoid_comm) monoid_comm |
|
174 |
by default (simp_all add: split_paired_all mult_prod_def comm) |
|
175 |
||
19281
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>" |
23952 | 179 |
begin |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
180 |
|
23952 | 181 |
lemma cancel: |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
182 |
"(x \<^loc>\<otimes> y = x \<^loc>\<otimes> z) = (y = z)" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
183 |
proof |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
184 |
fix x y z :: 'a |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
185 |
assume eq: "x \<^loc>\<otimes> y = x \<^loc>\<otimes> z" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
186 |
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
|
187 |
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
|
188 |
with neutl invl show "y = z" by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
189 |
next |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
190 |
fix x y z :: 'a |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
191 |
assume eq: "y = z" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
192 |
thus "x \<^loc>\<otimes> y = x \<^loc>\<otimes> z" by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
193 |
qed |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
194 |
|
24914
95cda5dd58d5
added proper subclass concept; improved class target
haftmann
parents:
24843
diff
changeset
|
195 |
subclass monoid |
95cda5dd58d5
added proper subclass concept; improved class target
haftmann
parents:
24843
diff
changeset
|
196 |
proof unfold_locales |
95cda5dd58d5
added proper subclass concept; improved class target
haftmann
parents:
24843
diff
changeset
|
197 |
fix x |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
198 |
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
|
199 |
with assoc [symmetric] neutl invl have "\<^loc>\<div> x \<^loc>\<otimes> (x \<^loc>\<otimes> \<^loc>\<one>) = \<^loc>\<div> x \<^loc>\<otimes> x" by simp |
24914
95cda5dd58d5
added proper subclass concept; improved class target
haftmann
parents:
24843
diff
changeset
|
200 |
with cancel show "x \<^loc>\<otimes> \<^loc>\<one> = x" by simp |
19281
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 |
|
24914
95cda5dd58d5
added proper subclass concept; improved class target
haftmann
parents:
24843
diff
changeset
|
203 |
end context group begin |
95cda5dd58d5
added proper subclass concept; improved class target
haftmann
parents:
24843
diff
changeset
|
204 |
|
95cda5dd58d5
added proper subclass concept; improved class target
haftmann
parents:
24843
diff
changeset
|
205 |
find_theorems name: neut |
95cda5dd58d5
added proper subclass concept; improved class target
haftmann
parents:
24843
diff
changeset
|
206 |
|
23952 | 207 |
lemma invr: |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
208 |
"x \<^loc>\<otimes> \<^loc>\<div> x = \<^loc>\<one>" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
209 |
proof - |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
210 |
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
|
211 |
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
|
212 |
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
|
213 |
with cancel show ?thesis .. |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
214 |
qed |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
215 |
|
23952 | 216 |
lemma all_inv [intro]: |
217 |
"(x\<Colon>'a) \<in> units" |
|
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
218 |
unfolding units_def |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
219 |
proof - |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
220 |
fix x :: "'a" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
221 |
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
|
222 |
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
|
223 |
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
|
224 |
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
|
225 |
qed |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
226 |
|
23952 | 227 |
lemma cancer: |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
228 |
"(y \<^loc>\<otimes> x = z \<^loc>\<otimes> x) = (y = z)" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
229 |
proof |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
230 |
assume eq: "y \<^loc>\<otimes> x = z \<^loc>\<otimes> x" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
231 |
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
|
232 |
with invr neutr show "y = z" by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
233 |
next |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
234 |
assume eq: "y = z" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
235 |
thus "y \<^loc>\<otimes> x = z \<^loc>\<otimes> x" by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
236 |
qed |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
237 |
|
23952 | 238 |
lemma inv_one: |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
239 |
"\<^loc>\<div> \<^loc>\<one> = \<^loc>\<one>" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
240 |
proof - |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
241 |
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
|
242 |
moreover from invr have "... = \<^loc>\<one>" by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
243 |
finally show ?thesis . |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
244 |
qed |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
245 |
|
23952 | 246 |
lemma inv_inv: |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
247 |
"\<^loc>\<div> (\<^loc>\<div> x) = x" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
248 |
proof - |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
249 |
from invl invr neutr |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
250 |
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
|
251 |
with assoc [symmetric] |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
252 |
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
|
253 |
with invl neutr show ?thesis by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
254 |
qed |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
255 |
|
23952 | 256 |
lemma inv_mult_group: |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
257 |
"\<^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
|
258 |
proof - |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
259 |
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
|
260 |
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
|
261 |
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
|
262 |
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
|
263 |
with invr neutr show ?thesis by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
264 |
qed |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
265 |
|
23952 | 266 |
lemma inv_comm: |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
267 |
"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
|
268 |
using invr invl by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
269 |
|
23952 | 270 |
definition |
271 |
pow :: "int \<Rightarrow> 'a \<Rightarrow> 'a" |
|
272 |
where |
|
273 |
"pow k x = (if k < 0 then \<^loc>\<div> (npow (nat (-k)) x) |
|
274 |
else (npow (nat k) x))" |
|
275 |
||
276 |
abbreviation |
|
277 |
pow_syn :: "'a \<Rightarrow> int \<Rightarrow> 'a" (infix "\<^loc>\<up>\<up>" 75) |
|
278 |
where |
|
279 |
"x \<^loc>\<up>\<up> k \<equiv> pow k x" |
|
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
280 |
|
23952 | 281 |
lemma int_pow_zero: |
282 |
"x \<^loc>\<up>\<up> (0\<Colon>int) = \<^loc>\<one>" |
|
283 |
using pow_def by simp |
|
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
284 |
|
23952 | 285 |
lemma int_pow_one: |
286 |
"\<^loc>\<one> \<^loc>\<up>\<up> (k\<Colon>int) = \<^loc>\<one>" |
|
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
287 |
using pow_def nat_pow_one inv_one by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
288 |
|
23952 | 289 |
end |
20427 | 290 |
|
21924 | 291 |
instance * :: (group, group) group |
20427 | 292 |
inv_prod_def: "\<div> x \<equiv> let (x1, x2) = x in (\<div> x1, \<div> x2)" |
22384
33a46e6c7f04
prefix of class interpretation not mandatory any longer
haftmann
parents:
22321
diff
changeset
|
293 |
by default (simp_all add: split_paired_all mult_prod_def one_prod_def inv_prod_def invl) |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
294 |
|
23952 | 295 |
class group_comm = group + monoid_comm |
296 |
||
297 |
instance int :: group_comm |
|
298 |
"\<div> k \<equiv> - (k\<Colon>int)" |
|
299 |
proof |
|
300 |
fix k :: int |
|
301 |
from mult_int_def one_int_def inv_int_def show "\<div> k \<otimes> k = \<one>" by simp |
|
302 |
qed |
|
303 |
||
21924 | 304 |
instance * :: (group_comm, group_comm) group_comm |
22384
33a46e6c7f04
prefix of class interpretation not mandatory any longer
haftmann
parents:
22321
diff
changeset
|
305 |
by default (simp_all add: split_paired_all mult_prod_def comm) |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
306 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
307 |
definition |
23952 | 308 |
"X a b c = (a \<otimes> \<one> \<otimes> b, a \<otimes> \<one> \<otimes> b, npow 3 [a, b] \<otimes> \<one> \<otimes> [a, b, c])" |
309 |
||
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21125
diff
changeset
|
310 |
definition |
24282 | 311 |
"Y a b c = (a, \<div> a) \<otimes> \<one> \<otimes> \<div> (b, \<div> pow (-3) c)" |
20383 | 312 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21125
diff
changeset
|
313 |
definition "x1 = X (1::nat) 2 3" |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21125
diff
changeset
|
314 |
definition "x2 = X (1::int) 2 3" |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21125
diff
changeset
|
315 |
definition "y2 = Y (1::int) 2 3" |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
316 |
|
24914
95cda5dd58d5
added proper subclass concept; improved class target
haftmann
parents:
24843
diff
changeset
|
317 |
export_code x1 x2 y2 pow in SML module_name Classpackage |
23810 | 318 |
in OCaml file - |
319 |
in Haskell file - |
|
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 |
end |