author | berghofe |
Fri, 01 Jul 2005 13:54:12 +0200 | |
changeset 16633 | 208ebc9311f2 |
parent 16486 | 1a12cdb6ee6b |
child 17876 | b9c92f384109 |
permissions | -rw-r--r-- |
14494
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
1 |
(* Title: HOL/Library/word_setup.ML |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
2 |
ID: $Id$ |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
3 |
Author: Sebastian Skalberg (TU Muenchen) |
15013 | 4 |
|
5 |
comments containing lcp are the removal of fast_bv_of_nat. |
|
14494
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
6 |
*) |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
7 |
|
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
8 |
local |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
9 |
fun is_const_bool (Const("True",_)) = true |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
10 |
| is_const_bool (Const("False",_)) = true |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
11 |
| is_const_bool _ = false |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
12 |
fun is_const_bit (Const("Word.bit.Zero",_)) = true |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
13 |
| is_const_bit (Const("Word.bit.One",_)) = true |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
14 |
| is_const_bit _ = false |
15013 | 15 |
fun num_is_usable (Const("Numeral.Pls",_)) = true |
16 |
| num_is_usable (Const("Numeral.Min",_)) = false |
|
17 |
| num_is_usable (Const("Numeral.Bit",_) $ w $ b) = |
|
14494
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
18 |
num_is_usable w andalso is_const_bool b |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
19 |
| num_is_usable _ = false |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
20 |
fun vec_is_usable (Const("List.list.Nil",_)) = true |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
21 |
| vec_is_usable (Const("List.list.Cons",_) $ b $ bs) = |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
22 |
vec_is_usable bs andalso is_const_bit b |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
23 |
| vec_is_usable _ = false |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
24 |
fun add_word thy = |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
25 |
let |
15013 | 26 |
(*lcp** val fast1_th = PureThy.get_thm thy "Word.fast_nat_to_bv_def"**) |
16486 | 27 |
val fast2_th = PureThy.get_thm thy (Name "Word.fast_bv_to_nat_def") |
15013 | 28 |
(*lcp** fun f sg thms (Const("Word.nat_to_bv",_) $ (Const("Numeral.number_of",_) $ t)) = |
14494
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
29 |
if num_is_usable t |
15531 | 30 |
then SOME (Drule.cterm_instantiate [(cterm_of sg (Var(("w",0),Type("Numeral.bin",[]))),cterm_of sg t)] fast1_th) |
31 |
else NONE |
|
32 |
| f _ _ _ = NONE **) |
|
14494
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
33 |
fun g sg thms (Const("Word.bv_to_nat",_) $ (t as (Const("List.list.Cons",_) $ _ $ _))) = |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
34 |
if vec_is_usable t |
15531 | 35 |
then SOME (Drule.cterm_instantiate [(cterm_of sg (Var(("bs",0),Type("List.list",[Type("Word.bit",[])]))),cterm_of sg t)] fast2_th) |
36 |
else NONE |
|
37 |
| g _ _ _ = NONE |
|
15013 | 38 |
(*lcp** val simproc1 = Simplifier.simproc (sign_of thy) "nat_to_bv" ["Word.nat_to_bv (number_of ?w)"] f ***) |
14494
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
39 |
val simproc2 = Simplifier.simproc (sign_of thy) "bv_to_nat" ["Word.bv_to_nat (?x # ?xs)"] g |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
40 |
in |
15013 | 41 |
Simplifier.change_simpset_of (op addsimprocs) [(*lcp*simproc1,**)simproc2] thy |
14494
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
42 |
end |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
43 |
in |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
44 |
val setup_word = [add_word] |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
45 |
end |