src/HOL/Import/HOL/HOL4Base.thy
author haftmann
Mon Jan 30 08:20:56 2006 +0100 (2006-01-30)
changeset 18851 9502ce541f01
parent 17727 83d64a461507
child 23290 c358025ad8db
permissions -rw-r--r--
adaptions to codegen_package
skalberg@15647
     1
(* AUTOMATICALLY GENERATED, DO NOT EDIT! *)
skalberg@15647
     2
wenzelm@17566
     3
theory HOL4Base imports "../HOL4Compat" "../HOL4Syntax" begin
skalberg@14516
     4
skalberg@14516
     5
;setup_theory bool
skalberg@14516
     6
skalberg@14516
     7
constdefs
obua@17652
     8
  ARB :: "'a" 
obua@17644
     9
  "ARB == SOME x::'a::type. True"
obua@17644
    10
obua@17644
    11
lemma ARB_DEF: "ARB = (SOME x::'a::type. True)"
skalberg@14516
    12
  by (import bool ARB_DEF)
skalberg@14516
    13
skalberg@14516
    14
constdefs
obua@17652
    15
  IN :: "'a => ('a => bool) => bool" 
obua@17644
    16
  "IN == %(x::'a::type) f::'a::type => bool. f x"
obua@17644
    17
obua@17644
    18
lemma IN_DEF: "IN = (%(x::'a::type) f::'a::type => bool. f x)"
skalberg@14516
    19
  by (import bool IN_DEF)
skalberg@14516
    20
skalberg@14516
    21
constdefs
obua@17652
    22
  RES_FORALL :: "('a => bool) => ('a => bool) => bool" 
obua@17644
    23
  "RES_FORALL ==
obua@17644
    24
