# HG changeset patch # User haftmann # Date 1360841096 -3600 # Node ID 222fb6cb2c3eaa088a4c08311271efb2aa22e246 # Parent da97167e03f7b2ee7091e76bd2a0c8725d4d21c3 factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions diff -r da97167e03f7 -r 222fb6cb2c3e src/HOL/Library/Code_Abstract_Nat.thy --- /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 = (\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: "(\n. f (Suc n) \ h n) \ f 0 \ g \ + f n \ 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 diff -r da97167e03f7 -r 222fb6cb2c3e src/HOL/Library/Code_Binary_Nat.thy --- 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 = (\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: "(\n. f (Suc n) \ h n) \ f 0 \ g \ - f n \ 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 diff -r da97167e03f7 -r 222fb6cb2c3e src/HOL/Library/Code_Target_Nat.thy --- 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)