contract equalities in transfer and transfer domain rules when they are registered
--- a/src/HOL/Tools/transfer.ML Wed Aug 07 15:40:29 2013 +0200
+++ b/src/HOL/Tools/transfer.ML Wed Aug 07 15:40:59 2013 +0200
@@ -199,7 +199,7 @@
end
handle TERM _ => thm
-fun abstract_equalities_transfer thm =
+fun abstract_equalities_transfer ctxt thm =
let
fun dest prop =
let
@@ -210,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
@@ -314,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 **)
@@ -668,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