# HG changeset patch # User Cezary Kaliszyk # Date 1256744937 -3600 # Node ID 9b8e039ae960a7c380a6dbd94c883b91cca9550a # Parent f9a25fe220377fb5bca81d62062a092fc8d14970 Some cleaning diff -r f9a25fe22037 -r 9b8e039ae960 FSet.thy --- a/FSet.thy Wed Oct 28 16:16:38 2009 +0100 +++ b/FSet.thy Wed Oct 28 16:48:57 2009 +0100 @@ -158,16 +158,15 @@ term fold thm fold_def -local_setup {* - old_make_const_def @{binding fmap} @{term "map::('a \ 'a) \ 'a list \ 'a list"} NoSyn - @{typ "'a list"} @{typ "'a fset"} #> snd -*} +quotient_def (for "'a fset") + fmap::"('a \ 'a) \ 'a fset \ 'a fset" +where + "fmap \ (map::('a \ 'a) \ 'a list \ 'a list)" term map term fmap thm fmap_def - ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def fmap_def fold_def} *} (* ML {* val consts = map (fst o dest_Const o fst o Logic.dest_equals o concl_of) fset_defs *} *) diff -r f9a25fe22037 -r 9b8e039ae960 LamEx.thy --- a/LamEx.thy Wed Oct 28 16:16:38 2009 +0100 +++ b/LamEx.thy Wed Oct 28 16:48:57 2009 +0100 @@ -53,7 +53,7 @@ ML {* val rty = @{typ "rlam"} *} ML {* val qty = @{typ "lam"} *} ML {* val rel = @{term "alpha"} *} -ML {* val rel_eqv = (#equiv_thm o hd) (quotdata_lookup @{theory}) *} +ML {* val rel_eqv = (#equiv_thm o hd) (quotdata_lookup @{context}) *} ML {* val rel_refl = @{thm EQUIV_REFL} OF [rel_eqv] *} ML {* val quot = @{thm QUOTIENT_lam} *} ML {* val rsp_thms = @{thms perm_rsp fresh_rsp rLam_rsp} @ @{thms ho_all_prs ho_ex_prs} *} @@ -77,94 +77,33 @@ thm supp_def local_setup {* - make_const_def @{binding lperm} @{term "perm :: ('a \ 'a) list \ rlam \ rlam"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd + old_make_const_def @{binding lperm} @{term "perm :: ('a \ 'a) list \ rlam \ rlam"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd *} 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_a = atomize_thm @{thm a3} *} 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 *} ML {* val t_d = repeat_eqsubst_thm @{context} t_defs_sym t_c *} ML {* val t_b = MetaSimplifier.rewrite_rule [reps_same] t_d *} -ML {* ObjectLogic.rulify t_b *} ML {* val rr = (add_lower_defs @{context} @{thms lperm_def}) *} -ML {* val rrr = @{thm eq_reflection} OF [rr] *} -ML {* MetaSimplifier.rewrite_rule [rrr] t_b *} +ML {* val rrr = @{thm eq_reflection} OF [hd (rev rr)] *} +lemma prod_fun_id: "prod_fun id id = id" + apply (simp add: prod_fun_def) +done +lemma map_id: "map id x = x" + apply (induct x) + apply (simp_all add: map.simps) +done +ML {* val rrrr = repeat_eqsubst_thm @{context} @{thms prod_fun_id map_id} rrr *} +ML {* val t_b' = eqsubst_thm @{context} [rrrr] t_b *} +ML {* ObjectLogic.rulify t_b' *}