merged

--- a/src/HOL/Nat_Transfer.thy	Tue Mar 09 23:32:49 2010 +0100
+++ b/src/HOL/Nat_Transfer.thy	Wed Mar 10 08:04:50 2010 +0100
@@ -27,17 +27,17 @@
 text {* set up transfer direction *}
 
 lemma transfer_morphism_nat_int: "transfer_morphism nat (op <= (0::int))"
-  by (simp add: transfer_morphism_def)
+  by (fact transfer_morphismI)
 
-declare transfer_morphism_nat_int [transfer
-  add mode: manual
+declare transfer_morphism_nat_int [transfer add
+  mode: manual
   return: nat_0_le
-  labels: natint
+  labels: nat_int
 ]
 
 text {* basic functions and relations *}
 
-lemma transfer_nat_int_numerals:
+lemma transfer_nat_int_numerals [transfer key: transfer_morphism_nat_int]:
     "(0::nat) = nat 0"
     "(1::nat) = nat 1"
     "(2::nat) = nat 2"
@@ -52,8 +52,7 @@
 lemma tsub_eq: "x >= y \<Longrightarrow> tsub x y = x - y"
   by (simp add: tsub_def)
 
-
-lemma transfer_nat_int_functions:
+lemma transfer_nat_int_functions [transfer key: transfer_morphism_nat_int]:
     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) + (nat y) = nat (x + y)"
     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) * (nat y) = nat (x * y)"
     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) - (nat y) = nat (tsub x y)"
@@ -61,7 +60,7 @@
   by (auto simp add: eq_nat_nat_iff nat_mult_distrib
       nat_power_eq tsub_def)
 
-lemma transfer_nat_int_function_closures:
+lemma transfer_nat_int_function_closures [transfer key: transfer_morphism_nat_int]:
     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x + y >= 0"
     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x * y >= 0"
     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> tsub x y >= 0"
@@ -73,7 +72,7 @@
     "int z >= 0"
   by (auto simp add: zero_le_mult_iff tsub_def)
 
-lemma transfer_nat_int_relations:
+lemma transfer_nat_int_relations [transfer key: transfer_morphism_nat_int]:
     "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>
       (nat (x::int) = nat y) = (x = y)"
     "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>
@@ -84,13 +83,6 @@
       (nat (x::int) dvd nat y) = (x dvd y)"
   by (auto simp add: zdvd_int)
 
-declare transfer_morphism_nat_int [transfer add return:
-  transfer_nat_int_numerals
-  transfer_nat_int_functions
-  transfer_nat_int_function_closures
-  transfer_nat_int_relations
-]
-
 
 text {* first-order quantifiers *}
 
@@ -108,7 +100,7 @@
   then show "\<exists>x. P x" by auto
 qed
 
-lemma transfer_nat_int_quantifiers:
+lemma transfer_nat_int_quantifiers [transfer key: transfer_morphism_nat_int]:
     "(ALL (x::nat). P x) = (ALL (x::int). x >= 0 \<longrightarrow> P (nat x))"
     "(EX (x::nat). P x) = (EX (x::int). x >= 0 & P (nat x))"
   by (rule all_nat, rule ex_nat)
@@ -123,18 +115,15 @@
   by auto
 
 declare transfer_morphism_nat_int [transfer add
-  return: transfer_nat_int_quantifiers
   cong: all_cong ex_cong]
 
 
 text {* if *}
 
-lemma nat_if_cong: "(if P then (nat x) else (nat y)) =
-    nat (if P then x else y)"
+lemma nat_if_cong [transfer key: transfer_morphism_nat_int]:
+  "(if P then (nat x) else (nat y)) = nat (if P then x else y)"
   by auto
 
-declare transfer_morphism_nat_int [transfer add return: nat_if_cong]
-
 
 text {* operations with sets *}
 
@@ -276,22 +265,18 @@
 
 text {* set up transfer direction *}
 
-lemma transfer_morphism_int_nat: "transfer_morphism int (UNIV :: nat set)"
-  by (simp add: transfer_morphism_def)
+lemma transfer_morphism_int_nat: "transfer_morphism int (\<lambda>n. True)"
+  by (fact transfer_morphismI)
 
 declare transfer_morphism_int_nat [transfer add
   mode: manual
-(*  labels: int-nat *)
   return: nat_int
+  labels: int_nat
 ]
 
 
 text {* basic functions and relations *}
 
-lemma UNIV_apply:
-  "UNIV x = True"
-  by (simp add: top_fun_eq top_bool_eq)
-
 definition
   is_nat :: "int \<Rightarrow> bool"
 where
@@ -335,7 +320,6 @@
   transfer_int_nat_functions
   transfer_int_nat_function_closures
   transfer_int_nat_relations
-  UNIV_apply
 ]
 
 

