--- a/FSet.thy Mon Nov 23 10:26:59 2009 +0100
+++ b/FSet.thy Mon Nov 23 13:24:12 2009 +0100
@@ -377,6 +377,8 @@
thm list.recs(2)
ML {* val t_a = atomize_thm @{thm list_induct_part} *}
+
+
(* prove {* build_regularize_goal t_a rty rel @{context} *}
ML_prf {* fun tac ctxt = FIRST' [
rtac rel_refl,
@@ -384,7 +386,7 @@
rtac @{thm universal_twice},
(rtac @{thm impI} THEN' atac),
rtac @{thm implication_twice},
- (*rtac @{thm equality_twice},*)
+ //comented out rtac @{thm equality_twice}, //
EqSubst.eqsubst_tac ctxt [0]
[(@{thm equiv_res_forall} OF [rel_eqv]),
(@{thm equiv_res_exists} OF [rel_eqv])],
@@ -393,7 +395,7 @@
]; *}
apply (atomize(full))
apply (tactic {* REPEAT_ALL_NEW (tac @{context}) 1 *})
- done*)
+ done *)
ML {* val t_r = regularize t_a rty rel rel_eqv rel_refl @{context} *}
ML {*
val rt = build_repabs_term @{context} t_r consts rty qty
@@ -589,9 +591,24 @@
ML {* val (tta, ttb) = (my_reg2 @{context} (prop_of t_a) (term_of glac)) *}
(* Does not work. *)
-(* ML {* val ttar = REGULARIZE_trm @{context} (prop_of t_a) (term_of glac) *} *)
+ML {*
+ prop_of t_a
+ |> Syntax.string_of_term @{context}
+ |> writeln
+*}
+
+ML {*
+ (term_of glac)
+ |> Syntax.string_of_term @{context}
+ |> writeln
+*}
+
+ML {* val ttar = REGULARIZE_trm @{context} (prop_of t_a) (term_of glac) *}
ML {* val tt = Syntax.check_term @{context} tta *}
+ML {* val ttr = Syntax.check_term @{context} ttar *}
+
+
prove t_r: {* Logic.mk_implies
((prop_of t_a), tt) *}
--- 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 *)
--- a/QuotMain.thy Mon Nov 23 10:26:59 2009 +0100
+++ b/QuotMain.thy Mon Nov 23 13:24:12 2009 +0100
@@ -1212,10 +1212,16 @@
let
val thy = ProofContext.theory_of lthy
in
- case (rty, qty) of
- (Type (s, tys), Type (s', tys')) =>
+ if rty = qty
+ then HOLogic.eq_const rty
+ else
+ case (rty, qty) of
+ (Type (s, tys), Type (s', tys')) =>
if s = s'
then let
+ val _ = tracing ("maps lookup for " ^ s)
+ val _ = tracing (Syntax.string_of_typ lthy rty)
+ val _ = tracing (Syntax.string_of_typ lthy qty)
val SOME map_info = maps_lookup thy s
val args = map (mk_resp_arg lthy) (tys ~~ tys')
in
@@ -1228,7 +1234,7 @@
in
#rel qinfo
end
- | _ => HOLogic.eq_const dummyT
+ | _ => HOLogic.eq_const dummyT
(* FIXME: do the types correspond to each other? *)
end
*}
@@ -1263,7 +1269,7 @@
| _ => f trm1 trm2
(* the major type of All and Ex quantifiers *)
-fun qnt_typ ty = domain_type (domain_type ty)
+fun qnt_typ ty = domain_type (domain_type ty)
*}
(*
@@ -1305,6 +1311,9 @@
| (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') =>
let
val subtrm = apply_subt (REGULARIZE_trm lthy) t t'
+ val _ = tracing "quantor types All"
+ val _ = tracing (Syntax.string_of_typ lthy ty)
+ val _ = tracing (Syntax.string_of_typ lthy ty')
in
if ty = ty'
then Const (@{const_name "All"}, ty) $ subtrm
@@ -1313,12 +1322,15 @@
| (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') =>
let
val subtrm = apply_subt (REGULARIZE_trm lthy) t t'
+ val _ = tracing "quantor types Ex"
+ val _ = tracing (Syntax.string_of_typ lthy ty)
+ val _ = tracing (Syntax.string_of_typ lthy ty')
in
if ty = ty'
then Const (@{const_name "Ex"}, ty) $ subtrm
else mk_bex $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm
end
- (* FIXME: Why is there a case for equality? Is it correct? *)
+ (* FIXME: should be replaced when fully applied? then 2nd argument *)
| (Const (@{const_name "op ="}, ty) $ t, Const (@{const_name "op ="}, ty') $ t') =>
let
val subtrm = REGULARIZE_trm lthy t t'