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)"
```