# HG changeset patch # User Cezary Kaliszyk # Date 1259306123 -3600 # Node ID 3f3927f793d456119509deda0c00533a5b229181 # Parent 5a9bdf81672d625cd6a50281cc11ee74c29e76d8 Removing arguments of tactics: absrep, rel_refl, reps_same are computed. diff -r 5a9bdf81672d -r 3f3927f793d4 FSet.thy --- a/FSet.thy Fri Nov 27 07:16:16 2009 +0100 +++ b/FSet.thy Fri Nov 27 08:15:23 2009 +0100 @@ -304,7 +304,7 @@ ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset"; *} ML {* val consts = lookup_quot_consts defs *} -ML {* fun lift_tac_fset lthy t = lift_tac lthy t rel_eqv rel_refl rty quot trans2 rsp_thms reps_same absrep defs *} +ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] rty [quot] trans2 rsp_thms defs *} lemma "IN x EMPTY = False" by (tactic {* lift_tac_fset @{context} @{thm m1} 1 *}) @@ -345,10 +345,10 @@ lemma "\P EMPTY; \a x. P x \ P (INSERT a x)\ \ P l" apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *}) -apply(tactic {* regularize_tac @{context} [rel_eqv] rel_refl 1 *}) +apply(tactic {* regularize_tac @{context} [rel_eqv] [rel_refl] 1 *}) prefer 2 -apply (tactic {* clean_tac @{context} quot defs reps_same absrep [(@{typ "('a list \ bool)"},@{typ "('a fset \ bool)"})] 1 *}) -apply(tactic {* r_mk_comb_tac' @{context} rty quot rel_refl trans2 rsp_thms 1*}) +apply (tactic {* clean_tac @{context} [quot] defs [(@{typ "('a list \ bool)"},@{typ "('a fset \ bool)"})] 1 *}) +apply(tactic {* r_mk_comb_tac' @{context} rty [quot] rel_refl trans2 rsp_thms 1*}) done quotient_def @@ -376,7 +376,7 @@ ML {* val rsp_thms = @{thms list_rec_rsp list_case_rsp} @ rsp_thms *} ML {* val defs = @{thms fset_rec_def fset_case_def} @ defs *} -ML {* fun lift_tac_fset lthy t = lift_tac lthy t rel_eqv rel_refl rty quot trans2 rsp_thms reps_same absrep defs *} +ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] rty [quot] trans2 rsp_thms defs *} lemma "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)" apply (tactic {* lift_tac_fset @{context} @{thm list.recs(2)} 1 *}) @@ -397,7 +397,7 @@ done -ML {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms *} +ML {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac lthy rty [quot] [rel_refl] trans2 rsp_thms *} @@ -405,7 +405,7 @@ (* Construction site starts here *) lemma "P (x :: 'a list) (EMPTY :: 'c fset) \ (\e t. P x t \ P x (INSERT e t)) \ P x l" apply (tactic {* procedure_tac @{context} @{thm list_induct_part} 1 *}) -apply (tactic {* regularize_tac @{context} [rel_eqv] rel_refl 1 *}) +apply (tactic {* regularize_tac @{context} [rel_eqv] [rel_refl] 1 *}) apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *}) apply (rule FUN_QUOTIENT) apply (rule FUN_QUOTIENT) @@ -454,25 +454,25 @@ apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *}) -apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP(1)} @{context} THEN' (RANGE [quotient_tac quot])) 1 *}) +apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP(1)} @{context} THEN' (RANGE [quotient_tac [quot]])) 1 *}) apply assumption apply (rule refl) apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *}) apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *}) -apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP(1)} @{context} THEN' (RANGE [quotient_tac quot])) 1 *}) +apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP(1)} @{context} THEN' (RANGE [quotient_tac [quot]])) 1 *}) apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *}) -apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP(1)} @{context} THEN' (RANGE [quotient_tac quot])) 1 *}) +apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP(1)} @{context} THEN' (RANGE [quotient_tac [quot]])) 1 *}) apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) -apply (tactic {* clean_tac @{context} quot defs reps_same absrep [(@{typ "('a list \ 'c list \ bool)"},@{typ "('a list \ 'c fset \ bool)"})] 1 *}) +apply (tactic {* clean_tac @{context} [quot] defs [(@{typ "('a list \ 'c list \ bool)"},@{typ "('a list \ 'c fset \ bool)"})] 1 *}) done end diff -r 5a9bdf81672d -r 3f3927f793d4 IntEx.thy --- a/IntEx.thy Fri Nov 27 07:16:16 2009 +0100 +++ b/IntEx.thy Fri Nov 27 08:15:23 2009 +0100 @@ -142,7 +142,7 @@ ML {* fun lift_tac_fset lthy t = - lift_tac lthy t rel_eqv rel_refl rty quot trans2 rsp_thms reps_same absrep defs + lift_tac lthy t [rel_eqv] rty [quot] trans2 rsp_thms defs *} lemma "PLUS a b = PLUS b a" @@ -167,9 +167,12 @@ lemma map_prs: "map REP_my_int (map ABS_my_int x) = x" sorry +lemma foldl_prs: "((op \ ===> op \ ===> op \) ===> op \ ===> op = ===> op \) foldl foldl" +sorry + lemma "foldl PLUS x [] = x" apply (tactic {* lift_tac_fset @{context} @{thm ho_tst} 1 *}) -apply (simp_all only: map_prs) +apply (simp_all only: map_prs foldl_prs) sorry (* @@ -187,8 +190,8 @@ lemma "PLUS (PLUS i j) k = PLUS i (PLUS j k)" apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *}) -apply(tactic {* regularize_tac @{context} [rel_eqv] rel_refl 1 *}) -apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms) 1 *}) +apply(tactic {* regularize_tac @{context} [rel_eqv] [rel_refl] 1 *}) +apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} rty [quot] [rel_refl] trans2 rsp_thms) 1 *}) oops diff -r 5a9bdf81672d -r 3f3927f793d4 LFex.thy --- a/LFex.thy Fri Nov 27 07:16:16 2009 +0100 +++ b/LFex.thy Fri Nov 27 08:15:23 2009 +0100 @@ -180,12 +180,6 @@ where "perm_trm \ (perm::'x prm \ trm \ trm)" -ML {* val defs = - @{thms TYP_def KPI_def TCONST_def TAPP_def TPI_def VAR_def CONS_def APP_def LAM_def - FV_kind_def FV_ty_def FV_trm_def perm_kind_def perm_ty_def perm_trm_def} -*} -ML {* val consts = lookup_quot_consts defs *} - thm akind_aty_atrm.induct lemma left_ball_regular: @@ -279,6 +273,10 @@ end *} +ML {* val defs = + @{thms TYP_def KPI_def TCONST_def TAPP_def TPI_def VAR_def CONS_def APP_def LAM_def + FV_kind_def FV_ty_def FV_trm_def perm_kind_def perm_ty_def perm_trm_def} +*} lemma "\P1 TYP TYP; \A A' K K' x. \(A::TY) = A'; P2 A A'; (K::KIND) = K'; P1 K K'\ \ P1 (KPI A x K) (KPI A' x K'); \A A' K x x' K'. @@ -301,8 +299,15 @@ apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *}) apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *}) prefer 2 -apply(tactic {* r_mk_comb_tac' @{context} rty quot rel_refl trans2 rsp_thms 1*}) -apply (tactic {* clean_tac @{context} quot defs reps_same absrep 1 *}) +thm QUOTIENT_TY +apply (tactic {* clean_tac @{context} @{thms QUOTIENT_KIND QUOTIENT_TY QUOTIENT_TRM} defs [] 1 *}) + + +print_quotients +apply(tactic {* r_mk_comb_tac' @{context} rty [quot] rel_refl trans2 [] 1*}) + + +ML {* val consts = lookup_quot_consts defs *} ML {* val rty_qty_rel = diff -r 5a9bdf81672d -r 3f3927f793d4 LamEx.thy --- a/LamEx.thy Fri Nov 27 07:16:16 2009 +0100 +++ b/LamEx.thy Fri Nov 27 08:15:23 2009 +0100 @@ -179,7 +179,7 @@ ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} ML {* val consts = lookup_quot_consts defs *} ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "lam" *} -ML {* fun lift_tac_lam lthy t = lift_tac lthy t rel_eqv rel_refl rty quot trans2 rsp_thms reps_same absrep defs *} +ML {* fun lift_tac_lam lthy t = lift_tac lthy t rel_eqv rel_refl rty [quot] trans2 rsp_thms reps_same absrep defs *} lemma pi_var: "(pi\('x \ 'x) list) \ Var a = Var (pi \ a)" apply (tactic {* lift_tac_lam @{context} @{thm pi_var_com} 1 *}) diff -r 5a9bdf81672d -r 3f3927f793d4 QuotMain.thy --- a/QuotMain.thy Fri Nov 27 07:16:16 2009 +0100 +++ b/QuotMain.thy Fri Nov 27 08:15:23 2009 +0100 @@ -293,8 +293,7 @@ val rty = Logic.unvarifyT (#rtyp quotdata) val rel = #rel quotdata val rel_eqv = #equiv_thm quotdata - val rel_refl_pre = @{thm EQUIV_REFL} OF [rel_eqv] - val rel_refl = @{thm spec} OF [MetaSimplifier.rewrite_rule [@{thm REFL_def}] rel_refl_pre] + val rel_refl = @{thm EQUIV_REFL} OF [rel_eqv] in (rty, rel, rel_refl, rel_eqv) end @@ -494,7 +493,7 @@ (ObjectLogic.full_atomize_tac) THEN' REPEAT_ALL_NEW (FIRST' [(K (print_tac "start")) THEN' (K no_tac), - DT ctxt "1" (rtac rel_refl), + DT ctxt "1" (FIRST' (map rtac rel_refl)), DT ctxt "2" atac, DT ctxt "3" (rtac @{thm universal_twice}), DT ctxt "4" (rtac @{thm impI} THEN' atac), @@ -503,7 +502,7 @@ [(@{thm equiv_res_forall} OF [rel_eqv]), (@{thm equiv_res_exists} OF [rel_eqv])]), (* For a = b \ a \ b *) - DT ctxt "7" (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl), + DT ctxt "7" (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' (FIRST' (map rtac rel_refl))), DT ctxt "8" (rtac @{thm RIGHT_RES_FORALL_REGULAR}) ]); *} @@ -590,7 +589,7 @@ (rtac @{thm bex_respects_refl} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])), rtac @{thm move_forall}, rtac @{thm move_exists}, - (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl) + (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' FIRST' (map rtac rel_refl)) ]) end *} @@ -720,12 +719,13 @@ ML {* -fun quotient_tac quot_thm = +fun quotient_tac quot_thms = REPEAT_ALL_NEW (FIRST' [ rtac @{thm FUN_QUOTIENT}, - rtac quot_thm, + FIRST' (map rtac quot_thms), rtac @{thm IDENTITY_QUOTIENT}, (* For functional identity quotients, (op = ---> op =) *) + (* TODO: think about the other way around, if we need to shorten the relation *) CHANGED o (simp_tac (HOL_ss addsimps @{thms id_simps})) ]) *} @@ -803,7 +803,7 @@ *} ML {* -fun r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms = +fun r_mk_comb_tac ctxt rty quot_thms rel_refl trans_thm rsp_thms = (FIRST' [ rtac trans_thm, LAMBDA_RES_TAC ctxt, @@ -814,12 +814,12 @@ FIRST' (map rtac rsp_thms), rtac refl, (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' - (RANGE [SOLVES' (quotient_tac quot_thm)])), + (RANGE [SOLVES' (quotient_tac quot_thms)])), (APPLY_RSP_TAC rty ctxt THEN' - (RANGE [SOLVES' (quotient_tac quot_thm), SOLVES' (quotient_tac quot_thm)])), + (RANGE [SOLVES' (quotient_tac quot_thms), SOLVES' (quotient_tac quot_thms)])), Cong_Tac.cong_tac @{thm cong}, rtac @{thm ext}, - rtac reflex_thm, + FIRST' (map rtac rel_refl), atac, SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})), WEAK_LAMBDA_RES_TAC ctxt, @@ -851,7 +851,7 @@ *) ML {* -fun r_mk_comb_tac' ctxt rty quot_thm reflex_thm trans_thm rsp_thms = +fun r_mk_comb_tac' ctxt rty quot_thms reflex_thm trans_thm rsp_thms = REPEAT_ALL_NEW (FIRST' [ (K (print_tac "start")) THEN' (K no_tac), DT ctxt "1" (rtac trans_thm), @@ -863,9 +863,9 @@ DT ctxt "7" (FIRST' (map rtac rsp_thms)), DT ctxt "8" (rtac refl), DT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP(1)} ctxt - THEN' (RANGE [SOLVES' (quotient_tac quot_thm)]))), + THEN' (RANGE [SOLVES' (quotient_tac quot_thms)]))), DT ctxt "A" ((APPLY_RSP_TAC rty ctxt THEN' - (RANGE [SOLVES' (quotient_tac quot_thm), SOLVES' (quotient_tac quot_thm)]))), + (RANGE [SOLVES' (quotient_tac quot_thms), SOLVES' (quotient_tac quot_thms)]))), DT ctxt "B" (Cong_Tac.cong_tac @{thm cong}), DT ctxt "C" (rtac @{thm ext}), DT ctxt "D" (rtac reflex_thm), @@ -898,7 +898,7 @@ val llhs = Syntax.check_term lthy lhs; val eq = Logic.mk_equals (llhs, rhs); val ceq = cterm_of (ProofContext.theory_of lthy') eq; - val sctxt = HOL_ss addsimps (absrep :: @{thms fun_map.simps id_simps}); + val sctxt = HOL_ss addsimps (@{thms fun_map.simps id_simps} @ absrep); val t = Goal.prove_internal [] ceq (fn _ => simp_tac sctxt 1) val t_id = MetaSimplifier.rewrite_rule @{thms id_simps} t; in @@ -950,7 +950,7 @@ *} ML {* -fun lambda_prs_conv1 ctxt quot ctrm = +fun lambda_prs_conv1 ctxt quot_thms ctrm = case (term_of ctrm) of ((Const (@{const_name "fun_map"}, _) $ r1 $ a2) $ (Abs _)) => let val (_, [ty_b, ty_a]) = dest_Type (fastype_of r1); @@ -962,7 +962,7 @@ val lpi = Drule.instantiate' tyinst tinst @{thm LAMBDA_PRS}; val tac = (compose_tac (false, lpi, 2)) THEN_ALL_NEW - (quotient_tac quot); + (quotient_tac quot_thms); val gc = Drule.strip_imp_concl (cprop_of lpi); val t = Goal.prove_internal [] gc (fn _ => tac 1) val te = @{thm eq_reflection} OF [t] @@ -1003,16 +1003,18 @@ *} ML {* -fun clean_tac lthy quot defs reps_same absrep aps = +fun clean_tac lthy quot defs aps = let val lower = flat (map (add_lower_defs lthy) defs) + val absrep = map (fn x => @{thm QUOTIENT_ABS_REP} OF [x]) quot + val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quot val aps_thms = map (applic_prs lthy absrep) aps in - EVERY' [TRY o REPEAT_ALL_NEW (allex_prs_tac lthy quot), + EVERY' [TRY o REPEAT_ALL_NEW (allex_prs_tac lthy quot), lambda_prs_tac lthy quot, TRY o REPEAT_ALL_NEW (EqSubst.eqsubst_tac lthy [0] aps_thms), TRY o REPEAT_ALL_NEW (EqSubst.eqsubst_tac lthy [0] lower), - simp_tac (HOL_ss addsimps [reps_same])] + simp_tac (HOL_ss addsimps reps_same)] end *} @@ -1114,7 +1116,7 @@ ML {* (* FIXME/TODO should only get as arguments the rthm like procedure_tac *) -fun lift_tac lthy rthm rel_eqv rel_refl rty quot trans2 rsp_thms reps_same absrep defs = +fun lift_tac lthy rthm rel_eqv rty quot trans2 rsp_thms defs = ObjectLogic.full_atomize_tac THEN' gen_frees_tac lthy THEN' Subgoal.FOCUS (fn {context, concl, ...} => @@ -1122,13 +1124,14 @@ val rthm' = atomize_thm rthm val rule = procedure_inst context (prop_of rthm') (term_of concl) val aps = find_aps (prop_of rthm') (term_of concl) + val rel_refl = map (fn x => @{thm EQUIV_REFL} OF [x]) rel_eqv in EVERY1 [rtac rule, RANGE [rtac rthm', - regularize_tac lthy [rel_eqv] rel_refl, + regularize_tac lthy rel_eqv rel_refl, REPEAT_ALL_NEW (r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms), - clean_tac lthy quot defs reps_same absrep aps]] + clean_tac lthy quot defs aps]] end) lthy *} diff -r 5a9bdf81672d -r 3f3927f793d4 QuotScript.thy --- a/QuotScript.thy Fri Nov 27 07:16:16 2009 +0100 +++ b/QuotScript.thy Fri Nov 27 08:15:23 2009 +0100 @@ -20,8 +20,8 @@ by (blast) lemma EQUIV_REFL: - shows "EQUIV E ==> REFL E" - by (simp add: EQUIV_REFL_SYM_TRANS) + shows "EQUIV E \ (\x. E x x)" + by (simp add: EQUIV_REFL_SYM_TRANS REFL_def) definition "PART_EQUIV E \ (\x. E x x) \ (\x y. E x y = (E x x \ E y y \ (E x = E y)))"