author | haftmann |
Sun, 23 Jul 2006 07:21:41 +0200 | |
changeset 20187 | af47971ea304 |
parent 20178 | e56fa3c8b1f1 |
child 20383 | 58f65fc90cf4 |
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 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
5 |
header {* Test and Examples for Pure/Tools/class_package.ML *} |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
6 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
7 |
theory Classpackage |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
8 |
imports Main |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
9 |
begin |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
10 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
11 |
class semigroup = |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
12 |
fixes mult :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<^loc>\<otimes>" 70) |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
13 |
assumes assoc: "x \<^loc>\<otimes> y \<^loc>\<otimes> z = x \<^loc>\<otimes> (y \<^loc>\<otimes> z)" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
14 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
15 |
instance nat :: semigroup |
20178 | 16 |
"m \<otimes> n \<equiv> m + n" |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
17 |
proof |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
18 |
fix m n q :: nat |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
19 |
from semigroup_nat_def show "m \<otimes> n \<otimes> q = m \<otimes> (n \<otimes> q)" by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
20 |
qed |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
21 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
22 |
instance int :: semigroup |
20178 | 23 |
"k \<otimes> l \<equiv> k + l" |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
24 |
proof |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
25 |
fix k l j :: int |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
26 |
from semigroup_int_def show "k \<otimes> l \<otimes> j = k \<otimes> (l \<otimes> j)" by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
27 |
qed |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
28 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
29 |
instance (type) list :: semigroup |
20178 | 30 |
"xs \<otimes> ys \<equiv> xs @ ys" |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
31 |
proof |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
32 |
fix xs ys zs :: "'a list" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
33 |
show "xs \<otimes> ys \<otimes> zs = xs \<otimes> (ys \<otimes> zs)" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
34 |
proof - |
20178 | 35 |
from semigroup_list_def have "\<And>xs ys\<Colon>'a list. xs \<otimes> ys \<equiv> xs @ ys" . |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
36 |
thus ?thesis by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
37 |
qed |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
38 |
qed |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
39 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
40 |
class monoidl = semigroup + |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
41 |
fixes one :: 'a ("\<^loc>\<one>") |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
42 |
assumes neutl: "\<^loc>\<one> \<^loc>\<otimes> x = x" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
43 |
|
20178 | 44 |
instance monoidl_num_def: nat :: monoidl and int :: monoidl |
45 |
"\<one> \<equiv> 0" |
|
46 |
"\<one> \<equiv> 0" |
|
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
47 |
proof |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
48 |
fix n :: nat |
20178 | 49 |
from monoidl_num_def show "\<one> \<otimes> n = n" by simp |
50 |
next |
|
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
51 |
fix k :: int |
20178 | 52 |
from monoidl_num_def show "\<one> \<otimes> k = k" by simp |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
53 |
qed |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
54 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
55 |
instance (type) list :: monoidl |
20178 | 56 |
"\<one> \<equiv> []" |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
57 |
proof |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
58 |
fix xs :: "'a list" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
59 |
show "\<one> \<otimes> xs = xs" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
60 |
proof - |
20178 | 61 |
from mult_list_def have "\<And>xs ys\<Colon>'a list. xs \<otimes> ys \<equiv> xs @ ys" . |
62 |
moreover from monoidl_list_def have "\<one> \<equiv> []\<Colon>'a list" by simp |
|
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
63 |
ultimately show ?thesis by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
64 |
qed |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
65 |
qed |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
66 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
67 |
class monoid = monoidl + |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
68 |
assumes neutr: "x \<^loc>\<otimes> \<^loc>\<one> = x" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
69 |
|
20178 | 70 |
instance monoid_list_def: (type) list :: monoid |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
71 |
proof |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
72 |
fix xs :: "'a list" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
73 |
show "xs \<otimes> \<one> = xs" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
74 |
proof - |
20178 | 75 |
from mult_list_def have "\<And>xs ys\<Colon>'a list. xs \<otimes> ys \<equiv> xs @ ys" . |
76 |
moreover from monoid_list_def have "\<one> \<equiv> []\<Colon>'a list" by simp |
|
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
77 |
ultimately show ?thesis by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
78 |
qed |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
79 |
qed |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
80 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
81 |
class monoid_comm = monoid + |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
82 |
assumes comm: "x \<^loc>\<otimes> y = y \<^loc>\<otimes> x" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
83 |
|
20178 | 84 |
instance monoid_comm_num_def: nat :: monoid_comm and int :: monoid_comm |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
85 |
proof |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
86 |
fix n :: nat |
20178 | 87 |
from monoid_comm_num_def show "n \<otimes> \<one> = n" by simp |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
88 |
next |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
89 |
fix n m :: nat |
20178 | 90 |
from monoid_comm_num_def show "n \<otimes> m = m \<otimes> n" by simp |
91 |
next |
|
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
92 |
fix k :: int |
20178 | 93 |
from monoid_comm_num_def show "k \<otimes> \<one> = k" by simp |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
94 |
next |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
95 |
fix k l :: int |
20178 | 96 |
from monoid_comm_num_def show "k \<otimes> l = l \<otimes> k" by simp |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
97 |
qed |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
98 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
99 |
definition (in monoid) |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
100 |
units :: "'a set" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
101 |
units_def: "units = { y. \<exists>x. x \<^loc>\<otimes> y = \<^loc>\<one> \<and> y \<^loc>\<otimes> x = \<^loc>\<one> }" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
102 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
103 |
lemma (in monoid) inv_obtain: |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
104 |
assumes ass: "x \<in> units" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
105 |
obtains y where "y \<^loc>\<otimes> x = \<^loc>\<one>" and "x \<^loc>\<otimes> y = \<^loc>\<one>" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
106 |
proof - |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
107 |
from ass units_def obtain y |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
108 |
where "y \<^loc>\<otimes> x = \<^loc>\<one>" and "x \<^loc>\<otimes> y = \<^loc>\<one>" by auto |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
109 |
thus ?thesis .. |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
110 |
qed |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
111 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
112 |
lemma (in monoid) inv_unique: |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
113 |
assumes eq: "y \<^loc>\<otimes> x = \<^loc>\<one>" "x \<^loc>\<otimes> y' = \<^loc>\<one>" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
114 |
shows "y = y'" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
115 |
proof - |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
116 |
from eq neutr have "y = y \<^loc>\<otimes> (x \<^loc>\<otimes> y')" by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
117 |
also with assoc have "... = (y \<^loc>\<otimes> x) \<^loc>\<otimes> y'" by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
118 |
also with eq neutl have "... = y'" by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
119 |
finally show ?thesis . |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
120 |
qed |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
121 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
122 |
lemma (in monoid) units_inv_comm: |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
123 |
assumes inv: "x \<^loc>\<otimes> y = \<^loc>\<one>" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
124 |
and G: "x \<in> units" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
125 |
shows "y \<^loc>\<otimes> x = \<^loc>\<one>" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
126 |
proof - |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
127 |
from G inv_obtain obtain z |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
128 |
where z_choice: "z \<^loc>\<otimes> x = \<^loc>\<one>" by blast |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
129 |
from inv neutl neutr have "x \<^loc>\<otimes> y \<^loc>\<otimes> x = x \<^loc>\<otimes> \<^loc>\<one>" by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
130 |
with assoc have "z \<^loc>\<otimes> x \<^loc>\<otimes> y \<^loc>\<otimes> x = z \<^loc>\<otimes> x \<^loc>\<otimes> \<^loc>\<one>" by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
131 |
with neutl z_choice show ?thesis by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
132 |
qed |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
133 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
134 |
consts |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
135 |
reduce :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
136 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
137 |
primrec |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
138 |
"reduce f g 0 x = g" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
139 |
"reduce f g (Suc n) x = f x (reduce f g n x)" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
140 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
141 |
definition (in monoid) |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
142 |
npow :: "nat \<Rightarrow> 'a \<Rightarrow> 'a" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
143 |
npow_def_prim: "npow n x = reduce (op \<^loc>\<otimes>) \<^loc>\<one> n x" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
144 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
145 |
abbreviation (in monoid) |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
146 |
abbrev_npow :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infix "\<^loc>\<up>" 75) |
20178 | 147 |
"x \<^loc>\<up> n \<equiv> npow n x" |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
148 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
149 |
lemma (in monoid) npow_def: |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
150 |
"x \<^loc>\<up> 0 = \<^loc>\<one>" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
151 |
"x \<^loc>\<up> Suc n = x \<^loc>\<otimes> x \<^loc>\<up> n" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
152 |
using npow_def_prim by simp_all |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
153 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
154 |
lemma (in monoid) nat_pow_one: |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
155 |
"\<^loc>\<one> \<^loc>\<up> n = \<^loc>\<one>" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
156 |
using npow_def neutl by (induct n) simp_all |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
157 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
158 |
lemma (in monoid) nat_pow_mult: |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
159 |
"npow n x \<^loc>\<otimes> npow m x = npow (n + m) x" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
160 |
proof (induct n) |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
161 |
case 0 with neutl npow_def show ?case by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
162 |
next |
19933 | 163 |
case (Suc n) with Suc.hyps assoc npow_def show ?case by simp |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
164 |
qed |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
165 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
166 |
lemma (in monoid) nat_pow_pow: |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
167 |
"npow n (npow m x) = npow (n * m) x" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
168 |
using npow_def nat_pow_mult by (induct n) simp_all |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
169 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
170 |
class group = monoidl + |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
171 |
fixes inv :: "'a \<Rightarrow> 'a" ("\<^loc>\<div> _" [81] 80) |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
172 |
assumes invl: "\<^loc>\<div> x \<^loc>\<otimes> x = \<^loc>\<one>" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
173 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
174 |
class group_comm = group + monoid_comm |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
175 |
|
20178 | 176 |
instance group_comm_int_def: int :: group_comm |
177 |
"\<div> k \<equiv> - (k\<Colon>int)" |
|
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
178 |
proof |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
179 |
fix k :: int |
20178 | 180 |
from group_comm_int_def show "\<div> k \<otimes> k = \<one>" by simp |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
181 |
qed |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
182 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
183 |
lemma (in group) cancel: |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
184 |
"(x \<^loc>\<otimes> y = x \<^loc>\<otimes> z) = (y = z)" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
185 |
proof |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
186 |
fix x y z :: 'a |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
187 |
assume eq: "x \<^loc>\<otimes> y = x \<^loc>\<otimes> z" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
188 |
hence "\<^loc>\<div> x \<^loc>\<otimes> (x \<^loc>\<otimes> y) = \<^loc>\<div> x \<^loc>\<otimes> (x \<^loc>\<otimes> z)" by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
189 |
with assoc have "\<^loc>\<div> x \<^loc>\<otimes> x \<^loc>\<otimes> y = \<^loc>\<div> x \<^loc>\<otimes> x \<^loc>\<otimes> z" by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
190 |
with neutl invl show "y = z" by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
191 |
next |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
192 |
fix x y z :: 'a |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
193 |
assume eq: "y = z" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
194 |
thus "x \<^loc>\<otimes> y = x \<^loc>\<otimes> z" by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
195 |
qed |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
196 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
197 |
lemma (in group) neutr: |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
198 |
"x \<^loc>\<otimes> \<^loc>\<one> = x" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
199 |
proof - |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
200 |
from invl have "\<^loc>\<div> x \<^loc>\<otimes> x = \<^loc>\<one>" by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
201 |
with assoc [symmetric] neutl invl have "\<^loc>\<div> x \<^loc>\<otimes> (x \<^loc>\<otimes> \<^loc>\<one>) = \<^loc>\<div> x \<^loc>\<otimes> x" by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
202 |
with cancel show ?thesis by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
203 |
qed |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
204 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
205 |
lemma (in group) invr: |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
206 |
"x \<^loc>\<otimes> \<^loc>\<div> x = \<^loc>\<one>" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
207 |
proof - |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
208 |
from neutl invl have "\<^loc>\<div> x \<^loc>\<otimes> x \<^loc>\<otimes> \<^loc>\<div> x = \<^loc>\<div> x" by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
209 |
with neutr have "\<^loc>\<div> x \<^loc>\<otimes> x \<^loc>\<otimes> \<^loc>\<div> x = \<^loc>\<div> x \<^loc>\<otimes> \<^loc>\<one> " by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
210 |
with assoc have "\<^loc>\<div> x \<^loc>\<otimes> (x \<^loc>\<otimes> \<^loc>\<div> x) = \<^loc>\<div> x \<^loc>\<otimes> \<^loc>\<one> " by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
211 |
with cancel show ?thesis .. |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
212 |
qed |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
213 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
214 |
interpretation group < monoid |
19928 | 215 |
proof - |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
216 |
fix x :: "'a" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
217 |
from neutr show "x \<^loc>\<otimes> \<^loc>\<one> = x" . |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
218 |
qed |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
219 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
220 |
instance group < monoid |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
221 |
proof |
20178 | 222 |
fix x :: "'a\<Colon>group" |
19928 | 223 |
from group.neutr show "x \<otimes> \<one> = x" . |
19281
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 |
lemma (in group) all_inv [intro]: |
20178 | 227 |
"(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
|
228 |
unfolding units_def |
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 |
fix x :: "'a" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
231 |
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
|
232 |
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
|
233 |
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
|
234 |
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
|
235 |
qed |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
236 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
237 |
lemma (in group) cancer: |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
238 |
"(y \<^loc>\<otimes> x = z \<^loc>\<otimes> x) = (y = z)" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
239 |
proof |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
240 |
assume eq: "y \<^loc>\<otimes> x = z \<^loc>\<otimes> x" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
241 |
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
|
242 |
with invr neutr show "y = z" by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
243 |
next |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
244 |
assume eq: "y = z" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
245 |
thus "y \<^loc>\<otimes> x = z \<^loc>\<otimes> x" by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
246 |
qed |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
247 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
248 |
lemma (in group) inv_one: |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
249 |
"\<^loc>\<div> \<^loc>\<one> = \<^loc>\<one>" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
250 |
proof - |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
251 |
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
|
252 |
moreover from invr have "... = \<^loc>\<one>" by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
253 |
finally show ?thesis . |
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 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
256 |
lemma (in group) inv_inv: |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
257 |
"\<^loc>\<div> (\<^loc>\<div> x) = 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 invr neutr |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
260 |
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
|
261 |
with assoc [symmetric] |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
262 |
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
|
263 |
with invl 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 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
266 |
lemma (in group) inv_mult_group: |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
267 |
"\<^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
|
268 |
proof - |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
269 |
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
|
270 |
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
|
271 |
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
|
272 |
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
|
273 |
with invr neutr show ?thesis by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
274 |
qed |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
275 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
276 |
lemma (in group) inv_comm: |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
277 |
"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
|
278 |
using invr invl by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
279 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
280 |
definition (in group) |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
281 |
pow :: "int \<Rightarrow> 'a \<Rightarrow> 'a" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
282 |
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
|
283 |
else (monoid.npow (op \<^loc>\<otimes>) \<^loc>\<one> (nat k) x))" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
284 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
285 |
abbreviation (in group) |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
286 |
abbrev_pow :: "'a \<Rightarrow> int \<Rightarrow> 'a" (infix "\<^loc>\<up>" 75) |
19928 | 287 |
"x \<^loc>\<up> k \<equiv> pow k x" |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
288 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
289 |
lemma (in group) int_pow_zero: |
20178 | 290 |
"x \<^loc>\<up> (0\<Colon>int) = \<^loc>\<one>" |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
291 |
using npow_def pow_def by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
292 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
293 |
lemma (in group) int_pow_one: |
20178 | 294 |
"\<^loc>\<one> \<^loc>\<up> (k\<Colon>int) = \<^loc>\<one>" |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
295 |
using pow_def nat_pow_one inv_one by simp |
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 |
instance group_prod_def: (group, group) * :: group |
20178 | 298 |
mult_prod_def: "x \<otimes> y \<equiv> let (x1, x2) = x; (y1, y2) = y in |
19958 | 299 |
(x1 \<otimes> y1, x2 \<otimes> y2)" |
20178 | 300 |
mult_one_def: "\<one> \<equiv> (\<one>, \<one>)" |
301 |
mult_inv_def: "\<div> x \<equiv> let (x1, x2) = x in (\<div> x1, \<div> x2)" |
|
19928 | 302 |
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
|
303 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
304 |
instance group_comm_prod_def: (group_comm, group_comm) * :: group_comm |
19928 | 305 |
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
|
306 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
307 |
definition |
20178 | 308 |
"x = ((2\<Colon>nat) \<otimes> \<one> \<otimes> 3, (2\<Colon>int) \<otimes> \<one> \<otimes> \<div> 3, [1\<Colon>nat, 2] \<otimes> \<one> \<otimes> [1, 2, 3])" |
309 |
"y = (2 \<Colon> int, \<div> 2 \<Colon> int) \<otimes> \<one> \<otimes> (3, \<div> 3)" |
|
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
310 |
|
20178 | 311 |
code_generate "op \<otimes>" \<one> inv |
19888 | 312 |
code_generate (ml, haskell) x |
313 |
code_generate (ml, haskell) y |
|
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
314 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
315 |
code_serialize ml (-) |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
316 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
317 |
end |