src/HOL/Library/Code_Abstract_Nat.thy
 author wenzelm Mon Dec 28 17:43:30 2015 +0100 (2015-12-28) changeset 61952 546958347e05 parent 60801 7664e0916eec child 69216 1a52baa70aed permissions -rw-r--r--
prefer symbols for "Union", "Inter";
 haftmann@51113 1 (* Title: HOL/Library/Code_Abstract_Nat.thy haftmann@51113 2 Author: Stefan Berghofer, Florian Haftmann, TU Muenchen haftmann@51113 3 *) haftmann@51113 4 wenzelm@60500 5 section \Avoidance of pattern matching on natural numbers\ haftmann@51113 6 haftmann@51113 7 theory Code_Abstract_Nat haftmann@51113 8 imports Main haftmann@51113 9 begin haftmann@51113 10 wenzelm@60500 11 text \ haftmann@51113 12 When natural numbers are implemented in another than the haftmann@51113 13 conventional inductive @{term "0::nat"}/@{term Suc} representation, haftmann@51113 14 it is necessary to avoid all pattern matching on natural numbers haftmann@51113 15 altogether. This is accomplished by this theory (up to a certain haftmann@51113 16 extent). wenzelm@60500 17 \ haftmann@51113 18 wenzelm@60500 19 subsection \Case analysis\ haftmann@51113 20 wenzelm@60500 21 text \ haftmann@51113 22 Case analysis on natural numbers is rephrased using a conditional haftmann@51113 23 expression: wenzelm@60500 24 \ haftmann@51113 25 haftmann@51113 26 lemma [code, code_unfold]: blanchet@55415 27 "case_nat = (\f g n. if n = 0 then f else g (n - 1))" haftmann@51113 28 by (auto simp add: fun_eq_iff dest!: gr0_implies_Suc) haftmann@51113 29 haftmann@51113 30 wenzelm@60500 31 subsection \Preprocessors\ haftmann@51113 32 wenzelm@60500 33 text \ haftmann@51113 34 The term @{term "Suc n"} is no longer a valid pattern. Therefore, haftmann@51113 35 all occurrences of this term in a position where a pattern is haftmann@51113 36 expected (i.e.~on the left-hand side of a code equation) must be wenzelm@56790 37 eliminated. This can be accomplished -- as far as possible -- by haftmann@51113 38 applying the following transformation rule: wenzelm@60500 39 \ haftmann@51113 40 haftmann@57426 41 lemma Suc_if_eq: haftmann@57426 42 assumes "\n. f (Suc n) \ h n" haftmann@57426 43 assumes "f 0 \ g" haftmann@57426 44 shows "f n \ if n = 0 then g else h (n - 1)" haftmann@57426 45 by (rule eq_reflection) (cases n, insert assms, simp_all) haftmann@51113 46 wenzelm@60500 47 text \ haftmann@51113 48 The rule above is built into a preprocessor that is plugged into haftmann@51113 49 the code generator. wenzelm@60500 50 \ haftmann@51113 51 wenzelm@60500 52 setup \ haftmann@51113 53 let haftmann@51113 54 haftmann@57427 55 val Suc_if_eq = Thm.incr_indexes 1 @{thm Suc_if_eq}; haftmann@57427 56 haftmann@55757 57 fun remove_suc ctxt thms = haftmann@51113 58 let haftmann@51113 59 val vname = singleton (Name.variant_list (map fst haftmann@51113 60 (fold (Term.add_var_names o Thm.full_prop_of) thms []))) "n"; wenzelm@59643 61 val cv = Thm.cterm_of ctxt (Var ((vname, 0), HOLogic.natT)); wenzelm@59582 62 val lhs_of = snd o Thm.dest_comb o fst o Thm.dest_comb o Thm.cprop_of; wenzelm@59582 63 val rhs_of = snd o Thm.dest_comb o Thm.cprop_of; wenzelm@59582 64 fun find_vars ct = (case Thm.term_of ct of haftmann@51113 65 (Const (@{const_name Suc}, _) \$ Var _) => [(cv, snd (Thm.dest_comb ct))] haftmann@51113 66 | _ \$ _ => haftmann@51113 67 let val (ct1, ct2) = Thm.dest_comb ct haftmann@51113 68 in haftmann@51113 69 map (apfst (fn ct => Thm.apply ct ct2)) (find_vars ct1) @ haftmann@51113 70 map (apfst (Thm.apply ct1)) (find_vars ct2) haftmann@51113 71 end haftmann@51113 72 | _ => []); haftmann@51113 73 val eqs = maps haftmann@57426 74 (fn thm => map (pair thm) (find_vars (lhs_of thm))) thms; haftmann@57426 75 fun mk_thms (thm, (ct, cv')) = haftmann@51113 76 let haftmann@57426 77 val thm' = haftmann@51113 78 Thm.implies_elim haftmann@51113 79 (Conv.fconv_rule (Thm.beta_conversion true) wenzelm@60801 80 (Thm.instantiate' wenzelm@59586 81 [SOME (Thm.ctyp_of_cterm ct)] [SOME (Thm.lambda cv ct), haftmann@57426 82 SOME (Thm.lambda cv' (rhs_of thm)), NONE, SOME cv'] haftmann@57427 83 Suc_if_eq)) (Thm.forall_intr cv' thm) haftmann@51113 84 in haftmann@57426 85 case map_filter (fn thm'' => haftmann@57426 86 SOME (thm'', singleton haftmann@57426 87 (Variable.trade (K (fn [thm'''] => [thm''' RS thm'])) wenzelm@59169 88 (Variable.declare_thm thm'' ctxt)) thm'') haftmann@51113 89 handle THM _ => NONE) thms of haftmann@51113 90 [] => NONE haftmann@57426 91 | thmps => haftmann@57426 92 let val (thms1, thms2) = split_list thmps haftmann@57426 93 in SOME (subtract Thm.eq_thm (thm :: thms1) thms @ thms2) end haftmann@51113 94 end haftmann@51113 95 in get_first mk_thms eqs end; haftmann@51113 96 wenzelm@59169 97 fun eqn_suc_base_preproc ctxt thms = haftmann@51113 98 let wenzelm@59582 99 val dest = fst o Logic.dest_equals o Thm.prop_of; haftmann@51113 100 val contains_suc = exists_Const (fn (c, _) => c = @{const_name Suc}); haftmann@51113 101 in haftmann@51113 102 if forall (can dest) thms andalso exists (contains_suc o dest) thms wenzelm@59169 103 then thms |> perhaps_loop (remove_suc ctxt) |> (Option.map o map) Drule.zero_var_indexes haftmann@51113 104 else NONE haftmann@51113 105 end; haftmann@51113 106 haftmann@51113 107 val eqn_suc_preproc = Code_Preproc.simple_functrans eqn_suc_base_preproc; haftmann@51113 108 haftmann@51113 109 in haftmann@51113 110 haftmann@51113 111 Code_Preproc.add_functrans ("eqn_Suc", eqn_suc_preproc) haftmann@51113 112 haftmann@51113 113 end; wenzelm@60500 114 \ haftmann@51113 115 haftmann@51113 116 end