src/HOL/Word/WordMain.thy
author kleing
Mon, 20 Aug 2007 04:34:31 +0200
changeset 24333 e77ea0ea7f2c
child 24350 4d74f37c6367
permissions -rw-r--r--
* HOL-Word: New extensive library and type for generic, fixed size machine words, with arithemtic, bit-wise, shifting and rotating operations, reflection into int, nat, and bool lists, automation for linear arithmetic (by automatic reflection into nat or int), including lemmas on overflow and monotonicity. Instantiated to all appropriate arithmetic type classes, supporting automatic simplification of numerals on all operations. Jointly developed by NICTA, Galois, and PSU. * still to do: README.html/document + moving some of the generic lemmas to appropriate place in distribution
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
     1
(* 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
     2
  ID:     $Id$
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
     3
  Author: Gerwin Klein, NICTA
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
     4
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
     5
  The main interface of the word library to other theories.
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
     6
*)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
     7
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
     8
theory WordMain imports WordGenLib
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
     9
begin
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    10
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    11
lemmas word_no_1 [simp] = word_1_no [symmetric]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    12
lemmas word_no_0 [simp] = word_0_no [symmetric]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    13
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    14
declare word_0_bl [simp]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    15
declare bin_to_bl_def [simp]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    16
declare to_bl_0 [simp]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    17
declare of_bl_True [simp]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    18
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    19
text "Examples"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    20
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    21
types word32 = "32 word"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    22
types word8 = "8 word"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    23
types byte = word8
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    24
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    25
text {* for more see WordExampes.thy *}
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    26
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    27
end