--- a/src/HOL/Tools/transfer.ML Mon May 13 12:13:24 2013 +0200
+++ b/src/HOL/Tools/transfer.ML Mon May 13 13:59:04 2013 +0200
@@ -1,5 +1,6 @@
(* Title: HOL/Tools/transfer.ML
Author: Brian Huffman, TU Muenchen
+ Author: Ondrej Kuncar, TU Muenchen
Generic theorem transfer method.
*)
@@ -7,12 +8,15 @@
signature TRANSFER =
sig
val prep_conv: conv
+ val get_transfer_raw: Proof.context -> thm list
val get_relator_eq: Proof.context -> thm list
val get_sym_relator_eq: Proof.context -> thm list
val get_relator_eq_raw: Proof.context -> thm list
- val get_transfer_raw: Proof.context -> thm list
+ val get_relator_domain: Proof.context -> thm list
val transfer_add: attribute
val transfer_del: attribute
+ val transfer_domain_add: attribute
+ val transfer_domain_del: attribute
val transfer_rule_of_term: Proof.context -> term -> thm
val transfer_tac: bool -> Proof.context -> int -> tactic
val transfer_prover_tac: Proof.context -> int -> tactic
@@ -31,28 +35,40 @@
known_frees : (string * typ) list,
compound_rhs : unit Net.net,
relator_eq : thm Item_Net.T,
- relator_eq_raw : thm Item_Net.T }
+ relator_eq_raw : thm Item_Net.T,
+ relator_domain : thm Item_Net.T }
val empty =
{ transfer_raw = Thm.full_rules,
known_frees = [],
compound_rhs = Net.empty,
relator_eq = Thm.full_rules,
- relator_eq_raw = Thm.full_rules }
+ relator_eq_raw = Thm.full_rules,
+ relator_domain = Thm.full_rules }
val extend = I
fun merge
( { transfer_raw = t1, known_frees = k1,
compound_rhs = c1, relator_eq = r1,
- relator_eq_raw = rw1 },
+ relator_eq_raw = rw1, relator_domain = rd1 },
{ transfer_raw = t2, known_frees = k2,
compound_rhs = c2, relator_eq = r2,
- relator_eq_raw = rw2 } ) =
+ relator_eq_raw = rw2, relator_domain = rd2 } ) =
{ transfer_raw = Item_Net.merge (t1, t2),
known_frees = Library.merge (op =) (k1, k2),
compound_rhs = Net.merge (K true) (c1, c2),
relator_eq = Item_Net.merge (r1, r2),
- relator_eq_raw = Item_Net.merge (rw1, rw2) }
+ relator_eq_raw = Item_Net.merge (rw1, rw2),
+ relator_domain = Item_Net.merge (rd1, rd2) }
)
+fun get_transfer_raw ctxt = ctxt
+ |> (Item_Net.content o #transfer_raw o Data.get o Context.Proof)
+
+fun get_known_frees ctxt = ctxt
+ |> (#known_frees o Data.get o Context.Proof)
+
+fun get_compound_rhs ctxt = ctxt
+ |> (#compound_rhs o Data.get o Context.Proof)
+
fun get_relator_eq ctxt = ctxt
|> (Item_Net.content o #relator_eq o Data.get o Context.Proof)
|> map safe_mk_meta_eq
@@ -64,34 +80,30 @@
fun get_relator_eq_raw ctxt = ctxt
|> (Item_Net.content o #relator_eq_raw o Data.get o Context.Proof)
-fun get_transfer_raw ctxt = ctxt
- |> (Item_Net.content o #transfer_raw o Data.get o Context.Proof)
-
-fun get_known_frees ctxt = ctxt
- |> (#known_frees o Data.get o Context.Proof)
+fun get_relator_domain ctxt = ctxt
+ |> (Item_Net.content o #relator_domain o Data.get o Context.Proof)
-fun get_compound_rhs ctxt = ctxt
- |> (#compound_rhs o Data.get o Context.Proof)
-
-fun map_data f1 f2 f3 f4 f5
- { transfer_raw, known_frees, compound_rhs, relator_eq, relator_eq_raw } =
+fun map_data f1 f2 f3 f4 f5 f6
+ { transfer_raw, known_frees, compound_rhs, relator_eq, relator_eq_raw, relator_domain } =
{ transfer_raw = f1 transfer_raw,
known_frees = f2 known_frees,
compound_rhs = f3 compound_rhs,
relator_eq = f4 relator_eq,
- relator_eq_raw = f5 relator_eq_raw }
+ relator_eq_raw = f5 relator_eq_raw,
+ relator_domain = f6 relator_domain }
-fun map_transfer_raw f = map_data f I I I I
-fun map_known_frees f = map_data I f I I I
-fun map_compound_rhs f = map_data I I f I I
-fun map_relator_eq f = map_data I I I f I
-fun map_relator_eq_raw f = map_data I I I I f
+fun map_transfer_raw f = map_data f I I I I I
+fun map_known_frees f = map_data I f I I I I
+fun map_compound_rhs f = map_data I I f I I I
+fun map_relator_eq f = map_data I I I f I I
+fun map_relator_eq_raw f = map_data I I I I f I
+fun map_relator_domain f = map_data I I I I I f
fun add_transfer_thm thm = Data.map
(map_transfer_raw (Item_Net.update thm) o
map_compound_rhs
(case HOLogic.dest_Trueprop (Thm.concl_of thm) of
- _ $ _ $ (rhs as (_ $ _)) => Net.insert_term (K true) (rhs, ())
+ (Const (@{const_name Rel}, _)) $ _ $ _ $ (rhs as (_ $ _)) => Net.insert_term (K true) (rhs, ())
| _ => I) o
map_known_frees (Term.add_frees (Thm.concl_of thm)))
@@ -111,20 +123,8 @@
in Drule.instantiate' [SOME cT, SOME cU] [SOME ct] Rel_rule end
(* Conversion to preprocess a transfer rule *)
-fun strip_args n = funpow n (fst o dest_comb)
-
fun safe_Rel_conv ct =
- let
- val head = ct |> term_of |> HOLogic.dest_Trueprop |> strip_args 2
- fun is_known (Const (s, _)) = (s = @{const_name DOM})
- | is_known _ = false
- in
- if not (is_known head)
- then HOLogic.Trueprop_conv (Conv.fun_conv (Conv.fun_conv Rel_conv)) ct
- else Conv.all_conv ct
- end
- handle TERM _ => Conv.all_conv ct
-;
+ Conv.try_conv (HOLogic.Trueprop_conv (Conv.fun_conv (Conv.fun_conv Rel_conv))) ct
fun prep_conv ct = (
Conv.implies_conv safe_Rel_conv prep_conv
@@ -185,6 +185,112 @@
gen_abstract_equalities (fn x => (x, I))
(rel_eq_thm RS @{thm is_equality_def [THEN iffD2]})
+fun abstract_equalities_domain 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)
+ in
+ (x $ y, fn comb' =>
+ let
+ val (x', y') = dest_comb comb'
+ in
+ Logic.list_implies (prems, HOLogic.mk_Trueprop (dom $ x' $ y'))
+ end)
+ end
+ in
+ gen_abstract_equalities dest thm
+ end
+
+
+(** Replacing explicit Domainp predicates with Domainp assumptions **)
+
+fun mk_Domainp_assm (T, R) =
+ HOLogic.mk_eq ((Const (@{const_name Domainp}, Term.fastype_of T --> Term.fastype_of R) $ T), R)
+
+val Domainp_lemma =
+ @{lemma "(!!R. Domainp T = R ==> PROP (P R)) == PROP (P (Domainp T))"
+ by (rule, drule meta_spec,
+ erule meta_mp, rule refl, simp)}
+
+fun fold_Domainp f (t as Const (@{const_name Domainp},_) $ (Var (_,_))) = f t
+ | fold_Domainp f (t $ u) = fold_Domainp f t #> fold_Domainp f u
+ | fold_Domainp f (Abs (_, _, t)) = fold_Domainp f t
+ | fold_Domainp _ _ = I
+
+fun subst_terms tab t =
+ let
+ val t' = Termtab.lookup tab t
+ in
+ case t' of
+ SOME t' => t'
+ | NONE =>
+ (case t of
+ u $ v => (subst_terms tab u) $ (subst_terms tab v)
+ | Abs (a, T, t) => Abs (a, T, subst_terms tab t)
+ | t => t)
+ end
+
+fun gen_abstract_domains (dest : term -> term * (term -> term)) thm =
+ let
+ val thy = Thm.theory_of_thm thm
+ val prop = Thm.prop_of thm
+ val (t, mk_prop') = dest prop
+ val Domainp_tms = rev (fold_Domainp (fn t => insert op= t) t [])
+ val Domainp_Ts = map (snd o dest_funT o snd o dest_Const o fst o dest_comb) Domainp_tms
+ val used = Term.add_free_names t []
+ val rels = map (snd o dest_comb) Domainp_tms
+ val rel_names = map (fst o fst o dest_Var) rels
+ val names = map (fn name => ("D" ^ name)) rel_names |> Name.variant_list used
+ val frees = map Free (names ~~ Domainp_Ts)
+ val prems = map (HOLogic.mk_Trueprop o mk_Domainp_assm) (rels ~~ frees);
+ val t' = subst_terms (fold Termtab.update (Domainp_tms ~~ frees) Termtab.empty) t
+ val prop1 = fold Logic.all frees (Logic.list_implies (prems, mk_prop' t'))
+ val prop2 = Logic.list_rename_params (rev names) prop1
+ val cprop = Thm.cterm_of thy prop2
+ val equal_thm = Raw_Simplifier.rewrite false [Domainp_lemma] cprop
+ fun forall_elim thm = Thm.forall_elim_vars (Thm.maxidx_of thm + 1) thm;
+ in
+ forall_elim (thm COMP (equal_thm COMP @{thm equal_elim_rule2}))
+ end
+ handle TERM _ => thm
+
+fun abstract_domains_transfer thm =
+ let
+ fun dest prop =
+ let
+ val prems = Logic.strip_imp_prems prop
+ val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop)
+ val ((rel, x), y) = apfst Term.dest_comb (Term.dest_comb concl)
+ in
+ (x, fn x' =>
+ Logic.list_implies (prems, HOLogic.mk_Trueprop (rel $ x' $ y)))
+ end
+ in
+ gen_abstract_domains dest thm
+ end
+
+fun detect_transfer_rules thm =
+ let
+ fun is_transfer_rule tm = case (HOLogic.dest_Trueprop tm) of
+ (Const (@{const_name HOL.eq}, _)) $ ((Const (@{const_name Domainp}, _)) $ _) $ _ => false
+ | _ $ _ $ _ => true
+ | _ => false
+ fun safe_transfer_rule_conv ctm =
+ if is_transfer_rule (term_of ctm) then safe_Rel_conv ctm else Conv.all_conv ctm
+ in
+ Conv.fconv_rule (Conv.prems_conv ~1 safe_transfer_rule_conv) thm
+ end
+
+(** Adding transfer domain rules **)
+
+fun add_transfer_domain_thm thm =
+ (add_transfer_thm o abstract_equalities_domain o detect_transfer_rules) thm
+
+fun del_transfer_domain_thm thm =
+ (del_transfer_thm o abstract_equalities_domain o detect_transfer_rules) thm
(** Transfer proof method **)
@@ -363,7 +469,7 @@
(* Attribute for transfer rules *)
-val prep_rule = abstract_equalities_transfer o Conv.fconv_rule prep_conv
+val prep_rule = abstract_domains_transfer o abstract_equalities_transfer o Conv.fconv_rule prep_conv
val transfer_add =
Thm.declaration_attribute (add_transfer_thm o prep_rule)
@@ -374,6 +480,15 @@
val transfer_attribute =
Attrib.add_del transfer_add transfer_del
+(* Attributes for transfer domain rules *)
+
+val transfer_domain_add = Thm.declaration_attribute add_transfer_domain_thm
+
+val transfer_domain_del = Thm.declaration_attribute del_transfer_domain_thm
+
+val transfer_domain_attribute =
+ Attrib.add_del transfer_domain_add transfer_domain_del
+
(* Theory setup *)
val relator_eq_setup =
@@ -392,12 +507,32 @@
#> Global_Theory.add_thms_dynamic (name, content)
end
+val relator_domain_setup =
+ let
+ val name = @{binding relator_domain}
+ fun add_thm thm = Data.map (map_relator_domain (Item_Net.update thm))
+ #> add_transfer_domain_thm thm
+ fun del_thm thm = Data.map (map_relator_domain (Item_Net.remove thm))
+ #> del_transfer_domain_thm thm
+ val add = Thm.declaration_attribute add_thm
+ val del = Thm.declaration_attribute del_thm
+ val text = "declaration of relator domain rule (used by transfer method)"
+ val content = Item_Net.content o #relator_domain o Data.get
+ in
+ Attrib.setup name (Attrib.add_del add del) text
+ #> Global_Theory.add_thms_dynamic (name, content)
+ end
+
+
val setup =
relator_eq_setup
+ #> relator_domain_setup
#> Attrib.setup @{binding transfer_rule} transfer_attribute
"transfer rule for transfer method"
#> Global_Theory.add_thms_dynamic
(@{binding transfer_raw}, Item_Net.content o #transfer_raw o Data.get)
+ #> Attrib.setup @{binding transfer_domain_rule} transfer_domain_attribute
+ "transfer domain rule for transfer method"
#> Global_Theory.add_thms_dynamic
(@{binding relator_eq_raw}, Item_Net.content o #relator_eq_raw o Data.get)
#> Method.setup @{binding transfer} (transfer_method true)