src/HOL/Import/HOL4Compat.thy
changeset 14516 a183dec876ab
child 14620 1be590fd2422
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Import/HOL4Compat.thy	Fri Apr 02 17:37:45 2004 +0200
     1.3 @@ -0,0 +1,533 @@
     1.4 +theory HOL4Compat = HOL4Setup + Divides + Primes + Real:
     1.5 +
     1.6 +lemma EXISTS_UNIQUE_DEF: "(Ex1 P) = (Ex P & (ALL x y. P x & P y --> (x = y)))"
     1.7 +  by auto
     1.8 +
     1.9 +lemma COND_DEF:"(If b t f) = (@x. ((b = True) --> (x = t)) & ((b = False) --> (x = f)))"
    1.10 +  by auto
    1.11 +
    1.12 +constdefs
    1.13 +  LET :: "['a \<Rightarrow> 'b,'a] \<Rightarrow> 'b"
    1.14 +  "LET f s == f s"
    1.15 +
    1.16 +lemma [hol4rew]: "LET f s = Let s f"
    1.17 +  by (simp add: LET_def Let_def)
    1.18 +
    1.19 +lemmas [hol4rew] = ONE_ONE_rew
    1.20 +
    1.21 +lemma bool_case_DEF: "(bool_case x y b) = (if b then x else y)"
    1.22 +  by simp;
    1.23 +
    1.24 +lemma INR_INL_11: "(ALL y x. (Inl x = Inl y) = (x = y)) & (ALL y x. (Inr x = Inr y) = (x = y))"
    1.25 +  by safe
    1.26 +
    1.27 +consts
    1.28 +  ISL :: "'a + 'b => bool"
    1.29 +  ISR :: "'a + 'b => bool"
    1.30 +
    1.31 +primrec ISL_def:
    1.32 +  "ISL (Inl x) = True"
    1.33 +  "ISL (Inr x) = False"
    1.34 +
    1.35 +primrec ISR_def:
    1.36 +  "ISR (Inl x) = False"
    1.37 +  "ISR (Inr x) = True"
    1.38 +
    1.39 +lemma ISL: "(ALL x. ISL (Inl x)) & (ALL y. ~ISL (Inr y))"
    1.40 +  by simp
    1.41 +
    1.42 +lemma ISR: "(ALL x. ISR (Inr x)) & (ALL y. ~ISR (Inl y))"
    1.43 +  by simp
    1.44 +
    1.45 +consts
    1.46 +  OUTL :: "'a + 'b => 'a"
    1.47 +  OUTR :: "'a + 'b => 'b"
    1.48 +
    1.49 +primrec OUTL_def:
    1.50 +  "OUTL (Inl x) = x"
    1.51 +
    1.52 +primrec OUTR_def:
    1.53 +  "OUTR (Inr x) = x"
    1.54 +
    1.55 +lemma OUTL: "OUTL (Inl x) = x"
    1.56 +  by simp
    1.57 +
    1.58 +lemma OUTR: "OUTR (Inr x) = x"
    1.59 +  by simp
    1.60 +
    1.61 +lemma sum_case_def: "(ALL f g x. sum_case f g (Inl x) = f x) & (ALL f g y. sum_case f g (Inr y) = g y)"
    1.62 +  by simp;
    1.63 +
    1.64 +lemma one: "ALL v. v = ()"
    1.65 +  by simp;
    1.66 +
    1.67 +lemma option_case_def: "(!u f. option_case u f None = u) & (!u f x. option_case u f (Some x) = f x)"
    1.68 +  by simp
    1.69 +
    1.70 +lemma OPTION_MAP_DEF: "(!f x. option_map f (Some x) = Some (f x)) & (!f. option_map f None = None)"
    1.71 +  by simp
    1.72 +
    1.73 +consts
    1.74 +  IS_SOME :: "'a option => bool"
    1.75 +  IS_NONE :: "'a option => bool"
    1.76 +
    1.77 +primrec IS_SOME_def:
    1.78 +  "IS_SOME (Some x) = True"
    1.79 +  "IS_SOME None = False"
    1.80 +
    1.81 +primrec IS_NONE_def:
    1.82 +  "IS_NONE (Some x) = False"
    1.83 +  "IS_NONE None = True"
    1.84 +
    1.85 +lemma IS_NONE_DEF: "(!x. IS_NONE (Some x) = False) & (IS_NONE None = True)"
    1.86 +  by simp
    1.87 +
    1.88 +lemma IS_SOME_DEF: "(!x. IS_SOME (Some x) = True) & (IS_SOME None = False)"
    1.89 +  by simp
    1.90 +
    1.91 +consts
    1.92 +  OPTION_JOIN :: "'a option option => 'a option"
    1.93 +
    1.94 +primrec OPTION_JOIN_def:
    1.95 +  "OPTION_JOIN None = None"
    1.96 +  "OPTION_JOIN (Some x) = x"
    1.97 +
    1.98 +lemma OPTION_JOIN_DEF: "(OPTION_JOIN None = None) & (ALL x. OPTION_JOIN (Some x) = x)"
    1.99 +  by simp;
   1.100 +
   1.101 +lemma PAIR: "(fst x,snd x) = x"
   1.102 +  by simp
   1.103 +
   1.104 +lemma PAIR_MAP: "prod_fun f g p = (f (fst p),g (snd p))"
   1.105 +  by (simp add: prod_fun_def split_def)
   1.106 +
   1.107 +lemma pair_case_def: "split = split"
   1.108 +  ..;
   1.109 +
   1.110 +lemma LESS_OR_EQ: "m <= (n::nat) = (m < n | m = n)"
   1.111 +  by auto
   1.112 +
   1.113 +constdefs
   1.114 +  nat_gt :: "nat => nat => bool"
   1.115 +  "nat_gt == %m n. n < m"
   1.116 +  nat_ge :: "nat => nat => bool"
   1.117 +  "nat_ge == %m n. nat_gt m n | m = n"
   1.118 +
   1.119 +lemma [hol4rew]: "nat_gt m n = (n < m)"
   1.120 +  by (simp add: nat_gt_def)
   1.121 +
   1.122 +lemma [hol4rew]: "nat_ge m n = (n <= m)"
   1.123 +  by (auto simp add: nat_ge_def nat_gt_def)
   1.124 +
   1.125 +lemma GREATER_DEF: "ALL m n. (n < m) = (n < m)"
   1.126 +  by simp
   1.127 +
   1.128 +lemma GREATER_OR_EQ: "ALL m n. n <= (m::nat) = (n < m | m = n)"
   1.129 +  by auto
   1.130 +
   1.131 +lemma LESS_DEF: "m < n = (? P. (!n. P (Suc n) --> P n) & P m & ~P n)"
   1.132 +proof safe
   1.133 +  assume "m < n"
   1.134 +  def P == "%n. n <= m"
   1.135 +  have "(!n. P (Suc n) \<longrightarrow> P n) & P m & ~P n"
   1.136 +  proof (auto simp add: P_def)
   1.137 +    assume "n <= m"
   1.138 +    from prems
   1.139 +    show False
   1.140 +      by auto
   1.141 +  qed
   1.142 +  thus "? P. (!n. P (Suc n) \<longrightarrow> P n) & P m & ~P n"
   1.143 +    by auto
   1.144 +next
   1.145 +  fix P
   1.146 +  assume alln: "!n. P (Suc n) \<longrightarrow> P n"
   1.147 +  assume pm: "P m"
   1.148 +  assume npn: "~P n"
   1.149 +  have "!k q. q + k = m \<longrightarrow> P q"
   1.150 +  proof
   1.151 +    fix k
   1.152 +    show "!q. q + k = m \<longrightarrow> P q"
   1.153 +    proof (induct k,simp_all)
   1.154 +      show "P m" .
   1.155 +    next
   1.156 +      fix k
   1.157 +      assume ind: "!q. q + k = m \<longrightarrow> P q"
   1.158 +      show "!q. Suc (q + k) = m \<longrightarrow> P q"
   1.159 +      proof (rule+)
   1.160 +	fix q
   1.161 +	assume "Suc (q + k) = m"
   1.162 +	hence "(Suc q) + k = m"
   1.163 +	  by simp
   1.164 +	with ind
   1.165 +	have psq: "P (Suc q)"
   1.166 +	  by simp
   1.167 +	from alln
   1.168 +	have "P (Suc q) --> P q"
   1.169 +	  ..
   1.170 +	with psq
   1.171 +	show "P q"
   1.172 +	  by simp
   1.173 +      qed
   1.174 +    qed
   1.175 +  qed
   1.176 +  hence "!q. q + (m - n) = m \<longrightarrow> P q"
   1.177 +    ..
   1.178 +  hence hehe: "n + (m - n) = m \<longrightarrow> P n"
   1.179 +    ..
   1.180 +  show "m < n"
   1.181 +  proof (rule classical)
   1.182 +    assume "~(m<n)"
   1.183 +    hence "n <= m"
   1.184 +      by simp
   1.185 +    with hehe
   1.186 +    have "P n"
   1.187 +      by simp
   1.188 +    with npn
   1.189 +    show "m < n"
   1.190 +      ..
   1.191 +  qed
   1.192 +qed;
   1.193 +
   1.194 +constdefs
   1.195 +  FUNPOW :: "('a => 'a) => nat => 'a => 'a"
   1.196 +  "FUNPOW f n == f ^ n"
   1.197 +
   1.198 +lemma FUNPOW: "(ALL f x. (f ^ 0) x = x) &
   1.199 +  (ALL f n x. (f ^ Suc n) x = (f ^ n) (f x))"
   1.200 +proof auto
   1.201 +  fix f n x
   1.202 +  have "ALL x. f ((f ^ n) x) = (f ^ n) (f x)"
   1.203 +    by (induct n,auto)
   1.204 +  thus "f ((f ^ n) x) = (f ^ n) (f x)"
   1.205 +    ..
   1.206 +qed
   1.207 +
   1.208 +lemma [hol4rew]: "FUNPOW f n = f ^ n"
   1.209 +  by (simp add: FUNPOW_def)
   1.210 +
   1.211 +lemma ADD: "(!n. (0::nat) + n = n) & (!m n. Suc m + n = Suc (m + n))"
   1.212 +  by simp
   1.213 +
   1.214 +lemma MULT: "(!n. (0::nat) * n = 0) & (!m n. Suc m * n = m * n + n)"
   1.215 +  by simp
   1.216 +
   1.217 +lemma SUB: "(!m. (0::nat) - m = 0) & (!m n. (Suc m) - n = (if m < n then 0 else Suc (m - n)))"
   1.218 +  apply simp
   1.219 +  apply arith
   1.220 +  done
   1.221 +
   1.222 +lemma MAX_DEF: "max (m::nat) n = (if m < n then n else m)"
   1.223 +  by (simp add: max_def)
   1.224 +
   1.225 +lemma MIN_DEF: "min (m::nat) n = (if m < n then m else n)"
   1.226 +  by (simp add: min_def)
   1.227 +
   1.228 +lemma DIVISION: "(0::nat) < n --> (!k. (k = k div n * n + k mod n) & k mod n < n)"
   1.229 +  by simp
   1.230 +
   1.231 +constdefs
   1.232 +  ALT_ZERO :: nat
   1.233 +  "ALT_ZERO == 0"
   1.234 +  NUMERAL_BIT1 :: "nat \<Rightarrow> nat"
   1.235 +  "NUMERAL_BIT1 n == n + (n + Suc 0)"
   1.236 +  NUMERAL_BIT2 :: "nat \<Rightarrow> nat"
   1.237 +  "NUMERAL_BIT2 n == n + (n + Suc (Suc 0))"
   1.238 +  NUMERAL :: "nat \<Rightarrow> nat"
   1.239 +  "NUMERAL x == x"
   1.240 +
   1.241 +lemma [hol4rew]: "NUMERAL ALT_ZERO = 0"
   1.242 +  by (simp add: ALT_ZERO_def NUMERAL_def)
   1.243 +
   1.244 +lemma [hol4rew]: "NUMERAL (NUMERAL_BIT1 ALT_ZERO) = 1"
   1.245 +  by (simp add: ALT_ZERO_def NUMERAL_BIT1_def NUMERAL_def)
   1.246 +
   1.247 +lemma [hol4rew]: "NUMERAL (NUMERAL_BIT2 ALT_ZERO) = 2"
   1.248 +  by (simp add: ALT_ZERO_def NUMERAL_BIT2_def NUMERAL_def)
   1.249 +
   1.250 +lemma EXP: "(!m. m ^ 0 = (1::nat)) & (!m n. m ^ Suc n = m * (m::nat) ^ n)"
   1.251 +  by auto
   1.252 +
   1.253 +lemma num_case_def: "(!b f. nat_case b f 0 = b) & (!b f n. nat_case b f (Suc n) = f n)"
   1.254 +  by simp;
   1.255 +
   1.256 +lemma divides_def: "(a::nat) dvd b = (? q. b = q * a)"
   1.257 +  by (auto simp add: dvd_def);
   1.258 +
   1.259 +lemma list_case_def: "(!v f. list_case v f [] = v) & (!v f a0 a1. list_case v f (a0#a1) = f a0 a1)"
   1.260 +  by simp
   1.261 +
   1.262 +consts
   1.263 +  list_size :: "('a \<Rightarrow> nat) \<Rightarrow> 'a list \<Rightarrow> nat"
   1.264 +
   1.265 +primrec
   1.266 +  "list_size f [] = 0"
   1.267 +  "list_size f (a0#a1) = 1 + (f a0 + list_size f a1)"
   1.268 +
   1.269 +lemma list_size_def: "(!f. list_size f [] = 0) &
   1.270 +         (!f a0 a1. list_size f (a0#a1) = 1 + (f a0 + list_size f a1))"
   1.271 +  by simp
   1.272 +
   1.273 +lemma list_case_cong: "! M M' v f. M = M' & (M' = [] \<longrightarrow>  v = v') &
   1.274 +           (!a0 a1. (M' = a0#a1) \<longrightarrow> (f a0 a1 = f' a0 a1)) -->
   1.275 +           (list_case v f M = list_case v' f' M')"
   1.276 +proof clarify
   1.277 +  fix M M' v f
   1.278 +  assume "M' = [] \<longrightarrow> v = v'"
   1.279 +    and "!a0 a1. M' = a0 # a1 \<longrightarrow> f a0 a1 = f' a0 a1"
   1.280 +  show "list_case v f M' = list_case v' f' M'"
   1.281 +  proof (rule List.list.case_cong)
   1.282 +    show "M' = M'"
   1.283 +      ..
   1.284 +  next
   1.285 +    assume "M' = []"
   1.286 +    with prems
   1.287 +    show "v = v'"
   1.288 +      by auto
   1.289 +  next
   1.290 +    fix a0 a1
   1.291 +    assume "M' = a0 # a1"
   1.292 +    with prems
   1.293 +    show "f a0 a1 = f' a0 a1"
   1.294 +      by auto
   1.295 +  qed
   1.296 +qed
   1.297 +
   1.298 +lemma list_Axiom: "ALL f0 f1. EX fn. (fn [] = f0) & (ALL a0 a1. fn (a0#a1) = f1 a0 a1 (fn a1))"
   1.299 +proof safe
   1.300 +  fix f0 f1
   1.301 +  def fn == "list_rec f0 f1"
   1.302 +  have "fn [] = f0 & (ALL a0 a1. fn (a0 # a1) = f1 a0 a1 (fn a1))"
   1.303 +    by (simp add: fn_def)
   1.304 +  thus "EX fn. fn [] = f0 & (ALL a0 a1. fn (a0 # a1) = f1 a0 a1 (fn a1))"
   1.305 +    by auto
   1.306 +qed
   1.307 +
   1.308 +lemma list_Axiom_old: "EX! fn. (fn [] = x) & (ALL h t. fn (h#t) = f (fn t) h t)"
   1.309 +proof safe
   1.310 +  def fn == "list_rec x (%h t r. f r h t)"
   1.311 +  have "fn [] = x & (ALL h t. fn (h # t) = f (fn t) h t)"
   1.312 +    by (simp add: fn_def)
   1.313 +  thus "EX fn. fn [] = x & (ALL h t. fn (h # t) = f (fn t) h t)"
   1.314 +    by auto
   1.315 +next
   1.316 +  fix fn1 fn2
   1.317 +  assume "ALL h t. fn1 (h # t) = f (fn1 t) h t"
   1.318 +  assume "ALL h t. fn2 (h # t) = f (fn2 t) h t"
   1.319 +  assume "fn2 [] = fn1 []"
   1.320 +  show "fn1 = fn2"
   1.321 +  proof
   1.322 +    fix xs
   1.323 +    show "fn1 xs = fn2 xs"
   1.324 +      by (induct xs,simp_all add: prems) 
   1.325 +  qed
   1.326 +qed
   1.327 +
   1.328 +lemma NULL_DEF: "(null [] = True) & (!h t. null (h # t) = False)"
   1.329 +  by simp
   1.330 +
   1.331 +constdefs
   1.332 +  sum :: "nat list \<Rightarrow> nat"
   1.333 +  "sum l == foldr (op +) l 0"
   1.334 +
   1.335 +lemma SUM: "(sum [] = 0) & (!h t. sum (h#t) = h + sum t)"
   1.336 +  by (simp add: sum_def)
   1.337 +
   1.338 +lemma APPEND: "(!l. [] @ l = l) & (!l1 l2 h. (h#l1) @ l2 = h# l1 @ l2)"
   1.339 +  by simp
   1.340 +
   1.341 +lemma FLAT: "(concat [] = []) & (!h t. concat (h#t) = h @ (concat t))"
   1.342 +  by simp
   1.343 +
   1.344 +lemma LENGTH: "(length [] = 0) & (!h t. length (h#t) = Suc (length t))"
   1.345 +  by simp
   1.346 +
   1.347 +lemma MAP: "(!f. map f [] = []) & (!f h t. map f (h#t) = f h#map f t)"
   1.348 +  by simp
   1.349 +
   1.350 +lemma MEM: "(!x. x mem [] = False) & (!x h t. x mem (h#t) = ((x = h) | x mem t))"
   1.351 +  by auto
   1.352 +
   1.353 +lemma FILTER: "(!P. filter P [] = []) & (!P h t.
   1.354 +           filter P (h#t) = (if P h then h#filter P t else filter P t))"
   1.355 +  by simp
   1.356 +
   1.357 +lemma REPLICATE: "(ALL x. replicate 0 x = []) &
   1.358 +  (ALL n x. replicate (Suc n) x = x # replicate n x)"
   1.359 +  by simp
   1.360 +
   1.361 +constdefs
   1.362 +  FOLDR :: "[['a,'b]\<Rightarrow>'b,'b,'a list] \<Rightarrow> 'b"
   1.363 +  "FOLDR f e l == foldr f l e"
   1.364 +
   1.365 +lemma [hol4rew]: "FOLDR f e l = foldr f l e"
   1.366 +  by (simp add: FOLDR_def)
   1.367 +
   1.368 +lemma FOLDR: "(!f e. foldr f [] e = e) & (!f e x l. foldr f (x#l) e = f x (foldr f l e))"
   1.369 +  by simp
   1.370 +
   1.371 +lemma FOLDL: "(!f e. foldl f e [] = e) & (!f e x l. foldl f e (x#l) = foldl f (f e x) l)"
   1.372 +  by simp
   1.373 +
   1.374 +lemma EVERY_DEF: "(!P. list_all P [] = True) & (!P h t. list_all P (h#t) = (P h & list_all P t))"
   1.375 +  by simp
   1.376 +
   1.377 +consts
   1.378 +  list_exists :: "['a \<Rightarrow> bool,'a list] \<Rightarrow> bool"
   1.379 +
   1.380 +primrec
   1.381 +  list_exists_Nil: "list_exists P Nil = False"
   1.382 +  list_exists_Cons: "list_exists P (x#xs) = (if P x then True else list_exists P xs)"
   1.383 +
   1.384 +lemma list_exists_DEF: "(!P. list_exists P [] = False) &
   1.385 +         (!P h t. list_exists P (h#t) = (P h | list_exists P t))"
   1.386 +  by simp
   1.387 +
   1.388 +consts
   1.389 +  map2 :: "[['a,'b]\<Rightarrow>'c,'a list,'b list] \<Rightarrow> 'c list"
   1.390 +
   1.391 +primrec
   1.392 +  map2_Nil: "map2 f [] l2 = []"
   1.393 +  map2_Cons: "map2 f (x#xs) l2 = f x (hd l2) # map2 f xs (tl l2)"
   1.394 +
   1.395 +lemma MAP2: "(!f. map2 f [] [] = []) & (!f h1 t1 h2 t2. map2 f (h1#t1) (h2#t2) = f h1 h2#map2 f t1 t2)"
   1.396 +  by simp
   1.397 +
   1.398 +lemma list_INDUCT: "\<lbrakk> P [] ; !t. P t \<longrightarrow> (!h. P (h#t)) \<rbrakk> \<Longrightarrow> !l. P l"
   1.399 +proof
   1.400 +  fix l
   1.401 +  assume "P []"
   1.402 +  assume allt: "!t. P t \<longrightarrow> (!h. P (h # t))"
   1.403 +  show "P l"
   1.404 +  proof (induct l)
   1.405 +    show "P []" .
   1.406 +  next
   1.407 +    fix h t
   1.408 +    assume "P t"
   1.409 +    with allt
   1.410 +    have "!h. P (h # t)"
   1.411 +      by auto
   1.412 +    thus "P (h # t)"
   1.413 +      ..
   1.414 +  qed
   1.415 +qed
   1.416 +
   1.417 +lemma list_CASES: "(l = []) | (? t h. l = h#t)"
   1.418 +  by (induct l,auto)
   1.419 +
   1.420 +constdefs
   1.421 +  ZIP :: "'a list * 'b list \<Rightarrow> ('a * 'b) list"
   1.422 +  "ZIP == %(a,b). zip a b"
   1.423 +
   1.424 +lemma ZIP: "(zip [] [] = []) &
   1.425 +  (!x1 l1 x2 l2. zip (x1#l1) (x2#l2) = (x1,x2)#zip l1 l2)"
   1.426 +  by simp
   1.427 +
   1.428 +lemma [hol4rew]: "ZIP (a,b) = zip a b"
   1.429 +  by (simp add: ZIP_def)
   1.430 +
   1.431 +consts
   1.432 +  unzip :: "('a * 'b) list \<Rightarrow> 'a list * 'b list"
   1.433 +
   1.434 +primrec
   1.435 +  unzip_Nil: "unzip [] = ([],[])"
   1.436 +  unzip_Cons: "unzip (xy#xys) = (let zs = unzip xys in (fst xy # fst zs,snd xy # snd zs))"
   1.437 +
   1.438 +lemma UNZIP: "(unzip [] = ([],[])) &
   1.439 +         (!x l. unzip (x#l) = (fst x#fst (unzip l),snd x#snd (unzip l)))"
   1.440 +  by (simp add: Let_def)
   1.441 +
   1.442 +lemma REVERSE: "(rev [] = []) & (!h t. rev (h#t) = (rev t) @ [h])"
   1.443 +  by simp;
   1.444 +
   1.445 +lemma REAL_SUP_ALLPOS: "\<lbrakk> ALL x. P (x::real) \<longrightarrow> 0 < x ; EX x. P x; EX z. ALL x. P x \<longrightarrow> x < z \<rbrakk> \<Longrightarrow> EX s. ALL y. (EX x. P x & y < x) = (y < s)"
   1.446 +proof safe
   1.447 +  fix x z
   1.448 +  assume allx: "ALL x. P x \<longrightarrow> 0 < x"
   1.449 +  assume px: "P x"
   1.450 +  assume allx': "ALL x. P x \<longrightarrow> x < z"
   1.451 +  have "EX s. ALL y. (EX x : Collect P. y < x) = (y < s)"
   1.452 +  proof (rule posreal_complete)
   1.453 +    show "ALL x : Collect P. 0 < x"
   1.454 +    proof safe
   1.455 +      fix x
   1.456 +      assume "P x"
   1.457 +      from allx
   1.458 +      have "P x \<longrightarrow> 0 < x"
   1.459 +	..
   1.460 +      thus "0 < x"
   1.461 +	by (simp add: prems)
   1.462 +    qed
   1.463 +  next
   1.464 +    from px
   1.465 +    show "EX x. x : Collect P"
   1.466 +      by auto
   1.467 +  next
   1.468 +    from allx'
   1.469 +    show "EX y. ALL x : Collect P. x < y"
   1.470 +      apply simp
   1.471 +      ..
   1.472 +  qed
   1.473 +  thus "EX s. ALL y. (EX x. P x & y < x) = (y < s)"
   1.474 +    by simp
   1.475 +qed
   1.476 +
   1.477 +lemma REAL_10: "~((1::real) = 0)"
   1.478 +  by simp
   1.479 +
   1.480 +lemma REAL_ADD_ASSOC: "(x::real) + (y + z) = x + y + z"
   1.481 +  by simp
   1.482 +
   1.483 +lemma REAL_MUL_ASSOC: "(x::real) * (y * z) = x * y * z"
   1.484 +  by simp
   1.485 +
   1.486 +lemma REAL_ADD_LINV:  "-x + x = (0::real)"
   1.487 +  by simp
   1.488 +
   1.489 +lemma REAL_MUL_LINV: "x ~= (0::real) ==> inverse x * x = 1"
   1.490 +  by simp
   1.491 +
   1.492 +lemma REAL_LT_TOTAL: "((x::real) = y) | x < y | y < x"
   1.493 +  by auto;
   1.494 +
   1.495 +lemma [hol4rew]: "real (0::nat) = 0"
   1.496 +  by simp
   1.497 +
   1.498 +lemma [hol4rew]: "real (1::nat) = 1"
   1.499 +  by simp
   1.500 +
   1.501 +lemma [hol4rew]: "real (2::nat) = 2"
   1.502 +  by simp
   1.503 +
   1.504 +lemma real_lte: "((x::real) <= y) = (~(y < x))"
   1.505 +  by auto
   1.506 +
   1.507 +lemma real_of_num: "((0::real) = 0) & (!n. real (Suc n) = real n + 1)"
   1.508 +  by (simp add: real_of_nat_Suc)
   1.509 +
   1.510 +lemma abs: "abs (x::real) = (if 0 <= x then x else -x)"
   1.511 +  by (simp add: real_abs_def)
   1.512 +
   1.513 +lemma pow: "(!x::real. x ^ 0 = 1) & (!x::real. ALL n. x ^ (Suc n) = x * x ^ n)"
   1.514 +  by simp;
   1.515 +
   1.516 +constdefs
   1.517 +  real_gt :: "real => real => bool" 
   1.518 +  "real_gt == %x y. y < x"
   1.519 +
   1.520 +lemma [hol4rew]: "real_gt x y = (y < x)"
   1.521 +  by (simp add: real_gt_def)
   1.522 +
   1.523 +lemma real_gt: "ALL x (y::real). (y < x) = (y < x)"
   1.524 +  by simp
   1.525 +
   1.526 +constdefs
   1.527 +  real_ge :: "real => real => bool"
   1.528 +  "real_ge x y == y <= x"
   1.529 +
   1.530 +lemma [hol4rew]: "real_ge x y = (y <= x)"
   1.531 +  by (simp add: real_ge_def)
   1.532 +
   1.533 +lemma real_ge: "ALL x y. (y <= x) = (y <= x)"
   1.534 +  by simp
   1.535 +
   1.536 +end