author | wenzelm |
Sun, 01 Oct 2006 18:29:32 +0200 | |
changeset 20813 | 379ce56e5dc2 |
parent 20597 | 65fe827aa595 |
child 21080 | 7d73aa966207 |
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 |
|
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 - |
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 |
|
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" . |
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 |
|
20597 | 70 |
instance monoid_list_def: 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" . |
76 |
moreover from monoid_list_def have "\<one> \<equiv> []\<Colon>'a list" by simp |
|
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
77 |
ultimately show ?thesis by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
78 |
qed |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
79 |
qed |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
80 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
81 |
class monoid_comm = monoid + |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
82 |
assumes comm: "x \<^loc>\<otimes> y = y \<^loc>\<otimes> x" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
83 |
|
20178 | 84 |
instance monoid_comm_num_def: nat :: monoid_comm and int :: monoid_comm |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
85 |
proof |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
86 |
fix n :: nat |
20178 | 87 |
from monoid_comm_num_def show "n \<otimes> \<one> = n" by simp |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
88 |
next |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
89 |
fix n m :: nat |
20178 | 90 |
from monoid_comm_num_def show "n \<otimes> m = m \<otimes> n" by simp |
91 |
next |
|
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
92 |
fix k :: int |
20178 | 93 |
from monoid_comm_num_def show "k \<otimes> \<one> = k" by simp |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
94 |
next |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
95 |
fix k l :: int |
20178 | 96 |
from monoid_comm_num_def show "k \<otimes> l = l \<otimes> k" by simp |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
97 |
qed |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
98 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
99 |
definition (in monoid) |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
100 |
units :: "'a set" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
101 |
units_def: "units = { y. \<exists>x. x \<^loc>\<otimes> y = \<^loc>\<one> \<and> y \<^loc>\<otimes> x = \<^loc>\<one> }" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
102 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
103 |
lemma (in monoid) inv_obtain: |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
104 |
assumes ass: "x \<in> units" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
105 |
obtains y where "y \<^loc>\<otimes> x = \<^loc>\<one>" and "x \<^loc>\<otimes> y = \<^loc>\<one>" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
106 |
proof - |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
107 |
from ass units_def obtain y |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
108 |
where "y \<^loc>\<otimes> x = \<^loc>\<one>" and "x \<^loc>\<otimes> y = \<^loc>\<one>" by auto |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
109 |
thus ?thesis .. |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
110 |
qed |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
111 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
112 |
lemma (in monoid) inv_unique: |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
113 |
assumes eq: "y \<^loc>\<otimes> x = \<^loc>\<one>" "x \<^loc>\<otimes> y' = \<^loc>\<one>" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
114 |
shows "y = y'" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
115 |
proof - |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
116 |
from eq neutr have "y = y \<^loc>\<otimes> (x \<^loc>\<otimes> y')" by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
117 |
also with assoc have "... = (y \<^loc>\<otimes> x) \<^loc>\<otimes> y'" by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
118 |
also with eq neutl have "... = y'" by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
119 |
finally show ?thesis . |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
120 |
qed |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
121 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
122 |
lemma (in monoid) units_inv_comm: |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
123 |
assumes inv: "x \<^loc>\<otimes> y = \<^loc>\<one>" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
124 |
and G: "x \<in> units" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
125 |
shows "y \<^loc>\<otimes> x = \<^loc>\<one>" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
126 |
proof - |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
127 |
from G inv_obtain obtain z |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
128 |
where z_choice: "z \<^loc>\<otimes> x = \<^loc>\<one>" by blast |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
129 |
from inv neutl neutr have "x \<^loc>\<otimes> y \<^loc>\<otimes> x = x \<^loc>\<otimes> \<^loc>\<one>" by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
130 |
with assoc have "z \<^loc>\<otimes> x \<^loc>\<otimes> y \<^loc>\<otimes> x = z \<^loc>\<otimes> x \<^loc>\<otimes> \<^loc>\<one>" by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
131 |
with neutl z_choice show ?thesis by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
132 |
qed |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
133 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
134 |
consts |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
135 |
reduce :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
136 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
137 |
primrec |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
138 |
"reduce f g 0 x = g" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
139 |
"reduce f g (Suc n) x = f x (reduce f g n x)" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
140 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
141 |
definition (in monoid) |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
142 |
npow :: "nat \<Rightarrow> 'a \<Rightarrow> 'a" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
143 |
npow_def_prim: "npow n x = reduce (op \<^loc>\<otimes>) \<^loc>\<one> n x" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
144 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
145 |
abbreviation (in monoid) |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
146 |
abbrev_npow :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infix "\<^loc>\<up>" 75) |
20178 | 147 |
"x \<^loc>\<up> n \<equiv> npow n x" |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
148 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
149 |
lemma (in monoid) npow_def: |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
150 |
"x \<^loc>\<up> 0 = \<^loc>\<one>" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
151 |
"x \<^loc>\<up> Suc n = x \<^loc>\<otimes> x \<^loc>\<up> n" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
152 |
using npow_def_prim by simp_all |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
153 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
154 |
lemma (in monoid) nat_pow_one: |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
155 |
"\<^loc>\<one> \<^loc>\<up> n = \<^loc>\<one>" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
156 |
using npow_def neutl by (induct n) simp_all |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
157 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
158 |
lemma (in monoid) nat_pow_mult: |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
159 |
"npow n x \<^loc>\<otimes> npow m x = npow (n + m) x" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
160 |
proof (induct n) |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
161 |
case 0 with neutl npow_def show ?case by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
162 |
next |
19933 | 163 |
case (Suc n) with Suc.hyps assoc npow_def show ?case by simp |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
164 |
qed |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
165 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
166 |
lemma (in monoid) nat_pow_pow: |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
167 |
"npow n (npow m x) = npow (n * m) x" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
168 |
using npow_def nat_pow_mult by (induct n) simp_all |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
169 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
170 |
class group = monoidl + |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
171 |
fixes inv :: "'a \<Rightarrow> 'a" ("\<^loc>\<div> _" [81] 80) |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
172 |
assumes invl: "\<^loc>\<div> x \<^loc>\<otimes> x = \<^loc>\<one>" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
173 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
174 |
class group_comm = group + monoid_comm |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
175 |
|
20178 | 176 |
instance group_comm_int_def: int :: group_comm |
177 |
"\<div> k \<equiv> - (k\<Colon>int)" |
|
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
178 |
proof |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
179 |
fix k :: int |
20178 | 180 |
from group_comm_int_def show "\<div> k \<otimes> k = \<one>" by simp |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
181 |
qed |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
182 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
183 |
lemma (in group) cancel: |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
184 |
"(x \<^loc>\<otimes> y = x \<^loc>\<otimes> z) = (y = z)" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
185 |
proof |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
186 |
fix x y z :: 'a |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
187 |
assume eq: "x \<^loc>\<otimes> y = x \<^loc>\<otimes> z" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
188 |
hence "\<^loc>\<div> x \<^loc>\<otimes> (x \<^loc>\<otimes> y) = \<^loc>\<div> x \<^loc>\<otimes> (x \<^loc>\<otimes> z)" by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
189 |
with assoc have "\<^loc>\<div> x \<^loc>\<otimes> x \<^loc>\<otimes> y = \<^loc>\<div> x \<^loc>\<otimes> x \<^loc>\<otimes> z" by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
190 |
with neutl invl show "y = z" by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
191 |
next |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
192 |
fix x y z :: 'a |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
193 |
assume eq: "y = z" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
194 |
thus "x \<^loc>\<otimes> y = x \<^loc>\<otimes> z" by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
195 |
qed |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
196 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
197 |
lemma (in group) neutr: |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
198 |
"x \<^loc>\<otimes> \<^loc>\<one> = x" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
199 |
proof - |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
200 |
from invl have "\<^loc>\<div> x \<^loc>\<otimes> x = \<^loc>\<one>" by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
201 |
with assoc [symmetric] neutl invl have "\<^loc>\<div> x \<^loc>\<otimes> (x \<^loc>\<otimes> \<^loc>\<one>) = \<^loc>\<div> x \<^loc>\<otimes> x" by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
202 |
with cancel show ?thesis by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
203 |
qed |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
204 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
205 |
lemma (in group) invr: |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
206 |
"x \<^loc>\<otimes> \<^loc>\<div> x = \<^loc>\<one>" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
207 |
proof - |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
208 |
from neutl invl have "\<^loc>\<div> x \<^loc>\<otimes> x \<^loc>\<otimes> \<^loc>\<div> x = \<^loc>\<div> x" by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
209 |
with neutr have "\<^loc>\<div> x \<^loc>\<otimes> x \<^loc>\<otimes> \<^loc>\<div> x = \<^loc>\<div> x \<^loc>\<otimes> \<^loc>\<one> " by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
210 |
with assoc have "\<^loc>\<div> x \<^loc>\<otimes> (x \<^loc>\<otimes> \<^loc>\<div> x) = \<^loc>\<div> x \<^loc>\<otimes> \<^loc>\<one> " by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
211 |
with cancel show ?thesis .. |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
212 |
qed |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
213 |
|
20383 | 214 |
instance group < monoid |
19928 | 215 |
proof - |
20383 | 216 |
fix x |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
217 |
from neutr show "x \<^loc>\<otimes> \<^loc>\<one> = x" . |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
218 |
qed |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
219 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
220 |
lemma (in group) all_inv [intro]: |
20178 | 221 |
"(x\<Colon>'a) \<in> monoid.units (op \<^loc>\<otimes>) \<^loc>\<one>" |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
222 |
unfolding units_def |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
223 |
proof - |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
224 |
fix x :: "'a" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
225 |
from invl invr have "\<^loc>\<div> x \<^loc>\<otimes> x = \<^loc>\<one>" and "x \<^loc>\<otimes> \<^loc>\<div> x = \<^loc>\<one>" . |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
226 |
then obtain y where "y \<^loc>\<otimes> x = \<^loc>\<one>" and "x \<^loc>\<otimes> y = \<^loc>\<one>" .. |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
227 |
hence "\<exists>y\<Colon>'a. y \<^loc>\<otimes> x = \<^loc>\<one> \<and> x \<^loc>\<otimes> y = \<^loc>\<one>" by blast |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
228 |
thus "x \<in> {y\<Colon>'a. \<exists>x\<Colon>'a. x \<^loc>\<otimes> y = \<^loc>\<one> \<and> y \<^loc>\<otimes> x = \<^loc>\<one>}" by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
229 |
qed |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
230 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
231 |
lemma (in group) cancer: |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
232 |
"(y \<^loc>\<otimes> x = z \<^loc>\<otimes> x) = (y = z)" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
233 |
proof |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
234 |
assume eq: "y \<^loc>\<otimes> x = z \<^loc>\<otimes> x" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
235 |
with assoc [symmetric] have "y \<^loc>\<otimes> (x \<^loc>\<otimes> \<^loc>\<div> x) = z \<^loc>\<otimes> (x \<^loc>\<otimes> \<^loc>\<div> x)" by (simp del: invr) |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
236 |
with invr neutr show "y = z" by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
237 |
next |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
238 |
assume eq: "y = z" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
239 |
thus "y \<^loc>\<otimes> x = z \<^loc>\<otimes> x" by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
240 |
qed |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
241 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
242 |
lemma (in group) inv_one: |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
243 |
"\<^loc>\<div> \<^loc>\<one> = \<^loc>\<one>" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
244 |
proof - |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
245 |
from neutl have "\<^loc>\<div> \<^loc>\<one> = \<^loc>\<one> \<^loc>\<otimes> (\<^loc>\<div> \<^loc>\<one>)" .. |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
246 |
moreover from invr have "... = \<^loc>\<one>" by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
247 |
finally show ?thesis . |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
248 |
qed |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
249 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
250 |
lemma (in group) inv_inv: |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
251 |
"\<^loc>\<div> (\<^loc>\<div> x) = x" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
252 |
proof - |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
253 |
from invl invr neutr |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
254 |
have "\<^loc>\<div> (\<^loc>\<div> x) \<^loc>\<otimes> \<^loc>\<div> x \<^loc>\<otimes> x = x \<^loc>\<otimes> \<^loc>\<div> x \<^loc>\<otimes> x" by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
255 |
with assoc [symmetric] |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
256 |
have "\<^loc>\<div> (\<^loc>\<div> x) \<^loc>\<otimes> (\<^loc>\<div> x \<^loc>\<otimes> x) = x \<^loc>\<otimes> (\<^loc>\<div> x \<^loc>\<otimes> x)" by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
257 |
with invl neutr show ?thesis by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
258 |
qed |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
259 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
260 |
lemma (in group) inv_mult_group: |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
261 |
"\<^loc>\<div> (x \<^loc>\<otimes> y) = \<^loc>\<div> y \<^loc>\<otimes> \<^loc>\<div> x" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
262 |
proof - |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
263 |
from invl have "\<^loc>\<div> (x \<^loc>\<otimes> y) \<^loc>\<otimes> (x \<^loc>\<otimes> y) = \<^loc>\<one>" by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
264 |
with assoc have "\<^loc>\<div> (x \<^loc>\<otimes> y) \<^loc>\<otimes> x \<^loc>\<otimes> y = \<^loc>\<one>" by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
265 |
with neutl have "\<^loc>\<div> (x \<^loc>\<otimes> y) \<^loc>\<otimes> x \<^loc>\<otimes> y \<^loc>\<otimes> \<^loc>\<div> y \<^loc>\<otimes> \<^loc>\<div> x = \<^loc>\<div> y \<^loc>\<otimes> \<^loc>\<div> x" by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
266 |
with assoc have "\<^loc>\<div> (x \<^loc>\<otimes> y) \<^loc>\<otimes> (x \<^loc>\<otimes> (y \<^loc>\<otimes> \<^loc>\<div> y) \<^loc>\<otimes> \<^loc>\<div> x) = \<^loc>\<div> y \<^loc>\<otimes> \<^loc>\<div> x" by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
267 |
with invr neutr show ?thesis by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
268 |
qed |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
269 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
270 |
lemma (in group) inv_comm: |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
271 |
"x \<^loc>\<otimes> \<^loc>\<div> x = \<^loc>\<div> x \<^loc>\<otimes> x" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
272 |
using invr invl by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
273 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
274 |
definition (in group) |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
275 |
pow :: "int \<Rightarrow> 'a \<Rightarrow> 'a" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
276 |
pow_def: "pow k x = (if k < 0 then \<^loc>\<div> (monoid.npow (op \<^loc>\<otimes>) \<^loc>\<one> (nat (-k)) x) |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
277 |
else (monoid.npow (op \<^loc>\<otimes>) \<^loc>\<one> (nat k) x))" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
278 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
279 |
abbreviation (in group) |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
280 |
abbrev_pow :: "'a \<Rightarrow> int \<Rightarrow> 'a" (infix "\<^loc>\<up>" 75) |
19928 | 281 |
"x \<^loc>\<up> k \<equiv> pow k x" |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
282 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
283 |
lemma (in group) int_pow_zero: |
20178 | 284 |
"x \<^loc>\<up> (0\<Colon>int) = \<^loc>\<one>" |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
285 |
using npow_def pow_def by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
286 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
287 |
lemma (in group) int_pow_one: |
20178 | 288 |
"\<^loc>\<one> \<^loc>\<up> (k\<Colon>int) = \<^loc>\<one>" |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
289 |
using pow_def nat_pow_one inv_one by simp |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
290 |
|
20597 | 291 |
instance semigroup_prod_def: * :: (semigroup, semigroup) semigroup |
20178 | 292 |
mult_prod_def: "x \<otimes> y \<equiv> let (x1, x2) = x; (y1, y2) = y in |
19958 | 293 |
(x1 \<otimes> y1, x2 \<otimes> y2)" |
20427 | 294 |
by default (simp_all add: split_paired_all semigroup_prod_def assoc) |
295 |
||
20597 | 296 |
instance monoidl_prod_def: * :: (monoidl, monoidl) monoidl |
20427 | 297 |
one_prod_def: "\<one> \<equiv> (\<one>, \<one>)" |
298 |
by default (simp_all add: split_paired_all monoidl_prod_def neutl) |
|
299 |
||
20597 | 300 |
instance monoid_prod_def: * :: (monoid, monoid) monoid |
20427 | 301 |
by default (simp_all add: split_paired_all monoid_prod_def neutr) |
302 |
||
20597 | 303 |
instance monoid_comm_prod_def: * :: (monoid_comm, monoid_comm) monoid_comm |
20427 | 304 |
by default (simp_all add: split_paired_all monoidl_prod_def comm) |
305 |
||
20597 | 306 |
instance group_prod_def: * :: (group, group) group |
20427 | 307 |
inv_prod_def: "\<div> x \<equiv> let (x1, x2) = x in (\<div> x1, \<div> x2)" |
308 |
by default (simp_all add: split_paired_all group_prod_def invl) |
|
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
309 |
|
20597 | 310 |
instance group_comm_prod_def: * :: (group_comm, group_comm) group_comm |
20427 | 311 |
by default (simp_all add: split_paired_all group_prod_def comm) |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
312 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
313 |
definition |
20383 | 314 |
"X a b c = (a \<otimes> \<one> \<otimes> b, a \<otimes> \<one> \<otimes> b, [a, b] \<otimes> \<one> \<otimes> [a, b, c])" |
315 |
"Y a b c = (a, \<div> a) \<otimes> \<one> \<otimes> \<div> (b, \<div> c)" |
|
316 |
||
317 |
definition |
|
318 |
"x1 = X (1::nat) 2 3" |
|
319 |
"x2 = X (1::int) 2 3" |
|
320 |
"y2 = Y (1::int) 2 3" |
|
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
321 |
|
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20427
diff
changeset
|
322 |
code_gen "op \<otimes>" \<one> inv |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20427
diff
changeset
|
323 |
code_gen X Y (SML) (Haskell) |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20427
diff
changeset
|
324 |
code_gen x1 x2 y2 (SML) (Haskell) |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
325 |
|
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20427
diff
changeset
|
326 |
code_gen (SML -) |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
327 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
328 |
end |