Quelle  Code_Abstract_Nat.thy

(*  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