%(p::'a::type => bool) m::'a::type => bool. ALL x::'a::type. IN x p --> m x"
obua@17644
    25
obua@17644
    26
lemma RES_FORALL_DEF: "RES_FORALL =
obua@17644
    27
(%(p::'a::type => bool) m::'a::type => bool.
obua@17644
    28
    ALL x::'a::type. IN x p --> m x)"
skalberg@14516
    29
  by (import bool RES_FORALL_DEF)
skalberg@14516
    30
skalberg@14516
    31
constdefs
obua@17652
    32
  RES_EXISTS :: "('a => bool) => ('a => bool) => bool" 
obua@17644
    33
  "RES_EXISTS ==
obua@17644
    34
%(p::'a::type => bool) m::'a::type => bool. EX x::'a::type. IN x p & m x"
obua@17644
    35
obua@17644
    36
lemma RES_EXISTS_DEF: "RES_EXISTS =
obua@17644
    37
(%(p::'a::type => bool) m::'a::type => bool. EX x::'a::type. IN x p & m x)"
skalberg@14516
    38
  by (import bool RES_EXISTS_DEF)
skalberg@14516
    39
skalberg@14516
    40
constdefs
obua@17652
    41
  RES_EXISTS_UNIQUE :: "('a => bool) => ('a => bool) => bool" 
skalberg@14516
    42
  "RES_EXISTS_UNIQUE ==
obua@17644
    43
%(p::'a::type => bool) m::'a::type => bool.
obua@17644
    44
   RES_EXISTS p m &
obua@17644
    45
   RES_FORALL p
obua@17644
    46
    (%x::'a::type. RES_FORALL p (%y::'a::type. m x & m y --> x = y))"
skalberg@14516
    47
skalberg@14516
    48
lemma RES_EXISTS_UNIQUE_DEF: "RES_EXISTS_UNIQUE =
obua@17644
    49
(%(p::'a::type => bool) m::'a::type => bool.
obua@17644
    50
    RES_EXISTS p m &
obua@17644
    51
    RES_FORALL p
obua@17644
    52
     (%x::'a::type. RES_FORALL p (%y::'a::type. m x & m y --> x = y)))"
skalberg@14516
    53
  by (import bool RES_EXISTS_UNIQUE_DEF)
skalberg@14516
    54
skalberg@14516
    55
constdefs
obua@17652
    56
  RES_SELECT :: "('a => bool) => ('a => bool) => 'a" 
obua@17644
    57
  "RES_SELECT ==
obua@17644
    58
%(p::'a::type => bool) m::'a::type => bool. SOME x::'a::type. IN x p & m x"
obua@17644
    59
obua@17644
    60
lemma RES_SELECT_DEF: "RES_SELECT =
obua@17644
    61
(%(p::'a::type => bool) m::'a::type => bool. SOME x::'a::type. IN x p & m x)"
skalberg@14516
    62
  by (import bool RES_SELECT_DEF)
skalberg@14516
    63
obua@17644
    64
lemma EXCLUDED_MIDDLE: "ALL t::bool. t | ~ t"
skalberg@14516
    65
  by (import bool EXCLUDED_MIDDLE)
skalberg@14516
    66
obua@17644
    67
lemma FORALL_THM: "All (f::'a::type => bool) = All f"
skalberg@14516
    68
  by (import bool FORALL_THM)
skalberg@14516
    69
obua@17644
    70
lemma EXISTS_THM: "Ex (f::'a::type => bool) = Ex f"
skalberg@14516
    71
  by (import bool EXISTS_THM)
skalberg@14516
    72
obua@17644
    73
lemma F_IMP: "ALL t::bool. ~ t --> t --> False"
skalberg@14516
    74
  by (import bool F_IMP)
skalberg@14516
    75
obua@17644
    76
lemma NOT_AND: "~ ((t::bool) & ~ t)"
skalberg@14516
    77
  by (import bool NOT_AND)
skalberg@14516
    78
obua@17644
    79
lemma AND_CLAUSES: "ALL t::bool.
skalberg@14516
    80
   (True & t) = t &
skalberg@14516
    81
   (t & True) = t & (False & t) = False & (t & False) = False & (t & t) = t"
skalberg@14516
    82
  by (import bool AND_CLAUSES)
skalberg@14516
    83
obua@17644
    84
lemma OR_CLAUSES: "ALL t::bool.
skalberg@14516
    85
   (True | t) = True &
skalberg@14516
    86
   (t | True) = True & (False | t) = t & (t | False) = t & (t | t) = t"
skalberg@14516
    87
  by (import bool OR_CLAUSES)
skalberg@14516
    88
obua@17644
    89
lemma IMP_CLAUSES: "ALL t::bool.
skalberg@14516
    90
   (True --> t) = t &
skalberg@14516
    91
   (t --> True) = True &
skalberg@14516
    92
   (False --> t) = True & (t --> t) = True & (t --> False) = (~ t)"
skalberg@14516
    93
  by (import bool IMP_CLAUSES)
skalberg@14516
    94
obua@17644
    95
lemma NOT_CLAUSES: "(ALL t::bool. (~ ~ t) = t) & (~ True) = False & (~ False) = True"
skalberg@14516
    96
  by (import bool NOT_CLAUSES)
skalberg@14516
    97
skalberg@14516
    98
lemma BOOL_EQ_DISTINCT: "True ~= False & False ~= True"
skalberg@14516
    99
  by (import bool BOOL_EQ_DISTINCT)
skalberg@14516
   100
obua@17644
   101
lemma EQ_CLAUSES: "ALL t::bool.
skalberg@14516
   102
   (True = t) = t &
skalberg@14516
   103
   (t = True) = t & (False = t) = (~ t) & (t = False) = (~ t)"
skalberg@14516
   104
  by (import bool EQ_CLAUSES)
skalberg@14516
   105
obua@17644
   106
lemma COND_CLAUSES: "ALL (t1::'a::type) t2::'a::type.
obua@17644
   107
   (if True then t1 else t2) = t1 & (if False then t1 else t2) = t2"
skalberg@14516
   108
  by (import bool COND_CLAUSES)
skalberg@14516
   109
obua@17644
   110
lemma SELECT_UNIQUE: "ALL (P::'a::type => bool) x::'a::type.
obua@17644
   111
   (ALL y::'a::type. P y = (y = x)) --> Eps P = x"
skalberg@14516
   112
  by (import bool SELECT_UNIQUE)
skalberg@14516
   113
obua@17644
   114
lemma BOTH_EXISTS_AND_THM: "ALL (P::bool) Q::bool.
obua@17644
   115
   (EX x::'a::type. P & Q) = ((EX x::'a::type. P) & (EX x::'a::type. Q))"
skalberg@14516
   116
  by (import bool BOTH_EXISTS_AND_THM)
skalberg@14516
   117
skalberg@14516
   118
lemma BOTH_FORALL_OR_THM: "ALL (P::bool) Q::bool.
obua@17644
   119
   (ALL x::'a::type. P | Q) = ((ALL x::'a::type. P) | (ALL x::'a::type. Q))"
skalberg@14516
   120
  by (import bool BOTH_FORALL_OR_THM)
skalberg@14516
   121
skalberg@14516
   122
lemma BOTH_FORALL_IMP_THM: "ALL (P::bool) Q::bool.
obua@17644
   123
   (ALL x::'a::type. P --> Q) =
obua@17644
   124
   ((EX x::'a::type. P) --> (ALL x::'a::type. Q))"
skalberg@14516
   125
  by (import bool BOTH_FORALL_IMP_THM)
skalberg@14516
   126
skalberg@14516
   127
lemma BOTH_EXISTS_IMP_THM: "ALL (P::bool) Q::bool.
obua@17644
   128
   (EX x::'a::type. P --> Q) =
obua@17644
   129
   ((ALL x::'a::type. P) --> (EX x::'a::type. Q))"
skalberg@14516
   130
  by (import bool BOTH_EXISTS_IMP_THM)
skalberg@14516
   131
obua@17644
   132
lemma OR_IMP_THM: "ALL (A::bool) B::bool. (A = (B | A)) = (B --> A)"
skalberg@14516
   133
  by (import bool OR_IMP_THM)
skalberg@14516
   134
obua@17644
   135
lemma DE_MORGAN_THM: "ALL (A::bool) B::bool. (~ (A & B)) = (~ A | ~ B) & (~ (A | B)) = (~ A & ~ B)"
skalberg@14516
   136
  by (import bool DE_MORGAN_THM)
skalberg@14516
   137
obua@17644
   138
lemma IMP_F_EQ_F: "ALL t::bool. (t --> False) = (t = False)"
skalberg@14516
   139
  by (import bool IMP_F_EQ_F)
skalberg@14516
   140
obua@17644
   141
lemma EQ_EXPAND: "ALL (t1::bool) t2::bool. (t1 = t2) = (t1 & t2 | ~ t1 & ~ t2)"
skalberg@14516
   142
  by (import bool EQ_EXPAND)
skalberg@14516
   143
obua@17644
   144
lemma COND_RATOR: "ALL (b::bool) (f::'a::type => 'b::type) (g::'a::type => 'b::type)
obua@17644
   145
   x::'a::type. (if b then f else g) x = (if b then f x else g x)"
skalberg@14516
   146
  by (import bool COND_RATOR)
skalberg@14516
   147
obua@17644
   148
lemma COND_ABS: "ALL (b::bool) (f::'a::type => 'b::type) g::'a::type => 'b::type.
obua@17644
   149
   (%x::'a::type. if b then f x else g x) = (if b then f else g)"
skalberg@14516
   150
  by (import bool COND_ABS)
skalberg@14516
   151
obua@17644
   152
lemma COND_EXPAND: "ALL (b::bool) (t1::bool) t2::bool.
obua@17644
   153
   (if b then t1 else t2) = ((~ b | t1) & (b | t2))"
skalberg@14516
   154
  by (import bool COND_EXPAND)
skalberg@14516
   155
obua@17644
   156
lemma ONE_ONE_THM: "ALL f::'a::type => 'b::type.
obua@17644
   157
   inj f = (ALL (x1::'a::type) x2::'a::type. f x1 = f x2 --> x1 = x2)"
skalberg@14516
   158
  by (import bool ONE_ONE_THM)
skalberg@14516
   159
obua@17644
   160
lemma ABS_REP_THM: "(All::(('a::type => bool) => bool) => bool)
obua@17644
   161
 (%P::'a::type => bool.
skalberg@14516
   162
     (op -->::bool => bool => bool)
obua@17644
   163
      ((Ex::(('b::type => 'a::type) => bool) => bool)
obua@17644
   164
        ((TYPE_DEFINITION::('a::type => bool)
obua@17644
   165
                           => ('b::type => 'a::type) => bool)
obua@17644
   166
          P))
obua@17644
   167
      ((Ex::(('b::type => 'a::type) => bool) => bool)
obua@17644
   168
        (%x::'b::type => 'a::type.
obua@17644
   169
            (Ex::(('a::type => 'b::type) => bool) => bool)
obua@17644
   170
             (%abs::'a::type => 'b::type.
skalberg@14516
   171
                 (op &::bool => bool => bool)
obua@17644
   172
                  ((All::('b::type => bool) => bool)
obua@17644
   173
                    (%a::'b::type.
obua@17644
   174
                        (op =::'b::type => 'b::type => bool) (abs (x a)) a))
obua@17644
   175
                  ((All::('a::type => bool) => bool)
obua@17644
   176
                    (%r::'a::type.
skalberg@14516
   177
                        (op =::bool => bool => bool) (P r)
obua@17644
   178
                         ((op =::'a::type => 'a::type => bool) (x (abs r))
obua@17644
   179
                           r)))))))"
skalberg@14516
   180
  by (import bool ABS_REP_THM)
skalberg@14516
   181
obua@17644
   182
lemma LET_RAND: "(P::'b::type => bool) (Let (M::'a::type) (N::'a::type => 'b::type)) =
obua@17644
   183
(let x::'a::type = M in P (N x))"
skalberg@14516
   184
  by (import bool LET_RAND)
skalberg@14516
   185
obua@17644
   186
lemma LET_RATOR: "Let (M::'a::type) (N::'a::type => 'b::type => 'c::type) (b::'b::type) =
obua@17644
   187
(let x::'a::type = M in N x b)"
skalberg@14516
   188
  by (import bool LET_RATOR)
skalberg@14516
   189
obua@17644
   190
lemma SWAP_FORALL_THM: "ALL P::'a::type => 'b::type => bool.
obua@17644
   191
   (ALL x::'a::type. All (P x)) = (ALL (y::'b::type) x::'a::type. P x y)"
skalberg@14516
   192
  by (import bool SWAP_FORALL_THM)
skalberg@14516
   193
obua@17644
   194
lemma SWAP_EXISTS_THM: "ALL P::'a::type => 'b::type => bool.
obua@17644
   195
   (EX x::'a::type. Ex (P x)) = (EX (y::'b::type) x::'a::type. P x y)"
skalberg@14516
   196
  by (import bool SWAP_EXISTS_THM)
skalberg@14516
   197
obua@17644
   198
lemma AND_CONG: "ALL (P::bool) (P'::bool) (Q::bool) Q'::bool.
obua@17644
   199
   (Q --> P = P') & (P' --> Q = Q') --> (P & Q) = (P' & Q')"
skalberg@14516
   200
  by (import bool AND_CONG)
skalberg@14516
   201
obua@17644
   202
lemma OR_CONG: "ALL (P::bool) (P'::bool) (Q::bool) Q'::bool.
obua@17644
   203
   (~ Q --> P = P') & (~ P' --> Q = Q') --> (P | Q) = (P' | Q')"
skalberg@14516
   204
  by (import bool OR_CONG)
skalberg@14516
   205
obua@17644
   206
lemma COND_CONG: "ALL (P::bool) (Q::bool) (x::'a::type) (x'::'a::type) (y::'a::type)
obua@17644
   207
   y'::'a::type.
skalberg@14516
   208
   P = Q & (Q --> x = x') & (~ Q --> y = y') -->
skalberg@14516
   209
   (if P then x else y) = (if Q then x' else y')"
skalberg@14516
   210
  by (import bool COND_CONG)
skalberg@14516
   211
obua@17644
   212
lemma MONO_COND: "((x::bool) --> (y::bool)) -->
obua@17644
   213
((z::bool) --> (w::bool)) -->
obua@17644
   214
(if b::bool then x else z) --> (if b then y else w)"
skalberg@14516
   215
  by (import bool MONO_COND)
skalberg@14516
   216
obua@17644
   217
lemma SKOLEM_THM: "ALL P::'a::type => 'b::type => bool.
obua@17644
   218
   (ALL x::'a::type. Ex (P x)) =
obua@17644
   219
   (EX f::'a::type => 'b::type. ALL x::'a::type. P x (f x))"
skalberg@14516
   220
  by (import bool SKOLEM_THM)
skalberg@14516
   221
obua@17644
   222
lemma bool_case_thm: "(ALL (e0::'a::type) e1::'a::type.
obua@17644
   223
    (case True of True => e0 | False => e1) = e0) &
obua@17644
   224
(ALL (e0::'a::type) e1::'a::type.
obua@17644
   225
    (case False of True => e0 | False => e1) = e1)"
skalberg@14516
   226
  by (import bool bool_case_thm)
skalberg@14516
   227
obua@17644
   228
lemma bool_case_ID: "ALL (x::'a::type) b::bool. (case b of True => x | _ => x) = x"
skalberg@14516
   229
  by (import bool bool_case_ID)
skalberg@14516
   230
obua@17644
   231
lemma boolAxiom: "ALL (e0::'a::type) e1::'a::type.
obua@17644
   232
   EX x::bool => 'a::type. x True = e0 & x False = e1"
skalberg@14516
   233
  by (import bool boolAxiom)
skalberg@14516
   234
obua@17644
   235
lemma UEXISTS_OR_THM: "ALL (P::'a::type => bool) Q::'a::type => bool.
obua@17644
   236
   (EX! x::'a::type. P x | Q x) --> Ex1 P | Ex1 Q"
skalberg@14516
   237
  by (import bool UEXISTS_OR_THM)
skalberg@14516
   238
obua@17644
   239
lemma UEXISTS_SIMP: "(EX! x::'a::type. (t::bool)) = (t & (ALL x::'a::type. All (op = x)))"
skalberg@14516
   240
  by (import bool UEXISTS_SIMP)
skalberg@14516
   241
skalberg@14516
   242
consts
obua@17652
   243
  RES_ABSTRACT :: "('a => bool) => ('a => 'b) => 'a => 'b" 
obua@17644
   244
obua@17644
   245
specification (RES_ABSTRACT) RES_ABSTRACT_DEF: "(ALL (p::'a::type => bool) (m::'a::type => 'b::type) x::'a::type.
skalberg@14516
   246
    IN x p --> RES_ABSTRACT p m x = m x) &
obua@17644
   247
(ALL (p::'a::type => bool) (m1::'a::type => 'b::type)
obua@17644
   248
    m2::'a::type => 'b::type.
obua@17644
   249
    (ALL x::'a::type. IN x p --> m1 x = m2 x) -->
skalberg@14516
   250
    RES_ABSTRACT p m1 = RES_ABSTRACT p m2)"
skalberg@14516
   251
  by (import bool RES_ABSTRACT_DEF)
skalberg@14516
   252
obua@17644
   253
lemma BOOL_FUN_CASES_THM: "ALL f::bool => bool.
obua@17644
   254
   f = (%b::bool. True) |
obua@17644
   255
   f = (%b::bool. False) | f = (%b::bool. b) | f = Not"
skalberg@14516
   256
  by (import bool BOOL_FUN_CASES_THM)
skalberg@14516
   257
obua@17644
   258
lemma BOOL_FUN_INDUCT: "ALL P::(bool => bool) => bool.
obua@17644
   259
   P (%b::bool. True) & P (%b::bool. False) & P (%b::bool. b) & P Not -->
obua@17644
   260
   All P"
skalberg@14516
   261
  by (import bool BOOL_FUN_INDUCT)
skalberg@14516
   262
skalberg@14516
   263
;end_setup
skalberg@14516
   264
skalberg@14516
   265
;setup_theory combin
skalberg@14516
   266
skalberg@14516
   267
constdefs
obua@17652
   268
  K :: "'a => 'b => 'a" 
obua@17644
   269
  "K == %(x::'a::type) y::'b::type. x"
obua@17644
   270
obua@17644
   271
lemma K_DEF: "K = (%(x::'a::type) y::'b::type. x)"
skalberg@14516
   272
  by (import combin K_DEF)
skalberg@14516
   273
skalberg@14516
   274
constdefs
obua@17652
   275
  S :: "('a => 'b => 'c) => ('a => 'b) => 'a => 'c" 
obua@17644
   276
  "S ==
obua@17644
   277
%(f::'a::type => 'b::type => 'c::type) (g::'a::type => 'b::type)
obua@17644
   278
   x::'a::type. f x (g x)"
obua@17644
   279
obua@17644
   280
lemma S_DEF: "S =
obua@17644
   281
(%(f::'a::type => 'b::type => 'c::type) (g::'a::type => 'b::type)
obua@17644
   282
    x::'a::type. f x (g x))"
skalberg@14516
   283
  by (import combin S_DEF)
skalberg@14516
   284
skalberg@14516
   285
constdefs
obua@17652
   286
  I :: "'a => 'a" 
obua@17644
   287
  "(op ==::('a::type => 'a::type) => ('a::type => 'a::type) => prop)
obua@17644
   288
 (I::'a::type => 'a::type)
obua@17644
   289
 ((S::('a::type => ('a::type => 'a::type) => 'a::type)
obua@17644
   290
      => ('a::type => 'a::type => 'a::type) => 'a::type => 'a::type)
obua@17644
   291
   (K::'a::type => ('a::type => 'a::type) => 'a::type)
obua@17644
   292
   (K::'a::type => 'a::type => 'a::type))"
obua@17644
   293
obua@17644
   294
lemma I_DEF: "(op =::('a::type => 'a::type) => ('a::type => 'a::type) => bool)
obua@17644
   295
 (I::'a::type => 'a::type)
obua@17644
   296
 ((S::('a::type => ('a::type => 'a::type) => 'a::type)
obua@17644
   297
      => ('a::type => 'a::type => 'a::type) => 'a::type => 'a::type)
obua@17644
   298
   (K::'a::type => ('a::type => 'a::type) => 'a::type)
obua@17644
   299
   (K::'a::type => 'a::type => 'a::type))"
skalberg@14516
   300
  by (import combin I_DEF)
skalberg@14516
   301
skalberg@14516
   302
constdefs
obua@17652
   303
  C :: "('a => 'b => 'c) => 'b => 'a => 'c" 
obua@17644
   304
  "C == %(f::'a::type => 'b::type => 'c::type) (x::'b::type) y::'a::type. f y x"
obua@17644
   305
obua@17644
   306
lemma C_DEF: "C =
obua@17644
   307
(%(f::'a::type => 'b::type => 'c::type) (x::'b::type) y::'a::type. f y x)"
skalberg@14516
   308
  by (import combin C_DEF)
skalberg@14516
   309
skalberg@14516
   310
constdefs
obua@17652
   311
  W :: "('a => 'a => 'b) => 'a => 'b" 
obua@17644
   312
  "W == %(f::'a::type => 'a::type => 'b::type) x::'a::type. f x x"
obua@17644
   313
obua@17644
   314
lemma W_DEF: "W = (%(f::'a::type => 'a::type => 'b::type) x::'a::type. f x x)"
skalberg@14516
   315
  by (import combin W_DEF)
skalberg@14516
   316
obua@17644
   317
lemma I_THM: "ALL x::'a::type. I x = x"
skalberg@14516
   318
  by (import combin I_THM)
skalberg@14516
   319
obua@17644
   320
lemma I_o_ID: "ALL f::'a::type => 'b::type. I o f = f & f o I = f"
skalberg@14516
   321
  by (import combin I_o_ID)
skalberg@14516
   322
skalberg@14516
   323
;end_setup
skalberg@14516
   324
skalberg@14516
   325
;setup_theory sum
skalberg@14516
   326
obua@17644
   327
lemma ISL_OR_ISR: "ALL x::'a::type + 'b::type. ISL x | ISR x"
skalberg@14516
   328
  by (import sum ISL_OR_ISR)
skalberg@14516
   329
obua@17644
   330
lemma INL: "ALL x::'a::type + 'b::type. ISL x --> Inl (OUTL x) = x"
skalberg@14516
   331
  by (import sum INL)
skalberg@14516
   332
obua@17644
   333
lemma INR: "ALL x::'a::type + 'b::type. ISR x --> Inr (OUTR x) = x"
skalberg@14516
   334
  by (import sum INR)
skalberg@14516
   335
obua@17644
   336
lemma sum_case_cong: "ALL (M::'b::type + 'c::type) (M'::'b::type + 'c::type)
obua@17644
   337
   (f::'b::type => 'a::type) g::'c::type => 'a::type.
skalberg@14516
   338
   M = M' &
obua@17644
   339
   (ALL x::'b::type. M' = Inl x --> f x = (f'::'b::type => 'a::type) x) &
obua@17644
   340
   (ALL y::'c::type. M' = Inr y --> g y = (g'::'c::type => 'a::type) y) -->
skalberg@14516
   341
   sum_case f g M = sum_case f' g' M'"
skalberg@14516
   342
  by (import sum sum_case_cong)
skalberg@14516
   343
skalberg@14516
   344
;end_setup
skalberg@14516
   345
skalberg@14516
   346
;setup_theory one
skalberg@14516
   347
skalberg@14516
   348
;end_setup
skalberg@14516
   349
skalberg@14516
   350
;setup_theory option
skalberg@14516
   351
skalberg@14516
   352
lemma option_CLAUSES: "(op &::bool => bool => bool)
obua@17644
   353
 ((All::('a::type => bool) => bool)
obua@17644
   354
   (%x::'a::type.
obua@17644
   355
       (All::('a::type => bool) => bool)
obua@17644
   356
        (%y::'a::type.
skalberg@14516
   357
            (op =::bool => bool => bool)
obua@17644
   358
             ((op =::'a::type option => 'a::type option => bool)
obua@17644
   359
               ((Some::'a::type ~=> 'a::type) x)
obua@17644
   360
               ((Some::'a::type ~=> 'a::type) y))
obua@17644
   361
             ((op =::'a::type => 'a::type => bool) x y))))
skalberg@14516
   362
 ((op &::bool => bool => bool)
obua@17644
   363
   ((All::('a::type => bool) => bool)
obua@17644
   364
     (%x::'a::type.
obua@17644
   365
         (op =::'a::type => 'a::type => bool)
obua@17644
   366
          ((the::'a::type option => 'a::type)
obua@17644
   367
            ((Some::'a::type ~=> 'a::type) x))
obua@17644
   368
          x))
skalberg@14516
   369
   ((op &::bool => bool => bool)
obua@17644
   370
     ((All::('a::type => bool) => bool)
obua@17644
   371
       (%x::'a::type.
skalberg@14516
   372
           (Not::bool => bool)
obua@17644
   373
            ((op =::'a::type option => 'a::type option => bool)
obua@17644
   374
              (None::'a::type option) ((Some::'a::type ~=> 'a::type) x))))
skalberg@14516
   375
     ((op &::bool => bool => bool)
obua@17644
   376
       ((All::('a::type => bool) => bool)
obua@17644
   377
         (%x::'a::type.
skalberg@14516
   378
             (Not::bool => bool)
obua@17644
   379
              ((op =::'a::type option => 'a::type option => bool)
obua@17644
   380
                ((Some::'a::type ~=> 'a::type) x) (None::'a::type option))))
skalberg@14516
   381
       ((op &::bool => bool => bool)
obua@17644
   382
         ((All::('a::type => bool) => bool)
obua@17644
   383
           (%x::'a::type.
skalberg@14516
   384
               (op =::bool => bool => bool)
obua@17644
   385
                ((IS_SOME::'a::type option => bool)
obua@17644
   386
                  ((Some::'a::type ~=> 'a::type) x))
skalberg@14516
   387
                (True::bool)))
skalberg@14516
   388
         ((op &::bool => bool => bool)
skalberg@14516
   389
           ((op =::bool => bool => bool)
obua@17644
   390
             ((IS_SOME::'a::type option => bool) (None::'a::type option))
obua@17644
   391
             (False::bool))
skalberg@14516
   392
           ((op &::bool => bool => bool)
obua@17644
   393
             ((All::('a::type option => bool) => bool)
obua@17644
   394
               (%x::'a::type option.
skalberg@14516
   395
                   (op =::bool => bool => bool)
obua@17644
   396
                    ((IS_NONE::'a::type option => bool) x)
obua@17644
   397
                    ((op =::'a::type option => 'a::type option => bool) x
obua@17644
   398
                      (None::'a::type option))))
skalberg@14516
   399
             ((op &::bool => bool => bool)
obua@17644
   400
               ((All::('a::type option => bool) => bool)
obua@17644
   401
                 (%x::'a::type option.
skalberg@14516
   402
                     (op =::bool => bool => bool)
obua@17644
   403
                      ((Not::bool => bool)
obua@17644
   404
                        ((IS_SOME::'a::type option => bool) x))
obua@17644
   405
                      ((op =::'a::type option => 'a::type option => bool) x
obua@17644
   406
                        (None::'a::type option))))
skalberg@14516
   407
               ((op &::bool => bool => bool)
obua@17644
   408
                 ((All::('a::type option => bool) => bool)
obua@17644
   409
                   (%x::'a::type option.
skalberg@14516
   410
                       (op -->::bool => bool => bool)
obua@17644
   411
                        ((IS_SOME::'a::type option => bool) x)
obua@17644
   412
                        ((op =::'a::type option => 'a::type option => bool)
obua@17644
   413
                          ((Some::'a::type ~=> 'a::type)
obua@17644
   414
                            ((the::'a::type option => 'a::type) x))
skalberg@14516
   415
                          x)))
skalberg@14516
   416
                 ((op &::bool => bool => bool)
obua@17644
   417
                   ((All::('a::type option => bool) => bool)
obua@17644
   418
                     (%x::'a::type option.
obua@17644
   419
                         (op =::'a::type option => 'a::type option => bool)
obua@17644
   420
                          ((option_case::'a::type option
obua@17644
   421
   => ('a::type ~=> 'a::type) => 'a::type option ~=> 'a::type)
obua@17644
   422
                            (None::'a::type option)
obua@17644
   423
                            (Some::'a::type ~=> 'a::type) x)
skalberg@14516
   424
                          x))
skalberg@14516
   425
                   ((op &::bool => bool => bool)
obua@17644
   426
                     ((All::('a::type option => bool) => bool)
obua@17644
   427
                       (%x::'a::type option.
obua@17644
   428
                           (op =::'a::type option
obua@17644
   429
                                  => 'a::type option => bool)
obua@17644
   430
                            ((option_case::'a::type option
obua@17644
   431
     => ('a::type ~=> 'a::type) => 'a::type option ~=> 'a::type)
obua@17644
   432
                              x (Some::'a::type ~=> 'a::type) x)
skalberg@14516
   433
                            x))
skalberg@14516
   434
                     ((op &::bool => bool => bool)
obua@17644
   435
                       ((All::('a::type option => bool) => bool)
obua@17644
   436
                         (%x::'a::type option.
skalberg@14516
   437
                             (op -->::bool => bool => bool)
obua@17644
   438
                              ((IS_NONE::'a::type option => bool) x)
obua@17644
   439
                              ((op =::'b::type => 'b::type => bool)
obua@17644
   440
                                ((option_case::'b::type
obua@17644
   441
         => ('a::type => 'b::type) => 'a::type option => 'b::type)
obua@17644
   442
                                  (e::'b::type) (f::'a::type => 'b::type) x)
skalberg@14516
   443
                                e)))
skalberg@14516
   444
                       ((op &::bool => bool => bool)
obua@17644
   445
                         ((All::('a::type option => bool) => bool)
obua@17644
   446
                           (%x::'a::type option.
skalberg@14516
   447
                               (op -->::bool => bool => bool)
obua@17644
   448
                                ((IS_SOME::'a::type option => bool) x)
obua@17644
   449
                                ((op =::'b::type => 'b::type => bool)
obua@17644
   450
                                  ((option_case::'b::type
obua@17644
   451
           => ('a::type => 'b::type) => 'a::type option => 'b::type)
skalberg@14516
   452
                                    e f x)
obua@17644
   453
                                  (f ((the::'a::type option => 'a::type)
obua@17644
   454
 x)))))
skalberg@14516
   455
                         ((op &::bool => bool => bool)
obua@17644
   456
                           ((All::('a::type option => bool) => bool)
obua@17644
   457
                             (%x::'a::type option.
skalberg@14516
   458
                                 (op -->::bool => bool => bool)
obua@17644
   459
                                  ((IS_SOME::'a::type option => bool) x)
obua@17644
   460
                                  ((op =::'a::type option
obua@17644
   461
    => 'a::type option => bool)
obua@17644
   462
                                    ((option_case::'a::type option
obua@17644
   463
             => ('a::type ~=> 'a::type) => 'a::type option ~=> 'a::type)
obua@17644
   464
(ea::'a::type option) (Some::'a::type ~=> 'a::type) x)
skalberg@14516
   465
                                    x)))
skalberg@14516
   466
                           ((op &::bool => bool => bool)
obua@17644
   467
                             ((All::('b::type => bool) => bool)
obua@17644
   468
                               (%u::'b::type.
obua@17644
   469
                                   (All::(('a::type => 'b::type) => bool)
obua@17644
   470
   => bool)
obua@17644
   471
                                    (%f::'a::type => 'b::type.
obua@17644
   472
  (op =::'b::type => 'b::type => bool)
obua@17644
   473
   ((option_case::'b::type
obua@17644
   474
                  => ('a::type => 'b::type) => 'a::type option => 'b::type)
obua@17644
   475
     u f (None::'a::type option))
skalberg@14516
   476
   u)))
skalberg@14516
   477
                             ((op &::bool => bool => bool)
obua@17644
   478
                               ((All::('b::type => bool) => bool)
obua@17644
   479
                                 (%u::'b::type.
obua@17644
   480
                                     (All::(('a::type => 'b::type) => bool)
obua@17644
   481
     => bool)
obua@17644
   482
(%f::'a::type => 'b::type.
obua@17644
   483
    (All::('a::type => bool) => bool)
obua@17644
   484
     (%x::'a::type.
obua@17644
   485
         (op =::'b::type => 'b::type => bool)
obua@17644
   486
          ((option_case::'b::type
obua@17644
   487
                         => ('a::type => 'b::type)
obua@17644
   488
                            => 'a::type option => 'b::type)
obua@17644
   489
            u f ((Some::'a::type ~=> 'a::type) x))
skalberg@14516
   490
          (f x)))))
skalberg@14516
   491
                               ((op &::bool => bool => bool)
obua@17644
   492
                                 ((All::(('a::type => 'b::type) => bool)
obua@17644
   493
  => bool)
obua@17644
   494
                                   (%f::'a::type => 'b::type.
obua@17644
   495
 (All::('a::type => bool) => bool)
obua@17644
   496
  (%x::'a::type.
obua@17644
   497
      (op =::'b::type option => 'b::type option => bool)
obua@17644
   498
       ((option_map::('a::type => 'b::type) => 'a::type option ~=> 'b::type)
obua@17644
   499
         f ((Some::'a::type ~=> 'a::type) x))
obua@17644
   500
       ((Some::'b::type ~=> 'b::type) (f x)))))
skalberg@14516
   501
                                 ((op &::bool => bool => bool)
obua@17644
   502
                                   ((All::(('a::type => 'b::type) => bool)
obua@17644
   503
    => bool)
obua@17644
   504
                                     (%f::'a::type => 'b::type.
obua@17644
   505
   (op =::'b::type option => 'b::type option => bool)
obua@17644
   506
    ((option_map::('a::type => 'b::type) => 'a::type option ~=> 'b::type) f
obua@17644
   507
      (None::'a::type option))
obua@17644
   508
    (None::'b::type option)))
skalberg@14516
   509
                                   ((op &::bool => bool => bool)
obua@17644
   510
                                     ((op =::'a::type option
obua@17644
   511
       => 'a::type option => bool)
obua@17644
   512
 ((OPTION_JOIN::'a::type option option ~=> 'a::type)
obua@17644
   513
   (None::'a::type option option))
obua@17644
   514
 (None::'a::type option))
obua@17644
   515
                                     ((All::('a::type option => bool)
obua@17644
   516
      => bool)
obua@17644
   517
 (%x::'a::type option.
obua@17644
   518
     (op =::'a::type option => 'a::type option => bool)
obua@17644
   519
      ((OPTION_JOIN::'a::type option option ~=> 'a::type)
obua@17644
   520
        ((Some::'a::type option ~=> 'a::type option) x))
skalberg@14516
   521
      x))))))))))))))))))))"
skalberg@14516
   522
  by (import option option_CLAUSES)
skalberg@14516
   523
obua@17644
   524
lemma option_case_compute: "option_case (e::'b::type) (f::'a::type => 'b::type) (x::'a::type option) =
skalberg@14516
   525
(if IS_SOME x then f (the x) else e)"
skalberg@14516
   526
  by (import option option_case_compute)
skalberg@14516
   527
obua@17644
   528
lemma OPTION_MAP_EQ_SOME: "ALL (f::'a::type => 'b::type) (x::'a::type option) y::'b::type.
obua@17644
   529
   (option_map f x = Some y) = (EX z::'a::type. x = Some z & y = f z)"
skalberg@14516
   530
  by (import option OPTION_MAP_EQ_SOME)
skalberg@14516
   531
obua@17644
   532
lemma OPTION_JOIN_EQ_SOME: "ALL (x::'a::type option option) xa::'a::type.
obua@17644
   533
   (OPTION_JOIN x = Some xa) = (x = Some (Some xa))"
skalberg@14516
   534
  by (import option OPTION_JOIN_EQ_SOME)
skalberg@14516
   535
obua@17644
   536
lemma option_case_cong: "ALL (M::'a::type option) (M'::'a::type option) (u::'b::type)
obua@17644
   537
   f::'a::type => 'b::type.
obua@17644
   538
   M = M' &
obua@17644
   539
   (M' = None --> u = (u'::'b::type)) &
obua@17644
   540
   (ALL x::'a::type. M' = Some x --> f x = (f'::'a::type => 'b::type) x) -->
skalberg@14516
   541
   option_case u f M = option_case u' f' M'"
skalberg@14516
   542
  by (import option option_case_cong)
skalberg@14516
   543
skalberg@14516
   544
;end_setup
skalberg@14516
   545
skalberg@14516
   546
;setup_theory marker
skalberg@14516
   547
skalberg@14516
   548
consts
obua@17652
   549
  stmarker :: "'a => 'a" 
skalberg@14516
   550
skalberg@14516
   551
defs
obua@17644
   552
  stmarker_primdef: "stmarker == %x::'a::type. x"
obua@17644
   553
obua@17644
   554
lemma stmarker_def: "ALL x::'a::type. stmarker x = x"
skalberg@14516
   555
  by (import marker stmarker_def)
skalberg@14516
   556
obua@17644
   557
lemma move_left_conj: "ALL (x::bool) (xa::bool) xb::bool.
skalberg@14516
   558
   (x & stmarker xb) = (stmarker xb & x) &
skalberg@14516
   559
   ((stmarker xb & x) & xa) = (stmarker xb & x & xa) &
skalberg@14516
   560
   (x & stmarker xb & xa) = (stmarker xb & x & xa)"
skalberg@14516
   561
  by (import marker move_left_conj)
skalberg@14516
   562
obua@17644
   563
lemma move_right_conj: "ALL (x::bool) (xa::bool) xb::bool.
skalberg@14516
   564
   (stmarker xb & x) = (x & stmarker xb) &
skalberg@14516
   565
   (x & xa & stmarker xb) = ((x & xa) & stmarker xb) &
skalberg@14516
   566
   ((x & stmarker xb) & xa) = ((x & xa) & stmarker xb)"
skalberg@14516
   567
  by (import marker move_right_conj)
skalberg@14516
   568
obua@17644
   569
lemma move_left_disj: "ALL (x::bool) (xa::bool) xb::bool.
skalberg@14516
   570
   (x | stmarker xb) = (stmarker xb | x) &
skalberg@14516
   571
   ((stmarker xb | x) | xa) = (stmarker xb | x | xa) &
skalberg@14516
   572
   (x | stmarker xb | xa) = (stmarker xb | x | xa)"
skalberg@14516
   573
  by (import marker move_left_disj)
skalberg@14516
   574
obua@17644
   575
lemma move_right_disj: "ALL (x::bool) (xa::bool) xb::bool.
skalberg@14516
   576
   (stmarker xb | x) = (x | stmarker xb) &
skalberg@14516
   577
   (x | xa | stmarker xb) = ((x | xa) | stmarker xb) &
skalberg@14516
   578
   ((x | stmarker xb) | xa) = ((x | xa) | stmarker xb)"
skalberg@14516
   579
  by (import marker move_right_disj)
skalberg@14516
   580
skalberg@14516
   581
;end_setup
skalberg@14516
   582
skalberg@14516
   583
;setup_theory relation
skalberg@14516
   584
skalberg@14516
   585
constdefs
obua@17652
   586
  TC :: "('a => 'a => bool) => 'a => 'a => bool" 
skalberg@14516
   587
  "TC ==
obua@17644
   588
%(R::'a::type => 'a::type => bool) (a::'a::type) b::'a::type.
obua@17644
   589
   ALL P::'a::type => 'a::type => bool.
obua@17644
   590
      (ALL (x::'a::type) y::'a::type. R x y --> P x y) &
obua@17644
   591
      (ALL (x::'a::type) (y::'a::type) z::'a::type.
obua@17644
   592
          P x y & P y z --> P x z) -->
skalberg@14516
   593
      P a b"
skalberg@14516
   594
obua@17644
   595
lemma TC_DEF: "ALL (R::'a::type => 'a::type => bool) (a::'a::type) b::'a::type.
skalberg@14516
   596
   TC R a b =
obua@17644
   597
   (ALL P::'a::type => 'a::type => bool.
obua@17644
   598
       (ALL (x::'a::type) y::'a::type. R x y --> P x y) &
obua@17644
   599
       (ALL (x::'a::type) (y::'a::type) z::'a::type.
obua@17644
   600
           P x y & P y z --> P x z) -->
skalberg@14516
   601
       P a b)"
skalberg@14516
   602
  by (import relation TC_DEF)
skalberg@14516
   603
skalberg@14516
   604
constdefs
obua@17652
   605
  RTC :: "('a => 'a => bool) => 'a => 'a => bool" 
skalberg@14516
   606
  "RTC ==
obua@17644
   607
%(R::'a::type => 'a::type => bool) (a::'a::type) b::'a::type.
obua@17644
   608
   ALL P::'a::type => 'a::type => bool.
obua@17644
   609
      (ALL x::'a::type. P x x) &
obua@17644
   610
      (ALL (x::'a::type) (y::'a::type) z::'a::type.
obua@17644
   611
          R x y & P y z --> P x z) -->
obua@17644
   612
      P a b"
obua@17644
   613
obua@17644
   614
lemma RTC_DEF: "ALL (R::'a::type => 'a::type => bool) (a::'a::type) b::'a::type.
skalberg@14516
   615
   RTC R a b =
obua@17644
   616
   (ALL P::'a::type => 'a::type => bool.
obua@17644
   617
       (ALL x::'a::type. P x x) &
obua@17644
   618
       (ALL (x::'a::type) (y::'a::type) z::'a::type.
obua@17644
   619
           R x y & P y z --> P x z) -->
obua@17644
   620
       P a b)"
skalberg@14516
   621
  by (import relation RTC_DEF)
skalberg@14516
   622
skalberg@14516
   623
consts
obua@17652
   624
  RC :: "('a => 'a => bool) => 'a => 'a => bool" 
skalberg@14516
   625
skalberg@14516
   626
defs
obua@17644
   627
  RC_primdef: "RC ==
obua@17644
   628
%(R::'a::type => 'a::type => bool) (x::'a::type) y::'a::type. x = y | R x y"
obua@17644
   629
obua@17644
   630
lemma RC_def: "ALL (R::'a::type => 'a::type => bool) (x::'a::type) y::'a::type.
obua@17644
   631
   RC R x y = (x = y | R x y)"
skalberg@14516
   632
  by (import relation RC_def)
skalberg@14516
   633
skalberg@14516
   634
consts
obua@17652
   635
  transitive :: "('a => 'a => bool) => bool" 
skalberg@14516
   636
skalberg@14516
   637
defs
obua@17644
   638
  transitive_primdef: "transitive ==
obua@17644
   639
%R::'a::type => 'a::type => bool.
obua@17644
   640
   ALL (x::'a::type) (y::'a::type) z::'a::type. R x y & R y z --> R x z"
obua@17644
   641
obua@17644
   642
lemma transitive_def: "ALL R::'a::type => 'a::type => bool.
obua@17644
   643
   transitive R =
obua@17644
   644
   (ALL (x::'a::type) (y::'a::type) z::'a::type. R x y & R y z --> R x z)"
skalberg@14516
   645
  by (import relation transitive_def)
skalberg@14516
   646
skalberg@14516
   647
constdefs
obua@17652
   648
  pred_reflexive :: "('a => 'a => bool) => bool" 
obua@17644
   649
  "pred_reflexive == %R::'a::type => 'a::type => bool. ALL x::'a::type. R x x"
obua@17644
   650
obua@17644
   651
lemma reflexive_def: "ALL R::'a::type => 'a::type => bool.
obua@17644
   652
   pred_reflexive R = (ALL x::'a::type. R x x)"
skalberg@14516
   653
  by (import relation reflexive_def)
skalberg@14516
   654
obua@17644
   655
lemma TC_TRANSITIVE: "ALL x::'a::type => 'a::type => bool. transitive (TC x)"
skalberg@14516
   656
  by (import relation TC_TRANSITIVE)
skalberg@14516
   657
obua@17644
   658
lemma RTC_INDUCT: "ALL (x::'a::type => 'a::type => bool) xa::'a::type => 'a::type => bool.
obua@17644
   659
   (ALL x::'a::type. xa x x) &
obua@17644
   660
   (ALL (xb::'a::type) (y::'a::type) z::'a::type.
obua@17644
   661
       x xb y & xa y z --> xa xb z) -->
obua@17644
   662
   (ALL (xb::'a::type) xc::'a::type. RTC x xb xc --> xa xb xc)"
skalberg@14516
   663
  by (import relation RTC_INDUCT)
skalberg@14516
   664
obua@17644
   665
lemma TC_RULES: "ALL x::'a::type => 'a::type => bool.
obua@17644
   666
   (ALL (xa::'a::type) xb::'a::type. x xa xb --> TC x xa xb) &
obua@17644
   667
   (ALL (xa::'a::type) (xb::'a::type) xc::'a::type.
obua@17644
   668
       TC x xa xb & TC x xb xc --> TC x xa xc)"
skalberg@14516
   669
  by (import relation TC_RULES)
skalberg@14516
   670
obua@17644
   671
lemma RTC_RULES: "ALL x::'a::type => 'a::type => bool.
obua@17644
   672
   (ALL xa::'a::type. RTC x xa xa) &
obua@17644
   673
   (ALL (xa::'a::type) (xb::'a::type) xc::'a::type.
obua@17644
   674
       x xa xb & RTC x xb xc --> RTC x xa xc)"
skalberg@14516
   675
  by (import relation RTC_RULES)
skalberg@14516
   676
obua@17644
   677
lemma RTC_STRONG_INDUCT: "ALL (R::'a::type => 'a::type => bool) P::'a::type => 'a::type => bool.
obua@17644
   678
   (ALL x::'a::type. P x x) &
obua@17644
   679
   (ALL (x::'a::type) (y::'a::type) z::'a::type.
obua@17644
   680
       R x y & RTC R y z & P y z --> P x z) -->
obua@17644
   681
   (ALL (x::'a::type) y::'a::type. RTC R x y --> P x y)"
skalberg@14516
   682
  by (import relation RTC_STRONG_INDUCT)
skalberg@14516
   683
obua@17644
   684
lemma RTC_RTC: "ALL (R::'a::type => 'a::type => bool) (x::'a::type) y::'a::type.
obua@17644
   685
   RTC R x y --> (ALL z::'a::type. RTC R y z --> RTC R x z)"
skalberg@14516
   686
  by (import relation RTC_RTC)
skalberg@14516
   687
obua@17644
   688
lemma RTC_TRANSITIVE: "ALL x::'a::type => 'a::type => bool. transitive (RTC x)"
skalberg@14516
   689
  by (import relation RTC_TRANSITIVE)
skalberg@14516
   690
obua@17644
   691
lemma RTC_REFLEXIVE: "ALL R::'a::type => 'a::type => bool. pred_reflexive (RTC R)"
skalberg@14516
   692
  by (import relation RTC_REFLEXIVE)
skalberg@14516
   693
obua@17644
   694
lemma RC_REFLEXIVE: "ALL R::'a::type => 'a::type => bool. pred_reflexive (RC R)"
skalberg@14516
   695
  by (import relation RC_REFLEXIVE)
skalberg@14516
   696
obua@17644
   697
lemma TC_SUBSET: "ALL (x::'a::type => 'a::type => bool) (xa::'a::type) xb::'a::type.
obua@17644
   698
   x xa xb --> TC x xa xb"
skalberg@14516
   699
  by (import relation TC_SUBSET)
skalberg@14516
   700
obua@17644
   701
lemma RTC_SUBSET: "ALL (R::'a::type => 'a::type => bool) (x::'a::type) y::'a::type.
obua@17644
   702
   R x y --> RTC R x y"
skalberg@14516
   703
  by (import relation RTC_SUBSET)
skalberg@14516
   704
obua@17644
   705
lemma RC_SUBSET: "ALL (R::'a::type => 'a::type => bool) (x::'a::type) y::'a::type.
obua@17644
   706
   R x y --> RC R x y"
skalberg@14516
   707
  by (import relation RC_SUBSET)
skalberg@14516
   708
obua@17644
   709
lemma RC_RTC: "ALL (R::'a::type => 'a::type => bool) (x::'a::type) y::'a::type.
obua@17644
   710
   RC R x y --> RTC R x y"
skalberg@14516
   711
  by (import relation RC_RTC)
skalberg@14516
   712
obua@17644
   713
lemma TC_INDUCT: "ALL (x::'a::type => 'a::type => bool) xa::'a::type => 'a::type => bool.
obua@17644
   714
   (ALL (xb::'a::type) y::'a::type. x xb y --> xa xb y) &
obua@17644
   715
   (ALL (x::'a::type) (y::'a::type) z::'a::type.
obua@17644
   716
       xa x y & xa y z --> xa x z) -->
obua@17644
   717
   (ALL (xb::'a::type) xc::'a::type. TC x xb xc --> xa xb xc)"
skalberg@14516
   718
  by (import relation TC_INDUCT)
skalberg@14516
   719
obua@17644
   720
lemma TC_INDUCT_LEFT1: "ALL (x::'a::type => 'a::type => bool) xa::'a::type => 'a::type => bool.
obua@17644
   721
   (ALL (xb::'a::type) y::'a::type. x xb y --> xa xb y) &
obua@17644
   722
   (ALL (xb::'a::type) (y::'a::type) z::'a::type.
obua@17644
   723
       x xb y & xa y z --> xa xb z) -->
obua@17644
   724
   (ALL (xb::'a::type) xc::'a::type. TC x xb xc --> xa xb xc)"
skalberg@14516
   725
  by (import relation TC_INDUCT_LEFT1)
skalberg@14516
   726
obua@17644
   727
lemma TC_STRONG_INDUCT: "ALL (R::'a::type => 'a::type => bool) P::'a::type => 'a::type => bool.
obua@17644
   728
   (ALL (x::'a::type) y::'a::type. R x y --> P x y) &
obua@17644
   729
   (ALL (x::'a::type) (y::'a::type) z::'a::type.
obua@17644
   730
       P x y & P y z & TC R x y & TC R y z --> P x z) -->
obua@17644
   731
   (ALL (u::'a::type) v::'a::type. TC R u v --> P u v)"
skalberg@14516
   732
  by (import relation TC_STRONG_INDUCT)
skalberg@14516
   733
obua@17644
   734
lemma TC_STRONG_INDUCT_LEFT1: "ALL (R::'a::type => 'a::type => bool) P::'a::type => 'a::type => bool.
obua@17644
   735
   (ALL (x::'a::type) y::'a::type. R x y --> P x y) &
obua@17644
   736
   (ALL (x::'a::type) (y::'a::type) z::'a::type.
obua@17644
   737
       R x y & P y z & TC R y z --> P x z) -->
obua@17644
   738
   (ALL (u::'a::type) v::'a::type. TC R u v --> P u v)"
skalberg@14516
   739
  by (import relation TC_STRONG_INDUCT_LEFT1)
skalberg@14516
   740
obua@17644
   741
lemma TC_RTC: "ALL (R::'a::type => 'a::type => bool) (x::'a::type) y::'a::type.
obua@17644
   742
   TC R x y --> RTC R x y"
skalberg@14516
   743
  by (import relation TC_RTC)
skalberg@14516
   744
obua@17644
   745
lemma RTC_TC_RC: "ALL (R::'a::type => 'a::type => bool) (x::'a::type) y::'a::type.
obua@17644
   746
   RTC R x y --> RC R x y | TC R x y"
skalberg@14516
   747
  by (import relation RTC_TC_RC)
skalberg@14516
   748
obua@17644
   749
lemma TC_RC_EQNS: "ALL R::'a::type => 'a::type => bool. RC (TC R) = RTC R & TC (RC R) = RTC R"
skalberg@14516
   750
  by (import relation TC_RC_EQNS)
skalberg@14516
   751
obua@17644
   752
lemma RC_IDEM: "ALL R::'a::type => 'a::type => bool. RC (RC R) = RC R"
skalberg@14516
   753
  by (import relation RC_IDEM)
skalberg@14516
   754
obua@17644
   755
lemma TC_IDEM: "ALL R::'a::type => 'a::type => bool. TC (TC R) = TC R"
skalberg@14516
   756
  by (import relation TC_IDEM)
skalberg@14516
   757
obua@17644
   758
lemma RTC_IDEM: "ALL R::'a::type => 'a::type => bool. RTC (RTC R) = RTC R"
skalberg@14516
   759
  by (import relation RTC_IDEM)
skalberg@14516
   760
obua@17644
   761
lemma RTC_CASES1: "ALL (x::'a::type => 'a::type => bool) (xa::'a::type) xb::'a::type.
obua@17644
   762
   RTC x xa xb = (xa = xb | (EX u::'a::type. x xa u & RTC x u xb))"
skalberg@14516
   763
  by (import relation RTC_CASES1)
skalberg@14516
   764
obua@17644
   765
lemma RTC_CASES2: "ALL (x::'a::type => 'a::type => bool) (xa::'a::type) xb::'a::type.
obua@17644
   766
   RTC x xa xb = (xa = xb | (EX u::'a::type. RTC x xa u & x u xb))"
skalberg@14516
   767
  by (import relation RTC_CASES2)
skalberg@14516
   768
obua@17644
   769
lemma RTC_CASES_RTC_TWICE: "ALL (x::'a::type => 'a::type => bool) (xa::'a::type) xb::'a::type.
obua@17644
   770
   RTC x xa xb = (EX u::'a::type. RTC x xa u & RTC x u xb)"
skalberg@14516
   771
  by (import relation RTC_CASES_RTC_TWICE)
skalberg@14516
   772
obua@17644
   773
lemma TC_CASES1: "ALL (R::'a::type => 'a::type => bool) (x::'a::type) z::'a::type.
obua@17644
   774
   TC R x z --> R x z | (EX y::'a::type. R x y & TC R y z)"
skalberg@14516
   775
  by (import relation TC_CASES1)
skalberg@14516
   776
obua@17644
   777
lemma TC_CASES2: "ALL (R::'a::type => 'a::type => bool) (x::'a::type) z::'a::type.
obua@17644
   778
   TC R x z --> R x z | (EX y::'a::type. TC R x y & R y z)"
skalberg@14516
   779
  by (import relation TC_CASES2)
skalberg@14516
   780
obua@17644
   781
lemma TC_MONOTONE: "ALL (R::'a::type => 'a::type => bool) Q::'a::type => 'a::type => bool.
obua@17644
   782
   (ALL (x::'a::type) y::'a::type. R x y --> Q x y) -->
obua@17644
   783
   (ALL (x::'a::type) y::'a::type. TC R x y --> TC Q x y)"
skalberg@14516
   784
  by (import relation TC_MONOTONE)
skalberg@14516
   785
obua@17644
   786
lemma RTC_MONOTONE: "ALL (R::'a::type => 'a::type => bool) Q::'a::type => 'a::type => bool.
obua@17644
   787
   (ALL (x::'a::type) y::'a::type. R x y --> Q x y) -->
obua@17644
   788
   (ALL (x::'a::type) y::'a::type. RTC R x y --> RTC Q x y)"
skalberg@14516
   789
  by (import relation RTC_MONOTONE)
skalberg@14516
   790
skalberg@14516
   791
constdefs
obua@17652
   792
  WF :: "('a => 'a => bool) => bool" 
obua@17644
   793
  "WF ==
obua@17644
   794
%R::'a::type => 'a::type => bool.
obua@17644
   795
   ALL B::'a::type => bool.
obua@17644
   796
      Ex B -->
obua@17644
   797
      (EX min::'a::type. B min & (ALL b::'a::type. R b min --> ~ B b))"
obua@17644
   798
obua@17644
   799
lemma WF_DEF: "ALL R::'a::type => 'a::type => bool.
obua@17644
   800
   WF R =
obua@17644
   801
   (ALL B::'a::type => bool.
obua@17644
   802
       Ex B -->
obua@17644
   803
       (EX min::'a::type. B min & (ALL b::'a::type. R b min --> ~ B b)))"
skalberg@14516
   804
  by (import relation WF_DEF)
skalberg@14516
   805
obua@17644
   806
lemma WF_INDUCTION_THM: "ALL R::'a::type => 'a::type => bool.
obua@17644
   807
   WF R -->
obua@17644
   808
   (ALL P::'a::type => bool.
obua@17644
   809
       (ALL x::'a::type. (ALL y::'a::type. R y x --> P y) --> P x) -->
obua@17644
   810
       All P)"
skalberg@14516
   811
  by (import relation WF_INDUCTION_THM)
skalberg@14516
   812
obua@17644
   813
lemma WF_NOT_REFL: "ALL (x::'a::type => 'a::type => bool) (xa::'a::type) xb::'a::type.
obua@17644
   814
   WF x --> x xa xb --> xa ~= xb"
skalberg@14516
   815
  by (import relation WF_NOT_REFL)
skalberg@14516
   816
skalberg@14516
   817
constdefs
obua@17652
   818
  EMPTY_REL :: "'a => 'a => bool" 
obua@17644
   819
  "EMPTY_REL == %(x::'a::type) y::'a::type. False"
obua@17644
   820
obua@17644
   821
lemma EMPTY_REL_DEF: "ALL (x::'a::type) y::'a::type. EMPTY_REL x y = False"
skalberg@14516
   822
  by (import relation EMPTY_REL_DEF)
skalberg@14516
   823
skalberg@14516
   824
lemma WF_EMPTY_REL: "WF EMPTY_REL"
skalberg@14516
   825
  by (import relation WF_EMPTY_REL)
skalberg@14516
   826
obua@17644
   827
lemma WF_SUBSET: "ALL (x::'a::type => 'a::type => bool) xa::'a::type => 'a::type => bool.
obua@17644
   828
   WF x & (ALL (xb::'a::type) y::'a::type. xa xb y --> x xb y) --> WF xa"
skalberg@14516
   829
  by (import relation WF_SUBSET)
skalberg@14516
   830
obua@17644
   831
lemma WF_TC: "ALL R::'a::type => 'a::type => bool. WF R --> WF (TC R)"
skalberg@14516
   832
  by (import relation WF_TC)
skalberg@14516
   833
skalberg@14516
   834
consts
obua@17652
   835
  inv_image :: "('b => 'b => bool) => ('a => 'b) => 'a => 'a => bool" 
skalberg@14516
   836
skalberg@14516
   837
defs
skalberg@14516
   838
  inv_image_primdef: "relation.inv_image ==
obua@17644
   839
%(R::'b::type => 'b::type => bool) (f::'a::type => 'b::type) (x::'a::type)
obua@17644
   840
   y::'a::type. R (f x) (f y)"
obua@17644
   841
obua@17644
   842
lemma inv_image_def: "ALL (R::'b::type => 'b::type => bool) f::'a::type => 'b::type.
obua@17644
   843
   relation.inv_image R f = (%(x::'a::type) y::'a::type. R (f x) (f y))"
skalberg@14516
   844
  by (import relation inv_image_def)
skalberg@14516
   845
obua@17644
   846
lemma WF_inv_image: "ALL (R::'b::type => 'b::type => bool) f::'a::type => 'b::type.
obua@17644
   847
   WF R --> WF (relation.inv_image R f)"
skalberg@14516
   848
  by (import relation WF_inv_image)
skalberg@14516
   849
skalberg@14516
   850
constdefs
obua@17652
   851
  RESTRICT :: "('a => 'b) => ('a => 'a => bool) => 'a => 'a => 'b" 
obua@17644
   852
  "RESTRICT ==
obua@17644
   853
%(f::'a::type => 'b::type) (R::'a::type => 'a::type => bool) (x::'a::type)
obua@17644
   854
   y::'a::type. if R y x then f y else ARB"
obua@17644
   855
obua@17644
   856
lemma RESTRICT_DEF: "ALL (f::'a::type => 'b::type) (R::'a::type => 'a::type => bool) x::'a::type.
obua@17644
   857
   RESTRICT f R x = (%y::'a::type. if R y x then f y else ARB)"
skalberg@14516
   858
  by (import relation RESTRICT_DEF)
skalberg@14516
   859
obua@17644
   860
lemma RESTRICT_LEMMA: "ALL (x::'a::type => 'b::type) (xa::'a::type => 'a::type => bool)
obua@17644
   861
   (xb::'a::type) xc::'a::type. xa xb xc --> RESTRICT x xa xc xb = x xb"
skalberg@14516
   862
  by (import relation RESTRICT_LEMMA)
skalberg@14516
   863
skalberg@14516
   864
consts
obua@17652
   865
  approx :: "('a => 'a => bool) => (('a => 'b) => 'a => 'b) => 'a => ('a => 'b) => bool" 
skalberg@14516
   866
skalberg@14516
   867
defs
obua@17644
   868
  approx_primdef: "approx ==
obua@17644
   869
%(R::'a::type => 'a::type => bool)
obua@17644
   870
   (M::('a::type => 'b::type) => 'a::type => 'b::type) (x::'a::type)
obua@17644
   871
   f::'a::type => 'b::type.
obua@17644
   872
   f = RESTRICT (%y::'a::type. M (RESTRICT f R y) y) R x"
obua@17644
   873
obua@17644
   874
lemma approx_def: "ALL (R::'a::type => 'a::type => bool)
obua@17644
   875
   (M::('a::type => 'b::type) => 'a::type => 'b::type) (x::'a::type)
obua@17644
   876
   f::'a::type => 'b::type.
obua@17644
   877
   approx R M x f = (f = RESTRICT (%y::'a::type. M (RESTRICT f R y) y) R x)"
skalberg@14516
   878
  by (import relation approx_def)
skalberg@14516
   879
skalberg@14516
   880
consts
obua@17652
   881
  the_fun :: "('a => 'a => bool) => (('a => 'b) => 'a => 'b) => 'a => 'a => 'b" 
skalberg@14516
   882
skalberg@14516
   883
defs
obua@17644
   884
  the_fun_primdef: "the_fun ==
obua@17644
   885
%(R::'a::type => 'a::type => bool)
obua@17644
   886
   (M::('a::type => 'b::type) => 'a::type => 'b::type) x::'a::type.
obua@17644
   887
   Eps (approx R M x)"
obua@17644
   888
obua@17644
   889
lemma the_fun_def: "ALL (R::'a::type => 'a::type => bool)
obua@17644
   890
   (M::('a::type => 'b::type) => 'a::type => 'b::type) x::'a::type.
obua@17644
   891
   the_fun R M x = Eps (approx R M x)"
skalberg@14516
   892
  by (import relation the_fun_def)
skalberg@14516
   893
skalberg@14516
   894
constdefs
obua@17652
   895
  WFREC :: "('a => 'a => bool) => (('a => 'b) => 'a => 'b) => 'a => 'b" 
skalberg@14516
   896
  "WFREC ==
obua@17644
   897
%(R::'a::type => 'a::type => bool)
obua@17644
   898
   (M::('a::type => 'b::type) => 'a::type => 'b::type) x::'a::type.
obua@17644
   899
   M (RESTRICT
obua@17644
   900
       (the_fun (TC R)
obua@17644
   901
         (%(f::'a::type => 'b::type) v::'a::type. M (RESTRICT f R v) v) x)
obua@17644
   902
       R x)
obua@17644
   903
    x"
obua@17644
   904
obua@17644
   905
lemma WFREC_DEF: "ALL (R::'a::type => 'a::type => bool)
obua@17644
   906
   M::('a::type => 'b::type) => 'a::type => 'b::type.
skalberg@14516
   907
   WFREC R M =
obua@17644
   908
   (%x::'a::type.
obua@17644
   909
       M (RESTRICT
obua@17644
   910
           (the_fun (TC R)
obua@17644
   911
             (%(f::'a::type => 'b::type) v::'a::type. M (RESTRICT f R v) v)
obua@17644
   912
             x)
obua@17644
   913
           R x)
obua@17644
   914
        x)"
skalberg@14516
   915
  by (import relation WFREC_DEF)
skalberg@14516
   916
obua@17644
   917
lemma WFREC_THM: "ALL (R::'a::type => 'a::type => bool)
obua@17644
   918
   M::('a::type => 'b::type) => 'a::type => 'b::type.
obua@17644
   919
   WF R --> (ALL x::'a::type. WFREC R M x = M (RESTRICT (WFREC R M) R x) x)"
skalberg@14516
   920
  by (import relation WFREC_THM)
skalberg@14516
   921
obua@17644
   922
lemma WFREC_COROLLARY: "ALL (M::('a::type => 'b::type) => 'a::type => 'b::type)
obua@17644
   923
   (R::'a::type => 'a::type => bool) f::'a::type => 'b::type.
obua@17644
   924
   f = WFREC R M --> WF R --> (ALL x::'a::type. f x = M (RESTRICT f R x) x)"
skalberg@14516
   925
  by (import relation WFREC_COROLLARY)
skalberg@14516
   926
obua@17644
   927
lemma WF_RECURSION_THM: "ALL R::'a::type => 'a::type => bool.
obua@17644
   928
   WF R -->
obua@17644
   929
   (ALL M::('a::type => 'b::type) => 'a::type => 'b::type.
obua@17644
   930
       EX! f::'a::type => 'b::type.
obua@17644
   931
          ALL x::'a::type. f x = M (RESTRICT f R x) x)"
skalberg@14516
   932
  by (import relation WF_RECURSION_THM)
skalberg@14516
   933
skalberg@14516
   934
;end_setup
skalberg@14516
   935
skalberg@14516
   936
;setup_theory pair
skalberg@14516
   937
obua@17644
   938
lemma CURRY_ONE_ONE_THM: "(curry (f::'a::type * 'b::type => 'c::type) =
obua@17644
   939
 curry (g::'a::type * 'b::type => 'c::type)) =
obua@17644
   940
(f = g)"
skalberg@14516
   941
  by (import pair CURRY_ONE_ONE_THM)
skalberg@14516
   942
skalberg@15647
   943
lemma UNCURRY_ONE_ONE_THM: "(op =::bool => bool => bool)
obua@17644
   944
 ((op =::('a::type * 'b::type => 'c::type)
obua@17644
   945
         => ('a::type * 'b::type => 'c::type) => bool)
obua@17644
   946
   ((split::('a::type => 'b::type => 'c::type)
obua@17644
   947
            => 'a::type * 'b::type => 'c::type)
obua@17644
   948
     (f::'a::type => 'b::type => 'c::type))
obua@17644
   949
   ((split::('a::type => 'b::type => 'c::type)
obua@17644
   950
            => 'a::type * 'b::type => 'c::type)
obua@17644
   951
     (g::'a::type => 'b::type => 'c::type)))
obua@17644
   952
 ((op =::('a::type => 'b::type => 'c::type)
obua@17644
   953
         => ('a::type => 'b::type => 'c::type) => bool)
obua@17644
   954
   f g)"
skalberg@14516
   955
  by (import pair UNCURRY_ONE_ONE_THM)
skalberg@14516
   956
obua@17644
   957
lemma pair_Axiom: "ALL f::'a::type => 'b::type => 'c::type.
obua@17644
   958
   EX x::'a::type * 'b::type => 'c::type.
obua@17644
   959
      ALL (xa::'a::type) y::'b::type. x (xa, y) = f xa y"
skalberg@14516
   960
  by (import pair pair_Axiom)
skalberg@14516
   961
obua@17644
   962
lemma UNCURRY_CONG: "ALL (M::'a::type * 'b::type) (M'::'a::type * 'b::type)
obua@17644
   963
   f::'a::type => 'b::type => 'c::type.
obua@17644
   964
   M = M' &
obua@17644
   965
   (ALL (x::'a::type) y::'b::type.
obua@17644
   966
       M' = (x, y) -->
obua@17644
   967
       f x y = (f'::'a::type => 'b::type => 'c::type) x y) -->
skalberg@14516
   968
   split f M = split f' M'"
skalberg@14516
   969
  by (import pair UNCURRY_CONG)
skalberg@14516
   970
obua@17644
   971
lemma ELIM_PEXISTS: "(EX p::'a::type * 'b::type.
obua@17644
   972
    (P::'a::type => 'b::type => bool) (fst p) (snd p)) =
obua@17644
   973
(EX p1::'a::type. Ex (P p1))"
skalberg@14516
   974
  by (import pair ELIM_PEXISTS)
skalberg@14516
   975
obua@17644
   976
lemma ELIM_PFORALL: "(ALL p::'a::type * 'b::type.
obua@17644
   977
    (P::'a::type => 'b::type => bool) (fst p) (snd p)) =
obua@17644
   978
(ALL p1::'a::type. All (P p1))"
skalberg@14516
   979
  by (import pair ELIM_PFORALL)
skalberg@14516
   980
obua@17644
   981
lemma PFORALL_THM: "(All::(('a::type => 'b::type => bool) => bool) => bool)
obua@17644
   982
 (%x::'a::type => 'b::type => bool.
skalberg@15647
   983
     (op =::bool => bool => bool)
obua@17644
   984
      ((All::('a::type => bool) => bool)
obua@17644
   985
        (%xa::'a::type. (All::('b::type => bool) => bool) (x xa)))
obua@17644
   986
      ((All::('a::type * 'b::type => bool) => bool)
obua@17644
   987
        ((split::('a::type => 'b::type => bool)
obua@17644
   988
                 => 'a::type * 'b::type => bool)
obua@17644
   989
          x)))"
skalberg@14516
   990
  by (import pair PFORALL_THM)
skalberg@14516
   991
obua@17644
   992
lemma PEXISTS_THM: "(All::(('a::type => 'b::type => bool) => bool) => bool)
obua@17644
   993
 (%x::'a::type => 'b::type => bool.
skalberg@15647
   994
     (op =::bool => bool => bool)
obua@17644
   995
      ((Ex::('a::type => bool) => bool)
obua@17644
   996
        (%xa::'a::type. (Ex::('b::type => bool) => bool) (x xa)))
obua@17644
   997
      ((Ex::('a::type * 'b::type => bool) => bool)
obua@17644
   998
        ((split::('a::type => 'b::type => bool)
obua@17644
   999
                 => 'a::type * 'b::type => bool)
obua@17644
  1000
          x)))"
skalberg@14516
  1001
  by (import pair PEXISTS_THM)
skalberg@14516
  1002
obua@17644
  1003
lemma LET2_RAND: "(All::(('c::type => 'd::type) => bool) => bool)
obua@17644
  1004
 (%x::'c::type => 'd::type.
obua@17644
  1005
     (All::('a::type * 'b::type => bool) => bool)
obua@17644
  1006
      (%xa::'a::type * 'b::type.
obua@17644
  1007
          (All::(('a::type => 'b::type => 'c::type) => bool) => bool)
obua@17644
  1008
           (%xb::'a::type => 'b::type => 'c::type.
obua@17644
  1009
               (op =::'d::type => 'd::type => bool)
obua@17644
  1010
                (x ((Let::'a::type * 'b::type
obua@17644
  1011
                          => ('a::type * 'b::type => 'c::type) => 'c::type)
obua@17644
  1012
                     xa ((split::('a::type => 'b::type => 'c::type)
obua@17644
  1013
                                 => 'a::type * 'b::type => 'c::type)
obua@17644
  1014
                          xb)))
obua@17644
  1015
                ((Let::'a::type * 'b::type
obua@17644
  1016
                       => ('a::type * 'b::type => 'd::type) => 'd::type)
obua@17644
  1017
                  xa ((split::('a::type => 'b::type => 'd::type)
obua@17644
  1018
                              => 'a::type * 'b::type => 'd::type)
obua@17644
  1019
                       (%(xa::'a::type) y::'b::type. x (xb xa y)))))))"
skalberg@14516
  1020
  by (import pair LET2_RAND)
skalberg@14516
  1021
obua@17644
  1022
lemma LET2_RATOR: "(All::('a1::type * 'a2::type => bool) => bool)
obua@17644
  1023
 (%x::'a1::type * 'a2::type.
obua@17644
  1024
     (All::(('a1::type => 'a2::type => 'b::type => 'c::type) => bool)
obua@17644
  1025
           => bool)
obua@17644
  1026
      (%xa::'a1::type => 'a2::type => 'b::type => 'c::type.
obua@17644
  1027
          (All::('b::type => bool) => bool)
obua@17644
  1028
           (%xb::'b::type.
obua@17644
  1029
               (op =::'c::type => 'c::type => bool)
obua@17644
  1030
                ((Let::'a1::type * 'a2::type
obua@17644
  1031
                       => ('a1::type * 'a2::type => 'b::type => 'c::type)
obua@17644
  1032
                          => 'b::type => 'c::type)
obua@17644
  1033
                  x ((split::('a1::type
obua@17644
  1034
                              => 'a2::type => 'b::type => 'c::type)
obua@17644
  1035
                             => 'a1::type * 'a2::type
obua@17644
  1036
                                => 'b::type => 'c::type)
obua@17644
  1037
                      xa)
skalberg@15647
  1038
                  xb)
obua@17644
  1039
                ((Let::'a1::type * 'a2::type
obua@17644
  1040
                       => ('a1::type * 'a2::type => 'c::type) => 'c::type)
obua@17644
  1041
                  x ((split::('a1::type => 'a2::type => 'c::type)
obua@17644
  1042
                             => 'a1::type * 'a2::type => 'c::type)
obua@17644
  1043
                      (%(x::'a1::type) y::'a2::type. xa x y xb))))))"
skalberg@14516
  1044
  by (import pair LET2_RATOR)
skalberg@14516
  1045
obua@17644
  1046
lemma pair_case_cong: "ALL (x::'a::type * 'b::type) (xa::'a::type * 'b::type)
obua@17644
  1047
   xb::'a::type => 'b::type => 'c::type.
obua@17644
  1048
   x = xa &
obua@17644
  1049
   (ALL (x::'a::type) y::'b::type.
obua@17644
  1050
       xa = (x, y) -->
obua@17644
  1051
       xb x y = (f'::'a::type => 'b::type => 'c::type) x y) -->
skalberg@14516
  1052
   split xb x = split f' xa"
skalberg@14516
  1053
  by (import pair pair_case_cong)
skalberg@14516
  1054
skalberg@14516
  1055
constdefs
obua@17652
  1056
  LEX :: "('a => 'a => bool) => ('b => 'b => bool) => 'a * 'b => 'a * 'b => bool" 
obua@17644
  1057
  "LEX ==
obua@17644
  1058
%(R1::'a::type => 'a::type => bool) (R2::'b::type => 'b::type => bool)
obua@17644
  1059
   (s::'a::type, t::'b::type) (u::'a::type, v::'b::type).
obua@17644
  1060
   R1 s u | s = u & R2 t v"
obua@17644
  1061
obua@17644
  1062
lemma LEX_DEF: "ALL (R1::'a::type => 'a::type => bool) R2::'b::type => 'b::type => bool.
obua@17644
  1063
   LEX R1 R2 =
obua@17644
  1064
   (%(s::'a::type, t::'b::type) (u::'a::type, v::'b::type).
obua@17644
  1065
       R1 s u | s = u & R2 t v)"
skalberg@14516
  1066
  by (import pair LEX_DEF)
skalberg@14516
  1067
obua@17644
  1068
lemma WF_LEX: "ALL (x::'a::type => 'a::type => bool) xa::'b::type => 'b::type => bool.
obua@17644
  1069
   WF x & WF xa --> WF (LEX x xa)"
skalberg@14516
  1070
  by (import pair WF_LEX)
skalberg@14516
  1071
skalberg@14516
  1072
constdefs
obua@17652
  1073
  RPROD :: "('a => 'a => bool) => ('b => 'b => bool) => 'a * 'b => 'a * 'b => bool" 
obua@17644
  1074
  "RPROD ==
obua@17644
  1075
%(R1::'a::type => 'a::type => bool) (R2::'b::type => 'b::type => bool)
obua@17644
  1076
   (s::'a::type, t::'b::type) (u::'a::type, v::'b::type). R1 s u & R2 t v"
obua@17644
  1077
obua@17644
  1078
lemma RPROD_DEF: "ALL (R1::'a::type => 'a::type => bool) R2::'b::type => 'b::type => bool.
obua@17644
  1079
   RPROD R1 R2 =
obua@17644
  1080
   (%(s::'a::type, t::'b::type) (u::'a::type, v::'b::type). R1 s u & R2 t v)"
skalberg@14516
  1081
  by (import pair RPROD_DEF)
skalberg@14516
  1082
obua@17644
  1083
lemma WF_RPROD: "ALL (R::'a::type => 'a::type => bool) Q::'b::type => 'b::type => bool.
obua@17644
  1084
   WF R & WF Q --> WF (RPROD R Q)"
skalberg@14516
  1085
  by (import pair WF_RPROD)
skalberg@14516
  1086
skalberg@14516
  1087
;end_setup
skalberg@14516
  1088
skalberg@14516
  1089
;setup_theory num
skalberg@14516
  1090
skalberg@14516
  1091
;end_setup
skalberg@14516
  1092
skalberg@14516
  1093
;setup_theory prim_rec
skalberg@14516
  1094
obua@17652
  1095
lemma LESS_0_0: "0 < Suc 0"
skalberg@14516
  1096
  by (import prim_rec LESS_0_0)
skalberg@14516
  1097
obua@17644
  1098
lemma LESS_LEMMA1: "ALL (x::nat) xa::nat. x < Suc xa --> x = xa | x < xa"
skalberg@14516
  1099
  by (import prim_rec LESS_LEMMA1)
skalberg@14516
  1100
obua@17644
  1101
lemma LESS_LEMMA2: "ALL (m::nat) n::nat. m = n | m < n --> m < Suc n"
skalberg@14516
  1102
  by (import prim_rec LESS_LEMMA2)
skalberg@14516
  1103
obua@17644
  1104
lemma LESS_THM: "ALL (m::nat) n::nat. (m < Suc n) = (m = n | m < n)"
skalberg@14516
  1105
  by (import prim_rec LESS_THM)
skalberg@14516
  1106
obua@17644
  1107
lemma LESS_SUC_IMP: "ALL (x::nat) xa::nat. x < Suc xa --> x ~= xa --> x < xa"
skalberg@14516
  1108
  by (import prim_rec LESS_SUC_IMP)
skalberg@14516
  1109
obua@17644
  1110
lemma EQ_LESS: "ALL n::nat. Suc (m::nat) = n --> m < n"
skalberg@14516
  1111
  by (import prim_rec EQ_LESS)
skalberg@14516
  1112
skalberg@14516
  1113
lemma NOT_LESS_EQ: "ALL (m::nat) n::nat. m = n --> ~ m < n"
skalberg@14516
  1114
  by (import prim_rec NOT_LESS_EQ)
skalberg@14516
  1115
skalberg@14516
  1116
constdefs
obua@17652
  1117
  SIMP_REC_REL :: "(nat => 'a) => 'a => ('a => 'a) => nat => bool" 
obua@17644
  1118
  "(op ==::((nat => 'a::type)
obua@17644
  1119
         => 'a::type => ('a::type => 'a::type) => nat => bool)
obua@17644
  1120
        => ((nat => 'a::type)
obua@17644
  1121
            => 'a::type => ('a::type => 'a::type) => nat => bool)
obua@17644
  1122
           => prop)
obua@17644
  1123
 (SIMP_REC_REL::(nat => 'a::type)
obua@17644
  1124
                => 'a::type => ('a::type => 'a::type) => nat => bool)
obua@17644
  1125
 (%(fun::nat => 'a::type) (x::'a::type) (f::'a::type => 'a::type) n::nat.
wenzelm@14847
  1126
     (op &::bool => bool => bool)
obua@17644
  1127
      ((op =::'a::type => 'a::type => bool) (fun (0::nat)) x)
wenzelm@14847
  1128
      ((All::(nat => bool) => bool)
wenzelm@14847
  1129
        (%m::nat.
wenzelm@14847
  1130
            (op -->::bool => bool => bool) ((op <::nat => nat => bool) m n)
obua@17644
  1131
             ((op =::'a::type => 'a::type => bool)
obua@17644
  1132
               (fun ((Suc::nat => nat) m)) (f (fun m))))))"
obua@17644
  1133
obua@17644
  1134
lemma SIMP_REC_REL: "(All::((nat => 'a::type) => bool) => bool)
obua@17644
  1135
 (%fun::nat => 'a::type.
obua@17644
  1136
     (All::('a::type => bool) => bool)
obua@17644
  1137
      (%x::'a::type.
obua@17644
  1138
          (All::(('a::type => 'a::type) => bool) => bool)
obua@17644
  1139
           (%f::'a::type => 'a::type.
wenzelm@14847
  1140
               (All::(nat => bool) => bool)
wenzelm@14847
  1141
                (%n::nat.
wenzelm@14847
  1142
                    (op =::bool => bool => bool)
obua@17644
  1143
                     ((SIMP_REC_REL::(nat => 'a::type)
obua@17644
  1144
                                     => 'a::type
obua@17644
  1145
  => ('a::type => 'a::type) => nat => bool)
wenzelm@14847
  1146
                       fun x f n)
wenzelm@14847
  1147
                     ((op &::bool => bool => bool)
obua@17644
  1148
                       ((op =::'a::type => 'a::type => bool) (fun (0::nat))
obua@17644
  1149
                         x)
wenzelm@14847
  1150
                       ((All::(nat => bool) => bool)
wenzelm@14847
  1151
                         (%m::nat.
wenzelm@14847
  1152
                             (op -->::bool => bool => bool)
wenzelm@14847
  1153
                              ((op <::nat => nat => bool) m n)
obua@17644
  1154
                              ((op =::'a::type => 'a::type => bool)
wenzelm@14847
  1155
                                (fun ((Suc::nat => nat) m))
wenzelm@14847
  1156
                                (f (fun m))))))))))"
skalberg@14516
  1157
  by (import prim_rec SIMP_REC_REL)
skalberg@14516
  1158
obua@17644
  1159
lemma SIMP_REC_EXISTS: "ALL (x::'a::type) (f::'a::type => 'a::type) n::nat.
obua@17644
  1160
   EX fun::nat => 'a::type. SIMP_REC_REL fun x f n"
skalberg@14516
  1161
  by (import prim_rec SIMP_REC_EXISTS)
skalberg@14516
  1162
obua@17644
  1163
lemma SIMP_REC_REL_UNIQUE: "ALL (x::'a::type) (xa::'a::type => 'a::type) (xb::nat => 'a::type)
obua@17644
  1164
   (xc::nat => 'a::type) (xd::nat) xe::nat.
skalberg@14516
  1165
   SIMP_REC_REL xb x xa xd & SIMP_REC_REL xc x xa xe -->
obua@17644
  1166
   (ALL n::nat. n < xd & n < xe --> xb n = xc n)"
skalberg@14516
  1167
  by (import prim_rec SIMP_REC_REL_UNIQUE)
skalberg@14516
  1168
obua@17644
  1169
lemma SIMP_REC_REL_UNIQUE_RESULT: "ALL (x::'a::type) (f::'a::type => 'a::type) n::nat.
obua@17644
  1170
   EX! y::'a::type.
obua@17644
  1171
      EX g::nat => 'a::type. SIMP_REC_REL g x f (Suc n) & y = g n"
skalberg@14516
  1172
  by (import prim_rec SIMP_REC_REL_UNIQUE_RESULT)
skalberg@14516
  1173
skalberg@14516
  1174
consts
obua@17652
  1175
  SIMP_REC :: "'a => ('a => 'a) => nat => 'a" 
obua@17644
  1176
obua@17644
  1177
specification (SIMP_REC) SIMP_REC: "ALL (x::'a::type) (f'::'a::type => 'a::type) n::nat.
obua@17644
  1178
   EX g::nat => 'a::type.
obua@17644
  1179
      SIMP_REC_REL g x f' (Suc n) & SIMP_REC x f' n = g n"
skalberg@14516
  1180
  by (import prim_rec SIMP_REC)
skalberg@14516
  1181
obua@17644
  1182
lemma LESS_SUC_SUC: "ALL m::nat. m < Suc m & m < Suc (Suc m)"
skalberg@14516
  1183
  by (import prim_rec LESS_SUC_SUC)
skalberg@14516
  1184
obua@17644
  1185
lemma SIMP_REC_THM: "ALL (x::'a::type) f::'a::type => 'a::type.
obua@17652
  1186
   SIMP_REC x f 0 = x &
obua@17644
  1187
   (ALL m::nat. SIMP_REC x f (Suc m) = f (SIMP_REC x f m))"
skalberg@14516
  1188
  by (import prim_rec SIMP_REC_THM)
skalberg@14516
  1189
skalberg@14516
  1190
constdefs
skalberg@14516
  1191
  PRE :: "nat => nat" 
obua@17652
  1192
  "PRE == %m::nat. if m = 0 then 0 else SOME n::nat. m = Suc n"
obua@17652
  1193
obua@17652
  1194
lemma PRE_DEF: "ALL m::nat. PRE m = (if m = 0 then 0 else SOME n::nat. m = Suc n)"
skalberg@14516
  1195
  by (import prim_rec PRE_DEF)
skalberg@14516
  1196
obua@17652
  1197
lemma PRE: "PRE 0 = 0 & (ALL m::nat. PRE (Suc m) = m)"
skalberg@14516
  1198
  by (import prim_rec PRE)
skalberg@14516
  1199
skalberg@14516
  1200
constdefs
obua@17652
  1201
  PRIM_REC_FUN :: "'a => ('a => nat => 'a) => nat => nat => 'a" 
obua@17644
  1202
  "PRIM_REC_FUN ==
obua@17644
  1203
%(x::'a::type) f::'a::type => nat => 'a::type.
obua@17644
  1204
   SIMP_REC (%n::nat. x) (%(fun::nat => 'a::type) n::nat. f (fun (PRE n)) n)"
obua@17644
  1205
obua@17644
  1206
lemma PRIM_REC_FUN: "ALL (x::'a::type) f::'a::type => nat => 'a::type.
obua@17644
  1207
   PRIM_REC_FUN x f =
obua@17644
  1208
   SIMP_REC (%n::nat. x) (%(fun::nat => 'a::type) n::nat. f (fun (PRE n)) n)"
skalberg@14516
  1209
  by (import prim_rec PRIM_REC_FUN)
skalberg@14516
  1210
obua@17644
  1211
lemma PRIM_REC_EQN: "ALL (x::'a::type) f::'a::type => nat => 'a::type.
obua@17652
  1212
   (ALL n::nat. PRIM_REC_FUN x f 0 n = x) &
obua@17644
  1213
   (ALL (m::nat) n::nat.
obua@17644
  1214
       PRIM_REC_FUN x f (Suc m) n = f (PRIM_REC_FUN x f m (PRE n)) n)"
skalberg@14516
  1215
  by (import prim_rec PRIM_REC_EQN)
skalberg@14516
  1216
skalberg@14516
  1217
constdefs
obua@17652
  1218
  PRIM_REC :: "'a => ('a => nat => 'a) => nat => 'a" 
obua@17644
  1219
  "PRIM_REC ==
obua@17644
  1220
%(x::'a::type) (f::'a::type => nat => 'a::type) m::nat.
obua@17644
  1221
   PRIM_REC_FUN x f m (PRE m)"
obua@17644
  1222
obua@17644
  1223
lemma PRIM_REC: "ALL (x::'a::type) (f::'a::type => nat => 'a::type) m::nat.
obua@17644
  1224
   PRIM_REC x f m = PRIM_REC_FUN x f m (PRE m)"
skalberg@14516
  1225
  by (import prim_rec PRIM_REC)
skalberg@14516
  1226
obua@17644
  1227
lemma PRIM_REC_THM: "ALL (x::'a::type) f::'a::type => nat => 'a::type.
obua@17652
  1228
   PRIM_REC x f 0 = x &
obua@17644
  1229
   (ALL m::nat. PRIM_REC x f (Suc m) = f (PRIM_REC x f m) m)"
skalberg@14516
  1230
  by (import prim_rec PRIM_REC_THM)
skalberg@14516
  1231
obua@17644
  1232
lemma DC: "ALL (P::'a::type => bool) (R::'a::type => 'a::type => bool) a::'a::type.
obua@17644
  1233
   P a & (ALL x::'a::type. P x --> (EX y::'a::type. P y & R x y)) -->
obua@17644
  1234
   (EX x::nat => 'a::type.
obua@17652
  1235
       x 0 = a & (ALL n::nat. P (x n) & R (x n) (x (Suc n))))"
skalberg@14516
  1236
  by (import prim_rec DC)
skalberg@14516
  1237
obua@17644
  1238
lemma num_Axiom_old: "ALL (e::'a::type) f::'a::type => nat => 'a::type.
obua@17644
  1239
   EX! fn1::nat => 'a::type.
obua@17652
  1240
      fn1 0 = e & (ALL n::nat. fn1 (Suc n) = f (fn1 n) n)"
skalberg@14516
  1241
  by (import prim_rec num_Axiom_old)
skalberg@14516
  1242
obua@17644
  1243
lemma num_Axiom: "ALL (e::'a::type) f::nat => 'a::type => 'a::type.
obua@17652
  1244
   EX x::nat => 'a::type. x 0 = e & (ALL n::nat. x (Suc n) = f n (x n))"
skalberg@14516
  1245
  by (import prim_rec num_Axiom)
skalberg@14516
  1246
skalberg@14516
  1247
consts
obua@17652
  1248
  wellfounded :: "('a => 'a => bool) => bool" 
skalberg@14516
  1249
skalberg@14516
  1250
defs
obua@17644
  1251
  wellfounded_primdef: "wellfounded ==
obua@17644
  1252
%R::'a::type => 'a::type => bool.
obua@17644
  1253
   ~ (EX f::nat => 'a::type. ALL n::nat. R (f (Suc n)) (f n))"
obua@17644
  1254
obua@17644
  1255
lemma wellfounded_def: "ALL R::'a::type => 'a::type => bool.
obua@17644
  1256
   wellfounded R =
obua@17644
  1257
   (~ (EX f::nat => 'a::type. ALL n::nat. R (f (Suc n)) (f n)))"
skalberg@14516
  1258
  by (import prim_rec wellfounded_def)
skalberg@14516
  1259
obua@17644
  1260
lemma WF_IFF_WELLFOUNDED: "ALL R::'a::type => 'a::type => bool. WF R = wellfounded R"
skalberg@14516
  1261
  by (import prim_rec WF_IFF_WELLFOUNDED)
skalberg@14516
  1262
obua@17644
  1263
lemma WF_PRED: "WF (%(x::nat) y::nat. y = Suc x)"
skalberg@14516
  1264
  by (import prim_rec WF_PRED)
skalberg@14516
  1265
skalberg@14516
  1266
lemma WF_LESS: "(WF::(nat => nat => bool) => bool) (op <::nat => nat => bool)"
skalberg@14516
  1267
  by (import prim_rec WF_LESS)
skalberg@14516
  1268
skalberg@14516
  1269
consts
obua@17652
  1270
  measure :: "('a => nat) => 'a => 'a => bool" 
skalberg@14516
  1271
skalberg@14516
  1272
defs
skalberg@14516
  1273
  measure_primdef: "prim_rec.measure == relation.inv_image op <"
skalberg@14516
  1274
skalberg@14516
  1275
lemma measure_def: "prim_rec.measure = relation.inv_image op <"
skalberg@14516
  1276
  by (import prim_rec measure_def)
skalberg@14516
  1277
obua@17644
  1278
lemma WF_measure: "ALL x::'a::type => nat. WF (prim_rec.measure x)"
skalberg@14516
  1279
  by (import prim_rec WF_measure)
skalberg@14516
  1280
obua@17644
  1281
lemma measure_thm: "ALL (x::'a::type => nat) (xa::'a::type) xb::'a::type.
obua@17644
  1282
   prim_rec.measure x xa xb = (x xa < x xb)"
skalberg@14516
  1283
  by (import prim_rec measure_thm)
skalberg@14516
  1284
skalberg@14516
  1285
;end_setup
skalberg@14516
  1286
skalberg@14516
  1287
;setup_theory arithmetic
skalberg@14516
  1288
skalberg@14516
  1289
constdefs
skalberg@14516
  1290
  nat_elim__magic :: "nat => nat" 
obua@17644
  1291
  "nat_elim__magic == %n::nat. n"
obua@17644
  1292
obua@17644
  1293
lemma nat_elim__magic: "ALL n::nat. nat_elim__magic n = n"
skalberg@14516
  1294
  by (import arithmetic nat_elim__magic)
skalberg@14516
  1295
skalberg@14516
  1296
consts
skalberg@14516
  1297
  EVEN :: "nat => bool" 
skalberg@14516
  1298
obua@17652
  1299
specification (EVEN) EVEN: "EVEN 0 = True & (ALL n::nat. EVEN (Suc n) = (~ EVEN n))"
skalberg@14516
  1300
  by (import arithmetic EVEN)
skalberg@14516
  1301
skalberg@14516
  1302
consts
skalberg@14516
  1303
  ODD :: "nat => bool" 
skalberg@14516
  1304
obua@17652
  1305
specification (ODD) ODD: "ODD 0 = False & (ALL n::nat. ODD (Suc n) = (~ ODD n))"
skalberg@14516
  1306
  by (import arithmetic ODD)
skalberg@14516
  1307
obua@17652
  1308
lemma TWO: "2 = Suc 1"
skalberg@14516
  1309
  by (import arithmetic TWO)
skalberg@14516
  1310
obua@17652
  1311
lemma NORM_0: "(op =::nat => nat => bool) (0::nat) (0::nat)"
skalberg@14516
  1312
  by (import arithmetic NORM_0)
skalberg@14516
  1313
obua@17644
  1314
lemma num_case_compute: "ALL n::nat.
obua@17644
  1315
   nat_case (f::'a::type) (g::nat => 'a::type) n =
obua@17652
  1316
   (if n = 0 then f else g (PRE n))"
skalberg@14516
  1317
  by (import arithmetic num_case_compute)
skalberg@14516
  1318
obua@17652
  1319
lemma ADD_CLAUSES: "0 + (m::nat) = m &
obua@17652
  1320
m + 0 = m & Suc m + (n::nat) = Suc (m + n) & m + Suc n = Suc (m + n)"
skalberg@14516
  1321
  by (import arithmetic ADD_CLAUSES)
skalberg@14516
  1322
skalberg@14516
  1323
lemma LESS_ADD: "ALL (m::nat) n::nat. n < m --> (EX p::nat. p + n = m)"
skalberg@14516
  1324
  by (import arithmetic LESS_ADD)
skalberg@14516
  1325
skalberg@14516
  1326
lemma LESS_ANTISYM: "ALL (m::nat) n::nat. ~ (m < n & n < m)"
skalberg@14516
  1327
  by (import arithmetic LESS_ANTISYM)
skalberg@14516
  1328
obua@17644
  1329
lemma LESS_LESS_SUC: "ALL (x::nat) xa::nat. ~ (x < xa & xa < Suc x)"
skalberg@14516
  1330
  by (import arithmetic LESS_LESS_SUC)
skalberg@14516
  1331
obua@17644
  1332
lemma FUN_EQ_LEMMA: "ALL (f::'a::type => bool) (x1::'a::type) x2::'a::type.
obua@17644
  1333
   f x1 & ~ f x2 --> x1 ~= x2"
skalberg@14516
  1334
  by (import arithmetic FUN_EQ_LEMMA)
skalberg@14516
  1335
obua@17644
  1336
lemma LESS_NOT_SUC: "ALL (m::nat) n::nat. m < n & n ~= Suc m --> Suc m < n"
skalberg@14516
  1337
  by (import arithmetic LESS_NOT_SUC)
skalberg@14516
  1338
obua@17652
  1339
lemma LESS_0_CASES: "ALL m::nat. 0 = m | 0 < m"
skalberg@14516
  1340
  by (import arithmetic LESS_0_CASES)
skalberg@14516
  1341
skalberg@14516
  1342
lemma LESS_CASES_IMP: "ALL (m::nat) n::nat. ~ m < n & m ~= n --> n < m"
skalberg@14516
  1343
  by (import arithmetic LESS_CASES_IMP)
skalberg@14516
  1344
skalberg@14516
  1345
lemma LESS_CASES: "ALL (m::nat) n::nat. m < n | n <= m"
skalberg@14516
  1346
  by (import arithmetic LESS_CASES)
skalberg@14516
  1347
obua@17644
  1348
lemma LESS_EQ_SUC_REFL: "ALL m::nat. m <= Suc m"
skalberg@14516
  1349
  by (import arithmetic LESS_EQ_SUC_REFL)
skalberg@14516
  1350
obua@17652
  1351
lemma LESS_ADD_NONZERO: "ALL (m::nat) n::nat. n ~= 0 --> m < m + n"
skalberg@14516
  1352
  by (import arithmetic LESS_ADD_NONZERO)
skalberg@14516
  1353
skalberg@14516
  1354
lemma LESS_EQ_ANTISYM: "ALL (x::nat) xa::nat. ~ (x < xa & xa <= x)"
skalberg@14516
  1355
  by (import arithmetic LESS_EQ_ANTISYM)
skalberg@14516
  1356
obua@17652
  1357
lemma SUB_0: "ALL m::nat. 0 - m = 0 & m - 0 = m"
skalberg@14516
  1358
  by (import arithmetic SUB_0)
skalberg@14516
  1359
obua@17652
  1360
lemma SUC_SUB1: "ALL m::nat. Suc m - 1 = m"
skalberg@14516
  1361
  by (import arithmetic SUC_SUB1)
skalberg@14516
  1362
obua@17652
  1363
lemma PRE_SUB1: "ALL m::nat. PRE m = m - 1"
skalberg@14516
  1364
  by (import arithmetic PRE_SUB1)
skalberg@14516
  1365
obua@17644
  1366
lemma MULT_CLAUSES: "ALL (x::nat) xa::nat.
obua@17652
  1367
   0 * x = 0 &
obua@17652
  1368
   x * 0 = 0 &
obua@17652
  1369
   1 * x = x &
obua@17652
  1370
   x * 1 = x & Suc x * xa = x * xa + xa & x * Suc xa = x + x * xa"
skalberg@14516
  1371
  by (import arithmetic MULT_CLAUSES)
skalberg@14516
  1372
obua@17644
  1373
lemma PRE_SUB: "ALL (m::nat) n::nat. PRE (m - n) = PRE m - n"
skalberg@14516
  1374
  by (import arithmetic PRE_SUB)
skalberg@14516
  1375
obua@17652
  1376
lemma ADD_EQ_1: "ALL (m::nat) n::nat. (m + n = 1) = (m = 1 & n = 0 | m = 0 & n = 1)"
skalberg@14516
  1377
  by (import arithmetic ADD_EQ_1)
skalberg@14516
  1378
obua@17652
  1379
lemma ADD_INV_0_EQ: "ALL (m::nat) n::nat. (m + n = m) = (n = 0)"
skalberg@14516
  1380
  by (import arithmetic ADD_INV_0_EQ)
skalberg@14516
  1381
obua@17652
  1382
lemma PRE_SUC_EQ: "ALL (m::nat) n::nat. 0 < n --> (m = PRE n) = (Suc m = n)"
skalberg@14516
  1383
  by (import arithmetic PRE_SUC_EQ)
skalberg@14516
  1384
obua@17652
  1385
lemma INV_PRE_EQ: "ALL (m::nat) n::nat. 0 < m & 0 < n --> (PRE m = PRE n) = (m = n)"
skalberg@14516
  1386
  by (import arithmetic INV_PRE_EQ)
skalberg@14516
  1387
obua@17644
  1388
lemma LESS_SUC_NOT: "ALL (m::nat) n::nat. m < n --> ~ n < Suc m"
skalberg@14516
  1389
  by (import arithmetic LESS_SUC_NOT)
skalberg@14516
  1390
skalberg@14516
  1391
lemma ADD_EQ_SUB: "ALL (m::nat) (n::nat) p::nat. n <= p --> (m + n = p) = (m = p - n)"
skalberg@14516
  1392
  by (import arithmetic ADD_EQ_SUB)
skalberg@14516
  1393
obua@17652
  1394
lemma LESS_ADD_1: "ALL (x::nat) xa::nat. xa < x --> (EX xb::nat. x = xa + (xb + 1))"
skalberg@14516
  1395
  by (import arithmetic LESS_ADD_1)
skalberg@14516
  1396
obua@17644
  1397
lemma NOT_ODD_EQ_EVEN: "ALL (n::nat) m::nat. Suc (n + n) ~= m + m"
skalberg@14516
  1398
  by (import arithmetic NOT_ODD_EQ_EVEN)
skalberg@14516
  1399
obua@17644
  1400
lemma MULT_SUC_EQ: "ALL (p::nat) (m::nat) n::nat. (n * Suc p = m * Suc p) = (n = m)"
skalberg@14516
  1401
  by (import arithmetic MULT_SUC_EQ)
skalberg@14516
  1402
obua@17644
  1403
lemma MULT_EXP_MONO: "ALL (p::nat) (q::nat) (n::nat) m::nat.
obua@17644
  1404
   (n * Suc q ^ p = m * Suc q ^ p) = (n = m)"
skalberg@14516
  1405
  by (import arithmetic MULT_EXP_MONO)
skalberg@14516
  1406
obua@17644
  1407
lemma LESS_ADD_SUC: "ALL (m::nat) n::nat. m < m + Suc n"
skalberg@14516
  1408
  by (import arithmetic LESS_ADD_SUC)
skalberg@14516
  1409
skalberg@14516
  1410
lemma LESS_OR_EQ_ADD: "ALL (n::nat) m::nat. n < m | (EX p::nat. n = p + m)"
skalberg@14516
  1411
  by (import arithmetic LESS_OR_EQ_ADD)
skalberg@14516
  1412
wenzelm@14847
  1413
lemma WOP: "(All::((nat => bool) => bool) => bool)
wenzelm@14847
  1414
 (%P::nat => bool.
wenzelm@14847
  1415
     (op -->::bool => bool => bool) ((Ex::(nat => bool) => bool) P)
wenzelm@14847
  1416
      ((Ex::(nat => bool) => bool)
wenzelm@14847
  1417
        (%n::nat.
wenzelm@14847
  1418
            (op &::bool => bool => bool) (P n)
wenzelm@14847
  1419
             ((All::(nat => bool) => bool)
wenzelm@14847
  1420
               (%m::nat.
wenzelm@14847
  1421
                   (op -->::bool => bool => bool)
wenzelm@14847
  1422
                    ((op <::nat => nat => bool) m n)
wenzelm@14847
  1423
                    ((Not::bool => bool) (P m)))))))"
skalberg@14516
  1424
  by (import arithmetic WOP)
skalberg@14516
  1425
obua@17652
  1426
lemma INV_PRE_LESS: "ALL m>0. ALL n::nat. (PRE m < PRE n) = (m < n)"
skalberg@14516
  1427
  by (import arithmetic INV_PRE_LESS)
skalberg@14516
  1428
obua@17652
  1429
lemma INV_PRE_LESS_EQ: "ALL n>0. ALL m::nat. (PRE m <= PRE n) = (m <= n)"
skalberg@14516
  1430
  by (import arithmetic INV_PRE_LESS_EQ)
skalberg@14516
  1431
obua@17652
  1432
lemma SUB_EQ_EQ_0: "ALL (m::nat) n::nat. (m - n = m) = (m = 0 | n = 0)"
skalberg@14516
  1433
  by (import arithmetic SUB_EQ_EQ_0)
skalberg@14516
  1434
obua@17652
  1435
lemma SUB_LESS_OR: "ALL (m::nat) n::nat. n < m --> n <= m - 1"
skalberg@14516
  1436
  by (import arithmetic SUB_LESS_OR)
skalberg@14516
  1437
skalberg@14516
  1438
lemma LESS_SUB_ADD_LESS: "ALL (n::nat) (m::nat) i::nat. i < n - m --> i + m < n"
skalberg@14516
  1439
  by (import arithmetic LESS_SUB_ADD_LESS)
skalberg@14516
  1440
skalberg@14516
  1441
lemma LESS_EQ_SUB_LESS: "ALL (x::nat) xa::nat. xa <= x --> (ALL c::nat. (x - xa < c) = (x < xa + c))"
skalberg@14516
  1442
  by (import arithmetic LESS_EQ_SUB_LESS)
skalberg@14516
  1443
obua@17644
  1444
lemma NOT_SUC_LESS_EQ: "ALL (x::nat) xa::nat. (~ Suc x <= xa) = (xa <= x)"
skalberg@14516
  1445
  by (import arithmetic NOT_SUC_LESS_EQ)
skalberg@14516
  1446
skalberg@14516
  1447
lemma SUB_LESS_EQ_ADD: "ALL (m::nat) p::nat. m <= p --> (ALL n::nat. (p - m <= n) = (p <= m + n))"
skalberg@14516
  1448
  by (import arithmetic SUB_LESS_EQ_ADD)
skalberg@14516
  1449
skalberg@14516
  1450
lemma SUB_CANCEL: "ALL (x::nat) (xa::nat) xb::nat.
skalberg@14516
  1451
   xa <= x & xb <= x --> (x - xa = x - xb) = (xa = xb)"
skalberg@14516
  1452
  by (import arithmetic SUB_CANCEL)
skalberg@14516
  1453
obua@17652
  1454
lemma NOT_EXP_0: "ALL (m::nat) n::nat. Suc n ^ m ~= 0"
skalberg@14516
  1455
  by (import arithmetic NOT_EXP_0)
skalberg@14516
  1456
obua@17652
  1457
lemma ZERO_LESS_EXP: "ALL (m::nat) n::nat. 0 < Suc n ^ m"
skalberg@14516
  1458
  by (import arithmetic ZERO_LESS_EXP)
skalberg@14516
  1459
obua@17652
  1460
lemma ODD_OR_EVEN: "ALL x::nat. EX xa::nat. x = Suc (Suc 0) * xa | x = Suc (Suc 0) * xa + 1"
skalberg@14516
  1461
  by (import arithmetic ODD_OR_EVEN)
skalberg@14516
  1462
obua@17644
  1463
lemma LESS_EXP_SUC_MONO: "ALL (n::nat) m::nat. Suc (Suc m) ^ n < Suc (Suc m) ^ Suc n"
skalberg@14516
  1464
  by (import arithmetic LESS_EXP_SUC_MONO)
skalberg@14516
  1465
skalberg@14516
  1466
lemma LESS_LESS_CASES: "ALL (m::nat) n::nat. m = n | m < n | n < m"
skalberg@14516
  1467
  by (import arithmetic LESS_LESS_CASES)
skalberg@14516
  1468
skalberg@14516
  1469
lemma LESS_EQUAL_ADD: "ALL (m::nat) n::nat. m <= n --> (EX p::nat. n = m + p)"
skalberg@14516
  1470
  by (import arithmetic LESS_EQUAL_ADD)
skalberg@14516
  1471
obua@17652
  1472
lemma MULT_EQ_1: "ALL (x::nat) y::nat. (x * y = 1) = (x = 1 & y = 1)"
skalberg@14516
  1473
  by (import arithmetic MULT_EQ_1)
skalberg@14516
  1474
skalberg@14516
  1475
consts
skalberg@14516
  1476
  FACT :: "nat => nat" 
skalberg@14516
  1477
obua@17652
  1478
specification (FACT) FACT: "FACT 0 = 1 & (ALL n::nat. FACT (Suc n) = Suc n * FACT n)"
skalberg@14516
  1479
  by (import arithmetic FACT)
skalberg@14516
  1480
obua@17652
  1481
lemma FACT_LESS: "ALL n::nat. 0 < FACT n"
skalberg@14516
  1482
  by (import arithmetic FACT_LESS)
skalberg@14516
  1483
obua@17644
  1484
lemma EVEN_ODD: "ALL n::nat. EVEN n = (~ ODD n)"
skalberg@14516
  1485
  by (import arithmetic EVEN_ODD)
skalberg@14516
  1486
obua@17644
  1487
lemma ODD_EVEN: "ALL x::nat. ODD x = (~ EVEN x)"
skalberg@14516
  1488
  by (import arithmetic ODD_EVEN)
skalberg@14516
  1489
obua@17644
  1490
lemma EVEN_OR_ODD: "ALL x::nat. EVEN x | ODD x"
skalberg@14516
  1491
  by (import arithmetic EVEN_OR_ODD)
skalberg@14516
  1492
obua@17644
  1493
lemma EVEN_AND_ODD: "ALL x::nat. ~ (EVEN x & ODD x)"
skalberg@14516
  1494
  by (import arithmetic EVEN_AND_ODD)
skalberg@14516
  1495
obua@17644
  1496
lemma EVEN_ADD: "ALL (m::nat) n::nat. EVEN (m + n) = (EVEN m = EVEN n)"
skalberg@14516
  1497
  by (import arithmetic EVEN_ADD)
skalberg@14516
  1498
obua@17644
  1499
lemma EVEN_MULT: "ALL (m::nat) n::nat. EVEN (m * n) = (EVEN m | EVEN n)"
skalberg@14516
  1500
  by (import arithmetic EVEN_MULT)
skalberg@14516
  1501
obua@17644
  1502
lemma ODD_ADD: "ALL (m::nat) n::nat. ODD (m + n) = (ODD m ~= ODD n)"
skalberg@14516
  1503
  by (import arithmetic ODD_ADD)
skalberg@14516
  1504
obua@17644
  1505
lemma ODD_MULT: "ALL (m::nat) n::nat. ODD (m * n) = (ODD m & ODD n)"
skalberg@14516
  1506
  by (import arithmetic ODD_MULT)
skalberg@14516
  1507
obua@17652
  1508
lemma EVEN_DOUBLE: "ALL n::nat. EVEN (2 * n)"
skalberg@14516
  1509
  by (import arithmetic EVEN_DOUBLE)
skalberg@14516
  1510
obua@17652
  1511
lemma ODD_DOUBLE: "ALL x::nat. ODD (Suc (2 * x))"
skalberg@14516
  1512
  by (import arithmetic ODD_DOUBLE)
skalberg@14516
  1513
obua@17644
  1514
lemma EVEN_ODD_EXISTS: "ALL x::nat.
obua@17652
  1515
   (EVEN x --> (EX m::nat. x = 2 * m)) &
obua@17652
  1516
   (ODD x --> (EX m::nat. x = Suc (2 * m)))"
skalberg@14516
  1517
  by (import arithmetic EVEN_ODD_EXISTS)
skalberg@14516
  1518
obua@17652
  1519
lemma EVEN_EXISTS: "ALL n::nat. EVEN n = (EX m::nat. n = 2 * m)"
skalberg@14516
  1520
  by (import arithmetic EVEN_EXISTS)
skalberg@14516
  1521
obua@17652
  1522
lemma ODD_EXISTS: "ALL n::nat. ODD n = (EX m::nat. n = Suc (2 * m))"
skalberg@14516
  1523
  by (import arithmetic ODD_EXISTS)
skalberg@14516
  1524
obua@17652
  1525
lemma NOT_SUC_LESS_EQ_0: "ALL x::nat. ~ Suc x <= 0"
skalberg@14516
  1526
  by (import arithmetic NOT_SUC_LESS_EQ_0)
skalberg@14516
  1527
obua@17644
  1528
lemma NOT_LEQ: "ALL (x::nat) xa::nat. (~ x <= xa) = (Suc xa <= x)"
skalberg@14516
  1529
  by (import arithmetic NOT_LEQ)
skalberg@14516
  1530
obua@17644
  1531
lemma NOT_NUM_EQ: "ALL (x::nat) xa::nat. (x ~= xa) = (Suc x <= xa | Suc xa <= x)"
skalberg@14516
  1532
  by (import arithmetic NOT_NUM_EQ)
skalberg@14516
  1533
obua@17644
  1534
lemma NOT_GREATER_EQ: "ALL (x::nat) xa::nat. (~ xa <= x) = (Suc x <= xa)"
skalberg@14516
  1535
  by (import arithmetic NOT_GREATER_EQ)
skalberg@14516
  1536
obua@17644
  1537
lemma SUC_ADD_SYM: "ALL (m::nat) n::nat. Suc (m + n) = Suc n + m"
skalberg@14516
  1538
  by (import arithmetic SUC_ADD_SYM)
skalberg@14516
  1539
obua@17644
  1540
lemma NOT_SUC_ADD_LESS_EQ: "ALL (m::nat) n::nat. ~ Suc (m + n) <= m"
skalberg@14516
  1541
  by (import arithmetic NOT_SUC_ADD_LESS_EQ)
skalberg@14516
  1542
skalberg@14516
  1543
lemma SUB_LEFT_ADD: "ALL (m::nat) (n::nat) p::nat.
skalberg@14516
  1544
   m + (n - p) = (if n <= p then m else m + n - p)"
skalberg@14516
  1545
  by (import arithmetic SUB_LEFT_ADD)
skalberg@14516
  1546
skalberg@14516
  1547
lemma SUB_RIGHT_ADD: "ALL (m::nat) (n::nat) p::nat. m - n + p = (if m <= n then p else m + p - n)"
skalberg@14516
  1548
  by (import arithmetic SUB_RIGHT_ADD)
skalberg@14516
  1549
skalberg@14516
  1550
lemma SUB_LEFT_SUB: "ALL (m::nat) (n::nat) p::nat.
skalberg@14516
  1551
   m - (n - p) = (if n <= p then m else m + p - n)"
skalberg@14516
  1552
  by (import arithmetic SUB_LEFT_SUB)
skalberg@14516
  1553
obua@17652
  1554
lemma SUB_LEFT_SUC: "ALL (m::nat) n::nat. Suc (m - n) = (if m <= n then Suc 0 else Suc m - n)"
skalberg@14516
  1555
  by (import arithmetic SUB_LEFT_SUC)
skalberg@14516
  1556
obua@17652
  1557
lemma SUB_LEFT_LESS_EQ: "ALL (m::nat) (n::nat) p::nat. (m <= n - p) = (m + p <= n | m <= 0)"
skalberg@14516
  1558
  by (import arithmetic SUB_LEFT_LESS_EQ)
skalberg@14516
  1559
skalberg@14516
  1560
lemma SUB_RIGHT_LESS_EQ: "ALL (m::nat) (n::nat) p::nat. (m - n <= p) = (m <= n + p)"
skalberg@14516
  1561
  by (import arithmetic SUB_RIGHT_LESS_EQ)
skalberg@14516
  1562
obua@17652
  1563
lemma SUB_RIGHT_LESS: "ALL (m::nat) (n::nat) p::nat. (m - n < p) = (m < n + p & 0 < p)"
skalberg@14516
  1564
  by (import arithmetic SUB_RIGHT_LESS)
skalberg@14516
  1565
obua@17652
  1566
lemma SUB_RIGHT_GREATER_EQ: "ALL (m::nat) (n::nat) p::nat. (p <= m - n) = (n + p <= m | p <= 0)"
skalberg@14516
  1567
  by (import arithmetic SUB_RIGHT_GREATER_EQ)
skalberg@14516
  1568
obua@17652
  1569
lemma SUB_LEFT_GREATER: "ALL (m::nat) (n::nat) p::nat. (n - p < m) = (n < m + p & 0 < m)"
skalberg@14516
  1570
  by (import arithmetic SUB_LEFT_GREATER)
skalberg@14516
  1571
skalberg@14516
  1572
lemma SUB_RIGHT_GREATER: "ALL (m::nat) (n::nat) p::nat. (p < m - n) = (n + p < m)"
skalberg@14516
  1573
  by (import arithmetic SUB_RIGHT_GREATER)
skalberg@14516
  1574
obua@17652
  1575
lemma SUB_LEFT_EQ: "ALL (m::nat) (n::nat) p::nat. (m = n - p) = (m + p = n | m <= 0 & n <= p)"
skalberg@14516
  1576
  by (import arithmetic SUB_LEFT_EQ)
skalberg@14516
  1577
obua@17652
  1578
lemma SUB_RIGHT_EQ: "ALL (m::nat) (n::nat) p::nat. (m - n = p) = (m = n + p | m <= n & p <= 0)"
skalberg@14516
  1579
  by (import arithmetic SUB_RIGHT_EQ)
skalberg@14516
  1580
obua@17652
  1581
lemma LE: "(ALL n::nat. (n <= 0) = (n = 0)) &
skalberg@14516
  1582
(ALL (m::nat) n::nat. (m <= Suc n) = (m = Suc n | m <= n))"
skalberg@14516
  1583
  by (import arithmetic LE)
skalberg@14516
  1584
obua@17652
  1585
lemma DA: "ALL (k::nat) n::nat. 0 < n --> (EX (x::nat) q::nat. k = q * n + x & x < n)"
skalberg@14516
  1586
  by (import arithmetic DA)
skalberg@14516
  1587
obua@17652
  1588
lemma DIV_LESS_EQ: "ALL n>0. ALL k::nat. k div n <= k"
skalberg@14516
  1589
  by (import arithmetic DIV_LESS_EQ)
skalberg@14516
  1590
skalberg@14516
  1591
lemma DIV_UNIQUE: "ALL (n::nat) (k::nat) q::nat.
skalberg@14516
  1592
   (EX r::nat. k = q * n + r & r < n) --> k div n = q"
skalberg@14516
  1593
  by (import arithmetic DIV_UNIQUE)
skalberg@14516
  1594
skalberg@14516
  1595
lemma MOD_UNIQUE: "ALL (n::nat) (k::nat) r::nat.
skalberg@14516
  1596
   (EX q::nat. k = q * n + r & r < n) --> k mod n = r"
skalberg@14516
  1597
  by (import arithmetic MOD_UNIQUE)
skalberg@14516
  1598
skalberg@14516
  1599
lemma DIV_MULT: "ALL (n::nat) r::nat. r < n --> (ALL q::nat. (q * n + r) div n = q)"
skalberg@14516
  1600
  by (import arithmetic DIV_MULT)
skalberg@14516
  1601
obua@17652
  1602
lemma MOD_EQ_0: "ALL n>0. ALL k::nat. k * n mod n = 0"
skalberg@14516
  1603
  by (import arithmetic MOD_EQ_0)
skalberg@14516
  1604
obua@17652
  1605
lemma ZERO_MOD: "(All::(nat => bool) => bool)
obua@17652
  1606
 (%n::nat.
obua@17652
  1607
     (op -->::bool => bool => bool) ((op <::nat => nat => bool) (0::nat) n)
obua@17652
  1608
      ((op =::nat => nat => bool) ((op mod::nat => nat => nat) (0::nat) n)
obua@17652
  1609
        (0::nat)))"
skalberg@14516
  1610
  by (import arithmetic ZERO_MOD)
skalberg@14516
  1611
obua@17652
  1612
lemma ZERO_DIV: "(All::(nat => bool) => bool)
obua@17652
  1613
 (%n::nat.
obua@17652
  1614
     (op -->::bool => bool => bool) ((op <::nat => nat => bool) (0::nat) n)
obua@17652
  1615
      ((op =::nat => nat => bool) ((op div::nat => nat => nat) (0::nat) n)
obua@17652
  1616
        (0::nat)))"
skalberg@14516
  1617
  by (import arithmetic ZERO_DIV)
skalberg@14516
  1618
skalberg@14516
  1619
lemma MOD_MULT: "ALL (n::nat) r::nat. r < n --> (ALL q::nat. (q * n + r) mod n = r)"
skalberg@14516
  1620
  by (import arithmetic MOD_MULT)
skalberg@14516
  1621
obua@17652
  1622
lemma MOD_TIMES: "ALL n>0. ALL (q::nat) r::nat. (q * n + r) mod n = r mod n"
skalberg@14516
  1623
  by (import arithmetic MOD_TIMES)
skalberg@14516
  1624
obua@17652
  1625
lemma MOD_PLUS: "ALL n>0. ALL (j::nat) k::nat. (j mod n + k mod n) mod n = (j + k) mod n"
skalberg@14516
  1626
  by (import arithmetic MOD_PLUS)
skalberg@14516
  1627
obua@17652
  1628
lemma MOD_MOD: "ALL n>0. ALL k::nat. k mod n mod n = k mod n"
skalberg@14516
  1629
  by (import arithmetic MOD_MOD)
skalberg@14516
  1630
obua@17652
  1631
lemma ADD_DIV_ADD_DIV: "ALL x>0. ALL (xa::nat) r::nat. (xa * x + r) div x = xa + r div x"
skalberg@14516
  1632
  by (import arithmetic ADD_DIV_ADD_DIV)
skalberg@14516
  1633
skalberg@14516
  1634
lemma MOD_MULT_MOD: "ALL (m::nat) n::nat.
obua@17652
  1635
   0 < n & 0 < m --> (ALL x::nat. x mod (n * m) mod n = x mod n)"
skalberg@14516
  1636
  by (import arithmetic MOD_MULT_MOD)
skalberg@14516
  1637
obua@17652
  1638
lemma DIVMOD_ID: "(All::(nat => bool) => bool)
obua@17652
  1639
 (%n::nat.
obua@17652
  1640
     (op -->::bool => bool => bool) ((op <::nat => nat => bool) (0::nat) n)
obua@17652
  1641
      ((op &::bool => bool => bool)
obua@17652
  1642
        ((op =::nat => nat => bool) ((op div::nat => nat => nat) n n)
obua@17652
  1643
          (1::nat))
obua@17652
  1644
        ((op =::nat => nat => bool) ((op mod::nat => nat => nat) n n)
obua@17652
  1645
          (0::nat))))"
skalberg@14516
  1646
  by (import arithmetic DIVMOD_ID)
skalberg@14516
  1647
skalberg@14516
  1648
lemma DIV_DIV_DIV_MULT: "ALL (x::nat) xa::nat.
obua@17652
  1649
   0 < x & 0 < xa --> (ALL xb::nat. xb div x div xa = xb div (x * xa))"
skalberg@14516
  1650
  by (import arithmetic DIV_DIV_DIV_MULT)
skalberg@14516
  1651
skalberg@14516
  1652
lemma DIV_P: "ALL (P::nat => bool) (p::nat) q::nat.
obua@17652
  1653
   0 < q --> P (p div q) = (EX (k::nat) r::nat. p = k * q + r & r < q & P k)"
skalberg@14516
  1654
  by (import arithmetic DIV_P)
skalberg@14516
  1655
skalberg@14516
  1656
lemma MOD_P: "ALL (P::nat => bool) (p::nat) q::nat.
obua@17652
  1657
   0 < q --> P (p mod q) = (EX (k::nat) r::nat. p = k * q + r & r < q & P r)"
skalberg@14516
  1658
  by (import arithmetic MOD_P)
skalberg@14516
  1659
obua@17652
  1660
lemma MOD_TIMES2: "ALL n>0. ALL (j::nat) k::nat. j mod n * (k mod n) mod n = j * k mod n"
skalberg@14516
  1661
  by (import arithmetic MOD_TIMES2)
skalberg@14516
  1662
skalberg@14516
  1663
lemma MOD_COMMON_FACTOR: "ALL (n::nat) (p::nat) q::nat.
obua@17652
  1664
   0 < n & 0 < q --> n * (p mod q) = n * p mod (n * q)"
skalberg@14516
  1665
  by (import arithmetic MOD_COMMON_FACTOR)
skalberg@14516
  1666
obua@17644
  1667
lemma num_case_cong: "ALL (M::nat) (M'::nat) (b::'a::type) f::nat => 'a::type.
obua@17644
  1668
   M = M' &
obua@17652
  1669
   (M' = 0 --> b = (b'::'a::type)) &
obua@17644
  1670
   (ALL n::nat. M' = Suc n --> f n = (f'::nat => 'a::type) n) -->
skalberg@14516
  1671
   nat_case b f M = nat_case b' f' M'"
skalberg@14516
  1672
  by (import arithmetic num_case_cong)
skalberg@14516
  1673
obua@17644
  1674
lemma SUC_ELIM_THM: "ALL P::nat => nat => bool.
obua@17652
  1675
   (ALL n::nat. P (Suc n) n) = (ALL n>0. P n (n - 1))"
skalberg@14516
  1676
  by (import arithmetic SUC_ELIM_THM)
skalberg@14516
  1677
skalberg@14516
  1678
lemma SUB_ELIM_THM: "(P::nat => bool) ((a::nat) - (b::nat)) =
obua@17652
  1679
(ALL x::nat. (b = a + x --> P 0) & (a = b + x --> P x))"
skalberg@14516
  1680
  by (import arithmetic SUB_ELIM_THM)
skalberg@14516
  1681
obua@17644
  1682
lemma PRE_ELIM_THM: "(P::nat => bool) (PRE (n::nat)) =
obua@17652
  1683
(ALL m::nat. (n = 0 --> P 0) & (n = Suc m --> P m))"
skalberg@14516
  1684
  by (import arithmetic PRE_ELIM_THM)
skalberg@14516
  1685
obua@17652
  1686
lemma MULT_INCREASES: "ALL (m::nat) n::nat. 1 < m & 0 < n --> Suc n <= m * n"
skalberg@14516
  1687
  by (import arithmetic MULT_INCREASES)
skalberg@14516
  1688
obua@17652
  1689
lemma EXP_ALWAYS_BIG_ENOUGH: "ALL b>1. ALL n::nat. EX m::nat. n <= b ^ m"
skalberg@14516
  1690
  by (import arithmetic EXP_ALWAYS_BIG_ENOUGH)
skalberg@14516
  1691
obua@17652
  1692
lemma EXP_EQ_0: "ALL (n::nat) m::nat. (n ^ m = 0) = (n = 0 & 0 < m)"
skalberg@14516
  1693
  by (import arithmetic EXP_EQ_0)
skalberg@14516
  1694
obua@17652
  1695
lemma EXP_1: "(All::(nat => bool) => bool)
obua@17652
  1696
 (%x::nat.
obua@17652
  1697
     (op &::bool => bool => bool)
obua@17652
  1698
      ((op =::nat => nat => bool) ((op ^::nat => nat => nat) (1::nat) x)
obua@17652
  1699
        (1::nat))
obua@17652
  1700
      ((op =::nat => nat => bool) ((op ^::nat => nat => nat) x (1::nat)) x))"
skalberg@14516
  1701
  by (import arithmetic EXP_1)
skalberg@14516
  1702
obua@17652
  1703
lemma EXP_EQ_1: "ALL (n::nat) m::nat. (n ^ m = 1) = (n = 1 | m = 0)"
skalberg@14516
  1704
  by (import arithmetic EXP_EQ_1)
skalberg@14516
  1705
skalberg@14516
  1706
lemma MIN_MAX_EQ: "ALL (x::nat) xa::nat. (min x xa = max x xa) = (x = xa)"
skalberg@14516
  1707
  by (import arithmetic MIN_MAX_EQ)
skalberg@14516
  1708
skalberg@14516
  1709
lemma MIN_MAX_LT: "ALL (x::nat) xa::nat. (min x xa < max x xa) = (x ~= xa)"
skalberg@14516
  1710
  by (import arithmetic MIN_MAX_LT)
skalberg@14516
  1711
skalberg@14516
  1712
lemma MIN_MAX_PRED: "ALL (P::nat => bool) (m::nat) n::nat.
skalberg@14516
  1713
   P m & P n --> P (min m n) & P (max m n)"
skalberg@14516
  1714
  by (import arithmetic MIN_MAX_PRED)
skalberg@14516
  1715
skalberg@14516
  1716
lemma MIN_LT: "ALL (x::nat) xa::nat.
skalberg@14516
  1717
   (min xa x < xa) = (xa ~= x & min xa x = x) &
skalberg@14516
  1718
   (min xa x < x) = (xa ~= x & min xa x = xa) &
skalberg@14516
  1719
   (xa < min xa x) = False & (x < min xa x) = False"
skalberg@14516
  1720
  by (import arithmetic MIN_LT)
skalberg@14516
  1721
skalberg@14516
  1722
lemma MAX_LT: "ALL (x::nat) xa::nat.
skalberg@14516
  1723
   (xa < max xa x) = (xa ~= x & max xa x = x) &
skalberg@14516
  1724
   (x < max xa x) = (xa ~= x & max xa x = xa) &
skalberg@14516
  1725
   (max xa x < xa) = False & (max xa x < x) = False"
skalberg@14516
  1726
  by (import arithmetic MAX_LT)
skalberg@14516
  1727
skalberg@14516
  1728
lemma MIN_LE: "ALL (x::nat) xa::nat. min xa x <= xa & min xa x <= x"
skalberg@14516
  1729
  by (import arithmetic MIN_LE)
skalberg@14516
  1730
skalberg@14516
  1731
lemma MAX_LE: "ALL (x::nat) xa::nat. xa <= max xa x & x <= max xa x"
skalberg@14516
  1732
  by (import arithmetic MAX_LE)
skalberg@14516
  1733
obua@17652
  1734
lemma MIN_0: "ALL x::nat. min x 0 = 0 & min 0 x = 0"
skalberg@14516
  1735
  by (import arithmetic MIN_0)
skalberg@14516
  1736
obua@17652
  1737
lemma MAX_0: "ALL x::nat. max x 0 = x & max 0 x = x"
skalberg@14516
  1738
  by (import arithmetic MAX_0)
skalberg@14516
  1739
skalberg@14516
  1740
lemma EXISTS_GREATEST: "ALL P::nat => bool.
skalberg@14516
  1741
   (Ex P & (EX x::nat. ALL y::nat. x < y --> ~ P y)) =
skalberg@14516
  1742
   (EX x::nat. P x & (ALL y::nat. x < y --> ~ P y))"
skalberg@14516
  1743
  by (import arithmetic EXISTS_GREATEST)
skalberg@14516
  1744
skalberg@14516
  1745
;end_setup
skalberg@14516
  1746
skalberg@14516
  1747
;setup_theory hrat
skalberg@14516
  1748
skalberg@14516
  1749
constdefs
skalberg@14516
  1750
  trat_1 :: "nat * nat" 
obua@17652
  1751
  "trat_1 == (0, 0)"
obua@17652
  1752
obua@17652
  1753
lemma trat_1: "trat_1 = (0, 0)"
skalberg@14516
  1754
  by (import hrat trat_1)
skalberg@14516
  1755
skalberg@14516
  1756
constdefs
skalberg@14516
  1757
  trat_inv :: "nat * nat => nat * nat" 
obua@17644
  1758
  "trat_inv == %(x::nat, y::nat). (y, x)"
obua@17644
  1759
obua@17644
  1760
lemma trat_inv: "ALL (x::nat) y::nat. trat_inv (x, y) = (y, x)"
skalberg@14516
  1761
  by (import hrat trat_inv)
skalberg@14516
  1762
skalberg@14516
  1763
constdefs
skalberg@14516
  1764
  trat_add :: "nat * nat => nat * nat => nat * nat" 
skalberg@14516
  1765
  "trat_add ==
obua@17644
  1766
%(x::nat, y::nat) (x'::nat, y'::nat).
skalberg@14516
  1767
   (PRE (Suc x * Suc y' + Suc x' * Suc y), PRE (Suc y * Suc y'))"
skalberg@14516
  1768
obua@17644
  1769
lemma trat_add: "ALL (x::nat) (y::nat) (x'::nat) y'::nat.
skalberg@14516
  1770
   trat_add (x, y) (x', y') =
skalberg@14516
  1771
   (PRE (Suc x * Suc y' + Suc x' * Suc y), PRE (Suc y * Suc y'))"
skalberg@14516
  1772
  by (import hrat trat_add)
skalberg@14516
  1773
skalberg@14516
  1774
constdefs
skalberg@14516
  1775
  trat_mul :: "nat * nat => nat * nat => nat * nat" 
obua@17644
  1776
  "trat_mul ==
obua@17644
  1777
%(x::nat, y::nat) (x'::nat, y'::nat).
obua@17644
  1778
   (PRE (Suc x * Suc x'), PRE (Suc y * Suc y'))"
obua@17644
  1779
obua@17644
  1780
lemma trat_mul: "ALL (x::nat) (y::nat) (x'::nat) y'::nat.
skalberg@14516
  1781
   trat_mul (x, y) (x', y') = (PRE (Suc x * Suc x'), PRE (Suc y * Suc y'))"
skalberg@14516
  1782
  by (import hrat trat_mul)
skalberg@14516
  1783
skalberg@14516
  1784
consts
skalberg@14516
  1785
  trat_sucint :: "nat => nat * nat" 
skalberg@14516
  1786
obua@17652
  1787
specification (trat_sucint) trat_sucint: "trat_sucint 0 = trat_1 &
obua@17644
  1788
(ALL n::nat. trat_sucint (Suc n) = trat_add (trat_sucint n) trat_1)"
skalberg@14516
  1789
  by (import hrat trat_sucint)
skalberg@14516
  1790
skalberg@14516
  1791
constdefs
skalberg@14516
  1792
  trat_eq :: "nat * nat => nat * nat => bool" 
obua@17644
  1793
  "trat_eq ==
obua@17644
  1794
%(x::nat, y::nat) (x'::nat, y'::nat). Suc x * Suc y' = Suc x' * Suc y"
obua@17644
  1795
obua@17644
  1796
lemma trat_eq: "ALL (x::nat) (y::nat) (x'::nat) y'::nat.
obua@17644
  1797
   trat_eq (x, y) (x', y') = (Suc x * Suc y' = Suc x' * Suc y)"
skalberg@14516
  1798
  by (import hrat trat_eq)
skalberg@14516
  1799
obua@17644
  1800
lemma TRAT_EQ_REFL: "ALL p::nat * nat. trat_eq p p"
skalberg@14516
  1801
  by (import hrat TRAT_EQ_REFL)
skalberg@14516
  1802
obua@17644
  1803
lemma TRAT_EQ_SYM: "ALL (p::nat * nat) q::nat * nat. trat_eq p q = trat_eq q p"
skalberg@14516
  1804
  by (import hrat TRAT_EQ_SYM)
skalberg@14516
  1805
obua@17644
  1806
lemma TRAT_EQ_TRANS: "ALL (p::nat * nat) (q::nat * nat) r::nat * nat.
obua@17644
  1807
   trat_eq p q & trat_eq q r --> trat_eq p r"
skalberg@14516
  1808
  by (import hrat TRAT_EQ_TRANS)
skalberg@14516
  1809
obua@17644
  1810
lemma TRAT_EQ_AP: "ALL (p::nat * nat) q::nat * nat. p = q --> trat_eq p q"
skalberg@14516
  1811
  by (import hrat TRAT_EQ_AP)
skalberg@14516
  1812
obua@17644
  1813
lemma TRAT_ADD_SYM_EQ: "ALL (h::nat * nat) i::nat * nat. trat_add h i = trat_add i h"
skalberg@14516
  1814
  by (import hrat TRAT_ADD_SYM_EQ)
skalberg@14516
  1815
obua@17644
  1816
lemma TRAT_MUL_SYM_EQ: "ALL (h::nat * nat) i::nat * nat. trat_mul h i = trat_mul i h"
skalberg@14516
  1817
  by (import hrat TRAT_MUL_SYM_EQ)
skalberg@14516
  1818
obua@17644
  1819
lemma TRAT_INV_WELLDEFINED: "ALL (p::nat * nat) q::nat * nat.
obua@17644
  1820
   trat_eq p q --> trat_eq (trat_inv p) (trat_inv q)"
skalberg@14516
  1821
  by (import hrat TRAT_INV_WELLDEFINED)
skalberg@14516
  1822
obua@17644
  1823
lemma TRAT_ADD_WELLDEFINED: "ALL (p::nat * nat) (q::nat * nat) r::nat * nat.
obua@17644
  1824
   trat_eq p q --> trat_eq (trat_add p r) (trat_add q r)"
skalberg@14516
  1825
  by (import hrat TRAT_ADD_WELLDEFINED)
skalberg@14516
  1826
obua@17644
  1827
lemma TRAT_ADD_WELLDEFINED2: "ALL (p1::nat * nat) (p2::nat * nat) (q1::nat * nat) q2::nat * nat.
skalberg@14516
  1828
   trat_eq p1 p2 & trat_eq q1 q2 -->
skalberg@14516
  1829
   trat_eq (trat_add p1 q1) (trat_add p2 q2)"
skalberg@14516
  1830
  by (import hrat TRAT_ADD_WELLDEFINED2)
skalberg@14516
  1831
obua@17644
  1832
lemma TRAT_MUL_WELLDEFINED: "ALL (p::nat * nat) (q::nat * nat) r::nat * nat.
obua@17644
  1833
   trat_eq p q --> trat_eq (trat_mul p r) (trat_mul q r)"
skalberg@14516
  1834
  by (import hrat TRAT_MUL_WELLDEFINED)
skalberg@14516
  1835
obua@17644
  1836
lemma TRAT_MUL_WELLDEFINED2: "ALL (p1::nat * nat) (p2::nat * nat) (q1::nat * nat) q2::nat * nat.
skalberg@14516
  1837
   trat_eq p1 p2 & trat_eq q1 q2 -->
skalberg@14516
  1838
   trat_eq (trat_mul p1 q1) (trat_mul p2 q2)"
skalberg@14516
  1839
  by (import hrat TRAT_MUL_WELLDEFINED2)
skalberg@14516
  1840
obua@17644
  1841
lemma TRAT_ADD_SYM: "ALL (h::nat * nat) i::nat * nat. trat_eq (trat_add h i) (trat_add i h)"
skalberg@14516
  1842
  by (import hrat TRAT_ADD_SYM)
skalberg@14516
  1843
obua@17644
  1844
lemma TRAT_ADD_ASSOC: "ALL (h::nat * nat) (i::nat * nat) j::nat * nat.
obua@17644
  1845
   trat_eq (trat_add h (trat_add i j)) (trat_add (trat_add h i) j)"
skalberg@14516
  1846
  by (import hrat TRAT_ADD_ASSOC)
skalberg@14516
  1847
obua@17644
  1848
lemma TRAT_MUL_SYM: "ALL (h::nat * nat) i::nat * nat. trat_eq (trat_mul h i) (trat_mul i h)"
skalberg@14516
  1849
  by (import hrat TRAT_MUL_SYM)
skalberg@14516
  1850
obua@17644
  1851
lemma TRAT_MUL_ASSOC: "ALL (h::nat * nat) (i::nat * nat) j::nat * nat.
obua@17644
  1852
   trat_eq (trat_mul h (trat_mul i j)) (trat_mul (trat_mul h i) j)"
skalberg@14516
  1853
  by (import hrat TRAT_MUL_ASSOC)
skalberg@14516
  1854
obua@17644
  1855
lemma TRAT_LDISTRIB: "ALL (h::nat * nat) (i::nat * nat) j::nat * nat.
skalberg@14516
  1856
   trat_eq (trat_mul h (trat_add i j))
skalberg@14516
  1857
    (trat_add (trat_mul h i) (trat_mul h j))"
skalberg@14516
  1858
  by (import hrat TRAT_LDISTRIB)
skalberg@14516
  1859
obua@17644
  1860
lemma TRAT_MUL_LID: "ALL h::nat * nat. trat_eq (trat_mul trat_1 h) h"
skalberg@14516
  1861
  by (import hrat TRAT_MUL_LID)
skalberg@14516
  1862
obua@17644
  1863
lemma TRAT_MUL_LINV: "ALL h::nat * nat. trat_eq (trat_mul (trat_inv h) h) trat_1"
skalberg@14516
  1864
  by (import hrat TRAT_MUL_LINV)
skalberg@14516
  1865
obua@17644
  1866
lemma TRAT_NOZERO: "ALL (h::nat * nat) i::nat * nat. ~ trat_eq (trat_add h i) h"
skalberg@14516
  1867
  by (import hrat TRAT_NOZERO)
skalberg@14516
  1868
obua@17644
  1869
lemma TRAT_ADD_TOTAL: "ALL (h::nat * nat) i::nat * nat.
skalberg@14516
  1870
   trat_eq h i |
obua@17644
  1871
   (EX d::nat * nat. trat_eq h (trat_add i d)) |
obua@17644
  1872
   (EX d::nat * nat. trat_eq i (trat_add h d))"
skalberg@14516
  1873
  by (import hrat TRAT_ADD_TOTAL)
skalberg@14516
  1874
obua@17652
  1875
lemma TRAT_SUCINT_0: "ALL n::nat. trat_eq (trat_sucint n) (n, 0)"
skalberg@14516
  1876
  by (import hrat TRAT_SUCINT_0)
skalberg@14516
  1877
obua@17644
  1878
lemma TRAT_ARCH: "ALL h::nat * nat.
obua@17644
  1879
   EX (n::nat) d::nat * nat. trat_eq (trat_sucint n) (trat_add h d)"
skalberg@14516
  1880
  by (import hrat TRAT_ARCH)
skalberg@14516
  1881
obua@17652
  1882
lemma TRAT_SUCINT: "trat_eq (trat_sucint 0) trat_1 &
obua@17644
  1883
(ALL n::nat.
obua@17644
  1884
    trat_eq (trat_sucint (Suc n)) (trat_add (trat_sucint n) trat_1))"
skalberg@14516
  1885
  by (import hrat TRAT_SUCINT)
skalberg@14516
  1886
obua@17644
  1887
lemma TRAT_EQ_EQUIV: "ALL (p::nat * nat) q::nat * nat. trat_eq p q = (trat_eq p = trat_eq q)"
skalberg@14516
  1888
  by (import hrat TRAT_EQ_EQUIV)
skalberg@14516
  1889
obua@17644
  1890
typedef (open) hrat = "{x::nat * nat => bool. EX xa::nat * nat. x = trat_eq xa}" 
skalberg@14516
  1891
  by (rule typedef_helper,import hrat hrat_TY_DEF)
skalberg@14516
  1892
skalberg@14516
  1893
lemmas hrat_TY_DEF = typedef_hol2hol4 [OF type_definition_hrat]
skalberg@14516
  1894
skalberg@14516
  1895
consts
skalberg@14516
  1896
  mk_hrat :: "(nat * nat => bool) => hrat" 
skalberg@14516
  1897
  dest_hrat :: "hrat => nat * nat => bool" 
skalberg@14516
  1898
obua@17644
  1899
specification (dest_hrat mk_hrat) hrat_tybij: "(ALL a::hrat. mk_hrat (dest_hrat a) = a) &
obua@17644
  1900
(ALL r::nat * nat => bool.
obua@17644
  1901
    (EX x::nat * nat. r = trat_eq x) = (dest_hrat (mk_hrat r) = r))"
skalberg@14516
  1902
  by (import hrat hrat_tybij)
skalberg@14516
  1903
skalberg@14516
  1904
constdefs
skalberg@14516
  1905
  hrat_1 :: "hrat" 
skalberg@14516
  1906
  "hrat_1 == mk_hrat (trat_eq trat_1)"
skalberg@14516
  1907
skalberg@14516
  1908
lemma hrat_1: "hrat_1 = mk_hrat (trat_eq trat_1)"
skalberg@14516
  1909
  by (import hrat hrat_1)
skalberg@14516
  1910
skalberg@14516
  1911
constdefs
skalberg@14516
  1912
  hrat_inv :: "hrat => hrat" 
obua@17644
  1913
  "hrat_inv == %T1::hrat. mk_hrat (trat_eq (trat_inv (Eps (dest_hrat T1))))"
obua@17644
  1914
obua@17644
  1915
lemma hrat_inv: "ALL T1::hrat.
obua@17644
  1916
   hrat_inv T1 = mk_hrat (trat_eq (trat_inv (Eps (dest_hrat T1))))"
skalberg@14516
  1917
  by (import hrat hrat_inv)
skalberg@14516
  1918
skalberg@14516
  1919
constdefs
skalberg@14516
  1920
  hrat_add :: "hrat => hrat => hrat" 
skalberg@14516
  1921
  "hrat_add ==
obua@17644
  1922
%(T1::hrat) T2::hrat.
skalberg@14516
  1923
   mk_hrat (trat_eq (trat_add (Eps (dest_hrat T1)) (Eps (dest_hrat T2))))"
skalberg@14516
  1924
obua@17644
  1925
lemma hrat_add: "ALL (T1::hrat) T2::hrat.
skalberg@14516
  1926
   hrat_add T1 T2 =
skalberg@14516
  1927
   mk_hrat (trat_eq (trat_add (Eps (dest_hrat T1)) (Eps (dest_hrat T2))))"
skalberg@14516
  1928
  by (import hrat hrat_add)
skalberg@14516
  1929
skalberg@14516
  1930
constdefs
skalberg@14516
  1931
  hrat_mul :: "hrat => hrat => hrat" 
skalberg@14516
  1932
  "hrat_mul ==
obua@17644
  1933
%(T1::hrat) T2::hrat.
skalberg@14516
  1934
   mk_hrat (trat_eq (trat_mul (Eps (dest_hrat T1)) (Eps (dest_hrat T2))))"
skalberg@14516
  1935
obua@17644
  1936
lemma hrat_mul: "ALL (T1::hrat) T2::hrat.
skalberg@14516
  1937
   hrat_mul T1 T2 =
skalberg@14516
  1938
   mk_hrat (trat_eq (trat_mul (Eps (dest_hrat T1)) (Eps (dest_hrat T2))))"
skalberg@14516
  1939
  by (import hrat hrat_mul)
skalberg@14516
  1940
skalberg@14516
  1941
constdefs
skalberg@14516
  1942
  hrat_sucint :: "nat => hrat" 
obua@17644
  1943
  "hrat_sucint == %T1::nat. mk_hrat (trat_eq (trat_sucint T1))"
obua@17644
  1944
obua@17644
  1945
lemma hrat_sucint: "ALL T1::nat. hrat_sucint T1 = mk_hrat (trat_eq (trat_sucint T1))"
skalberg@14516
  1946
  by (import hrat hrat_sucint)
skalberg@14516
  1947
obua@17644
  1948
lemma HRAT_ADD_SYM: "ALL (h::hrat) i::hrat. hrat_add h i = hrat_add i h"
skalberg@14516
  1949
  by (import hrat HRAT_ADD_SYM)
skalberg@14516
  1950
obua@17644
  1951
lemma HRAT_ADD_ASSOC: "ALL (h::hrat) (i::hrat) j::hrat.
obua@17644
  1952
   hrat_add h (hrat_add i j) = hrat_add (hrat_add h i) j"
skalberg@14516
  1953
  by (import hrat HRAT_ADD_ASSOC)
skalberg@14516
  1954
obua@17644
  1955
lemma HRAT_MUL_SYM: "ALL (h::hrat) i::hrat. hrat_mul h i = hrat_mul i h"
skalberg@14516
  1956
  by (import hrat HRAT_MUL_SYM)
skalberg@14516
  1957
obua@17644
  1958
lemma HRAT_MUL_ASSOC: "ALL (h::hrat) (i::hrat) j::hrat.
obua@17644
  1959
   hrat_mul h (hrat_mul i j) = hrat_mul (hrat_mul h i) j"
skalberg@14516
  1960
  by (import hrat HRAT_MUL_ASSOC)
skalberg@14516
  1961
obua@17644
  1962
lemma HRAT_LDISTRIB: "ALL (h::hrat) (i::hrat) j::hrat.
skalberg@14516
  1963
   hrat_mul h (hrat_add i j) = hrat_add (hrat_mul h i) (hrat_mul h j)"
skalberg@14516
  1964
  by (import hrat HRAT_LDISTRIB)
skalberg@14516
  1965
obua@17644
  1966
lemma HRAT_MUL_LID: "ALL h::hrat. hrat_mul hrat_1 h = h"
skalberg@14516
  1967
  by (import hrat HRAT_MUL_LID)
skalberg@14516
  1968
obua@17644
  1969
lemma HRAT_MUL_LINV: "ALL h::hrat. hrat_mul (hrat_inv h) h = hrat_1"
skalberg@14516
  1970
  by (import hrat HRAT_MUL_LINV)
skalberg@14516
  1971
obua@17644
  1972
lemma HRAT_NOZERO: "ALL (h::hrat) i::hrat. hrat_add h i ~= h"
skalberg@14516
  1973
  by (import hrat HRAT_NOZERO)
skalberg@14516
  1974
obua@17644
  1975
lemma HRAT_ADD_TOTAL: "ALL (h::hrat) i::hrat.
obua@17644
  1976
   h = i | (EX x::hrat. h = hrat_add i x) | (EX x::hrat. i = hrat_add h x)"
skalberg@14516
  1977
  by (import hrat HRAT_ADD_TOTAL)
skalberg@14516
  1978
obua@17644
  1979
lemma HRAT_ARCH: "ALL h::hrat. EX (x::nat) xa::hrat. hrat_sucint x = hrat_add h xa"
skalberg@14516
  1980
  by (import hrat HRAT_ARCH)
skalberg@14516
  1981
obua@17652
  1982
lemma HRAT_SUCINT: "hrat_sucint 0 = hrat_1 &
obua@17644
  1983
(ALL x::nat. hrat_sucint (Suc x) = hrat_add (hrat_sucint x) hrat_1)"
skalberg@14516
  1984
  by (import hrat HRAT_SUCINT)
skalberg@14516
  1985
skalberg@14516
  1986
;end_setup
skalberg@14516
  1987
skalberg@14516
  1988
;setup_theory hreal
skalberg@14516
  1989
skalberg@14516
  1990
constdefs
skalberg@14516
  1991
  hrat_lt :: "hrat => hrat => bool" 
obua@17644
  1992
  "hrat_lt == %(x::hrat) y::hrat. EX d::hrat. y = hrat_add x d"
obua@17644
  1993
obua@17644
  1994
lemma hrat_lt: "ALL (x::hrat) y::hrat. hrat_lt x y = (EX d::hrat. y = hrat_add x d)"
skalberg@14516
  1995
  by (import hreal hrat_lt)
skalberg@14516
  1996
obua@17644
  1997
lemma HRAT_LT_REFL: "ALL x::hrat. ~ hrat_lt x x"
skalberg@14516
  1998
  by (import hreal HRAT_LT_REFL)
skalberg@14516
  1999
obua@17644
  2000
lemma HRAT_LT_TRANS: "ALL (x::hrat) (y::hrat) z::hrat. hrat_lt x y & hrat_lt y z --> hrat_lt x z"
skalberg@14516
  2001
  by (import hreal HRAT_LT_TRANS)
skalberg@14516
  2002
obua@17644
  2003
lemma HRAT_LT_ANTISYM: "ALL (x::hrat) y::hrat. ~ (hrat_lt x y & hrat_lt y x)"
skalberg@14516
  2004
  by (import hreal HRAT_LT_ANTISYM)
skalberg@14516
  2005
obua@17644
  2006
lemma HRAT_LT_TOTAL: "ALL (x::hrat) y::hrat. x = y | hrat_lt x y | hrat_lt y x"
skalberg@14516
  2007
  by (import hreal HRAT_LT_TOTAL)
skalberg@14516
  2008
obua@17644
  2009
lemma HRAT_MUL_RID: "ALL x::hrat. hrat_mul x hrat_1 = x"
skalberg@14516
  2010
  by (import hreal HRAT_MUL_RID)
skalberg@14516
  2011
obua@17644
  2012
lemma HRAT_MUL_RINV: "ALL x::hrat. hrat_mul x (hrat_inv x) = hrat_1"
skalberg@14516
  2013
  by (import hreal HRAT_MUL_RINV)
skalberg@14516
  2014
obua@17644
  2015
lemma HRAT_RDISTRIB: "ALL (x::hrat) (y::hrat) z::hrat.
skalberg@14516
  2016
   hrat_mul (hrat_add x y) z = hrat_add (hrat_mul x z) (hrat_mul y z)"
skalberg@14516
  2017
  by (import hreal HRAT_RDISTRIB)
skalberg@14516
  2018
obua@17644
  2019
lemma HRAT_LT_ADDL: "ALL (x::hrat) y::hrat. hrat_lt x (hrat_add x y)"
skalberg@14516
  2020
  by (import hreal HRAT_LT_ADDL)
skalberg@14516
  2021
obua@17644
  2022
lemma HRAT_LT_ADDR: "ALL (x::hrat) xa::hrat. hrat_lt xa (hrat_add x xa)"
skalberg@14516
  2023
  by (import hreal HRAT_LT_ADDR)
skalberg@14516
  2024
obua@17644
  2025
lemma HRAT_LT_GT: "ALL (x::hrat) y::hrat. hrat_lt x y --> ~ hrat_lt y x"
skalberg@14516
  2026
  by (import hreal HRAT_LT_GT)
skalberg@14516
  2027
obua@17644
  2028
lemma HRAT_LT_NE: "ALL (x::hrat) y::hrat. hrat_lt x y --> x ~= y"
skalberg@14516
  2029
  by (import hreal HRAT_LT_NE)
skalberg@14516
  2030
obua@17644
  2031
lemma HRAT_EQ_LADD: "ALL (x::hrat) (y::hrat) z::hrat. (hrat_add x y = hrat_add x z) = (y = z)"
skalberg@14516
  2032
  by (import hreal HRAT_EQ_LADD)
skalberg@14516
  2033
obua@17644
  2034
lemma HRAT_EQ_LMUL: "ALL (x::hrat) (y::hrat) z::hrat. (hrat_mul x y = hrat_mul x z) = (y = z)"
skalberg@14516
  2035
  by (import hreal HRAT_EQ_LMUL)
skalberg@14516
  2036
obua@17644
  2037
lemma HRAT_LT_ADD2: "ALL (u::hrat) (v::hrat) (x::hrat) y::hrat.
skalberg@14516
  2038
   hrat_lt u x & hrat_lt v y --> hrat_lt (hrat_add u v) (hrat_add x y)"
skalberg@14516
  2039
  by (import hreal HRAT_LT_ADD2)
skalberg@14516
  2040
obua@17644
  2041
lemma HRAT_LT_LADD: "ALL (x::hrat) (y::hrat) z::hrat.
obua@17644
  2042
   hrat_lt (hrat_add z x) (hrat_add z y) = hrat_lt x y"
skalberg@14516
  2043
  by (import hreal HRAT_LT_LADD)
skalberg@14516
  2044
obua@17644
  2045
lemma HRAT_LT_RADD: "ALL (x::hrat) (y::hrat) z::hrat.
obua@17644
  2046
   hrat_lt (hrat_add x z) (hrat_add y z) = hrat_lt x y"
skalberg@14516
  2047
  by (import hreal HRAT_LT_RADD)
skalberg@14516
  2048
obua@17644
  2049
lemma HRAT_LT_MUL2: "ALL (u::hrat) (v::hrat) (x::hrat) y::hrat.
skalberg@14516
  2050
   hrat_lt u x & hrat_lt v y --> hrat_lt (hrat_mul u v) (hrat_mul x y)"
skalberg@14516
  2051
  by (import hreal HRAT_LT_MUL2)
skalberg@14516
  2052
obua@17644
  2053
lemma HRAT_LT_LMUL: "ALL (x::hrat) (y::hrat) z::hrat.
obua@17644
  2054
   hrat_lt (hrat_mul z x) (hrat_mul z y) = hrat_lt x y"
skalberg@14516
  2055
  by (import hreal HRAT_LT_LMUL)
skalberg@14516
  2056
obua@17644
  2057
lemma HRAT_LT_RMUL: "ALL (x::hrat) (y::hrat) z::hrat.
obua@17644
  2058
   hrat_lt (hrat_mul x z) (hrat_mul y z) = hrat_lt x y"
skalberg@14516
  2059
  by (import hreal HRAT_LT_RMUL)
skalberg@14516
  2060
obua@17644
  2061
lemma HRAT_LT_LMUL1: "ALL (x::hrat) y::hrat. hrat_lt (hrat_mul x y) y = hrat_lt x hrat_1"
skalberg@14516
  2062
  by (import hreal HRAT_LT_LMUL1)
skalberg@14516
  2063
obua@17644
  2064
lemma HRAT_LT_RMUL1: "ALL (x::hrat) y::hrat. hrat_lt (hrat_mul x y) x = hrat_lt y hrat_1"
skalberg@14516
  2065
  by (import hreal HRAT_LT_RMUL1)
skalberg@14516
  2066
obua@17644
  2067
lemma HRAT_GT_LMUL1: "ALL (x::hrat) y::hrat. hrat_lt y (hrat_mul x y) = hrat_lt hrat_1 x"
skalberg@14516
  2068
  by (import hreal HRAT_GT_LMUL1)
skalberg@14516
  2069
obua@17644
  2070
lemma HRAT_LT_L1: "ALL (x::hrat) y::hrat.
obua@17644
  2071
   hrat_lt (hrat_mul (hrat_inv x) y) hrat_1 = hrat_lt y x"
skalberg@14516
  2072
  by (import hreal HRAT_LT_L1)
skalberg@14516
  2073
obua@17644
  2074
lemma HRAT_LT_R1: "ALL (x::hrat) y::hrat.
obua@17644
  2075
   hrat_lt (hrat_mul x (hrat_inv y)) hrat_1 = hrat_lt x y"
skalberg@14516
  2076
  by (import hreal HRAT_LT_R1)
skalberg@14516
  2077
obua@17644
  2078
lemma HRAT_GT_L1: "ALL (x::hrat) y::hrat.
obua@17644
  2079
   hrat_lt hrat_1 (hrat_mul (hrat_inv x) y) = hrat_lt x y"
skalberg@14516
  2080
  by (import hreal HRAT_GT_L1)
skalberg@14516
  2081
obua@17644
  2082
lemma HRAT_INV_MUL: "ALL (x::hrat) y::hrat.
obua@17644
  2083
   hrat_inv (hrat_mul x y) = hrat_mul (hrat_inv x) (hrat_inv y)"
skalberg@14516
  2084
  by (import hreal HRAT_INV_MUL)
skalberg@14516
  2085
obua@17644
  2086
lemma HRAT_UP: "ALL x::hrat. Ex (hrat_lt x)"
skalberg@14516
  2087
  by (import hreal HRAT_UP)
skalberg@14516
  2088
obua@17644
  2089
lemma HRAT_DOWN: "ALL x::hrat. EX xa::hrat. hrat_lt xa x"
skalberg@14516
  2090
  by (import hreal HRAT_DOWN)
skalberg@14516
  2091
obua@17644
  2092
lemma HRAT_DOWN2: "ALL (x::hrat) y::hrat. EX xa::hrat. hrat_lt xa x & hrat_lt xa y"
skalberg@14516
  2093
  by (import hreal HRAT_DOWN2)
skalberg@14516
  2094
obua@17644
  2095
lemma HRAT_MEAN: "ALL (x::hrat) y::hrat.
obua@17644
  2096
   hrat_lt x y --> (EX xa::hrat. hrat_lt x xa & hrat_lt xa y)"
skalberg@14516
  2097
  by (import hreal HRAT_MEAN)
skalberg@14516
  2098
skalberg@14516
  2099
constdefs
skalberg@14516
  2100
  isacut :: "(hrat => bool) => bool" 
skalberg@14516
  2101
  "isacut ==
obua@17644
  2102
%C::hrat => bool.
obua@17644
  2103
   Ex C &
obua@17644
  2104
   (EX x::hrat. ~ C x) &
obua@17644
  2105
   (ALL (x::hrat) y::hrat. C x & hrat_lt y x --> C y) &
obua@17644
  2106
   (ALL x::hrat. C x --> (EX y::hrat. C y & hrat_lt x y))"
obua@17644
  2107
obua@17644
  2108
lemma isacut: "ALL C::hrat => bool.
skalberg@14516
  2109
   isacut C =
skalberg@14516
  2110
   (Ex C &
obua@17644
  2111
    (EX x::hrat. ~ C x) &
obua@17644
  2112
    (ALL (x::hrat) y::hrat. C x & hrat_lt y x --> C y) &
obua@17644
  2113
    (ALL x::hrat. C x --> (EX y::hrat. C y & hrat_lt x y)))"
skalberg@14516
  2114
  by (import hreal isacut)
skalberg@14516
  2115
skalberg@14516
  2116
constdefs
skalberg@14516
  2117
  cut_of_hrat :: "hrat => hrat => bool" 
obua@17644
  2118
  "cut_of_hrat == %(x::hrat) y::hrat. hrat_lt y x"
obua@17644
  2119
obua@17644
  2120
lemma cut_of_hrat: "ALL x::hrat. cut_of_hrat x = (%y::hrat. hrat_lt y x)"
skalberg@14516
  2121
  by (import hreal cut_of_hrat)
skalberg@14516
  2122
obua@17644
  2123
lemma ISACUT_HRAT: "ALL h::hrat. isacut (cut_of_hrat h)"
skalberg@14516
  2124
  by (import hreal ISACUT_HRAT)
skalberg@14516
  2125
skalberg@14516
  2126
typedef (open) hreal = "Collect isacut" 
skalberg@14516
  2127
  by (rule typedef_helper,import hreal hreal_TY_DEF)
skalberg@14516
  2128
skalberg@14516
  2129
lemmas hreal_TY_DEF = typedef_hol2hol4 [OF type_definition_hreal]
skalberg@14516
  2130
skalberg@14516
  2131
consts
skalberg@14516
  2132
  hreal :: "(hrat => bool) => hreal" 
skalberg@14516
  2133
  cut :: "hreal => hrat => bool" 
skalberg@14516
  2134
obua@17644
  2135
specification (cut hreal) hreal_tybij: "(ALL a::hreal. hreal (hreal.cut a) = a) &
obua@17644
  2136
(ALL r::hrat => bool. isacut r = (hreal.cut (hreal r) = r))"
skalberg@14516
  2137
  by (import hreal hreal_tybij)
skalberg@14516
  2138
obua@17644
  2139
lemma EQUAL_CUTS: "ALL (X::hreal) Y::hreal. hreal.cut X = hreal.cut Y --> X = Y"
skalberg@14516
  2140
  by (import hreal EQUAL_CUTS)
skalberg@14516
  2141
obua@17644
  2142
lemma CUT_ISACUT: "ALL x::hreal. isacut (hreal.cut x)"
skalberg@14516
  2143
  by (import hreal CUT_ISACUT)
skalberg@14516
  2144
obua@17644
  2145
lemma CUT_NONEMPTY: "ALL x::hreal. Ex (hreal.cut x)"
skalberg@14516
  2146
  by (import hreal CUT_NONEMPTY)
skalberg@14516
  2147
obua@17644
  2148
lemma CUT_BOUNDED: "ALL x::hreal. EX xa::hrat. ~ hreal.cut x xa"
skalberg@14516
  2149
  by (import hreal CUT_BOUNDED)
skalberg@14516
  2150
obua@17644
  2151
lemma CUT_DOWN: "ALL (x::hreal) (xa::hrat) xb::hrat.
obua@17644
  2152
   hreal.cut x xa & hrat_lt xb xa --> hreal.cut x xb"
skalberg@14516
  2153
  by (import hreal CUT_DOWN)
skalberg@14516
  2154
obua@17644
  2155
lemma CUT_UP: "ALL (x::hreal) xa::hrat.
obua@17644
  2156
   hreal.cut x xa --> (EX y::hrat. hreal.cut x y & hrat_lt xa y)"
skalberg@14516
  2157
  by (import hreal CUT_UP)
skalberg@14516
  2158
obua@17644
  2159
lemma CUT_UBOUND: "ALL (x::hreal) (xa::hrat) xb::hrat.
obua@17644
  2160
   ~ hreal.cut x xa & hrat_lt xa xb --> ~ hreal.cut x xb"
skalberg@14516
  2161
  by (import hreal CUT_UBOUND)
skalberg@14516
  2162
obua@17644
  2163
lemma CUT_STRADDLE: "ALL (X::hreal) (x::hrat) y::hrat.
obua@17644
  2164
   hreal.cut X x & ~ hreal.cut X y --> hrat_lt x y"
skalberg@14516
  2165
  by (import hreal CUT_STRADDLE)
skalberg@14516
  2166
obua@17644
  2167
lemma CUT_NEARTOP_ADD: "ALL (X::hreal) e::hrat.
obua@17644
  2168
   EX x::hrat. hreal.cut X x & ~ hreal.cut X (hrat_add x e)"
skalberg@14516
  2169
  by (import hreal CUT_NEARTOP_ADD)
skalberg@14516
  2170
obua@17644
  2171
lemma CUT_NEARTOP_MUL: "ALL (X::hreal) u::hrat.
obua@17644
  2172
   hrat_lt hrat_1 u -->
obua@17644
  2173
   (EX x::hrat. hreal.cut X x & ~ hreal.cut X (hrat_mul u x))"
skalberg@14516
  2174
  by (import hreal CUT_NEARTOP_MUL)
skalberg@14516
  2175
skalberg@14516
  2176
constdefs
skalberg@14516
  2177
  hreal_1 :: "hreal" 
skalberg@14516
  2178
  "hreal_1 == hreal (cut_of_hrat hrat_1)"
skalberg@14516
  2179
skalberg@14516
  2180
lemma hreal_1: "hreal_1 = hreal (cut_of_hrat hrat_1)"
skalberg@14516
  2181
  by (import hreal hreal_1)
skalberg@14516
  2182
skalberg@14516
  2183
constdefs
skalberg@14516
  2184
  hreal_add :: "hreal => hreal => hreal" 
skalberg@14516
  2185
  "hreal_add ==
obua@17644
  2186
%(X::hreal) Y::hreal.
obua@17644
  2187
   hreal
obua@17644
  2188
    (%w::hrat.
obua@17644
  2189
        EX (x::hrat) y::hrat.
obua@17644
  2190
           w = hrat_add x y & hreal.cut X x & hreal.cut Y y)"
obua@17644
  2191
obua@17644
  2192
lemma hreal_add: "ALL (X::hreal) Y::hreal.
skalberg@14516
  2193
   hreal_add X Y =
obua@17644
  2194
   hreal
obua@17644
  2195
    (%w::hrat.
obua@17644
  2196
        EX (x::hrat) y::hrat.
obua@17644
  2197
           w = hrat_add x y & hreal.cut X x & hreal.cut Y y)"
skalberg@14516
  2198
  by (import hreal hreal_add)
skalberg@14516
  2199
skalberg@14516
  2200
constdefs
skalberg@14516
  2201
  hreal_mul :: "hreal => hreal => hreal" 
skalberg@14516
  2202
  "hreal_mul ==
obua@17644
  2203
%(X::hreal) Y::hreal.
obua@17644
  2204
   hreal
obua@17644
  2205
    (%w::hrat.
obua@17644
  2206
        EX (x::hrat) y::hrat.
obua@17644
  2207
           w = hrat_mul x y & hreal.cut X x & hreal.cut Y y)"
obua@17644
  2208
obua@17644
  2209
lemma hreal_mul: "ALL (X::hreal) Y::hreal.
skalberg@14516
  2210
   hreal_mul X Y =
obua@17644
  2211
   hreal
obua@17644
  2212
    (%w::hrat.
obua@17644
  2213
        EX (x::hrat) y::hrat.
obua@17644
  2214
           w = hrat_mul x y & hreal.cut X x & hreal.cut Y y)"
skalberg@14516
  2215
  by (import hreal hreal_mul)
skalberg@14516
  2216
skalberg@14516
  2217
constdefs
skalberg@14516
  2218
  hreal_inv :: "hreal => hreal" 
skalberg@14516
  2219
  "hreal_inv ==
obua@17644
  2220
%X::hreal.
obua@17644
  2221
   hreal
obua@17644
  2222
    (%w::hrat.
obua@17644
  2223
        EX d::hrat.
obua@17644
  2224
           hrat_lt d hrat_1 &
obua@17644
  2225
           (ALL x::hrat. hreal.cut X x --> hrat_lt (hrat_mul w x) d))"
obua@17644
  2226
obua@17644
  2227
lemma hreal_inv: "ALL X::hreal.
skalberg@14516
  2228
   hreal_inv X =
skalberg@14516
  2229
   hreal
obua@17644
  2230
    (%w::hrat.
obua@17644
  2231
        EX d::hrat.
obua@17644
  2232
           hrat_lt d hrat_1 &
obua@17644
  2233
           (ALL x::hrat. hreal.cut X x --> hrat_lt (hrat_mul w x) d))"
skalberg@14516
  2234
  by (import hreal hreal_inv)
skalberg@14516
  2235
skalberg@14516
  2236
constdefs
skalberg@14516
  2237
  hreal_sup :: "(hreal => bool) => hreal" 
obua@17644
  2238
  "hreal_sup ==
obua@17644
  2239
%P::hreal => bool. hreal (%w::hrat. EX X::hreal. P X & hreal.cut X w)"
obua@17644
  2240
obua@17644
  2241
lemma hreal_sup: "ALL P::hreal => bool.
obua@17644
  2242
   hreal_sup P = hreal (%w::hrat. EX X::hreal. P X & hreal.cut X w)"
skalberg@14516
  2243
  by (import hreal hreal_sup)
skalberg@14516
  2244
skalberg@14516
  2245
constdefs
skalberg@14516
  2246
  hreal_lt :: "hreal => hreal => bool" 
obua@17644
  2247
  "hreal_lt ==
obua@17644
  2248
%(X::hreal) Y::hreal.
obua@17644
  2249
   X ~= Y & (ALL x::hrat. hreal.cut X x --> hreal.cut Y x)"
obua@17644
  2250
obua@17644
  2251
lemma hreal_lt: "ALL (X::hreal) Y::hreal.
obua@17644
  2252
   hreal_lt X Y = (X ~= Y & (ALL x::hrat. hreal.cut X x --> hreal.cut Y x))"
skalberg@14516
  2253
  by (import hreal hreal_lt)
skalberg@14516
  2254
obua@17644
  2255
lemma HREAL_INV_ISACUT: "ALL X::hreal.
skalberg@14516
  2256
   isacut
obua@17644
  2257
    (%w::hrat.
obua@17644
  2258
        EX d::hrat.
obua@17644
  2259
           hrat_lt d hrat_1 &
obua@17644
  2260
           (ALL x::hrat. hreal.cut X x --> hrat_lt (hrat_mul w x) d))"
skalberg@14516
  2261
  by (import hreal HREAL_INV_ISACUT)
skalberg@14516
  2262
obua@17644
  2263
lemma HREAL_ADD_ISACUT: "ALL (X::hreal) Y::hreal.
obua@17644
  2264
   isacut
obua@17644
  2265
    (%w::hrat.
obua@17644
  2266
        EX (x::hrat) y::hrat.
obua@17644
  2267
           w = hrat_add x y & hreal.cut X x & hreal.cut Y y)"
skalberg@14516
  2268
  by (import hreal HREAL_ADD_ISACUT)
skalberg@14516
  2269
obua@17644
  2270
lemma HREAL_MUL_ISACUT: "ALL (X::hreal) Y::hreal.
obua@17644
  2271
   isacut
obua@17644
  2272
    (%w::hrat.
obua@17644
  2273
        EX (x::hrat) y::hrat.
obua@17644
  2274
           w = hrat_mul x y & hreal.cut X x & hreal.cut Y y)"
skalberg@14516
  2275
  by (import hreal HREAL_MUL_ISACUT)
skalberg@14516
  2276
obua@17644
  2277
lemma HREAL_ADD_SYM: "ALL (X::hreal) Y::hreal. hreal_add X Y = hreal_add Y X"
skalberg@14516
  2278
  by (import hreal HREAL_ADD_SYM)
skalberg@14516
  2279
obua@17644
  2280
lemma HREAL_MUL_SYM: "ALL (X::hreal) Y::hreal. hreal_mul X Y = hreal_mul Y X"
skalberg@14516
  2281
  by (import hreal HREAL_MUL_SYM)
skalberg@14516
  2282
obua@17644
  2283
lemma HREAL_ADD_ASSOC: "ALL (X::hreal) (Y::hreal) Z::hreal.
obua@17644
  2284
   hreal_add X (hreal_add Y Z) = hreal_add (hreal_add X Y) Z"
skalberg@14516
  2285
  by (import hreal HREAL_ADD_ASSOC)
skalberg@14516
  2286
obua@17644
  2287
lemma HREAL_MUL_ASSOC: "ALL (X::hreal) (Y::hreal) Z::hreal.
obua@17644
  2288
   hreal_mul X (hreal_mul Y Z) = hreal_mul (hreal_mul X Y) Z"
skalberg@14516
  2289
  by (import hreal HREAL_MUL_ASSOC)
skalberg@14516
  2290
obua@17644
  2291
lemma HREAL_LDISTRIB: "ALL (X::hreal) (Y::hreal) Z::hreal.
skalberg@14516
  2292
   hreal_mul X (hreal_add Y Z) = hreal_add (hreal_mul X Y) (hreal_mul X Z)"
skalberg@14516
  2293
  by (import hreal HREAL_LDISTRIB)
skalberg@14516
  2294
obua@17644
  2295
lemma HREAL_MUL_LID: "ALL X::hreal. hreal_mul hreal_1 X = X"
skalberg@14516
  2296
  by (import hreal HREAL_MUL_LID)
skalberg@14516
  2297
obua@17644
  2298
lemma HREAL_MUL_LINV: "ALL X::hreal. hreal_mul (hreal_inv X) X = hreal_1"
skalberg@14516
  2299
  by (import hreal HREAL_MUL_LINV)
skalberg@14516
  2300
obua@17644
  2301
lemma HREAL_NOZERO: "ALL (X::hreal) Y::hreal. hreal_add X Y ~= X"
skalberg@14516
  2302
  by (import hreal HREAL_NOZERO)
skalberg@14516
  2303
skalberg@14516
  2304
constdefs
skalberg@14516
  2305
  hreal_sub :: "hreal => hreal => hreal" 
skalberg@14516
  2306
  "hreal_sub ==
obua@17644
  2307
%(Y::hreal) X::hreal.
obua@17644
  2308
   hreal
obua@17644
  2309
    (%w::hrat. EX x::hrat. ~ hreal.cut X x & hreal.cut Y (hrat_add x w))"
obua@17644
  2310
obua@17644
  2311
lemma hreal_sub: "ALL (Y::hreal) X::hreal.
skalberg@14516
  2312
   hreal_sub Y X =
obua@17644
  2313
   hreal
obua@17644
  2314
    (%w::hrat. EX x::hrat. ~ hreal.cut X x & hreal.cut Y (hrat_add x w))"
skalberg@14516
  2315
  by (import hreal hreal_sub)
skalberg@14516
  2316
obua@17644
  2317
lemma HREAL_LT_LEMMA: "ALL (X::hreal) Y::hreal.
obua@17644
  2318
   hreal_lt X Y --> (EX x::hrat. ~ hreal.cut X x & hreal.cut Y x)"
skalberg@14516
  2319
  by (import hreal HREAL_LT_LEMMA)
skalberg@14516
  2320
obua@17644
  2321
lemma HREAL_SUB_ISACUT: "ALL (X::hreal) Y::hreal.
skalberg@14516
  2322
   hreal_lt X Y -->
obua@17644
  2323
   isacut
obua@17644
  2324
    (%w::hrat. EX x::hrat. ~ hreal.cut X x & hreal.cut Y (hrat_add x w))"
skalberg@14516
  2325
  by (import hreal HREAL_SUB_ISACUT)
skalberg@14516
  2326
obua@17644
  2327
lemma HREAL_SUB_ADD: "ALL (X::hreal) Y::hreal. hreal_lt X Y --> hreal_add (hreal_sub Y X) X = Y"
skalberg@14516
  2328
  by (import hreal HREAL_SUB_ADD)
skalberg@14516
  2329
obua@17644
  2330
lemma HREAL_LT_TOTAL: "ALL (X::hreal) Y::hreal. X = Y | hreal_lt X Y | hreal_lt Y X"
skalberg@14516
  2331
  by (import hreal HREAL_LT_TOTAL)
skalberg@14516
  2332
obua@17644
  2333
lemma HREAL_LT: "ALL (X::hreal) Y::hreal. hreal_lt X Y = (EX D::hreal. Y = hreal_add X D)"
skalberg@14516
  2334
  by (import hreal HREAL_LT)
skalberg@14516
  2335
obua@17644
  2336
lemma HREAL_ADD_TOTAL: "ALL (X::hreal) Y::hreal.
obua@17644
  2337
   X = Y |
obua@17644
  2338
   (EX D::hreal. Y = hreal_add X D) | (EX D::hreal. X = hreal_add Y D)"
skalberg@14516
  2339
  by (import hreal HREAL_ADD_TOTAL)
skalberg@14516
  2340
obua@17644
  2341
lemma HREAL_SUP_ISACUT: "ALL P::hreal => bool.
obua@17644
  2342
   Ex P & (EX Y::hreal. ALL X::hreal. P X --> hreal_lt X Y) -->
obua@17644
  2343
   isacut (%w::hrat. EX X::hreal. P X & hreal.cut X w)"
skalberg@14516
  2344
  by (import hreal HREAL_SUP_ISACUT)
skalberg@14516
  2345
obua@17644
  2346
lemma HREAL_SUP: "ALL P::hreal => bool.
obua@17644
  2347
   Ex P & (EX Y::hreal. ALL X::hreal. P X --> hreal_lt X Y) -->
obua@17644
  2348
   (ALL Y::hreal.
obua@17644
  2349
       (EX X::hreal. P X & hreal_lt Y X) = hreal_lt Y (hreal_sup P))"
skalberg@14516
  2350
  by (import hreal HREAL_SUP)
skalberg@14516
  2351
skalberg@14516
  2352
;end_setup
skalberg@14516
  2353
skalberg@14516
  2354
;setup_theory numeral
skalberg@14516
  2355
skalberg@14516
  2356
lemma numeral_suc: "Suc ALT_ZERO = NUMERAL_BIT1 ALT_ZERO &
obua@17644
  2357
(ALL x::nat. Suc (NUMERAL_BIT1 x) = NUMERAL_BIT2 x) &
obua@17644
  2358
(ALL x::nat. Suc (NUMERAL_BIT2 x) = NUMERAL_BIT1 (Suc x))"
skalberg@14516
  2359
  by (import numeral numeral_suc)
skalberg@14516
  2360
skalberg@14516
  2361
constdefs
skalberg@14516
  2362
  iZ :: "nat => nat" 
obua@17644
  2363
  "iZ == %x::nat. x"
obua@17644
  2364
obua@17644
  2365
lemma iZ: "ALL x::nat. iZ x = x"
skalberg@14516
  2366
  by (import numeral iZ)
skalberg@14516
  2367
skalberg@14516
  2368
constdefs
skalberg@14516
  2369
  iiSUC :: "nat => nat" 
obua@17644
  2370
  "iiSUC == %n::nat. Suc (Suc n)"
obua@17644
  2371
obua@17644
  2372
lemma iiSUC: "ALL n::nat. iiSUC n = Suc (Suc n)"
skalberg@14516
  2373
  by (import numeral iiSUC)
skalberg@14516
  2374
obua@17652
  2375
lemma numeral_distrib: "(op &::bool => bool => bool)
obua@17652
  2376
 ((All::(nat => bool) => bool)
obua@17652
  2377
   (%x::nat.
obua@17652
  2378
       (op =::nat => nat => bool) ((op +::nat => nat => nat) (0::nat) x) x))
obua@17652
  2379
 ((op &::bool => bool => bool)
obua@17652
  2380
   ((All::(nat => bool) => bool)
obua@17652
  2381
     (%x::nat.
obua@17652
  2382
         (op =::nat => nat => bool) ((op +::nat => nat => nat) x (0::nat))
obua@17652
  2383
          x))
obua@17652
  2384
   ((op &::bool => bool => bool)
obua@17652
  2385
     ((All::(nat => bool) => bool)
obua@17652
  2386
       (%x::nat.
obua@17652
  2387
           (All::(nat => bool) => bool)
obua@17652
  2388
            (%xa::nat.
obua@17652
  2389
                (op =::nat => nat => bool)
obua@17652
  2390
                 ((op +::nat => nat => nat) ((NUMERAL::nat => nat) x)
obua@17652
  2391
                   ((NUMERAL::nat => nat) xa))
obua@17652
  2392
                 ((NUMERAL::nat => nat)
obua@17652
  2393
                   ((iZ::nat => nat) ((op +::nat => nat => nat) x xa))))))
obua@17652
  2394
     ((op &::bool => bool => bool)
obua@17652
  2395
       ((All::(nat => bool) => bool)
obua@17652
  2396
         (%x::nat.
obua@17652
  2397
             (op =::nat => nat => bool)
obua@17652
  2398
              ((op *::nat => nat => nat) (0::nat) x) (0::nat)))
obua@17652
  2399
       ((op &::bool => bool => bool)
obua@17652
  2400
         ((All::(nat => bool) => bool)
obua@17652
  2401
           (%x::nat.
obua@17652
  2402
               (op =::nat => nat => bool)
obua@17652
  2403
                ((op *::nat => nat => nat) x (0::nat)) (0::nat)))
obua@17652
  2404
         ((op &::bool => bool => bool)
obua@17652
  2405
           ((All::(nat => bool) => bool)
obua@17652
  2406
             (%x::nat.
obua@17652
  2407
                 (All::(nat => bool) => bool)
obua@17652
  2408
                  (%xa::nat.
obua@17652
  2409
                      (op =::nat => nat => bool)
obua@17652
  2410
                       ((op *::nat => nat => nat) ((NUMERAL::nat => nat) x)
obua@17652
  2411
                         ((NUMERAL::nat => nat) xa))
obua@17652
  2412
                       ((NUMERAL::nat => nat)
obua@17652
  2413
                         ((op *::nat => nat => nat) x xa)))))
obua@17652
  2414
           ((op &::bool => bool => bool)
obua@17652
  2415
             ((All::(nat => bool) => bool)
obua@17652
  2416
               (%x::nat.
obua@17652
  2417
                   (op =::nat => nat => bool)
obua@17652
  2418
                    ((op -::nat => nat => nat) (0::nat) x) (0::nat)))
obua@17652
  2419
             ((op &::bool => bool => bool)
obua@17652
  2420
               ((All::(nat => bool) => bool)
obua@17652
  2421
                 (%x::nat.
obua@17652
  2422
                     (op =::nat => nat => bool)
obua@17652
  2423
                      ((op -::nat => nat => nat) x (0::nat)) x))
obua@17652
  2424
               ((op &::bool => bool => bool)
obua@17652
  2425
                 ((All::(nat => bool) => bool)
obua@17652
  2426
                   (%x::nat.
obua@17652
  2427
                       (All::(nat => bool) => bool)
obua@17652
  2428
                        (%xa::nat.
obua@17652
  2429
                            (op =::nat => nat => bool)
obua@17652
  2430
                             ((op -::nat => nat => nat)
obua@17652
  2431
                               ((NUMERAL::nat => nat) x)
obua@17652
  2432
                               ((NUMERAL::nat => nat) xa))
obua@17652
  2433
                             ((NUMERAL::nat => nat)
obua@17652
  2434
                               ((op -::nat => nat => nat) x xa)))))
obua@17652
  2435
                 ((op &::bool => bool => bool)
obua@17652
  2436
                   ((All::(nat => bool) => bool)
obua@17652
  2437
                     (%x::nat.
obua@17652
  2438
                         (op =::nat => nat => bool)
obua@17652
  2439
                          ((op ^::nat => nat => nat) (0::nat)
obua@17652
  2440
                            ((NUMERAL::nat => nat)
obua@17652
  2441
                              ((NUMERAL_BIT1::nat => nat) x)))
obua@17652
  2442
                          (0::nat)))
obua@17652
  2443
                   ((op &::bool => bool => bool)
obua@17652
  2444
                     ((All::(nat => bool) => bool)
obua@17652
  2445
                       (%x::nat.
obua@17652
  2446
                           (op =::nat => nat => bool)
obua@17652
  2447
                            ((op ^::nat => nat => nat) (0::nat)
obua@17652
  2448
                              ((NUMERAL::nat => nat)
obua@17652
  2449
                                ((NUMERAL_BIT2::nat => nat) x)))
obua@17652
  2450
                            (0::nat)))
obua@17652
  2451
                     ((op &::bool => bool => bool)
obua@17652
  2452
                       ((All::(nat => bool) => bool)
obua@17652
  2453
                         (%x::nat.
obua@17652
  2454
                             (op =::nat => nat => bool)
obua@17652
  2455
                              ((op ^::nat => nat => nat) x (0::nat))
obua@17652
  2456
                              (1::nat)))
obua@17652
  2457
                       ((op &::bool => bool => bool)
obua@17652
  2458
                         ((All::(nat => bool) => bool)
obua@17652
  2459
                           (%x::nat.
obua@17652
  2460
                               (All::(nat => bool) => bool)
obua@17652
  2461
                                (%xa::nat.
obua@17652
  2462
                                    (op =::nat => nat => bool)
obua@17652
  2463
                                     ((op ^::nat => nat => nat)
obua@17652
  2464
 ((NUMERAL::nat => nat) x) ((NUMERAL::nat => nat) xa))
obua@17652
  2465
                                     ((NUMERAL::nat => nat)
obua@17652
  2466
 ((op ^::nat => nat => nat) x xa)))))
obua@17652
  2467
                         ((op &::bool => bool => bool)
obua@17652
  2468
                           ((op =::nat => nat => bool)
obua@17652
  2469
                             ((Suc::nat => nat) (0::nat)) (1::nat))
obua@17652
  2470
                           ((op &::bool => bool => bool)
obua@17652
  2471
                             ((All::(nat => bool) => bool)
obua@17652
  2472
                               (%x::nat.
obua@17652
  2473
                                   (op =::nat => nat => bool)
obua@17652
  2474
                                    ((Suc::nat => nat)
obua@17652
  2475
((NUMERAL::nat => nat) x))
obua@17652
  2476
                                    ((NUMERAL::nat => nat)
obua@17652
  2477
((Suc::nat => nat) x))))
obua@17652
  2478
                             ((op &::bool => bool => bool)
obua@17652
  2479
                               ((op =::nat => nat => bool)
obua@17652
  2480
                                 ((PRE::nat => nat) (0::nat)) (0::nat))
obua@17652
  2481
                               ((op &::bool => bool => bool)
obua@17652
  2482
                                 ((All::(nat => bool) => bool)
obua@17652
  2483
                                   (%x::nat.
obua@17652
  2484
 (op =::nat => nat => bool) ((PRE::nat => nat) ((NUMERAL::nat => nat) x))
obua@17652
  2485
  ((NUMERAL::nat => nat) ((PRE::nat => nat) x))))
obua@17652
  2486
                                 ((op &::bool => bool => bool)
obua@17652
  2487
                                   ((All::(nat => bool) => bool)
obua@17652
  2488
                                     (%x::nat.
obua@17652
  2489
   (op =::bool => bool => bool)
obua@17652
  2490
    ((op =::nat => nat => bool) ((NUMERAL::nat => nat) x) (0::nat))
obua@17652
  2491
    ((op =::nat => nat => bool) x (ALT_ZERO::nat))))
obua@17652
  2492
                                   ((op &::bool => bool => bool)
obua@17652
  2493
                                     ((All::(nat => bool) => bool)
obua@17652
  2494
 (%x::nat.
obua@17652
  2495
     (op =::bool => bool => bool)
obua@17652
  2496
      ((op =::nat => nat => bool) (0::nat) ((NUMERAL::nat => nat) x))
obua@17652
  2497
      ((op =::nat => nat => bool) x (ALT_ZERO::nat))))
obua@17652
  2498
                                     ((op &::bool => bool => bool)
obua@17652
  2499
 ((All::(nat => bool) => bool)
obua@17652
  2500
   (%x::nat.
obua@17652
  2501
       (All::(nat => bool) => bool)
obua@17652
  2502
        (%xa::nat.
obua@17652
  2503
            (op =::bool => bool => bool)
obua@17652
  2504
             ((op =::nat => nat => bool) ((NUMERAL::nat => nat) x)
obua@17652
  2505
               ((NUMERAL::nat => nat) xa))
obua@17652
  2506
             ((op =::nat => nat => bool) x xa))))
obua@17652
  2507
 ((op &::bool => bool => bool)
obua@17652
  2508
   ((All::(nat => bool) => bool)
obua@17652
  2509
     (%x::nat.
obua@17652
  2510
         (op =::bool => bool => bool)
obua@17652
  2511
          ((op <::nat => nat => bool) x (0::nat)) (False::bool)))
obua@17652
  2512
   ((op &::bool => bool => bool)
obua@17652
  2513
     ((All::(nat => bool) => bool)
obua@17652
  2514
       (%x::nat.
obua@17652
  2515
           (op =::bool => bool => bool)
obua@17652
  2516
            ((op <::nat => nat => bool) (0::nat) ((NUMERAL::nat => nat) x))
obua@17652
  2517
            ((op <::nat => nat => bool) (ALT_ZERO::nat) x)))
obua@17652
  2518
     ((op &::bool => bool => bool)
obua@17652
  2519
       ((All::(nat => bool) => bool)
obua@17652
  2520
         (%x::nat.
obua@17652
  2521
             (All::(nat => bool) => bool)
obua@17652
  2522
              (%xa::nat.
obua@17652
  2523
                  (op =::bool => bool => bool)
obua@17652
  2524
                   ((op <::nat => nat => bool) ((NUMERAL::nat => nat) x)
obua@17652
  2525
                     ((NUMERAL::nat => nat) xa))
obua@17652
  2526
                   ((op <::nat => nat => bool) x xa))))
obua@17652
  2527
       ((op &::bool => bool => bool)
obua@17652
  2528
         ((All::(nat => bool) => bool)
obua@17652
  2529
           (%x::nat.
obua@17652
  2530
               (op =::bool => bool => bool)
obua@17652
  2531
                ((op <::nat => nat => bool) x (0::nat)) (False::bool)))
obua@17652
  2532
         ((op &::bool => bool => bool)
obua@17652
  2533
           ((All::(nat => bool) => bool)
obua@17652
  2534
             (%x::nat.
obua@17652
  2535
                 (op =::bool => bool => bool)
obua@17652
  2536
                  ((op <::nat => nat => bool) (0::nat)
obua@17652
  2537
                    ((NUMERAL::nat => nat) x))
obua@17652
  2538
                  ((op <::nat => nat => bool) (ALT_ZERO::nat) x)))
obua@17652
  2539
           ((op &::bool => bool => bool)
obua@17652
  2540
             ((All::(nat => bool) => bool)
obua@17652
  2541
               (%x::nat.
obua@17652
  2542
                   (All::(nat => bool) => bool)
obua@17652
  2543
                    (%xa::nat.
obua@17652
  2544
                        (op =::bool => bool => bool)
obua@17652
  2545
                         ((op <::nat => nat => bool)
obua@17652
  2546
                           ((NUMERAL::nat => nat) xa)
obua@17652
  2547
                           ((NUMERAL::nat => nat) x))
obua@17652
  2548
                         ((op <::nat => nat => bool) xa x))))
obua@17652
  2549
             ((op &::bool => bool => bool)
obua@17652
  2550
               ((All::(nat => bool) => bool)
obua@17652
  2551
                 (%x::nat.
obua@17652
  2552
                     (op =::bool => bool => bool)
obua@17652
  2553
                      ((op <=::nat => nat => bool) (0::nat) x)
obua@17652
  2554
                      (True::bool)))
obua@17652
  2555
               ((op &::bool => bool => bool)
obua@17652
  2556
                 ((All::(nat => bool) => bool)
obua@17652
  2557
                   (%x::nat.
obua@17652
  2558
                       (op =::bool => bool => bool)
obua@17652
  2559
                        ((op <=::nat => nat => bool)
obua@17652
  2560
                          ((NUMERAL::nat => nat) x) (0::nat))
obua@17652
  2561
                        ((op <=::nat => nat => bool) x (ALT_ZERO::nat))))
obua@17652
  2562
                 ((op &::bool => bool => bool)
obua@17652
  2563
                   ((All::(nat => bool) => bool)
obua@17652
  2564
                     (%x::nat.
obua@17652
  2565
                         (All::(nat => bool) => bool)
obua@17652
  2566
                          (%xa::nat.
obua@17652
  2567
                              (op =::bool => bool => bool)
obua@17652
  2568
                               ((op <=::nat => nat => bool)
obua@17652
  2569
                                 ((NUMERAL::nat => nat) x)
obua@17652
  2570
                                 ((NUMERAL::nat => nat) xa))
obua@17652
  2571
                               ((op <=::nat => nat => bool) x xa))))
obua@17652
  2572
                   ((op &::bool => bool => bool)
obua@17652
  2573
                     ((All::(nat => bool) => bool)
obua@17652
  2574
                       (%x::nat.
obua@17652
  2575
                           (op =::bool => bool => bool)
obua@17652
  2576
                            ((op <=::nat => nat => bool) (0::nat) x)
obua@17652
  2577
                            (True::bool)))
obua@17652
  2578
                     ((op &::bool => bool => bool)
obua@17652
  2579
                       ((All::(nat => bool) => bool)
obua@17652
  2580
                         (%x::nat.
obua@17652
  2581
                             (op =::bool => bool => bool)
obua@17652
  2582
                              ((op <=::nat => nat => bool) x (0::nat))
obua@17652
  2583
                              ((op =::nat => nat => bool) x (0::nat))))
obua@17652
  2584
                       ((op &::bool => bool => bool)
obua@17652
  2585
                         ((All::(nat => bool) => bool)
obua@17652
  2586
                           (%x::nat.
obua@17652
  2587
                               (All::(nat => bool) => bool)
obua@17652
  2588
                                (%xa::nat.
obua@17652
  2589
                                    (op =::bool => bool => bool)
obua@17652
  2590
                                     ((op <=::nat => nat => bool)
obua@17652
  2591
 ((NUMERAL::nat => nat) xa) ((NUMERAL::nat => nat) x))
obua@17652
  2592
                                     ((op <=::nat => nat => bool) xa x))))
obua@17652
  2593
                         ((op &::bool => bool => bool)
obua@17652
  2594
                           ((All::(nat => bool) => bool)
obua@17652
  2595
                             (%x::nat.
obua@17652
  2596
                                 (op =::bool => bool => bool)
obua@17652
  2597
                                  ((ODD::nat => bool)
obua@17652
  2598
                                    ((NUMERAL::nat => nat) x))
obua@17652
  2599
                                  ((ODD::nat => bool) x)))
obua@17652
  2600
                           ((op &::bool => bool => bool)
obua@17652
  2601
                             ((All::(nat => bool) => bool)
obua@17652
  2602
                               (%x::nat.
obua@17652
  2603
                                   (op =::bool => bool => bool)
obua@17652
  2604
                                    ((EVEN::nat => bool)
obua@17652
  2605
((NUMERAL::nat => nat) x))
obua@17652
  2606
                                    ((EVEN::nat => bool) x)))
obua@17652
  2607
                             ((op &::bool => bool => bool)
obua@17652
  2608
                               ((Not::bool => bool)
obua@17652
  2609
                                 ((ODD::nat => bool) (0::nat)))
obua@17652
  2610
                               ((EVEN::nat => bool)
obua@17652
  2611
                                 (0::nat))))))))))))))))))))))))))))))))))))"
skalberg@14516
  2612
  by (import numeral numeral_distrib)
skalberg@14516
  2613
skalberg@14516
  2614
lemma numeral_iisuc: "iiSUC ALT_ZERO = NUMERAL_BIT2 ALT_ZERO &
obua@17644
  2615
iiSUC (NUMERAL_BIT1 (n::nat)) = NUMERAL_BIT1 (Suc n) &
skalberg@14516
  2616
iiSUC (NUMERAL_BIT2 n) = NUMERAL_BIT2 (Suc n)"
skalberg@14516
  2617
  by (import numeral numeral_iisuc)
skalberg@14516
  2618
obua@17644
  2619
lemma numeral_add: "ALL (x::nat) xa::nat.
skalberg@14516
  2620
   iZ (ALT_ZERO + x) = x &
skalberg@14516
  2621
   iZ (x + ALT_ZERO) = x &