(* Title: HOL/Library/Code_Abstract_Nat.thy
Author: Stefan Berghofer, Florian Haftmann, TU Muenchen
*)
section ‹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 🍋‹0::nat
›/
🍋‹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]:
"case_nat = (\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 🍋‹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:
assumes "\n. f (Suc n) \ h n"
assumes "f 0 \ g"
shows "f n \ if n = 0 then g else h (n - 1)"
by (rule eq_reflection) (cases n, insert assms, simp_all)
text ‹
The rule above
is built into a preprocessor that
is plugged into
the code generator.
›
setup ‹
let
val Suc_if_eq =
Thm.incr_indexes 1 @{
thm Suc_if_eq};
fun remove_suc ctxt thms =
let
val vname = singleton (Name.variant_list (map fst
(fold (
Term.add_var_names o
Thm.full_prop_of) thms [])))
"n";
val cv =
Thm.cterm_of ctxt (Var ((vname, 0), HOLogic.natT));
val lhs_of =
Thm.dest_arg1 o
Thm.cprop_of;
val rhs_of =
Thm.dest_arg o
Thm.cprop_of;
fun find_vars ct = (
case Thm.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.
apply ct ct2)) (find_vars ct1) @
map (apfst (
Thm.
apply ct1)) (find_vars ct2)
end
| _ => []);
val eqs = maps
(fn
thm => map (pair
thm) (find_vars (lhs_of
thm))) thms;
fun mk_thms (
thm, (ct, cv
')) =
let
val
thm' =
Thm.implies_elim
(Conv.fconv_rule (
Thm.beta_conversion true)
(
Thm.instantiate
'
[SOME (
Thm.ctyp_of_cterm ct)] [SOME (
Thm.lambda cv ct),
SOME (
Thm.lambda cv
' (rhs_of thm)), NONE, SOME cv']
Suc_if_eq)) (
Thm.forall_intr cv
' thm)
in
case map_filter (fn
thm'' =>
SOME (
thm'', singleton
(Variable.trade (K (fn [
thm'''] => [thm''' RS
thm']))
(Variable.declare_thm
thm'' ctxt))
thm'')
handle
THM _ => NONE) thms of
[] => NONE
| thmps =>
let val (thms1, thms2) = split_list thmps
in SOME (subtract
Thm.eq_thm (
thm :: thms1) thms @ thms2)
end
end
in get_first mk_thms eqs
end;
fun eqn_suc_base_preproc ctxt thms =
let
val dest = fst o Logic.dest_equals o
Thm.prop_of;
val contains_suc = exists_Const (fn (c, _) => c =
🍋‹Suc
›);
in
if forall (can dest) thms andalso exists (contains_suc o dest) thms
then thms |> perhaps_loop (remove_suc ctxt) |> (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
›
subsection ‹Candidates which need special treatment
›
lemma drop_bit_int_code [code]:
‹drop_bit n k = k div 2 ^ n
› for k :: int
by (fact drop_bit_eq_div)
lemma take_bit_num_code [code]:
‹take_bit_num n Num.One =
(
case n of 0
==> None | Suc n
==> Some Num.One)
›
‹take_bit_num n (Num.Bit0 m) =
(
case n of 0
==> None | Suc n
==> (
case take_bit_num n m of None
==> None | Some q
==> Some (Num.Bit0 q)
))›
‹take_bit_num n (Num.Bit1 m) =
(case n of 0 ==> None | Suc n ==> Some (case take_bit_num n m of None ==> Num.One | Some q ==> Num.Bit1 q))›
by (cases n; simp)+
end