--- a/src/HOL/Tools/transfer.ML	Tue Mar 09 23:32:49 2010 +0100
+++ b/src/HOL/Tools/transfer.ML	Wed Mar 10 08:04:50 2010 +0100
@@ -100,34 +100,42 @@
 
 (* applying transfer data *)
 
-fun transfer_thm inj_only ((a0, D0), (inj, embed, return, cong)) leave ctxt0 th =
+fun transfer_thm ((raw_a, raw_D), (inj, embed, return, cong)) leave ctxt1 thm =
   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 simpset = Simplifier.context ctxt''' HOL_ss
-      addsimps inj addsimps (if inj_only then [] else embed @ return) addcongs cong;
-    val th3 = Simplifier.asm_full_simplify simpset
-      (fold_rev implies_intr (map cprop_of hs) th2);
-  in hd (Variable.export ctxt''' ctxt0 [th3]) end;
+    (* identify morphism function *)
+    val ([a, D], ctxt2) = ctxt1
+      |> Variable.import true (map Drule.mk_term [raw_a, raw_D])
+      |>> map Drule.dest_term o snd;
+    val transform = Thm.capply @{cterm "Trueprop"} o Thm.capply D;
+    val T = Thm.typ_of (Thm.ctyp_of_term a);
+    val (aT, bT) = (Term.range_type T, Term.domain_type T);
+    
+    (* determine variables to transfer *)
+    val ctxt3 = ctxt2
+      |> Variable.declare_thm thm
+      |> Variable.declare_term (term_of a)
+      |> Variable.declare_term (term_of D);
+    val certify = Thm.cterm_of (ProofContext.theory_of ctxt3);
+    val vars = filter (fn ((v, _), T) => Type.could_unify (T, aT) andalso
+      not (member (op =) leave v)) (Term.add_vars (Thm.prop_of thm) []);
+    val c_vars = map (certify o Var) vars;
+    val (vs', ctxt4) = Variable.variant_fixes (map (fst o fst) vars) ctxt3;
+    val c_vars' = map (certify o (fn v => Free (v, bT))) vs';
+    val c_exprs' = map (Thm.capply a) c_vars';
 
-fun transfer_thm_multiple inj_only insts leave ctxt thm =
-  map (fn inst => transfer_thm false inst leave ctxt thm) insts;
+    (* transfer *)
+    val (hyps, ctxt5) = ctxt4
+      |> Assumption.add_assumes (map transform c_vars');
+    val simpset = Simplifier.context ctxt5 HOL_ss
+      addsimps (inj @ embed @ return) addcongs cong;
+    val thm' = thm
+      |> Drule.cterm_instantiate (c_vars ~~ c_exprs')
+      |> fold_rev Thm.implies_intr (map cprop_of hyps)
+      |> Simplifier.asm_full_simplify simpset
+  in singleton (Variable.export ctxt5 ctxt1) thm' end;
+
+fun transfer_thm_multiple insts leave ctxt thm =
+  map (fn inst => transfer_thm inst leave ctxt thm) insts;
 
 datatype selection = Direction of term * term | Hints of string list | Prop;
 
@@ -136,7 +144,7 @@
   | insts_for context thm Prop = get_by_prop context (Thm.prop_of thm);
 
 fun transfer context selection leave thm =
-  transfer_thm_multiple false (insts_for context thm selection) leave (Context.proof_of context) thm;
+  transfer_thm_multiple (insts_for context thm selection) leave (Context.proof_of context) thm;
 
 
 (* maintaining transfer data *)
@@ -147,7 +155,7 @@
   let
     fun add_del eq del add = union eq add #> subtract eq del;
     val guessed = if guess
-      then map (fn thm => transfer_thm true
+      then map (fn thm => transfer_thm
         ((a, D), (if null inj1 then inj2 else inj1, [], [], cong1)) [] ctxt thm RS sym) embed1
       else [];
   in
@@ -190,6 +198,7 @@
 
 val addN = "add";
 val delN = "del";
+val keyN = "key";
 val modeN = "mode";
 val automaticN = "automatic";
 val manualN = "manual";
@@ -202,8 +211,8 @@
 val leavingN = "leaving";
 val directionN = "direction";
 
-val any_keyword = keyword_colon addN || keyword_colon delN || keyword_colon modeN
-  || keyword_colon injN || keyword_colon embedN || keyword_colon returnN
+val any_keyword = keyword_colon addN || keyword_colon delN || keyword_colon keyN
+  || keyword_colon modeN || keyword_colon injN || keyword_colon embedN || keyword_colon returnN
   || keyword_colon congN || keyword_colon labelsN
   || keyword_colon leavingN || keyword_colon directionN;
 
@@ -222,18 +231,22 @@
   -- these_pair return -- these_pair cong -- these_pair labels
   >> (fn (((((inja, injd), (embeda, embedd)), (returna, returnd)), (conga, congd)),
        (hintsa, hintsd)) =>
-      ({inj = inja, embed = embeda, return = returna, cong = conga, hints = hintsa},
-        {inj = injd, embed = embedd, return = returnd, cong = congd, hints = hintsd}));
+      ({ inj = inja, embed = embeda, return = returna, cong = conga, hints = hintsa },
+        { inj = injd, embed = embedd, return = returnd, cong = congd, hints = hintsd }));
 
 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_attribute = Scan.lift (Args.$$$ delN >> K (Thm.declaration_attribute drop))
-  || Scan.unless any_keyword (keyword addN) |-- Scan.optional mode true -- entry_pair
+val transfer_attribute = keyword delN >> K (Thm.declaration_attribute drop)
+  || keyword addN |-- Scan.optional mode true -- entry_pair
     >> (fn (guess, (entry_add, entry_del)) => Thm.declaration_attribute
-      (fn thm => add thm guess entry_add #> del thm entry_del));
+      (fn thm => add thm guess entry_add #> del thm entry_del))
+  || keyword_colon keyN |-- Attrib.thm
+    >> (fn key => Thm.declaration_attribute
+      (fn thm => add key false
+        { inj = [], embed = [], return = [thm], cong = [], hints = [] }));
 
 val transferred_attribute = selection -- these (keyword_colon leavingN |-- names)
   >> (fn (selection, leave) => Thm.rule_attribute (fn context =>

--- a/src/HOL/ex/Transfer_Ex.thy	Tue Mar 09 23:32:49 2010 +0100
+++ b/src/HOL/ex/Transfer_Ex.thy	Wed Mar 10 08:04:50 2010 +0100
@@ -2,41 +2,46 @@
 header {* Various examples for transfer procedure *}
 
 theory Transfer_Ex
-imports Complex_Main
+imports Main
 begin
 
-(* nat to int *)
-
 lemma ex1: "(x::nat) + y = y + x"
   by auto
 
-thm ex1 [transferred]
+lemma "(0\<Colon>int) \<le> (y\<Colon>int) \<Longrightarrow> (0\<Colon>int) \<le> (x\<Colon>int) \<Longrightarrow> x + y = y + x"
+  by (fact ex1 [transferred])
 
 lemma ex2: "(a::nat) div b * b + a mod b = a"
   by (rule mod_div_equality)
 
-thm ex2 [transferred]
+lemma "(0\<Colon>int) \<le> (b\<Colon>int) \<Longrightarrow> (0\<Colon>int) \<le> (a\<Colon>int) \<Longrightarrow> a div b * b + a mod b = a"
+  by (fact ex2 [transferred])
 
 lemma ex3: "ALL (x::nat). ALL y. EX z. z >= x + y"
   by auto
 
-thm ex3 [transferred natint]
+lemma "\<forall>x\<ge>0\<Colon>int. \<forall>y\<ge>0\<Colon>int. \<exists>xa\<ge>0\<Colon>int. x + y \<le> xa"
+  by (fact ex3 [transferred nat_int])
 
 lemma ex4: "(x::nat) >= y \<Longrightarrow> (x - y) + y = x"
   by auto
 
-thm ex4 [transferred]
+lemma "(0\<Colon>int) \<le> (x\<Colon>int) \<Longrightarrow> (0\<Colon>int) \<le> (y\<Colon>int) \<Longrightarrow> y \<le> x \<Longrightarrow> tsub x y + y = x"
+  by (fact ex4 [transferred])
 
-lemma ex5: "(2::nat) * (SUM i <= n. i) = n * (n + 1)"
+lemma ex5: "(2::nat) * \<Sum>{..n} = n * (n + 1)"
   by (induct n rule: nat_induct, auto)
 
-thm ex5 [transferred]
+lemma "(0\<Colon>int) \<le> (n\<Colon>int) \<Longrightarrow> (2\<Colon>int) * \<Sum>{0\<Colon>int..n} = n * (n + (1\<Colon>int))"
+  by (fact ex5 [transferred])
+
+lemma "(0\<Colon>nat) \<le> (n\<Colon>nat) \<Longrightarrow> (2\<Colon>nat) * \<Sum>{0\<Colon>nat..n} = n * (n + (1\<Colon>nat))"
+  by (fact ex5 [transferred, transferred])
 
 theorem ex6: "0 <= (n::int) \<Longrightarrow> 2 * \<Sum>{0..n} = n * (n + 1)"
   by (rule ex5 [transferred])
 
-thm ex6 [transferred]
-
-thm ex5 [transferred, transferred]
+lemma "(0\<Colon>nat) \<le> (n\<Colon>nat) \<Longrightarrow> (2\<Colon>nat) * \<Sum>{0\<Colon>nat..n} = n * (n + (1\<Colon>nat))"
+  by (fact ex6 [transferred])
 
 end
\ No newline at end of file