# HG changeset patch # User Cezary Kaliszyk # Date 1256898329 -3600 # Node ID 02b14a21761a3217b7dec72ce7b8e953e77d16f1 # Parent e9cc3a3aa5d195b96333cc4d20ffb8456af457ed Cleaning of the interface to lift. diff -r e9cc3a3aa5d1 -r 02b14a21761a FSet.thy --- a/FSet.thy Thu Oct 29 17:35:03 2009 +0100 +++ b/FSet.thy Fri Oct 30 11:25:29 2009 +0100 @@ -177,17 +177,9 @@ term fmap thm fmap_def -ML {* val fset_defs = @{thms EMPTY_def IN_def FUNION_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 *} *) - -ML {* - val consts = [@{const_name "Nil"}, @{const_name "Cons"}, - @{const_name "membship"}, @{const_name "card1"}, - @{const_name "append"}, @{const_name "fold1"}, - @{const_name "map"}]; -*} - -ML {* val fset_defs_sym = add_lower_defs @{context} fset_defs *} +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 @@ -303,29 +295,15 @@ ((map f a) ::'a list) @ (map f b)" by simp (rule list_eq_refl) -ML {* val rty = @{typ "'a list"} *} ML {* val qty = @{typ "'a fset"} *} -ML {* val rel = @{term "list_eq"} *} -ML {* val rel_eqv = (#equiv_thm o hd) (quotdata_lookup @{context}) *} -ML {* val rel_refl = @{thm list_eq_refl} *} -ML {* val quot = @{thm QUOTIENT_fset} *} +ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} +ML {* val (trans2, reps_same, quot) = lookup_quot_thms @{context} "fset" *} + ML {* val rsp_thms = @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp} @ @{thms ho_all_prs ho_ex_prs} *} -ML {* val trans2 = @{thm QUOT_TYPE_I_fset.R_trans2} *} -ML {* val reps_same = @{thm QUOT_TYPE_I_fset.REPS_same} *} -ML {* val defs = fset_defs *} -(* ML {* val consts = map (fst o dest_Const o fst o Logic.dest_equals o concl_of) fset_defs *} *) -ML {* - val consts = [@{const_name "Nil"}, @{const_name "Cons"}, - @{const_name "membship"}, @{const_name "card1"}, - @{const_name "append"}, @{const_name "fold1"}, - @{const_name "map"}]; -*} -ML {* fun lift_thm_fset lthy t = - lift_thm lthy consts rty qty rel rel_eqv rel_refl quot rsp_thms trans2 reps_same defs t -*} +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) @@ -342,17 +320,17 @@ thm list.recs(2) ML {* val ind_r_a = atomize_thm @{thm list.induct} *} -(* prove {* build_regularize_goal ind_r_a @{typ "'a List.list"} @{term "op \"} @{context} *} +(* prove {* build_regularize_goal ind_r_a rty rel @{context} *} ML_prf {* fun tac ctxt = (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps - [(@{thm equiv_res_forall} OF [@{thm equiv_list_eq}]), - (@{thm equiv_res_exists} OF [@{thm equiv_list_eq}])])) THEN_ALL_NEW + [(@{thm equiv_res_forall} OF [rel_eqv]), + (@{thm equiv_res_exists} OF [rel_eqv])])) THEN_ALL_NEW (((rtac @{thm RIGHT_RES_FORALL_REGULAR}) THEN' (RANGE [fn _ => all_tac, atac]) THEN' (MetisTools.metis_tac ctxt [])) ORELSE' (MetisTools.metis_tac ctxt [])); *} apply (tactic {* tac @{context} 1 *}) *) -ML {* val ind_r_r = regularize ind_r_a @{typ "'a List.list"} @{term "op \"} @{thm equiv_list_eq} @{context} *} +ML {* val ind_r_r = regularize ind_r_a rty rel rel_eqv @{context} *} ML {* - val rt = build_repabs_term @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"} + 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 @@ -361,9 +339,7 @@ done*) ML {* val ind_r_t = Toplevel.program (fn () => - repabs @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"} - @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2} - (@{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp} @ @{thms ho_all_prs ho_ex_prs}) + repabs @{context} ind_r_r consts rty qty quot rel_refl trans2 rsp_thms ) *} ML {* val abs = findabs rty (prop_of (atomize_thm @{thm list.induct})) *} diff -r e9cc3a3aa5d1 -r 02b14a21761a IntEx.thy --- a/IntEx.thy Thu Oct 29 17:35:03 2009 +0100 +++ b/IntEx.thy Fri Oct 30 11:25:29 2009 +0100 @@ -12,6 +12,8 @@ apply(auto simp add: mem_def expand_fun_eq) done +print_theorems + quotient_def (for my_int) ZERO::"my_int" where @@ -114,21 +116,18 @@ "(intrel ===> intrel ===> intrel) my_plus my_plus" by (simp) -ML {* val consts = [@{const_name "my_plus"}] *} -ML {* val rty = @{typ "nat \ nat"} *} ML {* val qty = @{typ "my_int"} *} -ML {* val rel = @{term "intrel"} *} -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_my_int} *} +ML {* val ty_name = "my_int" *} ML {* val rsp_thms = @{thms ho_plus_rsp} @ @{thms ho_all_prs ho_ex_prs} *} -ML {* val trans2 = @{thm QUOT_TYPE_I_my_int.R_trans2} *} -ML {* val reps_same = @{thm QUOT_TYPE_I_my_int.REPS_same} *} ML {* val t_defs = @{thms PLUS_def} *} ML {* fun lift_thm_my_int lthy t = - lift_thm lthy consts rty qty rel rel_eqv rel_refl quot rsp_thms trans2 reps_same t_defs t + lift_thm lthy qty ty_name rsp_thms t_defs t +*} + +ML {* + val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty; *} ML {* lift_thm_my_int @{context} @{thm plus_sym_pre} *} diff -r e9cc3a3aa5d1 -r 02b14a21761a QuotMain.thy --- a/QuotMain.thy Thu Oct 29 17:35:03 2009 +0100 +++ b/QuotMain.thy Fri Oct 30 11:25:29 2009 +0100 @@ -950,7 +950,46 @@ *} ML {* -fun lift_thm lthy consts rty qty rel rel_eqv rel_refl quot rsp_thms trans2 reps_same t_defs t = let +fun lookup_quot_data lthy qty = + let + val SOME quotdata = find_first (fn x => #qtyp x = qty) (quotdata_lookup lthy) + val rty = #rtyp quotdata + val rel = #rel quotdata + val rel_eqv = #equiv_thm quotdata + val rel_refl_pre = @{thm EQUIV_REFL} OF [rel_eqv] + val rel_refl = @{thm spec} OF [MetaSimplifier.rewrite_rule [@{thm REFL_def}] rel_refl_pre] + in + (rty, rel, rel_refl, rel_eqv) + end +*} + +ML {* +fun lookup_quot_thms lthy qty_name = + let + val thy = ProofContext.theory_of lthy; + val trans2 = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".R_trans2") + val reps_same = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".REPS_same") + val quot = PureThy.get_thm thy ("QUOTIENT_" ^ qty_name) + in + (trans2, reps_same, quot) + end +*} + +ML {* +fun lookup_quot_consts defs = + let + fun dest_term (a $ b) = (a, b); + val def_terms = map (snd o Logic.dest_equals o concl_of) defs; + in + map (fst o dest_Const o snd o dest_term) def_terms + end +*} + +ML {* +fun lift_thm lthy qty qty_name rsp_thms defs t = let + val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data lthy qty; + val (trans2, reps_same, quot) = lookup_quot_thms lthy qty_name; + val consts = lookup_quot_consts defs; val t_a = atomize_thm t; val t_r = regularize t_a rty rel rel_eqv lthy; val t_t = repabs lthy t_r consts rty qty quot rel_refl trans2 rsp_thms; @@ -958,12 +997,14 @@ val simp_lam_prs_thms = map (make_simp_lam_prs_thm lthy quot) abs; val t_l = repeat_eqsubst_thm lthy simp_lam_prs_thms t_t; val t_a = simp_allex_prs lthy quot t_l; - val t_defs_sym = add_lower_defs lthy t_defs; - val t_d = repeat_eqsubst_thm lthy t_defs_sym t_a; + val defs_sym = add_lower_defs lthy defs; + val t_d = repeat_eqsubst_thm lthy defs_sym t_a; val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d; in ObjectLogic.rulify t_r end *} + end +