--- a/IntEx.thy Mon Nov 23 10:26:59 2009 +0100
+++ b/IntEx.thy Mon Nov 23 13:24:12 2009 +0100
@@ -187,22 +187,26 @@
val qty = fastype_of qtrm
in
case (rtrm, qtrm) of
- (Abs (x, T, t), Abs (x', T', t')) =>
+ (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') =>
+ Const (@{const_name "Ball"}, T) $ r $ (inj_REPABS lthy (t, t'))
+ | (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') =>
+ Const (@{const_name "Bex"}, T) $ r $ (inj_REPABS lthy (t, t'))
+ | (Const (@{const_name "Babs"}, T) $ r $ t, t') =>
+ Const (@{const_name "Babs"}, T) $ r $ (inj_REPABS lthy (t, t'))
+ | (Abs (x, T, t), Abs (x', T', t')) =>
let
val (y, s) = Term.dest_abs (x, T, t)
- val (y', s') = Term.dest_abs (x', T', t')
+ val (_, s') = Term.dest_abs (x', T', t')
val yvar = Free (y, T)
val res = lambda yvar (inj_REPABS lthy (s, s'))
in
- if T = T'
+ if rty = qty
then res
- else mk_repabs lthy (rty, qty) (replace_bnd0 (mk_repabs lthy (T, T') (Bound 0), res))
+ else if T = T'
+ then mk_repabs lthy (rty, qty) res
+ else mk_repabs lthy (rty, qty) (replace_bnd0 (mk_repabs lthy (T, T') (Bound 0), res))
end
- (* FIXME: Does one have to look at the abstraction or have to go under the lambda? *)
- | (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') =>
- Const (@{const_name "Ball"}, T) $ r $ (inj_REPABS lthy (t, t'))
- | (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') =>
- Const (@{const_name "Bex"}, T) $ r $ (inj_REPABS lthy (t, t'))
+ (* TODO: check what happens if head is a constant *)
| (_ $ _, _ $ _) =>
let
val (rhead, rargs) = strip_comb rtrm
@@ -213,9 +217,14 @@
in
if rty = qty
then result
- else mk_repabs lthy (rty, qty) res
+ else mk_repabs lthy (rty, qty) result
end
- (* FIXME: cases for frees and vars? *)
+ (* TODO: maybe leave result without mk_repabs when head is a constant *)
+ (* TODO: that we do not know how to lift *)
+ | (Const (s, T), Const (s', T')) =>
+ if T = T'
+ then rtrm
+ else mk_repabs lthy (T, T') rtrm
| _ => rtrm
end
*}
@@ -286,6 +295,10 @@
|> Syntax.check_term @{context}
*}
+
+ML {* val my_goal = cterm_of @{theory} (mk_inj_REPABS_goal @{context} (reg_atrm, aqtrm)) *}
+ML {* val yr_goal = cterm_of @{theory} (build_repabs_goal @{context} (@{thm testtest} OF [arthm]) consts rty qty) *}
+
prove {* mk_inj_REPABS_goal @{context} (reg_atrm, aqtrm) *}
apply(tactic {* ObjectLogic.full_atomize_tac 1 *})
(* does not work *)