# HG changeset patch # User Christian Urban # Date 1259845325 -3600 # Node ID 6cdba30c6d66dd3e95655cdfe9c7da8f8374510d # Parent bb23a7393de3e295d4417e533396bd10edf715ba# Parent 375e28eedee7fead2abb6036a23652186952d14f merged diff -r bb23a7393de3 -r 6cdba30c6d66 FSet.thy --- a/FSet.thy Thu Dec 03 14:00:43 2009 +0100 +++ b/FSet.thy Thu Dec 03 14:02:05 2009 +0100 @@ -174,8 +174,6 @@ term fmap thm fmap_def -ML {* val defs = @{thms EMPTY_def IN_def FUNION_def CARD_def INSERT_def fmap_def FOLD_def} *} - lemma memb_rsp: fixes z assumes a: "x \ y" @@ -299,14 +297,13 @@ 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] [quot] defs *} +ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] [quot] *} 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} [quot] [rel_refl] [trans2] 1 *}) -apply(tactic {* clean_tac @{context} [quot] defs 1*}) +apply(tactic {* clean_tac @{context} [quot] 1*}) done lemma "IN x (INSERT y xa) = (x = y \ IN x xa)" @@ -351,7 +348,7 @@ apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *}) apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) prefer 2 -apply(tactic {* clean_tac @{context} [quot] defs 1 *}) +apply(tactic {* clean_tac @{context} [quot] 1 *}) apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *) 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*}) (* 2 *) (* lam-lam-elim for R = (===>) *) @@ -433,10 +430,9 @@ where "INSERT2 \ op #" -ML {* val defs = @{thms EMPTY2_def INSERT2_def} @ defs *} ML {* val quot = @{thms QUOTIENT_fset QUOTIENT_fset2} *} ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy quot [rel_refl] [trans2] *} -ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] quot defs *} +ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] quot *} lemma "P (x :: 'a fset2) (EMPTY :: 'c fset) \ (\e t. P x t \ P x (INSERT e t)) \ P x l" apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *}) @@ -470,8 +466,7 @@ sorry 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] quot defs *} +ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] quot *} 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 *}) @@ -481,6 +476,5 @@ apply (tactic {* lift_tac_fset @{context} @{thm list.cases(2)} 1 *}) done -thm all_prs end diff -r bb23a7393de3 -r 6cdba30c6d66 IntEx.thy --- a/IntEx.thy Thu Dec 03 14:00:43 2009 +0100 +++ b/IntEx.thy Thu Dec 03 14:02:05 2009 +0100 @@ -136,12 +136,10 @@ ML {* val qty = @{typ "my_int"} *} ML {* val ty_name = "my_int" *} ML {* val rsp_thms = @{thms ho_plus_rsp} *} -ML {* val defs = @{thms PLUS_def} *} ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int"; *} -ML {* val consts = lookup_quot_consts defs *} -ML {* fun lift_tac_intex lthy t = lift_tac lthy t [rel_eqv] [quot] defs *} +ML {* fun lift_tac_intex lthy t = lift_tac lthy t [rel_eqv] [quot] *} ML {* fun inj_repabs_tac_intex lthy = inj_repabs_tac lthy [quot] [rel_refl] [trans2] *} ML {* fun all_inj_repabs_tac_intex lthy = all_inj_repabs_tac lthy [quot] [rel_refl] [trans2] *} @@ -151,7 +149,7 @@ apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *}) apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) prefer 2 -apply(tactic {* clean_tac @{context} [quot] defs 1 *}) +apply(tactic {* clean_tac @{context} [quot] 1 *}) apply(tactic {* inj_repabs_tac_intex @{context} 1*}) apply(tactic {* inj_repabs_tac_intex @{context} 1*}) apply(tactic {* inj_repabs_tac_intex @{context} 1*}) @@ -189,7 +187,7 @@ apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *}) apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) -apply(tactic {* clean_tac @{context} [quot] defs 1 *}) +apply(tactic {* clean_tac @{context} [quot] 1 *}) done lemma ho_tst: "foldl my_plus x [] = x" @@ -286,7 +284,7 @@ apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) apply(simp only: foldl_prs[OF QUOTIENT_my_int QUOTIENT_my_int]) apply(simp only: nil_prs) -apply(tactic {* clean_tac @{context} [quot] defs 1 *}) +apply(tactic {* clean_tac @{context} [quot] 1 *}) done lemma ho_tst2: "foldl my_plus x (h # t) \ my_plus h (foldl my_plus x t)" @@ -298,6 +296,6 @@ apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) apply(simp only: foldl_prs[OF QUOTIENT_my_int QUOTIENT_my_int]) apply(simp only: cons_prs[OF QUOTIENT_my_int]) -apply(tactic {* clean_tac @{context} [quot] defs 1 *}) +apply(tactic {* clean_tac @{context} [quot] 1 *}) done diff -r bb23a7393de3 -r 6cdba30c6d66 LFex.thy --- a/LFex.thy Thu Dec 03 14:00:43 2009 +0100 +++ b/LFex.thy Thu Dec 03 14:02:05 2009 +0100 @@ -216,11 +216,6 @@ thm akind_aty_atrm.induct thm kind_ty_trm.induct -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 quot = @{thms QUOTIENT_KIND QUOTIENT_TY QUOTIENT_TRM} val rel_refl = map (fn x => @{thm EQUIV_REFL} OF [x]) @{thms alpha_EQUIVs} @@ -264,16 +259,18 @@ 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 {* clean_tac @{context} quot 1 *}) (* Profiling: ML_prf {* fun ith i = (#concl (fst (Subgoal.focus @{context} i (#goal (Isar.goal ()))))) *} ML_prf {* profile 2 Seq.list_of ((clean_tac @{context} quot defs 1) (ith 3)) *} ML_prf {* profile 2 Seq.list_of ((regularize_tac @{context} @{thms alpha_EQUIVs} 1) (ith 1)) *} +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 {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *}) -prefer 2 -apply(tactic {* clean_tac @{context} quot defs 1 *}) -apply(tactic {* all_inj_repabs_tac @{context} quot rel_refl trans2 1*}) +apply(tactic {* all_inj_repabs_tac @{context} quot rel_refl trans2 1 *}) done (* Does not work: @@ -303,7 +300,7 @@ apply(tactic {* procedure_tac @{context} @{thm kind_ty_trm.induct} 1 *}) apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *}) apply(tactic {* all_inj_repabs_tac @{context} quot rel_refl trans2 1 *}) -apply(tactic {* clean_tac @{context} quot defs 1 *}) +apply(tactic {* clean_tac @{context} quot 1 *}) done print_quotients diff -r bb23a7393de3 -r 6cdba30c6d66 LamEx.thy --- a/LamEx.thy Thu Dec 03 14:00:43 2009 +0100 +++ b/LamEx.thy Thu Dec 03 14:02:05 2009 +0100 @@ -170,13 +170,11 @@ done ML {* val qty = @{typ "lam"} *} -ML {* val defs = @{thms Var_def App_def Lam_def perm_lam_def fv_def} *} ML {* val rsp_thms = @{thms perm_rsp fresh_rsp rVar_rsp rApp_rsp rLam_rsp rfv_rsp} *} 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] rty [quot] defs *} +ML {* fun lift_tac_lam lthy t = lift_tac lthy t [rel_eqv] [quot] *} lemma pi_var: "(pi\('x \ 'x) list) \ Var a = Var (pi \ a)" apply (tactic {* lift_tac_lam @{context} @{thm pi_var_com} 1 *}) @@ -337,7 +335,7 @@ prefer 2 apply (tactic {* all_inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *}) prefer 3 -apply (tactic {* clean_tac @{context} [quot] defs 1 *}) +apply (tactic {* clean_tac @{context} [quot] 1 *}) thm all_prs thm REP_ABS_RSP diff -r bb23a7393de3 -r 6cdba30c6d66 QuotMain.thy --- a/QuotMain.thy Thu Dec 03 14:00:43 2009 +0100 +++ b/QuotMain.thy Thu Dec 03 14:02:05 2009 +0100 @@ -790,24 +790,7 @@ *} ML {* -fun APPLY_RSP_TAC rty = - Subgoal.FOCUS (fn {concl, asms, ...} => - case ((HOLogic.dest_Trueprop (term_of concl))) of - ((_ $ (f $ _) $ (_ $ _))) => - let - val (asmf, asma) = find_qt_asm (map term_of asms); - val pat = Drule.strip_imp_concl (cprop_of @{thm APPLY_RSP}); - val insts = Thm.first_order_match (pat, concl) - in - if (fastype_of asmf) = (fastype_of f) - then no_tac - else rtac (Drule.instantiate insts @{thm APPLY_RSP}) 1 - end - | _ => no_tac) -*} - -ML {* -val APPLY_RSP_TAC' = +val APPLY_RSP_TAC = Subgoal.FOCUS (fn {concl, asms, context,...} => case ((HOLogic.dest_Trueprop (term_of concl))) of ((R2 $ (f $ x) $ (g $ y))) => @@ -953,7 +936,7 @@ THEN' (RANGE [SOLVES' (quotient_tac ctxt quot_thms)]))), (* R (t $ \) (t' $ \) ----> APPLY_RSP provided type of t needs lifting *) - NDT ctxt "A" (APPLY_RSP_TAC' ctxt THEN' + NDT ctxt "A" (APPLY_RSP_TAC ctxt THEN' (RANGE [SOLVES' (quotient_tac ctxt quot_thms), SOLVES' (quotient_tac ctxt quot_thms), quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])), @@ -1107,8 +1090,10 @@ *) ML {* -fun clean_tac lthy quot defs = +fun clean_tac lthy quot = let + val thy = ProofContext.theory_of lthy; + val defs = map (Thm.varifyT o #def) (qconsts_dest thy); val absrep = map (fn x => @{thm QUOTIENT_ABS_REP} OF [x]) quot val meta_absrep = map (fn x => @{thm eq_reflection} OF [x]) absrep; val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quot @@ -1232,7 +1217,7 @@ ML {* (* FIXME/TODO should only get as arguments the rthm like procedure_tac *) -fun lift_tac lthy rthm rel_eqv quot defs = +fun lift_tac lthy rthm rel_eqv quot = ObjectLogic.full_atomize_tac THEN' gen_frees_tac lthy THEN' Subgoal.FOCUS (fn {context, concl, ...} => @@ -1248,7 +1233,7 @@ RANGE [rtac rthm', regularize_tac lthy rel_eqv, rtac thm THEN' all_inj_repabs_tac lthy quot rel_refl trans2, - clean_tac lthy quot defs]] + clean_tac lthy quot]] end) lthy *} diff -r bb23a7393de3 -r 6cdba30c6d66 quotient_def.ML --- a/quotient_def.ML Thu Dec 03 14:00:43 2009 +0100 +++ b/quotient_def.ML Thu Dec 03 14:02:05 2009 +0100 @@ -97,7 +97,7 @@ val ((trm, thm), lthy') = define qconst_bname mx attr absrep_trm lthy val qconst_str = Binding.name_of qconst_bname - fun qcinfo phi = qconsts_transfer phi {qconst = trm, rconst = rhs} + fun qcinfo phi = qconsts_transfer phi {qconst = trm, rconst = rhs, def = thm} val lthy'' = Local_Theory.declaration true (fn phi => qconsts_update_gen qconst_str (qcinfo phi)) lthy' in diff -r bb23a7393de3 -r 6cdba30c6d66 quotient_info.ML --- a/quotient_info.ML Thu Dec 03 14:00:43 2009 +0100 +++ b/quotient_info.ML Thu Dec 03 14:02:05 2009 +0100 @@ -13,11 +13,12 @@ val quotdata_update: string -> (typ * typ * term * thm) -> Proof.context -> Proof.context val quotdata_dest: theory -> quotient_info list - type qconsts_info = {qconst: term, rconst: term} + type qconsts_info = {qconst: term, rconst: term, def: thm} val qconsts_transfer: morphism -> qconsts_info -> qconsts_info val qconsts_lookup: theory -> string -> qconsts_info option val qconsts_update_thy: string -> qconsts_info -> theory -> theory - val qconsts_update_gen: string -> qconsts_info -> Context.generic -> Context.generic + val qconsts_update_gen: string -> qconsts_info -> Context.generic -> Context.generic + val qconsts_dest: theory -> qconsts_info list val print_qconstinfo: Proof.context -> unit val rsp_rules_get: Proof.context -> thm list @@ -120,7 +121,7 @@ (* info about quotient constants *) -type qconsts_info = {qconst: term, rconst: term} +type qconsts_info = {qconst: term, rconst: term, def: thm} structure QConstsData = Theory_Data (type T = qconsts_info Symtab.table @@ -128,18 +129,23 @@ val extend = I val merge = Symtab.merge (K true)) -fun qconsts_transfer phi {qconst, rconst} = +fun qconsts_transfer phi {qconst, rconst, def} = {qconst = Morphism.term phi qconst, - rconst = Morphism.term phi rconst} + rconst = Morphism.term phi rconst, + def = Morphism.thm phi def} val qconsts_lookup = Symtab.lookup o QConstsData.get fun qconsts_update_thy k qcinfo = QConstsData.map (Symtab.update (k, qcinfo)) fun qconsts_update_gen k qcinfo = Context.mapping (qconsts_update_thy k qcinfo) I +fun qconsts_dest thy = + map snd (Symtab.dest (QConstsData.get thy)) + +(* We don't print the definition *) fun print_qconstinfo ctxt = let - fun prt_qconst {qconst, rconst} = + fun prt_qconst {qconst, rconst, def} = Pretty.block (separate (Pretty.brk 1) [Syntax.pretty_term ctxt qconst, Pretty.str ":=",