# HG changeset patch # User wenzelm # Date 1375883038 -7200 # Node ID 3695ce0f9f96001f8b7d57739885b7ac3fc23a77 # Parent 34c47bc771f28ee1d7dff4b0d01e3cd1988ba137# Parent 73e32ed924b3eeec85966e00deeb8aaad0593d92 merged diff -r 73e32ed924b3 -r 3695ce0f9f96 src/HOL/Tools/Lifting/lifting_setup.ML --- a/src/HOL/Tools/Lifting/lifting_setup.ML Wed Aug 07 15:35:33 2013 +0200 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML Wed Aug 07 15:43:58 2013 +0200 @@ -115,7 +115,8 @@ val pcr_cr_eq = pcr_rel_def |> Drule.cterm_instantiate args_inst - |> Conv.fconv_rule (Conv.arg_conv (Conv.arg1_conv (bottom_rewr_conv (Transfer.get_relator_eq lthy)))) + |> Conv.fconv_rule (Conv.arg_conv (Conv.arg1_conv + (Transfer.bottom_rewr_conv (Transfer.get_relator_eq lthy)))) in case (term_of o Thm.rhs_of) pcr_cr_eq of Const (@{const_name "relcompp"}, _) $ Const ("HOL.eq", _) $ _ => diff -r 73e32ed924b3 -r 3695ce0f9f96 src/HOL/Tools/Lifting/lifting_util.ML --- a/src/HOL/Tools/Lifting/lifting_util.ML Wed Aug 07 15:35:33 2013 +0200 +++ b/src/HOL/Tools/Lifting/lifting_util.ML Wed Aug 07 15:43:58 2013 +0200 @@ -26,7 +26,6 @@ val is_Type: typ -> bool val is_fun_rel: term -> bool val relation_types: typ -> typ * typ - val bottom_rewr_conv: thm list -> conv val mk_HOL_eq: thm -> thm val safe_HOL_meta_eq: thm -> thm end; @@ -107,8 +106,6 @@ ([typ1, typ2], @{typ bool}) => (typ1, typ2) | _ => error "relation_types: not a relation" -fun bottom_rewr_conv rewrs = Conv.bottom_conv (K (Conv.try_conv (Conv.rewrs_conv rewrs))) @{context} - fun mk_HOL_eq r = r RS @{thm meta_eq_to_obj_eq} fun safe_HOL_meta_eq r = mk_HOL_eq r handle Thm.THM _ => r diff -r 73e32ed924b3 -r 3695ce0f9f96 src/HOL/Tools/transfer.ML --- a/src/HOL/Tools/transfer.ML Wed Aug 07 15:35:33 2013 +0200 +++ b/src/HOL/Tools/transfer.ML Wed Aug 07 15:43:58 2013 +0200 @@ -7,6 +7,9 @@ signature TRANSFER = sig + val bottom_rewr_conv: thm list -> conv + val top_rewr_conv: thm list -> conv + val prep_conv: conv val get_transfer_raw: Proof.context -> thm list val get_relator_eq: Proof.context -> thm list @@ -132,6 +135,12 @@ (** Conversions **) +fun bottom_rewr_conv rewrs = Conv.bottom_conv (K (Conv.try_conv (Conv.rewrs_conv rewrs))) @{context} +fun top_rewr_conv rewrs = Conv.top_conv (K (Conv.try_conv (Conv.rewrs_conv rewrs))) @{context} + +fun transfer_rel_conv conv = + Conv.concl_conv ~1 (HOLogic.Trueprop_conv (Conv.fun2_conv (Conv.arg_conv conv))) + val Rel_rule = Thm.symmetric @{thm Rel_def} fun dest_funcT cT = @@ -190,7 +199,7 @@ end handle TERM _ => thm -fun abstract_equalities_transfer thm = +fun abstract_equalities_transfer ctxt thm = let fun dest prop = let @@ -201,26 +210,33 @@ (rel, fn rel' => Logic.list_implies (prems, HOLogic.mk_Trueprop (rel' $ x $ y))) end + val contracted_eq_thm = + Conv.fconv_rule (transfer_rel_conv (bottom_rewr_conv (get_relator_eq ctxt))) thm + handle CTERM _ => thm in - gen_abstract_equalities dest thm + gen_abstract_equalities dest contracted_eq_thm end fun abstract_equalities_relator_eq rel_eq_thm = gen_abstract_equalities (fn x => (x, I)) (rel_eq_thm RS @{thm is_equality_def [THEN iffD2]}) -fun abstract_equalities_domain thm = +fun abstract_equalities_domain ctxt thm = let fun dest prop = let val prems = Logic.strip_imp_prems prop val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop) - val ((dom, x), y) = apfst Term.dest_comb (Term.dest_comb concl) + val ((eq, dom), y) = apfst Term.dest_comb (Term.dest_comb concl) in - (x, fn x' => Logic.list_implies (prems, HOLogic.mk_Trueprop (dom $ x' $ y))) + (dom, fn dom' => Logic.list_implies (prems, HOLogic.mk_Trueprop (eq $ dom' $ y))) end + fun transfer_rel_conv conv = + Conv.concl_conv ~1 (HOLogic.Trueprop_conv (Conv.arg1_conv (Conv.arg_conv conv))) + val contracted_eq_thm = + Conv.fconv_rule (transfer_rel_conv (bottom_rewr_conv (get_relator_eq ctxt))) thm in - gen_abstract_equalities dest thm + gen_abstract_equalities dest contracted_eq_thm end @@ -305,11 +321,11 @@ (** Adding transfer domain rules **) -fun add_transfer_domain_thm thm = - (add_transfer_thm o abstract_equalities_domain o detect_transfer_rules) thm +fun add_transfer_domain_thm thm ctxt = + (add_transfer_thm o abstract_equalities_domain (Context.proof_of ctxt) o detect_transfer_rules) thm ctxt -fun del_transfer_domain_thm thm = - (del_transfer_thm o abstract_equalities_domain o detect_transfer_rules) thm +fun del_transfer_domain_thm thm ctxt = + (del_transfer_thm o abstract_equalities_domain (Context.proof_of ctxt) o detect_transfer_rules) thm ctxt (** Transfer proof method **) @@ -559,11 +575,13 @@ val rule1 = transfer_rule_of_term ctxt false rhs val rules = get_transfer_raw ctxt val eq_rules = get_relator_eq_raw ctxt + val expand_eq_in_rel = transfer_rel_conv (top_rewr_conv [@{thm fun_rel_eq[symmetric,THEN eq_reflection]}]) in EVERY [CONVERSION prep_conv i, rtac @{thm transfer_prover_start} i, - (rtac rule1 THEN_ALL_NEW + ((rtac rule1 ORELSE' (CONVERSION expand_eq_in_rel THEN' rtac rule1)) + THEN_ALL_NEW (REPEAT_ALL_NEW (resolve_tac rules) THEN_ALL_NEW (DETERM o eq_tac eq_rules))) (i+1), rtac @{thm refl} i] end) @@ -657,13 +675,16 @@ (* Attribute for transfer rules *) -val prep_rule = abstract_domains_transfer o abstract_equalities_transfer o Conv.fconv_rule prep_conv +fun prep_rule ctxt thm = + (abstract_domains_transfer o abstract_equalities_transfer ctxt o Conv.fconv_rule prep_conv) thm val transfer_add = - Thm.declaration_attribute (add_transfer_thm o prep_rule) + Thm.declaration_attribute (fn thm => fn ctxt => + (add_transfer_thm o prep_rule (Context.proof_of ctxt)) thm ctxt) val transfer_del = - Thm.declaration_attribute (del_transfer_thm o prep_rule) + Thm.declaration_attribute (fn thm => fn ctxt => + (del_transfer_thm o prep_rule (Context.proof_of ctxt)) thm ctxt) val transfer_attribute = Attrib.add_del transfer_add transfer_del