# HG changeset patch # User wenzelm # Date 1360857975 -3600 # Node ID e51e76ffaedd4de9427230990f5daaa36cd84e48 # Parent 47af65ef228e92489948679bec1586b0a7f9bb8c# Parent 386a117925db6f2c8349b23dc0b12b0403c28e7b merged diff -r 386a117925db -r e51e76ffaedd NEWS --- a/NEWS Thu Feb 14 16:36:21 2013 +0100 +++ b/NEWS Thu Feb 14 17:06:15 2013 +0100 @@ -10,6 +10,15 @@ (lin)order_topology. Allows to generalize theorems about limits and order. Instances are reals and extended reals. +*** HOL *** + +* Consolidation of library theories on product orders: + + Product_Lattice ~> Product_Order -- pointwise order on products + Product_ord ~> Product_Lexorder -- lexicographic order on products + +INCOMPATIBILITY. + New in Isabelle2013 (February 2013) ----------------------------------- diff -r 386a117925db -r e51e76ffaedd src/HOL/Big_Operators.thy --- a/src/HOL/Big_Operators.thy Thu Feb 14 16:36:21 2013 +0100 +++ b/src/HOL/Big_Operators.thy Thu Feb 14 17:06:15 2013 +0100 @@ -6,7 +6,7 @@ header {* Big operators and finite (non-empty) sets *} theory Big_Operators -imports Plain +imports Finite_Set Metis begin subsection {* Generic monoid operation over a set *} diff -r 386a117925db -r e51e76ffaedd src/HOL/Code_Evaluation.thy --- a/src/HOL/Code_Evaluation.thy Thu Feb 14 16:36:21 2013 +0100 +++ b/src/HOL/Code_Evaluation.thy Thu Feb 14 17:06:15 2013 +0100 @@ -5,7 +5,7 @@ header {* Term evaluation using the generic code generator *} theory Code_Evaluation -imports Plain Typerep New_DSequence +imports Typerep New_DSequence begin subsection {* Term representation *} diff -r 386a117925db -r e51e76ffaedd src/HOL/Codegenerator_Test/RBT_Set_Test.thy --- a/src/HOL/Codegenerator_Test/RBT_Set_Test.thy Thu Feb 14 16:36:21 2013 +0100 +++ b/src/HOL/Codegenerator_Test/RBT_Set_Test.thy Thu Feb 14 17:06:15 2013 +0100 @@ -22,23 +22,13 @@ lemma [code, code del]: "pred_of_set = pred_of_set" .. - -lemma [code, code del]: - "Cardinality.card' = Cardinality.card'" .. - -lemma [code, code del]: - "Cardinality.finite' = Cardinality.finite'" .. - -lemma [code, code del]: - "Cardinality.subset' = Cardinality.subset'" .. - -lemma [code, code del]: - "Cardinality.eq_set = Cardinality.eq_set" .. - - lemma [code, code del]: "acc = acc" .. +lemmas [code del] = + finite_set_code finite_coset_code + equal_set_code + (* If the code generation ends with an exception with the following message: '"List.set" is not a constructor, on left hand side of equation: ...', diff -r 386a117925db -r e51e76ffaedd src/HOL/Equiv_Relations.thy --- a/src/HOL/Equiv_Relations.thy Thu Feb 14 16:36:21 2013 +0100 +++ b/src/HOL/Equiv_Relations.thy Thu Feb 14 17:06:15 2013 +0100 @@ -5,7 +5,7 @@ header {* Equivalence Relations in Higher-Order Set Theory *} theory Equiv_Relations -imports Big_Operators Relation Plain +imports Big_Operators Relation begin subsection {* Equivalence relations -- set version *} diff -r 386a117925db -r e51e76ffaedd src/HOL/Int.thy --- a/src/HOL/Int.thy Thu Feb 14 16:36:21 2013 +0100 +++ b/src/HOL/Int.thy Thu Feb 14 17:06:15 2013 +0100 @@ -6,7 +6,7 @@ header {* The Integers as Equivalence Classes over Pairs of Natural Numbers *} theory Int -imports Equiv_Relations Wellfounded Quotient +imports Equiv_Relations Wellfounded Quotient FunDef begin subsection {* Definition of integers as a quotient type *} diff -r 386a117925db -r e51e76ffaedd src/HOL/Library/Cardinality.thy --- a/src/HOL/Library/Cardinality.thy Thu Feb 14 16:36:21 2013 +0100 +++ b/src/HOL/Library/Cardinality.thy Thu Feb 14 17:06:15 2013 +0100 @@ -199,7 +199,7 @@ subsection {* A type class for computing the cardinality of types *} definition is_list_UNIV :: "'a list \ bool" -where [code del]: "is_list_UNIV xs = (let c = CARD('a) in if c = 0 then False else size (remdups xs) = c)" +where "is_list_UNIV xs = (let c = CARD('a) in if c = 0 then False else size (remdups xs) = c)" lemma is_list_UNIV_iff: "is_list_UNIV xs \ set xs = UNIV" by(auto simp add: is_list_UNIV_def Let_def card_eq_0_iff List.card_set[symmetric] @@ -211,15 +211,6 @@ fixes card_UNIV :: "'a card_UNIV" assumes card_UNIV: "card_UNIV = Phantom('a) CARD('a)" -lemma card_UNIV_code [code_unfold]: - "CARD('a :: card_UNIV) = of_phantom (card_UNIV :: 'a card_UNIV)" -by(simp add: card_UNIV) - -lemma is_list_UNIV_code [code]: - "is_list_UNIV (xs :: 'a list) = - (let c = CARD('a :: card_UNIV) in if c = 0 then False else size (remdups xs) = c)" -by(rule is_list_UNIV_def) - subsection {* Instantiations for @{text "card_UNIV"} *} instantiation nat :: card_UNIV begin @@ -396,80 +387,66 @@ subsection {* Code setup for sets *} +text {* + Implement operations @{term "finite"}, @{term "card"}, @{term "op \"}, and @{term "op ="} + for sets using @{term "finite_UNIV"} and @{term "card_UNIV"}. +*} + lemma card_Compl: "finite A \ card (- A) = card (UNIV :: 'a set) - card (A :: 'a set)" by (metis Compl_eq_Diff_UNIV card_Diff_subset top_greatest) -context fixes xs :: "'a :: card_UNIV list" -begin +lemma card_coset_code [code]: + fixes xs :: "'a :: card_UNIV list" + shows "card (List.coset xs) = of_phantom (card_UNIV :: 'a card_UNIV) - length (remdups xs)" +by(simp add: List.card_set card_Compl card_UNIV) -definition card' :: "'a set \ nat" -where [simp, code del, code_abbrev]: "card' = card" - -lemma card'_code [code]: - "card' (set xs) = length (remdups xs)" - "card' (List.coset xs) = of_phantom (card_UNIV :: 'a card_UNIV) - length (remdups xs)" -by(simp_all add: List.card_set card_Compl card_UNIV) +lemma [code, code del]: "finite = finite" .. -lemma card'_UNIV [code_unfold]: - "card' (UNIV :: 'a :: card_UNIV set) = of_phantom (card_UNIV :: 'a card_UNIV)" -by(simp add: card_UNIV) - -definition finite' :: "'a set \ bool" -where [simp, code del, code_abbrev]: "finite' = finite" - -lemma finite'_code [code]: - "finite' (set xs) \ True" - "finite' (List.coset xs) \ of_phantom (finite_UNIV :: 'a finite_UNIV)" +lemma [code]: + fixes xs :: "'a :: card_UNIV list" + shows finite_set_code: + "finite (set xs) = True" + and finite_coset_code: + "finite (List.coset xs) \ of_phantom (finite_UNIV :: 'a finite_UNIV)" by(simp_all add: card_gt_0_iff finite_UNIV) -definition subset' :: "'a set \ 'a set \ bool" -where [simp, code del, code_abbrev]: "subset' = op \" - -lemma subset'_code [code]: - "subset' A (List.coset ys) \ (\y \ set ys. y \ A)" - "subset' (set ys) B \ (\y \ set ys. y \ B)" - "subset' (List.coset xs) (set ys) \ (let n = CARD('a) in n > 0 \ card(set (xs @ ys)) = n)" +lemma coset_subset_code [code]: + fixes xs :: "'a list" shows + "List.coset xs \ set ys \ (let n = CARD('a) in n > 0 \ card (set (xs @ ys)) = n)" by(auto simp add: Let_def card_gt_0_iff dest: card_eq_UNIV_imp_eq_UNIV intro: arg_cong[where f=card]) (metis finite_compl finite_set rev_finite_subset) -definition eq_set :: "'a set \ 'a set \ bool" -where [simp, code del, code_abbrev]: "eq_set = op =" - -lemma eq_set_code [code]: - fixes ys +lemma equal_set_code [code]: + fixes xs ys :: "'a :: equal list" defines "rhs \ let n = CARD('a) in if n = 0 then False else let xs' = remdups xs; ys' = remdups ys in length xs' + length ys' = n \ (\x \ set xs'. x \ set ys') \ (\y \ set ys'. y \ set xs')" - shows "eq_set (List.coset xs) (set ys) \ rhs" (is ?thesis1) - and "eq_set (set ys) (List.coset xs) \ rhs" (is ?thesis2) - and "eq_set (set xs) (set ys) \ (\x \ set xs. x \ set ys) \ (\y \ set ys. y \ set xs)" (is ?thesis3) - and "eq_set (List.coset xs) (List.coset ys) \ (\x \ set xs. x \ set ys) \ (\y \ set ys. y \ set xs)" (is ?thesis4) + shows "equal_class.equal (List.coset xs) (set ys) \ rhs" (is ?thesis1) + and "equal_class.equal (set ys) (List.coset xs) \ rhs" (is ?thesis2) + and "equal_class.equal (set xs) (set ys) \ (\x \ set xs. x \ set ys) \ (\y \ set ys. y \ set xs)" (is ?thesis3) + and "equal_class.equal (List.coset xs) (List.coset ys) \ (\x \ set xs. x \ set ys) \ (\y \ set ys. y \ set xs)" (is ?thesis4) proof - show ?thesis1 (is "?lhs \ ?rhs") proof assume ?lhs thus ?rhs - by(auto simp add: rhs_def Let_def List.card_set[symmetric] card_Un_Int[where A="set xs" and B="- set xs"] card_UNIV Compl_partition card_gt_0_iff dest: sym)(metis finite_compl finite_set) + by(auto simp add: equal_eq rhs_def Let_def List.card_set[symmetric] card_Un_Int[where A="set xs" and B="- set xs"] card_UNIV Compl_partition card_gt_0_iff dest: sym)(metis finite_compl finite_set) next assume ?rhs moreover have "\ \y\set xs. y \ set ys; \x\set ys. x \ set xs \ \ set xs \ set ys = {}" by blast ultimately show ?lhs - by(auto simp add: rhs_def Let_def List.card_set[symmetric] card_UNIV card_gt_0_iff card_Un_Int[where A="set xs" and B="set ys"] dest: card_eq_UNIV_imp_eq_UNIV split: split_if_asm) + by(auto simp add: equal_eq rhs_def Let_def List.card_set[symmetric] card_UNIV card_gt_0_iff card_Un_Int[where A="set xs" and B="set ys"] dest: card_eq_UNIV_imp_eq_UNIV split: split_if_asm) qed - thus ?thesis2 unfolding eq_set_def by blast - show ?thesis3 ?thesis4 unfolding eq_set_def List.coset_def by blast+ + thus ?thesis2 unfolding equal_eq by blast + show ?thesis3 ?thesis4 unfolding equal_eq List.coset_def by blast+ qed -end - notepad begin (* test code setup *) have "List.coset [True] = set [False] \ List.coset [] \ List.set [True, False] \ finite (List.coset [True])" by eval end -hide_const (open) card' finite' subset' eq_set - end diff -r 386a117925db -r e51e76ffaedd src/HOL/Library/Code_Abstract_Nat.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/Code_Abstract_Nat.thy Thu Feb 14 17:06:15 2013 +0100 @@ -0,0 +1,113 @@ +(* Title: HOL/Library/Code_Abstract_Nat.thy + Author: Stefan Berghofer, Florian Haftmann, TU Muenchen +*) + +header {* Avoidance of pattern matching on natural numbers *} + +theory Code_Abstract_Nat +imports Main +begin + +text {* + When natural numbers are implemented in another than the + conventional inductive @{term "0::nat"}/@{term Suc} representation, + it is necessary to avoid all pattern matching on natural numbers + altogether. This is accomplished by this theory (up to a certain + extent). +*} + +subsection {* Case analysis *} + +text {* + Case analysis on natural numbers is rephrased using a conditional + expression: +*} + +lemma [code, code_unfold]: + "nat_case = (\f g n. if n = 0 then f else g (n - 1))" + by (auto simp add: fun_eq_iff dest!: gr0_implies_Suc) + + +subsection {* Preprocessors *} + +text {* + The term @{term "Suc n"} is no longer a valid pattern. Therefore, + all occurrences of this term in a position where a pattern is + expected (i.e.~on the left-hand side of a code equation) must be + eliminated. This can be accomplished – as far as possible – by + applying the following transformation rule: +*} + +lemma Suc_if_eq: "(\n. f (Suc n) \ h n) \ f 0 \ g \ + f n \ if n = 0 then g else h (n - 1)" + by (rule eq_reflection) (cases n, simp_all) + +text {* + The rule above is built into a preprocessor that is plugged into + the code generator. +*} + +setup {* +let + +fun remove_suc thy thms = + let + val vname = singleton (Name.variant_list (map fst + (fold (Term.add_var_names o Thm.full_prop_of) thms []))) "n"; + val cv = cterm_of thy (Var ((vname, 0), HOLogic.natT)); + fun lhs_of th = snd (Thm.dest_comb + (fst (Thm.dest_comb (cprop_of th)))); + fun rhs_of th = snd (Thm.dest_comb (cprop_of th)); + fun find_vars ct = (case term_of ct of + (Const (@{const_name Suc}, _) $ Var _) => [(cv, snd (Thm.dest_comb ct))] + | _ $ _ => + let val (ct1, ct2) = Thm.dest_comb ct + in + map (apfst (fn ct => Thm.apply ct ct2)) (find_vars ct1) @ + map (apfst (Thm.apply ct1)) (find_vars ct2) + end + | _ => []); + val eqs = maps + (fn th => map (pair th) (find_vars (lhs_of th))) thms; + fun mk_thms (th, (ct, cv')) = + let + val th' = + Thm.implies_elim + (Conv.fconv_rule (Thm.beta_conversion true) + (Drule.instantiate' + [SOME (ctyp_of_term ct)] [SOME (Thm.lambda cv ct), + SOME (Thm.lambda cv' (rhs_of th)), NONE, SOME cv'] + @{thm Suc_if_eq})) (Thm.forall_intr cv' th) + in + case map_filter (fn th'' => + SOME (th'', singleton + (Variable.trade (K (fn [th'''] => [th''' RS th'])) + (Variable.global_thm_context th'')) th'') + handle THM _ => NONE) thms of + [] => NONE + | thps => + let val (ths1, ths2) = split_list thps + in SOME (subtract Thm.eq_thm (th :: ths1) thms @ ths2) end + end + in get_first mk_thms eqs end; + +fun eqn_suc_base_preproc thy thms = + let + val dest = fst o Logic.dest_equals o prop_of; + val contains_suc = exists_Const (fn (c, _) => c = @{const_name Suc}); + in + if forall (can dest) thms andalso exists (contains_suc o dest) thms + then thms |> perhaps_loop (remove_suc thy) |> (Option.map o map) Drule.zero_var_indexes + else NONE + end; + +val eqn_suc_preproc = Code_Preproc.simple_functrans eqn_suc_base_preproc; + +in + + Code_Preproc.add_functrans ("eqn_Suc", eqn_suc_preproc) + +end; +*} + +end diff -r 386a117925db -r e51e76ffaedd src/HOL/Library/Code_Binary_Nat.thy --- a/src/HOL/Library/Code_Binary_Nat.thy Thu Feb 14 16:36:21 2013 +0100 +++ b/src/HOL/Library/Code_Binary_Nat.thy Thu Feb 14 17:06:15 2013 +0100 @@ -1,11 +1,11 @@ (* Title: HOL/Library/Code_Binary_Nat.thy - Author: Stefan Berghofer, Florian Haftmann, TU Muenchen + Author: Florian Haftmann, TU Muenchen *) header {* Implementation of natural numbers as binary numerals *} theory Code_Binary_Nat -imports Main +imports Code_Abstract_Nat begin text {* @@ -146,104 +146,6 @@ by (simp_all add: nat_of_num_numeral) -subsection {* Case analysis *} - -text {* - Case analysis on natural numbers is rephrased using a conditional - expression: -*} - -lemma [code, code_unfold]: - "nat_case = (\f g n. if n = 0 then f else g (n - 1))" - by (auto simp add: fun_eq_iff dest!: gr0_implies_Suc) - - -subsection {* Preprocessors *} - -text {* - The term @{term "Suc n"} is no longer a valid pattern. - Therefore, all occurrences of this term in a position - where a pattern is expected (i.e.~on the left-hand side of a recursion - equation) must be eliminated. - This can be accomplished by applying the following transformation rules: -*} - -lemma Suc_if_eq: "(\n. f (Suc n) \ h n) \ f 0 \ g \ - f n \ if n = 0 then g else h (n - 1)" - by (rule eq_reflection) (cases n, simp_all) - -text {* - The rules above are built into a preprocessor that is plugged into - the code generator. Since the preprocessor for introduction rules - does not know anything about modes, some of the modes that worked - for the canonical representation of natural numbers may no longer work. -*} - -(*<*) -setup {* -let - -fun remove_suc thy thms = - let - val vname = singleton (Name.variant_list (map fst - (fold (Term.add_var_names o Thm.full_prop_of) thms []))) "n"; - val cv = cterm_of thy (Var ((vname, 0), HOLogic.natT)); - fun lhs_of th = snd (Thm.dest_comb - (fst (Thm.dest_comb (cprop_of th)))); - fun rhs_of th = snd (Thm.dest_comb (cprop_of th)); - fun find_vars ct = (case term_of ct of - (Const (@{const_name Suc}, _) $ Var _) => [(cv, snd (Thm.dest_comb ct))] - | _ $ _ => - let val (ct1, ct2) = Thm.dest_comb ct - in - map (apfst (fn ct => Thm.apply ct ct2)) (find_vars ct1) @ - map (apfst (Thm.apply ct1)) (find_vars ct2) - end - | _ => []); - val eqs = maps - (fn th => map (pair th) (find_vars (lhs_of th))) thms; - fun mk_thms (th, (ct, cv')) = - let - val th' = - Thm.implies_elim - (Conv.fconv_rule (Thm.beta_conversion true) - (Drule.instantiate' - [SOME (ctyp_of_term ct)] [SOME (Thm.lambda cv ct), - SOME (Thm.lambda cv' (rhs_of th)), NONE, SOME cv'] - @{thm Suc_if_eq})) (Thm.forall_intr cv' th) - in - case map_filter (fn th'' => - SOME (th'', singleton - (Variable.trade (K (fn [th'''] => [th''' RS th'])) - (Variable.global_thm_context th'')) th'') - handle THM _ => NONE) thms of - [] => NONE - | thps => - let val (ths1, ths2) = split_list thps - in SOME (subtract Thm.eq_thm (th :: ths1) thms @ ths2) end - end - in get_first mk_thms eqs end; - -fun eqn_suc_base_preproc thy thms = - let - val dest = fst o Logic.dest_equals o prop_of; - val contains_suc = exists_Const (fn (c, _) => c = @{const_name Suc}); - in - if forall (can dest) thms andalso exists (contains_suc o dest) thms - then thms |> perhaps_loop (remove_suc thy) |> (Option.map o map) Drule.zero_var_indexes - else NONE - end; - -val eqn_suc_preproc = Code_Preproc.simple_functrans eqn_suc_base_preproc; - -in - - Code_Preproc.add_functrans ("eqn_Suc", eqn_suc_preproc) - -end; -*} -(*>*) - code_modulename SML Code_Binary_Nat Arith diff -r 386a117925db -r e51e76ffaedd src/HOL/Library/Code_Numeral_Types.thy --- a/src/HOL/Library/Code_Numeral_Types.thy Thu Feb 14 16:36:21 2013 +0100 +++ b/src/HOL/Library/Code_Numeral_Types.thy Thu Feb 14 17:06:15 2013 +0100 @@ -13,9 +13,11 @@ typedef integer = "UNIV \ int set" morphisms int_of_integer integer_of_int .. +setup_lifting (no_code) type_definition_integer + lemma integer_eq_iff: "k = l \ int_of_integer k = int_of_integer l" - using int_of_integer_inject [of k l] .. + by transfer rule lemma integer_eqI: "int_of_integer k = int_of_integer l \ k = l" @@ -23,172 +25,199 @@ lemma int_of_integer_integer_of_int [simp]: "int_of_integer (integer_of_int k) = k" - using integer_of_int_inverse [of k] by simp + by transfer rule lemma integer_of_int_int_of_integer [simp]: "integer_of_int (int_of_integer k) = k" - using int_of_integer_inverse [of k] by simp + by transfer rule instantiation integer :: ring_1 begin -definition - "0 = integer_of_int 0" +lift_definition zero_integer :: integer + is "0 :: int" + . -lemma int_of_integer_zero [simp]: - "int_of_integer 0 = 0" - by (simp add: zero_integer_def) - -definition - "1 = integer_of_int 1" +declare zero_integer.rep_eq [simp] -lemma int_of_integer_one [simp]: - "int_of_integer 1 = 1" - by (simp add: one_integer_def) +lift_definition one_integer :: integer + is "1 :: int" + . + +declare one_integer.rep_eq [simp] -definition - "k + l = integer_of_int (int_of_integer k + int_of_integer l)" +lift_definition plus_integer :: "integer \ integer \ integer" + is "plus :: int \ int \ int" + . -lemma int_of_integer_plus [simp]: - "int_of_integer (k + l) = int_of_integer k + int_of_integer l" - by (simp add: plus_integer_def) +declare plus_integer.rep_eq [simp] -definition - "- k = integer_of_int (- int_of_integer k)" +lift_definition uminus_integer :: "integer \ integer" + is "uminus :: int \ int" + . -lemma int_of_integer_uminus [simp]: - "int_of_integer (- k) = - int_of_integer k" - by (simp add: uminus_integer_def) - -definition - "k - l = integer_of_int (int_of_integer k - int_of_integer l)" +declare uminus_integer.rep_eq [simp] -lemma int_of_integer_minus [simp]: - "int_of_integer (k - l) = int_of_integer k - int_of_integer l" - by (simp add: minus_integer_def) +lift_definition minus_integer :: "integer \ integer \ integer" + is "minus :: int \ int \ int" + . + +declare minus_integer.rep_eq [simp] -definition - "k * l = integer_of_int (int_of_integer k * int_of_integer l)" +lift_definition times_integer :: "integer \ integer \ integer" + is "times :: int \ int \ int" + . -lemma int_of_integer_times [simp]: - "int_of_integer (k * l) = int_of_integer k * int_of_integer l" - by (simp add: times_integer_def) +declare times_integer.rep_eq [simp] instance proof -qed (auto simp add: integer_eq_iff algebra_simps) +qed (transfer, simp add: algebra_simps)+ end +lemma [transfer_rule]: + "fun_rel HOL.eq cr_integer (of_nat :: nat \ int) (of_nat :: nat \ integer)" + by (unfold of_nat_def [abs_def]) transfer_prover + +lemma [transfer_rule]: + "fun_rel HOL.eq cr_integer (\k :: int. k :: int) (of_int :: int \ integer)" +proof - + have "fun_rel HOL.eq cr_integer (of_int :: int \ int) (of_int :: int \ integer)" + by (unfold of_int_of_nat [abs_def]) transfer_prover + then show ?thesis by (simp add: id_def) +qed + +lemma [transfer_rule]: + "fun_rel HOL.eq cr_integer (numeral :: num \ int) (numeral :: num \ integer)" +proof - + have "fun_rel HOL.eq cr_integer (numeral :: num \ int) (\n. of_int (numeral n))" + by transfer_prover + then show ?thesis by simp +qed + +lemma [transfer_rule]: + "fun_rel HOL.eq cr_integer (neg_numeral :: num \ int) (neg_numeral :: num \ integer)" + by (unfold neg_numeral_def [abs_def]) transfer_prover + +lemma [transfer_rule]: + "fun_rel HOL.eq (fun_rel HOL.eq cr_integer) (Num.sub :: _ \ _ \ int) (Num.sub :: _ \ _ \ integer)" + by (unfold Num.sub_def [abs_def]) transfer_prover + lemma int_of_integer_of_nat [simp]: "int_of_integer (of_nat n) = of_nat n" - by (induct n) simp_all + by transfer rule -definition integer_of_nat :: "nat \ integer" -where - "integer_of_nat = of_nat" +lift_definition integer_of_nat :: "nat \ integer" + is "of_nat :: nat \ int" + . lemma int_of_integer_integer_of_nat [simp]: "int_of_integer (integer_of_nat n) = of_nat n" - by (simp add: integer_of_nat_def) - -definition nat_of_integer :: "integer \ nat" -where - "nat_of_integer k = Int.nat (int_of_integer k)" + by transfer rule + +lift_definition nat_of_integer :: "integer \ nat" + is Int.nat + . lemma nat_of_integer_of_nat [simp]: "nat_of_integer (of_nat n) = n" - by (simp add: nat_of_integer_def) + by transfer simp lemma int_of_integer_of_int [simp]: "int_of_integer (of_int k) = k" - by (induct k) (simp_all, simp only: neg_numeral_def numeral_One int_of_integer_uminus int_of_integer_one) + by transfer simp lemma nat_of_integer_integer_of_nat [simp]: "nat_of_integer (integer_of_nat n) = n" - by (simp add: integer_of_nat_def) + by transfer simp lemma integer_of_int_eq_of_int [simp, code_abbrev]: "integer_of_int = of_int" - by rule (simp add: integer_eq_iff) + by transfer (simp add: fun_eq_iff) lemma of_int_integer_of [simp]: "of_int (int_of_integer k) = (k :: integer)" - by (simp add: integer_eq_iff) + by transfer rule lemma int_of_integer_numeral [simp]: "int_of_integer (numeral k) = numeral k" - using int_of_integer_of_int [of "numeral k"] by simp + by transfer rule lemma int_of_integer_neg_numeral [simp]: "int_of_integer (neg_numeral k) = neg_numeral k" - by (simp only: neg_numeral_def int_of_integer_uminus) simp + by transfer rule lemma int_of_integer_sub [simp]: "int_of_integer (Num.sub k l) = Num.sub k l" - by (simp only: Num.sub_def int_of_integer_minus int_of_integer_numeral) + by transfer rule instantiation integer :: "{ring_div, equal, linordered_idom}" begin -definition - "k div l = of_int (int_of_integer k div int_of_integer l)" +lift_definition div_integer :: "integer \ integer \ integer" + is "Divides.div :: int \ int \ int" + . -lemma int_of_integer_div [simp]: - "int_of_integer (k div l) = int_of_integer k div int_of_integer l" - by (simp add: div_integer_def) +declare div_integer.rep_eq [simp] -definition - "k mod l = of_int (int_of_integer k mod int_of_integer l)" +lift_definition mod_integer :: "integer \ integer \ integer" + is "Divides.mod :: int \ int \ int" + . + +declare mod_integer.rep_eq [simp] -lemma int_of_integer_mod [simp]: - "int_of_integer (k mod l) = int_of_integer k mod int_of_integer l" - by (simp add: mod_integer_def) +lift_definition abs_integer :: "integer \ integer" + is "abs :: int \ int" + . -definition - "\k\ = of_int \int_of_integer k\" +declare abs_integer.rep_eq [simp] -lemma int_of_integer_abs [simp]: - "int_of_integer \k\ = \int_of_integer k\" - by (simp add: abs_integer_def) +lift_definition sgn_integer :: "integer \ integer" + is "sgn :: int \ int" + . -definition - "sgn k = of_int (sgn (int_of_integer k))" +declare sgn_integer.rep_eq [simp] -lemma int_of_integer_sgn [simp]: - "int_of_integer (sgn k) = sgn (int_of_integer k)" - by (simp add: sgn_integer_def) +lift_definition less_eq_integer :: "integer \ integer \ bool" + is "less_eq :: int \ int \ bool" + . -definition - "k \ l \ int_of_integer k \ int_of_integer l" +lift_definition less_integer :: "integer \ integer \ bool" + is "less :: int \ int \ bool" + . -definition - "k < l \ int_of_integer k < int_of_integer l" - -definition - "HOL.equal k l \ HOL.equal (int_of_integer k) (int_of_integer l)" +lift_definition equal_integer :: "integer \ integer \ bool" + is "HOL.equal :: int \ int \ bool" + . instance proof -qed (auto simp add: integer_eq_iff algebra_simps - less_eq_integer_def less_integer_def equal_integer_def equal - intro: mult_strict_right_mono) +qed (transfer, simp add: algebra_simps equal less_le_not_le [symmetric] mult_strict_right_mono linear)+ end +lemma [transfer_rule]: + "fun_rel cr_integer (fun_rel cr_integer cr_integer) (min :: _ \ _ \ int) (min :: _ \ _ \ integer)" + by (unfold min_def [abs_def]) transfer_prover + +lemma [transfer_rule]: + "fun_rel cr_integer (fun_rel cr_integer cr_integer) (max :: _ \ _ \ int) (max :: _ \ _ \ integer)" + by (unfold max_def [abs_def]) transfer_prover + lemma int_of_integer_min [simp]: "int_of_integer (min k l) = min (int_of_integer k) (int_of_integer l)" - by (simp add: min_def less_eq_integer_def) + by transfer rule lemma int_of_integer_max [simp]: "int_of_integer (max k l) = max (int_of_integer k) (int_of_integer l)" - by (simp add: max_def less_eq_integer_def) + by transfer rule lemma nat_of_integer_non_positive [simp]: "k \ 0 \ nat_of_integer k = 0" - by (simp add: nat_of_integer_def less_eq_integer_def) + by transfer simp lemma of_nat_of_integer [simp]: "of_nat (nat_of_integer k) = max 0 k" - by (simp add: nat_of_integer_def integer_eq_iff less_eq_integer_def max_def) + by transfer auto subsection {* Code theorems for target language integers *} @@ -199,29 +228,36 @@ where [simp, code_abbrev]: "Pos = numeral" +lemma [transfer_rule]: + "fun_rel HOL.eq cr_integer numeral Pos" + by simp transfer_prover + definition Neg :: "num \ integer" where [simp, code_abbrev]: "Neg = neg_numeral" +lemma [transfer_rule]: + "fun_rel HOL.eq cr_integer neg_numeral Neg" + by simp transfer_prover + code_datatype "0::integer" Pos Neg text {* Auxiliary operations *} -definition dup :: "integer \ integer" -where - [simp]: "dup k = k + k" +lift_definition dup :: "integer \ integer" + is "\k::int. k + k" + . lemma dup_code [code]: "dup 0 = 0" "dup (Pos n) = Pos (Num.Bit0 n)" "dup (Neg n) = Neg (Num.Bit0 n)" - unfolding Pos_def Neg_def neg_numeral_def - by (simp_all add: numeral_Bit0) + by (transfer, simp only: neg_numeral_def numeral_Bit0 minus_add_distrib)+ -definition sub :: "num \ num \ integer" -where - [simp]: "sub m n = numeral m - numeral n" +lift_definition sub :: "num \ num \ integer" + is "\m n. numeral m - numeral n :: int" + . lemma sub_code [code]: "sub Num.One Num.One = 0" @@ -233,9 +269,7 @@ "sub (Num.Bit1 m) (Num.Bit1 n) = dup (sub m n)" "sub (Num.Bit1 m) (Num.Bit0 n) = dup (sub m n) + 1" "sub (Num.Bit0 m) (Num.Bit1 n) = dup (sub m n) - 1" - unfolding sub_def dup_def numeral.simps Pos_def Neg_def - neg_numeral_def numeral_BitM - by (simp_all only: algebra_simps add.comm_neutral) + by (transfer, simp add: dbl_def dbl_inc_def dbl_dec_def)+ text {* Implementations *} @@ -251,7 +285,7 @@ "Pos m + Neg n = sub m n" "Neg m + Pos n = sub n m" "Neg m + Neg n = Neg (m + n)" - by simp_all + by (transfer, simp)+ lemma uminus_integer_code [code]: "uminus 0 = (0::integer)" @@ -266,7 +300,7 @@ "Pos m - Neg n = Pos (m + n)" "Neg m - Pos n = Neg (m + n)" "Neg m - Neg n = sub n m" - by simp_all + by (transfer, simp)+ lemma abs_integer_code [code]: "\k\ = (if (k::integer) < 0 then - k else k)" @@ -322,15 +356,18 @@ (let j = sub k l in if j < 0 then (0, Pos k) else let (q, r) = divmod_abs j (Pos l) in (q + 1, r))" - by (auto simp add: prod_eq_iff integer_eq_iff Let_def prod_case_beta - sub_non_negative sub_negative div_pos_pos_trivial mod_pos_pos_trivial div_pos_geq mod_pos_geq) + apply (simp add: prod_eq_iff Let_def prod_case_beta) + apply transfer + apply (simp add: sub_non_negative sub_negative div_pos_pos_trivial mod_pos_pos_trivial div_pos_geq mod_pos_geq) + done -lemma divmod_integer_code [code]: "divmod_integer k l = - (if k = 0 then (0, 0) else if l = 0 then (0, k) else - (apsnd \ times \ sgn) l (if sgn k = sgn l - then divmod_abs k l - else (let (r, s) = divmod_abs k l in - if s = 0 then (- r, 0) else (- r - 1, \l\ - s))))" +lemma divmod_integer_code [code]: + "divmod_integer k l = + (if k = 0 then (0, 0) else if l = 0 then (0, k) else + (apsnd \ times \ sgn) l (if sgn k = sgn l + then divmod_abs k l + else (let (r, s) = divmod_abs k l in + if s = 0 then (- r, 0) else (- r - 1, \l\ - s))))" proof - have aux1: "\k l::int. sgn k = sgn l \ k = 0 \ l = 0 \ 0 < l \ 0 < k \ l < 0 \ k < 0" by (auto simp add: sgn_if) @@ -358,7 +395,7 @@ "HOL.equal (Neg k) 0 \ False" "HOL.equal (Neg k) (Pos l) \ False" "HOL.equal (Neg k) (Neg l) \ HOL.equal k l" - by (simp_all add: equal integer_eq_iff) + by (simp_all add: equal) lemma equal_integer_refl [code nbe]: "HOL.equal (k::integer) k \ True" @@ -374,7 +411,7 @@ "Neg k \ 0 \ True" "Neg k \ Pos l \ True" "Neg k \ Neg l \ l \ k" - by (simp_all add: less_eq_integer_def) + by simp_all lemma less_integer_code [code]: "0 < (0::integer) \ False" @@ -386,21 +423,21 @@ "Neg k < 0 \ True" "Neg k < Pos l \ True" "Neg k < Neg l \ l < k" - by (simp_all add: less_integer_def) + by simp_all -definition integer_of_num :: "num \ integer" -where - "integer_of_num = numeral" +lift_definition integer_of_num :: "num \ integer" + is "numeral :: num \ int" + . lemma integer_of_num [code]: "integer_of_num num.One = 1" "integer_of_num (num.Bit0 n) = (let k = integer_of_num n in k + k)" "integer_of_num (num.Bit1 n) = (let k = integer_of_num n in k + k + 1)" - by (simp_all only: Let_def) (simp_all only: integer_of_num_def numeral.simps) + by (transfer, simp only: numeral.simps Let_def)+ -definition num_of_integer :: "integer \ num" -where - "num_of_integer = num_of_nat \ nat_of_integer" +lift_definition num_of_integer :: "integer \ num" + is "num_of_nat \ nat" + . lemma num_of_integer_code [code]: "num_of_integer k = (if k \ 1 then Num.One @@ -587,9 +624,11 @@ typedef natural = "UNIV \ nat set" morphisms nat_of_natural natural_of_nat .. +setup_lifting (no_code) type_definition_natural + lemma natural_eq_iff [termination_simp]: "m = n \ nat_of_natural m = nat_of_natural n" - using nat_of_natural_inject [of m n] .. + by transfer rule lemma natural_eqI: "nat_of_natural m = nat_of_natural n \ m = n" @@ -597,168 +636,179 @@ lemma nat_of_natural_of_nat_inverse [simp]: "nat_of_natural (natural_of_nat n) = n" - using natural_of_nat_inverse [of n] by simp + by transfer rule lemma natural_of_nat_of_natural_inverse [simp]: "natural_of_nat (nat_of_natural n) = n" - using nat_of_natural_inverse [of n] by simp + by transfer rule instantiation natural :: "{comm_monoid_diff, semiring_1}" begin -definition - "0 = natural_of_nat 0" +lift_definition zero_natural :: natural + is "0 :: nat" + . -lemma nat_of_natural_zero [simp]: - "nat_of_natural 0 = 0" - by (simp add: zero_natural_def) +declare zero_natural.rep_eq [simp] -definition - "1 = natural_of_nat 1" +lift_definition one_natural :: natural + is "1 :: nat" + . -lemma nat_of_natural_one [simp]: - "nat_of_natural 1 = 1" - by (simp add: one_natural_def) - -definition - "m + n = natural_of_nat (nat_of_natural m + nat_of_natural n)" +declare one_natural.rep_eq [simp] -lemma nat_of_natural_plus [simp]: - "nat_of_natural (m + n) = nat_of_natural m + nat_of_natural n" - by (simp add: plus_natural_def) +lift_definition plus_natural :: "natural \ natural \ natural" + is "plus :: nat \ nat \ nat" + . -definition - "m - n = natural_of_nat (nat_of_natural m - nat_of_natural n)" +declare plus_natural.rep_eq [simp] -lemma nat_of_natural_minus [simp]: - "nat_of_natural (m - n) = nat_of_natural m - nat_of_natural n" - by (simp add: minus_natural_def) +lift_definition minus_natural :: "natural \ natural \ natural" + is "minus :: nat \ nat \ nat" + . + +declare minus_natural.rep_eq [simp] -definition - "m * n = natural_of_nat (nat_of_natural m * nat_of_natural n)" +lift_definition times_natural :: "natural \ natural \ natural" + is "times :: nat \ nat \ nat" + . -lemma nat_of_natural_times [simp]: - "nat_of_natural (m * n) = nat_of_natural m * nat_of_natural n" - by (simp add: times_natural_def) +declare times_natural.rep_eq [simp] instance proof -qed (auto simp add: natural_eq_iff algebra_simps) +qed (transfer, simp add: algebra_simps)+ end +lemma [transfer_rule]: + "fun_rel HOL.eq cr_natural (\n::nat. n) (of_nat :: nat \ natural)" +proof - + have "fun_rel HOL.eq cr_natural (of_nat :: nat \ nat) (of_nat :: nat \ natural)" + by (unfold of_nat_def [abs_def]) transfer_prover + then show ?thesis by (simp add: id_def) +qed + +lemma [transfer_rule]: + "fun_rel HOL.eq cr_natural (numeral :: num \ nat) (numeral :: num \ natural)" +proof - + have "fun_rel HOL.eq cr_natural (numeral :: num \ nat) (\n. of_nat (numeral n))" + by transfer_prover + then show ?thesis by simp +qed + lemma nat_of_natural_of_nat [simp]: "nat_of_natural (of_nat n) = n" - by (induct n) simp_all + by transfer rule lemma natural_of_nat_of_nat [simp, code_abbrev]: "natural_of_nat = of_nat" - by rule (simp add: natural_eq_iff) + by transfer rule lemma of_nat_of_natural [simp]: "of_nat (nat_of_natural n) = n" - using natural_of_nat_of_natural_inverse [of n] by simp + by transfer rule lemma nat_of_natural_numeral [simp]: "nat_of_natural (numeral k) = numeral k" - using nat_of_natural_of_nat [of "numeral k"] by simp + by transfer rule instantiation natural :: "{semiring_div, equal, linordered_semiring}" begin -definition - "m div n = natural_of_nat (nat_of_natural m div nat_of_natural n)" +lift_definition div_natural :: "natural \ natural \ natural" + is "Divides.div :: nat \ nat \ nat" + . + +declare div_natural.rep_eq [simp] -lemma nat_of_natural_div [simp]: - "nat_of_natural (m div n) = nat_of_natural m div nat_of_natural n" - by (simp add: div_natural_def) +lift_definition mod_natural :: "natural \ natural \ natural" + is "Divides.mod :: nat \ nat \ nat" + . -definition - "m mod n = natural_of_nat (nat_of_natural m mod nat_of_natural n)" +declare mod_natural.rep_eq [simp] -lemma nat_of_natural_mod [simp]: - "nat_of_natural (m mod n) = nat_of_natural m mod nat_of_natural n" - by (simp add: mod_natural_def) +lift_definition less_eq_natural :: "natural \ natural \ bool" + is "less_eq :: nat \ nat \ bool" + . + +declare less_eq_natural.rep_eq [termination_simp] -definition - [termination_simp]: "m \ n \ nat_of_natural m \ nat_of_natural n" +lift_definition less_natural :: "natural \ natural \ bool" + is "less :: nat \ nat \ bool" + . -definition - [termination_simp]: "m < n \ nat_of_natural m < nat_of_natural n" +declare less_natural.rep_eq [termination_simp] -definition - "HOL.equal m n \ HOL.equal (nat_of_natural m) (nat_of_natural n)" +lift_definition equal_natural :: "natural \ natural \ bool" + is "HOL.equal :: nat \ nat \ bool" + . instance proof -qed (auto simp add: natural_eq_iff algebra_simps - less_eq_natural_def less_natural_def equal_natural_def equal) +qed (transfer, simp add: algebra_simps equal less_le_not_le [symmetric] linear)+ end +lemma [transfer_rule]: + "fun_rel cr_natural (fun_rel cr_natural cr_natural) (min :: _ \ _ \ nat) (min :: _ \ _ \ natural)" + by (unfold min_def [abs_def]) transfer_prover + +lemma [transfer_rule]: + "fun_rel cr_natural (fun_rel cr_natural cr_natural) (max :: _ \ _ \ nat) (max :: _ \ _ \ natural)" + by (unfold max_def [abs_def]) transfer_prover + lemma nat_of_natural_min [simp]: "nat_of_natural (min k l) = min (nat_of_natural k) (nat_of_natural l)" - by (simp add: min_def less_eq_natural_def) + by transfer rule lemma nat_of_natural_max [simp]: "nat_of_natural (max k l) = max (nat_of_natural k) (nat_of_natural l)" - by (simp add: max_def less_eq_natural_def) + by transfer rule -definition natural_of_integer :: "integer \ natural" -where - "natural_of_integer = of_nat \ nat_of_integer" +lift_definition natural_of_integer :: "integer \ natural" + is "nat :: int \ nat" + . -definition integer_of_natural :: "natural \ integer" -where - "integer_of_natural = of_nat \ nat_of_natural" +lift_definition integer_of_natural :: "natural \ integer" + is "of_nat :: nat \ int" + . lemma natural_of_integer_of_natural [simp]: "natural_of_integer (integer_of_natural n) = n" - by (simp add: natural_of_integer_def integer_of_natural_def natural_eq_iff) + by transfer simp lemma integer_of_natural_of_integer [simp]: "integer_of_natural (natural_of_integer k) = max 0 k" - by (simp add: natural_of_integer_def integer_of_natural_def integer_eq_iff) + by transfer auto lemma int_of_integer_of_natural [simp]: "int_of_integer (integer_of_natural n) = of_nat (nat_of_natural n)" - by (simp add: integer_of_natural_def) + by transfer rule lemma integer_of_natural_of_nat [simp]: "integer_of_natural (of_nat n) = of_nat n" - by (simp add: integer_eq_iff) + by transfer rule lemma [measure_function]: - "is_measure nat_of_natural" by (rule is_measure_trivial) + "is_measure nat_of_natural" + by (rule is_measure_trivial) subsection {* Inductive represenation of target language naturals *} -definition Suc :: "natural \ natural" -where - "Suc = natural_of_nat \ Nat.Suc \ nat_of_natural" +lift_definition Suc :: "natural \ natural" + is Nat.Suc + . -lemma nat_of_natural_Suc [simp]: - "nat_of_natural (Suc n) = Nat.Suc (nat_of_natural n)" - by (simp add: Suc_def) +declare Suc.rep_eq [simp] rep_datatype "0::natural" Suc -proof - - fix P :: "natural \ bool" - fix n :: natural - assume "P 0" then have init: "P (natural_of_nat 0)" by simp - assume "\n. P n \ P (Suc n)" - then have "\n. P (natural_of_nat n) \ P (Suc (natural_of_nat n))" . - then have step: "\n. P (natural_of_nat n) \ P (natural_of_nat (Nat.Suc n))" - by (simp add: Suc_def) - from init step have "P (natural_of_nat (nat_of_natural n))" - by (rule nat.induct) - with natural_of_nat_of_natural_inverse show "P n" by simp -qed (simp_all add: natural_eq_iff) + by (transfer, fact nat.induct nat.inject nat.distinct)+ lemma natural_case [case_names nat, cases type: natural]: fixes m :: natural assumes "\n. m = of_nat n \ P" shows P - by (rule assms [of "nat_of_natural m"]) simp + using assms by transfer blast lemma [simp, code]: "natural_size = nat_of_natural" @@ -778,7 +828,7 @@ lemma natural_decr [termination_simp]: "n \ 0 \ nat_of_natural n - Nat.Suc 0 < nat_of_natural n" - by (simp add: natural_eq_iff) + by transfer simp lemma natural_zero_minus_one: "(0::natural) - 1 = 0" @@ -786,26 +836,26 @@ lemma Suc_natural_minus_one: "Suc n - 1 = n" - by (simp add: natural_eq_iff) + by transfer simp hide_const (open) Suc subsection {* Code refinement for target language naturals *} -definition Nat :: "integer \ natural" -where - "Nat = natural_of_integer" +lift_definition Nat :: "integer \ natural" + is nat + . lemma [code_post]: "Nat 0 = 0" "Nat 1 = 1" "Nat (numeral k) = numeral k" - by (simp_all add: Nat_def nat_of_integer_def natural_of_integer_def) + by (transfer, simp)+ lemma [code abstype]: "Nat (integer_of_natural n) = n" - by (unfold Nat_def) (fact natural_of_integer_of_natural) + by transfer simp lemma [code abstract]: "integer_of_natural (natural_of_nat n) = of_nat n" @@ -817,23 +867,23 @@ lemma [code_abbrev]: "natural_of_integer (Code_Numeral_Types.Pos k) = numeral k" - by (simp add: nat_of_integer_def natural_of_integer_def) + by transfer simp lemma [code abstract]: "integer_of_natural 0 = 0" - by (simp add: integer_eq_iff) + by transfer simp lemma [code abstract]: "integer_of_natural 1 = 1" - by (simp add: integer_eq_iff) + by transfer simp lemma [code abstract]: "integer_of_natural (Code_Numeral_Types.Suc n) = integer_of_natural n + 1" - by (simp add: integer_eq_iff) + by transfer simp lemma [code]: "nat_of_natural = nat_of_integer \ integer_of_natural" - by (simp add: integer_of_natural_def fun_eq_iff) + by transfer (simp add: fun_eq_iff) lemma [code, code_unfold]: "natural_case f g n = (if n = 0 then f else g (n - 1))" @@ -843,39 +893,39 @@ lemma [code abstract]: "integer_of_natural (m + n) = integer_of_natural m + integer_of_natural n" - by (simp add: integer_eq_iff) + by transfer simp lemma [code abstract]: "integer_of_natural (m - n) = max 0 (integer_of_natural m - integer_of_natural n)" - by (simp add: integer_eq_iff) + by transfer simp lemma [code abstract]: "integer_of_natural (m * n) = integer_of_natural m * integer_of_natural n" - by (simp add: integer_eq_iff of_nat_mult) + by transfer (simp add: of_nat_mult) lemma [code abstract]: "integer_of_natural (m div n) = integer_of_natural m div integer_of_natural n" - by (simp add: integer_eq_iff zdiv_int) + by transfer (simp add: zdiv_int) lemma [code abstract]: "integer_of_natural (m mod n) = integer_of_natural m mod integer_of_natural n" - by (simp add: integer_eq_iff zmod_int) + by transfer (simp add: zmod_int) lemma [code]: "HOL.equal m n \ HOL.equal (integer_of_natural m) (integer_of_natural n)" - by (simp add: equal natural_eq_iff integer_eq_iff) + by transfer (simp add: equal) lemma [code nbe]: "HOL.equal n (n::natural) \ True" by (simp add: equal) lemma [code]: - "m \ n \ (integer_of_natural m) \ integer_of_natural n" - by (simp add: less_eq_natural_def less_eq_integer_def) + "m \ n \ integer_of_natural m \ integer_of_natural n" + by transfer simp lemma [code]: - "m < n \ (integer_of_natural m) < integer_of_natural n" - by (simp add: less_natural_def less_integer_def) + "m < n \ integer_of_natural m < integer_of_natural n" + by transfer simp hide_const (open) Nat diff -r 386a117925db -r e51e76ffaedd src/HOL/Library/Code_Target_Int.thy --- a/src/HOL/Library/Code_Target_Int.thy Thu Feb 14 16:36:21 2013 +0100 +++ b/src/HOL/Library/Code_Target_Int.thy Thu Feb 14 17:06:15 2013 +0100 @@ -15,47 +15,47 @@ lemma [code]: "integer_of_int (int_of_integer k) = k" - by (simp add: integer_eq_iff) + by transfer rule lemma [code]: "Int.Pos = int_of_integer \ integer_of_num" - by (simp add: integer_of_num_def fun_eq_iff) + by transfer (simp add: fun_eq_iff) lemma [code]: "Int.Neg = int_of_integer \ uminus \ integer_of_num" - by (simp add: integer_of_num_def fun_eq_iff) + by transfer (simp add: fun_eq_iff) lemma [code_abbrev]: "int_of_integer (numeral k) = Int.Pos k" - by simp + by transfer simp lemma [code_abbrev]: "int_of_integer (neg_numeral k) = Int.Neg k" - by simp + by transfer simp lemma [code, symmetric, code_post]: "0 = int_of_integer 0" - by simp + by transfer simp lemma [code, symmetric, code_post]: "1 = int_of_integer 1" - by simp + by transfer simp lemma [code]: "k + l = int_of_integer (of_int k + of_int l)" - by simp + by transfer simp lemma [code]: "- k = int_of_integer (- of_int k)" - by simp + by transfer simp lemma [code]: "k - l = int_of_integer (of_int k - of_int l)" - by simp + by transfer simp lemma [code]: "Int.dup k = int_of_integer (Code_Numeral_Types.dup (of_int k))" - by simp + by transfer simp lemma [code, code del]: "Int.sub = Int.sub" .. @@ -79,15 +79,15 @@ lemma [code]: "HOL.equal k l = HOL.equal (of_int k :: integer) (of_int l)" - by (simp add: equal integer_eq_iff) + by transfer (simp add: equal) lemma [code]: "k \ l \ (of_int k :: integer) \ of_int l" - by (simp add: less_eq_int_def) + by transfer rule lemma [code]: "k < l \ (of_int k :: integer) < of_int l" - by (simp add: less_int_def) + by transfer rule lemma (in ring_1) of_int_code: "of_int k = (if k = 0 then 0 @@ -107,7 +107,7 @@ lemma [code]: "nat = nat_of_integer \ of_int" - by (simp add: fun_eq_iff nat_of_integer_def) + by transfer (simp add: fun_eq_iff) code_modulename SML Code_Target_Int Arith diff -r 386a117925db -r e51e76ffaedd src/HOL/Library/Code_Target_Nat.thy --- a/src/HOL/Library/Code_Target_Nat.thy Thu Feb 14 16:36:21 2013 +0100 +++ b/src/HOL/Library/Code_Target_Nat.thy Thu Feb 14 17:06:15 2013 +0100 @@ -1,83 +1,80 @@ (* Title: HOL/Library/Code_Target_Nat.thy - Author: Stefan Berghofer, Florian Haftmann, TU Muenchen + Author: Florian Haftmann, TU Muenchen *) header {* Implementation of natural numbers by target-language integers *} theory Code_Target_Nat -imports Main Code_Numeral_Types Code_Binary_Nat +imports Code_Abstract_Nat Code_Numeral_Types begin subsection {* Implementation for @{typ nat} *} -definition Nat :: "integer \ nat" -where - "Nat = nat_of_integer" +lift_definition Nat :: "integer \ nat" + is nat + . lemma [code_post]: "Nat 0 = 0" "Nat 1 = 1" "Nat (numeral k) = numeral k" - by (simp_all add: Nat_def nat_of_integer_def) + by (transfer, simp)+ lemma [code_abbrev]: "integer_of_nat = of_nat" - by (fact integer_of_nat_def) + by transfer rule lemma [code_unfold]: "Int.nat (int_of_integer k) = nat_of_integer k" - by (simp add: nat_of_integer_def) + by transfer rule lemma [code abstype]: "Code_Target_Nat.Nat (integer_of_nat n) = n" - by (simp add: Nat_def integer_of_nat_def) + by transfer simp lemma [code abstract]: "integer_of_nat (nat_of_integer k) = max 0 k" - by (simp add: integer_of_nat_def) + by transfer auto lemma [code_abbrev]: "nat_of_integer (numeral k) = nat_of_num k" - by (simp add: nat_of_integer_def nat_of_num_numeral) + by transfer (simp add: nat_of_num_numeral) lemma [code abstract]: "integer_of_nat (nat_of_num n) = integer_of_num n" - by (simp add: integer_eq_iff integer_of_num_def nat_of_num_numeral) + by transfer (simp add: nat_of_num_numeral) lemma [code abstract]: "integer_of_nat 0 = 0" - by (simp add: integer_eq_iff integer_of_nat_def) + by transfer simp lemma [code abstract]: "integer_of_nat 1 = 1" - by (simp add: integer_eq_iff integer_of_nat_def) + by transfer simp + +lemma [code]: + "Suc n = n + 1" + by simp lemma [code abstract]: "integer_of_nat (m + n) = of_nat m + of_nat n" - by (simp add: integer_eq_iff integer_of_nat_def) - -lemma [code abstract]: - "integer_of_nat (Code_Binary_Nat.dup n) = Code_Numeral_Types.dup (of_nat n)" - by (simp add: integer_eq_iff Code_Binary_Nat.dup_def integer_of_nat_def) - -lemma [code, code del]: - "Code_Binary_Nat.sub = Code_Binary_Nat.sub" .. + by transfer simp lemma [code abstract]: "integer_of_nat (m - n) = max 0 (of_nat m - of_nat n)" - by (simp add: integer_eq_iff integer_of_nat_def) + by transfer simp lemma [code abstract]: "integer_of_nat (m * n) = of_nat m * of_nat n" - by (simp add: integer_eq_iff of_nat_mult integer_of_nat_def) + by transfer (simp add: of_nat_mult) lemma [code abstract]: "integer_of_nat (m div n) = of_nat m div of_nat n" - by (simp add: integer_eq_iff zdiv_int integer_of_nat_def) + by transfer (simp add: zdiv_int) lemma [code abstract]: "integer_of_nat (m mod n) = of_nat m mod of_nat n" - by (simp add: integer_eq_iff zmod_int integer_of_nat_def) + by transfer (simp add: zmod_int) lemma [code]: "Divides.divmod_nat m n = (m div n, m mod n)" @@ -85,7 +82,7 @@ lemma [code]: "HOL.equal m n = HOL.equal (of_nat m :: integer) (of_nat n)" - by (simp add: equal integer_eq_iff) + by transfer (simp add: equal) lemma [code]: "m \ n \ (of_nat m :: integer) \ of_nat n" @@ -97,7 +94,7 @@ lemma num_of_nat_code [code]: "num_of_nat = num_of_integer \ of_nat" - by (simp add: fun_eq_iff num_of_integer_def integer_of_nat_def) + by transfer (simp add: fun_eq_iff) lemma (in semiring_1) of_nat_code: "of_nat n = (if n = 0 then 0 @@ -124,7 +121,7 @@ lemma [code abstract]: "integer_of_nat (nat k) = max 0 (integer_of_int k)" - by (simp add: integer_of_nat_def of_int_of_nat max_def) + by transfer auto code_modulename SML Code_Target_Nat Arith diff -r 386a117925db -r e51e76ffaedd src/HOL/Library/Finite_Lattice.thy --- a/src/HOL/Library/Finite_Lattice.thy Thu Feb 14 16:36:21 2013 +0100 +++ b/src/HOL/Library/Finite_Lattice.thy Thu Feb 14 17:06:15 2013 +0100 @@ -1,7 +1,7 @@ (* Author: Alessandro Coglio *) theory Finite_Lattice -imports Product_Lattice +imports Product_Order begin text {* A non-empty finite lattice is a complete lattice. diff -r 386a117925db -r e51e76ffaedd src/HOL/Library/Product_Lattice.thy --- a/src/HOL/Library/Product_Lattice.thy Thu Feb 14 16:36:21 2013 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,238 +0,0 @@ -(* Title: HOL/Library/Product_Lattice.thy - Author: Brian Huffman -*) - -header {* Lattice operations on product types *} - -theory Product_Lattice -imports "~~/src/HOL/Library/Product_plus" -begin - -subsection {* Pointwise ordering *} - -instantiation prod :: (ord, ord) ord -begin - -definition - "x \ y \ fst x \ fst y \ snd x \ snd y" - -definition - "(x::'a \ 'b) < y \ x \ y \ \ y \ x" - -instance .. - -end - -lemma fst_mono: "x \ y \ fst x \ fst y" - unfolding less_eq_prod_def by simp - -lemma snd_mono: "x \ y \ snd x \ snd y" - unfolding less_eq_prod_def by simp - -lemma Pair_mono: "x \ x' \ y \ y' \ (x, y) \ (x', y')" - unfolding less_eq_prod_def by simp - -lemma Pair_le [simp]: "(a, b) \ (c, d) \ a \ c \ b \ d" - unfolding less_eq_prod_def by simp - -instance prod :: (preorder, preorder) preorder -proof - fix x y z :: "'a \ 'b" - show "x < y \ x \ y \ \ y \ x" - by (rule less_prod_def) - show "x \ x" - unfolding less_eq_prod_def - by fast - assume "x \ y" and "y \ z" thus "x \ z" - unfolding less_eq_prod_def - by (fast elim: order_trans) -qed - -instance prod :: (order, order) order - by default auto - - -subsection {* Binary infimum and supremum *} - -instantiation prod :: (semilattice_inf, semilattice_inf) semilattice_inf -begin - -definition - "inf x y = (inf (fst x) (fst y), inf (snd x) (snd y))" - -lemma inf_Pair_Pair [simp]: "inf (a, b) (c, d) = (inf a c, inf b d)" - unfolding inf_prod_def by simp - -lemma fst_inf [simp]: "fst (inf x y) = inf (fst x) (fst y)" - unfolding inf_prod_def by simp - -lemma snd_inf [simp]: "snd (inf x y) = inf (snd x) (snd y)" - unfolding inf_prod_def by simp - -instance - by default auto - -end - -instantiation prod :: (semilattice_sup, semilattice_sup) semilattice_sup -begin - -definition - "sup x y = (sup (fst x) (fst y), sup (snd x) (snd y))" - -lemma sup_Pair_Pair [simp]: "sup (a, b) (c, d) = (sup a c, sup b d)" - unfolding sup_prod_def by simp - -lemma fst_sup [simp]: "fst (sup x y) = sup (fst x) (fst y)" - unfolding sup_prod_def by simp - -lemma snd_sup [simp]: "snd (sup x y) = sup (snd x) (snd y)" - unfolding sup_prod_def by simp - -instance - by default auto - -end - -instance prod :: (lattice, lattice) lattice .. - -instance prod :: (distrib_lattice, distrib_lattice) distrib_lattice - by default (auto simp add: sup_inf_distrib1) - - -subsection {* Top and bottom elements *} - -instantiation prod :: (top, top) top -begin - -definition - "top = (top, top)" - -lemma fst_top [simp]: "fst top = top" - unfolding top_prod_def by simp - -lemma snd_top [simp]: "snd top = top" - unfolding top_prod_def by simp - -lemma Pair_top_top: "(top, top) = top" - unfolding top_prod_def by simp - -instance - by default (auto simp add: top_prod_def) - -end - -instantiation prod :: (bot, bot) bot -begin - -definition - "bot = (bot, bot)" - -lemma fst_bot [simp]: "fst bot = bot" - unfolding bot_prod_def by simp - -lemma snd_bot [simp]: "snd bot = bot" - unfolding bot_prod_def by simp - -lemma Pair_bot_bot: "(bot, bot) = bot" - unfolding bot_prod_def by simp - -instance - by default (auto simp add: bot_prod_def) - -end - -instance prod :: (bounded_lattice, bounded_lattice) bounded_lattice .. - -instance prod :: (boolean_algebra, boolean_algebra) boolean_algebra - by default (auto simp add: prod_eqI inf_compl_bot sup_compl_top diff_eq) - - -subsection {* Complete lattice operations *} - -instantiation prod :: (complete_lattice, complete_lattice) complete_lattice -begin - -definition - "Sup A = (SUP x:A. fst x, SUP x:A. snd x)" - -definition - "Inf A = (INF x:A. fst x, INF x:A. snd x)" - -instance - by default (simp_all add: less_eq_prod_def Inf_prod_def Sup_prod_def - INF_lower SUP_upper le_INF_iff SUP_le_iff) - -end - -lemma fst_Sup: "fst (Sup A) = (SUP x:A. fst x)" - unfolding Sup_prod_def by simp - -lemma snd_Sup: "snd (Sup A) = (SUP x:A. snd x)" - unfolding Sup_prod_def by simp - -lemma fst_Inf: "fst (Inf A) = (INF x:A. fst x)" - unfolding Inf_prod_def by simp - -lemma snd_Inf: "snd (Inf A) = (INF x:A. snd x)" - unfolding Inf_prod_def by simp - -lemma fst_SUP: "fst (SUP x:A. f x) = (SUP x:A. fst (f x))" - by (simp add: SUP_def fst_Sup image_image) - -lemma snd_SUP: "snd (SUP x:A. f x) = (SUP x:A. snd (f x))" - by (simp add: SUP_def snd_Sup image_image) - -lemma fst_INF: "fst (INF x:A. f x) = (INF x:A. fst (f x))" - by (simp add: INF_def fst_Inf image_image) - -lemma snd_INF: "snd (INF x:A. f x) = (INF x:A. snd (f x))" - by (simp add: INF_def snd_Inf image_image) - -lemma SUP_Pair: "(SUP x:A. (f x, g x)) = (SUP x:A. f x, SUP x:A. g x)" - by (simp add: SUP_def Sup_prod_def image_image) - -lemma INF_Pair: "(INF x:A. (f x, g x)) = (INF x:A. f x, INF x:A. g x)" - by (simp add: INF_def Inf_prod_def image_image) - - -text {* Alternative formulations for set infima and suprema over the product -of two complete lattices: *} - -lemma Inf_prod_alt_def: "Inf A = (Inf (fst ` A), Inf (snd ` A))" -by (auto simp: Inf_prod_def INF_def) - -lemma Sup_prod_alt_def: "Sup A = (Sup (fst ` A), Sup (snd ` A))" -by (auto simp: Sup_prod_def SUP_def) - -lemma INFI_prod_alt_def: "INFI A f = (INFI A (fst o f), INFI A (snd o f))" -by (auto simp: INF_def Inf_prod_def image_compose) - -lemma SUPR_prod_alt_def: "SUPR A f = (SUPR A (fst o f), SUPR A (snd o f))" -by (auto simp: SUP_def Sup_prod_def image_compose) - -lemma INF_prod_alt_def: - "(INF x:A. f x) = (INF x:A. fst (f x), INF x:A. snd (f x))" -by (metis fst_INF snd_INF surjective_pairing) - -lemma SUP_prod_alt_def: - "(SUP x:A. f x) = (SUP x:A. fst (f x), SUP x:A. snd (f x))" -by (metis fst_SUP snd_SUP surjective_pairing) - - -subsection {* Complete distributive lattices *} - -(* Contribution: Alessandro Coglio *) - -instance prod :: - (complete_distrib_lattice, complete_distrib_lattice) complete_distrib_lattice -proof - case goal1 thus ?case - by (auto simp: sup_prod_def Inf_prod_def INF_prod_alt_def sup_Inf sup_INF) -next - case goal2 thus ?case - by (auto simp: inf_prod_def Sup_prod_def SUP_prod_alt_def inf_Sup inf_SUP) -qed - - -end diff -r 386a117925db -r e51e76ffaedd src/HOL/Library/Product_Lexorder.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/Product_Lexorder.thy Thu Feb 14 17:06:15 2013 +0100 @@ -0,0 +1,125 @@ +(* Title: HOL/Library/Product_Lexorder.thy + Author: Norbert Voelker +*) + +header {* Lexicographic order on product types *} + +theory Product_Lexorder +imports Main +begin + +instantiation prod :: (ord, ord) ord +begin + +definition + "x \ y \ fst x < fst y \ fst x \ fst y \ snd x \ snd y" + +definition + "x < y \ fst x < fst y \ fst x \ fst y \ snd x < snd y" + +instance .. + +end + +lemma less_eq_prod_simp [simp, code]: + "(x1, y1) \ (x2, y2) \ x1 < x2 \ x1 \ x2 \ y1 \ y2" + by (simp add: less_eq_prod_def) + +lemma less_prod_simp [simp, code]: + "(x1, y1) < (x2, y2) \ x1 < x2 \ x1 \ x2 \ y1 < y2" + by (simp add: less_prod_def) + +text {* A stronger version for partial orders. *} + +lemma less_prod_def': + fixes x y :: "'a::order \ 'b::ord" + shows "x < y \ fst x < fst y \ fst x = fst y \