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