--- a/QuotMain.thy Fri Nov 20 13:03:01 2009 +0100
+++ b/QuotMain.thy Sat Nov 21 02:49:39 2009 +0100
@@ -557,7 +557,62 @@
*}
ML {*
-fun get_fun_new flag (rty, qty) lthy ty =
+fun negF absF = repF
+ | negF repF = absF
+
+fun get_fun flag qenv lthy ty =
+let
+
+ fun get_fun_aux s fs =
+ (case (maps_lookup (ProofContext.theory_of lthy) s) of
+ SOME info => list_comb (Const (#mapfun info, dummyT), fs)
+ | NONE => error ("no map association for type " ^ s))
+
+ fun get_const flag qty =
+ let
+ val thy = ProofContext.theory_of lthy
+ val qty_name = Long_Name.base_name (fst (dest_Type qty))
+ in
+ case flag of
+ absF => Const (Sign.full_bname thy ("ABS_" ^ qty_name), dummyT)
+ | repF => Const (Sign.full_bname thy ("REP_" ^ qty_name), dummyT)
+ end
+
+ fun mk_identity ty = Abs ("", ty, Bound 0)
+
+in
+ if (AList.defined (op=) qenv ty)
+ then (get_const flag ty)
+ else (case ty of
+ TFree _ => mk_identity ty
+ | Type (_, []) => mk_identity ty
+ | Type ("fun" , [ty1, ty2]) =>
+ let
+ val fs_ty1 = get_fun (negF flag) qenv lthy ty1
+ val fs_ty2 = get_fun flag qenv lthy ty2
+ in
+ get_fun_aux "fun" [fs_ty1, fs_ty2]
+ end
+ | Type (s, tys) => get_fun_aux s (map (get_fun flag qenv lthy) tys)
+ | _ => error ("no type variables allowed"))
+end
+
+(* returns all subterms where two types differ *)
+fun diff (T, S) Ds =
+ case (T, S) of
+ (TVar v, TVar u) => if v = u then Ds else (T, S)::Ds
+ | (TFree x, TFree y) => if x = y then Ds else (T, S)::Ds
+ | (Type (a, Ts), Type (b, Us)) =>
+ if a = b then diffs (Ts, Us) Ds else (T, S)::Ds
+ | _ => (T, S)::Ds
+and diffs (T::Ts, U::Us) Ds = diffs (Ts, Us) (diff (T, U) Ds)
+ | diffs ([], []) Ds = Ds
+ | diffs _ _ = error "Unequal length of type arguments"
+
+*}
+
+ML {*
+fun get_fun_OLD flag (rty, qty) lthy ty =
let
val tys = find_matching_types rty ty;
val qenv = map (fn t => (exchange_ty lthy rty qty t, t)) tys;
@@ -657,11 +712,11 @@
fun mk_abs tm =
let
val ty = fastype_of tm
- in Syntax.check_term lthy ((get_fun_new absF (rty, qty) lthy ty) $ tm) end
+ in Syntax.check_term lthy ((get_fun_OLD absF (rty, qty) lthy ty) $ tm) end
fun mk_repabs tm =
let
val ty = fastype_of tm
- in Syntax.check_term lthy ((get_fun_new repF (rty, qty) lthy ty) $ (mk_abs tm)) end
+ in Syntax.check_term lthy ((get_fun_OLD repF (rty, qty) lthy ty) $ (mk_abs tm)) end
fun is_lifted_const (Const (x, _)) = member (op =) consts x
| is_lifted_const _ = false;
@@ -1008,11 +1063,11 @@
fun mk_rep tm =
let
val ty = exchange_ty lthy qty rty (fastype_of tm)
- in Syntax.check_term lthy ((get_fun_new repF (rty, qty) lthy ty) $ tm) end;
+ in Syntax.check_term lthy ((get_fun_OLD repF (rty, qty) lthy ty) $ tm) end;
fun mk_abs tm =
let
val ty = fastype_of tm
- in Syntax.check_term lthy ((get_fun_new absF (rty, qty) lthy ty) $ tm) end
+ in Syntax.check_term lthy ((get_fun_OLD absF (rty, qty) lthy ty) $ tm) end
val (l, ltl) = Term.strip_type ty;
val nl = map absty l;
val vs = map (fn _ => "x") l;
@@ -1149,7 +1204,6 @@
(******************************************)
(* exception for when qtrm and rtrm do not match *)
-ML {* exception LIFT_MATCH of string *}
ML {*
fun mk_resp_arg lthy (rty, qty) =
@@ -1161,7 +1215,7 @@
if s = s'
then let
val SOME map_info = maps_lookup thy s
- val args = map (mk_resp_arg lthy) (tys ~~tys')
+ val args = map (mk_resp_arg lthy) (tys ~~ tys')
in
list_comb (Const (#relfun map_info, dummyT), args)
end
@@ -1192,12 +1246,28 @@
fun qnt_typ ty = domain_type (domain_type ty)
*}
+(*
+Regularizing an rterm means:
+ - Quantifiers over a type that needs lifting are replaced by
+ bounded quantifiers, for example:
+ \<forall>x. P \<Longrightarrow> \<forall>x\<in>(Respects R). P
+ - Abstractions over a type that needs lifting are replaced
+ by bounded abstractions:
+ \<lambda>x. P \<Longrightarrow> Ball (Respects R) (\<lambda>x. P)
+
+ - Equalities over the type being lifted are replaced by
+ appropriate relations:
+ A = B \<Longrightarrow> A \<approx> B
+ Example with more complicated types of A, B:
+ A = B \<Longrightarrow> (op = \<Longrightarrow> op \<approx>) A B
+*)
+
ML {*
-fun REGULARIZE_aux lthy rtrm qtrm =
+fun REGULARIZE_trm lthy rtrm qtrm =
case (rtrm, qtrm) of
(Abs (x, T, t), Abs (x', T', t')) =>
let
- val subtrm = REGULARIZE_aux lthy t t'
+ val subtrm = REGULARIZE_trm lthy t t'
in
if T = T'
then Abs (x, T, subtrm)
@@ -1205,7 +1275,7 @@
end
| (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') =>
let
- val subtrm = apply_subt (REGULARIZE_aux lthy) t t'
+ val subtrm = apply_subt (REGULARIZE_trm lthy) t t'
in
if ty = ty'
then Const (@{const_name "All"}, ty) $ subtrm
@@ -1213,7 +1283,7 @@
end
| (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') =>
let
- val subtrm = apply_subt (REGULARIZE_aux lthy) t t'
+ val subtrm = apply_subt (REGULARIZE_trm lthy) t t'
in
if ty = ty'
then Const (@{const_name "Ex"}, ty) $ subtrm
@@ -1222,14 +1292,14 @@
(* FIXME: why is there a case for equality? is it correct? *)
| (Const (@{const_name "op ="}, ty) $ t, Const (@{const_name "op ="}, ty') $ t') =>
let
- val subtrm = REGULARIZE_aux lthy t t'
+ val subtrm = REGULARIZE_trm lthy t t'
in
if ty = ty'
then Const (@{const_name "op ="}, ty) $ subtrm
else mk_resp_arg lthy (ty, ty') $ subtrm
end
| (t1 $ t2, t1' $ t2') =>
- (REGULARIZE_aux lthy t1 t1') $ (REGULARIZE_aux lthy t2 t2')
+ (REGULARIZE_trm lthy t1 t1') $ (REGULARIZE_trm lthy t2 t2')
| (Free (x, ty), Free (x', ty')) =>
if x = x'
then rtrm
@@ -1246,11 +1316,98 @@
*}
ML {*
-fun REGULARIZE_trm lthy rtrm qtrm =
- REGULARIZE_aux lthy rtrm qtrm
- |> Syntax.check_term lthy
-
+fun mk_REGULARIZE_goal lthy rtrm qtrm =
+ Logic.mk_implies (rtrm, REGULARIZE_trm lthy rtrm qtrm |> Syntax.check_term lthy)
*}
+(*
+To prove that the old theorem implies the new one, we first
+atomize it and then try:
+ - Reflexivity of the relation
+ - Assumption
+ - Elimnating quantifiers on both sides of toplevel implication
+ - Simplifying implications on both sides of toplevel implication
+ - Ball (Respects ?E) ?P = All ?P
+ - (\<And>x. ?R x \<Longrightarrow> ?P x \<longrightarrow> ?Q x) \<Longrightarrow> All ?P \<longrightarrow> Ball ?R ?Q
+
+*)
+
+lemma my_equiv_res_forall2:
+ fixes P::"'a \<Rightarrow> bool"
+ fixes Q::"'b \<Rightarrow> bool"
+ assumes a: "(All Q) \<longrightarrow> (All P)"
+ shows "(All Q) \<longrightarrow> Ball (Respects E) P"
+using a by auto
+
+lemma my_equiv_res_exists:
+ fixes P::"'a \<Rightarrow> bool"
+ fixes Q::"'b \<Rightarrow> bool"
+ assumes a: "EQUIV E"
+ and b: "(Ex Q) \<longrightarrow> (Ex P)"
+ shows "(Ex Q) \<longrightarrow> Bex (Respects E) P"
+apply(subst equiv_res_exists)
+apply(rule a)
+apply(rule b)
+done
+
+ML {*
+fun REGULARIZE_tac lthy rel_refl rel_eqv =
+ ObjectLogic.full_atomize_tac THEN'
+ REPEAT_ALL_NEW (FIRST'
+ [rtac rel_refl,
+ atac,
+ rtac @{thm universal_twice},
+ rtac @{thm impI} THEN' atac,
+ rtac @{thm implication_twice},
+ rtac @{thm my_equiv_res_forall2},
+ rtac (rel_eqv RS @{thm my_equiv_res_exists}),
+ (* For a = b \<longrightarrow> a \<approx> b *)
+ rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl,
+ rtac @{thm RIGHT_RES_FORALL_REGULAR}])
+*}
+
+(* same version including debugging information *)
+ML {*
+fun my_print_tac ctxt s thm =
+let
+ val prems_str = prems_of thm
+ |> map (Syntax.string_of_term ctxt)
+ |> cat_lines
+ val _ = tracing (s ^ "\n" ^ prems_str)
+in
+ Seq.single thm
+end
+
+fun DT ctxt s tac = EVERY' [tac, K (my_print_tac ctxt ("after " ^ s))]
+*}
+
+ML {*
+fun REGULARIZE_tac' lthy rel_refl rel_eqv =
+ (REPEAT1 o FIRST1)
+ [(K (print_tac "start")) THEN' (K no_tac),
+ DT lthy "1" (rtac rel_refl),
+ DT lthy "2" atac,
+ DT lthy "3" (rtac @{thm universal_twice}),
+ DT lthy "4" (rtac @{thm impI} THEN' atac),
+ DT lthy "5" (rtac @{thm implication_twice}),
+ DT lthy "6" (rtac @{thm my_equiv_res_forall2}),
+ DT lthy "7" (rtac (rel_eqv RS @{thm my_equiv_res_exists})),
+ (* For a = b \<longrightarrow> a \<approx> b *)
+ DT lthy "8" (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl),
+ DT lthy "9" (rtac @{thm RIGHT_RES_FORALL_REGULAR})]
+*}
+
+ML {*
+fun REGULARIZE_prove rtrm qtrm rel_eqv rel_refl lthy =
+ let
+ val goal = mk_REGULARIZE_goal lthy rtrm qtrm
+ val cthm = Goal.prove lthy [] [] goal
+ (fn {context, ...} => REGULARIZE_tac context rel_refl rel_eqv 1)
+ in
+ cthm
+ end
+*}
+
+
end