# HG changeset patch # User Cezary Kaliszyk # Date 1259309792 -3600 # Node ID f24fd4689d0036f9bdbcb6833e59dc0851f4ee02 # Parent cb81b40137c25ab577643a45ee3b34dd46abf168 Cleaning of LFex. Lambda_prs fails to unify in 2 places. diff -r cb81b40137c2 -r f24fd4689d00 LFex.thy --- a/LFex.thy Fri Nov 27 08:22:46 2009 +0100 +++ b/LFex.thy Fri Nov 27 09:16:32 2009 +0100 @@ -296,13 +296,27 @@ \ P3 (LAM A x M) (LAM A' x' M')\ \ ((x1 :: KIND) = x2 \ P1 x1 x2) \ ((x3 ::TY) = x4 \ P2 x3 x4) \ ((x5 :: TRM) = x6 \ P3 x5 x6)" +apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *}) +ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *} +ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm akind_aty_atrm.induct})) (term_of qtm) *} apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *}) apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *}) prefer 2 -thm QUOTIENT_TY -apply (tactic {* clean_tac @{context} @{thms QUOTIENT_KIND QUOTIENT_TY QUOTIENT_TRM} defs [] 1 *}) +ML_prf {* val quot = @{thms QUOTIENT_KIND QUOTIENT_TY QUOTIENT_TRM} *} +apply (tactic {* REPEAT_ALL_NEW (allex_prs_tac @{context} quot) 1 *}) +apply (tactic {* lambda_prs_tac @{context} quot 1 *}) +ML_prf {* val absrep = map (fn x => @{thm QUOTIENT_ABS_REP} OF [x]) quot *} +ML_prf {* val aps_thms = map (applic_prs @{context} absrep) aps *} +apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) +ML_prf {* val lower = flat (map (add_lower_defs @{context}) defs) *} +apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] lower) 1 *}) +ML_prf {* val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quot *} +apply (tactic {* simp_tac (HOL_ss addsimps reps_same) 1 *}) +apply (tactic {* lambda_prs_tac @{context} quot 1 *}) +apply (tactic {* clean_tac @{context} defs aps 1 *}) +ML_prf {* *} print_quotients apply(tactic {* r_mk_comb_tac' @{context} rty [quot] rel_refl trans2 [] 1*})