src/HOL/Import/HOLLight/HOLLight.thy
author Cezary Kaliszyk <kaliszyk@in.tum.de>
Sat Jul 16 00:01:17 2011 +0200 (2011-07-16)
changeset 43843 16f2fd9103bd
parent 43786 fea3ed6951e3
child 44633 8a2fd7418435
permissions -rw-r--r--
HOL/Import: Fix errors with _mk_list
obua@17644
     1
(* AUTOMATICALLY GENERATED, DO NOT EDIT! *)
obua@17644
     2
kaliszyk@43786
     3
theory HOLLight imports "../HOLLightCompat" "../HOL4Syntax" begin 
obua@17644
     4
obua@17644
     5
;setup_theory hollight
obua@17644
     6
obua@17644
     7
consts
obua@17644
     8
  "_FALSITY_" :: "bool" ("'_FALSITY'_")
obua@17644
     9
obua@17644
    10
defs
obua@17644
    11
  "_FALSITY__def": "_FALSITY_ == False"
obua@17644
    12
obua@17644
    13
lemma DEF__FALSITY_: "_FALSITY_ = False"
obua@17644
    14
  by (import hollight DEF__FALSITY_)
obua@17644
    15
kaliszyk@43786
    16
lemma CONJ_ACI: "(p & q) = (q & p) &
kaliszyk@43786
    17
((p & q) & r) = (p & q & r) &
obua@17644
    18
(p & q & r) = (q & p & r) & (p & p) = p & (p & p & q) = (p & q)"
obua@17644
    19
  by (import hollight CONJ_ACI)
obua@17644
    20
kaliszyk@43786
    21
lemma DISJ_ACI: "(p | q) = (q | p) &
kaliszyk@43786
    22
((p | q) | r) = (p | q | r) &
obua@17644
    23
(p | q | r) = (q | p | r) & (p | p) = p & (p | p | q) = (p | q)"
obua@17644
    24
  by (import hollight DISJ_ACI)
obua@17644
    25
kaliszyk@43786
    26
lemma IMP_CONJ_ALT: "(p & q --> r) = (q --> p --> r)"
kaliszyk@43786
    27
  by (import hollight IMP_CONJ_ALT)
kaliszyk@43786
    28
kaliszyk@43786
    29
lemma EQ_CLAUSES: "(True = t) = t & (t = True) = t & (False = t) = (~ t) & (t = False) = (~ t)"
obua@17644
    30
  by (import hollight EQ_CLAUSES)
obua@17644
    31
obua@17644
    32
lemma NOT_CLAUSES_WEAK: "(~ True) = False & (~ False) = True"
obua@17644
    33
  by (import hollight NOT_CLAUSES_WEAK)
obua@17644
    34
kaliszyk@43786
    35
lemma AND_CLAUSES: "(True & t) = t &
kaliszyk@43786
    36
(t & True) = t & (False & t) = False & (t & False) = False & (t & t) = t"
obua@17644
    37
  by (import hollight AND_CLAUSES)
obua@17644
    38
kaliszyk@43786
    39
lemma OR_CLAUSES: "(True | t) = True &
kaliszyk@43786
    40
(t | True) = True & (False | t) = t & (t | False) = t & (t | t) = t"
obua@17644
    41
  by (import hollight OR_CLAUSES)
obua@17644
    42
kaliszyk@43786
    43
lemma IMP_CLAUSES: "(True --> t) = t &
kaliszyk@43786
    44
(t --> True) = True &
kaliszyk@43786
    45
(False --> t) = True & (t --> t) = True & (t --> False) = (~ t)"
obua@17644
    46
  by (import hollight IMP_CLAUSES)
obua@17644
    47
kaliszyk@43786
    48
lemma IMP_EQ_CLAUSE: "((x::'q_851) = x --> (p::bool)) = p"
obua@17644
    49
  by (import hollight IMP_EQ_CLAUSE)
obua@17644
    50
kaliszyk@43786
    51
lemma TRIV_EXISTS_AND_THM: "(EX x::'A. (P::bool) & (Q::bool)) = ((EX x::'A. P) & (EX x::'A. Q))"
obua@17644
    52
  by (import hollight TRIV_EXISTS_AND_THM)
obua@17644
    53
kaliszyk@43786
    54
lemma TRIV_AND_EXISTS_THM: "((EX x::'A. (P::bool)) & (EX x::'A. (Q::bool))) = (EX x::'A. P & Q)"
obua@17644
    55
  by (import hollight TRIV_AND_EXISTS_THM)
obua@17644
    56
kaliszyk@43786
    57
lemma TRIV_FORALL_OR_THM: "(ALL x::'A. (P::bool) | (Q::bool)) = ((ALL x::'A. P) | (ALL x::'A. Q))"
obua@17644
    58
  by (import hollight TRIV_FORALL_OR_THM)
obua@17644
    59
kaliszyk@43786
    60
lemma TRIV_OR_FORALL_THM: "((ALL x::'A. (P::bool)) | (ALL x::'A. (Q::bool))) = (ALL x::'A. P | Q)"
obua@17644
    61
  by (import hollight TRIV_OR_FORALL_THM)
obua@17644
    62
kaliszyk@43786
    63
lemma TRIV_FORALL_IMP_THM: "(ALL x::'A. (P::bool) --> (Q::bool)) = ((EX x::'A. P) --> (ALL x::'A. Q))"
obua@17644
    64
  by (import hollight TRIV_FORALL_IMP_THM)
obua@17644
    65
kaliszyk@43786
    66
lemma TRIV_EXISTS_IMP_THM: "(EX x::'A. (P::bool) --> (Q::bool)) = ((ALL x::'A. P) --> (EX x::'A. Q))"
obua@17644
    67
  by (import hollight TRIV_EXISTS_IMP_THM)
obua@17644
    68
kaliszyk@43786
    69
lemma EXISTS_UNIQUE_ALT: "Ex1 (P::'A => bool) = (EX x::'A. ALL y::'A. P y = (x = y))"
obua@17644
    70
  by (import hollight EXISTS_UNIQUE_ALT)
obua@17644
    71
kaliszyk@43786
    72
lemma SELECT_UNIQUE: "(!!y::'A. (P::'A => bool) y = (y = (x::'A))) ==> Eps P = x"
obua@17644
    73
  by (import hollight SELECT_UNIQUE)
obua@17644
    74
kaliszyk@43786
    75
lemma EXCLUDED_MIDDLE: "t | ~ t"
obua@17644
    76
  by (import hollight EXCLUDED_MIDDLE)
obua@17644
    77
kaliszyk@43786
    78
lemma COND_CLAUSES: "(if True then x::'A else (xa::'A)) = x & (if False then x else xa) = xa"
obua@17644
    79
  by (import hollight COND_CLAUSES)
obua@17644
    80
kaliszyk@43786
    81
lemma COND_EXPAND: "(if b then t1 else t2) = ((~ b | t1) & (b | t2))"
obua@17644
    82
  by (import hollight COND_EXPAND)
obua@17644
    83
kaliszyk@43786
    84
lemma COND_RATOR: "(if b::bool then f::'A => 'B else (g::'A => 'B)) (x::'A) =
kaliszyk@43786
    85
(if b then f x else g x)"
obua@17644
    86
  by (import hollight COND_RATOR)
obua@17644
    87
kaliszyk@43786
    88
lemma COND_ABS: "(%x::'A. if b::bool then (f::'A => 'B) x else (g::'A => 'B) x) =
kaliszyk@43786
    89
(if b then f else g)"
obua@17644
    90
  by (import hollight COND_ABS)
obua@17644
    91
kaliszyk@43786
    92
lemma MONO_COND: "[| (A --> B) & (C --> D); if b then A else C |] ==> if b then B else D"
obua@17644
    93
  by (import hollight MONO_COND)
obua@17644
    94
kaliszyk@43786
    95
lemma SKOLEM_THM: "(ALL x::'A. Ex ((P::'A => 'B => bool) x)) =
kaliszyk@43786
    96
