factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Code_Abstract_Nat.thy Thu Feb 14 12:24:56 2013 +0100
@@ -0,0 +1,113 @@
+(* Title: HOL/Library/Code_Abstract_Nat.thy
+ Author: Stefan Berghofer, Florian Haftmann, TU Muenchen
+*)
+
+header {* Avoidance of pattern matching on natural numbers *}
+
+theory Code_Abstract_Nat
+imports Main
+begin
+
+text {*
+ When natural numbers are implemented in another than the
+ conventional inductive @{term "0::nat"}/@{term Suc} representation,
+ it is necessary to avoid all pattern matching on natural numbers
+ altogether. This is accomplished by this theory (up to a certain
+ extent).
+*}
+
+subsection {* Case analysis *}
+
+text {*
+ Case analysis on natural numbers is rephrased using a conditional
+ expression:
+*}
+
+lemma [code, code_unfold]:
+ "nat_case = (\<lambda>f g n. if n = 0 then f else g (n - 1))"
+ by (auto simp add: fun_eq_iff dest!: gr0_implies_Suc)
+
+
+subsection {* Preprocessors *}
+
+text {*
+ The term @{term "Suc n"} is no longer a valid pattern. Therefore,
+ all occurrences of this term in a position where a pattern is
+ expected (i.e.~on the left-hand side of a code equation) must be
+ eliminated. This can be accomplished – as far as possible – by
+ applying the following transformation rule:
+*}
+
+lemma Suc_if_eq: "(\<And>n. f (Suc n) \<equiv> h n) \<Longrightarrow> f 0 \<equiv> g \<Longrightarrow>
+ f n \<equiv> if n = 0 then g else h (n - 1)"
+ by (rule eq_reflection) (cases n, simp_all)
+
+text {*
+ The rule above is built into a preprocessor that is plugged into
+ the code generator.
+*}
+
+setup {*
+let
+
+fun remove_suc thy thms =
+ let
+ val vname = singleton (Name.variant_list (map fst
+ (fold (Term.add_var_names o Thm.full_prop_of) thms []))) "n";
+ val cv = cterm_of thy (Var ((vname, 0), HOLogic.natT));
+ fun lhs_of th = snd (Thm.dest_comb
+ (fst (Thm.dest_comb (cprop_of th))));
+ fun rhs_of th = snd (Thm.dest_comb (cprop_of th));
+ fun find_vars ct = (case term_of ct of
+ (Const (@{const_name Suc}, _) $ Var _) => [(cv, snd (Thm.dest_comb ct))]
+ | _ $ _ =>
+ let val (ct1, ct2) = Thm.dest_comb ct
+ in
+ map (apfst (fn ct => Thm.apply ct ct2)) (find_vars ct1) @
+ map (apfst (Thm.apply ct1)) (find_vars ct2)
+ end
+ | _ => []);
+ val eqs = maps
+ (fn th => map (pair th) (find_vars (lhs_of th))) thms;
+ fun mk_thms (th, (ct, cv')) =
+ let
+ val th' =
+ Thm.implies_elim
+ (Conv.fconv_rule (Thm.beta_conversion true)
+ (Drule.instantiate'
+ [SOME (ctyp_of_term ct)] [SOME (Thm.lambda cv ct),
+ SOME (Thm.lambda cv' (rhs_of th)), NONE, SOME cv']
+ @{thm Suc_if_eq})) (Thm.forall_intr cv' th)
+ in
+ case map_filter (fn th'' =>
+ SOME (th'', singleton
+ (Variable.trade (K (fn [th'''] => [th''' RS th']))
+ (Variable.global_thm_context th'')) th'')
+ handle THM _ => NONE) thms of
+ [] => NONE
+ | thps =>
+ let val (ths1, ths2) = split_list thps
+ in SOME (subtract Thm.eq_thm (th :: ths1) thms @ ths2) end
+ end
+ in get_first mk_thms eqs end;
+
+fun eqn_suc_base_preproc thy thms =
+ let
+ val dest = fst o Logic.dest_equals o prop_of;
+ val contains_suc = exists_Const (fn (c, _) => c = @{const_name Suc});
+ in
+ if forall (can dest) thms andalso exists (contains_suc o dest) thms
+ then thms |> perhaps_loop (remove_suc thy) |> (Option.map o map) Drule.zero_var_indexes
+ else NONE
+ end;
+
+val eqn_suc_preproc = Code_Preproc.simple_functrans eqn_suc_base_preproc;
+
+in
+
+ Code_Preproc.add_functrans ("eqn_Suc", eqn_suc_preproc)
+
+end;
+*}
+
+end
--- a/src/HOL/Library/Code_Binary_Nat.thy Thu Feb 14 12:24:42 2013 +0100
+++ b/src/HOL/Library/Code_Binary_Nat.thy Thu Feb 14 12:24:56 2013 +0100
@@ -1,11 +1,11 @@
(* Title: HOL/Library/Code_Binary_Nat.thy
- Author: Stefan Berghofer, Florian Haftmann, TU Muenchen
+ Author: Florian Haftmann, TU Muenchen
*)
header {* Implementation of natural numbers as binary numerals *}
theory Code_Binary_Nat
-imports Main
+imports Code_Abstract_Nat
begin
text {*
@@ -146,104 +146,6 @@
by (simp_all add: nat_of_num_numeral)
-subsection {* Case analysis *}
-
-text {*
- Case analysis on natural numbers is rephrased using a conditional
- expression:
-*}
-
-lemma [code, code_unfold]:
- "nat_case = (\<lambda>f g n. if n = 0 then f else g (n - 1))"
- by (auto simp add: fun_eq_iff dest!: gr0_implies_Suc)
-
-
-subsection {* Preprocessors *}
-
-text {*
- The term @{term "Suc n"} is no longer a valid pattern.
- Therefore, all occurrences of this term in a position
- where a pattern is expected (i.e.~on the left-hand side of a recursion
- equation) must be eliminated.
- This can be accomplished by applying the following transformation rules:
-*}
-
-lemma Suc_if_eq: "(\<And>n. f (Suc n) \<equiv> h n) \<Longrightarrow> f 0 \<equiv> g \<Longrightarrow>
- f n \<equiv> if n = 0 then g else h (n - 1)"
- by (rule eq_reflection) (cases n, simp_all)
-
-text {*
- The rules above are built into a preprocessor that is plugged into
- the code generator. Since the preprocessor for introduction rules
- does not know anything about modes, some of the modes that worked
- for the canonical representation of natural numbers may no longer work.
-*}
-
-(*<*)
-setup {*
-let
-
-fun remove_suc thy thms =
- let
- val vname = singleton (Name.variant_list (map fst
- (fold (Term.add_var_names o Thm.full_prop_of) thms []))) "n";
- val cv = cterm_of thy (Var ((vname, 0), HOLogic.natT));
- fun lhs_of th = snd (Thm.dest_comb
- (fst (Thm.dest_comb (cprop_of th))));
- fun rhs_of th = snd (Thm.dest_comb (cprop_of th));
- fun find_vars ct = (case term_of ct of
- (Const (@{const_name Suc}, _) $ Var _) => [(cv, snd (Thm.dest_comb ct))]
- | _ $ _ =>
- let val (ct1, ct2) = Thm.dest_comb ct
- in
- map (apfst (fn ct => Thm.apply ct ct2)) (find_vars ct1) @
- map (apfst (Thm.apply ct1)) (find_vars ct2)
- end
- | _ => []);
- val eqs = maps
- (fn th => map (pair th) (find_vars (lhs_of th))) thms;
- fun mk_thms (th, (ct, cv')) =
- let
- val th' =
- Thm.implies_elim
- (Conv.fconv_rule (Thm.beta_conversion true)
- (Drule.instantiate'
- [SOME (ctyp_of_term ct)] [SOME (Thm.lambda cv ct),
- SOME (Thm.lambda cv' (rhs_of th)), NONE, SOME cv']
- @{thm Suc_if_eq})) (Thm.forall_intr cv' th)
- in
- case map_filter (fn th'' =>
- SOME (th'', singleton
- (Variable.trade (K (fn [th'''] => [th''' RS th']))
- (Variable.global_thm_context th'')) th'')
- handle THM _ => NONE) thms of
- [] => NONE
- | thps =>
- let val (ths1, ths2) = split_list thps
- in SOME (subtract Thm.eq_thm (th :: ths1) thms @ ths2) end
- end
- in get_first mk_thms eqs end;
-
-fun eqn_suc_base_preproc thy thms =
- let
- val dest = fst o Logic.dest_equals o prop_of;
- val contains_suc = exists_Const (fn (c, _) => c = @{const_name Suc});
- in
- if forall (can dest) thms andalso exists (contains_suc o dest) thms
- then thms |> perhaps_loop (remove_suc thy) |> (Option.map o map) Drule.zero_var_indexes
- else NONE
- end;
-
-val eqn_suc_preproc = Code_Preproc.simple_functrans eqn_suc_base_preproc;
-
-in
-
- Code_Preproc.add_functrans ("eqn_Suc", eqn_suc_preproc)
-
-end;
-*}
-(*>*)
-
code_modulename SML
Code_Binary_Nat Arith
--- a/src/HOL/Library/Code_Target_Nat.thy Thu Feb 14 12:24:42 2013 +0100
+++ b/src/HOL/Library/Code_Target_Nat.thy Thu Feb 14 12:24:56 2013 +0100
@@ -1,11 +1,11 @@
(* Title: HOL/Library/Code_Target_Nat.thy
- Author: Stefan Berghofer, Florian Haftmann, TU Muenchen
+ Author: Florian Haftmann, TU Muenchen
*)
header {* Implementation of natural numbers by target-language integers *}
theory Code_Target_Nat
-imports Main Code_Numeral_Types Code_Binary_Nat
+imports Code_Abstract_Nat Code_Numeral_Types
begin
subsection {* Implementation for @{typ nat} *}
@@ -52,18 +52,15 @@
"integer_of_nat 1 = 1"
by (simp add: integer_eq_iff integer_of_nat_def)
+lemma [code]:
+ "Suc n = n + 1"
+ by simp
+
lemma [code abstract]:
"integer_of_nat (m + n) = of_nat m + of_nat n"
by (simp add: integer_eq_iff integer_of_nat_def)
lemma [code abstract]:
- "integer_of_nat (Code_Binary_Nat.dup n) = Code_Numeral_Types.dup (of_nat n)"
- by (simp add: integer_eq_iff Code_Binary_Nat.dup_def integer_of_nat_def)
-
-lemma [code, code del]:
- "Code_Binary_Nat.sub = Code_Binary_Nat.sub" ..
-
-lemma [code abstract]:
"integer_of_nat (m - n) = max 0 (of_nat m - of_nat n)"
by (simp add: integer_eq_iff integer_of_nat_def)