src/HOL/Import/HOL4Compat.thy
 author webertj Wed Aug 30 03:19:08 2006 +0200 (2006-08-30) changeset 20432 07ec57376051 parent 20269 c40070317ab8 child 23389 aaca6a8e5414 permissions -rw-r--r--
lin_arith_prover: splitting reverted because of performance loss
```     1 (*  Title:      HOL/Import/HOL4Compat.thy
```
```     2     ID:         \$Id\$
```
```     3     Author:     Sebastian Skalberg (TU Muenchen)
```
```     4 *)
```
```     5
```
```     6 theory HOL4Compat imports HOL4Setup Divides Primes Real
```
```     7 begin
```
```     8
```
```     9 lemma EXISTS_UNIQUE_DEF: "(Ex1 P) = (Ex P & (ALL x y. P x & P y --> (x = y)))"
```
```    10   by auto
```
```    11
```
```    12 lemma COND_DEF:"(If b t f) = (@x. ((b = True) --> (x = t)) & ((b = False) --> (x = f)))"
```
```    13   by auto
```
```    14
```
```    15 constdefs
```
```    16   LET :: "['a \<Rightarrow> 'b,'a] \<Rightarrow> 'b"
```
```    17   "LET f s == f s"
```
```    18
```
```    19 lemma [hol4rew]: "LET f s = Let s f"
```
```    20   by (simp add: LET_def Let_def)
```
```    21
```
```    22 lemmas [hol4rew] = ONE_ONE_rew
```
```    23
```
```    24 lemma bool_case_DEF: "(bool_case x y b) = (if b then x else y)"
```
```    25   by simp;
```
```    26
```
```    27 lemma INR_INL_11: "(ALL y x. (Inl x = Inl y) = (x = y)) & (ALL y x. (Inr x = Inr y) = (x = y))"
```
```    28   by safe
```
```    29
```
```    30 (*lemma INL_neq_INR: "ALL v1 v2. Sum_Type.Inr v2 ~= Sum_Type.Inl v1"
```
```    31   by simp*)
```
```    32
```
```    33 consts
```
```    34   ISL :: "'a + 'b => bool"
```
```    35   ISR :: "'a + 'b => bool"
```
```    36
```
```    37 primrec ISL_def:
```
```    38   "ISL (Inl x) = True"
```
```    39   "ISL (Inr x) = False"
```
```    40
```
```    41 primrec ISR_def:
```
```    42   "ISR (Inl x) = False"
```
```    43   "ISR (Inr x) = True"
```
```    44
```
```    45 lemma ISL: "(ALL x. ISL (Inl x)) & (ALL y. ~ISL (Inr y))"
```
```    46   by simp
```
```    47
```
```    48 lemma ISR: "(ALL x. ISR (Inr x)) & (ALL y. ~ISR (Inl y))"
```
```    49   by simp
```
```    50
```
```    51 consts
```
```    52   OUTL :: "'a + 'b => 'a"
```
```    53   OUTR :: "'a + 'b => 'b"
```
```    54
```
```    55 primrec OUTL_def:
```
```    56   "OUTL (Inl x) = x"
```
```    57
```
```    58 primrec OUTR_def:
```
```    59   "OUTR (Inr x) = x"
```
```    60
```
```    61 lemma OUTL: "OUTL (Inl x) = x"
```
```    62   by simp
```
```    63
```
```    64 lemma OUTR: "OUTR (Inr x) = x"
```
```    65   by simp
```
```    66
```
```    67 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)"
```
```    68   by simp;
```
```    69
```
```    70 lemma one: "ALL v. v = ()"
```
```    71   by simp;
```
```    72
```
```    73 lemma option_case_def: "(!u f. option_case u f None = u) & (!u f x. option_case u f (Some x) = f x)"
```
```    74   by simp
```
```    75
```
```    76 lemma OPTION_MAP_DEF: "(!f x. option_map f (Some x) = Some (f x)) & (!f. option_map f None = None)"
```
```    77   by simp
```
```    78
```
```    79 consts
```
```    80   IS_SOME :: "'a option => bool"
```
```    81   IS_NONE :: "'a option => bool"
```
```    82
```
```    83 primrec IS_SOME_def:
```
```    84   "IS_SOME (Some x) = True"
```
```    85   "IS_SOME None = False"
```
```    86
```
```    87 primrec IS_NONE_def:
```
```    88   "IS_NONE (Some x) = False"
```
```    89   "IS_NONE None = True"
```
```    90
```
```    91 lemma IS_NONE_DEF: "(!x. IS_NONE (Some x) = False) & (IS_NONE None = True)"
```
```    92   by simp
```
```    93
```
```    94 lemma IS_SOME_DEF: "(!x. IS_SOME (Some x) = True) & (IS_SOME None = False)"
```
```    95   by simp
```
```    96
```
```    97 consts
```
```    98   OPTION_JOIN :: "'a option option => 'a option"
```
```    99
```
```   100 primrec OPTION_JOIN_def:
```
```   101   "OPTION_JOIN None = None"
```
```   102   "OPTION_JOIN (Some x) = x"
```
```   103
```
```   104 lemma OPTION_JOIN_DEF: "(OPTION_JOIN None = None) & (ALL x. OPTION_JOIN (Some x) = x)"
```
```   105   by simp;
```
```   106
```
```   107 lemma PAIR: "(fst x,snd x) = x"
```
```   108   by simp
```
```   109
```
```   110 lemma PAIR_MAP: "prod_fun f g p = (f (fst p),g (snd p))"
```
```   111   by (simp add: prod_fun_def split_def)
```
```   112
```
```   113 lemma pair_case_def: "split = split"
```
```   114   ..;
```
```   115
```
```   116 lemma LESS_OR_EQ: "m <= (n::nat) = (m < n | m = n)"
```
```   117   by auto
```
```   118
```
```   119 constdefs
```
```   120   nat_gt :: "nat => nat => bool"
```
```   121   "nat_gt == %m n. n < m"
```
```   122   nat_ge :: "nat => nat => bool"
```
```   123   "nat_ge == %m n. nat_gt m n | m = n"
```
```   124
```
```   125 lemma [hol4rew]: "nat_gt m n = (n < m)"
```
```   126   by (simp add: nat_gt_def)
```
```   127
```
```   128 lemma [hol4rew]: "nat_ge m n = (n <= m)"
```
```   129   by (auto simp add: nat_ge_def nat_gt_def)
```
```   130
```
```   131 lemma GREATER_DEF: "ALL m n. (n < m) = (n < m)"
```
```   132   by simp
```
```   133
```
```   134 lemma GREATER_OR_EQ: "ALL m n. n <= (m::nat) = (n < m | m = n)"
```
```   135   by auto
```
```   136
```
```   137 lemma LESS_DEF: "m < n = (? P. (!n. P (Suc n) --> P n) & P m & ~P n)"
```
```   138 proof safe
```
```   139   assume "m < n"
```
```   140   def P == "%n. n <= m"
```
```   141   have "(!n. P (Suc n) \<longrightarrow> P n) & P m & ~P n"
```
```   142   proof (auto simp add: P_def)
```
```   143     assume "n <= m"
```
```   144     from prems
```
```   145     show False
```
```   146       by auto
```
```   147   qed
```
```   148   thus "? P. (!n. P (Suc n) \<longrightarrow> P n) & P m & ~P n"
```
```   149     by auto
```
```   150 next
```
```   151   fix P
```
```   152   assume alln: "!n. P (Suc n) \<longrightarrow> P n"
```
```   153   assume pm: "P m"
```
```   154   assume npn: "~P n"
```
```   155   have "!k q. q + k = m \<longrightarrow> P q"
```
```   156   proof
```
```   157     fix k
```
```   158     show "!q. q + k = m \<longrightarrow> P q"
```
```   159     proof (induct k,simp_all)
```
```   160       show "P m" .
```
```   161     next
```
```   162       fix k
```
```   163       assume ind: "!q. q + k = m \<longrightarrow> P q"
```
```   164       show "!q. Suc (q + k) = m \<longrightarrow> P q"
```
```   165       proof (rule+)
```
```   166 	fix q
```
```   167 	assume "Suc (q + k) = m"
```
```   168 	hence "(Suc q) + k = m"
```
```   169 	  by simp
```
```   170 	with ind
```
```   171 	have psq: "P (Suc q)"
```
```   172 	  by simp
```
```   173 	from alln
```
```   174 	have "P (Suc q) --> P q"
```
```   175 	  ..
```
```   176 	with psq
```
```   177 	show "P q"
```
```   178 	  by simp
```
```   179       qed
```
```   180     qed
```
```   181   qed
```
```   182   hence "!q. q + (m - n) = m \<longrightarrow> P q"
```
```   183     ..
```
```   184   hence hehe: "n + (m - n) = m \<longrightarrow> P n"
```
```   185     ..
```
```   186   show "m < n"
```
```   187   proof (rule classical)
```
```   188     assume "~(m<n)"
```
```   189     hence "n <= m"
```
```   190       by simp
```
```   191     with hehe
```
```   192     have "P n"
```
```   193       by simp
```
```   194     with npn
```
```   195     show "m < n"
```
```   196       ..
```
```   197   qed
```
```   198 qed;
```
```   199
```
```   200 constdefs
```
```   201   FUNPOW :: "('a => 'a) => nat => 'a => 'a"
```
```   202   "FUNPOW f n == f ^ n"
```
```   203
```
```   204 lemma FUNPOW: "(ALL f x. (f ^ 0) x = x) &
```
```   205   (ALL f n x. (f ^ Suc n) x = (f ^ n) (f x))"
```
```   206 proof auto
```
```   207   fix f n x
```
```   208   have "ALL x. f ((f ^ n) x) = (f ^ n) (f x)"
```
```   209     by (induct n,auto)
```
```   210   thus "f ((f ^ n) x) = (f ^ n) (f x)"
```
```   211     ..
```
```   212 qed
```
```   213
```
```   214 lemma [hol4rew]: "FUNPOW f n = f ^ n"
```
```   215   by (simp add: FUNPOW_def)
```
```   216
```
```   217 lemma ADD: "(!n. (0::nat) + n = n) & (!m n. Suc m + n = Suc (m + n))"
```
```   218   by simp
```
```   219
```
```   220 lemma MULT: "(!n. (0::nat) * n = 0) & (!m n. Suc m * n = m * n + n)"
```
```   221   by simp
```
```   222
```
```   223 lemma SUB: "(!m. (0::nat) - m = 0) & (!m n. (Suc m) - n = (if m < n then 0 else Suc (m - n)))"
```
```   224   by (simp, arith)
```
```   225
```
```   226 lemma MAX_DEF: "max (m::nat) n = (if m < n then n else m)"
```
```   227   by (simp add: max_def)
```
```   228
```
```   229 lemma MIN_DEF: "min (m::nat) n = (if m < n then m else n)"
```
```   230   by (simp add: min_def)
```
```   231
```
```   232 lemma DIVISION: "(0::nat) < n --> (!k. (k = k div n * n + k mod n) & k mod n < n)"
```
```   233   by simp
```
```   234
```
```   235 constdefs
```
```   236   ALT_ZERO :: nat
```
```   237   "ALT_ZERO == 0"
```
```   238   NUMERAL_BIT1 :: "nat \<Rightarrow> nat"
```
```   239   "NUMERAL_BIT1 n == n + (n + Suc 0)"
```
```   240   NUMERAL_BIT2 :: "nat \<Rightarrow> nat"
```
```   241   "NUMERAL_BIT2 n == n + (n + Suc (Suc 0))"
```
```   242   NUMERAL :: "nat \<Rightarrow> nat"
```
```   243   "NUMERAL x == x"
```
```   244
```
```   245 lemma [hol4rew]: "NUMERAL ALT_ZERO = 0"
```
```   246   by (simp add: ALT_ZERO_def NUMERAL_def)
```
```   247
```
```   248 lemma [hol4rew]: "NUMERAL (NUMERAL_BIT1 ALT_ZERO) = 1"
```
```   249   by (simp add: ALT_ZERO_def NUMERAL_BIT1_def NUMERAL_def)
```
```   250
```
```   251 lemma [hol4rew]: "NUMERAL (NUMERAL_BIT2 ALT_ZERO) = 2"
```
```   252   by (simp add: ALT_ZERO_def NUMERAL_BIT2_def NUMERAL_def)
```
```   253
```
```   254 lemma EXP: "(!m. m ^ 0 = (1::nat)) & (!m n. m ^ Suc n = m * (m::nat) ^ n)"
```
```   255   by auto
```
```   256
```
```   257 lemma num_case_def: "(!b f. nat_case b f 0 = b) & (!b f n. nat_case b f (Suc n) = f n)"
```
```   258   by simp;
```
```   259
```
```   260 lemma divides_def: "(a::nat) dvd b = (? q. b = q * a)"
```
```   261   by (auto simp add: dvd_def);
```
```   262
```
```   263 lemma list_case_def: "(!v f. list_case v f [] = v) & (!v f a0 a1. list_case v f (a0#a1) = f a0 a1)"
```
```   264   by simp
```
```   265
```
```   266 consts
```
```   267   list_size :: "('a \<Rightarrow> nat) \<Rightarrow> 'a list \<Rightarrow> nat"
```
```   268
```
```   269 primrec
```
```   270   "list_size f [] = 0"
```
```   271   "list_size f (a0#a1) = 1 + (f a0 + list_size f a1)"
```
```   272
```
```   273 lemma list_size_def: "(!f. list_size f [] = 0) &
```
```   274          (!f a0 a1. list_size f (a0#a1) = 1 + (f a0 + list_size f a1))"
```
```   275   by simp
```
```   276
```
```   277 lemma list_case_cong: "! M M' v f. M = M' & (M' = [] \<longrightarrow>  v = v') &
```
```   278            (!a0 a1. (M' = a0#a1) \<longrightarrow> (f a0 a1 = f' a0 a1)) -->
```
```   279            (list_case v f M = list_case v' f' M')"
```
```   280 proof clarify
```
```   281   fix M M' v f
```
```   282   assume "M' = [] \<longrightarrow> v = v'"
```
```   283     and "!a0 a1. M' = a0 # a1 \<longrightarrow> f a0 a1 = f' a0 a1"
```
```   284   show "list_case v f M' = list_case v' f' M'"
```
```   285   proof (rule List.list.case_cong)
```
```   286     show "M' = M'"
```
```   287       ..
```
```   288   next
```
```   289     assume "M' = []"
```
```   290     with prems
```
```   291     show "v = v'"
```
```   292       by auto
```
```   293   next
```
```   294     fix a0 a1
```
```   295     assume "M' = a0 # a1"
```
```   296     with prems
```
```   297     show "f a0 a1 = f' a0 a1"
```
```   298       by auto
```
```   299   qed
```
```   300 qed
```
```   301
```
```   302 lemma list_Axiom: "ALL f0 f1. EX fn. (fn [] = f0) & (ALL a0 a1. fn (a0#a1) = f1 a0 a1 (fn a1))"
```
```   303 proof safe
```
```   304   fix f0 f1
```
```   305   def fn == "list_rec f0 f1"
```
```   306   have "fn [] = f0 & (ALL a0 a1. fn (a0 # a1) = f1 a0 a1 (fn a1))"
```
```   307     by (simp add: fn_def)
```
```   308   thus "EX fn. fn [] = f0 & (ALL a0 a1. fn (a0 # a1) = f1 a0 a1 (fn a1))"
```
```   309     by auto
```
```   310 qed
```
```   311
```
```   312 lemma list_Axiom_old: "EX! fn. (fn [] = x) & (ALL h t. fn (h#t) = f (fn t) h t)"
```
```   313 proof safe
```
```   314   def fn == "list_rec x (%h t r. f r h t)"
```
```   315   have "fn [] = x & (ALL h t. fn (h # t) = f (fn t) h t)"
```
```   316     by (simp add: fn_def)
```
```   317   thus "EX fn. fn [] = x & (ALL h t. fn (h # t) = f (fn t) h t)"
```
```   318     by auto
```
```   319 next
```
```   320   fix fn1 fn2
```
```   321   assume "ALL h t. fn1 (h # t) = f (fn1 t) h t"
```
```   322   assume "ALL h t. fn2 (h # t) = f (fn2 t) h t"
```
```   323   assume "fn2 [] = fn1 []"
```
```   324   show "fn1 = fn2"
```
```   325   proof
```
```   326     fix xs
```
```   327     show "fn1 xs = fn2 xs"
```
```   328       by (induct xs,simp_all add: prems)
```
```   329   qed
```
```   330 qed
```
```   331
```
```   332 lemma NULL_DEF: "(null [] = True) & (!h t. null (h # t) = False)"
```
```   333   by simp
```
```   334
```
```   335 constdefs
```
```   336   sum :: "nat list \<Rightarrow> nat"
```
```   337   "sum l == foldr (op +) l 0"
```
```   338
```
```   339 lemma SUM: "(sum [] = 0) & (!h t. sum (h#t) = h + sum t)"
```
```   340   by (simp add: sum_def)
```
```   341
```
```   342 lemma APPEND: "(!l. [] @ l = l) & (!l1 l2 h. (h#l1) @ l2 = h# l1 @ l2)"
```
```   343   by simp
```
```   344
```
```   345 lemma FLAT: "(concat [] = []) & (!h t. concat (h#t) = h @ (concat t))"
```
```   346   by simp
```
```   347
```
```   348 lemma LENGTH: "(length [] = 0) & (!h t. length (h#t) = Suc (length t))"
```
```   349   by simp
```
```   350
```
```   351 lemma MAP: "(!f. map f [] = []) & (!f h t. map f (h#t) = f h#map f t)"
```
```   352   by simp
```
```   353
```
```   354 lemma MEM: "(!x. x mem [] = False) & (!x h t. x mem (h#t) = ((x = h) | x mem t))"
```
```   355   by auto
```
```   356
```
```   357 lemma FILTER: "(!P. filter P [] = []) & (!P h t.
```
```   358            filter P (h#t) = (if P h then h#filter P t else filter P t))"
```
```   359   by simp
```
```   360
```
```   361 lemma REPLICATE: "(ALL x. replicate 0 x = []) &
```
```   362   (ALL n x. replicate (Suc n) x = x # replicate n x)"
```
```   363   by simp
```
```   364
```
```   365 constdefs
```
```   366   FOLDR :: "[['a,'b]\<Rightarrow>'b,'b,'a list] \<Rightarrow> 'b"
```
```   367   "FOLDR f e l == foldr f l e"
```
```   368
```
```   369 lemma [hol4rew]: "FOLDR f e l = foldr f l e"
```
```   370   by (simp add: FOLDR_def)
```
```   371
```
```   372 lemma FOLDR: "(!f e. foldr f [] e = e) & (!f e x l. foldr f (x#l) e = f x (foldr f l e))"
```
```   373   by simp
```
```   374
```
```   375 lemma FOLDL: "(!f e. foldl f e [] = e) & (!f e x l. foldl f e (x#l) = foldl f (f e x) l)"
```
```   376   by simp
```
```   377
```
```   378 lemma EVERY_DEF: "(!P. list_all P [] = True) & (!P h t. list_all P (h#t) = (P h & list_all P t))"
```
```   379   by simp
```
```   380
```
```   381 consts
```
```   382   list_exists :: "['a \<Rightarrow> bool,'a list] \<Rightarrow> bool"
```
```   383
```
```   384 primrec
```
```   385   list_exists_Nil: "list_exists P Nil = False"
```
```   386   list_exists_Cons: "list_exists P (x#xs) = (if P x then True else list_exists P xs)"
```
```   387
```
```   388 lemma list_exists_DEF: "(!P. list_exists P [] = False) &
```
```   389          (!P h t. list_exists P (h#t) = (P h | list_exists P t))"
```
```   390   by simp
```
```   391
```
```   392 consts
```
```   393   map2 :: "[['a,'b]\<Rightarrow>'c,'a list,'b list] \<Rightarrow> 'c list"
```
```   394
```
```   395 primrec
```
```   396   map2_Nil: "map2 f [] l2 = []"
```
```   397   map2_Cons: "map2 f (x#xs) l2 = f x (hd l2) # map2 f xs (tl l2)"
```
```   398
```
```   399 lemma MAP2: "(!f. map2 f [] [] = []) & (!f h1 t1 h2 t2. map2 f (h1#t1) (h2#t2) = f h1 h2#map2 f t1 t2)"
```
```   400   by simp
```
```   401
```
```   402 lemma list_INDUCT: "\<lbrakk> P [] ; !t. P t \<longrightarrow> (!h. P (h#t)) \<rbrakk> \<Longrightarrow> !l. P l"
```
```   403 proof
```
```   404   fix l
```
```   405   assume "P []"
```
```   406   assume allt: "!t. P t \<longrightarrow> (!h. P (h # t))"
```
```   407   show "P l"
```
```   408   proof (induct l)
```
```   409     show "P []" .
```
```   410   next
```
```   411     fix h t
```
```   412     assume "P t"
```
```   413     with allt
```
```   414     have "!h. P (h # t)"
```
```   415       by auto
```
```   416     thus "P (h # t)"
```
```   417       ..
```
```   418   qed
```
```   419 qed
```
```   420
```
```   421 lemma list_CASES: "(l = []) | (? t h. l = h#t)"
```
```   422   by (induct l,auto)
```
```   423
```
```   424 constdefs
```
```   425   ZIP :: "'a list * 'b list \<Rightarrow> ('a * 'b) list"
```
```   426   "ZIP == %(a,b). zip a b"
```
```   427
```
```   428 lemma ZIP: "(zip [] [] = []) &
```
```   429   (!x1 l1 x2 l2. zip (x1#l1) (x2#l2) = (x1,x2)#zip l1 l2)"
```
```   430   by simp
```
```   431
```
```   432 lemma [hol4rew]: "ZIP (a,b) = zip a b"
```
```   433   by (simp add: ZIP_def)
```
```   434
```
```   435 consts
```
```   436   unzip :: "('a * 'b) list \<Rightarrow> 'a list * 'b list"
```
```   437
```
```   438 primrec
```
```   439   unzip_Nil: "unzip [] = ([],[])"
```
```   440   unzip_Cons: "unzip (xy#xys) = (let zs = unzip xys in (fst xy # fst zs,snd xy # snd zs))"
```
```   441
```
```   442 lemma UNZIP: "(unzip [] = ([],[])) &
```
```   443          (!x l. unzip (x#l) = (fst x#fst (unzip l),snd x#snd (unzip l)))"
```
```   444   by (simp add: Let_def)
```
```   445
```
```   446 lemma REVERSE: "(rev [] = []) & (!h t. rev (h#t) = (rev t) @ [h])"
```
```   447   by simp;
```
```   448
```
```   449 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)"
```
```   450 proof safe
```
```   451   fix x z
```
```   452   assume allx: "ALL x. P x \<longrightarrow> 0 < x"
```
```   453   assume px: "P x"
```
```   454   assume allx': "ALL x. P x \<longrightarrow> x < z"
```
```   455   have "EX s. ALL y. (EX x : Collect P. y < x) = (y < s)"
```
```   456   proof (rule posreal_complete)
```
```   457     show "ALL x : Collect P. 0 < x"
```
```   458     proof safe
```
```   459       fix x
```
```   460       assume "P x"
```
```   461       from allx
```
```   462       have "P x \<longrightarrow> 0 < x"
```
```   463 	..
```
```   464       thus "0 < x"
```
```   465 	by (simp add: prems)
```
```   466     qed
```
```   467   next
```
```   468     from px
```
```   469     show "EX x. x : Collect P"
```
```   470       by auto
```
```   471   next
```
```   472     from allx'
```
```   473     show "EX y. ALL x : Collect P. x < y"
```
```   474       apply simp
```
```   475       ..
```
```   476   qed
```
```   477   thus "EX s. ALL y. (EX x. P x & y < x) = (y < s)"
```
```   478     by simp
```
```   479 qed
```
```   480
```
```   481 lemma REAL_10: "~((1::real) = 0)"
```
```   482   by simp
```
```   483
```
```   484 lemma REAL_ADD_ASSOC: "(x::real) + (y + z) = x + y + z"
```
```   485   by simp
```
```   486
```
```   487 lemma REAL_MUL_ASSOC: "(x::real) * (y * z) = x * y * z"
```
```   488   by simp
```
```   489
```
```   490 lemma REAL_ADD_LINV:  "-x + x = (0::real)"
```
```   491   by simp
```
```   492
```
```   493 lemma REAL_MUL_LINV: "x ~= (0::real) ==> inverse x * x = 1"
```
```   494   by simp
```
```   495
```
```   496 lemma REAL_LT_TOTAL: "((x::real) = y) | x < y | y < x"
```
```   497   by auto;
```
```   498
```
```   499 lemma [hol4rew]: "real (0::nat) = 0"
```
```   500   by simp
```
```   501
```
```   502 lemma [hol4rew]: "real (1::nat) = 1"
```
```   503   by simp
```
```   504
```
```   505 lemma [hol4rew]: "real (2::nat) = 2"
```
```   506   by simp
```
```   507
```
```   508 lemma real_lte: "((x::real) <= y) = (~(y < x))"
```
```   509   by auto
```
```   510
```
```   511 lemma real_of_num: "((0::real) = 0) & (!n. real (Suc n) = real n + 1)"
```
```   512   by (simp add: real_of_nat_Suc)
```
```   513
```
```   514 lemma abs: "abs (x::real) = (if 0 <= x then x else -x)"
```
```   515   by (simp add: abs_if)
```
```   516
```
```   517 lemma pow: "(!x::real. x ^ 0 = 1) & (!x::real. ALL n. x ^ (Suc n) = x * x ^ n)"
```
```   518   by simp
```
```   519
```
```   520 constdefs
```
```   521   real_gt :: "real => real => bool"
```
```   522   "real_gt == %x y. y < x"
```
```   523
```
```   524 lemma [hol4rew]: "real_gt x y = (y < x)"
```
```   525   by (simp add: real_gt_def)
```
```   526
```
```   527 lemma real_gt: "ALL x (y::real). (y < x) = (y < x)"
```
```   528   by simp
```
```   529
```
```   530 constdefs
```
```   531   real_ge :: "real => real => bool"
```
```   532   "real_ge x y == y <= x"
```
```   533
```
```   534 lemma [hol4rew]: "real_ge x y = (y <= x)"
```
```   535   by (simp add: real_ge_def)
```
```   536
```
```   537 lemma real_ge: "ALL x y. (y <= x) = (y <= x)"
```
```   538   by simp
```
```   539
```
```   540 end
```