# HG changeset patch # User haftmann # Date 1184874459 -7200 # Node ID 688a8a7bcd4ed7684189e631104c57f219654e9d # Parent 2c69bb1374b8213d326c54c2082f7abb82f064f0 uniform naming conventions for CG theories diff -r 2c69bb1374b8 -r 688a8a7bcd4e src/HOL/Complex/ex/ReflectedFerrack.thy --- a/src/HOL/Complex/ex/ReflectedFerrack.thy Thu Jul 19 21:47:38 2007 +0200 +++ b/src/HOL/Complex/ex/ReflectedFerrack.thy Thu Jul 19 21:47:39 2007 +0200 @@ -5,7 +5,7 @@ header {* Quatifier elimination for R(0,1,+,<) *} theory ReflectedFerrack - imports GCD Real EfficientNat + imports GCD Real Efficient_Nat uses ("linreif.ML") ("linrtac.ML") begin diff -r 2c69bb1374b8 -r 688a8a7bcd4e src/HOL/Extraction/Pigeonhole.thy --- a/src/HOL/Extraction/Pigeonhole.thy Thu Jul 19 21:47:38 2007 +0200 +++ b/src/HOL/Extraction/Pigeonhole.thy Thu Jul 19 21:47:39 2007 +0200 @@ -6,7 +6,7 @@ header {* The pigeonhole principle *} theory Pigeonhole -imports EfficientNat +imports Efficient_Nat begin text {* diff -r 2c69bb1374b8 -r 688a8a7bcd4e src/HOL/Extraction/ROOT.ML --- a/src/HOL/Extraction/ROOT.ML Thu Jul 19 21:47:38 2007 +0200 +++ b/src/HOL/Extraction/ROOT.ML Thu Jul 19 21:47:39 2007 +0200 @@ -11,5 +11,5 @@ time_use_thy "QuotRem"; time_use_thy "Warshall"; time_use_thy "Higman"; - no_document time_use_thy "EfficientNat"; + no_document time_use_thy "Efficient_Nat"; time_use_thy "Pigeonhole"); diff -r 2c69bb1374b8 -r 688a8a7bcd4e src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Thu Jul 19 21:47:38 2007 +0200 +++ b/src/HOL/IsaMakefile Thu Jul 19 21:47:39 2007 +0200 @@ -201,10 +201,9 @@ $(LOG)/HOL-Library.gz: $(OUT)/HOL \ Library/SetsAndFunctions.thy Library/BigO.thy Library/Ramsey.thy \ - Library/EfficientNat.thy Library/ExecutableSet.thy \ - Library/ExecutableRat.thy \ - Library/Executable_Real.thy \ - Library/MLString.thy Library/Infinite_Set.thy \ + Library/Efficient_Nat.thy Library/Executable_Set.thy \ + Library/Executable_Rat.thy Library/Executable_Real.thy \ + Library/ML_Int.thy Library/ML_String.thy Library/Infinite_Set.thy \ Library/FuncSet.thy Library/Library.thy \ Library/List_Prefix.thy Library/State_Monad.thy Library/Multiset.thy \ Library/NatPair.thy \ @@ -538,7 +537,7 @@ HOL-MicroJava: HOL $(LOG)/HOL-MicroJava.gz -$(LOG)/HOL-MicroJava.gz: $(OUT)/HOL Library/ExecutableSet.thy \ +$(LOG)/HOL-MicroJava.gz: $(OUT)/HOL Library/Executable_Set.thy \ MicroJava/ROOT.ML \ MicroJava/Comp/AuxLemmas.thy \ MicroJava/Comp/CorrComp.thy \ @@ -604,7 +603,7 @@ HOL-Extraction: HOL $(LOG)/HOL-Extraction.gz -$(LOG)/HOL-Extraction.gz: $(OUT)/HOL Library/EfficientNat.thy \ +$(LOG)/HOL-Extraction.gz: $(OUT)/HOL Library/Efficient_Nat.thy \ Extraction/Higman.thy Extraction/ROOT.ML Extraction/Pigeonhole.thy \ Extraction/QuotRem.thy \ Extraction/Warshall.thy Extraction/document/root.tex \ diff -r 2c69bb1374b8 -r 688a8a7bcd4e src/HOL/Library/EfficientNat.thy --- a/src/HOL/Library/EfficientNat.thy Thu Jul 19 21:47:38 2007 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,407 +0,0 @@ -(* Title: HOL/Library/EfficientNat.thy - ID: $Id$ - Author: Stefan Berghofer, TU Muenchen -*) - -header {* Implementation of natural numbers by integers *} - -theory EfficientNat -imports Main Pretty_Int -begin - -text {* -When generating code for functions on natural numbers, the canonical -representation using @{term "0::nat"} and @{term "Suc"} is unsuitable for -computations involving large numbers. The efficiency of the generated -code can be improved drastically by implementing natural numbers by -integers. To do this, just include this theory. -*} - -subsection {* Logical rewrites *} - -text {* - An int-to-nat conversion - restricted to non-negative ints (in contrast to @{const nat}). - Note that this restriction has no logical relevance and - is just a kind of proof hint -- nothing prevents you from - writing nonsense like @{term "nat_of_int (-4)"} -*} - -definition - nat_of_int :: "int \ nat" where - "k \ 0 \ nat_of_int k = nat k" - -definition - int' :: "nat \ int" where - "int' n = of_nat n" - -lemma int'_Suc [simp]: "int' (Suc n) = 1 + int' n" -unfolding int'_def by simp - -lemma int'_add: "int' (m + n) = int' m + int' n" -unfolding int'_def by (rule of_nat_add) - -lemma int'_mult: "int' (m * n) = int' m * int' n" -unfolding int'_def by (rule of_nat_mult) - -lemma nat_of_int_of_number_of: - fixes k - assumes "k \ 0" - shows "number_of k = nat_of_int (number_of k)" - unfolding nat_of_int_def [OF assms] nat_number_of_def number_of_is_id .. - -lemma nat_of_int_of_number_of_aux: - fixes k - assumes "Numeral.Pls \ k \ True" - shows "k \ 0" - using assms unfolding Pls_def by simp - -lemma nat_of_int_int: - "nat_of_int (int' n) = n" - using nat_of_int_def int'_def by simp - -lemma eq_nat_of_int: "int' n = x \ n = nat_of_int x" -by (erule subst, simp only: nat_of_int_int) - -text {* - Case analysis on natural numbers is rephrased using a conditional - expression: -*} - -lemma [code unfold, code inline del]: - "nat_case \ (\f g n. if n = 0 then f else g (n - 1))" -proof - - have rewrite: "\f g n. nat_case f g n = (if n = 0 then f else g (n - 1))" - proof - - fix f g n - show "nat_case f g n = (if n = 0 then f else g (n - 1))" - by (cases n) simp_all - qed - show "nat_case \ (\f g n. if n = 0 then f else g (n - 1))" - by (rule eq_reflection ext rewrite)+ -qed - -lemma [code inline]: - "nat_case = (\f g n. if n = 0 then f else g (nat_of_int (int' n - 1)))" -proof (rule ext)+ - fix f g n - show "nat_case f g n = (if n = 0 then f else g (nat_of_int (int' n - 1)))" - by (cases n) (simp_all add: nat_of_int_int) -qed - -text {* - Most standard arithmetic functions on natural numbers are implemented - using their counterparts on the integers: -*} - -lemma [code func]: "0 = nat_of_int 0" - by (simp add: nat_of_int_def) -lemma [code func, code inline]: "1 = nat_of_int 1" - by (simp add: nat_of_int_def) -lemma [code func]: "Suc n = nat_of_int (int' n + 1)" - by (simp add: eq_nat_of_int) -lemma [code]: "m + n = nat (int' m + int' n)" - by (simp add: int'_def nat_eq_iff2) -lemma [code func, code inline]: "m + n = nat_of_int (int' m + int' n)" - by (simp add: eq_nat_of_int int'_add) -lemma [code, code inline]: "m - n = nat (int' m - int' n)" - by (simp add: int'_def nat_eq_iff2 of_nat_diff) -lemma [code]: "m * n = nat (int' m * int' n)" - unfolding int'_def - by (simp add: of_nat_mult [symmetric] del: of_nat_mult) -lemma [code func, code inline]: "m * n = nat_of_int (int' m * int' n)" - by (simp add: eq_nat_of_int int'_mult) -lemma [code]: "m div n = nat (int' m div int' n)" - unfolding int'_def zdiv_int [symmetric] by simp -lemma [code func]: "m div n = fst (Divides.divmod m n)" - unfolding divmod_def by simp -lemma [code]: "m mod n = nat (int' m mod int' n)" - unfolding int'_def zmod_int [symmetric] by simp -lemma [code func]: "m mod n = snd (Divides.divmod m n)" - unfolding divmod_def by simp -lemma [code, code inline]: "(m < n) \ (int' m < int' n)" - unfolding int'_def by simp -lemma [code func, code inline]: "(m \ n) \ (int' m \ int' n)" - unfolding int'_def by simp -lemma [code func, code inline]: "m = n \ int' m = int' n" - unfolding int'_def by simp -lemma [code func]: "nat k = (if k < 0 then 0 else nat_of_int k)" -proof (cases "k < 0") - case True then show ?thesis by simp -next - case False then show ?thesis by (simp add: nat_of_int_def) -qed -lemma [code func]: - "int_aux i n = (if int' n = 0 then i else int_aux (i + 1) (nat_of_int (int' n - 1)))" -proof - - have "0 < n \ int' n = 1 + int' (nat_of_int (int' n - 1))" - proof - - assume prem: "n > 0" - then have "int' n - 1 \ 0" unfolding int'_def by auto - then have "nat_of_int (int' n - 1) = nat (int' n - 1)" by (simp add: nat_of_int_def) - with prem show "int' n = 1 + int' (nat_of_int (int' n - 1))" unfolding int'_def by simp - qed - then show ?thesis unfolding int_aux_def int'_def by simp -qed - -lemma div_nat_code [code func]: - "m div k = nat_of_int (fst (divAlg (int' m, int' k)))" - unfolding div_def [symmetric] int'_def zdiv_int [symmetric] - unfolding int'_def [symmetric] nat_of_int_int .. - -lemma mod_nat_code [code func]: - "m mod k = nat_of_int (snd (divAlg (int' m, int' k)))" - unfolding mod_def [symmetric] int'_def zmod_int [symmetric] - unfolding int'_def [symmetric] nat_of_int_int .. - -subsection {* Code generator setup for basic functions *} - -text {* - @{typ nat} is no longer a datatype but embedded into the integers. -*} - -code_datatype nat_of_int - -code_type nat - (SML "IntInf.int") - (OCaml "Big'_int.big'_int") - (Haskell "Integer") - -types_code - nat ("int") -attach (term_of) {* -val term_of_nat = HOLogic.mk_number HOLogic.natT o IntInf.fromInt; -*} -attach (test) {* -fun gen_nat i = random_range 0 i; -*} - -consts_code - "0 \ nat" ("0") - Suc ("(_ + 1)") - -text {* - Since natural numbers are implemented - using integers, the coercion function @{const "int"} of type - @{typ "nat \ int"} is simply implemented by the identity function, - likewise @{const nat_of_int} of type @{typ "int \ nat"}. - For the @{const "nat"} function for converting an integer to a natural - number, we give a specific implementation using an ML function that - returns its input value, provided that it is non-negative, and otherwise - returns @{text "0"}. -*} - -consts_code - int' ("(_)") - nat ("\nat") -attach {* -fun nat i = if i < 0 then 0 else i; -*} - -code_const int' - (SML "_") - (OCaml "_") - (Haskell "_") - -code_const nat_of_int - (SML "_") - (OCaml "_") - (Haskell "_") - - -subsection {* Preprocessors *} - -text {* - Natural numerals should be expressed using @{const nat_of_int}. -*} - -lemmas [code inline del] = nat_number_of_def - -ML {* -fun nat_of_int_of_number_of thy cts = - let - val simplify_less = Simplifier.rewrite - (HOL_basic_ss addsimps (@{thms less_numeral_code} @ @{thms less_eq_numeral_code})); - fun mk_rew (t, ty) = - if ty = HOLogic.natT andalso IntInf.<= (0, HOLogic.dest_numeral t) then - Thm.capply @{cterm "(op \) Numeral.Pls"} (Thm.cterm_of thy t) - |> simplify_less - |> (fn thm => @{thm nat_of_int_of_number_of_aux} OF [thm]) - |> (fn thm => @{thm nat_of_int_of_number_of} OF [thm]) - |> (fn thm => @{thm eq_reflection} OF [thm]) - |> SOME - else NONE - in - fold (HOLogic.add_numerals o Thm.term_of) cts [] - |> map_filter mk_rew - end; -*} - -setup {* - CodegenData.add_inline_proc ("nat_of_int_of_number_of", nat_of_int_of_number_of) -*} - -text {* - In contrast to @{term "Suc n"}, the term @{term "n + (1::nat)"} is no longer - a constructor term. 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 or in the arguments of an inductive relation in an introduction - rule) must be eliminated. - This can be accomplished by applying the following transformation rules: -*} - -theorem Suc_if_eq: "(\n. f (Suc n) = h n) \ f 0 = g \ - f n = (if n = 0 then g else h (n - 1))" - by (case_tac n) simp_all - -theorem Suc_clause: "(\n. P n (Suc n)) \ n \ 0 \ P (n - 1) n" - by (case_tac 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. -*} - -(*<*) - -ML {* -local - val Suc_if_eq = thm "Suc_if_eq"; - val Suc_clause = thm "Suc_clause"; - fun contains_suc t = member (op =) (term_consts t) "Suc"; -in - -fun remove_suc thy thms = - let - val Suc_if_eq' = Thm.transfer thy Suc_if_eq; - val vname = Name.variant (map fst - (fold (Term.add_varnames o Thm.full_prop_of) thms [])) "x"; - val cv = cterm_of thy (Var ((vname, 0), HOLogic.natT)); - fun lhs_of th = snd (Thm.dest_comb - (fst (Thm.dest_comb (snd (Thm.dest_comb (cprop_of th)))))); - fun rhs_of th = snd (Thm.dest_comb (snd (Thm.dest_comb (cprop_of th)))); - fun find_vars ct = (case term_of ct of - (Const ("Suc", _) $ Var _) => [(cv, snd (Thm.dest_comb ct))] - | _ $ _ => - let val (ct1, ct2) = Thm.dest_comb ct - in - map (apfst (fn ct => Thm.capply ct ct2)) (find_vars ct1) @ - map (apfst (Thm.capply 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.cabs cv ct), - SOME (Thm.cabs cv' (rhs_of th)), NONE, SOME cv'] - 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.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 - case get_first mk_thms eqs of - NONE => thms - | SOME x => remove_suc thy x - end; - -fun eqn_suc_preproc thy ths = - let - val dest = fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of - in - if forall (can dest) ths andalso - exists (contains_suc o dest) ths - then remove_suc thy ths else ths - end; - -fun remove_suc_clause thy thms = - let - val Suc_clause' = Thm.transfer thy Suc_clause; - val vname = Name.variant (map fst - (fold (Term.add_varnames o Thm.full_prop_of) thms [])) "x"; - fun find_var (t as Const ("Suc", _) $ (v as Var _)) = SOME (t, v) - | find_var (t $ u) = (case find_var t of NONE => find_var u | x => x) - | find_var _ = NONE; - fun find_thm th = - let val th' = Conv.fconv_rule ObjectLogic.atomize th - in Option.map (pair (th, th')) (find_var (prop_of th')) end - in - case get_first find_thm thms of - NONE => thms - | SOME ((th, th'), (Sucv, v)) => - let - val cert = cterm_of (Thm.theory_of_thm th); - val th'' = ObjectLogic.rulify (Thm.implies_elim - (Conv.fconv_rule (Thm.beta_conversion true) - (Drule.instantiate' [] - [SOME (cert (lambda v (Abs ("x", HOLogic.natT, - abstract_over (Sucv, - HOLogic.dest_Trueprop (prop_of th')))))), - SOME (cert v)] Suc_clause')) - (Thm.forall_intr (cert v) th')) - in - remove_suc_clause thy (map (fn th''' => - if (op = o pairself prop_of) (th''', th) then th'' else th''') thms) - end - end; - -fun clause_suc_preproc thy ths = - let - val dest = fst o HOLogic.dest_mem o HOLogic.dest_Trueprop - in - if forall (can (dest o concl_of)) ths andalso - exists (fn th => member (op =) (foldr add_term_consts - [] (map_filter (try dest) (concl_of th :: prems_of th))) "Suc") ths - then remove_suc_clause thy ths else ths - end; - -end; (*local*) - -fun lift_obj_eq f thy = - map (fn thm => thm RS @{thm meta_eq_to_obj_eq}) - #> f thy - #> map (fn thm => thm RS @{thm eq_reflection}) - #> map (Conv.fconv_rule Drule.beta_eta_conversion) -*} - -setup {* - Codegen.add_preprocessor eqn_suc_preproc - #> Codegen.add_preprocessor clause_suc_preproc - #> CodegenData.add_preproc ("eqn_Suc", lift_obj_eq eqn_suc_preproc) - #> CodegenData.add_preproc ("clause_Suc", lift_obj_eq clause_suc_preproc) -*} -(*>*) - - -subsection {* Module names *} - -code_modulename SML - Nat Integer - Divides Integer - EfficientNat Integer - -code_modulename OCaml - Nat Integer - Divides Integer - EfficientNat Integer - -code_modulename Haskell - Nat Integer - EfficientNat Integer - -hide const nat_of_int int' - -end diff -r 2c69bb1374b8 -r 688a8a7bcd4e src/HOL/Library/Efficient_Nat.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/Efficient_Nat.thy Thu Jul 19 21:47:39 2007 +0200 @@ -0,0 +1,408 @@ +(* Title: HOL/Library/Efficient_Nat.thy + ID: $Id$ + Author: Stefan Berghofer, TU Muenchen +*) + +header {* Implementation of natural numbers by integers *} + +theory Efficient_Nat +imports Main Pretty_Int +begin + +text {* +When generating code for functions on natural numbers, the canonical +representation using @{term "0::nat"} and @{term "Suc"} is unsuitable for +computations involving large numbers. The efficiency of the generated +code can be improved drastically by implementing natural numbers by +integers. To do this, just include this theory. +*} + +subsection {* Logical rewrites *} + +text {* + An int-to-nat conversion + restricted to non-negative ints (in contrast to @{const nat}). + Note that this restriction has no logical relevance and + is just a kind of proof hint -- nothing prevents you from + writing nonsense like @{term "nat_of_int (-4)"} +*} + +definition + nat_of_int :: "int \ nat" where + "k \ 0 \ nat_of_int k = nat k" + +definition + int' :: "nat \ int" where + "int' n = of_nat n" + +lemma int'_Suc [simp]: "int' (Suc n) = 1 + int' n" +unfolding int'_def by simp + +lemma int'_add: "int' (m + n) = int' m + int' n" +unfolding int'_def by (rule of_nat_add) + +lemma int'_mult: "int' (m * n) = int' m * int' n" +unfolding int'_def by (rule of_nat_mult) + +lemma nat_of_int_of_number_of: + fixes k + assumes "k \ 0" + shows "number_of k = nat_of_int (number_of k)" + unfolding nat_of_int_def [OF assms] nat_number_of_def number_of_is_id .. + +lemma nat_of_int_of_number_of_aux: + fixes k + assumes "Numeral.Pls \ k \ True" + shows "k \ 0" + using assms unfolding Pls_def by simp + +lemma nat_of_int_int: + "nat_of_int (int' n) = n" + using nat_of_int_def int'_def by simp + +lemma eq_nat_of_int: "int' n = x \ n = nat_of_int x" +by (erule subst, simp only: nat_of_int_int) + +text {* + Case analysis on natural numbers is rephrased using a conditional + expression: +*} + +lemma [code unfold, code inline del]: + "nat_case \ (\f g n. if n = 0 then f else g (n - 1))" +proof - + have rewrite: "\f g n. nat_case f g n = (if n = 0 then f else g (n - 1))" + proof - + fix f g n + show "nat_case f g n = (if n = 0 then f else g (n - 1))" + by (cases n) simp_all + qed + show "nat_case \ (\f g n. if n = 0 then f else g (n - 1))" + by (rule eq_reflection ext rewrite)+ +qed + +lemma [code inline]: + "nat_case = (\f g n. if n = 0 then f else g (nat_of_int (int' n - 1)))" +proof (rule ext)+ + fix f g n + show "nat_case f g n = (if n = 0 then f else g (nat_of_int (int' n - 1)))" + by (cases n) (simp_all add: nat_of_int_int) +qed + +text {* + Most standard arithmetic functions on natural numbers are implemented + using their counterparts on the integers: +*} + +lemma [code func]: "0 = nat_of_int 0" + by (simp add: nat_of_int_def) +lemma [code func, code inline]: "1 = nat_of_int 1" + by (simp add: nat_of_int_def) +lemma [code func]: "Suc n = nat_of_int (int' n + 1)" + by (simp add: eq_nat_of_int) +lemma [code]: "m + n = nat (int' m + int' n)" + by (simp add: int'_def nat_eq_iff2) +lemma [code func, code inline]: "m + n = nat_of_int (int' m + int' n)" + by (simp add: eq_nat_of_int int'_add) +lemma [code, code inline]: "m - n = nat (int' m - int' n)" + by (simp add: int'_def nat_eq_iff2 of_nat_diff) +lemma [code]: "m * n = nat (int' m * int' n)" + unfolding int'_def + by (simp add: of_nat_mult [symmetric] del: of_nat_mult) +lemma [code func, code inline]: "m * n = nat_of_int (int' m * int' n)" + by (simp add: eq_nat_of_int int'_mult) +lemma [code]: "m div n = nat (int' m div int' n)" + unfolding int'_def zdiv_int [symmetric] by simp +lemma [code func]: "m div n = fst (Divides.divmod m n)" + unfolding divmod_def by simp +lemma [code]: "m mod n = nat (int' m mod int' n)" + unfolding int'_def zmod_int [symmetric] by simp +lemma [code func]: "m mod n = snd (Divides.divmod m n)" + unfolding divmod_def by simp +lemma [code, code inline]: "(m < n) \ (int' m < int' n)" + unfolding int'_def by simp +lemma [code func, code inline]: "(m \ n) \ (int' m \ int' n)" + unfolding int'_def by simp +lemma [code func, code inline]: "m = n \ int' m = int' n" + unfolding int'_def by simp +lemma [code func]: "nat k = (if k < 0 then 0 else nat_of_int k)" +proof (cases "k < 0") + case True then show ?thesis by simp +next + case False then show ?thesis by (simp add: nat_of_int_def) +qed +lemma [code func]: + "int_aux n i = (if int' n = 0 then i else int_aux (nat_of_int (int' n - 1)) (i + 1))" +proof - + have "0 < n \ int' n = 1 + int' (nat_of_int (int' n - 1))" + proof - + assume prem: "n > 0" + then have "int' n - 1 \ 0" unfolding int'_def by auto + then have "nat_of_int (int' n - 1) = nat (int' n - 1)" by (simp add: nat_of_int_def) + with prem show "int' n = 1 + int' (nat_of_int (int' n - 1))" unfolding int'_def by simp + qed + then show ?thesis unfolding int_aux_def int'_def by auto +qed + +lemma div_nat_code [code func]: + "m div k = nat_of_int (fst (divAlg (int' m, int' k)))" + unfolding div_def [symmetric] int'_def zdiv_int [symmetric] + unfolding int'_def [symmetric] nat_of_int_int .. + +lemma mod_nat_code [code func]: + "m mod k = nat_of_int (snd (divAlg (int' m, int' k)))" + unfolding mod_def [symmetric] int'_def zmod_int [symmetric] + unfolding int'_def [symmetric] nat_of_int_int .. + + +subsection {* Code generator setup for basic functions *} + +text {* + @{typ nat} is no longer a datatype but embedded into the integers. +*} + +code_datatype nat_of_int + +code_type nat + (SML "IntInf.int") + (OCaml "Big'_int.big'_int") + (Haskell "Integer") + +types_code + nat ("int") +attach (term_of) {* +val term_of_nat = HOLogic.mk_number HOLogic.natT o IntInf.fromInt; +*} +attach (test) {* +fun gen_nat i = random_range 0 i; +*} + +consts_code + "0 \ nat" ("0") + Suc ("(_ + 1)") + +text {* + Since natural numbers are implemented + using integers, the coercion function @{const "int"} of type + @{typ "nat \ int"} is simply implemented by the identity function, + likewise @{const nat_of_int} of type @{typ "int \ nat"}. + For the @{const "nat"} function for converting an integer to a natural + number, we give a specific implementation using an ML function that + returns its input value, provided that it is non-negative, and otherwise + returns @{text "0"}. +*} + +consts_code + int' ("(_)") + nat ("\nat") +attach {* +fun nat i = if i < 0 then 0 else i; +*} + +code_const int' + (SML "_") + (OCaml "_") + (Haskell "_") + +code_const nat_of_int + (SML "_") + (OCaml "_") + (Haskell "_") + + +subsection {* Preprocessors *} + +text {* + Natural numerals should be expressed using @{const nat_of_int}. +*} + +lemmas [code inline del] = nat_number_of_def + +ML {* +fun nat_of_int_of_number_of thy cts = + let + val simplify_less = Simplifier.rewrite + (HOL_basic_ss addsimps (@{thms less_numeral_code} @ @{thms less_eq_numeral_code})); + fun mk_rew (t, ty) = + if ty = HOLogic.natT andalso IntInf.<= (0, HOLogic.dest_numeral t) then + Thm.capply @{cterm "(op \) Numeral.Pls"} (Thm.cterm_of thy t) + |> simplify_less + |> (fn thm => @{thm nat_of_int_of_number_of_aux} OF [thm]) + |> (fn thm => @{thm nat_of_int_of_number_of} OF [thm]) + |> (fn thm => @{thm eq_reflection} OF [thm]) + |> SOME + else NONE + in + fold (HOLogic.add_numerals o Thm.term_of) cts [] + |> map_filter mk_rew + end; +*} + +setup {* + CodegenData.add_inline_proc ("nat_of_int_of_number_of", nat_of_int_of_number_of) +*} + +text {* + In contrast to @{term "Suc n"}, the term @{term "n + (1::nat)"} is no longer + a constructor term. 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 or in the arguments of an inductive relation in an introduction + rule) must be eliminated. + This can be accomplished by applying the following transformation rules: +*} + +theorem Suc_if_eq: "(\n. f (Suc n) = h n) \ f 0 = g \ + f n = (if n = 0 then g else h (n - 1))" + by (case_tac n) simp_all + +theorem Suc_clause: "(\n. P n (Suc n)) \ n \ 0 \ P (n - 1) n" + by (case_tac 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. +*} + +(*<*) + +ML {* +local + val Suc_if_eq = thm "Suc_if_eq"; + val Suc_clause = thm "Suc_clause"; + fun contains_suc t = member (op =) (term_consts t) "Suc"; +in + +fun remove_suc thy thms = + let + val Suc_if_eq' = Thm.transfer thy Suc_if_eq; + val vname = Name.variant (map fst + (fold (Term.add_varnames o Thm.full_prop_of) thms [])) "x"; + val cv = cterm_of thy (Var ((vname, 0), HOLogic.natT)); + fun lhs_of th = snd (Thm.dest_comb + (fst (Thm.dest_comb (snd (Thm.dest_comb (cprop_of th)))))); + fun rhs_of th = snd (Thm.dest_comb (snd (Thm.dest_comb (cprop_of th)))); + fun find_vars ct = (case term_of ct of + (Const ("Suc", _) $ Var _) => [(cv, snd (Thm.dest_comb ct))] + | _ $ _ => + let val (ct1, ct2) = Thm.dest_comb ct + in + map (apfst (fn ct => Thm.capply ct ct2)) (find_vars ct1) @ + map (apfst (Thm.capply 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.cabs cv ct), + SOME (Thm.cabs cv' (rhs_of th)), NONE, SOME cv'] + 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.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 + case get_first mk_thms eqs of + NONE => thms + | SOME x => remove_suc thy x + end; + +fun eqn_suc_preproc thy ths = + let + val dest = fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of + in + if forall (can dest) ths andalso + exists (contains_suc o dest) ths + then remove_suc thy ths else ths + end; + +fun remove_suc_clause thy thms = + let + val Suc_clause' = Thm.transfer thy Suc_clause; + val vname = Name.variant (map fst + (fold (Term.add_varnames o Thm.full_prop_of) thms [])) "x"; + fun find_var (t as Const ("Suc", _) $ (v as Var _)) = SOME (t, v) + | find_var (t $ u) = (case find_var t of NONE => find_var u | x => x) + | find_var _ = NONE; + fun find_thm th = + let val th' = Conv.fconv_rule ObjectLogic.atomize th + in Option.map (pair (th, th')) (find_var (prop_of th')) end + in + case get_first find_thm thms of + NONE => thms + | SOME ((th, th'), (Sucv, v)) => + let + val cert = cterm_of (Thm.theory_of_thm th); + val th'' = ObjectLogic.rulify (Thm.implies_elim + (Conv.fconv_rule (Thm.beta_conversion true) + (Drule.instantiate' [] + [SOME (cert (lambda v (Abs ("x", HOLogic.natT, + abstract_over (Sucv, + HOLogic.dest_Trueprop (prop_of th')))))), + SOME (cert v)] Suc_clause')) + (Thm.forall_intr (cert v) th')) + in + remove_suc_clause thy (map (fn th''' => + if (op = o pairself prop_of) (th''', th) then th'' else th''') thms) + end + end; + +fun clause_suc_preproc thy ths = + let + val dest = fst o HOLogic.dest_mem o HOLogic.dest_Trueprop + in + if forall (can (dest o concl_of)) ths andalso + exists (fn th => member (op =) (foldr add_term_consts + [] (map_filter (try dest) (concl_of th :: prems_of th))) "Suc") ths + then remove_suc_clause thy ths else ths + end; + +end; (*local*) + +fun lift_obj_eq f thy = + map (fn thm => thm RS @{thm meta_eq_to_obj_eq}) + #> f thy + #> map (fn thm => thm RS @{thm eq_reflection}) + #> map (Conv.fconv_rule Drule.beta_eta_conversion) +*} + +setup {* + Codegen.add_preprocessor eqn_suc_preproc + #> Codegen.add_preprocessor clause_suc_preproc + #> CodegenData.add_preproc ("eqn_Suc", lift_obj_eq eqn_suc_preproc) + #> CodegenData.add_preproc ("clause_Suc", lift_obj_eq clause_suc_preproc) +*} +(*>*) + + +subsection {* Module names *} + +code_modulename SML + Nat Integer + Divides Integer + Efficient_Nat Integer + +code_modulename OCaml + Nat Integer + Divides Integer + Efficient_Nat Integer + +code_modulename Haskell + Nat Integer + Efficient_Nat Integer + +hide const nat_of_int int' + +end diff -r 2c69bb1374b8 -r 688a8a7bcd4e src/HOL/Library/ExecutableRat.thy --- a/src/HOL/Library/ExecutableRat.thy Thu Jul 19 21:47:38 2007 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,150 +0,0 @@ -(* Title: HOL/Library/ExecutableRat.thy - ID: $Id$ - Author: Florian Haftmann, TU Muenchen -*) - -header {* Executable implementation of rational numbers in HOL *} - -theory ExecutableRat -imports "~~/src/HOL/Real/Rational" "~~/src/HOL/NumberTheory/IntPrimes" -begin - -text {* - Actually \emph{nothing} is proved about this implementation. -*} - -subsection {* Representation and operations of executable rationals *} - -datatype erat = Rat bool nat nat - -axiomatization - div_zero :: erat - -fun - common :: "(nat * nat) \ (nat * nat) \ (nat * nat) * nat" where - "common (p1, q1) (p2, q2) = ( - let - q' = q1 * q2 div gcd (q1, q2) - in ((p1 * (q' div q1), p2 * (q' div q2)), q'))" - -definition - minus_sign :: "nat \ nat \ bool * nat" where - "minus_sign n m = (if n < m then (False, m - n) else (True, n - m))" - -fun - add_sign :: "bool * nat \ bool * nat \ bool * nat" where - "add_sign (True, n) (True, m) = (True, n + m)" -| "add_sign (False, n) (False, m) = (False, n + m)" -| "add_sign (True, n) (False, m) = minus_sign n m" -| "add_sign (False, n) (True, m) = minus_sign m n" - -definition - erat_of_quotient :: "int \ int \ erat" where - "erat_of_quotient k1 k2 = ( - let - l1 = nat (abs k1); - l2 = nat (abs k2); - m = gcd (l1, l2) - in Rat (k1 \ 0 \ k2 \ 0) (l1 div m) (l2 div m))" - -instance erat :: zero - zero_rat_def: "0 \ Rat True 0 1" .. - -instance erat :: one - one_rat_def: "1 \ Rat True 1 1" .. - -instance erat :: plus - add_rat_def: "r + s \ case r of Rat a1 p1 q1 \ case s of Rat a2 p2 q2 \ - let - ((r1, r2), den) = common (p1, q1) (p2, q2); - (sign, num) = add_sign (a1, r1) (a2, r2) - in Rat sign num den" .. - -instance erat :: minus - uminus_rat_def: "- r \ case r of Rat a p q \ - if p = 0 then Rat True 0 1 - else Rat (\ a) p q" .. - -instance erat :: times - times_rat_def: "r * s \ case r of Rat a1 p1 q1 \ case s of Rat a2 p2 q2 \ - let - p = p1 * p2; - q = q1 * q2; - m = gcd (p, q) - in Rat (a1 = a2) (p div m) (q div m)" .. - -instance erat :: inverse - inverse_rat_def: "inverse r \ case r of Rat a p q \ - if p = 0 then div_zero - else Rat a q p" .. - -instance erat :: ord - le_rat_def: "r1 \ r2 \ case r1 of Rat a1 p1 q1 \ case r2 of Rat a2 p2 q2 \ - (\ a1 \ a2) \ - (\ (a1 \ \ a2) \ - (let - ((r1, r2), dummy) = common (p1, q1) (p2, q2) - in if a1 then r1 \ r2 else r2 \ r1))" .. - - -subsection {* Code generator setup *} - -subsubsection {* code lemmas *} - -lemma number_of_rat [code unfold]: - "(number_of k \ rat) = Fract k 1" - unfolding Fract_of_int_eq rat_number_of_def by simp - -lemma rat_minus [code func]: - "(a\rat) - b = a + (- b)" unfolding diff_minus .. - -lemma rat_divide [code func]: - "(a\rat) / b = a * inverse b" unfolding divide_inverse .. - -instance rat :: eq .. - -subsubsection {* names *} - -code_modulename SML - ExecutableRat Rational - -code_modulename OCaml - ExecutableRat Rational - -code_modulename Haskell - ExecutableRat Rational - -subsubsection {* rat as abstype *} - -code_const div_zero - (SML "raise/ Fail/ \"Division by zero\"") - (OCaml "failwith \"Division by zero\"") - (Haskell "error/ \"Division by zero\"") - -code_abstype rat erat where - Fract \ erat_of_quotient - "0 \ rat" \ "0 \ erat" - "1 \ rat" \ "1 \ erat" - "op + \ rat \ rat \ rat" \ "op + \ erat \ erat \ erat" - "uminus \ rat \ rat" \ "uminus \ erat \ erat" - "op * \ rat \ rat \ rat" \ "op * \ erat \ erat \ erat" - "inverse \ rat \ rat" \ "inverse \ erat \ erat" - "op \ \ rat \ rat \ bool" \ "op \ \ erat \ erat \ bool" - "op = \ rat \ rat \ bool" \ "op = \ erat \ erat \ bool" - -types_code - rat ("{*erat*}") - -consts_code - div_zero ("(raise/ (Fail/ \"Division by zero\"))") - Fract ("({*erat_of_quotient*} (_) (_))") - "0 \ rat" ("({*Rat True 0 1*})") - "1 \ rat" ("({*Rat True 1 1*})") - "plus \ rat \ rat \ rat" ("({*op + \ erat \ erat \ erat*} (_) (_))") - "uminus \ rat \ rat" ("({*uminus \ erat \ erat*} (_))") - "op * \ rat \ rat \ rat" ("({*op * \ erat \ erat \ erat*} (_) (_))") - "inverse \ rat \ rat" ("({*inverse \ erat \ erat*} (_))") - "op \ \ rat \ rat \ bool" ("({*op \ \ erat \ erat \ bool*} (_) (_))") - "op = \ rat \ rat \ bool" ("({*op = \ erat \ erat \ bool*} (_) (_))") - -end diff -r 2c69bb1374b8 -r 688a8a7bcd4e src/HOL/Library/ExecutableSet.thy --- a/src/HOL/Library/ExecutableSet.thy Thu Jul 19 21:47:38 2007 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,360 +0,0 @@ -(* Title: HOL/Library/ExecutableSet.thy - ID: $Id$ - Author: Stefan Berghofer, TU Muenchen -*) - -header {* Implementation of finite sets by lists *} - -theory ExecutableSet -imports Main -begin - -subsection {* Definitional rewrites *} - -instance set :: (eq) eq .. - -lemma [code target: Set]: - "A = B \ A \ B \ B \ A" - by blast - -lemma [code func]: - "(A\'a\eq set) = B \ A \ B \ B \ A" - by blast - -lemma [code func]: - "(A\'a\eq set) \ B \ (\x\A. x \ B)" - unfolding subset_def .. - -lemma [code func]: - "(A\'a\eq set) \ B \ A \ B \ A \ B" - by blast - -lemma [code]: - "a \ A \ (\x\A. x = a)" - unfolding bex_triv_one_point1 .. - -definition - filter_set :: "('a \ bool) \ 'a set \ 'a set" where - "filter_set P xs = {x\xs. P x}" - -lemmas [symmetric, code inline] = filter_set_def - - -subsection {* Operations on lists *} - -subsubsection {* Basic definitions *} - -definition - flip :: "('a \ 'b \ 'c) \ 'b \ 'a \ 'c" where - "flip f a b = f b a" - -definition - member :: "'a list \ 'a \ bool" where - "member xs x \ x \ set xs" - -definition - insertl :: "'a \ 'a list \ 'a list" where - "insertl x xs = (if member xs x then xs else x#xs)" - -lemma [code target: List]: "member [] y \ False" - and [code target: List]: "member (x#xs) y \ y = x \ member xs y" - unfolding member_def by (induct xs) simp_all - -fun - drop_first :: "('a \ bool) \ 'a list \ 'a list" where - "drop_first f [] = []" -| "drop_first f (x#xs) = (if f x then xs else x # drop_first f xs)" -declare drop_first.simps [code del] -declare drop_first.simps [code target: List] - -declare remove1.simps [code del] -lemma [code target: List]: - "remove1 x xs = (if member xs x then drop_first (\y. y = x) xs else xs)" -proof (cases "member xs x") - case False thus ?thesis unfolding member_def by (induct xs) auto -next - case True - have "remove1 x xs = drop_first (\y. y = x) xs" by (induct xs) simp_all - with True show ?thesis by simp -qed - -lemma member_nil [simp]: - "member [] = (\x. False)" -proof - fix x - show "member [] x = False" unfolding member_def by simp -qed - -lemma member_insertl [simp]: - "x \ set (insertl x xs)" - unfolding insertl_def member_def mem_iff by simp - -lemma insertl_member [simp]: - fixes xs x - assumes member: "member xs x" - shows "insertl x xs = xs" - using member unfolding insertl_def by simp - -lemma insertl_not_member [simp]: - fixes xs x - assumes member: "\ (member xs x)" - shows "insertl x xs = x # xs" - using member unfolding insertl_def by simp - -lemma foldr_remove1_empty [simp]: - "foldr remove1 xs [] = []" - by (induct xs) simp_all - - -subsubsection {* Derived definitions *} - -function unionl :: "'a list \ 'a list \ 'a list" -where - "unionl [] ys = ys" -| "unionl xs ys = foldr insertl xs ys" -by pat_completeness auto -termination by lexicographic_order - -lemmas unionl_def = unionl.simps(2) - -function intersect :: "'a list \ 'a list \ 'a list" -where - "intersect [] ys = []" -| "intersect xs [] = []" -| "intersect xs ys = filter (member xs) ys" -by pat_completeness auto -termination by lexicographic_order - -lemmas intersect_def = intersect.simps(3) - -function subtract :: "'a list \ 'a list \ 'a list" -where - "subtract [] ys = ys" -| "subtract xs [] = []" -| "subtract xs ys = foldr remove1 xs ys" -by pat_completeness auto -termination by lexicographic_order - -lemmas subtract_def = subtract.simps(3) - -function map_distinct :: "('a \ 'b) \ 'a list \ 'b list" -where - "map_distinct f [] = []" -| "map_distinct f xs = foldr (insertl o f) xs []" -by pat_completeness auto -termination by lexicographic_order - -lemmas map_distinct_def = map_distinct.simps(2) - -function unions :: "'a list list \ 'a list" -where - "unions [] = []" -| "unions xs = foldr unionl xs []" -by pat_completeness auto -termination by lexicographic_order - -lemmas unions_def = unions.simps(2) - -consts intersects :: "'a list list \ 'a list" -primrec - "intersects (x#xs) = foldr intersect xs x" - -definition - map_union :: "'a list \ ('a \ 'b list) \ 'b list" where - "map_union xs f = unions (map f xs)" - -definition - map_inter :: "'a list \ ('a \ 'b list) \ 'b list" where - "map_inter xs f = intersects (map f xs)" - - -subsection {* Isomorphism proofs *} - -lemma iso_member: - "member xs x \ x \ set xs" - unfolding member_def mem_iff .. - -lemma iso_insert: - "set (insertl x xs) = insert x (set xs)" - unfolding insertl_def iso_member by (simp add: Set.insert_absorb) - -lemma iso_remove1: - assumes distnct: "distinct xs" - shows "set (remove1 x xs) = set xs - {x}" - using distnct set_remove1_eq by auto - -lemma iso_union: - "set (unionl xs ys) = set xs \ set ys" - unfolding unionl_def - by (induct xs arbitrary: ys) (simp_all add: iso_insert) - -lemma iso_intersect: - "set (intersect xs ys) = set xs \ set ys" - unfolding intersect_def Int_def by (simp add: Int_def iso_member) auto - -definition - subtract' :: "'a list \ 'a list \ 'a list" where - "subtract' = flip subtract" - -lemma iso_subtract: - fixes ys - assumes distnct: "distinct ys" - shows "set (subtract' ys xs) = set ys - set xs" - and "distinct (subtract' ys xs)" - unfolding subtract'_def flip_def subtract_def - using distnct by (induct xs arbitrary: ys) auto - -lemma iso_map_distinct: - "set (map_distinct f xs) = image f (set xs)" - unfolding map_distinct_def by (induct xs) (simp_all add: iso_insert) - -lemma iso_unions: - "set (unions xss) = \ set (map set xss)" - unfolding unions_def -proof (induct xss) - case Nil show ?case by simp -next - case (Cons xs xss) thus ?case by (induct xs) (simp_all add: iso_insert) -qed - -lemma iso_intersects: - "set (intersects (xs#xss)) = \ set (map set (xs#xss))" - by (induct xss) (simp_all add: Int_def iso_member, auto) - -lemma iso_UNION: - "set (map_union xs f) = UNION (set xs) (set o f)" - unfolding map_union_def iso_unions by simp - -lemma iso_INTER: - "set (map_inter (x#xs) f) = INTER (set (x#xs)) (set o f)" - unfolding map_inter_def iso_intersects by (induct xs) (simp_all add: iso_member, auto) - -definition - Blall :: "'a list \ ('a \ bool) \ bool" where - "Blall = flip list_all" -definition - Blex :: "'a list \ ('a \ bool) \ bool" where - "Blex = flip list_ex" - -lemma iso_Ball: - "Blall xs f = Ball (set xs) f" - unfolding Blall_def flip_def by (induct xs) simp_all - -lemma iso_Bex: - "Blex xs f = Bex (set xs) f" - unfolding Blex_def flip_def by (induct xs) simp_all - -lemma iso_filter: - "set (filter P xs) = filter_set P (set xs)" - unfolding filter_set_def by (induct xs) auto - -subsection {* code generator setup *} - -ML {* -nonfix inter; -nonfix union; -nonfix subset; -*} - -code_modulename SML - ExecutableSet List - Set List - -code_modulename OCaml - ExecutableSet List - Set List - -code_modulename Haskell - ExecutableSet List - Set List - -definition [code inline]: - "empty_list = []" - -lemma [code func]: - "insert (x \ 'a\eq) = insert x" .. - -lemma [code func]: - "(xs \ 'a\eq set) \ ys = xs \ ys" .. - -lemma [code func]: - "(xs \ 'a\eq set) \ ys = xs \ ys" .. - -lemma [code func]: - "(op -) (xs \ 'a\eq set) = (op -) (xs \ 'a\eq set)" .. - -lemma [code func]: - "image (f \ 'a \ 'b\eq) = image f" .. - -lemma [code func]: - "Union (xss \ 'a\eq set set) = Union xss" .. - -lemma [code func]: - "Inter (xss \ 'a\eq set set) = Inter xss" .. - -lemma [code func]: - "UNION xs (f \ 'a \ 'b\eq set) = UNION xs f" .. - -lemma [code func]: - "INTER xs (f \ 'a \ 'b\eq set) = INTER xs f" .. - -lemma [code func]: - "Ball (xs \ 'a\type set) = Ball xs" .. - -lemma [code func]: - "Bex (xs \ 'a\type set) = Bex xs" .. - -lemma [code func]: - "filter_set P (xs \ 'a\type set) = filter_set P xs" .. - - -code_abstype "'a set" "'a list" where - "{}" \ empty_list - insert \ insertl - "op \" \ unionl - "op \" \ intersect - "op - \ 'a set \ 'a set \ 'a set" \ subtract' - image \ map_distinct - Union \ unions - Inter \ intersects - UNION \ map_union - INTER \ map_inter - Ball \ Blall - Bex \ Blex - filter_set \ filter - - -subsubsection {* type serializations *} - -types_code - set ("_ list") -attach (term_of) {* -fun term_of_set f T [] = Const ("{}", Type ("set", [T])) - | term_of_set f T (x :: xs) = Const ("insert", - T --> Type ("set", [T]) --> Type ("set", [T])) $ f x $ term_of_set f T xs; -*} -attach (test) {* -fun gen_set' aG i j = frequency - [(i, fn () => aG j :: gen_set' aG (i-1) j), (1, fn () => [])] () -and gen_set aG i = gen_set' aG i i; -*} - - -subsubsection {* const serializations *} - -consts_code - "{}" ("{*[]*}") - insert ("{*insertl*}") - "op \" ("{*unionl*}") - "op \" ("{*intersect*}") - "op - \ 'a set \ 'a set \ 'a set" ("{* flip subtract *}") - image ("{*map_distinct*}") - Union ("{*unions*}") - Inter ("{*intersects*}") - UNION ("{*map_union*}") - INTER ("{*map_inter*}") - Ball ("{*Blall*}") - Bex ("{*Blex*}") - filter_set ("{*filter*}") - -end diff -r 2c69bb1374b8 -r 688a8a7bcd4e src/HOL/Library/Executable_Rat.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/Executable_Rat.thy Thu Jul 19 21:47:39 2007 +0200 @@ -0,0 +1,150 @@ +(* Title: HOL/Library/Executable_Rat.thy + ID: $Id$ + Author: Florian Haftmann, TU Muenchen +*) + +header {* Executable implementation of rational numbers in HOL *} + +theory Executable_Rat +imports "~~/src/HOL/Real/Rational" "~~/src/HOL/NumberTheory/IntPrimes" +begin + +text {* + Actually \emph{nothing} is proved about this implementation. +*} + +subsection {* Representation and operations of executable rationals *} + +datatype erat = Rat bool nat nat + +axiomatization + div_zero :: erat + +fun + common :: "(nat * nat) \ (nat * nat) \ (nat * nat) * nat" where + "common (p1, q1) (p2, q2) = ( + let + q' = q1 * q2 div gcd (q1, q2) + in ((p1 * (q' div q1), p2 * (q' div q2)), q'))" + +definition + minus_sign :: "nat \ nat \ bool * nat" where + "minus_sign n m = (if n < m then (False, m - n) else (True, n - m))" + +fun + add_sign :: "bool * nat \ bool * nat \ bool * nat" where + "add_sign (True, n) (True, m) = (True, n + m)" +| "add_sign (False, n) (False, m) = (False, n + m)" +| "add_sign (True, n) (False, m) = minus_sign n m" +| "add_sign (False, n) (True, m) = minus_sign m n" + +definition + erat_of_quotient :: "int \ int \ erat" where + "erat_of_quotient k1 k2 = ( + let + l1 = nat (abs k1); + l2 = nat (abs k2); + m = gcd (l1, l2) + in Rat (k1 \ 0 \ k2 \ 0) (l1 div m) (l2 div m))" + +instance erat :: zero + zero_rat_def: "0 \ Rat True 0 1" .. + +instance erat :: one + one_rat_def: "1 \ Rat True 1 1" .. + +instance erat :: plus + add_rat_def: "r + s \ case r of Rat a1 p1 q1 \ case s of Rat a2 p2 q2 \ + let + ((r1, r2), den) = common (p1, q1) (p2, q2); + (sign, num) = add_sign (a1, r1) (a2, r2) + in Rat sign num den" .. + +instance erat :: minus + uminus_rat_def: "- r \ case r of Rat a p q \ + if p = 0 then Rat True 0 1 + else Rat (\ a) p q" .. + +instance erat :: times + times_rat_def: "r * s \ case r of Rat a1 p1 q1 \ case s of Rat a2 p2 q2 \ + let + p = p1 * p2; + q = q1 * q2; + m = gcd (p, q) + in Rat (a1 = a2) (p div m) (q div m)" .. + +instance erat :: inverse + inverse_rat_def: "inverse r \ case r of Rat a p q \ + if p = 0 then div_zero + else Rat a q p" .. + +instance erat :: ord + le_rat_def: "r1 \ r2 \ case r1 of Rat a1 p1 q1 \ case r2 of Rat a2 p2 q2 \ + (\ a1 \ a2) \ + (\ (a1 \ \ a2) \ + (let + ((r1, r2), dummy) = common (p1, q1) (p2, q2) + in if a1 then r1 \ r2 else r2 \ r1))" .. + + +subsection {* Code generator setup *} + +subsubsection {* code lemmas *} + +lemma number_of_rat [code unfold]: + "(number_of k \ rat) = Fract k 1" + unfolding Fract_of_int_eq rat_number_of_def by simp + +lemma rat_minus [code func]: + "(a\rat) - b = a + (- b)" unfolding diff_minus .. + +lemma rat_divide [code func]: + "(a\rat) / b = a * inverse b" unfolding divide_inverse .. + +instance rat :: eq .. + +subsubsection {* names *} + +code_modulename SML + Executable_Rat Rational + +code_modulename OCaml + Executable_Rat Rational + +code_modulename Haskell + Executable_Rat Rational + +subsubsection {* rat as abstype *} + +code_const div_zero + (SML "raise/ Fail/ \"Division by zero\"") + (OCaml "failwith \"Division by zero\"") + (Haskell "error/ \"Division by zero\"") + +code_abstype rat erat where + Fract \ erat_of_quotient + "0 \ rat" \ "0 \ erat" + "1 \ rat" \ "1 \ erat" + "op + \ rat \ rat \ rat" \ "op + \ erat \ erat \ erat" + "uminus \ rat \ rat" \ "uminus \ erat \ erat" + "op * \ rat \ rat \ rat" \ "op * \ erat \ erat \ erat" + "inverse \ rat \ rat" \