src/HOL/Library/word_setup.ML
author berghofe
Fri, 01 Jul 2005 13:54:12 +0200
changeset 16633 208ebc9311f2
parent 16486 1a12cdb6ee6b
child 17876 b9c92f384109
permissions -rw-r--r--
Implemented trick (due to Tobias Nipkow) for fine-tuning simplification of premises of congruence rules.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
34264f5e4691 new treatment of binary numerals
paulson
parents: 14494
diff changeset
     4
34264f5e4691 new treatment of binary numerals
paulson
parents: 14494
diff changeset
     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
34264f5e4691 new treatment of binary numerals
paulson
parents: 14494
diff changeset
    15
    fun num_is_usable (Const("Numeral.Pls",_)) = true
34264f5e4691 new treatment of binary numerals
paulson
parents: 14494
diff changeset
    16
      | num_is_usable (Const("Numeral.Min",_)) = false
34264f5e4691 new treatment of binary numerals
paulson
parents: 14494
diff changeset
    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
34264f5e4691 new treatment of binary numerals
paulson
parents: 14494
diff changeset
    26
 (*lcp**	    val fast1_th = PureThy.get_thm thy "Word.fast_nat_to_bv_def"**)
16486
1a12cdb6ee6b get_thm(s): Name;
wenzelm
parents: 15531
diff changeset
    27
	    val fast2_th = PureThy.get_thm thy (Name "Word.fast_bv_to_nat_def")
15013
34264f5e4691 new treatment of binary numerals
paulson
parents: 14494
diff changeset
    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
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15463
diff changeset
    30
		then SOME (Drule.cterm_instantiate [(cterm_of sg (Var(("w",0),Type("Numeral.bin",[]))),cterm_of sg t)] fast1_th)
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15463
diff changeset
    31
		else NONE
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15463
diff changeset
    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
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15463
diff changeset
    35
		then SOME (Drule.cterm_instantiate [(cterm_of sg (Var(("bs",0),Type("List.list",[Type("Word.bit",[])]))),cterm_of sg t)] fast2_th)
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15463
diff changeset
    36
		else NONE
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15463
diff changeset
    37
	      | g _ _ _ = NONE
15013
34264f5e4691 new treatment of binary numerals
paulson
parents: 14494
diff changeset
    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
34264f5e4691 new treatment of binary numerals
paulson
parents: 14494
diff changeset
    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