# HG changeset patch # User Christian Urban # Date 1260225951 -3600 # Node ID ec37a279ca550097321560566aa928434a0fdd71 # Parent bb5d3278f02eac68ea294ff2d8d9c26f3ed91877 tuning of the code diff -r bb5d3278f02e -r ec37a279ca55 Quot/Examples/IntEx.thy --- a/Quot/Examples/IntEx.thy Mon Dec 07 21:54:14 2009 +0100 +++ b/Quot/Examples/IntEx.thy Mon Dec 07 23:45:51 2009 +0100 @@ -153,8 +153,6 @@ apply(rule refl) done - - lemma "PLUS a = PLUS a" apply(tactic {* procedure_tac @{context} @{thm test2} 1 *}) apply(rule impI) diff -r bb5d3278f02e -r ec37a279ca55 Quot/QuotMain.thy --- a/Quot/QuotMain.thy Mon Dec 07 21:54:14 2009 +0100 +++ b/Quot/QuotMain.thy Mon Dec 07 23:45:51 2009 +0100 @@ -144,9 +144,10 @@ declare [[map * = (prod_fun, prod_rel)]] declare [[map "fun" = (fun_map, fun_rel)]] -(* FIXME: This should throw an exception: -declare [[map "option" = (bla, blu)]] -*) + +(* FIXME: This should throw an exception: *) +(* declare [[map "option" = (bla, blu)]] *) + (* identity quotient is not here as it has to be applied first *) lemmas [quotient_thm] = @@ -294,7 +295,7 @@ | _ => false *} -section {* Regularization *} +section {* Computation of the Regularize Goal *} (* Regularizing an rtrm means: @@ -461,6 +462,8 @@ raise (LIFT_MATCH "regularize (default)") *} +section {* Regularize Tactic *} + ML {* fun equiv_tac ctxt = (K (print_tac "equiv tac")) THEN' @@ -532,20 +535,23 @@ shows "equivp R \ a = b \ R a b" by (simp add: equivp_reflp) -(* FIXME/TODO: How does regularizing work? *) -(* FIXME/TODO: needs to be adapted -To prove that the raw theorem implies the regularised one, -we try in order: +(* Regularize Tactic *) - - Reflexivity of the relation - - Assumption - - Elimnating quantifiers on both sides of toplevel implication - - Simplifying implications on both sides of toplevel implication - - Ball (Respects ?E) ?P = All ?P - - (\x. ?R x \ ?P x \ ?Q x) \ All ?P \ Ball ?R ?Q +(* 0. preliminary simplification step according to *) +thm ball_reg_eqv bex_reg_eqv babs_reg_eqv (* the latter of no use *) + 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 @@ -558,24 +564,19 @@ addsimprocs [simproc] addSolver equiv_solver (* TODO: Make sure that there are no list_rel, pair_rel etc involved *) (* can this cause loops in equiv_tac ? *) - val eq_eqvs = map (fn x => @{thm eq_imp_rel} OF [x]) (equiv_rules_get ctxt) + val eq_eqvs = map (OF1 @{thm eq_imp_rel}) (equiv_rules_get ctxt) in simp_tac simpset THEN' REPEAT_ALL_NEW (CHANGED o FIRST' [ - rtac @{thm ball_reg_right}, - rtac @{thm bex_reg_left}, + resolve_tac @{thms ball_reg_right bex_reg_left}, resolve_tac (Inductive.get_monos ctxt), - rtac @{thm ball_all_comm}, - rtac @{thm bex_ex_comm}, + resolve_tac @{thms ball_all_comm bex_ex_comm}, resolve_tac eq_eqvs, - (* should be equivalent to the above, but causes loops: *) - (* rtac @{thm eq_imp_rel} THEN' SOLVES' (equiv_tac ctxt), *) - (* the culprit is aslread rtac @{thm eq_imp_rel} *) simp_tac simpset]) end *} -section {* Injections of rep and abses *} +section {* Calculation of the Injected Goal *} (* Injecting repabs means: @@ -658,7 +659,7 @@ | _ => raise (LIFT_MATCH "injection") *} -section {* RepAbs Injection Tactic *} +section {* Injection Tactic *} ML {* fun quotient_tac ctxt = @@ -949,8 +950,8 @@ ML {* fun inj_repabs_tac ctxt = let - val rel_refl = map (fn x => @{thm equivp_reflp} OF [x]) (equiv_rules_get ctxt) - val trans2 = map (fn x => @{thm equals_rsp} OF [x]) (quotient_rules_get ctxt) + val rel_refl = map (OF1 @{thm equivp_reflp}) (equiv_rules_get ctxt) + val trans2 = map (OF1 @{thm equals_rsp}) (quotient_rules_get ctxt) in inj_repabs_step_tac ctxt rel_refl trans2 end @@ -1043,29 +1044,14 @@ fun lambda_prs_tac ctxt = CONVERSION (lambda_prs_conv ctxt) *} -(* - Cleaning the theorem consists of three rewriting steps. - The first two need to be done before fun_map is unfolded - - 1) lambda_prs: - (Rep1 ---> Abs2) (\x. Rep2 (f (Abs1 x))) ----> f - - Implemented as conversion since it is not a pattern. - - 2) all_prs (the same for exists): - Ball (Respects R) ((abs ---> id) f) ----> All f - - Rewriting with definitions from the argument defs - (rep ---> abs) oldConst ----> newconst - - 3) Quotient_rel_rep: - Rel (Rep x) (Rep y) ----> x = y - - Quotient_abs_rep: - Abs (Rep x) ----> x - - id_simps; fun_map.simps -*) +(* 1. conversion (is not a pattern) *) +thm lambda_prs +(* 2. folding of definitions: (rep ---> abs) oldConst == newconst *) +(* and simplification with *) +thm all_prs ex_prs +(* 3. simplification with *) +thm fun_map.simps id_simps Quotient_abs_rep Quotient_rel_rep +(* 4. Test for refl *) ML {* fun clean_tac lthy = @@ -1085,7 +1071,7 @@ end *} -section {* Genralisation of free variables in a goal *} +section {* Tactic for genralisation of free variables in a goal *} ML {* fun inst_spec ctrm = @@ -1115,7 +1101,7 @@ end) *} -section {* General outline of the lifting procedure *} +section {* General shape of the lifting procedure *} (* - A is the original raw theorem *) (* - B is the regularized theorem *) @@ -1132,8 +1118,8 @@ and c: "B = C" and d: "C = D" shows "D" - using a b c d - by simp +using a b c d +by simp ML {* fun lift_match_error ctxt fun_str rtrm qtrm = @@ -1156,11 +1142,9 @@ val reg_goal = Syntax.check_term ctxt (regularize_trm ctxt rtrm' qtrm') handle (LIFT_MATCH s) => lift_match_error ctxt s rtrm qtrm - val _ = warning "Regularization done." 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 - val _ = warning "RepAbs Injection done." in Drule.instantiate' [] [SOME (cterm_of thy rtrm'), @@ -1169,38 +1153,30 @@ end *} -(* Left for debugging *) ML {* +(* leaves three subgoales to be proved *) fun procedure_tac ctxt rthm = ObjectLogic.full_atomize_tac THEN' gen_frees_tac ctxt - THEN' CSUBGOAL (fn (gl, i) => - let - val rthm' = atomize_thm rthm - val rule = procedure_inst ctxt (prop_of rthm') (term_of gl) - val thm = Drule.instantiate' [] [SOME (snd (Thm.dest_comb gl))] @{thm QUOT_TRUE_i} - in - (rtac rule THEN' RANGE [rtac rthm', (fn _ => all_tac), rtac thm]) i - end) -*} - -ML {* -fun lift_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) - val thm = Drule.instantiate' [] [SOME (snd (Thm.dest_comb goal))] @{thm QUOT_TRUE_i} + val bare_goal = snd (Thm.dest_comb goal) + val quot_weak = Drule.instantiate' [] [SOME bare_goal] @{thm QUOT_TRUE_i} in - (rtac rule THEN' - RANGE [rtac rthm', - regularize_tac ctxt, - rtac thm THEN' all_inj_repabs_tac ctxt, - clean_tac ctxt]) i + (rtac rule THEN' RANGE [rtac rthm', K all_tac, rtac quot_weak]) i end) *} +ML {* +(* automated tactics *) +fun lift_tac ctxt rthm = + procedure_tac ctxt rthm + THEN' RANGE [regularize_tac ctxt, + all_inj_repabs_tac ctxt, + clean_tac ctxt] +*} + end