1 signature QUOTIENT_TERM = |
1 signature QUOTIENT_TERM = |
2 sig |
2 sig |
3 exception LIFT_MATCH of string |
3 exception LIFT_MATCH of string |
4 |
4 |
5 datatype flag = absF | repF |
5 datatype flag = absF | repF |
6 val get_fun: flag -> Proof.context -> typ * typ -> term |
6 val get_fun: flag -> Proof.context -> (typ * typ) -> term |
7 |
7 |
8 val regularize_trm: Proof.context -> term -> term -> term |
8 val regularize_trm: Proof.context -> (term * term) -> term |
9 val inj_repabs_trm: Proof.context -> (term * term) -> term |
9 val inj_repabs_trm: Proof.context -> (term * term) -> term |
10 end; |
10 end; |
11 |
11 |
12 structure Quotient_Term: QUOTIENT_TERM = |
12 structure Quotient_Term: QUOTIENT_TERM = |
13 struct |
13 struct |
154 |
154 |
155 (* - applies f to the subterm of an abstraction, *) |
155 (* - applies f to the subterm of an abstraction, *) |
156 (* otherwise to the given term, *) |
156 (* otherwise to the given term, *) |
157 (* - used by regularize, therefore abstracted *) |
157 (* - used by regularize, therefore abstracted *) |
158 (* variables do not have to be treated specially *) |
158 (* variables do not have to be treated specially *) |
159 fun apply_subt f trm1 trm2 = |
159 fun apply_subt f (trm1, trm2) = |
160 case (trm1, trm2) of |
160 case (trm1, trm2) of |
161 (Abs (x, T, t), Abs (_ , _, t')) => Abs (x, T, f t t') |
161 (Abs (x, T, t), Abs (_ , _, t')) => Abs (x, T, f (t, t')) |
162 | _ => f trm1 trm2 |
162 | _ => f (trm1, trm2) |
163 |
163 |
164 (* the major type of All and Ex quantifiers *) |
164 (* the major type of All and Ex quantifiers *) |
165 fun qnt_typ ty = domain_type (domain_type ty) |
165 fun qnt_typ ty = domain_type (domain_type ty) |
166 |
166 |
167 |
167 |
170 (* - the result still contains dummyTs *) |
170 (* - the result still contains dummyTs *) |
171 (* *) |
171 (* *) |
172 (* - for regularisation we do not need any *) |
172 (* - for regularisation we do not need any *) |
173 (* special treatment of bound variables *) |
173 (* special treatment of bound variables *) |
174 |
174 |
175 fun regularize_trm lthy rtrm qtrm = |
175 fun regularize_trm lthy (rtrm, qtrm) = |
176 case (rtrm, qtrm) of |
176 case (rtrm, qtrm) of |
177 (Abs (x, ty, t), Abs (_, ty', t')) => |
177 (Abs (x, ty, t), Abs (_, ty', t')) => |
178 let |
178 let |
179 val subtrm = Abs(x, ty, regularize_trm lthy t t') |
179 val subtrm = Abs(x, ty, regularize_trm lthy (t, t')) |
180 in |
180 in |
181 if ty = ty' then subtrm |
181 if ty = ty' then subtrm |
182 else mk_babs $ (mk_resp $ mk_resp_arg lthy (ty, ty')) $ subtrm |
182 else mk_babs $ (mk_resp $ mk_resp_arg lthy (ty, ty')) $ subtrm |
183 end |
183 end |
184 |
184 |
185 | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') => |
185 | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') => |
186 let |
186 let |
187 val subtrm = apply_subt (regularize_trm lthy) t t' |
187 val subtrm = apply_subt (regularize_trm lthy) (t, t') |
188 in |
188 in |
189 if ty = ty' then Const (@{const_name "All"}, ty) $ subtrm |
189 if ty = ty' then Const (@{const_name "All"}, ty) $ subtrm |
190 else mk_ball $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm |
190 else mk_ball $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm |
191 end |
191 end |
192 |
192 |
193 | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') => |
193 | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') => |
194 let |
194 let |
195 val subtrm = apply_subt (regularize_trm lthy) t t' |
195 val subtrm = apply_subt (regularize_trm lthy) (t, t') |
196 in |
196 in |
197 if ty = ty' then Const (@{const_name "Ex"}, ty) $ subtrm |
197 if ty = ty' then Const (@{const_name "Ex"}, ty) $ subtrm |
198 else mk_bex $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm |
198 else mk_bex $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm |
199 end |
199 end |
200 |
200 |
243 then rtrm else raise exc2 |
243 then rtrm else raise exc2 |
244 end |
244 end |
245 end |
245 end |
246 |
246 |
247 | (t1 $ t2, t1' $ t2') => |
247 | (t1 $ t2, t1' $ t2') => |
248 (regularize_trm lthy t1 t1') $ (regularize_trm lthy t2 t2') |
248 (regularize_trm lthy (t1, t1')) $ (regularize_trm lthy (t2, t2')) |
249 |
249 |
250 | (Bound i, Bound i') => |
250 | (Bound i, Bound i') => |
251 if i = i' then rtrm |
251 if i = i' then rtrm |
252 else raise (LIFT_MATCH "regularize (bounds mismatch)") |
252 else raise (LIFT_MATCH "regularize (bounds mismatch)") |
253 |
253 |