# HG changeset patch # User Cezary Kaliszyk # Date 1259917937 -3600 # Node ID bed81795848c6c937df60aab3e06c08f453b022c # Parent b00a9b58264d9c851bd418045950ee384cac4b69 Using APPLY_RSP1; again a little bit faster. diff -r b00a9b58264d -r bed81795848c FSet.thy --- a/FSet.thy Fri Dec 04 09:33:32 2009 +0100 +++ b/FSet.thy Fri Dec 04 10:12:17 2009 +0100 @@ -299,7 +299,7 @@ lemma "IN x EMPTY = False" apply(tactic {* procedure_tac @{context} @{thm m1} 1 *}) apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) -apply(tactic {* all_inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) +apply(tactic {* all_inj_repabs_tac' @{context} [rel_refl] [trans2] 1 *}) apply(tactic {* clean_tac @{context} 1*}) done @@ -327,7 +327,7 @@ apply(tactic {* lift_tac_fset @{context} @{thm fold1.simps(2)} 1 *}) done -ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy [rel_refl] [trans2] *} +ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac' lthy [rel_refl] [trans2] *} lemma "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)" apply (tactic {* lift_tac_fset @{context} @{thm map_append} 1 *}) @@ -389,6 +389,9 @@ apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *) apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *) apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) +apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *) +apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) +apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *) done lemma list_induct_part: diff -r b00a9b58264d -r bed81795848c LFex.thy --- a/LFex.thy Fri Dec 04 09:33:32 2009 +0100 +++ b/LFex.thy Fri Dec 04 10:12:17 2009 +0100 @@ -258,10 +258,12 @@ ((x5 :: TRM) = x6 \ P3 x5 x6)" using a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 apply - -apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *}) -apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *}) -prefer 2 +apply(tactic {* lift_tac @{context} @{thm akind_aty_atrm.induct} @{thms alpha_EQUIVs} 1 *}) +(*apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *}) +apply(tactic {* all_inj_repabs_tac' @{context} rel_refl trans2 1 *}) apply(tactic {* clean_tac @{context} 1 *}) +*) +(*apply(tactic {* all_inj_repabs_tac @{context} rel_refl trans2 1 *})*) (* Profiling: ML_prf {* fun ith i = (#concl (fst (Subgoal.focus @{context} i (#goal (Isar.goal ()))))) *} @@ -270,8 +272,6 @@ ML_prf {* PolyML.profiling 1 *} ML_prf {* profile 2 Seq.list_of ((all_inj_repabs_tac @{context} quot rel_refl trans2 1) (#goal (Isar.goal ()))) *} *) -apply(tactic {* all_inj_repabs_tac' @{context} rel_refl trans2 1 *}) -(*apply(tactic {* all_inj_repabs_tac @{context} rel_refl trans2 1 *})*) done (* Does not work: diff -r b00a9b58264d -r bed81795848c QuotMain.thy --- a/QuotMain.thy Fri Dec 04 09:33:32 2009 +0100 +++ b/QuotMain.thy Fri Dec 04 10:12:17 2009 +0100 @@ -813,6 +813,32 @@ | _ => no_tac) *} +ML {* +val APPLY_RSP1_TAC = + Subgoal.FOCUS (fn {concl, asms, context,...} => + case ((HOLogic.dest_Trueprop (term_of concl))) of + ((R2 $ (f $ x) $ (g $ y))) => + let + val (asmf, asma) = find_qt_asm (map term_of asms); + in + if (fastype_of asmf) = (fastype_of f) then no_tac else let + val ty_a = fastype_of x; + val ty_b = fastype_of asma; + val ty_c = range_type (type_of f); +(* val ty_d = range_type (type_of asmf);*) + val thy = ProofContext.theory_of context; + val ty_inst = map (fn x => SOME (ctyp_of thy x)) [ty_a, ty_b, ty_c]; + val [R2, f, g, x, y] = map (cterm_of thy) [R2, f, g, x, y]; + val t_inst = [NONE, NONE, NONE, SOME R2, SOME f, SOME g, SOME x, SOME y]; + val thm = Drule.instantiate' ty_inst t_inst @{thm APPLY_RSP1} + (*val _ = tracing (Syntax.string_of_term @{context} (prop_of thm))*) + in + rtac thm 1 + end + end + | _ => no_tac) +*} + ML {* fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac) @@ -1000,8 +1026,8 @@ fun inj_repabs_tac' ctxt rel_refl trans2 = (FIRST' [ inj_repabs_tac_fast ctxt trans2, - NDT ctxt "A" (APPLY_RSP_TAC ctxt THEN' - (RANGE [SOLVES' (quotient_tac ctxt), SOLVES' (quotient_tac ctxt), + NDT ctxt "A" (APPLY_RSP1_TAC ctxt THEN' + (RANGE [SOLVES' (quotient_tac ctxt), quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])), NDT ctxt "B" (Cong_Tac.cong_tac @{thm cong} THEN' (RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])), diff -r b00a9b58264d -r bed81795848c QuotScript.thy --- a/QuotScript.thy Fri Dec 04 09:33:32 2009 +0100 +++ b/QuotScript.thy Fri Dec 04 10:12:17 2009 +0100 @@ -329,9 +329,8 @@ lemma REP_ABS_RSP_LEFT: assumes q: "QUOTIENT R Abs Rep" and a: "R x1 x2" - and "R (Rep (Abs x1)) x2" shows "R x1 (Rep (Abs x2))" -using q a by (metis QUOTIENT_REL[OF q] QUOTIENT_ABS_REP[OF q] QUOTIENT_REP_REFL[OF q] QUOTIENT_SYM[of q]) +using q a by (metis QUOTIENT_REL[OF q] QUOTIENT_ABS_REP[OF q] QUOTIENT_REP_REFL[OF q]) (* ----------------------------------------------------- *) (* Quantifiers: FORALL, EXISTS, EXISTS_UNIQUE, *) @@ -382,6 +381,11 @@ using QUOTIENT_ABS_REP[OF q1] QUOTIENT_ABS_REP[OF q2] by auto (* ask peter: no use of q1 q2 *) +(* Cez: I can answer, + In the following theorem R2 can be instantiated with anything, + but we know some of the types of the Rep and Abs functions; + so by solving QUOTIENT assumptions we can get a unique R2 that + will be provable; which is why we need to use APPLY_RSP1 *) lemma APPLY_RSP: assumes q1: "QUOTIENT R1 Abs1 Rep1" and q2: "QUOTIENT R2 Abs2 Rep2" @@ -389,6 +393,12 @@ shows "R2 (f x) (g y)" using a by (rule FUN_REL_IMP) +lemma APPLY_RSP1: + assumes q: "QUOTIENT R1 Abs1 Rep1" + and a: "(R1 ===> R2) f g" "R1 x y" + shows "R2 ((f::'a\'c) x) ((g::'a\'c) y)" +using a by (rule FUN_REL_IMP) + lemma APPLY_RSP2: assumes a: "(R1 ===> R2) f g" "R1 x y" shows "R2 (f x) (g y)"