163
|
1 |
theory QuotTest
|
|
2 |
imports QuotMain
|
|
3 |
begin
|
|
4 |
|
254
|
5 |
|
163
|
6 |
section {* various tests for quotient types*}
|
|
7 |
datatype trm =
|
|
8 |
var "nat"
|
|
9 |
| app "trm" "trm"
|
|
10 |
| lam "nat" "trm"
|
|
11 |
|
|
12 |
axiomatization
|
177
bdfe4388955d
changed encoding from utf8 to ISO8 (needed to work with xemacs)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
13 |
RR :: "trm \<Rightarrow> trm \<Rightarrow> bool"
|
163
|
14 |
where
|
|
15 |
r_eq: "EQUIV RR"
|
|
16 |
|
185
|
17 |
print_quotients
|
163
|
18 |
|
|
19 |
quotient qtrm = trm / "RR"
|
|
20 |
apply(rule r_eq)
|
|
21 |
done
|
|
22 |
|
185
|
23 |
print_quotients
|
163
|
24 |
|
|
25 |
typ qtrm
|
|
26 |
term Rep_qtrm
|
|
27 |
term REP_qtrm
|
|
28 |
term Abs_qtrm
|
|
29 |
term ABS_qtrm
|
|
30 |
thm QUOT_TYPE_qtrm
|
|
31 |
thm QUOTIENT_qtrm
|
|
32 |
thm REP_qtrm_def
|
|
33 |
|
|
34 |
(* Test interpretation *)
|
|
35 |
thm QUOT_TYPE_I_qtrm.thm11
|
|
36 |
thm QUOT_TYPE.thm11
|
|
37 |
|
|
38 |
print_theorems
|
|
39 |
|
|
40 |
thm Rep_qtrm
|
|
41 |
|
|
42 |
text {* another test *}
|
|
43 |
datatype 'a trm' =
|
|
44 |
var' "'a"
|
|
45 |
| app' "'a trm'" "'a trm'"
|
|
46 |
| lam' "'a" "'a trm'"
|
|
47 |
|
177
bdfe4388955d
changed encoding from utf8 to ISO8 (needed to work with xemacs)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
48 |
consts R' :: "'a trm' \<Rightarrow> 'a trm' \<Rightarrow> bool"
|
163
|
49 |
axioms r_eq': "EQUIV R'"
|
|
50 |
|
|
51 |
quotient qtrm' = "'a trm'" / "R'"
|
|
52 |
apply(rule r_eq')
|
|
53 |
done
|
|
54 |
|
185
|
55 |
print_quotients
|
163
|
56 |
print_theorems
|
|
57 |
|
|
58 |
term ABS_qtrm'
|
|
59 |
term REP_qtrm'
|
|
60 |
thm QUOT_TYPE_qtrm'
|
|
61 |
thm QUOTIENT_qtrm'
|
|
62 |
thm Rep_qtrm'
|
|
63 |
|
|
64 |
|
|
65 |
text {* a test with lists of terms *}
|
|
66 |
datatype t =
|
|
67 |
vr "string"
|
|
68 |
| ap "t list"
|
|
69 |
| lm "string" "t"
|
|
70 |
|
177
bdfe4388955d
changed encoding from utf8 to ISO8 (needed to work with xemacs)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
71 |
consts Rt :: "t \<Rightarrow> t \<Rightarrow> bool"
|
163
|
72 |
axioms t_eq: "EQUIV Rt"
|
|
73 |
|
|
74 |
quotient qt = "t" / "Rt"
|
|
75 |
by (rule t_eq)
|
|
76 |
|
185
|
77 |
print_quotients
|
|
78 |
|
|
79 |
ML {*
|
230
|
80 |
get_fun repF [(@{typ qt}, @{typ qt})] @{context} @{typ "((((qt \<Rightarrow> qt) \<Rightarrow> qt) \<Rightarrow> qt) list) * nat"}
|
163
|
81 |
|> Syntax.string_of_term @{context}
|
|
82 |
|> writeln
|
|
83 |
*}
|
|
84 |
|
|
85 |
ML {*
|
230
|
86 |
get_fun absF [(@{typ qt}, @{typ t})] @{context} @{typ "qt * nat"}
|
163
|
87 |
|> Syntax.string_of_term @{context}
|
|
88 |
|> writeln
|
|
89 |
*}
|
|
90 |
|
|
91 |
ML {*
|
230
|
92 |
get_fun absF [(@{typ qt}, @{typ t})] @{context} @{typ "(qt \<Rightarrow> qt) \<Rightarrow> qt"}
|
163
|
93 |
|> Syntax.pretty_term @{context}
|
|
94 |
|> Pretty.string_of
|
|
95 |
|> writeln
|
|
96 |
*}
|
|
97 |
|
|
98 |
(* A test whether get_fun works properly
|
177
bdfe4388955d
changed encoding from utf8 to ISO8 (needed to work with xemacs)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
99 |
consts bla :: "(t \<Rightarrow> t) \<Rightarrow> t"
|
163
|
100 |
local_setup {*
|
305
|
101 |
make_const_def @{binding bla'} @{term "bla"} NoSyn @{typ "t"} @{typ "qt"} lthy |> snd
|
163
|
102 |
*}
|
|
103 |
*)
|
|
104 |
|
284
|
105 |
consts Rl :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
|
|
106 |
axioms Rl_eq: "EQUIV Rl"
|
|
107 |
|
|
108 |
quotient ql = "'a list" / "Rl"
|
|
109 |
by (rule Rl_eq)
|
|
110 |
|
|
111 |
ML {* val al = snd (dest_Free (term_of @{cpat "f :: ?'a list"})) *}
|
|
112 |
ML {* val aq = snd (dest_Free (term_of @{cpat "f :: ?'a ql"})) *}
|
285
|
113 |
ML {* val ttt = snd (dest_Free (term_of @{cpat "f :: ?'a ql \<Rightarrow> ?'a ql"})) *}
|
284
|
114 |
|
|
115 |
ML {*
|
285
|
116 |
fst (get_fun absF [(aq, al)] @{context} ttt)
|
|
117 |
|> cterm_of @{theory}
|
284
|
118 |
*}
|
|
119 |
|
285
|
120 |
ML {* val ttt2 = snd (dest_Free (term_of @{cpat "f :: nat ql \<Rightarrow> bool ql \<Rightarrow> 'a ql"})) *}
|
284
|
121 |
|
|
122 |
ML {*
|
285
|
123 |
fst (get_fun absF [(aq, al), (@{typ "nat ql"}, @{typ "nat list"}), (@{typ "bool ql"}, @{typ "bool list"})] @{context} ttt2)
|
|
124 |
|> cterm_of @{theory}
|
284
|
125 |
*}
|
|
126 |
|
230
|
127 |
quotient_def (for qt)
|
|
128 |
VR ::"string \<Rightarrow> qt"
|
|
129 |
where
|
|
130 |
"VR \<equiv> vr"
|
|
131 |
|
|
132 |
quotient_def (for qt)
|
|
133 |
AP ::"qt list \<Rightarrow> qt"
|
|
134 |
where
|
|
135 |
"AP \<equiv> ap"
|
|
136 |
|
|
137 |
quotient_def (for qt)
|
|
138 |
LM ::"string \<Rightarrow> qt \<Rightarrow> qt"
|
|
139 |
where
|
|
140 |
"LM \<equiv> lm"
|
163
|
141 |
|
|
142 |
term vr
|
|
143 |
term ap
|
|
144 |
term lm
|
|
145 |
thm VR_def AP_def LM_def
|
|
146 |
term LM
|
|
147 |
term VR
|
|
148 |
term AP
|
|
149 |
|
|
150 |
text {* a test with functions *}
|
|
151 |
datatype 'a t' =
|
|
152 |
vr' "string"
|
|
153 |
| ap' "('a t') * ('a t')"
|
177
bdfe4388955d
changed encoding from utf8 to ISO8 (needed to work with xemacs)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
154 |
| lm' "'a" "string \<Rightarrow> ('a t')"
|
163
|
155 |
|
177
bdfe4388955d
changed encoding from utf8 to ISO8 (needed to work with xemacs)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
156 |
consts Rt' :: "('a t') \<Rightarrow> ('a t') \<Rightarrow> bool"
|
163
|
157 |
axioms t_eq': "EQUIV Rt'"
|
|
158 |
|
|
159 |
quotient qt' = "'a t'" / "Rt'"
|
|
160 |
apply(rule t_eq')
|
|
161 |
done
|
|
162 |
|
185
|
163 |
print_quotients
|
163
|
164 |
print_theorems
|
|
165 |
|
230
|
166 |
|
|
167 |
quotient_def (for "'a qt'")
|
|
168 |
VR' ::"string \<Rightarrow> 'a qt"
|
|
169 |
where
|
|
170 |
"VR' \<equiv> vr'"
|
|
171 |
|
|
172 |
quotient_def (for "'a qt'")
|
|
173 |
AP' ::"('a qt') * ('a qt') \<Rightarrow> 'a qt"
|
|
174 |
where
|
|
175 |
"AP' \<equiv> ap'"
|
|
176 |
|
|
177 |
quotient_def (for "'a qt'")
|
|
178 |
LM' ::"'a \<Rightarrow> string \<Rightarrow> 'a qt'"
|
|
179 |
where
|
|
180 |
"LM' \<equiv> lm'"
|
163
|
181 |
|
|
182 |
term vr'
|
|
183 |
term ap'
|
|
184 |
term ap'
|
|
185 |
thm VR'_def AP'_def LM'_def
|
|
186 |
term LM'
|
|
187 |
term VR'
|
|
188 |
term AP'
|
|
189 |
|
|
190 |
text {* Tests of regularise *}
|
|
191 |
ML {*
|
177
bdfe4388955d
changed encoding from utf8 to ISO8 (needed to work with xemacs)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
192 |
cterm_of @{theory} (regularise @{term "\<lambda>x :: int. x"} @{typ "trm"} @{term "RR"} @{context});
|
bdfe4388955d
changed encoding from utf8 to ISO8 (needed to work with xemacs)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
193 |
cterm_of @{theory} (regularise @{term "\<lambda>x :: trm. x"} @{typ "trm"} @{term "RR"} @{context});
|
bdfe4388955d
changed encoding from utf8 to ISO8 (needed to work with xemacs)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
194 |
cterm_of @{theory} (regularise @{term "\<forall>x :: trm. P x"} @{typ "trm"} @{term "RR"} @{context});
|
bdfe4388955d
changed encoding from utf8 to ISO8 (needed to work with xemacs)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
195 |
cterm_of @{theory} (regularise @{term "\<exists>x :: trm. P x"} @{typ "trm"} @{term "RR"} @{context});
|
bdfe4388955d
changed encoding from utf8 to ISO8 (needed to work with xemacs)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
196 |
cterm_of @{theory} (regularise @{term "All (P :: trm \<Rightarrow> bool)"} @{typ "trm"} @{term "RR"} @{context});
|
163
|
197 |
*}
|
|
198 |
|
|
199 |
ML {*
|
177
bdfe4388955d
changed encoding from utf8 to ISO8 (needed to work with xemacs)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
200 |
cterm_of @{theory} (regularise @{term "\<exists>(y::trm). P (\<lambda>(x::trm). y)"} @{typ "trm"}
|
163
|
201 |
@{term "RR"} @{context});
|
177
bdfe4388955d
changed encoding from utf8 to ISO8 (needed to work with xemacs)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
202 |
cterm_of @{theory} (my_reg @{term "RR"} @{term "\<exists>(y::trm). P (\<lambda>(x::trm). y)"})
|
163
|
203 |
*}
|
|
204 |
|
|
205 |
ML {*
|
177
bdfe4388955d
changed encoding from utf8 to ISO8 (needed to work with xemacs)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
206 |
cterm_of @{theory} (regularise @{term "\<lambda>x::trm. x"} @{typ "trm"} @{term "RR"} @{context});
|
bdfe4388955d
changed encoding from utf8 to ISO8 (needed to work with xemacs)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
207 |
cterm_of @{theory} (my_reg @{term "RR"} @{term "\<lambda>x::trm. x"})
|
163
|
208 |
*}
|
|
209 |
|
|
210 |
ML {*
|
177
bdfe4388955d
changed encoding from utf8 to ISO8 (needed to work with xemacs)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
211 |
cterm_of @{theory} (regularise @{term "\<forall>(x::trm) (y::trm). P x y"} @{typ "trm"} @{term "RR"} @{context});
|
bdfe4388955d
changed encoding from utf8 to ISO8 (needed to work with xemacs)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
212 |
cterm_of @{theory} (my_reg @{term "RR"} @{term "\<forall>(x::trm) (y::trm). P x y"})
|
163
|
213 |
*}
|
|
214 |
|
|
215 |
ML {*
|
177
bdfe4388955d
changed encoding from utf8 to ISO8 (needed to work with xemacs)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
216 |
cterm_of @{theory} (regularise @{term "\<forall>x::trm. P x"} @{typ "trm"} @{term "RR"} @{context});
|
bdfe4388955d
changed encoding from utf8 to ISO8 (needed to work with xemacs)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
217 |
cterm_of @{theory} (my_reg @{term "RR"} @{term "\<forall>x::trm. P x"})
|
163
|
218 |
*}
|
|
219 |
|
|
220 |
ML {*
|
177
bdfe4388955d
changed encoding from utf8 to ISO8 (needed to work with xemacs)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
221 |
cterm_of @{theory} (regularise @{term "\<exists>x::trm. P x"} @{typ "trm"} @{term "RR"} @{context});
|
bdfe4388955d
changed encoding from utf8 to ISO8 (needed to work with xemacs)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
222 |
cterm_of @{theory} (my_reg @{term "RR"} @{term "\<exists>x::trm. P x"})
|
163
|
223 |
*}
|
|
224 |
|
|
225 |
(* my version is not eta-expanded, but that should be OK *)
|
|
226 |
ML {*
|
177
bdfe4388955d
changed encoding from utf8 to ISO8 (needed to work with xemacs)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
227 |
cterm_of @{theory} (regularise @{term "All (P::trm \<Rightarrow> bool)"} @{typ "trm"} @{term "RR"} @{context});
|
bdfe4388955d
changed encoding from utf8 to ISO8 (needed to work with xemacs)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
228 |
cterm_of @{theory} (my_reg @{term "RR"} @{term "All (P::trm \<Rightarrow> bool)"})
|
163
|
229 |
*}
|