--- a/src/HOL/Tools/transfer.ML Mon Mar 08 09:38:58 2010 +0100
+++ b/src/HOL/Tools/transfer.ML Mon Mar 08 09:38:59 2010 +0100
@@ -15,7 +15,12 @@
(* data administration *)
-val transM_pat = (Thm.dest_arg1 o Thm.dest_arg o cprop_of) @{thm TransferMorphism_def};
+fun check_morphism_key ctxt key =
+ let
+ val _ = (Thm.match o pairself Thm.cprop_of) (@{thm transfer_morphismI}, key)
+ handle Pattern.MATCH => error
+ ("Expected theorem of the form " ^ quote (Display.string_of_thm ctxt @{thm transfer_morphismI}));
+ in (Thm.dest_binop o Thm.dest_arg o Thm.cprop_of) key end;
type entry = { inj : thm list, emb : thm list, ret : thm list, cong : thm list,
guess : bool, hints : string list };
@@ -36,7 +41,7 @@
val get = Data.get o Context.Proof;
-fun del key = Data.map (remove (eq_fst Thm.eq_thm) (key, []))
+fun del key = Data.map (remove (eq_fst Thm.eq_thm) (key, []));
val del_attribute = Thm.declaration_attribute del;
@@ -47,41 +52,41 @@
HOL_ss addsimps inj addsimps (if inj_only then [] else emb @ ret) addcongs cg;
fun basic_transfer_rule inj_only a0 D0 e leave ctxt0 th =
- let
- val ([a,D], ctxt) = apfst (map Drule.dest_term o snd)
- (Variable.import true (map Drule.mk_term [a0, D0]) ctxt0);
- val (aT,bT) =
- let val T = typ_of (ctyp_of_term a)
- in (Term.range_type T, Term.domain_type T)
- end;
- val ctxt' = (Variable.declare_term (term_of a) o Variable.declare_term (term_of D)
- o Variable.declare_thm th) ctxt;
- val ns = filter (fn i => Type.could_unify (snd i, aT) andalso
- not (fst (fst i) mem_string leave)) (Term.add_vars (prop_of th) []);
- val (ins, ctxt'') = Variable.variant_fixes (map (fst o fst) ns) ctxt';
- val cns = map ((cterm_of o ProofContext.theory_of) ctxt'' o Var) ns;
- val cfis = map ((cterm_of o ProofContext.theory_of) ctxt'' o
- (fn n => Free (n, bT))) ins;
- 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;
- val th2 = fold Thm.elim_implies hs (fold_rev implies_intr (map cprop_of hs) th1);
- val th3 = Simplifier.asm_full_simplify (Simplifier.context ctxt'''
- (build_simpset inj_only e)) (fold_rev implies_intr (map cprop_of hs) th2);
-in hd (Variable.export ctxt''' ctxt0 [th3]) end;
+ let
+ val ([a, D], ctxt) = apfst (map Drule.dest_term o snd)
+ (Variable.import true (map Drule.mk_term [a0, D0]) ctxt0);
+ val (aT, bT) =
+ let val T = typ_of (ctyp_of_term a)
+ in (Term.range_type T, Term.domain_type T) end;
+ val ctxt' = (Variable.declare_term (term_of a) o Variable.declare_term (term_of D)
+ o Variable.declare_thm th) ctxt;
+ val ns = filter (fn i => Type.could_unify (snd i, aT) andalso
+ not (member (op =) leave (fst (fst i)))) (Term.add_vars (prop_of th) []);
+ val (ins, ctxt'') = Variable.variant_fixes (map (fst o fst) ns) ctxt';
+ 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 (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;
+ val th2 = fold Thm.elim_implies hs (fold_rev implies_intr (map cprop_of hs) th1);
+ val th3 = Simplifier.asm_full_simplify (Simplifier.context ctxt'''
+ (build_simpset inj_only e)) (fold_rev implies_intr (map cprop_of hs) th2);
+ in hd (Variable.export ctxt''' ctxt0 [th3]) end;
fun transfer_rule (a, D) leave (gctxt, th) =
let
fun transfer_ruleh a D leave ctxt th =
let
- val al = get ctxt
- val a0 = cterm_of (ProofContext.theory_of ctxt) a
- val D0 = cterm_of (ProofContext.theory_of ctxt) D
+ val al = get ctxt;
+ val certify = Thm.cterm_of (ProofContext.theory_of ctxt);
+ val a0 = certify a;
+ val D0 = certify D;
fun h (th', e) =
let
val (a',D') = (Thm.dest_binop o Thm.dest_arg o cprop_of) th'
- in if a0 aconvc a' andalso D0 aconvc D' then SOME e else NONE end
+ in if a0 aconvc a' andalso D0 aconvc D' then SOME e else NONE end;
in case get_first h al of
SOME e => basic_transfer_rule false a0 D0 e leave ctxt th
| NONE => error "Transfer: corresponding instance not found in context data"
@@ -93,9 +98,9 @@
fun splits P [] = []
| splits P (xxs as (x :: xs)) =
let
- val pss = filter (P x) xxs
- val qss = filter_out (P x) xxs
- in if null pss then [qss] else if null qss then [pss] else pss:: splits P qss end
+ val pss = filter (P x) xxs;
+ val qss = filter_out (P x) xxs;
+ in if null pss then [qss] else if null qss then [pss] else pss:: splits P qss end;
fun all_transfers leave (gctxt, th) =
let
@@ -132,7 +137,7 @@
fun transferred_attribute ls NONE leave =
if null ls then all_transfers leave else transfer_rule_by_hint ls leave
- | transferred_attribute _ (SOME (a, D)) leave = transfer_rule (a, D) leave
+ | transferred_attribute _ (SOME (a, D)) leave = transfer_rule (a, D) leave;
(* adding transfer data *)
@@ -144,8 +149,8 @@
(*? fun merge_update eq m (k, v) = AList.map_entry eq k (fn v' => m (v, v'));*)
fun merge_entries {inj = inj0, emb = emb0, ret = ret0, cong = cg0, guess = g0, hints = hints0}
- ({inj = inj1, emb = emb1, ret = ret1, cong = cg1, guess = g1, hints = hints1},
- {inj = inj2, emb = emb2, ret = ret2, cong = cg2, guess = g2, hints = hints2} : entry) =
+ ({inj = inj1, emb = emb1, ret = ret1, cong = cg1, guess = g1, hints = hints1},
+ {inj = inj2, emb = emb2, ret = ret2, cong = cg2, guess = g2, hints = hints2} : entry) =
let
fun h xs0 xs ys = subtract Thm.eq_thm xs0 (merge Thm.eq_thm (xs, ys))
in
@@ -157,26 +162,22 @@
fun add ((inja, injd), (emba, embd), (reta, retd), (cga, cgd), g, (hintsa, hintsd)) key =
Data.map (fn al =>
let
- val _ = Thm.match (transM_pat, Thm.dest_arg (Thm.cprop_of key))
- handle Pattern.MATCH =>
- error "Attribute expected Theorem of the form : TransferMorphism A a B b"
- 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 entry =
- if g then
- let val (a0,D0) = (Thm.dest_binop o Thm.dest_arg o cprop_of) key
- val ctxt0 = ProofContext.init (Thm.theory_of_thm key)
- val inj' =
- if null inja then
- #inj
- (case AList.lookup Thm.eq_thm al key of SOME e => e
- | NONE => error "Transfer: can not generate return rules on the fly, either add injectivity axiom or force manual mode with mode: manual")
- else inja
- val ret' = merge Thm.eq_thm (reta, map (fn th => basic_transfer_rule true a0 D0 {inj = inj', emb = [], ret = [], cong = cga, guess = g, hints = hintsa} [] ctxt0 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);
+ 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 entry = if g then
+ let
+ val inj' = if null inja then #inj
+ (case AList.lookup Thm.eq_thm al key of SOME e => e
+ | NONE => error "Transfer: cannot generate return rules on the fly, either add injectivity axiom or force manual mode with mode: manual")
+ else inja
+ val ret' = merge Thm.eq_thm (reta, map
+ (fn th => basic_transfer_rule true a0 D0 {inj = inj', emb = [], ret = [], cong = cga, guess = g,
+ hints = hintsa} [] ctxt0 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);
@@ -185,51 +186,54 @@
local
-fun keyword k = Scan.lift (Args.$$$ k) >> K ()
-fun keywordC k = Scan.lift (Args.$$$ k -- Args.colon) >> K ()
+fun these scan = Scan.optional scan [];
+fun these_pair scan = Scan.optional scan ([], []);
+
+fun keyword k = Scan.lift (Args.$$$ k) >> K ();
+fun keyword_colon k = Scan.lift (Args.$$$ k -- Args.colon) >> K ();
-val congN = "cong"
-val injN = "inj"
-val embedN = "embed"
-val returnN = "return"
-val addN = "add"
-val delN = "del"
-val modeN = "mode"
-val automaticN = "automatic"
-val manualN = "manual"
-val directionN = "direction"
-val labelsN = "labels"
-val leavingN = "leaving"
-
-val any_keyword = keywordC congN || keywordC injN || keywordC embedN || keywordC returnN || keywordC directionN || keywordC modeN || keywordC delN || keywordC labelsN || keywordC leavingN
+val congN = "cong";
+val injN = "inj";
+val embedN = "embed";
+val returnN = "return";
+val addN = "add";
+val delN = "del";
+val modeN = "mode";
+val automaticN = "automatic";
+val manualN = "manual";
+val directionN = "direction";
+val labelsN = "labels";
+val leavingN = "leaving";
-val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat
-val terms = thms >> map Drule.dest_term
-val types = thms >> (Logic.dest_type o HOLogic.dest_Trueprop o prop_of o hd)
-val name = Scan.lift Args.name
-val names = Scan.repeat (Scan.unless any_keyword name)
-fun optional scan = Scan.optional scan []
-fun optional2 scan = Scan.optional scan ([],[])
+val any_keyword = keyword_colon congN || keyword_colon injN || keyword_colon embedN
+ || keyword_colon returnN || keyword_colon directionN || keyword_colon modeN
+ || keyword_colon delN || keyword_colon labelsN || keyword_colon leavingN;
+
+val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
+val names = Scan.repeat (Scan.unless any_keyword (Scan.lift Args.name))
-val mode = keywordC modeN |-- ((Scan.lift (Args.$$$ manualN) >> K false) || (Scan.lift (Args.$$$ automaticN) >> K true))
-val inj = (keywordC injN |-- thms) -- optional (keywordC delN |-- thms)
-val embed = (keywordC embedN |-- thms) -- optional (keywordC delN |-- thms)
-val return = (keywordC returnN |-- thms) -- optional (keywordC delN |-- thms)
-val cong = (keywordC congN |-- thms) -- optional (keywordC delN |-- thms)
-val addscan = Scan.unless any_keyword (keyword addN)
-val labels = (keywordC labelsN |-- names) -- optional (keywordC delN |-- names)
-val entry = Scan.optional mode true -- optional2 inj -- optional2 embed -- optional2 return -- optional2 cong -- optional2 labels
+val mode = keyword_colon modeN |-- ((Scan.lift (Args.$$$ manualN) >> K false)
+ || (Scan.lift (Args.$$$ automaticN) >> K true));
+val inj = (keyword_colon injN |-- thms) -- these (keyword_colon delN |-- thms);
+val embed = (keyword_colon embedN |-- thms) -- these (keyword_colon delN |-- thms);
+val return = (keyword_colon returnN |-- thms) -- these (keyword_colon delN |-- thms);
+val cong = (keyword_colon congN |-- thms) -- these (keyword_colon delN |-- thms);
+val labels = (keyword_colon labelsN |-- names) -- these (keyword_colon delN |-- names);
-val transf_add = addscan |-- entry
+val entry = Scan.optional mode true -- these_pair inj -- these_pair embed
+ -- these_pair return -- these_pair cong -- these_pair labels;
+
+val transfer_directive = these names -- Scan.option (keyword_colon directionN
+ |-- (Args.term -- Args.term)) -- these (keyword_colon leavingN |-- names);
+
in
-val install_att_syntax =
- (Scan.lift (Args.$$$ delN >> K del_attribute) ||
- transf_add
+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 transferred_att_syntax = (optional names -- Scan.option (keywordC directionN |-- (Args.term -- Args.term))
- -- optional (keywordC leavingN |-- names) >> (fn ((hints, aD),leave) => transferred_attribute hints aD leave));
+val transferred_syntax = transfer_directive
+ >> (fn ((hints, aD), leave) => transferred_attribute hints aD leave);
end;
@@ -237,9 +241,9 @@
(* theory setup *)
val setup =
- Attrib.setup @{binding transfer} install_att_syntax
+ Attrib.setup @{binding transfer} transfer_syntax
"Installs transfer data" #>
- Attrib.setup @{binding transferred} transferred_att_syntax
+ Attrib.setup @{binding transferred} transferred_syntax
"Transfers theorems";
end;