src/HOL/Import/HOLLight/HOLLight.thy
author wenzelm
Wed Oct 19 21:52:27 2005 +0200 (2005-10-19)
changeset 17915 e38947f9ba5e
parent 17652 b1ef33ebfa17
child 19093 6d584f9d2021
permissions -rw-r--r--
isatool fixheaders;
obua@17644
     1
(* AUTOMATICALLY GENERATED, DO NOT EDIT! *)
obua@17644
     2
wenzelm@17915
     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
obua@17644
    16
lemma CONJ_ACI: "((p::bool) & (q::bool)) = (q & p) &
obua@17644
    17
((p & q) & (r::bool)) = (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
obua@17644
    21
lemma DISJ_ACI: "((p::bool) | (q::bool)) = (q | p) &
obua@17644
    22
((p | q) | (r::bool)) = (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
obua@17644
    26
lemma EQ_CLAUSES: "ALL t::bool.
obua@17644
    27
   (True = t) = t &
obua@17644
    28
   (t = True) = t & (False = t) = (~ t) & (t = False) = (~ t)"
obua@17644
    29
  by (import hollight EQ_CLAUSES)
obua@17644
    30
obua@17644
    31
lemma NOT_CLAUSES_WEAK: "(~ True) = False & (~ False) = True"
obua@17644
    32
  by (import hollight NOT_CLAUSES_WEAK)
obua@17644
    33
obua@17644
    34
lemma AND_CLAUSES: "ALL t::bool.
obua@17644
    35
   (True & t) = t &
obua@17644
    36
   (t & True) = t & (False & t) = False & (t & False) = False & (t & t) = t"
obua@17644
    37
  by (import hollight AND_CLAUSES)
obua@17644
    38
obua@17644
    39
lemma OR_CLAUSES: "ALL t::bool.
obua@17644
    40
   (True | t) = True &
obua@17644
    41
   (t | True) = True & (False | t) = t & (t | False) = t & (t | t) = t"
obua@17644
    42
  by (import hollight OR_CLAUSES)
obua@17644
    43
obua@17644
    44
lemma IMP_CLAUSES: "ALL t::bool.
obua@17644
    45
   (True --> t) = t &
obua@17644
    46
   (t --> True) = True &
obua@17644
    47
   (False --> t) = True & (t --> t) = True & (t --> False) = (~ t)"
obua@17644
    48
  by (import hollight IMP_CLAUSES)
obua@17644
    49
obua@17644
    50
lemma IMP_EQ_CLAUSE: "((x::'q_864::type) = x --> (p::bool)) = p"
obua@17644
    51
  by (import hollight IMP_EQ_CLAUSE)
obua@17644
    52
obua@17644
    53
lemma SWAP_FORALL_THM: "ALL P::'A::type => 'B::type => bool.
obua@17644
    54
   (ALL x::'A::type. All (P x)) = (ALL (y::'B::type) x::'A::type. P x y)"
obua@17644
    55
  by (import hollight SWAP_FORALL_THM)
obua@17644
    56
obua@17644
    57
lemma SWAP_EXISTS_THM: "ALL P::'A::type => 'B::type => bool.
obua@17644
    58
   (EX x::'A::type. Ex (P x)) = (EX (x::'B::type) xa::'A::type. P xa x)"
obua@17644
    59
  by (import hollight SWAP_EXISTS_THM)
obua@17644
    60
obua@17644
    61
lemma TRIV_EXISTS_AND_THM: "ALL (P::bool) Q::bool.
obua@17644
    62
   (EX x::'A::type. P & Q) = ((EX x::'A::type. P) & (EX x::'A::type. Q))"
obua@17644
    63
  by (import hollight TRIV_EXISTS_AND_THM)
obua@17644
    64
obua@17644
    65
lemma TRIV_AND_EXISTS_THM: "ALL (P::bool) Q::bool.
obua@17644
    66
   ((EX x::'A::type. P) & (EX x::'A::type. Q)) = (EX x::'A::type. P & Q)"
obua@17644
    67
  by (import hollight TRIV_AND_EXISTS_THM)
obua@17644
    68
obua@17644
    69
lemma TRIV_FORALL_OR_THM: "ALL (P::bool) Q::bool.
obua@17644
    70
   (ALL x::'A::type. P | Q) = ((ALL x::'A::type. P) | (ALL x::'A::type. Q))"
obua@17644
    71
  by (import hollight TRIV_FORALL_OR_THM)
obua@17644
    72
obua@17644
    73
lemma TRIV_OR_FORALL_THM: "ALL (P::bool) Q::bool.
obua@17644
    74
   ((ALL x::'A::type. P) | (ALL x::'A::type. Q)) = (ALL x::'A::type. P | Q)"
obua@17644
    75
  by (import hollight TRIV_OR_FORALL_THM)
obua@17644
    76
obua@17644
    77
lemma TRIV_FORALL_IMP_THM: "ALL (P::bool) Q::bool.
obua@17644
    78
   (ALL x::'A::type. P --> Q) =
obua@17644
    79
   ((EX x::'A::type. P) --> (ALL x::'A::type. Q))"
obua@17644
    80
  by (import hollight TRIV_FORALL_IMP_THM)
obua@17644
    81
obua@17644
    82
lemma TRIV_EXISTS_IMP_THM: "ALL (P::bool) Q::bool.
obua@17644
    83
   (EX x::'A::type. P --> Q) =
obua@17644
    84
   ((ALL x::'A::type. P) --> (EX x::'A::type. Q))"
obua@17644
    85
  by (import hollight TRIV_EXISTS_IMP_THM)
obua@17644
    86
obua@17644
    87
lemma EXISTS_UNIQUE_ALT: "ALL P::'A::type => bool.
obua@17644
    88
   Ex1 P = (EX x::'A::type. ALL y::'A::type. P y = (x = y))"
obua@17644
    89
  by (import hollight EXISTS_UNIQUE_ALT)
obua@17644
    90
obua@17644
    91
lemma SELECT_UNIQUE: "ALL (P::'A::type => bool) x::'A::type.
obua@17644
    92
   (ALL y::'A::type. P y = (y = x)) --> Eps P = x"
obua@17644
    93
  by (import hollight SELECT_UNIQUE)
obua@17644
    94
obua@17644
    95
lemma EXCLUDED_MIDDLE: "ALL t::bool. t | ~ t"
obua@17644
    96
  by (import hollight EXCLUDED_MIDDLE)
obua@17644
    97
obua@17644
    98
constdefs
obua@17652
    99
  COND :: "bool => 'A => 'A => 'A" 
obua@17644
   100
  "COND ==
obua@17644
   101
%(t::bool) (t1::'A::type) t2::'A::type.
obua@17644
   102
   SOME x::'A::type. (t = True --> x = t1) & (t = False --> x = t2)"
obua@17644
   103
obua@17644
   104
lemma DEF_COND: "COND =
obua@17644
   105
(%(t::bool) (t1::'A::type) t2::'A::type.
obua@17644
   106
    SOME x::'A::type. (t = True --> x = t1) & (t = False --> x = t2))"
obua@17644
   107
  by (import hollight DEF_COND)
obua@17644
   108
obua@17644
   109
lemma COND_CLAUSES: "ALL (x::'A::type) xa::'A::type. COND True x xa = x & COND False x xa = xa"
obua@17644
   110
  by (import hollight COND_CLAUSES)
obua@17644
   111
obua@17644
   112
lemma COND_EXPAND: "ALL (b::bool) (t1::bool) t2::bool. COND b t1 t2 = ((~ b | t1) & (b | t2))"
obua@17644
   113
  by (import hollight COND_EXPAND)
obua@17644
   114
obua@17644
   115
lemma COND_ID: "ALL (b::bool) t::'A::type. COND b t t = t"
obua@17644
   116
  by (import hollight COND_ID)
obua@17644
   117
obua@17644
   118
lemma COND_RAND: "ALL (b::bool) (f::'A::type => 'B::type) (x::'A::type) y::'A::type.
obua@17644
   119
   f (COND b x y) = COND b (f x) (f y)"
obua@17644
   120
  by (import hollight COND_RAND)
obua@17644
   121
obua@17644
   122
lemma COND_RATOR: "ALL (b::bool) (f::'A::type => 'B::type) (g::'A::type => 'B::type)
obua@17644
   123
   x::'A::type. COND b f g x = COND b (f x) (g x)"
obua@17644
   124
  by (import hollight COND_RATOR)
obua@17644
   125
obua@17644
   126
lemma COND_ABS: "ALL (b::bool) (f::'A::type => 'B::type) g::'A::type => 'B::type.
obua@17644
   127
   (%x::'A::type. COND b (f x) (g x)) = COND b f g"
obua@17644
   128
  by (import hollight COND_ABS)
obua@17644
   129
obua@17644
   130
lemma MONO_COND: "((A::bool) --> (B::bool)) & ((C::bool) --> (D::bool)) -->
obua@17644
   131
COND (b::bool) A C --> COND b B D"
obua@17644
   132
  by (import hollight MONO_COND)
obua@17644
   133
obua@17644
   134
lemma COND_ELIM_THM: "(P::'A::type => bool) (COND (c::bool) (x::'A::type) (y::'A::type)) =
obua@17644
   135
((c --> P x) & (~ c --> P y))"
obua@17644
   136
  by (import hollight COND_ELIM_THM)
obua@17644
   137
obua@17644
   138
lemma SKOLEM_THM: "ALL P::'A::type => 'B::type => bool.
obua@17644
   139
   (ALL x::'A::type. Ex (P x)) =
obua@17644
   140
   (EX x::'A::type => 'B::type. ALL xa::'A::type. P xa (x xa))"
obua@17644
   141
  by (import hollight SKOLEM_THM)
obua@17644
   142
obua@17644
   143
lemma UNIQUE_SKOLEM_ALT: "ALL P::'A::type => 'B::type => bool.
obua@17644
   144
   (ALL x::'A::type. Ex1 (P x)) =
obua@17644
   145
   (EX f::'A::type => 'B::type.
obua@17644
   146
       ALL (x::'A::type) y::'B::type. P x y = (f x = y))"
obua@17644
   147
  by (import hollight UNIQUE_SKOLEM_ALT)
obua@17644
   148
obua@17644
   149
lemma COND_EQ_CLAUSE: "COND ((x::'q_3000::type) = x) (y::'q_2993::type) (z::'q_2993::type) = y"
obua@17644
   150
  by (import hollight COND_EQ_CLAUSE)
obua@17644
   151
obua@17644
   152
lemma o_ASSOC: "ALL (f::'C::type => 'D::type) (g::'B::type => 'C::type)
obua@17644
   153
   h::'A::type => 'B::type. f o (g o h) = f o g o h"
obua@17644
   154
  by (import hollight o_ASSOC)
obua@17644
   155
obua@17644
   156
lemma I_O_ID: "ALL f::'A::type => 'B::type. id o f = f & f o id = f"
obua@17644
   157
  by (import hollight I_O_ID)
obua@17644
   158
obua@17644
   159
lemma EXISTS_ONE_REP: "EX x::bool. x"
obua@17644
   160
  by (import hollight EXISTS_ONE_REP)
obua@17644
   161
obua@17644
   162
lemma one_axiom: "ALL f::'A::type => unit. All (op = f)"
obua@17644
   163
  by (import hollight one_axiom)
obua@17644
   164
obua@17644
   165
lemma one_RECURSION: "ALL e::'A::type. EX x::unit => 'A::type. x () = e"
obua@17644
   166
  by (import hollight one_RECURSION)
obua@17644
   167
obua@17644
   168
lemma one_Axiom: "ALL e::'A::type. EX! fn::unit => 'A::type. fn () = e"
obua@17644
   169
  by (import hollight one_Axiom)
obua@17644
   170
obua@17644
   171
lemma th_cond: "(P::'A::type => bool => bool) (COND (b::bool) (x::'A::type) (y::'A::type))
obua@17644
   172
 b =
obua@17644
   173
(b & P x True | ~ b & P y False)"
obua@17644
   174
  by (import hollight th_cond)
obua@17644
   175
obua@17644
   176
constdefs
obua@17652
   177
  LET_END :: "'A => 'A" 
obua@17644
   178
  "LET_END == %t::'A::type. t"
obua@17644
   179
obua@17644
   180
lemma DEF_LET_END: "LET_END = (%t::'A::type. t)"
obua@17644
   181
  by (import hollight DEF_LET_END)
obua@17644
   182
obua@17644
   183
constdefs
obua@17652
   184
  GABS :: "('A => bool) => 'A" 
obua@17644
   185
  "(op ==::(('A::type => bool) => 'A::type)
obua@17644
   186
        => (('A::type => bool) => 'A::type) => prop)
obua@17644
   187
 (GABS::('A::type => bool) => 'A::type)
obua@17644
   188
 (Eps::('A::type => bool) => 'A::type)"
obua@17644
   189
obua@17644
   190
lemma DEF_GABS: "(op =::(('A::type => bool) => 'A::type)
obua@17644
   191
       => (('A::type => bool) => 'A::type) => bool)
obua@17644
   192
 (GABS::('A::type => bool) => 'A::type)
obua@17644
   193
 (Eps::('A::type => bool) => 'A::type)"
obua@17644
   194
  by (import hollight DEF_GABS)
obua@17644
   195
obua@17644
   196
constdefs
obua@17652
   197
  GEQ :: "'A => 'A => bool" 
obua@17644
   198
  "(op ==::('A::type => 'A::type => bool)
obua@17644
   199
        => ('A::type => 'A::type => bool) => prop)
obua@17644
   200
 (GEQ::'A::type => 'A::type => bool) (op =::'A::type => 'A::type => bool)"
obua@17644
   201
obua@17644
   202
lemma DEF_GEQ: "(op =::('A::type => 'A::type => bool)
obua@17644
   203
       => ('A::type => 'A::type => bool) => bool)
obua@17644
   204
 (GEQ::'A::type => 'A::type => bool) (op =::'A::type => 'A::type => bool)"
obua@17644
   205
  by (import hollight DEF_GEQ)
obua@17644
   206
obua@17644
   207
lemma PAIR_EXISTS_THM: "EX (x::'A::type => 'B::type => bool) (a::'A::type) b::'B::type.
obua@17644
   208
   x = Pair_Rep a b"
obua@17644
   209
  by (import hollight PAIR_EXISTS_THM)
obua@17644
   210
obua@17644
   211
constdefs
obua@17652
   212
  CURRY :: "('A * 'B => 'C) => 'A => 'B => 'C" 
obua@17644
   213
  "CURRY ==
obua@17644
   214
%(u::'A::type * 'B::type => 'C::type) (ua::'A::type) ub::'B::type.
obua@17644
   215
   u (ua, ub)"
obua@17644
   216
obua@17644
   217
lemma DEF_CURRY: "CURRY =
obua@17644
   218
(%(u::'A::type * 'B::type => 'C::type) (ua::'A::type) ub::'B::type.
obua@17644
   219
    u (ua, ub))"
obua@17644
   220
  by (import hollight DEF_CURRY)
obua@17644
   221
obua@17644
   222
constdefs
obua@17652
   223
  UNCURRY :: "('A => 'B => 'C) => 'A * 'B => 'C" 
obua@17644
   224
  "UNCURRY ==
obua@17644
   225
%(u::'A::type => 'B::type => 'C::type) ua::'A::type * 'B::type.
obua@17644
   226
   u (fst ua) (snd ua)"
obua@17644
   227
obua@17644
   228
lemma DEF_UNCURRY: "UNCURRY =
obua@17644
   229
(%(u::'A::type => 'B::type => 'C::type) ua::'A::type * 'B::type.
obua@17644
   230
    u (fst ua) (snd ua))"
obua@17644
   231
  by (import hollight DEF_UNCURRY)
obua@17644
   232
obua@17644
   233
constdefs
obua@17652
   234
  PASSOC :: "(('A * 'B) * 'C => 'D) => 'A * 'B * 'C => 'D" 
obua@17644
   235
  "PASSOC ==
obua@17644
   236
%(u::('A::type * 'B::type) * 'C::type => 'D::type)
obua@17644
   237
   ua::'A::type * 'B::type * 'C::type.
obua@17644
   238
   u ((fst ua, fst (snd ua)), snd (snd ua))"
obua@17644
   239
obua@17644
   240
lemma DEF_PASSOC: "PASSOC =
obua@17644
   241
(%(u::('A::type * 'B::type) * 'C::type => 'D::type)
obua@17644
   242
    ua::'A::type * 'B::type * 'C::type.
obua@17644
   243
    u ((fst ua, fst (snd ua)), snd (snd ua)))"
obua@17644
   244
  by (import hollight DEF_PASSOC)
obua@17644
   245
obua@17644
   246
lemma num_Axiom: "ALL (e::'A::type) f::'A::type => nat => 'A::type.
obua@17652
   247
   EX! fn::nat => 'A::type. fn 0 = e & (ALL n::nat. fn (Suc n) = f (fn n) n)"
obua@17644
   248
  by (import hollight num_Axiom)
obua@17644
   249
obua@17652
   250
lemma ADD_CLAUSES: "(ALL x::nat. 0 + x = x) &
obua@17652
   251
(ALL x::nat. x + 0 = x) &
obua@17644
   252
(ALL (x::nat) xa::nat. Suc x + xa = Suc (x + xa)) &
obua@17644
   253
(ALL (x::nat) xa::nat. x + Suc xa = Suc (x + xa))"
obua@17644
   254
  by (import hollight ADD_CLAUSES)
obua@17644
   255
obua@17644
   256
lemma ADD_AC: "(m::nat) + (n::nat) = n + m &
obua@17644
   257
m + n + (p::nat) = m + (n + p) & m + (n + p) = n + (m + p)"
obua@17644
   258
  by (import hollight ADD_AC)
obua@17644
   259
obua@17652
   260
lemma EQ_ADD_LCANCEL_0: "ALL (m::nat) n::nat. (m + n = m) = (n = 0)"
obua@17644
   261
  by (import hollight EQ_ADD_LCANCEL_0)
obua@17644
   262
obua@17652
   263
lemma EQ_ADD_RCANCEL_0: "ALL (x::nat) xa::nat. (x + xa = xa) = (x = 0)"
obua@17644
   264
  by (import hollight EQ_ADD_RCANCEL_0)
obua@17644
   265
obua@17652
   266
lemma ONE: "NUMERAL_BIT1 0 = Suc 0"
obua@17644
   267
  by (import hollight ONE)
obua@17644
   268
obua@17652
   269
lemma TWO: "NUMERAL_BIT0 (NUMERAL_BIT1 0) = Suc (NUMERAL_BIT1 0)"
obua@17644
   270
  by (import hollight TWO)
obua@17644
   271
obua@17652
   272
lemma ADD1: "ALL x::nat. Suc x = x + NUMERAL_BIT1 0"
obua@17644
   273
  by (import hollight ADD1)
obua@17644
   274
obua@17652
   275
lemma MULT_CLAUSES: "(ALL x::nat. 0 * x = 0) &
obua@17652
   276
(ALL x::nat. x * 0 = 0) &
obua@17652
   277
(ALL x::nat. NUMERAL_BIT1 0 * x = x) &
obua@17652
   278
(ALL x::nat. x * NUMERAL_BIT1 0 = x) &
obua@17644
   279
(ALL (x::nat) xa::nat. Suc x * xa = x * xa + xa) &
obua@17644
   280
(ALL (x::nat) xa::nat. x * Suc xa = x + x * xa)"
obua@17644
   281
  by (import hollight MULT_CLAUSES)
obua@17644
   282
obua@17644
   283
lemma MULT_AC: "(m::nat) * (n::nat) = n * m &
obua@17644
   284
m * n * (p::nat) = m * (n * p) & m * (n * p) = n * (m * p)"
obua@17644
   285
  by (import hollight MULT_AC)
obua@17644
   286
obua@17652
   287
lemma MULT_2: "ALL n::nat. NUMERAL_BIT0 (NUMERAL_BIT1 0) * n = n + n"
obua@17644
   288
  by (import hollight MULT_2)
obua@17644
   289
obua@17644
   290
lemma MULT_EQ_1: "ALL (m::nat) n::nat.
obua@17652
   291
   (m * n = NUMERAL_BIT1 0) = (m = NUMERAL_BIT1 0 & n = NUMERAL_BIT1 0)"
obua@17644
   292
  by (import hollight MULT_EQ_1)
obua@17644
   293
obua@17644
   294
constdefs
obua@17644
   295
  EXP :: "nat => nat => nat" 
obua@17644
   296
  "EXP ==
obua@17644
   297
SOME EXP::nat => nat => nat.
obua@17652
   298
   (ALL m::nat. EXP m 0 = NUMERAL_BIT1 0) &
obua@17644
   299
   (ALL (m::nat) n::nat. EXP m (Suc n) = m * EXP m n)"
obua@17644
   300
obua@17644
   301
lemma DEF_EXP: "EXP =
obua@17644
   302
(SOME EXP::nat => nat => nat.
obua@17652
   303
    (ALL m::nat. EXP m 0 = NUMERAL_BIT1 0) &
obua@17644
   304
    (ALL (m::nat) n::nat. EXP m (Suc n) = m * EXP m n))"
obua@17644
   305
  by (import hollight DEF_EXP)
obua@17644
   306
obua@17652
   307
lemma EXP_EQ_0: "ALL (m::nat) n::nat. (EXP m n = 0) = (m = 0 & n ~= 0)"
obua@17644
   308
  by (import hollight EXP_EQ_0)
obua@17644
   309
obua@17644
   310
lemma EXP_ADD: "ALL (m::nat) (n::nat) p::nat. EXP m (n + p) = EXP m n * EXP m p"
obua@17644
   311
  by (import hollight EXP_ADD)
obua@17644
   312
obua@17652
   313
lemma EXP_ONE: "ALL n::nat. EXP (NUMERAL_BIT1 0) n = NUMERAL_BIT1 0"
obua@17644
   314
  by (import hollight EXP_ONE)
obua@17644
   315
obua@17652
   316
lemma EXP_1: "ALL x::nat. EXP x (NUMERAL_BIT1 0) = x"
obua@17644
   317
  by (import hollight EXP_1)
obua@17644
   318
obua@17652
   319
lemma EXP_2: "ALL x::nat. EXP x (NUMERAL_BIT0 (NUMERAL_BIT1 0)) = x * x"
obua@17644
   320
  by (import hollight EXP_2)
obua@17644
   321
obua@17644
   322
lemma MULT_EXP: "ALL (p::nat) (m::nat) n::nat. EXP (m * n) p = EXP m p * EXP n p"
obua@17644
   323
  by (import hollight MULT_EXP)
obua@17644
   324
obua@17644
   325
lemma EXP_MULT: "ALL (m::nat) (n::nat) p::nat. EXP m (n * p) = EXP (EXP m n) p"
obua@17644
   326
  by (import hollight EXP_MULT)
obua@17644
   327
obua@17644
   328
consts
obua@17644
   329
  "<=" :: "nat => nat => bool" ("<=")
obua@17644
   330
obua@17644
   331
defs
obua@17644
   332
  "<=_def": "<= ==
obua@17644
   333
SOME u::nat => nat => bool.
obua@17652
   334
   (ALL m::nat. u m 0 = (m = 0)) &
obua@17644
   335
   (ALL (m::nat) n::nat. u m (Suc n) = (m = Suc n | u m n))"
obua@17644
   336
obua@17644
   337
lemma DEF__lessthan__equal_: "<= =
obua@17644
   338
(SOME u::nat => nat => bool.
obua@17652
   339
    (ALL m::nat. u m 0 = (m = 0)) &
obua@17644
   340
    (ALL (m::nat) n::nat. u m (Suc n) = (m = Suc n | u m n)))"
obua@17644
   341
  by (import hollight DEF__lessthan__equal_)
obua@17644
   342
obua@17644
   343
consts
obua@17644
   344
  "<" :: "nat => nat => bool" ("<")
obua@17644
   345
obua@17644
   346
defs
obua@17644
   347
  "<_def": "< ==
obua@17644
   348
SOME u::nat => nat => bool.
obua@17652
   349
   (ALL m::nat. u m 0 = False) &
obua@17644
   350
   (ALL (m::nat) n::nat. u m (Suc n) = (m = n | u m n))"
obua@17644
   351
obua@17644
   352
lemma DEF__lessthan_: "< =
obua@17644
   353
(SOME u::nat => nat => bool.
obua@17652
   354
    (ALL m::nat. u m 0 = False) &
obua@17644
   355
    (ALL (m::nat) n::nat. u m (Suc n) = (m = n | u m n)))"
obua@17644
   356
  by (import hollight DEF__lessthan_)
obua@17644
   357
obua@17644
   358
consts
obua@17644
   359
  ">=" :: "nat => nat => bool" (">=")
obua@17644
   360
obua@17644
   361
defs
obua@17644
   362
  ">=_def": ">= == %(u::nat) ua::nat. <= ua u"
obua@17644
   363
obua@17644
   364
lemma DEF__greaterthan__equal_: ">= = (%(u::nat) ua::nat. <= ua u)"
obua@17644
   365
  by (import hollight DEF__greaterthan__equal_)
obua@17644
   366
obua@17644
   367
consts
obua@17644
   368
  ">" :: "nat => nat => bool" (">")
obua@17644
   369
obua@17644
   370
defs
obua@17644
   371
  ">_def": "> == %(u::nat) ua::nat. < ua u"
obua@17644
   372
obua@17644
   373
lemma DEF__greaterthan_: "> = (%(u::nat) ua::nat. < ua u)"
obua@17644
   374
  by (import hollight DEF__greaterthan_)
obua@17644
   375
obua@17644
   376
lemma LE_SUC_LT: "ALL (m::nat) n::nat. <= (Suc m) n = < m n"
obua@17644
   377
  by (import hollight LE_SUC_LT)
obua@17644
   378
obua@17644
   379
lemma LT_SUC_LE: "ALL (m::nat) n::nat. < m (Suc n) = <= m n"
obua@17644
   380
  by (import hollight LT_SUC_LE)
obua@17644
   381
obua@17644
   382
lemma LE_SUC: "ALL (x::nat) xa::nat. <= (Suc x) (Suc xa) = <= x xa"
obua@17644
   383
  by (import hollight LE_SUC)
obua@17644
   384
obua@17644
   385
lemma LT_SUC: "ALL (x::nat) xa::nat. < (Suc x) (Suc xa) = < x xa"
obua@17644
   386
  by (import hollight LT_SUC)
obua@17644
   387
obua@17652
   388
lemma LE_0: "All (<= 0)"
obua@17644
   389
  by (import hollight LE_0)
obua@17644
   390
obua@17652
   391
lemma LT_0: "ALL x::nat. < 0 (Suc x)"
obua@17644
   392
  by (import hollight LT_0)
obua@17644
   393
obua@17644
   394
lemma LE_REFL: "ALL n::nat. <= n n"
obua@17644
   395
  by (import hollight LE_REFL)
obua@17644
   396
obua@17644
   397
lemma LT_REFL: "ALL n::nat. ~ < n n"
obua@17644
   398
  by (import hollight LT_REFL)
obua@17644
   399
obua@17644
   400
lemma LE_ANTISYM: "ALL (m::nat) n::nat. (<= m n & <= n m) = (m = n)"
obua@17644
   401
  by (import hollight LE_ANTISYM)
obua@17644
   402
obua@17644
   403
lemma LT_ANTISYM: "ALL (m::nat) n::nat. ~ (< m n & < n m)"
obua@17644
   404
  by (import hollight LT_ANTISYM)
obua@17644
   405
obua@17644
   406
lemma LET_ANTISYM: "ALL (m::nat) n::nat. ~ (<= m n & < n m)"
obua@17644
   407
  by (import hollight LET_ANTISYM)
obua@17644
   408
obua@17644
   409
lemma LTE_ANTISYM: "ALL (x::nat) xa::nat. ~ (< x xa & <= xa x)"
obua@17644
   410
  by (import hollight LTE_ANTISYM)
obua@17644
   411
obua@17644
   412
lemma LE_TRANS: "ALL (m::nat) (n::nat) p::nat. <= m n & <= n p --> <= m p"
obua@17644
   413
  by (import hollight LE_TRANS)
obua@17644
   414
obua@17644
   415
lemma LT_TRANS: "ALL (m::nat) (n::nat) p::nat. < m n & < n p --> < m p"
obua@17644
   416
  by (import hollight LT_TRANS)
obua@17644
   417
obua@17644
   418
lemma LET_TRANS: "ALL (m::nat) (n::nat) p::nat. <= m n & < n p --> < m p"
obua@17644
   419
  by (import hollight LET_TRANS)
obua@17644
   420
obua@17644
   421
lemma LTE_TRANS: "ALL (m::nat) (n::nat) p::nat. < m n & <= n p --> < m p"
obua@17644
   422
  by (import hollight LTE_TRANS)
obua@17644
   423
obua@17644
   424
lemma LE_CASES: "ALL (m::nat) n::nat. <= m n | <= n m"
obua@17644
   425
  by (import hollight LE_CASES)
obua@17644
   426
obua@17644
   427
lemma LT_CASES: "ALL (m::nat) n::nat. < m n | < n m | m = n"
obua@17644
   428
  by (import hollight LT_CASES)
obua@17644
   429
obua@17644
   430
lemma LET_CASES: "ALL (m::nat) n::nat. <= m n | < n m"
obua@17644
   431
  by (import hollight LET_CASES)
obua@17644
   432
obua@17644
   433
lemma LTE_CASES: "ALL (x::nat) xa::nat. < x xa | <= xa x"
obua@17644
   434
  by (import hollight LTE_CASES)
obua@17644
   435
obua@17652
   436
lemma LT_NZ: "ALL n::nat. < 0 n = (n ~= 0)"
obua@17644
   437
  by (import hollight LT_NZ)
obua@17644
   438
obua@17644
   439
lemma LE_LT: "ALL (m::nat) n::nat. <= m n = (< m n | m = n)"
obua@17644
   440
  by (import hollight LE_LT)
obua@17644
   441
obua@17644
   442
lemma LT_LE: "ALL (x::nat) xa::nat. < x xa = (<= x xa & x ~= xa)"
obua@17644
   443
  by (import hollight LT_LE)
obua@17644
   444
obua@17644
   445
lemma NOT_LE: "ALL (m::nat) n::nat. (~ <= m n) = < n m"
obua@17644
   446
  by (import hollight NOT_LE)
obua@17644
   447
obua@17644
   448
lemma NOT_LT: "ALL (m::nat) n::nat. (~ < m n) = <= n m"
obua@17644
   449
  by (import hollight NOT_LT)
obua@17644
   450
obua@17644
   451
lemma LT_IMP_LE: "ALL (x::nat) xa::nat. < x xa --> <= x xa"
obua@17644
   452
  by (import hollight LT_IMP_LE)
obua@17644
   453
obua@17644
   454
lemma EQ_IMP_LE: "ALL (m::nat) n::nat. m = n --> <= m n"
obua@17644
   455
  by (import hollight EQ_IMP_LE)
obua@17644
   456
obua@17644
   457
lemma LE_EXISTS: "ALL (m::nat) n::nat. <= m n = (EX d::nat. n = m + d)"
obua@17644
   458
  by (import hollight LE_EXISTS)
obua@17644
   459
obua@17644
   460
lemma LT_EXISTS: "ALL (m::nat) n::nat. < m n = (EX d::nat. n = m + Suc d)"
obua@17644
   461
  by (import hollight LT_EXISTS)
obua@17644
   462
obua@17644
   463
lemma LE_ADD: "ALL (m::nat) n::nat. <= m (m + n)"
obua@17644
   464
  by (import hollight LE_ADD)
obua@17644
   465
obua@17644
   466
lemma LE_ADDR: "ALL (x::nat) xa::nat. <= xa (x + xa)"
obua@17644
   467
  by (import hollight LE_ADDR)
obua@17644
   468
obua@17652
   469
lemma LT_ADD: "ALL (m::nat) n::nat. < m (m + n) = < 0 n"
obua@17644
   470
  by (import hollight LT_ADD)
obua@17644
   471
obua@17652
   472
lemma LT_ADDR: "ALL (x::nat) xa::nat. < xa (x + xa) = < 0 x"
obua@17644
   473
  by (import hollight LT_ADDR)
obua@17644
   474
obua@17644
   475
lemma LE_ADD_LCANCEL: "ALL (x::nat) (xa::nat) xb::nat. <= (x + xa) (x + xb) = <= xa xb"
obua@17644
   476
  by (import hollight LE_ADD_LCANCEL)
obua@17644
   477
obua@17644
   478
lemma LE_ADD_RCANCEL: "ALL (x::nat) (xa::nat) xb::nat. <= (x + xb) (xa + xb) = <= x xa"
obua@17644
   479
  by (import hollight LE_ADD_RCANCEL)
obua@17644
   480
obua@17644
   481
lemma LT_ADD_LCANCEL: "ALL (x::nat) (xa::nat) xb::nat. < (x + xa) (x + xb) = < xa xb"
obua@17644
   482
  by (import hollight LT_ADD_LCANCEL)
obua@17644
   483
obua@17644
   484
lemma LT_ADD_RCANCEL: "ALL (x::nat) (xa::nat) xb::nat. < (x + xb) (xa + xb) = < x xa"
obua@17644
   485
  by (import hollight LT_ADD_RCANCEL)
obua@17644
   486
obua@17644
   487
lemma LE_ADD2: "ALL (m::nat) (n::nat) (p::nat) q::nat.
obua@17644
   488
   <= m p & <= n q --> <= (m + n) (p + q)"
obua@17644
   489
  by (import hollight LE_ADD2)
obua@17644
   490
obua@17644
   491
lemma LET_ADD2: "ALL (m::nat) (n::nat) (p::nat) q::nat. <= m p & < n q --> < (m + n) (p + q)"
obua@17644
   492
  by (import hollight LET_ADD2)
obua@17644
   493
obua@17644
   494
lemma LTE_ADD2: "ALL (x::nat) (xa::nat) (xb::nat) xc::nat.
obua@17644
   495
   < x xb & <= xa xc --> < (x + xa) (xb + xc)"
obua@17644
   496
  by (import hollight LTE_ADD2)
obua@17644
   497
obua@17644
   498
lemma LT_ADD2: "ALL (m::nat) (n::nat) (p::nat) q::nat. < m p & < n q --> < (m + n) (p + q)"
obua@17644
   499
  by (import hollight LT_ADD2)
obua@17644
   500
obua@17652
   501
lemma LT_MULT: "ALL (m::nat) n::nat. < 0 (m * n) = (< 0 m & < 0 n)"
obua@17644
   502
  by (import hollight LT_MULT)
obua@17644
   503
obua@17644
   504
lemma LE_MULT2: "ALL (m::nat) (n::nat) (p::nat) q::nat.
obua@17644
   505
   <= m n & <= p q --> <= (m * p) (n * q)"
obua@17644
   506
  by (import hollight LE_MULT2)
obua@17644
   507
obua@17652
   508
lemma LT_LMULT: "ALL (m::nat) (n::nat) p::nat. m ~= 0 & < n p --> < (m * n) (m * p)"
obua@17644
   509
  by (import hollight LT_LMULT)
obua@17644
   510
obua@17652
   511
lemma LE_MULT_LCANCEL: "ALL (m::nat) (n::nat) p::nat. <= (m * n) (m * p) = (m = 0 | <= n p)"
obua@17644
   512
  by (import hollight LE_MULT_LCANCEL)
obua@17644
   513
obua@17652
   514
lemma LE_MULT_RCANCEL: "ALL (x::nat) (xa::nat) xb::nat. <= (x * xb) (xa * xb) = (<= x xa | xb = 0)"
obua@17644
   515
  by (import hollight LE_MULT_RCANCEL)
obua@17644
   516
obua@17652
   517
lemma LT_MULT_LCANCEL: "ALL (m::nat) (n::nat) p::nat. < (m * n) (m * p) = (m ~= 0 & < n p)"
obua@17644
   518
  by (import hollight LT_MULT_LCANCEL)
obua@17644
   519
obua@17652
   520
lemma LT_MULT_RCANCEL: "ALL (x::nat) (xa::nat) xb::nat. < (x * xb) (xa * xb) = (< x xa & xb ~= 0)"
obua@17644
   521
  by (import hollight LT_MULT_RCANCEL)
obua@17644
   522
obua@17644
   523
lemma LT_MULT2: "ALL (m::nat) (n::nat) (p::nat) q::nat. < m n & < p q --> < (m * p) (n * q)"
obua@17644
   524
  by (import hollight LT_MULT2)
obua@17644
   525
obua@17644
   526
lemma LE_SQUARE_REFL: "ALL n::nat. <= n (n * n)"
obua@17644
   527
  by (import hollight LE_SQUARE_REFL)
obua@17644
   528
obua@17644
   529
lemma WLOG_LE: "(ALL (m::nat) n::nat. (P::nat => nat => bool) m n = P n m) &
obua@17644
   530
(ALL (m::nat) n::nat. <= m n --> P m n) -->
obua@17644
   531
(ALL m::nat. All (P m))"
obua@17644
   532
  by (import hollight WLOG_LE)
obua@17644
   533
obua@17644
   534
lemma WLOG_LT: "(ALL m::nat. (P::nat => nat => bool) m m) &
obua@17644
   535
(ALL (m::nat) n::nat. P m n = P n m) &
obua@17644
   536
(ALL (m::nat) n::nat. < m n --> P m n) -->
obua@17644
   537
(ALL m::nat. All (P m))"
obua@17644
   538
  by (import hollight WLOG_LT)
obua@17644
   539
obua@17644
   540
lemma num_WF: "ALL P::nat => bool.
obua@17644
   541
   (ALL n::nat. (ALL m::nat. < m n --> P m) --> P n) --> All P"
obua@17644
   542
  by (import hollight num_WF)
obua@17644
   543
obua@17644
   544
lemma num_WOP: "ALL P::nat => bool. Ex P = (EX n::nat. P n & (ALL m::nat. < m n --> ~ P m))"
obua@17644
   545
  by (import hollight num_WOP)
obua@17644
   546
obua@17644
   547
lemma num_MAX: "ALL P::nat => bool.
obua@17644
   548
   (Ex P & (EX M::nat. ALL x::nat. P x --> <= x M)) =
obua@17644
   549
   (EX m::nat. P m & (ALL x::nat. P x --> <= x m))"
obua@17644
   550
  by (import hollight num_MAX)
obua@17644
   551
obua@17644
   552
constdefs
obua@17644
   553
  EVEN :: "nat => bool" 
obua@17644
   554
  "EVEN ==
obua@17644
   555
SOME EVEN::nat => bool.
obua@17652
   556
   EVEN 0 = True & (ALL n::nat. EVEN (Suc n) = (~ EVEN n))"
obua@17644
   557
obua@17644
   558
lemma DEF_EVEN: "EVEN =
obua@17644
   559
(SOME EVEN::nat => bool.
obua@17652
   560
    EVEN 0 = True & (ALL n::nat. EVEN (Suc n) = (~ EVEN n)))"
obua@17644
   561
  by (import hollight DEF_EVEN)
obua@17644
   562
obua@17644
   563
constdefs
obua@17644
   564
  ODD :: "nat => bool" 
obua@17644
   565
  "ODD ==
obua@17652
   566
SOME ODD::nat => bool. ODD 0 = False & (ALL n::nat. ODD (Suc n) = (~ ODD n))"
obua@17644
   567
obua@17644
   568
lemma DEF_ODD: "ODD =
obua@17644
   569
(SOME ODD::nat => bool.
obua@17652
   570
    ODD 0 = False & (ALL n::nat. ODD (Suc n) = (~ ODD n)))"
obua@17644
   571
  by (import hollight DEF_ODD)
obua@17644
   572
obua@17644
   573
lemma NOT_EVEN: "ALL n::nat. (~ EVEN n) = ODD n"
obua@17644
   574
  by (import hollight NOT_EVEN)
obua@17644
   575
obua@17644
   576
lemma NOT_ODD: "ALL n::nat. (~ ODD n) = EVEN n"
obua@17644
   577
  by (import hollight NOT_ODD)
obua@17644
   578
obua@17644
   579
lemma EVEN_OR_ODD: "ALL n::nat. EVEN n | ODD n"
obua@17644
   580
  by (import hollight EVEN_OR_ODD)
obua@17644
   581
obua@17644
   582
lemma EVEN_AND_ODD: "ALL x::nat. ~ (EVEN x & ODD x)"
obua@17644
   583
  by (import hollight EVEN_AND_ODD)
obua@17644
   584
obua@17644
   585
lemma EVEN_ADD: "ALL (m::nat) n::nat. EVEN (m + n) = (EVEN m = EVEN n)"
obua@17644
   586
  by (import hollight EVEN_ADD)
obua@17644
   587
obua@17644
   588
lemma EVEN_MULT: "ALL (m::nat) n::nat. EVEN (m * n) = (EVEN m | EVEN n)"
obua@17644
   589
  by (import hollight EVEN_MULT)
obua@17644
   590
obua@17652
   591
lemma EVEN_EXP: "ALL (m::nat) n::nat. EVEN (EXP m n) = (EVEN m & n ~= 0)"
obua@17644
   592
  by (import hollight EVEN_EXP)
obua@17644
   593
obua@17644
   594
lemma ODD_ADD: "ALL (m::nat) n::nat. ODD (m + n) = (ODD m ~= ODD n)"
obua@17644
   595
  by (import hollight ODD_ADD)
obua@17644
   596
obua@17644
   597
lemma ODD_MULT: "ALL (m::nat) n::nat. ODD (m * n) = (ODD m & ODD n)"
obua@17644
   598
  by (import hollight ODD_MULT)
obua@17644
   599
obua@17652
   600
lemma ODD_EXP: "ALL (m::nat) n::nat. ODD (EXP m n) = (ODD m | n = 0)"
obua@17644
   601
  by (import hollight ODD_EXP)
obua@17644
   602
obua@17652
   603
lemma EVEN_DOUBLE: "ALL n::nat. EVEN (NUMERAL_BIT0 (NUMERAL_BIT1 0) * n)"
obua@17644
   604
  by (import hollight EVEN_DOUBLE)
obua@17644
   605
obua@17652
   606
lemma ODD_DOUBLE: "ALL x::nat. ODD (Suc (NUMERAL_BIT0 (NUMERAL_BIT1 0) * x))"
obua@17644
   607
  by (import hollight ODD_DOUBLE)
obua@17644
   608
obua@17644
   609
lemma EVEN_EXISTS_LEMMA: "ALL n::nat.
obua@17652
   610
   (EVEN n --> (EX m::nat. n = NUMERAL_BIT0 (NUMERAL_BIT1 0) * m)) &
obua@17652
   611
   (~ EVEN n --> (EX m::nat. n = Suc (NUMERAL_BIT0 (NUMERAL_BIT1 0) * m)))"
obua@17644
   612
  by (import hollight EVEN_EXISTS_LEMMA)
obua@17644
   613
obua@17652
   614
lemma EVEN_EXISTS: "ALL n::nat. EVEN n = (EX m::nat. n = NUMERAL_BIT0 (NUMERAL_BIT1 0) * m)"
obua@17644
   615
  by (import hollight EVEN_EXISTS)
obua@17644
   616
obua@17652
   617
lemma ODD_EXISTS: "ALL n::nat. ODD n = (EX m::nat. n = Suc (NUMERAL_BIT0 (NUMERAL_BIT1 0) * m))"
obua@17644
   618
  by (import hollight ODD_EXISTS)
obua@17644
   619
obua@17644
   620
lemma EVEN_ODD_DECOMPOSITION: "ALL n::nat.
obua@17644
   621
   (EX (k::nat) m::nat.
obua@17652
   622
       ODD m & n = EXP (NUMERAL_BIT0 (NUMERAL_BIT1 0)) k * m) =
obua@17652
   623
   (n ~= 0)"
obua@17644
   624
  by (import hollight EVEN_ODD_DECOMPOSITION)
obua@17644
   625
obua@17652
   626
lemma SUB_0: "ALL x::nat. 0 - x = 0 & x - 0 = x"
obua@17644
   627
  by (import hollight SUB_0)
obua@17644
   628
obua@17644
   629
lemma SUB_PRESUC: "ALL (m::nat) n::nat. Pred (Suc m - n) = m - n"
obua@17644
   630
  by (import hollight SUB_PRESUC)
obua@17644
   631
obua@17652
   632
lemma SUB_EQ_0: "ALL (m::nat) n::nat. (m - n = 0) = <= m n"
obua@17644
   633
  by (import hollight SUB_EQ_0)
obua@17644
   634
obua@17652
   635
lemma ADD_SUBR: "ALL (x::nat) xa::nat. xa - (x + xa) = 0"
obua@17644
   636
  by (import hollight ADD_SUBR)
obua@17644
   637
obua@17644
   638
lemma SUB_ADD: "ALL (x::nat) xa::nat. <= xa x --> x - xa + xa = x"
obua@17644
   639
  by (import hollight SUB_ADD)
obua@17644
   640
obua@17652
   641
lemma SUC_SUB1: "ALL x::nat. Suc x - NUMERAL_BIT1 0 = x"
obua@17644
   642
  by (import hollight SUC_SUB1)
obua@17644
   643
obua@17644
   644
constdefs
obua@17644
   645
  FACT :: "nat => nat" 
obua@17644
   646
  "FACT ==
obua@17644
   647
SOME FACT::nat => nat.
obua@17652
   648
   FACT 0 = NUMERAL_BIT1 0 & (ALL n::nat. FACT (Suc n) = Suc n * FACT n)"
obua@17644
   649
obua@17644
   650
lemma DEF_FACT: "FACT =
obua@17644
   651
(SOME FACT::nat => nat.
obua@17652
   652
    FACT 0 = NUMERAL_BIT1 0 & (ALL n::nat. FACT (Suc n) = Suc n * FACT n))"
obua@17644
   653
  by (import hollight DEF_FACT)
obua@17644
   654
obua@17652
   655
lemma FACT_LT: "ALL n::nat. < 0 (FACT n)"
obua@17644
   656
  by (import hollight FACT_LT)
obua@17644
   657
obua@17652
   658
lemma FACT_LE: "ALL x::nat. <= (NUMERAL_BIT1 0) (FACT x)"
obua@17644
   659
  by (import hollight FACT_LE)
obua@17644
   660
obua@17644
   661
lemma FACT_MONO: "ALL (m::nat) n::nat. <= m n --> <= (FACT m) (FACT n)"
obua@17644
   662
  by (import hollight FACT_MONO)
obua@17644
   663
obua@17652
   664
lemma DIVMOD_EXIST: "ALL (m::nat) n::nat. n ~= 0 --> (EX (q::nat) r::nat. m = q * n + r & < r n)"
obua@17644
   665
  by (import hollight DIVMOD_EXIST)
obua@17644
   666
obua@17644
   667
lemma DIVMOD_EXIST_0: "ALL (m::nat) n::nat.
obua@17644
   668
   EX (x::nat) xa::nat.
obua@17652
   669
      COND (n = 0) (x = 0 & xa = 0) (m = x * n + xa & < xa n)"
obua@17644
   670
  by (import hollight DIVMOD_EXIST_0)
obua@17644
   671
obua@17644
   672
constdefs
obua@17644
   673
  DIV :: "nat => nat => nat" 
obua@17644
   674
  "DIV ==
obua@17644
   675
SOME q::nat => nat => nat.
obua@17644
   676
   EX r::nat => nat => nat.
obua@17644
   677
      ALL (m::nat) n::nat.
obua@17652
   678
         COND (n = 0) (q m n = 0 & r m n = 0)
obua@17644
   679
          (m = q m n * n + r m n & < (r m n) n)"
obua@17644
   680
obua@17644
   681
lemma DEF_DIV: "DIV =
obua@17644
   682
(SOME q::nat => nat => nat.
obua@17644
   683
    EX r::nat => nat => nat.
obua@17644
   684
       ALL (m::nat) n::nat.
obua@17652
   685
          COND (n = 0) (q m n = 0 & r m n = 0)
obua@17644
   686
           (m = q m n * n + r m n & < (r m n) n))"
obua@17644
   687
  by (import hollight DEF_DIV)
obua@17644
   688
obua@17644
   689
constdefs
obua@17644
   690
  MOD :: "nat => nat => nat" 
obua@17644
   691
  "MOD ==
obua@17644
   692
SOME r::nat => nat => nat.
obua@17644
   693
   ALL (m::nat) n::nat.
obua@17652
   694
      COND (n = 0) (DIV m n = 0 & r m n = 0)
obua@17644
   695
       (m = DIV m n * n + r m n & < (r m n) n)"
obua@17644
   696
obua@17644
   697
lemma DEF_MOD: "MOD =
obua@17644
   698
(SOME r::nat => nat => nat.
obua@17644
   699
    ALL (m::nat) n::nat.
obua@17652
   700
       COND (n = 0) (DIV m n = 0 & r m n = 0)
obua@17644
   701
        (m = DIV m n * n + r m n & < (r m n) n))"
obua@17644
   702
  by (import hollight DEF_MOD)
obua@17644
   703
obua@17652
   704
lemma DIVISION: "ALL (m::nat) n::nat. n ~= 0 --> m = DIV m n * n + MOD m n & < (MOD m n) n"
obua@17644
   705
  by (import hollight DIVISION)
obua@17644
   706
obua@17644
   707
lemma DIVMOD_UNIQ_LEMMA: "ALL (m::nat) (n::nat) (q1::nat) (r1::nat) (q2::nat) r2::nat.
obua@17644
   708
   (m = q1 * n + r1 & < r1 n) & m = q2 * n + r2 & < r2 n -->
obua@17644
   709
   q1 = q2 & r1 = r2"
obua@17644
   710
  by (import hollight DIVMOD_UNIQ_LEMMA)
obua@17644
   711
obua@17644
   712
lemma DIVMOD_UNIQ: "ALL (m::nat) (n::nat) (q::nat) r::nat.
obua@17644
   713
   m = q * n + r & < r n --> DIV m n = q & MOD m n = r"
obua@17644
   714
  by (import hollight DIVMOD_UNIQ)
obua@17644
   715
obua@17644
   716
lemma MOD_UNIQ: "ALL (m::nat) (n::nat) (q::nat) r::nat. m = q * n + r & < r n --> MOD m n = r"
obua@17644
   717
  by (import hollight MOD_UNIQ)
obua@17644
   718
obua@17644
   719
lemma DIV_UNIQ: "ALL (m::nat) (n::nat) (q::nat) r::nat. m = q * n + r & < r n --> DIV m n = q"
obua@17644
   720
  by (import hollight DIV_UNIQ)
obua@17644
   721
obua@17652
   722
lemma MOD_MULT: "ALL (x::nat) xa::nat. x ~= 0 --> MOD (x * xa) x = 0"
obua@17644
   723
  by (import hollight MOD_MULT)
obua@17644
   724
obua@17652
   725
lemma DIV_MULT: "ALL (x::nat) xa::nat. x ~= 0 --> DIV (x * xa) x = xa"
obua@17644
   726
  by (import hollight DIV_MULT)
obua@17644
   727
obua@17652
   728
lemma DIV_DIV: "ALL (m::nat) (n::nat) p::nat. n * p ~= 0 --> DIV (DIV m n) p = DIV m (n * p)"
obua@17644
   729
  by (import hollight DIV_DIV)
obua@17644
   730
obua@17644
   731
lemma MOD_LT: "ALL (m::nat) n::nat. < m n --> MOD m n = m"
obua@17644
   732
  by (import hollight MOD_LT)
obua@17644
   733
obua@17644
   734
lemma MOD_EQ: "ALL (m::nat) (n::nat) (p::nat) q::nat. m = n + q * p --> MOD m p = MOD n p"
obua@17644
   735
  by (import hollight MOD_EQ)
obua@17644
   736
obua@17644
   737
lemma DIV_MOD: "ALL (m::nat) (n::nat) p::nat.
obua@17652
   738
   n * p ~= 0 --> MOD (DIV m n) p = DIV (MOD m (n * p)) n"
obua@17644
   739
  by (import hollight DIV_MOD)
obua@17644
   740
obua@17652
   741
lemma DIV_1: "ALL n::nat. DIV n (NUMERAL_BIT1 0) = n"
obua@17644
   742
  by (import hollight DIV_1)
obua@17644
   743
obua@17652
   744
lemma EXP_LT_0: "ALL (x::nat) xa::nat. < 0 (EXP xa x) = (xa ~= 0 | x = 0)"
obua@17644
   745
  by (import hollight EXP_LT_0)
obua@17644
   746
obua@17652
   747
lemma DIV_LE: "ALL (m::nat) n::nat. n ~= 0 --> <= (DIV m n) m"
obua@17644
   748
  by (import hollight DIV_LE)
obua@17644
   749
obua@17644
   750
lemma DIV_MUL_LE: "ALL (m::nat) n::nat. <= (n * DIV m n) m"
obua@17644
   751
  by (import hollight DIV_MUL_LE)
obua@17644
   752
obua@17652
   753
lemma DIV_0: "ALL n::nat. n ~= 0 --> DIV 0 n = 0"
obua@17644
   754
  by (import hollight DIV_0)
obua@17644
   755
obua@17652
   756
lemma MOD_0: "ALL n::nat. n ~= 0 --> MOD 0 n = 0"
obua@17644
   757
  by (import hollight MOD_0)
obua@17644
   758
obua@17652
   759
lemma DIV_LT: "ALL (m::nat) n::nat. < m n --> DIV m n = 0"
obua@17644
   760
  by (import hollight DIV_LT)
obua@17644
   761
obua@17652
   762
lemma MOD_MOD: "ALL (m::nat) (n::nat) p::nat. n * p ~= 0 --> MOD (MOD m (n * p)) n = MOD m n"
obua@17644
   763
  by (import hollight MOD_MOD)
obua@17644
   764
obua@17652
   765
lemma MOD_MOD_REFL: "ALL (m::nat) n::nat. n ~= 0 --> MOD (MOD m n) n = MOD m n"
obua@17644
   766
  by (import hollight MOD_MOD_REFL)
obua@17644
   767
obua@17644
   768
lemma DIV_MULT2: "ALL (x::nat) (xa::nat) xb::nat.
obua@17652
   769
   x * xb ~= 0 --> DIV (x * xa) (x * xb) = DIV xa xb"
obua@17644
   770
  by (import hollight DIV_MULT2)
obua@17644
   771
obua@17644
   772
lemma MOD_MULT2: "ALL (x::nat) (xa::nat) xb::nat.
obua@17652
   773
   x * xb ~= 0 --> MOD (x * xa) (x * xb) = x * MOD xa xb"
obua@17644
   774
  by (import hollight MOD_MULT2)
obua@17644
   775
obua@17652
   776
lemma MOD_1: "ALL n::nat. MOD n (NUMERAL_BIT1 0) = 0"
obua@17644
   777
  by (import hollight MOD_1)
obua@17644
   778
obua@17644
   779
lemma MOD_EXISTS: "ALL (m::nat) n::nat.
obua@17652
   780
   (EX q::nat. m = n * q) = COND (n = 0) (m = 0) (MOD m n = 0)"
obua@17644
   781
  by (import hollight MOD_EXISTS)
obua@17644
   782
obua@17644
   783
lemma LT_EXP: "ALL (x::nat) (m::nat) n::nat.
obua@17644
   784
   < (EXP x m) (EXP x n) =
obua@17652
   785
   (<= (NUMERAL_BIT0 (NUMERAL_BIT1 0)) x & < m n | x = 0 & m ~= 0 & n = 0)"
obua@17644
   786
  by (import hollight LT_EXP)
obua@17644
   787
obua@17644
   788
lemma LE_EXP: "ALL (x::nat) (m::nat) n::nat.
obua@17644
   789
   <= (EXP x m) (EXP x n) =
obua@17652
   790
   COND (x = 0) (m = 0 --> n = 0) (x = NUMERAL_BIT1 0 | <= m n)"
obua@17644
   791
  by (import hollight LE_EXP)
obua@17644
   792
obua@17652
   793
lemma DIV_MONO: "ALL (m::nat) (n::nat) p::nat. p ~= 0 & <= m n --> <= (DIV m p) (DIV n p)"
obua@17644
   794
  by (import hollight DIV_MONO)
obua@17644
   795
obua@17644
   796
lemma DIV_MONO_LT: "ALL (m::nat) (n::nat) p::nat.
obua@17652
   797
   p ~= 0 & <= (m + p) n --> < (DIV m p) (DIV n p)"
obua@17644
   798
  by (import hollight DIV_MONO_LT)
obua@17644
   799
obua@17652
   800
lemma LE_LDIV: "ALL (a::nat) (b::nat) n::nat. a ~= 0 & <= b (a * n) --> <= (DIV b a) n"
obua@17644
   801
  by (import hollight LE_LDIV)
obua@17644
   802
obua@17652
   803
lemma LE_RDIV_EQ: "ALL (a::nat) (b::nat) n::nat. a ~= 0 --> <= n (DIV b a) = <= (a * n) b"
obua@17644
   804
  by (import hollight LE_RDIV_EQ)
obua@17644
   805
obua@17644
   806
lemma LE_LDIV_EQ: "ALL (a::nat) (b::nat) n::nat.
obua@17652
   807
   a ~= 0 --> <= (DIV b a) n = < b (a * (n + NUMERAL_BIT1 0))"
obua@17644
   808
  by (import hollight LE_LDIV_EQ)
obua@17644
   809
obua@17652
   810
lemma DIV_EQ_0: "ALL (m::nat) n::nat. n ~= 0 --> (DIV m n = 0) = < m n"
obua@17644
   811
  by (import hollight DIV_EQ_0)
obua@17644
   812
obua@17652
   813
lemma MOD_EQ_0: "ALL (m::nat) n::nat. n ~= 0 --> (MOD m n = 0) = (EX q::nat. m = q * n)"
obua@17644
   814
  by (import hollight MOD_EQ_0)
obua@17644
   815
obua@17652
   816
lemma EVEN_MOD: "ALL n::nat. EVEN n = (MOD n (NUMERAL_BIT0 (NUMERAL_BIT1 0)) = 0)"
obua@17644
   817
  by (import hollight EVEN_MOD)
obua@17644
   818
obua@17652
   819
lemma ODD_MOD: "ALL n::nat. ODD n = (MOD n (NUMERAL_BIT0 (NUMERAL_BIT1 0)) = NUMERAL_BIT1 0)"
obua@17644
   820
  by (import hollight ODD_MOD)
obua@17644
   821
obua@17652
   822
lemma MOD_MULT_RMOD: "ALL (m::nat) (n::nat) p::nat. n ~= 0 --> MOD (m * MOD p n) n = MOD (m * p) n"
obua@17644
   823
  by (import hollight MOD_MULT_RMOD)
obua@17644
   824
obua@17644
   825
lemma MOD_MULT_LMOD: "ALL (x::nat) (xa::nat) xb::nat.
obua@17652
   826
   xa ~= 0 --> MOD (MOD x xa * xb) xa = MOD (x * xb) xa"
obua@17644
   827
  by (import hollight MOD_MULT_LMOD)
obua@17644
   828
obua@17644
   829
lemma MOD_MULT_MOD2: "ALL (x::nat) (xa::nat) xb::nat.
obua@17652
   830
   xa ~= 0 --> MOD (MOD x xa * MOD xb xa) xa = MOD (x * xb) xa"
obua@17644
   831
  by (import hollight MOD_MULT_MOD2)
obua@17644
   832
obua@17644
   833
lemma MOD_EXP_MOD: "ALL (m::nat) (n::nat) p::nat.
obua@17652
   834
   n ~= 0 --> MOD (EXP (MOD m n) p) n = MOD (EXP m p) n"
obua@17644
   835
  by (import hollight MOD_EXP_MOD)
obua@17644
   836
obua@17644
   837
lemma MOD_MULT_ADD: "ALL (m::nat) (n::nat) p::nat. MOD (m * n + p) n = MOD p n"
obua@17644
   838
  by (import hollight MOD_MULT_ADD)
obua@17644
   839
obua@17644
   840
lemma MOD_ADD_MOD: "ALL (a::nat) (b::nat) n::nat.
obua@17652
   841
   n ~= 0 --> MOD (MOD a n + MOD b n) n = MOD (a + b) n"
obua@17644
   842
  by (import hollight MOD_ADD_MOD)
obua@17644
   843
obua@17644
   844
lemma DIV_ADD_MOD: "ALL (a::nat) (b::nat) n::nat.
obua@17652
   845
   n ~= 0 -->
obua@17644
   846
   (MOD (a + b) n = MOD a n + MOD b n) = (DIV (a + b) n = DIV a n + DIV b n)"
obua@17644
   847
  by (import hollight DIV_ADD_MOD)
obua@17644
   848
obua@17652
   849
lemma DIV_REFL: "ALL n::nat. n ~= 0 --> DIV n n = NUMERAL_BIT1 0"
obua@17644
   850
  by (import hollight DIV_REFL)
obua@17644
   851
obua@17652
   852
lemma MOD_LE: "ALL (m::nat) n::nat. n ~= 0 --> <= (MOD m n) m"
obua@17644
   853
  by (import hollight MOD_LE)
obua@17644
   854
obua@17652
   855
lemma DIV_MONO2: "ALL (m::nat) (n::nat) p::nat. p ~= 0 & <= p m --> <= (DIV n m) (DIV n p)"
obua@17644
   856
  by (import hollight DIV_MONO2)
obua@17644
   857
obua@17644
   858
lemma DIV_LE_EXCLUSION: "ALL (a::nat) (b::nat) (c::nat) d::nat.
obua@17652
   859
   b ~= 0 & < (b * c) ((a + NUMERAL_BIT1 0) * d) --> <= (DIV c d) (DIV a b)"
obua@17644
   860
  by (import hollight DIV_LE_EXCLUSION)
obua@17644
   861
obua@17652
   862
lemma DIV_EQ_EXCLUSION: "< ((b::nat) * (c::nat)) (((a::nat) + NUMERAL_BIT1 0) * (d::nat)) &
obua@17652
   863
< (a * d) ((c + NUMERAL_BIT1 0) * b) -->
obua@17644
   864
DIV a b = DIV c d"
obua@17644
   865
  by (import hollight DIV_EQ_EXCLUSION)
obua@17644
   866
obua@17644
   867
lemma SUB_ELIM_THM: "(P::nat => bool) ((a::nat) - (b::nat)) =
obua@17652
   868
(ALL x::nat. (b = a + x --> P 0) & (a = b + x --> P x))"
obua@17644
   869
  by (import hollight SUB_ELIM_THM)
obua@17644
   870
obua@17644
   871
lemma PRE_ELIM_THM: "(P::nat => bool) (Pred (n::nat)) =
obua@17652
   872
(ALL m::nat. (n = 0 --> P 0) & (n = Suc m --> P m))"
obua@17644
   873
  by (import hollight PRE_ELIM_THM)
obua@17644
   874
obua@17644
   875
lemma DIVMOD_ELIM_THM: "(P::nat => nat => bool) (DIV (m::nat) (n::nat)) (MOD m n) =
obua@17652
   876
(n = 0 & P 0 0 |
obua@17652
   877
 n ~= 0 & (ALL (q::nat) r::nat. m = q * n + r & < r n --> P q r))"
obua@17644
   878
  by (import hollight DIVMOD_ELIM_THM)
obua@17644
   879
obua@17644
   880
constdefs
obua@17652
   881
  eqeq :: "'q_9910 => 'q_9909 => ('q_9910 => 'q_9909 => bool) => bool" 
obua@17644
   882
  "eqeq ==
obua@17644
   883
%(u::'q_9910::type) (ua::'q_9909::type)
obua@17644
   884
   ub::'q_9910::type => 'q_9909::type => bool. ub u ua"
obua@17644
   885
obua@17644
   886
lemma DEF__equal__equal_: "eqeq =
obua@17644
   887
(%(u::'q_9910::type) (ua::'q_9909::type)
obua@17644
   888
    ub::'q_9910::type => 'q_9909::type => bool. ub u ua)"
obua@17644
   889
  by (import hollight DEF__equal__equal_)
obua@17644
   890
obua@17644
   891
constdefs
obua@17644
   892
  mod_nat :: "nat => nat => nat => bool" 
obua@17644
   893
  "mod_nat ==
obua@17644
   894
%(u::nat) (ua::nat) ub::nat. EX (q1::nat) q2::nat. ua + u * q1 = ub + u * q2"
obua@17644
   895
obua@17644
   896
lemma DEF_mod_nat: "mod_nat =
obua@17644
   897
(%(u::nat) (ua::nat) ub::nat.
obua@17644
   898
    EX (q1::nat) q2::nat. ua + u * q1 = ub + u * q2)"
obua@17644
   899
  by (import hollight DEF_mod_nat)
obua@17644
   900
obua@17644
   901
constdefs
obua@17644
   902
  minimal :: "(nat => bool) => nat" 
obua@17644
   903
  "minimal == %u::nat => bool. SOME n::nat. u n & (ALL m::nat. < m n --> ~ u m)"
obua@17644
   904
obua@17644
   905
lemma DEF_minimal: "minimal =
obua@17644
   906
(%u::nat => bool. SOME n::nat. u n & (ALL m::nat. < m n --> ~ u m))"
obua@17644
   907
  by (import hollight DEF_minimal)
obua@17644
   908
obua@17644
   909
lemma MINIMAL: "ALL P::nat => bool.
obua@17644
   910
   Ex P = (P (minimal P) & (ALL x::nat. < x (minimal P) --> ~ P x))"
obua@17644
   911
  by (import hollight MINIMAL)
obua@17644
   912
obua@17644
   913
constdefs
obua@17652
   914
  WF :: "('A => 'A => bool) => bool" 
obua@17644
   915
  "WF ==
obua@17644
   916
%u::'A::type => 'A::type => bool.
obua@17644
   917
   ALL P::'A::type => bool.
obua@17644
   918
      Ex P --> (EX x::'A::type. P x & (ALL y::'A::type. u y x --> ~ P y))"
obua@17644
   919
obua@17644
   920
lemma DEF_WF: "WF =
obua@17644
   921
(%u::'A::type => 'A::type => bool.
obua@17644
   922
    ALL P::'A::type => bool.
obua@17644
   923
       Ex P --> (EX x::'A::type. P x & (ALL y::'A::type. u y x --> ~ P y)))"
obua@17644
   924
  by (import hollight DEF_WF)
obua@17644
   925
obua@17644
   926
lemma WF_EQ: "WF (u_354::'A::type => 'A::type => bool) =
obua@17644
   927
(ALL P::'A::type => bool.
obua@17644
   928
    Ex P = (EX x::'A::type. P x & (ALL y::'A::type. u_354 y x --> ~ P y)))"
obua@17644
   929
  by (import hollight WF_EQ)
obua@17644
   930
obua@17644
   931
lemma WF_IND: "WF (u_354::'A::type => 'A::type => bool) =
obua@17644
   932
(ALL P::'A::type => bool.
obua@17644
   933
    (ALL x::'A::type. (ALL y::'A::type. u_354 y x --> P y) --> P x) -->
obua@17644
   934
    All P)"
obua@17644
   935
  by (import hollight WF_IND)
obua@17644
   936
obua@17644
   937
lemma WF_DCHAIN: "WF (u_354::'A::type => 'A::type => bool) =
obua@17644
   938
(~ (EX s::nat => 'A::type. ALL n::nat. u_354 (s (Suc n)) (s n)))"
obua@17644
   939
  by (import hollight WF_DCHAIN)
obua@17644
   940
obua@17644
   941
lemma WF_UREC: "WF (u_354::'A::type => 'A::type => bool) -->
obua@17644
   942
(ALL H::('A::type => 'B::type) => 'A::type => 'B::type.
obua@17644
   943
    (ALL (f::'A::type => 'B::type) (g::'A::type => 'B::type) x::'A::type.
obua@17644
   944
        (ALL z::'A::type. u_354 z x --> f z = g z) --> H f x = H g x) -->
obua@17644
   945
    (ALL (f::'A::type => 'B::type) g::'A::type => 'B::type.
obua@17644
   946
        (ALL x::'A::type. f x = H f x) & (ALL x::'A::type. g x = H g x) -->
obua@17644
   947
        f = g))"
obua@17644
   948
  by (import hollight WF_UREC)
obua@17644
   949
obua@17644
   950
lemma WF_UREC_WF: "(ALL H::('A::type => bool) => 'A::type => bool.
obua@17644
   951
    (ALL (f::'A::type => bool) (g::'A::type => bool) x::'A::type.
obua@17644
   952
        (ALL z::'A::type.
obua@17644
   953
            (u_354::'A::type => 'A::type => bool) z x --> f z = g z) -->
obua@17644
   954
        H f x = H g x) -->
obua@17644
   955
    (ALL (f::'A::type => bool) g::'A::type => bool.
obua@17644
   956
        (ALL x::'A::type. f x = H f x) & (ALL x::'A::type. g x = H g x) -->
obua@17644
   957
        f = g)) -->
obua@17644
   958
WF u_354"
obua@17644
   959
  by (import hollight WF_UREC_WF)
obua@17644
   960
obua@17644
   961
lemma WF_REC_INVARIANT: "WF (u_354::'A::type => 'A::type => bool) -->
obua@17644
   962
(ALL (H::('A::type => 'B::type) => 'A::type => 'B::type)
obua@17644
   963
    S::'A::type => 'B::type => bool.
obua@17644
   964
    (ALL (f::'A::type => 'B::type) (g::'A::type => 'B::type) x::'A::type.
obua@17644
   965
        (ALL z::'A::type. u_354 z x --> f z = g z & S z (f z)) -->
obua@17644
   966
        H f x = H g x & S x (H f x)) -->
obua@17644
   967
    (EX f::'A::type => 'B::type. ALL x::'A::type. f x = H f x))"
obua@17644
   968
  by (import hollight WF_REC_INVARIANT)
obua@17644
   969
obua@17644
   970
lemma WF_REC: "WF (u_354::'A::type => 'A::type => bool) -->
obua@17644
   971
(ALL H::('A::type => 'B::type) => 'A::type => 'B::type.
obua@17644
   972
    (ALL (f::'A::type => 'B::type) (g::'A::type => 'B::type) x::'A::type.
obua@17644
   973
        (ALL z::'A::type. u_354 z x --> f z = g z) --> H f x = H g x) -->
obua@17644
   974
    (EX f::'A::type => 'B::type. ALL x::'A::type. f x = H f x))"
obua@17644
   975
  by (import hollight WF_REC)
obua@17644
   976
obua@17644
   977
lemma WF_REC_WF: "(ALL H::('A::type => nat) => 'A::type => nat.
obua@17644
   978
    (ALL (f::'A::type => nat) (g::'A::type => nat) x::'A::type.
obua@17644
   979
        (ALL z::'A::type.
obua@17644
   980
            (u_354::'A::type => 'A::type => bool) z x --> f z = g z) -->
obua@17644
   981
        H f x = H g x) -->
obua@17644
   982
    (EX f::'A::type => nat. ALL x::'A::type. f x = H f x)) -->
obua@17644
   983
WF u_354"
obua@17644
   984
  by (import hollight WF_REC_WF)
obua@17644
   985
obua@17644
   986
lemma WF_EREC: "WF (u_354::'A::type => 'A::type => bool) -->
obua@17644
   987
(ALL H::('A::type => 'B::type) => 'A::type => 'B::type.
obua@17644
   988
    (ALL (f::'A::type => 'B::type) (g::'A::type => 'B::type) x::'A::type.
obua@17644
   989
        (ALL z::'A::type. u_354 z x --> f z = g z) --> H f x = H g x) -->
obua@17644
   990
    (EX! f::'A::type => 'B::type. ALL x::'A::type. f x = H f x))"
obua@17644
   991
  by (import hollight WF_EREC)
obua@17644
   992
obua@17644
   993
lemma WF_SUBSET: "(ALL (x::'A::type) y::'A::type.
obua@17644
   994
    (u_354::'A::type => 'A::type => bool) x y -->
obua@17644
   995
    (u_473::'A::type => 'A::type => bool) x y) &
obua@17644
   996
WF u_473 -->
obua@17644
   997
WF u_354"
obua@17644
   998
  by (import hollight WF_SUBSET)
obua@17644
   999
obua@17644
  1000
lemma WF_MEASURE_GEN: "ALL m::'A::type => 'B::type.
obua@17644
  1001
   WF (u_354::'B::type => 'B::type => bool) -->
obua@17644
  1002
   WF (%(x::'A::type) x'::'A::type. u_354 (m x) (m x'))"
obua@17644
  1003
  by (import hollight WF_MEASURE_GEN)
obua@17644
  1004
obua@17644
  1005
lemma WF_LEX_DEPENDENT: "ALL (R::'A::type => 'A::type => bool)
obua@17644
  1006
   S::'A::type => 'B::type => 'B::type => bool.
obua@17644
  1007
   WF R & (ALL x::'A::type. WF (S x)) -->
obua@17644
  1008
   WF (GABS
obua@17644
  1009
        (%f::'A::type * 'B::type => 'A::type * 'B::type => bool.
obua@17644
  1010
            ALL (r1::'A::type) s1::'B::type.
obua@17644
  1011
               GEQ (f (r1, s1))
obua@17644
  1012
                (GABS
obua@17644
  1013
                  (%f::'A::type * 'B::type => bool.
obua@17644
  1014
                      ALL (r2::'A::type) s2::'B::type.
obua@17644
  1015
                         GEQ (f (r2, s2))
obua@17644
  1016
                          (R r1 r2 | r1 = r2 & S r1 s1 s2)))))"
obua@17644
  1017
  by (import hollight WF_LEX_DEPENDENT)
obua@17644
  1018
obua@17644
  1019
lemma WF_LEX: "ALL (x::'A::type => 'A::type => bool) xa::'B::type => 'B::type => bool.
obua@17644
  1020
   WF x & WF xa -->
obua@17644
  1021
   WF (GABS
obua@17644
  1022
        (%f::'A::type * 'B::type => 'A::type * 'B::type => bool.
obua@17644
  1023
            ALL (r1::'A::type) s1::'B::type.
obua@17644
  1024
               GEQ (f (r1, s1))
obua@17644
  1025
                (GABS
obua@17644
  1026
                  (%f::'A::type * 'B::type => bool.
obua@17644
  1027
                      ALL (r2::'A::type) s2::'B::type.
obua@17644
  1028
                         GEQ (f (r2, s2)) (x r1 r2 | r1 = r2 & xa s1 s2)))))"
obua@17644
  1029
  by (import hollight WF_LEX)
obua@17644
  1030
obua@17644
  1031
lemma WF_POINTWISE: "WF (u_354::'A::type => 'A::type => bool) &
obua@17644
  1032
WF (u_473::'B::type => 'B::type => bool) -->
obua@17644
  1033
WF (GABS
obua@17644
  1034
     (%f::'A::type * 'B::type => 'A::type * 'B::type => bool.
obua@17644
  1035
         ALL (x1::'A::type) y1::'B::type.
obua@17644
  1036
            GEQ (f (x1, y1))
obua@17644
  1037
             (GABS
obua@17644
  1038
               (%f::'A::type * 'B::type => bool.
obua@17644
  1039
                   ALL (x2::'A::type) y2::'B::type.
obua@17644
  1040
                      GEQ (f (x2, y2)) (u_354 x1 x2 & u_473 y1 y2)))))"
obua@17644
  1041
  by (import hollight WF_POINTWISE)
obua@17644
  1042
obua@17644
  1043
lemma WF_num: "WF <"
obua@17644
  1044
  by (import hollight WF_num)
obua@17644
  1045
obua@17644
  1046
lemma WF_REC_num: "ALL H::(nat => 'A::type) => nat => 'A::type.
obua@17644
  1047
   (ALL (f::nat => 'A::type) (g::nat => 'A::type) x::nat.
obua@17644
  1048
       (ALL z::nat. < z x --> f z = g z) --> H f x = H g x) -->
obua@17644
  1049
   (EX f::nat => 'A::type. ALL x::nat. f x = H f x)"
obua@17644
  1050
  by (import hollight WF_REC_num)
obua@17644
  1051
obua@17644
  1052
consts
obua@17652
  1053
  measure :: "('q_11107 => nat) => 'q_11107 => 'q_11107 => bool" 
obua@17644
  1054
obua@17644
  1055
defs
obua@17644
  1056
  measure_def: "hollight.measure ==
obua@17644
  1057
%(u::'q_11107::type => nat) (x::'q_11107::type) y::'q_11107::type.
obua@17644
  1058
   < (u x) (u y)"
obua@17644
  1059
obua@17644
  1060
lemma DEF_measure: "hollight.measure =
obua@17644
  1061
(%(u::'q_11107::type => nat) (x::'q_11107::type) y::'q_11107::type.
obua@17644
  1062
    < (u x) (u y))"
obua@17644
  1063
  by (import hollight DEF_measure)
obua@17644
  1064
obua@17644
  1065
lemma WF_MEASURE: "ALL m::'A::type => nat. WF (hollight.measure m)"
obua@17644
  1066
  by (import hollight WF_MEASURE)
obua@17644
  1067
obua@17644
  1068
lemma MEASURE_LE: "(ALL x::'q_11137::type.
obua@17644
  1069
    hollight.measure (m::'q_11137::type => nat) x (a::'q_11137::type) -->
obua@17644
  1070
    hollight.measure m x (b::'q_11137::type)) =
obua@17644
  1071
<= (m a) (m b)"
obua@17644
  1072
  by (import hollight MEASURE_LE)
obua@17644
  1073
obua@17644
  1074
lemma WF_REFL: "ALL x::'A::type. WF (u_354::'A::type => 'A::type => bool) --> ~ u_354 x x"
obua@17644
  1075
  by (import hollight WF_REFL)
obua@17644
  1076
obua@17644
  1077
lemma WF_FALSE: "WF (%(x::'A::type) y::'A::type. False)"
obua@17644
  1078
  by (import hollight WF_FALSE)
obua@17644
  1079
obua@17644
  1080
lemma WF_REC_TAIL: "ALL (P::'A::type => bool) (g::'A::type => 'A::type) h::'A::type => 'B::type.
obua@17644
  1081
   EX f::'A::type => 'B::type.
obua@17644
  1082
      ALL x::'A::type. f x = COND (P x) (f (g x)) (h x)"
obua@17644
  1083
  by (import hollight WF_REC_TAIL)
obua@17644
  1084
obua@17644
  1085
lemma WF_REC_TAIL_GENERAL: "ALL (P::('A::type => 'B::type) => 'A::type => bool)
obua@17644
  1086
   (G::('A::type => 'B::type) => 'A::type => 'A::type)
obua@17644
  1087
   H::('A::type => 'B::type) => 'A::type => 'B::type.
obua@17644
  1088
   WF (u_354::'A::type => 'A::type => bool) &
obua@17644
  1089
   (ALL (f::'A::type => 'B::type) (g::'A::type => 'B::type) x::'A::type.
obua@17644
  1090
       (ALL z::'A::type. u_354 z x --> f z = g z) -->
obua@17644
  1091
       P f x = P g x & G f x = G g x & H f x = H g x) &
obua@17644
  1092
   (ALL (f::'A::type => 'B::type) (g::'A::type => 'B::type) x::'A::type.
obua@17644
  1093
       (ALL z::'A::type. u_354 z x --> f z = g z) --> H f x = H g x) &
obua@17644
  1094
   (ALL (f::'A::type => 'B::type) (x::'A::type) y::'A::type.
obua@17644
  1095
       P f x & u_354 y (G f x) --> u_354 y x) -->
obua@17644
  1096
   (EX f::'A::type => 'B::type.
obua@17644
  1097
       ALL x::'A::type. f x = COND (P f x) (f (G f x)) (H f x))"
obua@17644
  1098
  by (import hollight WF_REC_TAIL_GENERAL)
obua@17644
  1099
obua@17652
  1100
lemma ARITH_ZERO: "(op &::bool => bool => bool) ((op =::nat => nat => bool) (0::nat) (0::nat))
obua@17652
  1101
 ((op =::nat => nat => bool) ((NUMERAL_BIT0::nat => nat) (0::nat)) (0::nat))"
obua@17644
  1102
  by (import hollight ARITH_ZERO)
obua@17644
  1103
obua@17644
  1104
lemma ARITH_SUC: "(ALL x::nat. Suc x = Suc x) &
obua@17652
  1105
Suc 0 = NUMERAL_BIT1 0 &
obua@17644
  1106
(ALL x::nat. Suc (NUMERAL_BIT0 x) = NUMERAL_BIT1 x) &
obua@17644
  1107
(ALL x::nat. Suc (NUMERAL_BIT1 x) = NUMERAL_BIT0 (Suc x))"
obua@17644
  1108
  by (import hollight ARITH_SUC)
obua@17644
  1109
obua@17644
  1110
lemma ARITH_PRE: "(ALL x::nat. Pred x = Pred x) &
obua@17652
  1111
Pred 0 = 0 &
obua@17644
  1112
(ALL x::nat.
obua@17652
  1113
    Pred (NUMERAL_BIT0 x) = COND (x = 0) 0 (NUMERAL_BIT1 (Pred x))) &
obua@17644
  1114
(ALL x::nat. Pred (NUMERAL_BIT1 x) = NUMERAL_BIT0 x)"
obua@17644
  1115
  by (import hollight ARITH_PRE)
obua@17644
  1116
obua@17652
  1117
lemma ARITH_ADD: "(op &::bool => bool => bool)
obua@17652
  1118
 ((All::(nat => bool) => bool)
obua@17652
  1119
   (%x::nat.
obua@17652
  1120
       (All::(nat => bool) => bool)
obua@17652
  1121
        (%xa::nat.
obua@17652
  1122
            (op =::nat => nat => bool) ((op +::nat => nat => nat) x xa)
obua@17652
  1123
             ((op +::nat => nat => nat) x xa))))
obua@17652
  1124
 ((op &::bool => bool => bool)
obua@17652
  1125
   ((op =::nat => nat => bool) ((op +::nat => nat => nat) (0::nat) (0::nat))
obua@17652
  1126
     (0::nat))
obua@17652
  1127
   ((op &::bool => bool => bool)
obua@17652
  1128
     ((All::(nat => bool) => bool)
obua@17652
  1129
       (%x::nat.
obua@17652
  1130
           (op =::nat => nat => bool)
obua@17652
  1131
            ((op +::nat => nat => nat) (0::nat)
obua@17652
  1132
              ((NUMERAL_BIT0::nat => nat) x))
obua@17652
  1133
            ((NUMERAL_BIT0::nat => nat) x)))
obua@17652
  1134
     ((op &::bool => bool => bool)
obua@17652
  1135
       ((All::(nat => bool) => bool)
obua@17652
  1136
         (%x::nat.
obua@17652
  1137
             (op =::nat => nat => bool)
obua@17652
  1138
              ((op +::nat => nat => nat) (0::nat)
obua@17652
  1139
                ((NUMERAL_BIT1::nat => nat) x))
obua@17652
  1140
              ((NUMERAL_BIT1::nat => nat) x)))
obua@17652
  1141
       ((op &::bool => bool => bool)
obua@17652
  1142
         ((All::(nat => bool) => bool)
obua@17652
  1143
           (%x::nat.
obua@17652
  1144
               (op =::nat => nat => bool)
obua@17652
  1145
                ((op +::nat => nat => nat) ((NUMERAL_BIT0::nat => nat) x)
obua@17652
  1146
                  (0::nat))
obua@17652
  1147
                ((NUMERAL_BIT0::nat => nat) x)))
obua@17652
  1148
         ((op &::bool => bool => bool)
obua@17652
  1149
           ((All::(nat => bool) => bool)
obua@17652
  1150
             (%x::nat.
obua@17652
  1151
                 (op =::nat => nat => bool)
obua@17652
  1152
                  ((op +::nat => nat => nat) ((NUMERAL_BIT1::nat => nat) x)
obua@17652
  1153
                    (0::nat))
obua@17652
  1154
                  ((NUMERAL_BIT1::nat => nat) x)))
obua@17652
  1155
           ((op &::bool => bool => bool)
obua@17652
  1156
             ((All::(nat => bool) => bool)
obua@17652
  1157
               (%x::nat.
obua@17652
  1158
                   (All::(nat => bool) => bool)
obua@17652
  1159
                    (%xa::nat.
obua@17652
  1160
                        (op =::nat => nat => bool)
obua@17652
  1161
                         ((op +::nat => nat => nat)
obua@17652
  1162
                           ((NUMERAL_BIT0::nat => nat) x)
obua@17652
  1163
                           ((NUMERAL_BIT0::nat => nat) xa))
obua@17652
  1164
                         ((NUMERAL_BIT0::nat => nat)
obua@17652
  1165
                           ((op +::nat => nat => nat) x xa)))))
obua@17652
  1166
             ((op &::bool => bool => bool)
obua@17652
  1167
               ((All::(nat => bool) => bool)
obua@17652
  1168
                 (%x::nat.
obua@17652
  1169
                     (All::(nat => bool) => bool)
obua@17652
  1170
                      (%xa::nat.
obua@17652
  1171
                          (op =::nat => nat => bool)
obua@17652
  1172
                           ((op +::nat => nat => nat)
obua@17652
  1173
                             ((NUMERAL_BIT0::nat => nat) x)
obua@17652
  1174
                             ((NUMERAL_BIT1::nat => nat) xa))
obua@17652
  1175
                           ((NUMERAL_BIT1::nat => nat)
obua@17652
  1176
                             ((op +::nat => nat => nat) x xa)))))
obua@17652
  1177
               ((op &::bool => bool => bool)
obua@17652
  1178
                 ((All::(nat => bool) => bool)
obua@17652
  1179
                   (%x::nat.
obua@17652
  1180
                       (All::(nat => bool) => bool)
obua@17652
  1181
                        (%xa::nat.
obua@17652
  1182
                            (op =::nat => nat => bool)
obua@17652
  1183
                             ((op +::nat => nat => nat)
obua@17652
  1184
                               ((NUMERAL_BIT1::nat => nat) x)
obua@17652
  1185
                               ((NUMERAL_BIT0::nat => nat) xa))
obua@17652
  1186
                             ((NUMERAL_BIT1::nat => nat)
obua@17652
  1187
                               ((op +::nat => nat => nat) x xa)))))
obua@17652
  1188
                 ((All::(nat => bool) => bool)
obua@17652
  1189
                   (%x::nat.
obua@17652
  1190
                       (All::(nat => bool) => bool)
obua@17652
  1191
                        (%xa::nat.
obua@17652
  1192
                            (op =::nat => nat => bool)
obua@17652
  1193
                             ((op +::nat => nat => nat)
obua@17652
  1194
                               ((NUMERAL_BIT1::nat => nat) x)
obua@17652
  1195
                               ((NUMERAL_BIT1::nat => nat) xa))
obua@17652
  1196
                             ((NUMERAL_BIT0::nat => nat)
obua@17652
  1197
                               ((Suc::nat => nat)
obua@17652
  1198
                                 ((op +::nat => nat => nat) x
obua@17652
  1199
                                   xa))))))))))))))"
obua@17644
  1200
  by (import hollight ARITH_ADD)
obua@17644
  1201
obua@17652
  1202
lemma ARITH_MULT: "(op &::bool => bool => bool)
obua@17652
  1203
 ((All::(nat => bool) => bool)
obua@17652
  1204
   (%x::nat.
obua@17652
  1205
       (All::(nat => bool) => bool)
obua@17652
  1206
        (%xa::nat.
obua@17652
  1207
            (op =::nat => nat => bool) ((op *::nat => nat => nat) x xa)
obua@17652
  1208
             ((op *::nat => nat => nat) x xa))))
obua@17652
  1209
 ((op &::bool => bool => bool)
obua@17652
  1210
   ((op =::nat => nat => bool) ((op *::nat => nat => nat) (0::nat) (0::nat))
obua@17652
  1211
     (0::nat))
obua@17652
  1212
   ((op &::bool => bool => bool)
obua@17652
  1213
     ((All::(nat => bool) => bool)
obua@17652
  1214
       (%x::nat.
obua@17652
  1215
           (op =::nat => nat => bool)
obua@17652
  1216
            ((op *::nat => nat => nat) (0::nat)
obua@17652
  1217
              ((NUMERAL_BIT0::nat => nat) x))
obua@17652
  1218
            (0::nat)))
obua@17652
  1219
     ((op &::bool => bool => bool)
obua@17652
  1220
       ((All::(nat => bool) => bool)
obua@17652
  1221
         (%x::nat.
obua@17652
  1222
             (op =::nat => nat => bool)
obua@17652
  1223
              ((op *::nat => nat => nat) (0::nat)
obua@17652
  1224
                ((NUMERAL_BIT1::nat => nat) x))
obua@17652
  1225
              (0::nat)))
obua@17652
  1226
       ((op &::bool => bool => bool)
obua@17652
  1227
         ((All::(nat => bool) => bool)
obua@17652
  1228
           (%x::nat.
obua@17652
  1229
               (op =::nat => nat => bool)
obua@17652
  1230
                ((op *::nat => nat => nat) ((NUMERAL_BIT0::nat => nat) x)
obua@17652
  1231
                  (0::nat))
obua@17652
  1232
                (0::nat)))
obua@17652
  1233
         ((op &::bool => bool => bool)
obua@17652
  1234
           ((All::(nat => bool) => bool)
obua@17652
  1235
             (%x::nat.
obua@17652
  1236
                 (op =::nat => nat => bool)
obua@17652
  1237
                  ((op *::nat => nat => nat) ((NUMERAL_BIT1::nat => nat) x)
obua@17652
  1238
                    (0::nat))
obua@17652
  1239
                  (0::nat)))
obua@17652
  1240
           ((op &::bool => bool => bool)
obua@17652
  1241
             ((All::(nat => bool) => bool)
obua@17652
  1242
               (%x::nat.
obua@17652
  1243
                   (All::(nat => bool) => bool)
obua@17652
  1244
                    (%xa::nat.
obua@17652
  1245
                        (op =::nat => nat => bool)
obua@17652
  1246
                         ((op *::nat => nat => nat)
obua@17652
  1247
                           ((NUMERAL_BIT0::nat => nat) x)
obua@17652
  1248
                           ((NUMERAL_BIT0::nat => nat) xa))
obua@17652
  1249
                         ((NUMERAL_BIT0::nat => nat)
obua@17652
  1250
                           ((NUMERAL_BIT0::nat => nat)
obua@17652
  1251
                             ((op *::nat => nat => nat) x xa))))))
obua@17652
  1252
             ((op &::bool => bool => bool)
obua@17652
  1253
               ((All::(nat => bool) => bool)
obua@17652
  1254
                 (%x::nat.
obua@17652
  1255
                     (All::(nat => bool) => bool)
obua@17652
  1256
                      (%xa::nat.
obua@17652
  1257
                          (op =::nat => nat => bool)
obua@17652
  1258
                           ((op *::nat => nat => nat)
obua@17652
  1259
                             ((NUMERAL_BIT0::nat => nat) x)
obua@17652
  1260
                             ((NUMERAL_BIT1::nat => nat) xa))
obua@17652
  1261
                           ((op +::nat => nat => nat)
obua@17652
  1262
                             ((NUMERAL_BIT0::nat => nat) x)
obua@17652
  1263
                             ((NUMERAL_BIT0::nat => nat)
obua@17652
  1264
                               ((NUMERAL_BIT0::nat => nat)
obua@17652
  1265
                                 ((op *::nat => nat => nat) x xa)))))))
obua@17652
  1266
               ((op &::bool => bool => bool)
obua@17652
  1267
                 ((All::(nat => bool) => bool)
obua@17652
  1268
                   (%x::nat.
obua@17652
  1269
                       (All::(nat => bool) => bool)
obua@17652
  1270
                        (%xa::nat.
obua@17652
  1271
                            (op =::nat => nat => bool)
obua@17652
  1272
                             ((op *::nat => nat => nat)
obua@17652
  1273
                               ((NUMERAL_BIT1::nat => nat) x)
obua@17652
  1274
                               ((NUMERAL_BIT0::nat => nat) xa))
obua@17652
  1275
                             ((op +::nat => nat => nat)
obua@17652
  1276
                               ((NUMERAL_BIT0::nat => nat) xa)
obua@17652
  1277
                               ((NUMERAL_BIT0::nat => nat)
obua@17652
  1278
                                 ((NUMERAL_BIT0::nat => nat)
obua@17652
  1279
                                   ((op *::nat => nat => nat) x xa)))))))
obua@17652
  1280
                 ((All::(nat => bool) => bool)
obua@17652
  1281
                   (%x::nat.
obua@17652
  1282
                       (All::(nat => bool) => bool)
obua@17652
  1283
                        (%xa::nat.
obua@17652
  1284
                            (op =::nat => nat => bool)
obua@17652
  1285
                             ((op *::nat => nat => nat)
obua@17652
  1286
                               ((NUMERAL_BIT1::nat => nat) x)
obua@17652
  1287
                               ((NUMERAL_BIT1::nat => nat) xa))
obua@17652
  1288
                             ((op +::nat => nat => nat)
obua@17652
  1289
                               ((NUMERAL_BIT1::nat => nat) x)
obua@17652
  1290
                               ((op +::nat => nat => nat)
obua@17652
  1291
                                 ((NUMERAL_BIT0::nat => nat) xa)
obua@17652
  1292
                                 ((NUMERAL_BIT0::nat => nat)
obua@17652
  1293
                                   ((NUMERAL_BIT0::nat => nat)
obua@17652
  1294
                                     ((op *::nat => nat => nat) x
obua@17652
  1295
 xa))))))))))))))))"
obua@17644
  1296
  by (import hollight ARITH_MULT)
obua@17644
  1297
obua@17644
  1298
lemma ARITH_EXP: "(ALL (x::nat) xa::nat. EXP x xa = EXP x xa) &
obua@17652
  1299
EXP 0 0 = NUMERAL_BIT1 0 &
obua@17652
  1300
(ALL m::nat. EXP (NUMERAL_BIT0 m) 0 = NUMERAL_BIT1 0) &
obua@17652
  1301
(ALL m::nat. EXP (NUMERAL_BIT1 m) 0 = NUMERAL_BIT1 0) &
obua@17652
  1302
(ALL n::nat. EXP 0 (NUMERAL_BIT0 n) = EXP 0 n * EXP 0 n) &
obua@17644
  1303
(ALL (m::nat) n::nat.
obua@17644
  1304
    EXP (NUMERAL_BIT0 m) (NUMERAL_BIT0 n) =
obua@17644
  1305
    EXP (NUMERAL_BIT0 m) n * EXP (NUMERAL_BIT0 m) n) &
obua@17644
  1306
(ALL (m::nat) n::nat.
obua@17644
  1307
    EXP (NUMERAL_BIT1 m) (NUMERAL_BIT0 n) =
obua@17644
  1308
    EXP (NUMERAL_BIT1 m) n * EXP (NUMERAL_BIT1 m) n) &
obua@17652
  1309
(ALL n::nat. EXP 0 (NUMERAL_BIT1 n) = 0) &
obua@17644
  1310
(ALL (m::nat) n::nat.
obua@17644
  1311
    EXP (NUMERAL_BIT0 m) (NUMERAL_BIT1 n) =
obua@17644
  1312
    NUMERAL_BIT0 m * (EXP (NUMERAL_BIT0 m) n * EXP (NUMERAL_BIT0 m) n)) &
obua@17644
  1313
(ALL (m::nat) n::nat.
obua@17644
  1314
    EXP (NUMERAL_BIT1 m) (NUMERAL_BIT1 n) =
obua@17644
  1315
    NUMERAL_BIT1 m * (EXP (NUMERAL_BIT1 m) n * EXP (NUMERAL_BIT1 m) n))"
obua@17644
  1316
  by (import hollight ARITH_EXP)
obua@17644
  1317
obua@17644
  1318
lemma ARITH_EVEN: "(ALL x::nat. EVEN x = EVEN x) &
obua@17652
  1319
EVEN 0 = True &
obua@17644
  1320
(ALL x::nat. EVEN (NUMERAL_BIT0 x) = True) &
obua@17644
  1321
(ALL x::nat. EVEN (NUMERAL_BIT1 x) = False)"
obua@17644
  1322
  by (import hollight ARITH_EVEN)
obua@17644
  1323
obua@17644
  1324
lemma ARITH_ODD: "(ALL x::nat. ODD x = ODD x) &
obua@17652
  1325
ODD 0 = False &
obua@17644
  1326
(ALL x::nat. ODD (NUMERAL_BIT0 x) = False) &
obua@17644
  1327
(ALL x::nat. ODD (NUMERAL_BIT1 x) = True)"
obua@17644
  1328
  by (import hollight ARITH_ODD)
obua@17644
  1329
obua@17644
  1330
lemma ARITH_LE: "(ALL (x::nat) xa::nat. <= x xa = <= x xa) &
obua@17652
  1331
<= 0 0 = True &
obua@17652
  1332
(ALL x::nat. <= (NUMERAL_BIT0 x) 0 = (x = 0)) &
obua@17652
  1333
(ALL x::nat. <= (NUMERAL_BIT1 x) 0 = False) &
obua@17652
  1334
(ALL x::nat. <= 0 (NUMERAL_BIT0 x) = True) &
obua@17652
  1335
(ALL x::nat. <= 0 (NUMERAL_BIT1 x) = True) &
obua@17644
  1336
(ALL (x::nat) xa::nat. <= (NUMERAL_BIT0 x) (NUMERAL_BIT0 xa) = <= x xa) &
obua@17644
  1337
(ALL (x::nat) xa::nat. <= (NUMERAL_BIT0 x) (NUMERAL_BIT1 xa) = <= x xa) &
obua@17644
  1338
(ALL (x::nat) xa::nat. <= (NUMERAL_BIT1 x) (NUMERAL_BIT0 xa) = < x xa) &
obua@17644
  1339
(ALL (x::nat) xa::nat. <= (NUMERAL_BIT1 x) (NUMERAL_BIT1 xa) = <= x xa)"
obua@17644
  1340
  by (import hollight ARITH_LE)
obua@17644
  1341
obua@17644
  1342
lemma ARITH_LT: "(ALL (x::nat) xa::nat. < x xa = < x xa) &
obua@17652
  1343
< 0 0 = False &
obua@17652
  1344
(ALL x::nat. < (NUMERAL_BIT0 x) 0 = False) &
obua@17652
  1345
(ALL x::nat. < (NUMERAL_BIT1 x) 0 = False) &
obua@17652
  1346
(ALL x::nat. < 0 (NUMERAL_BIT0 x) = < 0 x) &
obua@17652
  1347
(ALL x::nat. < 0 (NUMERAL_BIT1 x) = True) &
obua@17644
  1348
(ALL (x::nat) xa::nat. < (NUMERAL_BIT0 x) (NUMERAL_BIT0 xa) = < x xa) &
obua@17644
  1349
(ALL (x::nat) xa::nat. < (NUMERAL_BIT0 x) (NUMERAL_BIT1 xa) = <= x xa) &
obua@17644
  1350
(ALL (x::nat) xa::nat. < (NUMERAL_BIT1 x) (NUMERAL_BIT0 xa) = < x xa) &
obua@17644
  1351
(ALL (x::nat) xa::nat. < (NUMERAL_BIT1 x) (NUMERAL_BIT1 xa) = < x xa)"
obua@17644
  1352
  by (import hollight ARITH_LT)
obua@17644
  1353
obua@17652
  1354
lemma ARITH_EQ: "(op &::bool => bool => bool)
obua@17652
  1355
 ((All::(nat => bool) => bool)
obua@17652
  1356
   (%x::nat.
obua@17652
  1357
       (All::(nat => bool) => bool)
obua@17652
  1358
        (%xa::nat.
obua@17652
  1359
            (op =::bool => bool => bool) ((op =::nat => nat => bool) x xa)
obua@17652
  1360
             ((op =::nat => nat => bool) x xa))))
obua@17652
  1361
 ((op &::bool => bool => bool)
obua@17652
  1362
   ((op =::bool => bool => bool)
obua@17652
  1363
     ((op =::nat => nat => bool) (0::nat) (0::nat)) (True::bool))
obua@17652
  1364
   ((op &::bool => bool => bool)
obua@17652
  1365
     ((All::(nat => bool) => bool)
obua@17652
  1366
       (%x::nat.
obua@17652
  1367
           (op =::bool => bool => bool)
obua@17652
  1368
            ((op =::nat => nat => bool) ((NUMERAL_BIT0::nat => nat) x)
obua@17652
  1369
              (0::nat))
obua@17652
  1370
            ((op =::nat => nat => bool) x (0::nat))))
obua@17652
  1371
     ((op &::bool => bool => bool)
obua@17652
  1372
       ((All::(nat => bool) => bool)
obua@17652
  1373
         (%x::nat.
obua@17652
  1374
             (op =::bool => bool => bool)
obua@17652
  1375
              ((op =::nat => nat => bool) ((NUMERAL_BIT1::nat => nat) x)
obua@17652
  1376
                (0::nat))
obua@17652
  1377
              (False::bool)))
obua@17652
  1378
       ((op &::bool => bool => bool)
obua@17652
  1379
         ((All::(nat => bool) => bool)
obua@17652
  1380
           (%x::nat.
obua@17652
  1381
               (op =::bool => bool => bool)
obua@17652
  1382
                ((op =::nat => nat => bool) (0::nat)
obua@17652
  1383
                  ((NUMERAL_BIT0::nat => nat) x))
obua@17652
  1384
                ((op =::nat => nat => bool) (0::nat) x)))
obua@17652
  1385
         ((op &::bool => bool => bool)
obua@17652
  1386
           ((All::(nat => bool) => bool)
obua@17652
  1387
             (%x::nat.
obua@17652
  1388
                 (op =::bool => bool => bool)
obua@17652
  1389
                  ((op =::nat => nat => bool) (0::nat)
obua@17652
  1390
                    ((NUMERAL_BIT1::nat => nat) x))
obua@17652
  1391
                  (False::bool)))
obua@17652
  1392
           ((op &::bool => bool => bool)
obua@17652
  1393
             ((All::(nat => bool) => bool)
obua@17652
  1394
               (%x::nat.
obua@17652
  1395
                   (All::(nat => bool) => bool)
obua@17652
  1396
                    (%xa::nat.
obua@17652
  1397
                        (op =::bool => bool => bool)
obua@17652
  1398
                         ((op =::nat => nat => bool)
obua@17652
  1399
                           ((NUMERAL_BIT0::nat => nat) x)
obua@17652
  1400
                           ((NUMERAL_BIT0::nat => nat) xa))
obua@17652
  1401
                         ((op =::nat => nat => bool) x xa))))
obua@17652
  1402
             ((op &::bool => bool => bool)
obua@17652
  1403
               ((All::(nat => bool) => bool)
obua@17652
  1404
                 (%x::nat.
obua@17652
  1405
                     (All::(nat => bool) => bool)
obua@17652
  1406
                      (%xa::nat.
obua@17652
  1407
                          (op =::bool => bool => bool)
obua@17652
  1408
                           ((op =::nat => nat => bool)
obua@17652
  1409
                             ((NUMERAL_BIT0::nat => nat) x)
obua@17652
  1410
                             ((NUMERAL_BIT1::nat => nat) xa))
obua@17652
  1411
                           (False::bool))))
obua@17652
  1412
               ((op &::bool => bool => bool)
obua@17652
  1413
                 ((All::(nat => bool) => bool)
obua@17652
  1414
                   (%x::nat.
obua@17652
  1415
                       (All::(nat => bool) => bool)
obua@17652
  1416
                        (%xa::nat.
obua@17652
  1417
                            (op =::bool => bool => bool)
obua@17652
  1418
                             ((op =::nat => nat => bool)
obua@17652
  1419
                               ((NUMERAL_BIT1::nat => nat) x)
obua@17652
  1420
                               ((NUMERAL_BIT0::nat => nat) xa))
obua@17652
  1421
                             (False::bool))))
obua@17652
  1422
                 ((All::(nat => bool) => bool)
obua@17652
  1423
                   (%x::nat.
obua@17652
  1424
                       (All::(nat => bool) => bool)
obua@17652
  1425
                        (%xa::nat.
obua@17652
  1426
                            (op =::bool => bool => bool)
obua@17652
  1427
                             ((op =::nat => nat => bool)
obua@17652
  1428
                               ((NUMERAL_BIT1::nat => nat) x)
obua@17652
  1429
                               ((NUMERAL_BIT1::nat => nat) xa))
obua@17652
  1430
                             ((op =::nat => nat => bool) x xa))))))))))))"
obua@17644
  1431
  by (import hollight ARITH_EQ)
obua@17644
  1432
obua@17652
  1433
lemma ARITH_SUB: "(op &::bool => bool => bool)
obua@17652
  1434
 ((All::(nat => bool) => bool)
obua@17652
  1435
   (%x::nat.
obua@17652
  1436
       (All::(nat => bool) => bool)
obua@17652
  1437
        (%xa::nat.
obua@17652
  1438
            (op =::nat => nat => bool) ((op -::nat => nat => nat) x xa)
obua@17652
  1439
             ((op -::nat => nat => nat) x xa))))
obua@17652
  1440
 ((op &::bool => bool => bool)
obua@17652
  1441
   ((op =::nat => nat => bool) ((op -::nat => nat => nat) (0::nat) (0::nat))
obua@17652
  1442
     (0::nat))
obua@17652
  1443
   ((op &::bool => bool => bool)
obua@17652
  1444
     ((All::(nat => bool) => bool)
obua@17652
  1445
       (%x::nat.
obua@17652
  1446
           (op =::nat => nat => bool)
obua@17652
  1447
            ((op -::nat => nat => nat) (0::nat)
obua@17652
  1448
              ((NUMERAL_BIT0::nat => nat) x))
obua@17652
  1449
            (0::nat)))
obua@17652
  1450
     ((op &::bool => bool => bool)
obua@17652
  1451
       ((All::(nat => bool) => bool)
obua@17652
  1452
         (%x::nat.
obua@17652
  1453
             (op =::nat => nat => bool)
obua@17652
  1454
              ((op -::nat => nat => nat) (0::nat)
obua@17652
  1455
                ((NUMERAL_BIT1::nat => nat) x))
obua@17652
  1456
              (0::nat)))
obua@17652
  1457
       ((op &::bool => bool => bool)
obua@17652
  1458
         ((All::(nat => bool) => bool)
obua@17652
  1459
           (%x::nat.
obua@17652
  1460
               (op =::nat => nat => bool)
obua@17652
  1461
                ((op -::nat => nat => nat) ((NUMERAL_BIT0::nat => nat) x)
obua@17652
  1462
                  (0::nat))
obua@17652
  1463
                ((NUMERAL_BIT0::nat => nat) x)))
obua@17652
  1464
         ((op &::bool => bool => bool)
obua@17652
  1465
           ((All::(nat => bool) => bool)
obua@17652
  1466
             (%x::nat.
obua@17652
  1467
                 (op =::nat => nat => bool)
obua@17652
  1468
                  ((op -::nat => nat => nat) ((NUMERAL_BIT1::nat => nat) x)
obua@17652
  1469
                    (0::nat))
obua@17652
  1470
                  ((NUMERAL_BIT1::nat => nat) x)))
obua@17652
  1471
           ((op &::bool => bool => bool)
obua@17652
  1472
             ((All::(nat => bool) => bool)
obua@17652
  1473
               (%m::nat.
obua@17652
  1474
                   (All::(nat => bool) => bool)
obua@17652
  1475
                    (%n::nat.
obua@17652
  1476
                        (op =::nat => nat => bool)
obua@17652
  1477
                         ((op -::nat => nat => nat)
obua@17652
  1478
                           ((NUMERAL_BIT0::nat => nat) m)
obua@17652
  1479
                           ((NUMERAL_BIT0::nat => nat) n))
obua@17652
  1480
                         ((NUMERAL_BIT0::nat => nat)
obua@17652
  1481
                           ((op -::nat => nat => nat) m n)))))
obua@17652
  1482
             ((op &::bool => bool => bool)
obua@17652
  1483
               ((All::(nat => bool) => bool)
obua@17652
  1484
                 (%m::nat.
obua@17652
  1485
                     (All::(nat => bool) => bool)
obua@17652
  1486
                      (%n::nat.
obua@17652
  1487
                          (op =::nat => nat => bool)
obua@17652
  1488
                           ((op -::nat => nat => nat)
obua@17652
  1489
                             ((NUMERAL_BIT0::nat => nat) m)
obua@17652
  1490
                             ((NUMERAL_BIT1::nat => nat) n))
obua@17652
  1491
                           ((Pred::nat => nat)
obua@17652
  1492
                             ((NUMERAL_BIT0::nat => nat)
obua@17652
  1493
                               ((op -::nat => nat => nat) m n))))))
obua@17652
  1494
               ((op &::bool => bool => bool)
obua@17652
  1495
                 ((All::(nat => bool) => bool)
obua@17652
  1496
                   (%m::nat.
obua@17652
  1497
                       (All::(nat => bool) => bool)
obua@17652
  1498
                        (%n::nat.
obua@17652
  1499
                            (op =::nat => nat => bool)
obua@17652
  1500
                             ((op -::nat => nat => nat)
obua@17652
  1501
                               ((NUMERAL_BIT1::nat => nat) m)
obua@17652
  1502
                               ((NUMERAL_BIT0::nat => nat) n))
obua@17652
  1503
                             ((COND::bool => nat => nat => nat)
obua@17652
  1504
                               ((<=::nat => nat => bool) n m)
obua@17652
  1505
                               ((NUMERAL_BIT1::nat => nat)
obua@17652
  1506
                                 ((op -::nat => nat => nat) m n))
obua@17652
  1507
                               (0::nat)))))
obua@17652
  1508
                 ((All::(nat => bool) => bool)
obua@17652
  1509
                   (%m::nat.
obua@17652
  1510
                       (All::(nat => bool) => bool)
obua@17652
  1511
                        (%n::nat.
obua@17652
  1512
                            (op =::nat => nat => bool)
obua@17652
  1513
                             ((op -::nat => nat => nat)
obua@17652
  1514
                               ((NUMERAL_BIT1::nat => nat) m)
obua@17652
  1515
                               ((NUMERAL_BIT1::nat => nat) n))
obua@17652
  1516
                             ((NUMERAL_BIT0::nat => nat)
obua@17652
  1517
                               ((op -::nat => nat => nat) m n)))))))))))))"
obua@17644
  1518
  by (import hollight ARITH_SUB)
obua@17644
  1519
obua@17644
  1520
lemma right_th: "(s::nat) * NUMERAL_BIT1 (x::nat) = s + NUMERAL_BIT0 (s * x)"
obua@17644
  1521
  by (import hollight right_th)
obua@17644
  1522
obua@17644
  1523
lemma SEMIRING_PTHS: "(ALL (x::'A::type) (y::'A::type) z::'A::type.
obua@17644
  1524
    (add::'A::type => 'A::type => 'A::type) x (add y z) = add (add x y) z) &
obua@17644
  1525
(ALL (x::'A::type) y::'A::type. add x y = add y x) &
obua@17644
  1526
(ALL x::'A::type. add (r0::'A::type) x = x) &
obua@17644
  1527
(ALL (x::'A::type) (y::'A::type) z::'A::type.
obua@17644
  1528
    (mul::'A::type => 'A::type => 'A::type) x (mul y z) = mul (mul x y) z) &
obua@17644
  1529
(ALL (x::'A::type) y::'A::type. mul x y = mul y x) &
obua@17644
  1530
(ALL x::'A::type. mul (r1::'A::type) x = x) &
obua@17644
  1531
(ALL x::'A::type. mul r0 x = r0) &
obua@17644
  1532
(ALL (x::'A::type) (y::'A::type) z::'A::type.
obua@17644
  1533
    mul x (add y z) = add (mul x y) (mul x z)) &
obua@17652
  1534
(ALL x::'A::type. (pwr::'A::type => nat => 'A::type) x 0 = r1) &
obua@17644
  1535
(ALL (x::'A::type) n::nat. pwr x (Suc n) = mul x (pwr x n)) -->
obua@17644
  1536
mul r1 (x::'A::type) = x &
obua@17644
  1537
add (mul (a::'A::type) (m::'A::type)) (mul (b::'A::type) m) =
obua@17644
  1538
mul (add a b) m &
obua@17644
  1539
add (mul a m) m = mul (add a r1) m &
obua@17644
  1540
add m (mul a m) = mul (add a r1) m &
obua@17644
  1541
add m m = mul (add r1 r1) m &
obua@17644
  1542
mul r0 m = r0 &
obua@17644
  1543
add r0 a = a &
obua@17644
  1544
add a r0 = a &
obua@17644
  1545
mul a b = mul b a &
obua@17644
  1546
mul (add a b) (c::'A::type) = add (mul a c) (mul b c) &
obua@17644
  1547
mul r0 a = r0 &
obua@17644
  1548
mul a r0 = r0 &
obua@17644
  1549
mul r1 a = a &
obua@17644
  1550
mul a r1 = a &
obua@17644
  1551
mul (mul (lx::'A::type) (ly::'A::type))
obua@17644
  1552
 (mul (rx::'A::type) (ry::'A::type)) =
obua@17644
  1553
mul (mul lx rx) (mul ly ry) &
obua@17644
  1554
mul (mul lx ly) (mul rx ry) = mul lx (mul ly (mul rx ry)) &
obua@17644
  1555
mul (mul lx ly) (mul rx ry) = mul rx (mul (mul lx ly) ry) &
obua@17644
  1556
mul (mul lx ly) rx = mul (mul lx rx) ly &
obua@17644
  1557
mul (mul lx ly) rx = mul lx (mul ly rx) &
obua@17644
  1558
mul lx rx = mul rx lx &
obua@17644
  1559
mul lx (mul rx ry) = mul (mul lx rx) ry &
obua@17644
  1560
mul lx (mul rx ry) = mul rx (mul lx ry) &
obua@17644
  1561
add (add a b) (add c (d::'A::type)) = add (add a c) (add b d) &
obua@17644
  1562
add (add a b) c = add a (add b c) &
obua@17644
  1563
add a (add c d) = add c (add a d) &
obua@17644
  1564
add (add a b) c = add (add a c) b &
obua@17644
  1565
add a c = add c a &
obua@17644
  1566
add a (add c d) = add (add a c) d &
obua@17644
  1567
mul (pwr x (p::nat)) (pwr x (q::nat)) = pwr x (p + q) &
obua@17644
  1568
mul x (pwr x q) = pwr x (Suc q) &
obua@17644
  1569
mul (pwr x q) x = pwr x (Suc q) &
obua@17652
  1570
mul x x = pwr x (NUMERAL_BIT0 (NUMERAL_BIT1 0)) &
obua@17644
  1571
pwr (mul x (y::'A::type)) q = mul (pwr x q) (pwr y q) &
obua@17644
  1572
pwr (pwr x p) q = pwr x (p * q) &
obua@17652
  1573
pwr x 0 = r1 &
obua@17652
  1574
pwr x (NUMERAL_BIT1 0) = x &
obua@17644
  1575
mul x (add y (z::'A::type)) = add (mul x y) (mul x z) &
obua@17644
  1576
pwr x (Suc q) = mul x (pwr x q)"
obua@17644
  1577
  by (import hollight SEMIRING_PTHS)
obua@17644
  1578
obua@17644
  1579
lemma sth: "(ALL (x::nat) (y::nat) z::nat. x + (y + z) = x + y + z) &
obua@17644
  1580
(ALL (x::nat) y::nat. x + y = y + x) &
obua@17652
  1581
(ALL x::nat. 0 + x = x) &
obua@17644
  1582
(ALL (x::nat) (y::nat) z::nat. x * (y * z) = x * y * z) &
obua@17644
  1583
(ALL (x::nat) y::nat. x * y = y * x) &
obua@17652
  1584
(ALL x::nat. NUMERAL_BIT1 0 * x = x) &
obua@17652
  1585
(ALL x::nat. 0 * x = 0) &
obua@17644
  1586
(ALL (x::nat) (xa::nat) xb::nat. x * (xa + xb) = x * xa + x * xb) &
obua@17652
  1587
(ALL x::nat. EXP x 0 = NUMERAL_BIT1 0) &
obua@17644
  1588
(ALL (x::nat) xa::nat. EXP x (Suc xa) = x * EXP x xa)"
obua@17644
  1589
  by (import hollight sth)
obua@17644
  1590
obua@17644
  1591
lemma NUM_INTEGRAL_LEMMA: "(w::nat) = (x::nat) + (d::nat) & (y::nat) = (z::nat) + (e::nat) -->
obua@17644
  1592
(w * y + x * z = w * z + x * y) = (w = x | y = z)"
obua@17644
  1593
  by (import hollight NUM_INTEGRAL_LEMMA)
obua@17644
  1594
obua@17652
  1595
lemma NUM_INTEGRAL: "(ALL x::nat. 0 * x = 0) &
obua@17644
  1596
(ALL (x::nat) (xa::nat) xb::nat. (x + xa = x + xb) = (xa = xb)) &
obua@17644
  1597
(ALL (w::nat) (x::nat) (y::nat) z::nat.
obua@17644
  1598
    (w * y + x * z = w * z + x * y) = (w = x | y = z))"
obua@17644
  1599
  by (import hollight NUM_INTEGRAL)
obua@17644
  1600
obua@17644
  1601
lemma INJ_INVERSE2: "ALL P::'A::type => 'B::type => 'C::type.
obua@17644
  1602
   (ALL (x1::'A::type) (y1::'B::type) (x2::'A::type) y2::'B::type.
obua@17644
  1603
       (P x1 y1 = P x2 y2) = (x1 = x2 & y1 = y2)) -->
obua@17644
  1604
   (EX (x::'C::type => 'A::type) Y::'C::type => 'B::type.
obua@17644
  1605
       ALL (xa::'A::type) y::'B::type. x (P xa y) = xa & Y (P xa y) = y)"
obua@17644
  1606
  by (import hollight INJ_INVERSE2)
obua@17644
  1607
obua@17644
  1608
constdefs
obua@17644
  1609
  NUMPAIR :: "nat => nat => nat" 
obua@17644
  1610
  "NUMPAIR ==
obua@17644
  1611
%(u::nat) ua::nat.
obua@17652
  1612
   EXP (NUMERAL_BIT0 (NUMERAL_BIT1 0)) u *
obua@17652
  1613
   (NUMERAL_BIT0 (NUMERAL_BIT1 0) * ua + NUMERAL_BIT1 0)"
obua@17644
  1614
obua@17644
  1615
lemma DEF_NUMPAIR: "NUMPAIR =
obua@17644
  1616
(%(u::nat) ua::nat.
obua@17652
  1617
    EXP (NUMERAL_BIT0 (NUMERAL_BIT1 0)) u *
obua@17652
  1618
    (NUMERAL_BIT0 (NUMERAL_BIT1 0) * ua + NUMERAL_BIT1 0))"
obua@17644
  1619
  by (import hollight DEF_NUMPAIR)
obua@17644
  1620
obua@17644
  1621
lemma NUMPAIR_INJ_LEMMA: "ALL (x::nat) (xa::nat) (xb::nat) xc::nat.
obua@17644
  1622
   NUMPAIR x xa = NUMPAIR xb xc --> x = xb"
obua@17644
  1623
  by (import hollight NUMPAIR_INJ_LEMMA)
obua@17644
  1624
obua@17644
  1625
lemma NUMPAIR_INJ: "ALL (x1::nat) (y1::nat) (x2::nat) y2::nat.
obua@17644
  1626
   (NUMPAIR x1 y1 = NUMPAIR x2 y2) = (x1 = x2 & y1 = y2)"
obua@17644
  1627
  by (import hollight NUMPAIR_INJ)
obua@17644
  1628
obua@17644
  1629
constdefs
obua@17644
  1630
  NUMFST :: "nat => nat" 
obua@17644
  1631
  "NUMFST ==
obua@17644
  1632
SOME X::nat => nat.
obua@17644
  1633
   EX Y::nat => nat.
obua@17644
  1634
      ALL (x::nat) y::nat. X (NUMPAIR x y) = x & Y (NUMPAIR x y) = y"
obua@17644
  1635
obua@17644
  1636
lemma DEF_NUMFST: "NUMFST =
obua@17644
  1637
(SOME X::nat => nat.
obua@17644
  1638
    EX Y::nat => nat.
obua@17644
  1639
       ALL (x::nat) y::nat. X (NUMPAIR x y) = x & Y (NUMPAIR x y) = y)"
obua@17644
  1640
  by (import hollight DEF_NUMFST)
obua@17644
  1641
obua@17644
  1642
constdefs
obua@17644
  1643
  NUMSND :: "nat => nat" 
obua@17644
  1644
  "NUMSND ==
obua@17644
  1645
SOME Y::nat => nat.
obua@17644
  1646
   ALL (x::nat) y::nat. NUMFST (NUMPAIR x y) = x & Y (NUMPAIR x y) = y"
obua@17644
  1647
obua@17644
  1648
lemma DEF_NUMSND: "NUMSND =
obua@17644
  1649
(SOME Y::nat => nat.
obua@17644
  1650
    ALL (x::nat) y::nat. NUMFST (NUMPAIR x y) = x & Y (NUMPAIR x y) = y)"
obua@17644
  1651
  by (import hollight DEF_NUMSND)
obua@17644
  1652
obua@17644
  1653
constdefs
obua@17644
  1654
  NUMSUM :: "bool => nat => nat" 
obua@17644
  1655
  "NUMSUM ==
obua@17644
  1656
%(u::bool) ua::nat.
obua@17652
  1657
   COND u (Suc (NUMERAL_BIT0 (NUMERAL_BIT1 0) * ua))
obua@17652
  1658
    (NUMERAL_BIT0 (NUMERAL_BIT1 0) * ua)"
obua@17644
  1659
obua@17644
  1660
lemma DEF_NUMSUM: "NUMSUM =
obua@17644
  1661
(%(u::bool) ua::nat.
obua@17652
  1662
    COND u (Suc (NUMERAL_BIT0 (NUMERAL_BIT1 0) * ua))
obua@17652
  1663
     (NUMERAL_BIT0 (NUMERAL_BIT1 0) * ua))"
obua@17644
  1664
  by (import hollight DEF_NUMSUM)
obua@17644
  1665
obua@17644
  1666
lemma NUMSUM_INJ: "ALL (b1::bool) (x1::nat) (b2::bool) x2::nat.
obua@17644
  1667
   (NUMSUM b1 x1 = NUMSUM b2 x2) = (b1 = b2 & x1 = x2)"
obua@17644
  1668
  by (import hollight NUMSUM_INJ)
obua@17644
  1669
obua@17644
  1670
constdefs
obua@17644
  1671
  NUMLEFT :: "nat => bool" 
obua@17644
  1672
  "NUMLEFT ==
obua@17644
  1673
SOME X::nat => bool.
obua@17644
  1674
   EX Y::nat => nat.
obua@17644
  1675
      ALL (x::bool) y::nat. X (NUMSUM x y) = x & Y (NUMSUM x y) = y"
obua@17644
  1676
obua@17644
  1677
lemma DEF_NUMLEFT: "NUMLEFT =
obua@17644
  1678
(SOME X::nat => bool.
obua@17644
  1679
    EX Y::nat => nat.
obua@17644
  1680
       ALL (x::bool) y::nat. X (NUMSUM x y) = x & Y (NUMSUM x y) = y)"
obua@17644
  1681
  by (import hollight DEF_NUMLEFT)
obua@17644
  1682
obua@17644
  1683
constdefs
obua@17644
  1684
  NUMRIGHT :: "nat => nat" 
obua@17644
  1685
  "NUMRIGHT ==
obua@17644
  1686
SOME Y::nat => nat.
obua@17644
  1687
   ALL (x::bool) y::nat. NUMLEFT (NUMSUM x y) = x & Y (NUMSUM x y) = y"
obua@17644
  1688
obua@17644
  1689
lemma DEF_NUMRIGHT: "NUMRIGHT =
obua@17644
  1690
(SOME Y::nat => nat.
obua@17644
  1691
    ALL (x::bool) y::nat. NUMLEFT (NUMSUM x y) = x & Y (NUMSUM x y) = y)"
obua@17644
  1692
  by (import hollight DEF_NUMRIGHT)
obua@17644
  1693
obua@17644
  1694
constdefs
obua@17652
  1695
  INJN :: "nat => nat => 'A => bool" 
obua@17644
  1696
  "INJN == %(u::nat) (n::nat) a::'A::type. n = u"
obua@17644
  1697
obua@17644
  1698
lemma DEF_INJN: "INJN = (%(u::nat) (n::nat) a::'A::type. n = u)"
obua@17644
  1699
  by (import hollight DEF_INJN)
obua@17644
  1700
obua@17644
  1701
lemma INJN_INJ: "(All::(nat => bool) => bool)
obua@17644
  1702
 (%n1::nat.
obua@17644
  1703
     (All::(nat => bool) => bool)
obua@17644
  1704
      (%n2::nat.
obua@17644
  1705
          (op =::bool => bool => bool)
obua@17644
  1706
           ((op =::(nat => 'A::type => bool)
obua@17644
  1707
                   => (nat => 'A::type => bool) => bool)
obua@17644
  1708
             ((INJN::nat => nat => 'A::type => bool) n1)
obua@17644
  1709
             ((INJN::nat => nat => 'A::type => bool) n2))
obua@17644
  1710
           ((op =::nat => nat => bool) n1 n2)))"
obua@17644
  1711
  by (import hollight INJN_INJ)
obua@17644
  1712
obua@17644
  1713
constdefs
obua@17652
  1714
  INJA :: "'A => nat => 'A => bool" 
obua@17644
  1715
  "INJA == %(u::'A::type) (n::nat) b::'A::type. b = u"
obua@17644
  1716
obua@17644
  1717
lemma DEF_INJA: "INJA = (%(u::'A::type) (n::nat) b::'A::type. b = u)"
obua@17644
  1718
  by (import hollight DEF_INJA)
obua@17644
  1719
obua@17644
  1720
lemma INJA_INJ: "ALL (a1::'A::type) a2::'A::type. (INJA a1 = INJA a2) = (a1 = a2)"
obua@17644
  1721
  by (import hollight INJA_INJ)
obua@17644
  1722
obua@17644
  1723
constdefs
obua@17652
  1724
  INJF :: "(nat => nat => 'A => bool) => nat => 'A => bool" 
obua@17644
  1725
  "INJF == %(u::nat => nat => 'A::type => bool) n::nat. u (NUMFST n) (NUMSND n)"
obua@17644
  1726
obua@17644
  1727
lemma DEF_INJF: "INJF =
obua@17644
  1728
(%(u::nat => nat => 'A::type => bool) n::nat. u (NUMFST n) (NUMSND n))"
obua@17644
  1729
  by (import hollight DEF_INJF)
obua@17644
  1730
obua@17644
  1731
lemma INJF_INJ: "ALL (f1::nat => nat => 'A::type => bool) f2::nat => nat => 'A::type => bool.
obua@17644
  1732
   (INJF f1 = INJF f2) = (f1 = f2)"
obua@17644
  1733
  by (import hollight INJF_INJ)
obua@17644
  1734
obua@17644
  1735
constdefs
obua@17652
  1736
  INJP :: "(nat => 'A => bool) => (nat => 'A => bool) => nat => 'A => bool" 
obua@17644
  1737
  "INJP ==
obua@17644
  1738
%(u::nat => 'A::type => bool) (ua::nat => 'A::type => bool) (n::nat)
obua@17644
  1739
   a::'A::type. COND (NUMLEFT n) (u (NUMRIGHT n) a) (ua (NUMRIGHT n) a)"
obua@17644
  1740
obua@17644
  1741
lemma DEF_INJP: "INJP =
obua@17644
  1742
(%(u::nat => 'A::type => bool) (ua::nat => 'A::type => bool) (n::nat)
obua@17644
  1743
    a::'A::type. COND (NUMLEFT n) (u (NUMRIGHT n) a) (ua (NUMRIGHT n) a))"
obua@17644
  1744
  by (import hollight DEF_INJP)
obua@17644
  1745
obua@17644
  1746
lemma INJP_INJ: "ALL (f1::nat => 'A::type => bool) (f1'::nat => 'A::type => bool)
obua@17644
  1747
   (f2::nat => 'A::type => bool) f2'::nat => 'A::type => bool.
obua@17644
  1748
   (INJP f1 f2 = INJP f1' f2') = (f1 = f1' & f2 = f2')"
obua@17644
  1749
  by (import hollight INJP_INJ)
obua@17644
  1750
obua@17644
  1751
constdefs
obua@17652
  1752
  ZCONSTR :: "nat => 'A => (nat => nat => 'A => bool) => nat => 'A => bool" 
obua@17644
  1753
  "ZCONSTR ==
obua@17644
  1754
%(u::nat) (ua::'A::type) ub::nat => nat => 'A::type => bool.
obua@17644
  1755
   INJP (INJN (Suc u)) (INJP (INJA ua) (INJF ub))"
obua@17644
  1756
obua@17644
  1757
lemma DEF_ZCONSTR: "ZCONSTR =
obua@17644
  1758
(%(u::nat) (ua::'A::type) ub::nat => nat => 'A::type => bool.
obua@17644
  1759
    INJP (INJN (Suc u)) (INJP (INJA ua) (INJF ub)))"
obua@17644
  1760
  by (import hollight DEF_ZCONSTR)
obua@17644
  1761
obua@17644
  1762
constdefs
obua@17652
  1763
  ZBOT :: "nat => 'A => bool" 
obua@17652
  1764
  "ZBOT == INJP (INJN 0) (SOME z::nat => 'A::type => bool. True)"
obua@17652
  1765
obua@17652
  1766
lemma DEF_ZBOT: "ZBOT = INJP (INJN 0) (SOME z::nat => 'A::type => bool. True)"
obua@17644
  1767
  by (import hollight DEF_ZBOT)
obua@17644
  1768
obua@17644
  1769
lemma ZCONSTR_ZBOT: "ALL (x::nat) (xa::'A::type) xb::nat => nat => 'A::type => bool.
obua@17644
  1770
   ZCONSTR x xa xb ~= ZBOT"
obua@17644
  1771
  by (import hollight ZCONSTR_ZBOT)
obua@17644
  1772
obua@17644
  1773
constdefs
obua@17652
  1774
  ZRECSPACE :: "(nat => 'A => bool) => bool" 
obua@17644
  1775
  "ZRECSPACE ==
obua@17644
  1776
%a::nat => 'A::type => bool.
obua@17644
  1777
   ALL ZRECSPACE'::(nat => 'A::type => bool) => bool.
obua@17644
  1778
      (ALL a::nat => 'A::type => bool.
obua@17644
  1779
          a = ZBOT |
obua@17644
  1780
          (EX (c::nat) (i::'A::type) r::nat => nat => 'A::type => bool.
obua@17644
  1781
              a = ZCONSTR c i r & (ALL n::nat. ZRECSPACE' (r n))) -->
obua@17644
  1782
          ZRECSPACE' a) -->
obua@17644
  1783
      ZRECSPACE' a"
obua@17644
  1784
obua@17644
  1785
lemma DEF_ZRECSPACE: "ZRECSPACE =
obua@17644
  1786
(%a::nat => 'A::type => bool.
obua@17644
  1787
    ALL ZRECSPACE'::(nat => 'A::type => bool) => bool.
obua@17644
  1788
       (ALL a::nat => 'A::type => bool.
obua@17644
  1789
           a = ZBOT |
obua@17644
  1790
           (EX (c::nat) (i::'A::type) r::nat => nat => 'A::type => bool.
obua@17644
  1791
               a = ZCONSTR c i r & (ALL n::nat. ZRECSPACE' (r n))) -->
obua@17644
  1792
           ZRECSPACE' a) -->
obua@17644
  1793
       ZRECSPACE' a)"
obua@17644
  1794
  by (import hollight DEF_ZRECSPACE)
obua@17644
  1795
obua@17644
  1796
typedef (open) ('A) recspace = "(Collect::((nat => 'A::type => bool) => bool)
obua@17644
  1797
          => (nat => 'A::type => bool) set)
obua@17644
  1798
 (ZRECSPACE::(nat => 'A::type => bool) => bool)"  morphisms "_dest_rec" "_mk_rec"
obua@17644
  1799
  apply (rule light_ex_imp_nonempty[where t="ZBOT::nat => 'A::type => bool"])
obua@17644
  1800
  by (import hollight TYDEF_recspace)
obua@17644
  1801
obua@17644
  1802
syntax
obua@17644
  1803
  "_dest_rec" :: _ ("'_dest'_rec")
obua@17644
  1804
obua@17644
  1805
syntax
obua@17644
  1806
  "_mk_rec" :: _ ("'_mk'_rec")
obua@17644
  1807
obua@17644
  1808
lemmas "TYDEF_recspace_@intern" = typedef_hol2hollight 
obua@17652
  1809
  [where a="a :: 'A recspace" and r=r ,
obua@17644
  1810
   OF type_definition_recspace]
obua@17644
  1811
obua@17644
  1812
constdefs
obua@17652
  1813
  BOTTOM :: "'A recspace" 
obua@17652
  1814
  "(op ==::'A::type recspace => 'A::type recspace => prop)
obua@17652
  1815
 (BOTTOM::'A::type recspace)
obua@17652
  1816
 ((_mk_rec::(nat => 'A::type => bool) => 'A::type recspace)
obua@17652
  1817
   (ZBOT::nat => 'A::type => bool))"
obua@17652
  1818
obua@17652
  1819
lemma DEF_BOTTOM: "(op =::'A::type recspace => 'A::type recspace => bool)
obua@17652
  1820
 (BOTTOM::'A::type recspace)
obua@17652
  1821
 ((_mk_rec::(nat => 'A::type => bool) => 'A::type recspace)
obua@17652
  1822
   (ZBOT::nat => 'A::type => bool))"
obua@17644
  1823
  by (import hollight DEF_BOTTOM)
obua@17644
  1824
obua@17644
  1825
constdefs
obua@17652
  1826
  CONSTR :: "nat => 'A => (nat => 'A recspace) => 'A recspace" 
obua@17652
  1827
  "(op ==::(nat => 'A::type => (nat => 'A::type recspace) => 'A::type recspace)
obua@17652
  1828
        => (nat
obua@17652
  1829
            => 'A::type => (nat => 'A::type recspace) => 'A::type recspace)
obua@17652
  1830
           => prop)
obua@17652
  1831
 (CONSTR::nat
obua@17652
  1832
          => 'A::type => (nat => 'A::type recspace) => 'A::type recspace)
obua@17652
  1833
 (%(u::nat) (ua::'A::type) ub::nat => 'A::type recspace.
obua@17652
  1834
     (_mk_rec::(nat => 'A::type => bool) => 'A::type recspace)
obua@17652
  1835
      ((ZCONSTR::nat
obua@17652
  1836
                 => 'A::type
obua@17652
  1837
                    => (nat => nat => 'A::type => bool)
obua@17652
  1838
                       => nat => 'A::type => bool)
obua@17652
  1839
        u ua
obua@17652
  1840
        (%n::nat.
obua@17652
  1841
            (_dest_rec::'A::type recspace => nat => 'A::type => bool)
obua@17652
  1842
             (ub n))))"
obua@17652
  1843
obua@17652
  1844
lemma DEF_CONSTR: "(op =::(nat => 'A::type => (nat => 'A::type recspace) => 'A::type recspace)
obua@17652
  1845
       => (nat
obua@17652
  1846
           => 'A::type => (nat => 'A::type recspace) => 'A::type recspace)
obua@17652
  1847
          => bool)
obua@17652
  1848
 (CONSTR::nat
obua@17652
  1849
          => 'A::type => (nat => 'A::type recspace) => 'A::type recspace)
obua@17652
  1850
 (%(u::nat) (ua::'A::type) ub::nat => 'A::type recspace.
obua@17652
  1851
     (_mk_rec::(nat => 'A::type => bool) => 'A::type recspace)
obua@17652
  1852
      ((ZCONSTR::nat
obua@17652
  1853
                 => 'A::type
obua@17652
  1854
                    => (nat => nat => 'A::type => bool)
obua@17652
  1855
                       => nat => 'A::type => bool)
obua@17652
  1856
        u ua
obua@17652
  1857
        (%n::nat.
obua@17652
  1858
            (_dest_rec::'A::type recspace => nat => 'A::type => bool)
obua@17652
  1859
             (ub n))))"
obua@17644
  1860
  by (import hollight DEF_CONSTR)
obua@17644
  1861
obua@17652
  1862
lemma MK_REC_INJ: "(All::((nat => 'A::type => bool) => bool) => bool)
obua@17652
  1863
 (%x::nat => 'A::type => bool.
obua@17652
  1864
     (All::((nat => 'A::type => bool) => bool) => bool)
obua@17652
  1865
      (%y::nat => 'A::type => bool.
obua@17652
  1866
          (op -->::bool => bool => bool)
obua@17652
  1867
           ((op =::'A::type recspace => 'A::type recspace => bool)
obua@17652
  1868
             ((_mk_rec::(nat => 'A::type => bool) => 'A::type recspace) x)
obua@17652
  1869
             ((_mk_rec::(nat => 'A::type => bool) => 'A::type recspace) y))
obua@17652
  1870
           ((op -->::bool => bool => bool)
obua@17652
  1871
             ((op &::bool => bool => bool)
obua@17652
  1872
               ((ZRECSPACE::(nat => 'A::type => bool) => bool) x)
obua@17652
  1873
               ((ZRECSPACE::(nat => 'A::type => bool) => bool) y))
obua@17652
  1874
             ((op =::(nat => 'A::type => bool)
obua@17652
  1875
                     => (nat => 'A::type => bool) => bool)
obua@17652
  1876
               x y))))"
obua@17644
  1877
  by (import hollight MK_REC_INJ)
obua@17644
  1878
obua@17644
  1879
lemma CONSTR_BOT: "ALL (c::nat) (i::'A::type) r::nat => 'A::type recspace.
obua@17644
  1880
   CONSTR c i r ~= BOTTOM"
obua@17644
  1881
  by (import hollight CONSTR_BOT)
obua@17644
  1882
obua@17644
  1883
lemma CONSTR_INJ: "ALL (c1::nat) (i1::'A::type) (r1::nat => 'A::type recspace) (c2::nat)
obua@17644
  1884
   (i2::'A::type) r2::nat => 'A::type recspace.
obua@17644
  1885
   (CONSTR c1 i1 r1 = CONSTR c2 i2 r2) = (c1 = c2 & i1 = i2 & r1 = r2)"
obua@17644
  1886
  by (import hollight CONSTR_INJ)
obua@17644
  1887
obua@17644
  1888
lemma CONSTR_IND: "ALL P::'A::type recspace => bool.
obua@17644
  1889
   P BOTTOM &
obua@17644
  1890
   (ALL (c::nat) (i::'A::type) r::nat => 'A::type recspace.
obua@17644
  1891
       (ALL n::nat. P (r n)) --> P (CONSTR c i r)) -->
obua@17644
  1892
   All P"
obua@17644
  1893
  by (import hollight CONSTR_IND)
obua@17644
  1894
obua@17644
  1895
lemma CONSTR_REC: "ALL Fn::nat
obua@17644
  1896
        => 'A::type
obua@17644
  1897
           => (nat => 'A::type recspace) => (nat => 'B::type) => 'B::type.
obua@17644
  1898
   EX f::'A::type recspace => 'B::type.
obua@17644
  1899
      ALL (c::nat) (i::'A::type) r::nat => 'A::type recspace.
obua@17644
  1900
         f (CONSTR c i r) = Fn c i r (%n::nat. f (r n))"
obua@17644
  1901
  by (import hollight CONSTR_REC)
obua@17644
  1902
obua@17644
  1903
constdefs
obua@17652
  1904
  FCONS :: "'A => (nat => 'A) => nat => 'A" 
obua@17644
  1905
  "FCONS ==
obua@17644
  1906
SOME FCONS::'A::type => (nat => 'A::type) => nat => 'A::type.
obua@17652
  1907
   (ALL (a::'A::type) f::nat => 'A::type. FCONS a f 0 = a) &
obua@17644
  1908
   (ALL (a::'A::type) (f::nat => 'A::type) n::nat. FCONS a f (Suc n) = f n)"
obua@17644
  1909
obua@17644
  1910
lemma DEF_FCONS: "FCONS =
obua@17644
  1911
(SOME FCONS::'A::type => (nat => 'A::type) => nat => 'A::type.
obua@17652
  1912
    (ALL (a::'A::type) f::nat => 'A::type. FCONS a f 0 = a) &
obua@17644
  1913
    (ALL (a::'A::type) (f::nat => 'A::type) n::nat.
obua@17644
  1914
        FCONS a f (Suc n) = f n))"
obua@17644
  1915
  by (import hollight DEF_FCONS)
obua@17644
  1916
obua@17652
  1917
lemma FCONS_UNDO: "ALL f::nat => 'A::type. f = FCONS (f 0) (f o Suc)"
obua@17644
  1918
  by (import hollight FCONS_UNDO)
obua@17644
  1919
obua@17644
  1920
constdefs
obua@17652
  1921
  FNIL :: "nat => 'A" 
obua@17644
  1922
  "FNIL == %u::nat. SOME x::'A::type. True"
obua@17644
  1923
obua@17644
  1924
lemma DEF_FNIL: "FNIL = (%u::nat. SOME x::'A::type. True)"
obua@17644
  1925
  by (import hollight DEF_FNIL)
obua@17644
  1926
obua@17644
  1927
typedef (open) ('A, 'B) sum = "(Collect::(('A::type * 'B::type) recspace => bool)
obua@17644
  1928
          => ('A::type * 'B::type) recspace set)
obua@17644
  1929
 (%a::('A::type * 'B::type) recspace.
obua@17644
  1930
     (All::((('A::type * 'B::type) recspace => bool) => bool) => bool)
obua@17644
  1931
      (%sum'::('A::type * 'B::type) recspace => bool.
obua@17644
  1932
          (op -->::bool => bool => bool)
obua@17644
  1933
           ((All::(('A::type * 'B::type) recspace => bool) => bool)
obua@17644
  1934
             (%a::('A::type * 'B::type) recspace.
obua@17644
  1935
                 (op -->::bool => bool => bool)
obua@17644
  1936
                  ((op |::bool => bool => bool)
obua@17644
  1937
                    ((Ex::('A::type => bool) => bool)
obua@17644
  1938
                      (%aa::'A::type.
obua@17644
  1939
                          (op =::('A::type * 'B::type) recspace
obua@17644
  1940
                                 => ('A::type * 'B::type) recspace => bool)
obua@17644
  1941
                           a ((CONSTR::nat
obua@17644
  1942
 => 'A::type * 'B::type
obua@17644
  1943
    => (nat => ('A::type * 'B::type) recspace)
obua@17644
  1944
       => ('A::type * 'B::type) recspace)
obua@17644
  1945
                               ((NUMERAL::nat => nat) (0::nat))
obua@17644
  1946
                               ((Pair::'A::type
obua@17644
  1947
 => 'B::type => 'A::type * 'B::type)
obua@17644
  1948
                                 aa ((Eps::('B::type => bool) => 'B::type)
obua@17644
  1949
(%v::'B::type. True::bool)))
obua@17644
  1950
                               (%n::nat.
obua@17644
  1951
                                   BOTTOM::('A::type *
obua@17644
  1952
      'B::type) recspace))))
obua@17644
  1953
                    ((Ex::('B::type => bool) => bool)
obua@17644
  1954
                      (%aa::'B::type.
obua@17644
  1955
                          (op =::('A::type * 'B::type) recspace
obua@17644
  1956
                                 => ('A::type * 'B::type) recspace => bool)
obua@17644
  1957
                           a ((CONSTR::nat
obua@17644
  1958
 => 'A::type * 'B::type
obua@17644
  1959
    => (nat => ('A::type * 'B::type) recspace)
obua@17644
  1960
       => ('A::type * 'B::type) recspace)
obua@17644
  1961
                               ((Suc::nat => nat)
obua@17644
  1962
                                 ((NUMERAL::nat => nat) (0::nat)))
obua@17644
  1963
                               ((Pair::'A::type
obua@17644
  1964
 => 'B::type => 'A::type * 'B::type)
obua@17644
  1965
                                 ((Eps::('A::type => bool) => 'A::type)
obua@17644
  1966
                                   (%v::'A::type. True::bool))
obua@17644
  1967
                                 aa)
obua@17644
  1968
                               (%n::nat.
obua@17644
  1969
                                   BOTTOM::('A::type *
obua@17644
  1970
      'B::type) recspace)))))
obua@17644
  1971
                  (sum' a)))
obua@17644
  1972
           (sum' a)))"  morphisms "_dest_sum" "_mk_sum"
obua@17644
  1973
  apply (rule light_ex_imp_nonempty[where t="(CONSTR::nat
obua@17644
  1974
         => 'A::type * 'B::type
obua@17644
  1975
            => (nat => ('A::type * 'B::type) recspace)
obua@17644
  1976
               => ('A::type * 'B::type) recspace)
obua@17644
  1977
 ((NUMERAL::nat => nat) (0::nat))
obua@17644
  1978
 ((Pair::'A::type => 'B::type => 'A::type * 'B::type) (a::'A::type)
obua@17644
  1979
   ((Eps::('B::type => bool) => 'B::type) (%v::'B::type. True::bool)))
obua@17644
  1980
 (%n::nat. BOTTOM::('A::type * 'B::type) recspace)"])
obua@17644
  1981
  by (import hollight TYDEF_sum)
obua@17644
  1982
obua@17644
  1983
syntax
obua@17644
  1984
  "_dest_sum" :: _ ("'_dest'_sum")
obua@17644
  1985
obua@17644
  1986
syntax
obua@17644
  1987
  "_mk_sum" :: _ ("'_mk'_sum")
obua@17644
  1988
obua@17644
  1989
lemmas "TYDEF_sum_@intern" = typedef_hol2hollight 
obua@17652
  1990
  [where a="a :: ('A, 'B) sum" and r=r ,
obua@17644
  1991
   OF type_definition_sum]
obua@17644
  1992
obua@17644
  1993
constdefs
obua@17652
  1994
  INL :: "'A => ('A, 'B) sum" 
obua@17652
  1995
  "(op ==::('A::type => ('A::type, 'B::type) sum)
obua@17652
  1996
        => ('A::type => ('A::type, 'B::type) sum) => prop)
obua@17652
  1997
 (INL::'A::type => ('A::type, 'B::type) sum)
obua@17652
  1998
 (%a::'A::type.
obua@17652
  1999
     (_mk_sum::('A::type * 'B::type) recspace => ('A::type, 'B::type) sum)
obua@17652
  2000
      ((CONSTR::nat
obua@17652
  2001
                => 'A::type * 'B::type
obua@17652
  2002
                   => (nat => ('A::type * 'B::type) recspace)
obua@17652
  2003
                      => ('A::type * 'B::type) recspace)
obua@17652
  2004
        (0::nat)
obua@17652
  2005
        ((Pair::'A::type => 'B::type => 'A::type * 'B::type) a
obua@17652
  2006
          ((Eps::('B::type => bool) => 'B::type)
obua@17652
  2007
            (%v::'B::type. True::bool)))
obua@17652
  2008
        (%n::nat. BOTTOM::('A::type * 'B::type) recspace)))"
obua@17652
  2009
obua@17652
  2010
lemma DEF_INL: "(op =::('A::type => ('A::type, 'B::type) sum)
obua@17652
  2011
       => ('A::type => ('A::type, 'B::type) sum) => bool)
obua@17652
  2012
 (INL::'A::type => ('A::type, 'B::type) sum)
obua@17652
  2013
 (%a::'A::type.
obua@17652
  2014
     (_mk_sum::('A::type * 'B::type) recspace => ('A::type, 'B::type) sum)
obua@17652
  2015
      ((CONSTR::nat
obua@17652
  2016
                => 'A::type * 'B::type
obua@17652
  2017
                   => (nat => ('A::type * 'B::type) recspace)
obua@17652
  2018
                      => ('A::type * 'B::type) recspace)
obua@17652
  2019
        (0::nat)
obua@17652
  2020
        ((Pair::'A::type => 'B::type => 'A::type * 'B::type) a
obua@17652
  2021
          ((Eps::('B::type => bool) => 'B::type)
obua@17652
  2022
            (%v::'B::type. True::bool)))
obua@17652
  2023
        (%n::nat. BOTTOM::('A::type * 'B::type) recspace)))"
obua@17644
  2024
  by (import hollight DEF_INL)
obua@17644
  2025
obua@17644
  2026
constdefs
obua@17652
  2027
  INR :: "'B => ('A, 'B) sum" 
obua@17652
  2028
  "(op ==::('B::type => ('A::type, 'B::type) sum)
obua@17652
  2029
        => ('B::type => ('A::type, 'B::type) sum) => prop)
obua@17652
  2030
 (INR::'B::type => ('A::type, 'B::type) sum)
obua@17652
  2031
 (%a::'B::type.
obua@17652
  2032
     (_mk_sum::('A::type * 'B::type) recspace => ('A::type, 'B::type) sum)
obua@17652
  2033
      ((CONSTR::nat
obua@17652
  2034
                => 'A::type * 'B::type
obua@17652
  2035
                   => (nat => ('A::type * 'B::type) recspace)
obua@17652
  2036
                      => ('A::type * 'B::type) recspace)
obua@17652
  2037
        ((Suc::nat => nat) (0::nat))
obua@17652
  2038
        ((Pair::'A::type => 'B::type => 'A::type * 'B::type)
obua@17652
  2039
          ((Eps::('A::type => bool) => 'A::type) (%v::'A::type. True::bool))
obua@17652
  2040
          a)
obua@17652
  2041
        (%n::nat. BOTTOM::('A::type * 'B::type) recspace)))"
obua@17652
  2042
obua@17652
  2043
lemma DEF_INR: "(op =::('B::type => ('A::type, 'B::type) sum)
obua@17652
  2044
       => ('B::type => ('A::type, 'B::type) sum) => bool)
obua@17652
  2045
 (INR::'B::type => ('A::type, 'B::type) sum)
obua@17652
  2046
 (%a::'B::type.
obua@17652
  2047
     (_mk_sum::('A::type * 'B::type) recspace => ('A::type, 'B::type) sum)
obua@17652
  2048
      ((CONSTR::nat
obua@17652
  2049
                => 'A::type * 'B::type
obua@17652
  2050
                   => (nat => ('A::type * 'B::type) recspace)
obua@17652
  2051
                      => ('A::type * 'B::type) recspace)
obua@17652
  2052
        ((Suc::nat => nat) (0::nat))
obua@17652
  2053
        ((Pair::'A::type => 'B::type => 'A::type * 'B::type)
obua@17652
  2054
          ((Eps::('A::type => bool) => 'A::type) (%v::'A::type. True::bool))
obua@17652
  2055
          a)
obua@17652
  2056
        (%n::nat. BOTTOM::('A::type * 'B::type) recspace)))"
obua@17644
  2057
  by (import hollight DEF_INR)
obua@17644
  2058
obua@17644
  2059
consts
obua@17652
  2060
  OUTL :: "('A, 'B) sum => 'A" 
obua@17644
  2061
obua@17644
  2062
defs
obua@17644
  2063
  OUTL_def: "hollight.OUTL ==
obua@17644
  2064
SOME OUTL::('A::type, 'B::type) sum => 'A::type.
obua@17644
  2065
   ALL x::'A::type. OUTL (INL x) = x"
obua@17644
  2066
obua@17644
  2067
lemma DEF_OUTL: "hollight.OUTL =
obua@17644
  2068
(SOME OUTL::('A::type, 'B::type) sum => 'A::type.
obua@17644
  2069
    ALL x::'A::type. OUTL (INL x) = x)"
obua@17644
  2070
  by (import hollight DEF_OUTL)
obua@17644
  2071
obua@17644
  2072
consts
obua@17652
  2073
  OUTR :: "('A, 'B) sum => 'B" 
obua@17644
  2074
obua@17644
  2075
defs
obua@17644
  2076
  OUTR_def: "hollight.OUTR ==
obua@17644
  2077
SOME OUTR::('A::type, 'B::type) sum => 'B::type.
obua@17644
  2078
   ALL y::'B::type. OUTR (INR y) = y"
obua@17644
  2079
obua@17644
  2080
lemma DEF_OUTR: "hollight.OUTR =
obua@17644
  2081
(SOME OUTR::('A::type, 'B::type) sum => 'B::type.
obua@17644
  2082
    ALL y::'B::type. OUTR (INR y) = y)"
obua@17644
  2083
  by (import hollight DEF_OUTR)
obua@17644
  2084
obua@17644
  2085
typedef (open) ('A) option = "(Collect::('A::type recspace => bool) => 'A::type recspace set)
obua@17644
  2086
 (%a::'A::type recspace.
obua@17644
  2087
     (All::(('A::type recspace => bool) => bool) => bool)
obua@17644
  2088
      (%option'::'A::type recspace => bool.
obua@17644
  2089
          (op -->::bool => bool => bool)
obua@17644
  2090
           ((All::('A::type recspace => bool) => bool)
obua@17644
  2091
             (%a::'A::type recspace.
obua@17644
  2092
                 (op -->::bool => bool => bool)
obua@17644
  2093
                  ((op |::bool => bool => bool)
obua@17644
  2094
                    ((op =::'A::type recspace => 'A::type recspace => bool)
obua@17644
  2095
                      a ((CONSTR::nat
obua@17644
  2096
                                  => 'A::type
obua@17644
  2097
                                     => (nat => 'A::type recspace)
obua@17644
  2098
  => 'A::type recspace)
obua@17644
  2099
                          ((NUMERAL::nat => nat) (0::nat))
obua@17644
  2100
                          ((Eps::('A::type => bool) => 'A::type)
obua@17644
  2101
                            (%v::'A::type. True::bool))
obua@17644
  2102
                          (%n::nat. BOTTOM::'A::type recspace)))
obua@17644
  2103
                    ((Ex::('A::type => bool) => bool)
obua@17644
  2104
                      (%aa::'A::type.
obua@17644
  2105
                          (op =::'A::type recspace
obua@17644
  2106
                                 => 'A::type recspace => bool)
obua@17644
  2107
                           a ((CONSTR::nat
obua@17644
  2108
 => 'A::type => (nat => 'A::type recspace) => 'A::type recspace)
obua@17644
  2109
                               ((Suc::nat => nat)
obua@17644
  2110
                                 ((NUMERAL::nat => nat) (0::nat)))
obua@17644
  2111
                               aa (%n::nat. BOTTOM::'A::type recspace)))))
obua@17644
  2112
                  (option' a)))
obua@17644
  2113
           (option' a)))"  morphisms "_dest_option" "_mk_option"
obua@17644
  2114
  apply (rule light_ex_imp_nonempty[where t="(CONSTR::nat => 'A::type => (nat => 'A::type recspace) => 'A::type recspace)
obua@17644
  2115
 ((NUMERAL::nat => nat) (0::nat))
obua@17644
  2116
 ((Eps::('A::type => bool) => 'A::type) (%v::'A::type. True::bool))
obua@17644
  2117
 (%n::nat. BOTTOM::'A::type recspace)"])
obua@17644
  2118
  by (import hollight TYDEF_option)
obua@17644
  2119
obua@17644
  2120
syntax
obua@17644
  2121
  "_dest_option" :: _ ("'_dest'_option")
obua@17644
  2122
obua@17644
  2123
syntax
obua@17644
  2124
  "_mk_option" :: _ ("'_mk'_option")
obua@17644
  2125
obua@17644
  2126
lemmas "TYDEF_option_@intern" = typedef_hol2hollight 
obua@17652
  2127
  [where a="a :: 'A hollight.option" and r=r ,
obua@17644
  2128
   OF type_definition_option]
obua@17644
  2129
obua@17644
  2130
constdefs
obua@17652
  2131
  NONE :: "'A hollight.option" 
obua@17652
  2132
  "(op ==::'A::type hollight.option => 'A::type hollight.option => prop)
obua@17652
  2133
 (NONE::'A::type hollight.option)
obua@17652
  2134
 ((_mk_option::'A::type recspace => 'A::type hollight.option)
obua@17652
  2135
   ((CONSTR::nat
obua@17652
  2136
             => 'A::type => (nat => 'A::type recspace) => 'A::type recspace)
obua@17652
  2137
     (0::nat)
obua@17652
  2138
     ((Eps::('A::type => bool) => 'A::type) (%v::'A::type. True::bool))
obua@17652
  2139
     (%n::nat. BOTTOM::'A::type recspace)))"
obua@17652
  2140
obua@17652
  2141
lemma DEF_NONE: "(op =::'A::type hollight.option => 'A::type hollight.option => bool)
obua@17652
  2142
 (NONE::'A::type hollight.option)
obua@17652
  2143
 ((_mk_option::'A::type recspace => 'A::type hollight.option)
obua@17652
  2144
   ((CONSTR::nat
obua@17652
  2145
             => 'A::type => (nat => 'A::type recspace) => 'A::type recspace)
obua@17652
  2146
     (0::nat)
obua@17652
  2147
     ((Eps::('A::type => bool) => 'A::type) (%v::'A::type. True::bool))
obua@17652
  2148
     (%n::nat. BOTTOM::'A::type recspace)))"
obua@17644
  2149
  by (import hollight DEF_NONE)
obua@17644
  2150
obua@17644
  2151
consts
obua@17652
  2152
  SOME :: "'A => 'A hollight.option" ("SOME")
obua@17644
  2153
obua@17644
  2154
defs
obua@17652
  2155
  SOME_def: "(op ==::('A::type => 'A::type hollight.option)
obua@17652
  2156
        => ('A::type => 'A::type hollight.option) => prop)
obua@17652
  2157
 (SOME::'A::type => 'A::type hollight.option)
obua@17652
  2158
 (%a::'A::type.
obua@17652
  2159
     (_mk_option::'A::type recspace => 'A::type hollight.option)
obua@17652
  2160
      ((CONSTR::nat
obua@17652
  2161
                => 'A::type
obua@17652
  2162
                   => (nat => 'A::type recspace) => 'A::type recspace)
obua@17652
  2163
        ((Suc::nat => nat) (0::nat)) a
obua@17652
  2164
        (%n::nat. BOTTOM::'A::type recspace)))"
obua@17652
  2165
obua@17652
  2166
lemma DEF_SOME: "(op =::('A::type => 'A::type hollight.option)
obua@17652
  2167
       => ('A::type => 'A::type hollight.option) => bool)
obua@17652
  2168
 (SOME::'A::type => 'A::type hollight.option)
obua@17652
  2169
 (%a::'A::type.
obua@17652
  2170
     (_mk_option::'A::type recspace => 'A::type hollight.option)
obua@17652
  2171
      ((CONSTR::nat
obua@17652
  2172
                => 'A::type
obua@17652
  2173
                   => (nat => 'A::type recspace) => 'A::type recspace)
obua@17652
  2174
        ((Suc::nat => nat) (0::nat)) a
obua@17652
  2175
        (%n::nat. BOTTOM::'A::type recspace)))"
obua@17644
  2176
  by (import hollight DEF_SOME)
obua@17644
  2177
obua@17644
  2178
typedef (open) ('A) list = "(Collect::('A::type recspace => bool) => 'A::type recspace set)
obua@17644
  2179
 (%a::'A::type recspace.
obua@17644
  2180
     (All::(('A::type recspace => bool) => bool) => bool)
obua@17644
  2181
      (%list'::'A::type recspace => bool.
obua@17644
  2182
          (op -->::bool => bool => bool)
obua@17644
  2183
           ((All::('A::type recspace => bool) => bool)
obua@17644
  2184
             (%a::'A::type recspace.
obua@17644
  2185
                 (op -->::bool => bool => bool)
obua@17644
  2186
                  ((op |::bool => bool => bool)
obua@17644
  2187
                    ((op =::'A::type recspace => 'A::type recspace => bool)
obua@17644
  2188
                      a ((CONSTR::nat
obua@17644
  2189
                                  => 'A::type
obua@17644
  2190
                                     => (nat => 'A::type recspace)
obua@17644
  2191
  => 'A::type recspace)
obua@17644
  2192
                          ((NUMERAL::nat => nat) (0::nat))
obua@17644
  2193
                          ((Eps::('A::type => bool) => 'A::type)
obua@17644
  2194
                            (%v::'A::type. True::bool))
obua@17644
  2195
                          (%n::nat. BOTTOM::'A::type recspace)))
obua@17644
  2196
                    ((Ex::('A::type => bool) => bool)
obua@17644
  2197
                      (%a0::'A::type.
obua@17644
  2198
                          (Ex::('A::type recspace => bool) => bool)
obua@17644
  2199
                           (%a1::'A::type recspace.
obua@17644
  2200
                               (op &::bool => bool => bool)
obua@17644
  2201
                                ((op =::'A::type recspace
obua@17644
  2202
  => 'A::type recspace => bool)
obua@17644
  2203
                                  a ((CONSTR::nat
obua@17644
  2204
        => 'A::type => (nat => 'A::type recspace) => 'A::type recspace)
obua@17644
  2205
((Suc::nat => nat) ((NUMERAL::nat => nat) (0::nat))) a0
obua@17644
  2206
((FCONS::'A::type recspace
obua@17644
  2207
         => (nat => 'A::type recspace) => nat => 'A::type recspace)
obua@17644
  2208
  a1 (%n::nat. BOTTOM::'A::type recspace))))
obua@17644
  2209
                                (list' a1)))))
obua@17644
  2210
                  (list' a)))
obua@17644
  2211
           (list' a)))"  morphisms "_dest_list" "_mk_list"
obua@17644
  2212
  apply (rule light_ex_imp_nonempty[where t="(CONSTR::nat => 'A::type => (nat => 'A::type recspace) => 'A::type recspace)
obua@17644
  2213
 ((NUMERAL::nat => nat) (0::nat))
obua@17644
  2214
 ((Eps::('A::type => bool) => 'A::type) (%v::'A::type. True::bool))
obua@17644
  2215
 (%n::nat. BOTTOM::'A::type recspace)"])
obua@17644
  2216
  by (import hollight TYDEF_list)
obua@17644
  2217
obua@17644
  2218
syntax
obua@17644
  2219
  "_dest_list" :: _ ("'_dest'_list")
obua@17644
  2220
obua@17644
  2221
syntax
obua@17644
  2222
  "_mk_list" :: _ ("'_mk'_list")
obua@17644
  2223
obua@17644
  2224
lemmas "TYDEF_list_@intern" = typedef_hol2hollight 
obua@17652
  2225
  [where a="a :: 'A hollight.list" and r=r ,
obua@17644
  2226
   OF type_definition_list]
obua@17644
  2227
obua@17644
  2228
constdefs
obua@17652
  2229
  NIL :: "'A hollight.list" 
obua@17652
  2230
  "(op ==::'A::type hollight.list => 'A::type hollight.list => prop)
obua@17652
  2231
 (NIL::'A::type hollight.list)
obua@17652
  2232
 ((_mk_list::'A::type recspace => 'A::type hollight.list)
obua@17652
  2233
   ((CONSTR::nat
obua@17652
  2234
             => 'A::type => (nat => 'A::type recspace) => 'A::type recspace)
obua@17652
  2235
     (0::nat)
obua@17652
  2236
     ((Eps::('A::type => bool) => 'A::type) (%v::'A::type. True::bool))
obua@17652
  2237
     (%n::nat. BOTTOM::'A::type recspace)))"
obua@17652
  2238
obua@17652
  2239
lemma DEF_NIL: "(op =::'A::type hollight.list => 'A::type hollight.list => bool)
obua@17652
  2240
 (NIL::'A::type hollight.list)
obua@17652
  2241
 ((_mk_list::'A::type recspace => 'A::type hollight.list)
obua@17652
  2242
   ((CONSTR::nat
obua@17652
  2243
             => 'A::type => (nat => 'A::type recspace) => 'A::type recspace)
obua@17652
  2244
     (0::nat)
obua@17652
  2245
     ((Eps::('A::type => bool) => 'A::type) (%v::'A::type. True::bool))
obua@17652
  2246
     (%n::nat. BOTTOM::'A::type recspace)))"
obua@17644
  2247
  by (import hollight DEF_NIL)
obua@17644
  2248
obua@17644
  2249
constdefs
obua@17652
  2250
  CONS :: "'A => 'A hollight.list => 'A hollight.list" 
obua@17652
  2251
  "(op ==::('A::type => 'A::type hollight.list => 'A::type hollight.list)
obua@17652
  2252
        => ('A::type => 'A::type hollight.list => 'A::type hollight.list)
obua@17652
  2253
           => prop)
obua@17652
  2254
 (CONS::'A::type => 'A::type hollight.list => 'A::type hollight.list)
obua@17652
  2255
 (%(a0::'A::type) a1::'A::type hollight.list.
obua@17652
  2256
     (_mk_list::'A::type recspace => 'A::type hollight.list)
obua@17652
  2257
      ((CONSTR::nat
obua@17652
  2258
                => 'A::type
obua@17652
  2259
                   => (nat => 'A::type recspace) => 'A::type recspace)
obua@17652
  2260
        ((Suc::nat => nat) (0::nat)) a0
obua@17652
  2261
        ((FCONS::'A::type recspace
obua@17652
  2262
                 => (nat => 'A::type recspace) => nat => 'A::type recspace)
obua@17652
  2263
          ((_dest_list::'A::type hollight.list => 'A::type recspace) a1)
obua@17652
  2264
          (%n::nat. BOTTOM::'A::type recspace))))"
obua@17652
  2265
obua@17652
  2266
lemma DEF_CONS: "(op =::('A::type => 'A::type hollight.list => 'A::type hollight.list)
obua@17652
  2267
       => ('A::type => 'A::type hollight.list => 'A::type hollight.list)
obua@17652
  2268
          => bool)
obua@17652
  2269
 (CONS::'A::type => 'A::type hollight.list => 'A::type hollight.list)
obua@17652
  2270
 (%(a0::'A::type) a1::'A::type hollight.list.
obua@17652
  2271
     (_mk_list::'A::type recspace => 'A::type hollight.list)
obua@17652
  2272
      ((CONSTR::nat
obua@17652
  2273
                => 'A::type
obua@17652
  2274
                   => (nat => 'A::type recspace) => 'A::type recspace)
obua@17652
  2275
        ((Suc::nat => nat) (0::nat)) a0
obua@17652
  2276
        ((FCONS::'A::type recspace
obua@17652
  2277
                 => (nat => 'A::type recspace) => nat => 'A::type recspace)
obua@17652
  2278
          ((_dest_list::'A::type hollight.list => 'A::type recspace) a1)
obua@17652
  2279
          (%n::nat. BOTTOM::'A::type recspace))))"
obua@17644
  2280
  by (import hollight DEF_CONS)
obua@17644
  2281
obua@17644
  2282
lemma pair_RECURSION: "ALL PAIR'::'A::type => 'B::type => 'C::type.
obua@17644
  2283
   EX x::'A::type * 'B::type => 'C::type.
obua@17644
  2284
      ALL (a0::'A::type) a1::'B::type. x (a0, a1) = PAIR' a0 a1"
obua@17644
  2285
  by (import hollight pair_RECURSION)
obua@17644
  2286
obua@17644
  2287
lemma num_RECURSION_STD: "ALL (e::'Z::type) f::nat => 'Z::type => 'Z::type.
obua@17652
  2288
   EX fn::nat => 'Z::type. fn 0 = e & (ALL n::nat. fn (Suc n) = f n (fn n))"
obua@17644
  2289
  by (import hollight num_RECURSION_STD)
obua@17644
  2290
obua@17644
  2291
constdefs
obua@17652
  2292
  ISO :: "('A => 'B) => ('B => 'A) => bool" 
obua@17644
  2293
  "ISO ==
obua@17644
  2294
%(u::'A::type => 'B::type) ua::'B::type => 'A::type.
obua@17644
  2295
   (ALL x::'B::type. u (ua x) = x) & (ALL y::'A::type. ua (u y) = y)"
obua@17644
  2296
obua@17644
  2297
lemma DEF_ISO: "ISO =
obua@17644
  2298
(%(u::'A::type => 'B::type) ua::'B::type => 'A::type.
obua@17644
  2299
    (ALL x::'B::type. u (ua x) = x) & (ALL y::'A::type. ua (u y) = y))"
obua@17644
  2300
  by (import hollight DEF_ISO)
obua@17644
  2301
obua@17644
  2302
lemma ISO_REFL: "ISO (%x::'A::type. x) (%x::'A::type. x)"
obua@17644
  2303
  by (import hollight ISO_REFL)
obua@17644
  2304
obua@17644
  2305
lemma ISO_FUN: "ISO (f::'A::type => 'A'::type) (f'::'A'::type => 'A::type) &
obua@17644
  2306
ISO (g::'B::type => 'B'::type) (g'::'B'::type => 'B::type) -->
obua@17644
  2307
ISO (%(h::'A::type => 'B::type) a'::'A'::type. g (h (f' a')))
obua@17644
  2308
 (%(h::'A'::type => 'B'::type) a::'A::type. g' (h (f a)))"
obua@17644
  2309
  by (import hollight ISO_FUN)
obua@17644
  2310
obua@17644
  2311
lemma ISO_USAGE: "ISO (f::'q_16585::type => 'q_16582::type)
obua@17644
  2312
 (g::'q_16582::type => 'q_16585::type) -->
obua@17644
  2313
(ALL P::'q_16585::type => bool. All P = (ALL x::'q_16582::type. P (g x))) &
obua@17644
  2314
(ALL P::'q_16585::type => bool. Ex P = (EX x::'q_16582::type. P (g x))) &
obua@17644
  2315
(ALL (a::'q_16585::type) b::'q_16582::type. (a = g b) = (f a = b))"
obua@17644
  2316
  by (import hollight ISO_USAGE)
obua@17644
  2317
obua@17644
  2318
typedef (open) N_2 = "{a::bool recspace.
obua@17644
  2319
 ALL u::bool recspace => bool.
obua@17644
  2320
    (ALL a::bool recspace.
obua@17652
  2321
        a = CONSTR (NUMERAL 0) (SOME x::bool. True) (%n::nat. BOTTOM) |
obua@17644
  2322
        a =
obua@17652
  2323
        CONSTR (Suc (NUMERAL 0)) (SOME x::bool. True) (%n::nat. BOTTOM) -->
obua@17644
  2324
        u a) -->
obua@17644
  2325
    u a}"  morphisms "_dest_2" "_mk_2"
obua@17652
  2326
  apply (rule light_ex_imp_nonempty[where t="CONSTR (NUMERAL 0) (SOME x::bool. True) (%n::nat. BOTTOM)"])
obua@17644
  2327
  by (import hollight TYDEF_2)
obua@17644
  2328
obua@17644
  2329
syntax
obua@17644
  2330
  "_dest_2" :: _ ("'_dest'_2")
obua@17644
  2331
obua@17644
  2332
syntax
obua@17644
  2333
  "_mk_2" :: _ ("'_mk'_2")
obua@17644
  2334
obua@17644
  2335
lemmas "TYDEF_2_@intern" = typedef_hol2hollight 
obua@17644
  2336
  [where a="a :: N_2" and r=r ,
obua@17644
  2337
   OF type_definition_N_2]
obua@17644
  2338
obua@17644
  2339
consts
obua@17644
  2340
  "_10288" :: "N_2" ("'_10288")
obua@17644
  2341
obua@17644
  2342
defs
obua@17652
  2343
  "_10288_def": "(op ==::N_2 => N_2 => prop) (_10288::N_2)
obua@17652
  2344
 ((_mk_2::bool recspace => N_2)
obua@17652
  2345
   ((CONSTR::nat => bool => (nat => bool recspace) => bool recspace)
obua@17652
  2346
     (0::nat) ((Eps::(bool => bool) => bool) (%x::bool. True::bool))
obua@17652
  2347
     (%n::nat. BOTTOM::bool recspace)))"
obua@17652
  2348
obua@17652
  2349
lemma DEF__10288: "(op =::N_2 => N_2 => bool) (_10288::N_2)
obua@17652
  2350
 ((_mk_2::bool recspace => N_2)
obua@17652
  2351
   ((CONSTR::nat => bool => (nat => bool recspace) => bool recspace)
obua@17652
  2352
     (0::nat) ((Eps::(bool => bool) => bool) (%x::bool. True::bool))
obua@17652
  2353
     (%n::nat. BOTTOM::bool recspace)))"
obua@17644
  2354
  by (import hollight DEF__10288)
obua@17644
  2355
obua@17644
  2356
consts
obua@17644
  2357
  "_10289" :: "N_2" ("'_10289")
obua@17644
  2358
obua@17644
  2359
defs
obua@17652
  2360
  "_10289_def": "(op ==::N_2 => N_2 => prop) (_10289::N_2)
obua@17652
  2361
 ((_mk_2::bool recspace => N_2)
obua@17652
  2362
   ((CONSTR::nat => bool => (nat => bool recspace) => bool recspace)
obua@17652
  2363
     ((Suc::nat => nat) (0::nat))
obua@17652
  2364
     ((Eps::(bool => bool) => bool) (%x::bool. True::bool))
obua@17652
  2365
     (%n::nat. BOTTOM::bool recspace)))"
obua@17652
  2366
obua@17652
  2367
lemma DEF__10289: "(op =::N_2 => N_2 => bool) (_10289::N_2)
obua@17652
  2368
 ((_mk_2::bool recspace => N_2)
obua@17652
  2369
   ((CONSTR::nat => bool => (nat => bool recspace) => bool recspace)
obua@17652
  2370
     ((Suc::nat => nat) (0::nat))
obua@17652
  2371
     ((Eps::(bool => bool) => bool) (%x::bool. True::bool))
obua@17652
  2372
     (%n::nat. BOTTOM::bool recspace)))"
obua@17644
  2373
  by (import hollight DEF__10289)
obua@17644
  2374
obua@17644
  2375
constdefs
obua@17644
  2376
  two_1 :: "N_2" 
obua@17644
  2377
  "two_1 == _10288"
obua@17644
  2378
obua@17644
  2379
lemma DEF_two_1: "two_1 = _10288"
obua@17644
  2380
  by (import hollight DEF_two_1)
obua@17644
  2381
obua@17644
  2382
constdefs
obua@17644
  2383
  two_2 :: "N_2" 
obua@17644
  2384
  "two_2 == _10289"
obua@17644
  2385
obua@17644
  2386
lemma DEF_two_2: "two_2 = _10289"
obua@17644
  2387
  by (import hollight DEF_two_2)
obua@17644
  2388
obua@17644
  2389
typedef (open) N_3 = "{a::bool recspace.
obua@17644
  2390
 ALL u::bool recspace => bool.
obua@17644
  2391
    (ALL a::bool recspace.
obua@17652
  2392
        a = CONSTR (NUMERAL 0) (SOME x::bool. True) (%n::nat. BOTTOM) |
obua@17644
  2393
        a =
obua@17652
  2394
        CONSTR (Suc (NUMERAL 0)) (SOME x::bool. True) (%n::nat. BOTTOM) |
obua@17644
  2395
        a =
obua@17652
  2396
        CONSTR (Suc (Suc (NUMERAL 0))) (SOME x::bool. True)
obua@17644
  2397
         (%n::nat. BOTTOM) -->
obua@17644
  2398
        u a) -->
obua@17644
  2399
    u a}"  morphisms "_dest_3" "_mk_3"
obua@17652
  2400
  apply (rule light_ex_imp_nonempty[where t="CONSTR (NUMERAL 0) (SOME x::bool. True) (%n::nat. BOTTOM)"])
obua@17644
  2401
  by (import hollight TYDEF_3)
obua@17644
  2402
obua@17644
  2403
syntax
obua@17644
  2404
  "_dest_3" :: _ ("'_dest'_3")
obua@17644
  2405
obua@17644
  2406
syntax
obua@17644
  2407
  "_mk_3" :: _ ("'_mk'_3")
obua@17644
  2408
obua@17644
  2409
lemmas "TYDEF_3_@intern" = typedef_hol2hollight 
obua@17644
  2410
  [where a="a :: N_3" and r=r ,
obua@17644
  2411
   OF type_definition_N_3]
obua@17644
  2412
obua@17644
  2413
consts
obua@17644
  2414
  "_10312" :: "N_3" ("'_10312")
obua@17644
  2415
obua@17644
  2416
defs
obua@17652
  2417
  "_10312_def": "(op ==::N_3 => N_3 => prop) (_10312::N_3)
obua@17652
  2418
 ((_mk_3::bool recspace => N_3)
obua@17652
  2419
   ((CONSTR::nat => bool => (nat => bool recspace) => bool recspace)
obua@17652
  2420
     (0::nat) ((Eps::(bool => bool) => bool) (%x::bool. True::bool))
obua@17652
  2421
     (%n::nat. BOTTOM::bool recspace)))"
obua@17652
  2422
obua@17652
  2423
lemma DEF__10312: "(op =::N_3 => N_3 => bool) (_10312::N_3)
obua@17652
  2424
 ((_mk_3::bool recspace => N_3)
obua@17652
  2425
   ((CONSTR::nat => bool => (nat => bool recspace) => bool recspace)
obua@17652
  2426
     (0::nat) ((Eps::(bool => bool) => bool) (%x::bool. True::bool))
obua@17652
  2427
     (%n::nat. BOTTOM::bool recspace)))"
obua@17644
  2428
  by (import hollight DEF__10312)
obua@17644
  2429
obua@17644
  2430
consts
obua@17644
  2431
  "_10313" :: "N_3" ("'_10313")
obua@17644
  2432
obua@17644
  2433
defs
obua@17652
  2434
  "_10313_def": "(op ==::N_3 => N_3 => prop) (_10313::N_3)
obua@17652
  2435
 ((_mk_3::bool recspace => N_3)
obua@17652
  2436
   ((CONSTR::nat => bool => (nat => bool recspace) => bool recspace)
obua@17652
  2437
     ((Suc::nat => nat) (0::nat))
obua@17652
  2438
     ((Eps::(bool => bool) => bool) (%x::bool. True::bool))
obua@17652
  2439
     (%n::nat. BOTTOM::bool recspace)))"
obua@17652
  2440
obua@17652
  2441
lemma DEF__10313: "(op =::N_3 => N_3 => bool) (_10313::N_3)
obua@17652
  2442
 ((_mk_3::bool recspace => N_3)
obua@17652
  2443
   ((CONSTR::nat => bool => (nat => bool recspace) => bool recspace)
obua@17652
  2444
     ((Suc::nat => nat) (0::nat))
obua@17652
  2445
     ((Eps::(bool => bool) => bool) (%x::bool. True::bool))
obua@17652
  2446
     (%n::nat. BOTTOM::bool recspace)))"
obua@17644
  2447
  by (import hollight DEF__10313)
obua@17644
  2448
obua@17644
  2449
consts
obua@17644
  2450
  "_10314" :: "N_3" ("'_10314")
obua@17644
  2451
obua@17644
  2452
defs
obua@17652
  2453
  "_10314_def": "(op ==::N_3 => N_3 => prop) (_10314::N_3)
obua@17652
  2454
 ((_mk_3::bool recspace => N_3)
obua@17652
  2455
   ((CONSTR::nat => bool => (nat => bool recspace) => bool recspace)
obua@17652
  2456
     ((Suc::nat => nat) ((Suc::nat => nat) (0::nat)))
obua@17652
  2457
     ((Eps::(bool => bool) => bool) (%x::bool. True::bool))
obua@17652
  2458
     (%n::nat. BOTTOM::bool recspace)))"
obua@17652
  2459
obua@17652
  2460
lemma DEF__10314: "(op =::N_3 => N_3 => bool) (_10314::N_3)
obua@17652
  2461
 ((_mk_3::bool recspace => N_3)
obua@17652
  2462
   ((CONSTR::nat => bool => (nat => bool recspace) => bool recspace)
obua@17652
  2463
     ((Suc::nat => nat) ((Suc::nat => nat) (0::nat)))
obua@17652
  2464
     ((Eps::(bool => bool) => bool) (%x::bool. True::bool))
obua@17652
  2465
     (%n::nat. BOTTOM::bool recspace)))"
obua@17644
  2466
  by (import hollight DEF__10314)
obua@17644
  2467
obua@17644
  2468
constdefs
obua@17644
  2469
  three_1 :: "N_3" 
obua@17644
  2470
  "three_1 == _10312"
obua@17644
  2471
obua@17644
  2472
lemma DEF_three_1: "three_1 = _10312"
obua@17644
  2473
  by (import hollight DEF_three_1)
obua@17644
  2474
obua@17644
  2475
constdefs
obua@17644
  2476
  three_2 :: "N_3" 
obua@17644
  2477
  "three_2 == _10313"
obua@17644
  2478
obua@17644
  2479
lemma DEF_three_2: "three_2 = _10313"
obua@17644
  2480
  by (import hollight DEF_three_2)
obua@17644
  2481
obua@17644
  2482
constdefs
obua@17644
  2483
  three_3 :: "N_3" 
obua@17644
  2484
  "three_3 == _10314"
obua@17644
  2485
obua@17644
  2486
lemma DEF_three_3: "three_3 = _10314"
obua@17644
  2487
  by (import hollight DEF_three_3)
obua@17644
  2488
obua@17644
  2489
lemma list_INDUCT: "ALL P::'A::type hollight.list => bool.
obua@17644
  2490
   P NIL &
obua@17644
  2491
   (ALL (a0::'A::type) a1::'A::type hollight.list.
obua@17644
  2492
       P a1 --> P (CONS a0 a1)) -->
obua@17644
  2493
   All P"
obua@17644
  2494
  by (import hollight list_INDUCT)
obua@17644
  2495
obua@17644
  2496
constdefs
obua@17652
  2497
  HD :: "'A hollight.list => 'A" 
obua@17644
  2498
  "HD ==
obua@17644
  2499
SOME HD::'A::type hollight.list => 'A::type.
obua@17644
  2500
   ALL (t::'A::type hollight.list) h::'A::type. HD (CONS h t) = h"
obua@17644
  2501
obua@17644
  2502
lemma DEF_HD: "HD =
obua@17644
  2503
(SOME HD::'A::type hollight.list => 'A::type.
obua@17644
  2504
    ALL (t::'A::type hollight.list) h::'A::type. HD (CONS h t) = h)"
obua@17644
  2505
  by (import hollight DEF_HD)
obua@17644
  2506
obua@17644
  2507
constdefs
obua@17652
  2508
  TL :: "'A hollight.list => 'A hollight.list" 
obua@17644
  2509
  "TL ==
obua@17644
  2510
SOME TL::'A::type hollight.list => 'A::type hollight.list.
obua@17644
  2511
   ALL (h::'A::type) t::'A::type hollight.list. TL (CONS h t) = t"
obua@17644
  2512
obua@17644
  2513
lemma DEF_TL: "TL =
obua@17644
  2514
(SOME TL::'A::type hollight.list => 'A::type hollight.list.
obua@17644
  2515
    ALL (h::'A::type) t::'A::type hollight.list. TL (CONS h t) = t)"
obua@17644
  2516
  by (import hollight DEF_TL)
obua@17644
  2517
obua@17644
  2518
constdefs
obua@17652
  2519
  APPEND :: "'A hollight.list => 'A hollight.list => 'A hollight.list" 
obua@17644
  2520
  "APPEND ==
obua@17644
  2521
SOME APPEND::'A::type hollight.list
obua@17644
  2522
             => 'A::type hollight.list => 'A::type hollight.list.
obua@17644
  2523
   (ALL l::'A::type hollight.list. APPEND NIL l = l) &
obua@17644
  2524
   (ALL (h::'A::type) (t::'A::type hollight.list) l::'A::type hollight.list.
obua@17644
  2525
       APPEND (CONS h t) l = CONS h (APPEND t l))"
obua@17644
  2526
obua@17644
  2527
lemma DEF_APPEND: "APPEND =
obua@17644
  2528
(SOME APPEND::'A::type hollight.list
obua@17644
  2529
              => 'A::type hollight.list => 'A::type hollight.list.
obua@17644
  2530
    (ALL l::'A::type hollight.list. APPEND NIL l = l) &
obua@17644
  2531
    (ALL (h::'A::type) (t::'A::type hollight.list)
obua@17644
  2532
        l::'A::type hollight.list.
obua@17644
  2533
        APPEND (CONS h t) l = CONS h (APPEND t l)))"
obua@17644
  2534
  by (import hollight DEF_APPEND)
obua@17644
  2535
obua@17644
  2536
constdefs
obua@17652
  2537
  REVERSE :: "'A hollight.list => 'A hollight.list" 
obua@17644
  2538
  "REVERSE ==
obua@17644
  2539
SOME REVERSE::'A::type hollight.list => 'A::type hollight.list.
obua@17644
  2540
   REVERSE NIL = NIL &
obua@17644
  2541
   (ALL (l::'A::type hollight.list) x::'A::type.
obua@17644
  2542
       REVERSE (CONS x l) = APPEND (REVERSE l) (CONS x NIL))"
obua@17644
  2543
obua@17644
  2544
lemma DEF_REVERSE: "REVERSE =
obua@17644
  2545
(SOME REVERSE::'A::type hollight.list => 'A::type hollight.list.
obua@17644
  2546
    REVERSE NIL = NIL &
obua@17644
  2547
    (ALL (l::'A::type hollight.list) x::'A::type.
obua@17644
  2548
        REVERSE (CONS x l) = APPEND (REVERSE l) (CONS x NIL)))"
obua@17644
  2549
  by (import hollight DEF_REVERSE)
obua@17644
  2550
obua@17644
  2551
constdefs
obua@17652
  2552
  LENGTH :: "'A hollight.list => nat" 
obua@17644
  2553
  "LENGTH ==
obua@17644
  2554
SOME LENGTH::'A::type hollight.list => nat.
obua@17652
  2555
   LENGTH NIL = 0 &
obua@17644
  2556
   (ALL (h::'A::type) t::'A::type hollight.list.
obua@17644
  2557
       LENGTH (CONS h t) = Suc (LENGTH t))"
obua@17644
  2558
obua@17644
  2559
lemma DEF_LENGTH: "LENGTH =
obua@17644
  2560
(SOME LENGTH::'A::type hollight.list => nat.
obua@17652
  2561
    LENGTH NIL = 0 &
obua@17644
  2562
    (ALL (h::'A::type) t::'A::type hollight.list.
obua@17644
  2563
        LENGTH (CONS h t) = Suc (LENGTH t)))"
obua@17644
  2564
  by (import hollight DEF_LENGTH)
obua@17644
  2565
obua@17644
  2566
constdefs
obua@17652
  2567
  MAP :: "('A => 'B) => 'A hollight.list => 'B hollight.list" 
obua@17644
  2568
  "MAP ==
obua@17644
  2569
SOME MAP::('A::type => 'B::type)
obua@17644
  2570
          => 'A::type hollight.list => 'B::type hollight.list.
obua@17644
  2571
   (ALL f::'A::type => 'B::type. MAP f NIL = NIL) &
obua@17644
  2572
   (ALL (f::'A::type => 'B::type) (h::'A::type) t::'A::type hollight.list.
obua@17644
  2573
       MAP f (CONS h t) = CONS (f h) (MAP f t))"
obua@17644
  2574
obua@17644
  2575
lemma DEF_MAP: "MAP =
obua@17644
  2576
(SOME MAP::('A::type => 'B::type)
obua@17644
  2577
           => 'A::type hollight.list => 'B::type hollight.list.
obua@17644
  2578
    (ALL f::'A::type => 'B::type. MAP f NIL = NIL) &
obua@17644
  2579
    (ALL (f::'A::type => 'B::type) (h::'A::type) t::'A::type hollight.list.
obua@17644
  2580
        MAP f (CONS h t) = CONS (f h) (MAP f t)))"