diff -r c129354f2ff6 -r 3104d62e7a16 Quot/QuotMain.thy --- a/Quot/QuotMain.thy Wed Dec 16 14:28:48 2009 +0100 +++ b/Quot/QuotMain.thy Thu Dec 17 14:58:33 2009 +0100 @@ -3,6 +3,8 @@ uses ("quotient_info.ML") ("quotient_typ.ML") ("quotient_def.ML") + ("quotient_term.ML") + ("quotient_tacs.ML") begin locale QUOT_TYPE = @@ -107,36 +109,31 @@ (* lifting of constants *) use "quotient_def.ML" -section {* Simset setup *} +(* the translation functions *) +use "quotient_term.ML" -(* Since HOL_basic_ss is too "big" for us, *) -(* we set up our own minimal simpset. *) -ML {* -fun mk_minimal_ss ctxt = - Simplifier.context ctxt empty_ss - setsubgoaler asm_simp_tac - setmksimps (mksimps []) -*} +(* tactics *) +lemma eq_imp_rel: + "equivp R ==> a = b --> R a b" +by (simp add: equivp_reflp) -ML {* -fun OF1 thm1 thm2 = thm2 RS thm1 -*} +definition + "QUOT_TRUE x \ True" -(* various tactic combinators *) -ML {* -fun SOLVES' tac = tac THEN_ALL_NEW (K no_tac) -*} +lemma quot_true_dests: + shows QT_all: "QUOT_TRUE (All P) \ QUOT_TRUE P" + and QT_ex: "QUOT_TRUE (Ex P) \ QUOT_TRUE P" + and QT_lam: "QUOT_TRUE (\x. P x) \ (\x. QUOT_TRUE (P x))" + and QT_ext: "(\x. QUOT_TRUE (a x) \ f x = g x) \ (QUOT_TRUE a \ f = g)" +by (simp_all add: QUOT_TRUE_def ext) -ML {* -(* prints warning, if goal is unsolved *) -fun WARN (tac, msg) i st = - case Seq.pull ((SOLVES' tac) i st) of - NONE => (warning msg; Seq.single st) - | seqcell => Seq.make (fn () => seqcell) +lemma QUOT_TRUE_imp: "QUOT_TRUE a \ QUOT_TRUE b" +by (simp add: QUOT_TRUE_def) -fun RANGE_WARN xs = RANGE (map WARN xs) -*} +lemma regularize_to_injection: "(QUOT_TRUE l \ y) \ (l = r) \ y" + by(auto simp add: QUOT_TRUE_def) +use "quotient_tacs.ML" section {* Atomize Infrastructure *} @@ -160,16 +157,6 @@ then show "A \ B" by (rule eq_reflection) qed -ML {* -fun atomize_thm thm = -let - val thm' = Thm.freezeT (forall_intr_vars thm) - val thm'' = ObjectLogic.atomize (cprop_of thm') -in - @{thm equal_elim_rule1} OF [thm'', thm'] -end -*} - section {* Infrastructure about id *} lemmas [id_simps] = @@ -177,902 +164,6 @@ id_apply[THEN eq_reflection] id_def[THEN eq_reflection,symmetric] -section {* Computation of the Regularize Goal *} - -(* -Regularizing an rtrm means: - - quantifiers over a type that needs lifting are replaced by - bounded quantifiers, for example: - \x. P \ \x \ (Respects R). P / All (Respects R) P - - the relation R is given by the rty and qty; - - - abstractions over a type that needs lifting are replaced - by bounded abstractions: - \x. P \ Ball (Respects R) (\x. P) - - - equalities over the type being lifted are replaced by - corresponding relations: - A = B \ A \ B - - example with more complicated types of A, B: - A = B \ (op = \ op \) A B -*) - -ML {* -(* builds the relation that is the argument of respects *) -fun mk_resp_arg lthy (rty, qty) = -let - val thy = ProofContext.theory_of lthy -in - 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 SOME map_info = maps_lookup thy s - val args = map (mk_resp_arg lthy) (tys ~~ tys') - in - list_comb (Const (#relfun map_info, dummyT), args) - end - else let - val SOME qinfo = quotdata_lookup_thy thy s' - (* FIXME: check in this case that the rty and qty *) - (* FIXME: correspond to each other *) - val (s, _) = dest_Const (#rel qinfo) - (* FIXME: the relation should only be the string *) - (* FIXME: and the type needs to be calculated as below; *) - (* FIXME: maybe one should actually have a term *) - (* FIXME: and one needs to force it to have this type *) - in - Const (s, rty --> rty --> @{typ bool}) - end - | _ => HOLogic.eq_const dummyT - (* FIXME: check that the types correspond to each other? *) -end -*} - -ML {* -val mk_babs = Const (@{const_name Babs}, dummyT) -val mk_ball = Const (@{const_name Ball}, dummyT) -val mk_bex = Const (@{const_name Bex}, dummyT) -val mk_resp = Const (@{const_name Respects}, dummyT) -*} - -ML {* -(* - applies f to the subterm of an abstraction, *) -(* otherwise to the given term, *) -(* - used by regularize, therefore abstracted *) -(* variables do not have to be treated specially *) - -fun apply_subt f trm1 trm2 = - case (trm1, trm2) of - (Abs (x, T, t), Abs (x', T', t')) => Abs (x, T, f t t') - | _ => f trm1 trm2 - -(* the major type of All and Ex quantifiers *) -fun qnt_typ ty = domain_type (domain_type ty) -*} - -ML {* -(* produces a regularized version of rtrm *) -(* - the result is contains dummyT *) -(* - does not need any special treatment of *) -(* bound variables *) - -fun regularize_trm lthy rtrm qtrm = - case (rtrm, qtrm) of - (Abs (x, ty, t), Abs (x', ty', t')) => - let - val subtrm = Abs(x, ty, regularize_trm lthy t t') - in - if ty = ty' then subtrm - else mk_babs $ (mk_resp $ mk_resp_arg lthy (ty, ty')) $ subtrm - end - - | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') => - let - val subtrm = apply_subt (regularize_trm lthy) t t' - in - if ty = ty' then Const (@{const_name "All"}, ty) $ subtrm - else mk_ball $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm - end - - | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') => - let - val subtrm = apply_subt (regularize_trm lthy) t t' - 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 - - | (* equalities need to be replaced by appropriate equivalence relations *) - (Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) => - if ty = ty' then rtrm - else mk_resp_arg lthy (domain_type ty, domain_type ty') - - | (* in this case we check whether the given equivalence relation is correct *) - (rel, Const (@{const_name "op ="}, ty')) => - let - val exc = LIFT_MATCH "regularise (relation mismatch)" - val rel_ty = (fastype_of rel) handle TERM _ => raise exc - val rel' = mk_resp_arg lthy (domain_type rel_ty, domain_type ty') - in - if rel' = rel then rtrm else raise exc - end - - | (_, Const _) => - let - fun same_name (Const (s, T)) (Const (s', T')) = (s = s') (*andalso (T = T')*) - | same_name _ _ = false - (* TODO/FIXME: This test is not enough. *) - (* Why? *) - (* Because constants can have the same name but not be the same - constant. All overloaded constants have the same name but because - of different types they do differ. - - This code will let one write a theorem where plus on nat is - matched to plus on int, even if the latter is defined differently. - - This would result in hard to understand failures in injection and - cleaning. *) - (* cu: if I also test the type, then something else breaks *) - in - if same_name rtrm qtrm then rtrm - else - let - val thy = ProofContext.theory_of lthy - val qtrm_str = Syntax.string_of_term lthy qtrm - val exc1 = LIFT_MATCH ("regularize (constant " ^ qtrm_str ^ " not found)") - val exc2 = LIFT_MATCH ("regularize (constant " ^ qtrm_str ^ " mismatch)") - val rtrm' = (#rconst (qconsts_lookup thy qtrm)) handle NotFound => raise exc1 - in - if Pattern.matches thy (rtrm', rtrm) - then rtrm else raise exc2 - end - end - - | (t1 $ t2, t1' $ t2') => - (regularize_trm lthy t1 t1') $ (regularize_trm lthy t2 t2') - - | (Free (x, ty), Free (x', ty')) => - (* this case cannot arrise as we start with two fully atomized terms *) - raise (LIFT_MATCH "regularize (frees)") - - | (Bound i, Bound i') => - if i = i' then rtrm - else raise (LIFT_MATCH "regularize (bounds mismatch)") - - | _ => - let - val rtrm_str = Syntax.string_of_term lthy rtrm - val qtrm_str = Syntax.string_of_term lthy qtrm - in - raise (LIFT_MATCH ("regularize failed (default: " ^ rtrm_str ^ "," ^ qtrm_str ^ ")")) - end -*} - -section {* Regularize Tactic *} - -ML {* -fun equiv_tac ctxt = - REPEAT_ALL_NEW (resolve_tac (equiv_rules_get ctxt)) - -fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss) -val equiv_solver = Simplifier.mk_solver' "Equivalence goal solver" equiv_solver_tac -*} - -ML {* -fun prep_trm thy (x, (T, t)) = - (cterm_of thy (Var (x, T)), cterm_of thy t) - -fun prep_ty thy (x, (S, ty)) = - (ctyp_of thy (TVar (x, S)), ctyp_of thy ty) -*} - -ML {* -fun matching_prs thy pat trm = -let - 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) -in - (map (prep_ty thy) tyenv, map (prep_trm thy) tenv) -end -*} - -ML {* -fun calculate_instance ctxt thm redex R1 R2 = -let - val thy = ProofContext.theory_of ctxt - val goal = Const (@{const_name "equivp"}, dummyT) $ R2 - |> Syntax.check_term ctxt - |> HOLogic.mk_Trueprop - val eqv_prem = Goal.prove ctxt [] [] goal (fn _ => equiv_tac ctxt 1) - val thm = (@{thm eq_reflection} OF [thm OF [eqv_prem]]) - val R1c = cterm_of thy R1 - val thmi = Drule.instantiate' [] [SOME R1c] thm - val inst = matching_prs thy (term_of (Thm.lhs_of thmi)) redex - val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi) -in - SOME thm2 -end -handle _ => NONE -(* FIXME/TODO: what is the place where the exception is raised: matching_prs? *) -*} - -ML {* -fun ball_bex_range_simproc ss redex = -let - val ctxt = Simplifier.the_context ss -in - case redex of - (Const (@{const_name "Ball"}, _) $ (Const (@{const_name "Respects"}, _) $ - (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) => - calculate_instance ctxt @{thm ball_reg_eqv_range} redex R1 R2 - - | (Const (@{const_name "Bex"}, _) $ (Const (@{const_name "Respects"}, _) $ - (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) => - calculate_instance ctxt @{thm bex_reg_eqv_range} redex R1 R2 - | _ => NONE -end -*} - -lemma eq_imp_rel: - shows "equivp R \ a = b \ R a b" -by (simp add: equivp_reflp) - -ML {* -(* test whether DETERM makes any difference *) -fun quotient_tac ctxt = SOLVES' - (REPEAT_ALL_NEW (FIRST' - [rtac @{thm identity_quotient}, - resolve_tac (quotient_rules_get ctxt)])) - -fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss) -val quotient_solver = Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac -*} - -ML {* -fun solve_quotient_assum ctxt thm = - case Seq.pull (quotient_tac ctxt 1 thm) of - SOME (t, _) => t - | _ => error "solve_quotient_assum failed. Maybe a quotient_thm is missing" -*} - - -(* 0. preliminary simplification step according to *) -thm ball_reg_eqv bex_reg_eqv babs_reg_eqv - ball_reg_eqv_range bex_reg_eqv_range -(* 1. eliminating simple Ball/Bex instances*) -thm ball_reg_right bex_reg_left -(* 2. monos *) -(* 3. commutation rules for ball and bex *) -thm ball_all_comm bex_ex_comm -(* 4. then rel-equality (which need to be instantiated to avoid loops) *) -thm eq_imp_rel -(* 5. then simplification like 0 *) -(* finally jump back to 1 *) - -ML {* -fun regularize_tac ctxt = -let - val thy = ProofContext.theory_of ctxt - val pat_ball = @{term "Ball (Respects (R1 ===> R2)) P"} - val pat_bex = @{term "Bex (Respects (R1 ===> R2)) P"} - val simproc = Simplifier.simproc_i thy "" [pat_ball, pat_bex] (K (ball_bex_range_simproc)) - val simpset = (mk_minimal_ss ctxt) - addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp} - addsimprocs [simproc] addSolver equiv_solver addSolver quotient_solver - val eq_eqvs = map (OF1 @{thm eq_imp_rel}) (equiv_rules_get ctxt) -in - simp_tac simpset THEN' - REPEAT_ALL_NEW (CHANGED o FIRST' [ - resolve_tac @{thms ball_reg_right bex_reg_left}, - resolve_tac (Inductive.get_monos ctxt), - resolve_tac @{thms ball_all_comm bex_ex_comm}, - resolve_tac eq_eqvs, - simp_tac simpset]) -end -*} - -section {* Calculation of the Injected Goal *} - -(* -Injecting repabs means: - - For abstractions: - * If the type of the abstraction doesn't need lifting we recurse. - * If it does we add RepAbs around the whole term and check if the - variable needs lifting. - * If it doesn't then we recurse - * If it does we recurse and put 'RepAbs' around all occurences - of the variable in the obtained subterm. This in combination - with the RepAbs above will let us change the type of the - abstraction with rewriting. - For applications: - * If the term is 'Respects' applied to anything we leave it unchanged - * If the term needs lifting and the head is a constant that we know - how to lift, we put a RepAbs and recurse - * If the term needs lifting and the head is a free applied to subterms - (if it is not applied we treated it in Abs branch) then we - put RepAbs and recurse - * Otherwise just recurse. -*) - -ML {* -fun mk_repabs lthy (T, T') trm = - Quotient_Def.get_fun repF lthy (T, T') - $ (Quotient_Def.get_fun absF lthy (T, T') $ trm) -*} - -ML {* -(* bound variables need to be treated properly, *) -(* as the type of subterms need to be calculated *) -(* in the abstraction case *) - -fun inj_repabs_trm lthy (rtrm, qtrm) = - case (rtrm, qtrm) of - (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') => - Const (@{const_name "Ball"}, T) $ r $ (inj_repabs_trm lthy (t, t')) - - | (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') => - Const (@{const_name "Bex"}, T) $ r $ (inj_repabs_trm lthy (t, t')) - - | (Const (@{const_name "Babs"}, T) $ r $ t, t' as (Abs _)) => - let - val rty = fastype_of rtrm - val qty = fastype_of qtrm - in - mk_repabs lthy (rty, qty) (Const (@{const_name "Babs"}, T) $ r $ (inj_repabs_trm lthy (t, t'))) - end - - | (Abs (x, T, t), Abs (x', T', t')) => - let - val rty = fastype_of rtrm - val qty = fastype_of qtrm - val (y, s) = Term.dest_abs (x, T, t) - val (_, s') = Term.dest_abs (x', T', t') - val yvar = Free (y, T) - val result = Term.lambda_name (y, yvar) (inj_repabs_trm lthy (s, s')) - in - if rty = qty then result - else mk_repabs lthy (rty, qty) result - end - - | (t $ s, t' $ s') => - (inj_repabs_trm lthy (t, t')) $ (inj_repabs_trm lthy (s, s')) - - | (Free (_, T), Free (_, T')) => - if T = T' then rtrm - else mk_repabs lthy (T, T') rtrm - - | (_, Const (@{const_name "op ="}, _)) => rtrm - - | (_, Const (_, T')) => - let - val rty = fastype_of rtrm - in - if rty = T' then rtrm - else mk_repabs lthy (rty, T') rtrm - end - - | _ => raise (LIFT_MATCH "injection") -*} - -section {* Injection Tactic *} - -definition - "QUOT_TRUE x \ True" - -ML {* -(* looks for QUOT_TRUE assumtions, and in case its argument *) -(* is an application, it returns the function and the argument *) -fun find_qt_asm asms = -let - fun find_fun trm = - case trm of - (Const(@{const_name Trueprop}, _) $ (Const (@{const_name QUOT_TRUE}, _) $ _)) => true - | _ => false -in - case find_first find_fun asms of - SOME (_ $ (_ $ (f $ a))) => SOME (f, a) - | _ => NONE -end -*} - -text {* -To prove that the regularised theorem implies the abs/rep injected, -we try: - - 1) theorems 'trans2' from the appropriate QUOT_TYPE - 2) remove lambdas from both sides: lambda_rsp_tac - 3) remove Ball/Bex from the right hand side - 4) use user-supplied RSP theorems - 5) remove rep_abs from the right side - 6) reflexivity of equality - 7) split applications of lifted type (apply_rsp) - 8) split applications of non-lifted type (cong_tac) - 9) apply extentionality - A) reflexivity of the relation - B) assumption - (Lambdas under respects may have left us some assumptions) - C) proving obvious higher order equalities by simplifying fun_rel - (not sure if it is still needed?) - D) unfolding lambda on one side - E) simplifying (= ===> =) for simpler respectfulness -*} - -lemma quot_true_dests: - shows QT_all: "QUOT_TRUE (All P) \ QUOT_TRUE P" - and QT_ex: "QUOT_TRUE (Ex P) \ QUOT_TRUE P" - and QT_lam: "QUOT_TRUE (\x. P x) \ (\x. QUOT_TRUE (P x))" - and QT_ext: "(\x. QUOT_TRUE (a x) \ f x = g x) \ (QUOT_TRUE a \ f = g)" -by (simp_all add: QUOT_TRUE_def ext) - -lemma QUOT_TRUE_imp: "QUOT_TRUE a \ QUOT_TRUE b" -by (simp add: QUOT_TRUE_def) - -lemma regularize_to_injection: "(QUOT_TRUE l \ y) \ (l = r) \ y" - by(auto simp add: QUOT_TRUE_def) - -ML {* -fun quot_true_simple_conv ctxt fnctn ctrm = - case (term_of ctrm) of - (Const (@{const_name QUOT_TRUE}, _) $ x) => - let - val fx = fnctn x; - val thy = ProofContext.theory_of ctxt; - val cx = cterm_of thy x; - val cfx = cterm_of thy fx; - val cxt = ctyp_of thy (fastype_of x); - val cfxt = ctyp_of thy (fastype_of fx); - val thm = Drule.instantiate' [SOME cxt, SOME cfxt] [SOME cx, SOME cfx] @{thm QUOT_TRUE_imp} - in - Conv.rewr_conv thm ctrm - end -*} - -ML {* -fun quot_true_conv ctxt fnctn ctrm = - case (term_of ctrm) of - (Const (@{const_name QUOT_TRUE}, _) $ _) => - quot_true_simple_conv ctxt fnctn ctrm - | _ $ _ => Conv.comb_conv (quot_true_conv ctxt fnctn) ctrm - | Abs _ => Conv.abs_conv (fn (_, ctxt) => quot_true_conv ctxt fnctn) ctxt ctrm - | _ => Conv.all_conv ctrm -*} - -ML {* -fun quot_true_tac ctxt fnctn = - CONVERSION - ((Conv.params_conv ~1 (fn ctxt => - (Conv.prems_conv ~1 (quot_true_conv ctxt fnctn)))) ctxt) -*} - -ML {* fun dest_comb (f $ a) = (f, a) *} -ML {* fun dest_bcomb ((_ $ l) $ r) = (l, r) *} -(* TODO: Can this be done easier? *) -ML {* -fun unlam t = - case t of - (Abs a) => snd (Term.dest_abs a) - | _ => unlam (Abs("", domain_type (fastype_of t), (incr_boundvars 1 t) $ (Bound 0))) -*} - -ML {* -fun dest_fun_type (Type("fun", [T, S])) = (T, S) - | dest_fun_type _ = error "dest_fun_type" -*} - -ML {* -val bare_concl = HOLogic.dest_Trueprop o Logic.strip_assums_concl -*} - -ML {* -(* we apply apply_rsp only in case if the type needs lifting, *) -(* which is the case if the type of the data in the QUOT_TRUE *) -(* assumption is different from the corresponding type in the goal *) -val apply_rsp_tac = - Subgoal.FOCUS (fn {concl, asms, context,...} => - let - val bare_concl = HOLogic.dest_Trueprop (term_of concl) - val qt_asm = find_qt_asm (map term_of asms) - in - case (bare_concl, qt_asm) of - (R2 $ (f $ x) $ (g $ y), SOME (qt_fun, qt_arg)) => - if (fastype_of qt_fun) = (fastype_of f) - then no_tac - else - let - val ty_x = fastype_of x - val ty_b = fastype_of qt_arg - val ty_f = range_type (fastype_of f) - val thy = ProofContext.theory_of context - val ty_inst = map (SOME o (ctyp_of thy)) [ty_x, ty_b, ty_f] - val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y]; - val inst_thm = Drule.instantiate' ty_inst ([NONE, NONE, NONE] @ t_inst) @{thm apply_rsp} - in - (rtac inst_thm THEN' quotient_tac context) 1 - end - | _ => no_tac - end) -*} - -thm equals_rsp - -ML {* -fun equals_rsp_tac R ctxt = -let - val ty = domain_type (fastype_of R); - val thy = ProofContext.theory_of ctxt - val thm = Drule.instantiate' - [SOME (ctyp_of thy ty)] [SOME (cterm_of thy R)] @{thm equals_rsp} -in - rtac thm THEN' quotient_tac ctxt -end -(* raised by instantiate' *) -handle THM _ => K no_tac - | TYPE _ => K no_tac - | TERM _ => K no_tac -*} - -ML {* -fun rep_abs_rsp_tac ctxt = - SUBGOAL (fn (goal, i) => - case (bare_concl goal) of - (rel $ _ $ (rep $ (abs $ _))) => - (let - val thy = ProofContext.theory_of ctxt; - val (ty_a, ty_b) = dest_fun_type (fastype_of abs); - val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b]; - val t_inst = map (SOME o (cterm_of thy)) [rel, abs, rep]; - val inst_thm = Drule.instantiate' ty_inst t_inst @{thm rep_abs_rsp} - in - (rtac inst_thm THEN' quotient_tac ctxt) i - end - handle THM _ => no_tac | TYPE _ => no_tac) - | _ => no_tac) -*} - -ML {* -fun inj_repabs_tac_match ctxt = SUBGOAL (fn (goal, i) => -(case (bare_concl goal) of - (* (R1 ===> R2) (\x\) (\y\) ----> \R1 x y\ \ R2 (\x) (\y) *) - (Const (@{const_name fun_rel}, _) $ _ $ _) $ (Abs _) $ (Abs _) - => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam - - (* (op =) (Ball\) (Ball\) ----> (op =) (\) (\) *) -| (Const (@{const_name "op ="},_) $ - (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ - (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _)) - => rtac @{thm ball_rsp} THEN' dtac @{thm QT_all} - - (* (R1 ===> op =) (Ball\) (Ball\) ----> \R1 x y\ \ (Ball\x) = (Ball\y) *) -| (Const (@{const_name fun_rel}, _) $ _ $ _) $ - (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ - (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) - => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam - - (* (op =) (Bex\) (Bex\) ----> (op =) (\) (\) *) -| Const (@{const_name "op ="},_) $ - (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ - (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) - => rtac @{thm bex_rsp} THEN' dtac @{thm QT_ex} - - (* (R1 ===> op =) (Bex\) (Bex\) ----> \R1 x y\ \ (Bex\x) = (Bex\y) *) -| (Const (@{const_name fun_rel}, _) $ _ $ _) $ - (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ - (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) - => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam - -| (_ $ - (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ - (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _)) - => rtac @{thm babs_rsp} THEN' RANGE [quotient_tac ctxt] - -| Const (@{const_name "op ="},_) $ (R $ _ $ _) $ (_ $ _ $ _) => - (rtac @{thm refl} ORELSE' - (equals_rsp_tac R ctxt THEN' RANGE [ - quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)])) - - (* reflexivity of operators arising from Cong_tac *) -| Const (@{const_name "op ="},_) $ _ $ _ => rtac @{thm refl} - - (* respectfulness of constants; in particular of a simple relation *) -| _ $ (Const _) $ (Const _) (* fun_rel, list_rel, etc but not equality *) - => resolve_tac (rsp_rules_get ctxt) THEN_ALL_NEW quotient_tac ctxt - - (* R (\) (Rep (Abs \)) ----> R (\) (\) *) - (* observe ---> *) -| _ $ _ $ _ - => (rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt) - ORELSE' rep_abs_rsp_tac ctxt - -| _ => K no_tac -) i) -*} - -ML {* -fun inj_repabs_step_tac ctxt rel_refl = - (FIRST' [ - inj_repabs_tac_match ctxt, - (* R (t $ \) (t' $ \) ----> apply_rsp provided type of t needs lifting *) - - apply_rsp_tac ctxt THEN' - RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)], - - (* (op =) (t $ \) (t' $ \) ----> Cong provided type of t does not need lifting *) - (* merge with previous tactic *) - Cong_Tac.cong_tac @{thm cong} THEN' - RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)], - - (* (op =) (\x\) (\x\) ----> (op =) (\) (\) *) - rtac @{thm ext} THEN' quot_true_tac ctxt unlam, - - (* resolving with R x y assumptions *) - atac, - - (* reflexivity of the basic relations *) - (* R \ \ *) - resolve_tac rel_refl]) -*} - -ML {* -fun inj_repabs_tac ctxt = -let - val rel_refl = map (OF1 @{thm equivp_reflp}) (equiv_rules_get ctxt) -in - inj_repabs_step_tac ctxt rel_refl -end - -fun all_inj_repabs_tac ctxt = - REPEAT_ALL_NEW (inj_repabs_tac ctxt) -*} - -section {* Cleaning of the Theorem *} - -ML {* -(* expands all fun_maps, except in front of bound variables *) - -fun fun_map_simple_conv xs ctxt ctrm = - case (term_of ctrm) of - ((Const (@{const_name "fun_map"}, _) $ _ $ _) $ h $ _) => - if (member (op=) xs h) - then Conv.all_conv ctrm - else Conv.rewr_conv @{thm fun_map.simps[THEN eq_reflection]} ctrm - | _ => Conv.all_conv ctrm - -fun fun_map_conv xs ctxt ctrm = - case (term_of ctrm) of - _ $ _ => (Conv.comb_conv (fun_map_conv xs ctxt) then_conv - fun_map_simple_conv xs ctxt) ctrm - | Abs _ => Conv.abs_conv (fn (x, ctxt) => fun_map_conv ((term_of x)::xs) ctxt) ctxt ctrm - | _ => Conv.all_conv ctrm - -fun fun_map_tac ctxt = CONVERSION (fun_map_conv [] ctxt) -*} - -ML {* -fun mk_abs u i t = - if incr_boundvars i u aconv t then Bound i - else (case t of - t1 $ t2 => (mk_abs u i t1) $ (mk_abs u i t2) - | Abs (s, T, t') => Abs (s, T, mk_abs u (i + 1) t') - | Bound j => if i = j then error "make_inst" else t - | _ => t) - -fun make_inst lhs t = -let - val _ $ (Abs (_, _, (_ $ ((f as Var (_, Type ("fun", [T, _]))) $ u)))) = lhs; - val _ $ (Abs (_, _, (_ $ g))) = t; -in - (f, Abs ("x", T, mk_abs u 0 g)) -end - -fun make_inst_id lhs t = -let - val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs; - val _ $ (Abs (_, _, g)) = t; -in - (f, Abs ("x", T, mk_abs u 0 g)) -end -*} - -ML {* -(* Simplifies a redex using the 'lambda_prs' theorem. *) -(* First instantiates the types and known subterms. *) -(* Then solves the quotient assumptions to get Rep2 and Abs1 *) -(* Finally instantiates the function f using make_inst *) -(* If Rep2 is identity then the pattern is simpler and make_inst_id is used *) -fun lambda_prs_simple_conv ctxt ctrm = - case (term_of ctrm) of - (Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _) => - (let - val thy = ProofContext.theory_of ctxt - val (ty_b, ty_a) = dest_fun_type (fastype_of r1) - val (ty_c, ty_d) = dest_fun_type (fastype_of a2) - val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d] - val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)] - val lpi = Drule.instantiate' tyinst tinst @{thm lambda_prs} - val te = @{thm eq_reflection} OF [solve_quotient_assum ctxt (solve_quotient_assum ctxt lpi)] - val ts = MetaSimplifier.rewrite_rule (id_simps_get ctxt) te - val make_inst = if ty_c = ty_d then make_inst_id else make_inst - val (insp, inst) = make_inst (term_of (Thm.lhs_of ts)) (term_of ctrm) - val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts - in - Conv.rewr_conv ti ctrm - end - handle _ => Conv.all_conv ctrm) - | _ => Conv.all_conv ctrm -*} - -ML {* -val lambda_prs_conv = - More_Conv.top_conv lambda_prs_simple_conv - -fun lambda_prs_tac ctxt = CONVERSION (lambda_prs_conv ctxt) -*} - -(* 1. folding of definitions and preservation lemmas; *) -(* and simplification with *) -thm babs_prs all_prs ex_prs -(* 2. unfolding of ---> in front of everything, except *) -(* bound variables (this prevents lambda_prs from *) -(* becoming stuck *) -thm fun_map.simps -(* 3. simplification with *) -thm lambda_prs -(* 4. simplification with *) -thm Quotient_abs_rep Quotient_rel_rep id_simps -(* 5. Test for refl *) - -ML {* -fun clean_tac lthy = - let - val thy = ProofContext.theory_of lthy; - val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy) - (* FIXME: why is the Thm.varifyT needed: example where it fails is LamEx *) - - val thms1 = defs @ (prs_rules_get lthy) @ @{thms babs_prs all_prs ex_prs} - val thms2 = @{thms Quotient_abs_rep Quotient_rel_rep} @ (id_simps_get lthy) - fun simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver - in - EVERY' [simp_tac (simps thms1), - fun_map_tac lthy, - lambda_prs_tac lthy, - simp_tac (simps thms2), - TRY o rtac refl] - end -*} - -section {* Tactic for Genralisation of Free Variables in a Goal *} - -ML {* -fun inst_spec ctrm = - Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec} - -fun inst_spec_tac ctrms = - EVERY' (map (dtac o inst_spec) ctrms) - -fun all_list xs trm = - fold (fn (x, T) => fn t' => HOLogic.mk_all (x, T, t')) xs trm - -fun apply_under_Trueprop f = - HOLogic.dest_Trueprop #> f #> HOLogic.mk_Trueprop - -fun gen_frees_tac ctxt = - SUBGOAL (fn (concl, i) => - let - val thy = ProofContext.theory_of ctxt - val vrs = Term.add_frees concl [] - val cvrs = map (cterm_of thy o Free) vrs - val concl' = apply_under_Trueprop (all_list vrs) concl - val goal = Logic.mk_implies (concl', concl) - val rule = Goal.prove ctxt [] [] goal - (K (EVERY1 [inst_spec_tac (rev cvrs), atac])) - in - rtac rule i - end) -*} - -section {* The General Shape of the Lifting Procedure *} - -(* - A is the original raw theorem *) -(* - B is the regularized theorem *) -(* - C is the rep/abs injected version of B *) -(* - D is the lifted theorem *) -(* *) -(* - 1st prem is the regularization step *) -(* - 2nd prem is the rep/abs injection step *) -(* - 3rd prem is the cleaning part *) -(* *) -(* the QUOT_TRUE premise in 2 records the lifted theorem *) - -ML {* -val lifting_procedure = - @{lemma "\A; - A \ B; - QUOT_TRUE D \ B = C; - C = D\ \ D" - by (simp add: QUOT_TRUE_def)} -*} - -ML {* -fun lift_match_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 = cat_lines [enclose "[" "]" fun_str, "The quotient theorem", qtrm_str, - "", "does not match with original theorem", rtrm_str] -in - error msg -end -*} - -ML {* -fun procedure_inst ctxt rtrm qtrm = -let - val thy = ProofContext.theory_of ctxt - 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_match_error ctxt s rtrm qtrm - val inj_goal = - Syntax.check_term ctxt (inj_repabs_trm ctxt (reg_goal, qtrm')) - handle (LIFT_MATCH s) => lift_match_error ctxt s rtrm qtrm -in - Drule.instantiate' [] - [SOME (cterm_of thy rtrm'), - SOME (cterm_of thy reg_goal), - NONE, - SOME (cterm_of thy inj_goal)] lifting_procedure -end -*} - -ML {* -(* the tactic leaves three subgoals to be proved *) -fun procedure_tac ctxt rthm = - ObjectLogic.full_atomize_tac - THEN' gen_frees_tac ctxt - THEN' CSUBGOAL (fn (goal, i) => - let - val rthm' = atomize_thm rthm - val rule = procedure_inst ctxt (prop_of rthm') (term_of goal) - in - (rtac rule THEN' rtac rthm') i - end) -*} - -section {* Automatic Proofs *} - - -ML {* -local - -val msg1 = "Regularize proof failed." -val msg2 = cat_lines ["Injection proof failed.", - "This is probably due to missing respects lemmas.", - "Try invoking the injection method manually to see", - "which lemmas are missing."] -val msg3 = "Cleaning proof failed." - -in - -fun lift_tac ctxt rthm = - procedure_tac ctxt rthm - THEN' RANGE_WARN - [(regularize_tac ctxt, msg1), - (all_inj_repabs_tac ctxt, msg2), - (clean_tac ctxt, msg3)] - -end -*} - section {* Methods / Interface *} ML {* @@ -1084,23 +175,23 @@ *} method_setup lifting = - {* Attrib.thm >> (mk_method1 lift_tac) *} + {* Attrib.thm >> (mk_method1 Quotient_Tacs.lift_tac) *} {* Lifting of theorems to quotient types. *} method_setup lifting_setup = - {* Attrib.thm >> (mk_method1 procedure_tac) *} + {* Attrib.thm >> (mk_method1 Quotient_Tacs.procedure_tac) *} {* Sets up the three goals for the lifting procedure. *} method_setup regularize = - {* Scan.succeed (mk_method2 regularize_tac) *} + {* Scan.succeed (mk_method2 Quotient_Tacs.regularize_tac) *} {* Proves automatically the regularization goals from the lifting procedure. *} method_setup injection = - {* Scan.succeed (mk_method2 all_inj_repabs_tac) *} + {* Scan.succeed (mk_method2 Quotient_Tacs.all_inj_repabs_tac) *} {* Proves automatically the rep/abs injection goals from the lifting procedure. *} method_setup cleaning = - {* Scan.succeed (mk_method2 clean_tac) *} + {* Scan.succeed (mk_method2 Quotient_Tacs.clean_tac) *} {* Proves automatically the cleaning goals from the lifting procedure. *} end