src/HOL/Library/word_setup.ML
author wenzelm
Thu Jan 19 21:22:08 2006 +0100 (2006-01-19 ago)
changeset 18708 4b3dadb4fe33
parent 17876 b9c92f384109
child 19806 f860b7a98445
permissions -rw-r--r--
setup: theory -> theory;
     1 (*  Title:      HOL/Library/word_setup.ML
     2     ID:         $Id$
     3     Author:     Sebastian Skalberg (TU Muenchen)
     4 
     5 comments containing lcp are the removal of fast_bv_of_nat.
     6 *)
     7 
     8 local
     9     fun is_const_bool (Const("True",_)) = true
    10       | is_const_bool (Const("False",_)) = true
    11       | is_const_bool _ = false
    12     fun is_const_bit (Const("Word.bit.Zero",_)) = true
    13       | is_const_bit (Const("Word.bit.One",_)) = true
    14       | is_const_bit _ = false
    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) =
    18 	num_is_usable w andalso is_const_bool b
    19       | num_is_usable _ = false
    20     fun vec_is_usable (Const("List.list.Nil",_)) = true
    21       | vec_is_usable (Const("List.list.Cons",_) $ b $ bs) =
    22 	vec_is_usable bs andalso is_const_bit b
    23       | vec_is_usable _ = false
    24     fun add_word thy =
    25 	let
    26  (*lcp**	    val fast1_th = PureThy.get_thm thy "Word.fast_nat_to_bv_def"**)
    27 	    val fast2_th = PureThy.get_thm thy (Name "Word.fast_bv_to_nat_def")
    28  (*lcp**	    fun f sg thms (Const("Word.nat_to_bv",_) $ (Const("Numeral.number_of",_) $ t)) =
    29 		if num_is_usable t
    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 **)
    33 	    fun g sg thms (Const("Word.bv_to_nat",_) $ (t as (Const("List.list.Cons",_) $ _ $ _))) =
    34 		if vec_is_usable t
    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
    38   (*lcp**	    val simproc1 = Simplifier.simproc (sign_of thy) "nat_to_bv" ["Word.nat_to_bv (number_of ?w)"] f ***)
    39 	    val simproc2 = Simplifier.simproc (sign_of thy) "bv_to_nat" ["Word.bv_to_nat (?x # ?xs)"] g
    40 	in
    41 	  Simplifier.change_simpset_of thy (fn ss => ss addsimprocs [(*lcp*simproc1,**)simproc2]);
    42           thy
    43 	end
    44 in
    45 val setup_word = add_word
    46 end