equal
deleted
inserted
replaced
1 theory QuotMain |
1 theory QuotMain |
2 imports QuotScript QuotList Prove |
2 imports QuotScript QuotList Prove |
3 uses ("quotient.ML") |
3 uses ("quotient.ML") |
4 begin |
4 begin |
5 |
5 |
6 ML {* Pretty.writeln *} |
6 definition |
7 ML {* LocalTheory.theory_result *} |
7 EQ_TRUE |
|
8 where |
|
9 "EQ_TRUE X \<equiv> (X = True)" |
|
10 |
|
11 lemma test: "EQ_TRUE ?X" |
|
12 unfolding EQ_TRUE_def |
|
13 by (rule refl) |
|
14 |
|
15 thm test |
8 |
16 |
9 locale QUOT_TYPE = |
17 locale QUOT_TYPE = |
10 fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
18 fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
11 and Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b" |
19 and Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b" |
12 and Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)" |
20 and Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)" |
148 section {* type definition for the quotient type *} |
156 section {* type definition for the quotient type *} |
149 |
157 |
150 use "quotient.ML" |
158 use "quotient.ML" |
151 |
159 |
152 (* mapfuns for some standard types *) |
160 (* mapfuns for some standard types *) |
153 setup {* |
161 |
154 maps_update @{type_name "list"} {mapfun = @{const_name "map"}, relfun = @{const_name "LIST_REL"}} #> |
162 ML {* quotdata_lookup @{theory} *} |
155 maps_update @{type_name "*"} {mapfun = @{const_name "prod_fun"}, relfun = @{const_name "prod_rel"}} #> |
163 setup {* quotdata_update_thy (@{typ nat}, @{typ bool}, @{term "True"})*} |
156 maps_update @{type_name "fun"} {mapfun = @{const_name "fun_map"}, relfun = @{const_name "FUN_REL"}} |
164 ML {* quotdata_lookup @{theory} *} |
157 *} |
165 |
158 |
166 ML {* print_quotdata @{context} *} |
159 |
167 |
160 ML {* maps_lookup @{theory} @{type_name list} *} |
168 ML {* maps_lookup @{theory} @{type_name list} *} |
161 |
169 |
162 ML {* |
170 ML {* |
163 val no_vars = Thm.rule_attribute (fn context => fn th => |
171 val no_vars = Thm.rule_attribute (fn context => fn th => |
206 val ftys = map (op -->) tys |
214 val ftys = map (op -->) tys |
207 in |
215 in |
208 (list_comb (Const (@{const_name "fun_map"}, ftys ---> oty --> nty), fs), (oty, nty)) |
216 (list_comb (Const (@{const_name "fun_map"}, ftys ---> oty --> nty), fs), (oty, nty)) |
209 end |
217 end |
210 |
218 |
211 fun get_const absF = (Const ("FSet.ABS_" ^ qty_name, rty --> qty), (rty, qty)) |
219 val thy = ProofContext.theory_of lthy |
212 | get_const repF = (Const ("FSet.REP_" ^ qty_name, qty --> rty), (qty, rty)) |
220 |
|
221 fun get_const absF = (Const (Sign.full_bname thy ("ABS_" ^ qty_name), rty --> qty), (rty, qty)) |
|
222 | get_const repF = (Const (Sign.full_bname thy ("REP_" ^ qty_name), qty --> rty), (qty, rty)) |
213 |
223 |
214 fun mk_identity ty = Abs ("", ty, Bound 0) |
224 fun mk_identity ty = Abs ("", ty, Bound 0) |
215 |
225 |
216 in |
226 in |
217 if ty = qty |
227 if ty = qty |