src/HOL/Tools/transfer.ML

--- 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;