haftmann@51113: (*  Title:      HOL/Library/Code_Abstract_Nat.thy
haftmann@51113:     Author:     Stefan Berghofer, Florian Haftmann, TU Muenchen
haftmann@51113: *)
haftmann@51113: 
haftmann@51113: header {* Avoidance of pattern matching on natural numbers *}
haftmann@51113: 
haftmann@51113: theory Code_Abstract_Nat
haftmann@51113: imports Main
haftmann@51113: begin
haftmann@51113: 
haftmann@51113: text {*
haftmann@51113:   When natural numbers are implemented in another than the
haftmann@51113:   conventional inductive @{term "0::nat"}/@{term Suc} representation,
haftmann@51113:   it is necessary to avoid all pattern matching on natural numbers
haftmann@51113:   altogether.  This is accomplished by this theory (up to a certain
haftmann@51113:   extent).
haftmann@51113: *}
haftmann@51113: 
haftmann@51113: subsection {* Case analysis *}
haftmann@51113: 
haftmann@51113: text {*
haftmann@51113:   Case analysis on natural numbers is rephrased using a conditional
haftmann@51113:   expression:
haftmann@51113: *}
haftmann@51113: 
haftmann@51113: lemma [code, code_unfold]:
blanchet@55415:   "case_nat = (\<lambda>f g n. if n = 0 then f else g (n - 1))"
haftmann@51113:   by (auto simp add: fun_eq_iff dest!: gr0_implies_Suc)
haftmann@51113: 
haftmann@51113: 
haftmann@51113: subsection {* Preprocessors *}
haftmann@51113: 
haftmann@51113: text {*
haftmann@51113:   The term @{term "Suc n"} is no longer a valid pattern.  Therefore,
haftmann@51113:   all occurrences of this term in a position where a pattern is
haftmann@51113:   expected (i.e.~on the left-hand side of a code equation) must be
wenzelm@56790:   eliminated.  This can be accomplished -- as far as possible -- by
haftmann@51113:   applying the following transformation rule:
haftmann@51113: *}
haftmann@51113: 
haftmann@57426: lemma Suc_if_eq:
haftmann@57426:   assumes "\<And>n. f (Suc n) \<equiv> h n"
haftmann@57426:   assumes "f 0 \<equiv> g"
haftmann@57426:   shows "f n \<equiv> if n = 0 then g else h (n - 1)"
haftmann@57426:   by (rule eq_reflection) (cases n, insert assms, simp_all)
haftmann@51113: 
haftmann@51113: text {*
haftmann@51113:   The rule above is built into a preprocessor that is plugged into
haftmann@51113:   the code generator.
haftmann@51113: *}
haftmann@51113: 
haftmann@51113: setup {*
haftmann@51113: let
haftmann@51113: 
haftmann@57427: val Suc_if_eq = Thm.incr_indexes 1 @{thm Suc_if_eq};
haftmann@57427: 
haftmann@55757: fun remove_suc ctxt thms =
haftmann@51113:   let
haftmann@55757:     val thy = Proof_Context.theory_of ctxt;
haftmann@51113:     val vname = singleton (Name.variant_list (map fst
haftmann@51113:       (fold (Term.add_var_names o Thm.full_prop_of) thms []))) "n";
haftmann@51113:     val cv = cterm_of thy (Var ((vname, 0), HOLogic.natT));
haftmann@57426:     val lhs_of = snd o Thm.dest_comb o fst o Thm.dest_comb o cprop_of;
haftmann@57426:     val rhs_of = snd o Thm.dest_comb o cprop_of;
haftmann@51113:     fun find_vars ct = (case term_of ct of
haftmann@51113:         (Const (@{const_name Suc}, _) $ Var _) => [(cv, snd (Thm.dest_comb ct))]
haftmann@51113:       | _ $ _ =>
haftmann@51113:         let val (ct1, ct2) = Thm.dest_comb ct
haftmann@51113:         in 
haftmann@51113:           map (apfst (fn ct => Thm.apply ct ct2)) (find_vars ct1) @
haftmann@51113:           map (apfst (Thm.apply ct1)) (find_vars ct2)
haftmann@51113:         end
haftmann@51113:       | _ => []);
haftmann@51113:     val eqs = maps
haftmann@57426:       (fn thm => map (pair thm) (find_vars (lhs_of thm))) thms;
haftmann@57426:     fun mk_thms (thm, (ct, cv')) =
haftmann@51113:       let
haftmann@57426:         val thm' =
haftmann@51113:           Thm.implies_elim
haftmann@51113:            (Conv.fconv_rule (Thm.beta_conversion true)
haftmann@51113:              (Drule.instantiate'
haftmann@51113:                [SOME (ctyp_of_term ct)] [SOME (Thm.lambda cv ct),
haftmann@57426:                  SOME (Thm.lambda cv' (rhs_of thm)), NONE, SOME cv']
haftmann@57427:                Suc_if_eq)) (Thm.forall_intr cv' thm)
haftmann@51113:       in
haftmann@57426:         case map_filter (fn thm'' =>
haftmann@57426:             SOME (thm'', singleton
haftmann@57426:               (Variable.trade (K (fn [thm'''] => [thm''' RS thm']))
haftmann@57426:                 (Variable.global_thm_context thm'')) thm'')
haftmann@51113:           handle THM _ => NONE) thms of
haftmann@51113:             [] => NONE
haftmann@57426:           | thmps =>
haftmann@57426:               let val (thms1, thms2) = split_list thmps
haftmann@57426:               in SOME (subtract Thm.eq_thm (thm :: thms1) thms @ thms2) end
haftmann@51113:       end
haftmann@51113:   in get_first mk_thms eqs end;
haftmann@51113: 
haftmann@51113: fun eqn_suc_base_preproc thy thms =
haftmann@51113:   let
haftmann@51113:     val dest = fst o Logic.dest_equals o prop_of;
haftmann@51113:     val contains_suc = exists_Const (fn (c, _) => c = @{const_name Suc});
haftmann@51113:   in
haftmann@51113:     if forall (can dest) thms andalso exists (contains_suc o dest) thms
haftmann@51113:       then thms |> perhaps_loop (remove_suc thy) |> (Option.map o map) Drule.zero_var_indexes
haftmann@51113:        else NONE
haftmann@51113:   end;
haftmann@51113: 
haftmann@51113: val eqn_suc_preproc = Code_Preproc.simple_functrans eqn_suc_base_preproc;
haftmann@51113: 
haftmann@51113: in
haftmann@51113: 
haftmann@51113:   Code_Preproc.add_functrans ("eqn_Suc", eqn_suc_preproc)
haftmann@51113: 
haftmann@51113: end;
haftmann@51113: *}
haftmann@51113: 
haftmann@51113: end