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

src/HOL/ex/Hex_Bin_Examples.thy

author | wenzelm |

Sun Nov 02 18:21:45 2014 +0100 (2014-11-02) | |

changeset 58889 | 5b7a9633cfa8 |

parent 41460 | ea56b98aee83 |

child 61343 | 5b5656a63bd6 |

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

modernized header uniformly as section;

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

2 Author: Gerwin Klein, NICTA

3 *)

5 section {* Examples for hexadecimal and binary numerals *}

7 theory Hex_Bin_Examples imports Main

8 begin

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

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

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

15 text {*

16 Just like decimal numeral they are polymorphic, for arithmetic

17 they need to be constrained

18 *}

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

21 text "The number of leading zeros is irrelevant"

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

24 text "Unary minus works as for decimal numerals"

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

27 text {*

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

29 *}

30 term "0b10"

31 term "0x0A"

33 text {*

34 The numerals 0 and 1 are syntactically different from the

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

36 are the same, though.

37 *}

38 lemma "0x01 = 1" oops

39 lemma "0x00 = 0" oops

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

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

45 end