author | haftmann |
Sun, 06 May 2007 21:50:17 +0200 | |
changeset 22845 | 5f9138bcb3d7 |
parent 22473 | 753123c89d72 |
child 23810 | f5e6932d0500 |
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 |
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 |
|
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 |
|
20597 | 29 |
instance list :: (type) 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 - |
21924 | 35 |
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
|
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 |
|
21924 | 44 |
instance nat :: monoidl and int :: monoidl |
20178 | 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 |
21924 | 49 |
from mult_nat_def one_nat_def show "\<one> \<otimes> n = n" by simp |
20178 | 50 |
next |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
51 |
fix k :: int |
21924 | 52 |
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
|
53 |
qed |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
54 |
|
20597 | 55 |
instance list :: (type) 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" . |
21924 | 62 |
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
|
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 |
|
21924 | 70 |
instance list :: (type) 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" . |
21924 | 76 |
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
|
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 |
|
21924 | 84 |
instance 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 |
21924 | 87 |
from mult_nat_def one_nat_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 |
21924 | 90 |
from mult_nat_def show "n \<otimes> m = m \<otimes> n" by simp |
20178 | 91 |
next |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
92 |
fix k :: int |
21924 | 93 |
from mult_int_def one_int_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 |
21924 | 96 |
from mult_int_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 |
|
21707 | 99 |
context monoid |
100 |
begin |
|
101 |
||
102 |
definition |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21125
diff
changeset
|
103 |
units :: "'a set" where |
21707 | 104 |
"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
|
105 |
|
22384
33a46e6c7f04
prefix of class interpretation not mandatory any longer
haftmann
parents:
22321
diff
changeset
|
106 |
end |
33a46e6c7f04
prefix of class interpretation not mandatory any longer
haftmann
parents:
22321
diff
changeset
|
107 |
|
33a46e6c7f04
prefix of class interpretation not mandatory any longer
haftmann
parents:
22321
diff
changeset
|
108 |
context monoid |
33a46e6c7f04
prefix of class interpretation not mandatory any longer
haftmann
parents:
22321
diff
changeset
|
109 |
begin |
33a46e6c7f04
prefix of class interpretation not mandatory any longer
haftmann
parents:
22321
diff
changeset
|
110 |
|
21707 | 111 |
lemma inv_obtain: |
112 |
assumes "x \<in> units" |
|
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
113 |
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
|
114 |
proof - |
21707 | 115 |
from assms units_def obtain y |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
116 |
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
|
117 |
thus ?thesis .. |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
118 |
qed |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
119 |
|
21707 | 120 |
lemma inv_unique: |
121 |
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
|
122 |
shows "y = y'" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
123 |
proof - |
21707 | 124 |
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
|
125 |
also with assoc have "... = (y \<^loc>\<otimes> x) \<^loc>\<otimes> y'" by simp |
21707 | 126 |
also with assms neutl have "... = y'" by simp |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
127 |
finally show ?thesis . |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
128 |
qed |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
129 |
|
21707 | 130 |
lemma units_inv_comm: |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
131 |
assumes inv: "x \<^loc>\<otimes> y = \<^loc>\<one>" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
132 |
and G: "x \<in> units" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
133 |
shows "y \<^loc>\<otimes> x = \<^loc>\<one>" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
134 |
proof - |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
135 |
from G inv_obtain obtain z |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
136 |
where z_choice: "z \<^loc>\<otimes> x = \<^loc>\<one>" by blast |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
137 |
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
|
138 |
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
|
139 |
with neutl z_choice show ?thesis by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
140 |
qed |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
141 |
|
21707 | 142 |
end |
143 |
||
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
144 |
consts |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
145 |
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
|
146 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
147 |
primrec |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
148 |
"reduce f g 0 x = g" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
149 |
"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
|
150 |
|
21707 | 151 |
context monoid |
152 |
begin |
|
153 |
||
154 |
definition |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21125
diff
changeset
|
155 |
npow :: "nat \<Rightarrow> 'a \<Rightarrow> 'a" where |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
156 |
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
|
157 |
|
22384
33a46e6c7f04
prefix of class interpretation not mandatory any longer
haftmann
parents:
22321
diff
changeset
|
158 |
end |
33a46e6c7f04
prefix of class interpretation not mandatory any longer
haftmann
parents:
22321
diff
changeset
|
159 |
|
33a46e6c7f04
prefix of class interpretation not mandatory any longer
haftmann
parents:
22321
diff
changeset
|
160 |
context monoid |
33a46e6c7f04
prefix of class interpretation not mandatory any longer
haftmann
parents:
22321
diff
changeset
|
161 |
begin |
33a46e6c7f04
prefix of class interpretation not mandatory any longer
haftmann
parents:
22321
diff
changeset
|
162 |
|
21707 | 163 |
abbreviation |
164 |
npow_syn :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infix "\<^loc>\<up>" 75) where |
|
20178 | 165 |
"x \<^loc>\<up> n \<equiv> npow n x" |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
166 |
|
21707 | 167 |
lemma npow_def: |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
168 |
"x \<^loc>\<up> 0 = \<^loc>\<one>" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
169 |
"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
|
170 |
using npow_def_prim by simp_all |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
171 |
|
21707 | 172 |
lemma nat_pow_one: |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
173 |
"\<^loc>\<one> \<^loc>\<up> n = \<^loc>\<one>" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
174 |
using npow_def neutl by (induct n) simp_all |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
175 |
|
21707 | 176 |
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
|
177 |
proof (induct n) |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
178 |
case 0 with neutl npow_def show ?case by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
179 |
next |
19933 | 180 |
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
|
181 |
qed |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
182 |
|
21707 | 183 |
lemma nat_pow_pow: "(x \<^loc>\<up> m) \<^loc>\<up> n = x \<^loc>\<up> (n * m)" |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
184 |
using npow_def nat_pow_mult by (induct n) simp_all |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
185 |
|
21707 | 186 |
end |
187 |
||
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
188 |
class group = monoidl + |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
189 |
fixes inv :: "'a \<Rightarrow> 'a" ("\<^loc>\<div> _" [81] 80) |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
190 |
assumes invl: "\<^loc>\<div> x \<^loc>\<otimes> x = \<^loc>\<one>" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
191 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
192 |
class group_comm = group + monoid_comm |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
193 |
|
21924 | 194 |
instance int :: group_comm |
20178 | 195 |
"\<div> k \<equiv> - (k\<Colon>int)" |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
196 |
proof |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
197 |
fix k :: int |
21924 | 198 |
from mult_int_def one_int_def inv_int_def show "\<div> k \<otimes> k = \<one>" by simp |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
199 |
qed |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
200 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
201 |
lemma (in group) cancel: |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
202 |
"(x \<^loc>\<otimes> y = x \<^loc>\<otimes> z) = (y = z)" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
203 |
proof |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
204 |
fix x y z :: 'a |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
205 |
assume eq: "x \<^loc>\<otimes> y = x \<^loc>\<otimes> z" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
206 |
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
|
207 |
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
|
208 |
with neutl invl show "y = z" by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
209 |
next |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
210 |
fix x y z :: 'a |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
211 |
assume eq: "y = z" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
212 |
thus "x \<^loc>\<otimes> y = x \<^loc>\<otimes> z" by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
213 |
qed |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
214 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
215 |
lemma (in group) neutr: |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
216 |
"x \<^loc>\<otimes> \<^loc>\<one> = x" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
217 |
proof - |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
218 |
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
|
219 |
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
|
220 |
with cancel show ?thesis by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
221 |
qed |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
222 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
223 |
lemma (in group) invr: |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
224 |
"x \<^loc>\<otimes> \<^loc>\<div> x = \<^loc>\<one>" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
225 |
proof - |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
226 |
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
|
227 |
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
|
228 |
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
|
229 |
with cancel show ?thesis .. |
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 |
|
22321 | 232 |
instance advanced group < monoid |
22179 | 233 |
proof unfold_locales |
20383 | 234 |
fix x |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
235 |
from neutr show "x \<^loc>\<otimes> \<^loc>\<one> = x" . |
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 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
238 |
lemma (in group) all_inv [intro]: |
20178 | 239 |
"(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
|
240 |
unfolding units_def |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
241 |
proof - |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
242 |
fix x :: "'a" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
243 |
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
|
244 |
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
|
245 |
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
|
246 |
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
|
247 |
qed |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
248 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
249 |
lemma (in group) cancer: |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
250 |
"(y \<^loc>\<otimes> x = z \<^loc>\<otimes> x) = (y = z)" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
251 |
proof |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
252 |
assume eq: "y \<^loc>\<otimes> x = z \<^loc>\<otimes> x" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
253 |
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
|
254 |
with invr neutr show "y = z" by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
255 |
next |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
256 |
assume eq: "y = z" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
257 |
thus "y \<^loc>\<otimes> x = z \<^loc>\<otimes> x" 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_one: |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
261 |
"\<^loc>\<div> \<^loc>\<one> = \<^loc>\<one>" |
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 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
|
264 |
moreover from invr have "... = \<^loc>\<one>" by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
265 |
finally show ?thesis . |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
266 |
qed |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
267 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
268 |
lemma (in group) inv_inv: |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
269 |
"\<^loc>\<div> (\<^loc>\<div> x) = x" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
270 |
proof - |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
271 |
from invl invr neutr |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
272 |
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
|
273 |
with assoc [symmetric] |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
274 |
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
|
275 |
with invl neutr show ?thesis by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
276 |
qed |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
277 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
278 |
lemma (in group) inv_mult_group: |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
279 |
"\<^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
|
280 |
proof - |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
281 |
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
|
282 |
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
|
283 |
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
|
284 |
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
|
285 |
with invr neutr show ?thesis by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
286 |
qed |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
287 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
288 |
lemma (in group) inv_comm: |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
289 |
"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
|
290 |
using invr invl by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
291 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
292 |
definition (in group) |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21125
diff
changeset
|
293 |
pow :: "int \<Rightarrow> 'a \<Rightarrow> 'a" where |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21125
diff
changeset
|
294 |
"pow k x = (if k < 0 then \<^loc>\<div> (monoid.npow (op \<^loc>\<otimes>) \<^loc>\<one> (nat (-k)) x) |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
295 |
else (monoid.npow (op \<^loc>\<otimes>) \<^loc>\<one> (nat k) x))" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
296 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
297 |
abbreviation (in group) |
21707 | 298 |
pow_syn :: "'a \<Rightarrow> int \<Rightarrow> 'a" (infix "\<^loc>\<up>" 75) where |
19928 | 299 |
"x \<^loc>\<up> k \<equiv> pow k x" |
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 |
lemma (in group) int_pow_zero: |
20178 | 302 |
"x \<^loc>\<up> (0\<Colon>int) = \<^loc>\<one>" |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
303 |
using npow_def pow_def by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
304 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
305 |
lemma (in group) int_pow_one: |
20178 | 306 |
"\<^loc>\<one> \<^loc>\<up> (k\<Colon>int) = \<^loc>\<one>" |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
307 |
using pow_def nat_pow_one inv_one by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
308 |
|
21924 | 309 |
instance * :: (semigroup, semigroup) semigroup |
20178 | 310 |
mult_prod_def: "x \<otimes> y \<equiv> let (x1, x2) = x; (y1, y2) = y in |
19958 | 311 |
(x1 \<otimes> y1, x2 \<otimes> y2)" |
22384
33a46e6c7f04
prefix of class interpretation not mandatory any longer
haftmann
parents:
22321
diff
changeset
|
312 |
by default (simp_all add: split_paired_all mult_prod_def assoc) |
20427 | 313 |
|
21924 | 314 |
instance * :: (monoidl, monoidl) monoidl |
20427 | 315 |
one_prod_def: "\<one> \<equiv> (\<one>, \<one>)" |
22384
33a46e6c7f04
prefix of class interpretation not mandatory any longer
haftmann
parents:
22321
diff
changeset
|
316 |
by default (simp_all add: split_paired_all mult_prod_def one_prod_def neutl) |
20427 | 317 |
|
21924 | 318 |
instance * :: (monoid, monoid) monoid |
22384
33a46e6c7f04
prefix of class interpretation not mandatory any longer
haftmann
parents:
22321
diff
changeset
|
319 |
by default (simp_all add: split_paired_all mult_prod_def one_prod_def monoid_class.mult_one.neutr) |
20427 | 320 |
|
21924 | 321 |
instance * :: (monoid_comm, monoid_comm) monoid_comm |
22384
33a46e6c7f04
prefix of class interpretation not mandatory any longer
haftmann
parents:
22321
diff
changeset
|
322 |
by default (simp_all add: split_paired_all mult_prod_def comm) |
20427 | 323 |
|
21924 | 324 |
instance * :: (group, group) group |
20427 | 325 |
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
|
326 |
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
|
327 |
|
21924 | 328 |
instance * :: (group_comm, group_comm) group_comm |
22384
33a46e6c7f04
prefix of class interpretation not mandatory any longer
haftmann
parents:
22321
diff
changeset
|
329 |
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
|
330 |
|
22424 | 331 |
|
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
332 |
definition |
20383 | 333 |
"X a b c = (a \<otimes> \<one> \<otimes> b, a \<otimes> \<one> \<otimes> b, [a, b] \<otimes> \<one> \<otimes> [a, b, c])" |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21125
diff
changeset
|
334 |
definition |
20383 | 335 |
"Y a b c = (a, \<div> a) \<otimes> \<one> \<otimes> \<div> (b, \<div> c)" |
336 |
||
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21125
diff
changeset
|
337 |
definition "x1 = X (1::nat) 2 3" |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21125
diff
changeset
|
338 |
definition "x2 = X (1::int) 2 3" |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21125
diff
changeset
|
339 |
definition "y2 = Y (1::int) 2 3" |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
340 |
|
22845 | 341 |
code_gen x1 x2 y2 in SML in OCaml file - in Haskell file - |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
342 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
343 |
end |