--- a/NEWS Sat Apr 21 14:53:04 2012 +0200
+++ b/NEWS Sat Apr 21 15:26:05 2012 +0200
@@ -657,6 +657,86 @@
* Theory Library/Multiset: Improved code generation of multisets.
+* New Transfer package:
+
+ - transfer_rule attribute: Maintains a collection of transfer rules,
+ which relate constants at two different types. Transfer rules may
+ relate different type instances of the same polymorphic constant,
+ or they may relate an operation on a raw type to a corresponding
+ operation on an abstract type (quotient or subtype). For example:
+
+ ((A ===> B) ===> list_all2 A ===> list_all2 B) map map
+ (cr_int ===> cr_int ===> cr_int) (%(x,y) (u,v). (x+u, y+v)) plus_int
+
+ - transfer method: Replaces a subgoal on abstract types with an
+ equivalent subgoal on the corresponding raw types. Constants are
+ replaced with corresponding ones according to the transfer rules.
+ Goals are generalized over all free variables by default; this is
+ necessary for variables whose types changes, but can be overridden
+ for specific variables with e.g. 'transfer fixing: x y z'.
+
+ - relator_eq attribute: Collects identity laws for relators of
+ various type constructors, e.g. "list_all2 (op =) = (op =)". The
+ transfer method uses these lemmas to infer transfer rules for
+ non-polymorphic constants on the fly.
+
+ - transfer_prover method: Assists with proving a transfer rule for a
+ new constant, provided the constant is defined in terms of other
+ constants that already have transfer rules. It should be applied
+ after unfolding the constant definitions.
+
+ - HOL/ex/Transfer_Int_Nat.thy: Example theory demonstrating transfer
+ from type nat to type int.
+
+* New Lifting package:
+
+ - lift_definition command: Defines operations on an abstract type in
+ terms of a corresponding operation on a representation type. Example
+ syntax:
+
+ lift_definition dlist_insert :: "'a => 'a dlist => 'a dlist"
+ is List.insert
+
+ Users must discharge a respectfulness proof obligation when each
+ constant is defined. (For a type copy, i.e. a typedef with UNIV,
+ the proof is discharged automatically.) The obligation is
+ presented in a user-friendly, readable form; a respectfulness
+ theorem in the standard format and a transfer rule are generated
+ by the package.
+
+ - Integration with code_abstype: For typedefs (e.g. subtypes
+ corresponding to a datatype invariant, such as dlist),
+ lift_definition generates a code certificate theorem and sets up
+ code generation for each constant.
+
+ - setup_lifting command: Sets up the Lifting package to work with
+ a user-defined type. The user must provide either a quotient
+ theorem or a type_definition theorem. The package configures
+ transfer rules for equality and quantifiers on the type, and sets
+ up the lift_definition command to work with the type.
+
+ - Usage examples: See Quotient_Examples/Lift_DList.thy,
+ Quotient_Examples/Lift_RBT.thy, Word/Word.thy and
+ Library/Float.thy.
+
+* Quotient package:
+
+ - The 'quotient_type' command now supports a 'morphisms' option with
+ rep and abs functions, similar to typedef.
+
+ - 'quotient_type' sets up new types to work with the Lifting and
+ Transfer packages, as with 'setup_lifting'.
+
+ - The 'quotient_definition' command now requires the user to prove a
+ respectfulness property at the point where the constant is
+ defined, similar to lift_definition; INCOMPATIBILITY. Users are
+ encouraged to use lift_definition + transfer instead of
+ quotient_definition + descending, which will eventually be
+ deprecated.
+
+ - Renamed predicate 'Quotient' to 'Quotient3', and renamed theorems
+ accordingly, INCOMPATIBILITY.
+
* New diagnostic command 'find_unused_assms' to find potentially
superfluous assumptions in theorems using Quickcheck.
--- a/src/HOL/IsaMakefile Sat Apr 21 14:53:04 2012 +0200
+++ b/src/HOL/IsaMakefile Sat Apr 21 15:26:05 2012 +0200
@@ -1036,6 +1036,7 @@
ex/Simproc_Tests.thy ex/SVC_Oracle.thy \
ex/sledgehammer_tactics.ML ex/Seq.thy ex/Sqrt.thy ex/Sqrt_Script.thy \
ex/Sudoku.thy ex/Tarski.thy ex/Termination.thy ex/Transfer_Ex.thy \
+ ex/Transfer_Int_Nat.thy \
ex/Tree23.thy ex/Unification.thy ex/While_Combinator_Example.thy \
ex/document/root.bib ex/document/root.tex ex/svc_funcs.ML \
ex/svc_test.thy ../Tools/interpretation_with_defs.ML
--- a/src/HOL/ex/ROOT.ML Sat Apr 21 14:53:04 2012 +0200
+++ b/src/HOL/ex/ROOT.ML Sat Apr 21 15:26:05 2012 +0200
@@ -57,6 +57,7 @@
"Sqrt",
"Sqrt_Script",
"Transfer_Ex",
+ "Transfer_Int_Nat",
"HarmonicSeries",
"Refute_Examples",
"Landau",
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Transfer_Int_Nat.thy Sat Apr 21 15:26:05 2012 +0200
@@ -0,0 +1,180 @@
+(* Title: HOL/ex/Transfer_Int_Nat.thy
+ Author: Brian Huffman, TU Muenchen
+*)
+
+header {* Using the transfer method between nat and int *}
+
+theory Transfer_Int_Nat
+imports GCD "~~/src/HOL/Library/Quotient_List"
+begin
+
+subsection {* Correspondence relation *}
+
+definition ZN :: "int \<Rightarrow> nat \<Rightarrow> bool"
+ where "ZN = (\<lambda>z n. z = of_nat n)"
+
+subsection {* Transfer rules *}
+
+lemma bi_unique_ZN [transfer_rule]: "bi_unique ZN"
+ unfolding ZN_def bi_unique_def by simp
+
+lemma right_total_ZN [transfer_rule]: "right_total ZN"
+ unfolding ZN_def right_total_def by simp
+
+lemma ZN_0 [transfer_rule]: "ZN 0 0"
+ unfolding ZN_def by simp
+
+lemma ZN_1 [transfer_rule]: "ZN 1 1"
+ unfolding ZN_def by simp
+
+lemma ZN_add [transfer_rule]: "(ZN ===> ZN ===> ZN) (op +) (op +)"
+ unfolding fun_rel_def ZN_def by simp
+
+lemma ZN_mult [transfer_rule]: "(ZN ===> ZN ===> ZN) (op *) (op *)"
+ unfolding fun_rel_def ZN_def by (simp add: int_mult)
+
+lemma ZN_diff [transfer_rule]: "(ZN ===> ZN ===> ZN) tsub (op -)"
+ unfolding fun_rel_def ZN_def tsub_def by (simp add: zdiff_int)
+
+lemma ZN_power [transfer_rule]: "(ZN ===> op = ===> ZN) (op ^) (op ^)"
+ unfolding fun_rel_def ZN_def by (simp add: int_power)
+
+lemma ZN_nat_id [transfer_rule]: "(ZN ===> op =) nat id"
+ unfolding fun_rel_def ZN_def by simp
+
+lemma ZN_id_int [transfer_rule]: "(ZN ===> op =) id int"
+ unfolding fun_rel_def ZN_def by simp
+
+lemma ZN_All [transfer_rule]:
+ "((ZN ===> op =) ===> op =) (Ball {0..}) All"
+ unfolding fun_rel_def ZN_def by (auto dest: zero_le_imp_eq_int)
+
+lemma ZN_transfer_forall [transfer_rule]:
+ "((ZN ===> op =) ===> op =) (transfer_bforall (\<lambda>x. 0 \<le> x)) transfer_forall"
+ unfolding transfer_forall_def transfer_bforall_def
+ unfolding fun_rel_def ZN_def by (auto dest: zero_le_imp_eq_int)
+
+lemma ZN_Ex [transfer_rule]: "((ZN ===> op =) ===> op =) (Bex {0..}) Ex"
+ unfolding fun_rel_def ZN_def Bex_def atLeast_iff
+ by (metis zero_le_imp_eq_int zero_zle_int)
+
+lemma ZN_le [transfer_rule]: "(ZN ===> ZN ===> op =) (op \<le>) (op \<le>)"
+ unfolding fun_rel_def ZN_def by simp
+
+lemma ZN_less [transfer_rule]: "(ZN ===> ZN ===> op =) (op <) (op <)"
+ unfolding fun_rel_def ZN_def by simp
+
+lemma ZN_eq [transfer_rule]: "(ZN ===> ZN ===> op =) (op =) (op =)"
+ unfolding fun_rel_def ZN_def by simp
+
+lemma ZN_Suc [transfer_rule]: "(ZN ===> ZN) (\<lambda>x. x + 1) Suc"
+ unfolding fun_rel_def ZN_def by simp
+
+lemma ZN_numeral [transfer_rule]:
+ "(op = ===> ZN) numeral numeral"
+ unfolding fun_rel_def ZN_def by simp
+
+lemma ZN_dvd [transfer_rule]: "(ZN ===> ZN ===> op =) (op dvd) (op dvd)"
+ unfolding fun_rel_def ZN_def by (simp add: zdvd_int)
+
+lemma ZN_div [transfer_rule]: "(ZN ===> ZN ===> ZN) (op div) (op div)"
+ unfolding fun_rel_def ZN_def by (simp add: zdiv_int)
+
+lemma ZN_mod [transfer_rule]: "(ZN ===> ZN ===> ZN) (op mod) (op mod)"
+ unfolding fun_rel_def ZN_def by (simp add: zmod_int)
+
+lemma ZN_gcd [transfer_rule]: "(ZN ===> ZN ===> ZN) gcd gcd"
+ unfolding fun_rel_def ZN_def by (simp add: transfer_int_nat_gcd)
+
+text {* For derived operations, we can use the @{text "transfer_prover"}
+ method to help generate transfer rules. *}
+
+lemma ZN_listsum [transfer_rule]: "(list_all2 ZN ===> ZN) listsum listsum"
+ unfolding listsum_def [abs_def] by transfer_prover
+
+subsection {* Transfer examples *}
+
+lemma
+ assumes "\<And>i::int. 0 \<le> i \<Longrightarrow> i + 0 = i"
+ shows "\<And>i::nat. i + 0 = i"
+apply transfer
+apply fact
+done
+
+lemma
+ assumes "\<And>i k::int. \<lbrakk>0 \<le> i; 0 \<le> k; i < k\<rbrakk> \<Longrightarrow> \<exists>j\<in>{0..}. i + j = k"
+ shows "\<And>i k::nat. i < k \<Longrightarrow> \<exists>j. i + j = k"
+apply transfer
+apply fact
+done
+
+lemma
+ assumes "\<forall>x\<in>{0::int..}. \<forall>y\<in>{0..}. x * y div y = x"
+ shows "\<forall>x y :: nat. x * y div y = x"
+apply transfer
+apply fact
+done
+
+lemma
+ assumes "\<And>m n::int. \<lbrakk>0 \<le> m; 0 \<le> n; m * n = 0\<rbrakk> \<Longrightarrow> m = 0 \<or> n = 0"
+ shows "m * n = (0::nat) \<Longrightarrow> m = 0 \<or> n = 0"
+apply transfer
+apply fact
+done
+
+lemma
+ assumes "\<forall>x\<in>{0::int..}. \<exists>y\<in>{0..}. \<exists>z\<in>{0..}. x + 3 * y = 5 * z"
+ shows "\<forall>x::nat. \<exists>y z. x + 3 * y = 5 * z"
+apply transfer
+apply fact
+done
+
+text {* The @{text "fixing"} option prevents generalization over the free
+ variable @{text "n"}, allowing the local transfer rule to be used. *}
+
+lemma
+ assumes [transfer_rule]: "ZN x n"
+ assumes "\<forall>i\<in>{0..}. i < x \<longrightarrow> 2 * i < 3 * x"
+ shows "\<forall>i. i < n \<longrightarrow> 2 * i < 3 * n"
+apply (transfer fixing: n)
+apply fact
+done
+
+lemma
+ assumes "gcd (2^i) (3^j) = (1::int)"
+ shows "gcd (2^i) (3^j) = (1::nat)"
+apply (transfer fixing: i j)
+apply fact
+done
+
+lemma
+ assumes "\<And>x y z::int. \<lbrakk>0 \<le> x; 0 \<le> y; 0 \<le> z\<rbrakk> \<Longrightarrow>
+ listsum [x, y, z] = 0 \<longleftrightarrow> list_all (\<lambda>x. x = 0) [x, y, z]"
+ shows "listsum [x, y, z] = (0::nat) \<longleftrightarrow> list_all (\<lambda>x. x = 0) [x, y, z]"
+apply transfer
+apply fact
+done
+
+text {* Quantifiers over higher types (e.g. @{text "nat list"}) may
+ generate @{text "Domainp"} assumptions when transferred. *}
+
+lemma
+ assumes "\<And>xs::int list. Domainp (list_all2 ZN) xs \<Longrightarrow>
+ (listsum xs = 0) = list_all (\<lambda>x. x = 0) xs"
+ shows "listsum xs = (0::nat) \<longleftrightarrow> list_all (\<lambda>x. x = 0) xs"
+apply transfer
+apply fact
+done
+
+text {* Equality on a higher type can be transferred if the relations
+ involved are bi-unique. *}
+
+lemma
+ assumes "\<And>xs\<Colon>int list. \<lbrakk>Domainp (list_all2 ZN) xs; xs \<noteq> []\<rbrakk> \<Longrightarrow>
+ listsum xs < listsum (map (\<lambda>x. x + 1) xs)"
+ shows "xs \<noteq> [] \<Longrightarrow> listsum xs < listsum (map Suc xs)"
+apply transfer
+apply fact
+done
+
+end