# HG changeset patch # User Christian Urban # Date 1263370760 -3600 # Node ID 433f7c17255f6bd3936a4535faa578e6d3dc2e79 # Parent 017cb46b27bb67bd7dd754adb26f46c928bd5e1c# Parent 3fd1365f57295c58b66603a72799dc7fad3d9fea merged diff -r 017cb46b27bb -r 433f7c17255f Quot/Examples/AbsRepTest.thy --- a/Quot/Examples/AbsRepTest.thy Wed Jan 13 00:46:31 2010 +0100 +++ b/Quot/Examples/AbsRepTest.thy Wed Jan 13 09:19:20 2010 +0100 @@ -145,9 +145,8 @@ lemma quotient_compose_list_gen_pre: assumes a: "equivp r2" and b: "Quotient r2 abs2 rep2" - shows "(list_rel r2 OO op \1 OO list_rel r2) r s = - ((list_rel r2 OO op \1 OO list_rel r2) r r \ - (list_rel r2 OO op \1 OO list_rel r2) s s \ + shows "(list_rel r2 OOO op \1) r s = + ((list_rel r2 OOO op \1) r r \ (list_rel r2 OOO op \1) s s \ abs_fset (map abs2 r) = abs_fset (map abs2 s))" apply rule apply rule @@ -199,7 +198,7 @@ lemma quotient_compose_list_gen: assumes a: "Quotient r2 abs2 rep2" and b: "equivp r2" (* reflp is not enough *) - shows "Quotient ((list_rel r2) OO (op \1) OO (list_rel r2)) + shows "Quotient ((list_rel r2) OOO (op \1)) (abs_fset \ (map abs2)) ((map rep2) \ rep_fset)" unfolding Quotient_def comp_def apply (rule)+ @@ -223,7 +222,7 @@ lemma quotient_compose_general: assumes a2: "Quotient r1 abs1 rep1" and "Quotient r2 abs2 rep2" - shows "Quotient ((list_rel r2) OO r1 OO (list_rel r2)) + shows "Quotient ((list_rel r2) OOO r1) (abs1 \ (map abs2)) ((map rep2) \ rep1)" sorry diff -r 017cb46b27bb -r 433f7c17255f Quot/Examples/FSet3.thy --- a/Quot/Examples/FSet3.thy Wed Jan 13 00:46:31 2010 +0100 +++ b/Quot/Examples/FSet3.thy Wed Jan 13 09:19:20 2010 +0100 @@ -254,10 +254,10 @@ by (simp add: id_simps) lemma concat_rsp[quot_respect]: - shows "(list_rel op \ OO op \ OO list_rel op \ ===> op \) concat concat" + shows "(list_rel op \ OOO op \ ===> op \) concat concat" sorry -lemma nil_rsp2[quot_respect]: "(list_rel op \ OO op \ OO list_rel op \) [] []" +lemma nil_rsp2[quot_respect]: "(list_rel op \ OOO op \) [] []" apply (metis FSet3.nil_rsp list_rel.simps(1) pred_comp.intros) done @@ -272,9 +272,8 @@ done lemma quotient_compose_list_pre: - "(list_rel op \ OO op \ OO list_rel op \) r s = - ((list_rel op \ OO op \ OO list_rel op \) r r \ - (list_rel op \ OO op \ OO list_rel op \) s s \ + "(list_rel op \ OOO op \) r s = + ((list_rel op \ OOO op \) r r \ (list_rel op \ OOO op \) s s \ abs_fset (map abs_fset r) = abs_fset (map abs_fset s))" apply rule apply rule @@ -323,8 +322,8 @@ done lemma quotient_compose_list[quot_thm]: - shows "Quotient ((list_rel op \) OO (op \) OO (list_rel op \)) - (abs_fset \ (map abs_fset)) ((map rep_fset) \ rep_fset)" + shows "Quotient ((list_rel op \) OOO (op \)) + (abs_fset \ (map abs_fset)) ((map rep_fset) \ rep_fset)" unfolding Quotient_def comp_def apply (rule)+ apply (simp add: abs_o_rep[OF Quotient_fset] id_simps Quotient_abs_rep[OF Quotient_fset]) @@ -354,7 +353,7 @@ (* Should be true *) lemma insert_rsp2[quot_respect]: - "(op \ ===> list_rel op \ OO op \ OO list_rel op \ ===> list_rel op \ OO op \ OO list_rel op \) op # op #" + "(op \ ===> list_rel op \ OOO op \ ===> list_rel op \ OOO op \) op # op #" apply auto apply (simp add: set_in_eq) sorry diff -r 017cb46b27bb -r 433f7c17255f Quot/quotient_def.ML --- a/Quot/quotient_def.ML Wed Jan 13 00:46:31 2010 +0100 +++ b/Quot/quotient_def.ML Wed Jan 13 09:19:20 2010 +0100 @@ -24,17 +24,17 @@ end -(* interface and syntax setup *) +(** interface and syntax setup **) + +(* the ML-interface takes -(* the ML-interface takes a 4-tuple consisting of *) -(* *) -(* - the mixfix annotation *) -(* - name and attributes *) -(* - the new constant as term *) -(* - the rhs of the definition as term *) -(* *) -(* it returns the defined constant and its definition *) -(* theorem; stores the data in the qconsts slot *) + - the mixfix annotation + - name and attributes + - the new constant as term + - the rhs of the definition as term + + it returns the defined constant and its definition + theorem; stores the data in the qconsts slot *) fun quotient_def mx attr lhs rhs lthy = let diff -r 017cb46b27bb -r 433f7c17255f Quot/quotient_info.ML --- a/Quot/quotient_info.ML Wed Jan 13 00:46:31 2010 +0100 +++ b/Quot/quotient_info.ML Wed Jan 13 09:19:20 2010 +0100 @@ -65,9 +65,8 @@ exception NotFound -(*******************) -(* data containers *) -(*******************) + +(** data containers **) (* info about map- and rel-functions for a type *) type maps_info = {mapfun: string, relmap: string} diff -r 017cb46b27bb -r 433f7c17255f Quot/quotient_tacs.ML --- a/Quot/quotient_tacs.ML Wed Jan 13 00:46:31 2010 +0100 +++ b/Quot/quotient_tacs.ML Wed Jan 13 09:19:20 2010 +0100 @@ -1,13 +1,13 @@ signature QUOTIENT_TACS = sig - val regularize_tac: Proof.context -> int -> tactic - val injection_tac: Proof.context -> int -> tactic - val all_injection_tac: Proof.context -> int -> tactic - val clean_tac: Proof.context -> int -> tactic - val procedure_tac: Proof.context -> thm -> int -> tactic - val lift_tac: Proof.context -> thm -> int -> tactic - val quotient_tac: Proof.context -> int -> tactic - val quot_true_tac: Proof.context -> (term -> term) -> int -> tactic + val regularize_tac: Proof.context -> int -> tactic + val injection_tac: Proof.context -> int -> tactic + val all_injection_tac: Proof.context -> int -> tactic + val clean_tac: Proof.context -> int -> tactic + val procedure_tac: Proof.context -> thm -> int -> tactic + val lift_tac: Proof.context -> thm -> int -> tactic + val quotient_tac: Proof.context -> int -> tactic + val quot_true_tac: Proof.context -> (term -> term) -> int -> tactic end; structure Quotient_Tacs: QUOTIENT_TACS = @@ -16,7 +16,8 @@ open Quotient_Info; open Quotient_Term; -(* various helper fuctions *) + +(** various helper fuctions **) (* Since HOL_basic_ss is too "big" for us, we *) (* need to set up our own minimal simpset. *) @@ -48,14 +49,14 @@ end -(*********************) -(* Regularize Tactic *) -(*********************) + +(*** Regularize Tactic ***) -(* solvers for equivp and quotient assumptions *) +(** solvers for equivp and quotient assumptions **) + (* FIXME / TODO: should this SOLVES' the goal, like with quotient_tac? *) (* FIXME / TODO: none of te examples break if added *) -fun equiv_tac ctxt = +fun equiv_tac ctxt = REPEAT_ALL_NEW (resolve_tac (equiv_rules_get ctxt)) fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss) @@ -63,13 +64,14 @@ (* FIXME / TODO: test whether DETERM makes any runtime-difference *) (* FIXME / TODO: reason: the tactic might back-track over the two alternatives in FIRST' *) -fun quotient_tac ctxt = SOLVES' +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 +val quotient_solver = + Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac fun solve_quotient_assm ctxt thm = case Seq.pull (quotient_tac ctxt 1 thm) of @@ -86,7 +88,7 @@ fun get_match_inst thy pat trm = let val univ = Unify.matchers thy [(pat, trm)] - val SOME (env, _) = Seq.pull univ (* raises BIND, if no unifier *) + val SOME (env, _) = Seq.pull univ (* raises BIND, if no unifier *) val tenv = Vartab.dest (Envir.term_env env) val tyenv = Vartab.dest (Envir.type_env env) in @@ -130,27 +132,22 @@ | _ => NONE end -(* 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-equalities, which need to be *) -(* instantiated with the followig theorem *) -(* to avoid loops: *) -(* thm eq_imp_rel *) -(* *) -(* 5. then simplification like 0 *) -(* *) -(* finally jump back to 1 *) +(* +0. preliminary simplification step according to + ball_reg_eqv bex_reg_eqv babs_reg_eqv ball_reg_eqv_range bex_reg_eqv_range + +1. eliminating simple Ball/Bex instances (ball_reg_right bex_reg_left) + +2. monos +3. commutation rules for ball and bex (ball_all_comm bex_ex_comm) + +4. then rel-equalities, which need to be instantiated with 'eq_imp_rel' + to avoid loops + +5. then simplification like 0 + +finally jump back to 1 *) fun regularize_tac ctxt = let val thy = ProofContext.theory_of ctxt @@ -158,7 +155,7 @@ val bex_pat = @{term "Bex (Respects (R1 ===> R2)) P"} val simproc = Simplifier.simproc_i thy "" [ball_pat, bex_pat] (K (ball_bex_range_simproc)) val simpset = (mk_minimal_ss ctxt) - addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp} @ (id_simps_get 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) @@ -173,12 +170,11 @@ end -(********************) -(* Injection Tactic *) -(********************) + +(*** Injection Tactic ***) -(* Looks for Quot_True assumtions, and in case its parameter *) -(* is an application, it returns the function and the argument. *) +(* Looks for Quot_True assumtions, and in case its parameter + is an application, it returns the function and the argument. *) fun find_qt_asm asms = let fun find_fun trm = @@ -232,9 +228,9 @@ val bare_concl = HOLogic.dest_Trueprop o Logic.strip_assums_concl -(* We apply apply_rsp only in case if the type needs lifting. *) -(* This is the case if the type of the data in the Quot_True *) -(* assumption is different from the corresponding type in the goal. *) +(* We apply apply_rsp only in case if the type needs lifting. + This 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 @@ -243,17 +239,18 @@ 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 + 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 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} + 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 @@ -281,44 +278,45 @@ (* TODO: Again, can one specify more concretely *) (* TODO: in terms of R when no_tac should be returned? *) -fun rep_abs_rsp_tac ctxt = +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) (* TODO: same here *) + case (try bare_concl goal) of + SOME (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]; + in + case try (map (SOME o (cterm_of thy))) [rel, abs, rep] of + SOME t_inst => + (case try (Drule.instantiate' ty_inst t_inst) @{thm rep_abs_rsp} of + SOME inst_thm => (rtac inst_thm THEN' quotient_tac ctxt) i + | NONE => no_tac) + | NONE => no_tac + end | _ => no_tac) -(* FIXME / TODO needs to be adapted *) (* -To prove that the regularised theorem implies the abs/rep injected, +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 + The deterministic part: + -) remove lambdas from both sides + -) prove Ball/Bex/Babs equalities using ball_rsp, bex_rsp, babs_rsp + -) prove Ball/Bex relations unfolding fun_rel_id + -) reflexivity of equality + -) prove equality of relations using equals_rsp + -) use user-supplied RSP theorems + -) solve 'relation of relations' goals using quot_rel_rsp + -) remove rep_abs from the right side (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 + Then in order: + -) split applications of lifted type (apply_rsp) + -) split applications of non-lifted type (cong_tac) + -) apply extentionality + -) assumption + -) reflexivity of the relation *) @@ -382,7 +380,7 @@ FIRST' [ injection_match_tac ctxt, - (* R (t $ ...) (t' $ ...) ----> apply_rsp provided type of t needs lifting *) + (* 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)], @@ -390,13 +388,13 @@ (* 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...) (%y...) ----> (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] @@ -405,24 +403,21 @@ let val rel_refl = map (OF1 @{thm equivp_reflp}) (equiv_rules_get ctxt) in - simp_tac ((mk_minimal_ss ctxt) addsimps (id_simps_get ctxt)) (* HACK? *) - THEN' injection_step_tac ctxt rel_refl + injection_step_tac ctxt rel_refl end fun all_injection_tac ctxt = REPEAT_ALL_NEW (injection_tac ctxt) -(***************************) -(* Cleaning of the Theorem *) -(***************************) -(* expands all fun_maps, except in front of the bound *) -(* variables listed in xs *) +(** Cleaning of the Theorem **) + +(* expands all fun_maps, except in front of the bound variables listed in xs *) fun fun_map_simple_conv xs ctrm = case (term_of ctrm) of ((Const (@{const_name "fun_map"}, _) $ _ $ _) $ h $ _) => - if (member (op=) xs 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 @@ -461,58 +456,52 @@ (f, Abs ("x", T, mk_abs u 0 g)) end -(* 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 an identity then the pattern is simpler and *) -(* make_inst_id is used *) +(* 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 an 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[THEN eq_reflection]} - val te = solve_quotient_assm ctxt (solve_quotient_assm ctxt lpi) - val ts = MetaSimplifier.rewrite_rule (id_simps_get ctxt) te - val (insp, inst) = - if ty_c = ty_d - then make_inst_id (term_of (Thm.lhs_of ts)) (term_of ctrm) - else 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) (* TODO: another catch all - can this be improved? *) + (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[THEN eq_reflection]} + val te = solve_quotient_assm ctxt (solve_quotient_assm ctxt lpi) + val ts = MetaSimplifier.rewrite_rule (id_simps_get ctxt) te + val (insp, inst) = + if ty_c = ty_d + then make_inst_id (term_of (Thm.lhs_of ts)) (term_of ctrm) + else 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 | _ => Conv.all_conv ctrm - fun lambda_prs_conv ctxt = More_Conv.top_conv lambda_prs_simple_conv ctxt 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 *) +(* Cleaning consists of: + 1. folding of definitions and preservation lemmas; + and simplification with babs_prs all_prs ex_prs -fun clean_tac_aux lthy = + 2. unfolding of ---> in front of everything, except + bound variables + (this prevents lambda_prs from becoming stuck) + + 3. simplification with lambda_prs + + 4. simplification with Quotient_abs_rep Quotient_rel_rep id_simps + + 5. test for refl *) +fun clean_tac lthy = let (* FIXME/TODO produce defs with lthy, like prs and ids *) val thy = ProofContext.theory_of lthy; @@ -520,24 +509,22 @@ (* FIXME: why is the Thm.varifyT needed: example where it fails is LamEx *) val prs = prs_rules_get lthy val ids = id_simps_get lthy - + fun mk_simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver val ss1 = mk_simps (defs @ prs @ @{thms babs_prs all_prs ex_prs}) - val ss2 = mk_simps (@{thms Quotient_abs_rep Quotient_rel_rep} @ ids) + val ss2 = mk_simps (@{thms Quotient_abs_rep Quotient_rel_rep} @ ids) in EVERY' [simp_tac ss1, fun_map_tac lthy, lambda_prs_tac lthy, simp_tac ss2, - TRY o rtac refl] + TRY o rtac refl] end -fun clean_tac lthy = REPEAT o CHANGED o (clean_tac_aux lthy) (* HACK?? *) -(****************************************************) -(* Tactic for Generalising Free Variables in a Goal *) -(****************************************************) +(** Tactic for Generalising Free Variables in a Goal **) + fun inst_spec ctrm = Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec} @@ -552,39 +539,38 @@ 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) + 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) -(**********************************************) -(* The General Shape of the Lifting Procedure *) -(**********************************************) + +(** 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 2nd records the lifted theorem *) + +(* - 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 -val lifting_procedure_thm = - @{lemma "[|A; - A --> B; - Quot_True D ==> B = C; - C = D|] ==> D" + - 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 2nd records the lifted theorem *) +val lifting_procedure_thm = + @{lemma "[|A; + A --> B; + Quot_True D ==> B = C; + C = D|] ==> D" by (simp add: Quot_True_def)} fun lift_match_error ctxt str rtrm qtrm = @@ -592,20 +578,20 @@ val rtrm_str = Syntax.string_of_term ctxt rtrm val qtrm_str = Syntax.string_of_term ctxt qtrm val msg = cat_lines [enclose "[" "]" str, "The quotient theorem", qtrm_str, - "", "does not match with original theorem", rtrm_str] + "", "does not match with original theorem", rtrm_str] in error msg end - + 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 = regularize_trm_chk ctxt (rtrm', qtrm') - handle (LIFT_MATCH str) => lift_match_error ctxt str rtrm qtrm + handle (LIFT_MATCH str) => lift_match_error ctxt str rtrm qtrm val inj_goal = inj_repabs_trm_chk ctxt (reg_goal, qtrm') - handle (LIFT_MATCH str) => lift_match_error ctxt str rtrm qtrm + handle (LIFT_MATCH str) => lift_match_error ctxt str rtrm qtrm in Drule.instantiate' [] [SOME (cterm_of thy rtrm'), diff -r 017cb46b27bb -r 433f7c17255f Quot/quotient_term.ML --- a/Quot/quotient_term.ML Wed Jan 13 00:46:31 2010 +0100 +++ b/Quot/quotient_term.ML Wed Jan 13 09:19:20 2010 +0100 @@ -1,20 +1,20 @@ signature QUOTIENT_TERM = sig - exception LIFT_MATCH of string - - datatype flag = absF | repF - - val absrep_fun: flag -> Proof.context -> (typ * typ) -> term - val absrep_fun_chk: flag -> Proof.context -> (typ * typ) -> term + exception LIFT_MATCH of string + + datatype flag = absF | repF + + val absrep_fun: flag -> Proof.context -> typ * typ -> term + val absrep_fun_chk: flag -> Proof.context -> typ * typ -> term - val equiv_relation: Proof.context -> (typ * typ) -> term - val equiv_relation_chk: Proof.context -> (typ * typ) -> term + val equiv_relation: Proof.context -> typ * typ -> term + val equiv_relation_chk: Proof.context -> typ * typ -> term - val regularize_trm: Proof.context -> (term * term) -> term - val regularize_trm_chk: Proof.context -> (term * term) -> term - - val inj_repabs_trm: Proof.context -> (term * term) -> term - val inj_repabs_trm_chk: Proof.context -> (term * term) -> term + val regularize_trm: Proof.context -> term * term -> term + val regularize_trm_chk: Proof.context -> term * term -> term + + val inj_repabs_trm: Proof.context -> term * term -> term + val inj_repabs_trm_chk: Proof.context -> term * term -> term end; structure Quotient_Term: QUOTIENT_TERM = @@ -52,7 +52,7 @@ fun get_mapfun ctxt s = let val thy = ProofContext.theory_of ctxt - val exc = LIFT_MATCH ("No map function for type " ^ (quote s) ^ " found.") + val exc = LIFT_MATCH ("No map function for type " ^ quote s ^ " found.") val mapfun = #mapfun (maps_lookup thy s) handle NotFound => raise exc in Const (mapfun, dummyT) @@ -89,7 +89,7 @@ fun get_rty_qty ctxt s = let val thy = ProofContext.theory_of ctxt - val exc = LIFT_MATCH ("No quotient type " ^ (quote s) ^ " found.") + val exc = LIFT_MATCH ("No quotient type " ^ quote s ^ " found.") val qdata = (quotdata_lookup thy s) handle NotFound => raise exc in (#rtyp qdata, #qtyp qdata) @@ -351,14 +351,14 @@ A = B ----> R A B - or + or A = B ----> (R ===> R) A B - + for more complicated types of A and B *) - + val mk_babs = Const (@{const_name Babs}, dummyT) val mk_ball = Const (@{const_name Ball}, dummyT) val mk_bex = Const (@{const_name Bex}, dummyT) @@ -375,9 +375,9 @@ | _ => f (trm1, trm2) (* the major type of All and Ex quantifiers *) -fun qnt_typ ty = domain_type (domain_type ty) +fun qnt_typ ty = domain_type (domain_type ty) -(* produces a regularized version of rtrm +(* produces a regularized version of rtrm - the result might contain dummyTs @@ -487,15 +487,14 @@ |> Syntax.check_term ctxt -(*********************) -(* Rep/Abs Injection *) -(*********************) + +(*** Rep/Abs Injection ***) (* Injection of Rep/Abs means: - For abstractions -: + For abstractions: + * If the type of the abstraction needs lifting, then we add Rep/Abs around the abstraction; otherwise we leave it unchanged. @@ -532,9 +531,8 @@ end -(* bound variables need to be treated properly, *) -(* as the type of subterms needs to be calculated *) - +(* bound variables need to be treated properly, + as the type of subterms needs to be calculated *) fun inj_repabs_trm ctxt (rtrm, qtrm) = case (rtrm, qtrm) of (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') => diff -r 017cb46b27bb -r 433f7c17255f Quot/quotient_typ.ML --- a/Quot/quotient_typ.ML Wed Jan 13 00:46:31 2010 +0100 +++ b/Quot/quotient_typ.ML Wed Jan 13 09:19:20 2010 +0100 @@ -218,7 +218,7 @@ val warns = map_check_aux rty [] in if null warns then () - else warning ("No map function defined for " ^ (commas warns) ^ + else warning ("No map function defined for " ^ commas warns ^ ". This will cause problems later on.") end @@ -227,16 +227,16 @@ (*** interface and syntax setup ***) -(* the ML-interface takes a list of 5-tuples consisting of - - - the name of the quotient type - - its free type variables (first argument) - - its mixfix annotation - - the type to be quotient - - the relation according to which the type is quotient - - it opens a proof-state in which one has to show that the - relations are equivalence relations +(* the ML-interface takes a list of 5-tuples consisting of: + + - the name of the quotient type + - its free type variables (first argument) + - its mixfix annotation + - the type to be quotient + - the relation according to which the type is quotient + + it opens a proof-state in which one has to show that the + relations are equivalence relations *) fun quotient_type quot_list lthy =