src/HOL/Import/HOL/HOL4Vec.thy
changeset 35416 d8d7d1b785af
parent 26086 3c243098b64a
child 44763 b50d5d694838
     1.1 --- a/src/HOL/Import/HOL/HOL4Vec.thy	Wed Feb 24 11:55:52 2010 +0100
     1.2 +++ b/src/HOL/Import/HOL/HOL4Vec.thy	Mon Mar 01 13:40:23 2010 +0100
     1.3 @@ -164,8 +164,7 @@
     1.4  lemma word_base0_def: "word_base0 = (%a::'a::type list. mk_word (CONSTR 0 a (%n::nat. BOTTOM)))"
     1.5    by (import word_base word_base0_def)
     1.6  
     1.7 -constdefs
     1.8 -  WORD :: "'a list => 'a word" 
     1.9 +definition WORD :: "'a list => 'a word" where 
    1.10    "WORD == word_base0"
    1.11  
    1.12  lemma WORD: "WORD = word_base0"
    1.13 @@ -680,8 +679,7 @@
    1.14  
    1.15  ;setup_theory word_num
    1.16  
    1.17 -constdefs
    1.18 -  LVAL :: "('a => nat) => nat => 'a list => nat" 
    1.19 +definition LVAL :: "('a => nat) => nat => 'a list => nat" where 
    1.20    "LVAL ==
    1.21  %(f::'a::type => nat) b::nat. foldl (%(e::nat) x::'a::type. b * e + f x) 0"
    1.22  
    1.23 @@ -756,8 +754,7 @@
    1.24      SNOC (frep (m mod b)) (NLIST n frep b (m div b)))"
    1.25    by (import word_num NLIST_DEF)
    1.26  
    1.27 -constdefs
    1.28 -  NWORD :: "nat => (nat => 'a) => nat => nat => 'a word" 
    1.29 +definition NWORD :: "nat => (nat => 'a) => nat => nat => 'a word" where 
    1.30    "NWORD ==
    1.31  %(n::nat) (frep::nat => 'a::type) (b::nat) m::nat. WORD (NLIST n frep b m)"
    1.32  
    1.33 @@ -1076,8 +1073,7 @@
    1.34     EXISTSABIT P (WCAT (w1, w2)) = (EXISTSABIT P w1 | EXISTSABIT P w2)"
    1.35    by (import word_bitop EXISTSABIT_WCAT)
    1.36  
    1.37 -constdefs
    1.38 -  SHR :: "bool => 'a => 'a word => 'a word * 'a" 
    1.39 +definition SHR :: "bool => 'a => 'a word => 'a word * 'a" where 
    1.40    "SHR ==
    1.41  %(f::bool) (b::'a::type) w::'a::type word.
    1.42     (WCAT
    1.43 @@ -1093,8 +1089,7 @@
    1.44      bit 0 w)"
    1.45    by (import word_bitop SHR_DEF)
    1.46  
    1.47 -constdefs
    1.48 -  SHL :: "bool => 'a word => 'a => 'a * 'a word" 
    1.49 +definition SHL :: "bool => 'a word => 'a => 'a * 'a word" where 
    1.50    "SHL ==
    1.51  %(f::bool) (w::'a::type word) b::'a::type.
    1.52     (bit (PRE (WORDLEN w)) w,
    1.53 @@ -1196,8 +1191,7 @@
    1.54  
    1.55  ;setup_theory bword_num
    1.56  
    1.57 -constdefs
    1.58 -  BV :: "bool => nat" 
    1.59 +definition BV :: "bool => nat" where 
    1.60    "BV == %b::bool. if b then Suc 0 else 0"
    1.61  
    1.62  lemma BV_DEF: "ALL b::bool. BV b = (if b then Suc 0 else 0)"
    1.63 @@ -1248,15 +1242,13 @@
    1.64               BNVAL (WCAT (w1, w2)) = BNVAL w1 * 2 ^ m + BNVAL w2))"
    1.65    by (import bword_num BNVAL_WCAT)
    1.66  
    1.67 -constdefs
    1.68 -  VB :: "nat => bool" 
    1.69 +definition VB :: "nat => bool" where 
    1.70    "VB == %n::nat. n mod 2 ~= 0"
    1.71  
    1.72  lemma VB_DEF: "ALL n::nat. VB n = (n mod 2 ~= 0)"
    1.73    by (import bword_num VB_DEF)
    1.74  
    1.75 -constdefs
    1.76 -  NBWORD :: "nat => nat => bool word" 
    1.77 +definition NBWORD :: "nat => nat => bool word" where 
    1.78    "NBWORD == %(n::nat) m::nat. WORD (NLIST n VB 2 m)"
    1.79  
    1.80  lemma NBWORD_DEF: "ALL (n::nat) m::nat. NBWORD n m = WORD (NLIST n VB 2 m)"