--- a/FSet.thy Tue Nov 24 19:09:29 2009 +0100
+++ b/FSet.thy Wed Nov 25 03:45:44 2009 +0100
@@ -376,6 +376,7 @@
Conv.concl_conv ~1 (lambda_prs_conv ctxt quot))) ctxt) i)
*}
+(*
ML {*
lambda_prs_conv @{context} quot
@{cterm "((ABS_fset ---> id) ---> id) (\<lambda>x\<Colon>'a list \<Rightarrow> bool. id ((f ((REP_fset ---> id) x) ((REP_fset ---> id) x))))"}
@@ -395,15 +396,16 @@
(ABS_fset ---> id) ((REP_fset ---> id) P) (REP_fset (ABS_fset list)))))"}
*}
-
+*)
lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"
apply(tactic {* procedure_tac @{thm list.induct} @{context} 1 *})
apply(tactic {* regularize_tac @{context} rel_eqv rel_refl 1 *})
apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms) 1 *})
apply(tactic {* REPEAT_ALL_NEW (allex_prs_tac @{context} quot) 1 *})
+oops
-
+(*
thm LAMBDA_PRS
apply(tactic {* EqSubst.eqsubst_tac @{context} [0] @{thms LAMBDA_PRS} 1 *})
@@ -414,19 +416,17 @@
apply(tactic {* clean_tac @{context} quot defs reps_same 1 *})
apply (tactic {* lift_tac_fset @{context} @{thm list.induct} 1 *})
ML {* lift_thm_fset @{context} @{thm list.induct} *}
-ML {* lift_thm_g_fset @{context} @{thm list.induct} @{term "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"} *}
-
-
+ML {* lift_thm_g_fset @{context} @{thm list.induct} @{term "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"} *}*)
-thm map_append
-lemma "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)"
+lemma "\<forall>f x xa. fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)"
apply(tactic {* procedure_tac @{thm map_append} @{context} 1 *})
-apply(tactic {* prepare_tac 1 *})
-thm map_append
-apply (tactic {* lift_tac_fset @{context} @{thm map_append} 1 *})
-done
+oops
+
+lemma "fmap f (FUNION (x::'b fset) (y::'b fset)) = FUNION (fmap f x) (fmap f y)"
+apply(tactic {* procedure_tac @{thm map_append} @{context} 1 *})
+oops
lemma "FUNION (FUNION x xa) xb = FUNION x (FUNION xa xb)"
--- a/IntEx.thy Tue Nov 24 19:09:29 2009 +0100
+++ b/IntEx.thy Wed Nov 25 03:45:44 2009 +0100
@@ -194,17 +194,6 @@
apply(tactic {* clean_tac @{context} quot @{thms PLUS_def} reps_same 1 *})
done
-apply(tactic {* REPEAT_ALL_NEW (allex_prs_tac @{context} quot) 1 *})
-apply(tactic {* REPEAT_ALL_NEW (lambda_prs_tac @{context} quot) 1 *})
-(* phase 2 *)
-ML_prf {*
- val lower = add_lower_defs @{context} @{thm PLUS_def}
-*}
-apply(tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] lower) 1*})
-apply(tactic {* simp_tac (HOL_ss addsimps [reps_same]) 1 *})
-done
-
-
(*
does not work.
@@ -236,7 +225,6 @@
val consts = lookup_quot_consts defs
*}
-ML {* cprem_of *}
ML {*
mk_inj_REPABS_goal @{context} (reg_atrm, aqtrm)
--- a/QuotMain.thy Tue Nov 24 19:09:29 2009 +0100
+++ b/QuotMain.thy Wed Nov 25 03:45:44 2009 +0100
@@ -1172,16 +1172,6 @@
val mk_resp = Const (@{const_name Respects}, dummyT)
*}
-ML {*
-fun trm_lift_error lthy rtrm qtrm =
-let
- val rtrm_str = quote (Syntax.string_of_term lthy rtrm)
- val qtrm_str = quote (Syntax.string_of_term lthy qtrm)
- val msg = ["The quotient theorem", qtrm_str, "and lifted theorem", rtrm_str, "do not match."]
-in
- raise error (space_implode " " msg)
-end
-*}
ML {*
(* - applies f to the subterm of an abstraction, *)
@@ -1265,16 +1255,23 @@
| (Free (x, ty), Free (x', ty')) =>
if x = x'
then rtrm (* FIXME: check whether types corresponds *)
- else trm_lift_error lthy rtrm qtrm
+ else raise (LIFT_MATCH "regularize (frees)")
| (Bound i, Bound i') =>
if i = i'
then rtrm
- else trm_lift_error lthy rtrm qtrm
+ else raise (LIFT_MATCH "regularize (bounds)")
| (Const (s, ty), Const (s', ty')) =>
if s = s' andalso ty = ty'
then rtrm
else rtrm (* FIXME: check correspondence according to definitions *)
- | _ => trm_lift_error lthy rtrm qtrm
+ | (rt, qt) =>
+ let
+ val _ = tracing "default execption"
+ val _ = tracing (PolyML.makestring rt)
+ val _ = tracing (PolyML.makestring qt)
+ in
+ raise (LIFT_MATCH "regularize (default)")
+ end
*}
ML {*
@@ -1433,7 +1430,7 @@
mk_repabs lthy (rty, qty) (list_comb (mk_repabs lthy (T, T') rhead, rargs'))
| (Abs _, Abs _, _ ) =>
mk_repabs lthy (rty, qty) (list_comb (inj_REPABS lthy (rhead, qhead), rargs'))
- | _ => trm_lift_error lthy rtrm qtrm
+ | _ => raise (LIFT_MATCH "injection")
end
end
*}
@@ -1528,22 +1525,33 @@
*}
ML {*
-fun spec_frees_tac [] = []
- | spec_frees_tac (x::xs) =
- let
- val spec' = Drule.instantiate' [SOME (ctyp_of_term x)] [NONE, SOME x] @{thm spec}
- in
- (rtac spec')::(spec_frees_tac xs)
- end
-*}
+fun inst_spec ctrm =
+let
+ val cty = ctyp_of_term ctrm
+in
+ Drule.instantiate' [SOME cty] [NONE, SOME ctrm] @{thm spec}
+end
+
+fun inst_spec_tac ctrms =
+ EVERY' (map (dtac o inst_spec) ctrms)
+
+fun abs_list (xs, t) =
+ fold (fn (x, T) => fn t' => HOLogic.all_const T $ (lambda (Free (x, T)) t')) xs t
-ML {*
-val prepare_tac = CSUBGOAL (fn (concl, i) =>
- let
- val vrs = Thm.add_cterm_frees concl []
- in
- EVERY' (ObjectLogic.full_atomize_tac::spec_frees_tac vrs) i
- end)
+fun gen_frees_tac ctxt =
+ SUBGOAL (fn (concl, i) =>
+ let
+ val thy = ProofContext.theory_of ctxt
+ val concl' = HOLogic.dest_Trueprop concl
+ val vrs = Term.add_frees concl' []
+ val cvrs = map (cterm_of thy o Free) vrs
+ val concl'' = HOLogic.mk_Trueprop (abs_list (vrs, concl'))
+ val goal = Logic.mk_implies (concl'', concl)
+ val rule = Goal.prove ctxt [] [] goal
+ (K ((inst_spec_tac (rev cvrs) THEN' atac) 1))
+ in
+ rtac rule i
+ end)
*}
lemma procedure:
@@ -1555,6 +1563,18 @@
using a b c d
by simp
+ML {*
+fun lift_error ctxt fun_str rtrm qtrm =
+let
+ val rtrm_str = Syntax.string_of_term ctxt rtrm
+ val qtrm_str = Syntax.string_of_term ctxt qtrm
+ val msg = [enclose "[" "]" fun_str, "The quotient theorem", qtrm_str,
+ "and the lifted theorem", rtrm_str, "do not match"]
+in
+ error (space_implode " " msg)
+end
+*}
+
ML {*
fun procedure_inst ctxt rtrm qtrm =
let
@@ -1562,7 +1582,9 @@
val rtrm' = HOLogic.dest_Trueprop rtrm
val qtrm' = HOLogic.dest_Trueprop qtrm
val reg_goal = Syntax.check_term ctxt (REGULARIZE_trm ctxt rtrm' qtrm')
+ handle (LIFT_MATCH s) => lift_error ctxt s rtrm qtrm
val inj_goal = Syntax.check_term ctxt (inj_REPABS ctxt (reg_goal, qtrm'))
+ handle (LIFT_MATCH s) => lift_error ctxt s rtrm qtrm
in
Drule.instantiate' []
[SOME (cterm_of thy rtrm'),
@@ -1574,17 +1596,19 @@
ML {*
fun procedure_tac rthm ctxt =
- prepare_tac THEN'
- Subgoal.FOCUS (fn {context, concl, ...} =>
- let
- val rthm' = atomize_thm rthm
- val rule = procedure_inst context (prop_of rthm') (term_of concl)
- in
- EVERY1 [rtac rule, rtac rthm']
- end) ctxt
+ ObjectLogic.full_atomize_tac
+ THEN' gen_frees_tac ctxt
+ 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
*}
+
ML {*
(* FIXME: allex_prs and lambda_prs can be one function *)
fun allex_prs_tac lthy quot =
@@ -1618,7 +1642,7 @@
val univ = Unify.matchers thy [(pat, trm)]
val SOME (env, _) = Seq.pull univ
val tenv = Vartab.dest (Envir.term_env env)
- val tyenv = Vartab.dest (Envir.type_env env)
+ val tyenv = Vartab.dest (Envir.type_env env)
in
(map (prep_ty thy) tyenv, map (prep_trm thy) tenv)
end
--- a/quotient.ML Tue Nov 24 19:09:29 2009 +0100
+++ b/quotient.ML Wed Nov 25 03:45:44 2009 +0100
@@ -1,5 +1,7 @@
signature QUOTIENT =
sig
+ exception LIFT_MATCH of string
+
val quotient_type: ((binding * mixfix) * (typ * term)) list -> Proof.context -> Proof.state
val quotient_type_cmd: (((bstring * mixfix) * string) * string) list -> Proof.context -> Proof.state
@@ -9,6 +11,8 @@
structure Quotient: QUOTIENT =
struct
+exception LIFT_MATCH of string
+
(* wrappers for define, note and theorem_i *)
fun define (name, mx, rhs) lthy =
let
--- a/quotient_def.ML Tue Nov 24 19:09:29 2009 +0100
+++ b/quotient_def.ML Wed Nov 25 03:45:44 2009 +0100
@@ -31,30 +31,11 @@
fun mk_identity ty = Const (@{const_name "id"}, ty --> ty)
-fun ty_strs lthy (ty1, ty2) =
- (quote (Syntax.string_of_typ lthy ty1),
- quote (Syntax.string_of_typ lthy ty2))
-
-fun ty_lift_error1 lthy rty qty =
-let
- val (rty_str, qty_str) = ty_strs lthy (rty, qty)
- val msg = ["quotient type", qty_str, "and lifted type", rty_str, "do not match."]
-in
- error (space_implode " " msg)
-end
-
-fun ty_lift_error2 lthy rty qty =
-let
- val (rty_str, qty_str) = ty_strs lthy (rty, qty)
- val msg = ["No type variables allowed in", qty_str, "and", rty_str, "."]
-in
- error (space_implode " " msg)
-end
-
fun get_fun_aux lthy s fs =
case (maps_lookup (ProofContext.theory_of lthy) s) of
SOME info => list_comb (Const (#mapfun info, dummyT), fs)
- | NONE => error (space_implode " " ["No map function for type", quote s, "."])
+ | NONE => raise
+ (LIFT_MATCH (space_implode " " ["get_fun_aux: no map for type", quote s, "."]))
fun get_const flag lthy _ qty =
(* FIXME: check here that _ and qty are related *)
@@ -93,9 +74,9 @@
| (TFree x, TFree x') =>
if x = x'
then mk_identity qty
- else ty_lift_error1 lthy rty qty
- | (TVar _, TVar _) => ty_lift_error2 lthy rty qty
- | _ => ty_lift_error1 lthy rty qty
+ else raise (LIFT_MATCH "get_fun")
+ | (TVar _, TVar _) => raise (LIFT_MATCH "get_fun")
+ | _ => raise (LIFT_MATCH "get_fun")
fun make_def qconst_bname qty mx attr rhs lthy =
let