--- a/FSet.thy Thu Nov 26 02:31:00 2009 +0100
+++ b/FSet.thy Thu Nov 26 03:18:38 2009 +0100
@@ -304,7 +304,7 @@
ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset"; *}
ML {* val consts = lookup_quot_consts defs *}
-ML {* fun lift_tac_fset lthy t = lift_tac lthy t rel_eqv rel_refl rty quot trans2 rsp_thms reps_same defs *}
+ML {* fun lift_tac_fset lthy t = lift_tac lthy t rel_eqv rel_refl rty quot trans2 rsp_thms reps_same absrep defs *}
lemma "IN x EMPTY = False"
by (tactic {* lift_tac_fset @{context} @{thm m1} 1 *})
@@ -334,8 +334,6 @@
done
lemma "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)"
-apply(tactic {* Induct.fix_tac @{context} 0 [("x", @{typ "'b fset"}), ("xa", @{typ "'b fset"})] 1 *})
-apply(tactic {* ObjectLogic.full_atomize_tac 1 *})
apply (tactic {* lift_tac_fset @{context} @{thm map_append} 1 *})
done
@@ -412,26 +410,14 @@
ML {* val rsp_thms = @{thms list_rec_rsp list_case_rsp} @ rsp_thms *}
ML {* val defs = @{thms fset_rec_def fset_case_def} @ defs *}
-ML {* fun lift_tac_fset lthy t = lift_tac lthy t rel_eqv rel_refl rty quot trans2 rsp_thms reps_same defs *}
+ML {* fun lift_tac_fset lthy t = lift_tac lthy t rel_eqv rel_refl rty quot trans2 rsp_thms reps_same absrep defs *}
-ML {* val aps = findaps rty (prop_of (atomize_thm @{thm list.recs(2)})) *}
-ML {* val app_prs_thms = map (applic_prs @{context} rty qty absrep) aps *}
lemma "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)"
apply (tactic {* lift_tac_fset @{context} @{thm list.recs(2)} 1 *})
-apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] app_prs_thms) 1 *})
-apply (tactic {* (simp_tac (HOL_ss addsimps
- @{thms eq_reflection[OF FUN_MAP_I] eq_reflection[OF id_apply] id_def_sym prod_fun_id map_id})) 1 *})
-ML_prf {* val lower = flat (map (add_lower_defs @{context}) defs) *}
-apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] lower) 1 *})
-apply (tactic {* simp_tac (HOL_ss addsimps [reps_same]) 1 *})
done
-ML {* val aps = findaps rty (prop_of (atomize_thm @{thm list.cases(2)})) *}
-ML {* val app_prs_thms = map (applic_prs @{context} rty qty absrep) aps *}
lemma "fset_case (f1::'t) f2 (INSERT a xa) = f2 a xa"
apply (tactic {* lift_tac_fset @{context} @{thm list.cases(2)} 1 *})
-apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] app_prs_thms) 1 *})
-apply (tactic {* simp_tac (HOL_ss addsimps [reps_same]) 1 *})
done
lemma list_induct_part:
@@ -452,7 +438,7 @@
(* Construction site starts here *)
lemma "P (x :: 'a list) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"
-apply (tactic {* procedure_tac @{thm list_induct_part} @{context} 1 *})
+apply (tactic {* procedure_tac @{context} @{thm list_induct_part} 1 *})
apply (tactic {* regularize_tac @{context} rel_eqv rel_refl 1 *})
apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *})
apply (rule FUN_QUOTIENT)
@@ -478,7 +464,6 @@
apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *})
apply (rule IDENTITY_QUOTIENT)
apply (rule FUN_QUOTIENT)
@@ -503,7 +488,6 @@
apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})
-apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})
apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP(1)} @{context} THEN' (RANGE [quotient_tac quot])) 1 *})
apply assumption
apply (rule refl)
@@ -522,14 +506,7 @@
apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (simp only:map_id)
-apply (tactic {* REPEAT_ALL_NEW (allex_prs_tac @{context} quot) 1 *})
-ML_prf {* val lower = flat (map (add_lower_defs @{context}) defs) *}
-apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] lower) 1 *})
-apply (tactic {* lambda_prs_tac @{context} quot 1 *})
-ML_prf {* val t = applic_prs @{context} rty qty absrep @{typ "('b \<Rightarrow> 'c list \<Rightarrow> bool)"} *}
-apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] [t]) 1 *})
-apply (tactic {* simp_tac (HOL_ss addsimps [reps_same]) 1 *})
+apply (tactic {* clean_tac @{context} quot defs reps_same absrep [(@{typ "('a list \<Rightarrow> 'c list \<Rightarrow> bool)"},@{typ "('a list \<Rightarrow> 'c fset \<Rightarrow> bool)"})] 1 *})
done
end
--- a/IntEx.thy Thu Nov 26 02:31:00 2009 +0100
+++ b/IntEx.thy Thu Nov 26 03:18:38 2009 +0100
@@ -142,7 +142,7 @@
ML {*
fun lift_tac_fset lthy t =
- lift_tac lthy t rel_eqv rel_refl rty quot trans2 rsp_thms reps_same defs
+ lift_tac lthy t rel_eqv rel_refl rty quot trans2 rsp_thms reps_same absrep defs
*}
lemma "PLUS a b = PLUS b a"
@@ -166,8 +166,6 @@
lemma "foldl PLUS x [] = x"
apply (tactic {* lift_tac_fset @{context} @{thm ho_tst} 1 *})
-prefer 3
-apply(tactic {* clean_tac @{context} quot @{thms PLUS_def} reps_same 1 *})
sorry
(*
--- a/LamEx.thy Thu Nov 26 02:31:00 2009 +0100
+++ b/LamEx.thy Thu Nov 26 03:18:38 2009 +0100
@@ -179,7 +179,7 @@
ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
ML {* val consts = lookup_quot_consts defs *}
ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "lam" *}
-ML {* fun lift_tac_lam lthy t = lift_tac lthy t rel_eqv rel_refl rty quot trans2 rsp_thms reps_same defs *}
+ML {* fun lift_tac_lam lthy t = lift_tac lthy t rel_eqv rel_refl rty quot trans2 rsp_thms reps_same absrep defs *}
lemma pi_var: "(pi\<Colon>('x \<times> 'x) list) \<bullet> Var a = Var (pi \<bullet> a)"
apply (tactic {* lift_tac_lam @{context} @{thm pi_var_com} 1 *})
@@ -224,16 +224,12 @@
apply (tactic {* lift_tac_lam @{context} @{thm alpha.cases} 1 *})
done
-ML {* val aps = findaps rty (prop_of (atomize_thm @{thm alpha.induct})) *}
-ML {* val app_prs_thms = map (applic_prs @{context} rty qty absrep) aps *}
lemma alpha_induct: "\<lbrakk>(qx\<Colon>lam) = (qxa\<Colon>lam); \<And>(a\<Colon>name) b\<Colon>name. a = b \<Longrightarrow> (qxb\<Colon>lam \<Rightarrow> lam \<Rightarrow> bool) (Var a) (Var b);
\<And>(x\<Colon>lam) (xa\<Colon>lam) (xb\<Colon>lam) xc\<Colon>lam. \<lbrakk>x = xa; qxb x xa; xb = xc; qxb xb xc\<rbrakk> \<Longrightarrow> qxb (App x xb) (App xa xc);
\<And>(x\<Colon>lam) (a\<Colon>name) (b\<Colon>name) xa\<Colon>lam.
\<lbrakk>x = [(a, b)] \<bullet> xa; qxb x ([(a, b)] \<bullet> xa); a \<notin> fv (Lam b x)\<rbrakk> \<Longrightarrow> qxb (Lam a x) (Lam b xa)\<rbrakk>
\<Longrightarrow> qxb qx qxa"
apply (tactic {* lift_tac_lam @{context} @{thm alpha.induct} 1 *})
-apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] app_prs_thms) 1 *})
-apply (tactic {* simp_tac (HOL_ss addsimps [reps_same]) 1 *})
done
lemma var_inject: "(Var a = Var b) = (a = b)"
--- a/QuotMain.thy Thu Nov 26 02:31:00 2009 +0100
+++ b/QuotMain.thy Thu Nov 26 03:18:38 2009 +0100
@@ -817,7 +817,9 @@
(FIRST' [
rtac trans_thm,
LAMBDA_RES_TAC ctxt,
+ rtac @{thm RES_FORALL_RSP},
ball_rsp_tac ctxt,
+ rtac @{thm RES_EXISTS_RSP},
bex_rsp_tac ctxt,
FIRST' (map rtac rsp_thms),
rtac refl,
@@ -928,7 +930,7 @@
*}
ML {*
-fun applic_prs lthy rty qty absrep ty =
+fun applic_prs_old lthy rty qty absrep ty =
let
val rty = Logic.varifyT rty;
val qty = Logic.varifyT qty;
@@ -961,6 +963,30 @@
end
*}
+ML {*
+fun applic_prs lthy absrep (rty, qty) =
+ let
+ fun mk_rep (T, T') tm = (Quotient_Def.get_fun repF lthy (T, T')) $ tm;
+ fun mk_abs (T, T') tm = (Quotient_Def.get_fun absF lthy (T, T')) $ tm;
+ val (raty, rgty) = Term.strip_type rty;
+ val (qaty, qgty) = Term.strip_type qty;
+ val vs = map (fn _ => "x") qaty;
+ val ((fname :: vfs), lthy') = Variable.variant_fixes ("f" :: vs) lthy;
+ val f = Free (fname, qaty ---> qgty);
+ val args = map Free (vfs ~~ qaty);
+ val rhs = list_comb(f, args);
+ val largs = map2 mk_rep (raty ~~ qaty) args;
+ val lhs = mk_abs (rgty, qgty) (list_comb((mk_rep (raty ---> rgty, qaty ---> qgty) f), largs));
+ val llhs = Syntax.check_term lthy lhs;
+ val eq = Logic.mk_equals (llhs, rhs);
+ val ceq = cterm_of (ProofContext.theory_of lthy') eq;
+ val sctxt = HOL_ss addsimps (absrep :: @{thms fun_map.simps map_id id_apply});
+ val t = Goal.prove_internal [] ceq (fn _ => simp_tac sctxt 1)
+ val t_id = MetaSimplifier.rewrite_rule @{thms eq_reflection[OF id_apply] id_def_sym} t;
+ in
+ singleton (ProofContext.export lthy' lthy) t_id
+ end
+*}
ML {*
fun findaps_all rty tm =
@@ -976,6 +1002,23 @@
ML {*
+fun find_aps_all rtm qtm =
+ case (rtm, qtm) of
+ (Abs(_, T1, s1), Abs(_, T2, s2)) =>
+ find_aps_all (subst_bound ((Free ("x", T1)), s1)) (subst_bound ((Free ("x", T2)), s2))
+ | (((f1 as (Free (_, T1))) $ a1), ((f2 as (Free (_, T2))) $ a2)) =>
+ let
+ val sub = (find_aps_all f1 f2) @ (find_aps_all a1 a2)
+ in
+ if T1 = T2 then sub else (T1, T2) :: sub
+ end
+ | ((f1 $ a1), (f2 $ a2)) => (find_aps_all f1 f2) @ (find_aps_all a1 a2)
+ | _ => [];
+
+fun find_aps rtm qtm = distinct (op =) (find_aps_all rtm qtm)
+*}
+
+ML {*
(* FIXME: allex_prs and lambda_prs can be one function *)
fun allex_prs_tac lthy quot =
(EqSubst.eqsubst_tac lthy [0] @{thms FORALL_PRS[symmetric] EXISTS_PRS[symmetric]})
@@ -1068,13 +1111,14 @@
*}
ML {*
-fun clean_tac lthy quot defs reps_same =
+fun clean_tac lthy quot defs reps_same absrep aps =
let
val lower = flat (map (add_lower_defs lthy) defs)
+ val aps_thms = map (applic_prs lthy absrep) aps
in
EVERY' [TRY o REPEAT_ALL_NEW (allex_prs_tac lthy quot),
lambda_prs_tac lthy quot,
- (* TODO: cleaning according to app_prs *)
+ TRY o REPEAT_ALL_NEW (EqSubst.eqsubst_tac lthy [0] aps_thms),
TRY o REPEAT_ALL_NEW (EqSubst.eqsubst_tac lthy [0] lower),
simp_tac (HOL_ss addsimps [reps_same])]
end
@@ -1165,30 +1209,40 @@
@{thm procedure}
end
*}
-
+
+(* Left for debugging *)
ML {*
-fun procedure_tac rthm ctxt =
- ObjectLogic.full_atomize_tac
- THEN' gen_frees_tac ctxt
+fun procedure_tac lthy rthm =
+ ObjectLogic.full_atomize_tac
+ THEN' gen_frees_tac lthy
THEN' Subgoal.FOCUS (fn {context, concl, ...} =>
- let
- val rthm' = atomize_thm rthm
- val rule = procedure_inst context (prop_of rthm') (Envir.beta_norm (term_of concl))
- in
- EVERY1 [rtac rule, rtac rthm']
- end) ctxt
+ let
+ val rthm' = atomize_thm rthm
+ val rule = procedure_inst context (prop_of rthm') (term_of concl)
+ in
+ rtac rule THEN' rtac rthm'
+ end 1) lthy
*}
ML {*
-fun lift_tac lthy thm rel_eqv rel_refl rty quot trans2 rsp_thms reps_same defs =
- procedure_tac thm lthy THEN'
- RANGE [regularize_tac lthy rel_eqv rel_refl,
- REPEAT_ALL_NEW (r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms),
- clean_tac lthy quot defs reps_same]
+fun lift_tac lthy rthm rel_eqv rel_refl rty quot trans2 rsp_thms reps_same absrep defs =
+ ObjectLogic.full_atomize_tac
+ THEN' gen_frees_tac lthy
+ THEN' Subgoal.FOCUS (fn {context, concl, ...} =>
+ let
+ val rthm' = atomize_thm rthm
+ val rule = procedure_inst context (prop_of rthm') (term_of concl)
+ val aps = find_aps (prop_of rthm') (term_of concl)
+ in
+ rtac rule THEN' RANGE [
+ rtac rthm',
+ regularize_tac lthy rel_eqv rel_refl,
+ REPEAT_ALL_NEW (r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms),
+ clean_tac lthy quot defs reps_same absrep aps
+ ]
+ end 1) lthy
*}
-
-
end
--- a/quotient_def.ML Thu Nov 26 02:31:00 2009 +0100
+++ b/quotient_def.ML Thu Nov 26 03:18:38 2009 +0100
@@ -55,6 +55,7 @@
change *)
fun get_fun flag lthy (rty, qty) =
+ if rty = qty then mk_identity qty else
case (rty, qty) of
(Type ("fun", [ty1, ty2]), Type ("fun", [ty1', ty2'])) =>
let