author haftmann Wed, 10 Mar 2010 08:04:50 +0100 changeset 35686 abf91fba0a70 parent 35682 5e6811f4294b (current diff) parent 35685 2fa645db6e58 (diff) child 35687 564a49e8be44 child 35695 80b2c22f8f00 child 35719 99b6152aedf5
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 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```