# HG changeset patch # User Cezary Kaliszyk # Date 1256742359 -3600 # Node ID f219011a5e3ce161793b96cd14d16e5a006fd2ab # Parent 329111e1c4baf6ec2eebc840d3f831884b8549bb Fixes diff -r 329111e1c4ba -r f219011a5e3c FSet.thy --- a/FSet.thy Wed Oct 28 15:25:36 2009 +0100 +++ b/FSet.thy Wed Oct 28 16:05:59 2009 +0100 @@ -306,8 +306,12 @@ apply (metis) done +ML {* (atomize_thm @{thm list_induct_hol4}) *} + +ML {* regularise (prop_of (atomize_thm @{thm list_induct_hol4})) @{typ "'a list"} @{term "op \"} @{context} *} + prove list_induct_r: {* - build_regularize_goal (atomize_thm @{thm list_induct_hol4}) @{typ "'a List.list"} @{term "op \"} @{context} *} + build_regularize_goal (atomize_thm @{thm list_induct_hol4}) @{typ "'a list"} @{term "op \"} @{context} *} apply (simp only: equiv_res_forall[OF equiv_list_eq]) thm RIGHT_RES_FORALL_REGULAR apply (rule RIGHT_RES_FORALL_REGULAR) diff -r 329111e1c4ba -r f219011a5e3c IntEx.thy --- a/IntEx.thy Wed Oct 28 15:25:36 2009 +0100 +++ b/IntEx.thy Wed Oct 28 16:05:59 2009 +0100 @@ -156,7 +156,7 @@ text {* Below is the construction site code used if things do now work *} -ML {* val t_a = atomize_thm @{thm plus_assoc_pre} *} +ML {* val t_a = atomize_thm @{thm plus_sym_pre} *} ML {* val t_r = regularize t_a rty rel rel_eqv @{context} *} ML {* val t_t = @@ -170,19 +170,13 @@ ML {* val abs = findabs rty (prop_of (atomize_thm @{thm plus_sym_pre})) *} ML {* val simp_lam_prs_thms = map (make_simp_lam_prs_thm @{context} quot) abs *} - -ML {* - fun simp_lam_prs lthy thm = - simp_lam_prs lthy (eqsubst_thm lthy simp_lam_prs_thms thm) - handle _ => thm -*} ML {* t_t *} -ML {* val t_l = simp_lam_prs @{context} t_t *} +ML {* val t_l = repeat_eqsubst_thm @{context} simp_lam_prs_thms t_t *} ML {* val t_a = simp_allex_prs @{context} quot t_l *} ML {* val t_defs_sym = add_lower_defs @{context} t_defs *} -ML {* val t_d = MetaSimplifier.rewrite_rule t_defs_sym t_a *} +ML {* val t_d = repeat_eqsubst_thm @{context} t_defs_sym t_a *} ML {* val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d *} ML {* ObjectLogic.rulify t_r *} diff -r 329111e1c4ba -r f219011a5e3c LamEx.thy --- a/LamEx.thy Wed Oct 28 15:25:36 2009 +0100 +++ b/LamEx.thy Wed Oct 28 16:05:59 2009 +0100 @@ -73,14 +73,88 @@ ML {* val t_b = MetaSimplifier.rewrite_rule [reps_same] t_d *} ML {* ObjectLogic.rulify t_b *} +thm fresh_def +thm supp_def + local_setup {* - make_const_def @{binding lfresh} @{term "fresh :: 'a \ rlam \ bool"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd #> make_const_def @{binding lperm} @{term "perm :: ('a \ 'a) list \ rlam \ rlam"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd *} -ML {* val consts = @{const_name fresh} :: @{const_name perm} :: consts *} -ML {* val defs = @{thms lfresh_def lperm_def} @ defs *} +ML {* val consts = @{const_name perm} :: consts *} +ML {* val defs = @{thms lperm_def} @ defs *} +ML {* val t_u = MetaSimplifier.rewrite_rule @{thms fresh_def supp_def} @{thm a3} *} +ML {* val t_a = atomize_thm t_u *} +ML {* val t_r = regularize t_a rty rel rel_eqv @{context} *} + +ML {* +fun r_mk_comb_tac_lam ctxt = r_mk_comb_tac ctxt rty quot rel_refl trans2 rsp_thms +*} + +prove {* build_repabs_goal @{context} t_r consts rty qty *} +apply (atomize(full)) +apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) +apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) +apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) +apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) +apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) +apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) +apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) +apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) +apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) +apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) +apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) +apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) +apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) +apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) +apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) +apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) +apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) +apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) +apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) +apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) +apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) +apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) +apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) +apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) +apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) +apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) +apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) +apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) +prefer 2 +apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_lam @{context}) 1 *}) +apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) +apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) +apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) +apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) +apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) +apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) +apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) +apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) +apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) +apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) +apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) +apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) +apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) +apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) +apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) +apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) +apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) +apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) +nitpick +apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) +apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) +apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) + + + + + + + ML {* val t_t = Toplevel.program (fn () => repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms) *} + +ML {* val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms *} + ML {* val t_l = repeat_eqsubst_thm @{context} simp_lam_prs_thms t_t *} ML {* val t_c = simp_allex_prs @{context} quot t_l *} ML {* val t_defs_sym = add_lower_defs @{context} defs *} @@ -94,7 +168,11 @@ - +local_setup {* + make_const_def @{binding lfresh} @{term "fresh :: 'a \ rlam \ bool"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd #> +*} +@{const_name fresh} :: +lfresh_def ML {* fun lift_thm_lam lthy t = lift_thm lthy consts rty qty rel rel_eqv rel_refl quot rsp_thms trans2 reps_same defs t diff -r 329111e1c4ba -r f219011a5e3c QuotMain.thy --- a/QuotMain.thy Wed Oct 28 15:25:36 2009 +0100 +++ b/QuotMain.thy Wed Oct 28 16:05:59 2009 +0100 @@ -397,10 +397,10 @@ ML {* fun atomize_thm thm = let - val thm' = forall_intr_vars thm + val thm' = Thm.freezeT (forall_intr_vars thm) val thm'' = ObjectLogic.atomize (cprop_of thm') in - Thm.freezeT @{thm Pure.equal_elim_rule1} OF [thm'', thm'] + @{thm Pure.equal_elim_rule1} OF [thm'', thm'] end *} diff -r 329111e1c4ba -r f219011a5e3c isar-keywords-prove.el --- a/isar-keywords-prove.el Wed Oct 28 15:25:36 2009 +0100 +++ b/isar-keywords-prove.el Wed Oct 28 16:05:59 2009 +0100 @@ -127,6 +127,7 @@ "method_setup" "moreover" "next" + "nitpick" "no_notation" "no_syntax" "no_translations" @@ -580,6 +581,7 @@ "apply_end" "back" "defer" + "nitpick" "prefer")) (provide 'isar-keywords)