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 |
|
6 definition |
|
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 |
|
16 |
5 |
17 locale QUOT_TYPE = |
6 locale QUOT_TYPE = |
18 fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
7 fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
19 and Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b" |
8 and Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b" |
20 and Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)" |
9 and Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)" |
153 end |
142 end |
154 |
143 |
155 |
144 |
156 section {* type definition for the quotient type *} |
145 section {* type definition for the quotient type *} |
157 |
146 |
|
147 ML {* Toplevel.theory *} |
|
148 |
158 use "quotient.ML" |
149 use "quotient.ML" |
159 |
150 |
160 (* mapfuns for some standard types *) |
151 declare [[map list = (map, LIST_REL)]] |
161 setup {* |
152 declare [[map * = (prod_fun, prod_rel)]] |
162 maps_update @{type_name "list"} {mapfun = @{const_name "map"}, relfun = @{const_name "LIST_REL"}} #> |
153 declare [[map "fun" = (fun_map, FUN_REL)]] |
163 maps_update @{type_name "*"} {mapfun = @{const_name "prod_fun"}, relfun = @{const_name "prod_rel"}} #> |
154 |
164 maps_update @{type_name "fun"} {mapfun = @{const_name "fun_map"}, relfun = @{const_name "FUN_REL"}} |
155 ML {* maps_lookup @{theory} "List.list" *} |
165 *} |
156 ML {* maps_lookup @{theory} "*" *} |
|
157 ML {* maps_lookup @{theory} "fun" *} |
166 |
158 |
167 ML {* |
159 ML {* |
168 val no_vars = Thm.rule_attribute (fn context => fn th => |
160 val no_vars = Thm.rule_attribute (fn context => fn th => |
169 let |
161 let |
170 val ctxt = Variable.set_body false (Context.proof_of context); |
162 val ctxt = Variable.set_body false (Context.proof_of context); |
171 val ((_, [th']), _) = Variable.import true [th] ctxt; |
163 val ((_, [th']), _) = Variable.import true [th] ctxt; |
172 in th' end); |
164 in th' end); |
173 *} |
165 *} |
174 |
166 |
175 section {* lifting of constants *} |
167 section {* lifting of constants *} |
|
168 |
|
169 ML {* |
|
170 |
|
171 *} |
176 |
172 |
177 ML {* |
173 ML {* |
178 (* calculates the aggregate abs and rep functions for a given type; |
174 (* calculates the aggregate abs and rep functions for a given type; |
179 repF is for constants' arguments; absF is for constants; |
175 repF is for constants' arguments; absF is for constants; |
180 function types need to be treated specially, since repF and absF |
176 function types need to be treated specially, since repF and absF |