# HG changeset patch # User Cezary Kaliszyk # Date 1257261439 -3600 # Node ID 3764566c115128764d3132ac4ed43bf9a26381e1 # Parent c18308f60f0ef1434ad4a44d687a63525857522e Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP diff -r c18308f60f0e -r 3764566c1151 FSet.thy --- a/FSet.thy Tue Nov 03 14:04:45 2009 +0100 +++ b/FSet.thy Tue Nov 03 16:17:19 2009 +0100 @@ -309,9 +309,6 @@ ML {* fun lift_thm_fset lthy t = lift_thm lthy qty "fset" rsp_thms defs t *} -lemma eq_r: "a = b \ a \ b" -by (simp add: list_eq_refl) - (* ML {* lift_thm_fset @{context} @{thm neq_Nil_conv} *} *) ML {* lift_thm_fset @{context} @{thm m1} *} ML {* lift_thm_fset @{context} @{thm m2} *} @@ -320,6 +317,7 @@ ML {* lift_thm_fset @{context} @{thm card1_suc} *} (*ML {* lift_thm_fset @{context} @{thm map_append} *}*) ML {* lift_thm_fset @{context} @{thm append_assoc} *} +ML {* lift_thm_fset @{context} @{thm list.induct} *} thm fold1.simps(2) thm list.recs(2) @@ -343,17 +341,13 @@ apply (atomize(full)) apply (tactic {* tac @{context} 1 *}) *) ML {* val ind_r_r = regularize ind_r_a rty rel rel_eqv rel_refl @{context} *} -(* ML {* +(*ML {* val rt = build_repabs_term @{context} ind_r_r consts rty qty val rg = Logic.mk_equals ((Thm.prop_of ind_r_r), rt); *} prove rg apply(atomize(full)) ML_prf {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms *} -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 {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) done*) ML {* val ind_r_t = @@ -365,6 +359,8 @@ ML {* val abs = findabs rty (prop_of (atomize_thm @{thm list.induct})) *} ML {* val aps = findaps rty (prop_of (atomize_thm @{thm list.induct})) *} ML {* val simp_app_prs_thms = map (make_simp_prs_thm @{context} quot @{thm APP_PRS}) aps *} +thm APP_PRS +ML aps ML {* val simp_lam_prs_thms = map (make_simp_prs_thm @{context} quot @{thm LAMBDA_PRS}) abs *} ML {* val ind_r_l = repeat_eqsubst_thm @{context} (simp_app_prs_thms @ simp_lam_prs_thms) ind_r_t *} ML {* val thm = @{thm FORALL_PRS[OF FUN_QUOTIENT[OF QUOTIENT_fset IDENTITY_QUOTIENT]]} *} diff -r c18308f60f0e -r 3764566c1151 LamEx.thy --- a/LamEx.thy Tue Nov 03 14:04:45 2009 +0100 +++ b/LamEx.thy Tue Nov 03 16:17:19 2009 +0100 @@ -282,81 +282,17 @@ ML {* val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms *} ML {* val abs = findabs rty (prop_of (atomize_thm @{thm alpha.induct})) *} ML {* val aps = findaps rty (prop_of (atomize_thm @{thm alpha.induct})) *} -ML {* prop_of (atomize_thm @{thm alpha.induct}) *} -ML {* - fun findall_all rty qty tm = - case tm of - Const (@{const_name All}, T) $ (s as (Abs(_, _, b))) => - let - val tys = findall_all rty qty s - in if needs_lift rty T then - (( T) :: tys) - else tys end - | Abs(_, T, b) => - findall_all rty qty (subst_bound ((Free ("x", T)), b)) - | f $ a => (findall_all rty qty f) @ (findall_all rty qty a) - | _ => []; - fun findall rty qty tm = - map domain_type ( - map (old_exchange_ty rty qty) - (distinct (op =) (findall_all rty qty tm)) - ) -*} -ML {* val alls = findall rty qty (prop_of (atomize_thm @{thm alpha.induct})) *} - -ML {* -fun make_simp_all_prs_thm lthy quot_thm thm typ = - let - val (_, [lty, rty]) = dest_Type typ; - val thy = ProofContext.theory_of lthy; - val (lcty, rcty) = (ctyp_of thy lty, ctyp_of thy rty) - val inst = [NONE, SOME lcty]; - val lpi = Drule.instantiate' inst [] thm; - val tac = - (compose_tac (false, lpi, 1)) THEN_ALL_NEW - (quotient_tac quot_thm); - val gc = Drule.strip_imp_concl (cprop_of lpi); - val t = Goal.prove_internal [] gc (fn _ => tac 1) - in - MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] t - end -*} +ML {* val (alls, exs) = findallex rty qty (prop_of (atomize_thm @{thm alpha.induct})) *} +ML {* val allthms = map (make_allex_prs_thm @{context} quot @{thm FORALL_PRS} ) alls *} +ML {* val exthms = map (make_allex_prs_thm @{context} quot @{thm EXISTS_PRS} ) exs *} +ML {* val t_a = MetaSimplifier.rewrite_rule allthms t_t *} ML {* val simp_app_prs_thms = map (make_simp_prs_thm @{context} quot @{thm APP_PRS}) aps *} -ML {* val aps = @{typ "LamEx.rlam \ bool"} :: aps; *} ML {* val simp_lam_prs_thms = map (make_simp_prs_thm @{context} quot @{thm LAMBDA_PRS}) abs *} -ML {* val t_l = repeat_eqsubst_thm @{context} (simp_app_prs_thms @ simp_lam_prs_thms) t_a *} -ML {* val typ = hd (alls) *} - - -ML {* - val (_, [lty, rty]) = dest_Type typ; - val thy = @{theory}; - val (lcty, rcty) = (ctyp_of thy lty, ctyp_of thy rty) - val inst = [NONE, SOME lcty]; - val lpi = Drule.instantiate' inst [] @{thm FORALL_PRS}; - val tac = - (compose_tac (false, lpi, 1)) THEN_ALL_NEW - (quotient_tac quot); - val gc = Drule.strip_imp_concl (cprop_of lpi); -*} -prove tst: {*term_of gc*} -apply (tactic {*compose_tac (false, lpi, 1) 1 *}) -apply (tactic {*quotient_tac quot 1 *}) -done -thm tst - - - - - -ML {* val thms = (make_simp_all_prs_thm @{context} quot @{thm FORALL_PRS} o domain_type) (hd (rev alls)) *} -ML {* val thm = - @{thm FORALL_PRS[OF FUN_QUOTIENT[OF QUOTIENT_lam FUN_QUOTIENT[OF QUOTIENT_lam IDENTITY_QUOTIENT]]]} *} -ML {* val t_a = simp_allex_prs quot [thm] t_t *} +ML {* val t_l = repeat_eqsubst_thm @{context} (simp_lam_prs_thms) t_a *} +ML {* val t_l1 = repeat_eqsubst_thm @{context} simp_app_prs_thms t_l *} ML {* val defs_sym = add_lower_defs @{context} defs; *} ML {* val defs_sym_eq = map (fn x => eq_reflection OF [x]) defs_sym *} -ML t_l -ML {* val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_l *} +ML {* val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_l1 *} ML {* val t_d = repeat_eqsubst_thm @{context} defs_sym t_d0 *} ML {* val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d *} ML {* val t_r1 = repeat_eqsubst_thm @{context} @{thms fun_map.simps} t_r *} diff -r c18308f60f0e -r 3764566c1151 QuotMain.thy --- a/QuotMain.thy Tue Nov 03 14:04:45 2009 +0100 +++ b/QuotMain.thy Tue Nov 03 16:17:19 2009 +0100 @@ -538,12 +538,13 @@ *} lemma universal_twice: "(\x. (P x \ Q x)) \ ((\x. P x) \ (\x. Q x))" -apply (auto) -done +by auto lemma implication_twice: "(c \ a) \ (a \ b \ d) \ (a \ b) \ (c \ d)" -apply (auto) -done +by auto + +(*lemma equality_twice: "a = c \ b = d \ (a = b \ c = d)" +by auto*) ML {* fun regularize thm rty rel rel_eqv rel_refl lthy = @@ -557,6 +558,7 @@ rtac @{thm universal_twice}, (rtac @{thm impI} THEN' atac), rtac @{thm implication_twice}, + (*rtac @{thm equality_twice},*) EqSubst.eqsubst_tac ctxt [0] [(@{thm equiv_res_forall} OF [rel_eqv]), (@{thm equiv_res_exists} OF [rel_eqv])], @@ -708,21 +710,6 @@ ) *} -ML {* -fun res_forall_rsp_tac ctxt = - (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps})) - THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI} - THEN' instantiate_tac @{thm RES_FORALL_RSP} ctxt THEN' - (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps})) -*} - -ML {* -fun res_exists_rsp_tac ctxt = - (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps})) - THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI} - THEN' instantiate_tac @{thm RES_EXISTS_RSP} ctxt THEN' - (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps})) -*} ML {* @@ -770,6 +757,34 @@ *} ML {* +val res_forall_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} => + let + val _ $ (_ $ (Const (@{const_name Ball}, _) $ _) $ (Const (@{const_name Ball}, _) $ _)) = term_of concl + in + ((simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps})) + THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI} + THEN' instantiate_tac @{thm RES_FORALL_RSP} ctxt THEN' + (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))) 1 + end + handle _ => no_tac + ) +*} + +ML {* +val res_exists_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} => + let + val _ $ (_ $ (Const (@{const_name Bex}, _) $ _) $ (Const (@{const_name Bex}, _) $ _)) = term_of concl + in + ((simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps})) + THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI} + THEN' instantiate_tac @{thm RES_EXISTS_RSP} ctxt THEN' + (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))) 1 + end + handle _ => no_tac + ) +*} + +ML {* fun r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms = (FIRST' [ (* rtac @{thm FUN_QUOTIENT}, @@ -779,10 +794,7 @@ LAMBDA_RES_TAC ctxt, res_forall_rsp_tac ctxt, res_exists_rsp_tac ctxt, - ( - (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps rsp_thms)) - THEN_ALL_NEW (fn _ => no_tac) - ), + FIRST' (map rtac rsp_thms), (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])), rtac refl, (* rtac @{thm arg_cong2[of _ _ _ _ "op ="]},*) @@ -893,17 +905,63 @@ *} ML {* - fun simp_allex_prs quot thms thm = + fun findallex_all rty qty tm = + case tm of + Const (@{const_name All}, T) $ (s as (Abs(_, _, b))) => + let + val (tya, tye) = findallex_all rty qty s + in if needs_lift rty T then + ((T :: tya), tye) + else (tya, tye) end + | Const (@{const_name Ex}, T) $ (s as (Abs(_, _, b))) => + let + val (tya, tye) = findallex_all rty qty s + in if needs_lift rty T then + (tya, (T :: tye)) + else (tya, tye) end + | Abs(_, T, b) => + findallex_all rty qty (subst_bound ((Free ("x", T)), b)) + | f $ a => + let + val (a1, e1) = findallex_all rty qty f; + val (a2, e2) = findallex_all rty qty a; + in (a1 @ a2, e1 @ e2) end + | _ => ([], []); +*} +ML {* + fun findallex rty qty tm = let - val ts = [@{thm FORALL_PRS} OF [quot], @{thm EXISTS_PRS} OF [quot]] @ thms - val sym_ts = map (fn x => @{thm "HOL.sym"} OF [x]) ts; - val eq_ts = map (fn x => @{thm "eq_reflection"} OF [x]) sym_ts + val (a, e) = findallex_all rty qty tm; + val (ad, ed) = (map domain_type a, map domain_type e); + val (au, eu) = (distinct (op =) ad, distinct (op =) ed) in - MetaSimplifier.rewrite_rule eq_ts thm + (map (old_exchange_ty rty qty) au, map (old_exchange_ty rty qty) eu) end *} ML {* +fun make_allex_prs_thm lthy quot_thm thm typ = + let + val (_, [lty, rty]) = dest_Type typ; + val thy = ProofContext.theory_of lthy; + val (lcty, rcty) = (ctyp_of thy lty, ctyp_of thy rty) + val inst = [NONE, SOME lcty]; + val lpi = Drule.instantiate' inst [] thm; + val tac = + (compose_tac (false, lpi, 1)) THEN_ALL_NEW + (quotient_tac quot_thm); + val gc = Drule.strip_imp_concl (cprop_of lpi); + val t = Goal.prove_internal [] gc (fn _ => tac 1) + val t_noid = MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] t; + val t_sym = @{thm "HOL.sym"} OF [t_noid]; + val t_eq = @{thm "eq_reflection"} OF [t_sym] + in + t_eq + end +*} + + +ML {* fun lookup_quot_data lthy qty = let val SOME quotdata = find_first (fn x => matches ((#qtyp x), qty)) (quotdata_lookup lthy) @@ -947,11 +1005,14 @@ val t_a = atomize_thm t; val t_r = regularize t_a rty rel rel_eqv rel_refl lthy; val t_t = repabs lthy t_r consts rty qty quot rel_refl trans2 rsp_thms; + val (alls, exs) = findallex rty qty (prop_of t_a); + val allthms = map (make_allex_prs_thm lthy quot @{thm FORALL_PRS}) alls + val exthms = map (make_allex_prs_thm lthy quot @{thm EXISTS_PRS}) exs + val t_a = MetaSimplifier.rewrite_rule (allthms @ exthms) t_t val abs = findabs rty (prop_of t_a); val aps = findaps rty (prop_of t_a); val app_prs_thms = map (make_simp_prs_thm lthy quot @{thm APP_PRS}) aps; val lam_prs_thms = map (make_simp_prs_thm lthy quot @{thm LAMBDA_PRS}) abs; - val t_a = simp_allex_prs quot [] t_t; val t_l = repeat_eqsubst_thm lthy (lam_prs_thms @ app_prs_thms) t_a; val defs_sym = add_lower_defs lthy defs; val defs_sym_eq = map (fn x => eq_reflection OF [x]) defs_sym;