(* Title: HOL/Tools/transfer.ML
Author: Brian Huffman, TU Muenchen
Author: Ondrej Kuncar, TU Muenchen
Generic theorem transfer method.
*)
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_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
val setup: theory -> theory
end
structure Transfer : TRANSFER =
struct
(** Theory Data **)
structure Data = Generic_Data
(
type T =
{ transfer_raw : thm Item_Net.T,
known_frees : (string * typ) list,
compound_rhs : unit Net.net,
relator_eq : 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_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_domain = rd1 },
{ transfer_raw = t2, known_frees = k2,
compound_rhs = c2, relator_eq = r2,
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_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
fun get_sym_relator_eq ctxt = ctxt
|> (Item_Net.content o #relator_eq o Data.get o Context.Proof)
|> map (Thm.symmetric o safe_mk_meta_eq)
fun get_relator_eq_raw ctxt = ctxt
|> (Item_Net.content o #relator_eq_raw 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 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_domain = f6 relator_domain }
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
(Const (@{const_name Rel}, _)) $ _ $ _ $ (rhs as (_ $ _)) => Net.insert_term (K true) (rhs, ())
| _ => I) o
map_known_frees (Term.add_frees (Thm.concl_of thm)))
fun del_transfer_thm thm = Data.map (map_transfer_raw (Item_Net.remove thm))
(** Conversions **)
val Rel_rule = Thm.symmetric @{thm Rel_def}
fun dest_funcT cT =
(case Thm.dest_ctyp cT of [T, U] => (T, U)
| _ => raise TYPE ("dest_funcT", [Thm.typ_of cT], []))
fun Rel_conv ct =
let val (cT, cT') = dest_funcT (Thm.ctyp_of_term ct)
val (cU, _) = dest_funcT cT'
in Drule.instantiate' [SOME cT, SOME cU] [SOME ct] Rel_rule end
(* Conversion to preprocess a transfer rule *)
fun safe_Rel_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
else_conv
safe_Rel_conv
else_conv
Conv.all_conv) ct
(** Replacing explicit equalities with is_equality premises **)
fun mk_is_equality t =
Const (@{const_name is_equality}, Term.fastype_of t --> HOLogic.boolT) $ t
val is_equality_lemma =
@{lemma "(!!R. is_equality R ==> PROP (P R)) == PROP (P (op =))"
by (unfold is_equality_def, rule, drule meta_spec,
erule meta_mp, rule refl, simp)}
fun gen_abstract_equalities (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 add_eqs = Term.fold_aterms
(fn t as Const (@{const_name HOL.eq}, _) => insert (op =) t | _ => I)
val eq_consts = rev (add_eqs t [])
val eqTs = map (snd o dest_Const) eq_consts
val used = Term.add_free_names prop []
val names = map (K "") eqTs |> Name.variant_list used
val frees = map Free (names ~~ eqTs)
val prems = map (HOLogic.mk_Trueprop o mk_is_equality) frees
val prop1 = mk_prop' (Term.subst_atomic (eq_consts ~~ frees) t)
val prop2 = fold Logic.all frees (Logic.list_implies (prems, prop1))
val cprop = Thm.cterm_of thy prop2
val equal_thm = Raw_Simplifier.rewrite false [is_equality_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_equalities_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
(rel, fn rel' =>
Logic.list_implies (prems, HOLogic.mk_Trueprop (rel' $ x $ y)))
end
in
gen_abstract_equalities dest 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 =
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, fn x' => Logic.list_implies (prems, HOLogic.mk_Trueprop (dom $ x' $ y)))
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 **)
val post_simps =
@{thms transfer_forall_eq [symmetric]
transfer_implies_eq [symmetric] transfer_bforall_unfold}
fun gen_frees_tac keepers ctxt = SUBGOAL (fn (t, i) =>
let
val keepers = keepers @ get_known_frees ctxt
val vs = rev (Term.add_frees t [])
val vs' = filter_out (member (op =) keepers) vs
in
Induct.arbitrary_tac ctxt 0 vs' i
end)
fun mk_relT (T, U) = T --> U --> HOLogic.boolT
fun mk_Rel t =
let val T = fastype_of t
in Const (@{const_name Transfer.Rel}, T --> T) $ t end
fun transfer_rule_of_terms ctxt tab t u =
let
val thy = Proof_Context.theory_of ctxt
(* precondition: T must consist of only TFrees and function space *)
fun rel (T as TFree (a, _)) U =
Free (the (AList.lookup (op =) tab a), mk_relT (T, U))
| rel (T as Type ("fun", [T1, T2])) (U as Type ("fun", [U1, U2])) =
let
val r1 = rel T1 U1
val r2 = rel T2 U2
val rT = fastype_of r1 --> fastype_of r2 --> mk_relT (T, U)
in
Const (@{const_name fun_rel}, rT) $ r1 $ r2
end
| rel T U = raise TYPE ("rel", [T, U], [])
fun zip _ thms (Bound i) (Bound _) = (nth thms i, [])
| zip ctxt thms (Abs (x, T, t)) (Abs (y, U, u)) =
let
val ([x', y'], ctxt') = Variable.variant_fixes [x, y] ctxt
val prop = mk_Rel (rel T U) $ Free (x', T) $ Free (y', U)
val cprop = Thm.cterm_of thy (HOLogic.mk_Trueprop prop)
val thm0 = Thm.assume cprop
val (thm1, hyps) = zip ctxt' (thm0 :: thms) t u
val ((r1, x), y) = apfst Thm.dest_comb (Thm.dest_comb (Thm.dest_arg cprop))
val r2 = Thm.dest_fun2 (Thm.dest_arg (cprop_of thm1))
val (a1, (b1, _)) = apsnd dest_funcT (dest_funcT (ctyp_of_term r1))
val (a2, (b2, _)) = apsnd dest_funcT (dest_funcT (ctyp_of_term r2))
val tinsts = [SOME a1, SOME b1, SOME a2, SOME b2]
val insts = [SOME (Thm.dest_arg r1), SOME (Thm.dest_arg r2)]
val rule = Drule.instantiate' tinsts insts @{thm Rel_abs}
val thm2 = Thm.forall_intr x (Thm.forall_intr y (Thm.implies_intr cprop thm1))
in
(thm2 COMP rule, hyps)
end
| zip ctxt thms (f $ t) (g $ u) =
let
val (thm1, hyps1) = zip ctxt thms f g
val (thm2, hyps2) = zip ctxt thms t u
in
(thm2 RS (thm1 RS @{thm Rel_app}), hyps1 @ hyps2)
end
| zip _ _ (t as Free (_, T)) u =
let
val U = fastype_of u
val prop = mk_Rel (rel T U) $ t $ u
val cprop = Thm.cterm_of thy (HOLogic.mk_Trueprop prop)
in
(Thm.assume cprop, [cprop])
end
| zip _ _ t u = raise TERM ("zip_relterm", [t, u])
val r = mk_Rel (rel (fastype_of t) (fastype_of u))
val goal = HOLogic.mk_Trueprop (r $ t $ u)
val rename = Thm.trivial (cterm_of thy goal)
val (thm, hyps) = zip ctxt [] t u
in
Drule.implies_intr_list hyps (thm RS rename)
end
fun transfer_rule_of_term ctxt t =
let
val compound_rhs = get_compound_rhs ctxt
val is_rhs = not o null o Net.unify_term compound_rhs
fun dummy ctxt =
let
val (c, ctxt) = yield_singleton Variable.variant_fixes "a" ctxt
in
(Free (c, dummyT), ctxt)
end
(* create a lambda term of the same shape as the given term *)
fun skeleton (Bound i) ctxt = (Bound i, ctxt)
| skeleton (Abs (x, _, t)) ctxt =
let
val (t', ctxt) = skeleton t ctxt
in
(Abs (x, dummyT, t'), ctxt)
end
| skeleton (tu as (t $ u)) ctxt =
if is_rhs tu andalso not (Term.is_open tu) then dummy ctxt else
let
val (t', ctxt) = skeleton t ctxt
val (u', ctxt) = skeleton u ctxt
in
(t' $ u', ctxt)
end
| skeleton _ ctxt = dummy ctxt
val s = skeleton t ctxt |> fst |> Syntax.check_term ctxt |>
map_types (map_type_tfree (fn (a, _) => TFree (a, HOLogic.typeS)))
val frees = map fst (Term.add_frees s [])
val tfrees = map fst (Term.add_tfrees s [])
fun prep a = "R" ^ Library.unprefix "'" a
val (rnames, ctxt') = Variable.variant_fixes (map prep tfrees) ctxt
val thm = transfer_rule_of_terms ctxt' (tfrees ~~ rnames) s t
in
Thm.generalize (tfrees, rnames @ frees) (Thm.maxidx_of thm + 1) thm
end
fun eq_tac eq_rules = TRY o REPEAT_ALL_NEW (resolve_tac eq_rules) THEN_ALL_NEW rtac @{thm is_equality_eq}
fun transfer_tac equiv ctxt i =
let
val pre_simps = @{thms transfer_forall_eq transfer_implies_eq}
val start_rule =
if equiv then @{thm transfer_start} else @{thm transfer_start'}
val rules = get_transfer_raw ctxt
val eq_rules = get_relator_eq_raw ctxt
(* allow unsolved subgoals only for standard transfer method, not for transfer' *)
val end_tac = if equiv then K all_tac else K no_tac
val err_msg = "Transfer failed to convert goal to an object-logic formula"
fun main_tac (t, i) =
rtac start_rule i THEN
(rtac (transfer_rule_of_term ctxt (HOLogic.dest_Trueprop t))
THEN_ALL_NEW
(SOLVED' (REPEAT_ALL_NEW (resolve_tac rules) THEN_ALL_NEW (DETERM o eq_tac eq_rules))
ORELSE' end_tac)) (i + 1)
handle TERM (_, ts) => raise TERM (err_msg, ts)
in
EVERY
[rewrite_goal_tac pre_simps i THEN
SUBGOAL main_tac i,
(* FIXME: rewrite_goal_tac does unwanted eta-contraction *)
rewrite_goal_tac post_simps i,
rtac @{thm _} i]
end
fun transfer_prover_tac ctxt = SUBGOAL (fn (t, i) =>
let
val rhs = (snd o Term.dest_comb o HOLogic.dest_Trueprop) t
val rule1 = transfer_rule_of_term ctxt rhs
val rules = get_transfer_raw ctxt
val eq_rules = get_relator_eq_raw ctxt
in
EVERY
[CONVERSION prep_conv i,
rtac @{thm transfer_prover_start} i,
(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)
(** Methods and attributes **)
val free = Args.context -- Args.term >> (fn (_, Free v) => v | (ctxt, t) =>
error ("Bad free variable: " ^ Syntax.string_of_term ctxt t))
val fixing = Scan.optional (Scan.lift (Args.$$$ "fixing" -- Args.colon)
|-- Scan.repeat free) []
fun transfer_method equiv : (Proof.context -> Method.method) context_parser =
fixing >> (fn vs => fn ctxt =>
SIMPLE_METHOD' (gen_frees_tac vs ctxt THEN' transfer_tac equiv ctxt))
val transfer_prover_method : (Proof.context -> Method.method) context_parser =
Scan.succeed (fn ctxt => SIMPLE_METHOD' (transfer_prover_tac ctxt))
(* Attribute for transfer rules *)
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)
val transfer_del =
Thm.declaration_attribute (del_transfer_thm o prep_rule)
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 =
let
val name = @{binding relator_eq}
fun add_thm thm = Data.map (map_relator_eq (Item_Net.update thm))
#> Data.map (map_relator_eq_raw (Item_Net.update (abstract_equalities_relator_eq thm)))
fun del_thm thm = Data.map (map_relator_eq (Item_Net.remove thm))
#> Data.map (map_relator_eq_raw (Item_Net.remove (abstract_equalities_relator_eq thm)))
val add = Thm.declaration_attribute add_thm
val del = Thm.declaration_attribute del_thm
val text = "declaration of relator equality rule (used by transfer method)"
val content = Item_Net.content o #relator_eq o Data.get
in
Attrib.setup name (Attrib.add_del add del) text
#> 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)
"generic theorem transfer method"
#> Method.setup @{binding transfer'} (transfer_method false)
"generic theorem transfer method"
#> Method.setup @{binding transfer_prover} transfer_prover_method
"for proving transfer rules"
end