src/HOL/Import/HOL4Compat.thy
changeset 35416 d8d7d1b785af
parent 32960 69916a850301
child 37596 248db70c9bcf
     1.1 --- a/src/HOL/Import/HOL4Compat.thy	Wed Feb 24 11:55:52 2010 +0100
     1.2 +++ b/src/HOL/Import/HOL4Compat.thy	Mon Mar 01 13:40:23 2010 +0100
     1.3 @@ -15,8 +15,7 @@
     1.4  lemma COND_DEF:"(If b t f) = (@x. ((b = True) --> (x = t)) & ((b = False) --> (x = f)))"
     1.5    by auto
     1.6  
     1.7 -constdefs
     1.8 -  LET :: "['a \<Rightarrow> 'b,'a] \<Rightarrow> 'b"
     1.9 +definition LET :: "['a \<Rightarrow> 'b,'a] \<Rightarrow> 'b" where
    1.10    "LET f s == f s"
    1.11  
    1.12  lemma [hol4rew]: "LET f s = Let s f"
    1.13 @@ -119,10 +118,10 @@
    1.14  lemma LESS_OR_EQ: "m <= (n::nat) = (m < n | m = n)"
    1.15    by auto
    1.16  
    1.17 -constdefs
    1.18 -  nat_gt :: "nat => nat => bool"
    1.19 +definition nat_gt :: "nat => nat => bool" where
    1.20    "nat_gt == %m n. n < m"
    1.21 -  nat_ge :: "nat => nat => bool"
    1.22 +
    1.23 +definition nat_ge :: "nat => nat => bool" where
    1.24    "nat_ge == %m n. nat_gt m n | m = n"
    1.25  
    1.26  lemma [hol4rew]: "nat_gt m n = (n < m)"
    1.27 @@ -200,8 +199,7 @@
    1.28    qed
    1.29  qed;
    1.30  
    1.31 -constdefs
    1.32 -  FUNPOW :: "('a => 'a) => nat => 'a => 'a"
    1.33 +definition FUNPOW :: "('a => 'a) => nat => 'a => 'a" where
    1.34    "FUNPOW f n == f ^^ n"
    1.35  
    1.36  lemma FUNPOW: "(ALL f x. (f ^^ 0) x = x) &
    1.37 @@ -229,14 +227,16 @@
    1.38  lemma DIVISION: "(0::nat) < n --> (!k. (k = k div n * n + k mod n) & k mod n < n)"
    1.39    by simp
    1.40  
    1.41 -constdefs
    1.42 -  ALT_ZERO :: nat
    1.43 +definition ALT_ZERO :: nat where 
    1.44    "ALT_ZERO == 0"
    1.45 -  NUMERAL_BIT1 :: "nat \<Rightarrow> nat"
    1.46 +
    1.47 +definition NUMERAL_BIT1 :: "nat \<Rightarrow> nat" where 
    1.48    "NUMERAL_BIT1 n == n + (n + Suc 0)"
    1.49 -  NUMERAL_BIT2 :: "nat \<Rightarrow> nat"
    1.50 +
    1.51 +definition NUMERAL_BIT2 :: "nat \<Rightarrow> nat" where 
    1.52    "NUMERAL_BIT2 n == n + (n + Suc (Suc 0))"
    1.53 -  NUMERAL :: "nat \<Rightarrow> nat"
    1.54 +
    1.55 +definition NUMERAL :: "nat \<Rightarrow> nat" where 
    1.56    "NUMERAL x == x"
    1.57  
    1.58  lemma [hol4rew]: "NUMERAL ALT_ZERO = 0"
    1.59 @@ -329,8 +329,7 @@
    1.60  lemma NULL_DEF: "(null [] = True) & (!h t. null (h # t) = False)"
    1.61    by simp
    1.62  
    1.63 -constdefs
    1.64 -  sum :: "nat list \<Rightarrow> nat"
    1.65 +definition sum :: "nat list \<Rightarrow> nat" where
    1.66    "sum l == foldr (op +) l 0"
    1.67  
    1.68  lemma SUM: "(sum [] = 0) & (!h t. sum (h#t) = h + sum t)"
    1.69 @@ -359,8 +358,7 @@
    1.70    (ALL n x. replicate (Suc n) x = x # replicate n x)"
    1.71    by simp
    1.72  
    1.73 -constdefs
    1.74 -  FOLDR :: "[['a,'b]\<Rightarrow>'b,'b,'a list] \<Rightarrow> 'b"
    1.75 +definition FOLDR :: "[['a,'b]\<Rightarrow>'b,'b,'a list] \<Rightarrow> 'b" where
    1.76    "FOLDR f e l == foldr f l e"
    1.77  
    1.78  lemma [hol4rew]: "FOLDR f e l = foldr f l e"
    1.79 @@ -418,8 +416,7 @@
    1.80  lemma list_CASES: "(l = []) | (? t h. l = h#t)"
    1.81    by (induct l,auto)
    1.82  
    1.83 -constdefs
    1.84 -  ZIP :: "'a list * 'b list \<Rightarrow> ('a * 'b) list"
    1.85 +definition ZIP :: "'a list * 'b list \<Rightarrow> ('a * 'b) list" where
    1.86    "ZIP == %(a,b). zip a b"
    1.87  
    1.88  lemma ZIP: "(zip [] [] = []) &
    1.89 @@ -514,8 +511,7 @@
    1.90  lemma pow: "(!x::real. x ^ 0 = 1) & (!x::real. ALL n. x ^ (Suc n) = x * x ^ n)"
    1.91    by simp
    1.92  
    1.93 -constdefs
    1.94 -  real_gt :: "real => real => bool" 
    1.95 +definition real_gt :: "real => real => bool" where 
    1.96    "real_gt == %x y. y < x"
    1.97  
    1.98  lemma [hol4rew]: "real_gt x y = (y < x)"
    1.99 @@ -524,8 +520,7 @@
   1.100  lemma real_gt: "ALL x (y::real). (y < x) = (y < x)"
   1.101    by simp
   1.102  
   1.103 -constdefs
   1.104 -  real_ge :: "real => real => bool"
   1.105 +definition real_ge :: "real => real => bool" where
   1.106    "real_ge x y == y <= x"
   1.107  
   1.108  lemma [hol4rew]: "real_ge x y = (y <= x)"