# HG changeset patch # User Christian Urban # Date 1263372117 -3600 # Node ID bb012513fb39a292916d52bb4b380b5821f6aa32 # Parent 0ce025c02ef3257fce0761b9e4e1adbb6e5ecb27 tuned diff -r 0ce025c02ef3 -r bb012513fb39 Quot/quotient_def.ML --- a/Quot/quotient_def.ML Wed Jan 13 09:30:59 2010 +0100 +++ b/Quot/quotient_def.ML Wed Jan 13 09:41:57 2010 +0100 @@ -28,14 +28,14 @@ (* the ML-interface takes - - the mixfix annotation - - name and attributes - - the new constant as term - - the rhs of the definition as term + - 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 *) - + 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 val Free (lhs_str, lhs_ty) = lhs; (* FIXME/TODO: this throws an excpt., if the const is already def.*) diff -r 0ce025c02ef3 -r bb012513fb39 Quot/quotient_tacs.ML --- a/Quot/quotient_tacs.ML Wed Jan 13 09:30:59 2010 +0100 +++ b/Quot/quotient_tacs.ML Wed Jan 13 09:41:57 2010 +0100 @@ -97,10 +97,13 @@ end (* Calculates the instantiations for the lemmas: + ball_reg_eqv_range and bex_reg_eqv_range + Since the left-hand-side contains a non-pattern '?P (f ?x)' we rely on unification/instantiation to check whether the - theorem applies and return NONE if it doesn't. *) + theorem applies and return NONE if it doesn't. +*) fun calculate_inst ctxt ball_bex_thm redex R1 R2 = let fun get_lhs thm = fst (Logic.dest_equals (Thm.concl_of thm)) @@ -108,13 +111,12 @@ val typ_inst1 = map (SOME o ctyp_of thy) [domain_type (fastype_of R2)] val trm_inst1 = map (SOME o cterm_of thy) [R2, R1] in - (case try (Drule.instantiate' typ_inst1 trm_inst1) ball_bex_thm of + case try (Drule.instantiate' typ_inst1 trm_inst1) ball_bex_thm of NONE => NONE | SOME thm' => (case try (get_match_inst thy (get_lhs thm')) redex of NONE => NONE | SOME inst2 => try (Drule.instantiate inst2) thm') - ) end fun ball_bex_range_simproc ss redex = @@ -133,22 +135,24 @@ | _ => NONE end -(* -0. preliminary simplification step according to - ball_reg_eqv bex_reg_eqv babs_reg_eqv ball_reg_eqv_range bex_reg_eqv_range +(* Regularize works as follows: -1. eliminating simple Ball/Bex instances (ball_reg_right bex_reg_left) + 0. preliminary simplification step according to + ball_reg_eqv bex_reg_eqv babs_reg_eqv ball_reg_eqv_range bex_reg_eqv_range -2. monos + 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) + 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 -4. then rel-equalities, which need to be instantiated with 'eq_imp_rel' - to avoid loops + 5. then simplification like 0 -5. then simplification like 0 - -finally jump back to 1 *) + finally jump back to 1 +*) fun regularize_tac ctxt = let val thy = ProofContext.theory_of ctxt @@ -175,7 +179,8 @@ (*** Injection Tactic ***) (* Looks for Quot_True assumtions, and in case its parameter - is an application, it returns the function and the argument. *) + is an application, it returns the function and the argument. +*) fun find_qt_asm asms = let fun find_fun trm = @@ -231,7 +236,8 @@ (* 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. *) + assumption is different from the corresponding type in the goal. +*) val apply_rsp_tac = Subgoal.FOCUS (fn {concl, asms, context,...} => let @@ -259,7 +265,8 @@ end) (* Instantiates and applies 'equals_rsp'. Since the theorem is - complex we rely on instantiation to tell us if it applies *) + complex we rely on instantiation to tell us if it applies +*) fun equals_rsp_tac R ctxt = let val thy = ProofContext.theory_of ctxt @@ -298,29 +305,28 @@ | _ => no_tac) -(* -To prove that the regularised theorem implies the abs/rep injected, -we try: + +(* Injection means to prove that the regularised theorem implies + the abs/rep injected one. - 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) - 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 + 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) + + 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 *) - - fun injection_match_tac ctxt = SUBGOAL (fn (goal, i) => (case (bare_concl goal) of (* (R1 ===> R2) (%x...) (%x...) ----> [|R1 x y|] ==> R2 (...x) (...y) *) @@ -412,7 +418,7 @@ -(** Cleaning of the Theorem **) +(*** 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 = @@ -462,7 +468,8 @@ 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 *) + 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 _) => @@ -490,18 +497,20 @@ (* Cleaning consists of: - 1. folding of definitions and preservation lemmas; - and simplification with babs_prs all_prs ex_prs + + 1. folding of definitions and preservation lemmas; + and simplification with babs_prs all_prs ex_prs - 2. unfolding of ---> in front of everything, except - bound variables - (this prevents lambda_prs from becoming stuck) + 2. unfolding of ---> in front of everything, except + bound variables + (this prevents lambda_prs from becoming stuck) - 3. simplification with lambda_prs + 3. simplification with lambda_prs - 4. simplification with Quotient_abs_rep Quotient_rel_rep id_simps + 4. simplification with Quotient_abs_rep Quotient_rel_rep id_simps - 5. test for refl *) + 5. test for refl +*) fun clean_tac lthy = let (* FIXME/TODO produce defs with lthy, like prs and ids *) @@ -526,7 +535,6 @@ (** Tactic for Generalising Free Variables in a Goal **) - fun inst_spec ctrm = Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec} @@ -556,17 +564,17 @@ (** 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 + - 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 + - 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 *) + the Quot_True premise in 2nd records the lifted theorem +*) val lifting_procedure_thm = @{lemma "[|A; A --> B; diff -r 0ce025c02ef3 -r bb012513fb39 Quot/quotient_term.ML --- a/Quot/quotient_term.ML Wed Jan 13 09:30:59 2010 +0100 +++ b/Quot/quotient_term.ML Wed Jan 13 09:41:57 2010 +0100 @@ -175,7 +175,7 @@ ('a * 'a) list / 'a bar - The test is necessary in order to eliminate superflous + The test is necessary in order to eliminate superfluous identity maps. *) @@ -358,7 +358,6 @@ 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)