185 let |
185 let |
186 val rty = fastype_of rtrm |
186 val rty = fastype_of rtrm |
187 val qty = fastype_of qtrm |
187 val qty = fastype_of qtrm |
188 in |
188 in |
189 case (rtrm, qtrm) of |
189 case (rtrm, qtrm) of |
190 (Abs (x, T, t), Abs (x', T', t')) => |
190 (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') => |
|
191 Const (@{const_name "Ball"}, T) $ r $ (inj_REPABS lthy (t, t')) |
|
192 | (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') => |
|
193 Const (@{const_name "Bex"}, T) $ r $ (inj_REPABS lthy (t, t')) |
|
194 | (Const (@{const_name "Babs"}, T) $ r $ t, t') => |
|
195 Const (@{const_name "Babs"}, T) $ r $ (inj_REPABS lthy (t, t')) |
|
196 | (Abs (x, T, t), Abs (x', T', t')) => |
191 let |
197 let |
192 val (y, s) = Term.dest_abs (x, T, t) |
198 val (y, s) = Term.dest_abs (x, T, t) |
193 val (y', s') = Term.dest_abs (x', T', t') |
199 val (_, s') = Term.dest_abs (x', T', t') |
194 val yvar = Free (y, T) |
200 val yvar = Free (y, T) |
195 val res = lambda yvar (inj_REPABS lthy (s, s')) |
201 val res = lambda yvar (inj_REPABS lthy (s, s')) |
196 in |
202 in |
197 if T = T' |
203 if rty = qty |
198 then res |
204 then res |
199 else mk_repabs lthy (rty, qty) (replace_bnd0 (mk_repabs lthy (T, T') (Bound 0), res)) |
205 else if T = T' |
|
206 then mk_repabs lthy (rty, qty) res |
|
207 else mk_repabs lthy (rty, qty) (replace_bnd0 (mk_repabs lthy (T, T') (Bound 0), res)) |
200 end |
208 end |
201 (* FIXME: Does one have to look at the abstraction or have to go under the lambda? *) |
209 (* TODO: check what happens if head is a constant *) |
202 | (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') => |
|
203 Const (@{const_name "Ball"}, T) $ r $ (inj_REPABS lthy (t, t')) |
|
204 | (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') => |
|
205 Const (@{const_name "Bex"}, T) $ r $ (inj_REPABS lthy (t, t')) |
|
206 | (_ $ _, _ $ _) => |
210 | (_ $ _, _ $ _) => |
207 let |
211 let |
208 val (rhead, rargs) = strip_comb rtrm |
212 val (rhead, rargs) = strip_comb rtrm |
209 val (qhead, qargs) = strip_comb qtrm |
213 val (qhead, qargs) = strip_comb qtrm |
210 val rhead' = inj_REPABS lthy (rhead, qhead) |
214 val rhead' = inj_REPABS lthy (rhead, qhead) |
211 val rargs' = map (inj_REPABS lthy) (rargs ~~ qargs) |
215 val rargs' = map (inj_REPABS lthy) (rargs ~~ qargs) |
212 val result = list_comb (rhead', rargs') |
216 val result = list_comb (rhead', rargs') |
213 in |
217 in |
214 if rty = qty |
218 if rty = qty |
215 then result |
219 then result |
216 else mk_repabs lthy (rty, qty) res |
220 else mk_repabs lthy (rty, qty) result |
217 end |
221 end |
218 (* FIXME: cases for frees and vars? *) |
222 (* TODO: maybe leave result without mk_repabs when head is a constant *) |
|
223 (* TODO: that we do not know how to lift *) |
|
224 | (Const (s, T), Const (s', T')) => |
|
225 if T = T' |
|
226 then rtrm |
|
227 else mk_repabs lthy (T, T') rtrm |
219 | _ => rtrm |
228 | _ => rtrm |
220 end |
229 end |
221 *} |
230 *} |
222 |
231 |
223 ML {* |
232 ML {* |