# HG changeset patch # User wenzelm # Date 1335014765 -7200 # Node ID d6a3b69f4404a6ff0864b51ec7db43568e648bf5 # Parent b9e132e54d25c0dacbc1119ea8eb22e53c23abec# Parent 4605d4341b8b12908c90773b4a1895694a414483 merged diff -r 4605d4341b8b -r d6a3b69f4404 NEWS --- 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. diff -r 4605d4341b8b -r d6a3b69f4404 src/HOL/IsaMakefile --- 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 diff -r 4605d4341b8b -r d6a3b69f4404 src/HOL/ex/ROOT.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", diff -r 4605d4341b8b -r d6a3b69f4404 src/HOL/ex/Transfer_Int_Nat.thy --- /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 \ nat \ bool" + where "ZN = (\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 (\x. 0 \ 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 \) (op \)" + 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) (\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 "\i::int. 0 \ i \ i + 0 = i" + shows "\i::nat. i + 0 = i" +apply transfer +apply fact +done + +lemma + assumes "\i k::int. \0 \ i; 0 \ k; i < k\ \ \j\{0..}. i + j = k" + shows "\i k::nat. i < k \ \j. i + j = k" +apply transfer +apply fact +done + +lemma + assumes "\x\{0::int..}. \y\{0..}. x * y div y = x" + shows "\x y :: nat. x * y div y = x" +apply transfer +apply fact +done + +lemma + assumes "\m n::int. \0 \ m; 0 \ n; m * n = 0\ \ m = 0 \ n = 0" + shows "m * n = (0::nat) \ m = 0 \ n = 0" +apply transfer +apply fact +done + +lemma + assumes "\x\{0::int..}. \y\{0..}. \z\{0..}. x + 3 * y = 5 * z" + shows "\x::nat. \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 "\i\{0..}. i < x \ 2 * i < 3 * x" + shows "\i. i < n \ 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 "\x y z::int. \0 \ x; 0 \ y; 0 \ z\ \ + listsum [x, y, z] = 0 \ list_all (\x. x = 0) [x, y, z]" + shows "listsum [x, y, z] = (0::nat) \ list_all (\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 "\xs::int list. Domainp (list_all2 ZN) xs \ + (listsum xs = 0) = list_all (\x. x = 0) xs" + shows "listsum xs = (0::nat) \ list_all (\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 "\xs\int list. \Domainp (list_all2 ZN) xs; xs \ []\ \ + listsum xs < listsum (map (\x. x + 1) xs)" + shows "xs \ [] \ listsum xs < listsum (map Suc xs)" +apply transfer +apply fact +done + +end