(EX x::'A => 'B. ALL xa::'A. P xa (x xa))"
obua@17644
    97
  by (import hollight SKOLEM_THM)
obua@17644
    98
kaliszyk@43786
    99
lemma UNIQUE_SKOLEM_ALT: "(ALL x::'A. Ex1 ((P::'A => 'B => bool) x)) =
kaliszyk@43786
   100
(EX f::'A => 'B. ALL (x::'A) y::'B. P x y = (f x = y))"
obua@17644
   101
  by (import hollight UNIQUE_SKOLEM_ALT)
obua@17644
   102
kaliszyk@43786
   103
lemma COND_EQ_CLAUSE: "(if (x::'q_2963) = x then y::'q_2956 else (z::'q_2956)) = y"
obua@17644
   104
  by (import hollight COND_EQ_CLAUSE)
obua@17644
   105
kaliszyk@43786
   106
lemma bool_RECURSION: "EX x::bool => 'A. x False = (a::'A) & x True = (b::'A)"
kaliszyk@43786
   107
  by (import hollight bool_RECURSION)
kaliszyk@43786
   108
kaliszyk@43786
   109
lemma o_ASSOC: "(f::'C => 'D) o ((g::'B => 'C) o (h::'A => 'B)) = f o g o h"
obua@17644
   110
  by (import hollight o_ASSOC)
obua@17644
   111
kaliszyk@43786
   112
lemma I_O_ID: "id o (f::'A => 'B) = f & f o id = f"
obua@17644
   113
  by (import hollight I_O_ID)
obua@17644
   114
kaliszyk@43786
   115
lemma EXISTS_ONE_REP: "EX x. x"
obua@17644
   116
  by (import hollight EXISTS_ONE_REP)
obua@17644
   117
kaliszyk@43786
   118
lemma one_axiom: "(f::'A => unit) = (x::'A => unit)"
obua@17644
   119
  by (import hollight one_axiom)
obua@17644
   120
kaliszyk@43786
   121
lemma one_RECURSION: "EX x::unit => 'A. x () = (e::'A)"
obua@17644
   122
  by (import hollight one_RECURSION)
obua@17644
   123
kaliszyk@43786
   124
lemma one_Axiom: "EX! fn::unit => 'A. fn () = (e::'A)"
obua@17644
   125
  by (import hollight one_Axiom)
obua@17644
   126
kaliszyk@43786
   127
lemma th_cond: "(b = False --> x = x0) & (b = True --> x = x1) ==> x = (b & x1 | ~ b & x0)"
obua@17644
   128
  by (import hollight th_cond)
obua@17644
   129
kaliszyk@43786
   130
definition
kaliszyk@43786
   131
  LET_END :: "'A => 'A"  where
kaliszyk@43786
   132
  "LET_END == %t::'A. t"
kaliszyk@43786
   133
kaliszyk@43786
   134
lemma DEF_LET_END: "LET_END = (%t::'A. t)"
obua@17644
   135
  by (import hollight DEF_LET_END)
obua@17644
   136
kaliszyk@43786
   137
consts
kaliszyk@43786
   138
  "_SEQPATTERN" :: "('q_4007 => 'q_4004 => bool)
kaliszyk@43786
   139
=> ('q_4007 => 'q_4004 => bool) => 'q_4007 => 'q_4004 => bool" ("'_SEQPATTERN")
kaliszyk@43786
   140
kaliszyk@43786
   141
defs
kaliszyk@43786
   142
  "_SEQPATTERN_def": "_SEQPATTERN ==
kaliszyk@43786
   143
%(r::'q_4007 => 'q_4004 => bool) (s::'q_4007 => 'q_4004 => bool) x::'q_4007.
kaliszyk@43786
   144
   if Ex (r x) then r x else s x"
kaliszyk@43786
   145
kaliszyk@43786
   146
lemma DEF__SEQPATTERN: "_SEQPATTERN =
kaliszyk@43786
   147
(%(r::'q_4007 => 'q_4004 => bool) (s::'q_4007 => 'q_4004 => bool)
kaliszyk@43786
   148
    x::'q_4007. if Ex (r x) then r x else s x)"
kaliszyk@43786
   149
  by (import hollight DEF__SEQPATTERN)
kaliszyk@43786
   150
kaliszyk@43786
   151
consts
kaliszyk@43786
   152
  "_UNGUARDED_PATTERN" :: "bool => bool => bool" ("'_UNGUARDED'_PATTERN")
kaliszyk@43786
   153
kaliszyk@43786
   154
defs
kaliszyk@43786
   155
  "_UNGUARDED_PATTERN_def": "_UNGUARDED_PATTERN == op &"
kaliszyk@43786
   156
kaliszyk@43786
   157
lemma DEF__UNGUARDED_PATTERN: "_UNGUARDED_PATTERN = op &"
kaliszyk@43786
   158
  by (import hollight DEF__UNGUARDED_PATTERN)
kaliszyk@43786
   159
kaliszyk@43786
   160
consts
kaliszyk@43786
   161
  "_GUARDED_PATTERN" :: "bool => bool => bool => bool" ("'_GUARDED'_PATTERN")
kaliszyk@43786
   162
kaliszyk@43786
   163
defs
kaliszyk@43786
   164
  "_GUARDED_PATTERN_def": "_GUARDED_PATTERN == %p g r. p & g & r"
kaliszyk@43786
   165
kaliszyk@43786
   166
lemma DEF__GUARDED_PATTERN: "_GUARDED_PATTERN = (%p g r. p & g & r)"
kaliszyk@43786
   167
  by (import hollight DEF__GUARDED_PATTERN)
kaliszyk@43786
   168
kaliszyk@43786
   169
consts
kaliszyk@43786
   170
  "_MATCH" :: "'q_4049 => ('q_4049 => 'q_4053 => bool) => 'q_4053" ("'_MATCH")
kaliszyk@43786
   171
kaliszyk@43786
   172
defs
kaliszyk@43786
   173
  "_MATCH_def": "_MATCH ==
kaliszyk@43786
   174
%(e::'q_4049) r::'q_4049 => 'q_4053 => bool.
kaliszyk@43786
   175
   if Ex1 (r e) then Eps (r e) else SOME z::'q_4053. False"
kaliszyk@43786
   176
kaliszyk@43786
   177
lemma DEF__MATCH: "_MATCH =
kaliszyk@43786
   178
(%(e::'q_4049) r::'q_4049 => 'q_4053 => bool.
kaliszyk@43786
   179
    if Ex1 (r e) then Eps (r e) else SOME z::'q_4053. False)"
kaliszyk@43786
   180
  by (import hollight DEF__MATCH)
kaliszyk@43786
   181
kaliszyk@43786
   182
consts
kaliszyk@43786
   183
  "_FUNCTION" :: "('q_4071 => 'q_4075 => bool) => 'q_4071 => 'q_4075" ("'_FUNCTION")
kaliszyk@43786
   184
kaliszyk@43786
   185
defs
kaliszyk@43786
   186
  "_FUNCTION_def": "_FUNCTION ==
kaliszyk@43786
   187
%(r::'q_4071 => 'q_4075 => bool) x::'q_4071.
kaliszyk@43786
   188
   if Ex1 (r x) then Eps (r x) else SOME z::'q_4075. False"
kaliszyk@43786
   189
kaliszyk@43786
   190
lemma DEF__FUNCTION: "_FUNCTION =
kaliszyk@43786
   191
(%(r::'q_4071 => 'q_4075 => bool) x::'q_4071.
kaliszyk@43786
   192
    if Ex1 (r x) then Eps (r x) else SOME z::'q_4075. False)"
kaliszyk@43786
   193
  by (import hollight DEF__FUNCTION)
kaliszyk@43786
   194
kaliszyk@43786
   195
lemma PAIR_EXISTS_THM: "EX (x::'A => 'B => bool) (a::'A) b::'B. x = Pair_Rep a b"
obua@17644
   196
  by (import hollight PAIR_EXISTS_THM)
obua@17644
   197
kaliszyk@43786
   198
lemma pair_RECURSION: "EX x::'A * 'B => 'C.
kaliszyk@43786
   199
   ALL (a0::'A) a1::'B. x (a0, a1) = (PAIR'::'A => 'B => 'C) a0 a1"
kaliszyk@43786
   200
  by (import hollight pair_RECURSION)
kaliszyk@43786
   201
kaliszyk@43786
   202
definition
kaliszyk@43786
   203
  UNCURRY :: "('A => 'B => 'C) => 'A * 'B => 'C"  where
kaliszyk@43786
   204
  "UNCURRY == %(u::'A => 'B => 'C) ua::'A * 'B. u (fst ua) (snd ua)"
kaliszyk@43786
   205
kaliszyk@43786
   206
lemma DEF_UNCURRY: "UNCURRY = (%(u::'A => 'B => 'C) ua::'A * 'B. u (fst ua) (snd ua))"
obua@17644
   207
  by (import hollight DEF_UNCURRY)
obua@17644
   208
kaliszyk@43786
   209
definition
kaliszyk@43786
   210
  PASSOC :: "(('A * 'B) * 'C => 'D) => 'A * 'B * 'C => 'D"  where
obua@17644
   211
  "PASSOC ==
kaliszyk@43786
   212
%(u::('A * 'B) * 'C => 'D) ua::'A * 'B * 'C.
obua@17644
   213
   u ((fst ua, fst (snd ua)), snd (snd ua))"
obua@17644
   214
obua@17644
   215
lemma DEF_PASSOC: "PASSOC =
kaliszyk@43786
   216
(%(u::('A * 'B) * 'C => 'D) ua::'A * 'B * 'C.
obua@17644
   217
    u ((fst ua, fst (snd ua)), snd (snd ua)))"
obua@17644
   218
  by (import hollight DEF_PASSOC)
obua@17644
   219
kaliszyk@43786
   220
lemma LAMBDA_PAIR_THM: "(x::'q_4547 * 'q_4546 => 'q_4539) =
kaliszyk@43786
   221
(SOME f::'q_4547 * 'q_4546 => 'q_4539.
kaliszyk@43786
   222
    ALL (xa::'q_4547) y::'q_4546. f (xa, y) = x (xa, y))"
kaliszyk@43786
   223
  by (import hollight LAMBDA_PAIR_THM)
kaliszyk@43786
   224
kaliszyk@43786
   225
lemma FORALL_PAIRED_THM: "All (SOME f::'q_4576 * 'q_4575 => bool.
kaliszyk@43786
   226
        ALL (x::'q_4576) y::'q_4575.
kaliszyk@43786
   227
           f (x, y) = (P::'q_4576 => 'q_4575 => bool) x y) =
kaliszyk@43786
   228
(ALL x::'q_4576. All (P x))"
kaliszyk@43786
   229
  by (import hollight FORALL_PAIRED_THM)
kaliszyk@43786
   230
kaliszyk@43786
   231
lemma EXISTS_PAIRED_THM: "Ex (SOME f::'q_4612 * 'q_4611 => bool.
kaliszyk@43786
   232
       ALL (x::'q_4612) y::'q_4611.
kaliszyk@43786
   233
          f (x, y) = (P::'q_4612 => 'q_4611 => bool) x y) =
kaliszyk@43786
   234
(EX x::'q_4612. Ex (P x))"
kaliszyk@43786
   235
  by (import hollight EXISTS_PAIRED_THM)
kaliszyk@43786
   236
kaliszyk@43786
   237
lemma FORALL_TRIPLED_THM: "All (SOME f::'q_4649 * 'q_4648 * 'q_4647 => bool.
kaliszyk@43786
   238
        ALL (x::'q_4649) (y::'q_4648) z::'q_4647.
kaliszyk@43786
   239
           f (x, y, z) = (P::'q_4649 => 'q_4648 => 'q_4647 => bool) x y z) =
kaliszyk@43786
   240
(ALL (x::'q_4649) y::'q_4648. All (P x y))"
kaliszyk@43786
   241
  by (import hollight FORALL_TRIPLED_THM)
kaliszyk@43786
   242
kaliszyk@43786
   243
lemma EXISTS_TRIPLED_THM: "Ex (SOME f::'q_4695 * 'q_4694 * 'q_4693 => bool.
kaliszyk@43786
   244
       ALL (x::'q_4695) (y::'q_4694) z::'q_4693.
kaliszyk@43786
   245
          f (x, y, z) = (P::'q_4695 => 'q_4694 => 'q_4693 => bool) x y z) =
kaliszyk@43786
   246
(EX (x::'q_4695) y::'q_4694. Ex (P x y))"
kaliszyk@43786
   247
  by (import hollight EXISTS_TRIPLED_THM)
kaliszyk@43786
   248
kaliszyk@43786
   249
lemma IND_SUC_0_EXISTS: "EX (x::ind => ind) z::ind.
kaliszyk@43786
   250
   (ALL (x1::ind) x2::ind. (x x1 = x x2) = (x1 = x2)) &
kaliszyk@43786
   251
   (ALL xa::ind. x xa ~= z)"
kaliszyk@43786
   252
  by (import hollight IND_SUC_0_EXISTS)
kaliszyk@43786
   253
kaliszyk@43786
   254
definition
kaliszyk@43786
   255
  IND_SUC :: "ind => ind"  where
kaliszyk@43786
   256
  "IND_SUC ==
kaliszyk@43786
   257
SOME f. EX z. (ALL x1 x2. (f x1 = f x2) = (x1 = x2)) & (ALL x. f x ~= z)"
kaliszyk@43786
   258
kaliszyk@43786
   259
lemma DEF_IND_SUC: "IND_SUC =
kaliszyk@43786
   260
(SOME f. EX z. (ALL x1 x2. (f x1 = f x2) = (x1 = x2)) & (ALL x. f x ~= z))"
kaliszyk@43786
   261
  by (import hollight DEF_IND_SUC)
kaliszyk@43786
   262
kaliszyk@43786
   263
definition
kaliszyk@43786
   264
  IND_0 :: "ind"  where
kaliszyk@43786
   265
  "IND_0 ==
kaliszyk@43786
   266
SOME z.
kaliszyk@43786
   267
   (ALL x1 x2. (IND_SUC x1 = IND_SUC x2) = (x1 = x2)) &
kaliszyk@43786
   268
   (ALL x. IND_SUC x ~= z)"
kaliszyk@43786
   269
kaliszyk@43786
   270
lemma DEF_IND_0: "IND_0 =
kaliszyk@43786
   271
(SOME z.
kaliszyk@43786
   272
    (ALL x1 x2. (IND_SUC x1 = IND_SUC x2) = (x1 = x2)) &
kaliszyk@43786
   273
    (ALL x. IND_SUC x ~= z))"
kaliszyk@43786
   274
  by (import hollight DEF_IND_0)
kaliszyk@43786
   275
kaliszyk@43786
   276
definition
kaliszyk@43786
   277
  NUM_REP :: "ind => bool"  where
kaliszyk@43786
   278
  "NUM_REP ==
kaliszyk@43786
   279
%a. ALL NUM_REP'.
kaliszyk@43786
   280
       (ALL a.
kaliszyk@43786
   281
           a = IND_0 | (EX i. a = IND_SUC i & NUM_REP' i) -->
kaliszyk@43786
   282
           NUM_REP' a) -->
kaliszyk@43786
   283
       NUM_REP' a"
kaliszyk@43786
   284
kaliszyk@43786
   285
lemma DEF_NUM_REP: "NUM_REP =
kaliszyk@43786
   286
(%a. ALL NUM_REP'.
kaliszyk@43786
   287
        (ALL a.
kaliszyk@43786
   288
            a = IND_0 | (EX i. a = IND_SUC i & NUM_REP' i) -->
kaliszyk@43786
   289
            NUM_REP' a) -->
kaliszyk@43786
   290
        NUM_REP' a)"
kaliszyk@43786
   291
  by (import hollight DEF_NUM_REP)
kaliszyk@43786
   292
kaliszyk@43786
   293
lemma num_RECURSION_STD: "EX fn::nat => 'Z.
kaliszyk@43786
   294
   fn (0::nat) = (e::'Z) &
kaliszyk@43786
   295
   (ALL n::nat. fn (Suc n) = (f::nat => 'Z => 'Z) n (fn n))"
kaliszyk@43786
   296
  by (import hollight num_RECURSION_STD)
kaliszyk@43786
   297
kaliszyk@43786
   298
lemma ADD_CLAUSES: "(ALL x::nat. (0::nat) + x = x) &
kaliszyk@43786
   299
(ALL x::nat. x + (0::nat) = x) &
obua@17644
   300
(ALL (x::nat) xa::nat. Suc x + xa = Suc (x + xa)) &
obua@17644
   301
(ALL (x::nat) xa::nat. x + Suc xa = Suc (x + xa))"
obua@17644
   302
  by (import hollight ADD_CLAUSES)
obua@17644
   303
obua@17644
   304
lemma ADD_AC: "(m::nat) + (n::nat) = n + m &
obua@17644
   305
m + n + (p::nat) = m + (n + p) & m + (n + p) = n + (m + p)"
obua@17644
   306
  by (import hollight ADD_AC)
obua@17644
   307
kaliszyk@43786
   308
lemma EQ_ADD_LCANCEL_0: "((m::nat) + (n::nat) = m) = (n = (0::nat))"
obua@17644
   309
  by (import hollight EQ_ADD_LCANCEL_0)
obua@17644
   310
kaliszyk@43786
   311
lemma EQ_ADD_RCANCEL_0: "((x::nat) + (xa::nat) = xa) = (x = (0::nat))"
obua@17644
   312
  by (import hollight EQ_ADD_RCANCEL_0)
obua@17644
   313
kaliszyk@43786
   314
lemma BIT1: "2 * x + 1 = Suc (x + x)"
kaliszyk@43786
   315
  by (import hollight BIT1)
kaliszyk@43786
   316
kaliszyk@43786
   317
lemma BIT1_THM: "2 * x + 1 = Suc (x + x)"
kaliszyk@43786
   318
  by (import hollight BIT1_THM)
kaliszyk@43786
   319
kaliszyk@43786
   320
lemma TWO: "2 = Suc 1"
obua@17644
   321
  by (import hollight TWO)
obua@17644
   322
kaliszyk@43786
   323
lemma MULT_CLAUSES: "(ALL x::nat. (0::nat) * x = (0::nat)) &
kaliszyk@43786
   324
(ALL x::nat. x * (0::nat) = (0::nat)) &
kaliszyk@43786
   325
(ALL x::nat. (1::nat) * x = x) &
kaliszyk@43786
   326
(ALL x::nat. x * (1::nat) = x) &
obua@17644
   327
(ALL (x::nat) xa::nat. Suc x * xa = x * xa + xa) &
obua@17644
   328
(ALL (x::nat) xa::nat. x * Suc xa = x + x * xa)"
obua@17644
   329
  by (import hollight MULT_CLAUSES)
obua@17644
   330
obua@17644
   331
lemma MULT_AC: "(m::nat) * (n::nat) = n * m &
obua@17644
   332
m * n * (p::nat) = m * (n * p) & m * (n * p) = n * (m * p)"
obua@17644
   333
  by (import hollight MULT_AC)
obua@17644
   334
kaliszyk@43786
   335
lemma EXP_EQ_1: "((x::nat) ^ (n::nat) = (1::nat)) = (x = (1::nat) | n = (0::nat))"
kaliszyk@43786
   336
  by (import hollight EXP_EQ_1)
kaliszyk@43786
   337
kaliszyk@43786
   338
lemma LT_ANTISYM: "~ ((m::nat) < (n::nat) & n < m)"
obua@17644
   339
  by (import hollight LT_ANTISYM)
obua@17644
   340
kaliszyk@43786
   341
lemma LET_ANTISYM: "~ ((m::nat) <= (n::nat) & n < m)"
obua@17644
   342
  by (import hollight LET_ANTISYM)
obua@17644
   343
kaliszyk@43786
   344
lemma LTE_ANTISYM: "~ ((x::nat) < (xa::nat) & xa <= x)"
obua@17644
   345
  by (import hollight LTE_ANTISYM)
obua@17644
   346
kaliszyk@43786
   347
lemma LT_CASES: "(m::nat) < (n::nat) | n < m | m = n"
obua@17644
   348
  by (import hollight LT_CASES)
obua@17644
   349
kaliszyk@43786
   350
lemma LTE_CASES: "(x::nat) < (xa::nat) | xa <= x"
obua@17644
   351
  by (import hollight LTE_CASES)
obua@17644
   352
kaliszyk@43786
   353
lemma LE_1: "(ALL x::nat. x ~= (0::nat) --> (0::nat) < x) &
kaliszyk@43786
   354
(ALL x::nat. x ~= (0::nat) --> (1::nat) <= x) &
kaliszyk@43786
   355
(ALL x>0::nat. x ~= (0::nat)) &
kaliszyk@43786
   356
(ALL x>0::nat. (1::nat) <= x) &
kaliszyk@43786
   357
(ALL x>=1::nat. (0::nat) < x) & (ALL x>=1::nat. x ~= (0::nat))"
kaliszyk@43786
   358
  by (import hollight LE_1)
kaliszyk@43786
   359
kaliszyk@43786
   360
lemma LT_EXISTS: "(m < n) = (EX d. n = m + Suc d)"
obua@17644
   361
  by (import hollight LT_EXISTS)
obua@17644
   362
kaliszyk@43786
   363
lemma LT_ADD: "((m::nat) < m + (n::nat)) = ((0::nat) < n)"
obua@17644
   364
  by (import hollight LT_ADD)
obua@17644
   365
kaliszyk@43786
   366
lemma LT_ADDR: "((xa::nat) < (x::nat) + xa) = ((0::nat) < x)"
obua@17644
   367
  by (import hollight LT_ADDR)
obua@17644
   368
kaliszyk@43786
   369
lemma LT_LMULT: "(m::nat) ~= (0::nat) & (n::nat) < (p::nat) ==> m * n < m * p"
obua@17644
   370
  by (import hollight LT_LMULT)
obua@17644
   371
kaliszyk@43786
   372
lemma LE_MULT_LCANCEL: "((m::nat) * (n::nat) <= m * (p::nat)) = (m = (0::nat) | n <= p)"
obua@17644
   373
  by (import hollight LE_MULT_LCANCEL)
obua@17644
   374
kaliszyk@43786
   375
lemma LE_MULT_RCANCEL: "((x::nat) * (xb::nat) <= (xa::nat) * xb) = (x <= xa | xb = (0::nat))"
obua@17644
   376
  by (import hollight LE_MULT_RCANCEL)
obua@17644
   377
kaliszyk@43786
   378
lemma LT_MULT_LCANCEL: "((m::nat) * (n::nat) < m * (p::nat)) = (m ~= (0::nat) & n < p)"
obua@17644
   379
  by (import hollight LT_MULT_LCANCEL)
obua@17644
   380
kaliszyk@43786
   381
lemma LT_MULT_RCANCEL: "((x::nat) * (xb::nat) < (xa::nat) * xb) = (x < xa & xb ~= (0::nat))"
obua@17644
   382
  by (import hollight LT_MULT_RCANCEL)
obua@17644
   383
kaliszyk@43786
   384
lemma LT_MULT2: "(m::nat) < (n::nat) & (p::nat) < (q::nat) ==> m * p < n * q"
obua@17644
   385
  by (import hollight LT_MULT2)
obua@17644
   386
obua@17644
   387
lemma WLOG_LE: "(ALL (m::nat) n::nat. (P::nat => nat => bool) m n = P n m) &
kaliszyk@43786
   388
(ALL (m::nat) n::nat. m <= n --> P m n)
kaliszyk@43786
   389
==> P (m::nat) (x::nat)"
obua@17644
   390
  by (import hollight WLOG_LE)
obua@17644
   391
obua@17644
   392
lemma WLOG_LT: "(ALL m::nat. (P::nat => nat => bool) m m) &
obua@17644
   393
(ALL (m::nat) n::nat. P m n = P n m) &
kaliszyk@43786
   394
(ALL (m::nat) n::nat. m < n --> P m n)
kaliszyk@43786
   395
==> P (m::nat) (x::nat)"
obua@17644
   396
  by (import hollight WLOG_LT)
obua@17644
   397
kaliszyk@43786
   398
lemma num_WOP: "Ex (P::nat => bool) = (EX n::nat. P n & (ALL m<n. ~ P m))"
obua@17644
   399
  by (import hollight num_WOP)
obua@17644
   400
kaliszyk@43786
   401
lemma num_MAX: "(Ex (P::nat => bool) & (EX M::nat. ALL x::nat. P x --> x <= M)) =
kaliszyk@43786
   402
(EX m::nat. P m & (ALL x::nat. P x --> x <= m))"
obua@17644
   403
  by (import hollight num_MAX)
obua@17644
   404
kaliszyk@43786
   405
lemma NOT_EVEN: "odd (n::nat) = odd n"
obua@17644
   406
  by (import hollight NOT_EVEN)
obua@17644
   407
kaliszyk@43786
   408
lemma NOT_ODD: "(~ odd (n::nat)) = even n"
obua@17644
   409
  by (import hollight NOT_ODD)
obua@17644
   410
kaliszyk@43786
   411
lemma EVEN_OR_ODD: "even (n::nat) | odd n"
obua@17644
   412
  by (import hollight EVEN_OR_ODD)
obua@17644
   413
kaliszyk@43786
   414
lemma EVEN_AND_ODD: "~ (even (x::nat) & odd x)"
obua@17644
   415
  by (import hollight EVEN_AND_ODD)
obua@17644
   416
kaliszyk@43786
   417
lemma EVEN_EXP: "even ((m::nat) ^ (n::nat)) = (even m & n ~= (0::nat))"
obua@17644
   418
  by (import hollight EVEN_EXP)
obua@17644
   419
kaliszyk@43786
   420
lemma ODD_MULT: "odd ((m::nat) * (n::nat)) = (odd m & odd n)"
obua@17644
   421
  by (import hollight ODD_MULT)
obua@17644
   422
kaliszyk@43786
   423
lemma ODD_EXP: "odd ((m::nat) ^ (n::nat)) = (odd m | n = (0::nat))"
obua@17644
   424
  by (import hollight ODD_EXP)
obua@17644
   425
kaliszyk@43786
   426
lemma EVEN_DOUBLE: "even ((2::nat) * (n::nat))"
obua@17644
   427
  by (import hollight EVEN_DOUBLE)
obua@17644
   428
kaliszyk@43786
   429
lemma ODD_DOUBLE: "odd (Suc (2 * x))"
obua@17644
   430
  by (import hollight ODD_DOUBLE)
obua@17644
   431
kaliszyk@43786
   432
lemma EVEN_EXISTS_LEMMA: "(even n --> (EX m. n = 2 * m)) & (odd n --> (EX m. n = Suc (2 * m)))"
obua@17644
   433
  by (import hollight EVEN_EXISTS_LEMMA)
obua@17644
   434
kaliszyk@43786
   435
lemma EVEN_ODD_DECOMPOSITION: "(EX (k::nat) m::nat. odd m & (n::nat) = (2::nat) ^ k * m) = (n ~= (0::nat))"
obua@17644
   436
  by (import hollight EVEN_ODD_DECOMPOSITION)
obua@17644
   437
kaliszyk@43786
   438
lemma SUB_0: "(0::nat) - (x::nat) = (0::nat) & x - (0::nat) = x"
obua@17644
   439
  by (import hollight SUB_0)
obua@17644
   440
kaliszyk@43786
   441
lemma SUB_PRESUC: "Suc m - n - Suc 0 = m - n"
obua@17644
   442
  by (import hollight SUB_PRESUC)
obua@17644
   443
kaliszyk@43786
   444
lemma ADD_SUBR: "(xa::nat) - ((x::nat) + xa) = (0::nat)"
obua@17644
   445
  by (import hollight ADD_SUBR)
obua@17644
   446
kaliszyk@43786
   447
lemma EVEN_SUB: "even ((m::nat) - (n::nat)) = (m <= n | even m = even n)"
kaliszyk@43786
   448
  by (import hollight EVEN_SUB)
kaliszyk@43786
   449
kaliszyk@43786
   450
lemma ODD_SUB: "odd ((x::nat) - (xa::nat)) = (xa < x & odd x ~= odd xa)"
kaliszyk@43786
   451
  by (import hollight ODD_SUB)
kaliszyk@43786
   452
kaliszyk@43786
   453
lemma EXP_LT_0: "((0::nat) < (xa::nat) ^ (x::nat)) = (xa ~= (0::nat) | x = (0::nat))"
kaliszyk@43786
   454
  by (import hollight EXP_LT_0)
kaliszyk@43786
   455
kaliszyk@43786
   456
lemma LT_EXP: "((x::nat) ^ (m::nat) < x ^ (n::nat)) =
kaliszyk@43786
   457
((2::nat) <= x & m < n | x = (0::nat) & m ~= (0::nat) & n = (0::nat))"
kaliszyk@43786
   458
  by (import hollight LT_EXP)
kaliszyk@43786
   459
kaliszyk@43786
   460
lemma LE_EXP: "((x::nat) ^ (m::nat) <= x ^ (n::nat)) =
kaliszyk@43786
   461
(if x = (0::nat) then m = (0::nat) --> n = (0::nat)
kaliszyk@43786
   462
 else x = (1::nat) | m <= n)"
kaliszyk@43786
   463
  by (import hollight LE_EXP)
kaliszyk@43786
   464
kaliszyk@43786
   465
lemma EQ_EXP: "((x::nat) ^ (m::nat) = x ^ (n::nat)) =
kaliszyk@43786
   466
(if x = (0::nat) then (m = (0::nat)) = (n = (0::nat))
kaliszyk@43786
   467
 else x = (1::nat) | m = n)"
kaliszyk@43786
   468
  by (import hollight EQ_EXP)
kaliszyk@43786
   469
kaliszyk@43786
   470
lemma EXP_MONO_LE_IMP: "(x::nat) <= (xa::nat) ==> x ^ (xb::nat) <= xa ^ xb"
kaliszyk@43786
   471
  by (import hollight EXP_MONO_LE_IMP)
kaliszyk@43786
   472
kaliszyk@43786
   473
lemma EXP_MONO_LT_IMP: "(x::nat) < (y::nat) & (n::nat) ~= (0::nat) ==> x ^ n < y ^ n"
kaliszyk@43786
   474
  by (import hollight EXP_MONO_LT_IMP)
kaliszyk@43786
   475
kaliszyk@43786
   476
lemma EXP_MONO_LE: "((x::nat) ^ (n::nat) <= (y::nat) ^ n) = (x <= y | n = (0::nat))"
kaliszyk@43786
   477
  by (import hollight EXP_MONO_LE)
kaliszyk@43786
   478
kaliszyk@43786
   479
lemma EXP_MONO_LT: "((x::nat) ^ (xb::nat) < (xa::nat) ^ xb) = (x < xa & xb ~= (0::nat))"
kaliszyk@43786
   480
  by (import hollight EXP_MONO_LT)
kaliszyk@43786
   481
kaliszyk@43786
   482
lemma EXP_MONO_EQ: "((x::nat) ^ (xb::nat) = (xa::nat) ^ xb) = (x = xa | xb = (0::nat))"
kaliszyk@43786
   483
  by (import hollight EXP_MONO_EQ)
kaliszyk@43786
   484
kaliszyk@43786
   485
lemma DIVMOD_EXIST: "(n::nat) ~= (0::nat) ==> EX (q::nat) r::nat. (m::nat) = q * n + r & r < n"
obua@17644
   486
  by (import hollight DIVMOD_EXIST)
obua@17644
   487
kaliszyk@43786
   488
lemma DIVMOD_EXIST_0: "EX (x::nat) xa::nat.
kaliszyk@43786
   489
   if (n::nat) = (0::nat) then x = (0::nat) & xa = (m::nat)
kaliszyk@43786
   490
   else m = x * n + xa & xa < n"
obua@17644
   491
  by (import hollight DIVMOD_EXIST_0)
obua@17644
   492
kaliszyk@43786
   493
lemma DIVISION: "(n::nat) ~= (0::nat) ==> (m::nat) = m div n * n + m mod n & m mod n < n"
obua@17644
   494
  by (import hollight DIVISION)
obua@17644
   495
kaliszyk@43786
   496
lemma DIVMOD_UNIQ_LEMMA: "((m::nat) = (q1::nat) * (n::nat) + (r1::nat) & r1 < n) &
kaliszyk@43786
   497
m = (q2::nat) * n + (r2::nat) & r2 < n
kaliszyk@43786
   498
==> q1 = q2 & r1 = r2"
obua@17644
   499
  by (import hollight DIVMOD_UNIQ_LEMMA)
obua@17644
   500
kaliszyk@43786
   501
lemma DIVMOD_UNIQ: "(m::nat) = (q::nat) * (n::nat) + (r::nat) & r < n
kaliszyk@43786
   502
==> m div n = q & m mod n = r"
obua@17644
   503
  by (import hollight DIVMOD_UNIQ)
obua@17644
   504
kaliszyk@43786
   505
lemma MOD_UNIQ: "(m::nat) = (q::nat) * (n::nat) + (r::nat) & r < n ==> m mod n = r"
obua@17644
   506
  by (import hollight MOD_UNIQ)
obua@17644
   507
kaliszyk@43786
   508
lemma DIV_UNIQ: "(m::nat) = (q::nat) * (n::nat) + (r::nat) & r < n ==> m div n = q"
obua@17644
   509
  by (import hollight DIV_UNIQ)
obua@17644
   510
kaliszyk@43786
   511
lemma MOD_EQ: "(m::nat) = (n::nat) + (q::nat) * (p::nat) ==> m mod p = n mod p"
obua@17644
   512
  by (import hollight MOD_EQ)
obua@17644
   513
kaliszyk@43786
   514
lemma DIV_LE: "(n::nat) ~= (0::nat) ==> (m::nat) div n <= m"
obua@17644
   515
  by (import hollight DIV_LE)
obua@17644
   516
kaliszyk@43786
   517
lemma DIV_MUL_LE: "(n::nat) * ((m::nat) div n) <= m"
obua@17644
   518
  by (import hollight DIV_MUL_LE)
obua@17644
   519
kaliszyk@43786
   520
lemma MOD_MOD: "(n::nat) * (p::nat) ~= (0::nat) ==> (m::nat) mod (n * p) mod n = m mod n"
obua@17644
   521
  by (import hollight MOD_MOD)
obua@17644
   522
kaliszyk@43786
   523
lemma MOD_MOD_REFL: "(n::nat) ~= (0::nat) ==> (m::nat) mod n mod n = m mod n"
obua@17644
   524
  by (import hollight MOD_MOD_REFL)
obua@17644
   525
kaliszyk@43786
   526
lemma DIV_MULT2: "(x::nat) * (xb::nat) ~= (0::nat) ==> x * (xa::nat) div (x * xb) = xa div xb"
obua@17644
   527
  by (import hollight DIV_MULT2)
obua@17644
   528
kaliszyk@43786
   529
lemma MOD_MULT2: "(x::nat) * (xb::nat) ~= (0::nat)
kaliszyk@43786
   530
==> x * (xa::nat) mod (x * xb) = x * (xa mod xb)"
obua@17644
   531
  by (import hollight MOD_MULT2)
obua@17644
   532
kaliszyk@43786
   533
lemma MOD_EXISTS: "(EX q::nat. (m::nat) = (n::nat) * q) =
kaliszyk@43786
   534
(if n = (0::nat) then m = (0::nat) else m mod n = (0::nat))"
obua@17644
   535
  by (import hollight MOD_EXISTS)
obua@17644
   536
kaliszyk@43786
   537
lemma LE_RDIV_EQ: "(a::nat) ~= (0::nat) ==> ((n::nat) <= (b::nat) div a) = (a * n <= b)"
kaliszyk@43786
   538
  by (import hollight LE_RDIV_EQ)
kaliszyk@43786
   539
kaliszyk@43786
   540
lemma LE_LDIV_EQ: "(a::nat) ~= (0::nat)
kaliszyk@43786
   541
==> ((b::nat) div a <= (n::nat)) = (b < a * (n + (1::nat)))"
kaliszyk@43786
   542
  by (import hollight LE_LDIV_EQ)
kaliszyk@43786
   543
kaliszyk@43786
   544
lemma LE_LDIV: "(x::nat) ~= (0::nat) & (xa::nat) <= x * (xb::nat) ==> xa div x <= xb"
kaliszyk@43786
   545
  by (import hollight LE_LDIV)
kaliszyk@43786
   546
kaliszyk@43786
   547
lemma DIV_MONO: "(p::nat) ~= (0::nat) & (m::nat) <= (n::nat) ==> m div p <= n div p"
obua@17644
   548
  by (import hollight DIV_MONO)
obua@17644
   549
kaliszyk@43786
   550
lemma DIV_MONO_LT: "(p::nat) ~= (0::nat) & (m::nat) + p <= (n::nat) ==> m div p < n div p"
obua@17644
   551
  by (import hollight DIV_MONO_LT)
obua@17644
   552
kaliszyk@43786
   553
lemma DIV_EQ_0: "(n::nat) ~= (0::nat) ==> ((m::nat) div n = (0::nat)) = (m < n)"
obua@17644
   554
  by (import hollight DIV_EQ_0)
obua@17644
   555
kaliszyk@43786
   556
lemma MOD_EQ_0: "(n::nat) ~= (0::nat)
kaliszyk@43786
   557
==> ((m::nat) mod n = (0::nat)) = (EX q::nat. m = q * n)"
obua@17644
   558
  by (import hollight MOD_EQ_0)
obua@17644
   559
kaliszyk@43786
   560
lemma EVEN_MOD: "even (n::nat) = (n mod (2::nat) = (0::nat))"
obua@17644
   561
  by (import hollight EVEN_MOD)
obua@17644
   562
kaliszyk@43786
   563
lemma ODD_MOD: "odd (n::nat) = (n mod (2::nat) = (1::nat))"
obua@17644
   564
  by (import hollight ODD_MOD)
obua@17644
   565
kaliszyk@43786
   566
lemma MOD_MULT_RMOD: "(n::nat) ~= (0::nat) ==> (m::nat) * ((p::nat) mod n) mod n = m * p mod n"
obua@17644
   567
  by (import hollight MOD_MULT_RMOD)
obua@17644
   568
kaliszyk@43786
   569
lemma MOD_MULT_LMOD: "(xa::nat) ~= (0::nat) ==> (x::nat) mod xa * (xb::nat) mod xa = x * xb mod xa"
obua@17644
   570
  by (import hollight MOD_MULT_LMOD)
obua@17644
   571
kaliszyk@43786
   572
lemma MOD_MULT_MOD2: "(xa::nat) ~= (0::nat)
kaliszyk@43786
   573
==> (x::nat) mod xa * ((xb::nat) mod xa) mod xa = x * xb mod xa"
obua@17644
   574
  by (import hollight MOD_MULT_MOD2)
obua@17644
   575
kaliszyk@43786
   576
lemma MOD_EXP_MOD: "(n::nat) ~= (0::nat) ==> ((m::nat) mod n) ^ (p::nat) mod n = m ^ p mod n"
obua@17644
   577
  by (import hollight MOD_EXP_MOD)
obua@17644
   578
kaliszyk@43786
   579
lemma MOD_ADD_MOD: "(n::nat) ~= (0::nat)
kaliszyk@43786
   580
==> ((a::nat) mod n + (b::nat) mod n) mod n = (a + b) mod n"
obua@17644
   581
  by (import hollight MOD_ADD_MOD)
obua@17644
   582
kaliszyk@43786
   583
lemma DIV_ADD_MOD: "(n::nat) ~= (0::nat)
kaliszyk@43786
   584
==> (((a::nat) + (b::nat)) mod n = a mod n + b mod n) =
kaliszyk@43786
   585
    ((a + b) div n = a div n + b div n)"
obua@17644
   586
  by (import hollight DIV_ADD_MOD)
obua@17644
   587
kaliszyk@43786
   588
lemma MOD_LE: "(n::nat) ~= (0::nat) ==> (m::nat) mod n <= m"
obua@17644
   589
  by (import hollight MOD_LE)
obua@17644
   590
kaliszyk@43786
   591
lemma DIV_MONO2: "(p::nat) ~= (0::nat) & p <= (m::nat) ==> (n::nat) div m <= n div p"
obua@17644
   592
  by (import hollight DIV_MONO2)
obua@17644
   593
kaliszyk@43786
   594
lemma DIV_LE_EXCLUSION: "(b::nat) ~= (0::nat) & b * (c::nat) < ((a::nat) + (1::nat)) * (d::nat)
kaliszyk@43786
   595
==> c div d <= a div b"
obua@17644
   596
  by (import hollight DIV_LE_EXCLUSION)
obua@17644
   597
kaliszyk@43786
   598
lemma DIV_EQ_EXCLUSION: "(b::nat) * (c::nat) < ((a::nat) + (1::nat)) * (d::nat) &
kaliszyk@43786
   599
a * d < (c + (1::nat)) * b
kaliszyk@43786
   600
==> a div b = c div d"
obua@17644
   601
  by (import hollight DIV_EQ_EXCLUSION)
obua@17644
   602
kaliszyk@43786
   603
lemma MULT_DIV_LE: "(p::nat) ~= (0::nat) ==> (m::nat) * ((n::nat) div p) <= m * n div p"
kaliszyk@43786
   604
  by (import hollight MULT_DIV_LE)
kaliszyk@43786
   605
kaliszyk@43786
   606
lemma DIV_DIV: "(xa::nat) * (xb::nat) ~= (0::nat)
kaliszyk@43786
   607
==> (x::nat) div xa div xb = x div (xa * xb)"
kaliszyk@43786
   608
  by (import hollight DIV_DIV)
kaliszyk@43786
   609
kaliszyk@43786
   610
lemma DIV_MOD: "(xa::nat) * (xb::nat) ~= (0::nat)
kaliszyk@43786
   611
==> (x::nat) div xa mod xb = x mod (xa * xb) div xa"
kaliszyk@43786
   612
  by (import hollight DIV_MOD)
kaliszyk@43786
   613
kaliszyk@43786
   614
lemma PRE_ELIM_THM: "P (n - Suc 0) = (ALL m. n = Suc m | m = 0 & n = 0 --> P m)"
kaliszyk@43786
   615
  by (import hollight PRE_ELIM_THM)
kaliszyk@43786
   616
obua@17644
   617
lemma SUB_ELIM_THM: "(P::nat => bool) ((a::nat) - (b::nat)) =
kaliszyk@43786
   618
(ALL d::nat. a = b + d | a < b & d = (0::nat) --> P d)"
obua@17644
   619
  by (import hollight SUB_ELIM_THM)
obua@17644
   620
kaliszyk@43786
   621
lemma DIVMOD_ELIM_THM: "(P::nat => nat => bool) ((m::nat) div (n::nat)) (m mod n) =
kaliszyk@43786
   622
(ALL (x::nat) xa::nat.
kaliszyk@43786
   623
    n = (0::nat) & x = (0::nat) & xa = m | m = x * n + xa & xa < n -->
kaliszyk@43786
   624
    P x xa)"
obua@17644
   625
  by (import hollight DIVMOD_ELIM_THM)
obua@17644
   626
kaliszyk@43786
   627
definition
kaliszyk@43786
   628
  minimal :: "(nat => bool) => nat"  where
kaliszyk@43786
   629
  "minimal == %u. SOME n. u n & (ALL m<n. ~ u m)"
kaliszyk@43786
   630
kaliszyk@43786
   631
lemma DEF_minimal: "minimal = (%u. SOME n. u n & (ALL m<n. ~ u m))"
obua@17644
   632
  by (import hollight DEF_minimal)
obua@17644
   633
kaliszyk@43786
   634
lemma MINIMAL: "Ex P = (P (minimal P) & (ALL x<minimal P. ~ P x))"
obua@17644
   635
  by (import hollight MINIMAL)
obua@17644
   636
kaliszyk@43786
   637
lemma TRANSITIVE_STEPWISE_LT_EQ: "(!!x y z. R x y & R y z ==> R x z)
kaliszyk@43786
   638
==> (ALL m n. m < n --> R m n) = (ALL n. R n (Suc n))"
kaliszyk@43786
   639
  by (import hollight TRANSITIVE_STEPWISE_LT_EQ)
kaliszyk@43786
   640
kaliszyk@43786
   641
lemma TRANSITIVE_STEPWISE_LT: "[| (ALL x y z. R x y & R y z --> R x z) & (ALL n. R n (Suc n)); m < n |]
kaliszyk@43786
   642
==> R m n"
kaliszyk@43786
   643
  by (import hollight TRANSITIVE_STEPWISE_LT)
kaliszyk@43786
   644
kaliszyk@43786
   645
lemma TRANSITIVE_STEPWISE_LE_EQ: "(ALL x. R x x) & (ALL x y z. R x y & R y z --> R x z)
kaliszyk@43786
   646
==> (ALL m n. m <= n --> R m n) = (ALL n. R n (Suc n))"
kaliszyk@43786
   647
  by (import hollight TRANSITIVE_STEPWISE_LE_EQ)
kaliszyk@43786
   648
kaliszyk@43786
   649
lemma TRANSITIVE_STEPWISE_LE: "[| (ALL x. R x x) &
kaliszyk@43786
   650
   (ALL x y z. R x y & R y z --> R x z) & (ALL n. R n (Suc n));
kaliszyk@43786
   651
   m <= n |]
kaliszyk@43786
   652
==> R m n"
kaliszyk@43786
   653
  by (import hollight TRANSITIVE_STEPWISE_LE)
kaliszyk@43786
   654
kaliszyk@43786
   655
lemma WF_EQ: "wfP (u_556::'A => 'A => bool) =
kaliszyk@43786
   656
(ALL P::'A => bool.
kaliszyk@43786
   657
    Ex P = (EX x::'A. P x & (ALL y::'A. u_556 y x --> ~ P y)))"
obua@17644
   658
  by (import hollight WF_EQ)
obua@17644
   659
kaliszyk@43786
   660
lemma WF_IND: "wfP (u_556::'A => 'A => bool) =
kaliszyk@43786
   661
(ALL P::'A => bool.
kaliszyk@43786
   662
    (ALL x::'A. (ALL y::'A. u_556 y x --> P y) --> P x) --> All P)"
obua@17644
   663
  by (import hollight WF_IND)
obua@17644
   664
kaliszyk@43786
   665
lemma WF_DCHAIN: "wfP (u_556::'A => 'A => bool) =
kaliszyk@43786
   666
(~ (EX s::nat => 'A. ALL n::nat. u_556 (s (Suc n)) (s n)))"
obua@17644
   667
  by (import hollight WF_DCHAIN)
obua@17644
   668
kaliszyk@43786
   669
lemma WF_UREC: "[| wfP (u_556::'A => 'A => bool);
kaliszyk@43786
   670
   !!(f::'A => 'B) (g::'A => 'B) x::'A.
kaliszyk@43786
   671
      (!!z::'A. u_556 z x ==> f z = g z)
kaliszyk@43786
   672
      ==> (H::('A => 'B) => 'A => 'B) f x = H g x;
kaliszyk@43786
   673
   (ALL x::'A. (f::'A => 'B) x = H f x) &
kaliszyk@43786
   674
   (ALL x::'A. (g::'A => 'B) x = H g x) |]
kaliszyk@43786
   675
==> f = g"
obua@17644
   676
  by (import hollight WF_UREC)
obua@17644
   677
kaliszyk@43786
   678
lemma WF_UREC_WF: "(!!(H::('A => bool) => 'A => bool) (f::'A => bool) g::'A => bool.
kaliszyk@43786
   679
    [| !!(f::'A => bool) (g::'A => bool) x::'A.
kaliszyk@43786
   680
          (!!z::'A. (u_556::'A => 'A => bool) z x ==> f z = g z)
kaliszyk@43786
   681
          ==> H f x = H g x;
kaliszyk@43786
   682
       (ALL x::'A. f x = H f x) & (ALL x::'A. g x = H g x) |]
kaliszyk@43786
   683
    ==> f = g)
kaliszyk@43786
   684
==> wfP u_556"
obua@17644
   685
  by (import hollight WF_UREC_WF)
obua@17644
   686
kaliszyk@43786
   687
lemma WF_REC_INVARIANT: "[| wfP (u_556::'A => 'A => bool);
kaliszyk@43786
   688
   !!(f::'A => 'B) (g::'A => 'B) x::'A.
kaliszyk@43786
   689
      (!!z::'A. u_556 z x ==> f z = g z & (S::'A => 'B => bool) z (f z))
kaliszyk@43786
   690
      ==> (H::('A => 'B) => 'A => 'B) f x = H g x & S x (H f x) |]
kaliszyk@43786
   691
==> EX f::'A => 'B. ALL x::'A. f x = H f x"
obua@17644
   692
  by (import hollight WF_REC_INVARIANT)
obua@17644
   693
kaliszyk@43786
   694
lemma WF_REC: "[| wfP (u_556::'A => 'A => bool);
kaliszyk@43786
   695
   !!(f::'A => 'B) (g::'A => 'B) x::'A.
kaliszyk@43786
   696
      (!!z::'A. u_556 z x ==> f z = g z)
kaliszyk@43786
   697
      ==> (H::('A => 'B) => 'A => 'B) f x = H g x |]
kaliszyk@43786
   698
==> EX f::'A => 'B. ALL x::'A. f x = H f x"
obua@17644
   699
  by (import hollight WF_REC)
obua@17644
   700
kaliszyk@43786
   701
lemma WF_REC_WF: "(!!H::('A => nat) => 'A => nat.
kaliszyk@43786
   702
    (!!(f::'A => nat) (g::'A => nat) x::'A.
kaliszyk@43786
   703
        (!!z::'A. (u_556::'A => 'A => bool) z x ==> f z = g z)
kaliszyk@43786
   704
        ==> H f x = H g x)
kaliszyk@43786
   705
    ==> EX f::'A => nat. ALL x::'A. f x = H f x)
kaliszyk@43786
   706
==> wfP u_556"
obua@17644
   707
  by (import hollight WF_REC_WF)
obua@17644
   708
kaliszyk@43786
   709
lemma WF_EREC: "[| wfP (u_556::'A => 'A => bool);
kaliszyk@43786
   710
   !!(f::'A => 'B) (g::'A => 'B) x::'A.
kaliszyk@43786
   711
      (!!z::'A. u_556 z x ==> f z = g z)
kaliszyk@43786
   712
      ==> (H::('A => 'B) => 'A => 'B) f x = H g x |]
kaliszyk@43786
   713
==> EX! f::'A => 'B. ALL x::'A. f x = H f x"
obua@17644
   714
  by (import hollight WF_EREC)
obua@17644
   715
kaliszyk@43786
   716
lemma WF_SUBSET: "(ALL (x::'A) y::'A.
kaliszyk@43786
   717
    (u_556::'A => 'A => bool) x y --> (u_670::'A => 'A => bool) x y) &
kaliszyk@43786
   718
wfP u_670
kaliszyk@43786
   719
==> wfP u_556"
obua@17644
   720
  by (import hollight WF_SUBSET)
obua@17644
   721
kaliszyk@43786
   722
lemma WF_MEASURE_GEN: "wfP (u_556::'B => 'B => bool)
kaliszyk@43786
   723
==> wfP (%(x::'A) x'::'A. u_556 ((m::'A => 'B) x) (m x'))"
obua@17644
   724
  by (import hollight WF_MEASURE_GEN)
obua@17644
   725
kaliszyk@43786
   726
lemma WF_LEX_DEPENDENT: "wfP (R::'A => 'A => bool) & (ALL x::'A. wfP ((S::'A => 'B => 'B => bool) x))
kaliszyk@43786
   727
==> wfP (SOME f::'A * 'B => 'A * 'B => bool.
kaliszyk@43786
   728
            ALL (r1::'A) s1::'B.
kaliszyk@43786
   729
               f (r1, s1) =
kaliszyk@43786
   730
               (SOME f::'A * 'B => bool.
kaliszyk@43786
   731
                   ALL (r2::'A) s2::'B.
kaliszyk@43786
   732
                      f (r2, s2) = (R r1 r2 | r1 = r2 & S r1 s1 s2)))"
obua@17644
   733
  by (import hollight WF_LEX_DEPENDENT)
obua@17644
   734
kaliszyk@43786
   735
lemma WF_LEX: "wfP (x::'A => 'A => bool) & wfP (xa::'B => 'B => bool)
kaliszyk@43786
   736
==> wfP (SOME f::'A * 'B => 'A * 'B => bool.
kaliszyk@43786
   737
            ALL (r1::'A) s1::'B.
kaliszyk@43786
   738
               f (r1, s1) =
kaliszyk@43786
   739
               (SOME f::'A * 'B => bool.
kaliszyk@43786
   740
                   ALL (r2::'A) s2::'B.
kaliszyk@43786
   741
                      f (r2, s2) = (x r1 r2 | r1 = r2 & xa s1 s2)))"
obua@17644
   742
  by (import hollight WF_LEX)
obua@17644
   743
kaliszyk@43786
   744
lemma WF_POINTWISE: "wfP (u_556::'A => 'A => bool) & wfP (u_670::'B => 'B => bool)
kaliszyk@43786
   745
==> wfP (SOME f::'A * 'B => 'A * 'B => bool.
kaliszyk@43786
   746
            ALL (x1::'A) y1::'B.
kaliszyk@43786
   747
               f (x1, y1) =
kaliszyk@43786
   748
               (SOME f::'A * 'B => bool.
kaliszyk@43786
   749
                   ALL (x2::'A) y2::'B.
kaliszyk@43786
   750
                      f (x2, y2) = (u_556 x1 x2 & u_670 y1 y2)))"
obua@17644
   751
  by (import hollight WF_POINTWISE)
obua@17644
   752
kaliszyk@43786
   753
lemma WF_num: "(wfP::(nat => nat => bool) => bool) (op <::nat => nat => bool)"
obua@17644
   754
  by (import hollight WF_num)
obua@17644
   755
kaliszyk@43786
   756
lemma WF_REC_num: "(!!(f::nat => 'A) (g::nat => 'A) x::nat.
kaliszyk@43786
   757
    (!!z::nat. z < x ==> f z = g z)
kaliszyk@43786
   758
    ==> (H::(nat => 'A) => nat => 'A) f x = H g x)
kaliszyk@43786
   759
==> EX f::nat => 'A. ALL x::nat. f x = H f x"
obua@17644
   760
  by (import hollight WF_REC_num)
obua@17644
   761
kaliszyk@43786
   762
lemma WF_MEASURE: "wfP (%(a::'A) b::'A. measure (m::'A => nat) (a, b))"
obua@17644
   763
  by (import hollight WF_MEASURE)
obua@17644
   764
kaliszyk@43786
   765
lemma MEASURE_LE: "(ALL x::'q_12099.
kaliszyk@43786
   766
    measure (m::'q_12099 => nat) (x, a::'q_12099) -->
kaliszyk@43786
   767
    measure m (x, b::'q_12099)) =
kaliszyk@43786
   768
(m a <= m b)"
obua@17644
   769
  by (import hollight MEASURE_LE)
obua@17644
   770
kaliszyk@43786
   771
lemma WF_REFL: "wfP (u_556::'A => 'A => bool) ==> ~ u_556 (x::'A) x"
obua@17644
   772
  by (import hollight WF_REFL)
obua@17644
   773
kaliszyk@43786
   774
lemma WF_REC_TAIL: "EX f::'A => 'B.
kaliszyk@43786
   775
   ALL x::'A.
kaliszyk@43786
   776
      f x =
kaliszyk@43786
   777
      (if (P::'A => bool) x then f ((g::'A => 'A) x) else (h::'A => 'B) x)"
obua@17644
   778
  by (import hollight WF_REC_TAIL)
obua@17644
   779
kaliszyk@43786
   780
lemma WF_REC_TAIL_GENERAL: "wfP (u_556::'A => 'A => bool) &
kaliszyk@43786
   781
(ALL (f::'A => 'B) (g::'A => 'B) x::'A.
kaliszyk@43786
   782
    (ALL z::'A. u_556 z x --> f z = g z) -->
kaliszyk@43786
   783
    (P::('A => 'B) => 'A => bool) f x = P g x &
kaliszyk@43786
   784
    (G::('A => 'B) => 'A => 'A) f x = G g x &
kaliszyk@43786
   785
    (H::('A => 'B) => 'A => 'B) f x = H g x) &
kaliszyk@43786
   786
(ALL (f::'A => 'B) (g::'A => 'B) x::'A.
kaliszyk@43786
   787
    (ALL z::'A. u_556 z x --> f z = g z) --> H f x = H g x) &
kaliszyk@43786
   788
(ALL (f::'A => 'B) (x::'A) y::'A. P f x & u_556 y (G f x) --> u_556 y x)
kaliszyk@43786
   789
==> EX f::'A => 'B. ALL x::'A. f x = (if P f x then f (G f x) else H f x)"
obua@17644
   790
  by (import hollight WF_REC_TAIL_GENERAL)
obua@17644
   791
kaliszyk@43786
   792
lemma ARITH_ZERO: "(0::nat) = (0::nat) & (0::nat) = (0::nat)"
obua@17644
   793
  by (import hollight ARITH_ZERO)
obua@17644
   794
kaliszyk@43786
   795
lemma ARITH_SUC: "(ALL x. Suc x = Suc x) &
kaliszyk@43786
   796
Suc 0 = 1 &
kaliszyk@43786
   797
(ALL x. Suc (2 * x) = 2 * x + 1) & (ALL x. Suc (2 * x + 1) = 2 * Suc x)"
obua@17644
   798
  by (import hollight ARITH_SUC)
obua@17644
   799
kaliszyk@43786
   800
lemma ARITH_PRE: "(ALL x. x - Suc 0 = x - Suc 0) &
kaliszyk@43786
   801
0 - Suc 0 = 0 &
kaliszyk@43786
   802
(ALL x. 2 * x - Suc 0 = (if x = 0 then 0 else 2 * (x - Suc 0) + 1)) &
kaliszyk@43786
   803
(ALL x. 2 * x + 1 - Suc 0 = 2 * x)"
obua@17644
   804
  by (import hollight ARITH_PRE)
obua@17644
   805
kaliszyk@43786
   806
lemma ARITH_ADD: "(ALL (x::nat) xa::nat. x + xa = x + xa) &
kaliszyk@43786
   807
(0::nat) + (0::nat) = (0::nat) &
kaliszyk@43786
   808
(ALL x::nat. (0::nat) + (2::nat) * x = (2::nat) * x) &
kaliszyk@43786
   809
(ALL x::nat.
kaliszyk@43786
   810
    (0::nat) + ((2::nat) * x + (1::nat)) = (2::nat) * x + (1::nat)) &
kaliszyk@43786
   811
(ALL x::nat. (2::nat) * x + (0::nat) = (2::nat) * x) &
kaliszyk@43786
   812
(ALL x::nat. (2::nat) * x + (1::nat) + (0::nat) = (2::nat) * x + (1::nat)) &
kaliszyk@43786
   813
(ALL (x::nat) xa::nat. (2::nat) * x + (2::nat) * xa = (2::nat) * (x + xa)) &
kaliszyk@43786
   814
(ALL (x::nat) xa::nat.
kaliszyk@43786
   815
    (2::nat) * x + ((2::nat) * xa + (1::nat)) =
kaliszyk@43786
   816
    (2::nat) * (x + xa) + (1::nat)) &
kaliszyk@43786
   817
(ALL (x::nat) xa::nat.
kaliszyk@43786
   818
    (2::nat) * x + (1::nat) + (2::nat) * xa =
kaliszyk@43786
   819
    (2::nat) * (x + xa) + (1::nat)) &
kaliszyk@43786
   820
(ALL (x::nat) xa::nat.
kaliszyk@43786
   821
    (2::nat) * x + (1::nat) + ((2::nat) * xa + (1::nat)) =
kaliszyk@43786
   822
    (2::nat) * Suc (x + xa))"
obua@17644
   823
  by (import hollight ARITH_ADD)
obua@17644
   824
kaliszyk@43786
   825
lemma ARITH_MULT: "(ALL (x::nat) xa::nat. x * xa = x * xa) &
kaliszyk@43786
   826
(0::nat) * (0::nat) = (0::nat) &
kaliszyk@43786
   827
(ALL x::nat. (0::nat) * ((2::nat) * x) = (0::nat)) &
kaliszyk@43786
   828
(ALL x::nat. (0::nat) * ((2::nat) * x + (1::nat)) = (0::nat)) &
kaliszyk@43786
   829
(ALL x::nat. (2::nat) * x * (0::nat) = (0::nat)) &
kaliszyk@43786
   830
(ALL x::nat. ((2::nat) * x + (1::nat)) * (0::nat) = (0::nat)) &
kaliszyk@43786
   831
(ALL (x::nat) xa::nat.
kaliszyk@43786
   832
    (2::nat) * x * ((2::nat) * xa) = (2::nat) * ((2::nat) * (x * xa))) &
kaliszyk@43786
   833
(ALL (x::nat) xa::nat.
kaliszyk@43786
   834
    (2::nat) * x * ((2::nat) * xa + (1::nat)) =
kaliszyk@43786
   835
    (2::nat) * x + (2::nat) * ((2::nat) * (x * xa))) &
kaliszyk@43786
   836
(ALL (x::nat) xa::nat.
kaliszyk@43786
   837
    ((2::nat) * x + (1::nat)) * ((2::nat) * xa) =
kaliszyk@43786
   838
    (2::nat) * xa + (2::nat) * ((2::nat) * (x * xa))) &
kaliszyk@43786
   839
(ALL (x::nat) xa::nat.
kaliszyk@43786
   840
    ((2::nat) * x + (1::nat)) * ((2::nat) * xa + (1::nat)) =
kaliszyk@43786
   841
    (2::nat) * x + (1::nat) +
kaliszyk@43786
   842
    ((2::nat) * xa + (2::nat) * ((2::nat) * (x * xa))))"
obua@17644
   843
  by (import hollight ARITH_MULT)
obua@17644
   844
kaliszyk@43786
   845
lemma ARITH_EXP: "(ALL (x::nat) xa::nat. x ^ xa = x ^ xa) &
kaliszyk@43786
   846
(0::nat) ^ (0::nat) = (1::nat) &
kaliszyk@43786
   847
(ALL m::nat. ((2::nat) * m) ^ (0::nat) = (1::nat)) &
kaliszyk@43786
   848
(ALL m::nat. ((2::nat) * m + (1::nat)) ^ (0::nat) = (1::nat)) &
kaliszyk@43786
   849
(ALL n::nat. (0::nat) ^ ((2::nat) * n) = (0::nat) ^ n * (0::nat) ^ n) &
obua@17644
   850
(ALL (m::nat) n::nat.
kaliszyk@43786
   851
    ((2::nat) * m) ^ ((2::nat) * n) =
kaliszyk@43786
   852
    ((2::nat) * m) ^ n * ((2::nat) * m) ^ n) &
kaliszyk@43786
   853
(ALL (m::nat) n::nat.
kaliszyk@43786
   854
    ((2::nat) * m + (1::nat)) ^ ((2::nat) * n) =
kaliszyk@43786
   855
    ((2::nat) * m + (1::nat)) ^ n * ((2::nat) * m + (1::nat)) ^ n) &
kaliszyk@43786
   856
(ALL n::nat. (0::nat) ^ ((2::nat) * n + (1::nat)) = (0::nat)) &
obua@17644
   857
(ALL (m::nat) n::nat.
kaliszyk@43786
   858
    ((2::nat) * m) ^ ((2::nat) * n + (1::nat)) =
kaliszyk@43786
   859
    (2::nat) * m * (((2::nat) * m) ^ n * ((2::nat) * m) ^ n)) &
obua@17644
   860
(ALL (m::nat) n::nat.
kaliszyk@43786
   861
    ((2::nat) * m + (1::nat)) ^ ((2::nat) * n + (1::nat)) =
kaliszyk@43786
   862
    ((2::nat) * m + (1::nat)) *
kaliszyk@43786
   863
    (((2::nat) * m + (1::nat)) ^ n * ((2::nat) * m + (1::nat)) ^ n))"
obua@17644
   864
  by (import hollight ARITH_EXP)
obua@17644
   865
kaliszyk@43786
   866
lemma ARITH_EVEN: "(ALL x::nat. even x = even x) &
kaliszyk@43786
   867
even (0::nat) = True &
kaliszyk@43786
   868
(ALL x::nat. even ((2::nat) * x) = True) &
kaliszyk@43786
   869
(ALL x::nat. even ((2::nat) * x + (1::nat)) = False)"
obua@17644
   870
  by (import hollight ARITH_EVEN)
obua@17644
   871
kaliszyk@43786
   872
lemma ARITH_ODD: "(ALL x::nat. odd x = odd x) &
kaliszyk@43786
   873
odd (0::nat) = False &
kaliszyk@43786
   874
(ALL x::nat. odd ((2::nat) * x) = False) &
kaliszyk@43786
   875
(ALL x::nat. odd ((2::nat) * x + (1::nat)) = True)"
obua@17644
   876
  by (import hollight ARITH_ODD)
obua@17644
   877
kaliszyk@43786
   878
lemma ARITH_LE: "(ALL (x::nat) xa::nat. (x <= xa) = (x <= xa)) &
kaliszyk@43786
   879
((0::nat) <= (0::nat)) = True &
kaliszyk@43786
   880
(ALL x::nat. ((2::nat) * x <= (0::nat)) = (x <= (0::nat))) &
kaliszyk@43786
   881
(ALL x::nat. ((2::nat) * x + (1::nat) <= (0::nat)) = False) &
kaliszyk@43786
   882
(ALL x::nat. ((0::nat) <= (2::nat) * x) = True) &
kaliszyk@43786
   883
(ALL x::nat. ((0::nat) <= (2::nat) * x + (1::nat)) = True) &
kaliszyk@43786
   884
(ALL (x::nat) xa::nat. ((2::nat) * x <= (2::nat) * xa) = (x <= xa)) &
kaliszyk@43786
   885
(ALL (x::nat) xa::nat.
kaliszyk@43786
   886
    ((2::nat) * x <= (2::nat) * xa + (1::nat)) = (x <= xa)) &
kaliszyk@43786
   887
(ALL (x::nat) xa::nat.
kaliszyk@43786
   888
    ((2::nat) * x + (1::nat) <= (2::nat) * xa) = (x < xa)) &
kaliszyk@43786
   889
(ALL (x::nat) xa::nat.
kaliszyk@43786
   890
    ((2::nat) * x + (1::nat) <= (2::nat) * xa + (1::nat)) = (x <= xa))"
obua@17644
   891
  by (import hollight ARITH_LE)
obua@17644
   892
kaliszyk@43786
   893
lemma ARITH_LT: "(ALL (x::nat) xa::nat. (x < xa) = (x < xa)) &
kaliszyk@43786
   894
((0::nat) < (0::nat)) = False &
kaliszyk@43786
   895
(ALL x::nat. ((2::nat) * x < (0::nat)) = False) &
kaliszyk@43786
   896
(ALL x::nat. ((2::nat) * x + (1::nat) < (0::nat)) = False) &
kaliszyk@43786
   897
(ALL x::nat. ((0::nat) < (2::nat) * x) = ((0::nat) < x)) &
kaliszyk@43786
   898
(ALL x::nat. ((0::nat) < (2::nat) * x + (1::nat)) = True) &
kaliszyk@43786
   899
(ALL (x::nat) xa::nat. ((2::nat) * x < (2::nat) * xa) = (x < xa)) &
kaliszyk@43786
   900
(ALL (x::nat) xa::nat.
kaliszyk@43786
   901
    ((2::nat) * x < (2::nat) * xa + (1::nat)) = (x <= xa)) &
kaliszyk@43786
   902
(ALL (x::nat) xa::nat.
kaliszyk@43786
   903
    ((2::nat) * x + (1::nat) < (2::nat) * xa) = (x < xa)) &
kaliszyk@43786
   904
(ALL (x::nat) xa::nat.
kaliszyk@43786
   905
    ((2::nat) * x + (1::nat) < (2::nat) * xa + (1::nat)) = (x < xa))"
obua@17644
   906
  by (import hollight ARITH_LT)
obua@17644
   907
kaliszyk@43786
   908
lemma ARITH_EQ: "(ALL (x::nat) xa::nat. (x = xa) = (x = xa)) &
kaliszyk@43786
   909
((0::nat) = (0::nat)) = True &
kaliszyk@43786
   910
(ALL x::nat. ((2::nat) * x = (0::nat)) = (x = (0::nat))) &
kaliszyk@43786
   911
(ALL x::nat. ((2::nat) * x + (1::nat) = (0::nat)) = False) &
kaliszyk@43786
   912
(ALL x::nat. ((0::nat) = (2::nat) * x) = ((0::nat) = x)) &
kaliszyk@43786
   913
(ALL x::nat. ((0::nat) = (2::nat) * x + (1::nat)) = False) &
kaliszyk@43786
   914
(ALL (x::nat) xa::nat. ((2::nat) * x = (2::nat) * xa) = (x = xa)) &
kaliszyk@43786
   915
(ALL (x::nat) xa::nat. ((2::nat) * x = (2::nat) * xa + (1::nat)) = False) &
kaliszyk@43786
   916
(ALL (x::nat) xa::nat. ((2::nat) * x + (1::nat) = (2::nat) * xa) = False) &
kaliszyk@43786
   917
(ALL (x::nat) xa::nat.
kaliszyk@43786
   918
    ((2::nat) * x + (1::nat) = (2::nat) * xa + (1::nat)) = (x = xa))"
obua@17644
   919
  by (import hollight ARITH_EQ)
obua@17644
   920
kaliszyk@43786
   921
lemma ARITH_SUB: "(ALL (x::nat) xa::nat. x - xa = x - xa) &
kaliszyk@43786
   922
(0::nat) - (0::nat) = (0::nat) &
kaliszyk@43786
   923
(ALL x::nat. (0::nat) - (2::nat) * x = (0::nat)) &
kaliszyk@43786
   924
(ALL x::nat. (0::nat) - ((2::nat) * x + (1::nat)) = (0::nat)) &
kaliszyk@43786
   925
(ALL x::nat. (2::nat) * x - (0::nat) = (2::nat) * x) &
kaliszyk@43786
   926
(ALL x::nat. (2::nat) * x + (1::nat) - (0::nat) = (2::nat) * x + (1::nat)) &
kaliszyk@43786
   927
(ALL (m::nat) n::nat. (2::nat) * m - (2::nat) * n = (2::nat) * (m - n)) &
kaliszyk@43786
   928
(ALL (m::nat) n::nat.
kaliszyk@43786
   929
    (2::nat) * m - ((2::nat) * n + (1::nat)) =
kaliszyk@43786
   930
    (2::nat) * (m - n) - Suc (0::nat)) &
kaliszyk@43786
   931
(ALL (m::nat) n::nat.
kaliszyk@43786
   932
    (2::nat) * m + (1::nat) - (2::nat) * n =
kaliszyk@43786
   933
    (if n <= m then (2::nat) * (m - n) + (1::nat) else (0::nat))) &
kaliszyk@43786
   934
(ALL (m::nat) n::nat.
kaliszyk@43786
   935
    (2::nat) * m + (1::nat) - ((2::nat) * n + (1::nat)) =
kaliszyk@43786
   936
    (2::nat) * (m - n))"
obua@17644
   937
  by (import hollight ARITH_SUB)
obua@17644
   938
kaliszyk@43786
   939
lemma right_th: "(s::nat) * ((2::nat) * (x::nat) + (1::nat)) = s + (2::nat) * (s * x)"
obua@17644
   940
  by (import hollight right_th)
obua@17644
   941
kaliszyk@43786
   942
lemma SEMIRING_PTHS: "(ALL (x::'A) (y::'A) z::'A.
kaliszyk@43786
   943
    (add::'A => 'A => 'A) x (add y z) = add (add x y) z) &
kaliszyk@43786
   944
(ALL (x::'A) y::'A. add x y = add y x) &
kaliszyk@43786
   945
(ALL x::'A. add (r0::'A) x = x) &
kaliszyk@43786
   946
(ALL (x::'A) (y::'A) z::'A.
kaliszyk@43786
   947
    (mul::'A => 'A => 'A) x (mul y z) = mul (mul x y) z) &
kaliszyk@43786
   948
(ALL (x::'A) y::'A. mul x y = mul y x) &
kaliszyk@43786
   949
(ALL x::'A. mul (r1::'A) x = x) &
kaliszyk@43786
   950
(ALL x::'A. mul r0 x = r0) &
kaliszyk@43786
   951
(ALL (x::'A) (y::'A) z::'A. mul x (add y z) = add (mul x y) (mul x z)) &
kaliszyk@43786
   952
(ALL x::'A. (pwr::'A => nat => 'A) x (0::nat) = r1) &
kaliszyk@43786
   953
(ALL (x::'A) n::nat. pwr x (Suc n) = mul x (pwr x n))
kaliszyk@43786
   954
==> mul r1 (x::'A) = x &
kaliszyk@43786
   955
    add (mul (a::'A) (m::'A)) (mul (b::'A) m) = mul (add a b) m &
kaliszyk@43786
   956
    add (mul a m) m = mul (add a r1) m &
kaliszyk@43786
   957
    add m (mul a m) = mul (add a r1) m &
kaliszyk@43786
   958
    add m m = mul (add r1 r1) m &
kaliszyk@43786
   959
    mul r0 m = r0 &
kaliszyk@43786
   960
    add r0 a = a &
kaliszyk@43786
   961
    add a r0 = a &
kaliszyk@43786
   962
    mul a b = mul b a &
kaliszyk@43786
   963
    mul (add a b) (c::'A) = add (mul a c) (mul b c) &
kaliszyk@43786
   964
    mul r0 a = r0 &
kaliszyk@43786
   965
    mul a r0 = r0 &
kaliszyk@43786
   966
    mul r1 a = a &
kaliszyk@43786
   967
    mul a r1 = a &
kaliszyk@43786
   968
    mul (mul (lx::'A) (ly::'A)) (mul (rx::'A) (ry::'A)) =
kaliszyk@43786
   969
    mul (mul lx rx) (mul ly ry) &
kaliszyk@43786
   970
    mul (mul lx ly) (mul rx ry) = mul lx (mul ly (mul rx ry)) &
kaliszyk@43786
   971
    mul (mul lx ly) (mul rx ry) = mul rx (mul (mul lx ly) ry) &
kaliszyk@43786
   972
    mul (mul lx ly) rx = mul (mul lx rx) ly &
kaliszyk@43786
   973
    mul (mul lx ly) rx = mul lx (mul ly rx) &
kaliszyk@43786
   974
    mul lx rx = mul rx lx &
kaliszyk@43786
   975
    mul lx (mul rx ry) = mul (mul lx rx) ry &
kaliszyk@43786
   976
    mul lx (mul rx ry) = mul rx (mul lx ry) &
kaliszyk@43786
   977
    add (add a b) (add c (d::'A)) = add (add a c) (add b d) &
kaliszyk@43786
   978
    add (add a b) c = add a (add b c) &
kaliszyk@43786
   979
    add a (add c d) = add c (add a d) &
kaliszyk@43786
   980
    add (add a b) c = add (add a c) b &
kaliszyk@43786
   981
    add a c = add c a &
kaliszyk@43786
   982
    add a (add c d) = add (add a c) d &
kaliszyk@43786
   983
    mul (pwr x (p::nat)) (pwr x (q::nat)) = pwr x (p + q) &
kaliszyk@43786
   984
    mul x (pwr x q) = pwr x (Suc q) &
kaliszyk@43786
   985
    mul (pwr x q) x = pwr x (Suc q) &
kaliszyk@43786
   986
    mul x x = pwr x (2::nat) &
kaliszyk@43786
   987
    pwr (mul x (y::'A)) q = mul (pwr x q) (pwr y q) &
kaliszyk@43786
   988
    pwr (pwr x p) q = pwr x (p * q) &
kaliszyk@43786
   989
    pwr x (0::nat) = r1 &
kaliszyk@43786
   990
    pwr x (1::nat) = x &
kaliszyk@43786
   991
    mul x (add y (z::'A)) = add (mul x y) (mul x z) &
kaliszyk@43786
   992
    pwr x (Suc q) = mul x (pwr x q)"
obua@17644
   993
  by (import hollight SEMIRING_PTHS)
obua@17644
   994
kaliszyk@43786
   995
lemma NUM_INTEGRAL_LEMMA: "(w::nat) = (x::nat) + (d::nat) & (y::nat) = (z::nat) + (e::nat)
kaliszyk@43786
   996
==> (w * y + x * z = w * z + x * y) = (w = x | y = z)"
obua@17644
   997
  by (import hollight NUM_INTEGRAL_LEMMA)
obua@17644
   998
kaliszyk@43786
   999
lemma NUM_INTEGRAL: "(ALL x::nat. (0::nat) * x = (0::nat)) &
obua@17644
  1000
(ALL (x::nat) (xa::nat) xb::nat. (x + xa = x + xb) = (xa = xb)) &
obua@17644
  1001
(ALL (w::nat) (x::nat) (y::nat) z::nat.
obua@17644
  1002
    (w * y + x * z = w * z + x * y) = (w = x | y = z))"
obua@17644
  1003
  by (import hollight NUM_INTEGRAL)
obua@17644
  1004
kaliszyk@43786
  1005
lemma INJ_INVERSE2: "(!!(x1::'A) (y1::'B) (x2::'A) y2::'B.
kaliszyk@43786
  1006
    ((P::'A => 'B => 'C) x1 y1 = P x2 y2) = (x1 = x2 & y1 = y2))
kaliszyk@43786
  1007
==> EX (x::'C => 'A) Y::'C => 'B.
kaliszyk@43786
  1008
       ALL (xa::'A) y::'B. x (P xa y) = xa & Y (P xa y) = y"
obua@17644
  1009
  by (import hollight INJ_INVERSE2)
obua@17644
  1010
kaliszyk@43786
  1011
definition
kaliszyk@43786
  1012
  NUMPAIR :: "nat => nat => nat"  where
kaliszyk@43786
  1013
  "NUMPAIR == %u ua. 2 ^ u * (2 * ua + 1)"
kaliszyk@43786
  1014
kaliszyk@43786
  1015
lemma DEF_NUMPAIR: "NUMPAIR = (%u ua. 2 ^ u * (2 * ua + 1))"
obua@17644
  1016
  by (import hollight DEF_NUMPAIR)
obua@17644
  1017
kaliszyk@43786
  1018
lemma NUMPAIR_INJ_LEMMA: "NUMPAIR x xa = NUMPAIR xb xc ==> x = xb"
obua@17644
  1019
  by (import hollight NUMPAIR_INJ_LEMMA)
obua@17644
  1020
kaliszyk@43786
  1021
lemma NUMPAIR_INJ: "(NUMPAIR x1 y1 = NUMPAIR x2 y2) = (x1 = x2 & y1 = y2)"
obua@17644
  1022
  by (import hollight NUMPAIR_INJ)
obua@17644
  1023
kaliszyk@43786
  1024
definition
kaliszyk@43786
  1025
  NUMFST :: "nat => nat"  where
kaliszyk@43786
  1026
  "NUMFST == SOME X. EX Y. ALL x y. X (NUMPAIR x y) = x & Y (NUMPAIR x y) = y"
kaliszyk@43786
  1027
kaliszyk@43786
  1028
lemma DEF_NUMFST: "NUMFST = (SOME X. EX Y. ALL x y. X (NUMPAIR x y) = x & Y (NUMPAIR x y) = y)"
obua@17644
  1029
  by (import hollight DEF_NUMFST)
obua@17644
  1030
kaliszyk@43786
  1031
definition
kaliszyk@43786
  1032
  NUMSND :: "nat => nat"  where
kaliszyk@43786
  1033
  "NUMSND == SOME Y. ALL x y. NUMFST (NUMPAIR x y) = x & Y (NUMPAIR x y) = y"
kaliszyk@43786
  1034
kaliszyk@43786
  1035
lemma DEF_NUMSND: "NUMSND = (SOME Y. ALL x y. NUMFST (NUMPAIR x y) = x & Y (NUMPAIR x y) = y)"
obua@17644
  1036
  by (import hollight DEF_NUMSND)
obua@17644
  1037
kaliszyk@43786
  1038
definition
kaliszyk@43786
  1039
  NUMSUM :: "bool => nat => nat"  where
kaliszyk@43786
  1040
  "NUMSUM == %u ua. if u then Suc (2 * ua) else 2 * ua"
kaliszyk@43786
  1041
kaliszyk@43786
  1042
lemma DEF_NUMSUM: "NUMSUM = (%u ua. if u then Suc (2 * ua) else 2 * ua)"
obua@17644
  1043
  by (import hollight DEF_NUMSUM)
obua@17644
  1044
kaliszyk@43786
  1045
lemma NUMSUM_INJ: "(NUMSUM b1 x1 = NUMSUM b2 x2) = (b1 = b2 & x1 = x2)"
obua@17644
  1046
  by (import hollight NUMSUM_INJ)
obua@17644
  1047
kaliszyk@43786
  1048
definition
kaliszyk@43786
  1049
  NUMLEFT :: "nat => bool"  where
kaliszyk@43786
  1050
  "NUMLEFT == SOME X. EX Y. ALL x y. X (NUMSUM x y) = x & Y (NUMSUM x y) = y"
kaliszyk@43786
  1051
kaliszyk@43786
  1052
lemma DEF_NUMLEFT: "NUMLEFT = (SOME X. EX Y. ALL x y. X (NUMSUM x y) = x & Y (NUMSUM x y) = y)"
obua@17644
  1053
  by (import hollight DEF_NUMLEFT)
obua@17644
  1054
kaliszyk@43786
  1055
definition
kaliszyk@43786
  1056
  NUMRIGHT :: "nat => nat"  where
kaliszyk@43786
  1057
  "NUMRIGHT == SOME Y. ALL x y. NUMLEFT (NUMSUM x y) = x & Y (NUMSUM x y) = y"
kaliszyk@43786
  1058
kaliszyk@43786
  1059
lemma DEF_NUMRIGHT: "NUMRIGHT = (SOME Y. ALL x y. NUMLEFT (NUMSUM x y) = x & Y (NUMSUM x y) = y)"
obua@17644
  1060
  by (import hollight DEF_NUMRIGHT)
obua@17644
  1061
kaliszyk@43786
  1062
definition
kaliszyk@43786
  1063
  INJN :: "nat => nat => 'A => bool"  where
kaliszyk@43786
  1064
  "INJN == %(u::nat) (n::nat) a::'A. n = u"
kaliszyk@43786
  1065
kaliszyk@43786
  1066
lemma DEF_INJN: "INJN = (%(u::nat) (n::nat) a::'A. n = u)"
obua@17644
  1067
  by (import hollight DEF_INJN)
obua@17644
  1068
kaliszyk@43786
  1069
lemma INJN_INJ: "(op =::bool => bool => bool)
kaliszyk@43786
  1070
 ((op =::(nat => 'A::type => bool) => (nat => 'A::type => bool) => bool)
kaliszyk@43786
  1071
   ((INJN::nat => nat => 'A::type => bool) (n1::nat))
kaliszyk@43786
  1072
   ((INJN::nat => nat => 'A::type => bool) (n2::nat)))
kaliszyk@43786
  1073
 ((op =::nat => nat => bool) n1 n2)"
obua@17644
  1074
  by (import hollight INJN_INJ)
obua@17644
  1075
kaliszyk@43786
  1076
definition
kaliszyk@43786
  1077
  INJA :: "'A => nat => 'A => bool"  where
kaliszyk@43786
  1078
  "INJA == %(u::'A) (n::nat) b::'A. b = u"
kaliszyk@43786
  1079
kaliszyk@43786
  1080
lemma DEF_INJA: "INJA = (%(u::'A) (n::nat) b::'A. b = u)"
obua@17644
  1081
  by (import hollight DEF_INJA)
obua@17644
  1082
kaliszyk@43786
  1083
lemma INJA_INJ: "(INJA (a1::'A) = INJA (a2::'A)) = (a1 = a2)"
obua@17644
  1084
  by (import hollight INJA_INJ)
obua@17644
  1085
kaliszyk@43786
  1086
definition
kaliszyk@43786
  1087
  INJF :: "(nat => nat => 'A => bool) => nat => 'A => bool"  where
kaliszyk@43786
  1088
  "INJF == %(u::nat => nat => 'A => bool) n::nat. u (NUMFST n) (NUMSND n)"
kaliszyk@43786
  1089
kaliszyk@43786
  1090
lemma DEF_INJF: "INJF = (%(u::nat => nat => 'A => bool) n::nat. u (NUMFST n) (NUMSND n))"
obua@17644
  1091
  by (import hollight DEF_INJF)
obua@17644
  1092
kaliszyk@43786
  1093
lemma INJF_INJ: "(INJF (f1::nat => nat => 'A => bool) =
kaliszyk@43786
  1094
 INJF (f2::nat => nat => 'A => bool)) =
kaliszyk@43786
  1095
(f1 = f2)"
obua@17644
  1096
  by (import hollight INJF_INJ)
obua@17644
  1097
kaliszyk@43786
  1098
definition
kaliszyk@43786
  1099
  INJP :: "(nat => 'A => bool) => (nat => 'A => bool) => nat => 'A => bool"  where
obua@17644
  1100
  "INJP ==
kaliszyk@43786
  1101
%(u::nat => 'A => bool) (ua::nat => 'A => bool) (n::nat) a::'A.
kaliszyk@43786
  1102
   if NUMLEFT n then u (NUMRIGHT n) a else ua (NUMRIGHT n) a"
obua@17644
  1103
obua@17644
  1104
lemma DEF_INJP: "INJP =
kaliszyk@43786
  1105
(%(u::nat => 'A => bool) (ua::nat => 'A => bool) (n::nat) a::'A.
kaliszyk@43786
  1106
    if NUMLEFT n then u (NUMRIGHT n) a else ua (NUMRIGHT n) a)"
obua@17644
  1107
  by (import hollight DEF_INJP)
obua@17644
  1108
kaliszyk@43786
  1109
lemma INJP_INJ: "(INJP (f1::nat => 'A => bool) (f2::nat => 'A => bool) =
kaliszyk@43786
  1110
 INJP (f1'::nat => 'A => bool) (f2'::nat => 'A => bool)) =
kaliszyk@43786
  1111
(f1 = f1' & f2 = f2')"
obua@17644
  1112
  by (import hollight INJP_INJ)
obua@17644
  1113
kaliszyk@43786
  1114
definition
kaliszyk@43786
  1115
  ZCONSTR :: "nat => 'A => (nat => nat => 'A => bool) => nat => 'A => bool"  where
obua@17644
  1116
  "ZCONSTR ==
kaliszyk@43786
  1117
%(u::nat) (ua::'A) ub::nat => nat => 'A => bool.
obua@17644
  1118
   INJP (INJN (Suc u)) (INJP (INJA ua) (INJF ub))"
obua@17644
  1119
obua@17644
  1120
lemma DEF_ZCONSTR: "ZCONSTR =
kaliszyk@43786
  1121
(%(u::nat) (ua::'A) ub::nat => nat => 'A => bool.
obua@17644
  1122
    INJP (INJN (Suc u)) (INJP (INJA ua) (INJF ub)))"
obua@17644
  1123
  by (import hollight DEF_ZCONSTR)
obua@17644
  1124
kaliszyk@43786
  1125
definition
kaliszyk@43786
  1126
  ZBOT :: "nat => 'A => bool"  where
kaliszyk@43786
  1127
  "ZBOT == INJP (INJN (0::nat)) (SOME z::nat => 'A => bool. True)"
kaliszyk@43786
  1128
kaliszyk@43786
  1129
lemma DEF_ZBOT: "ZBOT = INJP (INJN (0::nat)) (SOME z::nat => 'A => bool. True)"
obua@17644
  1130
  by (import hollight DEF_ZBOT)
obua@17644
  1131
kaliszyk@43786
  1132
lemma ZCONSTR_ZBOT: "ZCONSTR (x::nat) (xa::'A) (xb::nat => nat => 'A => bool) ~= ZBOT"
obua@17644
  1133
  by (import hollight ZCONSTR_ZBOT)
obua@17644
  1134
kaliszyk@43786
  1135
definition
kaliszyk@43786
  1136
  ZRECSPACE :: "(nat => 'A => bool) => bool"  where
obua@17644
  1137
  "ZRECSPACE ==
kaliszyk@43786
  1138
%a::nat => 'A => bool.
kaliszyk@43786
  1139
   ALL ZRECSPACE'::(nat => 'A => bool) => bool.
kaliszyk@43786
  1140
      (ALL a::nat => 'A => bool.
obua@17644
  1141
          a = ZBOT |
kaliszyk@43786
  1142
          (EX (c::nat) (i::'A) r::nat => nat => 'A => bool.
obua@17644
  1143
              a = ZCONSTR c i r & (ALL n::nat. ZRECSPACE' (r n))) -->
obua@17644
  1144
          ZRECSPACE' a) -->
obua@17644
  1145
      ZRECSPACE' a"
obua@17644
  1146
obua@17644
  1147
lemma DEF_ZRECSPACE: "ZRECSPACE =
kaliszyk@43786
  1148
(%a::nat => 'A => bool.
kaliszyk@43786
  1149
    ALL ZRECSPACE'::(nat => 'A => bool) => bool.
kaliszyk@43786
  1150
       (ALL a::nat => 'A => bool.
obua@17644
  1151
           a = ZBOT |
kaliszyk@43786
  1152
           (EX (c::nat) (i::'A) r::nat => nat => 'A => bool.
obua@17644
  1153
               a = ZCONSTR c i r & (ALL n::nat. ZRECSPACE' (r n))) -->
obua@17644
  1154
           ZRECSPACE' a) -->
obua@17644
  1155
       ZRECSPACE' a)"
obua@17644
  1156
  by (import hollight DEF_ZRECSPACE)
obua@17644
  1157
kaliszyk@43786
  1158
typedef (open) ('A) recspace = "Collect ZRECSPACE"  morphisms "_dest_rec" "_mk_rec"
kaliszyk@43786
  1159
  apply (rule light_ex_imp_nonempty[where t="ZBOT"])
obua@17644
  1160
  by (import hollight TYDEF_recspace)
obua@17644
  1161
obua@17644
  1162
syntax
obua@17644
  1163
  "_dest_rec" :: _ ("'_dest'_rec")
obua@17644
  1164
obua@17644
  1165
syntax
obua@17644
  1166
  "_mk_rec" :: _ ("'_mk'_rec")
obua@17644
  1167
obua@17644
  1168
lemmas "TYDEF_recspace_@intern" = typedef_hol2hollight 
obua@17652
  1169
  [where a="a :: 'A recspace" and r=r ,
obua@17644
  1170
   OF type_definition_recspace]
obua@17644
  1171
kaliszyk@43786
  1172
definition
kaliszyk@43786
  1173
  BOTTOM :: "'A recspace"  where
kaliszyk@43786
  1174
  "BOTTOM == _mk_rec ZBOT"
kaliszyk@43786
  1175
kaliszyk@43786
  1176
lemma DEF_BOTTOM: "BOTTOM = _mk_rec ZBOT"
obua@17644
  1177
  by (import hollight DEF_BOTTOM)
obua@17644
  1178
kaliszyk@43786
  1179
definition
kaliszyk@43786
  1180
  CONSTR :: "nat => 'A => (nat => 'A recspace) => 'A recspace"  where
kaliszyk@43786
  1181
  "CONSTR ==
kaliszyk@43786
  1182
%(u::nat) (ua::'A::type) ub::nat => 'A::type recspace.
kaliszyk@43786
  1183
   _mk_rec (ZCONSTR u ua (%n::nat. _dest_rec (ub n)))"
kaliszyk@43786
  1184
kaliszyk@43786
  1185
lemma DEF_CONSTR: "CONSTR =
kaliszyk@43786
  1186
(%(u::nat) (ua::'A::type) ub::nat => 'A::type recspace.
kaliszyk@43786
  1187
    _mk_rec (ZCONSTR u ua (%n::nat. _dest_rec (ub n))))"
obua@17644
  1188
  by (import hollight DEF_CONSTR)
obua@17644
  1189
kaliszyk@43786
  1190
lemma MK_REC_INJ: "[| _mk_rec (x::nat => 'A::type => bool) =
kaliszyk@43786
  1191
   _mk_rec (y::nat => 'A::type => bool);
kaliszyk@43786
  1192
   ZRECSPACE x & ZRECSPACE y |]
kaliszyk@43786
  1193
==> x = y"
obua@17644
  1194
  by (import hollight MK_REC_INJ)
obua@17644
  1195
kaliszyk@43786
  1196
lemma CONSTR_BOT: "CONSTR (c::nat) (i::'A) (r::nat => 'A recspace) ~= BOTTOM"
obua@17644
  1197
  by (import hollight CONSTR_BOT)
obua@17644
  1198
kaliszyk@43786
  1199
lemma CONSTR_INJ: "(CONSTR (c1::nat) (i1::'A) (r1::nat => 'A recspace) =
kaliszyk@43786
  1200
 CONSTR (c2::nat) (i2::'A) (r2::nat => 'A recspace)) =
kaliszyk@43786
  1201
(c1 = c2 & i1 = i2 & r1 = r2)"
obua@17644
  1202
  by (import hollight CONSTR_INJ)
obua@17644
  1203
kaliszyk@43786
  1204
lemma CONSTR_IND: "(P::'A recspace => bool) BOTTOM &
kaliszyk@43786
  1205
(ALL (c::nat) (i::'A) r::nat => 'A recspace.
kaliszyk@43786
  1206
    (ALL n::nat. P (r n)) --> P (CONSTR c i r))
kaliszyk@43786
  1207
==> P (x::'A recspace)"
obua@17644
  1208
  by (import hollight CONSTR_IND)
obua@17644
  1209
kaliszyk@43786
  1210
lemma CONSTR_REC: "EX f::'A recspace => 'B.
kaliszyk@43786
  1211
   ALL (c::nat) (i::'A) r::nat => 'A recspace.
kaliszyk@43786
  1212
      f (CONSTR c i r) =
kaliszyk@43786
  1213
      (Fn::nat => 'A => (nat => 'A recspace) => (nat => 'B) => 'B) c i r
kaliszyk@43786
  1214
       (%n::nat. f (r n))"
obua@17644
  1215
  by (import hollight CONSTR_REC)
obua@17644
  1216
kaliszyk@43786
  1217
definition
kaliszyk@43786
  1218
  FCONS :: "'A => (nat => 'A) => nat => 'A"  where
obua@17644
  1219
  "FCONS ==
kaliszyk@43786
  1220
SOME FCONS::'A => (nat => 'A) => nat => 'A.
kaliszyk@43786
  1221
   (ALL (a::'A) f::nat => 'A. FCONS a f (0::nat) = a) &
kaliszyk@43786
  1222
   (ALL (a::'A) (f::nat => 'A) n::nat. FCONS a f (Suc n) = f n)"
obua@17644
  1223
obua@17644
  1224
lemma DEF_FCONS: "FCONS =
kaliszyk@43786
  1225
(SOME FCONS::'A => (nat => 'A) => nat => 'A.
kaliszyk@43786
  1226
    (ALL (a::'A) f::nat => 'A. FCONS a f (0::nat) = a) &
kaliszyk@43786
  1227
    (ALL (a::'A) (f::nat => 'A) n::nat. FCONS a f (Suc n) = f n))"
obua@17644
  1228
  by (import hollight DEF_FCONS)
obua@17644
  1229
kaliszyk@43786
  1230
lemma FCONS_UNDO: "(f::nat => 'A) = FCONS (f (0::nat)) (f o Suc)"
obua@17644
  1231
  by (import hollight FCONS_UNDO)
obua@17644
  1232
kaliszyk@43786
  1233
definition
kaliszyk@43786
  1234
  FNIL :: "nat => 'A"  where
kaliszyk@43786
  1235
  "FNIL == %u::nat. SOME x::'A. True"
kaliszyk@43786
  1236
kaliszyk@43786
  1237
lemma DEF_FNIL: "FNIL = (%u::nat. SOME x::'A. True)"
obua@17644
  1238
  by (import hollight DEF_FNIL)
obua@17644
  1239
kaliszyk@43786
  1240
definition
kaliszyk@43786
  1241
  ISO :: "('A => 'B) => ('B => 'A) => bool"  where
kaliszyk@43786
  1242
  "ISO ==
kaliszyk@43786
  1243
%(u::'A => 'B) ua::'B => 'A.
kaliszyk@43786
  1244
   (ALL x::'B. u (ua x) = x) & (ALL y::'A. ua (u y) = y)"
kaliszyk@43786
  1245
kaliszyk@43786
  1246
lemma DEF_ISO: "ISO =
kaliszyk@43786
  1247
(%(u::'A => 'B) ua::'B => 'A.
kaliszyk@43786
  1248
    (ALL x::'B. u (ua x) = x) & (ALL y::'A. ua (u y) = y))"
kaliszyk@43786
  1249
  by (import hollight DEF_ISO)
kaliszyk@43786
  1250
kaliszyk@43786
  1251
lemma ISO_REFL: "ISO (%x::'A. x) (%x::'A. x)"
kaliszyk@43786
  1252
  by (import hollight ISO_REFL)
kaliszyk@43786
  1253
kaliszyk@43786
  1254
lemma ISO_FUN: "ISO (f::'A => 'A') (f'::'A' => 'A) & ISO (g::'B => 'B') (g'::'B' => 'B)
kaliszyk@43786
  1255
==> ISO (%(h::'A => 'B) a'::'A'. g (h (f' a')))
kaliszyk@43786
  1256
     (%(h::'A' => 'B') a::'A. g' (h (f a)))"
kaliszyk@43786
  1257
  by (import hollight ISO_FUN)
kaliszyk@43786
  1258
kaliszyk@43786
  1259
lemma ISO_USAGE: "ISO (f::'q_17485 => 'q_17482) (g::'q_17482 => 'q_17485)
kaliszyk@43786
  1260
==> (ALL P::'q_17485 => bool. All P = (ALL x::'q_17482. P (g x))) &
kaliszyk@43786
  1261
    (ALL P::'q_17485 => bool. Ex P = (EX x::'q_17482. P (g x))) &
kaliszyk@43786
  1262
    (ALL (a::'q_17485) b::'q_17482. (a = g b) = (f a = b))"
kaliszyk@43786
  1263
  by (import hollight ISO_USAGE)
kaliszyk@43786
  1264
kaliszyk@43786
  1265
typedef (open) char = "{a. ALL char'.
kaliszyk@43786
  1266
       (ALL a.
kaliszyk@43786
  1267
           (EX a0 a1 a2 a3 a4 a5 a6 a7.
kaliszyk@43786
  1268
               a =
kaliszyk@43786
  1269
               CONSTR (NUMERAL 0) (a0, a1, a2, a3, a4, a5, a6, a7)
kaliszyk@43786
  1270
                (%n. BOTTOM)) -->
kaliszyk@43786
  1271
           char' a) -->
kaliszyk@43786
  1272
       char' a}"  morphisms "_dest_char" "_mk_char"
kaliszyk@43786
  1273
  apply (rule light_ex_imp_nonempty[where t="CONSTR (NUMERAL 0) (a0, a1, a2, a3, a4, a5, a6, a7) (%n. BOTTOM)"])
kaliszyk@43786
  1274
  by (import hollight TYDEF_char)
obua@17644
  1275
obua@17644
  1276
syntax
kaliszyk@43786
  1277
  "_dest_char" :: _ ("'_dest'_char")
obua@17644
  1278
obua@17644
  1279
syntax
kaliszyk@43786
  1280
  "_mk_char" :: _ ("'_mk'_char")
kaliszyk@43786
  1281
kaliszyk@43786
  1282
lemmas "TYDEF_char_@intern" = typedef_hol2hollight 
kaliszyk@43786
  1283
  [where a="a :: hollight.char" and r=r ,
kaliszyk@43786
  1284
   OF type_definition_char]
obua@17644
  1285
obua@17644
  1286
consts
kaliszyk@43786
  1287
  "_11937" :: "bool
kaliszyk@43786
  1288
=> bool => bool => bool => bool => bool => bool => bool => hollight.char" ("'_11937")
obua@17644
  1289
obua@17644
  1290
defs
kaliszyk@43786
  1291
  "_11937_def": "_11937 ==
kaliszyk@43786
  1292
%(a0::bool) (a1::bool) (a2::bool) (a3::bool) (a4::bool) (a5::bool)
kaliszyk@43786
  1293
   (a6::bool) a7::bool.
kaliszyk@43786
  1294
   _mk_char
kaliszyk@43786
  1295
    (CONSTR (0::nat) (a0, a1, a2, a3, a4, a5, a6, a7) (%n::nat. BOTTOM))"
kaliszyk@43786
  1296
kaliszyk@43786
  1297
lemma DEF__11937: "_11937 =
kaliszyk@43786
  1298
(%(a0::bool) (a1::bool) (a2::bool) (a3::bool) (a4::bool) (a5::bool)
kaliszyk@43786
  1299
    (a6::bool) a7::bool.
kaliszyk@43786
  1300
    _mk_char
kaliszyk@43786
  1301
     (CONSTR (0::nat) (a0, a1, a2, a3, a4, a5, a6, a7) (%n::nat. BOTTOM)))"
kaliszyk@43786
  1302
  by (import hollight DEF__11937)
kaliszyk@43786
  1303
kaliszyk@43786
  1304
definition
kaliszyk@43786
  1305
  ASCII :: "bool
kaliszyk@43786
  1306
=> bool => bool => bool => bool => bool => bool => bool => hollight.char"  where
kaliszyk@43786
  1307
  "ASCII == _11937"
kaliszyk@43786
  1308
kaliszyk@43786
  1309
lemma DEF_ASCII: "ASCII = _11937"
kaliszyk@43786
  1310
  by (import hollight DEF_ASCII)
obua@17644
  1311
obua@17644
  1312
consts
kaliszyk@43786
  1313
  dist :: "nat * nat => nat" 
obua@17644
  1314
obua@17644
  1315
defs
kaliszyk@43786
  1316
  dist_def: "hollight.dist == %u. fst u - snd u + (snd u - fst u)"
kaliszyk@43786
  1317
kaliszyk@43786
  1318
lemma DEF_dist: "hollight.dist = (%u. fst u - snd u + (snd u - fst u))"
obua@17644
  1319
  by (import hollight DEF_dist)
obua@17644
  1320
kaliszyk@43786
  1321
lemma DIST_REFL: "hollight.dist (x, x) = 0"
obua@17644
  1322
  by (import hollight DIST_REFL)
obua@17644
  1323
kaliszyk@43786
  1324
lemma DIST_LZERO: "hollight.dist (0, x) = x"
obua@17644
  1325
  by (import hollight DIST_LZERO)
obua@17644
  1326
kaliszyk@43786
  1327
lemma DIST_RZERO: "hollight.dist (x, 0) = x"
obua@17644
  1328
  by (import hollight DIST_RZERO)
obua@17644
  1329
kaliszyk@43786
  1330
lemma DIST_SYM: "hollight.dist (x, xa) = hollight.dist (xa, x)"
obua@17644
  1331
  by (import hollight DIST_SYM)
obua@17644
  1332
kaliszyk@43786
  1333
lemma DIST_LADD: "hollight.dist (x + xb, x + xa) = hollight.dist (xb, xa)"
obua@17644
  1334
  by (import hollight DIST_LADD)
obua@17644
  1335
kaliszyk@43786
  1336
lemma DIST_RADD: "hollight.dist (x + xa, xb + xa) = hollight.dist (x, xb)"
obua@17644
  1337
  by (import hollight DIST_RADD)
obua@17644
  1338
kaliszyk@43786
  1339
lemma DIST_LADD_0: "hollight.dist (x + xa, x) = xa"
obua@17644
  1340
  by (import hollight DIST_LADD_0)
obua@17644
  1341
kaliszyk@43786
  1342
lemma DIST_RADD_0: "hollight.dist (x, x + xa) = xa"
obua@17644
  1343
  by (import hollight DIST_RADD_0)
obua@17644
  1344
kaliszyk@43786
  1345
lemma DIST_LMUL: "x * hollight.dist (xa, xb) = hollight.dist (x * xa, x * xb)"
obua@17644
  1346
  by (import hollight DIST_LMUL)
obua@17644
  1347
kaliszyk@43786
  1348
lemma DIST_RMUL: "hollight.dist (x, xa) * xb = hollight.dist (x * xb, xa * xb)"
obua@17644
  1349
  by (import hollight DIST_RMUL)
obua@17644
  1350
kaliszyk@43786
  1351
lemma DIST_EQ_0: "(hollight.dist (x, xa) = 0) = (x = xa)"
obua@17644
  1352
  by (import hollight DIST_EQ_0)
obua@17644
  1353
kaliszyk@43786
  1354
lemma DIST_ELIM_THM: "P (hollight.dist (x, y)) =
kaliszyk@43786
  1355
(ALL d. (x = y + d --> P d) & (y = x + d --> P d))"
obua@17644
  1356
  by (import hollight DIST_ELIM_THM)
obua@17644
  1357
kaliszyk@43786
  1358
lemma DIST_LE_CASES: "(hollight.dist (m, n) <= p) = (m <= n + p & n <= m + p)"
obua@17644
  1359
  by (import hollight DIST_LE_CASES)
obua@17644
  1360
kaliszyk@43786
  1361
lemma DIST_TRIANGLE_LE: "hollight.dist (m, n) + hollight.dist (n, p) <= q
kaliszyk@43786
  1362
==> hollight.dist (m, p) <= q"
obua@17644
  1363
  by (import hollight DIST_TRIANGLE_LE)
obua@17644
  1364
kaliszyk@43786
  1365
lemma DIST_TRIANGLES_LE: "hollight.dist (m, n) <= r & hollight.dist (p, q) <= s
kaliszyk@43786
  1366
==> hollight.dist (m, p) <= hollight.dist (n, q) + (r + s)"
obua@17644
  1367
  by (import hollight DIST_TRIANGLES_LE)
obua@17644
  1368
kaliszyk@43786
  1369
lemma BOUNDS_LINEAR: "(ALL n::nat. (A::nat) * n <= (B::nat) * n + (C::nat)) = (A <= B)"
obua@17644
  1370
  by (import hollight BOUNDS_LINEAR)
obua@17644
  1371
kaliszyk@43786
  1372
lemma BOUNDS_LINEAR_0: "(ALL n::nat. (A::nat) * n <= (B::nat)) = (A = (0::nat))"
obua@17644
  1373
  by (import hollight BOUNDS_LINEAR_0)
obua@17644
  1374
kaliszyk@43786
  1375
lemma BOUNDS_DIVIDED: "(EX B::nat. ALL n::nat. (P::nat => nat) n <= B) =
kaliszyk@43786
  1376
(EX (x::nat) B::nat. ALL n::nat. n * P n <= x * n + B)"
obua@17644
  1377
  by (import hollight BOUNDS_DIVIDED)
obua@17644
  1378
kaliszyk@43786
  1379
lemma BOUNDS_NOTZERO: "(P::nat => nat => nat) (0::nat) (0::nat) = (0::nat) &
kaliszyk@43786
  1380
(ALL (m::nat) n::nat. P m n <= (A::nat) * (m + n) + (B::nat))
kaliszyk@43786
  1381
==> EX x::nat. ALL (m::nat) n::nat. P m n <= x * (m + n)"
obua@17644
  1382
  by (import hollight BOUNDS_NOTZERO)
obua@17644
  1383
kaliszyk@43786
  1384
lemma BOUNDS_IGNORE: "(EX B::nat. ALL i::nat. (P::nat => nat) i <= (Q::nat => nat) i + B) =
kaliszyk@43786
  1385
(EX (x::nat) N::nat. ALL i>=N. P i <= Q i + x)"
obua@17644
  1386
  by (import hollight BOUNDS_IGNORE)
obua@17644
  1387
kaliszyk@43786
  1388
definition
kaliszyk@43786
  1389
  is_nadd :: "(nat => nat) => bool"  where
obua@17644
  1390
  "is_nadd ==
kaliszyk@43786
  1391
%u. EX B. ALL m n. hollight.dist (m * u n, n * u m) <= B * (m + n)"
obua@17644
  1392
obua@17644
  1393
lemma DEF_is_nadd: "is_nadd =
kaliszyk@43786
  1394
(%u. EX B. ALL m n. hollight.dist (m * u n, n * u m) <= B * (m + n))"
obua@17644
  1395
  by (import hollight DEF_is_nadd)
obua@17644
  1396
kaliszyk@43786
  1397
lemma is_nadd_0: "is_nadd (%n. 0)"
obua@17644
  1398
  by (import hollight is_nadd_0)
obua@17644
  1399
obua@17644
  1400
typedef (open) nadd = "Collect is_nadd"  morphisms "dest_nadd" "mk_nadd"
kaliszyk@43786
  1401
  apply (rule light_ex_imp_nonempty[where t="%n. NUMERAL 0"])
obua@17644
  1402
  by (import hollight TYDEF_nadd)
obua@17644
  1403
obua@17644
  1404
syntax
obua@17644
  1405
  dest_nadd :: _ 
obua@17644
  1406
obua@17644
  1407
syntax
obua@17644
  1408
  mk_nadd :: _ 
obua@17644
  1409
obua@17644
  1410
lemmas "TYDEF_nadd_@intern" = typedef_hol2hollight 
obua@17644
  1411
  [where a="a :: nadd" and r=r ,
obua@17644
  1412
   OF type_definition_nadd]
obua@17644
  1413
kaliszyk@43786
  1414
lemma NADD_CAUCHY: "EX xa.
kaliszyk@43786
  1415
   ALL xb xc.
kaliszyk@43786
  1416
      hollight.dist (xb * dest_nadd x xc, xc * dest_nadd x xb)
kaliszyk@43786
  1417
      <= xa * (xb + xc)"
obua@17644
  1418
  by (import hollight NADD_CAUCHY)
obua@17644
  1419
kaliszyk@43786
  1420
lemma NADD_BOUND: "EX xa B. ALL n. dest_nadd x n <= xa * n + B"
obua@17644
  1421
  by (import hollight NADD_BOUND)
obua@17644
  1422
kaliszyk@43786
  1423
lemma NADD_MULTIPLICATIVE: "EX xa.
kaliszyk@43786
  1424
   ALL m n.
kaliszyk@43786
  1425
      hollight.dist (dest_nadd x (m * n), m * dest_nadd x n) <= xa * m + xa"
obua@17644
  1426
  by (import hollight NADD_MULTIPLICATIVE)
obua@17644
  1427
kaliszyk@43786
  1428
lemma NADD_ADDITIVE: "EX xa.
kaliszyk@43786
  1429
   ALL m n.
kaliszyk@43786
  1430
      hollight.dist (dest_nadd x (m + n), dest_nadd x m + dest_nadd x n)
kaliszyk@43786
  1431
      <= xa"
obua@17644
  1432
  by (import hollight NADD_ADDITIVE)
obua@17644
  1433
kaliszyk@43786
  1434
lemma NADD_SUC: "EX xa. ALL n. hollight.dist (dest_nadd x (Suc n), dest_nadd x n) <= xa"
obua@17644
  1435
  by (import hollight NADD_SUC)
obua@17644
  1436
kaliszyk@43786
  1437
lemma NADD_DIST_LEMMA: "EX xa. ALL m n. hollight.dist (dest_nadd x (m + n), dest_nadd x m) <= xa * n"
obua@17644
  1438
  by (import hollight NADD_DIST_LEMMA)
obua@17644
  1439
kaliszyk@43786
  1440
lemma NADD_DIST: "EX xa.
kaliszyk@43786
  1441
   ALL m n.
kaliszyk@43786
  1442
      hollight.dist (dest_nadd x m, dest_nadd x n)
kaliszyk@43786
  1443
      <= xa * hollight.dist (m, n)"
obua@17644
  1444
  by (import hollight NADD_DIST)
obua@17644
  1445
kaliszyk@43786
  1446
lemma NADD_ALTMUL: "EX A B.
kaliszyk@43786
  1447
   ALL n.
kaliszyk@43786
  1448
      hollight.dist
kaliszyk@43786
  1449
       (n * dest_nadd x (dest_nadd y n), dest_nadd x n * dest_nadd y n)
kaliszyk@43786
  1450
      <= A * n + B"
obua@17644
  1451
  by (import hollight NADD_ALTMUL)
obua@17644
  1452
kaliszyk@43786
  1453
definition
kaliszyk@43786
  1454
  nadd_eq :: "nadd => nadd => bool"  where
obua@17644
  1455
  "nadd_eq ==
kaliszyk@43786
  1456
%u ua. EX B. ALL n. hollight.dist (dest_nadd u n, dest_nadd ua n) <= B"
obua@17644
  1457
obua@17644
  1458
lemma DEF_nadd_eq: "nadd_eq =
kaliszyk@43786
  1459
(%u ua. EX B. ALL n. hollight.dist (dest_nadd u n, dest_nadd ua n) <= B)"
obua@17644
  1460
  by (import hollight DEF_nadd_eq)
obua@17644
  1461
kaliszyk@43786
  1462
lemma NADD_EQ_REFL: "nadd_eq x x"
obua@17644
  1463
  by (import hollight NADD_EQ_REFL)
obua@17644
  1464
kaliszyk@43786
  1465
lemma NADD_EQ_SYM: "nadd_eq x y = nadd_eq y x"
obua@17644
  1466
  by (import hollight NADD_EQ_SYM)
obua@17644
  1467
kaliszyk@43786
  1468
lemma NADD_EQ_TRANS: "nadd_eq x y & nadd_eq y z ==> nadd_eq x z"
obua@17644
  1469
  by (import hollight NADD_EQ_TRANS)
obua@17644
  1470
kaliszyk@43786
  1471
definition
kaliszyk@43786
  1472
  nadd_of_num :: "nat => nadd"  where
kaliszyk@43786
  1473
  "nadd_of_num == %u. mk_nadd (op * u)"
kaliszyk@43786
  1474
kaliszyk@43786
  1475
lemma DEF_nadd_of_num: "nadd_of_num = (%u. mk_nadd (op * u))"
obua@17644
  1476
  by (import hollight DEF_nadd_of_num)
obua@17644
  1477
kaliszyk@43786
  1478
lemma NADD_OF_NUM: "dest_nadd (nadd_of_num x) = op * x"
obua@17644
  1479
  by (import hollight NADD_OF_NUM)
obua@17644
  1480
kaliszyk@43786
  1481
lemma NADD_OF_NUM_WELLDEF: "m = n ==> nadd_eq (nadd_of_num m) (nadd_of_num n)"
obua@17644
  1482
  by (import hollight NADD_OF_NUM_WELLDEF)
obua@17644
  1483
kaliszyk@43786
  1484
lemma NADD_OF_NUM_EQ: "nadd_eq (nadd_of_num m) (nadd_of_num n) = (m = n)"
obua@17644
  1485
  by (import hollight NADD_OF_NUM_EQ)
obua@17644
  1486
kaliszyk@43786
  1487
definition
kaliszyk@43786
  1488
  nadd_le :: "nadd => nadd => bool"  where
kaliszyk@43786
  1489
  "nadd_le == %u ua. EX B. ALL n. dest_nadd u n <= dest_nadd ua n + B"
kaliszyk@43786
  1490
kaliszyk@43786
  1491
lemma DEF_nadd_le: "nadd_le = (%u ua. EX B. ALL n. dest_nadd u n <= dest_nadd ua n + B)"
obua@17644
  1492
  by (import hollight DEF_nadd_le)
obua@17644
  1493
kaliszyk@43786
  1494
lemma NADD_LE_WELLDEF_LEMMA: "nadd_eq x x' & nadd_eq y y' & nadd_le x y ==> nadd_le x' y'"
obua@17644
  1495
  by (import hollight NADD_LE_WELLDEF_LEMMA)
obua@17644
  1496
kaliszyk@43786
  1497
lemma NADD_LE_WELLDEF: "nadd_eq x x' & nadd_eq y y' ==> nadd_le x y = nadd_le x' y'"
obua@17644
  1498
  by (import hollight NADD_LE_WELLDEF)
obua@17644
  1499
kaliszyk@43786
  1500
lemma NADD_LE_REFL: "nadd_le x x"
obua@17644
  1501
  by (import hollight NADD_LE_REFL)
obua@17644
  1502
kaliszyk@43786
  1503
lemma NADD_LE_TRANS: "nadd_le x y & nadd_le y z ==> nadd_le x z"
obua@17644
  1504
  by (import hollight NADD_LE_TRANS)
obua@17644
  1505
kaliszyk@43786
  1506
lemma NADD_LE_ANTISYM: "(nadd_le x y & nadd_le y x) = nadd_eq x y"
obua@17644
  1507
  by (import hollight NADD_LE_ANTISYM)
obua@17644
  1508
kaliszyk@43786
  1509
lemma NADD_LE_TOTAL_LEMMA: "~ nadd_le x y ==> EX n. n ~= 0 & dest_nadd y n + B < dest_nadd x n"
obua@17644
  1510
  by (import hollight NADD_LE_TOTAL_LEMMA)
obua@17644
  1511
kaliszyk@43786
  1512
lemma NADD_LE_TOTAL: "nadd_le x y | nadd_le y x"
obua@17644
  1513
  by (import hollight NADD_LE_TOTAL)
obua@17644
  1514
kaliszyk@43786
  1515
lemma NADD_ARCH: "EX xa. nadd_le x (nadd_of_num xa)"
obua@17644
  1516
  by (import hollight NADD_ARCH)
obua@17644
  1517
kaliszyk@43786
  1518
lemma NADD_OF_NUM_LE: "nadd_le (nadd_of_num m) (nadd_of_num n) = (m <= n)"
obua@17644
  1519
  by (import hollight NADD_OF_NUM_LE)
obua@17644
  1520
kaliszyk@43786
  1521
definition
kaliszyk@43786
  1522
  nadd_add :: "nadd => nadd => nadd"  where
kaliszyk@43786
  1523
  "nadd_add == %u ua. mk_nadd (%n. dest_nadd u n + dest_nadd ua n)"
kaliszyk@43786
  1524
kaliszyk@43786
  1525
lemma DEF_nadd_add: "nadd_add = (%u ua. mk_nadd (%n. dest_nadd u n + dest_nadd ua n))"
obua@17644
  1526
  by (import hollight DEF_nadd_add)
obua@17644
  1527
kaliszyk@43786
  1528
lemma NADD_ADD: "dest_nadd (nadd_add x y) = (%n. dest_nadd x n + dest_nadd y n)"
obua@17644
  1529
  by (import hollight NADD_ADD)
obua@17644
  1530
kaliszyk@43786
  1531
lemma NADD_ADD_WELLDEF: "nadd_eq x x' & nadd_eq y y' ==> nadd_eq (nadd_add x y) (nadd_add x' y')"
obua@17644
  1532
  by (import hollight NADD_ADD_WELLDEF)
obua@17644
  1533
kaliszyk@43786
  1534
lemma NADD_ADD_SYM: "nadd_eq (nadd_add x y) (nadd_add y x)"
obua@17644
  1535
  by (import hollight NADD_ADD_SYM)
obua@17644
  1536
kaliszyk@43786
  1537
lemma NADD_ADD_ASSOC: "nadd_eq (nadd_add x (nadd_add y z)) (nadd_add (nadd_add x y) z)"
obua@17644
  1538
  by (import hollight NADD_ADD_ASSOC)
obua@17644
  1539
kaliszyk@43786
  1540
lemma NADD_ADD_LID: "nadd_eq (nadd_add (nadd_of_num 0) x) x"
obua@17644
  1541
  by (import hollight NADD_ADD_LID)
obua@17644
  1542
kaliszyk@43786
  1543
lemma NADD_ADD_LCANCEL: "nadd_eq (nadd_add x y) (nadd_add x z) ==> nadd_eq y z"
obua@17644
  1544
  by (import hollight NADD_ADD_LCANCEL)
obua@17644
  1545
kaliszyk@43786
  1546
lemma NADD_LE_ADD: "nadd_le x (nadd_add x y)"
obua@17644
  1547
  by (import hollight NADD_LE_ADD)
obua@17644
  1548
kaliszyk@43786
  1549
lemma NADD_LE_EXISTS: "nadd_le x y ==> EX d. nadd_eq y (nadd_add x d)"
obua@17644
  1550
  by (import hollight NADD_LE_EXISTS)
obua@17644
  1551
kaliszyk@43786
  1552
lemma NADD_OF_NUM_ADD: "nadd_eq (nadd_add (nadd_of_num x) (nadd_of_num xa)) (nadd_of_num (x + xa))"
obua@17644
  1553
  by (import hollight NADD_OF_NUM_ADD)
obua@17644
  1554
kaliszyk@43786
  1555
definition
kaliszyk@43786
  1556
  nadd_mul :: "nadd => nadd => nadd"  where
kaliszyk@43786
  1557
  "nadd_mul == %u ua. mk_nadd (%n. dest_nadd u (dest_nadd ua n))"
kaliszyk@43786
  1558
kaliszyk@43786
  1559
lemma DEF_nadd_mul: "nadd_mul = (%u ua. mk_nadd (%n. dest_nadd u (dest_nadd ua n)))"
obua@17644
  1560
  by (import hollight DEF_nadd_mul)
obua@17644
  1561
kaliszyk@43786
  1562
lemma NADD_MUL: "dest_nadd (nadd_mul x y) = (%n. dest_nadd x (dest_nadd y n))"
obua@17644
  1563
  by (import hollight NADD_MUL)
obua@17644
  1564
kaliszyk@43786
  1565
lemma NADD_MUL_SYM: "nadd_eq (nadd_mul x y) (nadd_mul y x)"
obua@17644
  1566
  by (import hollight NADD_MUL_SYM)
obua@17644
  1567
kaliszyk@43786
  1568
lemma NADD_MUL_ASSOC: "nadd_eq (nadd_mul x (nadd_mul y z)) (nadd_mul (nadd_mul x y) z)"
obua@17644
  1569
  by (import hollight NADD_MUL_ASSOC)
obua@17644
  1570
kaliszyk@43786
  1571
lemma NADD_MUL_LID: "nadd_eq (nadd_mul (nadd_of_num 1) x) x"
obua@17644
  1572
  by (import hollight NADD_MUL_LID)
obua@17644
  1573
kaliszyk@43786
  1574
lemma NADD_LDISTRIB: "nadd_eq (nadd_mul x (nadd_add y z)) (nadd_add (nadd_mul x y) (nadd_mul x z))"
obua@17644
  1575
  by (import hollight NADD_LDISTRIB)
obua@17644
  1576
kaliszyk@43786
  1577
lemma NADD_MUL_WELLDEF_LEMMA: "nadd_eq y y' ==> nadd_eq (nadd_mul x y) (nadd_mul x y')"
obua@17644
  1578
  by (import hollight NADD_MUL_WELLDEF_LEMMA)
obua@17644
  1579
kaliszyk@43786
  1580
lemma NADD_MUL_WELLDEF: "nadd_eq x x' & nadd_eq y y' ==> nadd_eq (nadd_mul x y) (nadd_mul x' y')"
obua@17644
  1581
  by (import hollight NADD_MUL_WELLDEF)
obua@17644
  1582
kaliszyk@43786
  1583
lemma NADD_OF_NUM_MUL: "nadd_eq (nadd_mul (nadd_of_num x) (nadd_of_num xa)) (nadd_of_num (x * xa))"
obua@17644
  1584
  by (import hollight NADD_OF_NUM_MUL)
obua@17644
  1585
kaliszyk@43786
  1586
lemma NADD_LE_0: "nadd_le (nadd_of_num 0) x"
obua@17644
  1587
  by (import hollight NADD_LE_0)
obua@17644
  1588
kaliszyk@43786
  1589
lemma NADD_EQ_IMP_LE: "nadd_eq x y ==> nadd_le x y"
obua@17644
  1590
  by (import hollight NADD_EQ_IMP_LE)
obua@17644
  1591
kaliszyk@43786
  1592
lemma NADD_LE_LMUL: "nadd_le y z ==> nadd_le (nadd_mul x y) (nadd_mul x z)"
obua@17644
  1593
  by (import hollight NADD_LE_LMUL)
obua@17644
  1594
kaliszyk@43786
  1595
lemma NADD_LE_RMUL: "nadd_le x y ==> nadd_le (nadd_mul x z) (nadd_mul y z)"
obua@17644
  1596
  by (import hollight NADD_LE_RMUL)
obua@17644
  1597
kaliszyk@43786
  1598
lemma NADD_LE_RADD: "nadd_le (nadd_add x z) (nadd_add y z) = nadd_le x y"
obua@17644
  1599
  by (import hollight NADD_LE_RADD)
obua@17644
  1600
kaliszyk@43786
  1601
lemma NADD_LE_LADD: "nadd_le (nadd_add x y) (nadd_add x z) = nadd_le y z"
obua@17644
  1602
  by (import hollight NADD_LE_LADD)
obua@17644
  1603
kaliszyk@43786
  1604
lemma NADD_RDISTRIB: "nadd_eq (nadd_mul (nadd_add x y) z) (nadd_add (nadd_mul x z) (nadd_mul y z))"
obua@17644
  1605
  by (import hollight NADD_RDISTRIB)
obua@17644
  1606
kaliszyk@43786
  1607
lemma NADD_ARCH_MULT: "~ nadd_eq x (nadd_of_num 0)
kaliszyk@43786
  1608
==> EX xa. nadd_le (nadd_of_num k) (nadd_mul (nadd_of_num xa) x)"
obua@17644
  1609
  by (import hollight NADD_ARCH_MULT)
obua@17644
  1610
kaliszyk@43786
  1611
lemma NADD_ARCH_ZERO: "(!!n. nadd_le (nadd_mul (nadd_of_num n) x) k) ==> nadd_eq x (nadd_of_num 0)"
obua@17644
  1612
  by (import hollight NADD_ARCH_ZERO)
obua@17644
  1613
kaliszyk@43786
  1614
lemma NADD_ARCH_LEMMA: "(!!n. nadd_le (nadd_mul (nadd_of_num n) x)
kaliszyk@43786
  1615
       (nadd_add (nadd_mul (nadd_of_num n) y) z))
kaliszyk@43786
  1616
==> nadd_le x y"
obua@17644
  1617
  by (import hollight NADD_ARCH_LEMMA)
obua@17644
  1618
kaliszyk@43786
  1619
lemma NADD_COMPLETE: "Ex P & (EX M. ALL x. P x --> nadd_le x M)
kaliszyk@43786
  1620
==> EX M. (ALL x. P x --> nadd_le x M) &
kaliszyk@43786
  1621
          (ALL M'. (ALL x. P x --> nadd_le x M') --> nadd_le M M')"
obua@17644
  1622
  by (import hollight NADD_COMPLETE)
obua@17644
  1623
kaliszyk@43786
  1624
lemma NADD_UBOUND: "EX xa N. ALL n>=N. dest_nadd x n <= xa * n"
obua@17644
  1625
  by (import hollight NADD_UBOUND)
obua@17644
  1626
kaliszyk@43786
  1627
lemma NADD_NONZERO: "~ nadd_eq x (nadd_of_num 0) ==> EX N. ALL n>=N. dest_nadd x n ~= 0"
obua@17644
  1628
  by (import hollight NADD_NONZERO)
obua@17644
  1629
kaliszyk@43786
  1630
lemma NADD_LBOUND: "~ nadd_eq x (nadd_of_num 0) ==> EX A N. ALL n>=N. n <= A * dest_nadd x n"
obua@17644
  1631
  by (import hollight NADD_LBOUND)
obua@17644
  1632
kaliszyk@43786
  1633
definition
kaliszyk@43786
  1634
  nadd_rinv :: "nadd => nat => nat"  where
kaliszyk@43786
  1635
  "nadd_rinv == %u n. n * n div dest_nadd u n"
kaliszyk@43786
  1636
kaliszyk@43786
  1637
lemma DEF_nadd_rinv: "nadd_rinv = (%u n. n * n div dest_nadd u n)"
obua@17644
  1638
  by (import hollight DEF_nadd_rinv)
obua@17644
  1639
kaliszyk@43786
  1640
lemma NADD_MUL_LINV_LEMMA0: "~ nadd_eq x (nadd_of_num 0) ==> EX xa B. ALL i. nadd_rinv x i <= xa * i + B"
obua@17644
  1641
  by (import hollight NADD_MUL_LINV_LEMMA0)
obua@17644
  1642
kaliszyk@43786
  1643
lemma NADD_MUL_LINV_LEMMA1: "dest_nadd x n ~= 0
kaliszyk@43786
  1644
==> hollight.dist (dest_nadd x n * nadd_rinv x n, n * n) <= dest_nadd x n"
obua@17644
  1645
  by (import hollight NADD_MUL_LINV_LEMMA1)
obua@17644
  1646
kaliszyk@43786
  1647
lemma NADD_MUL_LINV_LEMMA2: "~ nadd_eq x (nadd_of_num 0)
kaliszyk@43786
  1648
==> EX N. ALL n>=N.
kaliszyk@43786
  1649
             hollight.dist (dest_nadd x n * nadd_rinv x n, n * n)
kaliszyk@43786
  1650
             <= dest_nadd x n"
obua@17644
  1651
  by (import hollight NADD_MUL_LINV_LEMMA2)
obua@17644
  1652
kaliszyk@43786
  1653
lemma NADD_MUL_LINV_LEMMA3: "~ nadd_eq x (nadd_of_num 0)
kaliszyk@43786
  1654
==> EX N. ALL m n.
kaliszyk@43786
  1655
             N <= n -->
kaliszyk@43786
  1656
             hollight.dist
kaliszyk@43786
  1657
              (m * (dest_nadd x m * (dest_nadd x n * nadd_rinv x n)),
kaliszyk@43786
  1658
               m * (dest_nadd x m * (n * n)))
kaliszyk@43786
  1659
             <= m * (dest_nadd x m * dest_nadd x n)"
obua@17644
  1660
  by (import hollight NADD_MUL_LINV_LEMMA3)
obua@17644
  1661
kaliszyk@43786
  1662
lemma NADD_MUL_LINV_LEMMA4: "~ nadd_eq x (nadd_of_num 0)
kaliszyk@43786
  1663
==> EX N. ALL m n.
kaliszyk@43786
  1664
             N <= m & N <= n -->
kaliszyk@43786
  1665
             dest_nadd x m * dest_nadd x n *
kaliszyk@43786
  1666
             hollight.dist (m * nadd_rinv x n, n * nadd_rinv x m)
kaliszyk@43786
  1667
             <= m * n *
kaliszyk@43786
  1668
                hollight.dist (m * dest_nadd x n, n * dest_nadd x m) +
kaliszyk@43786
  1669
                dest_nadd x m * dest_nadd x n * (m + n)"
obua@17644
  1670
  by (import hollight NADD_MUL_LINV_LEMMA4)
obua@17644
  1671
kaliszyk@43786
  1672
lemma NADD_MUL_LINV_LEMMA5: "~ nadd_eq x (nadd_of_num 0)
kaliszyk@43786
  1673
==> EX B N.
kaliszyk@43786
  1674
       ALL m n.
kaliszyk@43786
  1675
          N <= m & N <= n -->
kaliszyk@43786
  1676
          dest_nadd x m * dest_nadd x n *
kaliszyk@43786
  1677
          hollight.dist (m * nadd_rinv x n, n * nadd_rinv x m)
kaliszyk@43786
  1678
          <= B * (m * n * (m + n))"
obua@17644
  1679
  by (import hollight NADD_MUL_LINV_LEMMA5)
obua@17644
  1680
kaliszyk@43786
  1681
lemma NADD_MUL_LINV_LEMMA6: "~ nadd_eq x (nadd_of_num 0)
kaliszyk@43786
  1682
==> EX B N.
kaliszyk@43786
  1683
       ALL m n.
kaliszyk@43786
  1684
          N <= m & N <= n -->
kaliszyk@43786
  1685
          m * n * hollight.dist (m * nadd_rinv x n, n * nadd_rinv x m)
kaliszyk@43786
  1686
          <= B * (m * n * (m + n))"
obua@17644
  1687
  by (import hollight NADD_MUL_LINV_LEMMA6)
obua@17644
  1688
kaliszyk@43786
  1689
lemma NADD_MUL_LINV_LEMMA7: "~ nadd_eq x (nadd_of_num 0)
kaliszyk@43786
  1690
==> EX B N.
kaliszyk@43786
  1691
       ALL m n.
kaliszyk@43786
  1692
          N <= m & N <= n -->
kaliszyk@43786
  1693
          hollight.dist (m * nadd_rinv x n, n * nadd_rinv x m)
kaliszyk@43786
  1694
          <= B * (m + n)"
obua@17644
  1695
  by (import hollight NADD_MUL_LINV_LEMMA7)
obua@17644
  1696
kaliszyk@43786
  1697
lemma NADD_MUL_LINV_LEMMA7a: "~ nadd_eq x (nadd_of_num 0)
kaliszyk@43786
  1698
==> EX A B.
kaliszyk@43786
  1699
       ALL m n.
kaliszyk@43786
  1700
          m <= N -->
kaliszyk@43786
  1701
          hollight.dist (m * nadd_rinv x n, n * nadd_rinv x m) <= A * n + B"
obua@17644
  1702
  by (import hollight NADD_MUL_LINV_LEMMA7a)
obua@17644
  1703
kaliszyk@43786
  1704
lemma NADD_MUL_LINV_LEMMA8: "~ nadd_eq x (nadd_of_num 0)
kaliszyk@43786
  1705
==> EX B. ALL m n.
kaliszyk@43786
  1706
             hollight.dist (m * nadd_rinv x n, n * nadd_rinv x m)
kaliszyk@43786
  1707
             <= B * (m + n)"
obua@17644
  1708
  by (import hollight NADD_MUL_LINV_LEMMA8)
obua@17644
  1709
kaliszyk@43786
  1710
definition
kaliszyk@43786
  1711
  nadd_inv :: "nadd => nadd"  where
obua@17644
  1712
  "nadd_inv ==
kaliszyk@43786
  1713
%u. if nadd_eq u (nadd_of_num 0) then nadd_of_num 0
kaliszyk@43786
  1714
    else mk_nadd (nadd_rinv u)"
obua@17644
  1715
obua@17644
  1716
lemma DEF_nadd_inv: "nadd_inv =
kaliszyk@43786
  1717
(%u. if nadd_eq u (nadd_of_num 0) then nadd_of_num 0
kaliszyk@43786
  1718
     else mk_nadd (nadd_rinv u))"
obua@17644
  1719
  by (import hollight DEF_nadd_inv)
obua@17644
  1720
kaliszyk@43786
  1721
lemma NADD_INV: "dest_nadd (nadd_inv x) =
kaliszyk@43786
  1722
(if nadd_eq x (nadd_of_num 0) then %n. 0 else nadd_rinv x)"
obua@17644
  1723
  by (import hollight NADD_INV)
obua@17644
  1724
kaliszyk@43786
  1725
lemma NADD_MUL_LINV: "~ nadd_eq x (nadd_of_num 0)
kaliszyk@43786
  1726
==> nadd_eq (nadd_mul (nadd_inv x) x) (nadd_of_num 1)"
obua@17644
  1727
  by (import hollight NADD_MUL_LINV)
obua@17644
  1728
obua@17652
  1729
lemma NADD_INV_0: "nadd_eq (nadd_inv (nadd_of_num 0)) (nadd_of_num 0)"
obua@17644
  1730
  by (import hollight NADD_INV_0)
obua@17644
  1731
kaliszyk@43786
  1732
lemma NADD_INV_WELLDEF: "nadd_eq x y ==> nadd_eq (nadd_inv x) (nadd_inv y)"
obua@17644
  1733
  by (import hollight NADD_INV_WELLDEF)
obua@17644
  1734
kaliszyk@43786
  1735
typedef (open) hreal = "{s. EX x. s = nadd_eq x}"  morphisms "dest_hreal" "mk_hreal"
kaliszyk@43786
  1736
  apply (rule light_ex_imp_nonempty[where t="nadd_eq x"])
obua@17644
  1737
  by (import hollight TYDEF_hreal)
obua@17644
  1738
obua@17644
  1739
syntax
obua@17644
  1740
  dest_hreal :: _ 
obua@17644
  1741
obua@17644
  1742
syntax
obua@17644
  1743
  mk_hreal :: _ 
obua@17644
  1744
obua@17644
  1745
lemmas "TYDEF_hreal_@intern" = typedef_hol2hollight 
obua@17644
  1746
  [where a="a :: hreal" and r=r ,
obua@17644
  1747
   OF type_definition_hreal]
obua@17644
  1748
kaliszyk@43786
  1749
definition
kaliszyk@43786
  1750
  hreal_of_num :: "nat => hreal"  where
kaliszyk@43786
  1751
  "hreal_of_num == %m. mk_hreal (nadd_eq (nadd_of_num m))"
kaliszyk@43786
  1752
kaliszyk@43786
  1753
lemma DEF_hreal_of_num: "hreal_of_num = (%m. mk_hreal (nadd_eq (nadd_of_num m)))"
obua@17644
  1754
  by (import hollight DEF_hreal_of_num)
obua@17644
  1755
kaliszyk@43786
  1756
definition
kaliszyk@43786
  1757
  hreal_add :: "hreal => hreal => hreal"  where
obua@17644
  1758
  "hreal_add ==
kaliszyk@43786
  1759
%x y. mk_hreal
kaliszyk@43786
  1760
       (%u. EX xa ya.
kaliszyk@43786
  1761
               nadd_eq (nadd_add xa ya) u &
kaliszyk@43786
  1762
               dest_hreal x xa & dest_hreal y ya)"
obua@17644
  1763
obua@17644
  1764
lemma DEF_hreal_add: "hreal_add =
kaliszyk@43786
  1765
(%x y. mk_hreal
kaliszyk@43786
  1766
        (%u. EX xa ya.
kaliszyk@43786
  1767
                nadd_eq (nadd_add xa ya) u &
kaliszyk@43786
  1768
                dest_hreal x xa & dest_hreal y ya))"
obua@17644
  1769
  by (import hollight DEF_hreal_add)
obua@17644
  1770
kaliszyk@43786
  1771
definition
kaliszyk@43786
  1772
  hreal_mul :: "hreal => hreal => hreal"  where
obua@17644
  1773
  "hreal_mul ==
kaliszyk@43786
  1774
%x y. mk_hreal
kaliszyk@43786
  1775
       (%u. EX xa ya.
kaliszyk@43786
  1776
               nadd_eq (nadd_mul xa ya) u &
kaliszyk@43786
  1777
               dest_hreal x xa & dest_hreal y ya)"
obua@17644
  1778
obua@17644
  1779
lemma DEF_hreal_mul: "hreal_mul =
kaliszyk@43786
  1780
(%x y. mk_hreal
kaliszyk@43786
  1781
        (%u. EX xa ya.
kaliszyk@43786
  1782
                nadd_eq (nadd_mul xa ya) u &
kaliszyk@43786
  1783
                dest_hreal x xa & dest_hreal y ya))"
obua@17644
  1784
  by (import hollight DEF_hreal_mul)
obua@17644
  1785
kaliszyk@43786
  1786
definition
kaliszyk@43786
  1787
  hreal_le :: "hreal => hreal => bool"  where
obua@17644
  1788
  "hreal_le ==
kaliszyk@43786
  1789
%x y. SOME u.
kaliszyk@43786
  1790
         EX xa ya. nadd_le xa ya = u & dest_hreal x xa & dest_hreal y ya"
obua@17644
  1791
obua@17644
  1792
lemma DEF_hreal_le: "hreal_le =
kaliszyk@43786
  1793
(%x y. SOME u.
kaliszyk@43786
  1794
          EX xa ya. nadd_le xa ya = u & dest_hreal x xa & dest_hreal y ya)"
obua@17644
  1795
  by (import hollight DEF_hreal_le)
obua@17644
  1796
kaliszyk@43786
  1797
definition
kaliszyk@43786
  1798
  hreal_inv :: "hreal => hreal"  where
obua@17644
  1799
  "hreal_inv ==
kaliszyk@43786
  1800
%x. mk_hreal (%u. EX xa. nadd_eq (nadd_inv xa) u & dest_hreal x xa)"
obua@17644
  1801
obua@17644
  1802
lemma DEF_hreal_inv: "hreal_inv =
kaliszyk@43786
  1803
(%x. mk_hreal (%u. EX xa. nadd_eq (nadd_inv xa) u & dest_hreal x xa))"
obua@17644
  1804
  by (import hollight DEF_hreal_inv)
obua@17644
  1805
kaliszyk@43786
  1806
lemma HREAL_LE_EXISTS_DEF: "hreal_le m n = (EX d. n = hreal_add m d)"
obua@17644
  1807
  by (import hollight HREAL_LE_EXISTS_DEF)
obua@17644
  1808
kaliszyk@43786
  1809
lemma HREAL_EQ_ADD_LCANCEL: "(hreal_add m n = hreal_add m p) = (n = p)"
obua@17644
  1810
  by (import hollight HREAL_EQ_ADD_LCANCEL)
obua@17644
  1811
kaliszyk@43786
  1812
lemma HREAL_EQ_ADD_RCANCEL: "(hreal_add x xb = hreal_add xa xb) = (x = xa)"
obua@17644
  1813
  by (import hollight HREAL_EQ_ADD_RCANCEL)
obua@17644
  1814
kaliszyk@43786
  1815
lemma HREAL_LE_ADD_LCANCEL: "hreal_le (hreal_add x xa) (hreal_add x xb) = hreal_le xa xb"
obua@17644
  1816
  by (import hollight HREAL_LE_ADD_LCANCEL)
obua@17644
  1817
kaliszyk@43786
  1818
lemma HREAL_LE_ADD_RCANCEL: "hreal_le (hreal_add x xb) (hreal_add xa xb) = hreal_le x xa"
obua@17644
  1819
  by (import hollight HREAL_LE_ADD_RCANCEL)
obua@17644
  1820
kaliszyk@43786
  1821
lemma HREAL_ADD_RID: "hreal_add x (hreal_of_num 0) = x"
obua@17644
  1822
  by (import hollight HREAL_ADD_RID)
obua@17644
  1823
kaliszyk@43786
  1824
lemma HREAL_ADD_RDISTRIB: "hreal_mul (hreal_add x xa) xb = hreal_add (hreal_mul x xb) (hreal_mul xa xb)"
obua@17644
  1825
  by (import hollight HREAL_ADD_RDISTRIB)
obua@17644
  1826
kaliszyk@43786
  1827
lemma HREAL_MUL_LZERO: "hreal_mul (hreal_of_num 0) m = hreal_of_num 0"
obua@17644
  1828
  by (import hollight HREAL_MUL_LZERO)
obua@17644
  1829
kaliszyk@43786
  1830
lemma HREAL_MUL_RZERO: "hreal_mul x (hreal_of_num 0) = hreal_of_num 0"
obua@17644
  1831
  by (import hollight HREAL_MUL_RZERO)
obua@17644
  1832
kaliszyk@43786
  1833
lemma HREAL_ADD_AC: "hreal_add m n = hreal_add n m &
kaliszyk@43786
  1834
hreal_add (hreal_add m n) p = hreal_add m (hreal_add n p) &
obua@17644
  1835
hreal_add m (hreal_add n p) = hreal_add n (hreal_add m p)"
obua@17644
  1836
  by (import hollight HREAL_ADD_AC)
obua@17644
  1837
kaliszyk@43786
  1838
lemma HREAL_LE_ADD2: "hreal_le a b & hreal_le c d ==> hreal_le (hreal_add a c) (hreal_add b d)"
obua@17644
  1839
  by (import hollight HREAL_LE_ADD2)
obua@17644
  1840
kaliszyk@43786
  1841
lemma HREAL_LE_MUL_RCANCEL_IMP: "hreal_le a b ==> hreal_le (hreal_mul a c) (hreal_mul b c)"
obua@17644
  1842
  by (import hollight HREAL_LE_MUL_RCANCEL_IMP)
obua@17644
  1843
kaliszyk@43786
  1844
definition
kaliszyk@43786
  1845
  treal_of_num :: "nat => hreal * hreal"  where
kaliszyk@43786
  1846
  "treal_of_num == %u. (hreal_of_num u, hreal_of_num 0)"
kaliszyk@43786
  1847
kaliszyk@43786
  1848
lemma DEF_treal_of_num: "treal_of_num = (%u. (hreal_of_num u, hreal_of_num 0))"
obua@17644
  1849
  by (import hollight DEF_treal_of_num)
obua@17644
  1850
kaliszyk@43786
  1851
definition
kaliszyk@43786
  1852
  treal_neg :: "hreal * hreal => hreal * hreal"  where
kaliszyk@43786
  1853
  "treal_neg == %u. (snd u, fst u)"
kaliszyk@43786
  1854
kaliszyk@43786
  1855
lemma DEF_treal_neg: "treal_neg = (%u. (snd u, fst u))"
obua@17644
  1856
  by (import hollight DEF_treal_neg)
obua@17644
  1857
kaliszyk@43786
  1858
definition
kaliszyk@43786
  1859
  treal_add :: "hreal * hreal => hreal * hreal => hreal * hreal"  where
kaliszyk@43786
  1860
  "treal_add == %u ua. (hreal_add (fst u) (fst ua), hreal_add (snd u) (snd ua))"
obua@17644
  1861
obua@17644
  1862
lemma DEF_treal_add: "treal_add =
kaliszyk@43786
  1863
(%u ua. (hreal_add (fst u) (fst ua), hreal_add (snd u) (snd ua)))"
obua@17644
  1864
  by (import hollight DEF_treal_add)
obua@17644
  1865
kaliszyk@43786
  1866
definition
kaliszyk@43786
  1867
  treal_mul :: "hreal * hreal => hreal * hreal => hreal * hreal"  where
obua@17644
  1868
  "treal_mul ==
kaliszyk@43786
  1869
%u ua.
obua@17644
  1870
   (hreal_add (hreal_mul (fst u) (fst ua)) (hreal_mul (snd u) (snd ua)),
obua@17644
  1871
    hreal_add (hreal_mul (fst u) (snd ua)) (hreal_mul (snd u) (fst ua)))"
obua@17644
  1872
obua@17644
  1873
lemma DEF_treal_mul: "treal_mul =
kaliszyk@43786
  1874
(%u ua.
obua@17644
  1875
    (hreal_add (hreal_mul (fst u) (fst ua)) (hreal_mul (snd u) (snd ua)),
obua@17644
  1876
     hreal_add (hreal_mul (fst u) (snd ua)) (hreal_mul (snd u) (fst ua))))"
obua@17644
  1877
  by (import hollight DEF_treal_mul)
obua@17644
  1878
kaliszyk@43786
  1879
definition
kaliszyk@43786
  1880
  treal_le :: "hreal * hreal => hreal * hreal => bool"  where
obua@17644
  1881
  "treal_le ==
kaliszyk@43786
  1882
%u ua. hreal_le (hreal_add (fst u) (snd ua)) (hreal_add (fst ua) (snd u))"
obua@17644
  1883
obua@17644
  1884
lemma DEF_treal_le: "treal_le =
kaliszyk@43786
  1885
(%u ua. hreal_le (hreal_add (fst u) (snd ua)) (hreal_add (fst ua) (snd u)))"
obua@17644
  1886
  by (import hollight DEF_treal_le)
obua@17644
  1887
kaliszyk@43786
  1888
definition
kaliszyk@43786
  1889
  treal_inv :: "hreal * hreal => hreal * hreal"  where
obua@17644
  1890
  "treal_inv ==
kaliszyk@43786
  1891
%u. if fst u = snd u then (hreal_of_num 0, hreal_of_num 0)
kaliszyk@43786
  1892
    else if hreal_le (snd u) (fst u)
kaliszyk@43786
  1893
         then (hreal_inv (SOME d. fst u = hreal_add (snd u) d),
kaliszyk@43786
  1894
               hreal_of_num 0)
kaliszyk@43786
  1895
         else (hreal_of_num 0,
kaliszyk@43786
  1896
               hreal_inv (SOME d. snd u = hreal_add (fst u) d))"
obua@17644
  1897
obua@17644
  1898
lemma DEF_treal_inv: "treal_inv =
kaliszyk@43786
  1899
(%u. if fst u = snd u then (hreal_of_num 0, hreal_of_num 0)
kaliszyk@43786
  1900
     else if hreal_le (snd u) (fst u)
kaliszyk@43786
  1901
          then (hreal_inv (SOME d. fst u = hreal_add (snd u) d),
kaliszyk@43786
  1902
                hreal_of_num 0)
kaliszyk@43786
  1903
          else (hreal_of_num 0,
kaliszyk@43786
  1904
                hreal_inv (SOME d. snd u = hreal_add (fst u) d)))"
obua@17644
  1905
  by (import hollight DEF_treal_inv)
obua@17644
  1906
kaliszyk@43786
  1907
definition
kaliszyk@43786
  1908
  treal_eq :: "hreal * hreal => hreal * hreal => bool"  where
kaliszyk@43786
  1909
  "treal_eq == %u ua. hreal_add (fst u) (snd ua) = hreal_add (fst ua) (snd u)"
kaliszyk@43786
  1910
kaliszyk@43786
  1911
lemma DEF_treal_eq: "treal_eq = (%u ua. hreal_add (fst u) (snd ua) = hreal_add (fst ua) (snd u))"
obua@17644
  1912
  by (import hollight DEF_treal_eq)
obua@17644
  1913
kaliszyk@43786
  1914
lemma TREAL_EQ_REFL: "treal_eq x x"
obua@17644
  1915
  by (import hollight TREAL_EQ_REFL)
obua@17644
  1916
kaliszyk@43786
  1917
lemma TREAL_EQ_SYM: "treal_eq x y = treal_eq y x"
obua@17644
  1918
  by (import hollight TREAL_EQ_SYM)
obua@17644
  1919
kaliszyk@43786
  1920
lemma TREAL_EQ_TRANS: "treal_eq x y & treal_eq y z ==> treal_eq x z"
obua@17644
  1921
  by (import hollight TREAL_EQ_TRANS)
obua@17644
  1922
kaliszyk@43786
  1923
lemma TREAL_EQ_AP: "x = xa ==> treal_eq x xa"
obua@17644
  1924
  by (import hollight TREAL_EQ_AP)
obua@17644
  1925
kaliszyk@43786
  1926
lemma TREAL_OF_NUM_EQ: "treal_eq (treal_of_num x) (treal_of_num xa) = (x = xa)"
obua@17644
  1927
  by (import hollight TREAL_OF_NUM_EQ)
obua@17644
  1928
kaliszyk@43786
  1929
lemma TREAL_OF_NUM_LE: "treal_le (treal_of_num x) (treal_of_num xa) = (x <= xa)"
obua@17644
  1930
  by (import hollight TREAL_OF_NUM_LE)
obua@17644
  1931
kaliszyk@43786
  1932
lemma TREAL_OF_NUM_ADD: "treal_eq (treal_add (treal_of_num x) (treal_of_num xa))
kaliszyk@43786
  1933
 (treal_of_num (x + xa))"
obua@17644
  1934
  by (import hollight TREAL_OF_NUM_ADD)
obua@17644
  1935
kaliszyk@43786
  1936
lemma TREAL_OF_NUM_MUL: "treal_eq (treal_mul (treal_of_num x) (treal_of_num xa))
kaliszyk@43786
  1937
 (treal_of_num (x * xa))"
obua@17644
  1938
  by (import hollight TREAL_OF_NUM_MUL)
obua@17644
  1939
kaliszyk@43786
  1940
lemma TREAL_ADD_SYM_EQ: "treal_add x y = treal_add y x"
obua@17644
  1941
  by (import hollight TREAL_ADD_SYM_EQ)
obua@17644
  1942
kaliszyk@43786
  1943
lemma TREAL_MUL_SYM_EQ: "treal_mul x y = treal_mul y x"
obua@17644
  1944
  by (import hollight TREAL_MUL_SYM_EQ)
obua@17644
  1945
kaliszyk@43786
  1946
lemma TREAL_ADD_SYM: "treal_eq (treal_add x y) (treal_add y x)"
obua@17644
  1947
  by (import hollight TREAL_ADD_SYM)
obua@17644
  1948
kaliszyk@43786
  1949
lemma TREAL_ADD_ASSOC: "treal_eq (treal_add x (treal_add y z)) (treal_add (treal_add x y) z)"
obua@17644
  1950
  by (import hollight TREAL_ADD_ASSOC)
obua@17644
  1951
kaliszyk@43786
  1952
lemma TREAL_ADD_LID: "treal_eq (treal_add (treal_of_num 0) x) x"
obua@17644
  1953
  by (import hollight TREAL_ADD_LID)
obua@17644
  1954
kaliszyk@43786
  1955
lemma TREAL_ADD_LINV: "treal_eq (treal_add (treal_neg x) x) (treal_of_num 0)"
obua@17644
  1956
  by (import hollight TREAL_ADD_LINV)
obua@17644
  1957
kaliszyk@43786
  1958
lemma TREAL_MUL_SYM: "treal_eq (treal_mul x xa) (treal_mul xa x)"
obua@17644
  1959
  by (import hollight TREAL_MUL_SYM)
obua@17644
  1960
kaliszyk@43786
  1961
lemma TREAL_MUL_ASSOC: "treal_eq (treal_mul x (treal_mul y z)) (treal_mul (treal_mul x y) z)"
obua@17644
  1962
  by (import hollight TREAL_MUL_ASSOC)
obua@17644
  1963
kaliszyk@43786
  1964
lemma TREAL_MUL_LID: "treal_eq (treal_mul (treal_of_num 1) x) x"
obua@17644
  1965
  by (import hollight TREAL_MUL_LID)
obua@17644
  1966
kaliszyk@43786
  1967
lemma TREAL_ADD_LDISTRIB: "treal_eq (treal_mul x (treal_add y z))
kaliszyk@43786
  1968
 (treal_add (treal_mul x y) (treal_mul x z))"
obua@17644
  1969
  by (import hollight TREAL_ADD_LDISTRIB)
obua@17644
  1970
kaliszyk@43786
  1971
lemma TREAL_LE_REFL: "treal_le x x"
obua@17644
  1972
  by (import hollight TREAL_LE_REFL)
obua@17644
  1973
kaliszyk@43786
  1974
lemma TREAL_LE_ANTISYM: "(treal_le x y & treal_le y x) = treal_eq x y"
obua@17644
  1975
  by (import hollight TREAL_LE_ANTISYM)
obua@17644
  1976
kaliszyk@43786
  1977
lemma TREAL_LE_TRANS: "treal_le x y & treal_le y z ==> treal_le x z"
obua@17644
  1978
  by (import hollight TREAL_LE_TRANS)
obua@17644
  1979
kaliszyk@43786
  1980
lemma TREAL_LE_TOTAL: "treal_le x y | treal_le y x"
obua@17644
  1981
  by (import hollight TREAL_LE_TOTAL)
obua@17644
  1982
kaliszyk@43786
  1983
lemma TREAL_LE_LADD_IMP: "treal_le y z ==> treal_le (treal_add x y) (treal_add x z)"
obua@17644
  1984
  by (import hollight TREAL_LE_LADD_IMP)
obua@17644
  1985
kaliszyk@43786
  1986
lemma TREAL_LE_MUL: "treal_le (treal_of_num 0) x & treal_le (treal_of_num 0) y
kaliszyk@43786
  1987
==> treal_le (treal_of_num 0) (treal_mul x y)"
obua@17644
  1988
  by (import hollight TREAL_LE_MUL)
obua@17644
  1989
obua@17652
  1990
lemma TREAL_INV_0: "treal_eq (treal_inv (treal_of_num 0)) (treal_of_num 0)"
obua@17644
  1991
  by (import hollight TREAL_INV_0)
obua@17644
  1992
kaliszyk@43786
  1993
lemma TREAL_MUL_LINV: "~ treal_eq x (treal_of_num 0)
kaliszyk@43786
  1994
==> treal_eq (treal_mul (treal_inv x) x) (treal_of_num 1)"
obua@17644
  1995
  by (import hollight TREAL_MUL_LINV)
obua@17644
  1996
kaliszyk@43786
  1997
lemma TREAL_OF_NUM_WELLDEF: "m = n ==> treal_eq (treal_of_num m) (treal_of_num n)"
obua@17644
  1998
  by (import hollight TREAL_OF_NUM_WELLDEF)
obua@17644
  1999
kaliszyk@43786
  2000
lemma TREAL_NEG_WELLDEF: "treal_eq x1 x2 ==> treal_eq (treal_neg x1) (treal_neg x2)"
obua@17644
  2001
  by (import hollight TREAL_NEG_WELLDEF)
obua@17644
  2002
kaliszyk@43786
  2003
lemma TREAL_ADD_WELLDEFR: "treal_eq x1 x2 ==> treal_eq (treal_add x1 y) (treal_add x2 y)"
obua@17644
  2004
  by (import hollight TREAL_ADD_WELLDEFR)
obua@17644
  2005
kaliszyk@43786
  2006
lemma TREAL_ADD_WELLDEF: "treal_eq x1 x2 & treal_eq y1 y2
kaliszyk@43786
  2007
==> treal_eq (treal_add x1 y1) (treal_add x2 y2)"
obua@17644
  2008
  by (import hollight TREAL_ADD_WELLDEF)
obua@17644
  2009
kaliszyk@43786
  2010
lemma TREAL_MUL_WELLDEFR: "treal_eq x1 x2 ==> treal_eq (treal_mul x1 y) (treal_mul x2 y)"
obua@17644
  2011
  by (import hollight TREAL_MUL_WELLDEFR)
obua@17644
  2012
kaliszyk@43786
  2013
lemma TREAL_MUL_WELLDEF: "treal_eq x1 x2 & treal_eq y1 y2
kaliszyk@43786
  2014
==> treal_eq (treal_mul x1 y1) (treal_mul x2 y2)"
obua@17644
  2015
  by (import hollight TREAL_MUL_WELLDEF)
obua@17644
  2016
kaliszyk@43786
  2017
lemma TREAL_EQ_IMP_LE: "treal_eq x y ==> treal_le x y"
obua@17644
  2018
  by (import hollight TREAL_EQ_IMP_LE)
obua@17644
  2019
kaliszyk@43786
  2020
lemma TREAL_LE_WELLDEF: "treal_eq x1 x2 & treal_eq y1 y2 ==> treal_le x1 y1 = treal_le x2 y2"
obua@17644
  2021
  by (import hollight TREAL_LE_WELLDEF)
obua@17644
  2022
kaliszyk@43786
  2023
lemma TREAL_INV_WELLDEF: "treal_eq x y ==> treal_eq (treal_inv x) (treal_inv y)"
obua@17644
  2024
  by (import hollight TREAL_INV_WELLDEF)
obua@17644
  2025
kaliszyk@43786
  2026
typedef (open) real = "{s. EX x. s = treal_eq x}"  morphisms "dest_real" "mk_real"
kaliszyk@43786
  2027
  apply (rule light_ex_imp_nonempty[where t="treal_eq x"])
obua@17644
  2028
  by (import hollight TYDEF_real)
obua@17644
  2029
obua@17644
  2030
syntax
obua@17644
  2031
  dest_real :: _ 
obua@17644
  2032
obua@17644
  2033
syntax
obua@17644
  2034
  mk_real :: _ 
obua@17644
  2035
obua@17644
  2036
lemmas "TYDEF_real_@intern" = typedef_hol2hollight 
obua@17644
  2037
  [where a="a :: hollight.real" and r=r ,
obua@17644
  2038
   OF type_definition_real]
obua@17644
  2039
kaliszyk@43786
  2040
definition
kaliszyk@43786
  2041
  real_of_num :: "nat => hollight.real"  where
kaliszyk@43786
  2042
  "real_of_num == %m. mk_real (treal_eq (treal_of_num m))"
kaliszyk@43786
  2043
kaliszyk@43786
  2044
lemma DEF_real_of_num: "real_of_num = (%m. mk_real (treal_eq (treal_of_num m)))"
obua@17644
  2045
  by (import hollight DEF_real_of_num)
obua@17644
  2046
kaliszyk@43786
  2047
definition
kaliszyk@43786
  2048
  real_neg :: "hollight.real => hollight.real"  where
obua@17644
  2049
  "real_neg ==
kaliszyk@43786
  2050
%x1. mk_real (%u. EX x1a. treal_eq (treal_neg x1a) u & dest_real x1 x1a)"
obua@17644
  2051
obua@17644
  2052
lemma DEF_real_neg: "real_neg =
kaliszyk@43786
  2053
(%x1. mk_real (%u. EX x1a. treal_eq (treal_neg x1a) u & dest_real x1 x1a))"
obua@17644
  2054
  by (import hollight DEF_real_neg)
obua@17644
  2055
kaliszyk@43786
  2056
definition
kaliszyk@43786
  2057
  real_add :: "hollight.real => hollight.real => hollight.real"  where
obua@17644
  2058
  "real_add ==
kaliszyk@43786
  2059
%x1 y1.
obua@17644
  2060
   mk_real
kaliszyk@43786
  2061
    (%u. EX x1a y1a.
kaliszyk@43786
  2062
            treal_eq (treal_add x1a y1a) u &
kaliszyk@43786
  2063
            dest_real x1 x1a & dest_real y1 y1a)"
obua@17644
  2064
obua@17644
  2065
lemma DEF_real_add: "real_add =
kaliszyk@43786
  2066
(%x1 y1.
obua@17644
  2067
    mk_real
kaliszyk@43786
  2068
     (%u. EX x1a y1a.
kaliszyk@43786
  2069
             treal_eq (treal_add x1a y1a) u &
kaliszyk@43786
  2070
             dest_real x1 x1a & dest_real y1 y1a))"
obua@17644
  2071
  by (import hollight DEF_real_add)
obua@17644
  2072
kaliszyk@43786
  2073
definition
kaliszyk@43786
  2074
  real_mul :: "hollight.real => hollight.real => hollight.real"  where
obua@17644
  2075
  "real_mul ==
kaliszyk@43786
  2076
%x1 y1.
obua@17644
  2077
   mk_real
kaliszyk@43786
  2078
    (%u. EX x1a y1a.
kaliszyk@43786
  2079
            treal_eq (treal_mul x1a y1a) u &
kaliszyk@43786
  2080
            dest_real x1 x1a & dest_real y1 y1a)"
obua@17644
  2081
obua@17644
  2082
lemma DEF_real_mul: "real_mul =
kaliszyk@43786
  2083
(%x1 y1.
obua@17644
  2084
    mk_real
kaliszyk@43786
  2085
     (%u. EX x1a y1a.
kaliszyk@43786
  2086
             treal_eq (treal_mul x1a y1a) u &
kaliszyk@43786
  2087
             dest_real x1 x1a & dest_real y1 y1a))"
obua@17644
  2088
  by (import hollight DEF_real_mul)
obua@17644
  2089
kaliszyk@43786
  2090
definition
kaliszyk@43786
  2091
  real_le :: "hollight.real => hollight.real => bool"  where
obua@17644
  2092
  "real_le ==
kaliszyk@43786
  2093
%x1 y1.
kaliszyk@43786
  2094
   SOME u.
kaliszyk@43786
  2095
      EX x1a y1a. treal_le x1a y1a = u & dest_real x1 x1a & dest_real y1 y1a"
obua@17644
  2096
obua@17644
  2097
lemma DEF_real_le: "real_le =
kaliszyk@43786
  2098
(%x1 y1.
kaliszyk@43786
  2099
    SOME u.
kaliszyk@43786
  2100
       EX x1a y1a.
obua@17644
  2101
          treal_le x1a y1a = u & dest_real x1 x1a & dest_real y1 y1a)"
obua@17644
  2102
  by (import hollight DEF_real_le)
obua@17644
  2103
kaliszyk@43786
  2104
definition
kaliszyk@43786
  2105
  real_inv :: "hollight.real => hollight.real"  where
obua@17644
  2106
  "real_inv ==
kaliszyk@43786
  2107
%x. mk_real (%u. EX xa. treal_eq (treal_inv xa) u & dest_real x xa)"
obua@17644
  2108
obua@17644
  2109
lemma DEF_real_inv: "real_inv =
kaliszyk@43786
  2110
(%x. mk_real (%u. EX xa. treal_eq (treal_inv xa) u & dest_real x xa))"
obua@17644
  2111
  by (import hollight DEF_real_inv)
obua@17644
  2112
kaliszyk@43786
  2113
definition
kaliszyk@43786
  2114
  real_sub :: "hollight.real => hollight.real => hollight.real"  where
kaliszyk@43786
  2115
  "real_sub == %u ua. real_add u (real_neg ua)"
kaliszyk@43786
  2116
kaliszyk@43786
  2117
lemma DEF_real_sub: "real_sub = (%u ua. real_add u (real_neg ua))"
obua@17644
  2118
  by (import hollight DEF_real_sub)
obua@17644
  2119
kaliszyk@43786
  2120
definition
kaliszyk@43786
  2121
  real_lt :: "hollight.real => hollight.real => bool"  where
kaliszyk@43786
  2122
  "real_lt == %u ua. ~ real_le ua u"
kaliszyk@43786
  2123
kaliszyk@43786
  2124
lemma DEF_real_lt: "real_lt = (%u ua. ~ real_le ua u)"
obua@17644
  2125
  by (import hollight DEF_real_lt)
obua@17644
  2126
kaliszyk@43786
  2127
definition
kaliszyk@43786
  2128
  real_ge :: "hollight.real => hollight.real => bool"  where
kaliszyk@43786
  2129
  "real_ge == %u ua. real_le ua u"
kaliszyk@43786
  2130
kaliszyk@43786
  2131
lemma DEF_real_ge: "real_ge = (%u ua. real_le ua u)"
obua@17644
  2132
  by (import hollight DEF_real_ge)
obua@17644
  2133
kaliszyk@43786
  2134
definition
kaliszyk@43786
  2135
  real_gt :: "hollight.real => hollight.real => bool"  where
kaliszyk@43786
  2136
  "real_gt == %u ua. real_lt ua u"
kaliszyk@43786
  2137
kaliszyk@43786
  2138
lemma DEF_real_gt: "real_gt = (%u ua. real_lt ua u)"
obua@17644
  2139
  by (import hollight DEF_real_gt)
obua@17644
  2140
kaliszyk@43786
  2141
definition
kaliszyk@43786
  2142
  real_abs :: "hollight.real => hollight.real"  where
kaliszyk@43786
  2143
  "real_abs == %u. if real_le (real_of_num 0) u then u else real_neg u"
kaliszyk@43786
  2144
kaliszyk@43786
  2145
lemma DEF_real_abs: "real_abs = (%u. if real_le (real_of_num 0) u then u else real_neg u)"
obua@17644
  2146
  by (import hollight DEF_real_abs)
obua@17644
  2147
kaliszyk@43786
  2148
definition
kaliszyk@43786
  2149
  real_pow :: "hollight.real => nat => hollight.real"  where
obua@17644
  2150
  "real_pow ==
kaliszyk@43786
  2151
SOME real_pow.
kaliszyk@43786
  2152
   (ALL x. real_pow x 0 = real_of_num 1) &
kaliszyk@43786
  2153
   (ALL x n. real_pow x (Suc n) = real_mul x (real_pow x n))"
obua@17644
  2154
obua@17644
  2155
lemma DEF_real_pow: "real_pow =
kaliszyk@43786
  2156
(SOME real_pow.
kaliszyk@43786
  2157
    (ALL x. real_pow x 0 = real_of_num 1) &
kaliszyk@43786
  2158
    (ALL x n. real_pow x (Suc n) = real_mul x (real_pow x n)))"
obua@17644
  2159
  by (import hollight DEF_real_pow)
obua@17644
  2160
kaliszyk@43786
  2161
definition
kaliszyk@43786
  2162
  real_div :: "hollight.real => hollight.real => hollight.real"  where
kaliszyk@43786
  2163
  "real_div == %u ua. real_mul u (real_inv ua)"
kaliszyk@43786
  2164
kaliszyk@43786
  2165
lemma DEF_real_div: "real_div = (%u ua. real_mul u (real_inv ua))"
obua@17644
  2166
  by (import hollight DEF_real_div)
obua@17644
  2167
kaliszyk@43786
  2168
definition
kaliszyk@43786
  2169
  real_max :: "hollight.real => hollight.real => hollight.real"  where
kaliszyk@43786
  2170
  "real_max == %u ua. if real_le u ua then ua else u"
kaliszyk@43786
  2171
kaliszyk@43786
  2172
lemma DEF_real_max: "real_max = (%u ua. if real_le u ua then ua else u)"
obua@17644
  2173
  by (import hollight DEF_real_max)
obua@17644
  2174
kaliszyk@43786
  2175
definition
kaliszyk@43786
  2176
  real_min :: "hollight.real => hollight.real => hollight.real"  where
kaliszyk@43786
  2177
  "real_min == %u ua. if real_le u ua then u else ua"
kaliszyk@43786
  2178
kaliszyk@43786
  2179
lemma DEF_real_min: "real_min = (%u ua. if real_le u ua then u else ua)"
obua@17644
  2180
  by (import hollight DEF_real_min)
obua@17644
  2181
kaliszyk@43786
  2182
lemma REAL_HREAL_LEMMA1: "EX x. (ALL xa. real_le (real_of_num 0) xa = (EX y. xa = x y)) &
kaliszyk@43786
  2183
      (ALL y z. hreal_le y z = real_le (x y) (x z))"
obua@17644
  2184
  by (import hollight REAL_HREAL_LEMMA1)
obua@17644
  2185
kaliszyk@43786
  2186
lemma REAL_HREAL_LEMMA2: "EX x r.
kaliszyk@43786
  2187
   (ALL xa. x (r xa) = xa) &
kaliszyk@43786
  2188
   (ALL xa. real_le (real_of_num 0) xa --> r (x xa) = xa) &
kaliszyk@43786
  2189
   (ALL x. real_le (real_of_num 0) (r x)) &
kaliszyk@43786
  2190
   (ALL x y. hreal_le x y = real_le (r x) (r y))"
obua@17644
  2191
  by (import hollight REAL_HREAL_LEMMA2)
obua@17644
  2192
kaliszyk@43786
  2193
lemma REAL_COMPLETE_SOMEPOS: "(EX x. P x & real_le (real_of_num 0) x) & (EX M. ALL x. P x --> real_le x M)
kaliszyk@43786
  2194
==> EX M. (ALL x. P x --> real_le x M) &
kaliszyk@43786
  2195
          (ALL M'. (ALL x. P x --> real_le x M') --> real_le M M')"
obua@17644
  2196
  by (import hollight REAL_COMPLETE_SOMEPOS)
obua@17644
  2197
kaliszyk@43786
  2198
lemma REAL_COMPLETE: "Ex P & (EX M. ALL x. P x --> real_le x M)
kaliszyk@43786
  2199
==> EX M. (ALL x. P x --> real_le x M) &
kaliszyk@43786
  2200
          (ALL M'. (ALL x. P x --> real_le x M') --> real_le M M')"
obua@17644
  2201
  by (import hollight REAL_COMPLETE)
obua@17644
  2202
kaliszyk@43786
  2203
lemma REAL_ADD_AC: "real_add m n = real_add n m &
kaliszyk@43786
  2204
real_add (real_add m n) p = real_add m (real_add n p) &
obua@17644
  2205
real_add m (real_add n p) = real_add n (real_add m p)"
obua@17644
  2206
  by (import hollight REAL_ADD_AC)
obua@17644
  2207
kaliszyk@43786
  2208
lemma REAL_ADD_RINV: "real_add x (real_neg x) = real_of_num 0"
obua@17644
  2209
  by (import hollight REAL_ADD_RINV)
obua@17644
  2210
kaliszyk@43786
  2211
lemma REAL_EQ_ADD_LCANCEL: "(real_add x y = real_add x z) = (y = z)"
obua@17644
  2212
  by (import hollight REAL_EQ_ADD_LCANCEL)
obua@17644
  2213
kaliszyk@43786
  2214
lemma REAL_EQ_ADD_RCANCEL: "(real_add x z = real_add y z) = (x = y)"
obua@17644
  2215
  by (import hollight REAL_EQ_ADD_RCANCEL)
obua@17644
  2216
kaliszyk@43786
  2217
lemma REAL_MUL_RZERO: "real_mul x (real_of_num 0) = real_of_num 0"
obua@19093
  2218
  by (import hollight REAL_MUL_RZERO)
obua@19093
  2219
kaliszyk@43786
  2220
lemma REAL_MUL_LZERO: "real_mul (real_of_num 0) x = real_of_num 0"
obua@19093
  2221
  by (import hollight REAL_MUL_LZERO)
obua@19093
  2222
kaliszyk@43786
  2223
lemma REAL_NEG_NEG: "real_neg (real_neg x) = x"
obua@17644
  2224
  by (import hollight REAL_NEG_NEG)
obua@17644
  2225
kaliszyk@43786
  2226
lemma REAL_MUL_RNEG: "real_mul x (real_neg y) = real_neg (real_mul x y)"
obua@17644
  2227
  by (import hollight REAL_MUL_RNEG)
obua@17644
  2228
kaliszyk@43786
  2229
lemma REAL_MUL_LNEG: "real_mul (real_neg x) y = real_neg (real_mul x y)"
obua@17644
  2230
  by (import hollight REAL_MUL_LNEG)
obua@17644
  2231
kaliszyk@43786
  2232
lemma REAL_NEG_ADD: "real_neg (real_add x y) = real_add (real_neg x) (real_neg y)"
obua@19093
  2233
  by (import hollight REAL_NEG_ADD)
obua@19093
  2234
kaliszyk@43786
  2235
lemma REAL_ADD_RID: "real_add x (real_of_num 0) = x"
obua@17644
  2236
  by (import hollight REAL_ADD_RID)
obua@17644
  2237
obua@19093
  2238
lemma REAL_NEG_0: "real_neg (real_of_num 0) = real_of_num 0"
obua@19093
  2239
  by (import hollight REAL_NEG_0)
obua@19093
  2240
kaliszyk@43786
  2241
lemma REAL_LE_LNEG: "real_le (real_neg x) y = real_le (real_of_num 0) (real_add x y)"
obua@17644
  2242
  by (import hollight REAL_LE_LNEG)
obua@17644
  2243
kaliszyk@43786
  2244
lemma REAL_LE_NEG2: "real_le (real_neg x) (real_neg y) = real_le y x"
obua@17644
  2245
  by (import hollight REAL_LE_NEG2)
obua@17644
  2246
kaliszyk@43786
  2247
lemma REAL_LE_RNEG: "real_le x (real_neg y) = real_le (real_add x y) (real_of_num 0)"
obua@17644
  2248
  by (import hollight REAL_LE_RNEG)
obua@17644
  2249
kaliszyk@43786
  2250
lemma REAL_OF_NUM_POW: "real_pow (real_of_num x) n = real_of_num (x ^ n)"
obua@17644
  2251
  by (import hollight REAL_OF_NUM_POW)
obua@17644
  2252
kaliszyk@43786
  2253
lemma REAL_POW_NEG: "real_pow (real_neg x) n =
kaliszyk@43786
  2254
(if even n then real_pow x n else real_neg (real_pow x n))"
obua@17644
  2255
  by (import hollight REAL_POW_NEG)
obua@17644
  2256
kaliszyk@43786
  2257
lemma REAL_ABS_NUM: "real_abs (real_of_num x) = real_of_num x"
obua@17644
  2258
  by (import hollight REAL_ABS_NUM)
obua@17644
  2259
kaliszyk@43786
  2260
lemma REAL_ABS_NEG: "real_abs (real_neg x) = real_abs x"
obua@17644
  2261
  by (import hollight REAL_ABS_NEG)
obua@17644
  2262
kaliszyk@43786
  2263
lemma REAL_LTE_TOTAL: "real_lt x xa | real_le xa x"
obua@17644
  2264
  by (import hollight REAL_LTE_TOTAL)
obua@17644
  2265
kaliszyk@43786
  2266
lemma REAL_LET_TOTAL: "real_le x xa | real_lt xa x"
obua@17644
  2267
  by (import hollight REAL_LET_TOTAL)
obua@17644
  2268
kaliszyk@43786
  2269
lemma REAL_LT_IMP_LE: "real_lt x y ==> real_le x y"
obua@19093
  2270
  by (import hollight REAL_LT_IMP_LE)
obua@19093
  2271
kaliszyk@43786
  2272
lemma REAL_LTE_TRANS: "real_lt x y & real_le y z ==> real_lt x z"
obua@19093
  2273
  by (import hollight REAL_LTE_TRANS)
obua@19093
  2274
kaliszyk@43786
  2275
lemma REAL_LET_TRANS: "real_le x y & real_lt y z ==> real_lt x z"
obua@17644
  2276
  by (import hollight REAL_LET_TRANS)
obua@17644
  2277
kaliszyk@43786
  2278
lemma REAL_LT_TRANS: "real_lt x y & real_lt y z ==> real_lt x z"
obua@17644
  2279
  by (import hollight REAL_LT_TRANS)
obua@17644
  2280
kaliszyk@43786
  2281
lemma REAL_LE_ADD: "real_le (real_of_num 0) x & real_le (real_of_num 0) y
kaliszyk@43786
  2282
==> real_le (real_of_num 0) (real_add x y)"
obua@17644
  2283
  by (import hollight REAL_LE_ADD)
obua@17644
  2284
kaliszyk@43786
  2285
lemma REAL_LTE_ANTISYM: "~ (real_lt x y & real_le y x)"
obua@17644
  2286
  by (import hollight REAL_LTE_ANTISYM)
obua@17644
  2287
kaliszyk@43786
  2288
lemma REAL_SUB_LE: "real_le (real_of_num 0) (real_sub x xa) = real_le xa x"
obua@19093
  2289
  by (import hollight REAL_SUB_LE)
obua@19093
  2290
kaliszyk@43786
  2291
lemma REAL_NEG_SUB: "real_neg (real_sub x xa) = real_sub xa x"
obua@19093
  2292
  by (import hollight REAL_NEG_SUB)
obua@19093
  2293
kaliszyk@43786
  2294
lemma REAL_LE_LT: "real_le x xa = (real_lt x xa | x = xa)"
obua@19093
  2295
  by (import hollight REAL_LE_LT)
obua@19093
  2296
kaliszyk@43786
  2297
lemma REAL_SUB_LT: "real_lt (real_of_num 0) (real_sub x xa) = real_lt xa x"
obua@19093
  2298
  by (import hollight REAL_SUB_LT)
obua@19093
  2299
kaliszyk@43786
  2300
lemma REAL_NOT_LT: "(~ real_lt x xa) = real_le xa x"
obua@19093
  2301
  by (import hollight REAL_NOT_LT)
obua@19093
  2302
kaliszyk@43786
  2303
lemma REAL_SUB_0: "(real_sub x y = real_of_num 0) = (x = y)"
obua@19093
  2304
  by (import hollight REAL_SUB_0)
obua@19093
  2305
kaliszyk@43786
  2306
lemma REAL_LT_LE: "real_lt x y = (real_le x y & x ~= y)"
obua@19093
  2307
  by (import hollight REAL_LT_LE)
obua@19093
  2308
kaliszyk@43786
  2309
lemma REAL_LT_REFL: "~ real_lt x x"
obua@17644
  2310
  by (import hollight REAL_LT_REFL)
obua@17644
  2311
kaliszyk@43786
  2312
lemma REAL_LTE_ADD: "real_lt (real_of_num 0) x & real_le (real_of_num 0) y
kaliszyk@43786
  2313
==> real_lt (real_of_num 0) (real_add x y)"
obua@19093
  2314
  by (import hollight REAL_LTE_ADD)
obua@19093
  2315
kaliszyk@43786
  2316
lemma REAL_LET_ADD: "real_le (real_of_num 0) x & real_lt (real_of_num 0) y
kaliszyk@43786
  2317
==> real_lt (real_of_num 0) (real_add x y)"
obua@17644
  2318
  by (import hollight REAL_LET_ADD)
obua@17644
  2319
kaliszyk@43786
  2320
lemma REAL_LT_ADD: "real_lt (real_of_num 0) x & real_lt (real_of_num 0) y
kaliszyk@43786
  2321
==> real_lt (real_of_num 0) (real_add x y)"
obua@19093
  2322
  by (import hollight REAL_LT_ADD)
obua@19093
  2323
kaliszyk@43786
  2324
lemma REAL_ENTIRE: "(real_mul x y = real_of_num 0) = (x = real_of_num 0 | y = real_of_num 0)"
obua@17644
  2325
  by (import hollight REAL_ENTIRE)
obua@17644
  2326
kaliszyk@43786
  2327
lemma REAL_LE_NEGTOTAL: "real_le (real_of_num 0) x | real_le (real_of_num 0) (real_neg x)"
obua@19093
  2328
  by (import hollight REAL_LE_NEGTOTAL)
obua@19093
  2329
kaliszyk@43786
  2330
lemma REAL_LE_SQUARE: "real_le (real_of_num 0) (real_mul x x)"
obua@19093
  2331
  by (import hollight REAL_LE_SQUARE)
obua@19093
  2332
kaliszyk@43786
  2333
lemma REAL_MUL_RID: "real_mul x (real_of_num 1) = x"
obua@19093
  2334
  by (import hollight REAL_MUL_RID)
obua@19093
  2335
kaliszyk@43786
  2336
lemma REAL_POW_2: "real_pow x 2 = real_mul x x"
obua@17644
  2337
  by (import hollight REAL_POW_2)
obua@17644
  2338
kaliszyk@43786
  2339
lemma REAL_POLY_CLAUSES: "(ALL x y z. real_add x (real_add y z) = real_add (real_add x y) z) &
kaliszyk@43786
  2340
(ALL x y. real_add x y = real_add y x) &
kaliszyk@43786
  2341
(ALL x. real_add (real_of_num 0) x = x) &
kaliszyk@43786
  2342
(ALL x y z. real_mul x (real_mul y z) = real_mul (real_mul x y) z) &
kaliszyk@43786
  2343
(ALL x y. real_mul x y = real_mul y x) &
kaliszyk@43786
  2344
(ALL x. real_mul (real_of_num 1) x = x) &
kaliszyk@43786
  2345
(ALL x. real_mul (real_of_num 0) x = real_of_num 0) &
kaliszyk@43786
  2346
(ALL x xa xb.
obua@17644
  2347
    real_mul x (real_add xa xb) =
obua@17644
  2348
    real_add (real_mul x xa) (real_mul x xb)) &
kaliszyk@43786
  2349
(ALL x. real_pow x 0 = real_of_num 1) &
kaliszyk@43786
  2350
(ALL x xa. real_pow x (Suc xa) = real_mul x (real_pow x xa))"
obua@17644
  2351
  by (import hollight REAL_POLY_CLAUSES)
obua@17644
  2352
kaliszyk@43786
  2353
lemma REAL_POLY_NEG_CLAUSES: "(ALL x. real_neg x = real_mul (real_neg (real_of_num 1)) x) &
kaliszyk@43786
  2354
(ALL x xa.
kaliszyk@43786
  2355
    real_sub x xa = real_add x (real_mul (real_neg (real_of_num 1)) xa))"
obua@17644
  2356
  by (import hollight REAL_POLY_NEG_CLAUSES)
obua@17644
  2357
kaliszyk@43786
  2358
lemma REAL_POS: "real_le (real_of_num 0) (real_of_num x)"
obua@19093
  2359
  by (import hollight REAL_POS)
obua@19093
  2360
kaliszyk@43786
  2361
lemma REAL_OF_NUM_LT: "real_lt (real_of_num x) (real_of_num xa) = (x < xa)"
obua@17644
  2362
  by (import hollight REAL_OF_NUM_LT)
obua@17644
  2363
kaliszyk@43786
  2364
lemma REAL_OF_NUM_GE: "real_ge (real_of_num x) (real_of_num xa) = (xa <= x)"
obua@17644
  2365
  by (import hollight REAL_OF_NUM_GE)
obua@17644
  2366
kaliszyk@43786
  2367
lemma REAL_OF_NUM_GT: "real_gt (real_of_num x) (real_of_num xa) = (xa < x)"
obua@17644
  2368
  by (import hollight REAL_OF_NUM_GT)
obua@17644
  2369
kaliszyk@43786
  2370
lemma REAL_OF_NUM_MAX: "real_max (real_of_num x) (real_of_num xa) = real_of_num (max x xa)"
kaliszyk@43786
  2371
  by (import hollight REAL_OF_NUM_MAX)
kaliszyk@43786
  2372
kaliszyk@43786
  2373
lemma REAL_OF_NUM_MIN: "real_min (real_of_num x) (real_of_num xa) = real_of_num (min x xa)"
kaliszyk@43786
  2374
  by (import hollight REAL_OF_NUM_MIN)
kaliszyk@43786
  2375
kaliszyk@43786
  2376
lemma REAL_OF_NUM_SUC: "real_add (real_of_num x) (real_of_num 1) = real_of_num (Suc x)"
obua@17644
  2377
  by (import hollight REAL_OF_NUM_SUC)
obua@17644
  2378
kaliszyk@43786
  2379
lemma REAL_OF_NUM_SUB: "m <= n ==> real_sub (real_of_num n) (real_of_num m) = real_of_num (n - m)"
obua@17644
  2380
  by (import hollight REAL_OF_NUM_SUB)
obua@17644
  2381
kaliszyk@43786
  2382
lemma REAL_MUL_AC: "real_mul m n = real_mul n m &
kaliszyk@43786
  2383
real_mul (real_mul m n) p = real_mul m (real_mul n p) &
obua@17644
  2384
real_mul m (real_mul n p) = real_mul n (real_mul m p)"
obua@17644
  2385
  by (import hollight REAL_MUL_AC)
obua@17644
  2386
kaliszyk@43786
  2387
lemma REAL_ADD_RDISTRIB: "real_mul (real_add x y) z = real_add (real_mul x z) (real_mul y z)"
obua@17644
  2388
  by (import hollight REAL_ADD_RDISTRIB)
obua@17644
  2389
kaliszyk@43786
  2390
lemma REAL_LT_LADD_IMP: "real_lt y z ==> real_lt (real_add x y) (real_add x z)"
obua@17644
  2391
  by (import hollight REAL_LT_LADD_IMP)
obua@17644
  2392
kaliszyk@43786
  2393
lemma REAL_LT_MUL: "real_lt (real_of_num 0) x & real_lt (real_of_num 0) y
kaliszyk@43786
  2394
==> real_lt (real_of_num 0) (real_mul x y)"
obua@17644
  2395
  by (import hollight REAL_LT_MUL)
obua@17644
  2396
kaliszyk@43786
  2397
lemma REAL_EQ_ADD_LCANCEL_0: "(real_add x y = x) = (y = real_of_num 0)"
obua@17644
  2398
  by (import hollight REAL_EQ_ADD_LCANCEL_0)
obua@17644
  2399
kaliszyk@43786
  2400
lemma REAL_EQ_ADD_RCANCEL_0: "(real_add x y = y) = (x = real_of_num 0)"
obua@17644
  2401
  by (import hollight REAL_EQ_ADD_RCANCEL_0)
obua@17644
  2402
kaliszyk@43786
  2403
lemma REAL_LNEG_UNIQ: "(real_add x y = real_of_num 0) = (x = real_neg y)"
obua@19093
  2404
  by (import hollight REAL_LNEG_UNIQ)
obua@19093
  2405
kaliszyk@43786
  2406
lemma REAL_RNEG_UNIQ: "(real_add x y = real_of_num 0) = (y = real_neg x)"
obua@19093
  2407
  by (import hollight REAL_RNEG_UNIQ)
obua@19093
  2408
kaliszyk@43786
  2409
lemma REAL_NEG_LMUL: "real_neg (real_mul x y) = real_mul (real_neg x) y"
obua@19093
  2410
  by (import hollight REAL_NEG_LMUL)
obua@19093
  2411
kaliszyk@43786
  2412
lemma REAL_NEG_RMUL: "real_neg (real_mul x y) = real_mul x (real_neg y)"
obua@19093
  2413
  by (import hollight REAL_NEG_RMUL)
obua@19093
  2414
kaliszyk@43786
  2415
lemma REAL_NEGNEG: "real_neg (real_neg x) = x"
obua@19093
  2416
  by (import hollight REAL_NEGNEG)
obua@19093
  2417
kaliszyk@43786
  2418
lemma REAL_NEG_MUL2: "real_mul (real_neg x) (real_neg y) = real_mul x y"
obua@19093
  2419
  by (import hollight REAL_NEG_MUL2)
obua@19093
  2420
kaliszyk@43786
  2421
lemma REAL_LT_LADD: "real_lt (real_add x y) (real_add x z) = real_lt y z"
obua@19093
  2422
  by (import hollight REAL_LT_LADD)
obua@19093
  2423
kaliszyk@43786
  2424
lemma REAL_LT_RADD: "real_lt (real_add x z) (real_add y z) = real_lt x y"
obua@19093
  2425
  by (import hollight REAL_LT_RADD)
obua@19093
  2426
kaliszyk@43786
  2427
lemma REAL_LT_ANTISYM: "~ (real_lt x y & real_lt y x)"
obua@19093
  2428
  by (import hollight REAL_LT_ANTISYM)
obua@19093
  2429
kaliszyk@43786
  2430
lemma REAL_LT_GT: "real_lt x y ==> ~ real_lt y x"
obua@19093
  2431
  by (import hollight REAL_LT_GT)
obua@19093
  2432
kaliszyk@43786
  2433
lemma REAL_NOT_EQ: "(x ~= y) = (real_lt x y | real_lt y x)"
obua@17644
  2434
  by (import hollight REAL_NOT_EQ)
obua@17644
  2435
kaliszyk@43786
  2436
lemma REAL_LET_ANTISYM: "~ (real_le x y & real_lt y x)"
obua@17644
  2437
  by (import hollight REAL_LET_ANTISYM)
obua@17644
  2438
kaliszyk@43786
  2439
lemma REAL_NEG_LT0: "real_lt (real_neg x) (real_of_num 0) = real_lt (real_of_num 0) x"
obua@19093
  2440
  by (import hollight REAL_NEG_LT0)
obua@19093
  2441
kaliszyk@43786
  2442
lemma REAL_NEG_GT0: "real_lt (real_of_num 0) (real_neg x) = real_lt x (real_of_num 0)"
obua@19093
  2443
  by (import hollight REAL_NEG_GT0)
obua@19093
  2444
kaliszyk@43786
  2445
lemma REAL_NEG_LE0: "real_le (real_neg x) (real_of_num 0) = real_le (real_of_num 0) x"
obua@19093
  2446
  by (import hollight REAL_NEG_LE0)
obua@19093
  2447
kaliszyk@43786
  2448
lemma REAL_NEG_GE0: "real_le (real_of_num 0) (real_neg x) = real_le x (real_of_num 0)"
obua@19093
  2449
  by (import hollight REAL_NEG_GE0)
obua@19093
  2450
kaliszyk@43786
  2451
lemma REAL_LT_TOTAL: "x = y | real_lt x y | real_lt y x"
obua@17644
  2452
  by (import hollight REAL_LT_TOTAL)
obua@17644
  2453
kaliszyk@43786
  2454
lemma REAL_LT_NEGTOTAL: "x = real_of_num 0 |
kaliszyk@43786
  2455
real_lt (real_of_num 0) x | real_lt (real_of_num 0) (real_neg x)"
obua@19093
  2456
  by (import hollight REAL_LT_NEGTOTAL)
obua@19093
  2457
kaliszyk@43786
  2458
lemma REAL_LE_01: "real_le (real_of_num 0) (real_of_num 1)"
obua@17644
  2459
  by (import hollight REAL_LE_01)
obua@17644
  2460
kaliszyk@43786
  2461
lemma REAL_LT_01: "real_lt (real_of_num 0) (real_of_num 1)"
obua@19093
  2462
  by (import hollight REAL_LT_01)
obua@19093
  2463
kaliszyk@43786
  2464
lemma REAL_LE_LADD: "real_le (real_add x y) (real_add x z) = real_le y z"
obua@19093
  2465
  by (import hollight REAL_LE_LADD)
obua@19093
  2466
kaliszyk@43786
  2467
lemma REAL_LE_RADD: "real_le (real_add x z) (real_add y z) = real_le x y"
obua@19093
  2468
  by (import hollight REAL_LE_RADD)
obua@19093
  2469
kaliszyk@43786
  2470
lemma REAL_LT_ADD2: "real_lt w x & real_lt y z ==> real_lt (real_add w y) (real_add x z)"
obua@19093
  2471
  by (import hollight REAL_LT_ADD2)
obua@19093
  2472
kaliszyk@43786
  2473
lemma REAL_LE_ADD2: "real_le w x & real_le y z ==> real_le (real_add w y) (real_add x z)"
obua@17644
  2474
  by (import hollight REAL_LE_ADD2)
obua@17644
  2475
kaliszyk@43786
  2476
lemma REAL_LT_LNEG: "real_lt (real_neg x) xa = real_lt (real_of_num 0) (real_add x xa)"
obua@17644
  2477
  by (import hollight REAL_LT_LNEG)
obua@17644
  2478
kaliszyk@43786
  2479
lemma REAL_LT_RNEG: "real_lt x (real_neg xa) = real_lt (real_add x xa) (real_of_num 0)"
obua@17644
  2480
  by (import hollight REAL_LT_RNEG)
obua@17644
  2481
kaliszyk@43786
  2482
lemma REAL_LT_ADDNEG: "real_lt y (real_add x (real_neg z)) = real_lt (real_add y z) x"
obua@19093
  2483
  by (import hollight REAL_LT_ADDNEG)
obua@19093
  2484
kaliszyk@43786
  2485
lemma REAL_LT_ADDNEG2: "real_lt (real_add x (real_neg y)) z = real_lt x (real_add z y)"
obua@19093
  2486
  by (import hollight REAL_LT_ADDNEG2)
obua@19093
  2487
kaliszyk@43786
  2488
lemma REAL_LT_ADD1: "real_le x y ==> real_lt x (real_add y (real_of_num 1))"
obua@19093
  2489
  by (import hollight REAL_LT_ADD1)
obua@19093
  2490
kaliszyk@43786
  2491
lemma REAL_SUB_ADD: "real_add (real_sub x y) y = x"
obua@19093
  2492
  by (import hollight REAL_SUB_ADD)
obua@19093
  2493
kaliszyk@43786
  2494
lemma REAL_SUB_ADD2: "real_add y (real_sub x y) = x"
obua@19093
  2495
  by (import hollight REAL_SUB_ADD2)
obua@19093
  2496
kaliszyk@43786
  2497
lemma REAL_SUB_REFL: "real_sub x x = real_of_num 0"
obua@19093
  2498
  by (import hollight REAL_SUB_REFL)
obua@19093
  2499
kaliszyk@43786
  2500
lemma REAL_LE_DOUBLE: "real_le (real_of_num 0) (real_add x x) = real_le (real_of_num 0) x"
obua@19093
  2501
  by (import hollight REAL_LE_DOUBLE)
obua@19093
  2502
kaliszyk@43786
  2503
lemma REAL_LE_NEGL: "real_le (real_neg x) x = real_le (real_of_num 0) x"
obua@19093
  2504
  by (import hollight REAL_LE_NEGL)
obua@19093
  2505
kaliszyk@43786
  2506
lemma REAL_LE_NEGR: "real_le x (real_neg x) = real_le x (real_of_num 0)"
obua@19093
  2507
  by (import hollight REAL_LE_NEGR)
obua@19093
  2508
kaliszyk@43786
  2509
lemma REAL_NEG_EQ_0: "(real_neg x = real_of_num 0) = (x = real_of_num 0)"
obua@17644
  2510
  by (import hollight REAL_NEG_EQ_0)
obua@17644
  2511
kaliszyk@43786
  2512
lemma REAL_ADD_SUB: "real_sub (real_add x y) x = y"
obua@17644
  2513
  by (import hollight REAL_ADD_SUB)
obua@17644
  2514
kaliszyk@43786
  2515
lemma REAL_NEG_EQ: "(real_neg x = y) = (x = real_neg y)"
obua@19093
  2516
  by (import hollight REAL_NEG_EQ)
obua@19093
  2517
kaliszyk@43786
  2518
lemma REAL_NEG_MINUS1: "real_neg x = real_mul (real_neg (real_of_num 1)) x"
obua@19093
  2519
  by (import hollight REAL_NEG_MINUS1)
obua@19093
  2520
kaliszyk@43786
  2521
lemma REAL_LT_IMP_NE: "real_lt x y ==> x ~= y"
obua@19093
  2522
  by (import hollight REAL_LT_IMP_NE)
obua@19093
  2523
kaliszyk@43786
  2524
lemma REAL_LE_ADDR: "real_le x (real_add x y) = real_le (real_of_num 0) y"
obua@17644
  2525
  by (import hollight REAL_LE_ADDR)
obua@17644
  2526
kaliszyk@43786
  2527
lemma REAL_LE_ADDL: "real_le y (real_add x y) = real_le (real_of_num 0) x"
obua@17644
  2528
  by (import hollight REAL_LE_ADDL)
obua@17644
  2529
kaliszyk@43786
  2530
lemma REAL_LT_ADDR: "real_lt x (real_add x y) = real_lt (real_of_num 0) y"
obua@17644
  2531
  by (import hollight REAL_LT_ADDR)
obua@17644
  2532