# HG changeset patch # User haftmann # Date 1155017984 -7200 # Node ID 50aaae6ae4db639ad1d4a20cd08480c19d53c7ab # Parent 0bfdbbe657eb2c7f7d332c7c686dd20d7c5173ce cleanup code generation for Numerals diff -r 0bfdbbe657eb -r 50aaae6ae4db src/HOL/Integ/IntArith.thy --- a/src/HOL/Integ/IntArith.thy Tue Aug 08 08:19:39 2006 +0200 +++ b/src/HOL/Integ/IntArith.thy Tue Aug 08 08:19:44 2006 +0200 @@ -361,6 +361,96 @@ apply (frule pos_zmult_eq_1_iff_lemma, auto) done + +subsection {* code generator setup *} + +code_alias + "Numeral.bin" "IntDef.bin" + "Numeral.bit" "IntDef.bit" + "Numeral.Pls" "IntDef.Pls" + "Numeral.Min" "IntDef.Min" + "Numeral.Bit" "IntDef.Bit" + "Numeral.Abs_Bin" "IntDef.Bin" + "Numeral.Rep_Bin" "IntDef.int_of_bin" + "Numeral.B0" "IntDef.B0" + "Numeral.B1" "IntDef.B1" + +lemma + number_of_is_rep_bin [code inline]: "number_of = Rep_Bin" +proof + fix b + show "number_of b = Rep_Bin b" + unfolding int_number_of_def by simp +qed + +lemma zero_is_num_zero [code, code inline]: + "(0::int) = Rep_Bin Numeral.Pls" + unfolding Pls_def Abs_Bin_inverse' .. + +lemma one_is_num_one [code, code inline]: + "(1::int) = Rep_Bin (Numeral.Pls BIT bit.B1)" + unfolding Pls_def Bit_def Abs_Bin_inverse' by simp + +lemma negate_bin_minus: + "(Rep_Bin b :: int) = - Rep_Bin (bin_minus b)" + unfolding bin_minus_def Abs_Bin_inverse' by simp + +lemmas [code inline] = + bin_minus_Pls bin_minus_Min bin_minus_1 bin_minus_0 + bin_pred_Pls bin_pred_Min bin_pred_1 bin_pred_0 + +ML {* +structure Numeral = +struct + +val negate_bin_minus_thm = eq_reflection OF [thm "negate_bin_minus"]; +val number_of_is_rep_bin_thm = eq_reflection OF [thm "number_of_is_rep_bin"]; + +fun int_of_numeral thy num = HOLogic.dest_binum num + handle TERM _ + => error ("not a number: " ^ Sign.string_of_term thy num); + +fun elim_negate thy thms = + let + val thms' = map (rewrite_rule [number_of_is_rep_bin_thm]) thms; + fun bins_of (Const _) = + I + | bins_of (Var _) = + I + | bins_of (Free _) = + I + | bins_of (Bound _) = + I + | bins_of (Abs (_, _, t)) = + bins_of t + | bins_of (t as _ $ _) = + case strip_comb t + of (Const ("Numeral.Rep_Bin", _), [bin]) => cons bin + | (t', ts) => bins_of t' #> fold bins_of ts; + fun is_negative bin = case try HOLogic.dest_binum bin + of SOME i => i < 0 + | _ => false; + fun instantiate_with bin = + Drule.instantiate' [] [(SOME o cterm_of thy) bin] negate_bin_minus_thm; + val rewrites = + [] + |> fold (bins_of o prop_of) thms' + |> filter is_negative + |> map instantiate_with + in if null rewrites then thms' else + thms' + |> map (rewrite_rule rewrites) + end; + +end; +*} + +setup {* + CodegenTheorems.add_preproc Numeral.elim_negate + #> CodegenPackage.add_appconst ("Numeral.Rep_Bin", CodegenPackage.appgen_rep_bin Numeral.int_of_numeral) +*} + + subsection {* legacy ML bindings *} ML diff -r 0bfdbbe657eb -r 50aaae6ae4db src/HOL/Integ/IntDef.thy --- a/src/HOL/Integ/IntDef.thy Tue Aug 08 08:19:39 2006 +0200 +++ b/src/HOL/Integ/IntDef.thy Tue Aug 08 08:19:44 2006 +0200 @@ -924,23 +924,6 @@ haskell (infix 4 "<=") ML {* -fun mk_int_to_nat bin = - Const ("IntDef.nat", HOLogic.intT --> HOLogic.natT) - $ (Const ("Numeral.number_of", HOLogic.binT --> HOLogic.intT) $ bin); - -fun bin_to_int thy bin = HOLogic.dest_binum bin - handle TERM _ - => error ("not a number: " ^ Sign.string_of_term thy bin); - -fun appgen_number thy tabs (app as ((_, ty), _)) = - let - val _ = case strip_type ty - of (_, Type (ty', [])) => if ty' = "IntDef.int" then () - else error ("not integer type: " ^ quote ty'); - in - CodegenPackage.appgen_number_of bin_to_int thy tabs app - end; - fun number_of_codegen thy defs gr dep module b (Const ("Numeral.number_of", Type ("fun", [_, T as Type ("IntDef.int", [])])) $ bin) = (SOME (fst (Codegen.invoke_tycodegen thy defs dep module false (gr, T)), @@ -951,12 +934,10 @@ Const ("IntDef.nat", HOLogic.intT --> HOLogic.natT) $ (Const ("Numeral.number_of", HOLogic.binT --> HOLogic.intT) $ bin))) | number_of_codegen _ _ _ _ _ _ _ = NONE; - *} setup {* Codegen.add_codegen "number_of_codegen" number_of_codegen - (* #> CodegenPackage.add_appconst ("Numeral.number_of", appgen_number) *) *} quickcheck_params [default_type = int] diff -r 0bfdbbe657eb -r 50aaae6ae4db src/HOL/Integ/NatBin.thy --- a/src/HOL/Integ/NatBin.thy Tue Aug 08 08:19:39 2006 +0200 +++ b/src/HOL/Integ/NatBin.thy Tue Aug 08 08:19:44 2006 +0200 @@ -776,71 +776,13 @@ "(k*m) div (k*n) = (if k = (0::nat) then 0 else m div n)" by (simp add: nat_mult_div_cancel1) + subsection {* code generator setup *} -lemma elim_nat [code inline]: - "(number_of n :: nat) = nat (number_of n)" - by simp - -lemma elim_zero [code inline]: - "(0::int) = number_of (Numeral.Pls)" - by simp - -lemma elim_one [code inline]: - "(1::int) = number_of (Numeral.Pls BIT bit.B1)" - by simp - -lemma elim_one_nat [code inline]: - "1 = Suc 0" - by simp - -lemmas [code inline] = - bin_minus_Pls bin_minus_Min bin_minus_1 bin_minus_0 - bin_pred_Pls bin_pred_Min bin_pred_1 bin_pred_0 - -lemma elim_negate: - "(number_of n :: int) == - number_of (bin_minus n)" - unfolding number_of_minus IntDef.zminus_zminus by (rule reflexive) +lemma number_of_is_nat_rep_bin [code inline]: + "(number_of b :: nat) = nat (Rep_Bin b)" + unfolding nat_number_of_def int_number_of_def by simp -ML {* -local - val elim_negate_thm = thm "elim_negate"; -in fun elim_negate thy thms = - let - fun bins_of (Const _) = - I - | bins_of (Var _) = - I - | bins_of (Free _) = - I - | bins_of (Bound _) = - I - | bins_of (Abs (_, _, t)) = - bins_of t - | bins_of (t as _ $ _) = - case strip_comb t - of (Const ("Numeral.number_of", _), [bin]) => cons bin - | (t', ts) => bins_of t' #> fold bins_of ts; - fun is_negative bin = case try HOLogic.dest_binum bin - of SOME i => i < 0 - | _ => false; - fun instantiate_with bin = - Drule.instantiate' [] [(SOME o cterm_of thy) bin] elim_negate_thm; - val rewrites = - [] - |> fold (bins_of o prop_of) thms - |> filter is_negative - |> map instantiate_with - in - thms - |> map (rewrite_rule rewrites) - end; -end; (*local*) -*} - -setup {* - CodegenTheorems.add_preproc elim_negate -*} subsection {* legacy ML bindings *} diff -r 0bfdbbe657eb -r 50aaae6ae4db src/HOL/Integ/Numeral.thy --- a/src/HOL/Integ/Numeral.thy Tue Aug 08 08:19:39 2006 +0200 +++ b/src/HOL/Integ/Numeral.thy Tue Aug 08 08:19:44 2006 +0200 @@ -27,7 +27,6 @@ bin = "UNIV::int set" by (auto) - text{*This datatype avoids the use of type @{typ bool}, which would make all of the rewrite rules higher-order. If the use of datatype causes problems, this two-element type can easily be formalized using typedef.*} @@ -87,6 +86,9 @@ bin_mult :: "[bin,bin]=>bin" "bin_mult v w == Abs_Bin(Rep_Bin v * Rep_Bin w)" +lemma Abs_Bin_inverse': + "Rep_Bin (Abs_Bin x) = x" +by (rule Abs_Bin_inverse) (auto simp add: Bin_def) lemmas Bin_simps = bin_succ_def bin_pred_def bin_minus_def bin_add_def bin_mult_def diff -r 0bfdbbe657eb -r 50aaae6ae4db src/HOL/List.thy --- a/src/HOL/List.thy Tue Aug 08 08:19:39 2006 +0200 +++ b/src/HOL/List.thy Tue Aug 08 08:19:44 2006 +0200 @@ -2726,7 +2726,6 @@ val list_codegen_setup = Codegen.add_codegen "list_codegen" list_codegen #> Codegen.add_codegen "char_codegen" char_codegen - #> CodegenPackage.add_appconst ("Numeral.number_of", appgen_number) #> fold (CodegenPackage.add_pretty_list "Nil" "Cons") [ ("ml", (7, "::")), ("haskell", (5, ":")) diff -r 0bfdbbe657eb -r 50aaae6ae4db src/HOL/Nat.thy --- a/src/HOL/Nat.thy Tue Aug 08 08:19:39 2006 +0200 +++ b/src/HOL/Nat.thy Tue Aug 08 08:19:44 2006 +0200 @@ -1043,6 +1043,10 @@ subsection {* Code generator setup *} +lemma one_is_suc_zero [code inline]: + "1 = Suc 0" + by simp + code_alias "nat" "Nat.nat" "0" "Nat.Zero"