summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/ex/Hex_Bin_Examples.thy

author | nipkow |

Fri Mar 06 17:38:47 2009 +0100 (2009-03-06) | |

changeset 30313 | b2441b0c8d38 |

parent 20866 | bc366b4b6ea4 |

child 41460 | ea56b98aee83 |

permissions | -rw-r--r-- |

added lemmas

1 (* Title: HOL/ex/Hex_Bin_Examples.thy

2 ID: $Id$

3 Author: Gerwin Klein, NICTA

4 *)

6 header {* Examples for hexadecimal and binary numerals *}

8 theory Hex_Bin_Examples imports Main

9 begin

12 text "Hex and bin numerals can be used like normal decimal numerals in input"

13 lemma "0xFF = 255" by (rule refl)

14 lemma "0xF = 0b1111" by (rule refl)

16 text {*

17 Just like decimal numeral they are polymorphic, for arithmetic

18 they need to be constrained

19 *}

20 lemma "0x0A + 0x10 = (0x1A :: nat)" by simp

22 text "The number of leading zeros is irrelevant"

23 lemma "0b00010000 = 0x10" by (rule refl)

25 text "Unary minus works as for decimal numerals"

26 lemma "- 0x0A = - 10" by (rule refl)

28 text {*

29 Hex and bin numerals are printed as decimal: @{term "0b10"}

30 *}

31 term "0b10"

32 term "0x0A"

34 text {*

35 The numerals 0 and 1 are syntactically different from the

36 constants 0 and 1. For the usual numeric types, their values

37 are the same, though.

38 *}

39 lemma "0x01 = 1" oops

40 lemma "0x00 = 0" oops

42 lemma "0x01 = (1::nat)" by simp

43 lemma "0b0000 = (0::int)" by simp

46 end