13 end; |
13 end; |
14 |
14 |
15 structure Quotient_Def: QUOTIENT_DEF = |
15 structure Quotient_Def: QUOTIENT_DEF = |
16 struct |
16 struct |
17 |
17 |
|
18 (* wrapper for define *) |
18 fun define name mx attr rhs lthy = |
19 fun define name mx attr rhs lthy = |
19 let |
20 let |
20 val ((rhs, (_ , thm)), lthy') = |
21 val ((rhs, (_ , thm)), lthy') = |
21 LocalTheory.define Thm.internalK ((name, mx), (attr, rhs)) lthy |
22 LocalTheory.define Thm.internalK ((name, mx), (attr, rhs)) lthy |
22 in |
23 in |
118 and diffs (T::Ts, U::Us) Ds = diffs (Ts, Us) (diff (T, U) Ds) |
119 and diffs (T::Ts, U::Us) Ds = diffs (Ts, Us) (diff (T, U) Ds) |
119 | diffs ([], []) Ds = Ds |
120 | diffs ([], []) Ds = Ds |
120 | diffs _ _ = error "Unequal length of type arguments" |
121 | diffs _ _ = error "Unequal length of type arguments" |
121 |
122 |
122 |
123 |
|
124 (* sanity check that the calculated quotient environment |
|
125 matches with the stored quotient environment. *) |
123 fun error_msg lthy (qty, rty) = |
126 fun error_msg lthy (qty, rty) = |
124 let |
127 let |
125 val qtystr = quote (Syntax.string_of_typ lthy qty) |
128 val qtystr = quote (Syntax.string_of_typ lthy qty) |
126 val rtystr = quote (Syntax.string_of_typ lthy rty) |
129 val rtystr = quote (Syntax.string_of_typ lthy rty) |
127 in |
130 in |
128 error (implode ["Quotient type ", qtystr, " does not match with ", rtystr]) |
131 error (implode ["Quotient type ", qtystr, " does not match with ", rtystr]) |
129 end |
132 end |
130 |
133 |
131 fun sanity_chk lthy qenv = |
134 fun sanity_chk lthy qenv = |
132 let |
135 let |
133 val qenv' = Quotient_Info.mk_qenv lthy |
136 val qenv' = Quotient_Info.mk_qenv lthy |
134 val thy = ProofContext.theory_of lthy |
137 val thy = ProofContext.theory_of lthy |
135 |
138 |
136 fun is_inst thy (qty, rty) (qty', rty') = |
139 fun is_inst thy (qty, rty) (qty', rty') = |
137 if Sign.typ_instance thy (qty, qty') |
140 if Sign.typ_instance thy (qty, qty') |
138 then let |
141 then let |
139 val inst = Sign.typ_match thy (qty', qty) Vartab.empty |
142 val inst = Sign.typ_match thy (qty', qty) Vartab.empty |
140 in |
143 in |
141 rty = Envir.subst_type inst rty' |
144 rty = Envir.subst_type inst rty' |
142 end |
145 end |
143 else false |
146 else false |
144 |
147 |
145 fun chk_inst (qty, rty) = |
148 fun chk_inst (qty, rty) = |
146 if exists (is_inst thy (qty, rty)) qenv' then true |
149 if exists (is_inst thy (qty, rty)) qenv' then true |
147 else error_msg lthy (qty, rty) |
150 else error_msg lthy (qty, rty) |
148 in |
151 in |
149 forall chk_inst qenv |
152 forall chk_inst qenv |
150 end |
153 end |
151 |
154 |
152 |
155 |
160 in |
163 in |
161 sanity_chk lthy qenv; |
164 sanity_chk lthy qenv; |
162 make_def bind rhs qty mx attr qenv lthy |
165 make_def bind rhs qty mx attr qenv lthy |
163 end |
166 end |
164 |
167 |
165 |
|
166 val quotdef_parser = |
|
167 (OuterParse.binding -- |
|
168 (OuterParse.$$$ "::" |-- OuterParse.!!! (OuterParse.typ -- |
|
169 OuterParse.opt_mixfix' --| OuterParse.where_)) >> OuterParse.triple2) -- |
|
170 (SpecParse.opt_thm_name ":" -- OuterParse.prop) |
|
171 |
|
172 fun quotdef_cmd ((bind, qtystr, mx), (attr, propstr)) lthy = |
168 fun quotdef_cmd ((bind, qtystr, mx), (attr, propstr)) lthy = |
173 let |
169 let |
174 val qty = (Syntax.check_typ lthy o Syntax.parse_typ lthy) qtystr |
170 val qty = (Syntax.check_typ lthy o Syntax.parse_typ lthy) qtystr |
175 val prop = (Syntax.check_prop lthy o Syntax.parse_prop lthy) propstr |
171 val prop = (Syntax.check_prop lthy o Syntax.parse_prop lthy) propstr |
176 in |
172 in |
177 quotdef ((bind, qty, mx), (attr, prop)) lthy |> snd |
173 quotdef ((bind, qty, mx), (attr, prop)) lthy |> snd |
178 end |
174 end |
179 |
175 |
|
176 |
|
177 val quotdef_parser = |
|
178 (OuterParse.binding -- |
|
179 (OuterParse.$$$ "::" |-- OuterParse.!!! (OuterParse.typ -- |
|
180 OuterParse.opt_mixfix' --| OuterParse.where_)) >> OuterParse.triple2) -- |
|
181 (SpecParse.opt_thm_name ":" -- OuterParse.prop) |
|
182 |
180 val _ = OuterSyntax.local_theory "quotient_def" "lifted definition of constants" |
183 val _ = OuterSyntax.local_theory "quotient_def" "lifted definition of constants" |
181 OuterKeyword.thy_decl (quotdef_parser >> quotdef_cmd) |
184 OuterKeyword.thy_decl (quotdef_parser >> quotdef_cmd) |
182 |
185 |
183 end; (* structure *) |
186 end; (* structure *) |
184 |
187 |