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