# HG changeset patch # User Cezary Kaliszyk # Date 1257435837 -3600 # Node ID bd76f0398aa99e1fe47e74ca4a5cb8923576a9cc # Parent 6150e27d18d9ca10177546d44efa4e2413617480 More functionality for lifting list.cases and list.recs. diff -r 6150e27d18d9 -r bd76f0398aa9 FSet.thy --- a/FSet.thy Thu Nov 05 13:47:41 2009 +0100 +++ b/FSet.thy Thu Nov 05 16:43:57 2009 +0100 @@ -175,8 +175,6 @@ ML {* prop_of @{thm fmap_def} *} ML {* val defs = @{thms EMPTY_def IN_def FUNION_def CARD_def INSERT_def fmap_def FOLD_def} *} -ML {* val consts = lookup_quot_consts defs *} -ML {* val defs_sym = add_lower_defs @{context} defs *} lemma memb_rsp: fixes z @@ -272,40 +270,18 @@ apply(auto intro: list_eq.intros) done -lemma fun_rel_id: - "(op = ===> op =) \ op =" - apply (rule eq_reflection) - apply (rule ext) - apply (rule ext) - apply (simp) - apply (auto) - apply (rule ext) - apply (simp) - done - lemma ho_map_rsp: "((op = ===> op =) ===> op \ ===> op \) map map" - by (simp add: fun_rel_id map_rsp) + by (simp add: FUN_REL_EQ map_rsp) lemma map_append : "(map f (a @ b)) \ (map f a) @ (map f b)" by simp (rule list_eq_refl) -lemma op_eq_twice: "(op = ===> op =) = (op =)" - apply (rule ext) - apply (rule ext) - apply (simp add: FUN_REL.simps) - apply auto - apply (rule ext) - apply simp -done - - - lemma ho_fold_rsp: "((op = ===> op = ===> op =) ===> (op = ===> op =) ===> op = ===> op \ ===> op =) fold1 fold1" - apply (auto simp add: op_eq_twice) + apply (auto simp add: FUN_REL_EQ) sorry print_quotients @@ -329,45 +305,51 @@ ML {* lift_thm_fset @{context} @{thm list.induct} *} ML {* lift_thm_fset @{context} @{thm fold1.simps(2)} *} -term list_rec - quotient_def fset_rec::"'a \ ('b \ 'b fset \ 'a \ 'a) \ 'b fset \ 'a" where "fset_rec \ list_rec" -(* ML {* Toplevel.program (fn () => lift_thm_fset @{context} @{thm list.recs(2)}) *} *) +quotient_def + fset_case::"'a \ ('b \ 'b fset \ 'a) \ 'b fset \ 'a" +where + "fset_case \ list_case" + +lemma list_rec_rsp: + "(op = ===> (op = ===> op \ ===> op =) ===> op \ ===> op =) list_rec list_rec" + apply (auto simp add: FUN_REL_EQ) + sorry -thm list.recs(2) -thm list.cases +lemma list_case_rsp: + "(op = ===> (op = ===> op \ ===> op =) ===> op \ ===> op =) list_case list_case" + apply (auto simp add: FUN_REL_EQ) + 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_thm_fset lthy t = lift_thm lthy qty "fset" rsp_thms defs t *} + +ML {* map (lift_thm_fset @{context}) @{thms list.recs} *} +ML {* map (lift_thm_fset @{context}) @{thms list.cases} *} + +(* Construction site starts here *) + + ML {* val consts = lookup_quot_consts defs *} -ML {* val defs_sym = add_lower_defs @{context} defs *} +ML {* val defs_sym = flat (map (add_lower_defs @{context}) defs) *} 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 t_a = atomize_thm @{thm list.recs(2)} *} -ML {* val p_a = cprop_of t_a *} -ML {* val pp = (snd o Thm.dest_abs NONE o snd o Thm.dest_comb o snd o Thm.dest_comb) p_a *} -ML {* needs_lift @{typ "'a list"} @{typ "'a \ 'a list \ 't \ 't"} *} -ML {* cterm_of @{theory} (tyRel @{typ "'a \ 'a list \ 't \ 't"} (Logic.varifyT @{typ "'a list"}) @{term "f::('a list \ 'a list \ bool)"} @{context}) *} - - -ML {* val tt = (my_reg @{context} (@{term list_eq}) ( @{typ "'a list"}) (term_of pp)) *} -ML {* val (_, [R, _]) = strip_comb tt *} -ML {* val (_, [R]) = strip_comb R *} -ML {* val (f, [R1, R2]) = strip_comb R *} -ML {* val (f, [R1, R2]) = strip_comb R2 *} -ML {* val (f, [R1, R2]) = strip_comb R2 *} - -ML {* cterm_of @{theory} R2 *} - (* prove {* build_regularize_goal t_a rty rel @{context} *} ML_prf {* fun tac ctxt = FIRST' [ rtac rel_refl, @@ -385,7 +367,6 @@ apply (atomize(full)) apply (tactic {* REPEAT_ALL_NEW (tac @{context}) 1 *}) done*) - ML {* val t_r = Toplevel.program (fn () => regularize t_a rty rel rel_eqv rel_refl @{context}) *} ML {* val rt = build_repabs_term @{context} t_r consts rty qty @@ -400,10 +381,6 @@ ML_prf {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms *} apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) -"(op = ===> (op = ===> op \ ===> op = ===> op =) ===> op \ ===> op =) list_rec list_rec" -"QUOTIENT op = (id ---> id) (id ---> id)" -"(op = ===> op \ ===> op =) x y" - done ML {* val t_t = Toplevel.program (fn () => @@ -411,17 +388,20 @@ ) *} -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 abs = findabs rty (prop_of (t_a)) *} +ML {* val aps = findaps rty (prop_of (t_a)) *} ML {* val lam_prs_thms = map (make_simp_prs_thm @{context} quot @{thm LAMBDA_PRS}) abs *} ML {* val app_prs_thms = map (applic_prs @{context} rty qty absrep) aps *} ML {* val lam_prs_thms = map Thm.varifyT lam_prs_thms *} -ML {* val t_l = repeat_eqsubst_thm @{context} (app_prs_thms @ lam_prs_thms) t_t *} +ML {* t_t *} +ML {* val t_l0 = repeat_eqsubst_thm @{context} (lam_prs_thms) t_t *} +ML {* val t_l = repeat_eqsubst_thm @{context} (app_prs_thms) t_l0 *} ML {* val (alls, exs) = findallex @{context} rty qty (prop_of t_a); *} ML {* val allthms = map (make_allex_prs_thm @{context} quot @{thm FORALL_PRS}) alls *} ML {* val t_a = MetaSimplifier.rewrite_rule (allthms) t_l *} -ML {* val defs_sym = add_lower_defs @{context} defs *} -ML {* val t_d = repeat_eqsubst_thm @{context} defs_sym t_a *} +ML {* val defs_sym = flat (map (add_lower_defs @{context}) defs) *} +ML {* val t_id = simp_ids @{context} t_a *} +ML {* val t_d = repeat_eqsubst_thm @{context} defs_sym t_id *} ML {* val t_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} t_d *} ML {* ObjectLogic.rulify t_s *} diff -r 6150e27d18d9 -r bd76f0398aa9 LamEx.thy --- a/LamEx.thy Thu Nov 05 13:47:41 2009 +0100 +++ b/LamEx.thy Thu Nov 05 16:43:57 2009 +0100 @@ -259,7 +259,7 @@ ML {* val consts = lookup_quot_consts defs *} ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "lam" *} -ML {* val t_a = atomize_thm @{thm alpha.induct} *} +ML {* val t_a = atomize_thm @{thm alpha.cases} *} (* prove {* build_regularize_goal t_a rty rel @{context} *} ML_prf {* fun tac ctxt = (FIRST' [ @@ -278,13 +278,13 @@ apply (tactic {* tac @{context} 1 *}) *) ML {* val t_r = regularize t_a rty rel rel_eqv rel_refl @{context} *} -(*ML {* +ML {* val rt = build_repabs_term @{context} t_r consts rty qty val rg = Logic.mk_equals ((Thm.prop_of t_r), rt); *} prove rg apply(atomize(full)) -ML_prf {* +(*ML_prf {* fun r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms = (FIRST' [ rtac trans_thm, @@ -308,10 +308,37 @@ ), WEAK_LAMBDA_RES_TAC ctxt ]); +*}*) +ML_prf {* fun r_mk_comb_tac_lam lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms *} +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 {* REPEAT_ALL_NEW (r_mk_comb_tac_lam @{context}) 1 *}) -*) + 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})) *} diff -r 6150e27d18d9 -r bd76f0398aa9 QuotMain.thy --- a/QuotMain.thy Thu Nov 05 13:47:41 2009 +0100 +++ b/QuotMain.thy Thu Nov 05 16:43:57 2009 +0100 @@ -669,14 +669,13 @@ ) *} - - ML {* fun quotient_tac quot_thm = REPEAT_ALL_NEW (FIRST' [ rtac @{thm FUN_QUOTIENT}, rtac quot_thm, - rtac @{thm IDENTITY_QUOTIENT} + rtac @{thm IDENTITY_QUOTIENT}, + (fn i => CHANGED (simp_tac (HOL_ss addsimps @{thms FUN_MAP_I}) i) THEN rtac @{thm IDENTITY_QUOTIENT} i) ]) *} @@ -766,7 +765,8 @@ (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps})) THEN_ALL_NEW (fn _ => no_tac) ), - WEAK_LAMBDA_RES_TAC ctxt + WEAK_LAMBDA_RES_TAC ctxt, + (fn i => CHANGED (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ}) i)) ]) *} @@ -793,26 +793,32 @@ apply (simp_all add: map.simps) done +ML {* +fun simp_ids lthy thm = + thm + |> MetaSimplifier.rewrite_rule @{thms id_def_sym} + |> repeat_eqsubst_thm lthy @{thms FUN_MAP_I id_apply prod_fun_id map_id} +*} + text {* expects atomized definition *} ML {* - fun add_lower_defs_aux ctxt thm = + fun add_lower_defs_aux lthy thm = let val e1 = @{thm fun_cong} OF [thm]; - val f = eqsubst_thm ctxt @{thms fun_map.simps} e1; - val g = MetaSimplifier.rewrite_rule @{thms id_def_sym} f; - val h = repeat_eqsubst_thm ctxt @{thms FUN_MAP_I id_apply prod_fun_id map_id} g + val f = eqsubst_thm lthy @{thms fun_map.simps} e1; + val g = simp_ids lthy f in - thm :: (add_lower_defs_aux ctxt h) + (simp_ids lthy thm) :: (add_lower_defs_aux lthy g) end - handle _ => [thm] + handle _ => [simp_ids lthy thm] *} ML {* -fun add_lower_defs ctxt defs = +fun add_lower_defs lthy def = let - val defs_pre_sym = map symmetric defs - val defs_atom = map atomize_thm defs_pre_sym - val defs_all = flat (map (add_lower_defs_aux ctxt) defs_atom) + val def_pre_sym = symmetric def + val def_atom = atomize_thm def_pre_sym + val defs_all = add_lower_defs_aux lthy def_atom in map Thm.varifyT defs_all end @@ -1012,9 +1018,10 @@ val app_prs_thms = map (applic_prs lthy rty qty absrep) aps; val lam_prs_thms = map (make_simp_prs_thm lthy quot @{thm LAMBDA_PRS}) abs; 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 = flat (map (add_lower_defs lthy) defs); val defs_sym_eq = map (fn x => eq_reflection OF [x]) defs_sym; - val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_l; + val t_id = simp_ids lthy t_l; + val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_id; val t_d = repeat_eqsubst_thm lthy defs_sym t_d0; val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d; val t_rv = ObjectLogic.rulify t_r