# HG changeset patch # User haftmann # Date 1268055716 -3600 # Node ID 4b01ddafc8a954b7446f83adaf7e313620905a06 # Parent 8f4b2e8543e77b2e27294fc871e73f2f1bc2dfb2 proper ML interface; further polishing diff -r 8f4b2e8543e7 -r 4b01ddafc8a9 src/HOL/Tools/transfer.ML --- a/src/HOL/Tools/transfer.ML Mon Mar 08 13:22:41 2010 +0100 +++ b/src/HOL/Tools/transfer.ML Mon Mar 08 14:41:56 2010 +0100 @@ -1,11 +1,16 @@ -(* Author: Amine Chaieb, University of Cambridge, 2009 - Author: Jeremy Avigad, Carnegie Mellon University +(* Author: Amine Chaieb, University of Cambridge, 2009 + Jeremy Avigad, Carnegie Mellon University + Florian Haftmann, TU Muenchen + +Simple transfer principle on theorems. *) signature TRANSFER = sig + datatype selection = Direction of term * term | Hints of string list | Prop + val transfer: Context.generic -> selection -> string list -> thm -> thm type entry - val get: Proof.context -> (thm * entry) list + val add: entry * entry -> thm -> Context.generic -> Context.generic val del: thm -> Context.generic -> Context.generic val setup: theory -> theory end; @@ -90,9 +95,7 @@ (* applying transfer data *) -val get = Data.get o Context.Proof; - -fun transfer_thm inj_only a0 D0 {inj = inj, emb = emb, ret = ret, cong = cg, guess = g, hints = hints} +fun transfer_thm inj_only a0 D0 {inj = inj, emb = emb, ret = ret, cong = cg, guess = _, hints = _} leave ctxt0 th = let val ([a, D], ctxt) = apfst (map Drule.dest_term o snd) @@ -108,7 +111,7 @@ val certify = Thm.cterm_of (ProofContext.theory_of ctxt''); val cns = map (certify o Var) ns; val cfis = map (certify o (fn n => Free (n, bT))) ins; - val cis = map (Thm.capply a) cfis + val cis = map (Thm.capply a) cfis; val (hs, ctxt''') = Assumption.add_assumes (map (fn ct => Thm.capply @{cterm "Trueprop"} (Thm.capply D ct)) cfis) ctxt''; val th1 = Drule.cterm_instantiate (cns ~~ cis) th; @@ -123,22 +126,14 @@ Conjunction.intr_balanced (map (fn ((a, D), e) => transfer_thm false a D e leave ctxt thm) insts); -fun transfer_by_direction (a, D) leave (context, thm) = - let - val ((a0, D0), e) = get_by_direction context (a, D); - in (context, transfer_thm false a0 D0 e leave (Context.proof_of context) thm) end; +datatype selection = Direction of term * term | Hints of string list | Prop; -fun transfer_by_hints hints leave (context, thm) = - (context, transfer_thm_multiple false (get_by_hints context hints) - leave (Context.proof_of context) thm); +fun insts_for context thm (Direction direction) = [get_by_direction context direction] + | insts_for context thm (Hints hints) = get_by_hints context hints + | insts_for context thm Prop = get_by_prop context (Thm.prop_of thm); -fun transfer_by_prop leave (context, thm) = - (context, transfer_thm_multiple false (get_by_prop context (Thm.prop_of thm)) - leave (Context.proof_of context) thm); - -fun transferred_attribute [] NONE leave = transfer_by_prop leave - | transferred_attribute hints NONE leave = transfer_by_hints hints leave - | transferred_attribute _ (SOME (a, D)) leave = transfer_by_direction (a, D) leave; +fun transfer context selection leave thm = + transfer_thm_multiple false (insts_for context thm selection) leave (Context.proof_of context) thm; (* maintaining transfer data *) @@ -160,13 +155,13 @@ hints = subtract (op =) hints0 (union (op =) hints1 hints2) } end; -fun add ((inja, injd), (emba, embd), (reta, retd), (cga, cgd), g, (hintsa, hintsd)) key = - Data.map (fn al => +fun add (e0 as {inj = inja, emb = emba, ret = reta, cong = cga, guess = g, hints = hintsa}, + ed as {inj = injd, emb = embd, ret = retd, cong = cgd, guess = _, hints = hintsd}) key context = + context + |> Data.map (fn al => let - val ctxt0 = ProofContext.init (Thm.theory_of_thm key); (*FIXME*) - val (a0, D0) = check_morphism_key ctxt0 key; - val e0 = {inj = inja, emb = emba, ret = reta, cong = cga, guess = g, hints = hintsa}; - val ed = {inj = injd, emb = embd, ret = retd, cong = cgd, guess = g, hints = hintsd}; + val ctxt = Context.proof_of context; + val (a0, D0) = check_morphism_key ctxt key; val entry = if g then let val inj' = if null inja then #inj @@ -175,17 +170,13 @@ else inja val ret' = merge Thm.eq_thm (reta, map (fn th => transfer_thm true a0 D0 {inj = inj', emb = [], ret = [], cong = cga, guess = g, - hints = hintsa} [] ctxt0 th RS sym) emba); + hints = hintsa} [] ctxt th RS sym) emba); in {inj = inja, emb = emba, ret = ret', cong = cga, guess = g, hints = hintsa} end else e0; in merge_update Thm.eq_thm (merge_entries ed) (key, entry) al end); -fun add_attribute args = Thm.declaration_attribute (add args); - fun del key = Data.map (remove (eq_fst Thm.eq_thm) (key, [])); -val del_attribute = Thm.declaration_attribute del; - (* syntax *) @@ -225,20 +216,23 @@ val cong = (keyword_colon congN |-- thms) -- these (keyword_colon delN |-- thms); val labels = (keyword_colon labelsN |-- names) -- these (keyword_colon delN |-- names); -val entry = Scan.optional mode true -- these_pair inj -- these_pair embed - -- these_pair return -- these_pair cong -- these_pair labels; +val entry_pair = Scan.optional mode true -- these_pair inj -- these_pair embed + -- these_pair return -- these_pair cong -- these_pair labels + >> (fn (((((g, (inja, injd)), (emba, embd)), (reta, retd)), (cga, cgd)), (hintsa, hintsd)) => + ({inj = inja, emb = emba, ret = reta, cong = cga, guess = g, hints = hintsa}, + {inj = injd, emb = embd, ret = retd, cong = cgd, guess = g, hints = hintsd})); -val transfer_directive = these names -- Scan.option (keyword_colon directionN - |-- (Args.term -- Args.term)) -- these (keyword_colon leavingN |-- names); +val selection = (keyword_colon directionN |-- (Args.term -- Args.term) >> Direction) + || these names >> (fn hints => if null hints then Prop else Hints hints); in -val transfer_syntax = (Scan.lift (Args.$$$ delN >> K del_attribute) - || Scan.unless any_keyword (keyword addN) |-- entry - >> (fn (((((g, inj), embed), ret), cg), hints) => add_attribute (inj, embed, ret, cg, g, hints))) +val transfer_attribute = Scan.lift (Args.$$$ delN >> K (Thm.declaration_attribute del)) + || Scan.unless any_keyword (keyword addN) |-- entry_pair + >> (fn entry_pair => Thm.declaration_attribute (add entry_pair)) -val transferred_syntax = transfer_directive - >> (fn ((hints, direction), leave) => transferred_attribute hints direction leave); +val transferred_attribute = selection -- these (keyword_colon leavingN |-- names) + >> (fn (selection, leave) => Thm.rule_attribute (fn context => transfer context selection leave)); end; @@ -246,9 +240,9 @@ (* theory setup *) val setup = - Attrib.setup @{binding transfer} transfer_syntax + Attrib.setup @{binding transfer} transfer_attribute "Installs transfer data" #> - Attrib.setup @{binding transferred} transferred_syntax + Attrib.setup @{binding transferred} transferred_attribute "Transfers theorems"; end;