--- 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
--- 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 {*
--- 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");
--- 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 \
--- 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 \<Rightarrow> nat" where
- "k \<ge> 0 \<Longrightarrow> nat_of_int k = nat k"
-
-definition
- int' :: "nat \<Rightarrow> 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 \<ge> 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 \<le> k \<equiv> True"
- shows "k \<ge> 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 \<Longrightarrow> 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 \<equiv> (\<lambda>f g n. if n = 0 then f else g (n - 1))"
-proof -
- have rewrite: "\<And>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 \<equiv> (\<lambda>f g n. if n = 0 then f else g (n - 1))"
- by (rule eq_reflection ext rewrite)+
-qed
-
-lemma [code inline]:
- "nat_case = (\<lambda>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) \<longleftrightarrow> (int' m < int' n)"
- unfolding int'_def by simp
-lemma [code func, code inline]: "(m \<le> n) \<longleftrightarrow> (int' m \<le> int' n)"
- unfolding int'_def by simp
-lemma [code func, code inline]: "m = n \<longleftrightarrow> 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 \<Longrightarrow> int' n = 1 + int' (nat_of_int (int' n - 1))"
- proof -
- assume prem: "n > 0"
- then have "int' n - 1 \<ge> 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 \<Colon> nat" ("0")
- Suc ("(_ + 1)")
-
-text {*
- Since natural numbers are implemented
- using integers, the coercion function @{const "int"} of type
- @{typ "nat \<Rightarrow> int"} is simply implemented by the identity function,
- likewise @{const nat_of_int} of type @{typ "int \<Rightarrow> 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 ("\<module>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 \<le>) 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: "(\<And>n. f (Suc n) = h n) \<Longrightarrow> f 0 = g \<Longrightarrow>
- f n = (if n = 0 then g else h (n - 1))"
- by (case_tac n) simp_all
-
-theorem Suc_clause: "(\<And>n. P n (Suc n)) \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> 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
--- /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 \<Rightarrow> nat" where
+ "k \<ge> 0 \<Longrightarrow> nat_of_int k = nat k"
+
+definition
+ int' :: "nat \<Rightarrow> 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 \<ge> 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 \<le> k \<equiv> True"
+ shows "k \<ge> 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 \<Longrightarrow> 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 \<equiv> (\<lambda>f g n. if n = 0 then f else g (n - 1))"
+proof -
+ have rewrite: "\<And>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 \<equiv> (\<lambda>f g n. if n = 0 then f else g (n - 1))"
+ by (rule eq_reflection ext rewrite)+
+qed
+
+lemma [code inline]:
+ "nat_case = (\<lambda>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) \<longleftrightarrow> (int' m < int' n)"
+ unfolding int'_def by simp
+lemma [code func, code inline]: "(m \<le> n) \<longleftrightarrow> (int' m \<le> int' n)"
+ unfolding int'_def by simp
+lemma [code func, code inline]: "m = n \<longleftrightarrow> 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 \<Longrightarrow> int' n = 1 + int' (nat_of_int (int' n - 1))"
+ proof -
+ assume prem: "n > 0"
+ then have "int' n - 1 \<ge> 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 \<Colon> nat" ("0")
+ Suc ("(_ + 1)")
+
+text {*
+ Since natural numbers are implemented
+ using integers, the coercion function @{const "int"} of type
+ @{typ "nat \<Rightarrow> int"} is simply implemented by the identity function,
+ likewise @{const nat_of_int} of type @{typ "int \<Rightarrow> 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 ("\<module>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 \<le>) 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: "(\<And>n. f (Suc n) = h n) \<Longrightarrow> f 0 = g \<Longrightarrow>
+ f n = (if n = 0 then g else h (n - 1))"
+ by (case_tac n) simp_all
+
+theorem Suc_clause: "(\<And>n. P n (Suc n)) \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> 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
--- 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) \<Rightarrow> (nat * nat) \<Rightarrow> (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 \<Rightarrow> nat \<Rightarrow> bool * nat" where
- "minus_sign n m = (if n < m then (False, m - n) else (True, n - m))"
-
-fun
- add_sign :: "bool * nat \<Rightarrow> bool * nat \<Rightarrow> 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 \<Rightarrow> int \<Rightarrow> erat" where
- "erat_of_quotient k1 k2 = (
- let
- l1 = nat (abs k1);
- l2 = nat (abs k2);
- m = gcd (l1, l2)
- in Rat (k1 \<le> 0 \<longleftrightarrow> k2 \<le> 0) (l1 div m) (l2 div m))"
-
-instance erat :: zero
- zero_rat_def: "0 \<equiv> Rat True 0 1" ..
-
-instance erat :: one
- one_rat_def: "1 \<equiv> Rat True 1 1" ..
-
-instance erat :: plus
- add_rat_def: "r + s \<equiv> case r of Rat a1 p1 q1 \<Rightarrow> case s of Rat a2 p2 q2 \<Rightarrow>
- 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 \<equiv> case r of Rat a p q \<Rightarrow>
- if p = 0 then Rat True 0 1
- else Rat (\<not> a) p q" ..
-
-instance erat :: times
- times_rat_def: "r * s \<equiv> case r of Rat a1 p1 q1 \<Rightarrow> case s of Rat a2 p2 q2 \<Rightarrow>
- 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 \<equiv> case r of Rat a p q \<Rightarrow>
- if p = 0 then div_zero
- else Rat a q p" ..
-
-instance erat :: ord
- le_rat_def: "r1 \<le> r2 \<equiv> case r1 of Rat a1 p1 q1 \<Rightarrow> case r2 of Rat a2 p2 q2 \<Rightarrow>
- (\<not> a1 \<and> a2) \<or>
- (\<not> (a1 \<and> \<not> a2) \<and>
- (let
- ((r1, r2), dummy) = common (p1, q1) (p2, q2)
- in if a1 then r1 \<le> r2 else r2 \<le> r1))" ..
-
-
-subsection {* Code generator setup *}
-
-subsubsection {* code lemmas *}
-
-lemma number_of_rat [code unfold]:
- "(number_of k \<Colon> rat) = Fract k 1"
- unfolding Fract_of_int_eq rat_number_of_def by simp
-
-lemma rat_minus [code func]:
- "(a\<Colon>rat) - b = a + (- b)" unfolding diff_minus ..
-
-lemma rat_divide [code func]:
- "(a\<Colon>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 \<equiv> erat_of_quotient
- "0 \<Colon> rat" \<equiv> "0 \<Colon> erat"
- "1 \<Colon> rat" \<equiv> "1 \<Colon> erat"
- "op + \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat" \<equiv> "op + \<Colon> erat \<Rightarrow> erat \<Rightarrow> erat"
- "uminus \<Colon> rat \<Rightarrow> rat" \<equiv> "uminus \<Colon> erat \<Rightarrow> erat"
- "op * \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat" \<equiv> "op * \<Colon> erat \<Rightarrow> erat \<Rightarrow> erat"
- "inverse \<Colon> rat \<Rightarrow> rat" \<equiv> "inverse \<Colon> erat \<Rightarrow> erat"
- "op \<le> \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool" \<equiv> "op \<le> \<Colon> erat \<Rightarrow> erat \<Rightarrow> bool"
- "op = \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool" \<equiv> "op = \<Colon> erat \<Rightarrow> erat \<Rightarrow> bool"
-
-types_code
- rat ("{*erat*}")
-
-consts_code
- div_zero ("(raise/ (Fail/ \"Division by zero\"))")
- Fract ("({*erat_of_quotient*} (_) (_))")
- "0 \<Colon> rat" ("({*Rat True 0 1*})")
- "1 \<Colon> rat" ("({*Rat True 1 1*})")
- "plus \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat" ("({*op + \<Colon> erat \<Rightarrow> erat \<Rightarrow> erat*} (_) (_))")
- "uminus \<Colon> rat \<Rightarrow> rat" ("({*uminus \<Colon> erat \<Rightarrow> erat*} (_))")
- "op * \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat" ("({*op * \<Colon> erat \<Rightarrow> erat \<Rightarrow> erat*} (_) (_))")
- "inverse \<Colon> rat \<Rightarrow> rat" ("({*inverse \<Colon> erat \<Rightarrow> erat*} (_))")
- "op \<le> \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool" ("({*op \<le> \<Colon> erat \<Rightarrow> erat \<Rightarrow> bool*} (_) (_))")
- "op = \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool" ("({*op = \<Colon> erat \<Rightarrow> erat \<Rightarrow> bool*} (_) (_))")
-
-end
--- 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 \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
- by blast
-
-lemma [code func]:
- "(A\<Colon>'a\<Colon>eq set) = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
- by blast
-
-lemma [code func]:
- "(A\<Colon>'a\<Colon>eq set) \<subseteq> B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
- unfolding subset_def ..
-
-lemma [code func]:
- "(A\<Colon>'a\<Colon>eq set) \<subset> B \<longleftrightarrow> A \<subseteq> B \<and> A \<noteq> B"
- by blast
-
-lemma [code]:
- "a \<in> A \<longleftrightarrow> (\<exists>x\<in>A. x = a)"
- unfolding bex_triv_one_point1 ..
-
-definition
- filter_set :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" where
- "filter_set P xs = {x\<in>xs. P x}"
-
-lemmas [symmetric, code inline] = filter_set_def
-
-
-subsection {* Operations on lists *}
-
-subsubsection {* Basic definitions *}
-
-definition
- flip :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c" where
- "flip f a b = f b a"
-
-definition
- member :: "'a list \<Rightarrow> 'a \<Rightarrow> bool" where
- "member xs x \<longleftrightarrow> x \<in> set xs"
-
-definition
- insertl :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
- "insertl x xs = (if member xs x then xs else x#xs)"
-
-lemma [code target: List]: "member [] y \<longleftrightarrow> False"
- and [code target: List]: "member (x#xs) y \<longleftrightarrow> y = x \<or> member xs y"
- unfolding member_def by (induct xs) simp_all
-
-fun
- drop_first :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> '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 (\<lambda>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 (\<lambda>y. y = x) xs" by (induct xs) simp_all
- with True show ?thesis by simp
-qed
-
-lemma member_nil [simp]:
- "member [] = (\<lambda>x. False)"
-proof
- fix x
- show "member [] x = False" unfolding member_def by simp
-qed
-
-lemma member_insertl [simp]:
- "x \<in> 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: "\<not> (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 \<Rightarrow> 'a list \<Rightarrow> '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 \<Rightarrow> 'a list \<Rightarrow> '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 \<Rightarrow> 'a list \<Rightarrow> '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 \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> '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 \<Rightarrow> '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 \<Rightarrow> 'a list"
-primrec
- "intersects (x#xs) = foldr intersect xs x"
-
-definition
- map_union :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b list) \<Rightarrow> 'b list" where
- "map_union xs f = unions (map f xs)"
-
-definition
- map_inter :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b list) \<Rightarrow> 'b list" where
- "map_inter xs f = intersects (map f xs)"
-
-
-subsection {* Isomorphism proofs *}
-
-lemma iso_member:
- "member xs x \<longleftrightarrow> x \<in> 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 \<union> set ys"
- unfolding unionl_def
- by (induct xs arbitrary: ys) (simp_all add: iso_insert)
-
-lemma iso_intersect:
- "set (intersect xs ys) = set xs \<inter> set ys"
- unfolding intersect_def Int_def by (simp add: Int_def iso_member) auto
-
-definition
- subtract' :: "'a list \<Rightarrow> 'a list \<Rightarrow> '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) = \<Union> 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)) = \<Inter> 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 \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" where
- "Blall = flip list_all"
-definition
- Blex :: "'a list \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 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 \<Colon> 'a\<Colon>eq) = insert x" ..
-
-lemma [code func]:
- "(xs \<Colon> 'a\<Colon>eq set) \<union> ys = xs \<union> ys" ..
-
-lemma [code func]:
- "(xs \<Colon> 'a\<Colon>eq set) \<inter> ys = xs \<inter> ys" ..
-
-lemma [code func]:
- "(op -) (xs \<Colon> 'a\<Colon>eq set) = (op -) (xs \<Colon> 'a\<Colon>eq set)" ..
-
-lemma [code func]:
- "image (f \<Colon> 'a \<Rightarrow> 'b\<Colon>eq) = image f" ..
-
-lemma [code func]:
- "Union (xss \<Colon> 'a\<Colon>eq set set) = Union xss" ..
-
-lemma [code func]:
- "Inter (xss \<Colon> 'a\<Colon>eq set set) = Inter xss" ..
-
-lemma [code func]:
- "UNION xs (f \<Colon> 'a \<Rightarrow> 'b\<Colon>eq set) = UNION xs f" ..
-
-lemma [code func]:
- "INTER xs (f \<Colon> 'a \<Rightarrow> 'b\<Colon>eq set) = INTER xs f" ..
-
-lemma [code func]:
- "Ball (xs \<Colon> 'a\<Colon>type set) = Ball xs" ..
-
-lemma [code func]:
- "Bex (xs \<Colon> 'a\<Colon>type set) = Bex xs" ..
-
-lemma [code func]:
- "filter_set P (xs \<Colon> 'a\<Colon>type set) = filter_set P xs" ..
-
-
-code_abstype "'a set" "'a list" where
- "{}" \<equiv> empty_list
- insert \<equiv> insertl
- "op \<union>" \<equiv> unionl
- "op \<inter>" \<equiv> intersect
- "op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" \<equiv> subtract'
- image \<equiv> map_distinct
- Union \<equiv> unions
- Inter \<equiv> intersects
- UNION \<equiv> map_union
- INTER \<equiv> map_inter
- Ball \<equiv> Blall
- Bex \<equiv> Blex
- filter_set \<equiv> 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 \<union>" ("{*unionl*}")
- "op \<inter>" ("{*intersect*}")
- "op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> '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
--- /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) \<Rightarrow> (nat * nat) \<Rightarrow> (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 \<Rightarrow> nat \<Rightarrow> bool * nat" where
+ "minus_sign n m = (if n < m then (False, m - n) else (True, n - m))"
+
+fun
+ add_sign :: "bool * nat \<Rightarrow> bool * nat \<Rightarrow> 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 \<Rightarrow> int \<Rightarrow> erat" where
+ "erat_of_quotient k1 k2 = (
+ let
+ l1 = nat (abs k1);
+ l2 = nat (abs k2);
+ m = gcd (l1, l2)
+ in Rat (k1 \<le> 0 \<longleftrightarrow> k2 \<le> 0) (l1 div m) (l2 div m))"
+
+instance erat :: zero
+ zero_rat_def: "0 \<equiv> Rat True 0 1" ..
+
+instance erat :: one
+ one_rat_def: "1 \<equiv> Rat True 1 1" ..
+
+instance erat :: plus
+ add_rat_def: "r + s \<equiv> case r of Rat a1 p1 q1 \<Rightarrow> case s of Rat a2 p2 q2 \<Rightarrow>
+ 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 \<equiv> case r of Rat a p q \<Rightarrow>
+ if p = 0 then Rat True 0 1
+ else Rat (\<not> a) p q" ..
+
+instance erat :: times
+ times_rat_def: "r * s \<equiv> case r of Rat a1 p1 q1 \<Rightarrow> case s of Rat a2 p2 q2 \<Rightarrow>
+ 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 \<equiv> case r of Rat a p q \<Rightarrow>
+ if p = 0 then div_zero
+ else Rat a q p" ..
+
+instance erat :: ord
+ le_rat_def: "r1 \<le> r2 \<equiv> case r1 of Rat a1 p1 q1 \<Rightarrow> case r2 of Rat a2 p2 q2 \<Rightarrow>
+ (\<not> a1 \<and> a2) \<or>
+ (\<not> (a1 \<and> \<not> a2) \<and>
+ (let
+ ((r1, r2), dummy) = common (p1, q1) (p2, q2)
+ in if a1 then r1 \<le> r2 else r2 \<le> r1))" ..
+
+
+subsection {* Code generator setup *}
+
+subsubsection {* code lemmas *}
+
+lemma number_of_rat [code unfold]:
+ "(number_of k \<Colon> rat) = Fract k 1"
+ unfolding Fract_of_int_eq rat_number_of_def by simp
+
+lemma rat_minus [code func]:
+ "(a\<Colon>rat) - b = a + (- b)" unfolding diff_minus ..
+
+lemma rat_divide [code func]:
+ "(a\<Colon>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 \<equiv> erat_of_quotient
+ "0 \<Colon> rat" \<equiv> "0 \<Colon> erat"
+ "1 \<Colon> rat" \<equiv> "1 \<Colon> erat"
+ "op + \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat" \<equiv> "op + \<Colon> erat \<Rightarrow> erat \<Rightarrow> erat"
+ "uminus \<Colon> rat \<Rightarrow> rat" \<equiv> "uminus \<Colon> erat \<Rightarrow> erat"
+ "op * \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat" \<equiv> "op * \<Colon> erat \<Rightarrow> erat \<Rightarrow> erat"
+ "inverse \<Colon> rat \<Rightarrow> rat" \<equiv> "inverse \<Colon> erat \<Rightarrow> erat"
+ "op \<le> \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool" \<equiv> "op \<le> \<Colon> erat \<Rightarrow> erat \<Rightarrow> bool"
+ "op = \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool" \<equiv> "op = \<Colon> erat \<Rightarrow> erat \<Rightarrow> bool"
+
+types_code
+ rat ("{*erat*}")
+
+consts_code
+ div_zero ("(raise/ (Fail/ \"Division by zero\"))")
+ Fract ("({*erat_of_quotient*} (_) (_))")
+ "0 \<Colon> rat" ("({*Rat True 0 1*})")
+ "1 \<Colon> rat" ("({*Rat True 1 1*})")
+ "plus \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat" ("({*op + \<Colon> erat \<Rightarrow> erat \<Rightarrow> erat*} (_) (_))")
+ "uminus \<Colon> rat \<Rightarrow> rat" ("({*uminus \<Colon> erat \<Rightarrow> erat*} (_))")
+ "op * \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat" ("({*op * \<Colon> erat \<Rightarrow> erat \<Rightarrow> erat*} (_) (_))")
+ "inverse \<Colon> rat \<Rightarrow> rat" ("({*inverse \<Colon> erat \<Rightarrow> erat*} (_))")
+ "op \<le> \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool" ("({*op \<le> \<Colon> erat \<Rightarrow> erat \<Rightarrow> bool*} (_) (_))")
+ "op = \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool" ("({*op = \<Colon> erat \<Rightarrow> erat \<Rightarrow> bool*} (_) (_))")
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Executable_Set.thy Thu Jul 19 21:47:39 2007 +0200
@@ -0,0 +1,360 @@
+(* Title: HOL/Library/Executable_Set.thy
+ ID: $Id$
+ Author: Stefan Berghofer, TU Muenchen
+*)
+
+header {* Implementation of finite sets by lists *}
+
+theory Executable_Set
+imports Main
+begin
+
+subsection {* Definitional rewrites *}
+
+instance set :: (eq) eq ..
+
+lemma [code target: Set]:
+ "A = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
+ by blast
+
+lemma [code func]:
+ "(A\<Colon>'a\<Colon>eq set) = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
+ by blast
+
+lemma [code func]:
+ "(A\<Colon>'a\<Colon>eq set) \<subseteq> B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
+ unfolding subset_def ..
+
+lemma [code func]:
+ "(A\<Colon>'a\<Colon>eq set) \<subset> B \<longleftrightarrow> A \<subseteq> B \<and> A \<noteq> B"
+ by blast
+
+lemma [code]:
+ "a \<in> A \<longleftrightarrow> (\<exists>x\<in>A. x = a)"
+ unfolding bex_triv_one_point1 ..
+
+definition
+ filter_set :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" where
+ "filter_set P xs = {x\<in>xs. P x}"
+
+lemmas [symmetric, code inline] = filter_set_def
+
+
+subsection {* Operations on lists *}
+
+subsubsection {* Basic definitions *}
+
+definition
+ flip :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c" where
+ "flip f a b = f b a"
+
+definition
+ member :: "'a list \<Rightarrow> 'a \<Rightarrow> bool" where
+ "member xs x \<longleftrightarrow> x \<in> set xs"
+
+definition
+ insertl :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+ "insertl x xs = (if member xs x then xs else x#xs)"
+
+lemma [code target: List]: "member [] y \<longleftrightarrow> False"
+ and [code target: List]: "member (x#xs) y \<longleftrightarrow> y = x \<or> member xs y"
+ unfolding member_def by (induct xs) simp_all
+
+fun
+ drop_first :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> '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 (\<lambda>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 (\<lambda>y. y = x) xs" by (induct xs) simp_all
+ with True show ?thesis by simp
+qed
+
+lemma member_nil [simp]:
+ "member [] = (\<lambda>x. False)"
+proof
+ fix x
+ show "member [] x = False" unfolding member_def by simp
+qed
+
+lemma member_insertl [simp]:
+ "x \<in> 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: "\<not> (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 \<Rightarrow> 'a list \<Rightarrow> '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 \<Rightarrow> 'a list \<Rightarrow> '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 \<Rightarrow> 'a list \<Rightarrow> '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 \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> '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 \<Rightarrow> '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 \<Rightarrow> 'a list"
+primrec
+ "intersects (x#xs) = foldr intersect xs x"
+
+definition
+ map_union :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b list) \<Rightarrow> 'b list" where
+ "map_union xs f = unions (map f xs)"
+
+definition
+ map_inter :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b list) \<Rightarrow> 'b list" where
+ "map_inter xs f = intersects (map f xs)"
+
+
+subsection {* Isomorphism proofs *}
+
+lemma iso_member:
+ "member xs x \<longleftrightarrow> x \<in> 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 \<union> set ys"
+ unfolding unionl_def
+ by (induct xs arbitrary: ys) (simp_all add: iso_insert)
+
+lemma iso_intersect:
+ "set (intersect xs ys) = set xs \<inter> set ys"
+ unfolding intersect_def Int_def by (simp add: Int_def iso_member) auto
+
+definition
+ subtract' :: "'a list \<Rightarrow> 'a list \<Rightarrow> '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) = \<Union> 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)) = \<Inter> 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 \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" where
+ "Blall = flip list_all"
+definition
+ Blex :: "'a list \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 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
+ Executable_Set List
+ Set List
+
+code_modulename OCaml
+ Executable_Set List
+ Set List
+
+code_modulename Haskell
+ Executable_Set List
+ Set List
+
+definition [code inline]:
+ "empty_list = []"
+
+lemma [code func]:
+ "insert (x \<Colon> 'a\<Colon>eq) = insert x" ..
+
+lemma [code func]:
+ "(xs \<Colon> 'a\<Colon>eq set) \<union> ys = xs \<union> ys" ..
+
+lemma [code func]:
+ "(xs \<Colon> 'a\<Colon>eq set) \<inter> ys = xs \<inter> ys" ..
+
+lemma [code func]:
+ "(op -) (xs \<Colon> 'a\<Colon>eq set) = (op -) (xs \<Colon> 'a\<Colon>eq set)" ..
+
+lemma [code func]:
+ "image (f \<Colon> 'a \<Rightarrow> 'b\<Colon>eq) = image f" ..
+
+lemma [code func]:
+ "Union (xss \<Colon> 'a\<Colon>eq set set) = Union xss" ..
+
+lemma [code func]:
+ "Inter (xss \<Colon> 'a\<Colon>eq set set) = Inter xss" ..
+
+lemma [code func]:
+ "UNION xs (f \<Colon> 'a \<Rightarrow> 'b\<Colon>eq set) = UNION xs f" ..
+
+lemma [code func]:
+ "INTER xs (f \<Colon> 'a \<Rightarrow> 'b\<Colon>eq set) = INTER xs f" ..
+
+lemma [code func]:
+ "Ball (xs \<Colon> 'a\<Colon>type set) = Ball xs" ..
+
+lemma [code func]:
+ "Bex (xs \<Colon> 'a\<Colon>type set) = Bex xs" ..
+
+lemma [code func]:
+ "filter_set P (xs \<Colon> 'a\<Colon>type set) = filter_set P xs" ..
+
+
+code_abstype "'a set" "'a list" where
+ "{}" \<equiv> empty_list
+ insert \<equiv> insertl
+ "op \<union>" \<equiv> unionl
+ "op \<inter>" \<equiv> intersect
+ "op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" \<equiv> subtract'
+ image \<equiv> map_distinct
+ Union \<equiv> unions
+ Inter \<equiv> intersects
+ UNION \<equiv> map_union
+ INTER \<equiv> map_inter
+ Ball \<equiv> Blall
+ Bex \<equiv> Blex
+ filter_set \<equiv> 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 \<union>" ("{*unionl*}")
+ "op \<inter>" ("{*intersect*}")
+ "op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> '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
--- a/src/HOL/Library/Graphs.thy Thu Jul 19 21:47:38 2007 +0200
+++ b/src/HOL/Library/Graphs.thy Thu Jul 19 21:47:39 2007 +0200
@@ -6,7 +6,7 @@
header {* General Graphs as Sets *}
theory Graphs
-imports Main SCT_Misc Kleene_Algebras ExecutableSet
+imports Main SCT_Misc Kleene_Algebras Executable_Set
begin
subsection {* Basic types, Size Change Graphs *}
--- a/src/HOL/Library/Library.thy Thu Jul 19 21:47:38 2007 +0200
+++ b/src/HOL/Library/Library.thy Thu Jul 19 21:47:39 2007 +0200
@@ -9,15 +9,15 @@
Coinductive_List
Commutative_Ring
Continuity
- EfficientNat
+ Efficient_Nat
Eval
- ExecutableRat
+ Executable_Rat
Executable_Real
- ExecutableSet
+ Executable_Set
FuncSet
GCD
Infinite_Set
- MLString
+ ML_String
Multiset
NatPair
Nat_Infinity
--- a/src/HOL/Library/MLString.thy Thu Jul 19 21:47:38 2007 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,73 +0,0 @@
-(* ID: $Id$
- Author: Florian Haftmann, TU Muenchen
-*)
-
-header {* Monolithic strings for ML *}
-
-theory MLString
-imports List
-begin
-
-subsection {* Motivation *}
-
-text {*
- Strings are represented in HOL as list of characters.
- For code generation to Haskell, this is no problem
- since in Haskell "abc" is equivalent to ['a', 'b', 'c'].
- On the other hand, in ML all strings have to
- be represented as list of characters which
- is awkward to read. This theory provides a distinguished
- datatype for strings which then by convention
- are serialized as monolithic ML strings.
-*}
-
-
-subsection {* Datatype of monolithic strings *}
-
-datatype ml_string = STR string
-
-lemmas [code func del] = ml_string.recs ml_string.cases
-
-lemma [code func]: "size (s\<Colon>ml_string) = 0"
- by (cases s) simp_all
-
-subsection {* ML interface *}
-
-ML {*
-structure MLString =
-struct
-
-fun mk s = @{term STR} $ HOLogic.mk_string s;
-
-end;
-*}
-
-
-subsection {* Code serialization *}
-
-code_type ml_string
- (SML "string")
-
-setup {*
-let
- val charr = @{const_name Char}
- val nibbles = [@{const_name Nibble0}, @{const_name Nibble1},
- @{const_name Nibble2}, @{const_name Nibble3},
- @{const_name Nibble4}, @{const_name Nibble5},
- @{const_name Nibble6}, @{const_name Nibble7},
- @{const_name Nibble8}, @{const_name Nibble9},
- @{const_name NibbleA}, @{const_name NibbleB},
- @{const_name NibbleC}, @{const_name NibbleD},
- @{const_name NibbleE}, @{const_name NibbleF}];
-in
- CodegenSerializer.add_pretty_ml_string "SML"
- charr nibbles @{const_name Nil} @{const_name Cons} @{const_name STR}
-end
-*}
-
-code_reserved SML string
-
-code_const "op = \<Colon> ml_string \<Rightarrow> ml_string \<Rightarrow> bool"
- (SML "!((_ : string) = _)")
-
-end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/ML_String.thy Thu Jul 19 21:47:39 2007 +0200
@@ -0,0 +1,73 @@
+(* ID: $Id$
+ Author: Florian Haftmann, TU Muenchen
+*)
+
+header {* Monolithic strings for ML *}
+
+theory ML_String
+imports List
+begin
+
+subsection {* Motivation *}
+
+text {*
+ Strings are represented in HOL as list of characters.
+ For code generation to Haskell, this is no problem
+ since in Haskell "abc" is equivalent to ['a', 'b', 'c'].
+ On the other hand, in ML all strings have to
+ be represented as list of characters which
+ is awkward to read. This theory provides a distinguished
+ datatype for strings which then by convention
+ are serialized as monolithic ML strings.
+*}
+
+
+subsection {* Datatype of monolithic strings *}
+
+datatype ml_string = STR string
+
+lemmas [code func del] = ml_string.recs ml_string.cases
+
+lemma [code func]: "size (s\<Colon>ml_string) = 0"
+ by (cases s) simp_all
+
+subsection {* ML interface *}
+
+ML {*
+structure ML_String =
+struct
+
+fun mk s = @{term STR} $ HOLogic.mk_string s;
+
+end;
+*}
+
+
+subsection {* Code serialization *}
+
+code_type ml_string
+ (SML "string")
+
+setup {*
+let
+ val charr = @{const_name Char}
+ val nibbles = [@{const_name Nibble0}, @{const_name Nibble1},
+ @{const_name Nibble2}, @{const_name Nibble3},
+ @{const_name Nibble4}, @{const_name Nibble5},
+ @{const_name Nibble6}, @{const_name Nibble7},
+ @{const_name Nibble8}, @{const_name Nibble9},
+ @{const_name NibbleA}, @{const_name NibbleB},
+ @{const_name NibbleC}, @{const_name NibbleD},
+ @{const_name NibbleE}, @{const_name NibbleF}];
+in
+ CodegenSerializer.add_pretty_ml_string "SML"
+ charr nibbles @{const_name Nil} @{const_name Cons} @{const_name STR}
+end
+*}
+
+code_reserved SML string
+
+code_const "op = \<Colon> ml_string \<Rightarrow> ml_string \<Rightarrow> bool"
+ (SML "!((_ : string) = _)")
+
+end
--- a/src/HOL/Library/Pure_term.thy Thu Jul 19 21:47:38 2007 +0200
+++ b/src/HOL/Library/Pure_term.thy Thu Jul 19 21:47:39 2007 +0200
@@ -6,7 +6,7 @@
header {* Embedding (a subset of) the Pure term algebra in HOL *}
theory Pure_term
-imports MLString
+imports ML_String
begin
subsection {* Definitions *}
@@ -47,16 +47,16 @@
structure Pure_term =
struct
-val mk_sort = HOLogic.mk_list @{typ class} o map MLString.mk;
+val mk_sort = HOLogic.mk_list @{typ class} o map ML_String.mk;
fun mk_typ f (Type (tyco, tys)) =
- @{term Type} $ MLString.mk tyco
+ @{term Type} $ ML_String.mk tyco
$ HOLogic.mk_list @{typ typ} (map (mk_typ f) tys)
| mk_typ f (TFree v) =
f v;
fun mk_term f g (Const (c, ty)) =
- @{term Const} $ MLString.mk c $ g ty
+ @{term Const} $ ML_String.mk c $ g ty
| mk_term f g (t1 $ t2) =
@{term App} $ mk_term f g t1 $ mk_term f g t2
| mk_term f g (Free v) = f v;
--- a/src/HOL/Library/SCT_Implementation.thy Thu Jul 19 21:47:38 2007 +0200
+++ b/src/HOL/Library/SCT_Implementation.thy Thu Jul 19 21:47:39 2007 +0200
@@ -6,7 +6,7 @@
header {* Implemtation of the SCT criterion *}
theory SCT_Implementation
-imports ExecutableSet SCT_Definition SCT_Theorem
+imports Executable_Set SCT_Definition SCT_Theorem
begin
fun edges_match :: "('n \<times> 'e \<times> 'n) \<times> ('n \<times> 'e \<times> 'n) \<Rightarrow> bool"
--- a/src/HOL/MicroJava/BV/BVExample.thy Thu Jul 19 21:47:38 2007 +0200
+++ b/src/HOL/MicroJava/BV/BVExample.thy Thu Jul 19 21:47:39 2007 +0200
@@ -6,7 +6,7 @@
header {* \isaheader{Example Welltypings}\label{sec:BVExample} *}
theory BVExample
-imports JVMListExample BVSpecTypeSafe JVM ExecutableSet
+imports JVMListExample BVSpecTypeSafe JVM Executable_Set
begin
text {*
--- a/src/HOL/ex/Codegenerator_Rat.thy Thu Jul 19 21:47:38 2007 +0200
+++ b/src/HOL/ex/Codegenerator_Rat.thy Thu Jul 19 21:47:39 2007 +0200
@@ -6,7 +6,7 @@
header {* Simple example for executable rational numbers *}
theory Codegenerator_Rat
-imports ExecutableRat EfficientNat
+imports Executable_Rat Efficient_Nat
begin
definition
--- a/src/HOL/ex/NBE.thy Thu Jul 19 21:47:38 2007 +0200
+++ b/src/HOL/ex/NBE.thy Thu Jul 19 21:47:39 2007 +0200
@@ -3,7 +3,7 @@
Work in progress
*)
-theory NBE imports Main ExecutableSet begin
+theory NBE imports Main Executable_Set begin
ML"set quick_and_dirty"
--- a/src/HOL/ex/ROOT.ML Thu Jul 19 21:47:38 2007 +0200
+++ b/src/HOL/ex/ROOT.ML Thu Jul 19 21:47:39 2007 +0200
@@ -16,8 +16,8 @@
no_document time_use_thy "Pretty_Int";
time_use_thy "Random";
-no_document time_use_thy "ExecutableRat";
-no_document time_use_thy "EfficientNat";
+no_document time_use_thy "Executable_Rat";
+no_document time_use_thy "Efficient_Nat";
time_use_thy "Codegenerator_Rat";
no_document time_use_thy "Codegenerator";
--- a/src/HOL/ex/Reflected_Presburger.thy Thu Jul 19 21:47:38 2007 +0200
+++ b/src/HOL/ex/Reflected_Presburger.thy Thu Jul 19 21:47:39 2007 +0200
@@ -1,5 +1,5 @@
theory Reflected_Presburger
-imports GCD EfficientNat
+imports GCD Efficient_Nat
uses ("coopereif.ML") ("coopertac.ML")
begin