# HG changeset patch # User Christian Urban # Date 1259117227 -3600 # Node ID f7dee6e808eb7fb6f098a41a02a85a2f6d389be0 # Parent 980fdf92a83418156e7205d6a8aba43de231d9d4# Parent eef425e473cc32bf8c8b5fe7758c8465e5a62e15 merged diff -r eef425e473cc -r f7dee6e808eb FSet.thy diff -r eef425e473cc -r f7dee6e808eb IntEx.thy --- a/IntEx.thy Tue Nov 24 20:13:16 2009 +0100 +++ b/IntEx.thy Wed Nov 25 03:47:07 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) diff -r eef425e473cc -r f7dee6e808eb QuotMain.thy --- a/QuotMain.thy Tue Nov 24 20:13:16 2009 +0100 +++ b/QuotMain.thy Wed Nov 25 03:47:07 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 diff -r eef425e473cc -r f7dee6e808eb quotient.ML --- a/quotient.ML Tue Nov 24 20:13:16 2009 +0100 +++ b/quotient.ML Wed Nov 25 03:47:07 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 diff -r eef425e473cc -r f7dee6e808eb quotient_def.ML --- a/quotient_def.ML Tue Nov 24 20:13:16 2009 +0100 +++ b/quotient_def.ML Wed Nov 25 03:47:07 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